New debugging tactic nassert:

 nassert H1: t1 ... Hn: tn \vdash T

asserts (using OCaml's assert) that the current goal is equal (using
OCaml equality) to the one given the user. The substitution is fully
expanded just before calling OCaml equality.

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 062f2c0d216a0d16a7363dae3f8464031c14343b..7c0a3fc99d48041bc79f74e844389189be8d3332 100644 (file)
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -51,6 +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
    | 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 ebf0d8a63b8497de710e1b55756cc7f3f79ae4f8..1ad89f462f4c19e0580b3ce831f64275a70a5012 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -586,6 +586,10 @@ 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) ->
+     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))
   | 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 56da062e87a3b3d9087002e55c826a02f991774b..db5fa1294383e2e60b35fc8cb3b5712922a81650 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -182,6 +182,15 @@ EXTEND
   using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
   ntactic: [
     [ IDENT "napply"; t = tactic_term -> GrafiteAst.NApply (loc, t)
+    | IDENT "nassert";
+        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)
     | 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/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml
index 86487e20d5cc575dc054ef92b4fad67482e865d1..55448ae2db03615416aec06118be58bacb492a58 100644 (file)
--- a/helm/software/components/ng_tactics/nTacStatus.ml
+++ b/helm/software/components/ng_tactics/nTacStatus.ml
@@ -319,3 +319,26 @@ let analyse_indty status ty =
 ;;
 
 let mk_cic_term c t = None,c,t ;;
+
+let apply_subst status ctx t =
+ let status, (name,_,t) = relocate status ctx t in
+ let _,_,_,subst,_ = status.pstatus in
+ let rec aux ctx =
+  function
+     NCic.Meta (i,lc) ->
+      (try
+        let _,_,t,_ = NCicUtils.lookup_subst i subst in
+        let t = NCicSubstitution.subst_meta lc t in
+         aux ctx t
+       with
+        Not_found ->
+         match lc with
+            _,NCic.Irl _ -> NCic.Meta (i,lc)
+          | n,NCic.Ctx l ->
+             NCic.Meta
+              (i,(0,NCic.Ctx
+                  (List.map (fun t -> aux ctx (NCicSubstitution.lift n t)) l))))
+   | t -> NCicUtils.map (fun item ctx -> item::ctx) ctx aux t
+ in
+  status, (name, ctx, aux ctx t)
+;;

diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli
index 81436f53d63c48f5f534c8618efe8a796dbd6e68..c0f0ca4db019d2d25963612581daec13d99a4ffb 100644 (file)
--- a/helm/software/components/ng_tactics/nTacStatus.mli
+++ b/helm/software/components/ng_tactics/nTacStatus.mli
@@ -56,6 +56,9 @@ val unify:
 val refine: 
   lowtac_status -> NCic.context -> cic_term -> cic_term option -> 
     lowtac_status * cic_term * cic_term (* status, term, type *)
+val apply_subst:
+  lowtac_status -> NCic.context -> cic_term -> lowtac_status * cic_term
+
 
 val get_goalty: lowtac_status -> int -> cic_term
 val mk_meta: 

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 30ccaf86da29d3820a5da3ebdb85ab03c46055dd..3be17c5e7eca608993a2304e663b9670643f9ec6 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -496,3 +496,44 @@ let case1_tac name =
               ~what:("",0,Ast.Ident (name,None));
               if name = "_clearme" then clear_tac ["_clearme"] else id_tac ]
 ;;
+
+let assert_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 status,gty' = term_of_cic_term status gty (ctx_of gty) in
+ assert (concl=gty');
+ 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);
+          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);
+          status,item::ctx
+      | _ -> assert false
+   ) hyps (ctx_of gty) (status,[])
+ in
+  exec id_tac status goal)
+;;

diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli
index 0605b993ff125785f7b121a4f3ce2b89cfa4ff5a..4c3e4d159fda1da9163b3edc711ce252d07ddbf1 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -48,4 +48,6 @@ val letin_tac:
       where:NTacStatus.tactic_pattern ->
       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 ->
+  NTacStatus.tactic