From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 31 Jan 2005 17:29:03 +0000 (+0000)
Subject: added save_object_to_disk and basedir
X-Git-Tag: V_0_1_0~82
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2ae59c483cf9aa1bab99bc9e6449a21f5ccc010b;p=helm.git

added save_object_to_disk and basedir
---

diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml
index 818f7fe94..f52901ea6 100644
--- a/helm/matita/matitaInterpreter.ml
+++ b/helm/matita/matitaInterpreter.ml
@@ -47,6 +47,8 @@ let uri name =
 *)
 
 let baseuri = lazy (ref ("cic:/matita/" ^ Helm_registry.get "matita.owner"))
+let basedir = ref ((Unix.getpwuid (Unix.getuid ())).Unix.pw_dir) ;;
+
 let qualify name =
   let baseuri = !(Lazy.force baseuri) in
   if baseuri.[String.length baseuri - 1] = '/' then
@@ -156,11 +158,21 @@ class sharedState
           console#echo_message (sprintf "base uri is \"%s\""
             !(Lazy.force baseuri));
           Quiet
+      | TacticAst.Command (TacticAst.Basedir (Some path)) ->
+          basedir := path;
+          console#echo_message (sprintf "base dir set to \"%s\"" path);
+          Quiet
+      | TacticAst.Command (TacticAst.Basedir None) ->
+          console#echo_message (sprintf "base dir is \"%s\"" !basedir);
+          Quiet
       | TacticAst.Command (TacticAst.Check term) ->
           let (_, _, term,ugraph) = 
 	    disambiguate ~disambiguator ~currentProof term 
 	  in
           let (context, metasenv) = get_context_and_metasenv currentProof in
+(* this is the Eval Compute
+          let term = CicReduction.whd context term in
+*)         
           let dummyno = CicMkImplicit.new_meta metasenv [] in
           let ty,ugraph1 = 
 	    CicTypeChecker.type_of_aux' metasenv context term ugraph 
@@ -264,6 +276,62 @@ let inddef_of_ast params indTypes (disambiguator:MatitaTypes.disambiguator) =
   let cicIndTypes = List.rev cicIndTypes in
   (UriManager.uri_of_string uri, (cicIndTypes, [], paramsno))
 
+ (* 
+ *
+ *
+ * FIXME this should be in another module, shared with gTopLevel 
+ *
+ *
+ * *)
+let
+ save_object_to_disk uri annobj ids_to_inner_sorts ids_to_inner_types pathname
+=
+ let name =
+  let struri = UriManager.string_of_uri uri in
+  let idx = (String.rindex struri '/') + 1 in
+   String.sub struri idx (String.length struri - idx)
+ in
+  let path = pathname ^ "/" ^ name in
+  let xml, bodyxml =
+   Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:false
+    annobj 
+  in
+  let xmlinnertypes =
+   Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
+    ~ask_dtd_to_the_getter:false
+  in
+   (* innertypes *)
+   let innertypesuri = UriManager.innertypesuri_of_uri uri in
+    Xml.pp ~quiet:true xmlinnertypes (Some (path ^ ".types.xml")) ;
+    Http_getter.register' innertypesuri
+     (Helm_registry.get "local_library.url" ^
+       Str.replace_first (Str.regexp "^cic:") ""
+        (UriManager.string_of_uri innertypesuri) ^ ".xml"
+     ) ;
+    (* constant type / variable / mutual inductive types definition *)
+    Xml.pp ~quiet:true xml (Some (path ^ ".xml")) ;
+    Http_getter.register' uri
+     (Helm_registry.get "local_library.url" ^
+       Str.replace_first (Str.regexp "^cic:") ""
+        (UriManager.string_of_uri uri) ^ ".xml"
+     ) ;
+    match bodyxml with
+       None -> ()
+     | Some bodyxml' ->
+        (* constant body *)
+        let bodyuri =
+         match UriManager.bodyuri_of_uri uri with
+            None -> assert false
+          | Some bodyuri -> bodyuri
+        in
+         Xml.pp ~quiet:true bodyxml' (Some (path ^ ".body.xml")) ;
+         Http_getter.register' bodyuri
+          (Helm_registry.get "local_library.url" ^
+            Str.replace_first (Str.regexp "^cic:") ""
+             (UriManager.string_of_uri bodyuri) ^ ".xml"
+          )
+;;
+
   (* TODO Zack a lot more to be done here:
     * - save object to disk in xml format
     * - register uri to the getter