From: Enrico Tassi 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