X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=ea5afab4c5c97b60f4dd5783abe6923c7da92413;hb=63b86fce8a75490b957e7301517b9006f58321b6;hp=ec9f3866fdab4bbffab2ce894ab17e937b809cef;hpb=b266ed97b63400d62ab4ba6a4ebdfbc1d5b0c2bb;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index ec9f3866f..ea5afab4c 100644
--- 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 []
 ;;
@@ -747,6 +747,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
         let obj = uri,height,[],[],obj_kind in
         let old_status = status in
         let status = NCicLibrary.add_obj status obj in
+(*         prerr_endline (NCicPp.ppobj obj); *)
         HLog.message ("New object: " ^ NUri.string_of_uri uri);
          (try
        (*prerr_endline (NCicPp.ppobj obj);*)
@@ -774,9 +775,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 +792,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 +862,39 @@ 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, selection, sort) ->
+     if status#ng_mode <> `CommandMode then
+      raise (GrafiteTypes.Command_error "Not in command mode")
+     else
+      let metasenv,subst,status,sort = match sort with
+        | None -> [],[],status,NCic.Sort NCic.Prop
+        | Some s -> GrafiteDisambiguate.disambiguate_nterm None status [] [] []
+                      (text,prefix_len,s) 
+      in
+      assert (metasenv = []);
+      let sort = NCicReduction.whd ~subst [] sort in
+      let sort = match sort with 
+          NCic.Sort s -> s
+        | _ ->  raise (Invalid_argument (Printf.sprintf "ninverter: found target %s, which is not a sort" 
+                                           (NCicPp.ppterm ~metasenv ~subst ~context:[] sort)))
+      in
+      let status = status#set_ng_mode `ProofMode in
+      let metasenv,subst,status,indty =
+       GrafiteDisambiguate.disambiguate_nterm None status [] [] subst (text,prefix_len,indty) in
+      let indtyno,(_,leftno,tys,_,_) = match indty with
+          NCic.Const ((NReference.Ref (_,NReference.Ind (_,indtyno,_))) as r) -> 
+            indtyno, NCicEnvironment.get_checked_indtys r
+        | _ -> prerr_endline ("engine: indty ="  ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] indty) ; assert false in
+      let it = List.nth tys indtyno in
+     let status,obj = NInversion.mk_inverter name it leftno ?selection sort 
+                        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