diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-24 14:24:52 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-24 14:24:52 +0000 |
commit | 13964049858427c5447394c733011f7a0c4f4117 (patch) | |
tree | 08827bd1e7e4c54f10c1c77d1d1bf9509d6f9054 /checker | |
parent | 6e88e153b42dadb0ded217ad85916ef071455f8b (diff) |
Checker: remove some dead code
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13462 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'checker')
-rw-r--r-- | checker/check.ml | 15 | ||||
-rw-r--r-- | checker/checker.ml | 5 | ||||
-rw-r--r-- | checker/closure.ml | 228 | ||||
-rw-r--r-- | checker/closure.mli | 24 | ||||
-rw-r--r-- | checker/declarations.ml | 87 | ||||
-rw-r--r-- | checker/declarations.mli | 5 | ||||
-rw-r--r-- | checker/environ.ml | 9 | ||||
-rw-r--r-- | checker/environ.mli | 2 | ||||
-rw-r--r-- | checker/inductive.ml | 10 | ||||
-rw-r--r-- | checker/mod_checking.ml | 7 | ||||
-rw-r--r-- | checker/modops.ml | 15 | ||||
-rw-r--r-- | checker/modops.mli | 2 | ||||
-rw-r--r-- | checker/reduction.ml | 40 | ||||
-rw-r--r-- | checker/reduction.mli | 5 | ||||
-rw-r--r-- | checker/safe_typing.ml | 1 | ||||
-rw-r--r-- | checker/safe_typing.mli | 1 | ||||
-rw-r--r-- | checker/subtyping.ml | 5 | ||||
-rw-r--r-- | checker/subtyping.mli | 1 | ||||
-rw-r--r-- | checker/term.ml | 8 | ||||
-rw-r--r-- | checker/term.mli | 8 | ||||
-rw-r--r-- | checker/type_errors.ml | 3 | ||||
-rw-r--r-- | checker/type_errors.mli | 2 | ||||
-rw-r--r-- | checker/typeops.ml | 37 | ||||
-rw-r--r-- | checker/validate.ml | 3 |
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 *) |