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_disamb_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 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"
| Ko of (Stdpp.location * string) Lazy.t
| Uncertain of (Stdpp.location * string) Lazy.t
+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 *)
) [] defs
in
defs_dom @ where_dom
- | Ast.Ident (name, x) ->
- let x = match x with
+ | Ast.Ident (name, _x) ->
+ (* let x = match x with
| `Uri u -> Some u
- | _ -> None
- in
+ | _ -> None
+ in *)
(try
(* the next line can raise Not_found *)
ignore(find_in_context name context); []
;;
(* this function is used to get the children of a given node, together with
- * their context
+ * their context and their location
* contexts are expressed in the form of functions Ast -> Ast *)
-(* split : ('term -> 'a) -> 'term -> (('term -> 'a) * 'term) list *)
-let rec split ctx = function
+(* 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]
- | Ast.Appl tl -> list_split (*split*) (fun ctx0 t0 -> [ctx0,t0]) (fun x -> ctx (Ast.Appl x)) [] tl
+ [(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]
+ [ (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
- ;(fun v -> ctx (Ast.Binder (k,n',v))),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
- ((fun x -> ctx (Ast.Case (x,ity,outty,pl))),t)::
+ 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
- ; (fun x -> ctx (Ast.Cast (u,x))),v ]
+ [] 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
- ; (fun x -> ctx (Ast.LetIn (n',u,x))), 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
- ; (fun x -> ctx (Ast.LetIn (n',x,v))), u
- ; (fun x -> ctx (Ast.LetIn (n',u,x))), 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_split letrecaux_split (fun x -> ctx (Ast.LetRec(k,x,where))) [] funs
+ 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) list
- * returns all the possible top-level (ctx,t) for its input *)
+(* 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 as hd)::tl ->
+ | (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)
List.iter (fun (ctx',t') -> prerr_endline ("-- subnode " ^
(pp_term t'))) t0';
aux (tl@t0')) *)
- let t0' = split ctx0 t0 in
+ 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_split var_split (fun x -> Ast.Inductive (x,itl)) [] ls@
- list_split ity_split (fun x -> Ast.Inductive (ls,x)) [] 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]
+ [(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
- ;(fun x -> Ast.Theorem (flav,n,ty,Some x,p)), bo]
+ [(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_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
+ 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]) ;;
+let bfvisit = bfvisit (fun t -> [(fun x -> x),t,Stdpp.dummy_loc]) ;;
let domain_item_of_ast = function
| Ast.Ident (id,_) -> DisambiguateTypes.Id id
| _ -> 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
~use_coercions cic_thing expty ugraph ~localization_tbl
in match (refine_profiler.HExtlib.profile foo ()) with
| Ko x ->
- let _,err = Lazy.force x in
+ let loc,err = Lazy.force x in
debug_print (lazy ("test_interpr error: " ^ err));
- false
- | _ -> true
+ 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 _ -> false
- | _ -> true
+ | 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 =
+ ~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
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)) choices
+ List.map (fun t0 -> ctx (ast_of_alias_spec t t0), t0) choices
with
| Not_found -> []
in
match ts with
- | [] -> None
- | t0 :: tl ->
- debug_print (lazy ("disambiguate_list: t0 = " ^ pp_thing t0));
+ | [] -> [], errors
+ | _ ->
+ (* debug_print (lazy ("disambiguate_list: t0 = " ^ pp_thing t0)); *)
let is_ambiguous = function
| Ast.Ident (_,`Ambiguous)
| Ast.Num (_,None)
| Ast.Symbol (sym,_) -> "SYM " ^ sym
| _ -> "ERROR!"
in
- (* 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)
- | Some (ctx, 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
- debug_print (lazy "-- possible instances:");
- List.iter
- (fun u0 -> debug_print (lazy ("-- instance: " ^ (pp_thing u0)))) instances;
- (* perforate ambiguous subterms and test refinement *)
- debug_print (lazy "-- survivors:");
- let survivors = List.filter test_interpr instances in
- List.iter
- (fun u0 -> debug_print (lazy ("-- survivor: " ^ (pp_thing u0)))) survivors;
- disambiguate_list (survivors@tl)
+ 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
+ ~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)
=
~env ~universe ~uri ~interpretate_thing ~refine_thing ~ugraph:base_univ ~mk_localization_tbl
in
(* real function *)
- let rec aux tl =
- match disambiguate_list ~mk_localization_tbl ~context ~metasenv ~subst
+ 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 with
- | None -> []
- | Some (t,tl') -> t::aux tl'
+ ~pp_term tl []
in
-
let refine t =
let localization_tbl = mk_localization_tbl 503 in
debug_print (lazy "before 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 ->
- let _,err = Lazy.force x in
+ | Uncertain x | Ko x ->
+ let loc,err = Lazy.force x in
debug_print (lazy ("refinement uncertain after disambiguation: " ^ err));
- assert false
- | _ -> assert false
+ raise (NoWellTypedInterpretation (loc,err))
in
- if not (test_interpr thing) then
- (debug_print (lazy ("preliminary test fail: " ^ pp_thing thing));
- raise (NoWellTypedInterpretation (0,[])))
- else
- let res = aux [thing] in
- let res =
- HExtlib.filter_map (fun t ->
- try Some (refine t)
- with _ ->
- debug_print (lazy ("can't interpretate/refine " ^ (pp_thing t)));None) res
+ 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
- | [] -> raise (NoWellTypedInterpretation (0,[]))
- | [t] -> res,false
- | _ ->
- let choices = List.map (fun (t,_,_,_,_) -> pp_thing t) res in
- let user_choice = interactive_ast_choice choices in
- [ List.nth res user_choice ], true
- (* let pp_thing (t,_,_,_,_,_) = prerr_endline ("interpretation: " ^ (pp_thing t)) in
- List.iter pp_thing res; res,true *)
+ (match res with
+ | [] -> prerr_endline ((string_of_int (List.length errors)) ^ " error frames");Disamb_failure errors
+ | _ -> Disamb_success res)
;;
projects / helm.git / blobdiff