-(*
-let disambiguate_thing
- ~context ~metasenv ~subst ~use_coercions
- ~string_context_of_context
- ~initial_ugraph:base_univ ~expty
- ~mk_implicit ~description_of_alias ~fix_instance
- ~aliases ~universe ~lookup_in_library
- ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
- ~mk_localization_tbl
- (thing_txt,thing_txt_prefix_len,thing)
-=
- debug_print (lazy "DISAMBIGUATE INPUT");
- debug_print (lazy ("TERM IS: " ^ (pp_thing thing)));
- let thing_dom =
- domain_of_thing ~context:(string_context_of_context context) thing in
- debug_print
- (lazy (sprintf "DISAMBIGUATION DOMAIN: %s"(string_of_domain thing_dom)));
- let current_dom =
- Environment.fold (fun item _ dom -> item :: dom) aliases [] in
- let todo_dom = domain_diff thing_dom current_dom in
- debug_print
- (lazy (sprintf "DISAMBIGUATION DOMAIN AFTER DIFF: %s"(string_of_domain todo_dom)));
- (* (2) lookup function for any item (Id/Symbol/Num) *)
- let lookup_choices =
- fun item ->
- match universe with
- | None ->
- lookup_in_library
- interactive_user_uri_choice
- input_or_locate_uri item
- | Some e ->
- (try
- fix_instance item (Environment.find item e)
- with Not_found -> [])
- in
-
- (* items with 1 choice are interpreted ASAP *)
- let aliases, todo_dom =
- let rec aux (aliases,acc) = function
- | [] -> aliases, acc
- | (Node (_, item,extra) as node) :: tl ->
- let choices = lookup_choices item in
- if List.length choices <> 1 then aux (aliases, acc@[node]) tl
- else
- let tl = tl @ extra in
- if Environment.mem item aliases then aux (aliases, acc) tl
- else aux (Environment.add item (List.hd choices) aliases, acc) tl
- in
- aux (aliases,[]) todo_dom
- in
-
-(*
- (* <benchmark> *)
- let _ =
- if benchmark then begin
- let per_item_choices =
- List.map
- (fun dom_item ->
- try
- let len = List.length (lookup_choices dom_item) in
- debug_print (lazy (sprintf "BENCHMARK %s: %d"
- (string_of_domain_item dom_item) len));
- len
- with No_choices _ -> 0)
- thing_dom
- in
- max_refinements := List.fold_left ( * ) 1 per_item_choices;
- actual_refinements := 0;
- domain_size := List.length thing_dom;
- choices_avg :=
- (float_of_int !max_refinements) ** (1. /. float_of_int !domain_size)
- end
- in
- (* </benchmark> *)
-*)
-
- (* (3) test an interpretation filling with meta uninterpreted identifiers
- *)
- let test_env aliases todo_dom ugraph =
- try
- let rec aux env = function
- | [] -> env
- | Node (_, item, l) :: tl ->
- let env =
- Environment.add item
- (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
- let localization_tbl = mk_localization_tbl 503 in
- let cic_thing =
- interpretate_thing ~context ~env:filled_env
- ~uri ~is_path:false thing ~localization_tbl
- in
-let foo () =
- refine_thing metasenv subst context uri
- ~use_coercions cic_thing expty ugraph ~localization_tbl
-in refine_profiler.HExtlib.profile foo ()
- with
- | Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg))
- | Invalid_choice loc_msg -> Ko loc_msg
- in
- (* (4) build all possible interpretations *)
- let (@@) (l1,l2,l3) (l1',l2',l3') = l1@l1', l2@l2', l3@l3' in
- (* aux returns triples Ok/Uncertain/Ko *)
- (* rem_dom is the concatenation of all the remainin domains *)
- let rec aux aliases diff lookup_in_todo_dom todo_dom rem_dom =
- debug_print (lazy ("ZZZ: " ^ string_of_domain todo_dom));
- match todo_dom with
- | [] ->
- assert (lookup_in_todo_dom = None);
- (match test_env aliases rem_dom base_univ with
- | Ok (thing, metasenv,subst,new_univ) ->
- [ aliases, diff, metasenv, subst, thing, new_univ ], [], []
- | Ko loc_msg -> [],[],[aliases,diff,loc_msg,true]
- | Uncertain loc_msg ->
- [],[aliases,diff,loc_msg],[])
- | Node (locs,item,inner_dom) :: remaining_dom ->
- debug_print (lazy (sprintf "CHOOSED ITEM: %s"
- (string_of_domain_item item)));
- let choices =
- match lookup_in_todo_dom with
- None -> lookup_choices item
- | Some choices -> choices in
- match choices with
- [] ->
- [], [],
- [aliases, diff,
- (lazy (List.hd locs,
- "No choices for " ^ string_of_domain_item item)),
- true]
-(*
- | [codomain_item] ->
- (* just one choice. We perform a one-step look-up and
- if the next set of choices is also a singleton we
- skip this refinement step *)
- 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
- let lookup_in_todo_dom,next_choice_is_single =
- match remaining_dom with
- [] -> None,false
- | (_,he)::_ ->
- let choices = lookup_choices he in
- Some choices,List.length choices = 1
- in
- if next_choice_is_single then
- aux new_env new_diff lookup_in_todo_dom remaining_dom
- base_univ
- else
- (match test_env new_env remaining_dom base_univ with
- | Ok (thing, metasenv),new_univ ->
- (match remaining_dom with
- | [] ->
- [ new_env, new_diff, metasenv, thing, new_univ ], []
- | _ ->
- aux new_env new_diff lookup_in_todo_dom
- remaining_dom new_univ)
- | Uncertain (loc,msg),new_univ ->
- (match remaining_dom with
- | [] -> [], [new_env,new_diff,loc,msg,true]
- | _ ->
- aux new_env new_diff lookup_in_todo_dom
- remaining_dom new_univ)
- | Ko (loc,msg),_ -> [], [new_env,new_diff,loc,msg,true])
-*)
- | _::_ ->
- let mark_not_significant failures =
- List.map
- (fun (env, diff, loc_msg, _b) ->
- env, diff, loc_msg, false)
- failures in
- let classify_errors ((ok_l,uncertain_l,error_l) as outcome) =
- if ok_l <> [] || uncertain_l <> [] then
- ok_l,uncertain_l,mark_not_significant error_l
- else
- outcome in
- let rec filter = function
- | [] -> [],[],[]
- | 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
- (inner_dom@remaining_dom@rem_dom) base_univ
- with
- | Ok (thing, metasenv,subst,new_univ) ->
-(* prerr_endline "OK"; *)
- let res =
- (match inner_dom with
- | [] ->
- [new_env,new_diff,metasenv,subst,thing,new_univ],
- [], []
- | _ ->
- aux new_env new_diff None inner_dom
- (remaining_dom@rem_dom)
- )
- in
- res @@ filter tl
- | Uncertain loc_msg ->
-(* prerr_endline ("UNCERTAIN"); *)
- let res =
- (match inner_dom with
- | [] -> [],[new_env,new_diff,loc_msg],[]
- | _ ->
- aux new_env new_diff None inner_dom
- (remaining_dom@rem_dom)
- )
- in
- res @@ filter tl
- | Ko loc_msg ->
-(* prerr_endline "KO"; *)
- let res = [],[],[new_env,new_diff,loc_msg,true] in
- res @@ filter tl)
- in
- let ok_l,uncertain_l,error_l =
- classify_errors (filter choices)
- in
- let res_after_ok_l =
- List.fold_right
- (fun (env,diff,_,_,_,_) res ->
- aux env diff None remaining_dom rem_dom @@ res
- ) ok_l ([],[],error_l)
- in
- List.fold_right
- (fun (env,diff,_) res ->
- aux env diff None remaining_dom rem_dom @@ res
- ) uncertain_l res_after_ok_l
- in
- let aux' aliases diff lookup_in_todo_dom todo_dom =
- if todo_dom = [] then
- aux aliases diff lookup_in_todo_dom todo_dom []
- else
- match test_env aliases todo_dom base_univ with
- | Ok _
- | Uncertain _ ->
- aux aliases diff lookup_in_todo_dom todo_dom []
- | Ko (loc_msg) -> [],[],[aliases,diff,loc_msg,true]
- in
- let res =
- match aux' aliases [] None todo_dom with
- | [],uncertain,errors ->
- let errors =
- List.map
- (fun (env,diff,loc_msg) -> (env,diff,loc_msg,true)
- ) uncertain @ errors
- in
- let errors =
- List.map
- (fun (env,diff,loc_msg,significant) ->
- let env' =
- filter_map_domain
- (fun locs domain_item ->
- try
- let description =
- 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,description_of_alias b) diff in
- env',diff,loc_msg,significant
- ) errors
- in
- raise (NoWellTypedInterpretation (0,errors))
- | [_,diff,metasenv,subst,t,ugraph],_,_ ->
- debug_print (lazy "SINGLE INTERPRETATION");
- [diff,metasenv,subst,t,ugraph], false
- | l,_,_ ->
- debug_print
- (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l)));
- let choices =
- List.map
- (fun (env, _, _, _, _, _) ->
- map_domain
- (fun locs domain_item ->
- let description =
- description_of_alias (Environment.find domain_item env)
- in
- locs,descr_of_domain_item domain_item, description)
- thing_dom)
- l
- in
- let choosed =
- interactive_interpretation_choice
- thing_txt thing_txt_prefix_len choices
- in
- (List.map (fun n->let _,d,m,s,t,u= List.nth l n in d,m,s,t,u)
- choosed),
- true
- in
- res
- *)