From: Andrea Asperti Date: Wed, 3 Nov 2010 14:13:11 +0000 (+0000) Subject: - LexiconAst merged into GrafiteAst X-Git-Tag: make_still_working~2741 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cd664aefb80554952ed9b010f0c5199ce3a6f8f2;p=helm.git - LexiconAst merged into GrafiteAst - all lexicon stuff made functional (more or less) - no more .lexicon files --- diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml index 46dfef451..173912e1f 100644 --- a/matita/components/grafite/grafiteAst.ml +++ b/matita/components/grafite/grafiteAst.ml @@ -83,12 +83,22 @@ type nmacro = * 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 @@ -99,6 +109,16 @@ type ncommand = 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 @@ -113,3 +133,9 @@ type comment = 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 diff --git a/matita/components/grafite/grafiteAstPp.ml b/matita/components/grafite/grafiteAstPp.ml index 202e1776c..4ea07a54f 100644 --- a/matita/components/grafite/grafiteAstPp.ml +++ b/matita/components/grafite/grafiteAstPp.ml @@ -26,6 +26,7 @@ (* $Id$ *) open GrafiteAst +open Printf let tactical_terminator = "" let tactic_terminator = tactical_terminator @@ -112,6 +113,53 @@ let pp_nmacro = function | 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 @@ -127,10 +175,19 @@ let pp_ncommand = function (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 diff --git a/matita/components/grafite/grafiteAstPp.mli b/matita/components/grafite/grafiteAstPp.mli index 11c1782fa..19de8bc8c 100644 --- a/matita/components/grafite/grafiteAstPp.mli +++ b/matita/components/grafite/grafiteAstPp.mli @@ -28,4 +28,6 @@ val pp_comment: map_unicode_to_tex:bool -> GrafiteAst.comment -> string 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 diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index 00160ac81..e96790860 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -25,7 +25,6 @@ (* $Id$ *) -exception Drop (* mo file name, ma file name *) exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro @@ -292,8 +291,18 @@ let subst_metasenv_and_fix_names status = ;; -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 @@ -372,7 +381,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = (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 @@ -404,7 +413,8 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = 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"; *) @@ -478,7 +488,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = 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") @@ -494,7 +504,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = 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 @@ -511,7 +521,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = 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) -> @@ -543,10 +553,86 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = 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, [] @@ -554,29 +640,12 @@ 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 @@ -593,15 +662,16 @@ and eval_executable opts status (text,prefix_len,ex) = | 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) ;; diff --git a/matita/components/grafite_engine/grafiteEngine.mli b/matita/components/grafite_engine/grafiteEngine.mli index 10bc4d36d..9b1979970 100644 --- a/matita/components/grafite_engine/grafiteEngine.mli +++ b/matita/components/grafite_engine/grafiteEngine.mli @@ -23,12 +23,12 @@ * 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 -> diff --git a/matita/components/grafite_engine/grafiteTypes.ml b/matita/components/grafite_engine/grafiteTypes.ml index 82fc6d605..573fa28c9 100644 --- a/matita/components/grafite_engine/grafiteTypes.ml +++ b/matita/components/grafite_engine/grafiteTypes.ml @@ -41,6 +41,7 @@ class status = fun (b : string) -> 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 diff --git a/matita/components/grafite_engine/grafiteTypes.mli b/matita/components/grafite_engine/grafiteTypes.mli index 92af84bab..fd89f4648 100644 --- a/matita/components/grafite_engine/grafiteTypes.mli +++ b/matita/components/grafite_engine/grafiteTypes.mli @@ -38,6 +38,7 @@ class status : 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] diff --git a/matita/components/grafite_parser/.depend b/matita/components/grafite_parser/.depend index df2432b9f..dff050549 100644 --- a/matita/components/grafite_parser/.depend +++ b/matita/components/grafite_parser/.depend @@ -2,13 +2,13 @@ dependenciesParser.cmi: 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 diff --git a/matita/components/grafite_parser/cicNotation2.mli b/matita/components/grafite_parser/cicNotation2.mli index 6c9c44167..d6cdfe852 100644 --- a/matita/components/grafite_parser/cicNotation2.mli +++ b/matita/components/grafite_parser/cicNotation2.mli @@ -25,5 +25,5 @@ (** @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 diff --git a/matita/components/grafite_parser/grafiteDisambiguate.ml b/matita/components/grafite_parser/grafiteDisambiguate.ml index 143ac5e11..f82759195 100644 --- a/matita/components/grafite_parser/grafiteDisambiguate.ml +++ b/matita/components/grafite_parser/grafiteDisambiguate.ml @@ -27,13 +27,13 @@ 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 @@ -55,7 +55,7 @@ let __Implicit = "__Implicit__" 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 @@ -69,11 +69,11 @@ let ncic_mk_choice status = function (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 @@ -84,9 +84,9 @@ let ncic_mk_choice status = function 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 @@ -97,7 +97,7 @@ 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 _ -> []) @@ -109,13 +109,13 @@ let fix_instance item l = 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 @@ -128,16 +128,18 @@ let disambiguate_nterm expty estatus context metasenv subst thing 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 ;; @@ -209,14 +211,15 @@ let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) = 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 ;; diff --git a/matita/components/grafite_parser/grafiteDisambiguate.mli b/matita/components/grafite_parser/grafiteDisambiguate.mli index 200d507a8..0074b2916 100644 --- a/matita/components/grafite_parser/grafiteDisambiguate.mli +++ b/matita/components/grafite_parser/grafiteDisambiguate.mli @@ -27,13 +27,13 @@ exception BaseUriNotSetYet 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 @@ -57,5 +57,3 @@ type pattern = val disambiguate_npattern: GrafiteAst.npattern Disambiguate.disambiguator_input -> pattern - - diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml index 29d52c01f..b3e42e63e 100644 --- a/matita/components/grafite_parser/grafiteParser.ml +++ b/matita/components/grafite_parser/grafiteParser.ml @@ -27,11 +27,8 @@ 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 @@ -440,7 +437,7 @@ EXTEND 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))) @@ -453,14 +450,14 @@ EXTEND 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: [ @@ -524,11 +521,9 @@ EXTEND 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: [ [ @@ -587,12 +582,12 @@ EXTEND 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) @@ -617,16 +612,14 @@ EXTEND ]; 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 *) @@ -642,7 +635,7 @@ type db = ast_statement localized_option Grammar.Entry.e ;; class type g_status = object - inherit LexiconEngine.g_status + inherit LexiconTypes.g_status method parser_db: db end @@ -650,7 +643,7 @@ class status = 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 diff --git a/matita/components/grafite_parser/grafiteParser.mli b/matita/components/grafite_parser/grafiteParser.mli index 4e4b035ab..dc39ab316 100644 --- a/matita/components/grafite_parser/grafiteParser.mli +++ b/matita/components/grafite_parser/grafiteParser.mli @@ -29,19 +29,17 @@ type 'a localized_option = 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 diff --git a/matita/components/lexicon/.depend b/matita/components/lexicon/.depend index fbe5dd026..43aa8b202 100644 --- a/matita/components/lexicon/.depend +++ b/matita/components/lexicon/.depend @@ -1,19 +1,9 @@ -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 diff --git a/matita/components/lexicon/Makefile b/matita/components/lexicon/Makefile index d5b16e924..1213f0b52 100644 --- a/matita/components/lexicon/Makefile +++ b/matita/components/lexicon/Makefile @@ -2,14 +2,11 @@ PACKAGE = lexicon 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) diff --git a/matita/components/lexicon/cicNotation.ml b/matita/components/lexicon/cicNotation.ml deleted file mode 100644 index 1934c8526..000000000 --- a/matita/components/lexicon/cicNotation.ml +++ /dev/null @@ -1,73 +0,0 @@ -(* 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 - diff --git a/matita/components/lexicon/cicNotation.mli b/matita/components/lexicon/cicNotation.mli deleted file mode 100644 index 16422729b..000000000 --- a/matita/components/lexicon/cicNotation.mli +++ /dev/null @@ -1,43 +0,0 @@ -(* 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 - diff --git a/matita/components/lexicon/lexiconAst.ml b/matita/components/lexicon/lexiconAst.ml deleted file mode 100644 index b0b9399b5..000000000 --- a/matita/components/lexicon/lexiconAst.ml +++ /dev/null @@ -1,62 +0,0 @@ -(* 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 diff --git a/matita/components/lexicon/lexiconAstPp.ml b/matita/components/lexicon/lexiconAstPp.ml deleted file mode 100644 index cf8ea3d03..000000000 --- a/matita/components/lexicon/lexiconAstPp.ml +++ /dev/null @@ -1,89 +0,0 @@ -(* 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 diff --git a/matita/components/lexicon/lexiconAstPp.mli b/matita/components/lexicon/lexiconAstPp.mli deleted file mode 100644 index b7ad59f3c..000000000 --- a/matita/components/lexicon/lexiconAstPp.mli +++ /dev/null @@ -1,29 +0,0 @@ -(* 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 - diff --git a/matita/components/lexicon/lexiconEngine.ml b/matita/components/lexicon/lexiconEngine.ml index d92b74091..ce7e4e2aa 100644 --- a/matita/components/lexicon/lexiconEngine.ml +++ b/matita/components/lexicon/lexiconEngine.ml @@ -25,186 +25,31 @@ (* $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 diff --git a/matita/components/lexicon/lexiconEngine.mli b/matita/components/lexicon/lexiconEngine.mli index ad1ce3f86..6209ce40d 100644 --- a/matita/components/lexicon/lexiconEngine.mli +++ b/matita/components/lexicon/lexiconEngine.mli @@ -23,33 +23,10 @@ * 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 diff --git a/matita/components/lexicon/lexiconMarshal.ml b/matita/components/lexicon/lexiconMarshal.ml deleted file mode 100644 index 5e74e8815..000000000 --- a/matita/components/lexicon/lexiconMarshal.ml +++ /dev/null @@ -1,66 +0,0 @@ -(* 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 - diff --git a/matita/components/lexicon/lexiconMarshal.mli b/matita/components/lexicon/lexiconMarshal.mli deleted file mode 100644 index 930d73f8d..000000000 --- a/matita/components/lexicon/lexiconMarshal.mli +++ /dev/null @@ -1,32 +0,0 @@ -(* 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 - diff --git a/matita/components/lexicon/lexiconSync.ml b/matita/components/lexicon/lexiconSync.ml index ce9f56482..322279769 100644 --- a/matita/components/lexicon/lexiconSync.ml +++ b/matita/components/lexicon/lexiconSync.ml @@ -29,11 +29,11 @@ let alias_diff ~from status = 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 @@ -42,7 +42,7 @@ let alias_diff ~from status = with Not_found -> (domain_item,codomain_item)::acc) - status#lstatus.LexiconEngine.aliases [] + status#lstatus.LexiconTypes.aliases [] ;; let add_aliases_for_objs status = @@ -54,8 +54,8 @@ 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 diff --git a/matita/components/lexicon/lexiconSync.mli b/matita/components/lexicon/lexiconSync.mli index a081e53f1..f19906528 100644 --- a/matita/components/lexicon/lexiconSync.mli +++ b/matita/components/lexicon/lexiconSync.mli @@ -24,13 +24,12 @@ *) 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 diff --git a/matita/components/lexicon/lexiconTypes.ml b/matita/components/lexicon/lexiconTypes.ml new file mode 100644 index 000000000..f0cf75946 --- /dev/null +++ b/matita/components/lexicon/lexiconTypes.ml @@ -0,0 +1,56 @@ +(* 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 diff --git a/matita/components/lexicon/lexiconTypes.mli b/matita/components/lexicon/lexiconTypes.mli new file mode 100644 index 000000000..813b9955b --- /dev/null +++ b/matita/components/lexicon/lexiconTypes.mli @@ -0,0 +1,47 @@ +(* 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 diff --git a/matita/components/ng_library/nCicLibrary.mli b/matita/components/ng_library/nCicLibrary.mli index bad0d8975..b2015a952 100644 --- a/matita/components/ng_library/nCicLibrary.mli +++ b/matita/components/ng_library/nCicLibrary.mli @@ -12,6 +12,7 @@ (* $Id$ *) exception LibraryOutOfSync of string Lazy.t +exception IncludedFileNotCompiled of string * string type timestamp diff --git a/matita/components/statuses.txt b/matita/components/statuses.txt index 03b17e31d..e2be9b49b 100644 --- a/matita/components/statuses.txt +++ b/matita/components/statuses.txt @@ -1,11 +1,10 @@ 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 diff --git a/matita/matita/.depend b/matita/matita/.depend index e07465dfd..ffe6ee646 100644 --- a/matita/matita/.depend +++ b/matita/matita/.depend @@ -7,17 +7,17 @@ lablGraphviz.cmx: lablGraphviz.cmi 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: @@ -46,16 +46,14 @@ matitaMisc.cmo: buildTimeConf.cmo matitaMisc.cmi 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 @@ -71,7 +69,8 @@ matitaEngine.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: diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml index 5cf0ad95d..0c389d66f 100644 --- a/matita/matita/matitaEngine.ml +++ b/matita/matita/matitaEngine.ml @@ -51,12 +51,12 @@ let eval_macro_screenshot (status : GrafiteTypes.status) name = *) ;; -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 @@ -68,7 +68,7 @@ let eval_ast ?do_heavy_checks status (text,prefix_len,ast) = 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 @@ -81,7 +81,8 @@ let eval_ast ?do_heavy_checks status (text,prefix_len,ast) = 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 @@ -105,25 +106,26 @@ let eval_from_stream ~first_statement_only ~include_paths 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 diff --git a/matita/matita/matitaEngine.mli b/matita/matita/matitaEngine.mli index 945e7f348..e559d5a0c 100644 --- a/matita/matita/matitaEngine.mli +++ b/matita/matita/matitaEngine.mli @@ -24,12 +24,13 @@ *) 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 @@ -49,4 +50,4 @@ val eval_from_stream : 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 diff --git a/matita/matita/matitaExcPp.ml b/matita/matita/matitaExcPp.ml index f6bd9b90c..a36a723ae 100644 --- a/matita/matita/matitaExcPp.ml +++ b/matita/matita/matitaExcPp.ml @@ -114,10 +114,12 @@ let compact_disambiguation_errors all_passes errorll = 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 diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml index a2f03e056..a42500bd6 100644 --- a/matita/matita/matitaGui.ml +++ b/matita/matita/matitaGui.ml @@ -75,12 +75,6 @@ let save_moo grafite_status = 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 @@ -326,13 +320,13 @@ let rec interactive_error_interp ~all_passes 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 diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml index 78e0a13a5..4b7b376b4 100644 --- a/matita/matita/matitaMathView.ml +++ b/matita/matita/matitaMathView.ml @@ -1036,12 +1036,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) 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 ()); @@ -1104,7 +1098,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) 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 @@ -1136,7 +1129,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) | `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) @@ -1226,7 +1218,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) 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; @@ -1254,9 +1246,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) 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 diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index 6221e4901..864583d88 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -80,7 +80,7 @@ let eval_with_engine include_paths guistuff grafite_status user_goal 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 @@ -92,7 +92,7 @@ let eval_with_engine include_paths guistuff grafite_status user_goal 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 @@ -103,11 +103,10 @@ let eval_with_engine include_paths guistuff grafite_status user_goal * 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 _ -> @@ -115,13 +114,10 @@ let wrap_with_make include_paths (f : #LexiconEngine.status GrafiteParser.statem 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 @@ -209,17 +205,17 @@ script ex loc 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 @@ -280,10 +276,9 @@ class script ~(source_view: GSourceView2.source_view) 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 *) @@ -422,13 +417,7 @@ object (self) 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; @@ -700,11 +689,9 @@ object (self) 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 ???? *) @@ -717,7 +704,7 @@ object (self) 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 diff --git a/matita/matita/matitacLib.ml b/matita/matita/matitacLib.ml index cc0793c96..23a0ca15f 100644 --- a/matita/matita/matitacLib.ml +++ b/matita/matita/matitacLib.ml @@ -29,7 +29,7 @@ open Printf open GrafiteTypes -exception AttemptToInsertAnAlias of LexiconEngine.status +exception AttemptToInsertAnAlias of LexiconTypes.status let slash_n_RE = Pcre.regexp "\\n" ;; @@ -49,43 +49,6 @@ let clean_exit baseuri rc = 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 _ -> [] ;; @@ -160,7 +123,7 @@ let compile atstart options fname = 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 *) @@ -172,14 +135,6 @@ let compile atstart options fname = 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 @@ -220,19 +175,14 @@ let compile atstart options fname = | [] -> 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 @@ -332,29 +282,16 @@ module F = 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;;