module Ast = NotationPt
-(* the integer is an offset to be added to each location *)
-exception Ambiguous_input
-(* the integer is an offset to be added to each location *)
-exception NoWellTypedInterpretation of
- int *
- ((Stdpp.location list * string * string) list *
- (DisambiguateTypes.domain_item * string) list *
- (Stdpp.location * string) Lazy.t * bool) list
+exception NoWellTypedInterpretation of (Stdpp.location * string)
+
exception PathNotWellFormed
(** raised when an environment is not enough informative to decide *)
type domain = domain_tree list
and domain_tree = Node of Stdpp.location list * domain_item * domain
+(*
let mono_uris_callback ~selection_mode ?ok
?(enable_button_for_non_vars = true) ~title ~msg ~id =
if Helm_registry.get_opt_default Helm_registry.get_bool ~default:true
else
raise Ambiguous_input
-let mono_interp_callback _ _ _ = raise Ambiguous_input
+let mono_interp_callback _ _ _ = assert false
+let mono_disamb_callback _ = assert false
let _choose_uris_callback = ref mono_uris_callback
let _choose_interp_callback = ref mono_interp_callback
+let _choose_disamb_callback = ref mono_disamb_callback
let set_choose_uris_callback f = _choose_uris_callback := f
let set_choose_interp_callback f = _choose_interp_callback := f
+let set_choose_disamb_callback f = _choose_disamb_callback := f
let interactive_user_uri_choice = !_choose_uris_callback
let interactive_interpretation_choice interp = !_choose_interp_callback interp
+let interactive_ast_choice interp = !_choose_disamb_callback interp
+*)
+
let input_or_locate_uri ~(title:string) ?id () = None
(* Zack: I try to avoid using this callback. I therefore assume that
* the presence of an identifier that can't be resolved via "locate"
let choices_avg = ref 0.
*)
-let descr_of_domain_item = function
- | Id s -> s
- | Symbol (s, _) -> s
- | Num i -> string_of_int i
-
type ('term,'metasenv,'subst,'graph) test_result =
| Ok of 'term * 'metasenv * 'subst * 'graph
| Ko of (Stdpp.location * string) Lazy.t
| Uncertain of (Stdpp.location * string) Lazy.t
-let resolve ~env ~mk_choice (item: domain_item) arg =
+type ('alias,'ast_thing,'metasenv,'subst,'thing,'ugraph) disamb_result =
+ | Disamb_success of ('ast_thing * 'metasenv * 'subst * 'thing * 'ugraph) list
+ (* each element of this list is a list of partially instantiated asts,
+ * sharing the last instantiated node, together with the location of that
+ * node; each ast is associated with the actual instantiation of the node,
+ * the refinement error, and the location at which refinement fails *)
+ | Disamb_failure of
+ (('ast_thing * 'alias option * Stdpp.location * string) list * Stdpp.location) list
+
+let resolve ~env ~universe ~mk_choice item interpr arg =
+ (* let _ = (mk_choice : (GrafiteAst.alias_spec -> 'b
+ DisambiguateTypes.codomain_item)) in *)
try
- match snd (mk_choice (Environment.find item env)), arg with
+ let interpr =
+ match interpr with
+ | None -> InterprEnv.find item env
+ | Some i -> i
+ in
+ (* one, and only one interpretation is returned (or Not_found) *)
+ (*if (List.length interpr <> 1)
+ then (let strinterpr =
+ String.concat ", " (List.map GrafiteAst.description_of_alias interpr) in
+ prerr_endline (Printf.sprintf "choices for %s: %s"
+ (DisambiguateTypes.string_of_domain_item item) strinterpr);
+ assert false)
+ else
+ let interpr = List.hd interpr in*)
+ match snd (mk_choice interpr), arg with
`Num_interp f, `Num_arg n -> f n
| `Sym_interp f, `Args l -> f l
| `Sym_interp f, `Num_arg n -> (* Implicit number! *) f []
| _,_ -> assert false
with Not_found ->
- failwith ("Domain item not found: " ^
- (DisambiguateTypes.string_of_domain_item item))
+ failwith (": InterprEnv.find failed")
(* TODO move it to Cic *)
let find_in_context name context =
let string_of_name =
function
- | Ast.Ident (n, None) -> Some n
+ | Ast.Ident (n, _) -> Some n
| _ -> assert false
;;
+(* XXX: assuming the domain is composed of uninterpreted items only *)
let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
| Ast.AttributedTerm (`Loc loc, term) ->
domain_of_term ~loc ~context term
| Ast.AttributedTerm (_, term) ->
domain_of_term ~loc ~context term
- | Ast.Symbol (symbol, instance) ->
- [ Node ([loc], Symbol (symbol, instance), []) ]
+ | Ast.Symbol (name, attr) ->
+ (match attr with
+ | None -> [ Node ([loc], Symbol name, []) ]
+ | _ -> [])
(* to be kept in sync with Ast.Appl (Ast.Symbol ...) *)
- | Ast.Appl (Ast.Symbol (symbol, instance) as hd :: args)
- | Ast.Appl (Ast.AttributedTerm (_,Ast.Symbol (symbol, instance)) as hd :: args)
+ | Ast.Appl (Ast.Symbol (name, None) as hd :: args)
+ | Ast.Appl (Ast.AttributedTerm (_,Ast.Symbol (name,None)) as hd :: args)
->
let args_dom =
List.fold_right
Ast.AttributedTerm (`Loc loc,_) -> loc
| _ -> loc
in
- [ Node ([loc], Symbol (symbol, instance), args_dom) ]
- | Ast.Appl (Ast.Ident (name, subst) as hd :: args)
- | Ast.Appl (Ast.AttributedTerm (_,Ast.Ident (name, subst)) as hd :: args) ->
+ [ Node ([loc], Symbol name, args_dom) ]
+ | Ast.Appl (Ast.Ident (id,`Ambiguous) as hd :: args)
+ | Ast.Appl (Ast.AttributedTerm (_,Ast.Ident (id,`Ambiguous)) as hd :: args) ->
let args_dom =
List.fold_right
(fun term acc -> domain_of_term ~loc ~context term @ acc)
in
(try
(* the next line can raise Not_found *)
- ignore(find_in_context name context);
- if subst <> None then
- Ast.fail loc "Explicit substitutions not allowed here"
- else
+ ignore(find_in_context id context);
args_dom
with Not_found ->
- (match subst with
- | None -> [ Node ([loc], Id name, args_dom) ]
- | Some subst ->
- let terms =
- List.fold_left
- (fun dom (_, term) ->
- let dom' = domain_of_term ~loc ~context term in
- dom @ dom')
- [] subst in
- [ Node ([loc], Id name, terms @ args_dom) ]))
+ [ Node ([loc], Id id, args_dom) ] )
| Ast.Appl terms ->
List.fold_right
(fun term acc -> domain_of_term ~loc ~context term @ acc)
domain_of_term ~loc
~context:(string_of_name var :: context) body in
(match kind with
- | `Exists -> [ Node ([loc], Symbol ("exists", 0), (type_dom @ body_dom)) ]
+ | `Exists -> [ Node ([loc], Symbol "exists", (type_dom @ body_dom)) ]
| _ -> type_dom @ body_dom)
| Ast.Case (term, indty_ident, outtype, branches) ->
let term_dom = domain_of_term ~loc ~context term in
let outtype_dom = domain_of_term_option ~loc ~context outtype in
let rec get_first_constructor = function
| [] -> []
- | (Ast.Pattern (head, _, _), _) :: _ -> [ Node ([loc], Id head, []) ]
+ | (Ast.Pattern (head, Some r, _), _) :: _ -> []
+ (* [ Node ([loc], Id (head,Some (NReference.string_of_reference r)), []) ] *)
+ | (Ast.Pattern (head, None, _), _) :: _ ->
+ [ Node ([loc], Id head, []) ]
| _ :: tl -> get_first_constructor tl in
let do_branch =
function
List.fold_left (fun dom branch -> dom @ do_branch branch) [] branches in
(match indty_ident with
| None -> get_first_constructor branches
- | Some (ident, _) -> [ Node ([loc], Id ident, []) ])
+ | Some (ident, None) -> [ Node ([loc], Id ident , []) ]
+ | Some (ident, Some r) -> [])
+ (* [ Node ([loc], Id (ident,Some (NReference.string_of_reference r)), []) ]) *)
@ term_dom @ outtype_dom @ branches_dom
| Ast.Cast (term, ty) ->
let term_dom = domain_of_term ~loc ~context term in
) [] defs
in
defs_dom @ where_dom
- | Ast.Ident (name, subst) ->
+ | Ast.Ident (name, _x) ->
+ (* let x = match x with
+ | `Uri u -> Some u
+ | _ -> None
+ in *)
(try
(* the next line can raise Not_found *)
- ignore(find_in_context name context);
- if subst <> None then
- Ast.fail loc "Explicit substitutions not allowed here"
- else
- []
+ ignore(find_in_context name context); []
with Not_found ->
+ (*
(match subst with
| None -> [ Node ([loc], Id name, []) ]
| Some subst ->
let dom' = domain_of_term ~loc ~context term in
dom @ dom')
[] subst in
- [ Node ([loc], Id name, terms) ]))
- | Ast.Uri _ -> []
+ [ Node ([loc], Id name, terms) ]))*)
+ [ Node ([loc], Id name, []) ])
| Ast.NRef _ -> []
| Ast.NCic _ -> []
| Ast.Implicit _ -> []
- | Ast.Num (num, i) -> [ Node ([loc], Num i, []) ]
+ | Ast.Num (num, i) -> [ Node ([loc], Num, []) ]
| Ast.Meta (index, local_context) ->
List.fold_left
(fun dom term -> dom @ domain_of_term_option ~loc ~context term)
uniq_domain (domain_of_obj ~context obj)
(* dom1 \ dom2 *)
+(* XXX: possibly should take into account locs? *)
let domain_diff dom1 dom2 =
(* let domain_diff = Domain.diff *)
let is_in_dom2 elt =
List.exists
(function
- | Symbol (symb, 0) ->
+ | Symbol symb ->
(match elt with
- Symbol (symb',_) when symb = symb' -> true
+ Symbol symb' when symb = symb' -> true
| _ -> false)
- | Num i ->
+ | Num ->
(match elt with
- Num _ -> true
+ Num -> true
| _ -> false)
| item -> elt = item
) dom2
let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
-let disambiguate_thing
- ~context ~metasenv ~subst ~use_coercions
- ~string_context_of_context
- ~initial_ugraph:base_univ ~expty
- ~mk_implicit ~description_of_alias ~fix_instance
- ~aliases ~universe ~lookup_in_library
- ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
- ~mk_localization_tbl
- (thing_txt,thing_txt_prefix_len,thing)
-=
- debug_print (lazy "DISAMBIGUATE INPUT");
- debug_print (lazy ("TERM IS: " ^ (pp_thing thing)));
- let thing_dom =
- domain_of_thing ~context:(string_context_of_context context) thing in
- debug_print
- (lazy (sprintf "DISAMBIGUATION DOMAIN: %s"(string_of_domain thing_dom)));
- let current_dom =
- Environment.fold (fun item _ dom -> item :: dom) aliases [] in
- let todo_dom = domain_diff thing_dom current_dom in
- debug_print
- (lazy (sprintf "DISAMBIGUATION DOMAIN AFTER DIFF: %s"(string_of_domain todo_dom)));
- (* (2) lookup function for any item (Id/Symbol/Num) *)
- let lookup_choices =
- fun item ->
- match universe with
- | None ->
- lookup_in_library
- interactive_user_uri_choice
- input_or_locate_uri item
- | Some e ->
- (try
- fix_instance item (Environment.find item e)
- with Not_found -> [])
- in
+(* generic function lifting splitting from type T to type (T list) *)
+let rec list_split item_split ctx pre post =
+ match post with
+ | [] -> []
+ | x :: post' ->
+ (item_split (fun v1 -> ctx (pre@v1::post')) x)@
+ list_split item_split ctx (pre@[x]) post'
+;;
- (* items with 1 choice are interpreted ASAP *)
- let aliases, todo_dom =
- let rec aux (aliases,acc) = function
- | [] -> aliases, acc
- | (Node (_, item,extra) as node) :: tl ->
- let choices = lookup_choices item in
- if List.length choices <> 1 then aux (aliases, acc@[node]) tl
- else
- let tl = tl @ extra in
- if Environment.mem item aliases then aux (aliases, acc) tl
- else aux (Environment.add item (List.hd choices) aliases, acc) tl
- in
- aux (aliases,[]) todo_dom
- in
+(* splits a 'term capture_variable *)
+let var_split ctx = function
+ | (_,None) -> []
+ | (v,Some ty) -> [(fun x -> ctx (v,Some x)),ty]
+;;
-(*
- (* <benchmark> *)
- let _ =
- if benchmark then begin
- let per_item_choices =
- List.map
- (fun dom_item ->
- try
- let len = List.length (lookup_choices dom_item) in
- debug_print (lazy (sprintf "BENCHMARK %s: %d"
- (string_of_domain_item dom_item) len));
- len
- with No_choices _ -> 0)
- thing_dom
- in
- max_refinements := List.fold_left ( * ) 1 per_item_choices;
- actual_refinements := 0;
- domain_size := List.length thing_dom;
- choices_avg :=
- (float_of_int !max_refinements) ** (1. /. float_of_int !domain_size)
- end
- in
- (* </benchmark> *)
-*)
+let ity_split ctx (n,isind,ty,cl) =
+ [(fun x -> ctx (n,isind,x,cl)),ty]@
+ list_split (fun ctx0 (v,ty) -> [(fun x -> ctx0 (v,x)),ty])
+ (fun x -> ctx (n,isind,ty,x)) [] cl
+;;
+
+let field_split ctx (n,ty,b,m) =
+ [(fun x -> ctx (n,x,b,m)),ty]
+;;
- (* (3) test an interpretation filling with meta uninterpreted identifiers
- *)
- let test_env aliases todo_dom ugraph =
- try
- let rec aux env = function
- | [] -> env
- | Node (_, item, l) :: tl ->
- let env =
- Environment.add item
- (mk_implicit
- (match item with | Id _ | Num _ -> true | Symbol _ -> false))
- env in
- aux (aux env l) tl in
- let filled_env = aux aliases todo_dom in
- let localization_tbl = mk_localization_tbl 503 in
- let cic_thing =
- interpretate_thing ~context ~env:filled_env
- ~uri ~is_path:false thing ~localization_tbl
+(* splits a defn. in a mutual LetRec block *)
+let letrecaux_split ctx (args,f,bo,n) =
+ list_split var_split (fun x -> ctx (x,f,bo,n)) [] args@
+ var_split (fun x -> ctx (args,x,bo,n)) f@
+ [(fun x -> ctx (args,f,x,n)),bo]
+;;
+
+let mk_ident s = function
+| None -> Ast.Ident (s,`Ambiguous)
+| Some u -> Ast.Ident (s,`Uri (NReference.string_of_reference u))
+;;
+
+(* splits a pattern (for case analysis) *)
+let pattern_split ctx = function
+ | Ast.Wildcard -> []
+ | Ast.Pattern (s,href,pl) ->
+ let rec auxpatt pre = function
+ | [] -> []
+ | (x,Some y as x')::post' ->
+ ((fun v -> ctx (Ast.Pattern (s,href,pre@(x,Some v)::post'))),y)
+ ::auxpatt (pre@[x']) post'
+ | (x,None as x')::post' -> auxpatt (pre@[x']) post'
+ in
+ ((fun x ->
+ let id0, href0 =
+ match x with
+ | Ast.Ident (id,`Ambiguous) -> id, None
+ | Ast.Ident (id,`Uri u) -> id, Some u
+ | _ -> assert false
in
-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
- let aux' aliases diff lookup_in_todo_dom todo_dom =
- if todo_dom = [] then
- aux aliases diff lookup_in_todo_dom todo_dom []
- else
- match test_env aliases todo_dom base_univ with
- | Ok _
- | Uncertain _ ->
- aux aliases diff lookup_in_todo_dom todo_dom []
- | Ko (loc_msg) -> [],[],[aliases,diff,loc_msg,true]
+ 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
in
+ let find_choices item =
+ let a2s = function
+ | GrafiteAst.Ident_alias (_id,uri) -> uri
+ | GrafiteAst.Symbol_alias (_id,_,desc) -> desc
+ | GrafiteAst.Number_alias (_,desc) -> desc
+ in
+ let d2s = function
+ | Id id
+ | Symbol id -> id
+ | Num -> "NUM"
+ in
let res =
- match aux' aliases [] None todo_dom with
- | [],uncertain,errors ->
- let errors =
- List.map
- (fun (env,diff,loc_msg) -> (env,diff,loc_msg,true)
- ) uncertain @ errors
- in
- let errors =
- List.map
- (fun (env,diff,loc_msg,significant) ->
- let env' =
- filter_map_domain
- (fun locs domain_item ->
- try
- let description =
- description_of_alias (Environment.find domain_item env)
- in
- Some (locs,descr_of_domain_item domain_item,description)
- with
- Not_found -> None)
- thing_dom
- in
- let diff= List.map (fun a,b -> a,description_of_alias b) diff in
- env',diff,loc_msg,significant
- ) errors
- in
- raise (NoWellTypedInterpretation (0,errors))
- | [_,diff,metasenv,subst,t,ugraph],_,_ ->
- debug_print (lazy "SINGLE INTERPRETATION");
- [diff,metasenv,subst,t,ugraph], false
- | l,_,_ ->
- debug_print
- (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l)));
- let choices =
- List.map
- (fun (env, _, _, _, _, _) ->
- map_domain
- (fun locs domain_item ->
- let description =
- description_of_alias (Environment.find domain_item env)
- in
- locs,descr_of_domain_item domain_item, description)
- thing_dom)
- l
- in
- let choosed =
- interactive_interpretation_choice
- thing_txt thing_txt_prefix_len choices
- in
- (List.map (fun n->let _,d,m,s,t,u= List.nth l n in d,m,s,t,u)
- choosed),
- true
+ Environment.find item universe
in
- res
+ debug_print (lazy (Printf.sprintf "choices for %s :\n%s"
+ (d2s item) (String.concat ", " (List.map a2s res))));
+ res
+ in
+
+ let get_instances ctx t =
+ try
+ let choices = find_choices (domain_item_of_ast t) in
+ List.map (fun t0 -> ctx (ast_of_alias_spec t t0), t0) choices
+ with
+ | Not_found -> []
+ in
+
+ match ts with
+ | [] -> [], errors
+ | _ ->
+ (* debug_print (lazy ("disambiguate_list: t0 = " ^ pp_thing t0)); *)
+ let is_ambiguous = function
+ | Ast.Ident (_,`Ambiguous)
+ | Ast.Num (_,None)
+ | Ast.Symbol (_,None) -> true
+ | Ast.Case (_,Some (ity,None),_,_) -> true
+ | _ -> false
+ in
+ let astpp = function
+ | Ast.Ident (id,_) -> "ID " ^ id
+ | Ast.Num _ -> "NUM"
+ | Ast.Symbol (sym,_) -> "SYM " ^ sym
+ | _ -> "ERROR!"
+ in
+ let process_ast t0 =
+ (* get first ambiguous subterm (or return disambiguated term) *)
+ match visit ~pp_term is_ambiguous t0 with
+ | None ->
+(* debug_print (lazy ("visit -- not ambiguous node:\n" ^ pp_thing
+ * t0));*)
+ (* Some (t0,tl), errors *)
+ raise Not_ambiguous
+ | Some (ctx, t, loc_t) ->
+ debug_print (lazy ("visit -- found ambiguous node: " ^ astpp t ^
+ "\nin " ^ pp_thing (ctx t)));
+ (* get possible instantiations of t *)
+ let instances = get_instances ctx t in
+ if instances = [] then
+ raise (NoWellTypedInterpretation (loc_t, "No choices for " ^ astpp t));
+ debug_print (lazy "-- possible instances:");
+(* List.iter
+ (fun u0 -> debug_print (lazy ("-- instance: " ^ (pp_thing u0))))
+instances; *)
+ (* perforate ambiguous subterms and test refinement *)
+ let instances = List.map (fun (x,a) -> (x,Some a),test_interpr x) instances in
+ debug_print (lazy "-- survivors:");
+ let survivors, defuncts =
+ List.partition (fun (_,o) -> o = None) instances in
+ survivors, (defuncts, loc_t)
+
+ in
+ try
+ let ts', new_errors = List.split (List.map process_ast ts) in
+ let ts' = List.map (fun ((t,_),_) -> t) (List.flatten ts') in
+ let errors' = match new_errors with
+ | (_,l)::_ ->
+ let ne' =
+ List.map (fun (a,b) -> a, HExtlib.unopt b)
+ (List.flatten (List.map fst new_errors)) in
+ let ne' = List.map (fun ((x,a),(l,e)) -> x,a,l,e) ne' in
+ (ne',l)::errors
+ | _ -> errors
+ in disambiguate_list ts' errors'
+ with Not_ambiguous -> ts,errors
+;;
+
+let disambiguate_thing
+ ~context ~metasenv ~subst ~use_coercions
+ ~string_context_of_context ~initial_ugraph:base_univ
+ ~expty ~mk_implicit ~description_of_alias
+ ~fix_instance ~aliases ~universe
+ ~lookup_in_library ~uri ~pp_thing ~pp_term
+ ~domain_of_thing ~interpretate_thing ~refine_thing
+ ~visit ~mk_localization_tbl
+ (thing_txt,thing_txt_prefix_len,thing)
+=
+ let env = aliases in
+
+ let test_interpr = test_interpr ~context ~metasenv ~subst ~use_coercions ~expty
+ ~env ~universe ~uri ~interpretate_thing ~refine_thing ~ugraph:base_univ ~mk_localization_tbl
+ in
+(* real function *)
+ let aux tl =
+ disambiguate_list ~mk_localization_tbl ~context ~metasenv ~subst
+ ~interpretate_thing ~refine_thing ~ugraph:base_univ ~visit
+ ~use_coercions ~expty ~uri ~env ~universe ~pp_thing
+ ~pp_term tl []
+ in
+ let refine t =
+ let localization_tbl = mk_localization_tbl 503 in
+ debug_print (lazy "before interpretate_thing");
+ let t' =
+ interpretate_thing ~context ~env ~universe ~uri ~is_path:false t ~localization_tbl
+ in
+ debug_print (lazy "after interpretate_thing");
+ match refine_thing metasenv subst context uri ~use_coercions t' expty
+ base_univ ~localization_tbl with
+ | Ok (t',m',s',u') -> t,m',s',t',u'
+ | Uncertain x | Ko x ->
+ let loc,err = Lazy.force x in
+ debug_print (lazy ("refinement uncertain after disambiguation: " ^ err));
+ raise (NoWellTypedInterpretation (loc,err))
+ in
+ match (test_interpr thing) with
+ | Some (loc,err) ->
+ debug_print (lazy ("preliminary test fail: " ^ pp_thing thing));
+ Disamb_failure ([[thing,None,loc,err],loc])
+ | None ->
+ let res,errors = aux [thing] in
+ let res,inner_errors =
+ List.split
+ (List.map (fun t ->
+ try (Some (refine t), None)
+ (* this error is actually a singleton *)
+ with NoWellTypedInterpretation loc_err ->
+ debug_print (lazy ("can't interpretate/refine " ^ (pp_thing t)));
+ None, Some loc_err) res) in
+ let res = HExtlib.filter_map (fun x -> x) res in
+ let inner_errors =
+ HExtlib.filter_map
+ (function Some (loc,err) -> Some (thing,None,loc,err) | None -> None)
+ inner_errors
+ in
+ let errors =
+ if inner_errors <> [] then (inner_errors,Stdpp.dummy_loc)::errors
+ else errors
+ in
+ (match res with
+ | [] -> prerr_endline ((string_of_int (List.length errors)) ^ " error frames");Disamb_failure errors
+ | _ -> Disamb_success res)
+;;
+
projects / helm.git / blobdiff