X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=d61ad61039dc54f450067d8e5be6c5f452bf4dde;hb=c2a0823b4837cfe8ca7f89e68f58cd97efacf367;hp=9c0f456b2d653854e1b696625b14ea2856696ef8;hpb=5a88ca4db8f9d97a58add90a8a23f06960d9364f;p=helm.git

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index 9c0f456b2..d61ad6103 100644
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -62,7 +62,7 @@ let eval_unification_hint status t n =
   NCicLibrary.dump_obj status (inject_unification_hint (t,n))
 ;;
 
-let basic_index_obj l status =
+let basic_index_obj l (status:#NCic.status) =
   status#set_auto_cache 
     (List.fold_left
       (fun t (ks,v) -> 
@@ -275,25 +275,75 @@ let index_obj_for_auto status (uri, height, _, _, kind) =
    NCicLibrary.dump_obj status (record_index_obj data)
 ;; 
 
-let index_eq uri status =
+let basic_extract_obj obj status =
+ try
+  ignore (Helm_registry.get "extract_haskell");
+  let status,(msg,infos) = NCicExtraction.haskell_of_obj status obj in
+   prerr_endline msg;
+   status,infos
+ with
+    Helm_registry.Key_not_found _ -> status,NCicExtraction.empty_info
+  | exn -> prerr_endline ("EXTRACTION FAILURE: " ^ Printexc.to_string exn); assert false
+;;
+
+let inject_extract_obj =
+ let basic_extract_obj info
+   ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
+   ~alias_only status
+ =
+  let info= NCicExtraction.refresh_uri_in_info ~refresh_uri_in_reference info in
+   status#set_extraction_db
+    (NCicExtraction.register_infos status#extraction_db info)
+ in
+  GrafiteTypes.Serializer.register#run "extraction" basic_extract_obj
+;;
+
+let eval_extract_obj status obj = 
+ let status,infos = basic_extract_obj obj status in
+  NCicLibrary.dump_obj status (inject_extract_obj infos)
+;;
+
+(*
+module EmptyC = 
+  struct
+    let metasenv = []
+    let subst = []
+    let context = []
+  end
+*)
+
+let index_eq print uri (status:#NCic.status) =
   let eq_status = status#eq_cache in
-  let eq_status = NCicParamod.index_obj status eq_status uri in
-    status#set_eq_cache eq_status
+  let eq_status,clause = NCicParamod.index_obj status eq_status uri in
+  if print then
+   ((*let module NCicBlob =
+    struct
+     include NCicBlob.NCicBlob(EmptyC)
+     let pp t = status#ppterm ~metasenv:[] ~subst:[] ~context:[] t
+    end in
+   let module Pp = Pp.Pp(NCicBlob) in*)
+   (match clause with
+     | Some (*clause*) (_,Terms.Equation (_,_,_,o),_,_) ->
+        HLog.debug ("Indexed with orientation: " ^ Pp.string_of_comparison o);
+        (*HLog.debug ("Indexed as:" ^ Pp.pp_unit_clause clause)*)
+     | _ -> HLog.debug "Not indexed (i.e. pruned)")) ;
+  status#set_eq_cache eq_status
 ;;
 
 let record_index_eq =
  let basic_index_eq uri
    ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference 
    ~alias_only status
-   = if not alias_only then index_eq (NCicLibrary.refresh_uri uri) status else
-     status
+   = if not alias_only then index_eq false (NCicLibrary.refresh_uri uri) status 
+     else
+      status
  in
   GrafiteTypes.Serializer.register#run "index_eq" basic_index_eq
 ;;
 
 let index_eq_for_auto status uri =
  if NnAuto.is_a_fact_obj status uri then
-   let newstatus = index_eq uri status in
+   let newstatus = index_eq true uri status in
      if newstatus#eq_cache == status#eq_cache then status 
      else
        ((*prerr_endline ("recording " ^ (NUri.string_of_uri uri));*)
@@ -485,14 +535,47 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
       GrafiteTypes.Serializer.require
        ~alias_only ~baseuri ~fname:fullpath status
   | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n
-  | GrafiteAst.NCoercion (loc, name, compose, t, ty, source, target) ->
+  | GrafiteAst.NCoercion (loc, name, compose, None) ->
+     let status, t, ty, source, target =
+       let o_t = NotationPt.Ident (name,None) in
+       let metasenv,subst, status,t =
+         GrafiteDisambiguate.disambiguate_nterm 
+           status None [] [] [] ("",0,o_t) in
+       assert( metasenv = [] && subst = []);
+       let ty = NCicTypeChecker.typeof status [] [] [] t in
+       let source, target =
+         let clean = function
+           | NCic.Appl (NCic.Const _ as r :: l) -> 
+               NotationPt.Appl (NotationPt.NCic r ::
+                 List.map (fun _ -> NotationPt.Implicit `JustOne)l)
+           | NCic.Const _ as r -> NotationPt.NCic r
+           | NCic.Sort _ as r -> NotationPt.NCic r (* FG: missing case *)
+	   | _ -> assert false
+	 in
+         let rec aux = function
+           | NCic.Prod (_,_, (NCic.Prod _ as rest)) -> aux rest
+           | NCic.Prod (name, src, tgt) -> (name, clean src), clean tgt
+           | _ -> assert false
+	 in
+	 aux ty
+       in
+       status, o_t, NotationPt.NCic ty, source, target
+     in
+     let status, composites =
+      NCicCoercDeclaration.eval_ncoercion status name compose t ty source
+       target
+     in
+     let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *)
+     let aliases = GrafiteDisambiguate.aliases_for_objs status composites in
+      eval_alias status (mode,aliases)
+  | GrafiteAst.NCoercion (loc, name, compose, Some (t, ty, source, target)) ->
      let status, composites =
       NCicCoercDeclaration.eval_ncoercion status name compose t ty source
        target in
      let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *)
      let aliases = GrafiteDisambiguate.aliases_for_objs status composites in
       eval_alias status (mode,aliases)
-  | GrafiteAst.NQed loc ->
+  | GrafiteAst.NQed (loc,index) ->
      if status#ng_mode <> `ProofMode then
       raise (GrafiteTypes.Command_error "Not in proof mode")
      else
@@ -512,7 +595,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
               (match spec with
               | NReference.Def _ -> NReference.Def height
               | NReference.Fix (i,j,_) -> NReference.Fix(i,j,height)
-              | NReference.CoFix _ -> NReference.CoFix height
+              | NReference.CoFix i -> NReference.CoFix i
               | NReference.Ind _ | NReference.Con _
               | NReference.Decl as s -> s))
           | t -> NCicUtils.map status (fun _ () -> ()) () fix t
@@ -527,7 +610,9 @@ let rec eval_ncommand ~include_paths 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
-        let index_obj =
+        let status = eval_extract_obj status obj in
+       (try
+        let index_obj = index &&
          match obj_kind with
             NCic.Constant (_,_,_,_,(_,`Example,_))
           | NCic.Fixpoint (_,_,(_,`Example,_)) -> false
@@ -537,7 +622,9 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
          if index_obj then
           let status = index_obj_for_auto status obj in
            (try index_eq_for_auto status uri
-           with _ -> status)
+           with
+              Sys.Break as exn -> raise exn
+            | _ -> status)
          else
           status in
 (*
@@ -547,7 +634,6 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
 	in *)
 (*         prerr_endline (status#ppobj obj); *)
         HLog.message ("New object: " ^ NUri.string_of_uri uri);
-         (try
        (*prerr_endline (status#ppobj obj);*)
            let boxml = NCicElim.mk_elims status obj in
            let boxml = boxml @ NCicElim.mk_projections status obj in
@@ -561,7 +647,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
                try
                 let nstatus =
                  eval_ncommand ~include_paths opts status
-                  ("",0,GrafiteAst.NObj (HExtlib.dummy_floc,boxml))
+                  ("",0,GrafiteAst.NObj (HExtlib.dummy_floc,boxml,true))
                 in
                 if nstatus#ng_mode <> `CommandMode then
                   begin
@@ -577,11 +663,21 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
                   (*HLog.warn "error in generating projection/eliminator";*)
                   status
              ) status boxml in             
-           let _,_,_,_,nobj = obj in 
+           let _,_,_,_,nobj = obj in
+           (* attempting to generate an inversion principle on the maximum
+            * universe can take a long time to fail: this code removes maximal
+            * sorts from the universe list *)
+           let universes = NCicEnvironment.get_universes () in
+           let max_univ = List.fold_left max [] universes in
+           let universes = 
+             List.filter (fun x -> NCicEnvironment.universe_lt x max_univ)
+               universes
+           in
            let status = match nobj with
-               NCic.Inductive (is_ind,leftno,[it],_) ->
-                 let _,ind_name,ty,cl = it in
-                 List.fold_left 
+               NCic.Inductive (is_ind,leftno,itl,_) ->
+                 List.fold_left (fun status it ->      
+                 (let _,ind_name,ty,cl = it in
+                  List.fold_left 
                    (fun status outsort ->
                       let status = status#set_ng_mode `ProofMode in
                       try
@@ -593,14 +689,16 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
                        let _,_,menv,_,_ = invobj in
                         (match menv with
                              [] -> eval_ncommand ~include_paths opts status
-                                    ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+                                    ("",0,GrafiteAst.NQed (Stdpp.dummy_loc,false))
                            | _ -> status))
                        (* XXX *)
-                      with _ -> (*HLog.warn "error in generating inversion principle"; *)
+                      with
+                         Sys.Break as exn -> raise exn
+                       | _ -> (*HLog.warn "error in generating inversion principle"; *)
                                 let status = status#set_ng_mode `CommandMode in status)
                   status
                   (NCic.Prop::
-                    List.map (fun s -> NCic.Type s) (NCicEnvironment.get_universes ()))
+                    List.map (fun s -> NCic.Type s) universes))) status itl
               | _ -> status
            in
            let status = match nobj with
@@ -618,7 +716,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
                        let _,_,menv,_,_ = invobj in
                         (match menv with
                              [] -> eval_ncommand ~include_paths opts status
-                                    ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+                                    ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false))
                            | _ -> status))
                        (* XXX *)
                       with 
@@ -645,10 +743,12 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
                        let _,_,menv,_,_ = invobj in
                         (match menv with
                              [] -> eval_ncommand ~include_paths opts status
-                                    ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+                                    ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false))
                            | _ -> status))
                        (* XXX *)
-                      with _ -> (*HLog.warn "error in generating discrimination principle"; *)
+                      with
+                         Sys.Break as exn -> raise exn
+                       | _ -> (*HLog.warn "error in generating discrimination principle"; *)
                                 let status = status#set_ng_mode `CommandMode in
                                 status)
                   status' itl
@@ -717,8 +817,8 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
        let status = status#set_stack ninitial_stack in
        let status = subst_metasenv_and_fix_names status in
        let status = status#set_ng_mode `ProofMode in
-       eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
-  | GrafiteAst.NObj (loc,obj) ->
+       eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false))
+  | GrafiteAst.NObj (loc,obj,index) ->
      if status#ng_mode <> `CommandMode then
       raise (GrafiteTypes.Command_error "Not in command mode")
      else
@@ -733,7 +833,8 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
       let status = status#set_ng_mode `ProofMode in
       (match nmenv with
           [] ->
-           eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+           eval_ncommand ~include_paths opts status
+             ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,index))
         | _ -> status)
   | GrafiteAst.NDiscriminator (loc, indty) ->
       if status#ng_mode <> `CommandMode then
