-let foo () =
- refine_thing metasenv subst context uri
- ~use_coercions cic_thing expty ugraph ~localization_tbl
-in refine_profiler.HExtlib.profile foo ()
- with
- | Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg))
- | Invalid_choice loc_msg -> Ko loc_msg
- in
- (* (4) build all possible interpretations *)
- let (@@) (l1,l2,l3) (l1',l2',l3') = l1@l1', l2@l2', l3@l3' in
- (* aux returns triples Ok/Uncertain/Ko *)
- (* rem_dom is the concatenation of all the remainin domains *)
- let rec aux aliases diff lookup_in_todo_dom todo_dom rem_dom =
- debug_print (lazy ("ZZZ: " ^ string_of_domain todo_dom));
- match todo_dom with
- | [] ->
- assert (lookup_in_todo_dom = None);
- (match test_env aliases rem_dom base_univ with
- | Ok (thing, metasenv,subst,new_univ) ->
- [ aliases, diff, metasenv, subst, thing, new_univ ], [], []
- | Ko loc_msg -> [],[],[aliases,diff,loc_msg,true]
- | Uncertain loc_msg ->
- [],[aliases,diff,loc_msg],[])
- | Node (locs,item,inner_dom) :: remaining_dom ->
- debug_print (lazy (sprintf "CHOOSED ITEM: %s"
- (string_of_domain_item item)));
- let choices =
- match lookup_in_todo_dom with
- None -> lookup_choices item
- | Some choices -> choices in
- match choices with
- [] ->
- [], [],
- [aliases, diff,
- (lazy (List.hd locs,
- "No choices for " ^ string_of_domain_item item)),
- true]
-(*
- | [codomain_item] ->
- (* just one choice. We perform a one-step look-up and
- if the next set of choices is also a singleton we
- skip this refinement step *)
- debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));
- let new_env = Environment.add item codomain_item aliases in
- let new_diff = (item,codomain_item)::diff in
- let lookup_in_todo_dom,next_choice_is_single =
- match remaining_dom with
- [] -> None,false
- | (_,he)::_ ->
- let choices = lookup_choices he in
- Some choices,List.length choices = 1
- in
- if next_choice_is_single then
- aux new_env new_diff lookup_in_todo_dom remaining_dom
- base_univ
- else
- (match test_env new_env remaining_dom base_univ with
- | Ok (thing, metasenv),new_univ ->
- (match remaining_dom with
- | [] ->
- [ new_env, new_diff, metasenv, thing, new_univ ], []
- | _ ->
- aux new_env new_diff lookup_in_todo_dom
- remaining_dom new_univ)
- | Uncertain (loc,msg),new_univ ->
- (match remaining_dom with
- | [] -> [], [new_env,new_diff,loc,msg,true]
- | _ ->
- aux new_env new_diff lookup_in_todo_dom
- remaining_dom new_univ)
- | Ko (loc,msg),_ -> [], [new_env,new_diff,loc,msg,true])
-*)
- | _::_ ->
- let mark_not_significant failures =
- List.map
- (fun (env, diff, loc_msg, _b) ->
- env, diff, loc_msg, false)
- failures in
- let classify_errors ((ok_l,uncertain_l,error_l) as outcome) =
- if ok_l <> [] || uncertain_l <> [] then
- ok_l,uncertain_l,mark_not_significant error_l
- else
- outcome in
- let rec filter = function
- | [] -> [],[],[]
- | codomain_item :: tl ->
- (*debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));*)
- let new_env = Environment.add item codomain_item aliases in
- let new_diff = (item,codomain_item)::diff in
- (match
- test_env new_env
- (inner_dom@remaining_dom@rem_dom) base_univ
- with
- | Ok (thing, metasenv,subst,new_univ) ->
-(* prerr_endline "OK"; *)
- let res =
- (match inner_dom with
- | [] ->
- [new_env,new_diff,metasenv,subst,thing,new_univ],
- [], []
- | _ ->
- aux new_env new_diff None inner_dom
- (remaining_dom@rem_dom)
- )
- in
- res @@ filter tl
- | Uncertain loc_msg ->
-(* prerr_endline ("UNCERTAIN"); *)
- let res =
- (match inner_dom with
- | [] -> [],[new_env,new_diff,loc_msg],[]
- | _ ->
- aux new_env new_diff None inner_dom
- (remaining_dom@rem_dom)
- )
- in
- res @@ filter tl
- | Ko loc_msg ->
-(* prerr_endline "KO"; *)
- let res = [],[],[new_env,new_diff,loc_msg,true] in
- res @@ filter tl)
- in
- let ok_l,uncertain_l,error_l =
- classify_errors (filter choices)
- in
- let res_after_ok_l =
- List.fold_right
- (fun (env,diff,_,_,_,_) res ->
- aux env diff None remaining_dom rem_dom @@ res
- ) ok_l ([],[],error_l)
- in
- List.fold_right
- (fun (env,diff,_) res ->
- aux env diff None remaining_dom rem_dom @@ res
- ) uncertain_l res_after_ok_l
+ let href0 = HExtlib.map_option NReference.reference_of_string href0
+ in ctx (Ast.Pattern (id0,href0,pl))),
+ mk_ident s href)::auxpatt [] pl
+;;
+
+ (* this function is used to get the children of a given node, together with
+ * their context and their location
+ * contexts are expressed in the form of functions Ast -> Ast *)
+(* split : location -> ('term -> 'a) -> 'term -> (('term -> 'a) * 'term * loc) list *)
+let rec split loc ctx t =
+ let loc_of_attr oldloc = function
+ | `Loc l -> l
+ | _ -> oldloc
+ in
+ 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 Some (loc,err)
+ | _ -> 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