X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationMatcher.ml;h=a10d0a8bddd92068e77fb4bd598e092a8876c2c1;hb=13494c7c3ca9fde61c7476d0be6109b33c64b3a7;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..a10d0a8bd 100644 --- a/helm/ocaml/cic_notation/cicNotationMatcher.ml +++ b/helm/ocaml/cic_notation/cicNotationMatcher.ml @@ -25,8 +25,9 @@ open Printf -module Pt = CicNotationPt +module Ast = CicNotationPt module Env = CicNotationEnv +module Pp = CicNotationPp module Util = CicNotationUtil type pattern_id = int @@ -121,6 +122,20 @@ struct | 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 -> match terms with @@ -137,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 @@ -179,13 +193,14 @@ module Matcher21 = struct module Pattern21 = struct - type pattern_t = Pt.term - type term_t = Pt.term - let classify = function - | Pt.Variable _ -> Variable - | Pt.Magic _ - | Pt.Layout _ - | Pt.Literal _ as t -> assert false + type pattern_t = Ast.term + type term_t = Ast.term + let rec classify = function + | Ast.AttributedTerm (_, t) -> classify t + | Ast.Variable _ -> Variable + | Ast.Magic _ + | Ast.Layout _ + | Ast.Literal _ as t -> assert false | _ -> Constructor let tag_of_pattern = CicNotationTag.get_tag let tag_of_term = CicNotationTag.get_tag @@ -198,14 +213,14 @@ struct let add_magic m = let name = Util.fresh_name () in magic_map := (name, m) :: !magic_map; - Pt.Variable (Pt.TermVar name) + Ast.Variable (Ast.TermVar name) in let rec aux = function - | Pt.AttributedTerm (_, t) -> aux t - | Pt.Literal _ - | Pt.Layout _ -> assert false - | Pt.Variable v -> Pt.Variable v - | Pt.Magic m -> add_magic m + | Ast.AttributedTerm (_, t) -> assert false + | Ast.Literal _ + | Ast.Layout _ -> assert false + | Ast.Variable v -> Ast.Variable v + | Ast.Magic m -> add_magic m | t -> Util.visit_ast aux t in let term' = aux term in @@ -215,11 +230,11 @@ struct List.map2 (fun p t -> match p, t with - Pt.Variable (Pt.TermVar name), _ -> + Ast.Variable (Ast.TermVar name), _ -> name, (Env.TermType, Env.TermValue t) - | Pt.Variable (Pt.NumVar name), (Pt.Num (s, _)) -> + | Ast.Variable (Ast.NumVar name), (Ast.Num (s, _)) -> name, (Env.NumType, Env.NumValue s) - | Pt.Variable (Pt.IdentVar name), (Pt.Ident (s, None)) -> + | Ast.Variable (Ast.IdentVar name), (Ast.Ident (s, None)) -> name, (Env.StringType, Env.StringValue s) | _ -> assert false) pl tl @@ -240,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 @@ -251,9 +267,14 @@ 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 = let candidates = @@ -265,44 +286,67 @@ 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) -> + | 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 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)) - | Pt.Default (p_some, p_none) -> (* p_none can't bound names *) + 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!!! *) + + | Ast.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) + + | Ast.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)) + + | Ast.Fail -> (fun _ _ -> None) + | _ -> assert false end @@ -330,20 +374,23 @@ struct Hashtbl.hash mask, tl let mask_of_appl_pattern = function - | Pt.UriPattern s -> Uri (UriManager.uri_of_string s), [] - | Pt.VarPattern _ -> Blob, [] - | Pt.ApplPattern pl -> Appl (List.map (fun _ -> Blob) pl), pl + | Ast.UriPattern uri -> Uri uri, [] + | Ast.ImplicitPattern + | Ast.VarPattern _ -> Blob, [] + | Ast.ApplPattern pl -> Appl (List.map (fun _ -> Blob) pl), pl let tag_of_pattern p = let mask, pl = mask_of_appl_pattern p in Hashtbl.hash mask, pl - type pattern_t = Pt.cic_appl_pattern + type pattern_t = Ast.cic_appl_pattern type term_t = Cic.annterm let classify = function - | Pt.VarPattern _ -> Variable - | _ -> Constructor + | Ast.ImplicitPattern + | Ast.VarPattern _ -> Variable + | Ast.UriPattern _ + | Ast.ApplPattern _ -> Constructor end module M = Matcher (Pattern32) @@ -356,7 +403,8 @@ struct List.map2 (fun p t -> match p with - | Pt.VarPattern name -> name, t + | Ast.ImplicitPattern -> Util.fresh_name (), t + | Ast.VarPattern name -> name, t | _ -> assert false) pl matched_terms in