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
| 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
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
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
"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 ^ "\""
| 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 =
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
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 []
;;
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
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 []
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
{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
(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)))
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 =
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 = {
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)
}
type ng_status =
| ProofMode of NTacStatus.tac_status
- | CommandMode of NEstatus.extra_status
+ | CommandMode of NEstatus.status
type status = {
moo_content_rev: GrafiteMarshal.moo;
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
| 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
type ng_status =
| ProofMode of NTacStatus.tac_status
- | CommandMode of NEstatus.extra_status
+ | CommandMode of NEstatus.status
type status = {
moo_content_rev: GrafiteMarshal.moo;
(** 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
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
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
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
cicNotation2.cmi:
nEstatus.cmi:
grafiteDisambiguate.cmi: nEstatus.cmi
-grafiteWalker.cmi: grafiteParser.cmi
print_grammar.cmi:
dependenciesParser.cmo: dependenciesParser.cmi
dependenciesParser.cmx: dependenciesParser.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
cicNotation2.mli \
nEstatus.mli \
grafiteDisambiguate.mli \
- grafiteWalker.mli \
print_grammar.mli \
$(NULL)
IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
(* $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
* 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
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
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
;;
~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
(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],_ ->
(* let time = Unix.gettimeofday () in *)
- let lexicon_status = estatus.NEstatus.lstatus in
let (diff, metasenv, _, cic, _) =
singleton "third"
(CicDisambiguate.disambiguate_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
(* 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
~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 =
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) ->
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 =
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
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 ->
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 *
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
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
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
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<def>> ; 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<def>> (* ≝ *); body = term -> body ] ->
G.NObj (loc, N.Theorem (nflavour, name, typ, body))
| nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
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<def>> (* ≝ *); body = term -> body ] ->
- G.Obj (loc, N.Theorem (flavour, name, typ, body))
- | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
- 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) *)
| _ -> 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<def>> ; 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<def>> (* ≝ *); body = term -> body ] ->
+ G.Obj (loc, N.Theorem (flavour, name, typ, body))
+ | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
+ 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;
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)
]];
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)
[ 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
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 [] ;;
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
+++ /dev/null
-(* 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)
-
+++ /dev/null
-(* 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 <fname, raw statement>, 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
-
(* $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
(* $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
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
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;
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 ->
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
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) ->
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
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 =
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
| 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),
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;
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
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
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 =
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
*)
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
type lowtac_status = {
pstatus : NCic.obj;
- estatus : NEstatus.extra_status;
+ estatus : NEstatus.status;
}
type lowtactic = lowtac_status -> int -> lowtac_status
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)
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 }
;;
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
type lowtac_status = {
pstatus : NCic.obj;
- estatus : NEstatus.extra_status;
+ estatus : NEstatus.status;
}
type lowtactic = lowtac_status -> int -> lowtac_status
(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
;;
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 =
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 _ ->
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 =
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 ->
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 =
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
;;
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
| 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 _ ->
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
;;
* 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
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
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
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;
* 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 <- [];
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 _
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)
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
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
open GrafiteTypes
-exception AttemptToInsertAnAlias of LexiconEngine.status
+exception AttemptToInsertAnAlias of #LexiconEngine.status
let slash_n_RE = Pcre.regexp "\\n" ;;
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 *)
| [] -> 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
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
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
projects / helm.git / commitdiff