X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationMatcher.ml;h=a10d0a8bddd92068e77fb4bd598e092a8876c2c1;hb=13494c7c3ca9fde61c7476d0be6109b33c64b3a7;hp=6b1266ec8c41bd62410c3f68f443f1e18af10fa1;hpb=ea7808d83a7d6e03c0e163f0691e268dcd7c2ea4;p=helm.git diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.ml b/helm/ocaml/cic_notation/cicNotationMatcher.ml index 6b1266ec8..a10d0a8bd 100644 --- a/helm/ocaml/cic_notation/cicNotationMatcher.ml +++ b/helm/ocaml/cic_notation/cicNotationMatcher.ml @@ -25,9 +25,9 @@ open Printf -module Pp = CicNotationPp -module Pt = CicNotationPt +module Ast = CicNotationPt module Env = CicNotationEnv +module Pp = CicNotationPp module Util = CicNotationUtil type pattern_id = int @@ -122,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 @@ -138,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 @@ -180,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 @@ -199,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) -> assert false - | 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 @@ -216,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 @@ -237,36 +251,30 @@ 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 -> - prerr_endline ("all magics processed ENV = " ^ Pp.pp_env env) ; - Some env) + (fun 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 -> - 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 = @@ -283,7 +291,7 @@ struct 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 @@ -313,7 +321,7 @@ struct | 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 *) + | 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 @@ -323,26 +331,21 @@ struct | 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 + | 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 -> - 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) + 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 @@ -371,20 +374,23 @@ struct Hashtbl.hash mask, tl let mask_of_appl_pattern = function - | Pt.UriPattern uri -> Uri uri, [] - | 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) @@ -397,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