open Printf
+module Pp = CicNotationPp
module Pt = CicNotationPt
module Env = CicNotationEnv
module Util = CicNotationUtil
let magichecker map =
List.fold_left
(fun f (name, m) ->
+ prerr_endline ("compiling magichecker for " ^ name) ;
let m_checker = compile_magic m in
(fun env ->
match m_checker (Env.lookup_term env name) env with
| None -> None
- | Some env' -> f env'))
- (fun env -> Some env)
+ | Some env' ->
+ f env'))
+ (fun env ->
+ prerr_endline ("all magics processed ENV = " ^ Pp.pp_env env) ;
+ Some env)
map
in
let magichooser candidates =
List.fold_left
(fun f (pid, pl, checker) ->
+ List.iter (fun p -> prerr_endline ("P = " ^ Pp.pp_term p)) pl ;
(fun matched_terms ->
let env = env_of_matched pl matched_terms in
match checker env with
| None -> f matched_terms
- | Some env -> Some (env, pid)))
+ | Some env ->
+ prerr_endline (String.concat " / " (List.map Pp.pp_term pl)) ;
+ prerr_endline ("magichoose found a match for " ^ Pp.pp_env env ^ " " ^ string_of_int pid) ;
+ let magic_map =
+ try List.assoc pid magic_maps with Not_found -> assert false
+ in
+ let env' = Env.remove_names env (List.map fst magic_map) in
+ Some (env', pid)))
(fun _ -> None)
candidates
in
pid, pl, magichecker magic_map)
rows
in
- magichooser candidates
+ magichooser candidates
in
M.compiler rows' match_cb (fun _ -> None)
and compile_magic = function
| Pt.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 compiled = compiler [p_base, 0; p_rec, 1] in
- (fun term env ->
- let rec aux term =
- match compiled term with
- | None -> None
- | Some (env', 0) -> Some (env', [])
- | Some (env', 1) ->
- begin
- let acc = Env.lookup_term env' acc_name in
- let env'' = Env.remove env' acc_name in
- match aux acc with
- | None -> None
- | Some (base_env, rec_envl) ->
- Some (base_env, env'' :: rec_envl )
- end
- | _ -> assert false
- in
- match aux term with
- | None -> None
- | Some (base_env, rec_envl) ->
- Some (base_env @ Env.coalesce_env p_rec_decls rec_envl))
+ let compiled_base = compiler [p_base, 0]
+ and compiled_rec = compiler [p_rec, 0] in
+ (fun term env ->
+ let aux_base term =
+ match compiled_base term with
+ | None -> None
+ | Some (env', _) -> Some (env', [])
+ in
+ let rec aux term =
+ match compiled_rec term with
+ | None -> aux_base term
+ | Some (env', _) ->
+ begin
+ let acc = Env.lookup_term env' acc_name in
+ let env'' = Env.remove_name env' acc_name in
+ match aux acc with
+ | None -> aux_base term
+ | Some (base_env, rec_envl) ->
+ Some (base_env, env'' :: rec_envl)
+ end
+ in
+ match aux term with
+ | None -> None
+ | Some (base_env, rec_envl) ->
+ Some (base_env @ Env.coalesce_env p_rec_decls rec_envl @ env)) (* @ env LUCA!!! *)
+
| Pt.Default (p_some, p_none) -> (* p_none can't bound names *)
let p_some_decls = Env.declarations_of_term p_some in
let none_env = List.map Env.opt_binding_of_name p_some_decls in
let compiled = compiler [p_some, 0] in
(fun term env ->
match compiled term with
- | None -> Some none_env
+ | None -> Some none_env (* LUCA: @ env ??? *)
| Some (env', 0) -> Some (List.map Env.opt_binding_some env' @ env)
| _ -> assert false)
+
+ | Pt.If (guard, p) ->
+ prerr_endline ("guard = " ^ CicNotationPp.pp_term guard) ;
+ prerr_endline ("p = " ^ CicNotationPp.pp_term p) ;
+ let compiled_guard = compiler [guard, 0]
+ and compiled_p = compiler [p, 0] in
+ (fun term env ->
+ prerr_endline "GUARDIA?" ;
+ match compiled_guard term with
+ | None ->
+ prerr_endline "SONO CAZZI H2SO4" ;
+ None
+ | Some _ ->
+ begin
+ prerr_endline "OKKKKKKKKKKKKKK" ;
+ match compiled_p term with
+ | None -> None
+ | Some (env', _) ->
+ prerr_endline "guardia ok" ;
+ Some (env' @ env)
+ end)
+
| _ -> assert false
end
| Ast.AttributedTerm (_, t) -> subst env t
| Ast.Variable var ->
let name, expected_ty = CicNotationEnv.declaration_of_var var in
+ prerr_endline ("searching for " ^ name);
let ty, value =
try
List.assoc name env
let rec pp_value = function
| CicNotationEnv.NumValue _ as v -> v
| CicNotationEnv.StringValue _ as v -> v
+(* | CicNotationEnv.TermValue t when t == term -> CicNotationEnv.TermValue (pp_ast0 t pp_ast1) *)
| CicNotationEnv.TermValue t -> CicNotationEnv.TermValue (pp_ast1 t)
| CicNotationEnv.OptValue None as v -> v
| CicNotationEnv.OptValue (Some v) ->
match term with
| Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, pp_ast1 t)
| _ ->
- (match (get_compiled21 ()) term with
- | None -> pp_ast0 term pp_ast1
- | Some (env, pid) ->
- let precedence, associativity, l1 =
- try
- Hashtbl.find level1_patterns21 pid
- with Not_found -> assert false
- in
- Ast.AttributedTerm (`Level (precedence, associativity),
- (instantiate21 (ast_env_of_env env) l1)))
+ begin
+ match (get_compiled21 ()) term with
+ | None -> pp_ast0 term pp_ast1
+ | Some (env, pid) ->
+ let precedence, associativity, l1 =
+ try
+ Hashtbl.find level1_patterns21 pid
+ with Not_found -> assert false
+ in
+ prerr_endline ("IN " ^ CicNotationPp.pp_term term);
+ (* LUCA: il termine legato e' lo stesso termine di partenza per cui si innesca il loop infinito *)
+ let res = Ast.AttributedTerm (`Level (precedence, associativity),
+ (instantiate21 (ast_env_of_env env) l1))
+ in
+ prerr_endline "OUT";
+ res
+ end
+
let instantiate32 term_info env symbol args =
let rec instantiate_arg = function
projects / helm.git / commitdiff