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 ec9f3866fdab4bbffab2ce894ab17e937b809cef..0806057ec14ab1d67189dba4832028c6509576db 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -501,25 +501,25 @@ let eval_unification_hint status t n =
   status,`New []
 ;;
 
-let basic_eval_add_constraint (s,u1,u2) status =
- NCicLibrary.add_constraint status s u1 u2
+let basic_eval_add_constraint (u1,u2) status =
+ NCicLibrary.add_constraint status u1 u2
 ;;
 
 let inject_constraint =
- let basic_eval_add_constraint (s,u1,u2) 
+ let basic_eval_add_constraint (u1,u2) 
        ~refresh_uri_in_universe 
        ~refresh_uri_in_term
  =
   let u1 = refresh_uri_in_universe u1 in 
   let u2 = refresh_uri_in_universe u2 in 
-  basic_eval_add_constraint (s,u1,u2)
+  basic_eval_add_constraint (u1,u2)
  in
   NRstatus.Serializer.register "constraints" basic_eval_add_constraint
 ;;
 
-let eval_add_constraint status s u1 u2 = 
- let status = basic_eval_add_constraint (s,u1,u2) status in
- let dump = inject_constraint (s,u1,u2)::status#dump in
+let eval_add_constraint status u1 u2 = 
+ let status = basic_eval_add_constraint (u1,u2) status in
+ let dump = inject_constraint (u1,u2)::status#dump in
  let status = status#set_dump dump in
   status,`Old []
 ;;
@@ -774,9 +774,9 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
                 in
                 status, concat_nuris uris nuris
                with
-                NCicTypeChecker.TypeCheckerFailure msg
-                 when Lazy.force msg =
-                 "Sort elimination not allowed" ->
+               | MultiPassDisambiguator.DisambiguationError _ 
+               | NCicTypeChecker.TypeCheckerFailure _ ->
+                  HLog.warn "error in generating projection/eliminator";
                   status,uris
              ) (status,`New [] (* uris *)) boxml in
            let coercions =
@@ -791,17 +791,21 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
            let status,uris =
             List.fold_left
              (fun (status,uris) (name,cpos,arity) ->
-               let metasenv,subst,status,t =
-                GrafiteDisambiguate.disambiguate_nterm None status [] [] []
-                 ("",0,CicNotationPt.Ident (name,None)) in
-               assert (metasenv = [] && subst = []);
-               let status, nuris = 
-                 NCicCoercDeclaration.
-                   basic_eval_and_record_ncoercion_from_t_cpos_arity 
-                    status (name,t,cpos,arity)
-               in
-               let uris = concat_nuris nuris uris in
-               status, uris) 
+               try
+                 let metasenv,subst,status,t =
+                  GrafiteDisambiguate.disambiguate_nterm None status [] [] []
+                   ("",0,CicNotationPt.Ident (name,None)) in
+                 assert (metasenv = [] && subst = []);
+                 let status, nuris = 
+                   NCicCoercDeclaration.
+                     basic_eval_and_record_ncoercion_from_t_cpos_arity 
+                      status (name,t,cpos,arity)
+                 in
+                 let uris = concat_nuris nuris uris in
+                 status, uris
+               with MultiPassDisambiguator.DisambiguationError _-> 
+                 HLog.warn ("error in generating coercion: "^name);
+                 status, uris) 
              (status,uris) coercions
            in
             status,uris
@@ -857,8 +861,29 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
           [] ->
            eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
         | _ -> status,`New [])
-  | GrafiteAst.NUnivConstraint (loc,strict,u1,u2) ->
-      eval_add_constraint status strict [false,u1] [false,u2]
+  | 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]
 ;;
 
 let rec eval_command = {ec_go = fun ~disambiguate_command opts status