(fun (i,res) (name,_,_,_) ->
i + 1,(name,name,Cic.MutInd (uri,i,[]))::res
) (0,[]) tyl) in
- let con_env = DisambiguateTypes.singleton_env_of_list name_to_uris env in
+ let con_env = DisambiguateTypes.env_of_list name_to_uris env in
let undebrujin t =
snd
(List.fold_right
context:Cic.context ->
metasenv:Cic.metasenv ->
?initial_ugraph:CicUniv.universe_graph ->
- aliases:aliases -> (* previous interpretation status *)
+ aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
+ universe:DisambiguateTypes.multiple_environment option ->
CicNotationPt.term ->
(environment * (* new interpretation status *)
Cic.metasenv * (* new metasenv *)
val disambiguate_obj :
?fresh_instances:bool ->
dbd:Mysql.dbd ->
- aliases:aliases -> (* previous interpretation status *)
+ aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
+ universe:DisambiguateTypes.multiple_environment option ->
uri:UriManager.uri option -> (* required only for inductive types *)
GrafiteAst.obj ->
(environment * (* new interpretation status *)
uris
let disambiguate_thing ~dbd ~context ~metasenv
- ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases
+ ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe
~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing thing
=
debug_print "DISAMBIGUATE INPUT";
- let current_env, multi_aliases_env =
- match aliases with
- | false, e -> Environment.hd e, None
- | true, e -> Environment.empty, Some e
- in
let disambiguate_context = (* cic context -> disambiguate context *)
List.map
(function None -> Cic.Anonymous | Some (name, _) -> name)
debug_print (sprintf "DISAMBIGUATION DOMAIN: %s"
(string_of_domain thing_dom));
debug_print (sprintf "DISAMBIGUATION ENVIRONMENT: %s"
- (DisambiguatePp.pp_environment (snd aliases)));
+ (DisambiguatePp.pp_environment aliases));
+ debug_print (sprintf "DISAMBIGUATION UNIVERSE: %s"
+ (match universe with None -> "None" | Some _ -> "Some _"));
let current_dom =
- Environment.fold (fun item _ dom -> item :: dom) current_env []
+ Environment.fold (fun item _ dom -> item :: dom) aliases []
in
let todo_dom = domain_diff thing_dom current_dom in
(* (2) lookup function for any item (Id/Symbol/Num) *)
| Num instance ->
DisambiguateChoices.lookup_num_choices ()
in
- match multi_aliases_env with
+ match universe with
| None -> lookup_in_library ()
| Some e ->
(try
(* (3) test an interpretation filling with meta uninterpreted identifiers
*)
- let test_env current_env todo_dom ugraph =
+ let test_env aliases todo_dom ugraph =
let filled_env =
List.fold_left
(fun env item ->
(match item with
| Id _ | Num _ -> (fun _ _ _ -> Cic.Implicit (Some `Closed))
| Symbol _ -> (fun _ _ _ -> Cic.Implicit None))) env)
- current_env todo_dom
+ aliases todo_dom
in
try
let cic_thing =
| Invalid_choice -> Ko, ugraph
in
(* (4) build all possible interpretations *)
- let rec aux current_env todo_dom base_univ =
+ let rec aux aliases todo_dom base_univ =
match todo_dom with
| [] ->
- (match test_env current_env [] base_univ with
+ (match test_env aliases [] base_univ with
| Ok (thing, metasenv),new_univ ->
- [ current_env, metasenv, thing, new_univ ]
+ [ aliases, metasenv, thing, new_univ ]
| Ko,_ | Uncertain,_ -> [])
| item :: remaining_dom ->
debug_print (sprintf "CHOOSED ITEM: %s"
| codomain_item :: tl ->
debug_print (sprintf "%s CHOSEN" (fst codomain_item)) ;
let new_env =
- Environment.add item codomain_item current_env
+ Environment.add item codomain_item aliases
in
(match test_env new_env remaining_dom univ with
| Ok (thing, metasenv),new_univ ->
let base_univ = initial_ugraph in
try
let res =
- match aux current_env todo_dom base_univ with
+ match aux aliases todo_dom base_univ with
| [] -> raise NoWellTypedInterpretation
| [ e,me,t,u ] ->
debug_print "SINGLE INTERPRETATION";
let choices, b = res in
(List.map
(fun (env, metasenv, t, ugraph) ->
- Environment.fold Environment.cons env (snd aliases),
+ Environment.fold Environment.add env aliases,
metasenv, t, ugraph)
choices),
b
failwith "Disambiguate: circular dependency"
let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
- ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases term
+ ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe term
=
let term =
if fresh_instances then CicNotationUtil.freshen_term term else term
in
disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases
- ~uri:None ~pp_thing:CicNotationPp.pp_term
+ ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
~domain_of_thing:domain_of_term ~interpretate_thing:interpretate_term
~refine_thing:refine_term term
- let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~uri obj =
+ let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri
+ obj
+ =
let obj =
if fresh_instances then CicNotationUtil.freshen_obj obj else obj
in
- disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~uri
+ disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~universe ~uri
~pp_thing:GrafiteAstPp.pp_obj ~domain_of_thing:domain_of_obj
~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
obj
let ast = CicNotationParser.parse_level2_ast (Stream.of_string term) in
try
fst (Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast
- ?initial_ugraph ~aliases:(false, aliases))
+ ?initial_ugraph ~aliases ~universe:None)
with Exit -> raise (Ambiguous_term term)
end
let parse_environment str =
let stream = Stream.of_string str in
let environment = ref Environment.empty in
+ let multiple_environment = ref Environment.empty in
try
while true do
let alias =
Num instance,
DisambiguateChoices.lookup_num_by_dsc desc
in
- environment := Environment.cons key value !environment;
+ environment := Environment.add key value !environment;
+ multiple_environment := Environment.cons key value !multiple_environment;
done;
assert false
with End_of_file ->
- !environment
+ !environment, !multiple_environment
let aliases_of_environment env =
Environment.fold
- (fun domain_item codomain_items acc ->
- List.fold_left
- (fun strings (dsc, _) ->
- let s =
- match domain_item with
- | Id id -> GrafiteAst.Ident_alias (id, dsc)
- | Symbol (symb, i) -> GrafiteAst.Symbol_alias (symb, i, dsc)
- | Num i -> GrafiteAst.Number_alias (i, dsc)
- in
- s :: strings)
- acc codomain_items)
+ (fun domain_item (dsc,_) acc ->
+ let s =
+ match domain_item with
+ | Id id -> GrafiteAst.Ident_alias (id, dsc)
+ | Symbol (symb, i) -> GrafiteAst.Symbol_alias (symb, i, dsc)
+ | Num i -> GrafiteAst.Number_alias (i, dsc)
+ in
+ s :: acc)
env []
let commands_of_environment env =
type codomain_item =
string * (* description *)
- (singleton_environment -> string -> Cic.term list -> Cic.term)
+ (environment -> string -> Cic.term list -> Cic.term)
(* environment, literal number, arguments as needed *)
-and environment = codomain_item list Environment.t
+and environment = codomain_item Environment.t
+
+type multiple_environment = codomain_item list Environment.t
-and singleton_environment = codomain_item Environment.t
(** adds a (name,uri) list l to a disambiguation environment e **)
-let env_of_list l 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 singleton_env_of_list l e =
+let env_of_list l e =
List.fold_left
(fun e (name,descr,t) -> Environment.add (Id name) (descr,fun _ _ _ -> t) e)
e l
let string_of_domain dom =
String.concat "; " (List.map string_of_domain_item dom)
-let empty_environment = Environment.empty
-
let floc_of_loc (loc_begin, loc_end) =
let floc_begin =
{ Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1;
projects / helm.git / commitdiff