New debugging tactic nassert:

[helm.git] / helm / software / components / ng_tactics / nTactics.ml

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)
+;;