(* $Id$ *)
-open Printf
-
module Ast = NotationPt
module Env = NotationEnv
-module Pp = NotationPp
module Util = NotationUtil
let get_tag term0 =
| _ -> PatternMatcher.Constructor
let tag_of_pattern = get_tag
let tag_of_term t = get_tag t
- let string_of_term = NotationPp.pp_term
- let string_of_pattern = NotationPp.pp_term
+
+ (* Debugging only *)
+ (*CSC: new NCicPp.status is the best I can do now *)
+ let string_of_term = NotationPp.pp_term (new NCicPp.status)
+ let string_of_pattern = NotationPp.pp_term (new NCicPp.status)
end
module M = PatternMatcher.Matcher (Pattern21)
Ast.Variable (Ast.TermVar (name,Ast.Level 0))
in
let rec aux = function
- | Ast.AttributedTerm (_, t) -> assert false
+ | Ast.AttributedTerm (_, _t) -> assert false
| Ast.Literal _
| Ast.Layout _ -> assert false
| Ast.Variable v -> Ast.Variable v
| Ast.Variable (Ast.NumVar name), (Ast.Num (s, _)) ->
name, (Env.NumType, Env.NumValue s)
| Ast.Variable (Ast.IdentVar name), (Ast.Ident (s, None)) ->
- name, (Env.StringType, Env.StringValue s)
- | _ -> assert false)
+ name, (Env.StringType, Env.StringValue (Env.Ident s))
+ | _ -> assert false (* activate the DEBUGGING CODE below *))
pl tl
with Invalid_argument _ -> assert false
in
magichooser candidates
in
+(* DEBUGGING CODE
+fun input ->
+let (fst,_)::_ = rows in
+prerr_endline ("RIGA: " ^ NotationPp.pp_term (new NCicPp.status) fst);
+prerr_endline ("CONTRO: " ^ NotationPp.pp_term (new NCicPp.status) input);
+*)
M.compiler rows' match_cb (fun _ -> None)
+(* DEBUGGING CODE
+input
+*)
and compile_magic = function
- | Ast.Fold (kind, p_base, names, p_rec) ->
+ | Ast.Fold (_kind, p_base, names, p_rec) ->
let p_rec_decls = Env.declarations_of_term p_rec in
(* LUCA: p_rec_decls should not contain "names" *)
let acc_name = try List.hd names with Failure _ -> assert false in
let rec aux term =
match compiled_rec term with
| None -> aux_base term
- | Some (env', ctors', _) ->
+ | Some (env', _ctors', _) ->
begin
let acc = Env.lookup_term env' acc_name in
let env'' = Env.remove_name env' acc_name in
| Some (env', ctors', 0) ->
let env' =
List.map
- (fun (name, (ty, v)) as binding ->
+ (fun (name, (_ty, _v)) as binding ->
if List.exists (fun (name', _) -> name = name') p_opt_decls
then Env.opt_binding_some binding
else binding)