summaryrefslogtreecommitdiff
path: root/checker
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
commit5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch)
tree631ad791a7685edafeb1fb2e8faeedc8379318ae /checker
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'checker')
-rw-r--r--checker/check.ml36
-rw-r--r--checker/check.mllib34
-rw-r--r--checker/check_stat.ml6
-rw-r--r--checker/checker.ml108
-rw-r--r--checker/closure.ml52
-rw-r--r--checker/closure.mli5
-rw-r--r--checker/declarations.ml875
-rw-r--r--checker/declarations.mli69
-rw-r--r--checker/environ.ml109
-rw-r--r--checker/environ.mli16
-rw-r--r--checker/include24
-rw-r--r--checker/indtypes.ml120
-rw-r--r--checker/inductive.ml164
-rw-r--r--checker/mod_checking.ml305
-rw-r--r--checker/modops.ml405
-rw-r--r--checker/modops.mli32
-rw-r--r--checker/reduction.ml51
-rw-r--r--checker/reduction.mli5
-rw-r--r--checker/safe_typing.ml40
-rw-r--r--checker/subtyping.ml252
-rw-r--r--checker/term.ml82
-rw-r--r--checker/type_errors.ml4
-rw-r--r--checker/type_errors.mli12
-rw-r--r--checker/typeops.ml66
-rw-r--r--checker/validate.ml16
25 files changed, 1516 insertions, 1372 deletions
diff --git a/checker/check.ml b/checker/check.ml
index 82df62b4..b2aa6555 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -24,10 +24,10 @@ type section_path = {
basename : string }
let dir_of_path p =
make_dirpath (List.map id_of_string p.dirpath)
-let path_of_dirpath dir =
+let path_of_dirpath dir =
match repr_dirpath dir with
[] -> failwith "path_of_dirpath"
- | l::dir ->
+ | l::dir ->
{dirpath=List.map string_of_id dir;basename=string_of_id l}
let pr_dirlist dp =
prlist_with_sep (fun _ -> str".") str (List.rev dp)
@@ -40,7 +40,7 @@ type library_objects
type compilation_unit_name = dir_path
-type library_disk = {
+type library_disk = {
md_name : compilation_unit_name;
md_compiled : Safe_typing.compiled_library;
md_objects : library_objects;
@@ -48,7 +48,7 @@ type library_disk = {
md_imports : compilation_unit_name list }
(************************************************************************)
-(*s Modules on disk contain the following informations (after the magic
+(*s Modules on disk contain the following informations (after the magic
number, and before the digest). *)
(*s Modules loaded in memory contain the following informations. They are
@@ -61,7 +61,7 @@ type library_t = {
library_deps : (compilation_unit_name * Digest.t) list;
library_digest : Digest.t }
-module LibraryOrdered =
+module LibraryOrdered =
struct
type t = dir_path
let compare d1 d2 =
@@ -121,7 +121,7 @@ let load_paths = ref ([],[] : System.physical_path list * logical_path list)
let get_load_paths () = fst !load_paths
(* Hints to partially detects if two paths refer to the same repertory *)
-let rec remove_path_dot p =
+let rec remove_path_dot p =
let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *)
let n = String.length curdir in
if String.length p > n && String.sub p 0 n = curdir then
@@ -139,7 +139,7 @@ let strip_path p =
let canonical_path_name p =
let current = Sys.getcwd () in
- try
+ try
Sys.chdir p;
let p' = Sys.getcwd () in
Sys.chdir current;
@@ -148,7 +148,7 @@ let canonical_path_name p =
(* We give up to find a canonical name and just simplify it... *)
strip_path p
-let find_logical_path phys_dir =
+let find_logical_path phys_dir =
let phys_dir = canonical_path_name phys_dir in
match list_filter2 (fun p d -> p = phys_dir) !load_paths with
| _,[dir] -> dir
@@ -159,7 +159,7 @@ 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
+ List.exists check_p lp
let remove_load_path dir =
load_paths := list_filter2 (fun p d -> p <> dir) !load_paths
@@ -171,7 +171,7 @@ let add_load_path (phys_path,coq_path) =
let phys_path = canonical_path_name phys_path in
match list_filter2 (fun p d -> p = phys_path) !load_paths with
| _,[dir] ->
- if coq_path <> dir
+ if coq_path <> dir
(* If this is not the default -I . to coqtop *)
&& not
(phys_path = canonical_path_name Filename.current_dir_name
@@ -195,7 +195,7 @@ 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)
(************************************************************************)
@@ -235,8 +235,8 @@ let locate_qualified_library qid =
let dir =
extend_dirpath (find_logical_path path) (id_of_string qid.basename) in
(* Look if loaded *)
- try
- (dir, library_full_filename dir)
+ try
+ (dir, library_full_filename dir)
with Not_found ->
(dir, file)
with Not_found -> raise LibNotFound
@@ -245,7 +245,7 @@ let explain_locate_library_error qid = function
| LibUnmappedDir ->
let prefix = qid.dirpath in
errorlabstrm "load_absolute_library_from"
- (str "Cannot load " ++ pr_path qid ++ str ":" ++ spc () ++
+ (str "Cannot load " ++ pr_path qid ++ str ":" ++ spc () ++
str "no physical path bound to" ++ spc () ++ pr_dirlist prefix ++ fnl ())
| LibNotFound ->
errorlabstrm "load_absolute_library_from"
@@ -261,7 +261,7 @@ let try_locate_absolute_library dir =
let try_locate_qualified_library qid =
try
locate_qualified_library qid
- with e ->
+ with e ->
explain_locate_library_error qid e
(************************************************************************)
@@ -300,7 +300,7 @@ 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,digest) =
try
let ch = with_magic_number_check raw_intern_library f in
let (md:library_disk) = System.marshal_in ch in
@@ -312,7 +312,7 @@ let intern_from_file (dir, f) =
Flags.if_verbose msgnl(str" done]");
md,digest
with e -> Flags.if_verbose msgnl(str" failed!]"); raise e in
- depgraph := LibraryMap.add md.md_name md.md_deps !depgraph;
+ depgraph := LibraryMap.add md.md_name md.md_deps !depgraph;
mk_library md f digest
let get_deps (dir, f) =
@@ -366,7 +366,7 @@ let recheck_library ~norec ~admit ~check =
let nochk = fold_deps_list LibrarySet.add nrl LibrarySet.empty in
let nochk = fold_deps_list LibrarySet.remove ml nochk in
let nochk = fold_deps_list LibrarySet.add al nochk in
- (* explicitely required modules cannot be skipped... *)
+ (* explicitly required modules cannot be skipped... *)
let nochk =
List.fold_right LibrarySet.remove (List.map fst (nrl@ml)) nochk in
(* *)
diff --git a/checker/check.mllib b/checker/check.mllib
new file mode 100644
index 00000000..08dd78bc
--- /dev/null
+++ b/checker/check.mllib
@@ -0,0 +1,34 @@
+Coq_config
+Pp_control
+Pp
+Compat
+Flags
+Segmenttree
+Unicodetable
+Util
+Option
+Hashcons
+System
+Envars
+Predicate
+Rtree
+Names
+Univ
+Esubst
+Validate
+Term
+Declarations
+Environ
+Closure
+Reduction
+Type_errors
+Modops
+Inductive
+Typeops
+Indtypes
+Subtyping
+Mod_checking
+Safe_typing
+Check
+Check_stat
+Checker
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index 6ea153a3..170ac638 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -17,7 +17,7 @@ open Environ
let memory_stat = ref false
-let print_memory_stat () =
+let print_memory_stat () =
if !memory_stat then begin
Format.printf "total heap size = %d kbytes\n" (heap_size_kb ());
Format.print_newline();
@@ -33,11 +33,11 @@ let pr_engt = function
str "Theory: Set is predicative"
let cst_filter f csts =
- Cmap.fold
+ Cmap_env.fold
(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 = cb.const_body = None
let pr_ax csts =
let axs = cst_filter is_ax csts in
diff --git a/checker/checker.ml b/checker/checker.ml
index 70e2eb97..e15c37e6 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -23,14 +23,14 @@ let parse_dir s =
if n>=len then dirs else
let pos =
try
- String.index_from s n '.'
+ String.index_from s n '.'
with Not_found -> len
in
let dir = String.sub s n (pos-n) in
- decoupe_dirs (dir::dirs) (pos+1)
+ decoupe_dirs (dir::dirs) (pos+1)
in
decoupe_dirs [] 0
-let dirpath_of_string s =
+let dirpath_of_string s =
match parse_dir s with
[] -> invalid_arg "dirpath_of_string"
| dir -> make_dirpath (List.map id_of_string dir)
@@ -43,7 +43,7 @@ let (/) = Filename.concat
let get_version_date () =
try
- let coqlib = Envars.coqlib () in
+ let coqlib = Envars.coqlib () in
let ch = open_in (Filename.concat coqlib "revision") in
let ver = input_line ch in
let rev = input_line ch in
@@ -67,8 +67,8 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath =
let convert_string d =
try id_of_string d
- with _ ->
- if_verbose warning
+ with _ ->
+ if_verbose warning
("Directory "^d^" cannot be used as a Coq identifier (skipped)");
flush_all ();
failwith "caught"
@@ -90,45 +90,38 @@ let includes = ref []
let push_include (s, alias) = includes := (s,alias,false) :: !includes
let push_rec_include (s, alias) = includes := (s,alias,true) :: !includes
-let check_coq_overwriting p =
- if string_of_id (list_last (repr_dirpath p)) = "Coq" then
- error "The \"Coq\" logical root directory is reserved for the Coq library"
-
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
- check_coq_overwriting p;
push_rec_include (d, p)
let set_include d p =
let p = dirpath_of_string p in
- check_coq_overwriting p;
push_include (d,p)
let set_rec_include d p =
let p = dirpath_of_string p in
- check_coq_overwriting p;
push_rec_include(d,p)
(* Initializes the LoadPath *)
let init_load_path () =
let coqlib = Envars.coqlib () in
let user_contrib = coqlib/"user-contrib" in
- let contrib = coqlib/"contrib" in
+ let plugins = coqlib/"plugins" in
(* first user-contrib *)
- if Sys.file_exists user_contrib then
+ if Sys.file_exists user_contrib then
add_rec_path user_contrib Check.default_root_prefix;
- (* then contrib *)
- add_rec_path contrib (Names.make_dirpath [coq_root]);
+ (* then plugins *)
+ add_rec_path plugins (Names.make_dirpath [coq_root]);
(* then standard library *)
-(* List.iter
+(* List.iter
(fun (s,alias) ->
- add_rec_path (coqlib/s) ([alias; coq_root]))
+ add_rec_path (coqlib/s) ([alias; coq_root]))
theories_dirs_map;*)
add_rec_path (coqlib/"theories") (Names.make_dirpath[coq_root]);
(* then current directory *)
add_path "." Check.default_root_prefix;
(* additional loadpath, given with -I -include -R options *)
- List.iter
+ List.iter
(fun (s,alias,reci) ->
if reci then add_rec_path s alias else add_path s alias)
(List.rev !includes);
@@ -163,7 +156,7 @@ let compile_files () =
Check.recheck_library
~norec:(List.rev !norec_list)
~admit:(List.rev !admit_list)
- ~check:(List.rev !compile_list)
+ ~check:(List.rev !compile_list)
let version () =
Printf.printf "The Coq Proof Checker, version %s (%s)\n"
@@ -180,7 +173,7 @@ let print_usage_channel co command =
" -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 -as coqdir recursively map physical dir to logical coqdir
-R dir coqdir (idem)
-admit module load module and dependencies without checking
@@ -189,9 +182,10 @@ let print_usage_channel co command =
-where print Coq's standard library location and exit
-v print Coq version and exit
-boot boot mode
- -o print the list of assumptions
- -m print the maximum heap size
-
+ -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
@@ -217,9 +211,9 @@ let anomaly_string () = str "Anomaly: "
let report () = (str "." ++ spc () ++ str "Please report.")
let print_loc loc =
- if loc = dummy_loc then
+ if loc = dummy_loc then
(str"<unknown>")
- else
+ else
let loc = unloc loc in
(int (fst loc) ++ str"-" ++ int (snd loc))
let guill s = "\""^s^"\""
@@ -228,41 +222,41 @@ let where s =
if !Flags.debug then (str"in " ++ str s ++ str":" ++ spc ()) else (mt ())
let rec explain_exn = function
- | Stream.Failure ->
+ | Stream.Failure ->
hov 0 (anomaly_string () ++ str "uncaught Stream.Failure.")
- | Stream.Error txt ->
+ | Stream.Error txt ->
hov 0 (str "Syntax error: " ++ str txt)
- | Token.Error txt ->
+ | Token.Error txt ->
hov 0 (str "Syntax error: " ++ str txt)
- | Sys_error msg ->
+ | Sys_error msg ->
hov 0 (anomaly_string () ++ str "uncaught exception Sys_error " ++ str (guill msg) ++ report() )
- | UserError(s,pps) ->
+ | UserError(s,pps) ->
hov 1 (str "User error: " ++ where s ++ pps)
- | Out_of_memory ->
+ | Out_of_memory ->
hov 0 (str "Out of memory")
- | Stack_overflow ->
+ | Stack_overflow ->
hov 0 (str "Stack overflow")
- | Anomaly (s,pps) ->
+ | 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) ++
+ 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 " from character " ++ int pos1 ++
str " to " ++ int pos2)
else
(str " at line " ++ int pos1 ++
str " character " ++ int pos2)
++ report ())
- | Not_found ->
+ | Not_found ->
hov 0 (anomaly_string () ++ str "uncaught exception Not_found" ++ report ())
- | Failure s ->
+ | Failure s ->
hov 0 (str "Failure: " ++ str s ++ report ())
- | Invalid_argument s ->
+ | Invalid_argument s ->
hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ str (guill s) ++ report ())
- | Sys.Break ->
+ | Sys.Break ->
hov 0 (fnl () ++ str "User interrupt.")
| Univ.UniverseInconsistency (o,u,v) ->
- let msg =
+ let msg =
if !Flags.debug (*!Constrextern.print_universes*) then
spc() ++ str "(cannot enforce" ++ spc() ++ (*Univ.pr_uni u ++*) spc() ++
str (match o with Univ.Lt -> "<" | Univ.Le -> "<=" | Univ.Eq -> "=")
@@ -270,12 +264,12 @@ let rec explain_exn = function
else
mt() in
hov 0 (str "Error: Universe inconsistency" ++ msg ++ str ".")
- | TypeError(ctx,te) ->
+ | TypeError(ctx,te) ->
(* hov 0 (str "Error:" ++ spc () ++ Himsg.explain_type_error ctx *)
(* te)*)
hov 0 (str "Type error")
- | Indtypes.InductiveError e ->
+ | Indtypes.InductiveError e ->
hov 0 (str "Error related to inductive types")
(* let ctx = Check.get_env() in
hov 0
@@ -286,9 +280,9 @@ let rec explain_exn = function
++ explain_exn exc)
| Assert_failure (s,b,e) ->
hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++
- (if s <> "" then
+ (if s <> "" then
if Sys.ocaml_version = "3.06" then
- (str ("(file \"" ^ s ^ "\", characters ") ++
+ (str ("(file \"" ^ s ^ "\", characters ") ++
int b ++ str "-" ++ int e ++ str ")")
else
(str ("(file \"" ^ s ^ "\", line ") ++ int b ++
@@ -298,13 +292,13 @@ let rec explain_exn = function
(mt ())) ++
report ())
| reraise ->
- hov 0 (anomaly_string () ++ str "Uncaught exception " ++
+ hov 0 (anomaly_string () ++ str "Uncaught exception " ++
str (Printexc.to_string reraise)++report())
-let parse_args() =
+let parse_args argv =
let rec parse = function
| [] -> ()
- | "-impredicative-set" :: rem ->
+ | "-impredicative-set" :: rem ->
set_engagement Declarations.ImpredicativeSet; parse rem
| ("-I"|"-include") :: d :: "-as" :: p :: rem -> set_include d p; parse rem
@@ -325,7 +319,7 @@ let parse_args() =
| ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
| ("-v"|"--version") :: _ -> version ()
- | "-boot" :: rem -> boot := true; parse rem
+ | "-boot" :: rem -> boot := true; parse rem
| ("-m" | "--memory") :: rem -> Check_stat.memory_stat := true; parse rem
| ("-o" | "--output-context") :: rem ->
Check_stat.output_context := true; parse rem
@@ -346,8 +340,8 @@ let parse_args() =
| s :: rem -> add_compile s; parse rem
in
try
- parse (List.tl (Array.to_list Sys.argv))
- with
+ parse (List.tl (Array.to_list argv))
+ with
| UserError(_,s) as e -> begin
try
Stream.empty s; exit 1
@@ -360,12 +354,12 @@ let parse_args() =
(* To prevent from doing the initialization twice *)
let initialized = ref false
-let init() =
+let init_with_argv argv =
if not !initialized then begin
initialized := true;
Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
try
- parse_args();
+ parse_args argv;
if_verbose print_header ();
init_load_path ();
engage ();
@@ -376,13 +370,15 @@ let init() =
exit 1
end
+let init() = init_with_argv Sys.argv
+
let run () =
- try
+ try
compile_files ();
flush_all()
with e ->
(Pp.ppnl(explain_exn e);
- flush_all();
+ flush_all();
exit 1)
let start () = init(); run(); Check_stat.stats(); exit 0
diff --git a/checker/closure.ml b/checker/closure.ml
index ccbfbc4c..7ccf06b9 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -38,7 +38,7 @@ let incr_cnt red cnt =
if red then begin
if !stats then incr cnt;
true
- end else
+ end else
false
let with_stats c =
@@ -127,13 +127,13 @@ module RedFlags = (struct
{ red with r_const = Idpred.remove id l1, l2 }
let red_add_transparent red tr =
- { red with r_const = tr }
+ { red with r_const = tr }
let mkflags = List.fold_left red_add no_red
let red_set red = function
| BETA -> incr_cnt red.r_beta beta
- | CONST kn ->
+ | CONST kn ->
let (_,l) = red.r_const in
let c = Cpred.mem kn l in
incr_cnt c delta
@@ -165,7 +165,7 @@ 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 unfold_red kn =
let flag = match kn with
| EvalVarRef id -> fVAR id
| EvalConstRef kn -> fCONST kn
@@ -187,7 +187,7 @@ let betadeltaiota_red = {
r_const = true,[],[];
r_zeta = true;
r_evar = true;
- r_iota = true }
+ r_iota = true }
let betaiota_red = {
r_beta = true;
@@ -195,7 +195,7 @@ let betaiota_red = {
r_zeta = false;
r_evar = false;
r_iota = true }
-
+
let beta_red = {
r_beta = true;
r_const = false,[],[];
@@ -231,7 +231,7 @@ let unfold_red kn =
(* 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
+ Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of
a LetIn expression is Letin reduction *)
type red_kind =
@@ -278,7 +278,7 @@ 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] ->
+ | 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
@@ -339,7 +339,7 @@ type 'a infos = {
let info_flags info = info.i_flags
let ref_value_cache info ref =
- try
+ try
Some (Hashtbl.find info.i_tab ref)
with Not_found ->
try
@@ -360,7 +360,7 @@ let ref_value_cache info ref =
let defined_vars flags env =
(* if red_local_const (snd flags) then*)
- fold_named_context
+ fold_named_context
(fun (id,b,_) e ->
match b with
| None -> e
@@ -370,7 +370,7 @@ let defined_vars flags env =
let defined_rels flags env =
(* if red_local_const (snd flags) then*)
- fold_rel_context
+ fold_rel_context
(fun (id,b,t) (i,subs) ->
match b with
| None -> (i+1, subs)
@@ -380,6 +380,11 @@ let defined_rels flags env =
let mind_equiv_infos info = mind_equiv info.i_env
+let eq_table_key k1 k2 =
+ match k1,k2 with
+ | ConstKey con1 ,ConstKey con2 -> eq_con_chk con1 con2
+ | _,_ -> k1=k2
+
let create mk_cl flgs env =
{ i_flags = flgs;
i_repr = mk_cl;
@@ -417,8 +422,8 @@ let neutr = function
| (Whnf|Norm) -> Whnf
| (Red|Cstr) -> Red
-type fconstr = {
- mutable norm: red_state;
+type fconstr = {
+ mutable norm: red_state;
mutable term: fterm }
and fterm =
@@ -456,7 +461,7 @@ let update v1 (no,t) =
else {norm=no;term=t}
(**********************************************************************)
-(* The type of (machine) stacks (= lambda-bar-calculus' contexts) *)
+(* The type of (machine) stacks (= lambda-bar-calculus' contexts) *)
type stack_member =
| Zapp of fconstr array
@@ -496,9 +501,6 @@ let rec decomp_stack = function
| _ ->
Some (v.(0), (Zapp (Array.sub v 1 (Array.length v - 1)) :: s)))
| _ -> None
-let rec decomp_stackn = function
- | Zapp v :: s -> if Array.length v = 0 then decomp_stackn s else (v, s)
- | _ -> assert false
let array_of_stack s =
let rec stackrec = function
| [] -> []
@@ -507,7 +509,7 @@ let array_of_stack s =
in Array.concat (stackrec s)
let rec stack_assign s p c = match s with
| Zapp args :: s ->
- let q = Array.length args in
+ let q = Array.length args in
if p >= q then
Zapp args :: stack_assign s (p-q) c
else
@@ -515,7 +517,7 @@ let rec stack_assign s p c = match s with
nargs.(p) <- c;
Zapp nargs :: s)
| _ -> s
-let rec stack_tail p s =
+let rec stack_tail p s =
if p = 0 then s else
match s with
| Zapp args :: s ->
@@ -547,8 +549,6 @@ let lift_fconstr k f =
if k=0 then f else lft_fconstr k f
let lift_fconstr_vect k v =
if k=0 then v else Array.map (fun f -> lft_fconstr k f) v
-let lift_fconstr_list k l =
- if k=0 then l else List.map (fun f -> lft_fconstr k f) l
let clos_rel e i =
match expand_rel i e with
@@ -780,7 +780,7 @@ let term_of_fconstr =
(* fstrong applies unfreeze_fun recursively on the (freeze) term and
* yields a term. Assumes that the unfreeze_fun never returns a
- * FCLOS term.
+ * FCLOS term.
let rec fstrong unfreeze_fun lfts v =
to_constr (fstrong unfreeze_fun) lfts (unfreeze_fun v)
*)
@@ -857,12 +857,6 @@ let get_nth_arg 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 *)
-let get_arg h stk =
- let (depth,stk') = strip_update_shift h stk in
- match decomp_stack stk' with
- Some (v, s') -> (Some (depth,v), s')
- | None -> (None, zshift depth stk')
-
let rec get_args n tys f e stk =
match stk with
Zupdate r :: s ->
@@ -979,7 +973,7 @@ let rec knr info m stk =
| FLambda(n,tys,f,e) when red_set info.i_flags fBETA ->
(match get_args n tys f e stk with
Inl e', s -> knit info e' f s
- | Inr lam, s -> (lam,s))
+ | Inr lam, s -> (lam,s))
| FFlex(ConstKey kn) when red_set info.i_flags (fCONST kn) ->
(match ref_value_cache info (ConstKey kn) with
Some v -> kni info v stk
diff --git a/checker/closure.mli b/checker/closure.mli
index fa302de6..4d302add 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -24,7 +24,7 @@ val with_stats: 'a Lazy.t -> 'a
(*s Delta implies all consts (both global (= by
[kernel_name]) and local (= by [Rel] or [Var])), all evars, and letin's.
- Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of
+ Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of
a LetIn expression is Letin reduction *)
type transparent_state = Idpred.t * Cpred.t
@@ -102,7 +102,7 @@ type fconstr
type fterm =
| FRel of int
| FAtom of constr (* Metas and Sorts *)
- | FCast of fconstr * cast_kind * fconstr
+ | FCast of fconstr * cast_kind * fconstr
| FFlex of table_key
| FInd of inductive
| FConstruct of constructor
@@ -177,6 +177,7 @@ val unfold_reference : clos_infos -> table_key -> fconstr option
(* [mind_equiv] checks whether two inductive types are intentionally equal *)
val mind_equiv_infos : clos_infos -> inductive -> inductive -> bool
+val eq_table_key : table_key -> table_key -> bool
(************************************************************************)
(*i This is for lazy debug *)
diff --git a/checker/declarations.ml b/checker/declarations.ml
index c6a7b4b4..699f6c90 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -30,356 +30,623 @@ let val_cst_type =
val_sum "constant_type" 0 [|[|val_constr|];[|val_rctxt;val_pol_arity|]|]
-type substitution_domain =
- MSI of mod_self_id
+type substitution_domain =
| MBI of mod_bound_id
| MPI of module_path
let val_subst_dom =
- val_sum "substitution_domain" 0 [|[|val_uid|];[|val_uid|];[|val_mp|]|]
+ val_sum "substitution_domain" 0 [|[|val_uid|];[|val_mp|]|]
-module Umap = Map.Make(struct
+module Umap = Map.Make(struct
type t = substitution_domain
let compare = Pervasives.compare
end)
-type resolver
-type substitution = (module_path * resolver option) Umap.t
+type delta_hint =
+ Inline of 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
+
+let empty_delta_resolver = Deltamap.empty
+
+type substitution = (module_path * delta_resolver) Umap.t
type 'a subst_fun = substitution -> 'a -> 'a
-let val_res = val_opt no_val
+let val_res_dom =
+ val_sum "delta_key" 0 [|[|val_kn|];[|val_mp|]|]
+
+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 val_subst =
val_map ~name:"substitution"
val_subst_dom (val_tuple "substition range" [|val_mp;val_res|])
-let fold_subst fs fb fp =
+let fold_subst fb fp =
Umap.fold
(fun k (mp,_) acc ->
match k with
- MSI msid -> fs msid mp acc
| MBI mbid -> fb mbid mp acc
| MPI mp1 -> fp mp1 mp acc)
let empty_subst = Umap.empty
-let add_msid msid mp =
- Umap.add (MSI msid) (mp,None)
let add_mbid mbid mp =
- Umap.add (MBI mbid) (mp,None)
+ Umap.add (MBI mbid) (mp,empty_delta_resolver)
let add_mp mp1 mp2 =
- Umap.add (MPI mp1) (mp2,None)
+ Umap.add (MPI mp1) (mp2,empty_delta_resolver)
-let map_msid msid mp = add_msid msid mp empty_subst
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 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"
+ in
+ try
+ sub_mp mp
+ with
+ Not_found -> mp
+
+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
+
+
+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
+
+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 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
+
+
+
+let inline_of_delta resolver =
+ let extract key hint l =
+ match key,hint with
+ |KN kn, Inline _ -> kn::l
+ | _,_ -> l
+ in
+ Deltamap.fold extract resolver []
+
+exception Not_inline
+
+let constant_of_delta_with_inline resolve con =
+ 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
+
let subst_mp0 sub mp = (* 's like subst *)
let rec aux mp =
match mp with
- | MPself sid ->
- let mp',resolve = Umap.find (MSI sid) sub in
+ | MPfile sid ->
+ let mp',resolve = Umap.find (MPI (MPfile sid)) sub in
mp',resolve
| MPbound bid ->
- let mp',resolve = Umap.find (MBI bid) sub in
- mp',resolve
+ 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
+ end
| MPdot (mp1,l) as mp2 ->
begin
- try
+ try
let mp',resolve = Umap.find (MPI mp2) sub in
mp',resolve
- with Not_found ->
+ with Not_found ->
let mp1',resolve = aux mp1 in
MPdot (mp1',l),resolve
end
- | _ -> raise Not_found
in
try
- Some (aux mp)
+ Some (aux mp)
with Not_found -> None
-
-
-let subst_mp0 sub mp = (* 's like subst *)
- let rec aux mp =
- match mp with
- | MPself sid -> fst (Umap.find (MSI sid) sub)
- | MPbound bid -> fst (Umap.find (MBI bid) sub)
- | MPdot (mp1,l) as mp2 ->
- begin
- try fst (Umap.find (MPI mp2) sub)
- with Not_found -> MPdot (aux mp1,l)
- end
-
- | _ -> raise Not_found
- in
- try Some (aux mp) with Not_found -> None
-
let subst_mp sub mp =
match subst_mp0 sub mp with
None -> mp
- | Some mp' -> mp'
+ | Some (mp',_) -> mp'
-let subst_kn0 sub kn =
+let subst_kn_delta sub kn =
let mp,dir,l = repr_kn kn in
match subst_mp0 sub mp with
- Some mp' ->
- Some (make_kn mp' dir l)
- | None -> None
+ Some (mp',resolve) ->
+ solve_delta_kn resolve (make_kn mp' dir l)
+ | None -> kn
let subst_kn sub kn =
- match subst_kn0 sub kn with
- None -> kn
- | Some kn' -> kn'
+ let mp,dir,l = repr_kn kn in
+ match subst_mp0 sub mp with
+ Some (mp',_) ->
+ make_kn mp' dir l
+ | None -> kn
+
+exception No_subst
+
+type sideconstantsubst =
+ | User
+ | Canonical
+
+let subst_ind 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
+ 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 mp,dir,l = repr_con con in
- match subst_mp0 sub mp with
- None -> con
- | Some mp' -> make_con mp' dir l
+ let kn1,kn2 = user_con con,canonical_con con in
+ let mp1,dir,l = repr_kn kn1 in
+ let mp2,_,_ = repr_kn kn2 in
+ try
+ let side,con',resolve =
+ match subst_mp0 sub mp1,subst_mp0 sub mp2 with
+ None,None ->raise No_subst
+ | Some (mp',resolve),None -> User,(make_con_equiv mp' mp2 dir l), resolve
+ | None, Some(mp',resolve)-> Canonical,(make_con_equiv mp1 mp' dir l), resolve
+ | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical,
+ (make_con_equiv mp1' mp2' dir l), resolve2
+ in
+ match constant_of_delta_with_inline resolve con' with
+ None -> begin
+ match side with
+ |User ->
+ let con = constant_of_delta resolve con' in
+ con,Const con
+ |Canonical ->
+ let con = constant_of_delta2 resolve con' in
+ con,Const con
+ end
+ | Some t -> con',t
+ with No_subst -> con , Const con
+
let subst_con0 sub con =
- let mp,dir,l = repr_con con in
- match subst_mp0 sub mp with
- None -> None
- | Some mp' ->
- let con' = make_con mp' dir l in
- Some (Const 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
+ Some (Const con)
+ |Canonical ->
+ let con = constant_of_delta2 resolve con' in
+ Some (Const con)
+ end
+ | t -> t
+ with No_subst -> Some (Const con)
-let rec map_kn f f' c =
+
+let rec map_kn f f' c =
let func = map_kn f f' in
match c with
- | Const kn ->
+ | Const kn ->
(match f' kn with
None -> c
| Some const ->const)
- | Ind (kn,i) ->
+ | Ind (kn,i) ->
(match f kn with
None -> c
| Some kn' ->
Ind (kn',i))
- | Construct ((kn,i),j) ->
+ | Construct ((kn,i),j) ->
(match f kn with
None -> c
| Some kn' ->
Construct ((kn',i),j))
- | Case (ci,p,ct,l) ->
+ | 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 p' = func p in
let ct' = func ct in
let l' = array_smartmap func l in
- if (ci.ci_ind==ci_ind && p'==p
+ if (ci.ci_ind==ci_ind && p'==p
&& l'==l && ct'==ct)then c
- else
+ else
Case ({ci with ci_ind = ci_ind},
- p',ct', l')
- | Cast (ct,k,t) ->
+ p',ct', l')
+ | Cast (ct,k,t) ->
let ct' = func ct in
let t'= func t in
- if (t'==t && ct'==ct) then c
+ if (t'==t && ct'==ct) then c
else Cast (ct', k, t')
- | Prod (na,t,ct) ->
+ | Prod (na,t,ct) ->
let ct' = func ct in
let t'= func t in
- if (t'==t && ct'==ct) then c
+ if (t'==t && ct'==ct) then c
else Prod (na, t', ct')
- | Lambda (na,t,ct) ->
+ | Lambda (na,t,ct) ->
let ct' = func ct in
let t'= func t in
- if (t'==t && ct'==ct) then c
+ if (t'==t && ct'==ct) then c
else Lambda (na, t', ct')
- | LetIn (na,b,t,ct) ->
+ | LetIn (na,b,t,ct) ->
let ct' = func ct in
let t'= func t in
let b'= func b in
- if (t'==t && ct'==ct && b==b') then c
+ if (t'==t && ct'==ct && b==b') then c
else LetIn (na, b', t', ct')
- | App (ct,l) ->
+ | App (ct,l) ->
let ct' = func ct in
let l' = array_smartmap func l in
if (ct'== ct && l'==l) then c
else App (ct',l')
- | Evar (e,l) ->
+ | Evar (e,l) ->
let l' = array_smartmap func l in
if (l'==l) then c
else Evar (e,l')
| Fix (ln,(lna,tl,bl)) ->
let tl' = array_smartmap func tl in
let bl' = array_smartmap func bl in
- if (bl == bl'&& tl == tl') then c
+ if (bl == bl'&& tl == tl') then c
else Fix (ln,(lna,tl',bl'))
| CoFix(ln,(lna,tl,bl)) ->
let tl' = array_smartmap func tl in
let bl' = array_smartmap func bl in
- if (bl == bl'&& tl == tl') then c
+ if (bl == bl'&& tl == tl') then c
else CoFix (ln,(lna,tl',bl'))
| _ -> c
-let subst_mps sub =
- map_kn (subst_kn0 sub) (subst_con0 sub)
+let subst_mps sub =
+ map_kn (subst_mind0 sub) (subst_con0 sub)
+
+
+type 'a lazy_subst =
+ | LSval of 'a
+ | LSlazy of substitution list * 'a
+
+type 'a substituted = 'a lazy_subst ref
+
+let val_substituted val_a =
+ val_ref
+ (val_sum "constr_substituted" 0
+ [|[|val_a|];[|val_list val_subst;val_a|]|])
+let from_val a = ref (LSval a)
+
let rec replace_mp_in_mp mpfrom mpto mp =
match mp with
| _ when mp = mpfrom -> mpto
- | MPdot (mp1,l) ->
+ | MPdot (mp1,l) ->
let mp1' = replace_mp_in_mp mpfrom mpto mp1 in
if mp1==mp1' then mp
else MPdot (mp1',l)
| _ -> mp
-let replace_mp_in_con mpfrom mpto kn =
- let mp,dir,l = kn in
- let mp'' = replace_mp_in_mp mpfrom mpto mp in
- if mp==mp'' then kn
- else (mp'', dir, l)
-
-type 'a lazy_subst =
- | LSval of 'a
- | LSlazy of substitution * 'a
+let rec mp_in_mp mp mp1 =
+ match mp1 with
+ | _ when mp1 = mp -> true
+ | MPdot (mp2,l) -> mp_in_mp mp mp2
+ | _ -> false
-type 'a substituted = 'a lazy_subst ref
-
-let from_val a = ref (LSval a)
-
-let force fsubst r =
- match !r with
- | LSval a -> a
- | LSlazy(s,a) ->
- let a' = fsubst s a in
- r := LSval a';
- a'
-
-
-
-let join (subst1 : substitution) (subst2 : substitution) =
- let apply_subst (sub : substitution) key (mp,_) =
- match subst_mp0 sub mp with
- None -> mp,None
- | Some mp' -> mp',None in
- let subst = Umap.mapi (apply_subst subst2) subst1 in
- (Umap.fold Umap.add subst2 subst)
-
-let subst_key subst1 subst2 =
- let replace_in_key key mp sub=
- let newkey =
- match key with
- | MPI mp1 ->
- begin
- match subst_mp0 subst1 mp1 with
- | None -> None
- | Some mp2 -> Some (MPI mp2)
- end
- | _ -> None
- in
- match newkey with
- | None -> Umap.add key mp sub
- | Some mpi -> Umap.add mpi mp sub
+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
in
- Umap.fold replace_in_key subst2 empty_subst
-
-let update_subst_alias subst1 subst2 =
- let subst_inv key (mp,_) sub =
- let newmp =
- match key with
- | MBI msid -> Some (MPbound msid)
- | MSI msid -> Some (MPself msid)
- | _ -> None
- in
- match newmp with
- | None -> sub
- | Some mpi -> match mp with
- | MPbound mbid -> Umap.add (MBI mbid) (mpi,None) sub
- | MPself msid -> Umap.add (MSI msid) (mpi,None) sub
- | _ -> Umap.add (MPI mp) (mpi,None) sub
- in
- let subst_mbi = Umap.fold subst_inv subst2 empty_subst in
- let alias_subst key (mp,_) sub=
- let newkey =
- match key with
- | MPI mp1 ->
- begin
- match subst_mp0 subst_mbi mp1 with
- | None -> None
- | Some mp2 -> Some (MPI mp2)
- end
- | _ -> None
- in
- match newkey with
- | None -> Umap.add key (mp,None) sub
- | Some mpi -> Umap.add mpi (mp,None) sub
+ Deltamap.fold prefixmp 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
in
- Umap.fold alias_subst subst1 empty_subst
-
-let join_alias (subst1 : substitution) (subst2 : substitution) =
- let apply_subst (sub : substitution) key (mp,_) =
- match subst_mp0 sub mp with
- None -> mp,None
- | Some mp' -> mp',None in
- Umap.mapi (apply_subst subst2) subst1
-
-
-let update_subst subst1 subst2 =
- let subst_inv key (mp,_) l =
- let newmp =
- match key with
- | MBI msid -> MPbound msid
- | MSI msid -> MPself msid
- | MPI mp -> mp
- in
- match mp with
- | MPbound mbid -> ((MBI mbid),newmp)::l
- | MPself msid -> ((MSI msid),newmp)::l
- | _ -> ((MPI mp),newmp)::l
- in
- let subst_mbi = Umap.fold subst_inv subst2 [] in
- let alias_subst key (mp,_) sub=
- let newsetkey =
- match key with
- | MPI mp1 ->
- let compute_set_newkey l (k,mp') =
- let mp_from_key = match k with
- | MBI msid -> MPbound msid
- | MSI msid -> MPself msid
- | MPI mp -> mp
- in
- let new_mp1 = replace_mp_in_mp mp_from_key mp' mp1 in
- if new_mp1 == mp1 then l else (MPI new_mp1)::l
- in
- begin
- match List.fold_left compute_set_newkey [] subst_mbi with
- | [] -> None
- | l -> Some (l)
- end
- | _ -> None
+ Deltamap.fold apply_subst resolver empty_delta_resolver
+
+let subst_mp_delta sub mp key=
+ match subst_mp0 sub mp with
+ None -> empty_delta_resolver,mp
+ | 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
+ in
+ Deltamap.fold apply_subst resolver empty_delta_resolver
+
+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
- match newsetkey with
- | None -> sub
- | Some l ->
- List.fold_left (fun s k -> Umap.add k (mp,None) s)
- sub l
+ Deltamap.fold apply_res resolver1 empty_delta_resolver
+
+let add_delta_resolver resolver1 resolver2 =
+ if resolver1 == resolver2 then
+ resolver2
+ else
+ Deltamap.fold Deltamap.add (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
in
- Umap.fold alias_subst subst1 empty_subst
+ Umap.fold prefixmp subst empty_subst
+let join (subst1 : substitution) (subst2 : substitution) =
+ let apply_subst key (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 =
+ match resolve' with
+ Some res ->
+ add_delta_resolver
+ (subst_dom_codom_delta_resolver subst2 resolve) res
+ | 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 force fsubst r =
+ match !r with
+ | LSval a -> a
+ | LSlazy(s,a) ->
+ let subst = List.fold_left join empty_subst (List.rev s) in
+ let a' = fsubst subst a in
+ r := LSval a';
+ a'
let subst_substituted s r =
match !r with
- | LSval a -> ref (LSlazy(s,a))
+ | LSval a -> ref (LSlazy([s],a))
| LSlazy(s',a) ->
- let s'' = join s' s in
- ref (LSlazy(s'',a))
+ ref (LSlazy(s::s',a))
-let force_constr = force subst_mps
+let force_constr = force subst_mps
type constr_substituted = constr substituted
-let val_cstr_subst =
- val_ref
- (val_sum "constr_substituted" 0
- [|[|val_constr|];[|val_subst;val_constr|]|])
+let val_cstr_subst = val_substituted val_constr
let subst_constr_subst = subst_substituted
@@ -390,12 +657,17 @@ type constant_body = {
const_body_code : to_patch_substituted;
(* const_type_code : Cemitcodes.to_patch; *)
const_constraints : Univ.constraints;
- const_opaque : bool;
+ const_opaque : bool;
const_inline : bool}
let val_cb = val_tuple "constant_body"
- [|val_nctxt;val_opt val_cstr_subst; val_cst_type;no_val;val_cstrs;
- val_bool; val_bool |]
+ [|val_nctxt;
+ val_opt val_cstr_subst;
+ val_cst_type;
+ no_val;
+ val_cstrs;
+ val_bool;
+ val_bool |]
let subst_rel_declaration sub (id,copt,t as x) =
@@ -405,21 +677,21 @@ let subst_rel_declaration sub (id,copt,t as x) =
let subst_rel_context sub = list_smartmap (subst_rel_declaration sub)
-type recarg =
- | Norec
- | Mrec of int
+type recarg =
+ | Norec
+ | Mrec of int
| Imbr of inductive
let val_recarg = val_sum "recarg" 1 (* Norec *)
[|[|val_int|] (* Mrec *);[|val_ind|] (* Imbr *)|]
let subst_recarg sub r = match r with
| Norec | Mrec _ -> r
- | Imbr (kn,i) -> let kn' = subst_kn sub kn in
+ | 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
let val_wfp = val_rec_sum "wf_paths" 0
- (fun val_wfp ->
+ (fun val_wfp ->
[|[|val_int;val_int|]; (* Rtree.Param *)
[|val_recarg;val_array val_wfp|]; (* Rtree.Node *)
[|val_int;val_array val_wfp|] (* Rtree.Rec *)
@@ -454,7 +726,7 @@ type monomorphic_inductive_arity = {
let val_mono_ind_arity =
val_tuple"monomorphic_inductive_arity"[|val_constr;val_sort|]
-type inductive_arity =
+type inductive_arity =
| Monomorphic of monomorphic_inductive_arity
| Polymorphic of polymorphic_arity
let val_ind_arity = val_sum "inductive_arity" 0
@@ -486,6 +758,9 @@ type one_inductive_body = {
(* Number of expected real arguments of the type (no let, no params) *)
mind_nrealargs : int;
+ (* Length of realargs context (with let, no params) *)
+ mind_nrealargs_ctxt : int;
+
(* List of allowed elimination sorts *)
mind_kelim : sorts_family list;
@@ -506,13 +781,13 @@ type one_inductive_body = {
(* number of no constant constructor *)
mind_nb_args : int;
- mind_reloc_tbl : reloc_table;
+ mind_reloc_tbl : reloc_table;
}
let val_one_ind = val_tuple "one_inductive_body"
[|val_id;val_rctxt;val_ind_arity;val_array val_id;val_array val_constr;
- val_int; val_list val_sortfam;val_array val_constr;val_array val_int;
- val_wfp; val_int; val_int; no_val|]
+ val_int;val_int;val_list val_sortfam;val_array val_constr;val_array val_int;
+ val_wfp;val_int;val_int;no_val|]
type mutual_inductive_body = {
@@ -544,12 +819,10 @@ type mutual_inductive_body = {
(* Universes constraints enforced by the inductive declaration *)
mind_constraints : Univ.constraints;
- (* Source of the inductive block when aliased in a module *)
- mind_equiv : kernel_name option
}
let val_ind_pack = val_tuple "mutual_inductive_body"
[|val_array val_one_ind;val_bool;val_bool;val_int;val_nctxt;
- val_int; val_int; val_rctxt;val_cstrs;val_opt val_kn|]
+ val_int; val_int; val_rctxt;val_cstrs|]
let subst_arity sub = function
@@ -565,7 +838,7 @@ let subst_const_body sub cb = {
(*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_inline = cb.const_inline}
let subst_arity sub = function
| Monomorphic s ->
@@ -575,152 +848,158 @@ let subst_arity sub = function
}
| Polymorphic s as x -> x
-let subst_mind_packet sub mbp =
+let subst_mind_packet sub mbp =
{ mind_consnames = mbp.mind_consnames;
mind_consnrealdecls = mbp.mind_consnrealdecls;
mind_typename = mbp.mind_typename;
- mind_nf_lc = array_smartmap (subst_mps sub) mbp.mind_nf_lc;
+ mind_nf_lc = array_smartmap (subst_mps sub) mbp.mind_nf_lc;
mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt;
mind_arity = subst_arity sub mbp.mind_arity;
mind_user_lc = array_smartmap (subst_mps sub) mbp.mind_user_lc;
mind_nrealargs = mbp.mind_nrealargs;
+ mind_nrealargs_ctxt = mbp.mind_nrealargs_ctxt;
mind_kelim = mbp.mind_kelim;
- mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*);
+ mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*);
mind_nb_constant = mbp.mind_nb_constant;
mind_nb_args = mbp.mind_nb_args;
mind_reloc_tbl = mbp.mind_reloc_tbl }
-let subst_mind sub mib =
- { mind_record = mib.mind_record ;
+let subst_mind sub mib =
+ { mind_record = mib.mind_record ;
mind_finite = mib.mind_finite ;
mind_ntypes = mib.mind_ntypes ;
mind_hyps = (assert (mib.mind_hyps=[]); []) ;
mind_nparams = mib.mind_nparams;
mind_nparams_rec = mib.mind_nparams_rec;
- mind_params_ctxt =
+ mind_params_ctxt =
map_rel_context (subst_mps sub) mib.mind_params_ctxt;
mind_packets = array_smartmap (subst_mind_packet sub) mib.mind_packets ;
- mind_constraints = mib.mind_constraints ;
- mind_equiv = Option.map (subst_kn sub) mib.mind_equiv }
+ mind_constraints = mib.mind_constraints }
(* Modules *)
(* Whenever you change these types, please do update the validation
functions below *)
-type structure_field_body =
+type structure_field_body =
| SFBconst of constant_body
| SFBmind of mutual_inductive_body
| SFBmodule of module_body
- | SFBalias of module_path * struct_expr_body option * Univ.constraints option
| SFBmodtype of module_type_body
and structure_body = (label * structure_field_body) list
and struct_expr_body =
| SEBident of module_path
- | SEBfunctor of mod_bound_id * module_type_body * struct_expr_body
- | SEBstruct of mod_self_id * structure_body
- | SEBapply of struct_expr_body * struct_expr_body
- * Univ.constraints
+ | SEBfunctor of mod_bound_id * module_type_body * struct_expr_body
+ | SEBapply of struct_expr_body * struct_expr_body * Univ.constraints
+ | SEBstruct of structure_body
| SEBwith of struct_expr_body * with_declaration_body
and with_declaration_body =
- With_module_body of identifier list * module_path *
- struct_expr_body option * Univ.constraints
+ With_module_body of identifier list * module_path
| With_definition_body of identifier list * constant_body
-
-and module_body =
- { mod_expr : struct_expr_body option;
- mod_type : struct_expr_body option;
+
+and module_body =
+ { mod_mp : module_path;
+ mod_expr : struct_expr_body option;
+ mod_type : struct_expr_body;
+ mod_type_alg : struct_expr_body option;
mod_constraints : Univ.constraints;
- mod_alias : substitution;
+ mod_delta : delta_resolver;
mod_retroknowledge : action list}
-and module_type_body =
- { typ_expr : struct_expr_body;
- typ_strength : module_path option;
- typ_alias : substitution}
+and module_type_body =
+ { typ_mp : module_path;
+ typ_expr : struct_expr_body;
+ typ_expr_alg : struct_expr_body option ;
+ typ_constraints : Univ.constraints;
+ typ_delta :delta_resolver}
(* the validation functions: *)
let rec val_sfb o = val_sum "struct_field_body" 0
[|[|val_cb|]; (* SFBconst *)
[|val_ind_pack|]; (* SFBmind *)
[|val_module|]; (* SFBmodule *)
- [|val_mp;val_opt val_seb;val_opt val_cstrs|]; (* SFBalias *)
[|val_modtype|] (* SFBmodtype *)
|] o
and val_sb o = val_list (val_tuple"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 *)
- [|val_uid;val_sb|]; (* SEBstruct *)
[|val_seb;val_seb;val_cstrs|]; (* SEBapply *)
+ [|val_sb|]; (* SEBstruct *)
[|val_seb;val_with|] (* SEBwith *)
|] o
and val_with o = val_sum "with_declaration_body" 0
- [|[|val_list val_id;val_mp;val_cstrs|];
+ [|[|val_list val_id;val_mp|];
[|val_list val_id;val_cb|]|] o
and val_module o = val_tuple "module_body"
- [|val_opt val_seb;val_opt val_seb;val_cstrs;val_subst;no_val|] o
+ [|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"
- [|val_seb;val_opt val_mp;val_subst|] o
+ [|val_mp;val_seb;val_opt val_seb;val_cstrs;val_res|] o
+
-
let rec subst_with_body sub = function
- | With_module_body(id,mp,typ_opt,cst) ->
- With_module_body(id,subst_mp sub mp,
- Option.smartmap (subst_struct_expr sub) typ_opt,cst)
+ | With_module_body(id,mp) ->
+ With_module_body(id,subst_mp sub mp)
| With_definition_body(id,cb) ->
With_definition_body( id,subst_const_body sub cb)
-and subst_modtype sub mtb =
+and subst_modtype sub mtb=
let typ_expr' = subst_struct_expr sub mtb.typ_expr in
- if typ_expr'==mtb.typ_expr then
- mtb
+ let typ_alg' =
+ Option.smartmap
+ (subst_struct_expr sub) mtb.typ_expr_alg in
+ let mp = subst_mp sub mtb.typ_mp
+ in
+ if typ_expr'==mtb.typ_expr &&
+ typ_alg'==mtb.typ_expr_alg && mp==mtb.typ_mp then
+ mtb
else
- { mtb with
- typ_expr = typ_expr'}
-
+ {mtb with
+ typ_mp = mp;
+ typ_expr = typ_expr';
+ typ_expr_alg = typ_alg'}
+
and subst_structure sub sign =
- let subst_body = function
+ let subst_body = function
SFBconst cb ->
SFBconst (subst_const_body sub cb)
| SFBmind mib ->
SFBmind (subst_mind sub mib)
| SFBmodule mb ->
- SFBmodule (subst_module sub mb)
+ SFBmodule (subst_module sub mb)
| SFBmodtype mtb ->
SFBmodtype (subst_modtype sub mtb)
- | SFBalias (mp,typ_opt ,cst) ->
- SFBalias (subst_mp sub mp,Option.smartmap (subst_struct_expr sub) typ_opt,cst)
in
List.map (fun (l,b) -> (l,subst_body b)) sign
-and subst_module sub mb =
- let mtb' = Option.smartmap (subst_struct_expr sub) mb.mod_type in
- (* This is similar to the previous case. In this case we have
- a module M in a signature that is knows to be equivalent to a module M'
- (because the signature is "K with Module M := M'") and we are substituting
- M' with some M''. *)
- let me' = Option.smartmap (subst_struct_expr sub) mb.mod_expr in
- let mb_alias = join_alias mb.mod_alias sub in
- if mtb'==mb.mod_type && mb.mod_expr == me'
- && mb_alias == mb.mod_alias
- then mb else
- { mod_expr = me';
- mod_type=mtb';
- mod_constraints=mb.mod_constraints;
- mod_alias = mb_alias;
- mod_retroknowledge=mb.mod_retroknowledge}
+and subst_module sub mb =
+ let mtb' = subst_struct_expr sub mb.mod_type in
+ let typ_alg' = Option.smartmap
+ (subst_struct_expr sub ) mb.mod_type_alg in
+ let me' = Option.smartmap
+ (subst_struct_expr sub) mb.mod_expr in
+ let mp = subst_mp sub mb.mod_mp in
+ if mtb'==mb.mod_type && mb.mod_expr == me'
+ && mp == mb.mod_mp
+ then mb else
+ { mb with
+ mod_mp = mp;
+ mod_expr = me';
+ mod_type_alg = typ_alg';
+ mod_type=mtb'}
and subst_struct_expr sub = function
- | SEBident mp -> SEBident (subst_mp sub mp)
- | SEBfunctor (msid, mtb, meb') ->
- SEBfunctor(msid,subst_modtype sub mtb,subst_struct_expr sub meb')
- | SEBstruct (msid,str)->
- SEBstruct(msid, subst_structure sub str)
+ | SEBident mp -> SEBident (subst_mp sub mp)
+ | SEBfunctor (mbid, mtb, meb') ->
+ SEBfunctor(mbid,subst_modtype sub mtb
+ ,subst_struct_expr sub meb')
+ | SEBstruct (str)->
+ SEBstruct( subst_structure sub str)
| SEBapply (meb1,meb2,cst)->
SEBapply(subst_struct_expr sub meb1,
subst_struct_expr sub meb2,
@@ -728,7 +1007,5 @@ and subst_struct_expr sub = function
| SEBwith (meb,wdb)->
SEBwith(subst_struct_expr sub meb,
subst_with_body sub wdb)
-
-let subst_signature_msid msid mp =
- subst_structure (map_msid msid mp)
+
diff --git a/checker/declarations.mli b/checker/declarations.mli
index d71e625f..b39fd6f2 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -25,7 +25,7 @@ type constant_type =
| NonPolymorphicType of constr
| PolymorphicArity of rel_context * polymorphic_arity
-type constr_substituted
+type constr_substituted
val force_constr : constr_substituted -> constr
val from_val : constr -> constr_substituted
@@ -35,14 +35,14 @@ type constant_body = {
const_type : constant_type;
const_body_code : to_patch_substituted;
const_constraints : Univ.constraints;
- const_opaque : bool;
+ const_opaque : bool;
const_inline : bool}
(* Mutual inductives *)
-type recarg =
- | Norec
- | Mrec of int
+type recarg =
+ | Norec
+ | Mrec of int
| Imbr of inductive
type wf_paths = recarg Rtree.t
@@ -56,7 +56,7 @@ type monomorphic_inductive_arity = {
mind_sort : sorts;
}
-type inductive_arity =
+type inductive_arity =
| Monomorphic of monomorphic_inductive_arity
| Polymorphic of polymorphic_arity
@@ -86,6 +86,9 @@ type one_inductive_body = {
(* Number of expected real arguments of the type (no let, no params) *)
mind_nrealargs : int;
+ (* Length of realargs context (with let, no params) *)
+ mind_nrealargs_ctxt : int;
+
(* List of allowed elimination sorts *)
mind_kelim : sorts_family list;
@@ -106,7 +109,7 @@ type one_inductive_body = {
(* number of no constant constructor *)
mind_nb_args : int;
- mind_reloc_tbl : reloc_table;
+ mind_reloc_tbl : reloc_table;
}
type mutual_inductive_body = {
@@ -138,53 +141,52 @@ type mutual_inductive_body = {
(* Universes constraints enforced by the inductive declaration *)
mind_constraints : Univ.constraints;
- (* Source of the inductive block when aliased in a module *)
- mind_equiv : kernel_name option
}
(* Modules *)
type substitution
+type delta_resolver
+val empty_delta_resolver : delta_resolver
-type structure_field_body =
+type structure_field_body =
| SFBconst of constant_body
| SFBmind of mutual_inductive_body
| SFBmodule of module_body
- | SFBalias of module_path * struct_expr_body option
- * Univ.constraints option
| SFBmodtype of module_type_body
and structure_body = (label * structure_field_body) list
and struct_expr_body =
| SEBident of module_path
- | SEBfunctor of mod_bound_id * module_type_body * struct_expr_body
- | SEBstruct of mod_self_id * structure_body
- | SEBapply of struct_expr_body * struct_expr_body
- * Univ.constraints
+ | SEBfunctor of mod_bound_id * module_type_body * struct_expr_body
+ | SEBapply of struct_expr_body * struct_expr_body * Univ.constraints
+ | SEBstruct of structure_body
| SEBwith of struct_expr_body * with_declaration_body
and with_declaration_body =
- With_module_body of identifier list * module_path *
- struct_expr_body option * Univ.constraints
+ With_module_body of identifier list * module_path
| With_definition_body of identifier list * constant_body
-
-and module_body =
- { mod_expr : struct_expr_body option;
- mod_type : struct_expr_body option;
+
+and module_body =
+ { mod_mp : module_path;
+ mod_expr : struct_expr_body option;
+ mod_type : struct_expr_body;
+ mod_type_alg : struct_expr_body option;
mod_constraints : Univ.constraints;
- mod_alias : substitution;
+ mod_delta : delta_resolver;
mod_retroknowledge : action list}
-and module_type_body =
- { typ_expr : struct_expr_body;
- typ_strength : module_path option;
- typ_alias : substitution}
+and module_type_body =
+ { typ_mp : module_path;
+ typ_expr : struct_expr_body;
+ typ_expr_alg : struct_expr_body option ;
+ typ_constraints : Univ.constraints;
+ typ_delta :delta_resolver}
(* Substitutions *)
val fold_subst :
- (mod_self_id -> module_path -> 'a -> 'a) ->
(mod_bound_id -> module_path -> 'a -> 'a) ->
(module_path -> module_path -> 'a -> 'a) ->
substitution -> 'a -> 'a
@@ -192,26 +194,21 @@ val fold_subst :
type 'a subst_fun = substitution -> 'a -> 'a
val empty_subst : substitution
-val add_msid : mod_self_id -> module_path -> substitution -> substitution
val add_mbid : mod_bound_id -> module_path -> substitution -> substitution
val add_mp : module_path -> module_path -> substitution -> substitution
-val map_msid : mod_self_id -> module_path -> substitution
val map_mbid : mod_bound_id -> module_path -> substitution
val map_mp : module_path -> module_path -> substitution
+val mp_in_delta : module_path -> delta_resolver -> bool
+val mind_of_delta : delta_resolver -> mutual_inductive -> mutual_inductive
val subst_const_body : constant_body subst_fun
val subst_mind : mutual_inductive_body subst_fun
val subst_modtype : substitution -> module_type_body -> module_type_body
val subst_struct_expr : substitution -> struct_expr_body -> struct_expr_body
val subst_structure : substitution -> structure_body -> structure_body
-val subst_signature_msid :
- mod_self_id -> module_path -> structure_body -> structure_body
+val subst_module : substitution -> module_body -> module_body
val join : substitution -> substitution -> substitution
-val join_alias : substitution -> substitution -> substitution
-val update_subst_alias : substitution -> substitution -> substitution
-val update_subst : substitution -> substitution -> substitution
-val subst_key : substitution -> substitution -> substitution
(* Validation *)
val val_eng : Obj.t -> unit
diff --git a/checker/environ.ml b/checker/environ.ml
index 4bdbeee6..a72aae91 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -5,11 +5,11 @@ open Term
open Declarations
type globals = {
- env_constants : constant_body Cmap.t;
- env_inductives : mutual_inductive_body KNmap.t;
+ env_constants : constant_body Cmap_env.t;
+ env_inductives : mutual_inductive_body Mindmap_env.t;
+ env_inductives_eq : kernel_name KNmap.t;
env_modules : module_body MPmap.t;
- env_modtypes : module_type_body MPmap.t;
- env_alias : module_path MPmap.t }
+ env_modtypes : module_type_body MPmap.t}
type stratification = {
env_universes : universes;
@@ -25,11 +25,11 @@ type env = {
let empty_env = {
env_globals =
- { env_constants = Cmap.empty;
- env_inductives = KNmap.empty;
+ { env_constants = Cmap_env.empty;
+ env_inductives = Mindmap_env.empty;
+ env_inductives_eq = KNmap.empty;
env_modules = MPmap.empty;
- env_modtypes = MPmap.empty;
- env_alias = MPmap.empty };
+ env_modtypes = MPmap.empty};
env_named_context = [];
env_rel_context = [];
env_stratification =
@@ -71,17 +71,17 @@ let push_rel d env =
env_rel_context = d :: env.env_rel_context }
let push_rel_context ctxt x = fold_rel_context push_rel ctxt ~init:x
-
+
let push_rec_types (lna,typarray,_) env =
let ctxt = array_map2_i (fun i na t -> (na, None, lift i t)) lna typarray in
Array.fold_left (fun e assum -> push_rel assum e) env ctxt
(* Named context *)
-let push_named d env =
+let push_named d env =
(* if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context);
assert (env.env_rel_context = []); *)
- { env with
+ { env with
env_named_context = d :: env.env_named_context }
let lookup_named id env =
@@ -98,30 +98,30 @@ let named_type id env =
(* Universe constraints *)
let add_constraints c env =
- if c == Constraint.empty then
- env
+ if c == Constraint.empty then
+ env
else
let s = env.env_stratification in
- { env with env_stratification =
+ { env with env_stratification =
{ s with env_universes = merge_constraints c s.env_universes } }
(* Global constants *)
let lookup_constant kn env =
- Cmap.find kn env.env_globals.env_constants
+ Cmap_env.find kn env.env_globals.env_constants
let add_constant kn cs env =
- let new_constants =
- Cmap.add kn cs env.env_globals.env_constants in
- let new_globals =
- { env.env_globals with
- env_constants = new_constants } in
+ let new_constants =
+ Cmap_env.add kn cs env.env_globals.env_constants in
+ let new_globals =
+ { env.env_globals with
+ 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
+ cb.const_type
type const_evaluation_result = NoBody | Opaque
@@ -144,60 +144,53 @@ let evaluable_constant cst env =
with Not_found | NotEvaluableConst _ -> false
(* Mutual Inductives *)
-let lookup_mind kn env =
- KNmap.find kn env.env_globals.env_inductives
+let scrape_mind env kn=
+ try
+ KNmap.find kn env.env_globals.env_inductives_eq
+ with
+ Not_found -> kn
+
+let mind_equiv env (kn1,i1) (kn2,i2) =
+ i1 = i2 &&
+ scrape_mind env (user_mind kn1) = scrape_mind env (user_mind kn2)
-let rec scrape_mind env kn =
- match (lookup_mind kn env).mind_equiv with
- | None -> kn
- | Some kn' -> scrape_mind env kn'
+
+let lookup_mind kn env =
+ Mindmap_env.find kn env.env_globals.env_inductives
let add_mind kn mib env =
- let new_inds = KNmap.add kn mib env.env_globals.env_inductives in
- let new_globals =
- { env.env_globals with
- env_inductives = new_inds } in
+ let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in
+ let kn1,kn2 = user_mind kn,canonical_mind kn in
+ let new_inds_eq = if kn1=kn2 then
+ env.env_globals.env_inductives_eq
+ else
+ KNmap.add kn1 kn2 env.env_globals.env_inductives_eq in
+ let new_globals =
+ { env.env_globals with
+ env_inductives = new_inds;
+ env_inductives_eq = new_inds_eq} in
{ env with env_globals = new_globals }
-let rec mind_equiv env (kn1,i1) (kn2,i2) =
- let rec equiv kn1 kn2 =
- kn1 = kn2 ||
- scrape_mind env kn1 = scrape_mind env kn2 in
- i1 = i2 && equiv kn1 kn2
-
(* Modules *)
-let add_modtype ln mtb env =
+let add_modtype ln mtb env =
let new_modtypes = MPmap.add ln mtb env.env_globals.env_modtypes in
- let new_globals =
- { env.env_globals with
+ let new_globals =
+ { env.env_globals with
env_modtypes = new_modtypes } in
{ env with env_globals = new_globals }
-let shallow_add_module mp mb env =
+let shallow_add_module mp mb env =
let new_mods = MPmap.add mp mb env.env_globals.env_modules in
- let new_globals =
- { env.env_globals with
+ let new_globals =
+ { env.env_globals with
env_modules = new_mods } in
{ env with env_globals = new_globals }
-let register_alias mp1 mp2 env =
- let new_alias = MPmap.add mp1 mp2 env.env_globals.env_alias in
- let new_globals =
- { env.env_globals with
- env_alias = new_alias } in
- { env with env_globals = new_globals }
-
-let rec scrape_alias mp env =
- try
- let mp1 = MPmap.find mp env.env_globals.env_alias in
- scrape_alias mp1 env
- with
- Not_found -> mp
-let lookup_module mp env =
+let lookup_module mp env =
MPmap.find mp env.env_globals.env_modules
-let lookup_modtype ln env =
+let lookup_modtype ln env =
MPmap.find ln env.env_globals.env_modtypes
diff --git a/checker/environ.mli b/checker/environ.mli
index 1541bf0d..023acd0b 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -4,12 +4,11 @@ open Term
(* Environments *)
type globals = {
- env_constants : Declarations.constant_body Cmap.t;
- env_inductives : Declarations.mutual_inductive_body KNmap.t;
+ env_constants : Declarations.constant_body Cmap_env.t;
+ env_inductives : Declarations.mutual_inductive_body Mindmap_env.t;
+ env_inductives_eq : kernel_name KNmap.t;
env_modules : Declarations.module_body MPmap.t;
- env_modtypes : Declarations.module_type_body MPmap.t;
- env_alias : module_path MPmap.t;
-}
+ env_modtypes : Declarations.module_type_body MPmap.t}
type stratification = {
env_universes : Univ.universes;
env_engagement : Declarations.engagement option;
@@ -59,19 +58,18 @@ val constant_opt_value : env -> constant -> constr option
val evaluable_constant : constant -> env -> bool
(* Inductives *)
+val mind_equiv : env -> inductive -> inductive -> bool
+
val lookup_mind :
mutual_inductive -> env -> Declarations.mutual_inductive_body
-val scrape_mind : env -> mutual_inductive -> mutual_inductive
+
val add_mind :
mutual_inductive -> Declarations.mutual_inductive_body -> env -> env
-val mind_equiv : env -> inductive -> inductive -> bool
(* Modules *)
val add_modtype :
module_path -> Declarations.module_type_body -> env -> env
val shallow_add_module :
module_path -> Declarations.module_body -> env -> env
-val register_alias : module_path -> module_path -> env -> env
-val scrape_alias : module_path -> env -> module_path
val lookup_module : module_path -> env -> Declarations.module_body
val lookup_modtype : module_path -> env -> Declarations.module_type_body
diff --git a/checker/include b/checker/include
index 331eb45c..b7d46d4b 100644
--- a/checker/include
+++ b/checker/include
@@ -8,20 +8,26 @@
(mainly run_l and norec).
*)
-#cd ".."
+#cd "..";;
#directory "lib";;
#directory "kernel";;
#directory "checker";;
+#directory "+camlp4";;
+#directory "+camlp5";;
#load "unix.cma";;
#load "str.cma";;
#load "gramlib.cma";;
+(*#load "toplevellib.cma";;
+
+#directory "/usr/lib/ocaml/compiler-libs/utils";;
+let _ = Clflags.recursive_types:=true;;
+*)
#load "check.cma";;
open Typeops;;
open Check;;
-
open Pp;;
open Util;;
open Names;;
@@ -70,10 +76,11 @@ let prenv e =
pp pe;;
*)
+(*
let prsub s =
let string_of_mp mp =
let s = string_of_mp mp in
- (match mp with MPself _ -> "#self."|MPbound _ -> "#bound."|_->"")^s in
+ (match mp with MPbound _ -> "#bound."|_->"")^s in
pp (hv 0
(fold_subst
(fun msid mp strm ->
@@ -86,6 +93,7 @@ let prsub s =
str"P " ++ str (string_of_mp mp1) ++ str " |-> " ++
str (string_of_mp mp) ++ fnl() ++ strm) s (mt())))
;;
+*)
#install_printer prid;;
#install_printer prcon;;
@@ -100,10 +108,10 @@ let prsub s =
#install_printer prcstrs;;
(*#install_printer prus;;*)
(*#install_printer prenv;;*)
-(*#install_printer prenvu;;*)
-#install_printer prsub;;
+(*#install_printer prenvu;;
+#install_printer prsub;;*)
-Checker.init();;
+Checker.init_with_argv [|""|];;
Flags.make_silent false;;
Flags.debug := true;;
Sys.catch_break true;;
@@ -114,7 +122,7 @@ let module_of_file f =
;;
let mod_access m fld =
match m.mod_expr with
- Some(SEBstruct(msid,l)) -> List.assoc fld l
+ Some(SEBstruct l) -> List.assoc fld l
| _ -> failwith "bad structure type"
;;
@@ -153,7 +161,7 @@ let read_mod s f =
engagement option);;
let deref_mod md s =
- let (Some (SEBstruct(msid,l))) = md.mod_expr in
+ let (Some (SEBstruct l)) = md.mod_expr in
List.assoc (label_of_id(id_of_string s)) l
;;
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 4c9b3d61..de57c50a 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -22,13 +22,11 @@ open Environ
let rec debug_string_of_mp = function
| MPfile sl -> string_of_dirpath sl
| MPbound uid -> "bound("^string_of_mbid uid^")"
- | MPself uid -> "self("^string_of_msid uid^")"
- | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l
+ | MPdot (mp,l) -> debug_string_of_mp mp ^ "." ^ string_of_label l
let rec string_of_mp = function
| MPfile sl -> string_of_dirpath sl
| MPbound uid -> string_of_mbid uid
- | MPself uid -> string_of_msid uid
| MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l
let string_of_mp mp =
@@ -38,8 +36,9 @@ let prkn kn =
let (mp,_,l) = repr_kn kn in
str(string_of_mp mp ^ "." ^ string_of_label l)
let prcon c =
- let (mp,_,l) = repr_con c in
- str(string_of_mp mp ^ "." ^ string_of_label l)
+ let ck = canonical_con c in
+ let uk = user_con c in
+ if ck=uk then prkn uk else (prkn uk ++str"(="++prkn ck++str")")
(* Same as noccur_between but may perform reductions.
Could be refined more... *)
@@ -119,23 +118,24 @@ let is_small_constr infos = List.for_all (fun s -> is_small_sort s) infos
let is_logic_constr infos = List.for_all (fun s -> is_logic_sort s) infos
(* An inductive definition is a "unit" if it has only one constructor
- and that all arguments expected by this constructor are
- logical, this is the case for equality, conjunction of logical properties
+ and that all arguments expected by this constructor are
+ logical, this is the case for equality, conjunction of logical properties
*)
let is_unit constrsinfos =
match constrsinfos with (* One info = One constructor *)
- | [|constrinfos|] -> is_logic_constr constrinfos
+ | [|constrinfos|] -> is_logic_constr constrinfos
| [||] -> (* type without constructors *) true
| _ -> false
let small_unit constrsinfos =
- let issmall = array_for_all is_small_constr constrsinfos
+ let issmall = array_for_all is_small_constr constrsinfos
and isunit = is_unit constrsinfos in
issmall, isunit
(* check information related to inductive arity *)
let typecheck_arity env params inds =
let nparamargs = rel_context_nhyps params in
+ let nparamdecls = rel_context_length params in
let check_arity arctxt = function
Monomorphic mar ->
let ar = mar.mind_user_arity in
@@ -154,8 +154,12 @@ let typecheck_arity env params inds =
(* Arities (with params) are typed-checked here *)
let arity = check_arity ar_ctxt ind.mind_arity in
(* mind_nrealargs *)
- if ind.mind_nrealargs <> rel_context_nhyps ar_ctxt - nparamargs then
+ let nrealargs = rel_context_nhyps ar_ctxt - nparamargs in
+ if ind.mind_nrealargs <> nrealargs then
failwith "bad number of real inductive arguments";
+ let nrealargs_ctxt = rel_context_length ar_ctxt - nparamdecls in
+ if ind.mind_nrealargs_ctxt <> nrealargs_ctxt then
+ failwith "bad length of real inductive arguments signature";
(* We do not need to generate the universe of full_arity; if
later, after the validation of the inductive definition,
full_arity is used as argument or subject to cast, an
@@ -273,20 +277,20 @@ exception IllFormedInd of ill_formed_ind
let mind_extract_params = decompose_prod_n_assum
-let explain_ind_err ntyp env0 nbpar c err =
+let explain_ind_err ntyp env0 nbpar c err =
let (lpar,c') = mind_extract_params nbpar c in
let env = push_rel_context lpar env0 in
match err with
- | LocalNonPos kt ->
+ | LocalNonPos kt ->
raise (InductiveError (NonPos (env,c',Rel (kt+nbpar))))
- | LocalNotEnoughArgs kt ->
- raise (InductiveError
+ | LocalNotEnoughArgs kt ->
+ raise (InductiveError
(NotEnoughArgs (env,c',Rel (kt+nbpar))))
| LocalNotConstructor ->
- raise (InductiveError
+ raise (InductiveError
(NotConstructor (env,c',Rel (ntyp+nbpar))))
| LocalNonPar (n,l) ->
- raise (InductiveError
+ raise (InductiveError
(NonPar (env,c',n,Rel (nbpar-n+1), Rel (l+nbpar))))
let failwith_non_pos n ntypes c =
@@ -307,7 +311,7 @@ let failwith_non_pos_list n ntypes l =
let check_correct_par (env,n,ntypes,_) hyps l largs =
let nparams = rel_context_nhyps hyps in
let largs = Array.of_list largs in
- if Array.length largs < nparams then
+ if Array.length largs < nparams then
raise (IllFormedInd (LocalNotEnoughArgs l));
let (lpar,largs') = array_chop nparams largs in
let nhyps = List.length hyps in
@@ -319,18 +323,18 @@ let check_correct_par (env,n,ntypes,_) hyps l largs =
| Rel w when w = index -> check (k-1) (index+1) hyps
| _ -> raise (IllFormedInd (LocalNonPar (k+1,l)))
in check (nparams-1) (n-nhyps) hyps;
- if not (array_for_all (noccur_between n ntypes) largs') then
+ if not (array_for_all (noccur_between n ntypes) largs') then
failwith_non_pos_vect n ntypes largs'
(* Arguments of constructor: check the number of recursive parameters nrecp.
- the first parameters which are constant in recursive arguments
- n is the current depth, nmr is the maximum number of possible
+ the first parameters which are constant in recursive arguments
+ n is the current depth, nmr is the maximum number of possible
recursive parameters *)
-let check_rec_par (env,n,_,_) hyps nrecp largs =
+let check_rec_par (env,n,_,_) hyps nrecp largs =
let (lpar,_) = list_chop nrecp largs in
- let rec find index =
- function
+ let rec find index =
+ function
| ([],_) -> ()
| (_,[]) ->
failwith "number of recursive parameters cannot be greater than the number of parameters."
@@ -347,14 +351,14 @@ let lambda_implicit_lift n a =
(* This removes global parameters of the inductive types in lc (for
nested inductive types only ) *)
-let abstract_mind_lc env ntyps npars lc =
- if npars = 0 then
+let abstract_mind_lc env ntyps npars lc =
+ if npars = 0 then
lc
- else
- let make_abs =
+ else
+ let make_abs =
list_tabulate
- (function i -> lambda_implicit_lift npars (Rel (i+1))) ntyps
- in
+ (function i -> lambda_implicit_lift npars (Rel (i+1))) ntyps
+ in
Array.map (substl make_abs) lc
(* [env] is the typing environment
@@ -362,7 +366,7 @@ let abstract_mind_lc env ntyps npars lc =
[ntypes] is the number of inductive types in the definition
(i.e. range of inductives is [n; n+ntypes-1])
[lra] is the list of recursive tree of each variable
- *)
+ *)
let ienv_push_var (env, n, ntypes, lra) (x,a,ra) =
(push_rel (x,None,a) env, n+1, ntypes, (Norec,ra)::lra)
@@ -372,7 +376,7 @@ let ienv_push_inductive (env, n, ntypes, ra_env) (mi,lpar) =
let env' =
push_rel (Anonymous,None,
hnf_prod_applist env (type_of_inductive env specif) lpar) env in
- let ra_env' =
+ let ra_env' =
(Imbr mi,(Rtree.mk_rec_calls 1).(0)) ::
List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in
(* New index of the inductive types *)
@@ -384,7 +388,7 @@ let ienv_push_inductive (env, n, ntypes, ra_env) (mi,lpar) =
let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp i 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 =
+ let rec check_pos (env, n, ntypes, ra_env as ienv) c =
let x,largs = decompose_app (whd_betadeltaiota env c) in
match x with
| Prod (na,b,d) ->
@@ -395,7 +399,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp i indlc =
check_pos (ienv_push_var ienv (na, b, mk_norec)) d)
| Rel k ->
(try
- let (ra,rarg) = List.nth ra_env (k-1) in
+ let (ra,rarg) = List.nth ra_env (k-1) in
(match ra with
Mrec _ -> check_rec_par ienv hyps nrecp largs
| _ -> ());
@@ -408,9 +412,9 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp i indlc =
parameter, then we have an imbricated type *)
if List.for_all (noccur_between n ntypes) largs then mk_norec
else check_positive_imbr ienv (ind_kn, largs)
- | err ->
+ | err ->
if noccur_between n ntypes x &&
- List.for_all (noccur_between n ntypes) largs
+ List.for_all (noccur_between n ntypes) largs
then mk_norec
else failwith_non_pos_list n ntypes (x::largs)
@@ -419,14 +423,14 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp i indlc =
let (mib,mip) = lookup_mind_specif env mi in
let auxnpar = mib.mind_nparams_rec in
let (lpar,auxlargs) =
- try list_chop auxnpar largs
- with Failure _ -> raise (IllFormedInd (LocalNonPos n)) in
+ try list_chop auxnpar largs
+ with Failure _ -> raise (IllFormedInd (LocalNonPos n)) in
(* If the inductive appears in the args (non params) then the
definition is not positive. *)
if not (List.for_all (noccur_between n ntypes) auxlargs) then
raise (IllFormedInd (LocalNonPos n));
(* We do not deal with imbricated mutual inductive types *)
- let auxntyp = mib.mind_ntypes in
+ let auxntyp = mib.mind_ntypes in
if auxntyp <> 1 then raise (IllFormedInd (LocalNonPos n));
(* The nested inductive type with parameters removed *)
let auxlcvect = abstract_mind_lc env auxntyp auxnpar mip.mind_nf_lc in
@@ -435,30 +439,30 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp i indlc =
let (env',_,_,_ as ienv') = ienv_push_inductive ienv (mi,lpar) in
(* Parameters expressed in env' *)
let lpar' = List.map (lift auxntyp) lpar in
- let irecargs =
+ let irecargs =
(* fails if the inductive type occurs non positively *)
- (* when substituted *)
- Array.map
- (function c ->
- let c' = hnf_prod_applist env' c lpar' in
- check_constructors ienv' false c')
- auxlcvect in
+ (* when substituted *)
+ Array.map
+ (function c ->
+ let c' = hnf_prod_applist env' c lpar' in
+ check_constructors ienv' false c')
+ auxlcvect in
(Rtree.mk_rec [|mk_paths (Imbr mi) irecargs|]).(0)
-
+
(* check the inductive types occur positively in the products of C, if
check_head=true, also check the head corresponds to a constructor of
- the ith type *)
-
- and check_constructors ienv check_head c =
- let rec check_constr_rec (env,n,ntypes,ra_env as ienv) lrec c =
+ the ith type *)
+
+ and check_constructors ienv check_head c =
+ let rec check_constr_rec (env,n,ntypes,ra_env as ienv) lrec c =
let x,largs = decompose_app (whd_betadeltaiota env c) in
match x with
- | Prod (na,b,d) ->
+ | Prod (na,b,d) ->
assert (largs = []);
- let recarg = check_pos ienv b in
+ let recarg = check_pos ienv b in
let ienv' = ienv_push_var ienv (na,b,mk_norec) in
check_constr_rec ienv' (recarg::lrec) d
-
+
| hd ->
if check_head then
if hd = Rel (n+ntypes-i-1) then
@@ -477,7 +481,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp i indlc =
let _,rawc = mind_extract_params lparams c in
try
check_constructors ienv true rawc
- with IllFormedInd err ->
+ with IllFormedInd err ->
explain_ind_err (ntypes-i) env lparams c err)
indlc
in mk_paths (Mrec i) irecargs
@@ -500,9 +504,9 @@ let check_positivity env_ar params nrecp inds =
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 i mip.mind_nf_lc
in
- let irecargs = Array.mapi check_one inds in
+ let irecargs = Array.mapi check_one inds in
let wfp = Rtree.mk_rec irecargs in
array_iter2 (fun ind wfpi -> check_subtree ind.mind_recargs wfpi) inds wfp
@@ -510,7 +514,7 @@ let check_positivity env_ar params nrecp inds =
(************************************************************************)
let check_inductive env kn mib =
- Flags.if_verbose msgnl (str " checking ind: " ++ prkn kn);
+ Flags.if_verbose msgnl (str " checking ind: " ++ pr_mind kn);
(* check mind_constraints: should be consistent with env *)
let env = add_constraints mib.mind_constraints env in
(* check mind_record : TODO ? check #constructor = 1 ? *)
@@ -535,8 +539,6 @@ let check_inductive env kn mib =
(* check mind_nparams_rec: positivity condition *)
check_positivity env_ar params mib.mind_nparams_rec mib.mind_packets;
(* check mind_equiv... *)
- if mib.mind_equiv <> None then
- msg_warning (str"TODO: mind_equiv not checked");
(* Now we can add the inductive *)
add_mind kn mib env
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 05ab5a84..19c7a6cf 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -58,7 +58,7 @@ let inductive_params (mib,_) = mib.mind_nparams
(* inductives *)
let ind_subst mind mib =
let ntypes = mib.mind_ntypes in
- let make_Ik k = Ind (mind,ntypes-k-1) in
+ let make_Ik k = Ind (mind,ntypes-k-1) in
list_tabulate make_Ik ntypes
(* Instantiate inductives in constructor type *)
@@ -67,7 +67,7 @@ let constructor_instantiate mind mib c =
substl s c
let instantiate_params full t args sign =
- let fail () =
+ let fail () =
anomaly "instantiate_params: type, ctxt and args mismatch" in
let (rem_args, subs, ty) =
fold_rel_context
@@ -78,7 +78,7 @@ let instantiate_params full t args sign =
| (_,[],_) -> if full then fail() else ([], subs, ty)
| _ -> fail ())
sign
- ~init:(args,[],t)
+ ~init:(args,[],t)
in
if rem_args <> [] then fail();
substl subs ty
@@ -104,11 +104,11 @@ let full_constructor_instantiate ((mind,_),(mib,_),params) =
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:
I_i: forall uniformparams:utyps, forall otherparams:otyps, Type(a)
-uniformargs : utyps
+uniformargs : utyps
otherargs : otyps
I_1:forall ...,s_1;...I_n:forall ...,s_n |- sort(C_kj(uniformargs)) = s_kj
s'_k = max(..s_kj..)
@@ -221,7 +221,7 @@ let type_of_constructor cstr (mib,mip) =
if i > nconstr then error "Not enough constructors in the type";
constructor_instantiate (fst ind) mib specif.(i-1)
-let arities_of_specif kn (mib,mip) =
+let arities_of_specif kn (mib,mip) =
let specif = mip.mind_nf_lc in
Array.map (constructor_instantiate kn mib) specif
@@ -241,7 +241,7 @@ let error_elim_expln kp ki =
let inductive_sort_family mip =
match mip.mind_arity with
- | Monomorphic s -> family_of_sort s.mind_sort
+ | Monomorphic s -> family_of_sort s.mind_sort
| Polymorphic _ -> InType
let mind_arity mip =
@@ -253,26 +253,30 @@ let get_instantiated_arity (mib,mip) params =
let elim_sorts (_,mip) = mip.mind_kelim
-let rel_list n m =
- let rec reln l p =
- if p>m then l else reln (Rel(n+p)::l) (p+1)
- in
- reln [] 1
+let extended_rel_list n hyps =
+ let rec reln l p = function
+ | (_,None,_) :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps
+ | (_,Some _,_) :: hyps -> reln l (p+1) hyps
+ | [] -> l
+ in
+ reln [] 1 hyps
let build_dependent_inductive ind (_,mip) params =
- let nrealargs = mip.mind_nrealargs in
- applist
- (Ind ind, (List.map (lift nrealargs) params)@(rel_list 0 nrealargs))
+ let realargs,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
+ applist
+ (Ind ind,
+ List.map (lift mip.mind_nrealargs_ctxt) params
+ @ extended_rel_list 0 realargs)
(* This exception is local *)
exception LocalArity of (sorts_family * sorts_family * arity_error) option
let check_allowed_sort ksort specif =
- if not (List.exists ((=) ksort) (elim_sorts specif)) then
+ if not (List.exists ((=) ksort) (elim_sorts specif)) then
let s = inductive_sort_family (snd specif) in
raise (LocalArity (Some(ksort,s,error_elim_expln ksort s)))
-let is_correct_arity env c (p,pj) ind specif params =
+let is_correct_arity env c (p,pj) ind specif params =
let arsign,_ = get_instantiated_arity specif params in
let rec srec env pt ar =
let pt' = whd_betadeltaiota env pt in
@@ -283,9 +287,9 @@ let is_correct_arity env c (p,pj) ind specif params =
srec (push_rel (na1,None,a1) env) t ar'
| Prod (_,a1,a2), [] -> (* whnf of t was not needed here! *)
let ksort = match (whd_betadeltaiota env a2) with
- | Sort s -> family_of_sort s
+ | Sort s -> family_of_sort s
| _ -> raise (LocalArity None) in
- let dep_ind = build_dependent_inductive ind specif params in
+ let dep_ind = build_dependent_inductive ind specif params in
(try conv env a1 dep_ind
with NotConvertible -> raise (LocalArity None));
check_allowed_sort ksort specif;
@@ -295,7 +299,7 @@ let is_correct_arity env c (p,pj) ind specif params =
false
| _ ->
raise (LocalArity None)
- in
+ in
try srec env pj (List.rev arsign)
with LocalArity kinds ->
error_elim_arity env ind (elim_sorts specif) c (p,pj) kinds
@@ -332,7 +336,7 @@ let build_case_type dep p c realargs =
beta_appvect p (Array.of_list args)
let type_case_branches env (ind,largs) (p,pj) c =
- let specif = lookup_mind_specif env ind in
+ let specif = lookup_mind_specif env ind in
let nparams = inductive_params specif in
let (params,realargs) = list_chop nparams largs in
let dep = is_correct_arity env c (p,pj) ind specif params in
@@ -347,7 +351,7 @@ let type_case_branches env (ind,largs) (p,pj) c =
let check_case_info env indsp ci =
let (mib,mip) = lookup_mind_specif env indsp in
if
- not (mind_equiv env indsp ci.ci_ind) or
+ not (eq_ind indsp ci.ci_ind) or
(mib.mind_nparams <> ci.ci_npar) or
(mip.mind_consnrealdecls <> ci.ci_cstr_nargs)
then raise (TypeError(env,WrongCaseInfo(indsp,ci)))
@@ -357,7 +361,7 @@ let check_case_info env indsp ci =
(* Guard conditions for fix and cofix-points *)
-(* Check if t is a subterm of Rel n, and gives its specification,
+(* Check if t is a subterm of Rel n, and gives its specification,
assuming lst already gives index of
subterms with corresponding specifications of recursive arguments *)
@@ -415,7 +419,7 @@ let subterm_spec_glb =
(* branches do not return objects with same spec *)
else Not_subterm in
Array.fold_left glb2 Dead_code
-
+
type guard_env =
{ env : env;
(* dB of last fixpoint *)
@@ -439,7 +443,7 @@ let make_renv env minds recarg (kn,tyi) =
genv = [Subterm(Large,mind_recvec.(tyi))] }
let push_var renv (x,ty,spec) =
- { renv with
+ { renv with
env = push_rel (x,None,ty) renv.env;
rel_min = renv.rel_min+1;
genv = spec:: renv.genv }
@@ -451,7 +455,7 @@ let push_var_renv renv (x,ty) =
push_var renv (x,ty,Not_subterm)
(* Fetch recursive information about a variable p *)
-let subterm_var p renv =
+let subterm_var p renv =
try List.nth renv.genv (p-1)
with Failure _ | Invalid_argument _ -> Not_subterm
@@ -461,7 +465,7 @@ let add_subterm renv (x,a,spec) =
let push_ctxt_renv renv ctxt =
let n = rel_context_length ctxt in
- { renv with
+ { renv with
env = push_rel_context ctxt renv.env;
rel_min = renv.rel_min+n;
genv = iterate (fun ge -> Not_subterm::ge) n renv.genv }
@@ -500,8 +504,8 @@ let lookup_subterms env ind =
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 rec push_branch_args renv lrec c =
+let case_branches_specif renv c_spec ind lbr =
+ let rec push_branch_args renv lrec c =
match lrec with
ra::lr ->
let c' = whd_betadeltaiota renv.env c in
@@ -517,7 +521,7 @@ let case_branches_specif renv c_spec ind lbr =
let sub_spec = Array.map (List.map spec_of_tree) (dest_subterms t) in
assert (Array.length sub_spec = Array.length lbr);
array_map2 (push_branch_args renv) sub_spec lbr
- | Dead_code ->
+ | Dead_code ->
let t = dest_subterms (lookup_subterms renv.env ind) in
let sub_spec = Array.map (List.map (fun _ -> Dead_code)) t in
assert (Array.length sub_spec = Array.length lbr);
@@ -530,10 +534,10 @@ let case_branches_specif renv c_spec ind lbr =
about variables.
*)
-let rec subterm_specif renv t =
+let rec subterm_specif renv t =
(* maybe reduction is not always necessary! *)
let f,l = decompose_app (whd_betadeltaiota renv.env t) in
- match f with
+ match f with
| Rel k -> subterm_var k renv
| Case (ci,_,c,lbr) ->
@@ -545,7 +549,7 @@ let rec subterm_specif renv t =
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
@@ -568,7 +572,7 @@ let rec subterm_specif renv t =
(* Why Strict here ? To be general, it could also be
Large... *)
assign_var_spec renv' (nbfix-i, Subterm(Strict,recargs)) in
- let decrArg = recindxs.(i) 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
@@ -582,7 +586,7 @@ let rec subterm_specif renv t =
assign_var_spec renv'' (1, arg_spec) in
subterm_specif renv'' strippedBody)
- | Lambda (x,a,b) ->
+ | Lambda (x,a,b) ->
assert (l=[]);
subterm_specif (push_var_renv renv (x,a)) b
@@ -594,7 +598,7 @@ let rec subterm_specif renv t =
(* Check term c can be applied to one of the mutual fixpoints. *)
-let check_is_subterm renv c =
+let check_is_subterm renv c =
match subterm_specif renv c with
Subterm (Strict,_) | Dead_code -> true
| _ -> false
@@ -622,21 +626,21 @@ let error_partial_apply renv fx =
given [recpos], the decreasing arguments of each mutually defined
fixpoint. *)
let check_one_fix renv recpos def =
- let nfi = Array.length recpos in
+ 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 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
match f with
- | Rel p ->
- (* Test if [p] is a fixpoint (recursive call) *)
+ | 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;
- (* the position of the invoked fixpoint: *)
+ (* 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
@@ -668,9 +672,9 @@ let check_one_fix renv recpos def =
(* Enables to traverse Fixpoint definitions in a more intelligent
way, ie, the rule :
if - g = Fix g/p := [y1:T1]...[yp:Tp]e &
- - f is guarded with respect to the set of pattern variables S
+ - 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
+ - f is guarded with respect to the set of pattern variables S
in T1 ... Tp &
- ap is a sub-term of the formal argument of f &
- f is guarded with respect to the set of pattern variables
@@ -682,10 +686,10 @@ let check_one_fix renv recpos def =
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
+ let renv' = push_fix_renv renv recdef in
if (List.length l < (decrArg+1)) then
Array.iter (check_rec_call renv') bodies
- else
+ else
Array.iteri
(fun j body ->
if i=j then
@@ -695,8 +699,8 @@ let check_one_fix renv recpos def =
else check_rec_call renv' body)
bodies
- | Const kn ->
- if evaluable_constant kn renv.env then
+ | Const kn ->
+ if evaluable_constant kn renv.env then
try List.iter (check_rec_call renv) l
with (FixGuardError _ ) ->
check_rec_call renv(applist(constant_value renv.env kn, l))
@@ -704,14 +708,14 @@ let check_one_fix renv recpos def =
(* The cases below simply check recursively the condition on the
subterms *)
- | Cast (a,_, b) ->
+ | Cast (a,_, b) ->
List.iter (check_rec_call renv) (a::b::l)
| Lambda (x,a,b) ->
List.iter (check_rec_call renv) (a::l);
check_rec_call (push_var_renv renv (x,a)) b
- | Prod (x,a,b) ->
+ | Prod (x,a,b) ->
List.iter (check_rec_call renv) (a::l);
check_rec_call (push_var_renv renv (x,a)) b
@@ -755,9 +759,9 @@ let check_one_fix renv recpos def =
let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
- let nbfix = Array.length bodies in
+ let nbfix = Array.length bodies in
if nbfix = 0
- or Array.length nvect <> nbfix
+ or Array.length nvect <> nbfix
or Array.length types <> nbfix
or Array.length names <> nbfix
or bodynum < 0
@@ -767,18 +771,18 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
let raise_err env i err =
error_ill_formed_rec_body env err names i in
(* Check the i-th definition with recarg k *)
- let find_ind i k def =
- (* check fi does not appear in the k+1 first abstractions,
+ let find_ind i k def =
+ (* check fi does not appear in the k+1 first abstractions,
gives the type of the k+1-eme abstraction (must be an inductive) *)
- let rec check_occur env n def =
+ let rec check_occur env n def =
match (whd_betadeltaiota env def) with
- | Lambda (x,a,b) ->
+ | Lambda (x,a,b) ->
if noccur_with_meta n nbfix a then
let env' = push_rel (x, None, a) env in
if n = k+1 then
(* get the inductive type of the fixpoint *)
- let (mind, _) =
- try find_inductive env a
+ let (mind, _) =
+ try find_inductive env a
with Not_found ->
raise_err env i (RecursionNotOnInductiveType a) in
(mind, (env', b))
@@ -818,17 +822,17 @@ let rec codomain_is_coind env c =
let b = whd_betadeltaiota env c in
match b with
| Prod (x,a,b) ->
- codomain_is_coind (push_rel (x, None, a) env) b
- | _ ->
+ codomain_is_coind (push_rel (x, None, a) env) b
+ | _ ->
(try find_coinductive env b
with Not_found ->
raise (CoFixGuardError (env, CodomainNotInductiveType b)))
-let check_one_cofix env nbfix def deftype =
+let check_one_cofix env nbfix def deftype =
let rec check_rec_call env alreadygrd n vlra t =
if not (noccur_with_meta n nbfix t) then
let c,args = decompose_app (whd_betadeltaiota env t) in
- match c with
+ match c with
| Rel p when n <= p && p < n+nbfix ->
(* recursive call: must be guarded and no nested recursive
call allowed *)
@@ -836,14 +840,14 @@ let check_one_cofix env nbfix def deftype =
raise (CoFixGuardError (env,UnguardedRecursiveCall t))
else if not(List.for_all (noccur_with_meta n nbfix) args) then
raise (CoFixGuardError (env,NestedRecursiveOccurrences))
-
+
| Construct (_,i as cstr_kn) ->
- let lra = vlra.(i-1) in
+ let lra = vlra.(i-1) in
let mI = inductive_of_constructor cstr_kn in
let (mib,mip) = lookup_mind_specif env mI in
let realargs = list_skipn mib.mind_nparams args in
let rec process_args_of_constr = function
- | (t::lr), (rar::lrar) ->
+ | (t::lr), (rar::lrar) ->
if rar = mk_norec then
if noccur_with_meta n nbfix t
then process_args_of_constr (lr, lrar)
@@ -854,26 +858,26 @@ let check_one_cofix env nbfix def deftype =
check_rec_call env true n spec t;
process_args_of_constr (lr, lrar)
| [],_ -> ()
- | _ -> anomaly_ill_typed ()
+ | _ -> anomaly_ill_typed ()
in process_args_of_constr (realargs, lra)
-
+
| Lambda (x,a,b) ->
assert (args = []);
if noccur_with_meta n nbfix a then
let env' = push_rel (x, None, a) env in
check_rec_call env' alreadygrd (n+1) vlra b
- else
+ else
raise (CoFixGuardError (env,RecCallInTypeOfAbstraction a))
-
+
| CoFix (j,(_,varit,vdefs as recdef)) ->
if (List.for_all (noccur_with_meta n nbfix) args)
- then
+ then
let nbfix = Array.length vdefs in
if (array_for_all (noccur_with_meta n nbfix) varit) then
let env' = push_rec_types recdef env in
(Array.iter (check_rec_call env' alreadygrd (n+1) vlra) vdefs;
List.iter (check_rec_call env alreadygrd n vlra) args)
- else
+ else
raise (CoFixGuardError (env,RecCallInTypeOfDef c))
else
raise (CoFixGuardError (env,UnguardedRecursiveCall c))
@@ -883,31 +887,31 @@ let check_one_cofix env nbfix def deftype =
if (noccur_with_meta n nbfix tm) then
if (List.for_all (noccur_with_meta n nbfix) args) then
Array.iter (check_rec_call env alreadygrd n vlra) vrest
- else
+ else
raise (CoFixGuardError (env,RecCallInCaseFun c))
- else
+ else
raise (CoFixGuardError (env,RecCallInCaseArg c))
- else
+ else
raise (CoFixGuardError (env,RecCallInCasePred c))
-
+
| Meta _ -> ()
| Evar _ ->
List.iter (check_rec_call env alreadygrd n vlra) args
-
- | _ -> raise (CoFixGuardError (env,NotGuardedForm t)) in
+
+ | _ -> raise (CoFixGuardError (env,NotGuardedForm t)) in
let (mind, _) = codomain_is_coind env deftype in
let vlra = lookup_subterms env mind in
check_rec_call env false 1 (dest_subterms vlra) def
-(* The function which checks that the whole block of definitions
+(* The function which checks that the whole block of definitions
satisfies the guarded condition *)
-let check_cofix env (bodynum,(names,types,bodies as recdef)) =
- let nbfix = Array.length bodies in
+let check_cofix env (bodynum,(names,types,bodies as recdef)) =
+ let nbfix = Array.length bodies in
for i = 0 to nbfix-1 do
let fixenv = push_rec_types recdef env in
try check_one_cofix fixenv nbfix bodies.(i) types.(i)
- with CoFixGuardError (errenv,err) ->
+ with CoFixGuardError (errenv,err) ->
error_ill_formed_rec_body errenv err names i
done
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 24000591..23ba4893 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -31,7 +31,7 @@ let check_constant_declaration env kn cb =
(match cb.const_type with
NonPolymorphicType ty ->
let ty, cu = refresh_arity ty in
- let envty = add_constraints cu env' in
+ let envty = add_constraints cu env' in
let _ = infer_type envty ty in
(match cb.const_body with
| Some bd ->
@@ -58,19 +58,15 @@ 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
+let rec list_fold_map2 f e = function
| [] -> (e,[],[])
- | h::t ->
+ | 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_alias (s1:substitution) s2 =
- if s1 <> s2 then failwith "Incorrect alias"
-
let check_definition_sub env cb1 cb2 =
- let check_type env t1 t2 =
+ let check_type env t1 t2 =
(* If the type of a constant is generated, it may mention
non-variable algebraic universes that the general conversion
@@ -81,7 +77,7 @@ let check_definition_sub env cb1 cb2 =
Gamma |- A |> T, Gamma |- A' |> T' and Gamma |- A=A' then T <= T').
Hence they don't have to be checked again *)
- let t1,t2 =
+ let t1,t2 =
if isArity t2 then
let (ctx2,s2) = destArity t2 in
match s2 with
@@ -135,38 +131,38 @@ let lookup_modtype mp env =
with Not_found ->
failwith ("Unknown module type: "^string_of_mp mp)
-
-let rec check_with env mtb with_decl =
+let rec check_with env mtb with_decl mp=
match with_decl with
- | With_definition_body _ ->
- check_with_aux_def env mtb with_decl;
- empty_subst
- | With_module_body _ ->
- check_with_aux_mod env mtb with_decl
+ | With_definition_body _ ->
+ check_with_aux_def env mtb with_decl mp;
+ mtb
+ | With_module_body _ ->
+ check_with_aux_mod env mtb with_decl mp;
+ mtb
-and check_with_aux_def env mtb with_decl =
- let msid,sig_b = match (eval_struct env mtb) with
- | SEBstruct(msid,sig_b) ->
- msid,sig_b
+and check_with_aux_def env mtb with_decl mp =
+ let sig_b = match mtb with
+ | SEBstruct(sig_b) ->
+ sig_b
| _ -> error_signature_expected mtb
in
- let id,idl = match with_decl with
- | With_definition_body (id::idl,_) | With_module_body (id::idl,_,_,_) ->
+ let id,idl = match with_decl with
+ | With_definition_body (id::idl,_) | With_module_body (id::idl,_) ->
id,idl
- | With_definition_body ([],_) | With_module_body ([],_,_,_) -> assert false
+ | With_definition_body ([],_) | With_module_body ([],_) -> assert false
in
let l = label_of_id id in
try
let rev_before,spec,after = list_split_assoc l [] sig_b in
let before = List.rev rev_before in
- let env' = Modops.add_signature (MPself msid) before env in
+ let env' = Modops.add_signature mp before empty_delta_resolver env in
match with_decl with
| With_definition_body ([],_) -> assert false
- | With_definition_body ([id],c) ->
+ | With_definition_body ([id],c) ->
let cb = match spec with
SFBconst cb -> cb
| _ -> error_not_a_constant l
- in
+ in
check_definition_sub env' c cb
| With_definition_body (_::_,_) ->
let old = match spec with
@@ -179,9 +175,9 @@ and check_with_aux_def env mtb with_decl =
let new_with_decl = match with_decl with
With_definition_body (_,c) ->
With_definition_body (idl,c)
- | With_module_body (_,c,t,cst) ->
- With_module_body (idl,c,t,cst) in
- check_with_aux_def env' (type_of_mb env old) new_with_decl
+ | With_module_body (_,c) ->
+ With_module_body (idl,c) in
+ check_with_aux_def env' old.mod_type new_with_decl (MPdot(mp,l))
| Some msb ->
error_a_generative_module_expected l
end
@@ -190,46 +186,35 @@ and check_with_aux_def env mtb with_decl =
Not_found -> error_no_such_label l
| Reduction.NotConvertible -> error_with_incorrect l
-and check_with_aux_mod env mtb with_decl =
- let initmsid,msid,sig_b =
- match eval_struct env mtb with
- | SEBstruct(msid,sig_b) ->
- let msid'=(refresh_msid msid) in
- msid,msid',(subst_signature_msid msid (MPself(msid')) sig_b)
+and check_with_aux_mod env mtb with_decl mp =
+ let sig_b =
+ match mtb with
+ | SEBstruct(sig_b) ->
+ sig_b
| _ -> error_signature_expected mtb in
- let id,idl = match with_decl with
- | With_definition_body (id::idl,_) | With_module_body (id::idl,_,_,_) ->
+ let id,idl = match with_decl with
+ | With_definition_body (id::idl,_) | With_module_body (id::idl,_) ->
id,idl
- | With_definition_body ([],_) | With_module_body ([],_,_,_) -> assert false
+ | With_definition_body ([],_) | With_module_body ([],_) -> assert false
in
let l = label_of_id id in
try
let rev_before,spec,after = list_split_assoc l [] sig_b in
let before = List.rev rev_before in
let rec mp_rec = function
- | [] -> MPself initmsid
+ | [] -> mp
| i::r -> MPdot(mp_rec r,label_of_id i)
- in
- let env' = Modops.add_signature (MPself msid) before env in
+ in
+ let env' = Modops.add_signature mp before empty_delta_resolver env in
match with_decl with
- | With_module_body ([],_,_,_) -> assert false
- | With_module_body ([id], mp,_,_) ->
- let old,alias = match spec with
- SFBmodule msb -> Some msb,None
- | SFBalias (mp',_,_) -> None,Some mp'
+ | With_module_body ([],_) -> assert false
+ | With_module_body ([id], mp1) ->
+ let _ = match spec with
+ SFBmodule msb -> msb
| _ -> error_not_a_module l
in
- let mtb' = lookup_modtype mp env' in
- let _ =
- match old,alias with
- Some msb,None -> ()
- | None,Some mp' ->
- check_modpath_equiv env' mp mp'
- | _,_ ->
- anomaly "Mod_typing:no implementation and no alias"
- in
- join (map_mp (mp_rec [id]) mp) mtb'.typ_alias
- | With_module_body (_::_,mp,_,_) ->
+ let _ = (lookup_module mp1 env) in ()
+ | With_module_body (_::_,mp) ->
let old = match spec with
SFBmodule msb -> msb
| _ -> error_not_a_module l
@@ -238,14 +223,12 @@ and check_with_aux_mod env mtb with_decl =
match old.mod_expr with
None ->
let new_with_decl = match with_decl with
- With_definition_body (_,c) ->
+ With_definition_body (_,c) ->
With_definition_body (idl,c)
- | With_module_body (_,c,t,cst) ->
- With_module_body (idl,c,t,cst) in
- let sub =
- check_with_aux_mod env'
- (type_of_mb env old) new_with_decl in
- join (map_mp (mp_rec idl) mp) sub
+ | With_module_body (_,c) ->
+ With_module_body (idl,c) in
+ check_with_aux_mod env'
+ old.mod_type new_with_decl (MPdot(mp,l))
| Some msb ->
error_a_generative_module_expected l
end
@@ -255,113 +238,111 @@ and check_with_aux_mod env mtb with_decl =
| Reduction.NotConvertible -> error_with_incorrect l
and check_module_type env mty =
- if mty.typ_strength <> None then
- failwith "strengthening of module types not supported";
- let sub = check_modexpr env mty.typ_expr in
- check_alias mty.typ_alias sub
+ let _ = check_modtype env mty.typ_expr mty.typ_mp in ()
-and check_module env mb =
- let sub =
- match mb.mod_expr, mb.mod_type with
- | None, None ->
- anomaly "Mod_typing.translate_module: empty type and expr in module entry"
- | None, Some mtb -> check_modexpr env mtb
-
- | Some mexpr, _ ->
- let sub1 = check_modexpr env mexpr in
- (match mb.mod_type with
- | None -> sub1
- | Some mte ->
- let sub2 = check_modexpr env mte in
- check_subtypes env
- {typ_expr = mexpr;
- typ_strength = None;
- typ_alias = sub1;}
- {typ_expr = mte;
- typ_strength = None;
- typ_alias = sub2;};
- sub2) in
- check_alias mb.mod_alias sub
-
-and check_structure_field (s,env) mp lab = function
+
+and check_module env mp mb =
+ match mb.mod_expr, mb.mod_type with
+ | None,mtb ->
+ let _ = check_modtype env mtb mb.mod_mp in ()
+ | Some mexpr, mtb when mtb==mexpr ->
+ let _ = check_modtype env mtb mb.mod_mp in ()
+ | Some mexpr, _ ->
+ let sign = check_modexpr env mexpr mb.mod_mp mb.mod_delta in
+ let _ = check_modtype env mb.mod_type mb.mod_mp mb.mod_delta in
+ check_subtypes env
+ {typ_mp=mp;
+ typ_expr=sign;
+ typ_expr_alg=None;
+ typ_constraints=Univ.Constraint.empty;
+ typ_delta = mb.mod_delta;}
+ {typ_mp=mp;
+ typ_expr=mb.mod_type;
+ typ_expr_alg=None;
+ typ_constraints=Univ.Constraint.empty;
+ typ_delta = mb.mod_delta;};
+
+and check_structure_field env mp lab res = function
| SFBconst cb ->
let c = make_con mp empty_dirpath lab in
- (s,check_constant_declaration env c cb)
+ check_constant_declaration env c cb
| SFBmind mib ->
- let kn = make_kn mp empty_dirpath lab in
- (s,Indtypes.check_inductive env kn mib)
+ let kn = make_mind mp empty_dirpath lab in
+ let kn = mind_of_delta res kn in
+ Indtypes.check_inductive env kn mib
| SFBmodule msb ->
- check_module env msb;
- let mp1 = MPdot(mp,lab) in
- let is_fun, sub = Modops.update_subst env msb mp1 in
- ((if is_fun then s else join s sub),
- Modops.add_module (MPdot(mp,lab)) msb env)
- | SFBalias(mp2,_,cst) ->
- (* cf Safe_typing.add_alias *)
- (try
- let mp' = MPdot(mp,lab) in
- let mp2' = scrape_alias mp2 env in
- let _,sub = Modops.update_subst env (lookup_module mp2' env) mp2' in
- let sub = update_subst sub (map_mp mp' mp2') in
- let sub = join_alias sub (map_mp mp' mp2') in
- let sub = add_mp mp' mp2' sub in
- (join s sub, register_alias mp' mp2 env)
- with Not_found -> failwith "unknown aliased module")
+ let _= check_module env (MPdot(mp,lab)) msb in
+ Modops.add_module msb env
| SFBmodtype mty ->
- let kn = MPdot(mp, lab) in
check_module_type env mty;
- (join s mty.typ_alias, add_modtype kn mty env)
-
-and check_modexpr env mse = match mse with
+ add_modtype (MPdot(mp,lab)) mty env
+
+and check_modexpr env mse mp_mse res = match mse with
+ | SEBident mp ->
+ let mb = lookup_module mp env in
+ (subst_and_strengthen mb mp_mse env).mod_type
+ | SEBfunctor (arg_id, mtb, body) ->
+ check_module_type env mtb ;
+ let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in
+ let sign = check_modexpr env' body mp_mse res in
+ SEBfunctor (arg_id, mtb, sign)
+ | SEBapply (f,m,cst) ->
+ let sign = check_modexpr env f mp_mse res in
+ let farg_id, farg_b, fbody_b = destr_functor env sign in
+ let mp =
+ try (path_of_mexpr m)
+ with Not_path -> error_application_to_not_path m
+ (* place for nondep_supertype *) in
+ let mtb = module_type_of_module env (Some mp) (lookup_module mp env) in
+ check_subtypes env mtb farg_b;
+ (subst_struct_expr (map_mbid farg_id mp) fbody_b)
+ | SEBwith(mte, with_decl) ->
+ let sign = check_modexpr env mte mp_mse res in
+ let sign = check_with env sign with_decl mp_mse in
+ sign
+ | SEBstruct(msb) ->
+ let _ = List.fold_left (fun env (lab,mb) ->
+ check_structure_field env mp_mse lab res mb) env msb in
+ SEBstruct(msb)
+
+and check_modtype env mse mp_mse res = match mse with
| SEBident mp ->
- let mp = scrape_alias mp env in
let mtb = lookup_modtype mp env in
- mtb.typ_alias
+ mtb.typ_expr
| SEBfunctor (arg_id, mtb, body) ->
check_module_type env mtb;
- let env' = add_module (MPbound arg_id) (module_body_of_type mtb) env in
- let sub = check_modexpr env' body in
- sub
+ let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in
+ let body = check_modtype env' body mp_mse res in
+ SEBfunctor(arg_id,mtb,body)
| SEBapply (f,m,cst) ->
- let sub1 = check_modexpr env f in
- let f'= eval_struct env f in
- let farg_id, farg_b, fbody_b = destr_functor env f' in
+ let sign = check_modtype env f mp_mse res in
+ let farg_id, farg_b, fbody_b = destr_functor env sign in
let mp =
- try scrape_alias (path_of_mexpr m) env
+ try (path_of_mexpr m)
with Not_path -> error_application_to_not_path m
- (* place for nondep_supertype *) in
- let mtb = lookup_modtype mp env in
- check_subtypes env mtb farg_b;
- let sub2 = match eval_struct env m with
- | SEBstruct (msid,sign) ->
- join_alias
- (subst_key (map_msid msid mp) mtb.typ_alias)
- (map_msid msid mp)
- | _ -> mtb.typ_alias in
- let sub3 = join_alias sub1 (map_mbid farg_id mp) in
- let sub4 = update_subst sub2 sub3 in
- join sub3 sub4
+ (* place for nondep_supertype *) in
+ let mtb = module_type_of_module env (Some mp) (lookup_module mp env) in
+ check_subtypes env mtb farg_b;
+ subst_struct_expr (map_mbid farg_id mp) fbody_b
| SEBwith(mte, with_decl) ->
- let sub1 = check_modexpr env mte in
- let sub2 = check_with env mte with_decl in
- join sub1 sub2
- | SEBstruct(msid,msb) ->
- let mp = MPself msid in
- let (sub,_) =
- List.fold_left (fun env (lab,mb) ->
- check_structure_field env mp lab mb) (empty_subst,env) msb in
- sub
-
+ let sign = check_modtype env mte mp_mse res in
+ let sign = check_with env sign with_decl mp_mse in
+ sign
+ | SEBstruct(msb) ->
+ let _ = List.fold_left (fun env (lab,mb) ->
+ check_structure_field env mp_mse lab res mb) env msb in
+ SEBstruct(msb)
+
(*
-let rec add_struct_expr_constraints env = function
+ let rec add_struct_expr_constraints env = function
| SEBident _ -> env
-
- | SEBfunctor (_,mtb,meb) ->
- add_struct_expr_constraints
- (add_modtype_constraints env mtb) meb
+
+ | SEBfunctor (_,mtb,meb) ->
+ add_struct_expr_constraints
+ (add_modtype_constraints env mtb) meb
| SEBstruct (_,structure_body) ->
- List.fold_left
+ List.fold_left
(fun env (l,item) -> add_struct_elem_constraints env item)
env
structure_body
@@ -369,20 +350,20 @@ let rec add_struct_expr_constraints env = function
| SEBapply (meb1,meb2,cst) ->
(* let g = Univ.merge_constraints cst Univ.initial_universes in
msgnl(str"ADDING FUNCTOR APPLICATION CONSTRAINTS:"++fnl()++
- Univ.pr_universes g++str"============="++fnl());
+ Univ.pr_universes g++str"============="++fnl());
*)
- Environ.add_constraints cst
- (add_struct_expr_constraints
- (add_struct_expr_constraints env meb1)
+ Environ.add_constraints cst
+ (add_struct_expr_constraints
+ (add_struct_expr_constraints env meb1)
meb2)
| SEBwith(meb,With_definition_body(_,cb))->
Environ.add_constraints cb.const_constraints
(add_struct_expr_constraints env meb)
| SEBwith(meb,With_module_body(_,_,cst))->
Environ.add_constraints cst
- (add_struct_expr_constraints env meb)
-
-and add_struct_elem_constraints env = function
+ (add_struct_expr_constraints env meb)
+
+and add_struct_elem_constraints env = function
| SFBconst cb -> Environ.add_constraints cb.const_constraints env
| SFBmind mib -> Environ.add_constraints mib.mind_constraints env
| SFBmodule mb -> add_module_constraints env mb
@@ -390,18 +371,18 @@ and add_struct_elem_constraints env = function
| SFBalias (mp,None) -> env
| SFBmodtype mtb -> add_modtype_constraints env mtb
-and add_module_constraints env mb =
+and add_module_constraints env mb =
let env = match mb.mod_expr with
| None -> env
| Some meb -> add_struct_expr_constraints env meb
in
let env = match mb.mod_type with
| None -> env
- | Some mtb ->
+ | Some mtb ->
add_struct_expr_constraints env mtb
in
Environ.add_constraints mb.mod_constraints env
-and add_modtype_constraints env mtb =
+and add_modtype_constraints env mtb =
add_struct_expr_constraints env mtb.typ_expr
*)
diff --git a/checker/modops.ml b/checker/modops.ml
index 498bd775..458c84d8 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -18,7 +18,7 @@ open Declarations
open Environ
(*i*)
-let error_not_a_constant l =
+let error_not_a_constant l =
error ("\""^(string_of_label l)^"\" is not a constant")
let error_not_a_functor _ = error "Application of not a functor"
@@ -32,13 +32,12 @@ let error_not_match l _ =
let error_no_such_label l = error ("No such label "^string_of_label l)
-let error_no_such_label_sub l l1 l2 =
- let l1 = string_of_msid l1 in
- let l2 = string_of_msid l2 in
- error (l1^" is not a subtype of "^l2^".\nThe field "^
- string_of_label l^" is missing (or invisible) in "^l1^".")
+let error_no_such_label_sub l l1 =
+ let l1 = string_of_mp l1 in
+ error ("The field "^
+ string_of_label l^" is missing in "^l1^".")
-let error_not_a_module_loc loc s =
+let error_not_a_module_loc loc s =
user_err_loc (loc,"",str ("\""^string_of_label s^"\" is not a module"))
let error_not_a_module s = error_not_a_module_loc dummy_loc s
@@ -56,38 +55,6 @@ let error_signature_expected mtb =
let error_application_to_not_path _ = error "Application to not path"
-
-let module_body_of_type mtb =
- { mod_type = Some mtb.typ_expr;
- mod_expr = None;
- mod_constraints = Constraint.empty;
- mod_alias = mtb.typ_alias;
- mod_retroknowledge = []}
-
-let module_type_of_module mp mb =
- {typ_expr =
- (match mb.mod_type with
- | Some expr -> expr
- | None -> (match mb.mod_expr with
- | Some expr -> expr
- | None ->
- anomaly "Modops: empty expr and type"));
- typ_alias = mb.mod_alias;
- typ_strength = mp
- }
-
-
-
-let rec list_split_assoc k rev_before = function
- | [] -> raise Not_found
- | (k',b)::after when k=k' -> rev_before,b,after
- | h::tail -> list_split_assoc k (h::rev_before) tail
-
-let path_of_seb = function
- | SEBident mp -> mp
- | _ -> anomaly "Modops: evaluation failed."
-
-
let destr_functor env mtb =
match mtb with
| SEBfunctor (arg_id,arg_t,body_t) ->
@@ -95,254 +62,152 @@ let destr_functor env mtb =
| _ -> error_not_a_functor mtb
-let rec check_modpath_equiv env mp1 mp2 =
- if mp1=mp2 then () else
- let mp1 = scrape_alias mp1 env in
- let mp2 = scrape_alias mp2 env in
- if mp1=mp2 then ()
- else
- error_not_equal mp1 mp2
-
-
-
-let strengthen_const env mp l cb =
- match cb.const_opaque, cb.const_body with
- | false, Some _ -> cb
- | true, Some _
- | _, None ->
- let const = Const (make_con mp empty_dirpath l) in
- let const_subs = Some (Declarations.from_val const) in
- {cb with
- const_body = const_subs;
- const_opaque = false
- }
-
-let strengthen_mind env mp l mib = match mib.mind_equiv with
- | Some _ -> mib
- | None -> {mib with mind_equiv = Some (make_kn mp empty_dirpath l)}
+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;
+ mod_type_alg = mtb.typ_expr_alg;
+ mod_expr = None;
+ mod_constraints = mtb.typ_constraints;
+ mod_delta = mtb.typ_delta;
+ mod_retroknowledge = []}
-let rec eval_struct env = function
- | SEBident mp ->
- begin
- let mp = scrape_alias mp env in
- let mtb =lookup_modtype mp env in
- match mtb.typ_expr,mtb.typ_strength with
- mtb,None -> eval_struct env mtb
- | mtb,Some mp -> strengthen_mtb env mp (eval_struct env mtb)
- end
- | SEBapply (seb1,seb2,_) ->
- let svb1 = eval_struct env seb1 in
- let farg_id, farg_b, fbody_b = destr_functor env svb1 in
- let mp = path_of_seb seb2 in
- let mp = scrape_alias mp env in
- let sub_alias = (lookup_modtype mp env).typ_alias in
- let sub_alias = match eval_struct env (SEBident mp) with
- | SEBstruct (msid,sign) -> subst_key (map_msid msid mp) sub_alias
- | _ -> sub_alias in
- let sub_alias = update_subst_alias sub_alias
- (map_mbid farg_id mp) in
- eval_struct env (subst_struct_expr
- (join sub_alias (map_mbid farg_id mp)) fbody_b)
- | SEBwith (mtb,(With_definition_body _ as wdb)) ->
- merge_with env mtb wdb empty_subst
- | SEBwith (mtb, (With_module_body (_,mp,_,_) as wdb)) ->
- let alias_in_mp =
- (lookup_modtype mp env).typ_alias in
- merge_with env mtb wdb alias_in_mp
-(* | SEBfunctor(mbid,mtb,body) ->
- let env = add_module (MPbound mbid) (module_body_of_type mtb) env in
- SEBfunctor(mbid,mtb,eval_struct env body) *)
- | mtb -> mtb
-
-and type_of_mb env mb =
- match mb.mod_type,mb.mod_expr with
- None,Some b -> eval_struct env b
- | Some t, _ -> eval_struct env t
- | _,_ -> anomaly
- "Modops: empty type and empty expr"
-
-and merge_with env mtb with_decl alias=
- let msid,sig_b = match (eval_struct env mtb) with
- | SEBstruct(msid,sig_b) -> msid,sig_b
- | _ -> error_signature_expected mtb
- in
- let id,idl = match with_decl with
- | With_definition_body (id::idl,_) | With_module_body (id::idl,_,_,_) -> id,idl
- | With_definition_body ([],_) | With_module_body ([],_,_,_) -> assert false
- in
- let l = label_of_id id in
- try
- let rev_before,spec,after = list_split_assoc l [] sig_b in
- let before = List.rev rev_before in
- let rec mp_rec = function
- | [] -> MPself msid
- | i::r -> MPdot(mp_rec r,label_of_id i)
- in
- let new_spec,subst = match with_decl with
- | With_definition_body ([],_)
- | With_module_body ([],_,_,_) -> assert false
- | With_definition_body ([id],c) ->
- SFBconst c,None
- | With_module_body ([id], mp,typ_opt,cst) ->
- let mp' = scrape_alias mp env in
- SFBalias (mp,typ_opt,Some cst),
- Some(join (map_mp (mp_rec [id]) mp') alias)
- | With_definition_body (_::_,_)
- | With_module_body (_::_,_,_,_) ->
- let old = match spec with
- SFBmodule msb -> msb
- | _ -> error_not_a_module l
- in
- let new_with_decl,subst1 =
- match with_decl with
- With_definition_body (_,c) -> With_definition_body (idl,c),None
- | With_module_body (idc,mp,t,cst) ->
- With_module_body (idl,mp,t,cst),
- Some(map_mp (mp_rec idc) mp)
- in
- let subst = Option.fold_right join subst1 alias in
- let modtype =
- merge_with env (type_of_mb env old) new_with_decl alias in
- let msb =
- { mod_expr = None;
- mod_type = Some modtype;
- mod_constraints = old.mod_constraints;
- mod_alias = subst;
- mod_retroknowledge = old.mod_retroknowledge}
- in
- (SFBmodule msb),Some subst
- in
- SEBstruct(msid, before@(l,new_spec)::
- (Option.fold_right subst_structure subst after))
- with
- Not_found -> error_no_such_label l
+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
-and add_signature mp sign env =
+let rec add_signature mp sign resolver env =
let add_one env (l,elem) =
let kn = make_kn mp empty_dirpath l in
- let con = make_con mp empty_dirpath l in
+ let con = constant_of_kn kn in
+ let mind = mind_of_delta resolver (mind_of_kn kn) in
match elem with
- | SFBconst cb -> Environ.add_constant con cb env
- | SFBmind mib -> Environ.add_mind kn mib env
- | SFBmodule mb ->
- add_module (MPdot (mp,l)) mb env
+ | SFBconst cb ->
+ (* let con = constant_of_delta resolver con in*)
+ Environ.add_constant con cb env
+ | SFBmind mib ->
+ (* let mind = mind_of_delta resolver mind in*)
+ Environ.add_mind mind mib env
+ | SFBmodule mb -> add_module mb env
(* adds components as well *)
- | SFBalias (mp1,_,cst) ->
- Environ.register_alias (MPdot(mp,l)) mp1 env
- | SFBmodtype mtb -> Environ.add_modtype (MPdot(mp,l))
- mtb env
+ | SFBmodtype mtb -> Environ.add_modtype mtb.typ_mp mtb env
in
List.fold_left add_one env sign
-and add_module mp mb env =
+and add_module mb env =
+ let mp = mb.mod_mp in
let env = Environ.shallow_add_module mp mb env in
- let env =
- Environ.add_modtype mp (module_type_of_module (Some mp) mb) env
- in
- let mod_typ = type_of_mb env mb in
- match mod_typ with
- | SEBstruct (msid,sign) ->
- add_signature mp (subst_signature_msid msid mp sign) env
+ match mb.mod_type with
+ | SEBstruct (sign) ->
+ add_signature mp sign mb.mod_delta env
| SEBfunctor _ -> env
| _ -> anomaly "Modops:the evaluation of the structure failed "
-
-and constants_of_specification env mp sign =
- let aux (env,res) (l,elem) =
- match elem with
- | SFBconst cb -> env,((make_con mp empty_dirpath l),cb)::res
- | SFBmind _ -> env,res
- | SFBmodule mb ->
- let new_env = add_module (MPdot (mp,l)) mb env in
- new_env,(constants_of_modtype env (MPdot (mp,l))
- (type_of_mb env mb)) @ res
- | SFBalias (mp1,_,cst) ->
- let new_env = register_alias (MPdot (mp,l)) mp1 env in
- new_env,(constants_of_modtype env (MPdot (mp,l))
- (eval_struct env (SEBident mp1))) @ res
- | SFBmodtype mtb ->
- (* module type dans un module type.
- Il faut au moins mettre mtb dans l'environnement (avec le bon
- kn pour pouvoir continuer aller deplier les modules utilisant ce
- mtb
- ex:
- Module Type T1.
- Module Type T2.
- ....
- End T2.
- .....
- Declare Module M : T2.
- End T2
- si on ne rajoute pas T2 dans l'environement de typage
- on va exploser au moment du Declare Module
- *)
- let new_env = Environ.add_modtype (MPdot(mp,l)) mtb env in
- new_env, (constants_of_modtype env (MPdot(mp,l)) mtb.typ_expr) @ res
- in
- snd (List.fold_left aux (env,[]) sign)
+let strengthen_const env mp_from l cb resolver =
+ match cb.const_opaque, cb.const_body with
+ | false, Some _ -> cb
+ | true, Some _
+ | _, None ->
+ 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;
+ }
+
-and constants_of_modtype env mp modtype =
- match (eval_struct env modtype) with
- SEBstruct (msid,sign) ->
- constants_of_specification env mp
- (subst_signature_msid msid mp sign)
- | SEBfunctor _ -> []
- | _ -> anomaly "Modops:the evaluation of the structure failed "
+let rec strengthen_mod env mp_from mp_to mb =
+ if Declarations.mp_in_delta mb.mod_mp mb.mod_delta then
+ mb
+ else
+ match mb.mod_type with
+ | SEBstruct (sign) ->
+ let resolve_out,sign_out =
+ strengthen_sig env mp_from sign mp_to mb.mod_delta in
+ { mb with
+ mod_expr = Some (SEBident mp_to);
+ mod_type = SEBstruct(sign_out);
+ mod_type_alg = mb.mod_type_alg;
+ mod_constraints = mb.mod_constraints;
+ mod_delta = resolve_out(*add_mp_delta_resolver mp_from mp_to
+ (add_delta_resolver mb.mod_delta resolve_out)*);
+ mod_retroknowledge = mb.mod_retroknowledge}
+ | SEBfunctor _ -> mb
+ | _ -> anomaly "Modops:the evaluation of the structure failed "
+
+and strengthen_sig env mp_from sign mp_to resolver =
+ match sign with
+ | [] -> empty_delta_resolver,[]
+ | (l,SFBconst cb) :: rest ->
+ let item' =
+ l,SFBconst (strengthen_const env mp_from l cb resolver) in
+ let resolve_out,rest' =
+ strengthen_sig env mp_from rest mp_to resolver in
+ resolve_out,item'::rest'
+ | (_,SFBmind _ as item):: rest ->
+ let resolve_out,rest' =
+ strengthen_sig env mp_from rest mp_to resolver in
+ 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 env mp_from' mp_to' mb in
+ let item' = l,SFBmodule (mb_out) in
+ let env' = add_module mb_out env in
+ let resolve_out,rest' =
+ strengthen_sig env' mp_from rest mp_to resolver in
+ resolve_out
+ (*add_delta_resolver resolve_out mb.mod_delta*),
+ item':: rest'
+ | (l,SFBmodtype mty as item) :: rest ->
+ let env' = add_modtype
+ (MPdot(mp_from,l)) mty env
+ in
+ let resolve_out,rest' =
+ strengthen_sig env' mp_from rest mp_to resolver in
+ resolve_out,item::rest'
-and strengthen_mtb env mp mtb =
- let mtb1 = eval_struct env mtb in
- match mtb1 with
- | SEBfunctor _ -> mtb1
- | SEBstruct (msid,sign) ->
- SEBstruct (msid,strengthen_sig env msid sign mp)
- | _ -> anomaly "Modops:the evaluation of the structure failed "
+let strengthen env mtb mp =
+ match mtb.typ_expr with
+ | SEBstruct (sign) ->
+ let resolve_out,sign_out =
+ strengthen_sig env 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 "
-and strengthen_mod env mp mb =
- let mod_typ = type_of_mb env mb in
- { mod_expr = mb.mod_expr;
- mod_type = Some (strengthen_mtb env mp mod_typ);
- mod_constraints = mb.mod_constraints;
- mod_alias = mb.mod_alias;
- mod_retroknowledge = mb.mod_retroknowledge}
-
-and strengthen_sig env msid sign mp = match sign with
- | [] -> []
- | (l,SFBconst cb) :: rest ->
- let item' = l,SFBconst (strengthen_const env mp l cb) in
- let rest' = strengthen_sig env msid rest mp in
- item'::rest'
- | (l,SFBmind mib) :: rest ->
- let item' = l,SFBmind (strengthen_mind env mp l mib) in
- let rest' = strengthen_sig env msid rest mp in
- item'::rest'
- | (l,SFBmodule mb) :: rest ->
- let mp' = MPdot (mp,l) in
- let item' = l,SFBmodule (strengthen_mod env mp' mb) in
- let env' = add_module
- (MPdot (MPself msid,l)) mb env in
- let rest' = strengthen_sig env' msid rest mp in
- item':: rest'
- | ((l,SFBalias (mp1,_,cst)) as item) :: rest ->
- let env' = register_alias (MPdot(MPself msid,l)) mp1 env in
- let rest' = strengthen_sig env' msid rest mp in
- item::rest'
- | (l,SFBmodtype mty as item) :: rest ->
- let env' = add_modtype
- (MPdot((MPself msid),l))
- mty
- env
- in
- let rest' = strengthen_sig env' msid rest mp in
- item::rest'
+let subst_and_strengthen mb mp env =
+ strengthen_mod env mb.mod_mp mp
+ (subst_module (map_mp mb.mod_mp mp) mb)
-
-let strengthen env mtb mp = strengthen_mtb env mp mtb
-let update_subst env mb mp =
- match type_of_mb env mb with
- | SEBstruct(msid,str) -> false, join_alias
- (subst_key (map_msid msid mp) mb.mod_alias)
- (map_msid msid mp)
- | _ -> true, mb.mod_alias
+let module_type_of_module env mp mb =
+ match mp with
+ Some mp ->
+ strengthen env {
+ typ_mp = mp;
+ typ_expr = mb.mod_type;
+ typ_expr_alg = None;
+ typ_constraints = mb.mod_constraints;
+ typ_delta = mb.mod_delta} mp
+
+ | None ->
+ {typ_mp = mb.mod_mp;
+ typ_expr = mb.mod_type;
+ typ_expr_alg = None;
+ typ_constraints = mb.mod_constraints;
+ typ_delta = mb.mod_delta}
diff --git a/checker/modops.mli b/checker/modops.mli
index 17b063e2..4476013c 100644
--- a/checker/modops.mli
+++ b/checker/modops.mli
@@ -19,35 +19,27 @@ open Environ
(* Various operations on modules and module types *)
-(* make the environment entry out of type *)
-val module_body_of_type : module_type_body -> module_body
+(* make the envirconment entry out of type *)
+val module_body_of_type : module_path -> module_type_body -> module_body
-val module_type_of_module : module_path option -> module_body ->
- module_type_body
+val module_type_of_module : env -> module_path option -> module_body ->
+ module_type_body
-val destr_functor :
+val destr_functor :
env -> struct_expr_body -> mod_bound_id * module_type_body * struct_expr_body
-(* Evaluation functions *)
-val eval_struct : env -> struct_expr_body -> struct_expr_body
-
-val type_of_mb : env -> module_body -> struct_expr_body
-
-(* [add_signature mp sign env] assumes that the substitution [msid]
- $\mapsto$ [mp] has already been performed (or is not necessary, like
- when [mp = MPself msid]) *)
-val add_signature : module_path -> structure_body -> env -> env
+val add_signature : module_path -> structure_body -> delta_resolver -> env -> env
(* adds a module and its components, but not the constraints *)
-val add_module : module_path -> module_body -> env -> env
+val add_module : module_body -> env -> env
val check_modpath_equiv : env -> module_path -> module_path -> unit
-val strengthen : env -> struct_expr_body -> module_path -> struct_expr_body
+val strengthen : env -> module_type_body -> module_path -> module_type_body
-val update_subst : env -> module_body -> module_path -> bool * substitution
+val subst_and_strengthen : module_body -> module_path -> env -> module_body
-val error_incompatible_modtypes :
+val error_incompatible_modtypes :
module_type_body -> module_type_body -> 'a
val error_not_match : label -> structure_field_body -> 'a
@@ -57,13 +49,13 @@ val error_with_incorrect : label -> 'a
val error_no_such_label : label -> 'a
val error_no_such_label_sub :
- label -> mod_self_id -> mod_self_id -> 'a
+ label -> module_path -> 'a
val error_signature_expected : struct_expr_body -> 'a
val error_not_a_constant : label -> 'a
-val error_not_a_module : label -> 'a
+val error_not_a_module : label -> 'a
val error_a_generative_module_expected : label -> 'a
diff --git a/checker/reduction.ml b/checker/reduction.ml
index c398f0a4..54b8fd48 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -86,13 +86,13 @@ let whd_betaiotazeta env x =
Prod _|Lambda _|Fix _|CoFix _) -> x
| _ -> whd_val (create_clos_infos betaiotazeta env) (inject x)
-let whd_betadeltaiota env t =
+let whd_betadeltaiota env t =
match t with
| (Sort _|Meta _|Evar _|Ind _|Construct _|
Prod _|Lambda _|Fix _|CoFix _) -> t
| _ -> whd_val (create_clos_infos betadeltaiota env) (inject t)
-let whd_betadeltaiota_nolet env t =
+let whd_betadeltaiota_nolet env t =
match t with
| (Sort _|Meta _|Evar _|Ind _|Construct _|
Prod _|Lambda _|Fix _|CoFix _|LetIn _) -> t
@@ -107,6 +107,15 @@ 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 *)
(********************************************************************)
@@ -139,8 +148,8 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 =
(* Convertibility of sorts *)
-type conv_pb =
- | CONV
+type conv_pb =
+ | CONV
| CUMUL
let sort_cmp univ pb s0 s1 =
@@ -202,7 +211,7 @@ let oracle_order fl1 fl2 =
| _ -> false
(* Conversion between [lft1]term1 and [lft2]term2 *)
-let rec ccnv univ cv_pb infos lft1 lft2 term1 term2 =
+let rec ccnv univ cv_pb infos lft1 lft2 term1 term2 =
eqappr univ cv_pb infos (lft1, (term1,[])) (lft2, (term2,[]))
(* Conversion between [lft1](hd1 v1) and [lft2](hd2 v2) *)
@@ -224,7 +233,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
(* case of leaves *)
| (FAtom a1, FAtom a2) ->
(match a1, a2 with
- | (Sort s1, Sort s2) ->
+ | (Sort s1, Sort s2) ->
assert (is_empty_stack v1 && is_empty_stack v2);
sort_cmp univ cv_pb s1 s2
| (Meta n, Meta m) ->
@@ -247,7 +256,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
(* 2 constants, 2 local defined vars or 2 defined rels *)
| (FFlex fl1, FFlex fl2) ->
(try (* try first intensional equality *)
- if fl1 = fl2
+ if eq_table_key fl1 fl2
then convert_stacks univ infos lft1 lft2 v1 v2
else raise NotConvertible
with NotConvertible ->
@@ -272,15 +281,15 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
(* only one constant, defined var or defined rel *)
| (FFlex fl1, _) ->
(match unfold_reference infos fl1 with
- | Some def1 ->
+ | 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 ->
+ | Some def2 ->
eqappr univ cv_pb infos appr1 (lft2, whd_stack infos def2 v2)
| None -> raise NotConvertible)
-
+
(* other constructors *)
| (FLambda _, FLambda _) ->
assert (is_empty_stack v1 && is_empty_stack v2);
@@ -318,7 +327,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
let fcl1 = Array.map (mk_clos (subs_liftn n e1)) cl1 in
let fcl2 = Array.map (mk_clos (subs_liftn n e2)) cl2 in
convert_vect univ infos el1 el2 fty1 fty2;
- convert_vect univ infos
+ convert_vect univ infos
(el_liftn n el1) (el_liftn n el2) fcl1 fcl2;
convert_stacks univ infos lft1 lft2 v1 v2
else raise NotConvertible
@@ -341,7 +350,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
| ( (FLetIn _, _) | (FCases _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_)
| (_, FLetIn _) | (_,FCases _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _)
| (FLOCKED,_) | (_,FLOCKED) ) -> assert false
-
+
(* In all other cases, terms are not convertible *)
| _ -> raise NotConvertible
@@ -368,9 +377,9 @@ let conv = fconv CONV
let conv_leq = fconv CUMUL
let conv_leq_vecti env v1 v2 =
- array_fold_left2_i
+ array_fold_left2_i
(fun i _ t1 t2 ->
- (try conv_leq env t1 t2
+ (try conv_leq env t1 t2
with (NotConvertible|Invalid_argument _) ->
raise (NotConvertibleVect i));
())
@@ -382,13 +391,13 @@ let conv_leq_vecti env v1 v2 =
let vm_conv = ref fconv
let set_vm_conv f = vm_conv := f
-let vm_conv cv_pb env t1 t2 =
- try
+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
-
+
(********************************************************************)
(* Special-Purpose Reduction *)
(********************************************************************)
@@ -404,12 +413,12 @@ let hnf_prod_app env t n =
| Prod (_,_,b) -> subst1 n b
| _ -> anomaly "hnf_prod_app: Need a product"
-let hnf_prod_applist env t nl =
+let hnf_prod_applist env t nl =
List.fold_left (hnf_prod_app env) t nl
(* Dealing with arities *)
-let dest_prod env =
+let dest_prod env =
let rec decrec env m c =
let t = whd_betadeltaiota env c in
match t with
@@ -417,11 +426,11 @@ let dest_prod env =
let d = (n,None,a) in
decrec (push_rel d env) (d::m) c0
| _ -> m,t
- in
+ in
decrec env empty_rel_context
(* The same but preserving lets *)
-let dest_prod_assum env =
+let dest_prod_assum env =
let rec prodec_rec env l ty =
let rty = whd_betadeltaiota_nolet env ty in
match rty with
diff --git a/checker/reduction.mli b/checker/reduction.mli
index eb50ae32..81c93ee5 100644
--- a/checker/reduction.mli
+++ b/checker/reduction.mli
@@ -37,9 +37,12 @@ val vm_conv : conv_pb -> constr conversion_function
(************************************************************************)
-(* Builds an application node, reducing beta redexes it may produce. *)
+(* 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
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index f4ffb302..8f5d4573 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -30,9 +30,8 @@ let set_engagement c =
(* full_add_module adds module with universes and constraints *)
let full_add_module dp mb digest =
let env = !genv in
- let mp = MPfile dp in
let env = add_constraints mb.mod_constraints env in
- let env = Modops.add_module mp mb env in
+ let env = Modops.add_module mb env in
genv := add_digest env dp digest
(* Check that the engagement expected by a library matches the initial one *)
@@ -58,7 +57,7 @@ let check_imports f caller env needed =
try
let actual_stamp = lookup_digest env dp in
if stamp <> actual_stamp then report_clash f caller dp
- with Not_found ->
+ with Not_found ->
error ("Reference to unknown module " ^ (string_of_dirpath dp))
in
List.iter check needed
@@ -66,46 +65,46 @@ let check_imports f caller env needed =
(* Remove the body of opaque constants in modules *)
-(* also remove mod_expr ? *)
+(* also remove mod_expr ? Good idea!*)
let rec lighten_module mb =
{ mb with
mod_expr = Option.map lighten_modexpr mb.mod_expr;
- mod_type = Option.map lighten_modexpr mb.mod_type }
+ mod_type = lighten_modexpr mb.mod_type }
-and lighten_struct struc =
+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 _ | SFBalias _) as x -> x
+ | (SFBconst _ | SFBmind _ ) as x -> x
| SFBmodule m -> SFBmodule (lighten_module m)
- | SFBmodtype m -> SFBmodtype
- ({m with
+ | 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
+ SEBfunctor (mbid,
+ ({mty with
typ_expr = lighten_modexpr mty.typ_expr}),
lighten_modexpr mexpr)
| SEBident mp as x -> x
- | SEBstruct (msid, struc) ->
- SEBstruct (msid, lighten_struct struc)
+ | 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)
-
+ SEBwith (lighten_modexpr seb,wdcl)
+
let lighten_library (dp,mb,depends,s) = (dp,lighten_module mb,depends,s)
-type compiled_library =
+type compiled_library =
dir_path *
module_body *
(dir_path * Digest.t) list *
engagement option
-
+
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|]
@@ -119,20 +118,21 @@ let stamp_library file digest = ()
(* When the module is checked, digests do not need to match, but a
warning is issued in case of mismatch *)
-let import file (dp,mb,depends,engmt as vo) digest =
+let import file (dp,mb,depends,engmt as vo) digest =
Validate.apply !Flags.debug val_vo vo;
Flags.if_verbose msgnl (str "*** vo structure validated ***");
let env = !genv in
check_imports msg_warning dp env depends;
check_engagement env engmt;
- check_module (add_constraints mb.mod_constraints env) mb;
+ 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 =
+let unsafe_import file (dp,mb,depends,engmt as vo) digest =
+(* if !Flags.debug then 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/subtyping.ml b/checker/subtyping.ml
index 7a6868fe..3a100c01 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -19,29 +19,28 @@ open Reduction
open Inductive
open Modops
(*i*)
-open Pp
+open Pp
(* This local type is used to subtype a constant with a constructor or
an inductive type. It can also be useful to allow reorderings in
inductive types *)
-type namedobject =
+type namedobject =
| Constant of constant_body
| IndType of inductive * mutual_inductive_body
| IndConstr of constructor * mutual_inductive_body
| Module of module_body
| Modtype of module_type_body
- | Alias of module_path * struct_expr_body option
(* adds above information about one mutual inductive: all types and
constructors *)
-let add_nameobjects_of_mib ln mib map =
+let add_nameobjects_of_mib ln mib map =
let add_nameobjects_of_one j oib map =
let ip = (ln,j) in
- let map =
- array_fold_right_i
+ let map =
+ array_fold_right_i
(fun i id map ->
Labmap.add (label_of_id id) (IndConstr((ip,i+1), mib)) map)
oib.mind_consnames
@@ -54,19 +53,19 @@ let add_nameobjects_of_mib ln mib map =
(* creates namedobject map for the whole signature *)
-let make_label_map mp list =
- let add_one (l,e) map =
+let make_label_map mp list =
+ let add_one (l,e) map =
let add_map obj = Labmap.add l obj map in
match e with
| SFBconst cb -> add_map (Constant cb)
| SFBmind mib ->
- add_nameobjects_of_mib (make_kn mp empty_dirpath l) mib map
+ add_nameobjects_of_mib (make_mind mp empty_dirpath l) mib map
| SFBmodule mb -> add_map (Module mb)
| SFBmodtype mtb -> add_map (Modtype mtb)
- | SFBalias (mp,t,cst) -> add_map (Alias (mp,t))
in
List.fold_right add_one list Labmap.empty
+
let check_conv_error error f env a1 a2 =
try
f env a1 a2
@@ -74,20 +73,21 @@ let check_conv_error error f env a1 a2 =
NotConvertible -> error ()
(* for now we do not allow reorderings *)
-let check_inductive env msid1 l info1 mib2 spec2 =
- let kn = make_kn (MPself msid1) empty_dirpath l in
+let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2=
+ let kn = make_mind mp1 empty_dirpath l in
let error () = error_not_match l spec2 in
let check_conv f = check_conv_error error f in
- let mib1 =
+ let mib1 =
match info1 with
| IndType ((_,0), mib) -> mib
| _ -> error ()
in
+ let mib2 = subst_mind subst2 mib2 in
let check_inductive_type env t1 t2 =
(* Due to sort-polymorphism in inductive types, the conclusions of
t1 and t2, if in Type, are generated as the least upper bounds
- of the types of the constructors.
+ of the types of the constructors.
By monotonicity of the infered l.u.b. wrt subtyping (i.e. if X:U
|- T(X):s and |- M:U' and U'<=U then infer_type(T(M))<=s), each
@@ -114,7 +114,7 @@ let check_inductive env msid1 l info1 mib2 spec2 =
| Type _, Type _ -> (* shortcut here *) Prop Null, Prop Null
| (Prop _, Type _) | (Type _,Prop _) -> error ()
| _ -> (s1, s2) in
- check_conv conv_leq env
+ check_conv conv_leq env
(mkArity (ctx1,s1)) (mkArity (ctx2,s2))
in
@@ -145,7 +145,7 @@ let check_inductive env msid1 l info1 mib2 spec2 =
check (fun mib -> mib.mind_finite);
check (fun mib -> mib.mind_ntypes);
assert (mib1.mind_hyps=[] && mib2.mind_hyps=[]);
- assert (Array.length mib1.mind_packets >= 1
+ assert (Array.length mib1.mind_packets >= 1
&& Array.length mib2.mind_packets >= 1);
(* Check that the expected numbers of uniform parameters are the same *)
@@ -155,30 +155,30 @@ let check_inductive env msid1 l info1 mib2 spec2 =
(* the inductive types and constructors types have to be convertible *)
check (fun mib -> mib.mind_nparams);
- begin
+ (*begin
match mib2.mind_equiv with
| None -> ()
- | Some kn2' ->
+ | Some kn2' ->
let kn2 = scrape_mind env kn2' in
let kn1 = match mib1.mind_equiv with
None -> kn
| Some kn1' -> scrape_mind env kn1'
in
if kn1 <> kn2 then error ()
- end;
+ end;*)
(* we check that records and their field names are preserved. *)
check (fun mib -> mib.mind_record);
- if mib1.mind_record then begin
- let rec names_prod_letin t = match t with
+ if mib1.mind_record then begin
+ let rec names_prod_letin t = match t with
| Prod(n,_,t) -> n::(names_prod_letin t)
| LetIn(n,_,_,t) -> n::(names_prod_letin t)
| Cast(t,_,_) -> names_prod_letin t
| _ -> []
- in
+ in
assert (Array.length mib1.mind_packets = 1);
assert (Array.length mib2.mind_packets = 1);
- assert (Array.length mib1.mind_packets.(0).mind_user_lc = 1);
- assert (Array.length mib2.mind_packets.(0).mind_user_lc = 1);
+ assert (Array.length mib1.mind_packets.(0).mind_user_lc = 1);
+ assert (Array.length mib2.mind_packets.(0).mind_user_lc = 1);
check (fun mib -> names_prod_letin mib.mind_packets.(0).mind_user_lc.(0));
end;
(* we first check simple things *)
@@ -187,10 +187,10 @@ let check_inductive env msid1 l info1 mib2 spec2 =
let _ = array_map2_i check_cons_types mib1.mind_packets mib2.mind_packets
in ()
-let check_constant env msid1 l info1 cb2 spec2 =
+let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
let error () = error_not_match l spec2 in
let check_conv f = check_conv_error error f in
- let check_type env t1 t2 =
+ let check_type env t1 t2 =
(* If the type of a constant is generated, it may mention
non-variable algebraic universes that the general conversion
@@ -201,7 +201,7 @@ let check_constant env msid1 l info1 cb2 spec2 =
Gamma |- A |> T, Gamma |- A' |> T' and Gamma |- A=A' then T <= T').
Hence they don't have to be checked again *)
- let t1,t2 =
+ let t1,t2 =
if isArity t2 then
let (ctx2,s2) = destArity t2 in
match s2 with
@@ -236,30 +236,31 @@ let check_constant env msid1 l info1 cb2 spec2 =
(t1,t2) in
check_conv conv_leq env t1 t2
in
-
- match info1 with
- | Constant cb1 ->
- assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ;
- (*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;
- let con = make_con (MPself msid1) 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
- | _ -> ())
- | IndType ((kn,i),mind1) ->
- ignore (Util.error (
- "The kernel does not recognize yet that a parameter can be " ^
- "instantiated by an inductive type. Hint: you can rename the " ^
- "inductive type and give a definition to map the old name to the new " ^
- "name."));
+ 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
+ | _ -> ())
+ | IndType ((kn,i),mind1) ->
+ ignore (Util.error (
+ "The kernel does not recognize yet that a parameter can be " ^
+ "instantiated by an inductive type. Hint: you can rename the " ^
+ "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 () ;
let arity1 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in
@@ -278,111 +279,96 @@ let check_constant env msid1 l info1 cb2 spec2 =
check_conv conv env ty1 ty2
| _ -> error ()
-let rec check_modules env msid1 l msb1 msb2 =
- let mp = (MPdot(MPself msid1,l)) in
- let mty1 = module_type_of_module (Some mp) msb1 in
- let mty2 = module_type_of_module None msb2 in
- check_modtypes env mty1 mty2 false
-
+let rec check_modules env msb1 msb2 subst1 subst2 =
+ let mty1 = module_type_of_module env None msb1 in
+ let mty2 = module_type_of_module env None msb2 in
+ check_modtypes env mty1 mty2 subst1 subst2 false;
+
-and check_signatures env (msid1,sig1) alias (msid2,sig2') =
- let mp1 = MPself msid1 in
- let env = add_signature mp1 sig1 env in
- let alias = update_subst_alias alias (map_msid msid2 mp1) in
- let sig2 = subst_structure alias sig2' in
- let sig2 = subst_signature_msid msid2 mp1 sig2 in
+and check_signatures env mp1 sig1 sig2 subst1 subst2 =
let map1 = make_label_map mp1 sig1 in
- let check_one_body (l,spec2) =
- let info1 =
- try
- Labmap.find l map1
- with
- Not_found -> error_no_such_label_sub l msid1 msid2
+ let check_one_body (l,spec2) =
+ let info1 =
+ try
+ Labmap.find l map1
+ with
+ Not_found -> error_no_such_label_sub l mp1
in
match spec2 with
| SFBconst cb2 ->
- check_constant env msid1 l info1 cb2 spec2
- | SFBmind mib2 ->
- check_inductive env msid1 l info1 mib2 spec2
- | SFBmodule msb2 ->
+ check_constant env mp1 l info1 cb2 spec2 subst1 subst2
+ | SFBmind mib2 ->
+ check_inductive env mp1 l info1 mib2 spec2 subst1 subst2
+ | SFBmodule msb2 ->
begin
match info1 with
- | Module msb -> check_modules env msid1 l msb msb2
- | Alias (mp,typ_opt) ->let msb =
- {mod_expr = Some (SEBident mp);
- mod_type = typ_opt;
- mod_constraints = Constraint.empty;
- mod_alias = (lookup_modtype mp env).typ_alias;
- mod_retroknowledge = []} in
- check_modules env msid1 l msb msb2
- | _ -> error_not_match l spec2
- end
- | SFBalias (mp,typ_opt,_) ->
- begin
- match info1 with
- | Alias (mp1,_) -> check_modpath_equiv env mp mp1
- | Module msb ->
- let msb1 =
- {mod_expr = Some (SEBident mp);
- mod_type = typ_opt;
- mod_constraints = Constraint.empty;
- mod_alias = (lookup_modtype mp env).typ_alias;
- mod_retroknowledge = []} in
- check_modules env msid1 l msb msb1
+ | Module msb -> check_modules env msb msb2
+ subst1 subst2
| _ -> error_not_match l spec2
end
| SFBmodtype mtb2 ->
- let mtb1 =
+ let mtb1 =
match info1 with
| Modtype mtb -> mtb
| _ -> error_not_match l spec2
in
- check_modtypes env mtb1 mtb2 true
+ let env = add_module (module_body_of_type mtb2.typ_mp mtb2)
+ (add_module (module_body_of_type mtb1.typ_mp mtb1) env) in
+ check_modtypes env mtb1 mtb2 subst1 subst2 true
in
List.iter check_one_body sig2
-and check_modtypes env mtb1 mtb2 equiv =
- if mtb1==mtb2 then () else (* just in case :) *)
- let mtb1',mtb2'=
- (match mtb1.typ_strength with
- None -> eval_struct env mtb1.typ_expr,
- eval_struct env mtb2.typ_expr
- | Some mp -> strengthen env mtb1.typ_expr mp,
- eval_struct env mtb2.typ_expr) in
- let rec check_structure env str1 str2 equiv =
- match str1, str2 with
- | SEBstruct (msid1,list1),
- SEBstruct (msid2,list2) ->
- check_signatures env
- (msid1,list1) mtb1.typ_alias (msid2,list2);
- if equiv then
- check_signatures env
- (msid2,list2) mtb2.typ_alias (msid1,list1)
- | SEBfunctor (arg_id1,arg_t1,body_t1),
+and check_modtypes env mtb1 mtb2 subst1 subst2 equiv =
+ if mtb1==mtb2 then () else
+ let mtb1',mtb2'=mtb1.typ_expr,mtb2.typ_expr in
+ let rec check_structure env str1 str2 equiv subst1 subst2 =
+ match str1,str2 with
+ | SEBstruct (list1),
+ SEBstruct (list2) ->
+ check_signatures env
+ mtb1.typ_mp list1 list2 subst1 subst2;
+ if equiv then
+ check_signatures env
+ mtb2.typ_mp list2 list1 subst1 subst2
+ else
+ ()
+ | SEBfunctor (arg_id1,arg_t1,body_t1),
SEBfunctor (arg_id2,arg_t2,body_t2) ->
- check_modtypes env arg_t2 arg_t1 equiv;
+ check_modtypes env
+ arg_t2 arg_t1
+ (map_mp arg_t1.typ_mp arg_t2.typ_mp) subst2
+ equiv ;
(* contravariant *)
- let env =
- add_module (MPbound arg_id2) (module_body_of_type arg_t2) env
+ let env = add_module
+ (module_body_of_type (MPbound arg_id2) arg_t2) env
in
- let body_t1' =
- (* since we are just checking well-typedness we do not need
- to expand any constant. Hence the identity resolver. *)
- subst_struct_expr
- (map_mbid arg_id1 (MPbound arg_id2))
- body_t1
+ let env = match body_t1 with
+ SEBstruct str ->
+ add_module {mod_mp = mtb1.typ_mp;
+ mod_expr = None;
+ mod_type = body_t1;
+ mod_type_alg= None;
+ mod_constraints=mtb1.typ_constraints;
+ mod_retroknowledge = [];
+ mod_delta = mtb1.typ_delta} env
+ | _ -> env
in
- check_structure env (eval_struct env body_t1')
- (eval_struct env body_t2) equiv
+ check_structure env body_t1 body_t2 equiv
+ (join (map_mbid arg_id1 (MPbound arg_id2)) subst1)
+ subst2
| _ , _ -> error_incompatible_modtypes mtb1 mtb2
- in
+ in
if mtb1'== mtb2' then ()
- else check_structure env mtb1' mtb2' equiv
+ else check_structure env mtb1' mtb2' equiv subst1 subst2
-let check_subtypes env sup super =
+let check_subtypes env sup super =
(*if sup<>super then*)
- check_modtypes env sup super false
-
-let check_equal env sup super =
+ let env = add_module
+ (module_body_of_type sup.typ_mp sup) env in
+ check_modtypes env (strengthen env sup sup.typ_mp) super empty_subst
+ (map_mp super.typ_mp sup.typ_mp) false
+
+let check_equal env sup super =
(*if sup<>super then*)
- check_modtypes env sup super true
+ check_modtypes env sup super empty_subst
+ (map_mp super.typ_mp sup.typ_mp) true
diff --git a/checker/term.ml b/checker/term.ml
index f245d155..be70b864 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -28,7 +28,7 @@ type metavariable = int
type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle |
RegularStyle
type case_printing =
- { ind_nargs : int; (* number of real args of the inductive type *)
+ { ind_nargs : int; (* length of the arity of the inductive type *)
style : case_style }
type case_info =
{ ci_ind : inductive;
@@ -81,7 +81,7 @@ let val_fix f =
[|val_tuple"fix2"[|val_array val_int;val_int|];val_prec f|]
let val_cofix f = val_tuple"pcofixpoint"[|val_int;val_prec f|]
-type cast_kind = VMcast | DEFAULTcast
+type cast_kind = VMcast | DEFAULTcast
let val_cast = val_enum "cast_kind" 2
(*s*******************************************************************)
@@ -116,7 +116,7 @@ let val_constr = val_rec_sum "constr" 0 (fun val_constr -> [|
[|val_name;val_constr;val_constr|]; (* Lambda *)
[|val_name;val_constr;val_constr;val_constr|]; (* LetIn *)
[|val_constr;val_array val_constr|]; (* App *)
- [|val_kn|]; (* Const *)
+ [|val_con|]; (* Const *)
[|val_ind|]; (* Ind *)
[|val_cstr|]; (* Construct *)
[|val_ci;val_constr;val_constr;val_array val_constr|]; (* Case *)
@@ -135,7 +135,7 @@ let rec strip_outer_cast c = match c with
| _ -> c
let rec collapse_appl c = match c with
- | App (f,cl) ->
+ | App (f,cl) ->
let rec collapse_rec f cl2 =
match (strip_outer_cast f) with
| App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
@@ -171,7 +171,7 @@ let iter_constr_with_binders g f n c = match c with
| App (c,l) -> f n c; Array.iter (f n) l
| Evar (_,l) -> Array.iter (f n) l
| Case (_,p,c,bl) -> f n p; f n c; Array.iter (f n) bl
- | Fix (_,(_,tl,bl)) ->
+ | Fix (_,(_,tl,bl)) ->
Array.iter (f n) tl;
Array.iter (f (iterate g (Array.length tl) n)) bl
| CoFix (_,(_,tl,bl)) ->
@@ -183,11 +183,11 @@ exception LocalOccur
(* (closedn n M) raises FreeVar if a variable of height greater than n
occurs in M, returns () otherwise *)
-let closedn n c =
+let closedn n c =
let rec closed_rec n c = match c with
| Rel m -> if m>n then raise LocalOccur
| _ -> iter_constr_with_binders succ closed_rec n c
- in
+ in
try closed_rec n c; true with LocalOccur -> false
(* [closed0 M] is true iff [M] is a (deBruijn) closed term *)
@@ -196,21 +196,21 @@ let closed0 = closedn 0
(* (noccurn n M) returns true iff (Rel n) does NOT occur in term M *)
-let noccurn n term =
+let noccurn n term =
let rec occur_rec n c = match c with
| Rel m -> if m = n then raise LocalOccur
| _ -> iter_constr_with_binders succ occur_rec n c
- in
+ in
try occur_rec n term; true with LocalOccur -> false
-(* (noccur_between n m M) returns true iff (Rel p) does NOT occur in term M
+(* (noccur_between n m M) returns true iff (Rel p) does NOT occur in term M
for n <= p < n+m *)
-let noccur_between n m term =
+let noccur_between n m term =
let rec occur_rec n c = match c with
| Rel(p) -> if n<=p && p<n+m then raise LocalOccur
| _ -> iter_constr_with_binders succ occur_rec n c
- in
+ in
try occur_rec n term; true with LocalOccur -> false
(* Checking function for terms containing existential variables.
@@ -220,7 +220,7 @@ let noccur_between n m term =
which may contain the CoFix variables. These occurrences of CoFix variables
are not considered *)
-let noccur_with_meta n m term =
+let noccur_with_meta n m term =
let rec occur_rec n c = match c with
| Rel p -> if n<=p & p<n+m then raise LocalOccur
| App(f,cl) ->
@@ -261,18 +261,18 @@ let rec exliftn el c = match c with
(* Lifting the binding depth across k bindings *)
-let liftn k n =
+let liftn k n =
match el_liftn (pred n) (el_shft k ELID) with
| ELID -> (fun c -> c)
| el -> exliftn el
-
+
let lift k = liftn k 1
(*********************)
(* Substituting *)
(*********************)
-(* (subst1 M c) substitutes M for Rel(1) in c
+(* (subst1 M c) substitutes M for Rel(1) in c
we generalise it to (substl [M1,...,Mn] c) which substitutes in parallel
M1,...,Mn for respectively Rel(1),...,Rel(n) in c *)
@@ -291,15 +291,15 @@ let rec lift_substituend depth s =
let make_substituend c = { sinfo=Unknown; sit=c }
let substn_many lamv n c =
- let lv = Array.length lamv in
+ let lv = Array.length lamv in
if lv = 0 then c
- else
+ else
let rec substrec depth c = match c with
| Rel k ->
if k<=depth then c
else if k-depth <= lv then lift_substituend depth lamv.(k-depth-1)
else Rel (k-lv)
- | _ -> map_constr_with_binders succ substrec depth c in
+ | _ -> map_constr_with_binders succ substrec depth c in
substrec n c
let substnl laml n =
@@ -362,7 +362,7 @@ let extended_rel_list n hyps =
| (_,None,_) :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps
| (_,Some _,_) :: hyps -> reln l (p+1) hyps
| [] -> l
- in
+ in
reln [] 1 hyps
(* Iterate lambda abstractions *)
@@ -372,17 +372,17 @@ let compose_lam l b =
let rec lamrec = function
| ([], b) -> b
| ((v,t)::l, b) -> lamrec (l, Lambda (v,t,b))
- in
+ in
lamrec (l,b)
(* Transforms a lambda term [x1:T1]..[xn:Tn]T into the pair
([(xn,Tn);...;(x1,T1)],T), where T is not a lambda *)
-let decompose_lam =
+let decompose_lam =
let rec lamdec_rec l c = match c with
| Lambda (x,t,c) -> lamdec_rec ((x,t)::l) c
| Cast (c,_,_) -> lamdec_rec l c
| _ -> l,c
- in
+ in
lamdec_rec []
(* Decompose lambda abstractions and lets, until finding n
@@ -390,15 +390,15 @@ let decompose_lam =
let decompose_lam_n_assum n =
if n < 0 then
error "decompose_lam_n_assum: integer parameter must be positive";
- let rec lamdec_rec l n c =
- if n=0 then l,c
- else match c with
+ let rec lamdec_rec l n c =
+ if n=0 then l,c
+ else match c with
| Lambda (x,t,c) -> lamdec_rec ((x,None,t) :: l) (n-1) c
| LetIn (x,b,t,c) -> lamdec_rec ((x,Some b,t) :: l) n c
| Cast (c,_,_) -> lamdec_rec l n c
| c -> error "decompose_lam_n_assum: not enough abstractions"
- in
- lamdec_rec empty_rel_context n
+ in
+ lamdec_rec empty_rel_context n
(* Iterate products, with or without lets *)
@@ -410,27 +410,27 @@ let mkProd_or_LetIn (na,body,t) c =
let it_mkProd_or_LetIn = List.fold_left (fun c d -> mkProd_or_LetIn d c)
-let decompose_prod_assum =
+let decompose_prod_assum =
let rec prodec_rec l c =
match c with
| Prod (x,t,c) -> prodec_rec ((x,None,t) :: l) c
| LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t) :: l) c
| Cast (c,_,_) -> prodec_rec l c
| _ -> l,c
- in
+ in
prodec_rec empty_rel_context
let decompose_prod_n_assum n =
if n < 0 then
error "decompose_prod_n_assum: integer parameter must be positive";
- let rec prodec_rec l n c =
+ let rec prodec_rec l n c =
if n=0 then l,c
- else match c with
+ else match c with
| Prod (x,t,c) -> prodec_rec ((x,None,t) :: l) (n-1) c
| LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t) :: l) (n-1) c
| Cast (c,_,_) -> prodec_rec l n c
| c -> error "decompose_prod_n_assum: not enough assumptions"
- in
+ in
prodec_rec empty_rel_context n
@@ -443,7 +443,7 @@ let val_arity = val_tuple"arity"[|val_rctxt;val_constr|]
let mkArity (sign,s) = it_mkProd_or_LetIn (Sort s) sign
-let destArity =
+let destArity =
let rec prodec_rec l c =
match c with
| Prod (x,t,c) -> prodec_rec ((x,None,t)::l) c
@@ -451,7 +451,7 @@ let destArity =
| Cast (c,_,_) -> prodec_rec l c
| Sort s -> l,s
| _ -> anomaly "destArity: not an arity"
- in
+ in
prodec_rec []
let rec isArity c =
@@ -463,7 +463,7 @@ let rec isArity c =
| _ -> false
(*******************************)
-(* alpha conversion functions *)
+(* alpha conversion functions *)
(*******************************)
(* alpha conversion : ignore print names and casts *)
@@ -483,15 +483,15 @@ let compare_constr f t1 t2 =
if Array.length l1 = Array.length l2 then
f c1 c2 & array_for_all2 f l1 l2
else
- let (h1,l1) = decompose_app t1 in
+ let (h1,l1) = decompose_app t1 in
let (h2,l2) = decompose_app t2 in
if List.length l1 = List.length l2 then
f h1 h2 & List.for_all2 f l1 l2
else false
| Evar (e1,l1), Evar (e2,l2) -> e1 = e2 & array_for_all2 f l1 l2
- | Const c1, Const c2 -> c1 = c2
- | Ind c1, Ind c2 -> c1 = c2
- | Construct c1, Construct c2 -> c1 = c2
+ | Const c1, Const c2 -> eq_con_chk c1 c2
+ | Ind c1, Ind c2 -> eq_ind_chk c1 c2
+ | Construct (c1,i1), Construct (c2,i2) -> i1=i2 && eq_ind_chk c1 c2
| Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
f p1 p2 & f c1 c2 & array_for_all2 f bl1 bl2
| Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) ->
@@ -500,7 +500,7 @@ let compare_constr f t1 t2 =
ln1 = ln2 & array_for_all2 f tl1 tl2 & array_for_all2 f bl1 bl2
| _ -> false
-let rec eq_constr m n =
+let rec eq_constr m n =
(m==n) or
compare_constr eq_constr m n
diff --git a/checker/type_errors.ml b/checker/type_errors.ml
index a96bba6a..7c014105 100644
--- a/checker/type_errors.ml
+++ b/checker/type_errors.ml
@@ -81,10 +81,10 @@ let error_assumption env j =
let error_reference_variables env id =
raise (TypeError (env, ReferenceVariables id))
-let error_elim_arity env ind aritylst c pj okinds =
+let error_elim_arity env ind aritylst c pj okinds =
raise (TypeError (env, ElimArity (ind,aritylst,c,pj,okinds)))
-let error_case_not_inductive env j =
+let error_case_not_inductive env j =
raise (TypeError (env, CaseNotInductive j))
let error_number_branches env cj expn =
diff --git a/checker/type_errors.mli b/checker/type_errors.mli
index 2d8f8ff2..0482f2f2 100644
--- a/checker/type_errors.mli
+++ b/checker/type_errors.mli
@@ -73,11 +73,11 @@ val error_unbound_var : env -> variable -> 'a
val error_not_type : env -> unsafe_judgment -> 'a
val error_assumption : env -> unsafe_judgment -> 'a
-
+
val error_reference_variables : env -> constr -> 'a
-val error_elim_arity :
- env -> inductive -> sorts_family list -> constr -> unsafe_judgment ->
+val error_elim_arity :
+ env -> inductive -> sorts_family list -> constr -> unsafe_judgment ->
(sorts_family * sorts_family * arity_error) option -> 'a
val error_case_not_inductive : env -> unsafe_judgment -> 'a
@@ -90,11 +90,11 @@ val error_generalization : env -> name * constr -> unsafe_judgment -> 'a
val error_actual_type : env -> unsafe_judgment -> constr -> 'a
-val error_cant_apply_not_functional :
+val error_cant_apply_not_functional :
env -> unsafe_judgment -> unsafe_judgment array -> 'a
-val error_cant_apply_bad_type :
- env -> int * constr * constr ->
+val error_cant_apply_bad_type :
+ env -> int * constr * constr ->
unsafe_judgment -> unsafe_judgment array -> 'a
val error_ill_formed_rec_body :
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 1832ebec..e5cf6a6d 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -21,9 +21,9 @@ open Environ
let inductive_of_constructor = fst
let conv_leq_vecti env v1 v2 =
- array_fold_left2_i
+ array_fold_left2_i
(fun i _ t1 t2 ->
- (try conv_leq env t1 t2
+ (try conv_leq env t1 t2
with NotConvertible -> raise (NotConvertibleVect i)); ())
()
v1
@@ -57,18 +57,18 @@ let judge_of_prop = Sort (Type type1_univ)
let judge_of_type u = Sort (Type (super u))
(*s Type of a de Bruijn index. *)
-
-let judge_of_relative env n =
+
+let judge_of_relative env n =
try
let (_,_,typ) = lookup_rel n env in
lift n typ
- with Not_found ->
+ with Not_found ->
error_unbound_rel env n
(* Type of variables *)
let judge_of_variable env id =
try named_type id env
- with Not_found ->
+ with Not_found ->
error_unbound_var env id
(* Management of context of variables. *)
@@ -115,7 +115,7 @@ let extract_context_levels env =
let make_polymorphic_if_arity env t =
let params, ccl = dest_prod_assum env t in
match ccl with
- | Sort (Type u) ->
+ | 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)
@@ -141,10 +141,10 @@ let type_of_constant env cst =
let judge_of_constant_knowing_parameters env cst paramstyp =
let c = Const cst in
let cb =
- try lookup_constant cst env
+ try lookup_constant cst env
with Not_found ->
failwith ("Cannot find constant: "^string_of_con cst) in
- let _ = check_args env c cb.const_hyps in
+ let _ = check_args env c cb.const_hyps in
type_of_constant_knowing_parameters env cb.const_type paramstyp
let judge_of_constant env cst =
@@ -159,19 +159,19 @@ let judge_of_apply env (f,funj) argjv =
(match whd_betadeltaiota env typ with
| Prod (_,c1,c2) ->
(try conv_leq env hj c1
- with NotConvertible ->
+ with NotConvertible ->
error_cant_apply_bad_type env (n,c1, hj) (f,funj) argjv);
apply_rec (n+1) (subst1 h c2) restjl
| _ ->
error_cant_apply_not_functional env (f,funj) argjv)
- in
+ in
apply_rec 1 funj (Array.to_list argjv)
(* Type of product *)
let sort_of_product env domsort rangsort =
match (domsort, rangsort) with
- (* Product rule (s,Prop,Prop) *)
+ (* Product rule (s,Prop,Prop) *)
| (_, Prop Null) -> rangsort
(* Product rule (Prop/Set,Set,Set) *)
| (Prop _, Prop Pos) -> rangsort
@@ -187,7 +187,7 @@ let sort_of_product env domsort rangsort =
| (Prop Pos, Type u2) -> Type (sup type0_univ u2)
(* Product rule (Prop,Type_i,Type_i) *)
| (Prop Null, Type _) -> rangsort
- (* Product rule (Type_i,Type_i,Type_i) *)
+ (* Product rule (Type_i,Type_i,Type_i) *)
| (Type u1, Type u2) -> Type (sup u1 u2)
(* Type of a type cast *)
@@ -204,7 +204,7 @@ let judge_of_cast env (c,cj) k tj =
match k with
| VMcast -> vm_conv CUMUL
| DEFAULTcast -> conv_leq in
- try
+ try
conversion env cj tj
with NotConvertible ->
error_actual_type env (c,cj) tj
@@ -228,7 +228,7 @@ let judge_of_inductive_knowing_parameters env ind (paramstyp:constr array) =
let (mib,mip) =
try lookup_mind_specif env ind
with Not_found ->
- failwith ("Cannot find inductive: "^string_of_kn (fst ind)) in
+ failwith ("Cannot find inductive: "^string_of_mind (fst ind)) in
check_args env c mib.mind_hyps;
type_of_inductive_knowing_parameters env mip paramstyp
@@ -241,17 +241,17 @@ let judge_of_constructor env c =
let constr = Construct c in
let _ =
let ((kn,_),_) = c in
- let mib =
+ let mib =
try lookup_mind kn env
with Not_found ->
- failwith ("Cannot find inductive: "^string_of_kn (fst (fst c))) in
- check_args env constr mib.mind_hyps in
+ failwith ("Cannot find inductive: "^string_of_mind (fst (fst c))) in
+ check_args env constr mib.mind_hyps in
let specif = lookup_mind_specif env (inductive_of_constructor c) in
type_of_constructor c specif
(* Case. *)
-let check_branch_types env (c,cj) (lfj,explft) =
+let check_branch_types env (c,cj) (lfj,explft) =
try conv_leq_vecti env lfj explft
with
NotConvertibleVect i ->
@@ -321,22 +321,22 @@ let rec execute env cstr =
| Ind ind ->
(* Sort-polymorphism of inductive types *)
judge_of_inductive_knowing_parameters env ind jl
- | Const cst ->
+ | Const cst ->
(* Sort-polymorphism of constant *)
judge_of_constant_knowing_parameters env cst jl
- | _ ->
+ | _ ->
(* No sort-polymorphism *)
execute env f
in
let jl = array_map2 (fun c ty -> c,ty) args jl in
judge_of_apply env (f,j) jl
-
- | Lambda (name,c1,c2) ->
+
+ | Lambda (name,c1,c2) ->
let _ = execute_type env c1 in
let env1 = push_rel (name,None,c1) env in
- let j' = execute env1 c2 in
+ let j' = execute env1 c2 in
Prod(name,c1,j')
-
+
| Prod (name,c1,c2) ->
let varj = execute_type env c1 in
let env1 = push_rel (name,None,c1) env in
@@ -354,7 +354,7 @@ let rec execute env cstr =
let env1 = push_rel (name,Some c1,c2) env in
let j' = execute env1 c3 in
subst1 c1 j'
-
+
| Cast (c,k,t) ->
let cj = execute env c in
let _ = execute_type env t in
@@ -371,13 +371,13 @@ let rec execute env cstr =
let pj = execute env p in
let lfj = execute_array env lf in
judge_of_case env ci (p,pj) (c,cj) lfj
-
+
| Fix ((_,i as vni),recdef) ->
let fix_ty = execute_recdef env recdef i in
let fix = (vni,recdef) in
check_fix env fix;
fix_ty
-
+
| CoFix (i,recdef) ->
let fix_ty = execute_recdef env recdef i in
let cofix = (i,recdef) in
@@ -391,10 +391,10 @@ let rec execute env cstr =
| Evar _ ->
anomaly "the kernel does not support existential variables"
-and execute_type env constr =
+and execute_type env constr =
let j = execute env constr in
snd (type_judgment env (constr,j))
-
+
and execute_recdef env (names,lar,vdef) i =
let larj = execute_array env lar in
let larj = array_map2 (fun c ty -> c,ty) lar larj in
@@ -406,7 +406,7 @@ and execute_recdef env (names,lar,vdef) i =
and execute_array env = Array.map (execute env)
-and execute_list env = List.map (execute env)
+and execute_list env = List.map (execute env)
(* Derived functions *)
let infer env constr = execute env constr
@@ -418,7 +418,7 @@ let infer_v env cv = execute_array env cv
let check_ctxt env rels =
fold_rel_context (fun d env ->
match d with
- (_,None,ty) ->
+ (_,None,ty) ->
let _ = infer_type env ty in
push_rel d env
| (_,Some bd,ty) ->
@@ -436,7 +436,7 @@ let check_named_ctxt env ctxt =
failwith ("variable "^string_of_id id^" defined twice")
with Not_found -> () in
match d with
- (_,None,ty) ->
+ (_,None,ty) ->
let _ = infer_type env ty in
push_named d env
| (_,Some bd,ty) ->
diff --git a/checker/validate.ml b/checker/validate.ml
index 804bf7df..ab17aa7f 100644
--- a/checker/validate.ml
+++ b/checker/validate.ml
@@ -41,6 +41,8 @@ let pr_obj o = pr_obj_rec o; Format.print_newline()
exception ValidObjError of string * Obj.t
let fail o s = raise (ValidObjError(s,o))
+let ep s1 f s2 = f (s1^"/"^s2)
+
let apply debug f x =
let o = Obj.repr x in
try f o
@@ -49,7 +51,7 @@ let apply debug f x =
print_endline ("Validation failed: "^msg);
pr_obj obj
end;
- failwith "validation failed"
+ failwith "vo structure validation failed"
(* data not validated *)
let no_val (o:Obj.t) = ()
@@ -71,8 +73,7 @@ let val_block s o =
let val_tuple s v o =
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
+ if Obj.size o = n then Array.iteri (fun i f -> f (Obj.field o i)) v
else
fail o ("tuple:" ^s^" size found:"^string_of_int (Obj.size o))
@@ -88,7 +89,7 @@ let val_sum s cc vv 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^": max is "^string_of_int i))
+ else fail o ("bad tag in (sum type) "^s^": found "^string_of_int i))
else if Obj.is_int o then
let (n:int) = Obj.magic o in
(if n<0 || n>=cc then
@@ -161,11 +162,14 @@ let val_uid = val_tuple "uniq_ident" [|val_int;val_str;val_dp|]
let val_mp =
val_rec_sum "module_path" 0
- (fun vmp -> [|[|val_dp|];[|val_uid|];[|val_uid|];[|vmp;val_id|]|])
+ (fun vmp -> [|[|val_dp|];[|val_uid|];[|vmp;val_id|]|])
let val_kn = val_tuple "kernel_name" [|val_mp;val_dp;val_id|]
-let val_ind = val_tuple "inductive"[|val_kn;val_int|]
+let val_con =
+ val_tuple "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|]
(* univ *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-02 08:20:44 +0000