LexiconAst.alias_spec (they used to be DisambiguateTypes.codomain_item).
Benefit: it is now possible to use the very same set of aliases both for the
new and old terms. Moreover, this commits simplifies quite a bit of code.
Known bugs: when clicking the "OK" button in the error message disambiguation
window, an assertion is often raised. When the assertion is not raised, the
set of aliases that are printed are not syntactically/semantically correct.
PACKAGE = cic_disambiguation
NOTATIONS = number
INTERFACE_FILES = \
- disambiguateChoices.mli \
- cicDisambiguate.mli
+ cicDisambiguate.mli \
+ disambiguateChoices.mli
IMPLEMENTATION_FILES = \
$(patsubst %.mli, %.ml, $(INTERFACE_FILES)) \
$(patsubst %,%_notation.ml,$(NOTATIONS))
process_exn Stdpp.dummy_loc exn
;;
-let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
- ~localization_tbl
+let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri
+ ~is_path ast ~localization_tbl ~obj_context
=
(* create_dummy_ids shouldbe used only for interpretating patterns *)
assert (uri = None);
| CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term
| CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) ->
let cic_args = List.map (aux ~localize loc context) args in
- Disambiguate.resolve env
- (DisambiguateTypes.Symbol (symb, i)) ~args:cic_args ()
+ Disambiguate.resolve ~mk_choice ~env
+ (DisambiguateTypes.Symbol (symb, i)) (`Args cic_args)
| CicNotationPt.Appl terms ->
Cic.Appl (List.map (aux ~localize loc context) terms)
| CicNotationPt.Binder (binder_kind, (var, typ), body) ->
| `Pi
| `Forall -> Cic.Prod (cic_name, cic_type, cic_body)
| `Exists ->
- Disambiguate.resolve env (DisambiguateTypes.Symbol ("exists", 0))
- ~args:[ cic_type; Cic.Lambda (cic_name, cic_type, cic_body) ] ())
+ Disambiguate.resolve ~mk_choice ~env
+ (DisambiguateTypes.Symbol ("exists", 0))
+ (`Args [ cic_type; Cic.Lambda (cic_name, cic_type, cic_body) ]))
| CicNotationPt.Case (term, indty_ident, outtype, branches) ->
let cic_term = aux ~localize loc context term in
let cic_outtype = aux_option ~localize loc context None outtype in
match indty_ident with
| Some (indty_ident, _) ->
(match
- Disambiguate.resolve env
- (DisambiguateTypes.Id indty_ident) ()
+ Disambiguate.resolve ~mk_choice ~env
+ (DisambiguateTypes.Id indty_ident) (`Args [])
with
| Cic.MutInd (uri, tyno, _) -> (uri, tyno)
| Cic.Implicit _ ->
| (Ast.Wildcard, _) :: tl -> fst_constructor tl
| [] -> raise (DisambiguateTypes.Invalid_choice (lazy (loc,"The type of the term to be matched cannot be determined because it is an inductive type without constructors or because all patterns use wildcards")))
in
- (match Disambiguate.resolve env
- (DisambiguateTypes.Id (fst_constructor branches)) () with
+ (match Disambiguate.resolve ~mk_choice ~env
+ (DisambiguateTypes.Id (fst_constructor branches))
+ (`Args []) with
| Cic.MutConstruct (indtype_uri, indtype_no, _, _) ->
(indtype_uri, indtype_no)
| Cic.Implicit _ ->
with UriManager.IllFormedUri _ ->
CicNotationPt.fail loc "Ill formed URI"
else
- Disambiguate.resolve env (DisambiguateTypes.Id name) ()
+ try
+ List.assoc name obj_context
+ with
+ Not_found ->
+ Disambiguate.resolve ~mk_choice ~env
+ (DisambiguateTypes.Id name) (`Args [])
in
let mk_subst uris =
let ids_to_uris =
raise (DisambiguateTypes.Invalid_choice (lazy (loc,"Circular dependency in the environment")))))
| CicNotationPt.Implicit -> Cic.Implicit None
| CicNotationPt.UserInput -> Cic.Implicit (Some `Hole)
- | CicNotationPt.Num (num, i) -> Disambiguate.resolve env (DisambiguateTypes.Num i) ~num ()
+ | CicNotationPt.Num (num, i) ->
+ Disambiguate.resolve ~mk_choice ~env
+ (DisambiguateTypes.Num i) (`Num_arg num)
| CicNotationPt.Meta (index, subst) ->
let cic_subst =
List.map
| CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
| CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u)
| CicNotationPt.Symbol (symbol, instance) ->
- Disambiguate.resolve env (DisambiguateTypes.Symbol (symbol, instance)) ()
+ Disambiguate.resolve ~mk_choice ~env
+ (DisambiguateTypes.Symbol (symbol, instance)) (`Args [])
| _ -> assert false (* god bless Bologna *)
and aux_option ~localize loc context annotation = function
| None -> Cic.Implicit annotation
let localization_tbl = Cic.CicHash.create 23 in
(* here we are throwing away useful localization informations!!! *)
fst (
- interpretate_term ~create_dummy_ids:true
+ interpretate_term ~mk_choice:(fun _ -> assert false) ~create_dummy_ids:true
~context ~env:DisambiguateTypes.Environment.empty ~uri:None ~is_path:true
- path ~localization_tbl, localization_tbl)
+ path ~localization_tbl ~obj_context:[], localization_tbl)
-let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
+let interpretate_obj ~mk_choice ~context ~env ~uri ~is_path obj
+ ~localization_tbl
+=
assert (context = []);
assert (is_path = false);
- let interpretate_term = interpretate_term ~localization_tbl in
+ let interpretate_term ?(obj_context=[]) =
+ interpretate_term ~mk_choice ~localization_tbl ~obj_context in
match obj with
| CicNotationPt.Inductive (params,tyl) ->
let uri = match uri with Some uri -> uri | None -> assert false in
context,List.rev res in
let add_params =
List.fold_right (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
- let name_to_uris =
+ let obj_context =
snd (
List.fold_left
(*here the explicit_named_substituion is assumed to be of length 0 *)
- (fun (i,res) (name,_,_,_) ->
- i + 1,(name,name,Cic.MutInd (uri,i,[]))::res
- ) (0,[]) tyl) in
- let con_env = DisambiguateTypes.env_of_list name_to_uris env in
+ (fun (i,res) (name,_,_,_) -> i + 1,(name,Cic.MutInd (uri,i,[]))::res)
+ (0,[]) tyl) in
let tyl =
List.map
(fun (name,b,ty,cl) ->
List.map
(fun (name,ty) ->
let ty' =
- add_params (interpretate_term context con_env None false ty)
+ add_params
+ (interpretate_term ~obj_context ~context ~env ~uri:None
+ ~is_path:false ty)
in
name,ty'
) cl
Cic.Constant (name,bo',ty',[],attrs))
;;
-let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
- ~localization_tbl
+let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri
+ ~is_path ast ~localization_tbl
=
- let context = List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context in
-interpretate_term ~create_dummy_ids ~context ~env ~uri ~is_path ast
-~localization_tbl
-;;
-
-let mk_implicit =
- function true -> Cic.Implicit (Some `Closed)
- | _ -> Cic.Implicit None
+ let context =
+ List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context
+ in
+ interpretate_term ~mk_choice ~create_dummy_ids ~context ~env ~uri ~is_path
+ ast ~localization_tbl ~obj_context:[]
;;
let string_context_of_context =
(Cic.Anonymous,_) -> Some "_");;
let disambiguate_term ~context ~metasenv ~subst ?goal
- ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe
- ~lookup_in_library
- (text,prefix_len,term)
+ ?(initial_ugraph = CicUniv.oblivion_ugraph)
+ ~mk_implicit ~description_of_alias ~mk_choice
+ ~aliases ~universe ~lookup_in_library (text,prefix_len,term)
=
let hint = match goal with
| None -> (fun _ x -> x), fun k -> k
in
let localization_tbl = Cic.CicHash.create 503 in
MultiPassDisambiguator.disambiguate_thing ~context ~metasenv ~subst
- ~initial_ugraph ~aliases ~mk_implicit ~string_context_of_context
- ~universe ~lookup_in_library
+ ~initial_ugraph ~aliases ~string_context_of_context
+ ~universe ~lookup_in_library ~mk_implicit ~description_of_alias
~uri:None ~pp_thing:CicNotationPp.pp_term
~domain_of_thing:Disambiguate.domain_of_term
- ~interpretate_thing:(interpretate_term (?create_dummy_ids:None))
+ ~interpretate_thing:(interpretate_term (?create_dummy_ids:None) ~mk_choice)
~refine_thing:refine_term (text,prefix_len,term)
~localization_tbl
~hint
~freshen_thing:CicNotationUtil.freshen_term
~passes:(MultiPassDisambiguator.passes ())
-let disambiguate_obj ~aliases ~universe ~uri ~lookup_in_library
- (text,prefix_len,obj)
+let disambiguate_obj ~mk_implicit ~description_of_alias ~mk_choice
+ ~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj)
=
let hint = (fun _ x -> x), fun k -> k in
let localization_tbl = Cic.CicHash.create 503 in
MultiPassDisambiguator.disambiguate_thing ~context:[] ~metasenv:[] ~subst:[]
- ~aliases ~universe ~uri ~mk_implicit ~string_context_of_context
- ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term)
+ ~aliases ~universe ~uri ~string_context_of_context
+ ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term)
~domain_of_thing:Disambiguate.domain_of_obj
- ~lookup_in_library
+ ~lookup_in_library ~mk_implicit ~description_of_alias
~initial_ugraph:CicUniv.empty_ugraph
- ~interpretate_thing:interpretate_obj
+ ~interpretate_thing:(interpretate_obj ~mk_choice)
~refine_thing:refine_obj
~localization_tbl
~hint
subst:Cic.substitution ->
?goal:int ->
?initial_ugraph:CicUniv.universe_graph ->
- aliases:Cic.term DisambiguateTypes.environment ->
- universe:Cic.term DisambiguateTypes.multiple_environment option ->
+ mk_implicit:(bool -> 'alias) ->
+ description_of_alias:('alias -> string) ->
+ mk_choice:('alias -> Cic.term DisambiguateTypes.codomain_item) ->
+ aliases:'alias DisambiguateTypes.Environment.t ->
+ universe:'alias list DisambiguateTypes.Environment.t option ->
lookup_in_library:(
DisambiguateTypes.interactive_user_uri_choice_type ->
DisambiguateTypes.input_or_locate_uri_type ->
DisambiguateTypes.Environment.key ->
- Cic.term DisambiguateTypes.codomain_item list) ->
+ 'alias list) ->
CicNotationPt.term Disambiguate.disambiguator_input ->
- ((DisambiguateTypes.domain_item *
- Cic.term DisambiguateTypes.codomain_item) list *
+ ((DisambiguateTypes.domain_item * 'alias) list *
Cic.metasenv *
Cic.substitution *
Cic.term*
bool
val disambiguate_obj :
- aliases:Cic.term DisambiguateTypes.environment ->
- universe:Cic.term DisambiguateTypes.multiple_environment option ->
- uri:UriManager.uri option -> (* required only for inductive types *)
+ mk_implicit:(bool -> 'alias) ->
+ description_of_alias:('alias -> string) ->
+ mk_choice:('alias -> Cic.term DisambiguateTypes.codomain_item) ->
+ aliases:'alias DisambiguateTypes.Environment.t ->
+ universe:'alias list DisambiguateTypes.Environment.t option ->
lookup_in_library:(
DisambiguateTypes.interactive_user_uri_choice_type ->
DisambiguateTypes.input_or_locate_uri_type ->
DisambiguateTypes.Environment.key ->
- Cic.term DisambiguateTypes.codomain_item list) ->
+ 'alias list) ->
+ uri:UriManager.uri option -> (* required only for inductive types *)
CicNotationPt.term CicNotationPt.obj Disambiguate.disambiguator_input ->
- ((DisambiguateTypes.domain_item *
- Cic.term DisambiguateTypes.codomain_item) list *
+ ((DisambiguateTypes.domain_item * 'alias) list *
Cic.metasenv *
Cic.substitution *
Cic.obj *
let mk_choice ~mk_appl ~mk_implicit ~term_of_uri (dsc, args, appl_pattern)=
dsc,
- (fun env _ cic_args ->
+ `Sym_interp
+ (fun cic_args ->
let env',rest =
let names =
List.map (function CicNotationPt.IdentArg (_, name) -> name) args
let lookup_symbol_by_dsc ~mk_appl ~mk_implicit ~term_of_uri symbol dsc =
try
- mk_choice~mk_appl ~mk_implicit ~term_of_uri
+ mk_choice ~mk_appl ~mk_implicit ~term_of_uri
(List.find
(fun (dsc', _, _) -> dsc = dsc')
(TermAcicContent.lookup_interpretations symbol))
let _ =
DisambiguateChoices.add_num_choice
("natural number",
- (fun _ num _ -> LibraryObjects.build_nat (int_of_string num)));
+ `Num_interp (fun num -> LibraryObjects.build_nat (int_of_string num)));
DisambiguateChoices.add_num_choice
("Coq natural number",
- (fun _ num _ -> HelmLibraryObjects.build_nat (int_of_string num)));
+ `Num_interp (fun num -> HelmLibraryObjects.build_nat (int_of_string num)));
DisambiguateChoices.add_num_choice
("real number",
- (fun _ num _ -> HelmLibraryObjects.build_real (int_of_string num)));
+ `Num_interp (fun num -> HelmLibraryObjects.build_real (int_of_string num)));
DisambiguateChoices.add_num_choice
("binary positive number",
- (fun _ num _ ->
+ `Num_interp (fun num ->
let num = int_of_string num in
if num = 0 then
raise (DisambiguateTypes.Invalid_choice (lazy (Stdpp.dummy_loc, "0 is not a valid positive number")))
HelmLibraryObjects.build_bin_pos num));
DisambiguateChoices.add_num_choice
("binary integer number",
- (fun _ num _ ->
+ `Num_interp (fun num ->
let num = int_of_string num in
if num = 0 then
HelmLibraryObjects.BinInt.z0
(** raised when an environment is not enough informative to decide *)
exception Try_again of string Lazy.t
-type 'term aliases = bool * 'term DisambiguateTypes.environment
+type ('alias,'term) aliases= bool * 'term DisambiguateTypes.environment
type 'a disambiguator_input = string * int * 'a
type domain = domain_tree list
| Ko of (Stdpp.location * string) Lazy.t
| Uncertain of (Stdpp.location * string) Lazy.t
-let resolve (env: 'term codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () =
+let resolve ~env ~mk_choice (item: domain_item) arg =
try
- snd (Environment.find item env) env num args
+ match snd (mk_choice (Environment.find item env)), arg with
+ `Num_interp f, `Num_arg n -> f n
+ | `Sym_interp f, `Args l -> f l
+ | `Sym_interp f, `Num_arg n -> (* Implicit number! *) f []
+ | _,_ -> assert false
with Not_found ->
failwith ("Domain item not found: " ^
(DisambiguateTypes.string_of_domain_item item))
List.map
(fun (_,ty) -> domain_of_term context_w_types ty) cl))
tyl)
- | CicNotationPt.Record (params,var,ty,fields) ->
+ | Ast.Record (params,var,ty,fields) ->
let context, dom =
List.fold_left
(fun (context, dom) (var, ty) ->
metasenv:'metasenv ->
subst:'subst ->
use_coercions:bool ->
- mk_implicit:(bool -> 'refined_term) ->
string_context_of_context:('context -> string option list) ->
initial_ugraph:'ugraph ->
hint:
('metasenv -> 'raw_thing -> 'raw_thing) *
(('refined_thing,'metasenv,'subst,'ugraph) test_result ->
('refined_thing,'metasenv,'subst,'ugraph) test_result) ->
- aliases:'refined_term DisambiguateTypes.codomain_item
- DisambiguateTypes.Environment.t ->
- universe:'refined_term DisambiguateTypes.codomain_item list
- DisambiguateTypes.Environment.t option ->
+ mk_implicit:(bool -> 'alias) ->
+ description_of_alias:('alias -> string) ->
+ aliases:'alias DisambiguateTypes.Environment.t ->
+ universe:'alias list DisambiguateTypes.Environment.t option ->
lookup_in_library:(
DisambiguateTypes.interactive_user_uri_choice_type ->
DisambiguateTypes.input_or_locate_uri_type ->
DisambiguateTypes.Environment.key ->
- 'refined_term DisambiguateTypes.codomain_item list) ->
+ 'alias list) ->
uri:'uri ->
pp_thing:('ast_thing -> string) ->
domain_of_thing:(context: string option list -> 'ast_thing -> domain) ->
interpretate_thing:(
context:'context ->
- env:'refined_term DisambiguateTypes.codomain_item
- DisambiguateTypes.Environment.t ->
+ env:'alias DisambiguateTypes.Environment.t ->
uri:'uri ->
is_path:bool ->
'ast_thing ->
('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
localization_tbl:'cichash ->
string * int * 'ast_thing ->
- ((DisambiguateTypes.Environment.key *
- 'refined_term DisambiguateTypes.codomain_item) list *
+ ((DisambiguateTypes.Environment.key * 'alias) list *
'metasenv * 'subst * 'refined_thing * 'ugraph)
list * bool
end
let disambiguate_thing
~context ~metasenv ~subst ~use_coercions
- ~mk_implicit ~string_context_of_context
+ ~string_context_of_context
~initial_ugraph:base_univ ~hint
+ ~mk_implicit ~description_of_alias
~aliases ~universe ~lookup_in_library
~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
~localization_tbl
(* (2) lookup function for any item (Id/Symbol/Num) *)
let lookup_choices =
fun item ->
- let choices =
- match universe with
- | None ->
- lookup_in_library
- C.interactive_user_uri_choice
- C.input_or_locate_uri item
- | Some e ->
- (try
- let item =
- match item with
- | Symbol (symb, _) -> Symbol (symb, 0)
- | item -> item
- in
- Environment.find item e
- with Not_found ->
- lookup_in_library
- C.interactive_user_uri_choice
- C.input_or_locate_uri item)
- in
- choices
+ match universe with
+ | None ->
+ lookup_in_library
+ C.interactive_user_uri_choice
+ C.input_or_locate_uri item
+ | Some e ->
+ (try
+ let item =
+ match item with
+ | Symbol (symb, _) -> Symbol (symb, 0)
+ | item -> item
+ in
+ Environment.find item e
+ with Not_found ->
+ lookup_in_library
+ C.interactive_user_uri_choice
+ C.input_or_locate_uri item)
in
(*
(* <benchmark> *)
(* (3) test an interpretation filling with meta uninterpreted identifiers
*)
let test_env aliases todo_dom ugraph =
- let rec aux env = function
+ try
+ let rec aux env = function
| [] -> env
| Node (_, item, l) :: tl ->
let env =
Environment.add item
- ("Implicit",
- (match item with
- | Id _ | Num _ ->
- (fun _ _ _ -> mk_implicit true)
- | Symbol _ -> (fun _ _ _ -> mk_implicit false)))
+ (mk_implicit
+ (match item with | Id _ | Num _ -> true | Symbol _ -> false))
env in
aux (aux env l) tl in
- let filled_env = aux aliases todo_dom in
- try
+ let filled_env = aux aliases todo_dom in
let cic_thing =
interpretate_thing ~context ~env:filled_env
~uri ~is_path:false thing ~localization_tbl
let rec filter = function
| [] -> [],[],[]
| codomain_item :: tl ->
- debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));
+ (*debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));*)
let new_env = Environment.add item codomain_item aliases in
let new_diff = (item,codomain_item)::diff in
(match
| Ok _
| Uncertain _ ->
aux aliases diff lookup_in_todo_dom todo_dom []
- | Ko (loc_msg) -> [],[],[aliases,diff,loc_msg,true] in
+ | Ko (loc_msg) -> [],[],[aliases,diff,loc_msg,true]
+ in
let res =
match aux' aliases [] None todo_dom with
| [],uncertain,errors ->
(fun locs domain_item ->
try
let description =
- fst (Environment.find domain_item env)
+ description_of_alias (Environment.find domain_item env)
in
Some (locs,descr_of_domain_item domain_item,description)
with
Not_found -> None)
thing_dom
in
- let diff= List.map (fun a,b -> a,fst b) diff in
+ let diff= List.map (fun a,b -> a,description_of_alias b) diff in
env',diff,loc_msg,significant
) errors
in
map_domain
(fun locs domain_item ->
let description =
- fst (Environment.find domain_item env)
+ description_of_alias (Environment.find domain_item env)
in
locs,descr_of_domain_item domain_item, description)
thing_dom)
exception Try_again of string Lazy.t
val resolve :
- 'term DisambiguateTypes.environment ->
+ env:'alias DisambiguateTypes.Environment.t ->
+ mk_choice:('alias -> 'term DisambiguateTypes.codomain_item) ->
DisambiguateTypes.Environment.key ->
- ?num:string -> ?args:'term list -> unit -> 'term
+ [`Num_arg of string | `Args of 'term list] -> 'term
val find_in_context: string -> string option list -> int
val domain_of_ast_term: context:
metasenv:'metasenv ->
subst:'subst ->
use_coercions:bool ->
- mk_implicit:(bool -> 'refined_term) ->
string_context_of_context:('context -> string option list) ->
initial_ugraph:'ugraph ->
hint:
('metasenv -> 'raw_thing -> 'raw_thing) *
(('refined_thing,'metasenv,'subst,'ugraph) test_result ->
('refined_thing,'metasenv,'subst,'ugraph) test_result) ->
- aliases:'refined_term DisambiguateTypes.codomain_item
- DisambiguateTypes.Environment.t ->
- universe:'refined_term DisambiguateTypes.codomain_item list
- DisambiguateTypes.Environment.t option ->
+ mk_implicit:(bool -> 'alias) ->
+ description_of_alias:('alias -> string) ->
+ aliases:'alias DisambiguateTypes.Environment.t ->
+ universe:'alias list DisambiguateTypes.Environment.t option ->
lookup_in_library:(
DisambiguateTypes.interactive_user_uri_choice_type ->
DisambiguateTypes.input_or_locate_uri_type ->
DisambiguateTypes.Environment.key ->
- 'refined_term DisambiguateTypes.codomain_item list) ->
+ 'alias list) ->
uri:'uri ->
pp_thing:('ast_thing -> string) ->
domain_of_thing:(context: string option list -> 'ast_thing -> domain) ->
interpretate_thing:(
context:'context ->
- env:'refined_term DisambiguateTypes.codomain_item
- DisambiguateTypes.Environment.t ->
+ env:'alias DisambiguateTypes.Environment.t ->
uri:'uri ->
is_path:bool ->
'ast_thing ->
('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
localization_tbl:'cichash ->
string * int * 'ast_thing ->
- ((DisambiguateTypes.Environment.key *
- 'refined_term DisambiguateTypes.codomain_item) list *
+ ((DisambiguateTypes.Environment.key * 'alias) list *
'metasenv * 'subst * 'refined_thing * 'ugraph)
list * bool
end
(* $Id$ *)
-(*
-type term = CicNotationPt.term
-type tactic = (term, term, GrafiteAst.reduction, string) GrafiteAst.tactic
-type tactical = (term, term, GrafiteAst.reduction, string) GrafiteAst.tactical
-type script_entry =
- | Command of tactical
- | Comment of CicNotationPt.location * string
-type script = CicNotationPt.location * script_entry list
-*)
-
type domain_item =
| Id of string (* literal *)
| Symbol of string * int (* literal, instance num *)
with Not_found -> find (Num 0) env)
| _ -> find k env
- let cons k v env =
+ let cons desc_of_alias k v env =
try
let current = find k env in
- let dsc, _ = v in
- add k (v :: (List.filter (fun (dsc', _) -> dsc' <> dsc) current)) env
+ let dsc = desc_of_alias v in
+ add k (v :: (List.filter (fun x -> desc_of_alias x <> dsc) current)) env
with Not_found ->
add k [v] env
type 'term codomain_item =
string * (* description *)
- ('term environment -> string -> 'term list -> 'term)
- (* environment, literal number, arguments as needed *)
+ [`Num_interp of string -> 'term
+ |`Sym_interp of 'term list -> 'term]
and 'term environment = 'term codomain_item Environment.t
-type 'term multiple_environment = 'term codomain_item list Environment.t
-
-
-(** adds a (name,uri) list l to a disambiguation environment e **)
-let multiple_env_of_list l e =
- List.fold_left
- (fun e (name,descr,t) -> Environment.cons (Id name) (descr,fun _ _ _ -> t) e)
- e l
-
-let env_of_list l e =
- List.fold_left
- (fun e (name,descr,t) -> Environment.add (Id name) (descr,fun _ _ _ -> t) e)
- e l
+type 'term multiple_environment =
+ 'term codomain_item list Environment.t
type interactive_user_uri_choice_type =
selection_mode:[`SINGLE | `MULTIPLE] ->
module Environment:
sig
include Map.S with type key = domain_item
- val cons: domain_item -> ('a * 'b) -> ('a * 'b) list t -> ('a * 'b) list t
+ val cons: ('b -> 'a) -> domain_item -> 'b -> 'b list t -> 'b list t
val hd: 'a list t -> 'a t
(** last alias cons-ed will be processed first *)
type 'term codomain_item =
string * (* description *)
- ('term environment -> string -> 'term list -> 'term)
- (* environment, literal number, arguments as needed *)
+ [`Num_interp of string -> 'term
+ |`Sym_interp of 'term list -> 'term]
and 'term environment = 'term codomain_item Environment.t
-type 'term multiple_environment = 'term codomain_item list Environment.t
-
-(* a simple case of extension of a disambiguation environment *)
-val env_of_list:
- (string * string * 'term) list -> 'term environment -> 'term environment
-
-val multiple_env_of_list:
- (string * string * 'term) list -> 'term multiple_environment ->
- 'term multiple_environment
+type 'term multiple_environment =
+ 'term codomain_item list Environment.t
type interactive_user_uri_choice_type =
selection_mode:[`SINGLE | `MULTIPLE] ->
]
;;
-let drop_aliases ?(minimize_instances=false) (choices, user_asked) =
+let drop_aliases ?(minimize_instances=false) ~description_of_alias
+ (choices, user_asked)
+=
let module D = DisambiguateTypes in
+ let compare ci1 ci2 = description_of_alias ci1 = description_of_alias ci2 in
let minimize d =
if not minimize_instances then
d
let rec aux =
function
[] -> []
- | (D.Symbol (s,n),((descr,_) as ci)) as he::tl when n > 0 ->
+ | (D.Symbol (s,n),ci1) as he::tl when n > 0 ->
if
List.for_all
(function
- (D.Symbol (s2,_),(descr2,_)) -> s2 <> s || descr = descr2
+ (D.Symbol (s2,_),ci2) -> s2 <> s || compare ci1 ci2
| _ -> true
) d
then
- (D.Symbol (s,0),ci)::(aux tl)
+ (D.Symbol (s,0),ci1)::(aux tl)
else
he::(aux tl)
- | (D.Num n,((descr,_) as ci)) as he::tl when n > 0 ->
+ | (D.Num n,ci1) as he::tl when n > 0 ->
if
List.for_all
- (function (D.Num _,(descr2,_)) -> descr = descr2 | _ -> true) d
+ (function (D.Num _,ci2) -> compare ci1 ci2 | _ -> true) d
then
- (D.Num 0,ci)::(aux tl)
+ (D.Num 0,ci1)::(aux tl)
else
he::(aux tl)
| he::tl -> he::(aux tl)
(List.map (fun (_, a, b, c, d) -> [], a, b, c, d) choices),
user_asked
-let disambiguate_thing ~passes ~aliases ~universe ~f thing =
+let disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~f thing
+=
assert (universe <> None);
let library = false, DisambiguateTypes.Environment.empty, None in
let multi_aliases = false, DisambiguateTypes.Environment.empty, universe in
in
let set_aliases (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) =
if use_mono_aliases then
- drop_aliases ~minimize_instances:true res (* one shot aliases *)
+ drop_aliases ~minimize_instances:true ~description_of_alias res (* one shot aliases *)
else if user_asked then
- drop_aliases ~minimize_instances:true res (* one shot aliases *)
+ drop_aliases ~minimize_instances:true ~description_of_alias res (* one shot aliases *)
else
drop_aliases_and_clear_diff res
in
aux 1 [] passes
let disambiguate_thing ~passes ~freshen_thing ~context ~metasenv ~subst
- ~mk_implicit ~string_context_of_context ~initial_ugraph ~hint ~aliases
- ~universe ~lookup_in_library ~uri ~pp_thing ~domain_of_thing
- ~interpretate_thing ~refine_thing ~localization_tbl thing
+ ~string_context_of_context ~initial_ugraph ~hint ~mk_implicit
+ ~description_of_alias ~aliases ~universe ~lookup_in_library ~uri ~pp_thing
+ ~domain_of_thing ~interpretate_thing ~refine_thing ~localization_tbl thing
=
let f ~fresh_instances ~aliases ~universe ~use_coercions (txt,len,thing) =
let thing = if fresh_instances then freshen_thing thing else thing
in
Disambiguator.disambiguate_thing
- ~context ~metasenv ~subst ~use_coercions
- ~mk_implicit ~string_context_of_context
- ~initial_ugraph ~hint
+ ~context ~metasenv ~subst ~use_coercions ~string_context_of_context
+ ~initial_ugraph ~hint ~mk_implicit ~description_of_alias
~aliases ~universe ~lookup_in_library
~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
~localization_tbl (txt,len,thing)
in
- disambiguate_thing ~passes ~aliases ~universe ~f thing
+ disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~f thing
context:'context ->
metasenv:'metasenv ->
subst:'subst ->
- mk_implicit:(bool -> 'refined_term) ->
string_context_of_context:('context -> string option list) ->
initial_ugraph:'ugraph ->
hint:
('metasenv -> 'raw_thing -> 'raw_thing) *
(('refined_thing,'metasenv,'subst,'ugraph) Disambiguate.test_result ->
('refined_thing,'metasenv,'subst,'ugraph) Disambiguate.test_result) ->
- aliases:'refined_term DisambiguateTypes.codomain_item
- DisambiguateTypes.Environment.t ->
- universe:'refined_term DisambiguateTypes.codomain_item list
+ mk_implicit:(bool -> 'alias) ->
+ description_of_alias:('alias -> string) ->
+ aliases:'alias DisambiguateTypes.Environment.t ->
+ universe:'alias list
DisambiguateTypes.Environment.t option ->
lookup_in_library:(
DisambiguateTypes.interactive_user_uri_choice_type ->
DisambiguateTypes.input_or_locate_uri_type ->
DisambiguateTypes.Environment.key ->
- 'refined_term DisambiguateTypes.codomain_item list) ->
+ 'alias list) ->
uri:'uri ->
pp_thing:('ast_thing -> string) ->
domain_of_thing:
(context: string option list -> 'ast_thing -> Disambiguate.domain) ->
interpretate_thing:(
context:'context ->
- env:'refined_term DisambiguateTypes.codomain_item
- DisambiguateTypes.Environment.t ->
+ env:'alias DisambiguateTypes.Environment.t ->
uri:'uri ->
is_path:bool ->
'ast_thing ->
('refined_thing, 'metasenv,'subst,'ugraph) Disambiguate.test_result) ->
localization_tbl:'cichash ->
string * int * 'ast_thing ->
- ((DisambiguateTypes.Environment.key *
- 'refined_term DisambiguateTypes.codomain_item) list *
+ ((DisambiguateTypes.Environment.key * 'alias) list *
'metasenv * 'subst * 'refined_thing * 'ugraph)
list * bool
val parse_environment:
include_paths:string list ->
string ->
- Cic.term DisambiguateTypes.environment *
- Cic.term DisambiguateTypes.multiple_environment
+ 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
in
HLog.debug debug; assert false
+(*
let cic_codomain_of_uri uri =
(UriManager.string_of_uri uri,
let term =
in
fun _ _ _ -> term)
;;
-
-let cic_num_choices = DisambiguateChoices.lookup_num_choices;;
+*)
-let cic_mk_choice =
- DisambiguateChoices.mk_choice
- ~mk_implicit:(function
- | true -> Cic.Implicit (Some `Type)
- | false -> Cic.Implicit None)
- ~mk_appl:(function (Cic.Appl l)::tl -> Cic.Appl (l@tl) | l -> Cic.Appl l)
- ~term_of_uri:CicUtil.term_of_uri
+(*let cic_num_choices = DisambiguateChoices.lookup_num_choices;;*)
+
+let __Implicit = "__Implicit__"
+let __Closed_Implicit = "__Closed_Implicit__"
+
+let cic_mk_choice = function
+ | LexiconAst.Symbol_alias (name, _, dsc) ->
+ if name = __Implicit then
+ dsc, `Sym_interp (fun _ -> Cic.Implicit None)
+ else if name = __Closed_Implicit then
+ dsc, `Sym_interp (fun _ -> Cic.Implicit (Some `Closed))
+ else
+ DisambiguateChoices.cic_lookup_symbol_by_dsc name dsc
+ | LexiconAst.Number_alias (_, dsc) ->
+ DisambiguateChoices.lookup_num_by_dsc dsc
+ | LexiconAst.Ident_alias (name, uri) ->
+ uri, `Sym_interp
+ (fun l->assert(l = []);CicUtil.term_of_uri (UriManager.uri_of_string uri))
+;;
+
+let cic_mk_implicit b =
+ match b with
+ | false ->
+ LexiconAst.Symbol_alias (__Implicit,-1,"Fake Implicit")
+ | true ->
+ LexiconAst.Symbol_alias (__Closed_Implicit,-1,"Fake Closed Implicit")
;;
let ncic_codomain_of_uri uri =
;;
let ncic_num_choices _ = (*assert false*) [];;
-
let ncic_mk_choice =
DisambiguateChoices.mk_choice
~mk_implicit:(function
;;
let lookup_in_library
- codomain_of_uri mk_choice num_choices
interactive_user_uri_choice input_or_locate_uri item
=
+ let mk_ident_alias id u =
+ LexiconAst.Ident_alias (id,UriManager.string_of_uri u)
+ in
+ let mk_num_alias instance =
+ List.map
+ (fun dsc,_ -> LexiconAst.Number_alias (instance,dsc))
+ (DisambiguateChoices.lookup_num_choices())
+ in
+ let mk_symbol_alias symb ino (dsc, _,_) =
+ LexiconAst.Symbol_alias (symb,ino,dsc)
+ in
let dbd = LibraryDb.instance () in
let choices_of_id id =
let uris = Whelp.locate ~dbd id in
match item with
| DisambiguateTypes.Id id ->
let uris = choices_of_id id in
- List.map codomain_of_uri uris
- | DisambiguateTypes.Symbol (symb, _) ->
+ List.map (mk_ident_alias id) uris
+ | DisambiguateTypes.Symbol (symb, ino) ->
(try
- List.map mk_choice (TermAcicContent.lookup_interpretations symb)
+ List.map (mk_symbol_alias symb ino)
+ (TermAcicContent.lookup_interpretations symb)
with
TermAcicContent.Interpretation_not_found -> [])
- | DisambiguateTypes.Num instance -> num_choices ()
+ | DisambiguateTypes.Num instance -> mk_num_alias instance
;;
(** @param term not meaningful when context is given *)
(CicDisambiguate.disambiguate_term
~aliases:lexicon_status.LexiconEngine.aliases
?goal ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
- ~lookup_in_library:(lookup_in_library cic_codomain_of_uri cic_mk_choice
- cic_num_choices)
+ ~lookup_in_library
+ ~mk_choice:cic_mk_choice
+ ~mk_implicit:cic_mk_implicit
+ ~description_of_alias:LexiconAst.description_of_alias
~context ~metasenv ~subst:[] (text,prefix_len,term))
in
let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
let (diff, metasenv, _, cic, ugraph) =
singleton "second"
(CicDisambiguate.disambiguate_term
- ~lookup_in_library:(lookup_in_library cic_codomain_of_uri
- cic_mk_choice cic_num_choices)
+ ~lookup_in_library
+ ~mk_choice:cic_mk_choice
+ ~mk_implicit:cic_mk_implicit
+ ~description_of_alias:LexiconAst.description_of_alias
~initial_ugraph:ugraph ~aliases:lexicon_status.LexiconEngine.aliases
~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
~context ~metasenv ~subst:[] ?goal
let (diff, metasenv, _, cic, _) =
singleton "third"
(CicDisambiguate.disambiguate_obj
- ~lookup_in_library:(lookup_in_library cic_codomain_of_uri cic_mk_choice
- cic_num_choices)
+ ~lookup_in_library
+ ~mk_choice:cic_mk_choice
+ ~mk_implicit:cic_mk_implicit
+ ~description_of_alias:LexiconAst.description_of_alias
~aliases:lexicon_status.LexiconEngine.aliases
~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~uri
(text,prefix_len,obj)) in
(* composed magic: term + command magics. No need to change this value *)
let magic = magic + 10000 * CicNotationPt.magic
+let description_of_alias =
+ function
+ Ident_alias (_,desc)
+ | Symbol_alias (_,_,desc)
+ | Number_alias (_,desc) -> desc
let pp_l2_pattern = CicNotationPp.pp_term
let pp_alias = function
- | Ident_alias (id, uri) -> sprintf "alias id \"%s\" = \"%s\"" id uri
+ | Ident_alias (id, uri) -> sprintf "alias id \"%s\" = \"%s\"." id uri
| Symbol_alias (symb, instance, desc) ->
- sprintf "alias symbol \"%s\" %s= \"%s\""
+ sprintf "alias symbol \"%s\" %s= \"%s\"."
symb
(if instance=0 then "" else "(instance "^ string_of_int instance ^ ") ")
desc
| Number_alias (instance,desc) ->
- sprintf "alias num (instance %d) = \"%s\"" instance desc
+ sprintf "alias num (instance %d) = \"%s\"." instance desc
let pp_associativity = function
| Gramext.LeftA -> "left associative"
exception MetadataNotFound of string (* file name *)
type status = {
- aliases: Cic.term DisambiguateTypes.environment; (** disambiguation aliases *)
- multi_aliases: Cic.term DisambiguateTypes.multiple_environment;
+ 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 *)
}
else
let commands_of_aliases =
List.map
- (fun alias -> LexiconAst.Alias (HExtlib.dummy_floc, alias))
+ (fun _,alias -> LexiconAst.Alias (HExtlib.dummy_floc, alias))
in
let aliases =
List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc)
status.aliases new_aliases in
let multi_aliases =
- List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.cons d c acc)
- status.multi_aliases new_aliases in
+ List.fold_left (fun acc (d,c) ->
+ DisambiguateTypes.Environment.cons LexiconAst.description_of_alias
+ d c acc)
+ status.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 aliases =
- DisambiguatePp.aliases_of_domain_and_codomain_items_list new_aliases
- in
let status =
- add_lexicon_content (commands_of_aliases aliases) new_status
+ add_lexicon_content (commands_of_aliases new_aliases) new_status
in
status
->
let item = DisambiguateTypes.Id id in
(try
- let t =
- snd (DisambiguateTypes.Environment.find item status.aliases)
- status.aliases "" [] in
- let uri = CicUtil.uri_of_term t in
+ let uri =
+ match DisambiguateTypes.Environment.find item status.aliases with
+ LexiconAst.Ident_alias (_, uri)-> UriManager.uri_of_string uri
+ | _ -> assert false
+ in
CicNotationPt.UriPattern uri
with Not_found ->
prerr_endline ("Domain item not found: " ^
code in DisambiguatePp *)
match spec with
| LexiconAst.Ident_alias (id,uri) ->
- [DisambiguateTypes.Id id,
- (uri,(fun _ _ _-> CicUtil.term_of_uri(UriManager.uri_of_string uri)))]
+ [DisambiguateTypes.Id id,spec]
| LexiconAst.Symbol_alias (symb, instance, desc) ->
- [DisambiguateTypes.Symbol (symb,instance),
- DisambiguateChoices.cic_lookup_symbol_by_dsc symb desc]
+ [DisambiguateTypes.Symbol (symb,instance),spec]
| LexiconAst.Number_alias (instance,desc) ->
- [DisambiguateTypes.Num instance,
- DisambiguateChoices.lookup_num_by_dsc desc]
+ [DisambiguateTypes.Num instance,spec]
in
set_proof_aliases mode status diff
| LexiconAst.Interpretation (_, dsc, (symbol, _), _) as stm ->
let diff =
try
[DisambiguateTypes.Symbol (symbol, 0),
- DisambiguateChoices.cic_lookup_symbol_by_dsc symbol dsc]
+ LexiconAst.Symbol_alias (symbol,0,dsc)]
with
DisambiguateChoices.Choice_not_found msg ->
prerr_endline (Lazy.force msg);
exception IncludedFileNotCompiled of string * string
type status = {
- aliases: Cic.term DisambiguateTypes.environment;(** disambiguation aliases *)
- multi_aliases: Cic.term DisambiguateTypes.multiple_environment;
+ 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 eval_command : status -> LexiconAst.command -> status
val set_proof_aliases:
- status ->
- (DisambiguateTypes.Environment.key *
- Cic.term DisambiguateTypes.codomain_item) list ->
+ status -> (DisambiguateTypes.domain_item * LexiconAst.alias_spec) list ->
status
(* this callback is called on every lexicon command *)
let alias_diff ~from status =
let module Map = DisambiguateTypes.Environment in
Map.fold
- (fun domain_item (description1,_ as codomain_item) acc ->
+ (fun domain_item codomain_item acc ->
+ let description1 = LexiconAst.description_of_alias codomain_item in
try
- let description2,_ = Map.find domain_item from.LexiconEngine.aliases in
+ let description2 =
+ LexiconAst.description_of_alias
+ (Map.find domain_item from.LexiconEngine.aliases)
+ in
if description1 <> description2 then
(domain_item,codomain_item)::acc
else
Not_found ->
(domain_item,codomain_item)::acc)
status.LexiconEngine.aliases []
+;;
let alias_diff =
let profiler = HExtlib.profile "alias_diff(conteg. anche in include)" in
let build_aliases =
List.map
(fun (name,uri) ->
- DisambiguateTypes.Id name,
- (UriManager.string_of_uri uri, fun _ _ _ -> CicUtil.term_of_uri uri))
+ DisambiguateTypes.Id name, LexiconAst.Ident_alias (name,
+ UriManager.string_of_uri uri))
let add_aliases_for_inductive_def status types uri =
let aliases = build_aliases (extract_alias types uri) in
* order to be equal to aliases of the second argument *)
val alias_diff:
from:LexiconEngine.status -> LexiconEngine.status ->
- (DisambiguateTypes.domain_item *
- Cic.term DisambiguateTypes.codomain_item) list
+ (DisambiguateTypes.domain_item * LexiconAst.alias_spec) list
val push: unit -> unit
val pop: unit -> unit
aux 1 context
let interpretate_term
- ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast ~localization_tbl
+ ?(create_dummy_ids=false) ~mk_choice ~context ~env ~uri ~is_path ast
+ ~localization_tbl
=
(* create_dummy_ids shouldbe used only for interpretating patterns *)
assert (uri = None);
| CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term
| CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) ->
let cic_args = List.map (aux ~localize loc context) args in
- Disambiguate.resolve env (Symbol (symb, i)) ~args:cic_args ()
+ Disambiguate.resolve ~mk_choice ~env (Symbol (symb, i)) (`Args cic_args)
| CicNotationPt.Appl terms ->
NCic.Appl (List.map (aux ~localize loc context) terms)
| CicNotationPt.Binder (binder_kind, (var, typ), body) ->
| `Pi
| `Forall -> NCic.Prod (cic_name, cic_type, cic_body)
| `Exists ->
- Disambiguate.resolve env (Symbol ("exists", 0))
- ~args:[ cic_type; NCic.Lambda (cic_name, cic_type, cic_body) ] ())
+ Disambiguate.resolve ~env ~mk_choice (Symbol ("exists", 0))
+ (`Args [ cic_type; NCic.Lambda (cic_name, cic_type, cic_body) ]))
| CicNotationPt.Case (term, indty_ident, outtype, branches) ->
let cic_term = aux ~localize loc context term in
let cic_outtype = aux_option ~localize loc context `Term outtype in
let indtype_ref =
match indty_ident with
| Some (indty_ident, _) ->
- (match Disambiguate.resolve env (Id indty_ident) () with
+ (match Disambiguate.resolve ~env ~mk_choice
+ (Id indty_ident) (`Args []) with
| NCic.Const r -> r
| NCic.Implicit _ ->
raise (Disambiguate.Try_again
"because it is an inductive type without constructors "^
"or because all patterns use wildcards")))
in
- (match Disambiguate.resolve env (Id (fst_constructor branches)) () with
+ (match Disambiguate.resolve ~env ~mk_choice
+ (Id (fst_constructor branches)) (`Args []) with
| NCic.Const r -> r
| NCic.Implicit _ ->
raise (Disambiguate.Try_again
assert (subst = None);
(try
NCic.Rel (find_in_context name context)
- with Not_found -> Disambiguate.resolve env (Id name) ())
+ with Not_found ->
+ Disambiguate.resolve ~env ~mk_choice (Id name) (`Args []))
| CicNotationPt.Uri (name, subst) ->
assert (subst = None);
(try
| CicNotationPt.Implicit -> NCic.Implicit `Term
| CicNotationPt.UserInput -> assert false (*NCic.Implicit (Some `Hole)
patterns not implemented *)
- | CicNotationPt.Num (num, i) -> Disambiguate.resolve env (Num i) ~num ()
+ | CicNotationPt.Num (num, i) ->
+ Disambiguate.resolve ~env ~mk_choice (Num i) (`Num_arg num)
| CicNotationPt.Meta (index, subst) ->
let cic_subst =
List.map
| CicNotationPt.Sort (`CProp _u) -> NCic.Sort (NCic.Type
[false,NUri.uri_of_string "cic:/matita/pts/CProp.univ"])
| CicNotationPt.Symbol (symbol, instance) ->
- Disambiguate.resolve env (Symbol (symbol, instance)) ()
+ Disambiguate.resolve ~env ~mk_choice
+ (Symbol (symbol, instance)) (`Args [])
| _ -> assert false (* god bless Bologna *)
and aux_option ~localize loc context annotation = function
| None -> NCic.Implicit annotation
;;
let disambiguate_term ~context ~metasenv ~subst ?goal
+ ~mk_implicit ~description_of_alias ~mk_choice
~aliases ~universe ~lookup_in_library
(text,prefix_len,term)
=
MultiPassDisambiguator.disambiguate_thing
~freshen_thing:CicNotationUtil.freshen_term
~context ~metasenv ~initial_ugraph:() ~aliases
+ ~mk_implicit ~description_of_alias
~string_context_of_context:(List.map (fun (x,_) -> Some x))
~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
- ~mk_implicit:(function false -> NCic.Implicit `Term
- | true -> NCic.Implicit `Closed)
~passes:(MultiPassDisambiguator.passes ())
~lookup_in_library ~domain_of_thing:domain_of_term
- ~interpretate_thing:(interpretate_term (?create_dummy_ids:None))
+ ~interpretate_thing:(interpretate_term ~mk_choice (?create_dummy_ids:None))
~refine_thing:refine_term (text,prefix_len,term)
~localization_tbl ~hint ~subst
in
List.map (function (a,b,c,d,_) -> a,b,c,d) res, b
;;
+
metasenv:NCic.metasenv ->
subst:NCic.substitution ->
?goal:int ->
- aliases:NCic.term DisambiguateTypes.environment ->
- universe:NCic.term DisambiguateTypes.multiple_environment option ->
+ mk_implicit: (bool -> 'alias) ->
+ description_of_alias:('alias -> string) ->
+ mk_choice:('alias -> NCic.term DisambiguateTypes.codomain_item) ->
+ aliases:'alias DisambiguateTypes.Environment.t ->
+ universe:'alias list DisambiguateTypes.Environment.t option ->
lookup_in_library:(
DisambiguateTypes.interactive_user_uri_choice_type ->
DisambiguateTypes.input_or_locate_uri_type ->
DisambiguateTypes.Environment.key ->
- NCic.term DisambiguateTypes.codomain_item list) ->
+ 'alias list) ->
CicNotationPt.term Disambiguate.disambiguator_input ->
- ((DisambiguateTypes.domain_item *
- NCic.term DisambiguateTypes.codomain_item) list *
+ ((DisambiguateTypes.domain_item * 'alias) list *
NCic.metasenv *
NCic.substitution *
NCic.term) list *
in
addDebugItem "dump aliases" (fun _ ->
let status = script#lexicon_status in
- HLog.debug (DisambiguatePp.pp_environment status.LexiconEngine.aliases));
+ HLog.debug (String.concat "\n"
+ (DisambiguateTypes.Environment.fold
+ (fun _ x l -> (LexiconAstPp.pp_alias x)::l)
+ status.LexiconEngine.aliases [])));
addDebugItem "dump environment to \"env.dump\"" (fun _ ->
let oc = open_out "env.dump" in
CicEnvironment.dump_to_channel oc;
LexiconSync.alias_diff ~from:lexicon_status new_lexicon_status in
let _,intermediate_states =
List.fold_left
- (fun (lexicon_status,acc) (k,((v,_) as value)) ->
+ (fun (lexicon_status,acc) (k,value) ->
+ let v = LexiconAst.description_of_alias value in
let b =
try
(* this hack really sucks! *)
(fun (_,alias) ->
match alias with
None -> ()
- | Some (k,((v,_) as value)) ->
- let newtxt =
- DisambiguatePp.pp_environment
- (DisambiguateTypes.Environment.add k value
- DisambiguateTypes.Environment.empty)
- in
+ | Some (k,value) ->
+ let newtxt = LexiconAstPp.pp_alias value in
raise (TryingToAdd newtxt)) new_statuses;
let grafite_status,lexicon_status =
match new_statuses with
CicNotationPt.term GrafiteAst.reduction, CicNotationPt.term CicNotationPt.obj, string)
GrafiteAst.statement) ->
((GrafiteTypes.status * LexiconEngine.status) *
- (DisambiguateTypes.domain_item *
- Cic.term DisambiguateTypes.codomain_item) option
- ) list
+ (DisambiguateTypes.domain_item * LexiconAst.alias_spec) option) list
(* heavy checks slow down the compilation process but give you some interesting
CicNotationPt.term GrafiteAst.reduction, CicNotationPt.term CicNotationPt.obj, string)
GrafiteAst.statement -> unit) ->
((GrafiteTypes.status * LexiconEngine.status) *
- (DisambiguateTypes.domain_item *
- Cic.term DisambiguateTypes.codomain_item) option
- ) list
+ (DisambiguateTypes.domain_item * LexiconAst.alias_spec) option) list
(* this callback is called on every grafite command *)
val set_callback: (GrafiteParser.ast_statement -> unit) -> unit
String.concat "\n"
("" ::
List.map
- (fun k,value ->
- DisambiguatePp.pp_environment
- (DisambiguateTypes.Environment.add k
- (value,(fun _ _ _ -> Cic.Implicit None))
- DisambiguateTypes.Environment.empty))
+ (fun k,desc ->
+ let id = DisambiguateTypes.string_of_domain_item k in
+ LexiconAstPp.pp_alias (LexiconAst.Ident_alias (id,desc)))
diff) ^ "\n"
in
source_buffer#insert
let txt,_ = MatitaGtkMisc.utf8_parsed_text txt
(HExtlib.floc_of_loc (prefix_len,MatitaGtkMisc.utf8_string_length txt))
in
- prerr_endline ("txt:" ^ txt);
dialog#uriChoiceLabel#set_label txt;
List.iter model#easy_append uris;
let return v =
(fun (acc, to_prepend) (status,alias) ->
match alias with
| None -> (status,to_prepend ^ nonskipped_txt)::acc,""
- | Some (k,((v,_) as value)) ->
- let newtxt = DP.pp_environment (DTE.add k value DTE.empty) in
+ | Some (k,value) ->
+ let newtxt = LexiconAstPp.pp_alias value in
(status,to_prepend ^ newtxt ^ "\n")::acc, "")
([],skipped_txt) enriched_history_fragment
in
projects / helm.git / commitdiff