X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=f2876d2a9b6fb977cd0a42e5103ed85dbd657545;hb=489639a3c319d0349a9c864fd0eeaf659daa3d3f;hp=d61ad61039dc54f450067d8e5be6c5f452bf4dde;hpb=210b6e113724900dd5c5745da2881b868154d241;p=helm.git

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index d61ad6103..f2876d2a9 100644
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -55,7 +55,7 @@ let inject_unification_hint =
 
 let eval_unification_hint status t n = 
  let metasenv,subst,status,t =
-  GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,t) in
+  GrafiteDisambiguate.disambiguate_nterm status `XTSort [] [] [] ("",0,t) in
  assert (metasenv=[]);
  let t = NCicUntrusted.apply_subst status subst [] t in
  let status = basic_eval_unification_hint (t,n) status in
@@ -286,6 +286,15 @@ let basic_extract_obj obj status =
   | exn -> prerr_endline ("EXTRACTION FAILURE: " ^ Printexc.to_string exn); assert false
 ;;
 
+let basic_extract_ocaml_obj obj status =
+ try
+  let status  = OcamlExtraction.print_ocaml_of_obj status obj in
+  let infos,status = status#get_info in
+   status,infos
+ with
+  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
@@ -298,11 +307,28 @@ let inject_extract_obj =
   GrafiteTypes.Serializer.register#run "extraction" basic_extract_obj
 ;;
 
+let inject_extract_ocaml_obj =
+ let basic_extract_ocaml_obj info
+   ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
+   ~alias_only status
+ =
+  let info= OcamlExtractionTable.refresh_uri_in_info ~refresh_uri_in_reference ~refresh_uri:NCicLibrary.refresh_uri info in
+   status#set_ocaml_extraction_db
+    (OcamlExtractionTable.register_infos status#ocaml_extraction_db info)
+ in
+  GrafiteTypes.Serializer.register#run "ocaml_extraction" basic_extract_ocaml_obj
+;;
+
 let eval_extract_obj status obj = 
  let status,infos = basic_extract_obj obj status in
   NCicLibrary.dump_obj status (inject_extract_obj infos)
 ;;
 
+let eval_extract_ocaml_obj status obj = 
+ let status,infos = basic_extract_ocaml_obj obj status in
+  NCicLibrary.dump_obj status (inject_extract_ocaml_obj infos)
+;;
+
 (*
 module EmptyC = 
   struct
@@ -354,7 +380,7 @@ let index_eq_for_auto status uri =
 ;; 
 
 let inject_constraint =
- let basic_eval_add_constraint (u1,u2) 
+ let basic_eval_add_constraint (acyclic,u1,u2) 
      ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
      ~alias_only status
  =
@@ -364,7 +390,7 @@ let inject_constraint =
     (* NCicLibrary.add_constraint adds the constraint to the NCicEnvironment
      * and also to the storage (for undo/redo). During inclusion of compiled
      * files the storage must not be touched. *)
-    NCicEnvironment.add_lt_constraint u1 u2;
+    NCicEnvironment.add_lt_constraint acyclic u1 u2;
     status
   else
    status
@@ -372,12 +398,23 @@ let inject_constraint =
   GrafiteTypes.Serializer.register#run "constraints" basic_eval_add_constraint 
 ;;
 
-let eval_add_constraint status u1 u2 = 
- let status = NCicLibrary.add_constraint status u1 u2 in
-  NCicLibrary.dump_obj status (inject_constraint (u1,u2))
+let eval_add_constraint status acyclic u1 u2 = 
+ let status = NCicLibrary.add_constraint status acyclic u1 u2 in
+  NCicLibrary.dump_obj status (inject_constraint (acyclic,u1,u2))
 ;;
 
 let eval_ng_tac tac =
+ let just_to_tacstatus_just just text prefix_len =
+    match just with
+    | `Term t -> `Term (text,prefix_len,t)
+    | `Auto (l,params) -> 
+    (
+        match l with
+        | None -> `Auto (None,params)
+        | Some l -> `Auto (Some (List.map (fun t -> (text,prefix_len,t)) l),params)
+    )
+    | _ -> assert false
+ in
  let rec aux f (text, prefix_len, tac) =
   match tac with
   | GrafiteAst.NApply (_loc, t) -> NTactics.apply_tac (text,prefix_len,t) 
@@ -455,6 +492,43 @@ let eval_ng_tac tac =
       NTactics.block_tac (List.map (fun x -> aux f (text,prefix_len,x)) l)
   |GrafiteAst.NRepeat (_,tac) ->
       NTactics.repeat_tac (f f (text, prefix_len, tac))