@@ -752,7 +853,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
            it leftno status status#baseuri in
         let _,_,menv,_,_ = obj in
           (match menv with
-               [] -> eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+               [] -> eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false))
              | _ -> prerr_endline ("Discriminator: non empty metasenv");
                     status)
   | GrafiteAst.NInverter (loc, name, indty, selection, sort) ->
@@ -794,7 +895,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
        (match menv with
           [] ->
             eval_ncommand ~include_paths opts status
-             ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+             ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false))
         | _ -> assert false)
   | GrafiteAst.NUnivConstraint (loc,u1,u2) ->
       eval_add_constraint status [`Type,u1] [`Type,u2]
@@ -843,8 +944,13 @@ let rec eval_executable ~include_paths opts status (text,prefix_len,ex) =
        let status =
         List.fold_left 
           (fun status tac ->
+            let time0 = Unix.gettimeofday () in
             let status = eval_ng_tac (text,prefix_len,tac) status in
-            subst_metasenv_and_fix_names status)
+            let time3 = Unix.gettimeofday () in
+            HLog.debug ("... eval_ng_tac done in " ^ string_of_float (time3 -. time0) ^ "s");
+            let status = subst_metasenv_and_fix_names status in
+            let time3 = Unix.gettimeofday () in
+            HLog.debug ("... subst_metasenv_and_fix_names done in " ^ string_of_float (time3 -. time0) ^ "s"); status)
           status tacl
        in
         status