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 *)
+(* hard errors, spurious errors *)
exception NoWellTypedInterpretation of
- int *
- ((Stdpp.location list * string * string) list *
- (DisambiguateTypes.domain_item * string) list *
- (Stdpp.location * string) Lazy.t * bool) list
+ ((Stdpp.location * string) list *
+ (Stdpp.location * string) list)
+
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"
| 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
+ (* hard errors, spurious errors *)
+ (('ast_thing * 'alias option * Stdpp.location * string) list * Stdpp.location) list *
+ (('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 =
| _ -> 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 (name, attr) ->
- [ Node ([loc], 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 (name, attr) as hd :: args)
- | Ast.Appl (Ast.AttributedTerm (_,Ast.Symbol (name,attr)) 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 (name,attr), args_dom) ]
- | Ast.Appl (Ast.Ident (id,uri) as hd :: args)
- | Ast.Appl (Ast.AttributedTerm (_,Ast.Ident (id,uri)) as hd :: args) ->
- let uri = match uri with
- | `Uri u -> Some u
- | _ -> None
- in
+ [ 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)
ignore(find_in_context id context);
args_dom
with Not_found ->
- [ Node ([loc], Id (id,uri), 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",None), (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, Some r, _), _) :: _ ->
- [ Node ([loc], Id (head,Some (NReference.string_of_reference r)), []) ]
+ | (Ast.Pattern (head, Some r, _), _) :: _ -> []
+ (* [ Node ([loc], Id (head,Some (NReference.string_of_reference r)), []) ] *)
| (Ast.Pattern (head, None, _), _) :: _ ->
- [ Node ([loc], Id (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, None) -> [ Node ([loc], Id (ident,None) , []) ]
- | Some (ident, Some r) ->
- [ Node ([loc], Id (ident,Some (NReference.string_of_reference r)), []) ])
+ | 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, 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); []
dom @ dom')
[] subst in
[ Node ([loc], Id name, terms) ]))*)
- [ Node ([loc], Id (name,x), []) ])
+ [ 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,None) ->
+ | Symbol symb ->
(match elt with
- Symbol (symb',_) when symb = symb' -> true
+ Symbol symb' when symb = symb' -> true
| _ -> false)
- | Num _ ->
+ | Num ->
(match elt with
- Num _ -> true
+ Num -> true
| _ -> false)
| item -> elt = item
) dom2
[(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 -> []
((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 auxpatt [] pl
+ 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 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
+ * 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 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)); *)
- prerr_endline ("t0 = " ^ pp_term t0);
- if test t0 then (prerr_endline "caso 1"; Some hd)
+ debug_print (lazy ("visiting t0 = " ^ pp_term t0));
+ if test t0 then (debug_print (lazy "t0 is ambiguous"); Some hd)
else
- let t0' = split ctx0 t0 in
- (prerr_endline ("caso 2: length t0' = " ^ string_of_int
- (List.length t0')); aux (tl@t0' (*split ctx0 t0*)))
+ (*
+ (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_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 rec initialize_ast (* ~aliases *) ~universe ~lookup_in_library t =
- let mk_alias = function
- | Ast.Ident (id,_) -> DisambiguateTypes.Id (id,None)
- | Ast.Symbol (sym,_) -> DisambiguateTypes.Symbol (sym,None)
- | Ast.Num _ -> DisambiguateTypes.Num None
- | _ -> assert false
- in
- let lookup_choices =
- fun item ->
- (*match universe with
- | None ->
- lookup_in_library
- interactive_user_uri_choice
- input_or_locate_uri item
- | Some e ->
- (try Environment.find item e
- with Not_found -> [])
-*)
- (try Environment.find item universe
- with Not_found -> [])
- in
- match t with
- | Ast.Ident (_,None)
- | Ast.Num (_,None)
- | Ast.Symbol (_,None) ->
- let choices = lookup_choices (mk_alias t) in
- if List.length choices <> 1 then t
- else List.hd choices
- (* but we lose info on closedness *)
- | t -> Ast.map (initialize_ast ~universe ~lookup_in_library) 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,None)
- | Ast.Symbol (sym,_) -> DisambiguateTypes.Symbol (sym,None)
- | Ast.Num (n,_) -> DisambiguateTypes.Num None
- | Ast.Case(_,Some (ityname,_),_,_) -> DisambiguateTypes.Id (ityname,None)
+ | 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
;;
| _ -> assert false
;;
-let test_interpr ~context ~metasenv ~subst ~use_coercions ~expty ~env ~uri
+(* 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
+ 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 _ -> false
- | _ -> true
+ | 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 _ -> false
- | _ -> true
+ | 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 =
+ ~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 ~uri ~interpretate_thing ~refine_thing ~ugraph ~mk_localization_tbl
+ ~env ~universe ~uri ~interpretate_thing ~refine_thing ~ugraph ~mk_localization_tbl
in
let find_choices item =
let a2s = function
- | GrafiteAst.Ident_alias (id,_)
- | GrafiteAst.Symbol_alias (id,_,_) -> id
- | GrafiteAst.Number_alias _ -> "NUM"
+ | 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"
+ | Id id
+ | Symbol id -> id
+ | Num -> "NUM"
in
let res =
Environment.find item universe
in
- prerr_endline (Printf.sprintf "choices for %s :\n%s"
- (d2s item) (String.concat ", " (List.map a2s 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)) choices
+ List.map (fun t0 -> ctx (ast_of_alias_spec t t0), t0) choices
with
| Not_found -> []
in
match ts with
- | [] -> None
- | t0 :: tl ->
- prerr_endline ("disambiguation of 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 (_,None) -> true
- | Ast.Case (_,Some (ity,None),_,_) ->
- (prerr_endline ("ambiguous case" ^ ity);true)
- | Ast.Case (_,None,_,_) -> prerr_endline "amb1";false
- | Ast.Case (_,Some (ity,Some r),_,_) ->
- (prerr_endline ("amb2 " ^ NReference.string_of_reference r);false)
- | Ast.Ident (n,`Uri u) ->
- (prerr_endline ("uri " ^ u ^ "inside IDENT " ^ n) ;false )
+ | Ast.Case (_,Some (ity,None),_,_) -> true
| _ -> false
in
let astpp = function
| Ast.Symbol (sym,_) -> "SYM " ^ sym
| _ -> "ERROR!"
in
- (* get first ambiguous subterm (or return disambiguated term) *)
- match visit ~pp_term is_ambiguous t0 with
- | None ->
- prerr_endline ("not ambiguous:\n" ^ pp_thing t0);
- Some (t0,tl)
- | Some (ctx, t) ->
- prerr_endline ("disambiguating node " ^ astpp t ^
- "\nin " ^ pp_thing (ctx t));
- (* get possible instantiations of t *)
- let instances = get_instances ctx t in
- (* perforate ambiguous subterms and test refinement *)
- let survivors = List.filter test_interpr instances in
- 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
+ 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)
-
-(* let rec aux l =
- match l with
- | [] -> None
- | (ctx,u)::vl ->
- if test u
- then (ctx,u)
- else aux (vl@split ctx u)
- in aux [t]
-;;*)
-
-(* let rec instantiate_ast = function
- | Ident (n,Some _)
- | Symbol (s,Some _)
- | Num (n,Some _) as t -> []
- | Ident (n,None) -> (* output: all possible instantiations of n *)
- | Symbol (s,None) ->
- | Num (n,None) ->
-
-
- | AttributedTerm (a,u) -> AttributedTerm (a,f u)
- | Appl tl -> Appl (List.map f tl)
- | Binder (k,n,body) -> Binder (k,n,f body)
- | Case (t,ity,oty,pl) ->
- let pl' = List.map (fun (p,u) -> p,f u) pl in
- Case (f t,ity,map_option f oty,pl')
- | Cast (u,v) -> Cast (f u,f v)
- | LetIn (n,u,v) -> LetIn (n,f u,f v)
- | LetRec -> ada (* TODO *)
- | t -> 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)
=
-(* XXX: will be thrown away *)
- let todo_dom = domain_of_thing ~context:(string_context_of_context context) thing
- in
- let rec aux_env 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_env (aux_env env l) tl in
- let env = aux_env aliases todo_dom in
+ let env = aliases in
let test_interpr = test_interpr ~context ~metasenv ~subst ~use_coercions ~expty
- ~env ~uri ~interpretate_thing ~refine_thing ~ugraph:base_univ ~mk_localization_tbl
+ ~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
- match refine_thing metasenv subst context uri
- ~use_coercions
- (interpretate_thing ~context ~env ~uri ~is_path:false t ~localization_tbl)
- expty base_univ ~localization_tbl with
- | Ok (t',m',s',u') -> ([]:(Environment.key * 'f) list),m',s',t',u'
+ 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 ->
let _,err = Lazy.force x in
- prerr_endline ("refinement uncertain after disambiguation: " ^ err);
+ debug_print (lazy ("refinement uncertain after disambiguation: " ^ err));
assert false
| _ -> assert false
in
- if not (test_interpr thing) then raise (NoWellTypedInterpretation (0,[]))
- else
- let res = aux [thing] in
- let res =
- HExtlib.filter_map (fun t -> try Some (refine t) with _ -> 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 =
+ HExtlib.filter_map (fun t ->
+ try Some (refine t)
+ with _ ->
+(* debug_print (lazy ("can't interpretate/refine " ^ (pp_thing t)));*)
+ None) res
in
- match res with
- | [] -> raise (NoWellTypedInterpretation (0,[]))
- | [t] -> res,false
- | _ -> res,true
+ (match res with
+ | [] -> Disamb_failure (errors,[])
+ | _ -> Disamb_success res)
;;
-(*
-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
-
- (* 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
-
-(*
- (* <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> *)
-*)
-
- (* (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
- 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
- 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]
- 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
- in
- res
- *)
projects / helm.git / blobdiff