aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/check.ml15
-rw-r--r--checker/checker.ml5
-rw-r--r--checker/closure.ml228
-rw-r--r--checker/closure.mli24
-rw-r--r--checker/declarations.ml87
-rw-r--r--checker/declarations.mli5
-rw-r--r--checker/environ.ml9
-rw-r--r--checker/environ.mli2
-rw-r--r--checker/inductive.ml10
-rw-r--r--checker/mod_checking.ml7
-rw-r--r--checker/modops.ml15
-rw-r--r--checker/modops.mli2
-rw-r--r--checker/reduction.ml40
-rw-r--r--checker/reduction.mli5
-rw-r--r--checker/safe_typing.ml1
-rw-r--r--checker/safe_typing.mli1
-rw-r--r--checker/subtyping.ml5
-rw-r--r--checker/subtyping.mli1
-rw-r--r--checker/term.ml8
-rw-r--r--checker/term.mli8
-rw-r--r--checker/type_errors.ml3
-rw-r--r--checker/type_errors.mli2
-rw-r--r--checker/typeops.ml37
-rw-r--r--checker/validate.ml3
24 files changed, 6 insertions, 517 deletions
diff --git a/checker/check.ml b/checker/check.ml
index 7e834270d..570220981 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -10,7 +10,6 @@ open Pp
open Util
open Names
-let pr_id id = str (string_of_id id)
let pr_dirpath dp = str (string_of_dirpath dp)
let default_root_prefix = make_dirpath []
let split_dirpath d =
@@ -153,12 +152,6 @@ let find_logical_path phys_dir =
| _,[] -> default_root_prefix
| _,l -> anomaly ("Two logical paths are associated to "^phys_dir)
-let is_in_load_paths phys_dir =
- let dir = canonical_path_name phys_dir in
- let lp = get_load_paths () in
- let check_p = fun p -> (String.compare dir p) == 0 in
- List.exists check_p lp
-
let remove_load_path dir =
load_paths := list_filter2 (fun p d -> p <> dir) !load_paths
@@ -189,13 +182,9 @@ let add_load_path (phys_path,coq_path) =
load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths)
| _ -> anomaly ("Two logical paths are associated to "^phys_path)
-let physical_paths (dp,lp) = dp
-
let load_paths_of_dir_path dir =
fst (list_filter2 (fun p d -> d = dir) !load_paths)
-let get_full_load_paths () = List.combine (fst !load_paths) (snd !load_paths)
-
(************************************************************************)
(*s Locate absolute or partially qualified library names in the path *)
@@ -267,8 +256,8 @@ let try_locate_qualified_library qid =
(*s Loading from disk to cache (preparation phase) *)
-let (raw_extern_library, raw_intern_library) =
- System.raw_extern_intern Coq_config.vo_magic_number ".vo"
+let raw_intern_library =
+ snd (System.raw_extern_intern Coq_config.vo_magic_number ".vo")
let with_magic_number_check f a =
try f a
diff --git a/checker/checker.ml b/checker/checker.ml
index 9213eb134..9646141d0 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -91,9 +91,6 @@ let push_rec_include (s, alias) = includes := (s,alias,true) :: !includes
let set_default_include d =
push_include (d, Check.default_root_prefix)
-let set_default_rec_include d =
- let p = Check.default_root_prefix in
- push_rec_include (d, p)
let set_include d p =
let p = dirpath_of_string p in
push_include (d,p)
@@ -202,8 +199,6 @@ let usage () =
flush stderr;
exit 1
-let warning s = msg_warning (str s)
-
open Type_errors
let anomaly_string () = str "Anomaly: "
diff --git a/checker/closure.ml b/checker/closure.ml
index 41103e202..8cf8c4c07 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -63,11 +63,8 @@ module type RedFlagsSig = sig
val fVAR : identifier -> red_kind
val no_red : reds
val red_add : reds -> red_kind -> reds
- val red_sub : reds -> red_kind -> reds
- val red_add_transparent : reds -> transparent_state -> reds
val mkflags : red_kind list -> reds
val red_set : reds -> red_kind -> bool
- val red_get_const : reds -> bool * evaluable_global_reference list
end
module RedFlags = (struct
@@ -112,21 +109,6 @@ module RedFlags = (struct
let (l1,l2) = red.r_const in
{ red with r_const = Idpred.add id l1, l2 }
- let red_sub red = function
- | BETA -> { red with r_beta = false }
- | DELTA -> { red with r_delta = false }
- | CONST kn ->
- let (l1,l2) = red.r_const in
- { red with r_const = l1, Cpred.remove kn l2 }
- | IOTA -> { red with r_iota = false }
- | ZETA -> { red with r_zeta = false }
- | VAR id ->
- let (l1,l2) = red.r_const in
- { red with r_const = Idpred.remove id l1, l2 }
-
- let red_add_transparent red tr =
- { red with r_const = tr }
-
let mkflags = List.fold_left red_add no_red
let red_set red = function
@@ -144,160 +126,14 @@ module RedFlags = (struct
| DELTA -> (* Used for Rel/Var defined in context *)
incr_cnt red.r_delta delta
- let red_get_const red =
- let p1,p2 = red.r_const in
- let (b1,l1) = Idpred.elements p1 in
- let (b2,l2) = Cpred.elements p2 in
- if b1=b2 then
- let l1' = List.map (fun x -> EvalVarRef x) l1 in
- let l2' = List.map (fun x -> EvalConstRef x) l2 in
- (b1, l1' @ l2')
- else error "unrepresentable pair of predicate"
-
end : RedFlagsSig)
open RedFlags
let betadeltaiota = mkflags [fBETA;fDELTA;fZETA;fIOTA]
let betadeltaiotanolet = mkflags [fBETA;fDELTA;fIOTA]
-let betaiota = mkflags [fBETA;fIOTA]
-let beta = mkflags [fBETA]
let betaiotazeta = mkflags [fBETA;fIOTA;fZETA]
-let unfold_red kn =
- let flag = match kn with
- | EvalVarRef id -> fVAR id
- | EvalConstRef kn -> fCONST kn
- in (* Remove fZETA for finer behaviour ? *)
- mkflags [fBETA;flag;fIOTA;fZETA]
-
-(************************* Obsolète
-(* [r_const=(true,cl)] means all constants but those in [cl] *)
-(* [r_const=(false,cl)] means only those in [cl] *)
-type reds = {
- r_beta : bool;
- r_const : bool * constant_path list * identifier list;
- r_zeta : bool;
- r_evar : bool;
- r_iota : bool }
-
-let betadeltaiota_red = {
- r_beta = true;
- r_const = true,[],[];
- r_zeta = true;
- r_evar = true;
- r_iota = true }
-
-let betaiota_red = {
- r_beta = true;
- r_const = false,[],[];
- r_zeta = false;
- r_evar = false;
- r_iota = true }
-
-let beta_red = {
- r_beta = true;
- r_const = false,[],[];
- r_zeta = false;
- r_evar = false;
- r_iota = false }
-
-let no_red = {
- r_beta = false;
- r_const = false,[],[];
- r_zeta = false;
- r_evar = false;
- r_iota = false }
-
-let betaiotazeta_red = {
- r_beta = true;
- r_const = false,[],[];
- r_zeta = true;
- r_evar = false;
- r_iota = true }
-
-let unfold_red kn =
- let c = match kn with
- | EvalVarRef id -> false,[],[id]
- | EvalConstRef kn -> false,[kn],[]
- in {
- r_beta = true;
- r_const = c;
- r_zeta = true; (* false for finer behaviour ? *)
- r_evar = false;
- r_iota = true }
-
-(* Sets of reduction kinds.
- Main rule: delta implies all consts (both global (= by
- kernel_name) and local (= by Rel or Var)), all evars, and zeta (= letin's).
- Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of
- a LetIn expression is Letin reduction *)
-
-type red_kind =
- BETA | DELTA | ZETA | IOTA
- | CONST of constant_path list | CONSTBUT of constant_path list
- | VAR of identifier | VARBUT of identifier
-
-let rec red_add red = function
- | BETA -> { red with r_beta = true }
- | DELTA ->
- (match red.r_const with
- | _,_::_,[] | _,[],_::_ -> error "Conflict in the reduction flags"
- | _ -> { red with r_const = true,[],[]; r_zeta = true; r_evar = true })
- | CONST cl ->
- (match red.r_const with
- | true,_,_ -> error "Conflict in the reduction flags"
- | _,l1,l2 -> { red with r_const = false, list_union cl l1, l2 })
- | CONSTBUT cl ->
- (match red.r_const with
- | false,_::_,_ | false,_,_::_ ->
- error "Conflict in the reduction flags"
- | _,l1,l2 ->
- { red with r_const = true, list_union cl l1, l2;
- r_zeta = true; r_evar = true })
- | IOTA -> { red with r_iota = true }
- | ZETA -> { red with r_zeta = true }
- | VAR id ->
- (match red.r_const with
- | true,_,_ -> error "Conflict in the reduction flags"
- | _,l1,l2 -> { red with r_const = false, l1, list_union [id] l2 })
- | VARBUT cl ->
- (match red.r_const with
- | false,_::_,_ | false,_,_::_ ->
- error "Conflict in the reduction flags"
- | _,l1,l2 ->
- { red with r_const = true, l1, list_union [cl] l2;
- r_zeta = true; r_evar = true })
-
-let red_delta_set red =
- let b,_,_ = red.r_const in b
-
-let red_local_const = red_delta_set
-
-(* to know if a redex is allowed, only a subset of red_kind is used ... *)
-let red_set red = function
- | BETA -> incr_cnt red.r_beta beta
- | CONST [kn] ->
- let (b,l,_) = red.r_const in
- let c = List.mem kn l in
- incr_cnt ((b & not c) or (c & not b)) delta
- | VAR id -> (* En attendant d'avoir des kn pour les Var *)
- let (b,_,l) = red.r_const in
- let c = List.mem id l in
- incr_cnt ((b & not c) or (c & not b)) delta
- | ZETA -> incr_cnt red.r_zeta zeta
- | EVAR -> incr_cnt red.r_zeta evar
- | IOTA -> incr_cnt red.r_iota iota
- | DELTA -> red_delta_set red (*Used for Rel/Var defined in context*)
- (* Not for internal use *)
- | CONST _ | CONSTBUT _ | VAR _ | VARBUT _ -> failwith "not implemented"
-
-(* Gives the constant list *)
-let red_get_const red =
- let b,l1,l2 = red.r_const in
- let l1' = List.map (fun x -> EvalConstRef x) l1 in
- let l2' = List.map (fun x -> EvalVarRef x) l2 in
- b, l1' @ l2'
-fin obsolète **************)
+
(* specification of the reduction function *)
@@ -334,8 +170,6 @@ type 'a infos = {
i_vars : (identifier * constr) list;
i_tab : (table_key, 'a) Hashtbl.t }
-let info_flags info = info.i_flags
-
let ref_value_cache info ref =
try
Some (Hashtbl.find info.i_tab ref)
@@ -445,9 +279,6 @@ and fterm =
let fterm_of v = v.term
let set_norm v = v.norm <- Norm
-let is_val v = v.norm = Norm
-
-let mk_atom c = {norm=Norm;term=FAtom c}
(* Could issue a warning if no is still Red, pointing out that we loose
sharing. *)
@@ -470,7 +301,6 @@ type stack_member =
and stack = stack_member list
-let empty_stack = []
let append_stack v s =
if Array.length v = 0 then s else
match s with
@@ -484,52 +314,6 @@ let zshift n s =
| (_,Zshift(k)::s) -> Zshift(n+k)::s
| _ -> Zshift(n)::s
-let rec stack_args_size = function
- | Zapp v :: s -> Array.length v + stack_args_size s
- | Zshift(_)::s -> stack_args_size s
- | Zupdate(_)::s -> stack_args_size s
- | _ -> 0
-
-(* When used as an argument stack (only Zapp can appear) *)
-let rec decomp_stack = function
- | Zapp v :: s ->
- (match Array.length v with
- 0 -> decomp_stack s
- | 1 -> Some (v.(0), s)
- | _ ->
- Some (v.(0), (Zapp (Array.sub v 1 (Array.length v - 1)) :: s)))
- | _ -> None
-let array_of_stack s =
- let rec stackrec = function
- | [] -> []
- | Zapp args :: s -> args :: (stackrec s)
- | _ -> assert false
- in Array.concat (stackrec s)
-let rec stack_assign s p c = match s with
- | Zapp args :: s ->
- let q = Array.length args in
- if p >= q then
- Zapp args :: stack_assign s (p-q) c
- else
- (let nargs = Array.copy args in
- nargs.(p) <- c;
- Zapp nargs :: s)
- | _ -> s
-let rec stack_tail p s =
- if p = 0 then s else
- match s with
- | Zapp args :: s ->
- let q = Array.length args in
- if p >= q then stack_tail (p-q) s
- else Zapp (Array.sub args p (q-p)) :: s
- | _ -> failwith "stack_tail"
-let rec stack_nth s p = match s with
- | Zapp args :: s ->
- let q = Array.length args in
- if p >= q then stack_nth s (p-q)
- else args.(p)
- | _ -> raise Not_found
-
(* Lifting. Preserves sharing (useful only for cell with norm=Red).
lft_fconstr always create a new cell, while lift_fconstr avoids it
when the lift is 0. *)
@@ -807,16 +591,6 @@ let fapp_stack (m,stk) = zip m stk
(strip_update_shift, through get_arg). *)
(* optimised for the case where there are no shifts... *)
-let strip_update_shift head stk =
- assert (head.norm <> Red);
- let rec strip_rec h depth = function
- | Zshift(k)::s -> strip_rec (lift_fconstr k h) (depth+k) s
- | Zupdate(m)::s ->
- strip_rec (update m (h.norm,h.term)) depth s
- | stk -> (depth,stk) in
- strip_rec head 0 stk
-
-(* optimised for the case where there are no shifts... *)
let strip_update_shift_app head stk =
assert (head.norm <> Red);
let rec strip_rec rstk h depth = function
diff --git a/checker/closure.mli b/checker/closure.mli
index fba5b02b6..a1a23c6cb 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -49,33 +49,20 @@ module type RedFlagsSig = sig
(* Adds a reduction kind to a set *)
val red_add : reds -> red_kind -> reds
- (* Removes a reduction kind to a set *)
- val red_sub : reds -> red_kind -> reds
-
- (* Adds a reduction kind to a set *)
- val red_add_transparent : reds -> transparent_state -> reds
-
(* Build a reduction set from scratch = iter [red_add] on [no_red] *)
val mkflags : red_kind list -> reds
(* Tests if a reduction kind is set *)
val red_set : reds -> red_kind -> bool
-
- (* Gives the constant list *)
- val red_get_const : reds -> bool * evaluable_global_reference list
end
module RedFlags : RedFlagsSig
open RedFlags
-val beta : reds
-val betaiota : reds
val betadeltaiota : reds
val betaiotazeta : reds
val betadeltaiotanolet : reds
-val unfold_red : evaluable_global_reference -> reds
-
(***********************************************************************)
type table_key =
| ConstKey of constant
@@ -84,7 +71,6 @@ type table_key =
type 'a infos
val ref_value_cache: 'a infos -> table_key -> 'a option
-val info_flags: 'a infos -> reds
val create: ('a infos -> constr -> 'a) -> reds -> env -> 'a infos
(************************************************************************)
@@ -130,23 +116,13 @@ type stack_member =
and stack = stack_member list
-val empty_stack : stack
val append_stack : fconstr array -> stack -> stack
-val decomp_stack : stack -> (fconstr * stack) option
-val array_of_stack : stack -> fconstr array
-val stack_assign : stack -> int -> fconstr -> stack
-val stack_args_size : stack -> int
-val stack_tail : int -> stack -> stack
-val stack_nth : stack -> int -> fconstr
-
(* To lazy reduce a constr, create a [clos_infos] with
[create_clos_infos], inject the term to reduce with [inject]; then use
a reduction function *)
val inject : constr -> fconstr
-(* mk_atom: prevents a term from being evaluated *)
-val mk_atom : constr -> fconstr
val fterm_of : fconstr -> fterm
val term_of_fconstr : fconstr -> constr
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 70f16158e..664712dd5 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -76,14 +76,6 @@ let val_subst =
val_map ~name:"substitution"
val_subst_dom (val_tuple ~name:"substition range" [|val_mp;val_res|])
-
-let fold_subst fb fp =
- Umap.fold
- (fun k (mp,_) acc ->
- match k with
- | MBI mbid -> fb mbid mp acc
- | MPI mp1 -> fp mp1 mp acc)
-
let empty_subst = Umap.empty
let add_mbid mbid mp =
@@ -94,51 +86,9 @@ let add_mp mp1 mp2 =
let map_mbid mbid mp = add_mbid mbid mp empty_subst
let map_mp mp1 mp2 = add_mp mp1 mp2 empty_subst
-let add_inline_delta_resolver con =
- Deltamap.add (KN(user_con con)) (Inline None)
-
-let add_inline_constr_delta_resolver con cstr =
- Deltamap.add (KN(user_con con)) (Inline (Some cstr))
-
-let add_constant_delta_resolver con =
- Deltamap.add (KN(user_con con)) (Equiv (canonical_con con))
-
-let add_mind_delta_resolver mind =
- Deltamap.add (KN(user_mind mind)) (Equiv (canonical_mind mind))
-
-let add_mp_delta_resolver mp1 mp2 =
- Deltamap.add (MP mp1) (Prefix_equiv mp2)
-
let mp_in_delta mp =
Deltamap.mem (MP mp)
-let con_in_delta con resolver =
-try
- match Deltamap.find (KN(user_con con)) resolver with
- | Inline _ | Prefix_equiv _ -> false
- | Equiv _ -> true
-with
- Not_found -> false
-
-let mind_in_delta mind resolver =
-try
- match Deltamap.find (KN(user_mind mind)) resolver with
- | Inline _ | Prefix_equiv _ -> false
- | Equiv _ -> true
-with
- Not_found -> false
-
-let delta_of_mp resolve mp =
- try
- match Deltamap.find (MP mp) resolve with
- | Prefix_equiv mp1 -> mp1
- | _ -> anomaly "mod_subst: bad association in delta_resolver"
- with
- Not_found -> mp
-
-let remove_mp_delta_resolver resolver mp =
- Deltamap.remove (MP mp) resolver
-
exception Inline_kn
let rec find_prefix resolve mp =
@@ -213,16 +163,6 @@ let mind_of_delta2 resolve mind =
else
mind_of_kn_equiv kn1 new_kn
-
-
-let inline_of_delta resolver =
- let extract key hint l =
- match key,hint with
- |KN kn, Inline _ -> kn::l
- | _,_ -> l
- in
- Deltamap.fold extract resolver []
-
exception Not_inline
let constant_of_delta_with_inline resolve con =
@@ -341,33 +281,6 @@ let subst_mind0 sub mind =
with
No_subst -> Some mind
-let subst_con sub con =
- let kn1,kn2 = user_con con,canonical_con con in
- let mp1,dir,l = repr_kn kn1 in
- let mp2,_,_ = repr_kn kn2 in
- try
- let side,con',resolve =
- match subst_mp0 sub mp1,subst_mp0 sub mp2 with
- None,None ->raise No_subst
- | Some (mp',resolve),None -> User,(make_con_equiv mp' mp2 dir l), resolve
- | None, Some(mp',resolve)-> Canonical,(make_con_equiv mp1 mp' dir l), resolve
- | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical,
- (make_con_equiv mp1' mp2' dir l), resolve2
- in
- match constant_of_delta_with_inline resolve con' with
- None -> begin
- match side with
- |User ->
- let con = constant_of_delta resolve con' in
- con,Const con
- |Canonical ->
- let con = constant_of_delta2 resolve con' in
- con,Const con
- end
- | Some t -> con',t
- with No_subst -> con , Const con
-
-
let subst_con0 sub con =
let kn1,kn2 = user_con con,canonical_con con in
let mp1,dir,l = repr_kn kn1 in
diff --git a/checker/declarations.mli b/checker/declarations.mli
index b356ede17..ee44c8d5f 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -187,11 +187,6 @@ and module_type_body =
(* Substitutions *)
-val fold_subst :
- (mod_bound_id -> module_path -> 'a -> 'a) ->
- (module_path -> module_path -> 'a -> 'a) ->
- substitution -> 'a -> 'a
-
type 'a subst_fun = substitution -> 'a -> 'a
val empty_subst : substitution
diff --git a/checker/environ.ml b/checker/environ.ml
index a72aae91d..8c23a7e46 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -118,11 +118,6 @@ let add_constant kn cs env =
env_constants = new_constants } in
{ env with env_globals = new_globals }
-(* constant_type gives the type of a constant *)
-let constant_type env kn =
- let cb = lookup_constant kn env in
- cb.const_type
-
type const_evaluation_result = NoBody | Opaque
exception NotEvaluableConst of const_evaluation_result
@@ -134,10 +129,6 @@ let constant_value env kn =
| Some l_body -> force_constr l_body
| None -> raise (NotEvaluableConst NoBody)
-let constant_opt_value env cst =
- try Some (constant_value env cst)
- with NotEvaluableConst _ -> None
-
(* A global const is evaluable if it is defined and not opaque *)
let evaluable_constant cst env =
try let _ = constant_value env cst in true
diff --git a/checker/environ.mli b/checker/environ.mli
index 023acd0bf..add7c7060 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -50,11 +50,9 @@ val add_constraints : Univ.constraints -> env -> env
(* Constants *)
val lookup_constant : constant -> env -> Declarations.constant_body
val add_constant : constant -> Declarations.constant_body -> env -> env
-val constant_type : env -> constant -> Declarations.constant_type
type const_evaluation_result = NoBody | Opaque
exception NotEvaluableConst of const_evaluation_result
val constant_value : env -> constant -> constr
-val constant_opt_value : env -> constant -> constr option
val evaluable_constant : constant -> env -> bool
(* Inductives *)
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 756f43410..7a04cbfa3 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -81,8 +81,6 @@ let instantiate_params full t args sign =
if rem_args <> [] then fail();
substl subs ty
-let instantiate_partial_params = instantiate_params false
-
let full_inductive_instantiate mib params sign =
let dummy = Prop Null in
let t = mkArity (sign,dummy) in
@@ -98,10 +96,6 @@ let full_constructor_instantiate ((mind,_),(mib,_),params) =
(* Functions to build standard types related to inductive *)
-
-let number_of_inductives mib = Array.length mib.mind_packets
-let number_of_constructors mip = Array.length mip.mind_consnames
-
(*
Computing the actual sort of an applied or partially applied inductive type:
@@ -459,10 +453,6 @@ let subterm_var p renv =
try Lazy.force (List.nth renv.genv (p-1))
with Failure _ | Invalid_argument _ -> Not_subterm
-(* Add a variable and mark it as strictly smaller with information [spec]. *)
-let add_subterm renv (x,a,spec) =
- push_var renv (x,a,spec_of_tree spec)
-
let push_ctxt_renv renv ctxt =
let n = rel_context_length ctxt in
{ renv with
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 81154cba8..78408c68c 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -58,13 +58,6 @@ let rec list_split_assoc k rev_before = function
| (k',b)::after when k=k' -> rev_before,b,after
| h::tail -> list_split_assoc k (h::rev_before) tail
-let rec list_fold_map2 f e = function
- | [] -> (e,[],[])
- | h::t ->
- let e',h1',h2' = f e h in
- let e'',t1',t2' = list_fold_map2 f e' t in
- e'',h1'::t1',h2'::t2'
-
let check_definition_sub env cb1 cb2 =
let check_type env t1 t2 =
diff --git a/checker/modops.ml b/checker/modops.ml
index 61b0c3f05..b18b58a9f 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -23,8 +23,6 @@ let error_not_a_functor _ = error "Application of not a functor"
let error_incompatible_modtypes _ _ = error "Incompatible module types"
-let error_not_equal _ _ = error "Not equal modules"
-
let error_not_match l _ =
error ("Signature components for label "^string_of_label l^" do not match")
@@ -59,11 +57,6 @@ let destr_functor env mtb =
(arg_id,arg_t,body_t)
| _ -> error_not_a_functor mtb
-
-let is_functor = function
- | SEBfunctor (arg_id,arg_t,body_t) -> true
- | _ -> false
-
let module_body_of_type mp mtb =
{ mod_mp = mp;
mod_type = mtb.typ_expr;
@@ -73,14 +66,6 @@ let module_body_of_type mp mtb =
mod_delta = mtb.typ_delta;
mod_retroknowledge = []}
-let check_modpath_equiv env mp1 mp2 =
- if mp1=mp2 then () else
- (* let mb1=lookup_module mp1 env in
- let mb2=lookup_module mp2 env in
- if (delta_of_mp mb1.mod_delta mp1)=(delta_of_mp mb2.mod_delta mp2)
- then ()
- else*) error_not_equal mp1 mp2
-
let rec add_signature mp sign resolver env =
let add_one env (l,elem) =
let kn = make_kn mp empty_dirpath l in
diff --git a/checker/modops.mli b/checker/modops.mli
index f7aeb4dfa..b0bc0ee7f 100644
--- a/checker/modops.mli
+++ b/checker/modops.mli
@@ -31,8 +31,6 @@ val add_signature : module_path -> structure_body -> delta_resolver -> env -> en
(* adds a module and its components, but not the constraints *)
val add_module : module_body -> env -> env
-val check_modpath_equiv : env -> module_path -> module_path -> unit
-
val strengthen : env -> module_type_body -> module_path -> module_type_body
val subst_and_strengthen : module_body -> module_path -> env -> module_body
diff --git a/checker/reduction.ml b/checker/reduction.ml
index a86d23ecb..d8749f072 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -105,15 +105,6 @@ let beta_appvect c v =
| _ -> applist (substl env t, stack) in
stacklam [] c (Array.to_list v)
-let betazeta_appvect n c v =
- let rec stacklam n env t stack =
- if n = 0 then applist (substl env t, stack) else
- match t, stack with
- Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl
- | LetIn(_,b,_,c), _ -> stacklam (n-1) (b::env) c stack
- | _ -> anomaly "Not enough lambda/let's" in
- stacklam n [] c (Array.to_list v)
-
(********************************************************************)
(* Conversion *)
(********************************************************************)
@@ -371,31 +362,12 @@ let fconv cv_pb env t1 t2 =
if eq_constr t1 t2 then ()
else clos_fconv cv_pb env t1 t2
-let conv_cmp = fconv
let conv = fconv CONV
let conv_leq = fconv CUMUL
-let conv_leq_vecti env v1 v2 =
- array_fold_left2_i
- (fun i _ t1 t2 ->
- (try conv_leq env t1 t2
- with (NotConvertible|Invalid_argument _) ->
- raise (NotConvertibleVect i));
- ())
- ()
- v1
- v2
-
-(* option for conversion *)
-
-let vm_conv = ref fconv
-let set_vm_conv f = vm_conv := f
-let vm_conv cv_pb env t1 t2 =
- try
- !vm_conv cv_pb env t1 t2
- with Not_found | Invalid_argument _ ->
- (* If compilation fails, fall-back to closure conversion *)
- clos_fconv cv_pb env t1 t2
+(* option for conversion : no compilation for the checker *)
+
+let vm_conv = fconv
(********************************************************************)
(* Special-Purpose Reduction *)
@@ -450,9 +422,3 @@ let dest_arity env c =
| Sort s -> l,s
| _ -> error "not an arity"
-let is_arity env c =
- try
- let _ = dest_arity env c in
- true
- with UserError _ -> false
-
diff --git a/checker/reduction.mli b/checker/reduction.mli
index 0ca5f8368..6695fd031 100644
--- a/checker/reduction.mli
+++ b/checker/reduction.mli
@@ -29,7 +29,6 @@ type conv_pb = CONV | CUMUL
val conv : constr conversion_function
val conv_leq : constr conversion_function
-val conv_leq_vecti : constr array conversion_function
val vm_conv : conv_pb -> constr conversion_function
@@ -38,9 +37,6 @@ val vm_conv : conv_pb -> constr conversion_function
(* Builds an application node, reducing beta redexes it may produce. *)
val beta_appvect : constr -> constr array -> constr
-(* Builds an application node, reducing the [n] first beta-zeta redexes. *)
-val betazeta_appvect : int -> constr -> constr array -> constr
-
(* Pseudo-reduction rule Prod(x,A,B) a --> B[x\a] *)
val hnf_prod_applist : env -> constr -> constr list -> constr
@@ -52,4 +48,3 @@ val dest_prod : env -> constr -> rel_context * constr
val dest_prod_assum : env -> constr -> rel_context * constr
val dest_arity : env -> constr -> arity
-val is_arity : env -> constr -> bool
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 0b3ef54bb..eaf2aae80 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -18,7 +18,6 @@ open Environ
*)
let genv = ref empty_env
-let reset () = genv := empty_env
let get_env () = !genv
let set_engagement c =
diff --git a/checker/safe_typing.mli b/checker/safe_typing.mli
index 73f705182..986393b29 100644
--- a/checker/safe_typing.mli
+++ b/checker/safe_typing.mli
@@ -12,7 +12,6 @@ open Term
open Environ
(*i*)
-val reset : unit -> unit
val get_env : unit -> env
(* exporting and importing modules *)
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 8703f47ee..670f2783b 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -365,8 +365,3 @@ let check_subtypes env sup super =
(module_body_of_type sup.typ_mp sup) env in
check_modtypes env (strengthen env sup sup.typ_mp) super empty_subst
(map_mp super.typ_mp sup.typ_mp) false
-
-let check_equal env sup super =
- (*if sup<>super then*)
- check_modtypes env sup super empty_subst
- (map_mp super.typ_mp sup.typ_mp) true
diff --git a/checker/subtyping.mli b/checker/subtyping.mli
index 5092b3a12..07f48789d 100644
--- a/checker/subtyping.mli
+++ b/checker/subtyping.mli
@@ -14,6 +14,5 @@ open Environ
(*i*)
val check_subtypes : env -> module_type_body -> module_type_body -> unit
-val check_equal : env -> module_type_body -> module_type_body -> unit
diff --git a/checker/term.ml b/checker/term.ml
index 403fd7aa0..7d2241228 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -321,13 +321,6 @@ let val_rctxt = val_list val_rdecl
type named_declaration = identifier * constr option * constr
type rel_declaration = name * constr option * constr
-let map_named_declaration f (id, v, ty) = (id, Option.map f v, f ty)
-let map_rel_declaration = map_named_declaration
-
-let fold_named_declaration f (_, v, ty) a = f ty (Option.fold_right f v a)
-let fold_rel_declaration = fold_named_declaration
-
-
type named_context = named_declaration list
let empty_named_context = []
let fold_named_context f l ~init = List.fold_right f l init
@@ -438,7 +431,6 @@ let decompose_prod_n_assum n =
(***************************)
type arity = rel_context * sorts
-let val_arity = val_tuple ~name:"arity"[|val_rctxt;val_constr|]
let mkArity (sign,s) = it_mkProd_or_LetIn (Sort s) sign
diff --git a/checker/term.mli b/checker/term.mli
index 46ee12eca..0340c79b4 100644
--- a/checker/term.mli
+++ b/checker/term.mli
@@ -73,14 +73,6 @@ val subst1 : constr -> constr -> constr
type named_declaration = identifier * constr option * constr
type rel_declaration = name * constr option * constr
-val map_named_declaration :
- (constr -> constr) -> named_declaration -> named_declaration
-val map_rel_declaration :
- (constr -> constr) -> rel_declaration -> rel_declaration
-val fold_named_declaration :
- (constr -> 'a -> 'a) -> named_declaration -> 'a -> 'a
-val fold_rel_declaration :
- (constr -> 'a -> 'a) -> rel_declaration -> 'a -> 'a
type named_context = named_declaration list
val empty_named_context : named_context
val fold_named_context :
diff --git a/checker/type_errors.ml b/checker/type_errors.ml
index 2963b3ba3..126098325 100644
--- a/checker/type_errors.ml
+++ b/checker/type_errors.ml
@@ -92,9 +92,6 @@ let error_ill_formed_branch env c i actty expty =
raise (TypeError (env,
IllFormedBranch (c,i,nf_betaiota actty, nf_betaiota expty)))
-let error_generalization env nvar c =
- raise (TypeError (env, Generalization (nvar,c)))
-
let error_actual_type env j expty =
raise (TypeError (env, ActualType (j,expty)))
diff --git a/checker/type_errors.mli b/checker/type_errors.mli
index 036713538..17a210ef5 100644
--- a/checker/type_errors.mli
+++ b/checker/type_errors.mli
@@ -84,8 +84,6 @@ val error_number_branches : env -> unsafe_judgment -> int -> 'a
val error_ill_formed_branch : env -> constr -> int -> constr -> constr -> 'a
-val error_generalization : env -> name * constr -> unsafe_judgment -> 'a
-
val error_actual_type : env -> unsafe_judgment -> constr -> 'a
val error_cant_apply_not_functional :
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 97d122e32..c37f371f5 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -89,37 +89,6 @@ let check_args env c hyps =
with UserError _ | Not_found ->
error_reference_variables env c
-
-(* Checks if the given context of variables [hyps] is included in the
- current context of [env]. *)
-(*
-let check_hyps id env hyps =
- let hyps' = named_context env in
- if not (hyps_inclusion env hyps hyps') then
- error_reference_variables env id
-*)
-(* Instantiation of terms on real arguments. *)
-
-(* Make a type polymorphic if an arity *)
-
-let extract_level env p =
- let _,c = dest_prod_assum env p in
- match c with Sort (Type u) -> Some u | _ -> None
-
-let extract_context_levels env =
- List.fold_left
- (fun l (_,b,p) -> if b=None then extract_level env p::l else l) []
-
-let make_polymorphic_if_arity env t =
- let params, ccl = dest_prod_assum env t in
- match ccl with
- | Sort (Type u) ->
- let param_ccls = extract_context_levels env params in
- let s = { poly_param_levels = param_ccls; poly_level = u} in
- PolymorphicArity (params,s)
- | _ ->
- NonPolymorphicType t
-
(* Type of constants *)
let type_of_constant_knowing_parameters env t paramtyps =
@@ -133,9 +102,6 @@ let type_of_constant_knowing_parameters env t paramtyps =
let type_of_constant_type env t =
type_of_constant_knowing_parameters env t [||]
-let type_of_constant env cst =
- type_of_constant_type env (constant_type env cst)
-
let judge_of_constant_knowing_parameters env cst paramstyp =
let c = Const cst in
let cb =
@@ -404,12 +370,9 @@ and execute_recdef env (names,lar,vdef) i =
and execute_array env = Array.map (execute env)
-and execute_list env = List.map (execute env)
-
(* Derived functions *)
let infer env constr = execute env constr
let infer_type env constr = execute_type env constr
-let infer_v env cv = execute_array env cv
(* Typing of several terms. *)
diff --git a/checker/validate.ml b/checker/validate.ml
index 36c668af3..c5e0bd34d 100644
--- a/checker/validate.ml
+++ b/checker/validate.ml
@@ -117,9 +117,6 @@ let val_enum s n = val_sum s n [||]
let rec val_rec_sum name cc f ctx o =
val_sum name cc (f (overr (ctx/name) (val_rec_sum name cc f))) ctx o
-let rec val_rectype f o =
- f (val_rectype f) o
-
(**************************************************************************)
(* Builtin types *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 09:34:28 +0000