X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=c6139e0e574da702d0c95a3a20a41a70e5cfabdc;hb=1589ec067f5f18594dfcab61431adbe095db1bd1;hp=65dd17b6a096c1e144daf7068e80cf49cba2ce2d;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 65dd17b6a..c6139e0e5 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -67,12 +67,10 @@ let tactic_of_ast ast =
   | GrafiteAst.Clear (_,id) -> Tactics.clear id
   | GrafiteAst.ClearBody (_,id) -> Tactics.clearbody id
   | GrafiteAst.Contradiction _ -> Tactics.contradiction
-  | GrafiteAst.Compare (_, term) -> Tactics.compare term
   | GrafiteAst.Constructor (_, n) -> Tactics.constructor n
   | GrafiteAst.Cut (_, ident, term) ->
      let names = match ident with None -> [] | Some id -> [id] in
      Tactics.cut ~mk_fresh_name_callback:(namer_of names) term
-  | GrafiteAst.DecideEquality _ -> Tactics.decide_equality
   | GrafiteAst.Decompose (_, types, what, names) -> 
       let to_type = function
          | GrafiteAst.Type (uri, typeno) -> uri, typeno
@@ -394,11 +392,32 @@ type 'a eval_from_moo =
 let coercion_moo_statement_of uri =
   GrafiteAst.Coercion (HExtlib.dummy_floc, uri, false)
 
+let refinement_toolkit = {
+  RefinementTool.type_of_aux' = 
+    (fun ?localization_tbl e c t u ->
+      let saved = !CicRefine.insert_coercions in 
+      CicRefine.insert_coercions:= false;
+      let rc = 
+        try 
+          let t, ty, metasenv, ugraph = 
+            CicRefine.type_of_aux' ?localization_tbl e c t u in
+          RefinementTool.Success (t, ty, metasenv, ugraph)
+        with
+        | CicRefine.RefineFailure s
+        | CicRefine.Uncertain s 
+        | CicRefine.AssertFailure s -> RefinementTool.Exception s
+      in
+      CicRefine.insert_coercions := saved;
+      rc);
+  RefinementTool.ppsubst = CicMetaSubst.ppsubst;
+  RefinementTool.apply_subst = CicMetaSubst.apply_subst; 
+  RefinementTool.ppmetasenv = CicMetaSubst.ppmetasenv; 
+  RefinementTool.pack_coercion_obj = CicRefine.pack_coercion_obj;
+ }
+  
 let eval_coercion status ~add_composites uri =
- let basedir = Helm_registry.get "matita.basedir" in
  let status,compounds =
-   prerr_endline "evaluating a coercion command";
-  GrafiteSync.add_coercion ~basedir ~add_composites status uri in
+  GrafiteSync.add_coercion ~add_composites refinement_toolkit status uri in
  let moo_content = coercion_moo_statement_of uri in
  let status = GrafiteTypes.add_moo_content [moo_content] status in
   {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
@@ -507,10 +526,11 @@ let add_coercions_of_record_to_moo obj lemmas status =
             | _ -> None) 
           fields
       in
+      (*
       prerr_endline "wanted coercions:";
       List.iter 
         (fun u -> prerr_endline (UriManager.string_of_uri u)) 
-        wanted_coercions;
+        wanted_coercions; *)
       let coercions, moo_content = 
         List.split
           (HExtlib.filter_map 
@@ -523,32 +543,38 @@ let add_coercions_of_record_to_moo obj lemmas status =
                 None) 
             lemmas)
       in
-      prerr_endline "actual coercions:";
+      (* prerr_endline "actual coercions:";
       List.iter 
         (fun u -> prerr_endline (UriManager.string_of_uri u)) 
-        coercions;
+        coercions; *)
       let status = GrafiteTypes.add_moo_content moo_content status in 
       {status with 
         GrafiteTypes.coercions = coercions @ status.GrafiteTypes.coercions}, 
       lemmas
 
 let add_obj uri obj status =
- let basedir = Helm_registry.get "matita.basedir" in
- let status,lemmas = GrafiteSync.add_obj ~basedir uri obj status in
+ let status,lemmas = GrafiteSync.add_obj refinement_toolkit uri obj status in
  status, lemmas 
       
 let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
  let status,cmd = disambiguate_command status cmd in
- let basedir = Helm_registry.get "matita.basedir" in
  let status,uris =
   match cmd with
   | GrafiteAst.Default (loc, what, uris) as cmd ->
      LibraryObjects.set_default what uris;
      GrafiteTypes.add_moo_content [cmd] status,[]
   | GrafiteAst.Include (loc, baseuri) ->
-     let moopath = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in
-     if not (Sys.file_exists moopath) then
-       raise (IncludedFileNotCompiled moopath);
+     let moopath_rw, moopath_r = 
+       LibraryMisc.obj_file_of_baseuri 
+         ~must_exist:false ~baseuri ~writable:true,
+       LibraryMisc.obj_file_of_baseuri 
+         ~must_exist:false ~baseuri ~writable:false
+     in
+     let moopath = 
+       if Sys.file_exists moopath_r then moopath_r else
+         if Sys.file_exists moopath_rw then moopath_rw else
+           raise (IncludedFileNotCompiled moopath_rw)
+     in
      let status = eval_from_moo.efm_go status moopath in
      status,[]
   | GrafiteAst.Set (loc, name, value) -> 
@@ -564,11 +590,17 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
           HLog.error (sprintf "uri %s belongs to a read-only repository" value);
           raise (ReadOnlyUri value)
         end;
-        if not (GrafiteMisc.is_empty value) && opts.clean_baseuri then begin
+        if not (Http_getter_storage.is_empty value) && 
+           opts.clean_baseuri 
+          then begin
           HLog.message ("baseuri " ^ value ^ " is not empty");
           HLog.message ("cleaning baseuri " ^ value);
-          LibraryClean.clean_baseuris ~basedir [value];
+          LibraryClean.clean_baseuris [value];
+          assert (Http_getter_storage.is_empty value);
         end;
+        HExtlib.mkdir 
+          (Filename.dirname (Http_getter.filename ~writable:true (value ^
+            "/foo.con")));
       end;
       GrafiteTypes.set_option status name value,[]
   | GrafiteAst.Drop loc -> raise Drop
@@ -606,8 +638,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
           (match types with (name,_,_,_)::_ -> name | _ -> assert false)
        | _ -> assert false in
      let uri = 
-       UriManager.uri_of_string (GrafiteTypes.qualify status name ^ ext) 
-     in
+       UriManager.uri_of_string (GrafiteTypes.qualify status name ^ ext) in
+     let obj = CicRefine.pack_coercion_obj obj in
      let metasenv = GrafiteTypes.get_proof_metasenv status in
      match obj with
      | Cic.CurrentProof (_,metasenv',bo,ty,_,_) ->
@@ -642,9 +674,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
                  ("Theorem already proved: " ^ UriManager.string_of_uri x ^ 
                   "\nPlease use a variant."));
            end;
-         assert (metasenv = metasenv');
-         let initial_proof = (Some uri, metasenv, bo, ty) in
-         let initial_stack = Continuationals.Stack.of_metasenv metasenv in
+         let initial_proof = (Some uri, metasenv', bo, ty) in
+         let initial_stack = Continuationals.Stack.of_metasenv metasenv' in
          { status with GrafiteTypes.proof_status =
             GrafiteTypes.Incomplete_proof
              { GrafiteTypes.proof = initial_proof; stack = initial_stack } },