module Ast = NotationPt
-(* 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 *
((Stdpp.location list * string * string) list *
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
else
raise Ambiguous_input
-let mono_interp_callback _ _ _ = raise Ambiguous_input
-let mono_disamb_callback _ = raise Ambiguous_input
+let mono_interp_callback _ _ _ = assert false
+let mono_disamb_callback _ = assert false
let _choose_uris_callback = ref mono_uris_callback
let _choose_interp_callback = ref mono_interp_callback
let interactive_user_uri_choice = !_choose_uris_callback
let interactive_interpretation_choice interp = !_choose_interp_callback interp
let interactive_ast_choice interp = !_choose_disamb_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"
| [] -> None
| (ctx0,t0 as hd)::tl ->
(* prerr_endline ("ok! length tl = " ^ string_of_int (List.length tl)); *)
- prerr_endline ("visiting t0 = " ^ pp_term t0);
- if test t0 then (prerr_endline "t0 is ambiguous"; Some hd)
+ debug_print (lazy ("visiting t0 = " ^ pp_term t0));
+ if test t0 then (debug_print (lazy "t0 is ambiguous"); Some hd)
else
(*
(prerr_endline ("splitting not ambiguous t0:");
in match (refine_profiler.HExtlib.profile foo ()) with
| Ko x ->
let _,err = Lazy.force x in
- prerr_endline ("test_interpr error: " ^ err);
+ debug_print (lazy ("test_interpr error: " ^ err));
false
| _ -> true
with
let res =
Environment.find item universe
in
- prerr_endline (Printf.sprintf "choices for %s :\n%s"
- (d2s item) (String.concat ", " (List.map a2s res)));
+ debug_print (lazy (Printf.sprintf "choices for %s :\n%s"
+ (d2s item) (String.concat ", " (List.map a2s res))));
res
in
match ts with
| [] -> None
| t0 :: tl ->
- prerr_endline ("disambiguate_list: t0 = " ^ pp_thing t0);
+ debug_print (lazy ("disambiguate_list: t0 = " ^ pp_thing t0));
let is_ambiguous = function
| Ast.Ident (_,`Ambiguous)
| Ast.Num (_,None)
(* get first ambiguous subterm (or return disambiguated term) *)
match visit ~pp_term is_ambiguous t0 with
| None ->
- prerr_endline ("visit -- not ambiguous node:\n" ^ pp_thing t0);
+ debug_print (lazy ("visit -- not ambiguous node:\n" ^ pp_thing t0));
Some (t0,tl)
| Some (ctx, t) ->
- prerr_endline ("visit -- found ambiguous node: " ^ astpp t ^
- "\nin " ^ pp_thing (ctx t));
+ debug_print (lazy ("visit -- found ambiguous node: " ^ astpp t ^
+ "\nin " ^ pp_thing (ctx t)));
(* get possible instantiations of t *)
let instances = get_instances ctx t in
- prerr_endline ("-- possible instances:");
+ debug_print (lazy "-- possible instances:");
List.iter
- (fun u0 -> prerr_endline ("-- instance: " ^ (pp_thing u0))) instances;
+ (fun u0 -> debug_print (lazy ("-- instance: " ^ (pp_thing u0)))) instances;
(* perforate ambiguous subterms and test refinement *)
- prerr_endline ("-- survivors:");
+ debug_print (lazy "-- survivors:");
let survivors = List.filter test_interpr instances in
List.iter
- (fun u0 -> prerr_endline ("-- survivor: " ^ (pp_thing u0))) survivors;
+ (fun u0 -> debug_print (lazy ("-- survivor: " ^ (pp_thing u0)))) survivors;
disambiguate_list (survivors@tl)
;;
let refine t =
let localization_tbl = mk_localization_tbl 503 in
- prerr_endline "before interpretate_thing";
+ debug_print (lazy "before interpretate_thing");
let t' =
interpretate_thing ~context ~env ~universe ~uri ~is_path:false t ~localization_tbl
in
- prerr_endline "after interpretate_thing";
+ debug_print (lazy "after interpretate_thing");
match refine_thing metasenv subst context uri ~use_coercions t' expty
base_univ ~localization_tbl with
| Ok (t',m',s',u') -> t,m',s',t',u'
| Uncertain x ->
let _,err = Lazy.force x in
- prerr_endline ("refinement uncertain after disambiguation: " ^ err);
+ debug_print (lazy ("refinement uncertain after disambiguation: " ^ err));
assert false
| _ -> assert false
in
if not (test_interpr thing) then
- (prerr_endline ("preliminary test fail: " ^ pp_thing thing);
+ (debug_print (lazy ("preliminary test fail: " ^ pp_thing thing));
raise (NoWellTypedInterpretation (0,[])))
else
let res = aux [thing] in
let res =
HExtlib.filter_map (fun t ->
try Some (refine t)
- with _ -> prerr_endline ("can't interpretate/refine " ^ (pp_thing t));None) res
+ with _ ->
+ debug_print (lazy ("can't interpretate/refine " ^ (pp_thing t)));None) res
in
match res with
| [] -> raise (NoWellTypedInterpretation (0,[]))
+ (* XXX : the boolean seems not to play a role any longer *)
| [t] -> res,false
- | _ ->
- let choices = List.map (fun (t,_,_,_,_) -> pp_thing t) res in
+ | _ -> res, true
+ (* let choices = List.map (fun (t,_,_,_,_) -> pp_thing t) res in
let user_choice = interactive_ast_choice choices in
[ List.nth res user_choice ], true
(* let pp_thing (t,_,_,_,_,_) = prerr_endline ("interpretation: " ^ (pp_thing t)) in
- List.iter pp_thing res; res,true *)
+ List.iter pp_thing res; res,true *) *)
;;
projects / helm.git / blobdiff