diff options
Diffstat (limited to 'interp/implicit_quantifiers.ml')
| -rw-r--r-- | interp/implicit_quantifiers.ml | 172 |
1 files changed, 85 insertions, 87 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 1b0f1341..e304725d 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -9,45 +9,35 @@ (*i*) open Names open Decl_kinds -open Term -open Sign -open Evd -open Environ -open Nametab -open Mod_subst +open Errors open Util open Glob_term -open Topconstr +open Constrexpr open Libnames open Typeclasses open Typeclasses_errors open Pp open Libobject open Nameops +open Misctypes (*i*) -let generalizable_table = ref Idpred.empty - -let _ = - Summary.declare_summary "generalizable-ident" - { Summary.freeze_function = (fun () -> !generalizable_table); - Summary.unfreeze_function = (fun r -> generalizable_table := r); - Summary.init_function = (fun () -> generalizable_table := Idpred.empty) } +let generalizable_table = Summary.ref Id.Pred.empty ~name:"generalizable-ident" let declare_generalizable_ident table (loc,id) = - if id <> root_of_id id then + if not (Id.equal id (root_of_id id)) then user_err_loc(loc,"declare_generalizable_ident", (pr_id id ++ str " is not declarable as generalizable identifier: it must have no trailing digits, quote, or _")); - if Idpred.mem id table then + if Id.Pred.mem id table then user_err_loc(loc,"declare_generalizable_ident", (pr_id id++str" is already declared as a generalizable identifier")) - else Idpred.add id table + else Id.Pred.add id table let add_generalizable gen table = match gen with - | None -> Idpred.empty - | Some [] -> Idpred.full + | None -> Id.Pred.empty + | Some [] -> Id.Pred.full | Some l -> List.fold_left (fun table lid -> declare_generalizable_ident table lid) table l @@ -57,7 +47,7 @@ let cache_generalizable_type (_,(local,cmd)) = let load_generalizable_type _ (_,(local,cmd)) = generalizable_table := add_generalizable cmd !generalizable_table -let in_generalizable : bool * identifier located list option -> obj = +let in_generalizable : bool * Id.t Loc.located list option -> obj = declare_object {(default_object "GENERALIZED-IDENT") with load_function = load_generalizable_type; cache_function = cache_generalizable_type; @@ -67,29 +57,22 @@ let in_generalizable : bool * identifier located list option -> obj = let declare_generalizable local gen = Lib.add_anonymous_leaf (in_generalizable (local, gen)) -let find_generalizable_ident id = Idpred.mem (root_of_id id) !generalizable_table +let find_generalizable_ident id = Id.Pred.mem (root_of_id id) !generalizable_table let ids_of_list l = - List.fold_right Idset.add l Idset.empty - -let locate_reference qid = - match Nametab.locate_extended qid with - | TrueGlobal ref -> true - | SynDef kn -> true + List.fold_right Id.Set.add l Id.Set.empty let is_global id = - try - locate_reference (qualid_of_ident id) - with Not_found -> - false + try ignore (Nametab.locate_extended (qualid_of_ident id)); true + with Not_found -> false + +let is_named id env = + try ignore (Environ.lookup_named id env); true + with Not_found -> false let is_freevar ids env x = - try - if Idset.mem x ids then false - else - try ignore(Environ.lookup_named x env) ; false - with e when Errors.noncritical e -> not (is_global x) - with e when Errors.noncritical e -> true + not (Id.Set.mem x ids || is_named x env || is_global x) + (* Auxiliary functions for the inference of implicitly quantified variables. *) @@ -97,9 +80,9 @@ let ungeneralizable loc id = user_err_loc (loc, "Generalization", str "Unbound and ungeneralizable variable " ++ pr_id id) -let free_vars_of_constr_expr c ?(bound=Idset.empty) l = +let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l = let found loc id bdvars l = - if List.mem id l then l + if Id.List.mem id l then l else if is_freevar bdvars (Global.env ()) id then if find_generalizable_ident id then id :: l @@ -107,26 +90,26 @@ let free_vars_of_constr_expr c ?(bound=Idset.empty) l = else l in let rec aux bdvars l c = match c with - | CRef (Ident (loc,id)) -> found loc id bdvars l - | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id)) :: _, [], [])) when not (Idset.mem id bdvars) -> - fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux (Idset.add id bdvars) l c - | c -> fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c + | CRef (Ident (loc,id),_) -> found loc id bdvars l + | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id),_) :: _, [], [])) when not (Id.Set.mem id bdvars) -> + Topconstr.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add id bdvars) l c + | c -> Topconstr.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c in aux bound l c let ids_of_names l = List.fold_left (fun acc x -> match snd x with Name na -> na :: acc | Anonymous -> acc) [] l -let free_vars_of_binders ?(bound=Idset.empty) l (binders : local_binder list) = +let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder list) = let rec aux bdvars l c = match c with ((LocalRawAssum (n, _, c)) :: tl) -> let bound = ids_of_names n in let l' = free_vars_of_constr_expr c ~bound:bdvars l in - aux (Idset.union (ids_of_list bound) bdvars) l' tl + aux (Id.Set.union (ids_of_list bound) bdvars) l' tl | ((LocalRawDef (n, c)) :: tl) -> let bound = match snd n with Anonymous -> [] | Name n -> [n] in let l' = free_vars_of_constr_expr c ~bound:bdvars l in - aux (Idset.union (ids_of_list bound) bdvars) l' tl + aux (Id.Set.union (ids_of_list bound) bdvars) l' tl | [] -> bdvars, l in aux bound l binders @@ -134,13 +117,13 @@ let free_vars_of_binders ?(bound=Idset.empty) l (binders : local_binder list) = let add_name_to_ids set na = match na with | Anonymous -> set - | Name id -> Idset.add id set + | Name id -> Id.Set.add id set -let generalizable_vars_of_glob_constr ?(bound=Idset.empty) ?(allowed=Idset.empty) = +let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.empty) = let rec vars bound vs = function | GVar (loc,id) -> if is_freevar bound (Global.env ()) id then - if List.mem_assoc id vs then vs + if Id.List.mem_assoc id vs then vs else (id, loc) :: vs else vs | GApp (loc,f,args) -> List.fold_left (vars bound) vs (f::args) @@ -163,7 +146,7 @@ let generalizable_vars_of_glob_constr ?(bound=Idset.empty) ?(allowed=Idset.empty let vs3 = vars bound vs2 b1 in vars bound vs3 b2 | GRec (loc,fk,idl,bl,tyl,bv) -> - let bound' = Array.fold_right Idset.add idl bound in + let bound' = Array.fold_right Id.Set.add idl bound in let vars_fix i vs fid = let vs1,bound1 = List.fold_left @@ -179,13 +162,13 @@ let generalizable_vars_of_glob_constr ?(bound=Idset.empty) ?(allowed=Idset.empty let vs2 = vars bound1 vs1 tyl.(i) in vars bound1 vs2 bv.(i) in - array_fold_left_i vars_fix vs idl + Array.fold_left_i vars_fix vs idl | GCast (loc,c,k) -> let v = vars bound vs c in - (match k with CastConv (_,t) -> vars bound v t | _ -> v) + (match k with CastConv t | CastVM t -> vars bound v t | _ -> v) | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> vs and vars_pattern bound vs (loc,idl,p,c) = - let bound' = List.fold_right Idset.add idl bound in + let bound' = List.fold_right Id.Set.add idl bound in vars bound' vs c and vars_option bound vs = function None -> vs | Some p -> vars bound vs p @@ -196,7 +179,7 @@ let generalizable_vars_of_glob_constr ?(bound=Idset.empty) ?(allowed=Idset.empty in fun rt -> let vars = List.rev (vars bound [] rt) in List.iter (fun (id, loc) -> - if not (Idset.mem id allowed || find_generalizable_ident id) then + if not (Id.Set.mem id allowed || find_generalizable_ident id) then ungeneralizable loc id) vars; vars @@ -205,7 +188,7 @@ let rec make_fresh ids env x = let next_name_away_from na avoid = match na with - | Anonymous -> make_fresh avoid (Global.env ()) (id_of_string "anon") + | Anonymous -> make_fresh avoid (Global.env ()) (Id.of_string "anon") | Name id -> make_fresh avoid (Global.env ()) id let combine_params avoid fn applied needed = @@ -213,7 +196,11 @@ let combine_params avoid fn applied needed = List.partition (function (t, Some (loc, ExplByName id)) -> - if not (List.exists (fun (_, (id', _, _)) -> Name id = id') needed) then + let is_id (_, (na, _, _)) = match na with + | Name id' -> Id.equal id id' + | Anonymous -> false + in + if not (List.exists is_id needed) then user_err_loc (loc,"",str "Wrong argument name: " ++ Nameops.pr_id id); true | _ -> false) applied @@ -222,13 +209,17 @@ let combine_params avoid fn applied needed = (fun x -> match x with (t, Some (loc, ExplByName id)) -> id, t | _ -> assert false) named in - let needed = List.filter (fun (_, (_, b, _)) -> b = None) needed in + let is_unset (_, (_, b, _)) = match b with + | None -> true + | Some _ -> false + in + let needed = List.filter is_unset needed in let rec aux ids avoid app need = match app, need with [], [] -> List.rev ids, avoid - | app, (_, (Name id, _, _)) :: need when List.mem_assoc id named -> - aux (List.assoc id named :: ids) avoid app need + | app, (_, (Name id, _, _)) :: need when Id.List.mem_assoc id named -> + aux (Id.List.assoc id named :: ids) avoid app need | (x, None) :: app, (None, (Name id, _, _)) :: need -> aux (x :: ids) avoid app need @@ -244,25 +235,25 @@ let combine_params avoid fn applied needed = aux (t' :: ids) avoid' app need | (x,_) :: _, [] -> - user_err_loc (constr_loc x,"",str "Typeclass does not expect more arguments") + user_err_loc (Constrexpr_ops.constr_loc x,"",str "Typeclass does not expect more arguments") in aux [] avoid applied needed let combine_params_freevar = fun avoid (_, (na, _, _)) -> let id' = next_name_away_from na avoid in - (CRef (Ident (dummy_loc, id')), Idset.add id' avoid) + (CRef (Ident (Loc.ghost, id'),None), Id.Set.add id' avoid) let destClassApp cl = match cl with - | CApp (loc, (None, CRef ref), l) -> loc, ref, List.map fst l - | CAppExpl (loc, (None, ref), l) -> loc, ref, l - | CRef ref -> loc_of_reference ref, ref, [] + | CApp (loc, (None, CRef (ref,_)), l) -> loc, ref, List.map fst l + | CAppExpl (loc, (None, ref,_), l) -> loc, ref, l + | CRef (ref,_) -> loc_of_reference ref, ref, [] | _ -> raise Not_found let destClassAppExpl cl = match cl with - | CApp (loc, (None, CRef ref), l) -> loc, ref, l - | CRef ref -> loc_of_reference ref, ref, [] + | CApp (loc, (None, CRef (ref,_)), l) -> loc, ref, l + | CRef (ref,_) -> loc_of_reference ref, ref, [] | _ -> raise Not_found let implicit_application env ?(allow_partial=true) f ty = @@ -277,32 +268,37 @@ let implicit_application env ?(allow_partial=true) f ty = match is_class with | None -> ty, env | Some ((loc, id, par), gr) -> - let avoid = Idset.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in + let avoid = Id.Set.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in let c, avoid = let c = class_info gr in let (ci, rd) = c.cl_context in if not allow_partial then begin - let applen = List.fold_left (fun acc (x, y) -> if y = None then succ acc else acc) 0 par in - let needlen = List.fold_left (fun acc x -> if x = None then succ acc else acc) 0 ci in - if needlen <> applen then + let opt_succ x n = match x with + | None -> succ n + | Some _ -> n + in + let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in + let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in + if not (Int.equal needlen applen) then Typeclasses_errors.mismatched_ctx_inst (Global.env ()) Parameters (List.map fst par) rd end; let pars = List.rev (List.combine ci rd) in let args, avoid = combine_params avoid f par pars in - CAppExpl (loc, (None, id), args), avoid + CAppExpl (loc, (None, id, None), args), avoid in c, avoid let implicits_of_glob_constr ?(with_products=true) l = - let add_impl i na bk l = - if bk = Implicit then - let name = - match na with - | Name id -> Some id - | Anonymous -> None - in - (ExplByPos (i, name), (true, true, true)) :: l - else l in + let add_impl i na bk l = match bk with + | Implicit -> + let name = + match na with + | Name id -> Some id + | Anonymous -> None + in + (ExplByPos (i, name), (true, true, true)) :: l + | _ -> l + in let rec aux i c = let abs na bk b = add_impl i na bk (aux (succ i) b) @@ -310,15 +306,17 @@ let implicits_of_glob_constr ?(with_products=true) l = match c with | GProd (loc, na, bk, t, b) -> if with_products then abs na bk b - else - (if bk = Implicit then - msg_warning (str "Ignoring implicit status of product binder " ++ - pr_name na ++ str " and following binders"); - []) + else + let () = match bk with + | Implicit -> + msg_warning (strbrk "Ignoring implicit status of product binder " ++ + pr_name na ++ strbrk " and following binders") + | _ -> () + in [] | GLambda (loc, na, bk, t, b) -> abs na bk b | GLetIn (loc, na, t, b) -> aux i b | GRec (_, fix_kind, nas, args, tys, bds) -> let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in - list_fold_left_i (fun i l (na,bk,_,_) -> add_impl i na bk l) i (aux (List.length args.(nb) + i) bds.(nb)) args.(nb) + List.fold_left_i (fun i l (na,bk,_,_) -> add_impl i na bk l) i (aux (List.length args.(nb) + i) bds.(nb)) args.(nb) | _ -> [] in aux 1 l |