Skip to content

Commit

Permalink
Checker: remove some dead code
Browse files Browse the repository at this point in the history 
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13462 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information
letouzey committed Sep 24, 2010
1 parent 6e88e15 commit 1396404
Show file tree
Hide file tree
Showing 24 changed files with 6 additions and 517 deletions.
15 changes: 2 additions & 13 deletions checker/check.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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 *)

Expand Down Expand Up @@ -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
Expand Down
5 changes: 0 additions & 5 deletions checker/checker.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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: "
Expand Down
228 changes: 1 addition & 227 deletions checker/closure.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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 *)


Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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. *)
Expand All @@ -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
Expand All @@ -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. *)
Expand Down Expand Up @@ -806,16 +590,6 @@ let fapp_stack (m,stk) = zip m stk
(strip_update_shift_app), a fix (get_nth_arg) or an abstraction
(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);
Expand Down
Loading

0 comments on commit 1396404

Please sign in to comment.