From ee242468b221c64b25c99b52110fe00380f4eebe Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 9 Apr 2009 16:16:26 +0000 Subject: [PATCH] added letin, still broken --- .../software/components/grafite/grafiteAst.ml | 1 + .../grafite_engine/grafiteEngine.ml | 3 +++ .../grafite_parser/grafiteParser.ml | 3 +++ .../components/ng_tactics/nTactics.ml | 19 +++++++++++++++++++ .../components/ng_tactics/nTactics.mli | 5 +++++ 5 files changed, 31 insertions(+) diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 763911b79..062f2c0d2 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -59,6 +59,7 @@ type ntactic = | NGeneralize of loc * npattern | NId of loc | NIntro of loc * string + | NLetIn of loc * npattern * CicNotationPt.term * string | NRewrite of loc * direction * CicNotationPt.term * npattern type ('term, 'lazy_term, 'reduction, 'ident) tactic = diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 2099bf06a..ebf0d8a63 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -604,6 +604,9 @@ let eval_ng_tac (text, prefix_len, tac) = NTactics.generalize_tac ~where:(text,prefix_len,where) | GrafiteAst.NId _ -> (fun x -> x) | GrafiteAst.NIntro (_loc,n) -> NTactics.intro_tac n + | GrafiteAst.NLetIn (_loc,where,what,name) -> + NTactics.letin_tac ~where:(text,prefix_len,where) + ~what:(text,prefix_len,what) name | GrafiteAst.NRewrite (_loc,dir,what,where) -> NTactics.rewrite_tac ~dir ~what:(text,prefix_len,what) ~where:(text,prefix_len,where) diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index dacdc28bd..56da062e8 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -190,6 +190,9 @@ EXTEND GrafiteAst.NElim (loc, what, where) | IDENT "ngeneralize"; p=pattern_spec -> GrafiteAst.NGeneralize (loc, p) + | IDENT "nletin"; name = IDENT ; SYMBOL <:unicode> ; t = tactic_term; + where = pattern_spec -> + GrafiteAst.NLetIn (loc,where,t,name) | IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec -> GrafiteAst.NRewrite (loc, dir, what, where) | IDENT "nwhd"; delta = OPT [ IDENT "nodelta" -> () ]; diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index a6ae87be7..30ccaf86d 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -363,6 +363,25 @@ let change_tac ~where ~with_what = select0_tac ~where ~job:(`ChangeWith change) ;; +let letin_tac ~where:(_,_,(m,hyp,gp)) ~what:(_,_,w) name = + assert(m = None); + let where = Some w, [], + match gp with + | None -> Some Ast.Implicit + | Some where -> + Some + (List.fold_left + (fun t _ -> + Ast.Binder(`Pi,(Ast.Ident("_",None),Some Ast.UserInput),t)) + where hyp) + in + block_tac [ + generalize0_tac (List.map (fun (name,_) -> Ast.Ident (name,None)) hyp); + exact_tac ("",0,Ast.LetIn((Ast.Ident (name,None),None),w,Ast.Implicit)); + change_tac ~where:("",0,where) ~with_what:("",0,Ast.Ident (name,None)) + ] +;; + let apply_tac = exact_tac;; type indtyinfo = { diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli index 9eeebfe7f..0605b993f 100644 --- a/helm/software/components/ng_tactics/nTactics.mli +++ b/helm/software/components/ng_tactics/nTactics.mli @@ -44,3 +44,8 @@ val generalize_tac : where:NTacStatus.tactic_pattern -> NTacStatus.tactic val eval_tac: reduction:[ `Whd of bool ] -> where:NTacStatus.tactic_pattern -> NTacStatus.tactic +val letin_tac: + where:NTacStatus.tactic_pattern -> + what: NTacStatus.tactic_term -> + string -> NTacStatus.tactic + -- 2.39.2