assert_tac now takes a list of sequents and also checks that the number of

sequents is the appropriate one.

It is the first example of a high-tactic that works also with the stack.

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 7c0a3fc99d48041bc79f74e844389189be8d3332..2e6f450caaf03f61d7d8629869b7569596ae2062 100644 (file)
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -51,7 +51,7 @@ type 'term just =
 
 type ntactic =
    | NApply of loc * CicNotationPt.term
-   | NAssert of loc * (string * [`Decl of CicNotationPt.term | `Def of CicNotationPt.term * CicNotationPt.term]) list * CicNotationPt.term
+   | NAssert of loc * ((string * [`Decl of CicNotationPt.term | `Def of CicNotationPt.term * CicNotationPt.term]) list * CicNotationPt.term) list
    | NCases of loc * CicNotationPt.term * npattern  
    | NCase1 of loc * string
    | NChange of loc * npattern * CicNotationPt.term

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 1ad89f462f4c19e0580b3ce831f64275a70a5012..354413f1b9464307172ae2c18b3124887d3a07cd 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -586,10 +586,17 @@ let eval_ng_punct (_text, _prefix_len, punct) =
 let eval_ng_tac (text, prefix_len, tac) =
   match tac with
   | GrafiteAst.NApply (_loc, t) -> NTactics.apply_tac (text,prefix_len,t) 
-  | GrafiteAst.NAssert (_loc, hyps, concl) ->
+  | GrafiteAst.NAssert (_loc, seqs) ->
      NTactics.assert_tac
