added letin, still broken

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 763911b79ea245ae572da11306a1008d5d5d7695..062f2c0d216a0d16a7363dae3f8464031c14343b 100644 (file)
--- 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 2099bf06a8ed10987547cc8b7afa4ddddcc49cd3..ebf0d8a63b8497de710e1b55756cc7f3f79ae4f8 100644 (file)
--- 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 dacdc28bdb936f9035d6fc27f5633f0530c38134..56da062e87a3b3d9087002e55c826a02f991774b 100644 (file)
--- 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<def>> ; 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 a6ae87be720456623a3aaf9da1adaaea7a7dbb9f..30ccaf86da29d3820a5da3ebdb85ab03c46055dd 100644 (file)
--- 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 9eeebfe7fb2460739ed3c67f199f0e099d6a0b9b..0605b993ff125785f7b121a4f3ce2b89cfa4ff5a 100644 (file)
--- 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
+