1) GrafiteAst.NEval => GrafiteAst.NReduce

2) new tactic "nnormalize" implemented
3) "ngeneralize" now uses "wanted" when no term is selected
   (so that it is possible to use ngeneralize to move an
   hypothesis down)
4) new syntax for non punctuational tinycals was missing

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 6e48074ad56e4463174402abf3240ec93746970e..a2d1ef655cc09922eb497490d6b7f4f7639c8fcc 100644 (file)
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -56,11 +56,11 @@ type ntactic =
    | NCase1 of loc * string
    | NChange of loc * npattern * CicNotationPt.term
    | NElim of loc * CicNotationPt.term * npattern  
-   | NEval of loc * npattern * [ `Whd of bool ]
    | NGeneralize of loc * npattern
    | NId of loc
    | NIntro of loc * string
    | NLetIn of loc * npattern * CicNotationPt.term * string
+   | NReduce of loc * [ `Normalize of bool | `Whd of bool ] * npattern
    | 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 89f50c8fd39324eecfdec735cbbc67f6c5abef66..ccd02981f2f4f5a5516eb861dbca2e1cae29ca99 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -616,8 +616,6 @@ let eval_ng_tac (text, prefix_len, tac) =
       NTactics.elim_tac 
         ~what:(text,prefix_len,what)
         ~where:(text,prefix_len,where)
-  | GrafiteAst.NEval (_loc, where, reduction) ->
-      NTactics.eval_tac ~reduction ~where:(text,prefix_len,where)
   | GrafiteAst.NGeneralize (_loc, where) -> 
       NTactics.generalize_tac ~where:(text,prefix_len,where)
   | GrafiteAst.NId _ -> (fun x -> x)
@@ -625,6 +623,8 @@ let eval_ng_tac (text, prefix_len, tac) =
   | GrafiteAst.NLetIn (_loc,where,what,name) ->
       NTactics.letin_tac ~where:(text,prefix_len,where) 
         ~what:(text,prefix_len,what) name
+  | GrafiteAst.NReduce (_loc, reduction, where) ->
+      NTactics.reduce_tac ~reduction ~where:(text,prefix_len,where)
   | 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 547e510253f64302d3f48db36e3ff366074884bc..742e538febd09a0f50b3780a319ac3d67a08c81d 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -131,6 +131,15 @@ EXTEND
     | IDENT "unfold"; t = OPT tactic_term -> `Unfold t
     | IDENT "whd" -> `Whd ]
   ];
+  nreduction_kind: [
+    [ IDENT "nnormalize" ; delta = OPT [ IDENT "nodelta" -> () ] ->
+       let delta = match delta with None -> true | _ -> false in
+        `Normalize delta
+    (*| IDENT "unfold"; t = OPT tactic_term -> `Unfold t*)
+    | IDENT "nwhd" ; delta = OPT [ IDENT "nodelta" -> () ] ->
+       let delta = match delta with None -> true | _ -> false in
+        `Whd delta]
+  ];
   sequent_pattern_spec: [
    [ hyp_paths =
       LIST0
@@ -222,12 +231,10 @@ EXTEND
     | IDENT "nletin"; name = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term;
         where = pattern_spec ->
         G.NLetIn (loc,where,t,name)
+    | kind = nreduction_kind; p = pattern_spec ->
+        G.NReduce (loc, kind, p)
     | IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec ->
         G.NRewrite (loc, dir, what, where)
-    | IDENT "nwhd"; delta = OPT [ IDENT "nodelta" -> () ];
-      where = pattern_spec ->
-        let delta = match delta with None -> true | _ -> false in
-        G.NEval (loc, where, `Whd delta)
     | SYMBOL "#"; n=IDENT -> G.NIntro (loc,n)
     | SYMBOL "#"; SYMBOL "_" -> G.NIntro (loc,"_")
     | SYMBOL "*" -> G.NCase1 (loc,"_")

diff --git a/helm/software/components/ng_tactics/.depend b/helm/software/components/ng_tactics/.depend
index a4351be5484fa79762d43abd38df49ac08c23c93..2e34a62a912ffa6c454814fd5e8f2527b028617b 100644 (file)
--- a/helm/software/components/ng_tactics/.depend
+++ b/helm/software/components/ng_tactics/.depend
@@ -1,6 +1,8 @@
+nTacStatus.cmi: 
 nTactics.cmi: nTacStatus.cmi 
-nTacStatus.cmo: nTacStatus.cmi 
-nTacStatus.cmx: nTacStatus.cmi 
+nCicElim.cmi: 
+nTacStatus.cmo: nCicTacReduction.cmi nTacStatus.cmi 
+nTacStatus.cmx: nCicTacReduction.cmx nTacStatus.cmi 
 nTactics.cmo: nTacStatus.cmi nTactics.cmi 
 nTactics.cmx: nTacStatus.cmx nTactics.cmi 
 nCicElim.cmo: nCicElim.cmi 

diff --git a/helm/software/components/ng_tactics/.depend.opt b/helm/software/components/ng_tactics/.depend.opt
index a4351be5484fa79762d43abd38df49ac08c23c93..2e34a62a912ffa6c454814fd5e8f2527b028617b 100644 (file)
--- a/helm/software/components/ng_tactics/.depend.opt
+++ b/helm/software/components/ng_tactics/.depend.opt
@@ -1,6 +1,8 @@
+nTacStatus.cmi: 
 nTactics.cmi: nTacStatus.cmi 
-nTacStatus.cmo: nTacStatus.cmi 
-nTacStatus.cmx: nTacStatus.cmi 
+nCicElim.cmi: 
+nTacStatus.cmo: nCicTacReduction.cmi nTacStatus.cmi 
+nTacStatus.cmx: nCicTacReduction.cmx nTacStatus.cmi 
 nTactics.cmo: nTacStatus.cmi nTactics.cmi 
 nTactics.cmx: nTacStatus.cmx nTactics.cmi 
 nCicElim.cmo: nCicElim.cmi 

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 7937e8b4b4ddbb739ed6fb27bafa82a0b3f7f7ea..a0d8eba48a6b555718c45625968ccc6ddc451666 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -336,25 +336,37 @@ let generalize_tac ~where =
    select_tac ~where ~job:(`Collect l) true; 
    print_tac true "ha selezionato?";
    (fun s -> distribute_tac (fun status goal ->
-     if !l = [] then fail (lazy "No term to generalize");
-     let goalty = get_goalty status goal in
-     let canon = List.hd !l in
-     let status = 
+      let goalty = get_goalty status goal in
+      let status,canon,rest =
+       match !l with
+          [] ->
+           (match where with
+               _,_,(None,_,_)  -> fail (lazy "No term to generalize")
+             | txt,txtlen,(Some what,_,_) ->
+                let status, what =
+                 disambiguate status (txt,txtlen,what) None (ctx_of goalty)
+                in
+                 status,what,[]
+           )
+        | he::tl -> status,he,tl in
+      let status = 
        List.fold_left 
-         (fun s t -> unify s (ctx_of goalty) canon t) status (List.tl !l)
-     in
-     let status, canon = term_of_cic_term status canon (ctx_of goalty) in
-     instantiate status goal 
-      (mk_cic_term (ctx_of goalty) (NCic.Appl [NCic.Implicit `Term ; canon ]))
+         (fun s t -> unify s (ctx_of goalty) canon t) status rest in
+      let status, canon = term_of_cic_term status canon (ctx_of goalty) in
+      instantiate status goal 
+       (mk_cic_term (ctx_of goalty) (NCic.Appl [NCic.Implicit `Term ; canon ]))
    ) s) ]
 ;;
 
-let eval_tac ~reduction ~where =
+let reduce_tac ~reduction ~where =
   let change status t = 
     match reduction with
+    | `Normalize perform_delta ->
+        normalize status
+         ?delta:(if perform_delta then None else Some max_int) (ctx_of t) t
     | `Whd perform_delta -> 
-         whd status
-           ?delta:(if perform_delta then None else Some max_int) (ctx_of t) t
+        whd status
+         ?delta:(if perform_delta then None else Some max_int) (ctx_of t) t
   in
   let where = GrafiteDisambiguate.disambiguate_npattern where in
   select0_tac ~where ~job:(`ChangeWith change)

diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli
index b558b4c9b48cae4e627c2687d265e4c42eff6979..3e13035eb792d4188a976d88137f9fe0989a2b36 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -41,8 +41,8 @@ val rewrite_tac:
    what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> 
     NTacStatus.tactic
 val generalize_tac : where:NTacStatus.tactic_pattern -> NTacStatus.tactic
-val eval_tac: 
-      reduction:[ `Whd of bool ] ->
+val reduce_tac: 
+      reduction:[ `Normalize of bool | `Whd of bool ] ->
       where:NTacStatus.tactic_pattern -> NTacStatus.tactic
 val letin_tac: 
       where:NTacStatus.tactic_pattern ->