* marshalling *)
let magic = 35
+(* composed magic: term + command magics. No need to change this value *)
+let magic = magic + 10000 * NotationPt.magic
+
type command =
- | Include of loc * string * unit * string
| Set of loc * string * string
| Print of loc * string
+type alias_spec =
+ | Ident_alias of string * string (* identifier, uri *)
+ | Symbol_alias of string * int * string (* name, instance no, description *)
+ | Number_alias of int * string (* instance no, description *)
+
+type inclusion_mode = WithPreferences | WithoutPreferences (* aka aliases *)
+
type ncommand =
+ | Include of loc * inclusion_mode * string (* _,buri,_,path *)
| UnificationHint of loc * NotationPt.term * int (* term, precedence *)
| NObj of loc * NotationPt.term NotationPt.obj
| NDiscriminator of loc * NotationPt.term
NotationPt.term * NotationPt.term *
(string * NotationPt.term) * NotationPt.term
| NQed of loc
+ (* ex lexicon commands *)
+ | Alias of loc * alias_spec
+ (** parameters, name, type, fields *)
+ | Notation of loc * direction option * NotationPt.term * Gramext.g_assoc *
+ int * NotationPt.term
+ (* direction, l1 pattern, associativity, precedence, l2 pattern *)
+ | Interpretation of loc *
+ string * (string * NotationPt.argument_pattern list) *
+ NotationPt.cic_appl_pattern
+ (* description (i.e. id), symbol, arg pattern, appl pattern *)
type code =
| Command of loc * command
type statement =
| Executable of loc * code
| Comment of loc * comment
+
+let description_of_alias =
+ function
+ Ident_alias (_,desc)
+ | Symbol_alias (_,_,desc)
+ | Number_alias (_,desc) -> desc
(* $Id$ *)
open GrafiteAst
+open Printf
let tactical_terminator = ""
let tactic_terminator = tactical_terminator
| Screenshot (_, name) -> Printf.sprintf "screenshot \"%s\"" name
;;
+let pp_l1_pattern = NotationPp.pp_term
+let pp_l2_pattern = NotationPp.pp_term
+
+let pp_alias = function
+ | Ident_alias (id, uri) -> sprintf "alias id \"%s\" = \"%s\"." id uri
+ | Symbol_alias (symb, instance, desc) ->
+ sprintf "alias symbol \"%s\" %s= \"%s\"."
+ symb
+ (if instance=0 then "" else "(instance "^ string_of_int instance ^ ") ")
+ desc
+ | Number_alias (instance,desc) ->
+ sprintf "alias num (instance %d) = \"%s\"." instance desc
+
+let pp_associativity = function
+ | Gramext.LeftA -> "left associative"
+ | Gramext.RightA -> "right associative"
+ | Gramext.NonA -> "non associative"
+
+let pp_precedence i = sprintf "with precedence %d" i
+
+let pp_argument_pattern = function
+ | NotationPt.IdentArg (eta_depth, name) ->
+ let eta_buf = Buffer.create 5 in
+ for i = 1 to eta_depth do
+ Buffer.add_string eta_buf "\\eta."
+ done;
+ sprintf "%s%s" (Buffer.contents eta_buf) name
+
+let pp_interpretation dsc symbol arg_patterns cic_appl_pattern =
+ sprintf "interpretation \"%s\" '%s %s = %s."
+ dsc symbol
+ (String.concat " " (List.map pp_argument_pattern arg_patterns))
+ (NotationPp.pp_cic_appl_pattern cic_appl_pattern)
+
+let pp_dir_opt = function
+ | None -> ""
+ | Some `LeftToRight -> "> "
+ | Some `RightToLeft -> "< "
+
+let pp_notation dir_opt l1_pattern assoc prec l2_pattern =
+ sprintf "notation %s\"%s\" %s %s for %s."
+ (pp_dir_opt dir_opt)
+ (pp_l1_pattern l1_pattern)
+ (pp_associativity assoc)
+ (pp_precedence prec)
+ (pp_l2_pattern l2_pattern)
+
let pp_ncommand = function
| UnificationHint (_,t, n) ->
"unification hint " ^ string_of_int n ^ " " ^ NotationPp.pp_term t
(List.map
(fun (a,b) -> NUri.string_of_uri a ^ " ↦ " ^ NUri.string_of_uri b)
map)
+ | Include (_,mode,path) -> (* not precise, since path is absolute *)
+ if mode = WithPreferences then
+ "include \"" ^ path ^ "\"."
+ else
+ "include' \"" ^ path ^ "\"."
+ | Alias (_,s) -> pp_alias s
+ | Interpretation (_, dsc, (symbol, arg_patterns), cic_appl_pattern) ->
+ pp_interpretation dsc symbol arg_patterns cic_appl_pattern
+ | Notation (_, dir_opt, l1_pattern, assoc, prec, l2_pattern) ->
+ pp_notation dir_opt l1_pattern assoc prec l2_pattern
;;
let pp_command = function
- | Include (_,path,_,_) -> "include \"" ^ path ^ "\""
| Print (_,s) -> "print " ^ s
| Set (_, name, value) -> Printf.sprintf "set \"%s\" \"%s\"" name value
val pp_executable: map_unicode_to_tex:bool -> GrafiteAst.code -> string
+val pp_alias: GrafiteAst.alias_spec -> string
+
val pp_statement: GrafiteAst.statement -> map_unicode_to_tex:bool -> string
(* $Id$ *)
-exception Drop
(* mo file name, ma file name *)
exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro
;;
-let rec eval_ncommand opts status (text,prefix_len,cmd) =
+let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
match cmd with
+ | GrafiteAst.Include (loc, mode, fname) ->
+ let _root, baseuri, _fullpath, _rrelpath =
+ Librarian.baseuri_of_script ~include_paths fname in
+ let status,obj =
+ GrafiteTypes.Serializer.require ~baseuri:(NUri.uri_of_string baseuri)
+ status in
+ let status = status#set_dump (obj::status#dump) in
+ assert false (* mode must be passed to GrafiteTypes.Serializer.require
+ somehow *)
+ status,[]
| GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n
| GrafiteAst.NCoercion (loc, name, t, ty, source, target) ->
NCicCoercDeclaration.eval_ncoercion status name t ty source target
(fun (status,uris) boxml ->
try
let nstatus,nuris =
- eval_ncommand opts status
+ eval_ncommand ~include_paths opts status
("",0,GrafiteAst.NObj (HExtlib.dummy_floc,boxml))
in
if nstatus#ng_mode <> `CommandMode then
is_ind it leftno outsort status status#baseuri in
let _,_,menv,_,_ = invobj in
fst (match menv with
- [] -> eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+ [] -> eval_ncommand ~include_paths opts status
+ ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
| _ -> status,[]))
(* XXX *)
with _ -> (*HLog.warn "error in generating inversion principle"; *)
let status = status#set_stack ninitial_stack in
let status = subst_metasenv_and_fix_names status in
let status = status#set_ng_mode `ProofMode in
- eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+ eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
| GrafiteAst.NObj (loc,obj) ->
if status#ng_mode <> `CommandMode then
raise (GrafiteTypes.Command_error "Not in command mode")
let status = status#set_ng_mode `ProofMode in
(match nmenv with
[] ->
- eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+ eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
| _ -> status,[])
| GrafiteAst.NDiscriminator (_,_) -> assert false (*(loc, indty) ->
if status#ng_mode <> `CommandMode then
let status,obj = NDestructTac.mk_discriminator it status in
let _,_,menv,_,_ = obj in
(match menv with
- [] -> eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+ [] -> eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
| _ -> prerr_endline ("Discriminator: non empty metasenv");
status, []) *)
| GrafiteAst.NInverter (loc, name, indty, selection, sort) ->
let _,_,menv,_,_ = obj in
(match menv with
[] ->
- eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+ eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
| _ -> assert false)
| GrafiteAst.NUnivConstraint (loc,u1,u2) ->
eval_add_constraint status [`Type,u1] [`Type,u2]
+ (* ex lexicon commands *)
+ | GrafiteAst.Interpretation (loc, dsc, (symbol, args), cic_appl_pattern) ->
+ let rec disambiguate =
+ function
+ NotationPt.ApplPattern l ->
+ NotationPt.ApplPattern (List.map disambiguate l)
+ | NotationPt.VarPattern id
+ when not
+ (List.exists
+ (function (NotationPt.IdentArg (_,id')) -> id'=id) args)
+ ->
+ let item = DisambiguateTypes.Id id in
+ begin try
+ match DisambiguateTypes.Environment.find item status#lstatus.LexiconTypes.aliases with
+ GrafiteAst.Ident_alias (_, uri) ->
+ NotationPt.NRefPattern (NReference.reference_of_string uri)
+ | _ -> assert false
+ with Not_found ->
+ prerr_endline
+ ("LexiconEngine.eval_command: domain item not found: " ^
+ (DisambiguateTypes.string_of_domain_item item));
+ LexiconEngine.dump_aliases prerr_endline "" status;
+ raise
+ (Failure
+ ((DisambiguateTypes.string_of_domain_item item) ^ " not found"))
+ end
+ | p -> p
+ in
+ let cic_appl_pattern = disambiguate cic_appl_pattern in
+ let status =
+ Interpretations.add_interpretation status
+ dsc (symbol, args) cic_appl_pattern in
+ let mode = assert false in (* VEDI SOTTO *)
+ let diff =
+ [DisambiguateTypes.Symbol (symbol, 0),
+ GrafiteAst.Symbol_alias (symbol,0,dsc)] in
+ let status = LexiconEngine.set_proof_aliases status mode diff in
+ assert false (* MANCA SALVATAGGIO SU DISCO CHE DEVE TENERE IN CONTO
+ IL MODE WithPreference/WithOutPreferences*)
+ | GrafiteAst.Notation (loc, dir, l1, associativity, precedence, l2) ->
+ let l1 =
+ CicNotationParser.check_l1_pattern
+ l1 (dir = Some `RightToLeft) precedence associativity
+ in
+ let status =
+ if dir <> Some `RightToLeft then
+ CicNotationParser.extend status l1
+ (fun env loc ->
+ NotationPt.AttributedTerm
+ (`Loc loc,TermContentPres.instantiate_level2 env l2))
+ else status
+ in
+ let status =
+ if dir <> Some `LeftToRight then
+ let status = TermContentPres.add_pretty_printer status l2 l1 in
+ status
+ else
+ status
+ in
+ assert false (* MANCA SALVATAGGIO SU DISCO *)
+ status
+ | GrafiteAst.Alias (loc, spec) ->
+ let diff =
+ (*CSC: Warning: this code should be factorized with the corresponding
+ code in DisambiguatePp *)
+ match spec with
+ | GrafiteAst.Ident_alias (id,uri) ->
+ [DisambiguateTypes.Id id,spec]
+ | GrafiteAst.Symbol_alias (symb, instance, desc) ->
+ [DisambiguateTypes.Symbol (symb,instance),spec]
+ | GrafiteAst.Number_alias (instance,desc) ->
+ [DisambiguateTypes.Num instance,spec]
+ in
+ let mode = assert false in (* VEDI SOPRA *)
+ LexiconEngine.set_proof_aliases status mode diff;
+ assert false (* MANCA SALVATAGGIO SU DISCO *)
;;
let eval_comment opts status (text,prefix_len,c) = status, []
let rec eval_command opts status (text,prefix_len,cmd) =
let status,uris =
match cmd with
- | GrafiteAst.Include (loc, fname, mode, _) ->
- let include_paths = assert false in
- let never_include = assert false in
- let mode = assert false in
- let baseuri = assert false in
- let status =
- let _root, buri, fullpath, _rrelpath =
- Librarian.baseuri_of_script ~include_paths fname in
- if never_include then raise (GrafiteParser.NoInclusionPerformed fullpath)
- else
- LexiconEngine.eval_command status (LexiconAst.Include (loc,buri,mode,fullpath))
- in
- let status,obj =
- GrafiteTypes.Serializer.require ~baseuri:(NUri.uri_of_string baseuri)
- status in
- let status = status#set_dump (obj::status#dump) in
- status,[]
| GrafiteAst.Print (_,_) -> status,[]
| GrafiteAst.Set (loc, name, value) -> status, []
in
status,uris
-and eval_executable opts status (text,prefix_len,ex) =
+and eval_executable ~include_paths opts status (text,prefix_len,ex) =
match ex with
| GrafiteAst.NTactic (_(*loc*), tacl) ->
if status#ng_mode <> `ProofMode then
| GrafiteAst.Command (_, cmd) ->
eval_command opts status (text,prefix_len,cmd)
| GrafiteAst.NCommand (_, cmd) ->
- eval_ncommand opts status (text,prefix_len,cmd)
+ eval_ncommand ~include_paths opts status (text,prefix_len,cmd)
| GrafiteAst.NMacro (loc, macro) ->
raise (NMacro (loc,macro))
-and eval_ast ?(do_heavy_checks=false) status (text,prefix_len,st) =
+and eval_ast ~include_paths ?(do_heavy_checks=false) status (text,prefix_len,st)
+=
let opts = { do_heavy_checks = do_heavy_checks ; } in
match st with
| GrafiteAst.Executable (_,ex) ->
- eval_executable opts status (text,prefix_len,ex)
+ eval_executable ~include_paths opts status (text,prefix_len,ex)
| GrafiteAst.Comment (_,c) ->
eval_comment opts status (text,prefix_len,c)
;;
* http://helm.cs.unibo.it/
*)
-exception Drop
exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro
type 'a disambiguator_input = string * int * 'a
val eval_ast :
+ include_paths:string list ->
?do_heavy_checks:bool ->
GrafiteTypes.status ->
GrafiteAst.statement disambiguator_input ->
inherit ([Continuationals.Stack.t] NTacStatus.status fake_obj (Continuationals.Stack.empty))
inherit NCicLibrary.dumpable_status
inherit NCicLibrary.status
+ inherit GrafiteParser.status
val baseuri = b
val ng_mode = (`CommandMode : [`CommandMode | `ProofMode])
method baseuri = baseuri
inherit NTacStatus.tac_status
inherit NCicLibrary.dumpable_status
inherit NCicLibrary.status
+ inherit GrafiteParser.status
method baseuri: string
method set_baseuri: string -> 'self
method ng_mode: [`ProofMode | `CommandMode]
grafiteParser.cmi:
cicNotation2.cmi:
grafiteDisambiguate.cmi:
-print_grammar.cmi:
+print_grammar.cmi: grafiteParser.cmi
dependenciesParser.cmo: dependenciesParser.cmi
dependenciesParser.cmx: dependenciesParser.cmi
grafiteParser.cmo: grafiteParser.cmi
grafiteParser.cmx: grafiteParser.cmi
-cicNotation2.cmo: grafiteParser.cmi cicNotation2.cmi
-cicNotation2.cmx: grafiteParser.cmx cicNotation2.cmi
+cicNotation2.cmo: cicNotation2.cmi
+cicNotation2.cmx: cicNotation2.cmi
grafiteDisambiguate.cmo: grafiteDisambiguate.cmi
grafiteDisambiguate.cmx: grafiteDisambiguate.cmi
print_grammar.cmo: print_grammar.cmi
(** @param fname file from which load notation *)
val load_notation:
- #LexiconEngine.status as 'status -> include_paths:string list -> string ->
+ #LexiconTypes.status as 'status -> include_paths:string list -> string ->
'status
class type g_status =
object
- inherit LexiconEngine.g_status
+ inherit LexiconTypes.g_status
inherit NCicCoercion.g_status
end
class status =
object (self)
- inherit LexiconEngine.status
+ inherit LexiconTypes.status
inherit NCicCoercion.status
method set_grafite_disambiguate_status
: 'status. #g_status as 'status -> 'self
let __Closed_Implicit = "__Closed_Implicit__"
let ncic_mk_choice status = function
- | LexiconAst.Symbol_alias (name, _, dsc) ->
+ | GrafiteAst.Symbol_alias (name, _, dsc) ->
if name = __Implicit then
dsc, `Sym_interp (fun _ -> NCic.Implicit `Term)
else if name = __Closed_Implicit then
(NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l)
~term_of_nref:(fun nref -> NCic.Const nref)
name dsc
- | LexiconAst.Number_alias (_, dsc) ->
+ | GrafiteAst.Number_alias (_, dsc) ->
let desc,f = DisambiguateChoices.nlookup_num_by_dsc dsc in
desc, `Num_interp
(fun num -> match f with `Num_interp f -> f num | _ -> assert false)
- | LexiconAst.Ident_alias (name, uri) ->
+ | GrafiteAst.Ident_alias (name, uri) ->
uri, `Sym_interp
(fun l->assert(l = []);
let nref = NReference.reference_of_string uri in
let mk_implicit b =
match b with
| false ->
- LexiconAst.Symbol_alias (__Implicit,-1,"Fake Implicit")
+ GrafiteAst.Symbol_alias (__Implicit,-1,"Fake Implicit")
| true ->
- LexiconAst.Symbol_alias (__Closed_Implicit,-1,"Fake Closed Implicit")
+ GrafiteAst.Symbol_alias (__Closed_Implicit,-1,"Fake Closed Implicit")
;;
let nlookup_in_library
(try
let references = NCicLibrary.resolve id in
List.map
- (fun u -> LexiconAst.Ident_alias (id,NReference.string_of_reference u)
+ (fun u -> GrafiteAst.Ident_alias (id,NReference.string_of_reference u)
) references
with
NCicEnvironment.ObjectNotFound _ -> [])
DisambiguateTypes.Symbol (_,n) ->
List.map
(function
- LexiconAst.Symbol_alias (s,_,d) -> LexiconAst.Symbol_alias (s,n,d)
+ GrafiteAst.Symbol_alias (s,_,d) -> GrafiteAst.Symbol_alias (s,n,d)
| _ -> assert false
) l
| DisambiguateTypes.Num n ->
List.map
(function
- LexiconAst.Number_alias (_,d) -> LexiconAst.Number_alias (n,d)
+ GrafiteAst.Number_alias (_,d) -> GrafiteAst.Number_alias (n,d)
| _ -> assert false
) l
| DisambiguateTypes.Id _ -> l
singleton "first"
(NCicDisambiguate.disambiguate_term
~rdb:estatus
- ~aliases:estatus#lstatus.LexiconEngine.aliases
+ ~aliases:estatus#lstatus.LexiconTypes.aliases
~expty
- ~universe:(Some estatus#lstatus.LexiconEngine.multi_aliases)
+ ~universe:(Some estatus#lstatus.LexiconTypes.multi_aliases)
~lookup_in_library:nlookup_in_library
~mk_choice:(ncic_mk_choice estatus)
~mk_implicit ~fix_instance
- ~description_of_alias:LexiconAst.description_of_alias
+ ~description_of_alias:GrafiteAst.description_of_alias
~context ~metasenv ~subst thing)
in
- let estatus = LexiconEngine.set_proof_aliases estatus diff in
+ let estatus =
+ LexiconEngine.set_proof_aliases estatus GrafiteAst.WithPreferences diff
+ in
metasenv, subst, estatus, cic
;;
singleton "third"
(NCicDisambiguate.disambiguate_obj
~lookup_in_library:nlookup_in_library
- ~description_of_alias:LexiconAst.description_of_alias
+ ~description_of_alias:GrafiteAst.description_of_alias
~mk_choice:(ncic_mk_choice estatus)
~mk_implicit ~fix_instance
~uri
~rdb:estatus
- ~aliases:estatus#lstatus.LexiconEngine.aliases
- ~universe:(Some estatus#lstatus.LexiconEngine.multi_aliases)
+ ~aliases:estatus#lstatus.LexiconTypes.aliases
+ ~universe:(Some estatus#lstatus.LexiconTypes.multi_aliases)
(text,prefix_len,obj)) in
- let estatus = LexiconEngine.set_proof_aliases estatus diff in
+ let estatus = LexiconEngine.set_proof_aliases estatus
+ GrafiteAst.WithPreferences diff in
estatus, cic
;;
class type g_status =
object
- inherit LexiconEngine.g_status
+ inherit LexiconTypes.g_status
inherit NCicCoercion.g_status
end
class status :
object ('self)
- inherit LexiconEngine.status
+ inherit LexiconTypes.status
inherit NCicCoercion.status
method set_grafite_disambiguate_status: #g_status -> 'self
end
val disambiguate_npattern:
GrafiteAst.npattern Disambiguate.disambiguator_input -> pattern
-
-
module N = NotationPt
module G = GrafiteAst
-module L = LexiconAst
module LE = LexiconEngine
-exception NoInclusionPerformed of string (* full path *)
-
type 'a localized_option =
LSome of 'a
| LNone of G.loc
if (try ignore (NReference.reference_of_string uri); true
with NReference.IllFormedReference _ -> false)
then
- L.Ident_alias (id, uri)
+ G.Ident_alias (id, uri)
else
raise
(HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
let instance =
match instance with Some i -> i | None -> 0
in
- L.Symbol_alias (symbol, instance, dsc)
+ G.Symbol_alias (symbol, instance, dsc)
| IDENT "num";
instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
SYMBOL "="; dsc = QSTRING ->
let instance =
match instance with Some i -> i | None -> 0
in
- L.Number_alias (instance, dsc)
+ G.Number_alias (instance, dsc)
]
];
argument: [
include_command: [ [
IDENT "include" ; path = QSTRING ->
- loc,path,true,L.WithPreferences
- | IDENT "include" ; IDENT "source" ; path = QSTRING ->
- loc,path,false,L.WithPreferences
+ loc,path,G.WithPreferences
| IDENT "include'" ; path = QSTRING ->
- loc,path,true,L.WithoutPreferences
+ loc,path,G.WithoutPreferences
]];
grafite_ncommand: [ [
lexicon_command: [ [
IDENT "alias" ; spec = alias_spec ->
- L.Alias (loc, spec)
+ G.Alias (loc, spec)
| IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
- L.Notation (loc, dir, l1, assoc, prec, l2)
+ G.Notation (loc, dir, l1, assoc, prec, l2)
| IDENT "interpretation"; id = QSTRING;
(symbol, args, l3) = interpretation ->
- L.Interpretation (loc, id, (symbol, args), l3)
+ G.Interpretation (loc, id, (symbol, args), l3)
]];
executable: [
[ ncmd = grafite_ncommand; SYMBOL "." -> G.NCommand (loc, ncmd)
];
statement: [
[ ex = executable ->
- LSome (G.Executable (loc, ex))
+ LSome (G.Executable (loc, ex))
| com = comment ->
- LSome (G.Comment (loc, com))
- | (iloc,fname,normal,mode) = include_command ; SYMBOL "." ->
- LSome (G.Executable
- (loc,G.Command (loc,G.Include (iloc,fname,(),""))))
+ LSome (G.Comment (loc, com))
+ | (iloc,fname,mode) = include_command ; SYMBOL "." ->
+ LSome (G.Executable (loc,G.NCommand (loc,G.Include (iloc,mode,fname))))
| scom = lexicon_command ; SYMBOL "." ->
assert false
(*
- fun ?(never_include=false) ~include_paths status ->
let status = LE.eval_command status scom in
status, LNone loc
*)
class type g_status =
object
- inherit LexiconEngine.g_status
+ inherit LexiconTypes.g_status
method parser_db: db
end
let lstatus = assert false in
let grammar = CicNotationParser.level2_ast_grammar lstatus in
object
- inherit LexiconEngine.status
+ inherit LexiconTypes.status
val db =
mk_parser (Grammar.Entry.create grammar "statement") lstatus
method parser_db = db
type ast_statement = GrafiteAst.statement
-exception NoInclusionPerformed of string (* full path *)
-
type db
class type g_status =
object
- inherit LexiconEngine.g_status
+ inherit LexiconTypes.g_status
method parser_db: db
end
class status :
object('self)
- inherit LexiconEngine.status
+ inherit LexiconTypes.status
method parser_db : db
method set_parser_db : db -> 'self
method set_parser_status : 'status. #g_status as 'status -> 'self
-lexiconAstPp.cmi: lexiconAst.cmo
-lexiconMarshal.cmi: lexiconAst.cmo
-cicNotation.cmi: lexiconAst.cmo
-lexiconEngine.cmi: lexiconMarshal.cmi lexiconAst.cmo cicNotation.cmi
-lexiconSync.cmi: lexiconEngine.cmi lexiconAst.cmo
-lexiconAst.cmo:
-lexiconAst.cmx:
-lexiconAstPp.cmo: lexiconAst.cmo lexiconAstPp.cmi
-lexiconAstPp.cmx: lexiconAst.cmx lexiconAstPp.cmi
-lexiconMarshal.cmo: lexiconAstPp.cmi lexiconAst.cmo lexiconMarshal.cmi
-lexiconMarshal.cmx: lexiconAstPp.cmx lexiconAst.cmx lexiconMarshal.cmi
-cicNotation.cmo: lexiconAst.cmo cicNotation.cmi
-cicNotation.cmx: lexiconAst.cmx cicNotation.cmi
-lexiconEngine.cmo: lexiconMarshal.cmi lexiconAstPp.cmi lexiconAst.cmo \
- cicNotation.cmi lexiconEngine.cmi
-lexiconEngine.cmx: lexiconMarshal.cmx lexiconAstPp.cmx lexiconAst.cmx \
- cicNotation.cmx lexiconEngine.cmi
-lexiconSync.cmo: lexiconEngine.cmi lexiconAst.cmo lexiconSync.cmi
-lexiconSync.cmx: lexiconEngine.cmx lexiconAst.cmx lexiconSync.cmi
+lexiconTypes.cmi:
+lexiconEngine.cmi: lexiconTypes.cmi
+lexiconSync.cmi: lexiconTypes.cmi
+lexiconTypes.cmo: lexiconTypes.cmi
+lexiconTypes.cmx: lexiconTypes.cmi
+lexiconEngine.cmo: lexiconTypes.cmi lexiconEngine.cmi
+lexiconEngine.cmx: lexiconTypes.cmx lexiconEngine.cmi
+lexiconSync.cmo: lexiconTypes.cmi lexiconEngine.cmi lexiconSync.cmi
+lexiconSync.cmx: lexiconTypes.cmx lexiconEngine.cmx lexiconSync.cmi
PREDICATES =
INTERFACE_FILES = \
- lexiconAstPp.mli \
- lexiconMarshal.mli \
- cicNotation.mli \
- lexiconEngine.mli \
+ lexiconTypes.mli \
+ lexiconEngine.mli \
lexiconSync.mli \
$(NULL)
IMPLEMENTATION_FILES = \
- lexiconAst.ml \
$(INTERFACE_FILES:%.mli=%.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$ *)
-
-open LexiconAst
-
-class type g_status =
- object ('self)
- inherit Interpretations.g_status
- inherit TermContentPres.g_status
- inherit CicNotationParser.g_status
- end
-
-class status =
- object (self)
- inherit Interpretations.status
- inherit TermContentPres.status
- inherit CicNotationParser.status
- method set_notation_status
- : 'status. #g_status as 'status -> 'self
- = fun o -> ((self#set_interp_status o)#set_content_pres_status o)#set_notation_parser_status o
- end
-
-let process_notation status st =
- match st with
- | Notation (loc, dir, l1, associativity, precedence, l2) ->
- let l1 =
- CicNotationParser.check_l1_pattern
- l1 (dir = Some `RightToLeft) precedence associativity
- in
- let status =
- if dir <> Some `RightToLeft then
- CicNotationParser.extend status l1
- (fun env loc ->
- NotationPt.AttributedTerm
- (`Loc loc,TermContentPres.instantiate_level2 env l2))
- else status
- in
- let status =
- if dir <> Some `LeftToRight then
- let status = TermContentPres.add_pretty_printer status l2 l1 in
- status
- else
- status
- in
- status
- | Interpretation (loc, dsc, l2, l3) ->
- Interpretations.add_interpretation status dsc l2 l3
- | st -> status
-
+++ /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/
- *)
-
-class type g_status =
- object ('self)
- inherit Interpretations.g_status
- inherit TermContentPres.g_status
- inherit CicNotationParser.g_status
- end
-
-class status :
- object ('self)
- inherit Interpretations.status
- inherit TermContentPres.status
- inherit CicNotationParser.status
- method set_notation_status: #g_status -> 'self
- end
-
-val process_notation:
- #status as 'status -> LexiconAst.command -> 'status
-
+++ /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 direction = [ `LeftToRight | `RightToLeft ]
-
-type loc = Stdpp.location
-
-type alias_spec =
- | Ident_alias of string * string (* identifier, uri *)
- | Symbol_alias of string * int * string (* name, instance no, description *)
- | Number_alias of int * string (* instance no, description *)
-
-(** To be increased each time the command type below changes, used for "safe"
- * marshalling *)
-let magic = 6
-
-type inclusion_mode = WithPreferences | WithoutPreferences (* aka aliases *)
-
-type command =
- | Include of loc * string * inclusion_mode * string (* _,buri,_,path *)
- | Alias of loc * alias_spec
- (** parameters, name, type, fields *)
- | Notation of loc * direction option * NotationPt.term * Gramext.g_assoc *
- int * NotationPt.term
- (* direction, l1 pattern, associativity, precedence, l2 pattern *)
- | Interpretation of loc *
- string * (string * NotationPt.argument_pattern list) *
- NotationPt.cic_appl_pattern
- (* description (i.e. id), symbol, arg pattern, appl pattern *)
-
-(* composed magic: term + command magics. No need to change this value *)
-let magic = magic + 10000 * NotationPt.magic
-
-let description_of_alias =
- function
- Ident_alias (_,desc)
- | Symbol_alias (_,_,desc)
- | Number_alias (_,desc) -> desc
+++ /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$ *)
-
-open Printf
-
-open LexiconAst
-
-let pp_l1_pattern = NotationPp.pp_term
-let pp_l2_pattern = NotationPp.pp_term
-
-let pp_alias = function
- | Ident_alias (id, uri) -> sprintf "alias id \"%s\" = \"%s\"." id uri
- | Symbol_alias (symb, instance, desc) ->
- sprintf "alias symbol \"%s\" %s= \"%s\"."
- symb
- (if instance=0 then "" else "(instance "^ string_of_int instance ^ ") ")
- desc
- | Number_alias (instance,desc) ->
- sprintf "alias num (instance %d) = \"%s\"." instance desc
-
-let pp_associativity = function
- | Gramext.LeftA -> "left associative"
- | Gramext.RightA -> "right associative"
- | Gramext.NonA -> "non associative"
-
-let pp_precedence i = sprintf "with precedence %d" i
-
-let pp_argument_pattern = function
- | NotationPt.IdentArg (eta_depth, name) ->
- let eta_buf = Buffer.create 5 in
- for i = 1 to eta_depth do
- Buffer.add_string eta_buf "\\eta."
- done;
- sprintf "%s%s" (Buffer.contents eta_buf) name
-
-let pp_interpretation dsc symbol arg_patterns cic_appl_pattern =
- sprintf "interpretation \"%s\" '%s %s = %s."
- dsc symbol
- (String.concat " " (List.map pp_argument_pattern arg_patterns))
- (NotationPp.pp_cic_appl_pattern cic_appl_pattern)
-
-let pp_dir_opt = function
- | None -> ""
- | Some `LeftToRight -> "> "
- | Some `RightToLeft -> "< "
-
-let pp_notation dir_opt l1_pattern assoc prec l2_pattern =
- sprintf "notation %s\"%s\" %s %s for %s."
- (pp_dir_opt dir_opt)
- (pp_l1_pattern l1_pattern)
- (pp_associativity assoc)
- (pp_precedence prec)
- (pp_l2_pattern l2_pattern)
-
-let pp_command = function
- | Include (_,_,mode,path) -> (* not precise, since path is absolute *)
- if mode = WithPreferences then
- "include \"" ^ path ^ "\"."
- else
- "include' \"" ^ path ^ "\"."
- | Alias (_,s) -> pp_alias s
- | Interpretation (_, dsc, (symbol, arg_patterns), cic_appl_pattern) ->
- pp_interpretation dsc symbol arg_patterns cic_appl_pattern
- | Notation (_, dir_opt, l1_pattern, assoc, prec, l2_pattern) ->
- pp_notation dir_opt l1_pattern assoc prec l2_pattern
+++ /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/
- *)
-
-val pp_command: LexiconAst.command -> string
-
-val pp_alias: LexiconAst.alias_spec -> string
-
(* $Id$ *)
-module L = LexiconAst
-
-let debug = ref false
-
-(* lexicon file name * ma file name *)
-exception IncludedFileNotCompiled of string * string
-exception MetadataNotFound of string (* file name *)
-
-type lexicon_status = {
- aliases: L.alias_spec DisambiguateTypes.Environment.t;
- multi_aliases: L.alias_spec list DisambiguateTypes.Environment.t;
- lexicon_content_rev: LexiconMarshal.lexicon;
-}
-
-let initial_status = {
- aliases = DisambiguateTypes.Environment.empty;
- multi_aliases = DisambiguateTypes.Environment.empty;
- lexicon_content_rev = [];
-}
-
-class type g_status =
- object
- inherit CicNotation.g_status
- method lstatus: lexicon_status
- end
-
-class status =
- object(self)
- inherit CicNotation.status
- val lstatus = initial_status
- method lstatus = lstatus
- method set_lstatus v = {< lstatus = v >}
- method set_lexicon_engine_status : 'status. #g_status as 'status -> 'self
- = fun o -> (self#set_lstatus o#lstatus)#set_notation_status o
- end
-
let dump_aliases out msg status =
out (if msg = "" then "aliases dump:" else msg ^ ": aliases dump:");
DisambiguateTypes.Environment.iter
- (fun _ x -> out (LexiconAstPp.pp_alias x))
- status#lstatus.aliases
+ (fun _ x -> out (GrafiteAstPp.pp_alias x))
+ status#lstatus.LexiconTypes.aliases
-let add_lexicon_content cmds status =
- let content = status#lstatus.lexicon_content_rev in
- let content' =
- List.fold_right
- (fun cmd acc ->
- match cmd with
- | L.Alias _
- | L.Include _
- | L.Notation _ -> cmd :: (List.filter ((<>) cmd) acc)
- | L.Interpretation _ -> if List.exists ((=) cmd) acc then acc else cmd::acc)
- cmds content
- in
-(*
- prerr_endline ("new lexicon content: " ^
- String.concat "; " (List.map LexiconAstPp.pp_command content')
- );
-*)
- status#set_lstatus
- { status#lstatus with lexicon_content_rev = content' }
-
-let set_proof_aliases mode status new_aliases =
- if mode = L.WithoutPreferences then
- status
+let set_proof_aliases status mode new_aliases =
+ if mode = GrafiteAst.WithoutPreferences then
+ status
else
- let commands_of_aliases =
+ (* MATITA 1.0
+ let new_commands =
List.map
- (fun _,alias -> L.Alias (HExtlib.dummy_floc, alias))
- in
+ (fun _,alias -> GrafiteAst.Alias (HExtlib.dummy_floc, alias)) new_aliases
+ in *)
let aliases =
List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc)
- status#lstatus.aliases new_aliases in
+ status#lstatus.LexiconTypes.aliases new_aliases in
let multi_aliases =
List.fold_left (fun acc (d,c) ->
- DisambiguateTypes.Environment.cons L.description_of_alias
+ DisambiguateTypes.Environment.cons GrafiteAst.description_of_alias
d c acc)
- status#lstatus.multi_aliases new_aliases
+ status#lstatus.LexiconTypes.multi_aliases new_aliases
in
let new_status =
- { status#lstatus with
- multi_aliases = multi_aliases ; aliases = aliases} in
- let new_status = status#set_lstatus new_status in
- if new_aliases = [] then
- new_status
- else
- add_lexicon_content (commands_of_aliases new_aliases) new_status
-
-let rec eval_command ?(mode=L.WithPreferences) sstatus cmd =
-(*
- let bmode = match mode with L.WithPreferences -> true | _ -> false in
- Printf.eprintf "Include preferences: %b\n" bmode;
-*)
- let status = sstatus#lstatus in
- let cmd =
- match cmd with
- | L.Interpretation (loc, dsc, (symbol, args), cic_appl_pattern) ->
- let rec disambiguate =
- function
- NotationPt.ApplPattern l ->
- NotationPt.ApplPattern (List.map disambiguate l)
- | NotationPt.VarPattern id
- when not
- (List.exists
- (function (NotationPt.IdentArg (_,id')) -> id'=id) args)
- ->
- let item = DisambiguateTypes.Id id in
- begin try
- match DisambiguateTypes.Environment.find item status.aliases with
- L.Ident_alias (_, uri) ->
- NotationPt.NRefPattern (NReference.reference_of_string uri)
- | _ -> assert false
- with Not_found ->
- prerr_endline ("LexiconEngine.eval_command: domain item not found: " ^
- (DisambiguateTypes.string_of_domain_item item));
- dump_aliases prerr_endline "" sstatus;
- raise (Failure (
- (DisambiguateTypes.string_of_domain_item item) ^
- " not found"));
- end
- | p -> p
- in
- L.Interpretation
- (loc, dsc, (symbol, args), disambiguate cic_appl_pattern)
- | _-> cmd
- in
- let sstatus = CicNotation.process_notation sstatus cmd in
- let sstatus = sstatus#set_lstatus status in
- match cmd with
- | L.Include (loc, baseuri, mode, fullpath) ->
- let lexiconpath_rw, lexiconpath_r =
- LibraryMisc.lexicon_file_of_baseuri
- ~must_exist:false ~writable:true ~baseuri,
- LibraryMisc.lexicon_file_of_baseuri
- ~must_exist:false ~writable:false ~baseuri
- in
- let lexiconpath =
- if Sys.file_exists lexiconpath_rw then lexiconpath_rw else
- if Sys.file_exists lexiconpath_r then lexiconpath_r else
- raise (IncludedFileNotCompiled (lexiconpath_rw,fullpath))
- in
- let lexicon = LexiconMarshal.load_lexicon lexiconpath in
- List.fold_left (eval_command ~mode) sstatus lexicon
- | L.Alias (loc, spec) ->
- let diff =
- (*CSC: Warning: this code should be factorized with the corresponding
- code in DisambiguatePp *)
- match spec with
- | L.Ident_alias (id,uri) ->
- [DisambiguateTypes.Id id,spec]
- | L.Symbol_alias (symb, instance, desc) ->
- [DisambiguateTypes.Symbol (symb,instance),spec]
- | L.Number_alias (instance,desc) ->
- [DisambiguateTypes.Num instance,spec]
- in
- set_proof_aliases mode sstatus diff
- | L.Interpretation (_, dsc, (symbol, _), _) as stm ->
- let sstatus = add_lexicon_content [stm] sstatus in
- let diff =
- try
- [DisambiguateTypes.Symbol (symbol, 0),
- L.Symbol_alias (symbol,0,dsc)]
- with
- DisambiguateChoices.Choice_not_found msg ->
- prerr_endline (Lazy.force msg);
- assert false
- in
- let sstatus = set_proof_aliases mode sstatus diff in
- sstatus
- | L.Notation _ as stm ->
- add_lexicon_content [stm] sstatus
-
-let eval_command status cmd =
- if !debug then dump_aliases prerr_endline "before eval_command" status;
- let status = eval_command ?mode:None status cmd in
- if !debug then dump_aliases prerr_endline "after eval_command" status;
- status
-
-let set_proof_aliases status aliases =
- if !debug then dump_aliases prerr_endline "before set_proof_aliases" status;
- let status = set_proof_aliases L.WithPreferences status aliases in
- if !debug then dump_aliases prerr_endline "after set_proof_aliases" status;
- status
+ {LexiconTypes.multi_aliases = multi_aliases ; aliases = aliases}
+ in
+ status#set_lstatus new_status
* http://helm.cs.unibo.it/
*)
-exception IncludedFileNotCompiled of string * string
-
-type lexicon_status = {
- aliases: LexiconAst.alias_spec DisambiguateTypes.Environment.t;
- multi_aliases: LexiconAst.alias_spec list DisambiguateTypes.Environment.t;
- lexicon_content_rev: LexiconMarshal.lexicon;
-}
-
-class type g_status =
- object
- inherit CicNotation.g_status
- method lstatus: lexicon_status
- end
-
-class status :
- object ('self)
- inherit g_status
- inherit CicNotation.status
- method set_lstatus: lexicon_status -> 'self
- method set_lexicon_engine_status: #g_status -> 'self
- end
-
-val eval_command : #status as 'status -> LexiconAst.command -> 'status
-
val set_proof_aliases:
- #status as 'status ->
- (DisambiguateTypes.domain_item * LexiconAst.alias_spec) list -> 'status
+ #LexiconTypes.status as 'status ->
+ GrafiteAst.inclusion_mode ->
+ (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list -> 'status
(* args: print function, message (may be empty), status *)
-val dump_aliases: (string -> unit) -> string -> #status -> unit
+val dump_aliases: (string -> unit) -> string -> #LexiconTypes.status -> unit
+++ /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 lexicon = LexiconAst.command list
-
-let format_name = "lexicon"
-
-let save_lexicon_to_file ~fname lexicon =
- HMarshal.save ~fmt:format_name ~version:LexiconAst.magic ~fname lexicon
-
-let load_lexicon_from_file ~fname =
- let raw = HMarshal.load ~fmt:format_name ~version:LexiconAst.magic ~fname in
- (raw: lexicon)
-
-let rehash_cmd_uris =
- function
- | LexiconAst.Interpretation (loc, dsc, args, cic_appl_pattern) ->
- let rec aux =
- function
- | NotationPt.NRefPattern (NReference.Ref (uri,spec)) ->
- let uri = NCicLibrary.refresh_uri uri in
- NotationPt.NRefPattern (NReference.reference_of_spec uri spec)
- | NotationPt.ApplPattern args ->
- NotationPt.ApplPattern (List.map aux args)
- | NotationPt.VarPattern _
- | NotationPt.ImplicitPattern as pat -> pat
- in
- let appl_pattern = aux cic_appl_pattern in
- LexiconAst.Interpretation (loc, dsc, args, appl_pattern)
- | LexiconAst.Notation _
- | LexiconAst.Alias _ as cmd -> cmd
- | cmd ->
- prerr_endline "Found a command not expected in a .lexicon:";
- prerr_endline (LexiconAstPp.pp_command cmd);
- assert false
-
-let save_lexicon ~fname lexicon = save_lexicon_to_file ~fname (List.rev lexicon)
-
-let load_lexicon ~fname =
- let lexicon = load_lexicon_from_file ~fname in
- List.map rehash_cmd_uris lexicon
-
+++ /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 lexicon = LexiconAst.command list
-
-val save_lexicon: fname:string -> lexicon -> unit
-
- (** @raise HMarshal.* *)
-val load_lexicon: fname:string -> lexicon
-
let module Map = DisambiguateTypes.Environment in
Map.fold
(fun domain_item codomain_item acc ->
- let description1 = LexiconAst.description_of_alias codomain_item in
+ let description1 = GrafiteAst.description_of_alias codomain_item in
try
let description2 =
- LexiconAst.description_of_alias
- (Map.find domain_item from#lstatus.LexiconEngine.aliases)
+ GrafiteAst.description_of_alias
+ (Map.find domain_item from#lstatus.LexiconTypes.aliases)
in
if description1 <> description2 then
(domain_item,codomain_item)::acc
with
Not_found ->
(domain_item,codomain_item)::acc)
- status#lstatus.LexiconEngine.aliases []
+ status#lstatus.LexiconTypes.aliases []
;;
let add_aliases_for_objs status =
(fun u ->
let name = NCicPp.r2s true u in
DisambiguateTypes.Id name,
- LexiconAst.Ident_alias (name,NReference.string_of_reference u)
+ GrafiteAst.Ident_alias (name,NReference.string_of_reference u)
) references
in
- LexiconEngine.set_proof_aliases status new_env
+ LexiconEngine.set_proof_aliases status GrafiteAst.WithPreferences new_env
) status
*)
val add_aliases_for_objs:
- #LexiconEngine.status as 'status -> NUri.uri list -> 'status
+ #LexiconTypes.status as 'status -> NUri.uri list -> 'status
(** perform a diff between the aliases contained in two statuses, assuming
* that the second one can only have more aliases than the first one
* @return the list of aliases that should be added to aliases of from in
* order to be equal to aliases of the second argument *)
val alias_diff:
- from:#LexiconEngine.status -> #LexiconEngine.status ->
- (DisambiguateTypes.domain_item * LexiconAst.alias_spec) list
-
+ from:#LexiconTypes.status -> #LexiconTypes.status ->
+ (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list
--- /dev/null
+(* Copyright (C) 2004-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 lexicon_status = {
+ aliases: GrafiteAst.alias_spec DisambiguateTypes.Environment.t;
+ multi_aliases: GrafiteAst.alias_spec list DisambiguateTypes.Environment.t
+}
+
+let initial_status = {
+ aliases = DisambiguateTypes.Environment.empty;
+ multi_aliases = DisambiguateTypes.Environment.empty
+}
+
+class type g_status =
+ object
+ inherit Interpretations.g_status
+ inherit TermContentPres.g_status
+ inherit CicNotationParser.g_status
+ method lstatus: lexicon_status
+ end
+
+class status =
+ object(self)
+ inherit Interpretations.status
+ inherit TermContentPres.status
+ inherit CicNotationParser.status
+ val lstatus = initial_status
+ method lstatus = lstatus
+ method set_lstatus v = {< lstatus = v >}
+ method set_lexicon_engine_status : 'status. #g_status as 'status -> 'self
+ = fun o -> (((self#set_lstatus o#lstatus)#set_interp_status o)#set_content_pres_status o)#set_notation_parser_status o
+ end
--- /dev/null
+(* Copyright (C) 2004-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 lexicon_status = {
+ aliases: GrafiteAst.alias_spec DisambiguateTypes.Environment.t;
+ multi_aliases: GrafiteAst.alias_spec list DisambiguateTypes.Environment.t
+}
+
+class type g_status =
+ object
+ inherit Interpretations.g_status
+ inherit TermContentPres.g_status
+ inherit CicNotationParser.g_status
+ method lstatus: lexicon_status
+ end
+
+class status :
+ object ('self)
+ inherit g_status
+ inherit Interpretations.status
+ inherit TermContentPres.status
+ inherit CicNotationParser.status
+ method set_lstatus: lexicon_status -> 'self
+ method set_lexicon_engine_status: #g_status -> 'self
+ end
(* $Id$ *)
exception LibraryOutOfSync of string Lazy.t
+exception IncludedFileNotCompiled of string * string
type timestamp
grafitetypes -> tac -> auto + eq + (grafitedisambiguate = lexicon+nciccoercion)
|--> dumpable | |
|--> nciclibrary | unif_hint
- |
- interpretation + termcontentpres + notation_parser= cicnotation
-
-
-
+ |--> grafiteparser -> lexicon -> ... |
+ |-> interpretation
+ |-> termcontentpres
+ |-> notation_parser
ntermciccontent = nciccoercion+interpretation
matitaclean.cmo: matitaMisc.cmi matitaInit.cmi matitaclean.cmi
matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi
matitacLib.cmo: matitaMisc.cmi matitaExcPp.cmi matitaEngine.cmi \
- buildTimeConf.cmo applyTransformation.cmi matitacLib.cmi
+ buildTimeConf.cmo matitacLib.cmi
matitacLib.cmx: matitaMisc.cmx matitaExcPp.cmx matitaEngine.cmx \
- buildTimeConf.cmx applyTransformation.cmx matitacLib.cmi
+ buildTimeConf.cmx matitacLib.cmi
matitac.cmo: matitadep.cmi matitaclean.cmi matitacLib.cmi matitaMisc.cmi \
matitaInit.cmi
matitac.cmx: matitadep.cmx matitaclean.cmx matitacLib.cmx matitaMisc.cmx \
matitaInit.cmx
matitadep.cmo: matitaMisc.cmi matitaInit.cmi matitadep.cmi
matitadep.cmx: matitaMisc.cmx matitaInit.cmx matitadep.cmi
-matitaEngine.cmo: applyTransformation.cmi matitaEngine.cmi
-matitaEngine.cmx: applyTransformation.cmx matitaEngine.cmi
+matitaEngine.cmo: matitaEngine.cmi
+matitaEngine.cmx: matitaEngine.cmi
matitaExcPp.cmo: matitaEngine.cmi matitaExcPp.cmi
matitaExcPp.cmx: matitaEngine.cmx matitaExcPp.cmi
matitaGeneratedGui.cmo:
matitaMisc.cmx: buildTimeConf.cmx matitaMisc.cmi
matita.cmo: predefined_virtuals.cmi matitaTypes.cmi matitaScript.cmi \
matitaMathView.cmi matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi \
- buildTimeConf.cmo applyTransformation.cmi
+ buildTimeConf.cmo
matita.cmx: predefined_virtuals.cmx matitaTypes.cmx matitaScript.cmx \
matitaMathView.cmx matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx \
- buildTimeConf.cmx applyTransformation.cmx
+ buildTimeConf.cmx
matitaScript.cmo: virtuals.cmi matitacLib.cmi matitaTypes.cmi \
- matitaGtkMisc.cmi matitaEngine.cmi buildTimeConf.cmo \
- applyTransformation.cmi matitaScript.cmi
+ matitaGtkMisc.cmi matitaEngine.cmi buildTimeConf.cmo matitaScript.cmi
matitaScript.cmx: virtuals.cmx matitacLib.cmx matitaTypes.cmx \
- matitaGtkMisc.cmx matitaEngine.cmx buildTimeConf.cmx \
- applyTransformation.cmx matitaScript.cmi
+ matitaGtkMisc.cmx matitaEngine.cmx buildTimeConf.cmx matitaScript.cmi
matitaTypes.cmo: matitaTypes.cmi
matitaTypes.cmx: matitaTypes.cmi
predefined_virtuals.cmo: virtuals.cmi predefined_virtuals.cmi
matitaExcPp.cmi:
matitaGtkMisc.cmi: matitaGeneratedGui.cmo
matitaGui.cmi: matitaGuiTypes.cmi
-matitaGuiTypes.cmi: matitaTypes.cmi matitaGeneratedGui.cmo
+matitaGuiTypes.cmi: matitaTypes.cmi matitaGeneratedGui.cmo \
+ applyTransformation.cmi
matitaInit.cmi:
matitaMathView.cmi: matitaTypes.cmi matitaGuiTypes.cmi
matitaMisc.cmi:
*)
;;
-let eval_ast ?do_heavy_checks status (text,prefix_len,ast) =
- let dump = not (Helm_registry.get_bool "matita.moo") in
- let lexicon_status_ref = ref (status :> LexiconEngine.status) in
+let eval_ast ~include_paths ?do_heavy_checks status (text,prefix_len,ast) =
+ let lexicon_status_ref = ref (status :> LexiconTypes.status) in
let baseuri = status#baseuri in
let new_status,new_objs =
- GrafiteEngine.eval_ast ?do_heavy_checks status (text,prefix_len,ast)
+ GrafiteEngine.eval_ast ~include_paths ?do_heavy_checks status
+ (text,prefix_len,ast)
in
let new_status =
if !lexicon_status_ref#lstatus != status#lstatus then
let _,intermediate_states =
List.fold_left
(fun (status,acc) (k,value) ->
- let v = LexiconAst.description_of_alias value in
+ let v = GrafiteAst.description_of_alias value in
let b =
try
let NReference.Ref (uri,_) = NReference.reference_of_string v in
status,acc
else
let new_status =
- LexiconEngine.set_proof_aliases status [k,value]
+ LexiconEngine.set_proof_aliases status
+ GrafiteAst.WithPreferences [k,value]
in
new_status, (new_status ,Some (k,value))::acc
) (status,[]) new_aliases
let stop,g,s =
try
let cont =
- try Some (GrafiteParser.parse_statement ~include_paths str status)
+ try Some (GrafiteParser.parse_statement status str)
with End_of_file -> None in
match cont with
| None -> true, status, statuses
- | Some (status,ast) ->
+ | Some ast ->
(match ast with
GrafiteParser.LNone _ ->
watch_statuses status ;
false, status, ((status,None)::statuses)
| GrafiteParser.LSome ast ->
cb status ast;
- let new_statuses = eval_ast ?do_heavy_checks status ("",0,ast) in
+ let new_statuses =
+ eval_ast ~include_paths ?do_heavy_checks status ("",0,ast) in
if enforce_no_new_aliases then
List.iter
(fun (_,alias) ->
match alias with
None -> ()
| Some (k,value) ->
- let newtxt = LexiconAstPp.pp_alias value in
+ let newtxt = GrafiteAstPp.pp_alias value in
raise (TryingToAdd newtxt)) new_statuses;
let status =
match new_statuses with
*)
val eval_ast :
+ include_paths: string list ->
?do_heavy_checks:bool ->
GrafiteTypes.status ->
string * int *
GrafiteAst.statement ->
(GrafiteTypes.status *
- (DisambiguateTypes.domain_item * LexiconAst.alias_spec) option) list
+ (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) option) list
(* heavy checks slow down the compilation process but give you some interesting
Ulexing.lexbuf ->
(GrafiteTypes.status -> GrafiteAst.statement -> unit) ->
(GrafiteTypes.status *
- (DisambiguateTypes.domain_item * LexiconAst.alias_spec) option) list
+ (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) option) list
let rec to_string =
function
- | HExtlib.Localized (floc,exn) ->
+ HExtlib.Localized (floc,exn) ->
let _,msg = to_string exn in
let (x, y) = HExtlib.loc_of_floc floc in
Some floc, sprintf "Error at %d-%d: %s" x y msg
+ | NCicLibrary.IncludedFileNotCompiled (s1,s2) ->
+ None, "Including: "^s1^" "^s2^ "\nNothing to do... did you run matitadep?"
| GrafiteTypes.Command_error msg -> None, "Error: " ^ msg
| CicNotationParser.Parse_error err ->
None, sprintf "Parse error: %s" err
match script#bos, script#eos with
| true, _ -> ()
| _, true ->
- let lexicon_fname =
- LibraryMisc.lexicon_file_of_baseuri
- ~must_exist:false ~baseuri ~writable:true
- in
- LexiconMarshal.save_lexicon lexicon_fname
- grafite_status#lstatus.LexiconEngine.lexicon_content_rev;
GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
grafite_status#dump
| _ -> clean_current_baseuri grafite_status
let alias =
match k with
| DisambiguateTypes.Id id ->
- LexiconAst.Ident_alias (id, desc)
+ GrafiteAst.Ident_alias (id, desc)
| DisambiguateTypes.Symbol (symb, i)->
- LexiconAst.Symbol_alias (symb, i, desc)
+ GrafiteAst.Symbol_alias (symb, i, desc)
| DisambiguateTypes.Num i ->
- LexiconAst.Number_alias (i, desc)
+ GrafiteAst.Number_alias (i, desc)
in
- LexiconAstPp.pp_alias alias)
+ GrafiteAstPp.pp_alias alias)
diff) ^ "\n"
in
source_buffer#insert
let my_id = Oo.id self in
cicBrowsers := List.filter (fun b -> Oo.id b <> my_id) !cicBrowsers;
win#toplevel#misc#hide(); win#toplevel#destroy ());
- (* remove hbugs *)
- (*
- connect_menu_item win#hBugsTutorsMenuItem (fun () ->
- self#load (`HBugs `Tutors));
- *)
- win#hBugsTutorsMenuItem#misc#hide ();
connect_menu_item win#browserUrlMenuItem (fun () ->
win#browserUri#misc#grab_focus ());
method private _showList2 = win#mathOrListNotebook#goto_page 5
method private _showSearch = win#mathOrListNotebook#goto_page 6
method private _showGviz = win#mathOrListNotebook#goto_page 3
- method private _showHBugs = win#mathOrListNotebook#goto_page 4
method private back () =
try
| `NCic (term, ctx, metasenv, subst) ->
self#_loadTermNCic term metasenv subst ctx
| `Dir dir -> self#_loadDir dir
- | `HBugs `Tutors -> self#_loadHBugsTutors
| `NRef nref -> self#_loadNReference nref);
self#setEntry entry
end)
self#_showSearch
method private grammar () =
- self#_loadText (Print_grammar.ebnf_of_term ());
+ self#_loadText (Print_grammar.ebnf_of_term self#script#grafite_status);
method private home () =
self#_showMath;
lastDir <- dir;
self#_loadList l
- method private _loadHBugsTutors =
- self#_showHBugs
-
method private setEntry entry =
win#browserUri#set_text (MatitaTypes.string_of_entry entry);
current_entry <- entry
let text = skipped_txt ^ nonskipped_txt in
let prefix_len = MatitaGtkMisc.utf8_string_length skipped_txt in
let enriched_history_fragment =
- MatitaEngine.eval_ast ~do_heavy_checks:(Helm_registry.get_bool
+ MatitaEngine.eval_ast ~include_paths ~do_heavy_checks:(Helm_registry.get_bool
"matita.do_heavy_checks")
grafite_status (text,prefix_len,st)
in
match alias with
| None -> (status,to_prepend ^ nonskipped_txt)::acc,""
| Some (k,value) ->
- let newtxt = LexiconAstPp.pp_alias value in
+ let newtxt = GrafiteAstPp.pp_alias value in
(status,to_prepend ^ newtxt ^ "\n")::acc, "")
([],skipped_txt) enriched_history_fragment
in
* so that we can ensure the inclusion is performed after the included file
* is compiled (if needed). matitac does not need that, since it compiles files
* in the good order, here files may be compiled on demand. *)
-let wrap_with_make include_paths (f : #LexiconEngine.status GrafiteParser.statement) x =
- try
- f ~never_include:true ~include_paths x
- with
- | GrafiteParser.NoInclusionPerformed mafilename ->
+let wrap_with_make include_paths f x =
+ match f x with
+ GrafiteParser.LSome (GrafiteAst.Executable (_,GrafiteAst.NCommand
+ (_,GrafiteAst.Include (_,_,mafilename)))) as cmd ->
let root, buri, _, tgt =
try Librarian.baseuri_of_script ~include_paths mafilename
with Librarian.NoRootFor _ ->
HLog.error "please create it.";
raise (Failure ("No root file for "^mafilename))
in
- let b = MatitacLib.Make.make root [tgt] in
- if b then
- try f ~include_paths x with LexiconEngine.IncludedFileNotCompiled _ ->
- raise
- (Failure ("Including: "^tgt^
- "\nNothing to do... did you run matitadep?"))
+ if MatitacLib.Make.make root [tgt] then
+ cmd
else raise (Failure ("Compiling: " ^ tgt))
+ | cmd -> cmd
;;
let pp_eager_statement_ast = GrafiteAstPp.pp_statement
and eval_statement include_paths (buffer : GText.buffer) guistuff
grafite_status user_goal script statement
=
- let (grafite_status,st), unparsed_text =
+ let st,unparsed_text =
match statement with
| `Raw text ->
if Pcre.pmatch ~rex:only_dust_RE text then raise Margin;
let ast =
wrap_with_make include_paths
- (GrafiteParser.parse_statement (Ulexing.from_utf8_string text))
- grafite_status
+ (GrafiteParser.parse_statement grafite_status)
+ (Ulexing.from_utf8_string text)
in
ast, text
- | `Ast (st, text) -> (grafite_status, st), text
+ | `Ast (st, text) -> st, text
in
let text_of_loc floc =
let nonskipped_txt,_ = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in
let buffer = source_view#buffer in
let source_buffer = source_view#source_buffer in
let initial_statuses current baseuri =
- let empty_lstatus = new LexiconEngine.status in
+ let empty_lstatus = new LexiconTypes.status in
(match current with
Some current ->
- LexiconSync.time_travel ~present:current ~past:empty_lstatus;
NCicLibrary.time_travel
((new GrafiteTypes.status current#baseuri)#set_lstatus current#lstatus);
(* CSC: there is a known bug in invalidation; temporary fix here *)
bottom) and we will face a macro *)
userGoal <- None
- method private _retract offset grafite_status new_statements
- new_history
- =
- let cur_grafite_status =
- match history with s::_ -> s | [] -> assert false
- in
- LexiconSync.time_travel ~present:cur_grafite_status ~past:grafite_status;
+ method private _retract offset grafite_status new_statements new_history =
NCicLibrary.time_travel grafite_status;
statements <- new_statements;
history <- new_history;
method eos =
let rec is_there_only_comments lexicon_status s =
if Pcre.pmatch ~rex:only_dust_RE s then raise Margin;
- let lexicon_status,st =
- GrafiteParser.parse_statement (Ulexing.from_utf8_string s)
- ~include_paths:self#include_paths lexicon_status
- in
- match st with
+ match
+ GrafiteParser.parse_statement lexicon_status (Ulexing.from_utf8_string s)
+ with
| GrafiteParser.LSome (GrafiteAst.Comment (loc,_)) ->
let _,parsed_text_length = MatitaGtkMisc.utf8_parsed_text s loc in
(* CSC: why +1 in the following lines ???? *)
in
try is_there_only_comments self#grafite_status self#getFuture
with
- | LexiconEngine.IncludedFileNotCompiled _
+ | NCicLibrary.IncludedFileNotCompiled _
| HExtlib.Localized _
| CicNotationParser.Parse_error _ -> false
| Margin | End_of_file -> true
open GrafiteTypes
-exception AttemptToInsertAnAlias of LexiconEngine.status
+exception AttemptToInsertAnAlias of LexiconTypes.status
let slash_n_RE = Pcre.regexp "\\n" ;;
LibraryClean.clean_baseuris ~verbose:false [baseuri]; rc
;;
-let dump f =
- let module G = GrafiteAst in
- let module L = LexiconAst in
- let module H = HExtlib in
- let floc = H.dummy_floc in
- let nl_ast = G.Comment (floc, G.Note (floc, "")) in
- let pp_statement stm =
- GrafiteAstPp.pp_statement stm
- ~map_unicode_to_tex:(Helm_registry.get_bool
- "matita.paste_unicode_as_tex")
- in
- let pp_lexicon = LexiconAstPp.pp_command in
- let och = open_out f in
- let nl () = output_string och (pp_statement nl_ast) in
- MatitaMisc.out_preamble och;
- let grafite_parser_cb = function
- | G.Executable (loc, G.Command (_, G.Include (_,_))) -> ()
- | stm ->
- output_string och (pp_statement stm); nl (); nl ()
- in
- let lexicon_parser_cb cmd =
- output_string och (pp_lexicon cmd); nl (); nl ()
- in
- begin fun () ->
- Helm_registry.set_bool "matita.moo" false;
- GrafiteParser.set_grafite_callback grafite_parser_cb;
- GrafiteParser.set_lexicon_callback lexicon_parser_cb
- end,
- begin fun x ->
- close_out och;
- GrafiteParser.set_grafite_callback (fun _ -> ());
- GrafiteParser.set_lexicon_callback (fun _ -> ());
- Helm_registry.set_bool "matita.moo" true;
- x
- end
-;;
-
let get_macro_context = function _ -> []
;;
if Http_getter_storage.is_read_only baseuri then assert false;
activate_extraction baseuri fname ;
let lexicon_status =
- CicNotation2.load_notation ~include_paths:[] (new LexiconEngine.status)
+ CicNotation2.load_notation ~include_paths:[] (new LexiconTypes.status)
BuildTimeConf.core_notation_script
in
atstart (); (* FG: do not invoke before loading the core notation script *)
in
let time = Unix.time () in
try
- (* sanity checks *)
- 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
(* cleanup of previously compiled objects *)
if (not (Http_getter_storage.is_empty ~local:true baseuri))
then begin
| [] -> grafite_status
| (g,None)::_ -> g
| (g,Some _)::_ ->
- raise (AttemptToInsertAnAlias (g :> LexiconEngine.status))
+ raise (AttemptToInsertAnAlias (g :> LexiconTypes.status))
in
aux_for_dump print_cb grafite_status
in
let elapsed = Unix.time () -. time in
- 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 *)
- LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
- GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
- grafite_status#dump
+ GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
+ grafite_status#dump
end;
let tm = Unix.gmtime elapsed in
let sec = string_of_int tm.Unix.tm_sec ^ "''" in
let matita_debug = Helm_registry.get_bool "matita.debug" in
let compile atstart opts fname =
try
- GrafiteParser.push ();
- let rc = compile atstart opts fname in
- GrafiteParser.pop ();
- rc
+ (* MATITA 1.0: c'erano le push/pop per il parser; ma per
+ * l'environment nuovo? *)
+ compile atstart opts fname
with
- | Sys.Break ->
- GrafiteParser.pop ();
- false
+ | Sys.Break -> false
| exn when not matita_debug ->
HLog.error ("Unexpected " ^ snd(MatitaExcPp.to_string exn));
assert false
in
- if Filename.check_suffix fname ".mma" then
- let generated = Filename.chop_suffix fname ".mma" ^ ".ma" in
- let atstart, atexit = dump generated in
- let res = compile atstart options fname in
- let r = compact (atexit res) in
- if r then r else begin
-(* Sys.remove generated; *)
- Printf.printf "rm %s\n" generated; flush stdout; r
- end
- else
- compact (compile ignore options fname)
+ compact (compile ignore options fname)
;;
let load_deps_file = Librarian.load_deps_file;;
projects / helm.git / commitdiff