+  |GrafiteAst.Assume (_,id,t,t1) -> Declarative.assume id (text,prefix_len,t) (match t1 with None ->
+  None | Some t1 -> (Some (text,prefix_len,t1)))
+  |GrafiteAst.Suppose (_,t,id,t1) -> Declarative.suppose (text,prefix_len,t) id (match t1 with None
+  -> None | Some t1 -> (Some (text,prefix_len,t1)))
+  |GrafiteAst.By_just_we_proved (_,j,t1,s,t2) -> Declarative.by_just_we_proved
+  (just_to_tacstatus_just j text prefix_len) (text,prefix_len,t1) s (match t2 with None -> None |
+  Some t2 -> (Some (text,prefix_len,t2)))
+  |GrafiteAst.We_need_to_prove (_, t, id, t2) -> Declarative.we_need_to_prove (text,prefix_len,t) id
+  (match t2 with None -> None | Some t2 -> Some (text,prefix_len,t2))
+  | GrafiteAst.Bydone (_, j) -> Declarative.bydone (just_to_tacstatus_just j text prefix_len)
+  | GrafiteAst.ExistsElim (_, just, id1, t1, t2, id2) ->
+     Declarative.existselim (just_to_tacstatus_just just text prefix_len) id1 (text,prefix_len,t1)
+     (text,prefix_len,t2) id2
+  | GrafiteAst.AndElim(_,just,t1,id1,t2,id2) -> Declarative.andelim (just_to_tacstatus_just just
+    text prefix_len) (text,prefix_len,t1) id1 (text,prefix_len,t2) id2
+  | GrafiteAst.Thesisbecomes (_, t1, t2) -> Declarative.thesisbecomes (text,prefix_len,t1)
+  (match t2 with None -> None | Some t2 -> (Some (text,prefix_len,t2)))
+  | GrafiteAst.RewritingStep (_,rhs,just,cont) ->
+     Declarative.rewritingstep (text,prefix_len,rhs)
+                                (match just with 
+                                `Term t -> just_to_tacstatus_just just text prefix_len
+                                | `Auto params -> just_to_tacstatus_just just text prefix_len
+                                |`Proof -> `Proof
+                                |`SolveWith t -> `SolveWith (text,prefix_len,t)
+                                )
+                                cont
+  | GrafiteAst.Obtain (_,id,t1) ->
+     Declarative.obtain id (text,prefix_len,t1)
+  | GrafiteAst.Conclude (_,t1) ->
+     Declarative.conclude (text,prefix_len,t1)
+  | GrafiteAst.We_proceed_by_cases_on (_, t, t1) ->
+     Declarative.we_proceed_by_cases_on (text,prefix_len,t) (text,prefix_len,t1)
+  | GrafiteAst.We_proceed_by_induction_on (_, t, t1) ->
+     Declarative.we_proceed_by_induction_on (text,prefix_len,t) (text,prefix_len,t1)
+  | GrafiteAst.Byinduction (_, t, id) -> Declarative.byinduction (text,prefix_len,t) id
+  | GrafiteAst.Case (_,id,params) -> Declarative.case id params
+  | GrafiteAst.PrintStack (_) -> Declarative.print_stack
  in
   aux aux tac (* trick for non uniform recursion call *)
 ;;
@@ -523,6 +597,14 @@ let compute_relevance status uri =
       NCic.Inductive (ind,leftno,tys,attrs)
 ;;
 
+let extract_uris status uris =
+ List.fold_left
+  (fun status uri ->
+    let obj = NCicEnvironment.get_checked_obj status uri in
+     let status = eval_extract_obj status obj in
+      eval_extract_ocaml_obj status obj
+  ) status uris
+;;
 
 let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
   match cmd with
@@ -532,15 +614,18 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
      let baseuri = NUri.uri_of_string baseuri in
      (* MATITA 1.0: keep WithoutPreferences? *)
      let alias_only = (mode = GrafiteAst.OnlyPreferences) in
+     let status =
       GrafiteTypes.Serializer.require
-       ~alias_only ~baseuri ~fname:fullpath status
+       ~alias_only ~baseuri ~fname:fullpath status in
+     OcamlExtraction.print_open status
+      (NCicLibrary.get_transitively_included status)
   | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n
   | 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
+           status `XTNone [] [] [] ("",0,o_t) in
        assert( metasenv = [] && subst = []);
        let ty = NCicTypeChecker.typeof status [] [] [] t in
        let source, target =
@@ -561,17 +646,15 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
        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)
+      let cmd = 
+       GrafiteAst.NCoercion (loc, name, compose, Some (t, ty, source, target))
+      in
+      eval_ncommand ~include_paths opts status (text,prefix_len,cmd)
   | 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 status = extract_uris status composites in
      let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *)
      let aliases = GrafiteDisambiguate.aliases_for_objs status composites in
       eval_alias status (mode,aliases)
@@ -611,6 +694,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
         let old_status = status in
         let status = NCicLibrary.add_obj status obj in
         let status = eval_extract_obj status obj in
+        let status = eval_extract_ocaml_obj status obj in
        (try
         let index_obj = index &&
          match obj_kind with
@@ -627,6 +711,9 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
             | _ -> status)
          else
           status in
+        (* purge tinycals stack *)
+        let ninitial_stack = Continuationals.Stack.of_nmetasenv [] in
+        let status = status#set_stack ninitial_stack in
 (*
 	  try 
 	    index_eq uri status
@@ -637,7 +724,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
        (*prerr_endline (status#ppobj obj);*)
            let boxml = NCicElim.mk_elims status obj in
            let boxml = boxml @ NCicElim.mk_projections status obj in
-           let status = status#set_ng_mode `CommandMode in
+	   let status = status#set_ng_mode `CommandMode in
            let xxaliases = GrafiteDisambiguate.aliases_for_objs status [uri] in
            let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *)
            let status = eval_alias status (mode,xxaliases) in
