- (* get first ambiguous subterm (or return disambiguated term) *)
- match visit ~pp_term is_ambiguous t0 with
- | None ->
- debug_print (lazy ("visit -- not ambiguous node:\n" ^ pp_thing t0));
- Some (t0,tl)
- | Some (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
- debug_print (lazy "-- possible instances:");
- List.iter
- (fun u0 -> debug_print (lazy ("-- instance: " ^ (pp_thing u0)))) instances;
- (* perforate ambiguous subterms and test refinement *)
- debug_print (lazy "-- survivors:");
- let survivors = List.filter test_interpr instances in
- List.iter
- (fun u0 -> debug_print (lazy ("-- survivor: " ^ (pp_thing u0)))) survivors;
- disambiguate_list (survivors@tl)
+ let process_ast t0 =
+ (* get first ambiguous subterm (or return disambiguated term) *)
+ match visit ~pp_term is_ambiguous t0 with
+ | None ->
+(* debug_print (lazy ("visit -- not ambiguous node:\n" ^ pp_thing
+ * t0));*)
+ (* Some (t0,tl), errors *)
+ raise Not_ambiguous
+ | Some (ctx, t, loc_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
+ if instances = [] then
+ raise (NoWellTypedInterpretation (loc_t, "No choices for " ^ astpp t));
+ debug_print (lazy "-- possible instances:");
+(* List.iter
+ (fun u0 -> debug_print (lazy ("-- instance: " ^ (pp_thing u0))))
+instances; *)
+ (* perforate ambiguous subterms and test refinement *)
+ let instances = List.map (fun (x,a) -> (x,Some a),test_interpr x) instances in
+ debug_print (lazy "-- survivors:");
+ let survivors, defuncts =
+ List.partition (fun (_,o) -> o = None) instances in
+ survivors, (defuncts, loc_t)
+
+ in
+ try
+ let ts', new_errors = List.split (List.map process_ast ts) in
+ let ts' = List.map (fun ((t,_),_) -> t) (List.flatten ts') in
+ let errors' = match new_errors with
+ | (_,l)::_ ->
+ let ne' =
+ List.map (fun (a,b) -> a, HExtlib.unopt b)
+ (List.flatten (List.map fst new_errors)) in
+ let ne' = List.map (fun ((x,a),(l,e)) -> x,a,l,e) ne' in
+ (ne',l)::errors
+ | _ -> errors
+ in disambiguate_list ts' errors'
+ with Not_ambiguous -> ts,errors