aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/closure.ml15
-rw-r--r--checker/environ.ml23
-rw-r--r--checker/environ.mli7
-rw-r--r--checker/inductive.ml11
-rw-r--r--checker/term.ml10
-rw-r--r--checker/term.mli7
-rw-r--r--checker/typeops.ml8
7 files changed, 4 insertions, 77 deletions
diff --git a/checker/closure.ml b/checker/closure.ml
index 45452874e..3ed9dd27a 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -151,7 +151,6 @@ let betaiotazeta = mkflags [fBETA;fIOTA;fZETA]
* is stored in the table.
* * i_rels = (4,[(1,c);(3,d)]) means there are 4 free rel variables
* and only those with index 1 and 3 have bodies which are c and d resp.
- * * i_vars is the list of _defined_ named variables.
*
* ref_value_cache searchs in the tab, otherwise uses i_repr to
* compute the result and store it in the table. If the constant can't
@@ -171,7 +170,6 @@ type 'a infos = {
i_repr : 'a infos -> constr -> 'a;
i_env : env;
i_rels : int * (int * constr) list;
- i_vars : (Id.t * constr) list;
i_tab : (table_key, 'a) Hashtbl.t }
let ref_value_cache info ref =
@@ -183,7 +181,7 @@ let ref_value_cache info ref =
match ref with
| RelKey n ->
let (s,l) = info.i_rels in lift n (List.assoc (s-n) l)
- | VarKey id -> List.assoc id info.i_vars
+ | VarKey id -> raise Not_found
| ConstKey cst -> constant_value info.i_env cst
in
let v = info.i_repr info body in
@@ -194,16 +192,6 @@ let ref_value_cache info ref =
| NotEvaluableConst _ (* Const *)
-> None
-let defined_vars flags env =
-(* if red_local_const (snd flags) then*)
- fold_named_context
- (fun (id,b,_) e ->
- match b with
- | None -> e
- | Some body -> (id, body)::e)
- (named_context env) ~init:[]
-(* else []*)
-
let defined_rels flags env =
(* if red_local_const (snd flags) then*)
fold_rel_context
@@ -226,7 +214,6 @@ let create mk_cl flgs env =
i_repr = mk_cl;
i_env = env;
i_rels = defined_rels flgs env;
- i_vars = defined_vars flgs env;
i_tab = Hashtbl.create 17 }
diff --git a/checker/environ.ml b/checker/environ.ml
index c64495d41..1485d6bf0 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -20,7 +20,6 @@ type stratification = {
type env = {
env_globals : globals;
- env_named_context : named_context;
env_rel_context : rel_context;
env_stratification : stratification;
env_imports : Digest.t MPmap.t }
@@ -32,7 +31,6 @@ let empty_env = {
env_inductives_eq = KNmap.empty;
env_modules = MPmap.empty;
env_modtypes = MPmap.empty};
- env_named_context = [];
env_rel_context = [];
env_stratification =
{ env_universes = Univ.initial_universes;
@@ -41,7 +39,6 @@ let empty_env = {
let engagement env = env.env_stratification.env_engagement
let universes env = env.env_stratification.env_universes
-let named_context env = env.env_named_context
let rel_context env = env.env_rel_context
let set_engagement c env =
@@ -78,26 +75,6 @@ let push_rec_types (lna,typarray,_) env =
let ctxt = Array.map2_i (fun i na t -> (na, None, lift i t)) lna typarray in
Array.fold_left (fun e assum -> push_rel assum e) env ctxt
-(* Named context *)
-
-let push_named d env =
-(* if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context);
- assert (env.env_rel_context = []); *)
- { env with
- env_named_context = d :: env.env_named_context }
-
-let lookup_named id env =
- let rec lookup_named id = function
- | (id',_,_ as decl) :: _ when id=id' -> decl
- | _ :: sign -> lookup_named id sign
- | [] -> raise Not_found in
- lookup_named id env.env_named_context
-
-(* A local const is evaluable if it is defined *)
-
-let named_type id env =
- let (_,_,t) = lookup_named id env in t
-
(* Universe constraints *)
let add_constraints c env =
if c == empty_constraint then
diff --git a/checker/environ.mli b/checker/environ.mli
index 3cd4ca6e0..847af5231 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -16,7 +16,6 @@ type stratification = {
}
type env = {
env_globals : globals;
- env_named_context : named_context;
env_rel_context : rel_context;
env_stratification : stratification;
env_imports : Digest.t MPmap.t;
@@ -38,12 +37,6 @@ val push_rel : rel_declaration -> env -> env
val push_rel_context : rel_context -> env -> env
val push_rec_types : name array * constr array * 'a -> env -> env
-(* Named variables *)
-val named_context : env -> named_context
-val push_named : named_declaration -> env -> env
-val lookup_named : Id.t -> env -> named_declaration
-val named_type : Id.t -> env -> constr
-
(* Universes *)
val universes : env -> Univ.universes
val add_constraints : Univ.constraints -> env -> env
diff --git a/checker/inductive.ml b/checker/inductive.ml
index ac9bf415c..9e1524018 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -752,16 +752,7 @@ let check_one_fix renv recpos def =
| (Ind _ | Construct _) ->
List.iter (check_rec_call renv []) l
- | Var id ->
- begin
- match pi2 (lookup_named id renv.env) with
- | None ->
- List.iter (check_rec_call renv []) l
- | Some c ->
- try List.iter (check_rec_call renv []) l
- with (FixGuardError _) ->
- check_rec_call renv stack (applist(c,l))
- end
+ | Var _ -> anomaly (Pp.str "Section variable in Coqchk !")
| Sort _ -> assert (l = [])
diff --git a/checker/term.ml b/checker/term.ml
index a3c9225f5..371889436 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -209,12 +209,6 @@ let subst1 lam = substl [lam]
(* Type of assumptions and contexts *)
(***************************************************************************)
-type named_declaration = Id.t * constr option * constr
-type named_context = named_declaration list
-
-let empty_named_context = []
-let fold_named_context f l ~init = List.fold_right f l init
-
let empty_rel_context = []
let rel_context_length = List.length
let rel_context_nhyps hyps =
@@ -225,7 +219,7 @@ let rel_context_nhyps hyps =
nhyps 0 hyps
let fold_rel_context f l ~init = List.fold_right f l init
-let map_context f l =
+let map_rel_context f l =
let map_decl (n, body_o, typ as decl) =
let body_o' = Option.smartmap f body_o in
let typ' = f typ in
@@ -234,8 +228,6 @@ let map_context f l =
in
List.smartmap map_decl l
-let map_rel_context = map_context
-
let extended_rel_list n hyps =
let rec reln l p = function
| (_,None,_) :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps
diff --git a/checker/term.mli b/checker/term.mli
index 7316b18e5..68b408617 100644
--- a/checker/term.mli
+++ b/checker/term.mli
@@ -29,18 +29,11 @@ val substnl : constr list -> int -> constr -> constr
val substl : constr list -> constr -> constr
val subst1 : constr -> constr -> constr
-type named_declaration = Id.t * constr option * constr
-type named_context = named_declaration list
-val empty_named_context : named_context
-val fold_named_context :
- (named_declaration -> 'a -> 'a) -> named_context -> init:'a -> 'a
-
val empty_rel_context : rel_context
val rel_context_length : rel_context -> int
val rel_context_nhyps : rel_context -> int
val fold_rel_context :
(rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a
-val map_context : (constr -> constr) -> named_context -> named_context
val map_rel_context : (constr -> constr) -> rel_context -> rel_context
val extended_rel_list : int -> rel_context -> constr list
val compose_lam : (name * constr) list -> constr -> constr
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 7ff99bd93..f22649eb5 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -65,12 +65,6 @@ let judge_of_relative env n =
with Not_found ->
error_unbound_rel env n
-(* Type of variables *)
-let judge_of_variable env id =
- try named_type id env
- with Not_found ->
- error_unbound_var env id
-
(* Type of constants *)
let type_of_constant_knowing_parameters env t paramtyps =
@@ -247,7 +241,7 @@ let rec execute env cstr =
| Rel n -> judge_of_relative env n
- | Var id -> judge_of_variable env id
+ | Var _ -> anomaly (Pp.str "Section variable in Coqchk !")
| Const c -> judge_of_constant env c
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 17:16:23 +0000