From df1201e37d6f2631dc31ffc87b979a6c81180a3a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 18 Jun 2009 09:07:37 +0000 Subject: [PATCH] 1) grafiteWalker removed 2) ncommands and commands are now two distinct syntactic entries 3) NEstatus.status and LexiconEngine.status are now objects --- .../software/components/grafite/grafiteAst.ml | 5 +- .../components/grafite/grafiteAstPp.ml | 13 +- .../grafite_engine/grafiteEngine.ml | 180 +++++++++--------- .../components/grafite_engine/grafiteSync.ml | 15 +- .../components/grafite_engine/grafiteTypes.ml | 29 +-- .../grafite_engine/grafiteTypes.mli | 15 +- .../components/grafite_parser/.depend | 5 +- .../components/grafite_parser/.depend.opt | 7 +- .../components/grafite_parser/Makefile | 1 - .../components/grafite_parser/cicNotation2.ml | 16 +- .../grafite_parser/cicNotation2.mli | 14 +- .../grafite_parser/grafiteDisambiguate.ml | 73 +++---- .../grafite_parser/grafiteDisambiguate.mli | 16 +- .../grafite_parser/grafiteParser.ml | 129 +++++++------ .../grafite_parser/grafiteParser.mli | 14 +- .../grafite_parser/grafiteWalker.ml | 75 -------- .../grafite_parser/grafiteWalker.mli | 52 ----- .../components/grafite_parser/nEstatus.ml | 10 +- .../components/grafite_parser/nEstatus.mli | 10 +- .../components/grafite_parser/test_parser.ml | 2 +- .../components/lexicon/lexiconEngine.ml | 66 ++++--- .../components/lexicon/lexiconEngine.mli | 16 +- .../components/lexicon/lexiconSync.ml | 12 +- .../components/lexicon/lexiconSync.mli | 8 +- .../components/ng_tactics/nTacStatus.ml | 9 +- .../components/ng_tactics/nTacStatus.mli | 2 +- .../components/ng_tactics/nTactics.ml | 2 +- .../components/tptp_grafite/tptp2grafite.ml | 2 +- helm/software/matita/matita.ml | 2 +- helm/software/matita/matitaEngine.ml | 40 ++-- helm/software/matita/matitaGui.ml | 4 +- helm/software/matita/matitaScript.ml | 20 +- helm/software/matita/matitaWiki.ml | 10 +- helm/software/matita/matitacLib.ml | 10 +- 34 files changed, 349 insertions(+), 535 deletions(-) delete mode 100644 helm/software/components/grafite_parser/grafiteWalker.ml delete mode 100644 helm/software/components/grafite_parser/grafiteWalker.mli diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index fe060d415..6bf050fec 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -196,7 +196,6 @@ type ('term,'obj) command = int (* arity *) * int (* saturations *) | PreferCoercion of loc * 'term | Inverter of loc * string * 'term * bool list - | UnificationHint of loc * CicNotationPt.term * int (* term, precedence *) | Default of loc * string * UriManager.uri list | Drop of loc | Include of loc * bool (* normal? *) * string @@ -206,6 +205,9 @@ type ('term,'obj) command = | Set of loc * string * string | Print of loc * string | Qed of loc + +type ncommand = + | UnificationHint of loc * CicNotationPt.term * int (* term, precedence *) | NObj of loc * CicNotationPt.term CicNotationPt.obj | NUnivConstraint of loc * bool * NUri.uri * NUri.uri | NQed of loc @@ -226,6 +228,7 @@ type non_punctuation_tactical = type ('term, 'lazy_term, 'reduction, 'obj, 'ident) code = | Command of loc * ('term, 'obj) command + | NCommand of loc * ncommand | Macro of loc * ('term,'lazy_term) macro | NTactic of loc * ntactic list | Tactic of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic option diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index c1c83ee09..5f1213fa4 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -349,6 +349,13 @@ let pp_coercion ~term_pp t do_composites arity saturations= Printf.sprintf "coercion %s %d %d %s" (term_pp t) arity saturations (if do_composites then "" else "nocomposites") + +let pp_ncommand = function + | UnificationHint (_,t, n) -> + "unification hint " ^ string_of_int n ^ " " ^ CicNotationPp.pp_term t + | NObj (_,_) + | NUnivConstraint (_) -> "not supported" + | NQed (_) -> "nqed" let pp_command ~term_pp ~obj_pp = function | Index (_,_,uri) -> "Indexing " ^ UriManager.string_of_uri uri @@ -359,8 +366,6 @@ let pp_command ~term_pp ~obj_pp = function "prefer coercion " ^ term_pp t | Inverter (_,n,ty,params) -> "inverter " ^ n ^ " for " ^ term_pp ty ^ " " ^ List.fold_left (fun acc x -> acc ^ (match x with true -> "%" | _ -> "?")) "" params - | UnificationHint (_,t, n) -> - "unification hint " ^ string_of_int n ^ " " ^ CicNotationPp.pp_term t | Default (_,what,uris) -> pp_default what uris | Drop _ -> "drop" | Include (_,true,path) -> "include \"" ^ path ^ "\"" @@ -380,9 +385,6 @@ let pp_command ~term_pp ~obj_pp = function | None -> "") | Print (_,s) -> "print " ^ s | Set (_, name, value) -> Printf.sprintf "set \"%s\" \"%s\"" name value - | NObj (_,_) - | NUnivConstraint (_) -> "not supported" - | NQed (_) -> "nqed" | Pump (_) -> "not supported" let pp_punctuation_tactical = @@ -416,6 +418,7 @@ let pp_executable ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp = pp_non_punctuation_tactical tac ^ pp_punctuation_tactical punct | Command (_, cmd) -> pp_command ~term_pp ~obj_pp cmd ^ "." + | NCommand (_, cmd) -> pp_ncommand cmd ^ "." let pp_comment ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp = function diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index e0bcd031e..65b6683eb 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -488,11 +488,11 @@ let eval_unification_hint status t n = assert (metasenv=[]); let t = NCicUntrusted.apply_subst subst [] t in let status = GrafiteTypes.set_estatus estatus status in - let dstatus = - basic_eval_unification_hint (t,n) (GrafiteTypes.get_dstatus status) in - let dump = inject_unification_hint (t,n)::dstatus#dump in - let dstatus = dstatus#set_dump dump in - let status = GrafiteTypes.set_dstatus dstatus status in + let estatus = + basic_eval_unification_hint (t,n) (GrafiteTypes.get_estatus status) in + let dump = inject_unification_hint (t,n)::estatus#dump in + let estatus = estatus#set_dump dump in + let status = GrafiteTypes.set_estatus estatus status in status,`Old [] ;; @@ -667,6 +667,87 @@ let subst_metasenv_and_fix_names s = u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o}} ;; +let rec eval_ncommand opts status (text,prefix_len,cmd) = + match cmd with + | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n + | GrafiteAst.NQed loc -> + (match status.GrafiteTypes.ng_status with + | GrafiteTypes.ProofMode + { NTacStatus.istatus = + { NTacStatus.pstatus = pstatus; estatus = estatus } } -> + let uri,height,menv,subst,obj_kind = pstatus in + if menv <> [] then + raise + (GrafiteTypes.Command_error"You can't Qed an incomplete theorem") + else + let obj_kind = + NCicUntrusted.map_obj_kind + (NCicUntrusted.apply_subst subst []) obj_kind in + let height = NCicTypeChecker.height_of_obj_kind uri obj_kind in + (* fix the height inside the object *) + let rec fix () = function + | NCic.Const (NReference.Ref (u,spec)) when NUri.eq u uri -> + NCic.Const (NReference.reference_of_spec u + (match spec with + | NReference.Def _ -> NReference.Def height + | NReference.Fix (i,j,_) -> NReference.Fix(i,j,height) + | NReference.CoFix _ -> NReference.CoFix height + | NReference.Ind _ | NReference.Con _ + | NReference.Decl as s -> s)) + | t -> NCicUtils.map (fun _ () -> ()) () fix t + in + let obj_kind = + match obj_kind with + | NCic.Fixpoint _ -> + NCicUntrusted.map_obj_kind (fix ()) obj_kind + | _ -> obj_kind + in + let obj = uri,height,[],[],obj_kind in + NCicTypeChecker.typecheck_obj obj; + let estatus = NCicLibrary.add_obj estatus uri obj in + let objs = NCicElim.mk_elims obj in + let timestamp,uris_rev = + List.fold_left + (fun (estatus,uris_rev) (uri,_,_,_,_) as obj -> + NCicTypeChecker.typecheck_obj obj; + let estatus = NCicLibrary.add_obj estatus uri obj in + estatus,uri::uris_rev + ) (estatus,[]) objs in + let uris = uri::List.rev uris_rev in + GrafiteTypes.set_estatus estatus + {status with + GrafiteTypes.ng_status = + GrafiteTypes.CommandMode estatus },`New uris + | _ -> raise (GrafiteTypes.Command_error "Not in proof mode")) + | GrafiteAst.NObj (loc,obj) -> + let estatus = + match status.GrafiteTypes.ng_status with + | GrafiteTypes.ProofMode _ -> assert false + | GrafiteTypes.CommandMode es -> es + in + let estatus,obj = + GrafiteDisambiguate.disambiguate_nobj estatus + ~baseuri:(GrafiteTypes.get_baseuri status) (text,prefix_len,obj) in + let uri,height,nmenv,nsubst,nobj = obj in + let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in + let status = + { status with + GrafiteTypes.ng_status = + GrafiteTypes.ProofMode + (subst_metasenv_and_fix_names + { NTacStatus.gstatus = ninitial_stack; + istatus = { NTacStatus.pstatus = obj; estatus = estatus}}) + } + in + (match nmenv with + [] -> + eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc) + | _ -> status,`New []) + | GrafiteAst.NUnivConstraint (loc,strict,u1,u2) -> + NCicEnvironment.add_constraint strict [false,u1] [false,u2]; + status, `New [u1;u2] +;; + let rec eval_command = {ec_go = fun ~disambiguate_command opts status (text,prefix_len,cmd) -> let status,cmd = disambiguate_command status (text,prefix_len,cmd) in @@ -727,7 +808,6 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status Inversion_principle.build_inverter ~add_obj status uri indty_uri params in res,`Old uris - | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n | GrafiteAst.Default (loc, what, uris) as cmd -> LibraryObjects.set_default what uris; GrafiteTypes.add_moo_content [cmd] status,`Old [] @@ -745,11 +825,11 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status raise (IncludedFileNotCompiled (moopath_rw,baseuri)) in let status = eval_from_moo.efm_go status moopath in - let dstatus = GrafiteTypes.get_dstatus status in - let dstatus = + let estatus = GrafiteTypes.get_estatus status in + let estatus = NRstatus.Serializer.require ~baseuri:(NUri.uri_of_string baseuri) - dstatus in - let status = GrafiteTypes.set_dstatus dstatus status in + estatus in + let status = GrafiteTypes.set_estatus estatus status in (* debug let lt_uri = UriManager.uri_of_string "cic:/matita/nat/orders/lt.con" in let nat_uri = UriManager.uri_of_string "cic:/matita/nat/nat/nat.ind" in @@ -793,89 +873,11 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}, (*CSC: I throw away the arities *) `Old (uri::lemmas) - | GrafiteAst.NQed loc -> - (match status.GrafiteTypes.ng_status with - | GrafiteTypes.ProofMode - { NTacStatus.istatus = - { NTacStatus.pstatus = pstatus; estatus = estatus } } -> - let uri,height,menv,subst,obj_kind = pstatus in - if menv <> [] then - raise - (GrafiteTypes.Command_error"You can't Qed an incomplete theorem") - else - let obj_kind = - NCicUntrusted.map_obj_kind - (NCicUntrusted.apply_subst subst []) obj_kind in - let height = NCicTypeChecker.height_of_obj_kind uri obj_kind in - (* fix the height inside the object *) - let rec fix () = function - | NCic.Const (NReference.Ref (u,spec)) when NUri.eq u uri -> - NCic.Const (NReference.reference_of_spec u - (match spec with - | NReference.Def _ -> NReference.Def height - | NReference.Fix (i,j,_) -> NReference.Fix(i,j,height) - | NReference.CoFix _ -> NReference.CoFix height - | NReference.Ind _ | NReference.Con _ - | NReference.Decl as s -> s)) - | t -> NCicUtils.map (fun _ () -> ()) () fix t - in - let obj_kind = - match obj_kind with - | NCic.Fixpoint _ -> - NCicUntrusted.map_obj_kind (fix ()) obj_kind - | _ -> obj_kind - in - let obj = uri,height,[],[],obj_kind in - NCicTypeChecker.typecheck_obj obj; - let dstatus = estatus.NEstatus.rstatus in - let dstatus = NCicLibrary.add_obj dstatus uri obj in - let objs = NCicElim.mk_elims obj in - let timestamp,uris_rev = - List.fold_left - (fun (dstatus,uris_rev) (uri,_,_,_,_) as obj -> - NCicTypeChecker.typecheck_obj obj; - let dstatus = NCicLibrary.add_obj dstatus uri obj in - dstatus,uri::uris_rev - ) (dstatus,[]) objs in - let uris = uri::List.rev uris_rev in - GrafiteTypes.set_dstatus dstatus - {status with - GrafiteTypes.ng_status = - GrafiteTypes.CommandMode estatus },`New uris - | _ -> raise (GrafiteTypes.Command_error "Not in proof mode")) | GrafiteAst.Relation (loc, id, a, aeq, refl, sym, trans) -> Setoids.add_relation id a aeq refl sym trans; status, `Old [] (*CSC: TO BE FIXED *) | GrafiteAst.Set (loc, name, value) -> status, `Old [] (* GrafiteTypes.set_option status name value,[] *) - | GrafiteAst.NUnivConstraint (loc,strict,u1,u2) -> - NCicEnvironment.add_constraint strict [false,u1] [false,u2]; - status, `New [u1;u2] - | GrafiteAst.NObj (loc,obj) -> - let estatus = - match status.GrafiteTypes.ng_status with - | GrafiteTypes.ProofMode _ -> assert false - | GrafiteTypes.CommandMode es -> es - in - let estatus,obj = - GrafiteDisambiguate.disambiguate_nobj estatus - ~baseuri:(GrafiteTypes.get_baseuri status) (text,prefix_len,obj) in - let uri,height,nmenv,nsubst,nobj = obj in - let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in - let status = - { status with - GrafiteTypes.ng_status = - GrafiteTypes.ProofMode - (subst_metasenv_and_fix_names - { NTacStatus.gstatus = ninitial_stack; - istatus = { NTacStatus.pstatus = obj; estatus = estatus}}) - } - in - (match nmenv with - [] -> - eval_command.ec_go ~disambiguate_command opts status - ("",0,GrafiteAst.NQed Stdpp.dummy_loc) - | _ -> status,`New []) | GrafiteAst.Obj (loc,obj) -> let ext,name = match obj with @@ -988,6 +990,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status (punctuation_tactical_of_ast (text,prefix_len,punct)),`Old [] | GrafiteAst.Command (_, cmd) -> eval_command.ec_go ~disambiguate_command opts status (text,prefix_len,cmd) + | GrafiteAst.NCommand (_, cmd) -> + eval_ncommand opts status (text,prefix_len,cmd) | GrafiteAst.Macro (loc, macro) -> raise (Macro (loc,disambiguate_macro status (text,prefix_len,macro))) diff --git a/helm/software/components/grafite_engine/grafiteSync.ml b/helm/software/components/grafite_engine/grafiteSync.ml index 94170493b..74e2cf2e2 100644 --- a/helm/software/components/grafite_engine/grafiteSync.ml +++ b/helm/software/components/grafite_engine/grafiteSync.ml @@ -147,10 +147,10 @@ let add_coercion ~pack_coercion_obj ~add_composites status uri arity objects = lemmas @ status.GrafiteTypes.objects; } in - let dstatus = - NCicCoercion.index_old_db (CoercDb.dump ()) - (GrafiteTypes.get_dstatus status) in - let status = GrafiteTypes.set_dstatus dstatus status in + let estatus = + NCicCoercion.index_old_db (CoercDb.dump ()) (GrafiteTypes.get_estatus status) + in + let status = GrafiteTypes.set_estatus estatus status in status, lemmas let prefer_coercion s u = @@ -170,7 +170,7 @@ let time_travel ~present ~past = uri_list_diff present.GrafiteTypes.objects past.GrafiteTypes.objects in List.iter LibrarySync.remove_obj objs_to_remove; CoercDb.restore past.GrafiteTypes.coercions; - NCicLibrary.time_travel (GrafiteTypes.get_dstatus past) + NCicLibrary.time_travel (GrafiteTypes.get_estatus past) ;; let initial_status lexicon_status baseuri = { @@ -180,10 +180,7 @@ let initial_status lexicon_status baseuri = { coercions = CoercDb.empty_coerc_db; automation_cache = AutomationCache.empty (); baseuri = baseuri; - ng_status = GrafiteTypes.CommandMode { - NEstatus.lstatus = lexicon_status; - NEstatus.rstatus = new NRstatus.dumpable_status - }; + ng_status = GrafiteTypes.CommandMode (new NEstatus.status) } diff --git a/helm/software/components/grafite_engine/grafiteTypes.ml b/helm/software/components/grafite_engine/grafiteTypes.ml index 6033be8c2..82dae3d99 100644 --- a/helm/software/components/grafite_engine/grafiteTypes.ml +++ b/helm/software/components/grafite_engine/grafiteTypes.ml @@ -46,7 +46,7 @@ type proof_status = type ng_status = | ProofMode of NTacStatus.tac_status - | CommandMode of NEstatus.extra_status + | CommandMode of NEstatus.status type status = { moo_content_rev: GrafiteMarshal.moo; @@ -58,26 +58,6 @@ type status = { ng_status: ng_status; } -let get_lexicon x = - match x.ng_status with - | ProofMode t -> t.NTacStatus.istatus.NTacStatus.estatus.NEstatus.lstatus - | CommandMode e -> e.NEstatus.lstatus -;; - -let set_lexicon new_lexicon_status new_grafite_status = - { new_grafite_status with ng_status = - match new_grafite_status.ng_status with - | CommandMode estatus -> - CommandMode - { estatus with NEstatus.lstatus = new_lexicon_status } - | ProofMode t -> - ProofMode - { t with NTacStatus.istatus = - { t.NTacStatus.istatus with NTacStatus.estatus = - { t.NTacStatus.istatus.NTacStatus.estatus with NEstatus.lstatus = - new_lexicon_status }}}} -;; - let get_estatus x = match x.ng_status with | ProofMode t -> t.NTacStatus.istatus.NTacStatus.estatus @@ -94,13 +74,6 @@ let set_estatus e x = | CommandMode _ -> CommandMode e} ;; -let get_dstatus x = (get_estatus x).NEstatus.rstatus;; - -let set_dstatus h x = - let estatus = get_estatus x in - set_estatus { estatus with NEstatus.rstatus = h } x -;; - let get_current_proof status = match status.proof_status with | Incomplete_proof { proof = p } -> p diff --git a/helm/software/components/grafite_engine/grafiteTypes.mli b/helm/software/components/grafite_engine/grafiteTypes.mli index 8ed9fe489..867e5299e 100644 --- a/helm/software/components/grafite_engine/grafiteTypes.mli +++ b/helm/software/components/grafite_engine/grafiteTypes.mli @@ -44,7 +44,7 @@ type proof_status = type ng_status = | ProofMode of NTacStatus.tac_status - | CommandMode of NEstatus.extra_status + | CommandMode of NEstatus.status type status = { moo_content_rev: GrafiteMarshal.moo; @@ -61,11 +61,6 @@ val dump_status : status -> unit (** list is not reversed, head command will be the first emitted *) val add_moo_content: GrafiteMarshal.ast_command list -> status -> status -(* REOMVE ME -val get_option : status -> string -> option_value -val get_string_option : status -> string -> string -val set_option : status -> string -> string -> status -*) val get_baseuri: status -> string val get_current_proof: status -> ProofEngineTypes.proof @@ -73,12 +68,8 @@ val get_proof_metasenv: status -> Cic.metasenv val get_stack: status -> Continuationals.Stack.t val get_proof_context : status -> int -> Cic.context val get_proof_conclusion : status -> int -> Cic.term -val get_lexicon : status -> LexiconEngine.status -val get_estatus : status -> NEstatus.extra_status -val get_dstatus : status -> NRstatus.dumpable_status +val get_estatus : status -> NEstatus.status val set_stack: Continuationals.Stack.t -> status -> status val set_metasenv: Cic.metasenv -> status -> status -val set_lexicon : LexiconEngine.status -> status -> status -val set_estatus : NEstatus.extra_status -> status -> status -val set_dstatus : NRstatus.dumpable_status -> status -> status +val set_estatus : NEstatus.status -> status -> status diff --git a/helm/software/components/grafite_parser/.depend b/helm/software/components/grafite_parser/.depend index e970a6d1c..2766b04d0 100644 --- a/helm/software/components/grafite_parser/.depend +++ b/helm/software/components/grafite_parser/.depend @@ -2,8 +2,7 @@ dependenciesParser.cmi: grafiteParser.cmi: cicNotation2.cmi: nEstatus.cmi: -grafiteDisambiguate.cmi: -grafiteWalker.cmi: grafiteParser.cmi +grafiteDisambiguate.cmi: nEstatus.cmi print_grammar.cmi: dependenciesParser.cmo: dependenciesParser.cmi dependenciesParser.cmx: dependenciesParser.cmi @@ -15,7 +14,5 @@ nEstatus.cmo: nEstatus.cmi nEstatus.cmx: nEstatus.cmi grafiteDisambiguate.cmo: grafiteDisambiguate.cmi grafiteDisambiguate.cmx: grafiteDisambiguate.cmi -grafiteWalker.cmo: grafiteParser.cmi grafiteWalker.cmi -grafiteWalker.cmx: grafiteParser.cmx grafiteWalker.cmi print_grammar.cmo: print_grammar.cmi print_grammar.cmx: print_grammar.cmi diff --git a/helm/software/components/grafite_parser/.depend.opt b/helm/software/components/grafite_parser/.depend.opt index 86bad9e17..2766b04d0 100644 --- a/helm/software/components/grafite_parser/.depend.opt +++ b/helm/software/components/grafite_parser/.depend.opt @@ -3,7 +3,6 @@ grafiteParser.cmi: cicNotation2.cmi: nEstatus.cmi: grafiteDisambiguate.cmi: nEstatus.cmi -grafiteWalker.cmi: grafiteParser.cmi print_grammar.cmi: dependenciesParser.cmo: dependenciesParser.cmi dependenciesParser.cmx: dependenciesParser.cmi @@ -13,9 +12,7 @@ cicNotation2.cmo: grafiteParser.cmi cicNotation2.cmi cicNotation2.cmx: grafiteParser.cmx cicNotation2.cmi nEstatus.cmo: nEstatus.cmi nEstatus.cmx: nEstatus.cmi -grafiteDisambiguate.cmo: nEstatus.cmi grafiteDisambiguate.cmi -grafiteDisambiguate.cmx: nEstatus.cmx grafiteDisambiguate.cmi -grafiteWalker.cmo: grafiteParser.cmi grafiteWalker.cmi -grafiteWalker.cmx: grafiteParser.cmx grafiteWalker.cmi +grafiteDisambiguate.cmo: grafiteDisambiguate.cmi +grafiteDisambiguate.cmx: grafiteDisambiguate.cmi print_grammar.cmo: print_grammar.cmi print_grammar.cmx: print_grammar.cmi diff --git a/helm/software/components/grafite_parser/Makefile b/helm/software/components/grafite_parser/Makefile index 3a4acb3e1..892325d52 100644 --- a/helm/software/components/grafite_parser/Makefile +++ b/helm/software/components/grafite_parser/Makefile @@ -7,7 +7,6 @@ INTERFACE_FILES = \ cicNotation2.mli \ nEstatus.mli \ grafiteDisambiguate.mli \ - grafiteWalker.mli \ print_grammar.mli \ $(NULL) IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) diff --git a/helm/software/components/grafite_parser/cicNotation2.ml b/helm/software/components/grafite_parser/cicNotation2.ml index b3c8a59cc..e02517177 100644 --- a/helm/software/components/grafite_parser/cicNotation2.ml +++ b/helm/software/components/grafite_parser/cicNotation2.ml @@ -25,25 +25,13 @@ (* $Id$ *) -let load_notation ~include_paths fname = +let load_notation status ~include_paths fname = let ic = open_in fname in let lexbuf = Ulexing.from_utf8_channel ic in - let status = ref LexiconEngine.initial_status in + let status = ref status in try while true do status := fst (GrafiteParser.parse_statement ~include_paths lexbuf !status) done; assert false with End_of_file -> close_in ic; !status - -let parse_environment ~include_paths str = - let lexbuf = Ulexing.from_utf8_string str in - let status = ref LexiconEngine.initial_status in - try - while true do - status := fst (GrafiteParser.parse_statement ~include_paths lexbuf !status) - done; - assert false - with End_of_file -> - !status.LexiconEngine.aliases, - !status.LexiconEngine.multi_aliases diff --git a/helm/software/components/grafite_parser/cicNotation2.mli b/helm/software/components/grafite_parser/cicNotation2.mli index 9b47d8d6d..6c9c44167 100644 --- a/helm/software/components/grafite_parser/cicNotation2.mli +++ b/helm/software/components/grafite_parser/cicNotation2.mli @@ -23,15 +23,7 @@ * http://helm.cs.unibo.it/ *) -(** Note: notation is also loaded, but it cannot be undone since the - notation_ids part of the status is thrown away; - so far this function is useful only in Whelp *) -val parse_environment: - include_paths:string list -> - string -> - LexiconAst.alias_spec DisambiguateTypes.Environment.t * - LexiconAst.alias_spec list DisambiguateTypes.Environment.t - - (** @param fname file from which load notation *) -val load_notation: include_paths:string list -> string -> LexiconEngine.status +val load_notation: + #LexiconEngine.status as 'status -> include_paths:string list -> string -> + 'status diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index 4aadd7077..a0558d9f6 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -182,8 +182,8 @@ term = let (diff, metasenv, subst, cic, _) = singleton "first" (CicDisambiguate.disambiguate_term - ~aliases:lexicon_status.LexiconEngine.aliases - ~expty ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) + ~aliases:lexicon_status#lstatus.LexiconEngine.aliases + ~expty ~universe:(Some lexicon_status#lstatus.LexiconEngine.multi_aliases) ~lookup_in_library ~mk_choice:cic_mk_choice ~mk_implicit @@ -200,19 +200,18 @@ let disambiguate_nterm expty estatus context metasenv subst thing let diff, metasenv, subst, cic = singleton "first" (NCicDisambiguate.disambiguate_term - ~rdb:estatus.NEstatus.rstatus - ~aliases:estatus.NEstatus.lstatus.LexiconEngine.aliases + ~rdb:estatus + ~aliases:estatus#lstatus.LexiconEngine.aliases ~expty - ~universe:(Some estatus.NEstatus.lstatus.LexiconEngine.multi_aliases) + ~universe:(Some estatus#lstatus.LexiconEngine.multi_aliases) ~lookup_in_library:nlookup_in_library ~mk_choice:ncic_mk_choice ~mk_implicit ~description_of_alias:LexiconAst.description_of_alias ~context ~metasenv ~subst thing) in - let lexicon_status = - LexiconEngine.set_proof_aliases estatus.NEstatus.lstatus diff in - metasenv, subst, { estatus with NEstatus.lstatus = lexicon_status }, cic + let estatus = LexiconEngine.set_proof_aliases estatus diff in + metasenv, subst, estatus, cic ;; @@ -231,8 +230,8 @@ let disambiguate_lazy_term expty text prefix_len lexicon_status_ref term = ~mk_choice:cic_mk_choice ~mk_implicit ~description_of_alias:LexiconAst.description_of_alias - ~initial_ugraph:ugraph ~aliases:lexicon_status.LexiconEngine.aliases - ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) + ~initial_ugraph:ugraph ~aliases:lexicon_status#lstatus.LexiconEngine.aliases + ~universe:(Some lexicon_status#lstatus.LexiconEngine.multi_aliases) ~context ~metasenv ~subst:[] (text,prefix_len,term) ~expty) in let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in @@ -688,14 +687,14 @@ let disambiguate_obj estatus ?baseuri metasenv (text,prefix_len,obj) = (try (match NCicDisambiguate.disambiguate_obj - ~rdb:estatus.NEstatus.rstatus + ~rdb:estatus ~lookup_in_library:nlookup_in_library ~description_of_alias:LexiconAst.description_of_alias ~mk_choice:ncic_mk_choice ~mk_implicit ~uri:(OCic2NCic.nuri_of_ouri uri) - ~aliases:estatus.NEstatus.lstatus.LexiconEngine.aliases - ~universe:(Some estatus.NEstatus.lstatus.LexiconEngine.multi_aliases) + ~aliases:estatus#lstatus.LexiconEngine.aliases + ~universe:(Some estatus#lstatus.LexiconEngine.multi_aliases) (text,prefix_len,obj) with | [_,_,_,obj],_ -> @@ -728,7 +727,6 @@ let disambiguate_obj estatus ?baseuri metasenv (text,prefix_len,obj) = (* let time = Unix.gettimeofday () in *) - let lexicon_status = estatus.NEstatus.lstatus in let (diff, metasenv, _, cic, _) = singleton "third" (CicDisambiguate.disambiguate_obj @@ -736,8 +734,8 @@ let disambiguate_obj estatus ?baseuri metasenv (text,prefix_len,obj) = ~mk_choice:cic_mk_choice ~mk_implicit ~description_of_alias:LexiconAst.description_of_alias - ~aliases:lexicon_status.LexiconEngine.aliases - ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) + ~aliases:estatus#lstatus.LexiconEngine.aliases + ~universe:(Some estatus#lstatus.LexiconEngine.multi_aliases) ~uri:(Some uri) (text,prefix_len,obj)) in @@ -751,8 +749,8 @@ let disambiguate_obj estatus ?baseuri metasenv (text,prefix_len,obj) = (* try_new (Some cic); *) - let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in - { estatus with NEstatus.lstatus = lexicon_status }, metasenv, cic + let estatus = LexiconEngine.set_proof_aliases estatus diff in + estatus, metasenv, cic with | Sys.Break as exn -> raise exn @@ -783,20 +781,18 @@ let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) = ~mk_choice:ncic_mk_choice ~mk_implicit ~uri:(OCic2NCic.nuri_of_ouri uri) - ~rdb:estatus.NEstatus.rstatus - ~aliases:estatus.NEstatus.lstatus.LexiconEngine.aliases - ~universe:(Some estatus.NEstatus.lstatus.LexiconEngine.multi_aliases) + ~rdb:estatus + ~aliases:estatus#lstatus.LexiconEngine.aliases + ~universe:(Some estatus#lstatus.LexiconEngine.multi_aliases) (text,prefix_len,obj)) in - let lexicon_status = - LexiconEngine.set_proof_aliases estatus.NEstatus.lstatus diff in - { estatus with NEstatus.lstatus = lexicon_status }, cic + let estatus = LexiconEngine.set_proof_aliases estatus diff in + estatus, cic ;; let disambiguate_command estatus ?baseuri metasenv (text,prefix_len,cmd)= match cmd with - | GrafiteAst.NObj(loc,obj) -> estatus, metasenv, GrafiteAst.NObj(loc,obj) | GrafiteAst.Index(loc,key,uri) -> - let lexicon_status_ref = ref estatus.NEstatus.lstatus in + let lexicon_status_ref = ref estatus in let disambiguate_term = disambiguate_term None text prefix_len lexicon_status_ref [] in let disambiguate_term_option metasenv = @@ -807,41 +803,34 @@ let disambiguate_command estatus ?baseuri metasenv (text,prefix_len,cmd)= metasenv, Some t in let metasenv,key = disambiguate_term_option metasenv key in - { estatus with NEstatus.lstatus = !lexicon_status_ref }, - metasenv,GrafiteAst.Index(loc,key,uri) + !lexicon_status_ref,metasenv,GrafiteAst.Index(loc,key,uri) | GrafiteAst.Select (loc,uri) -> estatus, metasenv, GrafiteAst.Select(loc,uri) | GrafiteAst.Pump(loc,i) -> estatus, metasenv, GrafiteAst.Pump(loc,i) | GrafiteAst.PreferCoercion (loc,t) -> - let lexicon_status_ref = ref estatus.NEstatus.lstatus in + let lexicon_status_ref = ref estatus in let disambiguate_term = disambiguate_term None text prefix_len lexicon_status_ref [] in let metasenv,t = disambiguate_term metasenv t in - { estatus with NEstatus.lstatus = !lexicon_status_ref}, - metasenv, GrafiteAst.PreferCoercion (loc,t) + !lexicon_status_ref, metasenv, GrafiteAst.PreferCoercion (loc,t) | GrafiteAst.Coercion (loc,t,b,a,s) -> - let lexicon_status_ref = ref estatus.NEstatus.lstatus in + let lexicon_status_ref = ref estatus in let disambiguate_term = disambiguate_term None text prefix_len lexicon_status_ref [] in let metasenv,t = disambiguate_term metasenv t in - { estatus with NEstatus.lstatus = !lexicon_status_ref }, - metasenv, GrafiteAst.Coercion (loc,t,b,a,s) + !lexicon_status_ref, metasenv, GrafiteAst.Coercion (loc,t,b,a,s) | GrafiteAst.Inverter (loc,n,indty,params) -> - let lexicon_status_ref = ref estatus.NEstatus.lstatus in + let lexicon_status_ref = ref estatus in let disambiguate_term = disambiguate_term None text prefix_len lexicon_status_ref [] in let metasenv,indty = disambiguate_term metasenv indty in - { estatus with NEstatus.lstatus = !lexicon_status_ref }, - metasenv, GrafiteAst.Inverter (loc,n,indty,params) - | GrafiteAst.UnificationHint _ + !lexicon_status_ref, metasenv, GrafiteAst.Inverter (loc,n,indty,params) | GrafiteAst.Default _ | GrafiteAst.Drop _ | GrafiteAst.Include _ | GrafiteAst.Print _ | GrafiteAst.Qed _ - | GrafiteAst.NQed _ - | GrafiteAst.NUnivConstraint _ | GrafiteAst.Set _ as cmd -> estatus,metasenv,cmd | GrafiteAst.Obj (loc,obj) -> @@ -849,7 +838,7 @@ let disambiguate_command estatus ?baseuri metasenv (text,prefix_len,cmd)= disambiguate_obj estatus ?baseuri metasenv (text,prefix_len,obj)in estatus, metasenv, GrafiteAst.Obj (loc,obj) | GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) -> - let lexicon_status_ref = ref estatus.NEstatus.lstatus in + let lexicon_status_ref = ref estatus in let disambiguate_term = disambiguate_term None text prefix_len lexicon_status_ref [] in let disambiguate_term_option metasenv = @@ -864,7 +853,7 @@ let disambiguate_command estatus ?baseuri metasenv (text,prefix_len,cmd)= let metasenv,refl = disambiguate_term_option metasenv refl in let metasenv,sym = disambiguate_term_option metasenv sym in let metasenv,trans = disambiguate_term_option metasenv trans in - { estatus with NEstatus.lstatus = !lexicon_status_ref }, metasenv, + !lexicon_status_ref, metasenv, GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) let disambiguate_macro diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.mli b/helm/software/components/grafite_parser/grafiteDisambiguate.mli index 11fcbab1d..0592de671 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.mli +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.mli @@ -35,21 +35,21 @@ type lazy_tactic = GrafiteAst.tactic val disambiguate_tactic: - LexiconEngine.status ref -> + #LexiconEngine.status ref -> Cic.context -> Cic.metasenv -> int option -> tactic Disambiguate.disambiguator_input -> Cic.metasenv * lazy_tactic val disambiguate_command: - NEstatus.extra_status -> + #NEstatus.status as 'status -> ?baseuri:string -> Cic.metasenv -> ((CicNotationPt.term,CicNotationPt.term CicNotationPt.obj) GrafiteAst.command) Disambiguate.disambiguator_input -> - NEstatus.extra_status * Cic.metasenv * (Cic.term,Cic.obj) GrafiteAst.command + 'status * Cic.metasenv * (Cic.term,Cic.obj) GrafiteAst.command val disambiguate_macro: - LexiconEngine.status ref -> + #LexiconEngine.status ref -> Cic.metasenv -> Cic.context -> ((CicNotationPt.term,CicNotationPt.term) GrafiteAst.macro) Disambiguate.disambiguator_input -> @@ -57,16 +57,16 @@ val disambiguate_macro: val disambiguate_nterm : NCic.term option -> - NEstatus.extra_status -> + (#NEstatus.status as 'status) -> NCic.context -> NCic.metasenv -> NCic.substitution -> CicNotationPt.term Disambiguate.disambiguator_input -> - NCic.metasenv * NCic.substitution * NEstatus.extra_status * NCic.term + NCic.metasenv * NCic.substitution * 'status * NCic.term val disambiguate_nobj : - NEstatus.extra_status -> + #NEstatus.status as 'status -> ?baseuri:string -> (CicNotationPt.term CicNotationPt.obj) Disambiguate.disambiguator_input -> - NEstatus.extra_status * NCic.obj + 'status * NCic.obj type pattern = CicNotationPt.term Disambiguate.disambiguator_input option * diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 214a2d10e..ea74231ad 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -39,21 +39,23 @@ type 'a localized_option = type ast_statement = (N.term, N.term, N.term G.reduction, N.term N.obj, string) G.statement -type statement = - ?never_include:bool -> include_paths:string list -> LE.status -> - LE.status * ast_statement localized_option +type 'status statement = + ?never_include:bool -> + (* do not call LexiconEngine to do includes, always raise NoInclusionPerformed *) + include_paths:string list -> (#LE.status as 'status) -> + 'status * ast_statement localized_option -type parser_status = { +type 'status parser_status = { grammar : Grammar.g; term : N.term Grammar.Entry.e; - statement : statement Grammar.Entry.e; + statement : #LE.status as 'status statement Grammar.Entry.e; } let grafite_callback = ref (fun _ _ -> ()) -let set_grafite_callback cb = grafite_callback := cb +let set_grafite_callback cb = grafite_callback := Obj.magic cb let lexicon_callback = ref (fun _ _ -> ()) -let set_lexicon_callback cb = lexicon_callback := cb +let set_lexicon_callback cb = lexicon_callback := Obj.magic cb let initial_parser () = let grammar = CicNotationParser.level2_ast_grammar () in @@ -68,7 +70,7 @@ let add_raw_attribute ~text t = N.AttributedTerm (`Raw text, t) let default_associativity = Gramext.NonA -let mk_rec_corec ng ind_kind defs loc = +let mk_rec_corec ind_kind defs loc = (* In case of mutual definitions here we produce just the syntax tree for the first one. The others will be generated from the completely specified term just before @@ -93,12 +95,15 @@ let mk_rec_corec ng ind_kind defs loc = else `MutualDefinition in - if ng then - G.NObj (loc, N.Theorem(flavour, name, ty, - Some (N.LetRec (ind_kind, defs, body)))) - else - G.Obj (loc, N.Theorem(flavour, name, ty, - Some (N.LetRec (ind_kind, defs, body)))) + (loc, N.Theorem(flavour, name, ty, Some (N.LetRec (ind_kind, defs, body)))) + +let nmk_rec_corec ind_kind defs loc = + let loc,t = mk_rec_corec ind_kind defs loc in + G.NObj (loc,t) + +let mk_rec_corec ind_kind defs loc = + let loc,t = mk_rec_corec ind_kind defs loc in + G.Obj (loc,t) let npunct_of_punct = function | G.Branch loc -> G.NBranch loc @@ -773,56 +778,23 @@ EXTEND loc,path,true,L.WithoutPreferences ]]; - grafite_command: [ [ - IDENT "set"; n = QSTRING; v = QSTRING -> - G.Set (loc, n, v) - | IDENT "drop" -> G.Drop loc - | IDENT "print"; s = IDENT -> G.Print (loc,s) - | IDENT "qed" -> G.Qed loc - | IDENT "nqed" -> G.NQed loc - | IDENT "variant" ; name = IDENT; SYMBOL ":"; - typ = term; SYMBOL <:unicode> ; newname = IDENT -> - G.Obj (loc, - N.Theorem - (`Variant,name,typ,Some (N.Ident (newname, None)))) + grafite_ncommand: [ [ + IDENT "nqed" -> G.NQed loc | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term; body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> G.NObj (loc, N.Theorem (nflavour, name, typ, body)) | nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode> (* ≝ *); body = term -> G.NObj (loc, N.Theorem (nflavour, name, N.Implicit, Some body)) - | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term; - body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> - G.Obj (loc, N.Theorem (flavour, name, typ, body)) - | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode> (* ≝ *); - body = term -> - G.Obj (loc, - N.Theorem (flavour, name, N.Implicit, Some body)) - | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term -> - G.Obj (loc, N.Theorem (`Axiom, name, typ, None)) | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term -> G.NObj (loc, N.Theorem (`Axiom, name, typ, None)) - | LETCOREC ; defs = let_defs -> - mk_rec_corec false `CoInductive defs loc - | LETREC ; defs = let_defs -> - mk_rec_corec false `Inductive defs loc | NLETCOREC ; defs = let_defs -> - mk_rec_corec true `CoInductive defs loc + nmk_rec_corec `CoInductive defs loc | NLETREC ; defs = let_defs -> - mk_rec_corec true `Inductive defs loc - | IDENT "inductive"; spec = inductive_spec -> - let (params, ind_types) = spec in - G.Obj (loc, N.Inductive (params, ind_types)) + nmk_rec_corec `Inductive defs loc | IDENT "ninductive"; spec = inductive_spec -> let (params, ind_types) = spec in G.NObj (loc, N.Inductive (params, ind_types)) - | IDENT "coinductive"; spec = inductive_spec -> - let (params, ind_types) = spec in - let ind_types = (* set inductive flags to false (coinductive) *) - List.map (fun (name, _, term, ctors) -> (name, false, term, ctors)) - ind_types - in - G.Obj (loc, N.Inductive (params, ind_types)) | IDENT "ncoinductive"; spec = inductive_spec -> let (params, ind_types) = spec in let ind_types = (* set inductive flags to false (coinductive) *) @@ -851,6 +823,46 @@ EXTEND | _ -> raise (Failure "only a sort can be constrained") in G.NUnivConstraint (loc, strict,u1,u2) + | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term -> + G.UnificationHint (loc, t, n) + | IDENT "nrecord" ; (params,name,ty,fields) = record_spec -> + G.NObj (loc, N.Record (params,name,ty,fields)) + ]]; + + grafite_command: [ [ + IDENT "set"; n = QSTRING; v = QSTRING -> + G.Set (loc, n, v) + | IDENT "drop" -> G.Drop loc + | IDENT "print"; s = IDENT -> G.Print (loc,s) + | IDENT "qed" -> G.Qed loc + | IDENT "variant" ; name = IDENT; SYMBOL ":"; + typ = term; SYMBOL <:unicode> ; newname = IDENT -> + G.Obj (loc, + N.Theorem + (`Variant,name,typ,Some (N.Ident (newname, None)))) + | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term; + body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> + G.Obj (loc, N.Theorem (flavour, name, typ, body)) + | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode> (* ≝ *); + body = term -> + G.Obj (loc, + N.Theorem (flavour, name, N.Implicit, Some body)) + | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term -> + G.Obj (loc, N.Theorem (`Axiom, name, typ, None)) + | LETCOREC ; defs = let_defs -> + mk_rec_corec `CoInductive defs loc + | LETREC ; defs = let_defs -> + mk_rec_corec `Inductive defs loc + | IDENT "inductive"; spec = inductive_spec -> + let (params, ind_types) = spec in + G.Obj (loc, N.Inductive (params, ind_types)) + | IDENT "coinductive"; spec = inductive_spec -> + let (params, ind_types) = spec in + let ind_types = (* set inductive flags to false (coinductive) *) + List.map (fun (name, _, term, ctors) -> (name, false, term, ctors)) + ind_types + in + G.Obj (loc, N.Inductive (params, ind_types)) | IDENT "coercion" ; t = [ u = URI -> N.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ; arity = OPT int ; saturations = OPT int; @@ -864,16 +876,12 @@ EXTEND G.PreferCoercion (loc, t) | IDENT "pump" ; steps = int -> G.Pump(loc,steps) - | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term -> - G.UnificationHint (loc, t, n) | IDENT "inverter"; name = IDENT; IDENT "for"; indty = tactic_term; paramspec = inverter_param_list -> G.Inverter (loc, name, indty, paramspec) | IDENT "record" ; (params,name,ty,fields) = record_spec -> G.Obj (loc, N.Record (params,name,ty,fields)) - | IDENT "nrecord" ; (params,name,ty,fields) = record_spec -> - G.NObj (loc, N.Record (params,name,ty,fields)) | IDENT "default" ; what = QSTRING ; uris = LIST1 URI -> let uris = List.map UriManager.uri_of_string uris in G.Default (loc,what,uris) @@ -898,6 +906,7 @@ EXTEND ]]; executable: [ [ cmd = grafite_command; SYMBOL "." -> G.Command (loc, cmd) + | ncmd = grafite_ncommand; SYMBOL "." -> G.NCommand (loc, ncmd) | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical -> G.Tactic (loc, Some tac, punct) | punct = punctuation_tactical -> G.Tactic (loc, None, punct) @@ -929,19 +938,19 @@ EXTEND [ ex = executable -> fun ?(never_include=false) ~include_paths status -> let stm = G.Executable (loc, ex) in - !grafite_callback status stm; + Obj.magic !grafite_callback status stm; status, LSome stm | com = comment -> fun ?(never_include=false) ~include_paths status -> let stm = G.Comment (loc, com) in - !grafite_callback status stm; + Obj.magic !grafite_callback status stm; status, LSome stm | (iloc,fname,normal,mode) = include_command ; SYMBOL "." -> fun ?(never_include=false) ~include_paths status -> let stm = G.Executable (loc, G.Command (loc, G.Include (iloc, normal, fname))) in - !grafite_callback status stm; + Obj.magic !grafite_callback status stm; let _root, buri, fullpath, _rrelpath = Librarian.baseuri_of_script ~include_paths fname in @@ -983,9 +992,9 @@ let exc_located_wrapper f = let parse_statement lexbuf = exc_located_wrapper - (fun () -> (Grammar.Entry.parse !grafite_parser.statement (Obj.magic lexbuf))) + (fun () -> (Grammar.Entry.parse (Obj.magic !grafite_parser.statement) (Obj.magic lexbuf))) -let statement () = !grafite_parser.statement +let statement () = Obj.magic !grafite_parser.statement let history = ref [] ;; diff --git a/helm/software/components/grafite_parser/grafiteParser.mli b/helm/software/components/grafite_parser/grafiteParser.mli index 1413e93fd..08015d8dd 100644 --- a/helm/software/components/grafite_parser/grafiteParser.mli +++ b/helm/software/components/grafite_parser/grafiteParser.mli @@ -35,24 +35,24 @@ type ast_statement = exception NoInclusionPerformed of string (* full path *) -type statement = +type 'status statement = ?never_include:bool -> (* do not call LexiconEngine to do includes, always raise NoInclusionPerformed *) include_paths:string list -> - LexiconEngine.status -> - LexiconEngine.status * ast_statement localized_option + (#LexiconEngine.status as 'status) -> + 'status * ast_statement localized_option -val parse_statement: Ulexing.lexbuf -> statement (** @raise End_of_file *) +val parse_statement: Ulexing.lexbuf -> #LexiconEngine.status statement (** @raise End_of_file *) -val statement: unit -> statement Grammar.Entry.e +val statement: unit -> #LexiconEngine.status statement Grammar.Entry.e (* this callback is called before every grafite statement *) val set_grafite_callback: - (LexiconEngine.status -> ast_statement -> unit) -> unit + (#LexiconEngine.status -> ast_statement -> unit) -> unit (* this callback is called before every lexicon command *) val set_lexicon_callback: - (LexiconEngine.status -> LexiconAst.command -> unit) -> unit + (#LexiconEngine.status -> LexiconAst.command -> unit) -> unit val push : unit -> unit val pop : unit -> unit diff --git a/helm/software/components/grafite_parser/grafiteWalker.ml b/helm/software/components/grafite_parser/grafiteWalker.ml deleted file mode 100644 index 7e722bccf..000000000 --- a/helm/software/components/grafite_parser/grafiteWalker.ml +++ /dev/null @@ -1,75 +0,0 @@ -(* Copyright (C) 2006, 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 statement_test = - GrafiteParser.ast_statement GrafiteParser.localized_option -> bool - -let get_loc = - function - | GrafiteParser.LSome (GrafiteAst.Executable (loc, _)) - | GrafiteParser.LSome (GrafiteAst.Comment (loc, _)) - | GrafiteParser.LNone loc -> - loc - -let grep_statement ?(status = LexiconEngine.initial_status) ?(callback = ignore) - ~fname ~include_paths test -= - let content = HExtlib.input_file fname in - let lexbuf = Ulexing.from_utf8_string content in - let parse_fun status = - GrafiteParser.parse_statement lexbuf ~include_paths status in - let rec exaust acc status = (* extract "interesting" statement locations *) - let stm = - try Some (parse_fun status) - with End_of_file -> None in - match stm with - | None -> List.rev acc - | Some (status, stm) when test stm -> (* "interesting" statement *) - let loc_begin, loc_end = HExtlib.loc_of_floc (get_loc stm) in - let raw_statement = - Netconversion.ustring_sub `Enc_utf8 loc_begin (loc_end - loc_begin) - content in - callback raw_statement; - exaust (raw_statement :: acc) status - | Some (status, _stm) -> exaust acc status in - exaust [] status - -let ma_extension_test fname = Filename.check_suffix fname ".ma" - -let rgrep_statement ?status ?callback ?(fname_test = ma_extension_test) - ~dirname ~include_paths test -= - let files = HExtlib.find ~test:fname_test dirname in - List.flatten - (List.map - (fun fname -> - let callback = - match callback with - | None -> None - | Some f -> Some (fun s -> f (fname, s)) in - List.map (fun raw -> fname, raw) - (grep_statement ?status ?callback ~fname ~include_paths test)) - files) - diff --git a/helm/software/components/grafite_parser/grafiteWalker.mli b/helm/software/components/grafite_parser/grafiteWalker.mli deleted file mode 100644 index c9df8ab48..000000000 --- a/helm/software/components/grafite_parser/grafiteWalker.mli +++ /dev/null @@ -1,52 +0,0 @@ -(* Copyright (C) 2006, 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 statement_test = - GrafiteParser.ast_statement GrafiteParser.localized_option -> bool - - (** @param status initial status, defaults to LexiconEngine.initial_status - * @param callback if given it will be invoked as soon as a matching - * statement is found (i.e. it provides incremental notification in case - * grepping takes a while) *) -val grep_statement: - ?status: LexiconEngine.status -> - ?callback: (string -> unit) -> - fname:string -> - include_paths: string list -> - statement_test -> - string list - - (** As above, but act on all file (recursively) located under directory - * dirname whose name matches fname_test. Default test matches files with - * extension ".ma". - * @return list of pairs , as "grep -H" would do *) -val rgrep_statement: - ?status: LexiconEngine.status -> - ?callback: (string * string -> unit) -> - ?fname_test:(string -> bool) -> dirname:string -> - include_paths: string list -> - statement_test -> - (string * string) list - diff --git a/helm/software/components/grafite_parser/nEstatus.ml b/helm/software/components/grafite_parser/nEstatus.ml index 2ae7d01e4..1dc05aa51 100644 --- a/helm/software/components/grafite_parser/nEstatus.ml +++ b/helm/software/components/grafite_parser/nEstatus.ml @@ -11,8 +11,8 @@ (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) -type extra_status = { - lstatus : LexiconEngine.status; - rstatus : NRstatus.dumpable_status; -} - +class status = + object + inherit LexiconEngine.status + inherit NRstatus.dumpable_status + end diff --git a/helm/software/components/grafite_parser/nEstatus.mli b/helm/software/components/grafite_parser/nEstatus.mli index 2ae7d01e4..2c3acc751 100644 --- a/helm/software/components/grafite_parser/nEstatus.mli +++ b/helm/software/components/grafite_parser/nEstatus.mli @@ -11,8 +11,8 @@ (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) -type extra_status = { - lstatus : LexiconEngine.status; - rstatus : NRstatus.dumpable_status; -} - +class status : + object + inherit LexiconEngine.status + inherit NRstatus.dumpable_status + end diff --git a/helm/software/components/grafite_parser/test_parser.ml b/helm/software/components/grafite_parser/test_parser.ml index c87d41ed5..9f42238e9 100644 --- a/helm/software/components/grafite_parser/test_parser.ml +++ b/helm/software/components/grafite_parser/test_parser.ml @@ -67,7 +67,7 @@ let process_stream istream = let module G = GrafiteAst in let status = ref - (CicNotation2.load_notation + (CicNotation2.load_notation (new LexiconEngine.status) ~include_paths:[] (Helm_registry.get "notation.core_file")) in try diff --git a/helm/software/components/lexicon/lexiconEngine.ml b/helm/software/components/lexicon/lexiconEngine.ml index 805da25c8..699af578b 100644 --- a/helm/software/components/lexicon/lexiconEngine.ml +++ b/helm/software/components/lexicon/lexiconEngine.ml @@ -33,19 +33,13 @@ let debug = ref false exception IncludedFileNotCompiled of string * string exception MetadataNotFound of string (* file name *) -type status = { +type lexicon_status = { aliases: L.alias_spec DisambiguateTypes.Environment.t; multi_aliases: L.alias_spec list DisambiguateTypes.Environment.t; lexicon_content_rev: LexiconMarshal.lexicon; notation_ids: CicNotation.notation_id list; (** in-scope notation ids *) } -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.aliases - let initial_status = { aliases = DisambiguateTypes.Environment.empty; multi_aliases = DisambiguateTypes.Environment.empty; @@ -53,8 +47,21 @@ let initial_status = { notation_ids = []; } +class status = + object + val lstatus = initial_status + method lstatus = lstatus + method set_lstatus v = {< lstatus = v >} + 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 + let add_lexicon_content cmds status = - let content = status.lexicon_content_rev in + let content = status#lstatus.lexicon_content_rev in let content' = List.fold_right (fun cmd acc -> @@ -70,7 +77,8 @@ let add_lexicon_content cmds status = String.concat "; " (List.map LexiconAstPp.pp_command content') ); *) - { status with lexicon_content_rev = content' } + status#set_lstatus + { status#lstatus with lexicon_content_rev = content' } let set_proof_aliases mode status new_aliases = if mode = L.WithoutPreferences then @@ -82,30 +90,28 @@ let set_proof_aliases mode status new_aliases = in let aliases = List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc) - status.aliases new_aliases in + status#lstatus.aliases new_aliases in let multi_aliases = List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.cons L.description_of_alias d c acc) - status.multi_aliases new_aliases + status#lstatus.multi_aliases new_aliases in let new_status = - { status with multi_aliases = multi_aliases ; aliases = aliases} - in - if new_aliases = [] then - new_status - else - let status = - add_lexicon_content (commands_of_aliases new_aliases) new_status - in - 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) status cmd = +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) -> @@ -132,7 +138,7 @@ let rec eval_command ?(mode=L.WithPreferences) status cmd = with Not_found -> prerr_endline ("LexiconEngine.eval_command: domain item not found: " ^ (DisambiguateTypes.string_of_domain_item item)); - dump_aliases prerr_endline "" status; + dump_aliases prerr_endline "" sstatus; assert false end | p -> p @@ -144,6 +150,7 @@ let rec eval_command ?(mode=L.WithPreferences) status cmd = let notation_ids' = CicNotation.process_notation cmd in let status = { status with notation_ids = notation_ids' @ status.notation_ids } in + let sstatus = sstatus#set_lstatus status in match cmd with | L.Include (loc, baseuri, mode, fullpath) -> let lexiconpath_rw, lexiconpath_r = @@ -158,8 +165,7 @@ let rec eval_command ?(mode=L.WithPreferences) status cmd = raise (IncludedFileNotCompiled (lexiconpath_rw,fullpath)) in let lexicon = LexiconMarshal.load_lexicon lexiconpath in - let status = List.fold_left (eval_command ~mode) status lexicon in - status + List.fold_left (eval_command ~mode) sstatus lexicon | L.Alias (loc, spec) -> let diff = (*CSC: Warning: this code should be factorized with the corresponding @@ -172,9 +178,9 @@ let rec eval_command ?(mode=L.WithPreferences) status cmd = | L.Number_alias (instance,desc) -> [DisambiguateTypes.Num instance,spec] in - set_proof_aliases mode status diff + set_proof_aliases mode sstatus diff | L.Interpretation (_, dsc, (symbol, _), _) as stm -> - let status = add_lexicon_content [stm] status in + let sstatus = add_lexicon_content [stm] sstatus in let diff = try [DisambiguateTypes.Symbol (symbol, 0), @@ -184,10 +190,10 @@ let rec eval_command ?(mode=L.WithPreferences) status cmd = prerr_endline (Lazy.force msg); assert false in - let status = set_proof_aliases mode status diff in - status + let sstatus = set_proof_aliases mode sstatus diff in + sstatus | L.Notation _ as stm -> - add_lexicon_content [stm] status + add_lexicon_content [stm] sstatus let eval_command status cmd = if !debug then dump_aliases prerr_endline "before eval_command" status; diff --git a/helm/software/components/lexicon/lexiconEngine.mli b/helm/software/components/lexicon/lexiconEngine.mli index 11d92d462..07eb8d298 100644 --- a/helm/software/components/lexicon/lexiconEngine.mli +++ b/helm/software/components/lexicon/lexiconEngine.mli @@ -25,20 +25,24 @@ exception IncludedFileNotCompiled of string * string -type status = { +type lexicon_status = { aliases: LexiconAst.alias_spec DisambiguateTypes.Environment.t; multi_aliases: LexiconAst.alias_spec list DisambiguateTypes.Environment.t; lexicon_content_rev: LexiconMarshal.lexicon; notation_ids: CicNotation.notation_id list; (** in-scope notation ids *) } -val initial_status: status +class status : + object ('self) + method lstatus: lexicon_status + method set_lstatus: lexicon_status -> 'self + end -val eval_command : status -> LexiconAst.command -> status +val eval_command : #status as 'status -> LexiconAst.command -> 'status val set_proof_aliases: - status -> (DisambiguateTypes.domain_item * LexiconAst.alias_spec) list -> - status + #status as 'status -> + (DisambiguateTypes.domain_item * LexiconAst.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 -> #status -> unit diff --git a/helm/software/components/lexicon/lexiconSync.ml b/helm/software/components/lexicon/lexiconSync.ml index 616c3ef5a..c82caf337 100644 --- a/helm/software/components/lexicon/lexiconSync.ml +++ b/helm/software/components/lexicon/lexiconSync.ml @@ -33,7 +33,7 @@ let alias_diff ~from status = try let description2 = LexiconAst.description_of_alias - (Map.find domain_item from.LexiconEngine.aliases) + (Map.find domain_item from#lstatus.LexiconEngine.aliases) in if description1 <> description2 then (domain_item,codomain_item)::acc @@ -42,13 +42,9 @@ let alias_diff ~from status = with Not_found -> (domain_item,codomain_item)::acc) - status.LexiconEngine.aliases [] + status#lstatus.LexiconEngine.aliases [] ;; -let alias_diff = - let profiler = HExtlib.profile "alias_diff(conteg. anche in include)" in - fun ~from status -> profiler.HExtlib.profile (alias_diff ~from) status - (** given a uri and a type list (the contructors types) builds a list of pairs * (name,uri) that is used to generate automatic aliases **) let extract_alias types uri = @@ -125,8 +121,8 @@ let id_list_diff l2 l1 = let time_travel ~present ~past = let notation_to_remove = - id_list_diff present.LexiconEngine.notation_ids - past.LexiconEngine.notation_ids + id_list_diff present#lstatus.LexiconEngine.notation_ids + past#lstatus.LexiconEngine.notation_ids in List.iter CicNotation.remove_notation notation_to_remove diff --git a/helm/software/components/lexicon/lexiconSync.mli b/helm/software/components/lexicon/lexiconSync.mli index c2ff15c42..c645bfdbe 100644 --- a/helm/software/components/lexicon/lexiconSync.mli +++ b/helm/software/components/lexicon/lexiconSync.mli @@ -24,18 +24,18 @@ *) val add_aliases_for_objs: - LexiconEngine.status -> [`Old of UriManager.uri list | `New of NUri.uri list]-> - LexiconEngine.status + #LexiconEngine.status as 'status -> + [`Old of UriManager.uri list | `New of NUri.uri list]-> 'status val time_travel: - present:LexiconEngine.status -> past:LexiconEngine.status -> unit + present:#LexiconEngine.status -> past:#LexiconEngine.status -> unit (** 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 -> + from:#LexiconEngine.status -> #LexiconEngine.status -> (DisambiguateTypes.domain_item * LexiconAst.alias_spec) list val push: unit -> unit diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml index 6aaf4a4a8..cffda3b17 100644 --- a/helm/software/components/ng_tactics/nTacStatus.ml +++ b/helm/software/components/ng_tactics/nTacStatus.ml @@ -16,7 +16,7 @@ let fail msg = raise (Error msg) type lowtac_status = { pstatus : NCic.obj; - estatus : NEstatus.extra_status; + estatus : NEstatus.status; } type lowtactic = lowtac_status -> int -> lowtac_status @@ -83,8 +83,7 @@ let relocate status destination (name,source,t as orig) = let (metasenv, subst), t = NCicMetaSubst.delift ~unify:(fun m s c t1 t2 -> - try Some (NCicUnification.unify - status.estatus.NEstatus.rstatus m s c t1 t2) + try Some (NCicUnification.unify status.estatus m s c t1 t2) with | NCicUnification.UnificationFailure _ | NCicUnification.Uncertain _ -> None) @@ -147,7 +146,7 @@ let unify status ctx a b = let status, (_,_,b) = relocate status ctx b in let n,h,metasenv,subst,o = status.pstatus in let metasenv, subst = - NCicUnification.unify status.estatus.NEstatus.rstatus metasenv subst ctx a b + NCicUnification.unify status.estatus metasenv subst ctx a b in { status with pstatus = n,h,metasenv,subst,o } ;; @@ -160,7 +159,7 @@ let refine status ctx term expty = let status, (n,_, e) = relocate status ctx e in status, n, Some e in let name,height,metasenv,subst,obj = status.pstatus in - let rdb = status.estatus.NEstatus.rstatus in + let rdb = status.estatus in let metasenv, subst, t, ty = NCicRefiner.typeof rdb metasenv subst ctx term expty in diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli index cf94862eb..307154127 100644 --- a/helm/software/components/ng_tactics/nTacStatus.mli +++ b/helm/software/components/ng_tactics/nTacStatus.mli @@ -16,7 +16,7 @@ val fail: string lazy_t -> 'a type lowtac_status = { pstatus : NCic.obj; - estatus : NEstatus.extra_status; + estatus : NEstatus.status; } type lowtactic = lowtac_status -> int -> lowtac_status diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index e751cca58..aebcf4614 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -568,7 +568,7 @@ let auto ~params:(l,_) status goal = (status, (t,ty) :: l)) (status,[]) l in - let rdb = status.estatus.NEstatus.rstatus in + let rdb = status.estatus in Paramod.nparamod rdb metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l; status ;; diff --git a/helm/software/components/tptp_grafite/tptp2grafite.ml b/helm/software/components/tptp_grafite/tptp2grafite.ml index 7950ca15d..ca0534c52 100644 --- a/helm/software/components/tptp_grafite/tptp2grafite.ml +++ b/helm/software/components/tptp_grafite/tptp2grafite.ml @@ -272,7 +272,7 @@ let ng_generate_tactics fv ueq_case context arities = GA.NSkip floc; GA.NMerge floc]))]) fv)) else [])@ - [GA.Executable(floc,GA.Command(floc, GA.NQed(floc)))] + [GA.Executable(floc,GA.NCommand(floc, GA.NQed(floc)))] ;; let generate_tactics fv ueq_case = diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml index 658a3ad38..cc46c7649 100644 --- a/helm/software/matita/matita.ml +++ b/helm/software/matita/matita.ml @@ -140,7 +140,7 @@ let _ = ignore (GMenu.separator_item ~packing:gui#main#debugMenu_menu#append ()) in addDebugItem "dump aliases" (fun _ -> - let status = GrafiteTypes.get_lexicon script#grafite_status in + let status = GrafiteTypes.get_estatus script#grafite_status in LexiconEngine.dump_aliases HLog.debug "" status); (* FG: DEBUGGING addDebugItem "dump interpretations" (fun _ -> diff --git a/helm/software/matita/matitaEngine.ml b/helm/software/matita/matitaEngine.ml index e3040f8b3..6e6213734 100644 --- a/helm/software/matita/matitaEngine.ml +++ b/helm/software/matita/matitaEngine.ml @@ -40,14 +40,13 @@ let disambiguate_tactic text prefix_len lexicon_status_ref grafite_status goal t in GrafiteTypes.set_metasenv metasenv grafite_status,tac -let disambiguate_command estatus lexicon_status_ref grafite_status cmd = +let disambiguate_command lexicon_status_ref grafite_status cmd = let baseuri = GrafiteTypes.get_baseuri grafite_status in - let estatus,metasenv,cmd = + let lexicon_status,metasenv,cmd = GrafiteDisambiguate.disambiguate_command ~baseuri - { estatus with NEstatus.lstatus = !lexicon_status_ref } - (GrafiteTypes.get_proof_metasenv grafite_status) cmd + !lexicon_status_ref (GrafiteTypes.get_proof_metasenv grafite_status) cmd in - lexicon_status_ref := estatus.NEstatus.lstatus; + lexicon_status_ref := lexicon_status; GrafiteTypes.set_metasenv metasenv grafite_status,cmd let disambiguate_macro lexicon_status_ref grafite_status macro context = @@ -60,12 +59,10 @@ let disambiguate_macro lexicon_status_ref grafite_status macro context = GrafiteTypes.set_metasenv metasenv grafite_status,macro let eval_ast ?do_heavy_checks grafite_status (text,prefix_len,ast) = - let lexicon_status = GrafiteTypes.get_lexicon grafite_status in + let lexicon_status = GrafiteTypes.get_estatus grafite_status in let dump = not (Helm_registry.get_bool "matita.moo") in let lexicon_status_ref = ref lexicon_status in let baseuri = GrafiteTypes.get_baseuri grafite_status in - let changed_lexicon = ref false in - let wrap f x = changed_lexicon := true; f x in let new_grafite_status,new_objs = match ast with | G.Executable (_, G.Command (_, G.Coercion _)) when dump -> @@ -74,19 +71,17 @@ let eval_ast ?do_heavy_checks grafite_status (text,prefix_len,ast) = grafite_status, `Old [] | ast -> GrafiteEngine.eval_ast - ~disambiguate_tactic:(wrap (disambiguate_tactic text prefix_len lexicon_status_ref)) - ~disambiguate_command:(wrap - (disambiguate_command - (GrafiteTypes.get_estatus grafite_status) lexicon_status_ref)) - ~disambiguate_macro:(wrap (disambiguate_macro lexicon_status_ref)) + ~disambiguate_tactic:(disambiguate_tactic text prefix_len lexicon_status_ref) + ~disambiguate_command:(disambiguate_command lexicon_status_ref) + ~disambiguate_macro:(disambiguate_macro lexicon_status_ref) ?do_heavy_checks grafite_status (text,prefix_len,ast) in + let new_lexicon_status = GrafiteTypes.get_estatus new_grafite_status in let new_lexicon_status = - if !changed_lexicon then - !lexicon_status_ref - else - GrafiteTypes.get_lexicon new_grafite_status - in + if !lexicon_status_ref#lstatus != lexicon_status#lstatus then + new_lexicon_status#set_lstatus (!lexicon_status_ref#lstatus) + else + new_lexicon_status in let new_lexicon_status = LexiconSync.add_aliases_for_objs new_lexicon_status new_objs in let new_aliases = @@ -114,18 +109,17 @@ let eval_ast ?do_heavy_checks grafite_status (text,prefix_len,ast) = if b then lexicon_status,acc else - let new_lexicon_status = LexiconEngine.set_proof_aliases lexicon_status [k,value] in let grafite_status = - GrafiteTypes.set_lexicon new_lexicon_status grafite_status + GrafiteTypes.set_estatus new_lexicon_status grafite_status in new_lexicon_status, (grafite_status ,Some (k,value))::acc ) (lexicon_status,[]) new_aliases in let new_grafite_status = - GrafiteTypes.set_lexicon new_lexicon_status new_grafite_status + GrafiteTypes.set_estatus new_lexicon_status new_grafite_status in ((new_grafite_status),None)::intermediate_states ;; @@ -147,7 +141,7 @@ let eval_from_stream ~first_statement_only ~include_paths try let cont = try - let lexicon_status = GrafiteTypes.get_lexicon grafite_status in + let lexicon_status = GrafiteTypes.get_estatus grafite_status in Some (GrafiteParser.parse_statement ~include_paths str lexicon_status) with End_of_file -> None @@ -156,7 +150,7 @@ let eval_from_stream ~first_statement_only ~include_paths | None -> true, grafite_status, statuses | Some (lexicon_status,ast) -> let grafite_status = - GrafiteTypes.set_lexicon lexicon_status grafite_status + GrafiteTypes.set_estatus lexicon_status grafite_status in (match ast with GrafiteParser.LNone _ -> diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index e71eb4104..c5906e16a 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -88,9 +88,9 @@ let save_moo grafite_status = GrafiteMarshal.save_moo moo_fname grafite_status.GrafiteTypes.moo_content_rev; LexiconMarshal.save_lexicon lexicon_fname - (GrafiteTypes.get_lexicon grafite_status).LexiconEngine.lexicon_content_rev; + (GrafiteTypes.get_estatus grafite_status)#lstatus.LexiconEngine.lexicon_content_rev; NRstatus.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) - (GrafiteTypes.get_dstatus grafite_status)#dump + (GrafiteTypes.get_estatus grafite_status)#dump | _ -> clean_current_baseuri grafite_status ;; diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index 05dad0572..8de5ccebc 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -105,7 +105,7 @@ 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 : GrafiteParser.statement) x = +let wrap_with_make include_paths (f : #LexiconEngine.status GrafiteParser.statement) x = try f ~never_include:true ~include_paths x with @@ -612,12 +612,12 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff let ast = wrap_with_make include_paths (GrafiteParser.parse_statement (Ulexing.from_utf8_string text)) - (GrafiteTypes.get_lexicon grafite_status) + (GrafiteTypes.get_estatus grafite_status) in ast, text - | `Ast (st, text) -> (GrafiteTypes.get_lexicon grafite_status, st), text + | `Ast (st, text) -> (GrafiteTypes.get_estatus grafite_status, st), text in - let grafite_status = GrafiteTypes.set_lexicon lexicon_status grafite_status in + let grafite_status = GrafiteTypes.set_estatus lexicon_status grafite_status in let text_of_loc floc = let nonskipped_txt,_ = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in let start, stop = HExtlib.loc_of_floc floc in @@ -675,7 +675,7 @@ let buffer = source_view#buffer in let source_buffer = source_view#source_buffer in let initial_statuses baseuri = let lexicon_status = - CicNotation2.load_notation ~include_paths:[] + CicNotation2.load_notation ~include_paths:[] (new LexiconEngine.status) BuildTimeConf.core_notation_script in let grafite_status = GrafiteSync.init lexicon_status baseuri in @@ -816,8 +816,8 @@ object (self) match history with s::_ -> s | [] -> assert false in LexiconSync.time_travel - ~present:(GrafiteTypes.get_lexicon cur_grafite_status) - ~past:(GrafiteTypes.get_lexicon grafite_status); + ~present:(GrafiteTypes.get_estatus cur_grafite_status) + ~past:(GrafiteTypes.get_estatus grafite_status); GrafiteSync.time_travel ~present:cur_grafite_status ~past:grafite_status; statements <- new_statements; history <- new_history; @@ -985,8 +985,8 @@ object (self) * library_objects.set_default... *) GrafiteSync.time_travel ~present:self#grafite_status ~past:grafite_status; LexiconSync.time_travel - ~present:(GrafiteTypes.get_lexicon self#grafite_status) - ~past:(GrafiteTypes.get_lexicon grafite_status) + ~present:(GrafiteTypes.get_estatus self#grafite_status) + ~past:(GrafiteTypes.get_estatus grafite_status) method private reset_buffer = statements <- []; @@ -1142,7 +1142,7 @@ object (self) in try is_there_only_comments - (GrafiteTypes.get_lexicon self#grafite_status) self#getFuture + (GrafiteTypes.get_estatus self#grafite_status) self#getFuture with | LexiconEngine.IncludedFileNotCompiled _ | HExtlib.Localized _ diff --git a/helm/software/matita/matitaWiki.ml b/helm/software/matita/matitaWiki.ml index 7575eca10..268da7e51 100644 --- a/helm/software/matita/matitaWiki.ml +++ b/helm/software/matita/matitaWiki.ml @@ -141,8 +141,8 @@ let rec interactive_loop () = grafite_status := drop (to_be_dropped, !grafite_status) ; let grafite_status = safe_hd !grafite_status in LexiconSync.time_travel - ~present:(GrafiteTypes.get_lexicon cur_grafite_status) - ~past:(GrafiteTypes.get_lexicon grafite_status); + ~present:(GrafiteTypes.get_estatus cur_grafite_status) + ~past:(GrafiteTypes.get_estatus grafite_status); GrafiteSync.time_travel ~present:cur_grafite_status ~past:grafite_status; interactive_loop (Some n) @@ -204,7 +204,7 @@ let main () = let include_paths = Helm_registry.get_list Helm_registry.string "matita.includes" in grafite_status := [GrafiteSync.init (CicNotation2.load_notation ~include_paths - BuildTimeConf.core_notation_script) "cic:/matita/tests/"]; + (new LexiconEngine.status) BuildTimeConf.core_notation_script) "cic:/matita/tests/"]; Sys.catch_break true; let origcb = HLog.get_log_callback () in let origcb t s = origcb t ((if system_mode then "[S] " else "") ^ s) in @@ -226,8 +226,8 @@ let main () = match !grafite_status with | s::_ -> s.proof_status, s.moo_content_rev, - (GrafiteTypes.get_lexicon s).LexiconEngine.lexicon_content_rev, - (GrafiteTypes.get_dstatus s)#dump + (GrafiteTypes.get_estatus s)#lstatus.LexiconEngine.lexicon_content_rev, + (GrafiteTypes.get_estatus s)#dump | _ -> assert false in if proof_status <> GrafiteTypes.No_proof then diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml index e26a3f89d..b3b95325a 100644 --- a/helm/software/matita/matitacLib.ml +++ b/helm/software/matita/matitacLib.ml @@ -29,7 +29,7 @@ open Printf open GrafiteTypes -exception AttemptToInsertAnAlias of LexiconEngine.status +exception AttemptToInsertAnAlias of #LexiconEngine.status let slash_n_RE = Pcre.regexp "\\n" ;; @@ -175,7 +175,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:[] + CicNotation2.load_notation ~include_paths:[] (new LexiconEngine.status) BuildTimeConf.core_notation_script in atstart (); (* FG: do not invoke before loading the core notation script *) @@ -236,7 +236,7 @@ let compile atstart options fname = | [] -> grafite_status | (g,None)::_ -> g | (g,Some _)::_ -> - raise (AttemptToInsertAnAlias (GrafiteTypes.get_lexicon g)) + raise (AttemptToInsertAnAlias (GrafiteTypes.get_estatus g)) with MatitaEngine.EnrichedWithStatus (GrafiteEngine.Macro (floc, f), grafite) as exn -> match f (get_macro_context (Some grafite)) with @@ -258,7 +258,7 @@ let compile atstart options fname = let elapsed = Unix.time () -. time in let proof_status,moo_content_rev,lexicon_content_rev = grafite_status.proof_status, grafite_status.moo_content_rev, - (GrafiteTypes.get_lexicon grafite_status).LexiconEngine.lexicon_content_rev + (GrafiteTypes.get_estatus grafite_status)#lstatus.LexiconEngine.lexicon_content_rev in if proof_status <> GrafiteTypes.No_proof then (HLog.error @@ -275,7 +275,7 @@ let compile atstart options fname = GrafiteMarshal.save_moo moo_fname moo_content_rev; LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev; NRstatus.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) - (GrafiteTypes.get_dstatus grafite_status)#dump + (GrafiteTypes.get_estatus grafite_status)#dump end; let tm = Unix.gmtime elapsed in let sec = string_of_int tm.Unix.tm_sec ^ "''" in -- 2.39.2