class type g_status =
object
inherit Interpretations.g_status
+ inherit NCicLibrary.g_status
method disambiguate_db: db
end
class virtual status uid =
object (self)
inherit Interpretations.status uid
+ inherit NCicLibrary.status uid
val disambiguate_db = initial_status
method disambiguate_db = disambiguate_db
method set_disambiguate_db v = {< disambiguate_db = v >}
DisambiguateTypes.InterprEnv.empty } >}
method set_disambiguate_status
: 'status. #g_status as 'status -> 'self
- = fun o -> ((self#set_interp_status o)#set_disambiguate_db o#disambiguate_db)
+ = fun o -> ((self#set_interp_status o)#set_disambiguate_db
+ o#disambiguate_db)#set_lib_status o
end
(* let eval_with_new_aliases status f =
new_aliases,res
;;*)
+(* reports the first source of ambiguity and its possible interpretations *)
+exception Ambiguous_input of (Stdpp.location * GrafiteAst.alias_spec list)
+
+(* reports disambiguation errors *)
+exception Error of
+ (* location of a choice point *)
+ (Stdpp.location *
+ (* one possible choice (or no valid choice) *)
+ (GrafiteAst.alias_spec option *
+ (* list of asts together with the failing location and error msg *)
+ ((Stdpp.location * GrafiteAst.alias_spec) list *
+ Stdpp.location * string) list)
+ list)
+ list
+
let dump_aliases out msg status =
out (if msg = "" then "aliases dump:" else msg ^ ": aliases dump:");
DisambiguateTypes.InterprEnv.iter (fun _ x -> out (GrafiteAstPp.pp_alias x))
exception BaseUriNotSetYet
-let singleton msg = function
- | [x], _ -> x
- | l, _ ->
- let debug =
- Printf.sprintf "GrafiteDisambiguate.singleton (%s): %u interpretations"
- msg (List.length l)
- in
- prerr_endline debug; assert false
-
let __Implicit = "__Implicit__"
let __Closed_Implicit = "__Closed_Implicit__"
GrafiteAst.Symbol_alias (__Closed_Implicit,None,"Fake Closed Implicit")
;;
-let nlookup_in_library
+let nlookup_in_library status
interactive_user_uri_choice input_or_locate_uri item
=
match item with
| DisambiguateTypes.Id id ->
(try
- let references = NCicLibrary.resolve id in
+ let references = NCicLibrary.resolve status id in
List.map
(fun u ->
GrafiteAst.Ident_alias (id,NReference.string_of_reference u)
| _ -> assert false
;;
+(* this function, called on a list of choices that must
+ * be different, never fails and returns the location of
+ * the first ambiguity (and its possible interpretations) *)
+let rec find_diffs l =
+ let loc,_ = List.hd (List.hd l) in
+ let hds = List.map (fun x -> snd (List.hd x)) l in
+ let uniq_hds = HExtlib.list_uniq (List.sort Pervasives.compare hds) in
+
+ if List.length uniq_hds > 1
+ then loc, uniq_hds
+ else
+ let tls = List.map List.tl l in
+ find_diffs tls
+;;
+
+(* clusterize a list of errors according to the last chosen interpretation *)
+let clusterize diff (eframe,loc0) =
+ let rec aux = function
+ | [] -> []
+ | (_,choice,_,_ as x)::l0 ->
+ let matches,others = List.partition (fun (_,c,_,_) -> c = choice) l0 in
+ (choice,List.map (fun (a,_,l,e) -> diff a,l,e) (x::matches)) ::
+ aux others
+ in loc0, aux eframe
+
let disambiguate_nterm status expty context metasenv subst thing
=
- let newast, metasenv, subst, cic =
- singleton "first"
- (NCicDisambiguate.disambiguate_term
+ let _,_,thing' = thing in
+ match NCicDisambiguate.disambiguate_term
status
~aliases:status#disambiguate_db.interpr
~expty
~universe:(status#disambiguate_db.multi_aliases)
- ~lookup_in_library:nlookup_in_library
+ ~lookup_in_library:(nlookup_in_library status)
~mk_choice:(ncic_mk_choice status)
~mk_implicit ~fix_instance
~description_of_alias:GrafiteAst.description_of_alias
- ~context ~metasenv ~subst thing)
- in
- let _,_,thing' = thing in
- let diff = diff_term Stdpp.dummy_loc thing' newast in
- let status = add_to_interpr status diff
- in
- metasenv, subst, status, cic
+ ~context ~metasenv ~subst thing
+ with
+ | Disambiguate.Disamb_success [newast,metasenv,subst,cic,_] ->
+ let diff = diff_term Stdpp.dummy_loc thing' newast in
+ let status = add_to_interpr status diff
+ in
+ metasenv, subst, status, cic
+ | Disambiguate.Disamb_success (_::_ as choices) ->
+ let diffs =
+ List.map (fun (ast,_,_,_,_) ->
+ diff_term Stdpp.dummy_loc thing' ast) choices
+ in
+ raise (Ambiguous_input (find_diffs diffs))
+ | Disambiguate.Disamb_failure (l,_) ->
+ raise (Error (List.map (clusterize (diff_term Stdpp.dummy_loc thing')) l))
+ | _ -> assert false
;;
-
type pattern =
NotationPt.term Disambiguate.disambiguator_input option *
(string * NCic.term) list * NCic.term option
metasenv, `Auto params
;;
-let disambiguate_nobj status ?baseuri (text,prefix_len,obj) =
+let disambiguate_nobj status ?baseuri (text,prefix_len,obj as obj') =
let uri =
let baseuri =
match baseuri with Some x -> x | None -> raise BaseUriNotSetYet
in
NUri.uri_of_string (baseuri ^ "/" ^ name)
in
- let ast, _, _, cic =
- singleton "third"
- (NCicDisambiguate.disambiguate_obj
+
+ match NCicDisambiguate.disambiguate_obj
status
- ~lookup_in_library:nlookup_in_library
+ ~lookup_in_library:(nlookup_in_library status)
~description_of_alias:GrafiteAst.description_of_alias
~mk_choice:(ncic_mk_choice status)
~mk_implicit ~fix_instance ~uri
~aliases:status#disambiguate_db.interpr
~universe:(status#disambiguate_db.multi_aliases)
- (text,prefix_len,obj)) in
- let diff = diff_obj Stdpp.dummy_loc obj ast in
- let status = add_to_interpr status diff
- in
- status, cic
+ obj'
+ with
+ | Disambiguate.Disamb_success [newast,_,_,cic,_] ->
+ let diff = diff_obj Stdpp.dummy_loc obj newast in
+ let status = add_to_interpr status diff
+ in status, cic
+ | Disambiguate.Disamb_success (_::_ as choices) ->
+ let diffs =
+ List.map (fun (ast,_,_,_,_) ->
+ diff_obj Stdpp.dummy_loc obj ast) choices
+ in
+ raise (Ambiguous_input (find_diffs diffs))
+ | Disambiguate.Disamb_failure (l,_) ->
+ raise (Error (List.map (clusterize (diff_obj Stdpp.dummy_loc obj)) l))
+ | _ -> assert false
;;
let disambiguate_cic_appl_pattern status args =
List.concat
(List.map
(fun nref ->
- let references = NCicLibrary.aliases_of nref in
+ let references = NCicLibrary.aliases_of status nref in
List.map
(fun u ->
let name = NCicPp.r2s status true u in
projects / helm.git / blobdiff