Cic.Meta (index, cic_subst)
| CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
| CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
- | CicNotationPt.Sort `Type -> Cic.Sort (Cic.Type (CicUniv.fresh())) (* TASSI *)
+ | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
| CicNotationPt.Sort `CProp -> Cic.Sort Cic.CProp
| CicNotationPt.Symbol (symbol, instance) ->
resolve env (Symbol (symbol, instance)) ()
aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
universe:DisambiguateTypes.multiple_environment option ->
CicNotationPt.term ->
- (environment * (* new interpretation status *)
+ ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
Cic.metasenv * (* new metasenv *)
Cic.term*
CicUniv.universe_graph) list * (* disambiguated term *)
universe:DisambiguateTypes.multiple_environment option ->
uri:UriManager.uri option -> (* required only for inductive types *)
GrafiteAst.obj ->
- (environment * (* new interpretation status *)
+ ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
Cic.metasenv * (* new metasenv *)
Cic.obj *
CicUniv.universe_graph) list * (* disambiguated obj *)
fun _ _ _ -> term))
uris
-let refine_profiler = CicUtil.profile "disambiguate_thing.refine_thing"
+let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
let disambiguate_thing ~dbd ~context ~metasenv
?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe
let foo () =
let k,ugraph1 = refine_thing metasenv context uri cic_thing ugraph in
(k , ugraph1 )
-in refine_profiler.CicUtil.profile foo ()
+in refine_profiler.HExtlib.profile foo ()
with
| Try_again -> Uncertain, ugraph
| Invalid_choice -> Ko, ugraph
in
(* (4) build all possible interpretations *)
- let rec aux aliases todo_dom base_univ =
+ let rec aux aliases diff todo_dom base_univ =
match todo_dom with
| [] ->
(match test_env aliases [] base_univ with
| Ok (thing, metasenv),new_univ ->
- [ aliases, metasenv, thing, new_univ ]
+ [ aliases, diff, metasenv, thing, new_univ ]
| Ko,_ | Uncertain,_ -> [])
| item :: remaining_dom ->
debug_print (lazy (sprintf "CHOOSED ITEM: %s"
| codomain_item :: tl ->
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 test_env new_env remaining_dom univ with
| Ok (thing, metasenv),new_univ ->
(match remaining_dom with
- | [] -> [ new_env, metasenv, thing, new_univ ]
- | _ -> aux new_env remaining_dom new_univ )@
+ | [] -> [ new_env, new_diff, metasenv, thing, new_univ ]
+ | _ -> aux new_env new_diff remaining_dom new_univ )@
filter univ tl
| Uncertain,new_univ ->
(match remaining_dom with
| [] -> []
- | _ -> aux new_env remaining_dom new_univ )@
+ | _ -> aux new_env new_diff remaining_dom new_univ )@
filter univ tl
| Ko,_ -> filter univ tl)
in
let base_univ = initial_ugraph in
try
let res =
- match aux aliases todo_dom base_univ with
+ match aux aliases [] todo_dom base_univ with
| [] -> raise NoWellTypedInterpretation
- | [ e,me,t,u ] ->
+ | [_,diff,metasenv,t,ugraph] ->
debug_print (lazy "SINGLE INTERPRETATION");
- [ e,me,t,u ], false
+ [diff,metasenv,t,ugraph], false
| l ->
debug_print (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l)));
let choices =
List.map
- (fun (env, _, _, _) ->
+ (fun (env, _, _, _, _) ->
List.map
(fun domain_item ->
let description =
l
in
let choosed = C.interactive_interpretation_choice choices in
- (List.map (List.nth l) choosed), true
+ (List.map (fun n->let _,d,m,t,u= List.nth l n in d,m,t,u) choosed),
+ true
in
-(*
- (if benchmark then
- let res_size = List.length res in
- debug_print (lazy (sprintf
- ("BENCHMARK: %d/%d refinements performed, domain size %d, interps %d, k %.2f\n" ^^
- "BENCHMARK: estimated %.2f")
- !actual_refinements !max_refinements !domain_size res_size
- !choices_avg
- (float_of_int (!domain_size - 1) *. !choices_avg *. (float_of_int res_size) +. !choices_avg))));
-*)
- res
+ res
with
CicEnvironment.CircularDependency s ->
failwith "Disambiguate: circular dependency"