X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationMatcher.ml;h=7b85b96b5758845f8afff270b576e920274011ea;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=318361c447cbc787d8c1ad22b635b850ff81b37c;hpb=6ab174a7f866b87921e66fcc3fdd137a01456c78;p=helm.git diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.ml b/helm/ocaml/cic_notation/cicNotationMatcher.ml index 318361c44..7b85b96b5 100644 --- a/helm/ocaml/cic_notation/cicNotationMatcher.ml +++ b/helm/ocaml/cic_notation/cicNotationMatcher.ml @@ -55,6 +55,8 @@ sig val classify : pattern_t -> pattern_kind val tag_of_pattern : pattern_t -> tag_t * pattern_t list val tag_of_term : term_t -> tag_t * term_t list + val string_of_term: term_t -> string + val string_of_pattern: pattern_t -> string end module Matcher (P: PATTERN) = @@ -117,40 +119,43 @@ struct t let variable_closure ksucc = - (fun matched_terms terms -> + (fun matched_terms constructors terms -> (* prerr_endline "variable_closure"; *) match terms with - | hd :: tl -> ksucc (hd :: matched_terms) tl + | hd :: tl -> ksucc (hd :: matched_terms) constructors tl | _ -> assert false) let success_closure ksucc = - (fun matched_terms terms -> + (fun matched_terms constructors terms -> (* prerr_endline "success_closure"; *) - ksucc matched_terms) + ksucc matched_terms constructors) let constructor_closure ksuccs = - (fun matched_terms terms -> + (fun matched_terms constructors terms -> (* prerr_endline "constructor_closure"; *) match terms with | t :: tl -> (try let tag, subterms = P.tag_of_term t in + let constructors' = + if subterms = [] then t :: constructors else constructors + in let k' = List.assoc tag ksuccs in - k' matched_terms (subterms @ tl) + k' matched_terms constructors' (subterms @ tl) with Not_found -> None) | [] -> assert false) let backtrack_closure ksucc kfail = - (fun matched_terms terms -> + (fun matched_terms constructors terms -> (* prerr_endline "backtrack_closure"; *) - match ksucc matched_terms terms with + match ksucc matched_terms constructors terms with | Some x -> Some x - | None -> kfail matched_terms terms) + | None -> kfail matched_terms constructors terms) let compiler rows match_cb fail_k = let rec aux t = if t = [] then - (fun _ _ -> fail_k ()) + (fun _ _ _ -> fail_k ()) else if are_empty t then success_closure (match_cb (matched t)) else @@ -186,7 +191,7 @@ struct in let t = List.map (fun (p, pid) -> [], [p], pid) rows in let matcher = aux t in - (fun term -> matcher [] [term]) + (fun term -> matcher [] [] [term]) end module Matcher21 = @@ -204,6 +209,8 @@ struct | _ -> Constructor let tag_of_pattern = CicNotationTag.get_tag let tag_of_term t = CicNotationTag.get_tag t + let string_of_term = CicNotationPp.pp_term + let string_of_pattern = CicNotationPp.pp_term end module M = Matcher (Pattern21) @@ -254,27 +261,27 @@ struct List.fold_left (fun f (name, m) -> let m_checker = compile_magic m in - (fun env -> - match m_checker (Env.lookup_term env name) env with + (fun env ctors -> + match m_checker (Env.lookup_term env name) env ctors with | None -> None - | Some env' -> f env')) - (fun env -> Some env) + | Some (env, ctors) -> f env ctors)) + (fun env ctors -> Some (env, ctors)) map in let magichooser candidates = List.fold_left (fun f (pid, pl, checker) -> - (fun matched_terms -> + (fun matched_terms constructors -> let env = env_of_matched pl matched_terms in - match checker env with - | None -> f matched_terms - | Some env -> + match checker env constructors with + | None -> f matched_terms constructors + | Some (env, ctors') -> 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) + Some (env', ctors', pid))) + (fun _ _ -> None) (List.rev candidates) in let match_cb rows = @@ -298,29 +305,34 @@ struct let acc_name = try List.hd names with Failure _ -> assert false in let compiled_base = compiler [p_base, 0] and compiled_rec = compiler [p_rec, 0] in - (fun term env -> + (fun term env ctors -> let aux_base term = match compiled_base term with | None -> None - | Some (env', _) -> Some (env', []) + | Some (env', ctors', _) -> Some (env', ctors', []) in let rec aux term = match compiled_rec term with | None -> aux_base term - | Some (env', _) -> + | Some (env', ctors', _) -> 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) + | Some (base_env, ctors', rec_envl) -> + let ctors'' = ctors' @ ctors in + Some (base_env, ctors'',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!!! *) + | Some (base_env, ctors, rec_envl) -> + let env' = + base_env @ Env.coalesce_env p_rec_decls rec_envl @ env + (* @ env LUCA!!! *) + in + Some (env', ctors)) | Ast.Default (p_some, p_none) -> (* p_none can't bound names *) let p_some_decls = Env.declarations_of_term p_some in @@ -332,10 +344,10 @@ struct 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 -> + (fun term env ctors -> match compiled term with - | None -> Some none_env (* LUCA: @ env ??? *) - | Some (env', 0) -> + | None -> Some (none_env, ctors) (* LUCA: @ env ??? *) + | Some (env', ctors', 0) -> let env' = List.map (fun (name, (ty, v)) as binding -> @@ -344,24 +356,24 @@ struct else binding) env' in - Some (env' @ env) + Some (env' @ env, ctors' @ ctors) | _ -> 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 -> + (fun term env ctors -> let branch = match compiled_test term with - | None -> compiled_false - | Some _ -> compiled_true + | None -> compiled_false + | Some _ -> compiled_true in - match branch term with - | None -> None - | Some (env', _) -> Some (env' @ env)) + match branch term with + | None -> None + | Some (env', ctors', _) -> Some (env' @ env, ctors' @ ctors)) - | Ast.Fail -> (fun _ _ -> None) + | Ast.Fail -> (fun _ _ _ -> None) | _ -> assert false end @@ -402,6 +414,9 @@ struct type pattern_t = Ast.cic_appl_pattern type term_t = Cic.annterm + let string_of_pattern = GrafiteAstPp.pp_cic_appl_pattern + let string_of_term t = CicPp.ppterm (Deannotate.deannotate_term t) + let classify = function | Ast.ImplicitPattern | Ast.VarPattern _ -> Variable @@ -414,7 +429,7 @@ struct let compiler rows = let match_cb rows = let pl, pid = try List.hd rows with Not_found -> assert false in - (fun matched_terms -> + (fun matched_terms constructors -> let env = try List.map2 @@ -426,7 +441,7 @@ struct pl matched_terms with Invalid_argument _ -> assert false in - Some (env, pid)) + Some (env, constructors, pid)) in M.compiler rows match_cb (fun () -> None) end