module Ast = CicNotationPt
+(* the integer is an offset to be added to each location *)
+exception Ambiguous_input
(* the integer is an offset to be added to each location *)
exception NoWellTypedInterpretation of
int *
(** raised when an environment is not enough informative to decide *)
exception Try_again of string Lazy.t
-type ('alias,'term) aliases= bool * 'term DisambiguateTypes.environment
+type ('alias,'term) aliases =
+ bool * 'term DisambiguateTypes.codomain_item DisambiguateTypes.Environment.t
type 'a disambiguator_input = string * int * 'a
type domain = domain_tree list
and domain_tree = Node of Stdpp.location list * domain_item * domain
+let mono_uris_callback ~selection_mode ?ok
+ ?(enable_button_for_non_vars = true) ~title ~msg ~id =
+ if Helm_registry.get_opt_default Helm_registry.get_bool ~default:true
+ "matita.auto_disambiguation"
+ then
+ function l -> l
+ else
+ raise Ambiguous_input
+
+let mono_interp_callback _ _ _ = raise Ambiguous_input
+
+let _choose_uris_callback = ref mono_uris_callback
+let _choose_interp_callback = ref mono_interp_callback
+let set_choose_uris_callback f = _choose_uris_callback := f
+let set_choose_interp_callback f = _choose_interp_callback := f
+
+let interactive_user_uri_choice = !_choose_uris_callback
+let interactive_interpretation_choice interp = !_choose_interp_callback interp
+let input_or_locate_uri ~(title:string) ?id () = None
+ (* Zack: I try to avoid using this callback. I therefore assume that
+ * the presence of an identifier that can't be resolved via "locate"
+ * query is a syntax error *)
+
+
let rec string_of_domain =
function
[] -> ""
[] subst in
[ Node ([loc], Id name, terms) ]))
| Ast.Uri _ -> []
+ | Ast.NRef _ -> []
| Ast.Implicit -> []
| Ast.Num (num, i) -> [ Node ([loc], Num i, []) ]
| Ast.Meta (index, local_context) ->
let domain_of_obj ~context obj =
uniq_domain (domain_of_obj ~context obj)
-let domain_of_ast_term = domain_of_term;;
-
(* dom1 \ dom2 *)
let domain_diff dom1 dom2 =
(* let domain_diff = Domain.diff *)
in
aux dom1
-module type Disambiguator =
-sig
- val disambiguate_thing:
- context:'context ->
- metasenv:'metasenv ->
- subst:'subst ->
- use_coercions:bool ->
- 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) ->
- 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 ->
- 'alias list) ->
- uri:'uri ->
- pp_thing:('ast_thing -> string) ->
- domain_of_thing:(context: string option list -> 'ast_thing -> domain) ->
- interpretate_thing:(
- context:'context ->
- env:'alias DisambiguateTypes.Environment.t ->
- uri:'uri ->
- is_path:bool ->
- 'ast_thing ->
- localization_tbl:'cichash ->
- 'raw_thing) ->
- refine_thing:(
- 'metasenv -> 'subst -> 'context -> 'uri -> use_coercions:bool ->
- 'raw_thing -> 'ugraph -> localization_tbl:'cichash ->
- ('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
- localization_tbl:'cichash ->
- string * int * 'ast_thing ->
- ((DisambiguateTypes.Environment.key * 'alias) list *
- 'metasenv * 'subst * 'refined_thing * 'ugraph)
- list * bool
-end
-
-module Make (C: Callbacks) =
- struct
let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
- let disambiguate_thing
- ~context ~metasenv ~subst ~use_coercions
- ~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
- (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)));
-(*
- debug_print (lazy (sprintf "DISAMBIGUATION ENVIRONMENT: %s"
- (DisambiguatePp.pp_environment aliases)));
- debug_print (lazy (sprintf "DISAMBIGUATION UNIVERSE: %s"
- (match universe with None -> "None" | Some _ -> "Some _")));
-*)
- 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
- 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
+let disambiguate_thing
+ ~context ~metasenv ~subst ~use_coercions
+ ~string_context_of_context
+ ~initial_ugraph:base_univ ~expty
+ ~mk_implicit ~description_of_alias
+ ~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
+ let item =
+ match item with
+ | Symbol (symb, _) -> Symbol (symb, 0)
+ | item -> item
+ in
+ Environment.find item e
+ with Not_found -> [])
+ in
(*
(* <benchmark> *)
let _ =
(* </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 cic_thing =
- interpretate_thing ~context ~env:filled_env
- ~uri ~is_path:false thing ~localization_tbl
- in
- let cic_thing = (fst hint) metasenv cic_thing in
+ (* (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 () =
- let k =
- refine_thing metasenv subst context uri
- ~use_coercions cic_thing ugraph ~localization_tbl
- in
- let k = (snd hint) k in
- k
+ 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]
+ 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])
+ | [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) ->
- 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 ->
- 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 ->
- 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 =
- 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
+ | _::_ ->
+ 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 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
+ 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
- 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 =
- C.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
+ 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
- res
-
- end
+ 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
projects / helm.git / blobdiff