From d272210a331d720b08d50b845fa21fa7ec0d4252 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Tue, 2 Mar 2010 14:06:40 +0000 Subject: [PATCH] Added syntax for ninversion tactic (still experimental). --- .../software/components/grafite/grafiteAst.ml | 1 + .../components/grafite/grafiteAstPp.ml | 2 ++ .../grafite_engine/grafiteEngine.ml | 4 ++++ .../grafite_parser/grafiteParser.ml | 2 ++ .../components/ng_tactics/nInversion.ml | 6 ++--- .../components/ng_tactics/nTactics.ml | 23 +++++++++++++++++++ .../components/ng_tactics/nTactics.mli | 4 ++++ 7 files changed, 38 insertions(+), 4 deletions(-) diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index d436977e3..1910e34ac 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -65,6 +65,7 @@ type ntactic = | NGeneralize of loc * npattern | NId of loc | NIntro of loc * string + | NInversion of loc * CicNotationPt.term * npattern | NLApply of loc * CicNotationPt.term | NLetIn of loc * npattern * CicNotationPt.term * string | NReduce of loc * [ `Normalize of bool | `Whd of bool ] * npattern diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index 0db8efc1a..e022c6f33 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -118,6 +118,8 @@ let rec pp_ntactic ~map_unicode_to_tex = assert false ^ " " ^ assert false | NId _ -> "nid" | NIntro (_,n) -> "#" ^ n + | NInversion (_,what,where) -> "ninversion " ^ CicNotationPp.pp_term what ^ + assert false ^ " " ^ assert false | NLApply (_,t) -> "lapply " ^ CicNotationPp.pp_term t | NRewrite (_,dir,n,where) -> "nrewrite " ^ (match dir with `LeftToRight -> ">" | `RightToLeft -> "<") ^ diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 239d30d2d..783d7e6fc 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -805,6 +805,10 @@ let eval_ng_tac tac = NTactics.generalize_tac ~where:(text,prefix_len,where) | GrafiteAst.NId _ -> (fun x -> x) | GrafiteAst.NIntro (_loc,n) -> NTactics.intro_tac n + | GrafiteAst.NInversion (_loc, what, where) -> + NTactics.inversion_tac + ~what:(text,prefix_len,what) + ~where:(text,prefix_len,where) | GrafiteAst.NLApply (_loc, t) -> NTactics.lapply_tac (text,prefix_len,t) | GrafiteAst.NLetIn (_loc,where,what,name) -> NTactics.letin_tac ~where:(text,prefix_len,where) diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 7be30e407..ef354789a 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -268,6 +268,8 @@ EXTEND G.NElim (loc, what, where) | IDENT "ngeneralize"; p=pattern_spec -> G.NGeneralize (loc, p) + | IDENT "ninversion"; what = tactic_term ; where = pattern_spec -> + G.NInversion (loc, what, where) | IDENT "nlapply"; t = tactic_term -> G.NLApply (loc, t) | IDENT "nletin"; name = IDENT ; SYMBOL <:unicode> ; t = tactic_term; where = pattern_spec -> diff --git a/helm/software/components/ng_tactics/nInversion.ml b/helm/software/components/ng_tactics/nInversion.ml index 89a1dd1af..4b4b7246d 100644 --- a/helm/software/components/ng_tactics/nInversion.ml +++ b/helm/software/components/ng_tactics/nInversion.ml @@ -11,8 +11,8 @@ (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) -let pp m = prerr_endline (Lazy.force m);; -(* let pp _ = ();; *) +(* let pp m = prerr_endline (Lazy.force m);;*) +let pp _ = ();; let fresh_name = let i = ref 0 in @@ -130,11 +130,9 @@ let mk_inverter name it leftno ?selection outsort status baseuri = Some (CicNotationPt.Implicit `JustOne)), mk_appl (mk_id "P"::id_rs))))) in - pp (lazy ("and the theorem is: \n" ^ (CicNotationPp.pp_term theorem))); let t = mk_appl ( [mk_id (ind_name ^ "_" ^ suffix)]@ id_ls @ [lambdas] @ List.map mk_id hyplist @ HExtlib.mk_list (CicNotationPt.Implicit `JustOne) (List.length ys) @ [mk_id "Hterm"] ) in - pp (lazy ("and t is: \n" ^ (CicNotationPp.pp_term t))); let status, theorem = GrafiteDisambiguate.disambiguate_nobj status ~baseuri (baseuri ^ name ^ ".def", 0,CicNotationPt.Theorem (`Theorem,name,theorem,Some diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index f5ae3a721..675681540 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -652,3 +652,26 @@ let assert_tac seqs status = ) status ;; +let inversion_tac ~what:(txt,len,what) ~where = + let what = txt, len, Ast.Appl [what; Ast.Implicit `Vector] in + let indtyinfo = ref None in + let sort = ref (NCic.Rel 1) in + atomic_tac (block_tac [ + analyze_indty_tac ~what indtyinfo; + (fun s -> select_tac + ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1)) true s); + sort_of_goal_tac sort; + (fun status -> + let ity = HExtlib.unopt !indtyinfo in + let NReference.Ref (uri, _) = ity.reference in + let name = + NUri.name_of_uri uri ^ "_inv_" ^ + snd (NCicElim.ast_of_sort + (match !sort with NCic.Sort x -> x | _ -> assert false)) + in + let eliminator = + let _,_,w = what in + Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ] + in + exact_tac ("",0,eliminator) status) ]) +;; diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli index 74bbcbcb4..e1a5de895 100644 --- a/helm/software/components/ng_tactics/nTactics.mli +++ b/helm/software/components/ng_tactics/nTactics.mli @@ -95,3 +95,7 @@ val analyze_indty_tac : val find_in_context : 'a -> ('a * 'b) list -> int + +val inversion_tac: + what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> + 's NTacStatus.tactic -- 2.39.2