*)
let baseuri = lazy (ref ("cic:/matita/" ^ Helm_registry.get "matita.owner"))
-let basedir = ref ((Unix.getpwuid (Unix.getuid ())).Unix.pw_dir) ;;
+let basedir = lazy (ref (Helm_registry.get "matita.basedir"))
let qualify name =
let baseuri = !(Lazy.force baseuri) in
val dbd = MatitaMisc.dbd_instance ()
val currentProof = MatitaProof.instance ()
+ val disambiguator = MatitaDisambiguator.instance ()
(** eval a toplevel phrase in the current state and return the new state
*)
(** Implements phrases that should be accepted in all states *)
class sharedState
- ~(disambiguator: MatitaTypes.disambiguator)
~(console: #MatitaTypes.console)
?(mathViewer: MatitaTypes.mathViewer option)
()
!(Lazy.force baseuri));
Quiet
| TacticAst.Command (TacticAst.Basedir (Some path)) ->
- basedir := path;
+ Lazy.force 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);
+ console#echo_message (sprintf "base dir is \"%s\""
+ !(Lazy.force basedir));
Quiet
| TacticAst.Command (TacticAst.Check term) ->
let (_, _, term,ugraph) =
let cicIndTypes = List.rev cicIndTypes in
(UriManager.uri_of_string uri, (cicIndTypes, [], paramsno))
-let
- save_object_to_disk uri obj
-=
+let save_object_to_disk uri obj =
let ensure_path_exists path =
let dir = Filename.dirname path in
try
let annobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ =
Cic2acic.acic_object_of_cic_object ~eta_fix:false obj
in
-
(* prepare XML *)
let xml, bodyxml =
Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:false
Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
~ask_dtd_to_the_getter:false
in
-
(* prepare URIs and paths *)
let innertypesuri = UriManager.innertypesuri_of_uri uri in
let bodyuri = UriManager.bodyuri_of_uri uri in
let innertypesfilename = Str.replace_first (Str.regexp "^cic:") ""
(UriManager.string_of_uri innertypesuri) ^ ".xml" in
- let innertypespath = !basedir ^ "/" ^ innertypesfilename in
- let xmlfilename = Str.replace_first (Str.regexp "^cic:") ""
+ let innertypespath = !(Lazy.force basedir) ^ "/" ^ innertypesfilename in
+ let xmlfilename = Str.replace_first (Str.regexp "^cic:/") ""
(UriManager.string_of_uri uri) ^ ".xml" in
- let xmlpath = !basedir ^ "/" ^ xmlfilename in
- let xmlbodyfilename = Str.replace_first (Str.regexp "^cic:") ""
+ let xmlpath = !(Lazy.force basedir) ^ "/" ^ xmlfilename in
+ let xmlbodyfilename = Str.replace_first (Str.regexp "^cic:/") ""
(UriManager.string_of_uri uri) ^ ".body.xml" in
- let xmlbodypath = !basedir ^ "/" ^ xmlbodyfilename in
- let path_scheme_of path = "file:/" ^ path in
-
+ let xmlbodypath = !(Lazy.force basedir) ^ "/" ^ xmlbodyfilename in
+ let path_scheme_of path = "file://" ^ path in
+ MatitaMisc.mkdirs (List.map Filename.dirname [innertypespath; xmlpath]);
(* now write to disk *)
ensure_path_exists innertypespath;
Xml.pp ~quiet:true xmlinnertypes (Some innertypespath) ;
ensure_path_exists xmlpath;
Xml.pp ~quiet:true xml (Some xmlpath) ;
-
(* now register to the getter *)
Http_getter.register' innertypesuri (path_scheme_of innertypespath);
Http_getter.register' uri (path_scheme_of xmlpath);
-
(* now the optional body, both write and register *)
(match bodyxml,bodyuri with
None,None -> ()
Xml.pp ~quiet:true bodyxml (Some xmlbodypath) ;
Http_getter.register' bodyuri (path_scheme_of xmlbodypath)
| _-> assert false)
-;;
-
-
- (* TODO Zack a lot more to be done here:
- * - save object to disk in xml format
- * - register uri to the getter
+ (* TODO ZACK a lot more to be done here:
* - save universe file *)
let add_constant_to_world ~(console: #MatitaTypes.console)
~dbd ~uri ?body ~ty ?(params = []) ?(attrs = []) ~ugraph ()
let obj = Cic.Constant (name, body, ty, params, attrs) in
let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in
CicEnvironment.add_type_checked_term uri (obj, ugraph);
- MetadataDb.index_constant ~dbd
- ~owner:(Helm_registry.get "matita.owner") ~uri ~body ~ty;
+ MetadataDb.index_constant ~dbd ~uri ~body ~ty;
save_object_to_disk uri obj;
console#echo_message (sprintf "%s constant defined" suri)
end
let obj = Cic.InductiveDefinition (indTypes, params, leftno, attrs) in
let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in
CicEnvironment.put_inductive_definition uri (obj, ugraph);
- MetadataDb.index_inductive_def ~dbd
- ~owner:(Helm_registry.get "matita.owner") ~uri ~types:indTypes;
+ MetadataDb.index_inductive_def ~dbd ~uri ~types:indTypes;
save_object_to_disk uri obj;
console#echo_message (sprintf "%s inductive type defined" suri);
let elim sort =
end
(** Implements phrases that should be accepted only in Command state *)
-class commandState
- ~(disambiguator: MatitaTypes.disambiguator)
- ~(console: #MatitaTypes.console)
- ?mathViewer
- ()
-=
- let shared = new sharedState ~disambiguator ~console ?mathViewer () in
+class commandState ~(console: #MatitaTypes.console) ?mathViewer () =
+ let shared = new sharedState ~console ?mathViewer () in
object (self)
inherit interpreterState ~console
(** Implements phrases that should be accepted only in Proof state, basically
* tacticals *)
-class proofState
- ~(disambiguator: MatitaTypes.disambiguator)
- ~(console: #MatitaTypes.console)
- ?mathViewer
- ()
-=
- let shared = new sharedState ~disambiguator ~console ?mathViewer () in
+class proofState ~(console: #MatitaTypes.console) ?mathViewer () =
+ let shared = new sharedState ~console ?mathViewer () in
object (self)
inherit interpreterState ~console
| tactical -> shared#evalTactical tactical
end
-class interpreter
- ~(disambiguator: MatitaTypes.disambiguator)
- ~(console: #MatitaTypes.console)
- ?mathViewer
- ()
-=
- let commandState = new commandState ~disambiguator ~console ?mathViewer () in
- let proofState = new proofState ~disambiguator ~console ?mathViewer () in
+class interpreter ~(console: #MatitaTypes.console) ?mathViewer () =
+ let commandState = new commandState ~console ?mathViewer () in
+ let proofState = new proofState ~console ?mathViewer () in
object (self)
val mutable state = commandState
method evalAst ast = self#eval (fun () -> state#evalAst ast)
end
-let interpreter
- ~(disambiguator: MatitaTypes.disambiguator)
- ~(console: #MatitaTypes.console)
- ?mathViewer
- ()
-=
- new interpreter ~disambiguator ~console ?mathViewer ()
+let interpreter ~(console: #MatitaTypes.console) ?mathViewer () =
+ new interpreter ~console ?mathViewer ()
projects / helm.git / blobdiff