X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationMatcher.ml;h=318361c447cbc787d8c1ad22b635b850ff81b37c;hb=5c9e1997848c2f74297a5a243679f4bcb6ae0dc7;hp=1a0c024104feaaab9f730ed16c5101c3f72ce965;hpb=fa143d13b855aa48a11f3230a139f39ce2df0984;p=helm.git diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.ml b/helm/ocaml/cic_notation/cicNotationMatcher.ml index 1a0c02410..318361c44 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 @@ -116,45 +116,47 @@ struct | _ -> assert false) t - let variable_closure k = + let variable_closure ksucc = (fun matched_terms terms -> +(* prerr_endline "variable_closure"; *) match terms with - | hd :: tl -> k (hd :: matched_terms) tl + | hd :: tl -> ksucc (hd :: matched_terms) tl | _ -> assert false) - let constructor_closure ks k = + let success_closure ksucc = + (fun matched_terms terms -> +(* prerr_endline "success_closure"; *) + ksucc matched_terms) + + let constructor_closure ksuccs = (fun matched_terms terms -> +(* prerr_endline "constructor_closure"; *) match terms with | t :: tl -> (try let tag, subterms = P.tag_of_term t in - let k' = List.assoc tag ks in + let k' = List.assoc tag ksuccs in k' matched_terms (subterms @ tl) - with Not_found -> k matched_terms terms) + with Not_found -> None) | [] -> assert false) + let backtrack_closure ksucc kfail = + (fun matched_terms terms -> +(* prerr_endline "backtrack_closure"; *) + match ksucc matched_terms terms with + | Some x -> Some x + | None -> kfail matched_terms terms) + let compiler rows match_cb fail_k = - let rec aux t k = + let rec aux t = if t = [] then - k + (fun _ _ -> fail_k ()) else if are_empty t then - let res = match_cb (matched t) in - (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) + success_closure (match_cb (matched t)) else match horizontal_split t with | _, [], _ -> assert false - | Variable, t', [] -> variable_closure (aux (vertical_split t') k) + | Variable, t', [] -> variable_closure (aux (vertical_split t')) | Constructor, t', [] -> let tagl = List.map @@ -164,7 +166,7 @@ struct t' in let clusters = partition t' tagl in - let ks = + let ksuccs = List.map (fun (tag, cluster) -> let cluster' = @@ -176,14 +178,14 @@ struct | _ -> assert false) cluster in - tag, aux cluster' k) + tag, aux cluster') clusters in - constructor_closure ks k - | _, t', t'' -> aux t' (aux t'' k) + constructor_closure ksuccs + | _, t', t'' -> backtrack_closure (aux t') (aux t'') in let t = List.map (fun (p, pid) -> [], [p], pid) rows in - let matcher = aux t (fun _ _ -> fail_k ()) in + let matcher = aux t in (fun term -> matcher [] [term]) end @@ -191,16 +193,17 @@ 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 + let tag_of_term t = CicNotationTag.get_tag t end module M = Matcher (Pattern21) @@ -210,31 +213,33 @@ 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 term', !magic_map let env_of_matched pl tl = - List.map2 - (fun p t -> - match p, t with - Pt.Variable (Pt.TermVar name), _ -> - name, (Env.TermType, Env.TermValue t) - | Pt.Variable (Pt.NumVar name), (Pt.Num (s, _)) -> - name, (Env.NumType, Env.NumValue s) - | Pt.Variable (Pt.IdentVar name), (Pt.Ident (s, None)) -> - name, (Env.StringType, Env.StringValue s) - | _ -> assert false) - pl tl + try + List.map2 + (fun p t -> + match p, t with + Ast.Variable (Ast.TermVar name), _ -> + name, (Env.TermType, Env.TermValue t) + | Ast.Variable (Ast.NumVar name), (Ast.Num (s, _)) -> + name, (Env.NumType, Env.NumValue s) + | Ast.Variable (Ast.IdentVar name), (Ast.Ident (s, None)) -> + name, (Env.StringType, Env.StringValue s) + | _ -> assert false) + pl tl + with Invalid_argument _ -> assert false let rec compiler rows = let rows', magic_maps = @@ -248,36 +253,29 @@ 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) + | Some env' -> f 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 = @@ -289,12 +287,12 @@ 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 @@ -324,33 +322,46 @@ 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 p_none_decls = Env.declarations_of_term p_none in + let p_opt_decls = + List.filter + (fun decl -> not (List.mem decl p_none_decls)) + p_some_decls + in + let none_env = List.map Env.opt_binding_of_name p_opt_decls in let compiled = compiler [p_some, 0] in (fun term env -> match compiled term with | None -> Some none_env (* LUCA: @ env ??? *) - | Some (env', 0) -> Some (List.map Env.opt_binding_some env' @ env) + | Some (env', 0) -> + let env' = + List.map + (fun (name, (ty, v)) as binding -> + if List.exists (fun (name', _) -> name = name') p_opt_decls + then Env.opt_binding_some binding + else binding) + env' + in + 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 -> None - | Some _ -> - begin - 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 @@ -379,20 +390,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) @@ -402,12 +416,15 @@ struct 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.VarPattern name -> name, t - | _ -> assert false) - pl matched_terms + try + List.map2 + (fun p t -> + match p with + | Ast.ImplicitPattern -> Util.fresh_name (), t + | Ast.VarPattern name -> name, t + | _ -> assert false) + pl matched_terms + with Invalid_argument _ -> assert false in Some (env, pid)) in