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

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 7e314670b..ea5afab4c 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -41,6 +41,11 @@ type options = {
   do_heavy_checks: bool ; 
 }
 
+let concat_nuris uris nuris =
+   match uris,nuris with
+   | `New uris, `New nuris -> `New (nuris@uris)
+   | _ -> assert false
+;;
 (** create a ProofEngineTypes.mk_fresh_name_type function which uses given
   * names as long as they are available, then it fallbacks to name generation
   * using FreshNamesGenerator module *)
@@ -496,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 []
 ;;
@@ -656,6 +661,7 @@ let eval_ng_tac tac =
   | GrafiteAst.NConstructor (_loc,num,args) -> 
      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.NDot _ -> NTactics.dot_tac 
   | GrafiteAst.NElim (_loc, what, where) ->
       NTactics.elim_tac 
@@ -666,6 +672,7 @@ let eval_ng_tac tac =
       NTactics.generalize_tac ~where:(text,prefix_len,where)
   | GrafiteAst.NId _ -> (fun x -> x)
   | GrafiteAst.NIntro (_loc,n) -> NTactics.intro_tac n
+  | GrafiteAst.NLApply (_loc, t) -> NTactics.lapply_tac (text,prefix_len,t) 
   | GrafiteAst.NLetIn (_loc,where,what,name) ->
       NTactics.letin_tac ~where:(text,prefix_len,where) 
         ~what:(text,prefix_len,what) name
@@ -740,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);*)
@@ -765,13 +773,11 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
                  eval_ncommand opts status
                   ("",0,GrafiteAst.NObj (HExtlib.dummy_floc,boxml))
                 in
-                 match uris,nuris with
-                    `New uris, `New nuris -> status,`New (nuris@uris)
-                  | _ -> assert false
+                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 =
@@ -783,16 +789,25 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
                  (fun (name,is_coercion,arity) ->
                    if is_coercion then Some(name,leftno,arity) else None) fields
             | _ -> [] in
-           let status =
+           let status,uris =
             List.fold_left
-             (fun status (name,cpos,arity) ->
-               let metasenv,subst,status,t =
-                GrafiteDisambiguate.disambiguate_nterm None status [] [] []
-                 ("",0,CicNotationPt.Ident (name,None)) in
-               assert (metasenv = [] && subst = []);
-               NCicCoercDeclaration.basic_eval_and_inject_ncoercion_from_t_cpos_arity 
-                 status (name,t,cpos,arity)
-             ) status coercions
+             (fun (status,uris) (name,cpos,arity) ->
+               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
           with
@@ -847,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