X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationMatcher.ml;h=b9809335cf491d493c683dd81f69fe842398ac42;hb=b9af9f1c0de6a1735b492f5c793a87a8fce218cc;hp=f8f73e66bf9cba5dd2aadabb71feed686dcdcd91;hpb=bf6144a808a16d4e576e56593bbcd63b8db5fe4c;p=helm.git diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.ml b/helm/ocaml/cic_notation/cicNotationMatcher.ml index f8f73e66b..b9809335c 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 @@ -117,14 +118,26 @@ struct let variable_closure k = (fun matched_terms terms -> - prerr_endline "variable_closure"; match terms with | hd :: tl -> k (hd :: matched_terms) tl | _ -> assert false) + let success_closure ks k = + (fun matched_terms terms -> + match ks 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) + let constructor_closure ks k = (fun matched_terms terms -> - prerr_endline "constructor_closure"; match terms with | t :: tl -> (try @@ -139,8 +152,7 @@ struct if t = [] then k else if are_empty t then - let res = match_cb (matched t) in - (fun matched_terms _ -> res matched_terms) + success_closure (match_cb (matched t)) k else match horizontal_split t with | _, [], _ -> assert false @@ -183,11 +195,12 @@ struct struct type pattern_t = Pt.term type term_t = Pt.term - let classify = function + let rec classify = function + | Pt.AttributedTerm (_, t) -> classify t | Pt.Variable _ -> Variable | Pt.Magic _ | Pt.Layout _ - | Pt.Literal _ -> assert false + | Pt.Literal _ as t -> assert false | _ -> Constructor let tag_of_pattern = CicNotationTag.get_tag let tag_of_term = CicNotationTag.get_tag @@ -203,7 +216,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 @@ -226,9 +239,6 @@ struct | _ -> assert false) pl tl - let decls_of_pattern p = - List.map Env.declaration_of_var (Util.variables_of_term p) - let rec compiler rows = let rows', magic_maps = List.split @@ -245,7 +255,8 @@ struct (fun env -> match m_checker (Env.lookup_term env name) env with | None -> None - | Some env' -> f env')) + | Some env' -> + f env')) (fun env -> Some env) map in @@ -256,12 +267,16 @@ struct let env = env_of_matched pl matched_terms in match checker env with | None -> f matched_terms - | Some env -> Some (env, pid))) + | Some env -> + 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 = - prerr_endline (sprintf "match_cb on %d row(s)" (List.length rows)); let candidates = List.map (fun (pl, pid) -> @@ -271,36 +286,67 @@ struct pid, pl, magichecker magic_map) rows in - magichooser candidates + magichooser candidates in - M.compiler rows match_cb (fun _ -> None) + M.compiler rows' match_cb (fun _ -> None) and compile_magic = function | Pt.Fold (kind, p_base, names, p_rec) -> - let p_rec_decls = decls_of_pattern p_rec in + 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 t_magic = [p_base, 0; p_rec, 1] in - let compiled = compiler t_magic in + 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 -> - 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)) + match compiled term with + | None -> Some none_env (* LUCA: @ env ??? *) + | Some (env', 0) -> Some (List.map Env.opt_binding_some env' @ env) + | _ -> assert false) + + | Pt.If (p_test, p_true, p_false) -> + let compiled_test = compiler [p_test, 0] + and compiled_true = compiler [p_true, 0] + and compiled_false = compiler [p_false, 0] in + (fun term env -> + let branch = + match compiled_test term with + | None -> compiled_false + | Some _ -> compiled_true + in + match branch term with + | None -> None + | Some (env', _) -> Some (env' @ env)) + + | Pt.Fail -> (fun _ _ -> None) + | _ -> assert false end @@ -310,7 +356,7 @@ struct struct type cic_mask_t = Blob - | Uri of string + | Uri of UriManager.uri | Appl of cic_mask_t list let uri_of_term t = CicUtil.uri_of_term (Deannotate.deannotate_term t) @@ -328,7 +374,8 @@ struct Hashtbl.hash mask, tl let mask_of_appl_pattern = function - | Pt.UriPattern s -> Uri s, [] + | Pt.UriPattern uri -> Uri uri, [] + | Pt.ImplicitPattern | Pt.VarPattern _ -> Blob, [] | Pt.ApplPattern pl -> Appl (List.map (fun _ -> Blob) pl), pl @@ -340,21 +387,23 @@ struct type term_t = Cic.annterm let classify = function + | Pt.ImplicitPattern | Pt.VarPattern _ -> Variable - | _ -> Constructor + | Pt.UriPattern _ + | Pt.ApplPattern _ -> Constructor end module M = Matcher (Pattern32) let compiler rows = let match_cb rows = - prerr_endline (sprintf "match_cb on %d row(s)" (List.length rows)); let pl, pid = try List.hd rows with Not_found -> assert false in (fun matched_terms -> let env = List.map2 (fun p t -> match p with + | Pt.ImplicitPattern -> Util.fresh_name (), t | Pt.VarPattern name -> name, t | _ -> assert false) pl matched_terms