From ed5c4e15429c37bef0f59dfd7160f6883586ed0f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 19 Jun 2008 16:34:41 +0000 Subject: [PATCH] 1. bug fixed in generalize_pattern: a lazy const_tac should have been relocated. The interesting case is generalize in match a in \vdash % where a occurs in the goal under at least one binder 2. pattern for cases partially implemented. It is now possible to perform a case on the hypotheses as long as the conclusion and hypothesis patterns are trivial (i.e. %) --- .../software/components/grafite/grafiteAst.ml | 3 +- .../components/grafite/grafiteAstPp.ml | 3 +- .../grafite_engine/grafiteEngine.ml | 4 +-- .../grafite_parser/grafiteDisambiguate.ml | 5 ++-- .../grafite_parser/grafiteParser.ml | 7 ++++- .../components/tactics/primitiveTactics.ml | 30 ++++++++++++++++--- .../components/tactics/primitiveTactics.mli | 3 +- helm/software/components/tactics/tactics.mli | 1 + 8 files changed, 44 insertions(+), 12 deletions(-) diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index fc9ea8c5d..2290c4d0b 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -66,7 +66,8 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic = | ApplyS of loc * 'term * 'term auto_params | Assumption of loc | AutoBatch of loc * 'term auto_params - | Cases of loc * 'term * 'ident intros_spec + | Cases of loc * 'term * ('term, 'lazy_term, 'ident) pattern * + 'ident intros_spec | Change of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term | Clear of loc * 'ident list | ClearBody of loc * 'ident diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index 9fa1d05b6..84facde66 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -119,7 +119,8 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp = | AutoBatch (_,params) -> "autobatch " ^ pp_auto_params ~term_pp params | Assumption _ -> "assumption" - | Cases (_, term, specs) -> Printf.sprintf "cases " ^ term_pp term ^ + | Cases (_, term, pattern, specs) -> Printf.sprintf "cases " ^ term_pp term ^ + pp_tactic_pattern pattern ^ pp_intros_specs "names " specs | Change (_, where, with_what) -> Printf.sprintf "change %s with %s" (pp_tactic_pattern where) (lazy_term_pp with_what) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 3746403d9..8813e498b 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -89,9 +89,9 @@ let rec tactic_of_ast status ast = | GrafiteAst.AutoBatch (_,params) -> Tactics.auto ~params ~dbd:(LibraryDb.instance ()) ~universe:status.GrafiteTypes.universe - | GrafiteAst.Cases (_, what, (howmany, names)) -> + | GrafiteAst.Cases (_, what, pattern, (howmany, names)) -> Tactics.cases_intros ?howmany ~mk_fresh_name_callback:(namer_of names) - what + ~pattern what | GrafiteAst.Change (_, pattern, with_what) -> Tactics.change ~pattern with_what | GrafiteAst.Clear (_,id) -> Tactics.clear id diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index 73e71c815..71460415a 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -216,9 +216,10 @@ let rec disambiguate_tactic | GrafiteAst.AutoBatch (loc,params) -> let metasenv, params = disambiguate_auto_params metasenv params in metasenv,GrafiteAst.AutoBatch (loc,params) - | GrafiteAst.Cases (loc, what, idents) -> + | GrafiteAst.Cases (loc, what, pattern, idents) -> let metasenv,what = disambiguate_term context metasenv what in - metasenv,GrafiteAst.Cases (loc, what, idents) + let pattern = disambiguate_pattern pattern in + metasenv,GrafiteAst.Cases (loc, what, pattern, idents) | GrafiteAst.Change (loc, pattern, with_what) -> let with_what = disambiguate_lazy_term with_what in let pattern = disambiguate_pattern pattern in diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 6fcb9dba4..6ce615091 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -177,8 +177,13 @@ EXTEND | IDENT "autobatch"; params = auto_params -> GrafiteAst.AutoBatch (loc,params) | IDENT "cases"; what = tactic_term; + pattern = OPT pattern_spec; specs = intros_spec -> - GrafiteAst.Cases (loc, what, specs) + let pattern = match pattern with + | None -> None, [], Some Ast.UserInput + | Some pattern -> pattern + in + GrafiteAst.Cases (loc, what, pattern, specs) | IDENT "clear"; ids = LIST1 IDENT -> GrafiteAst.Clear (loc, ids) | IDENT "clearbody"; id = IDENT -> diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml index 7b58517f6..db8fe4376 100644 --- a/helm/software/components/tactics/primitiveTactics.ml +++ b/helm/software/components/tactics/primitiveTactics.ml @@ -743,7 +743,7 @@ let generalize_pattern_tac pattern = List.map (fun id -> let rel,_ = ProofEngineHelpers.find_hyp id context in - id,(Some (PET.const_lazy_term rel), [], Some (ProofEngineTypes.hole)) + id,(Some (fun ctx m u -> CicSubstitution.lift (List.length ctx - List.length context) rel,m,u), [], Some (ProofEngineTypes.hole)) ) generalize_hyps in let tactics = List.map @@ -886,14 +886,27 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term = PET.mk_tactic reorder_pattern ;; -let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term = - let cases_tac ~term (proof, goal) = +let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) ?(pattern = PET.conclusion_pattern None) term = + let cases_tac pattern (proof, goal) = let module TC = CicTypeChecker in let module U = UriManager in let module R = CicReduction in let module C = Cic in let (curi,metasenv,_subst, proofbo,proofty, attrs) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in + let pattern = pattern_after_generalize_pattern_tac pattern in + let _cpattern = + match pattern with + | None, [], Some cpattern -> + let rec is_hole = + function + Cic.Implicit (Some `Hole) -> true + | Cic.Prod (Cic.Anonymous,so,tgt) -> is_hole so && is_hole tgt + | _ -> false + in + if not (is_hole cpattern) then + raise (PET.Fail (lazy "not implemented")) + | _ -> raise (PET.Fail (lazy "not implemented")) in let termty,_ = TC.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in let termty = CicReduction.whd context termty in let (termty,metasenv',arguments,fresh_meta) = @@ -1016,7 +1029,16 @@ let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenera in proof'', patched_new_goals in - PET.mk_tactic (cases_tac ~term) + let reorder_pattern ((proof, goal) as status) = + let _,metasenv,_,_,_,_ = proof in + let conjecture = CicUtil.lookup_meta goal metasenv in + let _,context,_ = conjecture in + let pattern = ProofEngineHelpers.sort_pattern_hyps context pattern in + PET.apply_tactic + (Tacticals.then_ ~start:(generalize_pattern_tac pattern) + ~continuation:(PET.mk_tactic (cases_tac pattern))) status + in + PET.mk_tactic reorder_pattern ;; diff --git a/helm/software/components/tactics/primitiveTactics.mli b/helm/software/components/tactics/primitiveTactics.mli index 95ba654f5..0ca91fe2c 100644 --- a/helm/software/components/tactics/primitiveTactics.mli +++ b/helm/software/components/tactics/primitiveTactics.mli @@ -93,7 +93,8 @@ val elim_intros_tac: val cases_intros_tac: ?howmany:int -> ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> - Cic.term -> ProofEngineTypes.tactic + ?pattern:ProofEngineTypes.lazy_pattern -> Cic.term -> + ProofEngineTypes.tactic (* FG *) diff --git a/helm/software/components/tactics/tactics.mli b/helm/software/components/tactics/tactics.mli index 08b32e571..a0aa32b3c 100644 --- a/helm/software/components/tactics/tactics.mli +++ b/helm/software/components/tactics/tactics.mli @@ -14,6 +14,7 @@ val auto : val cases_intros : ?howmany:int -> ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> + ?pattern:ProofEngineTypes.lazy_pattern -> Cic.term -> ProofEngineTypes.tactic val change : ?with_cast:bool -> -- 2.39.2