Added initial support for inversion principles in Matita NG.

[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 482a138a6c8f4ce16863c36b5a92b3bfe561deb1..0806057ec14ab1d67189dba4832028c6509576db 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -861,6 +861,27 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
           [] ->
            eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
         | _ -> status,`New [])
+  | GrafiteAst.NInverter (loc, name, 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 _,leftno,tys,_,_ = match indty with
+          NCic.Const r -> NCicEnvironment.get_checked_indtys r
+        | _ -> assert false in
+      let it = match tys with
+          hd::tl -> hd
+        | _ -> assert false
+      in
+     let status,obj =
+      NInversion.mk_inverter name it leftno status status#baseuri in
+     let _,_,menv,_,_ = obj in
+     (match menv with
+        [] ->
+          eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+      | _ -> assert false)
   | GrafiteAst.NUnivConstraint (loc,u1,u2) ->
       eval_add_constraint status [`Type,u1] [`Type,u2]
 ;;