Implementation of ndestruct tactic (including destruction of constructor forms

[helm.git] / helm / software / components / grafite_engine / grafiteEngine.ml

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index fd8d776c180749023a85e4c87a4d266113482aa0..248c02fa50facd4ee613d89dd9e392e7bb5af269 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -759,6 +759,9 @@ let eval_ng_tac tac =
      NTactics.constructor_tac 
        ?num ~args:(List.map (fun x -> text,prefix_len,x) args)
   | GrafiteAst.NCut (_loc, t) -> NTactics.cut_tac (text,prefix_len,t) 
+(*| GrafiteAst.NDiscriminate (_,what) -> NDestructTac.discriminate_tac ~what:(text,prefix_len,what)
+  | GrafiteAst.NSubst (_,what) -> NDestructTac.subst_tac ~what:(text,prefix_len,what)*)
+  | GrafiteAst.NDestruct _ -> NDestructTac.destruct_tac
   | GrafiteAst.NDot _ -> NTactics.dot_tac 
   | GrafiteAst.NElim (_loc, what, where) ->
       NTactics.elim_tac 
@@ -775,6 +778,7 @@ let eval_ng_tac tac =
         ~what:(text,prefix_len,what) name
   | GrafiteAst.NMerge _ -> NTactics.merge_tac 
   | GrafiteAst.NPos (_,l) -> NTactics.pos_tac l
+  | GrafiteAst.NPosbyname (_,s) -> NTactics.case_tac s
   | GrafiteAst.NReduce (_loc, reduction, where) ->
       NTactics.reduce_tac ~reduction ~where:(text,prefix_len,where)
   | GrafiteAst.NRewrite (_loc,dir,what,where) ->
@@ -991,6 +995,24 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
           [] ->
            eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
         | _ -> status,`New [])
+  | GrafiteAst.NDiscriminator (_,_) -> assert false (*(loc, indty) ->
+      if status#ng_mode <> `CommandMode then
+        raise (GrafiteTypes.Command_error "Not in command mode")
+      else
+        let status = status#set_ng_mode `ProofMode in
+        let metasenv,subst,status,indty =
+          GrafiteDisambiguate.disambiguate_nterm None status [] [] [] (text,prefix_len,indty) in
+        let indtyno, (_,_,tys,_,_) = match indty with
+            NCic.Const ((NReference.Ref (_,NReference.Ind (_,indtyno,_))) as r) ->
+              indtyno, NCicEnvironment.get_checked_indtys r
+          | _ -> prerr_endline ("engine: indty expected... (fix this error message)"); assert false in
+        let it = List.nth tys indtyno in
+        let status,obj =  NDestructTac.mk_discriminator it status in
+        let _,_,menv,_,_ = obj in
+          (match menv with
+               [] -> eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+             | _ -> prerr_endline ("Discriminator: non empty metasenv");
+                    status, `New []) *)
   | GrafiteAst.NInverter (loc, name, indty, selection, sort) ->
      if status#ng_mode <> `CommandMode then
       raise (GrafiteTypes.Command_error "Not in command mode")