-      (List.map (function (id,`Decl t) -> id,`Decl (text,prefix_len,t) | (id,`Def (b,t)) -> id,`Def ((text,prefix_len,b),(text,prefix_len,t))) hyps,
-      (text,prefix_len,concl))
+      ((List.map
+        (function (hyps,concl) ->
+          List.map
+           (function
+              (id,`Decl t) -> id,`Decl (text,prefix_len,t)
+             |(id,`Def (b,t))->id,`Def((text,prefix_len,b),(text,prefix_len,t))
+           ) hyps,
+          (text,prefix_len,concl))
+       ) seqs)
   | GrafiteAst.NCases (_loc, what, where) ->
       NTactics.cases_tac 
         ~what:(text,prefix_len,what)

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index db5fa1294383e2e60b35fc8cb3b5712922a81650..7b4e6157b70fd43950da32b8d8f832628cbcffa5 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -183,14 +183,15 @@ EXTEND
   ntactic: [
     [ IDENT "napply"; t = tactic_term -> GrafiteAst.NApply (loc, t)
     | IDENT "nassert";
+       seqs = LIST0 [
         hyps = LIST0
          [ id = IDENT ; SYMBOL ":" ; ty = tactic_term -> id,`Decl ty
          | id = IDENT ; SYMBOL ":" ; ty = tactic_term ;
                         SYMBOL <:unicode<def>> ; bo = tactic_term ->
             id,`Def (bo,ty)];
         SYMBOL <:unicode<vdash>>;
-        concl = tactic_term ->
-         GrafiteAst.NAssert (loc, hyps, concl)
+        concl = tactic_term -> (hyps,concl) ] ->
+         GrafiteAst.NAssert (loc, seqs)
     | IDENT "ncases"; what = tactic_term ; where = pattern_spec ->
         GrafiteAst.NCases (loc, what, where)
     | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term -> 

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 3be17c5e7eca608993a2304e663b9670643f9ec6..110e882af2b02c51752ef2411e41f1c60c5047e4 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -497,43 +497,52 @@ let case1_tac name =
               if name = "_clearme" then clear_tac ["_clearme"] else id_tac ]
 ;;
 
-let assert_tac (hyps,concl) = distribute_tac (fun status goal ->
+let assert0_tac (hyps,concl) = distribute_tac (fun status goal ->
  let gty = get_goalty status goal in
- let status,concl = disambiguate status concl None (ctx_of gty) in
- let status,concl = term_of_cic_term status concl (ctx_of gty) in
+ let eq status ctx t1 t2 =
+  let status,t1 = disambiguate status t1 None ctx in
+  let status,t1 = apply_subst status ctx t1 in
+  let status,t1 = term_of_cic_term status t1 ctx in
+  let t2 = mk_cic_term ctx t2 in
+  let status,t2 = apply_subst status ctx t2 in
+  let status,t2 = term_of_cic_term status t2 ctx in
+  prerr_endline ("COMPARING: " ^ NCicPp.ppterm ~subst:[] ~metasenv:[] ~context:ctx t1 ^ " vs " ^ NCicPp.ppterm ~subst:[] ~metasenv:[] ~context:ctx t2);
+  assert (t1=t2);
+  status
+ in
  let status,gty' = term_of_cic_term status gty (ctx_of gty) in
- assert (concl=gty');
+ let status = eq status (ctx_of gty) concl gty' in
  let status,_ =
   List.fold_right2
    (fun (id1,e1) ((id2,e2) as item) (status,ctx) ->
      assert (id1=id2);
      match e1,e2 with
         `Decl t1, NCic.Decl t2 ->
-          let status,t1 = disambiguate status t1 None ctx in
-          let status,t1 = apply_subst status ctx t1 in
-          let status,t1 = term_of_cic_term status t1 ctx in
-          let t2 = mk_cic_term ctx t2 in
-          let status,t2 = apply_subst status ctx t2 in
-          let status,t2 = term_of_cic_term status t2 ctx in
-          assert (t1=t2);
+          let status = eq status ctx t1 t2 in
           status,item::ctx
       | `Def (b1,t1), NCic.Def (b2,t2) ->
-          let status,t1 = disambiguate status t1 None ctx in
-          let status,t1 = apply_subst status ctx t1 in
-          let status,t1 = term_of_cic_term status t1 ctx in
-          let status,b1 = disambiguate status b1 None ctx in
-          let status,b1 = apply_subst status ctx b1 in
-          let status,b1 = term_of_cic_term status b1 ctx in
-          let t2 = mk_cic_term ctx t2 in
-          let status,t2 = apply_subst status ctx t2 in
-          let status,t2 = term_of_cic_term status t2 ctx in
-          let b2 = mk_cic_term ctx b2 in
-          let status,b2 = apply_subst status ctx b2 in
-          let status,b2 = term_of_cic_term status b2 ctx in
-          assert (t1=t2 && b1=b2);
+          let status = eq status ctx t1 t2 in
+          let status = eq status ctx b1 b2 in
           status,item::ctx
       | _ -> assert false
    ) hyps (ctx_of gty) (status,[])
  in
   exec id_tac status goal)
 ;;
+
+let assert_tac seqs status =
+ match status.gstatus with
+  | [] -> assert false
+  | (g,_,_,_) :: s ->
+     assert (List.length g = List.length seqs);
+     (match seqs with
+         [] -> id_tac
+       | [seq] -> assert0_tac seq
+       | _ ->
+         block_tac
+          (branch_tac::
+          HExtlib.list_concat ~sep:[shift_tac]
+            (List.map (fun seq -> [assert0_tac seq]) seqs)@
+          [merge_tac])
+     ) status
+;;

diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli
index 4c3e4d159fda1da9163b3edc711ce252d07ddbf1..b558b4c9b48cae4e627c2687d265e4c42eff6979 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -49,5 +49,5 @@ val letin_tac:
       what: NTacStatus.tactic_term ->
       string -> NTacStatus.tactic
 val assert_tac:
- (string * [`Decl of NTacStatus.tactic_term | `Def of NTacStatus.tactic_term * NTacStatus.tactic_term]) list * NTacStatus.tactic_term ->
+ ((string * [`Decl of NTacStatus.tactic_term | `Def of NTacStatus.tactic_term * NTacStatus.tactic_term]) list * NTacStatus.tactic_term) list ->
   NTacStatus.tactic