let status,id = fresh_id status in
let ids =
try
- StringMap.find symbol status#interp_db.interpretations
+ id::StringMap.find symbol status#interp_db.interpretations
with Not_found -> [id] in
let status =
status#set_interp_db { status#interp_db with
(* composed magic: term + command magics. No need to change this value *)
let magic = magic + 10000 * NotationPt.magic
-type command =
- | Set of loc * string * string
- | Print of loc * string
-
type alias_spec =
| Ident_alias of string * string (* identifier, uri *)
| Symbol_alias of string * int * string (* name, instance no, description *)
type inclusion_mode = WithPreferences | WithoutPreferences (* aka aliases *)
-type ncommand =
+type command =
| Include of loc * inclusion_mode * string (* _,buri,_,path *)
| UnificationHint of loc * NotationPt.term * int (* term, precedence *)
| NObj of loc * NotationPt.term NotationPt.obj
(* description (i.e. id), symbol, arg pattern, appl pattern *)
type code =
- | Command of loc * command
- | NCommand of loc * ncommand
+ | NCommand of loc * command
| NMacro of loc * nmacro
| NTactic of loc * ntactic list
pp_notation dir_opt l1_pattern assoc prec l2_pattern
;;
-let pp_command = function
- | Print (_,s) -> "print " ^ s
- | Set (_, name, value) -> Printf.sprintf "set \"%s\" \"%s\"" name value
-
let pp_executable ~map_unicode_to_tex =
function
| NMacro (_, macro) -> pp_nmacro macro ^ "."
| NTactic (_,tacl) ->
String.concat " " (List.map (pp_ntactic ~map_unicode_to_tex) tacl)
- | Command (_, cmd) -> pp_command cmd ^ "."
| NCommand (_, cmd) -> pp_ncommand cmd ^ "."
let pp_comment ~map_unicode_to_tex =
* http://helm.cs.unibo.it/
*)
-val pp_command: GrafiteAst.command -> string
val pp_comment: map_unicode_to_tex:bool -> GrafiteAst.comment -> string
val pp_executable: map_unicode_to_tex:bool -> GrafiteAst.code -> string
let status = basic_eval_unification_hint (t,n) status in
let dump = inject_unification_hint (t,n)::status#dump in
let status = status#set_dump dump in
- status,[]
+ status
;;
let basic_index_obj l status =
let status = basic_eval_add_constraint (u1,u2) status in
let dump = inject_constraint (u1,u2)::status#dump in
let status = status#set_dump dump in
- status,[]
+ status
;;
let eval_ng_tac tac =
GrafiteTypes.Serializer.require ~baseuri:(NUri.uri_of_string baseuri)
status in
let status = status#set_dump (obj::status#dump) in
- assert false (* mode must be passed to GrafiteTypes.Serializer.require
+ assert false; (* mode must be passed to GrafiteTypes.Serializer.require
somehow *)
- status,[]
+ status
| GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n
| GrafiteAst.NCoercion (loc, name, t, ty, source, target) ->
+ let status, composites =
NCicCoercDeclaration.eval_ncoercion status name t ty source target
+ in
+ LexiconSync.add_aliases_for_objs status composites
| GrafiteAst.NQed loc ->
if status#ng_mode <> `ProofMode then
raise (GrafiteTypes.Command_error "Not in proof mode")
*)
let status = status#set_ng_mode `CommandMode in
let status = LexiconSync.add_aliases_for_objs status [uri] in
- let status,uris =
+ let status =
List.fold_left
- (fun (status,uris) boxml ->
+ (fun status boxml ->
try
- let nstatus,nuris =
+ let nstatus =
eval_ncommand ~include_paths opts status
("",0,GrafiteAst.NObj (HExtlib.dummy_floc,boxml))
in
begin
(*HLog.warn "error in generating projection/eliminator";*)
assert(status#ng_mode = `CommandMode);
- status, uris
+ status
end
else
- nstatus, uris@nuris
+ nstatus
with
| MultiPassDisambiguator.DisambiguationError _
| NCicTypeChecker.TypeCheckerFailure _ ->
(*HLog.warn "error in generating projection/eliminator";*)
- status,uris
- ) (status,[] (* uris *)) boxml in
+ status
+ ) status boxml in
let _,_,_,_,nobj = obj in
let status = match nobj with
NCic.Inductive (is_ind,leftno,[it],_) ->
(snd (NCicElim.ast_of_sort outsort)))
is_ind it leftno outsort status status#baseuri in
let _,_,menv,_,_ = invobj in
- fst (match menv with
+ (match menv with
[] -> eval_ncommand ~include_paths opts status
("",0,GrafiteAst.NQed Stdpp.dummy_loc)
- | _ -> status,[]))
+ | _ -> status))
(* XXX *)
with _ -> (*HLog.warn "error in generating inversion principle"; *)
let status = status#set_ng_mode `CommandMode in status)
(fun (name,is_coercion,arity) ->
if is_coercion then Some(name,leftno,arity) else None) fields
| _ -> [] in
- let status,uris =
+ let status =
List.fold_left
- (fun (status,uris) (name,cpos,arity) ->
+ (fun status (name,cpos,arity) ->
try
let metasenv,subst,status,t =
GrafiteDisambiguate.disambiguate_nterm None status [] [] []
basic_eval_and_record_ncoercion_from_t_cpos_arity
status (name,t,cpos,arity)
in
- let uris = nuris@uris in
- status, uris
+ LexiconSync.add_aliases_for_objs status nuris
with MultiPassDisambiguator.DisambiguationError _->
HLog.warn ("error in generating coercion: "^name);
- status, uris)
- (status,uris) coercions
+ status)
+ status coercions
in
- status,uris
+ status
with
exn ->
NCicLibrary.time_travel old_status;
(match nmenv with
[] ->
eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
- | _ -> status,[])
+ | _ -> status)
| GrafiteAst.NDiscriminator (_,_) -> assert false (*(loc, indty) ->
if status#ng_mode <> `CommandMode then
raise (GrafiteTypes.Command_error "Not in command mode")
let diff =
[DisambiguateTypes.Symbol (symbol, 0),
GrafiteAst.Symbol_alias (symbol,0,dsc)] in
- let status = LexiconEngine.set_proof_aliases status mode diff in
- status, []
+ let status =
+ LexiconEngine.set_proof_aliases status ~implicit_aliases:false mode diff
+ in
+ status
(*assert false*) (* MANCA SALVATAGGIO SU DISCO CHE DEVE TENERE IN CONTO
IL MODE WithPreference/WithOutPreferences*)
| GrafiteAst.Notation (loc, dir, l1, associativity, precedence, l2) ->
status
in
(* assert false (* MANCA SALVATAGGIO SU DISCO *) *)
- status, [] (* capire [] XX *)
+ status (* capire [] XX *)
| GrafiteAst.Alias (loc, spec) ->
let diff =
(*CSC: Warning: this code should be factorized with the corresponding
[DisambiguateTypes.Num instance,spec]
in
let mode = assert false in (* VEDI SOPRA *)
- LexiconEngine.set_proof_aliases status mode diff;
+ LexiconEngine.set_proof_aliases status ~implicit_aliases:false mode diff;
assert false (* MANCA SALVATAGGIO SU DISCO *)
;;
-let eval_comment opts status (text,prefix_len,c) = status, []
-
-let rec eval_command opts status (text,prefix_len,cmd) =
- let status,uris =
- match cmd with
- | GrafiteAst.Print (_,_) -> status,[]
- | GrafiteAst.Set (loc, name, value) -> status, []
- in
- status,uris
+let eval_comment opts status (text,prefix_len,c) = status
-and eval_executable ~include_paths opts status (text,prefix_len,ex) =
+let rec eval_executable ~include_paths opts status (text,prefix_len,ex) =
match ex with
| GrafiteAst.NTactic (_(*loc*), tacl) ->
if status#ng_mode <> `ProofMode then
subst_metasenv_and_fix_names status)
status tacl
in
- status,[]
- | GrafiteAst.Command (_, cmd) ->
- eval_command opts status (text,prefix_len,cmd)
+ status
| GrafiteAst.NCommand (_, cmd) ->
eval_ncommand ~include_paths opts status (text,prefix_len,cmd)
| GrafiteAst.NMacro (loc, macro) ->
type 'a disambiguator_input = string * int * 'a
val eval_ast :
- include_paths:string list ->
- ?do_heavy_checks:bool ->
- GrafiteTypes.status ->
- GrafiteAst.statement disambiguator_input ->
- (* the new status and generated objects, if any *)
- GrafiteTypes.status * NUri.uri list
+ include_paths:string list -> ?do_heavy_checks:bool ->
+ GrafiteTypes.status -> GrafiteAst.statement disambiguator_input ->
+ GrafiteTypes.status
~context ~metasenv ~subst thing)
in
let estatus =
- LexiconEngine.set_proof_aliases estatus GrafiteAst.WithPreferences diff
+ LexiconEngine.set_proof_aliases estatus ~implicit_aliases:true
+ GrafiteAst.WithPreferences diff
in
metasenv, subst, estatus, cic
;;
~aliases:estatus#lstatus.LexiconTypes.aliases
~universe:(Some estatus#lstatus.LexiconTypes.multi_aliases)
(text,prefix_len,obj)) in
- let estatus = LexiconEngine.set_proof_aliases estatus
- GrafiteAst.WithPreferences diff in
+ let estatus =
+ LexiconEngine.set_proof_aliases estatus ~implicit_aliases:true
+ GrafiteAst.WithPreferences diff
+ in
estatus, cic
;;
(fun _ x -> out (GrafiteAstPp.pp_alias x))
status#lstatus.LexiconTypes.aliases
-let set_proof_aliases status mode new_aliases =
+let set_proof_aliases status ~implicit_aliases mode new_aliases =
if mode = GrafiteAst.WithoutPreferences then
status
else
status#lstatus.LexiconTypes.multi_aliases new_aliases
in
let new_status =
- {LexiconTypes.multi_aliases = multi_aliases ; aliases = aliases}
+ {LexiconTypes.multi_aliases = multi_aliases ;
+ aliases = aliases;
+ new_aliases =
+ (if implicit_aliases then new_aliases else []) @
+ status#lstatus.LexiconTypes.new_aliases}
in
status#set_lstatus new_status
val set_proof_aliases:
#LexiconTypes.status as 'status ->
+ implicit_aliases:bool -> (* implicit ones are made explicit *)
GrafiteAst.inclusion_mode ->
(DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list -> 'status
(* $Id$ *)
-let alias_diff ~from status =
- let module Map = DisambiguateTypes.Environment in
- Map.fold
- (fun domain_item codomain_item acc ->
- let description1 = GrafiteAst.description_of_alias codomain_item in
- try
- let description2 =
- GrafiteAst.description_of_alias
- (Map.find domain_item from#lstatus.LexiconTypes.aliases)
- in
- if description1 <> description2 then
- (domain_item,codomain_item)::acc
- else
- acc
- with
- Not_found ->
- (domain_item,codomain_item)::acc)
- status#lstatus.LexiconTypes.aliases []
-;;
-
let add_aliases_for_objs status =
List.fold_left
(fun status nref ->
GrafiteAst.Ident_alias (name,NReference.string_of_reference u)
) references
in
- LexiconEngine.set_proof_aliases status GrafiteAst.WithPreferences new_env
+ LexiconEngine.set_proof_aliases status ~implicit_aliases:false
+ GrafiteAst.WithPreferences new_env
) status
val add_aliases_for_objs:
#LexiconTypes.status as 'status -> NUri.uri list -> 'status
-
- (** perform a diff between the aliases contained in two statuses, assuming
- * that the second one can only have more aliases than the first one
- * @return the list of aliases that should be added to aliases of from in
- * order to be equal to aliases of the second argument *)
-val alias_diff:
- from:#LexiconTypes.status -> #LexiconTypes.status ->
- (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list
type lexicon_status = {
aliases: GrafiteAst.alias_spec DisambiguateTypes.Environment.t;
- multi_aliases: GrafiteAst.alias_spec list DisambiguateTypes.Environment.t
+ multi_aliases: GrafiteAst.alias_spec list DisambiguateTypes.Environment.t;
+ new_aliases: (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list
}
let initial_status = {
aliases = DisambiguateTypes.Environment.empty;
- multi_aliases = DisambiguateTypes.Environment.empty
+ multi_aliases = DisambiguateTypes.Environment.empty;
+ new_aliases = []
}
class type g_status =
type lexicon_status = {
aliases: GrafiteAst.alias_spec DisambiguateTypes.Environment.t;
- multi_aliases: GrafiteAst.alias_spec list DisambiguateTypes.Environment.t
+ multi_aliases: GrafiteAst.alias_spec list DisambiguateTypes.Environment.t;
+ new_aliases: (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list
}
class type g_status =
*)
let rec close_db cache_of_processed_baseuri uris next =
- prerr_endline "CLOSE_DB "; uris (* MATITA 1.0 *)
+ uris (* MATITA 1.0 *)
;;
let clean_baseuris ?(verbose=true) buris =
* http://helm.cs.unibo.it/
*)
-
-(*
- (** {2 Persistant state handling} *)
-
-type interpretation_id
-
-val add_interpretation:
- string -> (* id / description *)
- string * NotationPt.argument_pattern list -> (* symbol, level 2 pattern *)
- NotationPt.cic_appl_pattern -> (* level 3 pattern *)
- interpretation_id
-
- (** @raise Interpretation_not_found *)
-val lookup_interpretations:
- string -> (* symbol *)
- (string * NotationPt.argument_pattern list *
- NotationPt.cic_appl_pattern) list
-
-exception Interpretation_not_found
-
- (** @raise Interpretation_not_found *)
-val remove_interpretation: interpretation_id -> unit
-
- (** {3 Interpretations toggling} *)
-
-val get_all_interpretations: unit -> (interpretation_id * string) list
-val get_active_interpretations: unit -> interpretation_id list
-val set_active_interpretations: interpretation_id list -> unit
-
- (** {2 acic -> content} *)
-
-val ast_of_acic:
- output_type:[`Pattern|`Term] ->
- (Cic.id, NotationPt.sort_kind) Hashtbl.t -> (* id -> sort *)
- Cic.annterm -> (* acic *)
- NotationPt.term (* ast *)
- * (Cic.id, UriManager.uri) Hashtbl.t (* id -> uri *)
-
- (** {2 content -> acic} *)
-
- (** @param env environment from argument_pattern to cic terms
- * @param pat cic_appl_pattern *)
-val instantiate_appl_pattern:
- mk_appl:('term list -> 'term) ->
- mk_implicit:(bool -> 'term) ->
- term_of_uri : (UriManager.uri -> 'term) ->
- (string * 'term) list -> NotationPt.cic_appl_pattern ->
- 'term
-
-val push: unit -> unit
-val pop: unit -> unit
-*)
-
-(*
-val nast_of_cic :
- output_type:[`Pattern | `Term ] ->
- subst:NCic.substitution -> context:NCic.context -> NCic.term ->
- NotationPt.term
-*)
-
type id = string
val hide_coercions: bool ref
;;
let eval_ast ~include_paths ?do_heavy_checks status (text,prefix_len,ast) =
- let lexicon_status_ref = ref (status :> LexiconTypes.status) in
let baseuri = status#baseuri in
- let new_status,new_objs =
+ let status =
+ status#set_lstatus { status#lstatus with LexiconTypes.new_aliases = [] } in
+ let status =
GrafiteEngine.eval_ast ~include_paths ?do_heavy_checks status
- (text,prefix_len,ast)
- in
- let new_status =
- if !lexicon_status_ref#lstatus != status#lstatus then
- new_status#set_lstatus (!lexicon_status_ref#lstatus)
- else
- new_status in
- let new_status = LexiconSync.add_aliases_for_objs new_status new_objs in
- let new_aliases = LexiconSync.alias_diff ~from:status new_status in
+ (text,prefix_len,ast) in
+ let new_aliases = status#lstatus.LexiconTypes.new_aliases in
let _,intermediate_states =
List.fold_left
(fun (status,acc) (k,value) ->
if b then
status,acc
else
- let new_status =
- LexiconEngine.set_proof_aliases status
+ let status =
+ LexiconEngine.set_proof_aliases status ~implicit_aliases:false
GrafiteAst.WithPreferences [k,value]
in
- new_status, (new_status ,Some (k,value))::acc
+ status, (status ,Some (k,value))::acc
) (status,[]) new_aliases
in
- ((new_status),None)::intermediate_states
+ (status,None)::intermediate_states
;;
exception TryingToAdd of string
projects / helm.git / commitdiff