X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationMatcher.ml;h=318361c447cbc787d8c1ad22b635b850ff81b37c;hb=5c9e1997848c2f74297a5a243679f4bcb6ae0dc7;hp=204e945fc0c8b700388b30502709afcee1b8631b;hpb=5d5e328a05ed70fcf565aef8f92b7ec87b2740f2;p=helm.git diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.ml b/helm/ocaml/cic_notation/cicNotationMatcher.ml index 204e945fc..318361c44 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 @@ -115,34 +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 _ -> res matched_terms) + 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 @@ -152,7 +166,7 @@ struct t' in let clusters = partition t' tagl in - let ks = + let ksuccs = List.map (fun (tag, cluster) -> let cluster' = @@ -164,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 @@ -179,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) @@ -198,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 = @@ -251,9 +268,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 = @@ -270,39 +292,77 @@ 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 - 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 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 - | Some (env', 0) -> Some (List.map Env.opt_binding_some env' @ env) + | None -> Some none_env (* LUCA: @ 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) + + | 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 +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) @@ -353,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