@@ -658,9 +745,11 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
                 else
                   nstatus
                with
-               | MultiPassDisambiguator.DisambiguationError _
+               | MultiPassDisambiguator.DisambiguationError _ ->
+                  HLog.warn "error in disambiguating projection/eliminator";
+                  status
                | NCicTypeChecker.TypeCheckerFailure _ ->
-                  (*HLog.warn "error in generating projection/eliminator";*)
+                  HLog.warn "error in typechecking projection/eliminator";
                   status
              ) status boxml in             
            let _,_,_,_,nobj = obj in
@@ -768,7 +857,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
              (fun status (name,cpos,arity) ->
                try
                  let metasenv,subst,status,t =
-                  GrafiteDisambiguate.disambiguate_nterm status None [] [] []
+                  GrafiteDisambiguate.disambiguate_nterm status `XTNone [] [] []
                    ("",0,NotationPt.Ident (name,None)) in
                  assert (metasenv = [] && subst = []);
                  let status, nuris = 
@@ -776,6 +865,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
                      basic_eval_and_record_ncoercion_from_t_cpos_arity 
                       status (name,true,t,cpos,arity) in
                  let aliases = GrafiteDisambiguate.aliases_for_objs status nuris in
+                 let status = extract_uris status nuris in
                   eval_alias status (mode,aliases)
                with MultiPassDisambiguator.DisambiguationError _-> 
                  HLog.warn ("error in generating coercion: "^name);
@@ -842,14 +932,14 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
       else
         let status = status#set_ng_mode `ProofMode in
         let metasenv,subst,status,indty =
-          GrafiteDisambiguate.disambiguate_nterm status None [] [] [] (text,prefix_len,indty) in
+          GrafiteDisambiguate.disambiguate_nterm status `XTNone [] [] [] (text,prefix_len,indty) in
         let indtyno, (_,_,tys,_,_),leftno = match indty with
             NCic.Const ((NReference.Ref (_,NReference.Ind (_,indtyno,leftno))) as r) ->
               indtyno, NCicEnvironment.get_checked_indtys status r, leftno
           | _ -> prerr_endline ("engine: indty expected... (fix this error message)"); assert false in
         let (_,ind_name,_,_ as it) = List.nth tys indtyno in
         let status,obj =  
-          NDestructTac.mk_discriminator ~use_jmeq:true (ind_name ^ "_jmdiscr")
+          NDestructTac.mk_discriminator ~use_jmeq:true ~force:true (ind_name ^ "_jmdiscr")
            it leftno status status#baseuri in
         let _,_,menv,_,_ = obj in
           (match menv with
@@ -863,7 +953,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
       let metasenv,subst,status,sort = match sort with
         | None -> [],[],status,NCic.Sort NCic.Prop
         | Some s ->
-           GrafiteDisambiguate.disambiguate_nterm status None [] [] []
+           GrafiteDisambiguate.disambiguate_nterm status `XTSort [] [] []
             (text,prefix_len,s) 
       in
       assert (metasenv = []);
@@ -877,7 +967,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
              (status#ppterm ~metasenv ~subst ~context:[] sort))) in
       let status = status#set_ng_mode `ProofMode in
       let metasenv,subst,status,indty =
-       GrafiteDisambiguate.disambiguate_nterm status None [] [] subst
+       GrafiteDisambiguate.disambiguate_nterm status `XTNone [] [] subst
         (text,prefix_len,indty) in
       let indtyno,(_,leftno,tys,_,_) =
        match indty with
@@ -897,8 +987,8 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
             eval_ncommand ~include_paths opts status
              ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false))
         | _ -> assert false)
-  | GrafiteAst.NUnivConstraint (loc,u1,u2) ->
-      eval_add_constraint status [`Type,u1] [`Type,u2]
+  | GrafiteAst.NUnivConstraint (loc,acyclic,u1,u2) ->
+      eval_add_constraint status acyclic [`Type,u1] [`Type,u2]
   (* ex lexicon commands *)
   | GrafiteAst.Interpretation (loc, dsc, (symbol, args), cic_appl_pattern) ->
      let cic_appl_pattern =