(* $Id$ *)
+module Ast = NotationPt
+
type db = {
- aliases: GrafiteAst.alias_spec DisambiguateTypes.Environment.t;
+ (* maps (loc,domain_item) to alias *)
+ interpr: GrafiteAst.alias_spec DisambiguateTypes.InterprEnv.t;
+ (* the universe of possible interpretations for all symbols/ids/nums *)
multi_aliases: GrafiteAst.alias_spec list DisambiguateTypes.Environment.t;
- new_aliases: (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list
+ (* new_aliases: ((Stdpp.location * DisambiguateTypes.domain_item) * GrafiteAst.alias_spec) list *)
}
+let get_interpr db =
+ db.interpr
+;;
+
let initial_status = {
- aliases = DisambiguateTypes.Environment.empty;
+ interpr = DisambiguateTypes.InterprEnv.empty;
multi_aliases = DisambiguateTypes.Environment.empty;
- new_aliases = []
+ (* new_aliases = [] *)
}
class type g_status =
object
inherit Interpretations.g_status
+ inherit NCicLibrary.g_status
method disambiguate_db: db
end
-class virtual status =
+class virtual status uid =
object (self)
- inherit Interpretations.status
+ 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 >}
+ method reset_disambiguate_db () =
+ {< disambiguate_db = { self#disambiguate_db with interpr =
+ 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 =
+(* let eval_with_new_aliases status f =
let status =
status#set_disambiguate_db { status#disambiguate_db with new_aliases = [] } in
let res = f status in
let new_aliases = status#disambiguate_db.new_aliases in
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.Environment.iter (fun _ x -> out (GrafiteAstPp.pp_alias x))
- status#disambiguate_db.aliases
+ DisambiguateTypes.InterprEnv.iter (fun _ x -> out (GrafiteAstPp.pp_alias x))
+ status#disambiguate_db.interpr
+
+let add_to_interpr status new_aliases =
+ let interpr =
+ List.fold_left (fun acc (k,c) ->
+ DisambiguateTypes.InterprEnv.add k c acc)
+ status#disambiguate_db.interpr new_aliases
+ in
+ let new_status =
+ {status#disambiguate_db with interpr = interpr }
+ in
+ status#set_disambiguate_db new_status
-let set_proof_aliases status ~implicit_aliases mode new_aliases =
- if mode = GrafiteAst.WithoutPreferences then
- status
- else
- let aliases =
- List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc)
- status#disambiguate_db.aliases new_aliases in
+let add_to_disambiguation_univ status new_aliases =
let multi_aliases =
List.fold_left (fun acc (d,c) ->
DisambiguateTypes.Environment.cons GrafiteAst.description_of_alias
status#disambiguate_db.multi_aliases new_aliases
in
let new_status =
- {multi_aliases = multi_aliases ;
- aliases = aliases;
- new_aliases =
- (if implicit_aliases then new_aliases else []) @
- status#disambiguate_db.new_aliases}
+ {status#disambiguate_db with multi_aliases = multi_aliases }
in
status#set_disambiguate_db new_status
-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
+exception BaseUriNotSetYet
let __Implicit = "__Implicit__"
let __Closed_Implicit = "__Closed_Implicit__"
-let ncic_mk_choice status = function
- | GrafiteAst.Symbol_alias (name, _, dsc) ->
+let ncic_mk_choice status a =
+ prerr_endline "ncic_mk_choice";
+ match a with
+ | GrafiteAst.Symbol_alias (name,_, dsc) ->
+ prerr_endline ("caso 1: " ^ name ^ "; " ^ dsc);
if name = __Implicit then
dsc, `Sym_interp (fun _ -> NCic.Implicit `Term)
else if name = __Closed_Implicit then
dsc, `Sym_interp (fun _ -> NCic.Implicit `Closed)
else
+ (prerr_endline (Printf.sprintf "mk_choice: symbol %s, interpr %s"
+ name dsc);
DisambiguateChoices.lookup_symbol_by_dsc status
~mk_implicit:(function
| true -> NCic.Implicit `Closed
~mk_appl:(function
(NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l)
~term_of_nref:(fun nref -> NCic.Const nref)
- name dsc
- | GrafiteAst.Number_alias (_, dsc) ->
+ name dsc)
+ | GrafiteAst.Number_alias (_,dsc) ->
+ prerr_endline ("caso 2: " ^ dsc);
let desc,f = DisambiguateChoices.nlookup_num_by_dsc dsc in
desc, `Num_interp
(fun num -> match f with `Num_interp f -> f num | _ -> assert false)
| GrafiteAst.Ident_alias (name, uri) ->
+ prerr_endline ("caso 3: " ^ name);
uri, `Sym_interp
(fun l->assert(l = []);
let nref = NReference.reference_of_string uri in
let mk_implicit b =
match b with
| false ->
- GrafiteAst.Symbol_alias (__Implicit,-1,"Fake Implicit")
+ GrafiteAst.Symbol_alias (__Implicit,None,"Fake Implicit")
| true ->
- GrafiteAst.Symbol_alias (__Closed_Implicit,-1,"Fake 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)
+ (fun u ->
+ GrafiteAst.Ident_alias (id,NReference.string_of_reference u)
) references
with
NCicEnvironment.ObjectNotFound _ -> [])
| _ -> []
;;
-let fix_instance item l =
+(* XXX TO BE REMOVED: no need to fix instances any more *)
+(*let fix_instance item l =
match item with
DisambiguateTypes.Symbol (_,n) ->
List.map
(function
- GrafiteAst.Symbol_alias (s,_,d) -> GrafiteAst.Symbol_alias (s,n,d)
+ GrafiteAst.Symbol_alias (s,d) -> GrafiteAst.Symbol_alias (s,n,d)
| _ -> assert false
) l
| DisambiguateTypes.Num n ->
| _ -> assert false
) l
| DisambiguateTypes.Id _ -> l
+;;*)
+let fix_instance _ l = l;;
+
+let rec diff_term loc t u = match (t,u) with
+ | Ast.AttributedTerm (`Loc l,t'), Ast.AttributedTerm (_,u') -> diff_term l t' u'
+ | Ast.AttributedTerm (_,t'), Ast.AttributedTerm (_,u') -> diff_term loc t' u'
+ | Ast.Appl tl, Ast.Appl ul ->
+ List.fold_left2 (fun acc t0 u0 -> diff_term loc t0 u0@acc) [] tl ul
+ | Ast.Binder (_,v1,b1), Ast.Binder (_,v2,b2) ->
+ diff_var loc v1 v2@ diff_term loc b1 b2
+ | Ast.Case (t1,ity1,outty1,pl1),Ast.Case (t2,ity2,outty2,pl2) ->
+ let ity_interp = match ity1,ity2 with
+ | Some (i,None), Some (_,Some r) ->
+ let uri = NReference.string_of_reference r in
+ [loc,GrafiteAst.Ident_alias (i,uri)]
+ | _ -> []
+ in
+ let oty_interp = match outty1,outty2 with
+ | Some o1, Some o2 -> diff_term loc o1 o2
+ | _ -> []
+ in
+ (* pl = (case_pattern * term) list *)
+ let auxpatt (c1,u1) (c2,u2) acc =
+ let diff_cp = match c1,c2 with
+ | Ast.Pattern (i,href1,vars1), Ast.Pattern (_,href2,vars2) ->
+ let diff_i = match href1,href2 with
+ | None, Some r ->
+ let uri = NReference.string_of_reference r in
+ [loc,GrafiteAst.Ident_alias (i,uri)]
+ | _ -> []
+ in
+ let diff_vars =
+ List.fold_right2 (fun v1 v2 acc0 -> diff_var loc v1 v2 @ acc0) vars1 vars2 []
+ in
+ diff_i @ diff_vars
+ | _ -> []
+ in
+ diff_term loc u1 u2 @ diff_cp @ acc
+ in
+ let pl_interp = List.fold_right2 auxpatt pl1 pl2 [] in
+ diff_term loc t1 t2 @ ity_interp @ oty_interp @ pl_interp
+ | Ast.Cast (u1,v1),Ast.Cast (u2,v2) ->
+ diff_term loc u1 u2@diff_term loc v1 v2
+ | Ast.LetIn (var1,u1,v1),Ast.LetIn (var2,u2,v2) ->
+ diff_var loc var1 var2 @ diff_term loc u1 u2 @ diff_term loc v1 v2
+ | Ast.LetRec (_,fl1,w1),Ast.LetRec (_,fl2,w2) ->
+ let diff_funs =
+ List.fold_right2
+ (fun (vars1,f1,b1,_) (vars2,f2,b2,_) acc ->
+ let diff_vars =
+ List.fold_right2
+ (fun v1 v2 acc0 -> diff_var loc v1 v2 @ acc0) vars1 vars2 []
+ in
+ diff_vars @ diff_var loc f1 f2 @ diff_term loc b1 b2 @ acc)
+ fl1 fl2 []
+ in
+ diff_funs @ diff_term loc w1 w2
+ | Ast.Ident (n,`Ambiguous),Ast.Ident (_,`Uri u) ->
+ [loc,GrafiteAst.Ident_alias (n,u)]
+ | Ast.Symbol (s, None),Ast.Symbol(_,Some (uri,desc)) ->
+ [loc,GrafiteAst.Symbol_alias (s,uri,desc)]
+ | Ast.Num (_, None),Ast.Num (_,Some (uri,desc)) ->
+ [loc,GrafiteAst.Number_alias (uri,desc)]
+ | _ -> [] (* leaves *)
+and diff_var loc (_,v1) (_,v2) = match v1,v2 with
+ | Some v1', Some v2' -> diff_term loc v1' v2'
+ | _ -> []
+;;
+
+let diff_obj loc o1 o2 = match o1,o2 with
+ | Ast.Inductive (ls1,itys1), Ast.Inductive (ls2,itys2) ->
+ let diff_ls =
+ List.fold_right2 (fun v1 v2 acc -> diff_var loc v1 v2 @ acc) ls1 ls2 []
+ in
+ let diff_itys =
+ List.fold_right2
+ (fun (i1,_,ty1,cl1) (i2,_,ty2,cl2) acc0 ->
+ let diff_cl =
+ List.fold_right2
+ (fun (_,u) (_,v) acc1 -> diff_term loc u v @ acc1)
+ cl1 cl2 []
+ in
+ diff_term loc ty1 ty2 @ diff_cl @ acc0)
+ itys1 itys2 []
+ in
+ diff_ls @ diff_itys
+ | Ast.Theorem (_,i1,b1,ty1,_), Ast.Theorem (_,i2,b2,ty2,_) ->
+ let diff_tys = match ty1,ty2 with
+ | Some ty1', Some ty2' -> diff_term loc ty1' ty2'
+ | _ -> []
+ in
+ diff_term loc b1 b2 @ diff_tys
+ | Ast.Record (ls1,_,ty1,fl1),Ast.Record (ls2,_,ty2,fl2) ->
+ let diff_ls =
+ List.fold_right2 (fun v1 v2 acc -> diff_var loc v1 v2 @ acc) ls1 ls2 []
+ in
+ let diff_fl =
+ List.fold_right2
+ (fun (_,f1,_,_) (_,f2,_,_) acc -> diff_term loc f1 f2 @ acc) fl1 fl2 []
+ in
+ diff_ls @ diff_term loc ty1 ty2 @ diff_fl
+ | _ -> 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 diff, metasenv, subst, cic =
- singleton "first"
- (NCicDisambiguate.disambiguate_term
+ let _,_,thing' = thing in
+ match NCicDisambiguate.disambiguate_term
status
- ~aliases:status#disambiguate_db.aliases
+ ~aliases:status#disambiguate_db.interpr
~expty
- ~universe:(Some status#disambiguate_db.multi_aliases)
- ~lookup_in_library:nlookup_in_library
+ ~universe:(status#disambiguate_db.multi_aliases)
+ ~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 status =
- set_proof_aliases status ~implicit_aliases:true GrafiteAst.WithPreferences
- 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 diff, _, _, 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.aliases
- ~universe:(Some status#disambiguate_db.multi_aliases)
- (text,prefix_len,obj)) in
- let status =
- set_proof_aliases status ~implicit_aliases:true GrafiteAst.WithPreferences
- diff
- in
- status, cic
+ ~aliases:status#disambiguate_db.interpr
+ ~universe:(status#disambiguate_db.multi_aliases)
+ 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 =
try
match
DisambiguateTypes.Environment.find item
- status#disambiguate_db.aliases
+ (* status#disambiguate_db.aliases *)
+ status#disambiguate_db.multi_aliases
with
- GrafiteAst.Ident_alias (_, uri) ->
+ (* XXX : we only try the first match *)
+ GrafiteAst.Ident_alias (_,uri)::_ ->
NotationPt.NRefPattern (NReference.reference_of_string uri)
| _ -> assert false
with Not_found ->
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
+ (* FIXME : we are forgetting the interpretation of the Id
+ * but is this useful anymore?!?!? *)
DisambiguateTypes.Id name,
GrafiteAst.Ident_alias (name,NReference.string_of_reference u)
) references) refs)
projects / helm.git / blobdiff