X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationMatcher.ml;h=39c82b7dadb66a1e095969c133ff2d9ab23d5078;hb=26cce624c98e795521078794c748758798031704;hp=1c1532548589c22faee9f03d5a83d0c161cce4ee;hpb=3d63cb9ed38f05c679fc3284a5b3bb4d92e52296;p=helm.git diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.ml b/helm/ocaml/cic_notation/cicNotationMatcher.ml index 1c1532548..39c82b7da 100644 --- a/helm/ocaml/cic_notation/cicNotationMatcher.ml +++ b/helm/ocaml/cic_notation/cicNotationMatcher.ml @@ -25,6 +25,7 @@ open Printf +module Pp = CicNotationPp module Pt = CicNotationPt module Env = CicNotationEnv module Util = CicNotationUtil @@ -138,7 +139,18 @@ struct k else if are_empty t then let res = match_cb (matched t) in - (fun matched_terms _ -> res matched_terms) + (fun matched_terms terms -> + match res matched_terms with + None -> + begin + (* the match has failed, we rollback the last matched term + * into the unmatched ones and call the failure continuation + *) + match matched_terms with + hd :: tl -> k tl (hd :: terms) + | _ -> assert false + end + | Some v -> Some v) else match horizontal_split t with | _, [], _ -> assert false @@ -201,7 +213,7 @@ struct Pt.Variable (Pt.TermVar name) in let rec aux = function - | Pt.AttributedTerm (_, t) -> aux t + | Pt.AttributedTerm (_, t) -> assert false | Pt.Literal _ | Pt.Layout _ -> assert false | Pt.Variable v -> Pt.Variable v @@ -236,24 +248,36 @@ struct 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 + (List.rev candidates) in let match_cb rows = let candidates = @@ -265,44 +289,79 @@ struct 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) -> + let compiled_guard = compiler [guard, 0] + and compiled_p = compiler [p, 0] in + (fun term env -> + match compiled_guard term with + | None -> None + | Some _ -> + begin + match compiled_p term with + | None -> None + | Some (env', _) -> + Some (env' @ env) + end) + + | Pt.Unless (guard, p) -> + let compiled_guard = compiler [guard, 0] + and compiled_p = compiler [p, 0] in + (fun term env -> + match compiled_guard term with + | None -> + begin + match compiled_p term with + | None -> None + | Some (env', _) -> + Some (env' @ env) + end + | Some _ -> None) + | _ -> assert false end @@ -330,7 +389,7 @@ struct Hashtbl.hash mask, tl let mask_of_appl_pattern = function - | Pt.UriPattern s -> Uri (UriManager.uri_of_string s), [] + | Pt.UriPattern uri -> Uri uri, [] | Pt.VarPattern _ -> Blob, [] | Pt.ApplPattern pl -> Appl (List.map (fun _ -> Blob) pl), pl