+ match t with
+ | Ast.AttributedTerm (attr,t) ->
+ [(fun x -> ctx (Ast.AttributedTerm(attr,x))),t, loc_of_attr loc attr]
+ | Ast.Appl tl -> list_split (*split*) (fun ctx0 t0 -> [ctx0,t0,loc]) (fun x -> ctx (Ast.Appl x)) [] tl
+ | Ast.Binder (k,((n,None) as n'),body) ->
+ [ (fun v -> ctx (Ast.Binder (k,n',v))),body, loc]
+ | Ast.Binder (k,((n,Some ty) as n'),body) ->
+ [(fun v -> ctx (Ast.Binder (k,(n,Some v),body))), ty, loc
+ ;(fun v -> ctx (Ast.Binder (k,n',v))),body, loc]
+ | Ast.Case (t,ity,outty,pl) ->
+ let outty_split = match outty with
+ | None -> []
+ | Some u -> [(fun x -> ctx (Ast.Case (t,ity,Some x,pl))),u]
+ in
+ List.map (fun (a,b) -> a,b,loc)
+ (((fun x -> ctx (Ast.Case (x,ity,outty,pl))),t)::
+ outty_split@list_split
+ (fun ctx0 (p,x) ->
+ ((fun y -> ctx0 (p,y)),x)::pattern_split
+ (fun y -> ctx0 (y,x)) p) (fun x -> ctx (Ast.Case(t,ity,outty,x)))
+ [] pl)
+ | Ast.Cast (u,v) -> [ (fun x -> ctx (Ast.Cast (x,v))),u,loc
+ ; (fun x -> ctx (Ast.Cast (u,x))),v,loc ]
+ | Ast.LetIn ((n,None) as n',u,v) ->
+ [ (fun x -> ctx (Ast.LetIn (n',x,v))), u,loc
+ ; (fun x -> ctx (Ast.LetIn (n',u,x))), v,loc ]
+ | Ast.LetIn ((n,Some t) as n',u,v) ->
+ [ (fun x -> ctx (Ast.LetIn ((n,Some x),u,v))), t,loc
+ ; (fun x -> ctx (Ast.LetIn (n',x,v))), u, loc
+ ; (fun x -> ctx (Ast.LetIn (n',u,x))), v, loc ]
+ | Ast.LetRec (k,funs,where) -> (* we do not use where any more?? *)
+ List.map (fun (a,b) -> a,b,loc)
+ (list_split letrecaux_split (fun x -> ctx (Ast.LetRec(k,x,where))) [] funs)
+ | _ -> [] (* leaves *)
+;;
+
+type 'ast marked_ast =
+ (NotationPt.term -> 'ast) * NotationPt.term * Stdpp.location
+
+(* top_split : 'a -> ((term -> 'a) * term * loc) list
+ * such that it returns all the possible top-level (ctx,t,dummy_loc) for its input *)
+let bfvisit ~pp_term top_split test t =
+ let rec aux = function
+ | [] -> None
+ | (ctx0,t0,loc as hd)::tl ->
+(* prerr_endline ("ok! length tl = " ^ string_of_int (List.length tl)); *)
+ 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:");
+ let t0' = split ctx0 t0 in
+ List.iter (fun (ctx',t') -> prerr_endline ("-- subnode " ^
+ (pp_term t'))) t0';
+ aux (tl@t0')) *)
+ let t0' = split loc ctx0 t0 in
+ aux (tl@t0')
+ (* in aux [(fun x -> x),t] *)
+ in aux (top_split t)
+;;
+
+let obj_split (o:Ast.term Ast.obj) = match o with
+ | Ast.Inductive (ls,itl) ->
+ List.map (fun (a,b) -> a,b,Stdpp.dummy_loc)
+ (list_split var_split (fun x -> Ast.Inductive (x,itl)) [] ls@
+ list_split ity_split (fun x -> Ast.Inductive (ls,x)) [] itl)
+ | Ast.Theorem (flav,n,ty,None,p) ->
+ [(fun x -> Ast.Theorem (flav,n,x,None,p)), ty, Stdpp.dummy_loc]
+ | Ast.Theorem (flav,n,ty,(Some bo as bo'),p) ->
+ [(fun x -> Ast.Theorem (flav,n,x,bo',p)), ty, Stdpp.dummy_loc
+ ;(fun x -> Ast.Theorem (flav,n,ty,Some x,p)), bo, Stdpp.dummy_loc]
+ | Ast.Record (ls,n,ty,fl) ->
+ List.map (fun (a,b) -> a,b,Stdpp.dummy_loc)
+ (list_split var_split (fun x -> Ast.Record (x,n,ty,fl)) [] ls@
+ [(fun x -> Ast.Record (ls,n,x,fl)),ty]@
+ list_split field_split (fun x -> Ast.Record (ls,n,ty,x)) [] fl)
+;;
+
+let bfvisit_obj = bfvisit obj_split;;
+
+let bfvisit = bfvisit (fun t -> [(fun x -> x),t,Stdpp.dummy_loc]) ;;
+
+let domain_item_of_ast = function
+ | Ast.Ident (id,_) -> DisambiguateTypes.Id id
+ | Ast.Symbol (sym,_) -> DisambiguateTypes.Symbol sym
+ | Ast.Num (n,_) -> DisambiguateTypes.Num
+ | Ast.Case(_,Some (ityname,_),_,_) -> DisambiguateTypes.Id ityname
+ | _ -> assert false
+;;
+
+let ast_of_alias_spec t alias = match (t,alias) with
+ | Ast.Ident _, GrafiteAst.Ident_alias (id,uri) -> Ast.Ident(id,`Uri uri)
+ | Ast.Case (t,_,oty,pl), GrafiteAst.Ident_alias (id,uri) ->
+ Ast.Case (t,Some (id,Some (NReference.reference_of_string uri)),oty,pl)
+ | _, GrafiteAst.Symbol_alias (sym,uri,desc) -> Ast.Symbol (sym,Some (uri,desc))
+ | Ast.Num(m,_), GrafiteAst.Number_alias (uri,desc) -> Ast.Num(m,Some (uri,desc))
+ | _ -> assert false
+;;
+
+(* returns an optional (loc*string):
+ * - None means success (the ast is refinable)
+ * - Some (loc,err) means refinement has failed with error err at location loc
+ *)
+let test_interpr ~context ~metasenv ~subst ~use_coercions ~expty ~env ~universe ~uri
+ ~interpretate_thing ~refine_thing ~ugraph ~mk_localization_tbl t =
+ try
+ let localization_tbl = mk_localization_tbl 503 in
+ let cic_thing =
+ interpretate_thing ~context ~env ~universe
+ ~uri ~is_path:false t ~localization_tbl
+ in
+ let foo () =
+ refine_thing metasenv subst context uri
+ ~use_coercions cic_thing expty ugraph ~localization_tbl
+ in match (refine_profiler.HExtlib.profile foo ()) with
+ | Ko x ->
+ let loc,err = Lazy.force x in
+ debug_print (lazy ("test_interpr error: " ^ err));
+ Some (loc,err)
+ | _ -> None
+ with
+ (*| Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg))
+ | Invalid_choice loc_msg -> Ko loc_msg*)
+ | Invalid_choice x ->
+ let loc,err = Lazy.force x in
+ debug_print (lazy ("test_interpr invalid choice: " ^ err));
+ Some (loc,err)
+ | e -> debug_print (lazy ("uncaught error: "^ Printexc.to_string e));None
+;;
+
+exception Not_ambiguous;;
+
+let rec disambiguate_list
+ ~context ~metasenv ~subst ~use_coercions ~expty ~env ~uri ~interpretate_thing
+ ~refine_thing ~ugraph ~visit ~universe ~mk_localization_tbl ~pp_thing ~pp_term
+ ts errors =
+
+ let disambiguate_list =
+ disambiguate_list ~context ~metasenv ~subst ~use_coercions ~expty ~env ~uri
+ ~interpretate_thing ~refine_thing ~ugraph ~visit ~universe
+ ~mk_localization_tbl ~pp_thing ~pp_term
+ in
+ let test_interpr = test_interpr ~context ~metasenv ~subst ~use_coercions ~expty
+ ~env ~universe ~uri ~interpretate_thing ~refine_thing ~ugraph ~mk_localization_tbl