+;;*)
+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