INTERFACE_FILES = \
grafiteAstPp.mli \
- grafiteMarshal.mli \
$(NULL)
IMPLEMENTATION_FILES = \
grafiteAst.ml \
+++ /dev/null
-(* Copyright (C) 2005, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-(* $Id$ *)
-
-type ast_command = GrafiteAst.command
-type moo = ast_command list
-
-let format_name = "grafite"
-
-let save_moo_to_file ~fname moo =
- HMarshal.save ~fmt:format_name ~version:GrafiteAst.magic ~fname moo
-
-let load_moo_from_file ~fname =
- let raw = HMarshal.load ~fmt:format_name ~version:GrafiteAst.magic ~fname in
- (raw: moo)
-
-let rehash_cmd_uris =
- function
- | GrafiteAst.Include _ as cmd -> cmd
- | cmd ->
- prerr_endline "Found a command not expected in a .moo:";
- let term_pp _ = assert false in
- let obj_pp _ = assert false in
- prerr_endline (GrafiteAstPp.pp_command cmd);
- assert false
-
-let save_moo ~fname moo = save_moo_to_file ~fname (List.rev moo)
-
-let load_moo ~fname =
- let moo = load_moo_from_file ~fname in
- List.map rehash_cmd_uris moo
-
+++ /dev/null
-(* Copyright (C) 2005, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-type ast_command = GrafiteAst.command
-type moo = ast_command list
-
-val save_moo: fname:string -> moo -> unit
-
- (** @raise Corrupt_moo *)
-val load_moo: fname:string -> moo
-
exception Drop
(* mo file name, ma file name *)
-(*exception IncludedFileNotCompiled of string * string *)
exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro
type 'a disambiguator_input = string * int * 'a
let status,uris =
match cmd with
| GrafiteAst.Include (loc, baseuri) ->
- (*
- let status =
- 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,baseuri))
- in
- eval_from_moo status moopath
- in
- let status = *)
NCicLibrary.Serializer.require ~baseuri:(NUri.uri_of_string baseuri)
- status (*in
- let status =
- GrafiteTypes.add_moo_content
- [GrafiteAst.Include (loc,baseuri)] status
- in
- status,[] *), []
+ status, []
| GrafiteAst.Print (_,_) -> status,[]
| GrafiteAst.Set (loc, name, value) -> status, []
in
| GrafiteAst.NMacro (loc, macro) ->
raise (NMacro (loc,macro))
-and eval_from_moo status fname =
- let ast_of_cmd cmd =
- ("",0,GrafiteAst.Executable (HExtlib.dummy_floc,
- GrafiteAst.Command (HExtlib.dummy_floc,
- cmd)))
- in
- let moo = GrafiteMarshal.load_moo fname in
- List.fold_left
- (fun status ast ->
- let ast = ast_of_cmd ast in
- let status,lemmas =
- eval_ast ~disambiguate_command:(fun status (_,_,cmd) -> status,cmd)
- status ast
- in
- assert (lemmas=[]);
- status)
- status moo
-
and eval_ast ~disambiguate_command ?(do_heavy_checks=false) status
(text,prefix_len,st)
=
*)
exception Drop
-(*exception IncludedFileNotCompiled of string * string*)
exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro
type 'a disambiguator_input = string * int * 'a
NCic.Constant([],"",None,NCic.Implicit `Closed,(`Provided,`Theorem,`Regular))
in
object
- val moo_content_rev = ([] : GrafiteMarshal.moo)
val baseuri = b
val ng_mode = (`CommandMode : [`CommandMode | `ProofMode])
- method moo_content_rev = moo_content_rev
- method set_moo_content_rev v = {< moo_content_rev = v >}
method baseuri = baseuri
method set_baseuri v = {< baseuri = v >}
method ng_mode = ng_mode;
(* Warning: #stack and #obj are meaningful iff #ng_mode is `ProofMode *)
inherit ([Continuationals.Stack.t] NTacStatus.status fake_obj (Continuationals.Stack.empty))
end
-
-let add_moo_content cmds status =
- let content = status#moo_content_rev in
- let content' = cmds@content in
-(* prerr_endline ("new moo content: " ^ String.concat " " (List.map
- GrafiteAstPp.pp_command content')); *)
- status#set_moo_content_rev content'
class status :
string ->
object ('self)
- method moo_content_rev: GrafiteMarshal.moo
- method set_moo_content_rev: GrafiteMarshal.moo -> 'self
method baseuri: string
method set_baseuri: string -> 'self
method ng_mode: [`ProofMode | `CommandMode]
(* Warning: #stack and #obj are meaningful iff #ng_mode is `ProofMode *)
inherit NTacStatus.tac_status
end
-
- (** list is not reversed, head command will be the first emitted *)
-val add_moo_content: GrafiteMarshal.ast_command list -> status -> status
match script#bos, script#eos with
| true, _ -> ()
| _, true ->
- let moo_fname =
- LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri
- ~writable:true in
let lexicon_fname =
LibraryMisc.lexicon_file_of_baseuri
~must_exist:false ~baseuri ~writable:true
in
- GrafiteMarshal.save_moo moo_fname grafite_status#moo_content_rev;
LexiconMarshal.save_lexicon lexicon_fname
grafite_status#lstatus.LexiconEngine.lexicon_content_rev;
NCicLibrary.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
aux_for_dump print_cb grafite_status
in
let elapsed = Unix.time () -. time in
- let moo_content_rev,lexicon_content_rev =
- grafite_status#moo_content_rev,
- grafite_status#lstatus.LexiconEngine.lexicon_content_rev
+ let lexicon_content_rev =
+ grafite_status#lstatus.LexiconEngine.lexicon_content_rev
in
(if Helm_registry.get_bool "matita.moo" then begin
(* FG: we do not generate .moo when dumping .mma files *)
- GrafiteMarshal.save_moo moo_fname moo_content_rev;
LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
NCicLibrary.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
grafite_status#dump
projects / helm.git / commitdiff