From 9fce3bebddf47429f6fcab726f11dafbf3295749 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 20 Dec 2006 22:34:35 +0000 Subject: [PATCH] New tactic cases (still to be documented). It is necessary for the declarative language and it is useful anyway. --- .../software/components/grafite/grafiteAst.ml | 1 + .../components/grafite/grafiteAstPp.ml | 2 + .../grafite_engine/grafiteEngine.ml | 3 + .../grafite_parser/grafiteDisambiguate.ml | 3 + .../grafite_parser/grafiteParser.ml | 11 ++- .../components/tactics/primitiveTactics.ml | 94 +++++++++++++++++++ .../components/tactics/primitiveTactics.mli | 4 + helm/software/components/tactics/tactics.ml | 1 + helm/software/components/tactics/tactics.mli | 9 +- helm/software/matita/matita.lang | 1 + 10 files changed, 124 insertions(+), 5 deletions(-) diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 897912915..7a9b7b5ae 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -49,6 +49,7 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic = | ApplyS of loc * 'term * (string * string) list | Assumption of loc | Auto of loc * (string * string) list + | Cases of loc * 'term * 'ident list | 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 840c16351..0530697ad 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -83,6 +83,8 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = String.concat " " (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params) | Assumption _ -> "assumption" + | Cases (_, term, idents) -> sprintf "cases " ^ term_pp term ^ + pp_intros_specs (None, idents) | Change (_, where, with_what) -> sprintf "change %s with %s" (pp_tactic_pattern where) (lazy_term_pp with_what) | Clear (_,ids) -> sprintf "clear %s" (pp_idents ids) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index a747223c7..082eee5f9 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -68,6 +68,9 @@ let tactic_of_ast status ast = | GrafiteAst.Auto (_,params) -> AutoTactic.auto_tac ~params ~dbd:(LibraryDb.instance ()) ~universe:status.GrafiteTypes.universe + | GrafiteAst.Cases (_, what, names) -> + Tactics.cases_intros ~mk_fresh_name_callback:(namer_of names) + 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 9eb1e53fa..42fbabacd 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -130,6 +130,9 @@ let disambiguate_tactic metasenv,GrafiteAst.Assumption loc | GrafiteAst.Auto (loc,params) -> metasenv,GrafiteAst.Auto (loc,params) + | GrafiteAst.Cases (loc, what, idents) -> + let metasenv,what = disambiguate_term context metasenv what in + metasenv,GrafiteAst.Cases (loc, what, 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 1321f613b..b2fb3616f 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -116,11 +116,15 @@ EXTEND | SYMBOL "<" -> `RightToLeft ] ]; int: [ [ num = NUMBER -> int_of_string num ] ]; + intros_names: [ + [ idents = OPT ident_list0 -> + match idents with None -> [] | Some idents -> idents + ] + ]; intros_spec: [ [ OPT [ IDENT "names" ]; num = OPT [ num = int -> num ]; - idents = OPT ident_list0 -> - let idents = match idents with None -> [] | Some idents -> idents in + idents = intros_names -> num, idents ] ]; @@ -138,6 +142,9 @@ EXTEND GrafiteAst.Assumption loc | IDENT "auto"; params = auto_params -> GrafiteAst.Auto (loc,params) + | IDENT "cases"; what = tactic_term; + (num, idents) = intros_spec -> + GrafiteAst.Cases (loc, what, idents) | 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 5f8533916..9f9da0818 100644 --- a/helm/software/components/tactics/primitiveTactics.ml +++ b/helm/software/components/tactics/primitiveTactics.ml @@ -560,6 +560,100 @@ let elim_tac ~term = mk_tactic (elim_tac ~term) ;; +let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term = + let cases_tac ~term (proof, goal) = + let module T = CicTypeChecker in + let module U = UriManager in + let module R = CicReduction in + let module C = Cic in + let (curi,metasenv,proofbo,proofty) = proof in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in + let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in + let termty = CicReduction.whd context termty in + let (termty,metasenv',arguments,fresh_meta) = + TermUtil.saturate_term + (ProofEngineHelpers.new_meta_of_proof proof) metasenv context termty 0 in + let term = if arguments = [] then term else Cic.Appl (term::arguments) in + let uri,exp_named_subst,typeno,args = + match termty with + C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[]) + | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) -> + (uri,exp_named_subst,typeno,args) + | _ -> raise NotAnInductiveTypeToEliminate + in + let paramsno,patterns = + match CicEnvironment.get_obj CicUniv.empty_ugraph uri with + C.InductiveDefinition (tys,_,paramsno,_),_ -> + let _,_,_,cl = List.nth tys typeno in + let rec aux n context t = + match n,CicReduction.whd context t with + 0,C.Prod (name,source,target) -> + let fresh_name = + mk_fresh_name_callback metasenv' context name + (*CSC: WRONG TYPE HERE: I can get a "bad" name*) + ~typ:source + in + C.Lambda (fresh_name,C.Implicit None, + aux 0 (Some (fresh_name,C.Decl source)::context) target) + | n,C.Prod (name,source,target) -> + let fresh_name = + mk_fresh_name_callback metasenv' context name + (*CSC: WRONG TYPE HERE: I can get a "bad" name*) + ~typ:source + in + aux (n-1) (Some (fresh_name,C.Decl source)::context) target + | 0,_ -> C.Implicit None + | _,_ -> assert false + in + paramsno, + List.map (function (_,cty) -> aux paramsno context cty) cl + | _ -> assert false + in + let outtype = + let target = + C.Lambda (C.Name "fixme",C.Implicit None, + ProofEngineReduction.replace_lifting + ~equality:(ProofEngineReduction.alpha_equivalence) + ~what:[CicSubstitution.lift (paramsno+1) term] + ~with_what:[C.Rel (paramsno+1)] + ~where:(CicSubstitution.lift (paramsno+1) ty)) + in + let rec add_lambdas = + function + 0 -> target + | n -> C.Lambda (C.Name "fixme",C.Implicit None,add_lambdas (n-1)) + in + add_lambdas paramsno + in + let term_to_refine = + C.MutCase (uri,typeno,outtype,term,patterns) + in +prerr_endline (CicMetaSubst.ppterm_in_context ~metasenv:metasenv' [] term_to_refine context); + let refined_term,_,metasenv'',_ = + CicRefine.type_of_aux' metasenv' context term_to_refine + CicUniv.empty_ugraph + in + let new_goals = + ProofEngineHelpers.compare_metasenvs + ~oldmetasenv:metasenv ~newmetasenv:metasenv'' + in + let proof' = curi,metasenv'',proofbo,proofty in + let proof'', new_goals' = + apply_tactic (apply_tac ~term:refined_term) (proof',goal) + in + (* The apply_tactic can have closed some of the new_goals *) + let patched_new_goals = + let (_,metasenv''',_,_) = proof'' in + List.filter + (function i -> List.exists (function (j,_,_) -> j=i) metasenv''' + ) new_goals @ new_goals' + in + proof'', patched_new_goals + in + mk_tactic (cases_tac ~term) +;; + + let elim_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) ?depth ?using what = Tacticals.then_ ~start:(elim_tac ~term:what) diff --git a/helm/software/components/tactics/primitiveTactics.mli b/helm/software/components/tactics/primitiveTactics.mli index 6e0c821cc..3e7a48581 100644 --- a/helm/software/components/tactics/primitiveTactics.mli +++ b/helm/software/components/tactics/primitiveTactics.mli @@ -77,6 +77,10 @@ val elim_intros_tac: ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic +val cases_intros_tac: + ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> + Cic.term -> ProofEngineTypes.tactic + (* FG *) (* inserts a hole in the context *) diff --git a/helm/software/components/tactics/tactics.ml b/helm/software/components/tactics/tactics.ml index c34355b8e..82c343085 100644 --- a/helm/software/components/tactics/tactics.ml +++ b/helm/software/components/tactics/tactics.ml @@ -30,6 +30,7 @@ let apply = PrimitiveTactics.apply_tac let applyS = Auto.applyS_tac let assumption = VariousTactics.assumption_tac let auto = AutoTactic.auto_tac +let cases_intros = PrimitiveTactics.cases_intros_tac let change = ReductionTactics.change_tac let clear = ProofEngineStructuralRules.clear let clearbody = ProofEngineStructuralRules.clearbody diff --git a/helm/software/components/tactics/tactics.mli b/helm/software/components/tactics/tactics.mli index d765a8ac0..c0702638f 100644 --- a/helm/software/components/tactics/tactics.mli +++ b/helm/software/components/tactics/tactics.mli @@ -1,4 +1,4 @@ -(* GENERATED FILE, DO NOT EDIT. STAMP:Tue Nov 28 11:13:28 CET 2006 *) +(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Dec 20 23:48:06 CET 2006 *) val absurd : term:Cic.term -> ProofEngineTypes.tactic val apply : term:Cic.term -> ProofEngineTypes.tactic val applyS : @@ -10,6 +10,9 @@ val assumption : ProofEngineTypes.tactic val auto : params:(string * string) list -> dbd:HMysql.dbd -> universe:Universe.universe -> ProofEngineTypes.tactic +val cases_intros : + ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> + Cic.term -> ProofEngineTypes.tactic val change : pattern:ProofEngineTypes.lazy_pattern -> Cic.lazy_term -> ProofEngineTypes.tactic @@ -24,8 +27,8 @@ val decompose : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> ?user_types:(UriManager.uri * int option) list -> ?what:string -> dbd:HMysql.dbd -> ProofEngineTypes.tactic -val demodulate : dbd:HMysql.dbd -> - universe:Universe.universe -> ProofEngineTypes.tactic +val demodulate : + dbd:HMysql.dbd -> universe:Universe.universe -> ProofEngineTypes.tactic val destruct : term:Cic.term -> ProofEngineTypes.tactic val elim_intros : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> diff --git a/helm/software/matita/matita.lang b/helm/software/matita/matita.lang index 02c7045ba..fbb21d6d1 100644 --- a/helm/software/matita/matita.lang +++ b/helm/software/matita/matita.lang @@ -85,6 +85,7 @@ assumption auto paramodulation + cases clear clearbody change -- 2.39.2