summaryrefslogtreecommitdiff
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/check.ml32
-rw-r--r--checker/check_stat.ml4
-rw-r--r--checker/check_stat.mli2
-rw-r--r--checker/checker.ml138
-rw-r--r--checker/closure.ml257
-rw-r--r--checker/closure.mli32
-rw-r--r--checker/declarations.ml713
-rw-r--r--checker/declarations.mli48
-rw-r--r--checker/environ.ml17
-rw-r--r--checker/environ.mli2
-rw-r--r--checker/indtypes.ml19
-rw-r--r--checker/indtypes.mli4
-rw-r--r--checker/inductive.ml352
-rw-r--r--checker/inductive.mli11
-rw-r--r--checker/mod_checking.ml40
-rw-r--r--checker/mod_checking.mli9
-rw-r--r--checker/modops.ml61
-rw-r--r--checker/modops.mli6
-rw-r--r--checker/reduction.ml92
-rw-r--r--checker/reduction.mli11
-rw-r--r--checker/safe_typing.ml153
-rw-r--r--checker/safe_typing.mli21
-rw-r--r--checker/subtyping.ml57
-rw-r--r--checker/subtyping.mli5
-rw-r--r--checker/term.ml41
-rw-r--r--checker/term.mli20
-rw-r--r--checker/type_errors.ml9
-rw-r--r--checker/type_errors.mli8
-rw-r--r--checker/typeops.ml43
-rw-r--r--checker/typeops.mli4
-rw-r--r--checker/validate.ml120
31 files changed, 959 insertions, 1372 deletions
diff --git a/checker/check.ml b/checker/check.ml
index 40119a7e..bb42b949 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -1,18 +1,15 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: library.ml 9679 2007-02-24 15:22:07Z herbelin $ *)
-
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 =
@@ -42,7 +39,7 @@ type compilation_unit_name = dir_path
type library_disk = {
md_name : compilation_unit_name;
- md_compiled : Safe_typing.compiled_library;
+ md_compiled : Safe_typing.LightenLibrary.lightened_compiled_library;
md_objects : library_objects;
md_deps : (compilation_unit_name * Digest.t) list;
md_imports : compilation_unit_name list }
@@ -155,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
@@ -191,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 *)
@@ -269,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
@@ -283,10 +270,10 @@ let with_magic_number_check f a =
(************************************************************************)
(* Internalise libraries *)
-let mk_library md f digest = {
+let mk_library md f table digest = {
library_name = md.md_name;
library_filename = f;
- library_compiled = md.md_compiled;
+ library_compiled = Safe_typing.LightenLibrary.load table md.md_compiled;
library_deps = md.md_deps;
library_digest = digest }
@@ -300,20 +287,21 @@ let depgraph = ref LibraryMap.empty
let intern_from_file (dir, f) =
Flags.if_verbose msg (str"[intern "++str f++str" ...");
- let (md,digest) =
+ let (md,table,digest) =
try
let ch = with_magic_number_check raw_intern_library f in
let (md:library_disk) = System.marshal_in ch in
let digest = System.marshal_in ch in
+ let table = (System.marshal_in ch : Safe_typing.LightenLibrary.table) in
close_in ch;
if dir <> md.md_name then
errorlabstrm "load_physical_library"
(name_clash_message dir md.md_name f);
Flags.if_verbose msgnl(str" done]");
- md,digest
+ md,table,digest
with e -> Flags.if_verbose msgnl(str" failed!]"); raise e in
depgraph := LibraryMap.add md.md_name md.md_deps !depgraph;
- mk_library md f digest
+ mk_library md f table digest
let get_deps (dir, f) =
try LibraryMap.find dir !depgraph
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index 88f2374b..5f28269e 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -37,7 +37,7 @@ let cst_filter f csts =
(fun c ce acc -> if f c ce then c::acc else acc)
csts []
-let is_ax _ cb = cb.const_body = None
+let is_ax _ cb = not (constant_has_body cb)
let pr_ax csts =
let axs = cst_filter is_ax csts in
diff --git a/checker/check_stat.mli b/checker/check_stat.mli
index d39eb454..353edda6 100644
--- a/checker/check_stat.mli
+++ b/checker/check_stat.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/checker/checker.ml b/checker/checker.ml
index 76f81264..34ba7b01 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -1,13 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqtop.ml 10153 2007-09-28 18:00:45Z glondu $ *)
-
+open Compat
open Pp
open Util
open System
@@ -32,11 +31,11 @@ let parse_dir s =
decoupe_dirs [] 0
let dirpath_of_string s =
match parse_dir s with
- [] -> invalid_arg "dirpath_of_string"
+ [] -> Check.default_root_prefix
| dir -> make_dirpath (List.map id_of_string dir)
let path_of_string s =
match parse_dir s with
- [] -> invalid_arg "dirpath_of_string"
+ [] -> invalid_arg "path_of_string"
| l::dir -> {dirpath=dir; basename=l}
let (/) = Filename.concat
@@ -73,17 +72,17 @@ let convert_string d =
flush_all ();
failwith "caught"
-let add_rec_path ~unix_path:dir ~coq_root:coq_dirpath =
- if exists_dir dir then
- let dirs = all_subdirs dir in
- let prefix = repr_dirpath coq_dirpath in
+let add_rec_path ~unix_path ~coq_root =
+ if exists_dir unix_path then
+ let dirs = all_subdirs ~unix_path in
+ let prefix = repr_dirpath coq_root in
let convert_dirs (lp,cp) =
(lp,make_dirpath (List.map convert_string (List.rev cp)@prefix)) in
let dirs = map_succeed convert_dirs dirs in
List.iter Check.add_load_path dirs;
- Check.add_load_path (dir,coq_dirpath)
+ Check.add_load_path (unix_path, coq_root)
else
- msg_warning (str ("Cannot open " ^ dir))
+ msg_warning (str ("Cannot open " ^ unix_path))
(* By the option -include -I or -R of the command line *)
let includes = ref []
@@ -92,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)
@@ -106,24 +102,27 @@ let set_rec_include d p =
let init_load_path () =
let coqlib = Envars.coqlib () in
let user_contrib = coqlib/"user-contrib" in
+ let xdg_dirs = Envars.xdg_dirs in
+ let coqpath = Envars.coqpath in
let plugins = coqlib/"plugins" in
- (* first user-contrib *)
- if Sys.file_exists user_contrib then
- add_rec_path user_contrib Check.default_root_prefix;
+ (* NOTE: These directories are searched from last to first *)
+ (* first standard library *)
+ add_rec_path ~unix_path:(coqlib/"theories") ~coq_root:(Names.make_dirpath[coq_root]);
(* then plugins *)
- add_rec_path plugins (Names.make_dirpath [coq_root]);
- (* then standard library *)
-(* List.iter
- (fun (s,alias) ->
- add_rec_path (coqlib/s) ([alias; coq_root]))
- theories_dirs_map;*)
- add_rec_path (coqlib/"theories") (Names.make_dirpath[coq_root]);
+ add_rec_path ~unix_path:plugins ~coq_root:(Names.make_dirpath [coq_root]);
+ (* then user-contrib *)
+ if Sys.file_exists user_contrib then
+ add_rec_path ~unix_path:user_contrib ~coq_root:Check.default_root_prefix;
+ (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME *)
+ List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix) xdg_dirs;
+ (* then directories in COQPATH *)
+ List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix) coqpath;
(* then current directory *)
- add_path "." Check.default_root_prefix;
+ add_path ~unix_path:"." ~coq_root:Check.default_root_prefix;
(* additional loadpath, given with -I -include -R options *)
List.iter
- (fun (s,alias,reci) ->
- if reci then add_rec_path s alias else add_path s alias)
+ (fun (unix_path, coq_root, reci) ->
+ if reci then add_rec_path ~unix_path ~coq_root else add_path ~unix_path ~coq_root)
(List.rev !includes);
includes := []
@@ -168,43 +167,41 @@ let version () =
let print_usage_channel co command =
output_string co command;
- output_string co "Coq options are:\n";
+ output_string co "coqchk options are:\n";
output_string co
-" -I dir -as coqdir map physical dir to logical coqdir
- -I dir map directory dir to the empty logical path
- -include dir (idem)
- -R dir -as coqdir recursively map physical dir to logical coqdir
- -R dir coqdir (idem)
-
- -admit module load module and dependencies without checking
- -norec module check module but admit dependencies without checking
-
- -where print Coq's standard library location and exit
- -v print Coq version and exit
- -boot boot mode
- -o, --output-context print the list of assumptions
- -m, --memoty print the maximum heap size
- -silent disable trace of constants being checked
-
- -impredicative-set set sort Set impredicative
-
- -h, --help print this list of options
-"
+" -I dir -as coqdir map physical dir to logical coqdir\
+\n -I dir map directory dir to the empty logical path\
+\n -include dir (idem)\
+\n -R dir -as coqdir recursively map physical dir to logical coqdir\
+\n -R dir coqdir (idem)\
+\n\
+\n -admit module load module and dependencies without checking\
+\n -norec module check module but admit dependencies without checking\
+\n\
+\n -where print coqchk's standard library location and exit\
+\n -v print coqchk version and exit\
+\n -boot boot mode\
+\n -o, --output-context print the list of assumptions\
+\n -m, --memory print the maximum heap size\
+\n -silent disable trace of constants being checked\
+\n\
+\n -impredicative-set set sort Set impredicative\
+\n\
+\n -h, --help print this list of options\
+\n"
(* print the usage on standard error *)
let print_usage = print_usage_channel stderr
let print_usage_coqtop () =
- print_usage "Usage: coqchk <options>\n\n"
+ print_usage "Usage: coqchk <options> modules\n\n"
let usage () =
print_usage_coqtop ();
flush stderr;
exit 1
-let warning s = msg_warning (str s)
-
open Type_errors
let anomaly_string () = str "Anomaly: "
@@ -239,14 +236,9 @@ let rec explain_exn = function
| Anomaly (s,pps) ->
hov 1 (anomaly_string () ++ where s ++ pps ++ report ())
| Match_failure(filename,pos1,pos2) ->
- hov 1 (anomaly_string () ++ str "Match failure in file " ++ str (guill filename) ++
- if Sys.ocaml_version = "3.06" then
- (str " from character " ++ int pos1 ++
- str " to " ++ int pos2)
- else
- (str " at line " ++ int pos1 ++
- str " character " ++ int pos2)
- ++ report ())
+ hov 1 (anomaly_string () ++ str "Match failure in file " ++
+ str (guill filename) ++ str " at line " ++ int pos1 ++
+ str " character " ++ int pos2 ++ report ())
| Not_found ->
hov 0 (anomaly_string () ++ str "uncaught exception Not_found" ++ report ())
| Failure s ->
@@ -274,22 +266,17 @@ let rec explain_exn = function
(* let ctx = Check.get_env() in
hov 0
(str "Error:" ++ spc () ++ Himsg.explain_inductive_error ctx e)*)
- | Stdpp.Exc_located (loc,exc) ->
+ | Loc.Exc_located (loc,exc) ->
hov 0 ((if loc = dummy_loc then (mt ())
else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
++ explain_exn exc)
| Assert_failure (s,b,e) ->
hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++
- (if s <> "" then
- if Sys.ocaml_version = "3.06" then
- (str ("(file \"" ^ s ^ "\", characters ") ++
- int b ++ str "-" ++ int e ++ str ")")
- else
- (str ("(file \"" ^ s ^ "\", line ") ++ int b ++
- str ", characters " ++ int e ++ str "-" ++
- int (e+6) ++ str ")")
- else
- (mt ())) ++
+ (if s = "" then mt ()
+ else
+ (str ("(file \"" ^ s ^ "\", line ") ++ int b ++
+ str ", characters " ++ int e ++ str "-" ++
+ int (e+6) ++ str ")")) ++
report ())
| reraise ->
hov 0 (anomaly_string () ++ str "Uncaught exception " ++
@@ -298,8 +285,15 @@ let rec explain_exn = function
let parse_args argv =
let rec parse = function
| [] -> ()
- | "-impredicative-set" :: rem ->
- set_engagement Declarations.ImpredicativeSet; parse rem
+ | "-impredicative-set" :: rem ->
+ set_engagement Declarations.ImpredicativeSet; parse rem
+
+ | "-coqlib" :: s :: rem ->
+ if not (exists_dir s) then
+ (msgnl (str ("Directory '"^s^"' does not exist")); exit 1);
+ Flags.coqlib := s;
+ Flags.coqlib_spec := true;
+ parse rem
| ("-I"|"-include") :: d :: "-as" :: p :: rem -> set_include d p; parse rem
| ("-I"|"-include") :: d :: "-as" :: [] -> usage ()
diff --git a/checker/closure.ml b/checker/closure.ml
index da25b3b3..033e2bd7 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: closure.ml 9983 2007-07-12 17:15:22Z barras $ *)
-
open Util
open Pp
open Term
@@ -54,6 +52,9 @@ type transparent_state = Idpred.t * Cpred.t
let all_opaque = (Idpred.empty, Cpred.empty)
let all_transparent = (Idpred.full, Cpred.full)
+let is_transparent_variable (ids, _) id = Idpred.mem id ids
+let is_transparent_constant (_, csts) cst = Cpred.mem cst csts
+
module type RedFlagsSig = sig
type reds
type red_kind
@@ -65,11 +66,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
@@ -114,21 +112,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
@@ -146,160 +129,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 *)
@@ -336,8 +173,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)
@@ -447,9 +282,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. *)
@@ -472,7 +304,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
@@ -486,52 +317,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. *)
@@ -643,7 +428,7 @@ let optimise_closure env c =
let (c',(_,s)) = compact_constr (0,[]) c 1 in
let env' =
Array.map (fun i -> clos_rel env i) (Array.of_list s) in
- (subs_cons (env', ESID 0),c')
+ (subs_cons (env', subs_id 0),c')
let mk_lambda env t =
let (env,t) = optimise_closure env t in
@@ -774,7 +559,7 @@ let term_of_fconstr =
| FFix(fx,e) when is_subs_id e & is_lift_id lfts -> Fix fx
| FCoFix(cfx,e) when is_subs_id e & is_lift_id lfts -> CoFix cfx
| _ -> to_constr term_of_fconstr_lift lfts v in
- term_of_fconstr_lift ELID
+ term_of_fconstr_lift el_id
@@ -809,16 +594,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
@@ -835,15 +610,15 @@ let strip_update_shift_app head stk =
let get_nth_arg head n stk =
assert (head.norm <> Red);
- let rec strip_rec rstk h depth n = function
+ let rec strip_rec rstk h n = function
| Zshift(k) as e :: s ->
- strip_rec (e::rstk) (lift_fconstr k h) (depth+k) n s
+ strip_rec (e::rstk) (lift_fconstr k h) n s
| Zapp args::s' ->
let q = Array.length args in
if n >= q
then
strip_rec (Zapp args::rstk)
- {norm=h.norm;term=FApp(h,args)} depth (n-q) s'
+ {norm=h.norm;term=FApp(h,args)} (n-q) s'
else
let bef = Array.sub args 0 n in
let aft = Array.sub args (n+1) (q-n-1) in
@@ -851,9 +626,9 @@ let get_nth_arg head n stk =
List.rev (if n = 0 then rstk else (Zapp bef :: rstk)) in
(Some (stk', args.(n)), append_stack aft s')
| Zupdate(m)::s ->
- strip_rec rstk (update m (h.norm,h.term)) depth n s
+ strip_rec rstk (update m (h.norm,h.term)) n s
| s -> (None, List.rev rstk @ s) in
- strip_rec [] head 0 n stk
+ strip_rec [] head n stk
(* Beta reduction: look for an applied argument in the stack.
Since the encountered update marks are removed, h must be a whnf *)
@@ -876,6 +651,12 @@ let rec get_args n tys f e stk =
get_args (n-na) etys f (subs_cons(l,e)) s
| _ -> (Inr {norm=Cstr;term=FLambda(n,tys,f,e)}, stk)
+(* Eta expansion: add a reference to implicit surrounding lambda at end of stack *)
+let rec eta_expand_stack = function
+ | (Zapp _ | Zfix _ | Zcase _ | Zshift _ | Zupdate _ as e) :: s ->
+ e :: eta_expand_stack s
+ | [] ->
+ [Zshift 1; Zapp [|{norm=Norm; term= FRel 1}|]]
(* Iota reduction: extract the arguments to be passed to the Case
branches *)
@@ -1025,7 +806,7 @@ let kh info v stk = fapp_stack(kni info v stk)
let whd_val info v =
with_stats (lazy (term_of_fconstr (kh info v [])))
-let inject = mk_clos (ESID 0)
+let inject = mk_clos (subs_id 0)
let whd_stack infos m stk =
let k = kni infos m stk in
diff --git a/checker/closure.mli b/checker/closure.mli
index 12cee770..707a51f9 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: closure.mli 9902 2007-06-21 17:01:21Z herbelin $ i*)
-
(*i*)
open Pp
open Names
@@ -32,6 +30,9 @@ type transparent_state = Idpred.t * Cpred.t
val all_opaque : transparent_state
val all_transparent : transparent_state
+val is_transparent_variable : transparent_state -> variable -> bool
+val is_transparent_constant : transparent_state -> constant -> bool
+
(* Sets of reduction kinds. *)
module type RedFlagsSig = sig
type reds
@@ -51,33 +52,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
@@ -86,7 +74,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
(************************************************************************)
@@ -132,23 +119,14 @@ 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
+val eta_expand_stack : stack -> stack
(* 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 0deb80a2..890996d1 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -20,7 +20,7 @@ type polymorphic_arity = {
poly_level : Univ.universe;
}
let val_pol_arity =
- val_tuple"polyorphic_arity"[|val_list(val_opt val_univ);val_univ|]
+ val_tuple ~name:"polyorphic_arity"[|val_list(val_opt val_univ);val_univ|]
type constant_type =
| NonPolymorphicType of constr
@@ -29,256 +29,164 @@ type constant_type =
let val_cst_type =
val_sum "constant_type" 0 [|[|val_constr|];[|val_rctxt;val_pol_arity|]|]
-
-type substitution_domain =
- | MBI of mod_bound_id
- | MPI of module_path
-
-let val_subst_dom =
- val_sum "substitution_domain" 0 [|[|val_uid|];[|val_mp|]|]
-
-module Umap = Map.Make(struct
- type t = substitution_domain
- let compare = Pervasives.compare
- end)
-
+(** Substitutions, code imported from kernel/mod_subst *)
type delta_hint =
- Inline of constr option
+ | Inline of int * constr option
| Equiv of kernel_name
- | Prefix_equiv of module_path
-
-type delta_key =
- KN of kernel_name
- | MP of module_path
-module Deltamap = Map.Make(struct
- type t = delta_key
- let compare = Pervasives.compare
- end)
-type delta_resolver = delta_hint Deltamap.t
+module Deltamap = struct
+ type t = module_path MPmap.t * delta_hint KNmap.t
+ let empty = MPmap.empty, KNmap.empty
+ let add_kn kn hint (mm,km) = (mm,KNmap.add kn hint km)
+ let add_mp mp mp' (mm,km) = (MPmap.add mp mp' mm, km)
+ let remove_mp mp (mm,km) = (MPmap.remove mp mm, km)
+ let find_mp mp map = MPmap.find mp (fst map)
+ let find_kn kn map = KNmap.find kn (snd map)
+ let mem_mp mp map = MPmap.mem mp (fst map)
+ let mem_kn kn map = KNmap.mem kn (snd map)
+ let fold_kn f map i = KNmap.fold f (snd map) i
+ let fold fmp fkn (mm,km) i =
+ MPmap.fold fmp mm (KNmap.fold fkn km i)
+ let join map1 map2 = fold add_mp add_kn map1 map2
+end
+
+type delta_resolver = Deltamap.t
let empty_delta_resolver = Deltamap.empty
+module MBImap = Map.Make
+ (struct
+ type t = mod_bound_id
+ let compare = Pervasives.compare
+ end)
+
+module Umap = struct
+ type 'a t = 'a MPmap.t * 'a MBImap.t
+ let empty = MPmap.empty, MBImap.empty
+ let is_empty (m1,m2) = MPmap.is_empty m1 && MBImap.is_empty m2
+ let add_mbi mbi x (m1,m2) = (m1,MBImap.add mbi x m2)
+ let add_mp mp x (m1,m2) = (MPmap.add mp x m1, m2)
+ let find_mp mp map = MPmap.find mp (fst map)
+ let find_mbi mbi map = MBImap.find mbi (snd map)
+ let mem_mp mp map = MPmap.mem mp (fst map)
+ let mem_mbi mbi map = MBImap.mem mbi (snd map)
+ let iter_mbi f map = MBImap.iter f (snd map)
+ let fold fmp fmbi (m1,m2) i =
+ MPmap.fold fmp m1 (MBImap.fold fmbi m2 i)
+ let join map1 map2 = fold add_mp add_mbi map1 map2
+end
+
type substitution = (module_path * delta_resolver) Umap.t
type 'a subst_fun = substitution -> 'a -> 'a
-let val_res_dom =
- val_sum "delta_key" 0 [|[|val_kn|];[|val_mp|]|]
+let empty_subst = Umap.empty
-let val_res =
- val_map ~name:"delta_resolver"
- val_res_dom
- (val_sum "delta_hint" 0 [|[|val_opt val_constr|];[|val_kn|];[|val_mp|]|])
+let is_empty_subst = Umap.is_empty
-let val_subst =
- val_map ~name:"substitution"
- val_subst_dom (val_tuple "substition range" [|val_mp;val_res|])
+let val_delta_hint =
+ val_sum "delta_hint" 0
+ [|[|val_int; val_opt val_constr|];[|val_kn|]|]
+let val_res =
+ val_tuple ~name:"delta_resolver"
+ [|val_map ~name:"delta_resolver" val_mp val_mp;
+ val_map ~name:"delta_resolver" val_kn val_delta_hint|]
-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 val_mp_res = val_tuple [|val_mp;val_res|]
-let empty_subst = Umap.empty
+let val_subst =
+ val_tuple ~name:"substitution"
+ [|val_map ~name:"substitution" val_mp val_mp_res;
+ val_map ~name:"substitution" val_uid val_mp_res|]
-let add_mbid mbid mp =
- Umap.add (MBI mbid) (mp,empty_delta_resolver)
-let add_mp mp1 mp2 =
- Umap.add (MPI mp1) (mp2,empty_delta_resolver)
+let add_mbid mbid mp = Umap.add_mbi mbid (mp,empty_delta_resolver)
+let add_mp mp1 mp2 = Umap.add_mp mp1 (mp2,empty_delta_resolver)
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 delta_of_kn resolve kn =
- try
- match Deltamap.find (KN kn) resolve with
- | Equiv kn1 -> kn1
- | Inline _ -> kn
- | _ -> anomaly
- "mod_subst: bad association in delta_resolver"
- with
- Not_found -> kn
-
-let remove_mp_delta_resolver resolver mp =
- Deltamap.remove (MP mp) resolver
-
-exception Inline_kn
+let mp_in_delta mp =
+ Deltamap.mem_mp mp
-let rec find_prefix resolve mp =
+let rec find_prefix resolve mp =
let rec sub_mp = function
- | MPdot(mp,l) as mp_sup ->
- (try
- match Deltamap.find (MP mp_sup) resolve with
- | Prefix_equiv mp1 -> mp1
- | _ -> anomaly
- "mod_subst: bad association in delta_resolver"
- with
- Not_found -> MPdot(sub_mp mp,l))
- | p ->
- match Deltamap.find (MP p) resolve with
- | Prefix_equiv mp1 -> mp1
- | _ -> anomaly
- "mod_subst: bad association in delta_resolver"
+ | MPdot(mp,l) as mp_sup ->
+ (try Deltamap.find_mp mp_sup resolve
+ with Not_found -> MPdot(sub_mp mp,l))
+ | p -> Deltamap.find_mp p resolve
in
- try
- sub_mp mp
- with
- Not_found -> mp
-
+ try sub_mp mp with Not_found -> mp
+
+(** Nota: the following function is slightly different in mod_subst
+ PL: Is it on purpose ? *)
+
let solve_delta_kn resolve kn =
- try
- match Deltamap.find (KN kn) resolve with
- | Equiv kn1 -> kn1
- | Inline _ -> raise Inline_kn
- | _ -> anomaly
- "mod_subst: bad association in delta_resolver"
- with
- Not_found | Inline_kn ->
- let mp,dir,l = repr_kn kn in
- let new_mp = find_prefix resolve mp in
- if mp == new_mp then
- kn
- else
- make_kn new_mp dir l
-
+ try
+ match Deltamap.find_kn kn resolve with
+ | Equiv kn1 -> kn1
+ | Inline _ -> raise Not_found
+ with Not_found ->
+ let mp,dir,l = repr_kn kn in
+ let new_mp = find_prefix resolve mp in
+ if mp == new_mp then
+ kn
+ else
+ make_kn new_mp dir l
+
+let gen_of_delta resolve x kn fix_can =
+ try
+ let new_kn = solve_delta_kn resolve kn in
+ if kn == new_kn then x else fix_can new_kn
+ with _ -> x
let constant_of_delta resolve con =
let kn = user_con con in
- let new_kn = solve_delta_kn resolve kn in
- if kn == new_kn then
- con
- else
- constant_of_kn_equiv kn new_kn
-
+ gen_of_delta resolve con kn (constant_of_kn_equiv kn)
+
let constant_of_delta2 resolve con =
- let kn = canonical_con con in
- let kn1 = user_con con in
- let new_kn = solve_delta_kn resolve kn in
- if kn == new_kn then
- con
- else
- constant_of_kn_equiv kn1 new_kn
+ let kn, kn' = canonical_con con, user_con con in
+ gen_of_delta resolve con kn (constant_of_kn_equiv kn')
let mind_of_delta resolve mind =
let kn = user_mind mind in
- let new_kn = solve_delta_kn resolve kn in
- if kn == new_kn then
- mind
- else
- mind_of_kn_equiv kn new_kn
-
-let mind_of_delta2 resolve mind =
- let kn = canonical_mind mind in
- let kn1 = user_mind mind in
- let new_kn = solve_delta_kn resolve kn in
- if kn == new_kn then
- mind
- else
- mind_of_kn_equiv kn1 new_kn
-
+ gen_of_delta resolve mind kn (mind_of_kn_equiv kn)
+let mind_of_delta2 resolve mind =
+ let kn, kn' = canonical_mind mind, user_mind mind in
+ gen_of_delta resolve mind kn (mind_of_kn_equiv 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 []
+let find_inline_of_delta kn resolve =
+ match Deltamap.find_kn kn resolve with
+ | Inline (_,o) -> o
+ | _ -> raise Not_found
-exception Not_inline
-
let constant_of_delta_with_inline resolve con =
let kn1,kn2 = canonical_con con,user_con con in
- try
- match Deltamap.find (KN kn2) resolve with
- | Inline None -> None
- | Inline (Some const) -> Some const
- | _ -> raise Not_inline
- with
- Not_found | Not_inline ->
- try match Deltamap.find (KN kn1) resolve with
- | Inline None -> None
- | Inline (Some const) -> Some const
- | _ -> raise Not_inline
- with
- Not_found | Not_inline -> None
+ try find_inline_of_delta kn2 resolve
+ with Not_found ->
+ try find_inline_of_delta kn1 resolve
+ with Not_found -> None
let subst_mp0 sub mp = (* 's like subst *)
let rec aux mp =
match mp with
- | MPfile sid ->
- let mp',resolve = Umap.find (MPI (MPfile sid)) sub in
- mp',resolve
+ | MPfile sid -> Umap.find_mp mp sub
| MPbound bid ->
begin
- try
- let mp',resolve = Umap.find (MBI bid) sub in
- mp',resolve
- with Not_found ->
- let mp',resolve = Umap.find (MPI mp) sub in
- mp',resolve
+ try Umap.find_mbi bid sub
+ with Not_found -> Umap.find_mp mp sub
end
| MPdot (mp1,l) as mp2 ->
begin
- try
- let mp',resolve = Umap.find (MPI mp2) sub in
- mp',resolve
+ try Umap.find_mp mp2 sub
with Not_found ->
let mp1',resolve = aux mp1 in
- MPdot (mp1',l),resolve
+ MPdot (mp1',l),resolve
end
in
- try
- Some (aux mp)
- with Not_found -> None
+ try Some (aux mp) with Not_found -> None
let subst_mp sub mp =
match subst_mp0 sub mp with
@@ -305,127 +213,58 @@ type sideconstantsubst =
| User
| Canonical
+
+let gen_subst_mp f sub mp1 mp2 =
+ match subst_mp0 sub mp1, subst_mp0 sub mp2 with
+ | None, None -> raise No_subst
+ | Some (mp',resolve), None -> User, (f mp' mp2), resolve
+ | None, Some (mp',resolve) -> Canonical, (f mp1 mp'), resolve
+ | Some (mp1',_), Some (mp2',resolve2) -> Canonical, (f mp1' mp2'), resolve2
+
let subst_ind sub mind =
- let kn1,kn2 = user_mind mind,canonical_mind mind in
+ let kn1,kn2 = user_mind mind, canonical_mind mind in
let mp1,dir,l = repr_kn kn1 in
let mp2,_,_ = repr_kn kn2 in
- try
- let side,mind',resolve =
- match subst_mp0 sub mp1,subst_mp0 sub mp2 with
- None,None ->raise No_subst
- | Some (mp',resolve),None -> User,(make_mind_equiv mp' mp2 dir l), resolve
- | None, Some(mp',resolve)-> Canonical,(make_mind_equiv mp1 mp' dir l), resolve
- | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical,
- (make_mind_equiv mp1' mp2' dir l), resolve2
- in
- match side with
- |User ->
- let mind = mind_of_delta resolve mind' in
- mind
- |Canonical ->
- let mind = mind_of_delta2 resolve mind' in
- mind
- with
- No_subst -> mind
-
-let subst_mind0 sub mind =
- let kn1,kn2 = user_mind mind,canonical_mind mind in
- let mp1,dir,l = repr_kn kn1 in
- let mp2,_,_ = repr_kn kn2 in
- try
- let side,mind',resolve =
- match subst_mp0 sub mp1,subst_mp0 sub mp2 with
- None,None ->raise No_subst
- | Some (mp',resolve),None -> User,(make_mind_equiv mp' mp2 dir l), resolve
- | None, Some(mp',resolve)-> Canonical,(make_mind_equiv mp1 mp' dir l), resolve
- | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical,
- (make_mind_equiv mp1' mp2' dir l), resolve2
- in
- match side with
- |User ->
- let mind = mind_of_delta resolve mind' in
- Some mind
- |Canonical ->
- let mind = mind_of_delta2 resolve mind' in
- Some 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 rebuild_mind mp1 mp2 = make_mind_equiv mp1 mp2 dir l in
+ try
+ let side,mind',resolve = gen_subst_mp rebuild_mind sub mp1 mp2 in
+ match side with
+ | User -> mind_of_delta resolve mind'
+ | Canonical -> mind_of_delta2 resolve mind'
+ with No_subst -> mind
let subst_con0 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
+ let rebuild_con mp1 mp2 = make_con_equiv mp1 mp2 dir l in
+ let dup con = con, Const con in
+ let side,con',resolve = gen_subst_mp rebuild_con sub mp1 mp2 in
+ match constant_of_delta_with_inline resolve con' with
+ | Some t -> con', t
+ | None ->
+ let con'' = match side with
+ | User -> constant_of_delta resolve con'
+ | Canonical -> constant_of_delta2 resolve con'
in
- match constant_of_delta_with_inline resolve con' with
- None ->begin
- match side with
- |User ->
- let con = constant_of_delta resolve con' in
- Some (Const con)
- |Canonical ->
- let con = constant_of_delta2 resolve con' in
- Some (Const con)
- end
- | t -> t
- with No_subst -> Some (Const con)
-
+ if con'' == con then raise No_subst else dup con''
let rec map_kn f f' c =
let func = map_kn f f' in
match c with
- | Const kn ->
- (match f' kn with
- None -> c
- | Some const ->const)
+ | Const kn -> (try snd (f' kn) with No_subst -> c)
| Ind (kn,i) ->
- (match f kn with
- None -> c
- | Some kn' ->
- Ind (kn',i))
+ let kn' = f kn in
+ if kn'==kn then c else Ind (kn',i)
| Construct ((kn,i),j) ->
- (match f kn with
- None -> c
- | Some kn' ->
- Construct ((kn',i),j))
+ let kn' = f kn in
+ if kn'==kn then c else Construct ((kn',i),j)
| Case (ci,p,ct,l) ->
let ci_ind =
let (kn,i) = ci.ci_ind in
- (match f kn with None -> ci.ci_ind | Some kn' -> kn',i ) in
+ let kn' = f kn in
+ if kn'==kn then ci.ci_ind else kn',i
+ in
let p' = func p in
let ct' = func ct in
let l' = array_smartmap func l in
@@ -476,8 +315,9 @@ let rec map_kn f f' c =
else CoFix (ln,(lna,tl',bl'))
| _ -> c
-let subst_mps sub =
- map_kn (subst_mind0 sub) (subst_con0 sub)
+let subst_mps sub c =
+ if is_empty_subst sub then c
+ else map_kn (subst_ind sub) (subst_con0 sub) c
type 'a lazy_subst =
@@ -507,125 +347,113 @@ let rec mp_in_mp mp mp1 =
| _ when mp1 = mp -> true
| MPdot (mp2,l) -> mp_in_mp mp mp2
| _ -> false
-
-let mp_in_key mp key =
- match key with
- | MP mp1 ->
- mp_in_mp mp mp1
- | KN kn ->
- let mp1,dir,l = repr_kn kn in
- mp_in_mp mp mp1
-
+
let subset_prefixed_by mp resolver =
- let prefixmp key hint resolv =
- if mp_in_key mp key then
- Deltamap.add key hint resolv
- else
- resolv
+ let mp_prefix mkey mequ rslv =
+ if mp_in_mp mp mkey then Deltamap.add_mp mkey mequ rslv else rslv
+ in
+ let kn_prefix kn hint rslv =
+ match hint with
+ | Inline _ -> rslv
+ | Equiv _ ->
+ if mp_in_mp mp (modpath kn) then Deltamap.add_kn kn hint rslv else rslv
in
- Deltamap.fold prefixmp resolver empty_delta_resolver
+ Deltamap.fold mp_prefix kn_prefix resolver empty_delta_resolver
let subst_dom_delta_resolver subst resolver =
- let apply_subst key hint resolver =
- match key with
- (MP mp) ->
- Deltamap.add (MP (subst_mp subst mp)) hint resolver
- | (KN kn) ->
- Deltamap.add (KN (subst_kn subst kn)) hint resolver
+ let mp_apply_subst mkey mequ rslv =
+ Deltamap.add_mp (subst_mp subst mkey) mequ rslv
in
- Deltamap.fold apply_subst resolver empty_delta_resolver
+ let kn_apply_subst kkey hint rslv =
+ Deltamap.add_kn (subst_kn subst kkey) hint rslv
+ in
+ Deltamap.fold mp_apply_subst kn_apply_subst resolver empty_delta_resolver
-let subst_mp_delta sub mp key=
+let subst_mp_delta sub mp mkey =
match subst_mp0 sub mp with
None -> empty_delta_resolver,mp
- | Some (mp',resolve) ->
+ | Some (mp',resolve) ->
let mp1 = find_prefix resolve mp' in
let resolve1 = subset_prefixed_by mp1 resolve in
- match key with
- MP mpk ->
- (subst_dom_delta_resolver
- (map_mp mp1 mpk) resolve1),mp1
- | _ -> anomaly "Mod_subst: Bad association in resolver"
-
-let subst_codom_delta_resolver subst resolver =
- let apply_subst key hint resolver =
- match hint with
- Prefix_equiv mp ->
- let derived_resolve,mpnew = subst_mp_delta subst mp key in
- Deltamap.fold Deltamap.add derived_resolve
- (Deltamap.add key (Prefix_equiv mpnew) resolver)
- | (Equiv kn) ->
- Deltamap.add key (Equiv (subst_kn_delta subst kn)) resolver
- | Inline None ->
- Deltamap.add key hint resolver
- | Inline (Some t) ->
- Deltamap.add key (Inline (Some (subst_mps subst t))) resolver
+ (subst_dom_delta_resolver
+ (map_mp mp1 mkey) resolve1),mp1
+
+let gen_subst_delta_resolver dom subst resolver =
+ let mp_apply_subst mkey mequ rslv =
+ let mkey' = if dom then subst_mp subst mkey else mkey in
+ let rslv',mequ' = subst_mp_delta subst mequ mkey in
+ Deltamap.join rslv' (Deltamap.add_mp mkey' mequ' rslv)
in
- Deltamap.fold apply_subst resolver empty_delta_resolver
+ let kn_apply_subst kkey hint rslv =
+ let kkey' = if dom then subst_kn subst kkey else kkey in
+ let hint' = match hint with
+ | Equiv kequ -> Equiv (subst_kn_delta subst kequ)
+ | Inline (lev,Some t) -> Inline (lev,Some (subst_mps subst t))
+ | Inline (_,None) -> hint
+ in
+ Deltamap.add_kn kkey' hint' rslv
+ in
+ Deltamap.fold mp_apply_subst kn_apply_subst resolver empty_delta_resolver
+
+let subst_codom_delta_resolver = gen_subst_delta_resolver false
+let subst_dom_codom_delta_resolver = gen_subst_delta_resolver true
-let subst_dom_codom_delta_resolver subst resolver =
- subst_dom_delta_resolver subst
- (subst_codom_delta_resolver subst resolver)
-
let update_delta_resolver resolver1 resolver2 =
- let apply_res key hint res =
- try
- match hint with
- Prefix_equiv mp ->
- let new_hint =
- Prefix_equiv (find_prefix resolver2 mp)
- in Deltamap.add key new_hint res
- | Equiv kn ->
- let new_hint =
- Equiv (solve_delta_kn resolver2 kn)
- in Deltamap.add key new_hint res
- | _ -> Deltamap.add key hint res
- with Not_found ->
- Deltamap.add key hint res
- in
- Deltamap.fold apply_res resolver1 empty_delta_resolver
+ let mp_apply_rslv mkey mequ rslv =
+ if Deltamap.mem_mp mkey resolver2 then rslv
+ else Deltamap.add_mp mkey (find_prefix resolver2 mequ) rslv
+ in
+ let kn_apply_rslv kkey hint rslv =
+ if Deltamap.mem_kn kkey resolver2 then rslv
+ else
+ let hint' = match hint with
+ | Equiv kequ -> Equiv (solve_delta_kn resolver2 kequ)
+ | _ -> hint
+ in
+ Deltamap.add_kn kkey hint' rslv
+ in
+ Deltamap.fold mp_apply_rslv kn_apply_rslv resolver1 empty_delta_resolver
let add_delta_resolver resolver1 resolver2 =
if resolver1 == resolver2 then
resolver2
+ else if resolver2 = empty_delta_resolver then
+ resolver1
else
- Deltamap.fold Deltamap.add (update_delta_resolver resolver1 resolver2)
- resolver2
+ Deltamap.join (update_delta_resolver resolver1 resolver2) resolver2
let substition_prefixed_by k mp subst =
- let prefixmp key (mp_to,reso) sub =
- match key with
- | MPI mpk ->
- if mp_in_mp mp mpk && mp <> mpk then
- let new_key = replace_mp_in_mp mp k mpk in
- Umap.add (MPI new_key) (mp_to,reso) sub
- else
- sub
- | _ -> sub
+ let mp_prefixmp kmp (mp_to,reso) sub =
+ if mp_in_mp mp kmp && mp <> kmp then
+ let new_key = replace_mp_in_mp mp k kmp in
+ Umap.add_mp new_key (mp_to,reso) sub
+ else sub
+ in
+ let mbi_prefixmp mbi _ sub = sub
in
- Umap.fold prefixmp subst empty_subst
+ Umap.fold mp_prefixmp mbi_prefixmp subst empty_subst
-let join (subst1 : substitution) (subst2 : substitution) =
- let apply_subst key (mp,resolve) res =
+let join subst1 subst2 =
+ let apply_subst mpk add (mp,resolve) res =
let mp',resolve' =
match subst_mp0 subst2 mp with
- None -> mp, None
- | Some (mp',resolve') -> mp'
- ,Some resolve' in
- let resolve'' : delta_resolver =
+ | None -> mp, None
+ | Some (mp',resolve') -> mp', Some resolve' in
+ let resolve'' =
match resolve' with
- Some res ->
- add_delta_resolver
+ | Some res ->
+ add_delta_resolver
(subst_dom_codom_delta_resolver subst2 resolve) res
- | None ->
+ | None ->
subst_codom_delta_resolver subst2 resolve
in
- let k = match key with MBI mp -> MPbound mp | MPI mp -> mp in
- let prefixed_subst = substition_prefixed_by k mp subst2 in
- Umap.fold Umap.add prefixed_subst
- (Umap.add key (mp',resolve'') res) in
- let subst = Umap.fold apply_subst subst1 empty_subst in
- (Umap.fold Umap.add subst2 subst)
+ let prefixed_subst = substition_prefixed_by mpk mp' subst2 in
+ Umap.join prefixed_subst (add (mp',resolve'') res)
+ in
+ let mp_apply_subst mp = apply_subst mp (Umap.add_mp mp) in
+ let mbi_apply_subst mbi = apply_subst (MPbound mbi) (Umap.add_mbi mbi) in
+ let subst = Umap.fold mp_apply_subst mbi_apply_subst subst1 empty_subst in
+ Umap.join subst2 subst
let force fsubst r =
match !r with
@@ -650,25 +478,67 @@ let val_cstr_subst = val_substituted val_constr
let subst_constr_subst = subst_substituted
+(** Beware! In .vo files, lazy_constr are stored as integers
+ used as indexes for a separate table. The actual lazy_constr is restored
+ later, by [Safe_typing.LightenLibrary.load]. This allows us
+ to use here a different definition of lazy_constr than coqtop:
+ since the checker will inspect all proofs parts, even opaque
+ ones, no need to use Lazy.t here *)
+
+type lazy_constr = constr_substituted
+let subst_lazy_constr = subst_substituted
+let force_lazy_constr = force_constr
+let lazy_constr_from_val c = c
+let val_lazy_constr = val_cstr_subst
+
+(** Inlining level of parameters at functor applications.
+ This is ignored by the checker. *)
+
+type inline = int option
+
+(** A constant can have no body (axiom/parameter), or a
+ transparent body, or an opaque one *)
+
+type constant_def =
+ | Undef of inline
+ | Def of constr_substituted
+ | OpaqueDef of lazy_constr
+
+let val_cst_def =
+ val_sum "constant_def" 0
+ [|[|val_opt val_int|]; [|val_cstr_subst|]; [|val_lazy_constr|]|]
+
+let subst_constant_def sub = function
+ | Undef inl -> Undef inl
+ | Def c -> Def (subst_constr_subst sub c)
+ | OpaqueDef lc -> OpaqueDef (subst_lazy_constr sub lc)
+
type constant_body = {
const_hyps : section_context; (* New: younger hyp at top *)
- const_body : constr_substituted option;
+ const_body : constant_def;
const_type : constant_type;
const_body_code : to_patch_substituted;
- (* const_type_code : Cemitcodes.to_patch; *)
- const_constraints : Univ.constraints;
- const_opaque : bool;
- const_inline : bool}
+ const_constraints : Univ.constraints }
-let val_cb = val_tuple "constant_body"
+let body_of_constant cb = match cb.const_body with
+ | Undef _ -> None
+ | Def c -> Some c
+ | OpaqueDef c -> Some c
+
+let constant_has_body cb = match cb.const_body with
+ | Undef _ -> false
+ | Def _ | OpaqueDef _ -> true
+
+let is_opaque cb = match cb.const_body with
+ | OpaqueDef _ -> true
+ | Def _ | Undef _ -> false
+
+let val_cb = val_tuple ~name:"constant_body"
[|val_nctxt;
- val_opt val_cstr_subst;
+ val_cst_def;
val_cst_type;
no_val;
- val_cstrs;
- val_bool;
- val_bool |]
-
+ val_cstrs|]
let subst_rel_declaration sub (id,copt,t as x) =
let copt' = Option.smartmap (subst_mps sub) copt in
@@ -679,14 +549,14 @@ let subst_rel_context sub = list_smartmap (subst_rel_declaration sub)
type recarg =
| Norec
- | Mrec of int
+ | Mrec of inductive
| Imbr of inductive
let val_recarg = val_sum "recarg" 1 (* Norec *)
- [|[|val_int|] (* Mrec *);[|val_ind|] (* Imbr *)|]
+ [|[|val_ind|] (* Mrec *);[|val_ind|] (* Imbr *)|]
let subst_recarg sub r = match r with
- | Norec | Mrec _ -> r
- | Imbr (kn,i) -> let kn' = subst_ind sub kn in
+ | Norec -> r
+ | (Mrec(kn,i)|Imbr (kn,i)) -> let kn' = subst_ind sub kn in
if kn==kn' then r else Imbr (kn',i)
type wf_paths = recarg Rtree.t
@@ -724,7 +594,7 @@ type monomorphic_inductive_arity = {
mind_sort : sorts;
}
let val_mono_ind_arity =
- val_tuple"monomorphic_inductive_arity"[|val_constr;val_sort|]
+ val_tuple ~name:"monomorphic_inductive_arity"[|val_constr;val_sort|]
type inductive_arity =
| Monomorphic of monomorphic_inductive_arity
@@ -784,7 +654,7 @@ type one_inductive_body = {
mind_reloc_tbl : reloc_table;
}
-let val_one_ind = val_tuple "one_inductive_body"
+let val_one_ind = val_tuple ~name:"one_inductive_body"
[|val_id;val_rctxt;val_ind_arity;val_array val_id;val_array val_constr;
val_int;val_int;val_list val_sortfam;val_array val_constr;val_array val_int;
val_wfp;val_int;val_int;no_val|]
@@ -820,7 +690,7 @@ type mutual_inductive_body = {
mind_constraints : Univ.constraints;
}
-let val_ind_pack = val_tuple "mutual_inductive_body"
+let val_ind_pack = val_tuple ~name:"mutual_inductive_body"
[|val_array val_one_ind;val_bool;val_bool;val_int;val_nctxt;
val_int; val_int; val_rctxt;val_cstrs|]
@@ -832,13 +702,10 @@ let subst_arity sub = function
(* TODO: should be changed to non-coping after Term.subst_mps *)
let subst_const_body sub cb = {
const_hyps = (assert (cb.const_hyps=[]); []);
- const_body = Option.map (subst_constr_subst sub) cb.const_body;
+ const_body = subst_constant_def sub cb.const_body;
const_type = subst_arity sub cb.const_type;
const_body_code = (*Cemitcodes.subst_to_patch_subst sub*) cb.const_body_code;
- (*const_type_code = Cemitcodes.subst_to_patch sub cb.const_type_code;*)
- const_constraints = cb.const_constraints;
- const_opaque = cb.const_opaque;
- const_inline = cb.const_inline}
+ const_constraints = cb.const_constraints}
let subst_arity sub = function
| Monomorphic s ->
@@ -923,7 +790,7 @@ let rec val_sfb o = val_sum "struct_field_body" 0
[|val_module|]; (* SFBmodule *)
[|val_modtype|] (* SFBmodtype *)
|] o
-and val_sb o = val_list (val_tuple"label*sfb"[|val_id;val_sfb|]) o
+and val_sb o = val_list (val_tuple ~name:"label*sfb"[|val_id;val_sfb|]) o
and val_seb o = val_sum "struct_expr_body" 0
[|[|val_mp|]; (* SEBident *)
[|val_uid;val_modtype;val_seb|]; (* SEBfunctor *)
@@ -934,10 +801,10 @@ and val_seb o = val_sum "struct_expr_body" 0
and val_with o = val_sum "with_declaration_body" 0
[|[|val_list val_id;val_mp|];
[|val_list val_id;val_cb|]|] o
-and val_module o = val_tuple "module_body"
+and val_module o = val_tuple ~name:"module_body"
[|val_mp;val_opt val_seb;val_seb;
val_opt val_seb;val_cstrs;val_res;no_val|] o
-and val_modtype o = val_tuple "module_type_body"
+and val_modtype o = val_tuple ~name:"module_type_body"
[|val_mp;val_seb;val_opt val_seb;val_cstrs;val_res|] o
diff --git a/checker/declarations.mli b/checker/declarations.mli
index b39fd6f2..90beb326 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -29,26 +29,53 @@ type constr_substituted
val force_constr : constr_substituted -> constr
val from_val : constr -> constr_substituted
+(** Beware! In .vo files, lazy_constr are stored as integers
+ used as indexes for a separate table. The actual lazy_constr is restored
+ later, by [Safe_typing.LightenLibrary.load]. This allows us
+ to use here a different definition of lazy_constr than coqtop:
+ since the checker will inspect all proofs parts, even opaque
+ ones, no need to use Lazy.t here *)
+
+type lazy_constr
+val force_lazy_constr : lazy_constr -> constr
+val lazy_constr_from_val : constr_substituted -> lazy_constr
+
+(** Inlining level of parameters at functor applications.
+ This is ignored by the checker. *)
+
+type inline = int option
+
+(** A constant can have no body (axiom/parameter), or a
+ transparent body, or an opaque one *)
+
+type constant_def =
+ | Undef of inline
+ | Def of constr_substituted
+ | OpaqueDef of lazy_constr
+
type constant_body = {
const_hyps : section_context; (* New: younger hyp at top *)
- const_body : constr_substituted option;
+ const_body : constant_def;
const_type : constant_type;
const_body_code : to_patch_substituted;
- const_constraints : Univ.constraints;
- const_opaque : bool;
- const_inline : bool}
+ const_constraints : Univ.constraints }
+
+val body_of_constant : constant_body -> constr_substituted option
+val constant_has_body : constant_body -> bool
+val is_opaque : constant_body -> bool
(* Mutual inductives *)
type recarg =
| Norec
- | Mrec of int
+ | Mrec of inductive
| Imbr of inductive
type wf_paths = recarg Rtree.t
val mk_norec : wf_paths
val mk_paths : recarg -> wf_paths list array -> wf_paths
+val dest_recarg : wf_paths -> recarg
val dest_subterms : wf_paths -> wf_paths list array
type monomorphic_inductive_arity = {
@@ -186,11 +213,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
@@ -211,6 +233,6 @@ val subst_module : substitution -> module_body -> module_body
val join : substitution -> substitution -> substitution
(* Validation *)
-val val_eng : Obj.t -> unit
-val val_module : Obj.t -> unit
-val val_modtype : Obj.t -> unit
+val val_eng : Validate.func
+val val_module : Validate.func
+val val_modtype : Validate.func
diff --git a/checker/environ.ml b/checker/environ.ml
index f7dd46f8..99b36457 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -98,7 +98,7 @@ let named_type id env =
(* Universe constraints *)
let add_constraints c env =
- if c == Constraint.empty then
+ if c == empty_constraint then
env
else
let s = env.env_stratification in
@@ -121,25 +121,16 @@ 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
let constant_value env kn =
let cb = lookup_constant kn env in
- if cb.const_opaque then raise (NotEvaluableConst Opaque);
match cb.const_body with
- | 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
+ | Def l_body -> force_constr l_body
+ | OpaqueDef _ -> raise (NotEvaluableConst Opaque)
+ | Undef _ -> raise (NotEvaluableConst NoBody)
(* A global const is evaluable if it is defined and not opaque *)
let evaluable_constant cst env =
diff --git a/checker/environ.mli b/checker/environ.mli
index ea446cdb..628febbb 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/indtypes.ml b/checker/indtypes.ml
index 277fed30..1e773df6 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: indtypes.ml 10296 2007-11-07 11:02:42Z barras $ *)
-
open Util
open Names
open Univ
@@ -178,7 +176,7 @@ let check_predicativity env s small level =
Type u, _ ->
let u' = fresh_local_univ () in
let cst =
- merge_constraints (enforce_geq u' u Constraint.empty)
+ merge_constraints (enforce_geq u' u empty_constraint)
(universes env) in
if not (check_geq cst u' level) then
failwith "impredicative Type inductive type"
@@ -394,7 +392,7 @@ let rec ienv_decompose_prod (env,_,_,_ as ienv) n c =
(* The recursive function that checks positivity and builds the list
of recursive arguments *)
-let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp i indlc =
+let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc =
let lparams = rel_context_length hyps in
(* check the inductive types occur positively in [c] *)
let rec check_pos (env, n, ntypes, ra_env as ienv) c =
@@ -496,7 +494,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp i indlc =
with IllFormedInd err ->
explain_ind_err (ntypes-i) env lparams c err)
indlc
- in mk_paths (Mrec i) irecargs
+ in mk_paths (Mrec ind) irecargs
let check_subtree (t1:'a) (t2:'a) =
if not (Rtree.compare_rtree (fun t1 t2 ->
@@ -507,16 +505,17 @@ let check_subtree (t1:'a) (t2:'a) =
failwith "bad recursive trees"
(* if t1=t2 then () else msg_warning (str"TODO: check recursive positions")*)
-let check_positivity env_ar params nrecp inds =
+let check_positivity env_ar mind params nrecp inds =
let ntypes = Array.length inds in
- let rc = Array.mapi (fun j t -> (Mrec j,t)) (Rtree.mk_rec_calls ntypes) in
+ let rc =
+ Array.mapi (fun j t -> (Mrec(mind,j),t)) (Rtree.mk_rec_calls ntypes) in
let lra_ind = List.rev (Array.to_list rc) in
let lparams = rel_context_length params in
let check_one i mip =
let ra_env =
list_tabulate (fun _ -> (Norec,mk_norec)) lparams @ lra_ind in
let ienv = (env_ar, 1+lparams, ntypes, ra_env) in
- check_positivity_one ienv params nrecp i mip.mind_nf_lc
+ check_positivity_one ienv params nrecp (mind,i) mip.mind_nf_lc
in
let irecargs = Array.mapi check_one inds in
let wfp = Rtree.mk_rec irecargs in
@@ -549,7 +548,7 @@ let check_inductive env kn mib =
(* - check constructor types *)
Array.iter (typecheck_one_inductive env_ar params mib) mib.mind_packets;
(* check mind_nparams_rec: positivity condition *)
- check_positivity env_ar params mib.mind_nparams_rec mib.mind_packets;
+ check_positivity env_ar kn params mib.mind_nparams_rec mib.mind_packets;
(* check mind_equiv... *)
(* Now we can add the inductive *)
add_mind kn mib env
diff --git a/checker/indtypes.mli b/checker/indtypes.mli
index bca0a643..4c2b078c 100644
--- a/checker/indtypes.mli
+++ b/checker/indtypes.mli
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: indtypes.mli 9831 2007-05-17 18:55:42Z herbelin $ i*)
-
(*i*)
open Names
open Univ
diff --git a/checker/inductive.ml b/checker/inductive.ml
index b9964fe6..7a04cbfa 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: inductive.ml 10172 2007-10-04 13:02:03Z herbelin $ *)
-
open Util
open Names
open Univ
@@ -83,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
@@ -100,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:
@@ -346,14 +338,14 @@ let type_case_branches env (ind,largs) (p,pj) c =
(************************************************************************)
-(* Checking the case annotation is relevent *)
+(* Checking the case annotation is relevant *)
let check_case_info env indsp ci =
let (mib,mip) = lookup_mind_specif env indsp in
if
not (eq_ind indsp ci.ci_ind) or
(mib.mind_nparams <> ci.ci_npar) or
- (mip.mind_consnrealdecls <> ci.ci_cstr_nargs)
+ (mip.mind_consnrealdecls <> ci.ci_cstr_ndecls)
then raise (TypeError(env,WrongCaseInfo(indsp,ci)))
(************************************************************************)
@@ -404,8 +396,10 @@ type subterm_spec =
| Dead_code
| Not_subterm
-let spec_of_tree t =
- if Rtree.eq_rtree (=) t mk_norec then Not_subterm else Subterm(Strict,t)
+let spec_of_tree t = lazy
+ (if Rtree.eq_rtree (=) (Lazy.force t) mk_norec
+ then Not_subterm
+ else Subterm(Strict,Lazy.force t))
let subterm_spec_glb =
let glb2 s1 s2 =
@@ -440,7 +434,7 @@ let make_renv env minds recarg (kn,tyi) =
rel_min = recarg+2;
inds = minds;
recvec = mind_recvec;
- genv = [Lazy.lazy_from_val (Subterm(Large,mind_recvec.(tyi)))] }
+ genv = [Lazy.lazy_from_val(Subterm(Large,mind_recvec.(tyi)))] }
let push_var renv (x,ty,spec) =
{ renv with
@@ -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,lazy (spec_of_tree (Lazy.force spec)))
-
let push_ctxt_renv renv ctxt =
let n = rel_context_length ctxt in
{ renv with
@@ -478,6 +468,15 @@ let push_fix_renv renv (_,v,_ as recdef) =
genv = iterate (fun ge -> Lazy.lazy_from_val Not_subterm::ge) n renv.genv }
+(* Definition and manipulation of the stack *)
+type stack_element = |SClosure of guard_env*constr |SArg of subterm_spec Lazy.t
+
+let push_stack_closures renv l stack =
+ List.fold_right (fun h b -> (SClosure (renv,h))::b) l stack
+
+let push_stack_args l stack =
+ List.fold_right (fun h b -> (SArg h)::b) l stack
+
(******************************)
(* Computing the recursive subterms of a term (propagation of size
information through Cases). *)
@@ -497,60 +496,38 @@ let lookup_subterms env ind =
let (_,mip) = lookup_mind_specif env ind in
mip.mind_recargs
-(*********************************)
-
-let match_trees t1 t2 =
- let v1 = dest_subterms t1 in
- let v2 = dest_subterms t2 in
- array_for_all2 (fun l1 l2 -> List.length l1 = List.length l2) v1 v2
+let match_inductive ind ra =
+ match ra with
+ | (Mrec i | Imbr i) -> eq_ind ind i
+ | Norec -> false
-(* In {match c as z in ind y_s return P with |C_i x_s => t end}
- [branches_specif renv c_spec ind] returns an array of x_s specs given
- c_spec the spec of c. *)
-let branches_specif renv c_spec ind =
- let (_,mip) = lookup_mind_specif renv.env ind in
+(* In {match c as z in ci y_s return P with |C_i x_s => t end}
+ [branches_specif renv c_spec ci] returns an array of x_s specs knowing
+ c_spec. *)
+let branches_specif renv c_spec ci =
let car =
(* We fetch the regular tree associated to the inductive of the match.
This is just to get the number of constructors (and constructor
arities) that fit the match branches without forcing c_spec.
Note that c_spec might be more precise than [v] below, because of
nested inductive types. *)
+ let (_,mip) = lookup_mind_specif renv.env ci.ci_ind in
let v = dest_subterms mip.mind_recargs in
Array.map List.length v in
Array.mapi
(fun i nca -> (* i+1-th cstructor has arity nca *)
let lvra = lazy
(match Lazy.force c_spec with
- Subterm (_,t) when match_trees mip.mind_recargs t ->
+ Subterm (_,t) when match_inductive ci.ci_ind (dest_recarg t) ->
let vra = Array.of_list (dest_subterms t).(i) in
assert (nca = Array.length vra);
- Array.map spec_of_tree vra
+ Array.map
+ (fun t -> Lazy.force (spec_of_tree (lazy t)))
+ vra
| Dead_code -> Array.create nca Dead_code
| _ -> Array.create nca Not_subterm) in
list_tabulate (fun j -> lazy (Lazy.force lvra).(j)) nca)
- car
-
-(* Propagation of size information through Cases: if the matched
- object is a recursive subterm then compute the information
- associated to its own subterms.
- Rq: if branch is not eta-long, then the recursive information
- is not propagated to the missing abstractions *)
-let case_branches_specif renv c_spec ind lbr =
- let vlrec = branches_specif renv c_spec ind in
- let rec push_branch_args renv lrec c =
- match lrec with
- ra::lr ->
- let c' = whd_betadeltaiota renv.env c in
- (match c' with
- Lambda(x,a,b) ->
- let renv' = push_var renv (x,a,ra) in
- push_branch_args renv' lr b
- | _ -> (* branch not in eta-long form: cannot perform rec. calls *)
- (renv,c'))
- | [] -> (renv, c) in
- assert (Array.length vlrec = Array.length lbr);
- array_map2 (push_branch_args renv) vlrec lbr
-
+ car
(* [subterm_specif renv t] computes the recursive structure of [t] and
compare its size with the size of the initial recursive argument of
@@ -558,78 +535,88 @@ let case_branches_specif renv c_spec ind lbr =
about variables.
*)
-let rec subterm_specif renv t =
+
+let rec subterm_specif renv stack t =
(* maybe reduction is not always necessary! *)
let f,l = decompose_app (whd_betadeltaiota renv.env t) in
- match f with
- | Rel k -> subterm_var k renv
-
- | Case (ci,_,c,lbr) ->
- let lbr_spec = case_subterm_specif renv ci c lbr in
- let stl =
- Array.map (fun (renv',br') -> subterm_specif renv' br')
- lbr_spec in
- subterm_spec_glb stl
-
- | Fix ((recindxs,i),(_,typarray,bodies as recdef)) ->
-(* when proving that the fixpoint f(x)=e is less than n, it is enough
- to prove that e is less than n assuming f is less than n
- furthermore when f is applied to a term which is strictly less than
- n, one may assume that x itself is strictly less than n
-*)
- let (ctxt,clfix) = dest_prod renv.env typarray.(i) in
- let oind =
- let env' = push_rel_context ctxt renv.env in
- try Some(fst(find_inductive env' clfix))
- with Not_found -> None in
- (match oind with
- None -> Not_subterm (* happens if fix is polymorphic *)
- | Some ind ->
- let nbfix = Array.length typarray in
- let recargs = lookup_subterms renv.env ind in
- (* pushing the fixpoints *)
- let renv' = push_fix_renv renv recdef in
- let renv' =
- (* Why Strict here ? To be general, it could also be
- Large... *)
- assign_var_spec renv'
- (nbfix-i, Lazy.lazy_from_val (Subterm(Strict,recargs))) in
- let decrArg = recindxs.(i) in
- let theBody = bodies.(i) in
- let nbOfAbst = decrArg+1 in
- let sign,strippedBody = decompose_lam_n_assum nbOfAbst theBody in
- (* pushing the fix parameters *)
- let renv'' = push_ctxt_renv renv' sign in
- let renv'' =
- if List.length l < nbOfAbst then renv''
- else
- let theDecrArg = List.nth l decrArg in
- let arg_spec = lazy_subterm_specif renv theDecrArg in
- assign_var_spec renv'' (1, arg_spec) in
- subterm_specif renv'' strippedBody)
-
- | Lambda (x,a,b) ->
- assert (l=[]);
- subterm_specif (push_var_renv renv (x,a)) b
-
- (* Metas and evars are considered OK *)
- | (Meta _|Evar _) -> Dead_code
-
- (* Other terms are not subterms *)
- | _ -> Not_subterm
-
-and lazy_subterm_specif renv t =
- lazy (subterm_specif renv t)
-
-and case_subterm_specif renv ci c lbr =
- if Array.length lbr = 0 then [||]
- else
- let c_spec = lazy_subterm_specif renv c in
- case_branches_specif renv c_spec ci.ci_ind lbr
-
-(* Check term c can be applied to one of the mutual fixpoints. *)
-let check_is_subterm renv c =
- match subterm_specif renv c with
+ match f with
+ | Rel k -> subterm_var k renv
+
+ | Case (ci,_,c,lbr) ->
+ let stack' = push_stack_closures renv l stack in
+ let cases_spec = branches_specif renv
+ (lazy_subterm_specif renv [] c) ci in
+ let stl =
+ Array.mapi (fun i br' ->
+ let stack_br = push_stack_args (cases_spec.(i)) stack' in
+ subterm_specif renv stack_br br')
+ lbr in
+ subterm_spec_glb stl
+
+ | Fix ((recindxs,i),(_,typarray,bodies as recdef)) ->
+ (* when proving that the fixpoint f(x)=e is less than n, it is enough
+ to prove that e is less than n assuming f is less than n
+ furthermore when f is applied to a term which is strictly less than
+ n, one may assume that x itself is strictly less than n
+ *)
+ let (ctxt,clfix) = dest_prod renv.env typarray.(i) in
+ let oind =
+ let env' = push_rel_context ctxt renv.env in
+ try Some(fst(find_inductive env' clfix))
+ with Not_found -> None in
+ (match oind with
+ None -> Not_subterm (* happens if fix is polymorphic *)
+ | Some ind ->
+ let nbfix = Array.length typarray in
+ let recargs = lookup_subterms renv.env ind in
+ (* pushing the fixpoints *)
+ let renv' = push_fix_renv renv recdef in
+ let renv' =
+ (* Why Strict here ? To be general, it could also be
+ Large... *)
+ assign_var_spec renv'
+ (nbfix-i, lazy (Subterm(Strict,recargs))) in
+ let decrArg = recindxs.(i) in
+ let theBody = bodies.(i) in
+ let nbOfAbst = decrArg+1 in
+ let sign,strippedBody = decompose_lam_n_assum nbOfAbst theBody in
+ (* pushing the fix parameters *)
+ let stack' = push_stack_closures renv l stack in
+ let renv'' = push_ctxt_renv renv' sign in
+ let renv'' =
+ if List.length stack' < nbOfAbst then renv''
+ else
+ let decrArg = List.nth stack' decrArg in
+ let arg_spec = stack_element_specif decrArg in
+ assign_var_spec renv'' (1, arg_spec) in
+ subterm_specif renv'' [] strippedBody)
+
+ | Lambda (x,a,b) ->
+ assert (l=[]);
+ let spec,stack' = extract_stack renv a stack in
+ subterm_specif (push_var renv (x,a,spec)) stack' b
+
+ (* Metas and evars are considered OK *)
+ | (Meta _|Evar _) -> Dead_code
+
+ (* Other terms are not subterms *)
+ | _ -> Not_subterm
+
+and lazy_subterm_specif renv stack t =
+ lazy (subterm_specif renv stack t)
+
+and stack_element_specif = function
+ |SClosure (h_renv,h) -> lazy_subterm_specif h_renv [] h
+ |SArg x -> x
+
+and extract_stack renv a = function
+ | [] -> Lazy.lazy_from_val Not_subterm , []
+ | h::t -> stack_element_specif h, t
+
+
+(* Check size x is a correct size for recursive calls. *)
+let check_is_subterm x =
+ match Lazy.force x with
Subterm (Strict,_) | Dead_code -> true
| _ -> false
@@ -637,7 +624,7 @@ let check_is_subterm renv c =
exception FixGuardError of env * guard_error
-let error_illegal_rec_call renv fx arg =
+let error_illegal_rec_call renv fx (arg_renv,arg) =
let (_,le_vars,lt_vars) =
List.fold_left
(fun (i,le,lt) sbt ->
@@ -647,7 +634,8 @@ let error_illegal_rec_call renv fx arg =
| _ -> (i+1, le ,lt))
(1,[],[]) renv.genv in
raise (FixGuardError (renv.env,
- RecursionOnIllegalTerm(fx,arg,le_vars,lt_vars)))
+ RecursionOnIllegalTerm(fx,(arg_renv.env, arg),
+ le_vars,lt_vars)))
let error_partial_apply renv fx =
raise (FixGuardError (renv.env,NotEnoughArgumentsForFixCall fx))
@@ -659,48 +647,57 @@ let check_one_fix renv recpos def =
let nfi = Array.length recpos in
(* Checks if [t] only make valid recursive calls *)
- let rec check_rec_call renv t =
+ let rec check_rec_call renv stack t =
(* if [t] does not make recursive calls, it is guarded: *)
if noccur_with_meta renv.rel_min nfi t then ()
else
- let (f,l) = decompose_app (whd_betaiotazeta renv.env t) in
+ let (f,l) = decompose_app (whd_betaiotazeta t) in
match f with
| Rel p ->
(* Test if [p] is a fixpoint (recursive call) *)
if renv.rel_min <= p & p < renv.rel_min+nfi then
begin
- List.iter (check_rec_call renv) l;
+ List.iter (check_rec_call renv []) l;
(* the position of the invoked fixpoint: *)
let glob = renv.rel_min+nfi-1-p in
(* the decreasing arg of the rec call: *)
let np = recpos.(glob) in
- if List.length l <= np then error_partial_apply renv glob
+ let stack' = push_stack_closures renv l stack in
+ if List.length stack' <= np then error_partial_apply renv glob
else
(* Check the decreasing arg is smaller *)
- let z = List.nth l np in
- if not (check_is_subterm renv z) then
- error_illegal_rec_call renv glob z
+ let z = List.nth stack' np in
+ if not (check_is_subterm (stack_element_specif z)) then
+ begin match z with
+ |SClosure (z,z') -> error_illegal_rec_call renv glob (z,z')
+ |SArg _ -> error_partial_apply renv glob
+ end
end
else
begin
match pi2 (lookup_rel p renv.env) with
| None ->
- List.iter (check_rec_call renv) l
+ List.iter (check_rec_call renv []) l
| Some c ->
- try List.iter (check_rec_call renv) l
- with FixGuardError _ -> check_rec_call renv (applist(c,l))
+ try List.iter (check_rec_call renv []) l
+ with FixGuardError _ ->
+ check_rec_call renv stack (applist(lift p c,l))
end
-
+
| Case (ci,p,c_0,lrest) ->
- List.iter (check_rec_call renv) (c_0::p::l);
+ List.iter (check_rec_call renv []) (c_0::p::l);
(* compute the recarg information for the arguments of
each branch *)
- let lbr = case_subterm_specif renv ci c_0 lrest in
- Array.iter (fun (renv',br') -> check_rec_call renv' br') lbr
+ let case_spec = branches_specif renv
+ (lazy_subterm_specif renv [] c_0) ci in
+ let stack' = push_stack_closures renv l stack in
+ Array.iteri (fun k br' ->
+ let stack_br = push_stack_args case_spec.(k) stack' in
+ check_rec_call renv stack_br br') lrest
(* Enables to traverse Fixpoint definitions in a more intelligent
way, ie, the rule :
- if - g = Fix g/p := [y1:T1]...[yp:Tp]e &
+ if - g = fix g (y1:T1)...(yp:Tp) {struct yp} := e &
- f is guarded with respect to the set of pattern variables S
in a1 ... am &
- f is guarded with respect to the set of pattern variables S
@@ -710,81 +707,80 @@ let check_one_fix renv recpos def =
S+{yp} in e
then f is guarded with respect to S in (g a1 ... am).
Eduardo 7/9/98 *)
-
| Fix ((recindxs,i),(_,typarray,bodies as recdef)) ->
- List.iter (check_rec_call renv) l;
- Array.iter (check_rec_call renv) typarray;
+ List.iter (check_rec_call renv []) l;
+ Array.iter (check_rec_call renv []) typarray;
let decrArg = recindxs.(i) in
let renv' = push_fix_renv renv recdef in
- if (List.length l < (decrArg+1)) then
- Array.iter (check_rec_call renv') bodies
- else
+ let stack' = push_stack_closures renv l stack in
Array.iteri
(fun j body ->
- if i=j then
- let theDecrArg = List.nth l decrArg in
- let arg_spec = lazy_subterm_specif renv theDecrArg in
- check_nested_fix_body renv' (decrArg+1) arg_spec body
- else check_rec_call renv' body)
+ if i=j && (List.length stack' > decrArg) then
+ let recArg = List.nth stack' decrArg in
+ let arg_sp = stack_element_specif recArg in
+ check_nested_fix_body renv' (decrArg+1) arg_sp body
+ else check_rec_call renv' [] body)
bodies
| Const kn ->
if evaluable_constant kn renv.env then
- try List.iter (check_rec_call renv) l
+ try List.iter (check_rec_call renv []) l
with (FixGuardError _ ) ->
- check_rec_call renv(applist(constant_value renv.env kn, l))
- else List.iter (check_rec_call renv) l
-
- (* The cases below simply check recursively the condition on the
- subterms *)
- | Cast (a,_, b) ->
- List.iter (check_rec_call renv) (a::b::l)
+ let value = (applist(constant_value renv.env kn, l)) in
+ check_rec_call renv stack value
+ else List.iter (check_rec_call renv []) l
| Lambda (x,a,b) ->
- List.iter (check_rec_call renv) (a::l);
- check_rec_call (push_var_renv renv (x,a)) b
+ assert (l = []);
+ check_rec_call renv [] a ;
+ let spec, stack' = extract_stack renv a stack in
+ check_rec_call (push_var renv (x,a,spec)) stack' b
| Prod (x,a,b) ->
- List.iter (check_rec_call renv) (a::l);
- check_rec_call (push_var_renv renv (x,a)) b
+ assert (l = [] && stack = []);
+ check_rec_call renv [] a;
+ check_rec_call (push_var_renv renv (x,a)) [] b
| CoFix (i,(_,typarray,bodies as recdef)) ->
- List.iter (check_rec_call renv) l;
- Array.iter (check_rec_call renv) typarray;
+ List.iter (check_rec_call renv []) l;
+ Array.iter (check_rec_call renv []) typarray;
let renv' = push_fix_renv renv recdef in
- Array.iter (check_rec_call renv') bodies
+ Array.iter (check_rec_call renv' []) bodies
- | (Ind _ | Construct _ | Sort _) ->
- List.iter (check_rec_call renv) l
+ | (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
+ List.iter (check_rec_call renv []) l
| Some c ->
- try List.iter (check_rec_call renv) l
- with (FixGuardError _) -> check_rec_call renv (applist(c,l))
+ try List.iter (check_rec_call renv []) l
+ with (FixGuardError _) ->
+ check_rec_call renv stack (applist(c,l))
end
+ | Sort _ -> assert (l = [])
+
(* l is not checked because it is considered as the meta's context *)
| (Evar _ | Meta _) -> ()
- | (App _|LetIn _) -> assert false (* beta zeta reduction *)
+ | (App _ | LetIn _ | Cast _) -> assert false (* beta zeta reduction *)
and check_nested_fix_body renv decr recArgsDecrArg body =
if decr = 0 then
- check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) body
+ check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) [] body
else
match body with
| Lambda (x,a,b) ->
- check_rec_call renv a;
+ check_rec_call renv [] a;
let renv' = push_var_renv renv (x,a) in
- check_nested_fix_body renv' (decr-1) recArgsDecrArg b
+ check_nested_fix_body renv' (decr-1) recArgsDecrArg b
| _ -> anomaly "Not enough abstractions in fix body"
-
+
in
- check_rec_call renv def
+ check_rec_call renv [] def
let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
diff --git a/checker/inductive.mli b/checker/inductive.mli
index e658a798..2cf7c70d 100644
--- a/checker/inductive.mli
+++ b/checker/inductive.mli
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: inductive.mli 9420 2006-12-08 15:34:09Z barras $ i*)
-
(*i*)
open Names
open Term
@@ -80,6 +78,7 @@ type guard_env =
genv : subterm_spec Lazy.t list;
}
-val subterm_specif : guard_env -> constr -> subterm_spec
-val case_branches_specif : guard_env -> subterm_spec Lazy.t -> inductive ->
- constr array -> (guard_env * constr) array
+type stack_element = |SClosure of guard_env*constr |SArg of subterm_spec Lazy.t
+val subterm_specif : guard_env -> stack_element list -> constr -> subterm_spec
+val branches_specif : guard_env -> subterm_spec Lazy.t -> case_info ->
+ subterm_spec Lazy.t list array
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 95387cac..9942816d 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -21,8 +21,8 @@ let refresh_arity ar =
Sort (Type u) when not (Univ.is_univ_variable u) ->
let u' = Univ.fresh_local_univ() in
mkArity (ctxt,Type u'),
- Univ.enforce_geq u' u Univ.Constraint.empty
- | _ -> ar, Univ.Constraint.empty
+ Univ.enforce_geq u' u Univ.empty_constraint
+ | _ -> ar, Univ.empty_constraint
let check_constant_declaration env kn cb =
Flags.if_verbose msgnl (str " checking cst: " ++ prcon kn);
@@ -33,7 +33,7 @@ let check_constant_declaration env kn cb =
let ty, cu = refresh_arity ty in
let envty = add_constraints cu env' in
let _ = infer_type envty ty in
- (match cb.const_body with
+ (match body_of_constant cb with
| Some bd ->
let j = infer env' (force_constr bd) in
conv_leq envty j ty
@@ -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 =
@@ -117,14 +110,19 @@ let check_definition_sub env cb1 cb2 =
let typ1 = Typeops.type_of_constant_type env cb1.const_type in
let typ2 = Typeops.type_of_constant_type env cb2.const_type in
check_type env typ1 typ2;
- (match cb2 with
- | {const_body=Some lc2;const_opaque=false} ->
- let c2 = force_constr lc2 in
- let c1 = match cb1.const_body with
- | Some lc1 -> force_constr lc1
- | None -> assert false in
- Reduction.conv env c1 c2
- | _ -> ())
+ (* In the spirit of subtyping.check_constant, we accept
+ any implementations of parameters and opaques terms,
+ as long as they have the right type *)
+ (match cb2.const_body with
+ | Undef _ | OpaqueDef _ -> ()
+ | Def lc2 ->
+ (match cb1.const_body with
+ | Def lc1 ->
+ let c1 = force_constr lc1 in
+ let c2 = force_constr lc2 in
+ Reduction.conv env c1 c2
+ (* Coq only places transparent cb in With_definition_body *)
+ | _ -> assert false))
let lookup_modtype mp env =
try Environ.lookup_modtype mp env
@@ -259,14 +257,14 @@ and check_module env mp mb =
{typ_mp=mp;
typ_expr=sign;
typ_expr_alg=None;
- typ_constraints=Univ.Constraint.empty;
+ typ_constraints=Univ.empty_constraint;
typ_delta = mb.mod_delta;}
and mtb2 =
{typ_mp=mp;
typ_expr=mb.mod_type;
typ_expr_alg=None;
- typ_constraints=Univ.Constraint.empty;
- typ_delta = mb.mod_delta;};
+ typ_constraints=Univ.empty_constraint;
+ typ_delta = mb.mod_delta;}
in
let env = add_module (module_body_of_type mp mtb1) env in
check_subtypes env mtb1 mtb2
diff --git a/checker/mod_checking.mli b/checker/mod_checking.mli
new file mode 100644
index 00000000..8021ed0f
--- /dev/null
+++ b/checker/mod_checking.mli
@@ -0,0 +1,9 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+val check_module : Environ.env -> Names.module_path -> Declarations.module_body -> unit
diff --git a/checker/modops.ml b/checker/modops.ml
index 38aeaee2..2dc5d062 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: modops.ml 9872 2007-05-30 16:01:18Z soubiran $ i*)
-
(*i*)
open Util
open Pp
@@ -25,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")
@@ -61,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;
@@ -75,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
@@ -112,23 +95,16 @@ and add_module mb env =
let strengthen_const mp_from l cb resolver =
- match cb.const_opaque, cb.const_body with
- | false, Some _ -> cb
- | true, Some _
- | _, None ->
+ match cb.const_body with
+ | Def _ -> cb
+ | _ ->
let con = make_con mp_from empty_dirpath l in
- (* let con = constant_of_delta resolver con in*)
- let const = Const con in
- let const_subs = Some (Declarations.from_val const) in
- {cb with
- const_body = const_subs;
- const_opaque = false;
- }
-
+ (* let con = constant_of_delta resolver con in*)
+ { cb with const_body = Def (Declarations.from_val (Const con)) }
let rec strengthen_mod mp_from mp_to mb =
if Declarations.mp_in_delta mb.mod_mp mb.mod_delta then
- mb
+ mb
else
match mb.mod_type with
| SEBstruct (sign) ->
@@ -154,34 +130,33 @@ and strengthen_sig mp_from sign mp_to resolver =
resolve_out,item'::rest'
| (_,SFBmind _ as item):: rest ->
let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
- resolve_out,item::rest'
+ resolve_out,item::rest'
| (l,SFBmodule mb) :: rest ->
let mp_from' = MPdot (mp_from,l) in
let mp_to' = MPdot(mp_to,l) in
let mb_out = strengthen_mod mp_from' mp_to' mb in
let item' = l,SFBmodule (mb_out) in
let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
- resolve_out, item'::rest'
- | (l,SFBmodtype mty as item) :: rest ->
+ resolve_out (*add_delta_resolver resolve_out mb.mod_delta*),
+ item':: rest'
+ | (l,SFBmodtype mty as item) :: rest ->
let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
- resolve_out, item::rest'
+ resolve_out,item::rest'
let strengthen mtb mp =
match mtb.typ_expr with
- | SEBstruct (sign) ->
+ | SEBstruct (sign) ->
let resolve_out,sign_out =
- strengthen_sig mtb.typ_mp sign mp mtb.typ_delta
- in
- {mtb with
- typ_expr = SEBstruct(sign_out);
- typ_delta = resolve_out(*add_delta_resolver mtb.typ_delta
+ strengthen_sig mtb.typ_mp sign mp mtb.typ_delta in
+ {mtb with
+ typ_expr = SEBstruct(sign_out);
+ typ_delta = resolve_out(*add_delta_resolver mtb.typ_delta
(add_mp_delta_resolver mtb.typ_mp mp resolve_out)*)}
| SEBfunctor _ -> mtb
| _ -> anomaly "Modops:the evaluation of the structure failed "
let subst_and_strengthen mb mp =
- strengthen_mod mb.mod_mp mp
- (subst_module (map_mp mb.mod_mp mp) mb)
+ strengthen_mod mb.mod_mp mp (subst_module (map_mp mb.mod_mp mp) mb)
let module_type_of_module mp mb =
diff --git a/checker/modops.mli b/checker/modops.mli
index 2f9f2e8c..5ed7b0ce 100644
--- a/checker/modops.mli
+++ b/checker/modops.mli
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: modops.mli 9821 2007-05-11 17:00:58Z aspiwack $ i*)
-
(*i*)
open Util
open Names
@@ -33,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 : module_type_body -> module_path -> module_type_body
val subst_and_strengthen : module_body -> module_path -> module_body
diff --git a/checker/reduction.ml b/checker/reduction.ml
index ba8ceeef..3aeaa102 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: reduction.ml 9215 2006-10-05 15:40:31Z herbelin $ *)
-
open Util
open Names
open Term
@@ -80,11 +78,11 @@ let pure_stack lfts stk =
(* Reduction Functions *)
(****************************************************************************)
-let whd_betaiotazeta env x =
+let whd_betaiotazeta x =
match x with
| (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _|
Prod _|Lambda _|Fix _|CoFix _) -> x
- | _ -> whd_val (create_clos_infos betaiotazeta env) (inject x)
+ | _ -> whd_val (create_clos_infos betaiotazeta empty_env) (inject x)
let whd_betadeltaiota env t =
match t with
@@ -107,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 *)
(********************************************************************)
@@ -219,7 +208,7 @@ let rec ccnv univ cv_pb infos lft1 lft2 term1 term2 =
and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
Util.check_for_interrupt ();
(* First head reduce both terms *)
- let rec whd_both (t1,stk1) (t2,stk2) =
+ let rec whd_both (t1,stk1) (t2,stk2) =
let st1' = whd_stack infos t1 stk1 in
let st2' = whd_stack infos t2 stk2 in
(* Now, whd_stack on term2 might have modified st1 (due to sharing),
@@ -279,20 +268,10 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
| None -> raise NotConvertible) in
eqappr univ cv_pb infos app1 app2)
- (* only one constant, defined var or defined rel *)
- | (FFlex fl1, _) ->
- (match unfold_reference infos fl1 with
- | Some def1 ->
- eqappr univ cv_pb infos (lft1, whd_stack infos def1 v1) appr2
- | None -> raise NotConvertible)
- | (_, FFlex fl2) ->
- (match unfold_reference infos fl2 with
- | Some def2 ->
- eqappr univ cv_pb infos appr1 (lft2, whd_stack infos def2 v2)
- | None -> raise NotConvertible)
-
(* other constructors *)
| (FLambda _, FLambda _) ->
+ (* Inconsistency: we tolerate that v1, v2 contain shift and update but
+ we throw them away *)
assert (is_empty_stack v1 && is_empty_stack v2);
let (_,ty1,bd1) = destFLambda mk_clos hd1 in
let (_,ty2,bd2) = destFLambda mk_clos hd2 in
@@ -305,6 +284,32 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
ccnv univ CONV infos el1 el2 c1 c'1;
ccnv univ cv_pb infos (el_lift el1) (el_lift el2) c2 c'2
+ (* Eta-expansion on the fly *)
+ | (FLambda _, _) ->
+ if v1 <> [] then
+ anomaly "conversion was given unreduced term (FLambda)";
+ let (_,_ty1,bd1) = destFLambda mk_clos hd1 in
+ eqappr univ CONV infos
+ (el_lift lft1,(bd1,[])) (el_lift lft2,(hd2,eta_expand_stack v2))
+ | (_, FLambda _) ->
+ if v2 <> [] then
+ anomaly "conversion was given unreduced term (FLambda)";
+ let (_,_ty2,bd2) = destFLambda mk_clos hd2 in
+ eqappr univ CONV infos
+ (el_lift lft1,(hd1,eta_expand_stack v1)) (el_lift lft2,(bd2,[]))
+
+ (* only one constant, defined var or defined rel *)
+ | (FFlex fl1, _) ->
+ (match unfold_reference infos fl1 with
+ | Some def1 ->
+ eqappr univ cv_pb infos (lft1, whd_stack infos def1 v1) appr2
+ | None -> raise NotConvertible)
+ | (_, FFlex fl2) ->
+ (match unfold_reference infos fl2 with
+ | Some def2 ->
+ eqappr univ cv_pb infos appr1 (lft2, whd_stack infos def2 v2)
+ | None -> raise NotConvertible)
+
(* Inductive types: MutInd MutConstruct Fix Cofix *)
| (FInd ind1, FInd ind2) ->
@@ -367,37 +372,18 @@ and convert_vect univ infos lft1 lft2 v1 v2 =
let clos_fconv cv_pb env t1 t2 =
let infos = create_clos_infos betaiotazeta env in
let univ = universes env in
- ccnv univ cv_pb infos ELID ELID (inject t1) (inject t2)
+ ccnv univ cv_pb infos el_id el_id (inject t1) (inject t2)
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 *)
@@ -452,9 +438,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 8e69da44..6695fd03 100644
--- a/checker/reduction.mli
+++ b/checker/reduction.mli
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: reduction.mli 7639 2005-12-02 10:01:15Z gregoire $ i*)
-
(*i*)
open Term
open Environ
@@ -16,7 +14,7 @@ open Environ
(************************************************************************)
(*s Reduction functions *)
-val whd_betaiotazeta : env -> constr -> constr
+val whd_betaiotazeta : constr -> constr
val whd_betadeltaiota : env -> constr -> constr
val whd_betadeltaiota_nolet : env -> constr -> constr
@@ -31,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
@@ -40,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
@@ -54,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 a669c5e8..bc067dc5 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -1,19 +1,16 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: safe_typing.ml 10275 2007-10-30 11:01:24Z barras $ *)
-
open Pp
open Util
open Names
open Declarations
open Environ
-open Mod_checking
(************************************************************************)
(*
@@ -21,7 +18,6 @@ open Mod_checking
*)
let genv = ref empty_env
-let reset () = genv := empty_env
let get_env () = !genv
let set_engagement c =
@@ -63,51 +59,116 @@ let check_imports f caller env needed =
List.iter check needed
-
-(* Remove the body of opaque constants in modules *)
-(* also remove mod_expr ? Good idea!*)
-let rec lighten_module mb =
- { mb with
- mod_expr = Option.map lighten_modexpr mb.mod_expr;
- mod_type = lighten_modexpr mb.mod_type }
-
-and lighten_struct struc =
- let lighten_body (l,body) = (l,match body with
- | SFBconst ({const_opaque=true} as x) -> SFBconst {x with const_body=None}
- | (SFBconst _ | SFBmind _ ) as x -> x
- | SFBmodule m -> SFBmodule (lighten_module m)
- | SFBmodtype m -> SFBmodtype
- ({m with
- typ_expr = lighten_modexpr m.typ_expr}))
- in
- List.map lighten_body struc
-
-and lighten_modexpr = function
- | SEBfunctor (mbid,mty,mexpr) ->
- SEBfunctor (mbid,
- ({mty with
- typ_expr = lighten_modexpr mty.typ_expr}),
- lighten_modexpr mexpr)
- | SEBident mp as x -> x
- | SEBstruct ( struc) ->
- SEBstruct ( lighten_struct struc)
- | SEBapply (mexpr,marg,u) ->
- SEBapply (lighten_modexpr mexpr,lighten_modexpr marg,u)
- | SEBwith (seb,wdcl) ->
- SEBwith (lighten_modexpr seb,wdcl)
-
-let lighten_library (dp,mb,depends,s) = (dp,lighten_module mb,depends,s)
-
-
type compiled_library =
dir_path *
module_body *
(dir_path * Digest.t) list *
engagement option
+ (* Store the body of modules' opaque constants inside a table.
+
+ This module is used during the serialization and deserialization
+ of vo files.
+
+ By adding an indirection to the opaque constant definitions, we
+ gain the ability not to load them. As these constant definitions
+ are usually big terms, we save a deserialization time as well as
+ some memory space. *)
+module LightenLibrary : sig
+ type table
+ type lightened_compiled_library
+ val load : table -> lightened_compiled_library -> compiled_library
+end = struct
+
+ (* The table is implemented as an array of [constr_substituted].
+ Keys are hence integers. To avoid changing the [compiled_library]
+ type, we brutally encode integers into [lazy_constr]. This isn't
+ pretty, but shouldn't be dangerous since the produced structure
+ [lightened_compiled_library] is abstract and only meant for writing
+ to .vo via Marshal (which doesn't care about types).
+ *)
+ type table = constr_substituted array
+ let key_of_lazy_constr (c:lazy_constr) = (Obj.magic c : int)
+
+ (* To avoid any future misuse of the lightened library that could
+ interpret encoded keys as real [constr_substituted], we hide
+ these kind of values behind an abstract datatype. *)
+ type lightened_compiled_library = compiled_library
+
+ (* Map a [compiled_library] to another one by just updating
+ the opaque term [t] to [on_opaque_const_body t]. *)
+ let traverse_library on_opaque_const_body =
+ let rec traverse_module mb =
+ match mb.mod_expr with
+ None ->
+ { mb with
+ mod_expr = None;
+ mod_type = traverse_modexpr mb.mod_type;
+ }
+ | Some impl when impl == mb.mod_type->
+ let mtb = traverse_modexpr mb.mod_type in
+ { mb with
+ mod_expr = Some mtb;
+ mod_type = mtb;
+ }
+ | Some impl ->
+ { mb with
+ mod_expr = Option.map traverse_modexpr mb.mod_expr;
+ mod_type = traverse_modexpr mb.mod_type;
+ }
+ and traverse_struct struc =
+ let traverse_body (l,body) = (l,match body with
+ | (SFBconst cb) when is_opaque cb ->
+ SFBconst {cb with const_body = on_opaque_const_body cb.const_body}
+ | (SFBconst _ | SFBmind _ ) as x ->
+ x
+ | SFBmodule m ->
+ SFBmodule (traverse_module m)
+ | SFBmodtype m ->
+ SFBmodtype ({m with typ_expr = traverse_modexpr m.typ_expr}))
+ in
+ List.map traverse_body struc
+
+ and traverse_modexpr = function
+ | SEBfunctor (mbid,mty,mexpr) ->
+ SEBfunctor (mbid,
+ ({mty with
+ typ_expr = traverse_modexpr mty.typ_expr}),
+ traverse_modexpr mexpr)
+ | SEBident mp as x -> x
+ | SEBstruct (struc) ->
+ SEBstruct (traverse_struct struc)
+ | SEBapply (mexpr,marg,u) ->
+ SEBapply (traverse_modexpr mexpr,traverse_modexpr marg,u)
+ | SEBwith (seb,wdcl) ->
+ SEBwith (traverse_modexpr seb,wdcl)
+ in
+ fun (dp,mb,depends,s) -> (dp,traverse_module mb,depends,s)
+
+ (* Loading is also a traversing that decodes the embedded keys that
+ are inside the [lightened_library]. If the [load_proof] flag is
+ set, we lookup inside the table to graft the
+ [constr_substituted]. Otherwise, we set the [const_body] field
+ to [None].
+ *)
+ let load table lightened_library =
+ let decode_key = function
+ | Undef _ | Def _ -> assert false
+ | OpaqueDef k ->
+ let k = key_of_lazy_constr k in
+ let body =
+ try table.(k)
+ with _ -> error "Error while retrieving an opaque body"
+ in
+ OpaqueDef (lazy_constr_from_val body)
+ in
+ traverse_library decode_key lightened_library
+
+end
+
open Validate
-let val_deps = val_list (val_tuple"dep"[|val_dp;no_val|])
-let val_vo = val_tuple "vo" [|val_dp;val_module;val_deps;val_opt val_eng|]
+let val_deps = val_list (val_tuple ~name:"dep"[|val_dp;no_val|])
+let val_vo = val_tuple ~name:"vo" [|val_dp;val_module;val_deps;val_opt val_eng|]
(* This function should append a certificate to the .vo file.
The digest must be part of the certicate to rule out attackers
@@ -124,15 +185,15 @@ let import file (dp,mb,depends,engmt as vo) digest =
let env = !genv in
check_imports msg_warning dp env depends;
check_engagement env engmt;
- check_module (add_constraints mb.mod_constraints env) mb.mod_mp mb;
+ Mod_checking.check_module (add_constraints mb.mod_constraints env) mb.mod_mp mb;
stamp_library file digest;
(* We drop proofs once checked *)
(* let mb = lighten_module mb in*)
full_add_module dp mb digest
(* When the module is admitted, digests *must* match *)
-let unsafe_import file (dp,mb,depends,engmt) digest =
-(* if !Flags.debug then Validate.apply !Flags.debug val_vo vo;*)
+let unsafe_import file (dp,mb,depends,engmt as vo) digest =
+ if !Flags.debug then ignore vo; (*Validate.apply !Flags.debug val_vo vo;*)
let env = !genv in
check_imports (errorlabstrm"unsafe_import") dp env depends;
check_engagement env engmt;
diff --git a/checker/safe_typing.mli b/checker/safe_typing.mli
index 00aa1a84..cd2c06d2 100644
--- a/checker/safe_typing.mli
+++ b/checker/safe_typing.mli
@@ -1,20 +1,17 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: safe_typing.mli 9821 2007-05-11 17:00:58Z aspiwack $ i*)
-
(*i*)
open Names
open Term
open Environ
(*i*)
-val reset : unit -> unit
val get_env : unit -> env
(* exporting and importing modules *)
@@ -25,3 +22,19 @@ val import :
System.physical_path -> compiled_library -> Digest.t -> unit
val unsafe_import :
System.physical_path -> compiled_library -> Digest.t -> unit
+
+(** Store the body of modules' opaque constants inside a table.
+
+ This module is used during the serialization and deserialization
+ of vo files.
+*)
+module LightenLibrary :
+sig
+ type table
+ type lightened_compiled_library
+
+ (** [load table lcl] builds a compiled library from a
+ lightened library [lcl] by remplacing every index by its related
+ opaque terms inside [table]. *)
+ val load : table -> lightened_compiled_library -> compiled_library
+end
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 4f113cf9..0c97254b 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: subtyping.ml 10664 2008-03-14 11:27:37Z soubiran $ i*)
-
(*i*)
open Util
open Names
@@ -239,22 +237,29 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
match info1 with
| Constant cb1 ->
assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ;
- (*Start by checking types*)
- let cb1 = subst_const_body subst1 cb1 in
- let cb2 = subst_const_body subst2 cb2 in
- let typ1 = Typeops.type_of_constant_type env cb1.const_type in
- let typ2 = Typeops.type_of_constant_type env cb2.const_type in
- check_type env typ1 typ2;
- let con = make_con mp1 empty_dirpath l in
- (match cb2 with
- | {const_body=Some lc2;const_opaque=false} ->
- let c2 = force_constr lc2 in
- let c1 = match cb1.const_body with
- | Some lc1 -> force_constr lc1
- | None -> Const con
- in
- check_conv conv env c1 c2
- | _ -> ())
+ let cb1 = subst_const_body subst1 cb1 in
+ let cb2 = subst_const_body subst2 cb2 in
+ (*Start by checking types*)
+ let typ1 = Typeops.type_of_constant_type env cb1.const_type in
+ let typ2 = Typeops.type_of_constant_type env cb2.const_type in
+ check_type env typ1 typ2;
+ (* Now we check the bodies:
+ - A transparent constant can only be implemented by a compatible
+ transparent constant.
+ - In the signature, an opaque is handled just as a parameter:
+ anything of the right type can implement it, even if bodies differ.
+ *)
+ (match cb2.const_body with
+ | Undef _ | OpaqueDef _ -> ()
+ | Def lc2 ->
+ (match cb1.const_body with
+ | Undef _ | OpaqueDef _ -> error ()
+ | Def lc1 ->
+ (* NB: cb1 might have been strengthened and appear as transparent.
+ Anyway [check_conv] will handle that afterwards. *)
+ let c1 = force_constr lc1 in
+ let c2 = force_constr lc2 in
+ check_conv conv env c1 c2))
| IndType ((kn,i),mind1) ->
ignore (Util.error (
"The kernel does not recognize yet that a parameter can be " ^
@@ -262,7 +267,7 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
"inductive type and give a definition to map the old name to the new " ^
"name."));
assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ;
- if cb2.const_body <> None then error () ;
+ if constant_has_body cb2 then error () ;
let arity1 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in
let typ2 = Typeops.type_of_constant_type env cb2.const_type in
check_conv conv_leq env arity1 typ2
@@ -273,7 +278,7 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
"constructor and give a definition to map the old name to the new " ^
"name."));
assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ;
- if cb2.const_body <> None then error () ;
+ if constant_has_body cb2 then error () ;
let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in
let ty2 = Typeops.type_of_constant_type env cb2.const_type in
check_conv conv env ty1 ty2
@@ -281,7 +286,7 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
let rec check_modules env msb1 msb2 subst1 subst2 =
let mty1 = module_type_of_module None msb1 in
- let mty2 = module_type_of_module None msb2 in
+ let mty2 = module_type_of_module None msb2 in
check_modtypes env mty1 mty2 subst1 subst2 false;
@@ -363,11 +368,5 @@ and check_modtypes env mtb1 mtb2 subst1 subst2 equiv =
else check_structure env mtb1' mtb2' equiv subst1 subst2
let check_subtypes env sup super =
- (*if sup<>super then*)
check_modtypes env (strengthen 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
+ (map_mp super.typ_mp sup.typ_mp) false
diff --git a/checker/subtyping.mli b/checker/subtyping.mli
index d9cbe5ad..ecdf5577 100644
--- a/checker/subtyping.mli
+++ b/checker/subtyping.mli
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: subtyping.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
-
(*i*)
open Univ
open Term
@@ -19,6 +17,5 @@ open Environ
known by [env] *)
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 61369586..ab40b6fa 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: term.ml 10098 2007-08-27 11:41:08Z herbelin $ *)
-
(* This module instantiates the structure of generic deBruijn terms to Coq *)
open Util
@@ -31,15 +29,15 @@ type case_printing =
{ ind_nargs : int; (* length of the arity of the inductive type *)
style : case_style }
type case_info =
- { ci_ind : inductive;
- ci_npar : int;
- ci_cstr_nargs : int array; (* number of real args of each constructor *)
- ci_pp_info : case_printing (* not interpreted by the kernel *)
+ { ci_ind : inductive;
+ ci_npar : int;
+ ci_cstr_ndecls : int array; (* number of pattern var of each constructor *)
+ ci_pp_info : case_printing (* not interpreted by the kernel *)
}
let val_ci =
let val_cstyle = val_enum "case_style" 5 in
- let val_cprint = val_tuple "case_printing" [|val_int;val_cstyle|] in
- val_tuple "case_info" [|val_ind;val_int;val_array val_int;val_cprint|]
+ let val_cprint = val_tuple ~name:"case_printing" [|val_int;val_cstyle|] in
+ val_tuple ~name:"case_info" [|val_ind;val_int;val_array val_int;val_cprint|]
(* Sorts. *)
@@ -73,13 +71,14 @@ type 'constr pfixpoint =
type 'constr pcofixpoint =
int * 'constr prec_declaration
-let val_evar f = val_tuple "pexistential" [|val_int;val_array f|]
+let val_evar f = val_tuple ~name:"pexistential" [|val_int;val_array f|]
let val_prec f =
- val_tuple "prec_declaration"[|val_array val_name; val_array f; val_array f|]
+ val_tuple ~name:"prec_declaration"
+ [|val_array val_name; val_array f; val_array f|]
let val_fix f =
- val_tuple"pfixpoint"
- [|val_tuple"fix2"[|val_array val_int;val_int|];val_prec f|]
-let val_cofix f = val_tuple"pcofixpoint"[|val_int;val_prec f|]
+ val_tuple ~name:"pfixpoint"
+ [|val_tuple~name:"fix2"[|val_array val_int;val_int|];val_prec f|]
+let val_cofix f = val_tuple ~name:"pcofixpoint"[|val_int;val_prec f|]
type cast_kind = VMcast | DEFAULTcast
let val_cast = val_enum "cast_kind" 2
@@ -262,7 +261,7 @@ let rec exliftn el c = match c with
(* Lifting the binding depth across k bindings *)
let liftn k n =
- match el_liftn (pred n) (el_shft k ELID) with
+ match el_liftn (pred n) (el_shft k el_id) with
| ELID -> (fun c -> c)
| el -> exliftn el
@@ -313,22 +312,15 @@ let subst1 lam = substl [lam]
(***************************************************************************)
let val_ndecl =
- val_tuple"named_declaration"[|val_id;val_opt val_constr;val_constr|]
+ val_tuple ~name:"named_declaration"[|val_id;val_opt val_constr;val_constr|]
let val_rdecl =
- val_tuple"rel_declaration"[|val_name;val_opt val_constr;val_constr|]
+ val_tuple ~name:"rel_declaration"[|val_name;val_opt val_constr;val_constr|]
let val_nctxt = val_list val_ndecl
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
@@ -439,7 +431,6 @@ let decompose_prod_n_assum n =
(***************************)
type arity = rel_context * sorts
-let val_arity = val_tuple"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 1367e581..0340c79b 100644
--- a/checker/term.mli
+++ b/checker/term.mli
@@ -12,7 +12,7 @@ type case_printing = { ind_nargs : int; style : case_style; }
type case_info = {
ci_ind : inductive;
ci_npar : int;
- ci_cstr_nargs : int array;
+ ci_cstr_ndecls : int array;
ci_pp_info : case_printing;
}
type contents = Pos | Null
@@ -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 :
@@ -111,8 +103,8 @@ val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool
val eq_constr : constr -> constr -> bool
(* Validation *)
-val val_sortfam : Obj.t -> unit
-val val_sort : Obj.t -> unit
-val val_constr : Obj.t -> unit
-val val_rctxt : Obj.t -> unit
-val val_nctxt : Obj.t -> unit
+val val_sortfam : Validate.func
+val val_sort : Validate.func
+val val_constr : Validate.func
+val val_rctxt : Validate.func
+val val_nctxt : Validate.func
diff --git a/checker/type_errors.ml b/checker/type_errors.ml
index bd3bb90d..12609832 100644
--- a/checker/type_errors.ml
+++ b/checker/type_errors.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: type_errors.ml 8845 2006-05-23 07:41:58Z herbelin $ *)
-
open Names
open Term
open Environ
@@ -22,7 +20,7 @@ type guard_error =
(* Fixpoints *)
| NotEnoughAbstractionInFixBody
| RecursionNotOnInductiveType of constr
- | RecursionOnIllegalTerm of int * constr * int list * int list
+ | RecursionOnIllegalTerm of int * (env * constr) * int list * int list
| NotEnoughArgumentsForFixCall of int
(* CoFixpoints *)
| CodomainNotInductiveType of constr
@@ -94,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 82cb3c55..17a210ef 100644
--- a/checker/type_errors.mli
+++ b/checker/type_errors.mli
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: type_errors.mli 8845 2006-05-23 07:41:58Z herbelin $ i*)
-
(*i*)
open Names
open Term
@@ -24,7 +22,7 @@ type guard_error =
(* Fixpoints *)
| NotEnoughAbstractionInFixBody
| RecursionNotOnInductiveType of constr
- | RecursionOnIllegalTerm of int * constr * int list * int list
+ | RecursionOnIllegalTerm of int * (env * constr) * int list * int list
| NotEnoughArgumentsForFixCall of int
(* CoFixpoints *)
| CodomainNotInductiveType of constr
@@ -86,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 dffc9fe1..5226db53 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: typeops.ml 9314 2006-10-29 20:11:08Z herbelin $ *)
-
open Util
open Names
open Univ
@@ -91,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 =
@@ -135,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 =
@@ -291,7 +255,7 @@ let refresh_arity env ar =
match hd with
Sort (Type u) when not (is_univ_variable u) ->
let u' = fresh_local_univ() in
- let env' = add_constraints (enforce_geq u' u Constraint.empty) env in
+ let env' = add_constraints (enforce_geq u' u empty_constraint) env in
env', mkArity (ctxt,Type u')
| _ -> env, ar
@@ -406,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/typeops.mli b/checker/typeops.mli
index f4f29fe5..eafe4735 100644
--- a/checker/typeops.mli
+++ b/checker/typeops.mli
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: typeops.mli 9427 2006-12-11 18:46:35Z bgregoir $ i*)
-
(*i*)
open Names
open Term
diff --git a/checker/validate.ml b/checker/validate.ml
index 7d368f05..c5e0bd34 100644
--- a/checker/validate.ml
+++ b/checker/validate.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
-
(* This module defines validation functions to ensure an imported
value (using input_value) has the correct structure. *)
@@ -38,44 +36,59 @@ let pr_obj o = pr_obj_rec o; Format.print_newline()
(**************************************************************************)
(* Obj low-level validators *)
-exception ValidObjError of string * Obj.t
-let fail o s = raise (ValidObjError(s,o))
+type error_context = string list
+let mt_ec : error_context = []
+let (/) (ctx:error_context) s : error_context = s::ctx
+let overr (ctx:error_context) f = (fun (_:error_context) -> f ctx)
+let ext s f (ctx:error_context) = f (ctx/s)
+
-let ep s1 f s2 = f (s1^"/"^s2)
+exception ValidObjError of string * error_context * Obj.t
+let fail ctx o s = raise (ValidObjError(s,ctx,o))
+
+type func = error_context -> Obj.t -> unit
let apply debug f x =
let o = Obj.repr x in
- try f o
- with ValidObjError(msg,obj) ->
+ try f mt_ec o
+ with ValidObjError(msg,ctx,obj) ->
if debug then begin
print_endline ("Validation failed: "^msg);
+ print_endline ("Context: "^String.concat"/"(List.rev ctx));
pr_obj obj
end;
failwith "vo structure validation failed"
(* data not validated *)
-let no_val (o:Obj.t) = ()
+let no_val (c:error_context) (o:Obj.t) = ()
(* Check that object o is a block with tag t *)
-let val_tag t o =
+let val_tag t ctx o =
if Obj.is_block o && Obj.tag o = t then ()
- else fail o ("expected tag "^string_of_int t)
+ else fail ctx o ("expected tag "^string_of_int t)
-let val_block s o =
+let val_block ctx o =
if Obj.is_block o then
(if Obj.tag o > Obj.no_scan_tag then
- fail o (s^": found no scan tag"))
- else fail o (s^": expected block obj")
+ fail ctx o "block: found no scan tag")
+ else fail ctx o "expected block obj"
(* Check that an object is a tuple (or a record). v is an array of
validation functions for each field. Its size corresponds to the
expected size of the object. *)
-let val_tuple s v o =
+let val_tuple ?name v ctx o =
+ let ctx = match name with
+ Some n -> ctx/n
+ | _ -> ctx in
let n = Array.length v in
- val_block ("tuple: "^s) o;
- if Obj.size o = n then Array.iteri (fun i f -> f (Obj.field o i)) v
+ let val_fld i f =
+ f (ctx/("fld="^string_of_int i)) (Obj.field o i) in
+ val_block ctx o;
+ if Obj.size o = n then Array.iteri val_fld v
else
- fail o ("tuple:" ^s^" size found:"^string_of_int (Obj.size o))
+ fail ctx o
+ ("tuple size: found "^string_of_int (Obj.size o)^
+ ", expected "^string_of_int n)
(* Check that the object is either a constant constructor of tag < cc,
or a constructed variant. each element of vv is an array of
@@ -83,70 +96,79 @@ let val_tuple s v o =
The size of vv corresponds to the number of non-constant
constructors, and the size of vv.(i) is the expected arity of the
i-th non-constant constructor. *)
-let val_sum s cc vv o =
+let val_sum name cc vv ctx o =
+ let ctx = ctx/name in
if Obj.is_block o then
- (val_block s o;
+ (val_block (ctx/name) o;
let n = Array.length vv in
let i = Obj.tag o in
- if i < n then val_tuple (s^"(tag "^string_of_int i^")") vv.(i) o
- else fail o ("bad tag in (sum type) "^s^": found "^string_of_int i))
+ let ctx' = if n=1 then ctx else ctx/("tag="^string_of_int i) in
+ if i < n then val_tuple vv.(i) ctx' o
+ else fail ctx' o ("sum: unexpected tag"))
else if Obj.is_int o then
let (n:int) = Obj.magic o in
(if n<0 || n>=cc then
- fail o (s^": bad constant constructor "^string_of_int n))
- else fail o ("not a sum ("^s^")")
+ fail ctx o ("bad constant constructor "^string_of_int n))
+ else fail ctx o "not a sum"
let val_enum s n = val_sum s n [||]
(* Recursive types: avoid looping by eta-expansion *)
-let rec val_rec_sum s cc f o =
- val_sum s cc (f (val_rec_sum s cc f)) o
-
-let rec val_rectype f o =
- f (val_rectype f) o
+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
(**************************************************************************)
(* Builtin types *)
(* Check the o is an array of values satisfying f. *)
-let val_array ?(name="array") f o =
- val_block name o;
+let val_array ?(pos=false) f ctx o =
+ let upd_ctx =
+ if pos then (fun i -> ctx/string_of_int i) else (fun _ -> ctx) in
+ val_block (ctx/"array") o;
for i = 0 to Obj.size o - 1 do
- (f (Obj.field o i):unit)
+ (f (upd_ctx i) (Obj.field o i):unit)
done
(* Integer validator *)
-let val_int o =
- if not (Obj.is_int o) then fail o "expected an int"
+let val_int ctx o =
+ if not (Obj.is_int o) then fail ctx o "expected an int"
(* String validator *)
-let val_str o =
- try val_tag Obj.string_tag o
- with Failure _ -> fail o "expected a string"
+let val_str ctx o =
+ try val_tag Obj.string_tag ctx o
+ with Failure _ -> fail ctx o "expected a string"
(* Booleans *)
let val_bool = val_enum "bool" 2
(* Option type *)
-let val_opt ?(name="option") f = val_sum name 1 [|[|f|]|]
+let val_opt ?(name="option") f =
+ val_sum name 1 [|[|f|]|]
(* Lists *)
-let val_list ?(name="list") f =
- val_rec_sum name 1 (fun vlist -> [|[|f;vlist|]|])
+let val_list ?(name="list") f ctx =
+ val_rec_sum name 1 (fun vlist -> [|[|ext "elem" f;vlist|]|])
+ ctx
(* Reference *)
-let val_ref ?(name="ref") f = val_tuple name [|f|]
+let val_ref ?(name="ref") f ctx =
+ val_tuple [|f|] (ctx/name)
(**************************************************************************)
(* Standard library types *)
(* Sets *)
let val_set ?(name="Set.t") f =
- val_rec_sum name 1 (fun vset -> [|[|vset;f;vset;val_int|]|])
+ val_rec_sum name 1
+ (fun vset -> [|[|vset;ext "elem" f;
+ vset;ext "bal" val_int|]|])
(* Maps *)
let rec val_map ?(name="Map.t") fk fv =
- val_rec_sum name 1 (fun vmap -> [|[|vmap;fk;fv;vmap;val_int|]|])
+ val_rec_sum name 1
+ (fun vmap ->
+ [|[|vmap; ext "key" fk; ext "value" fv;
+ vmap; ext "bal" val_int|]|])
(**************************************************************************)
(* Coq types *)
@@ -158,19 +180,19 @@ let val_dp = val_list ~name:"dirpath" val_id
let val_name = val_sum "name" 1 [|[|val_id|]|]
-let val_uid = val_tuple "uniq_ident" [|val_int;val_str;val_dp|]
+let val_uid = val_tuple ~name:"uniq_ident" [|val_int;val_str;val_dp|]
let val_mp =
val_rec_sum "module_path" 0
(fun vmp -> [|[|val_dp|];[|val_uid|];[|vmp;val_id|]|])
-let val_kn = val_tuple "kernel_name" [|val_mp;val_dp;val_id|]
+let val_kn = val_tuple ~name:"kernel_name" [|val_mp;val_dp;val_id|]
let val_con =
- val_tuple "constant/mutind" [|val_kn;val_kn|]
+ val_tuple ~name:"constant/mutind" [|val_kn;val_kn|]
-let val_ind = val_tuple "inductive"[|val_con;val_int|]
-let val_cstr = val_tuple "constructor"[|val_ind;val_int|]
+let val_ind = val_tuple ~name:"inductive"[|val_con;val_int|]
+let val_cstr = val_tuple ~name:"constructor"[|val_ind;val_int|]
(* univ *)
let val_level = val_sum "level" 1 [|[|val_dp;val_int|]|]
@@ -179,5 +201,5 @@ let val_univ = val_sum "univ" 0
let val_cstrs =
val_set ~name:"Univ.constraints"
- (val_tuple "univ_constraint"
+ (val_tuple ~name:"univ_constraint"
[|val_level;val_enum "order_request" 3;val_level|])