aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/check.ml34
-rw-r--r--checker/check_stat.ml4
-rw-r--r--checker/checker.ml80
-rw-r--r--checker/closure.ml36
-rw-r--r--checker/closure.mli4
-rw-r--r--checker/declarations.ml170
-rw-r--r--checker/declarations.mli24
-rw-r--r--checker/environ.ml50
-rw-r--r--checker/indtypes.ml100
-rw-r--r--checker/inductive.ml146
-rw-r--r--checker/mod_checking.ml78
-rw-r--r--checker/modops.ml128
-rw-r--r--checker/modops.mli10
-rw-r--r--checker/reduction.ml40
-rw-r--r--checker/reduction.mli2
-rw-r--r--checker/safe_typing.ml24
-rw-r--r--checker/subtyping.ml102
-rw-r--r--checker/term.ml72
-rw-r--r--checker/type_errors.ml4
-rw-r--r--checker/type_errors.mli12
-rw-r--r--checker/typeops.ml62
21 files changed, 591 insertions, 591 deletions
diff --git a/checker/check.ml b/checker/check.ml
index 82df62b4c..0a75f0137 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) =
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index 6ea153a3a..290e6ff8e 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();
@@ -37,7 +37,7 @@ let cst_filter f csts =
(fun c ce acc -> if f c ce then c::acc else acc)
csts []
-let is_ax _ cb = cb.const_body = None
+let is_ax _ cb = 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 85ad129c9..1df187328 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"
@@ -108,20 +108,20 @@ let init_load_path () =
let user_contrib = coqlib/"user-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 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);
@@ -156,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"
@@ -173,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
@@ -184,7 +184,7 @@ let print_usage_channel co command =
-boot boot mode
-o print the list of assumptions
-m print the maximum heap size
-
+
-impredicative-set set sort Set impredicative
-h, --help print this list of options
@@ -210,9 +210,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^"\""
@@ -221,41 +221,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 -> "=")
@@ -263,12 +263,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
@@ -279,9 +279,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 ++
@@ -291,13 +291,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 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
@@ -318,7 +318,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
@@ -340,7 +340,7 @@ let parse_args() =
in
try
parse (List.tl (Array.to_list Sys.argv))
- with
+ with
| UserError(_,s) as e -> begin
try
Stream.empty s; exit 1
@@ -370,12 +370,12 @@ let init() =
end
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 591b353db..b55c5848e 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)
@@ -417,8 +417,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 +456,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
@@ -504,7 +504,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
@@ -512,7 +512,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 ->
@@ -775,7 +775,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)
*)
@@ -968,7 +968,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 fa302de64..260d159b3 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
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 8cbc964f4..0066e7848 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -30,15 +30,15 @@ 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 =
+ MSI of mod_self_id
| MBI of mod_bound_id
| MPI of module_path
let val_subst_dom =
val_sum "substitution_domain" 0 [|[|val_uid|];[|val_uid|];[|val_mp|]|]
-module Umap = Map.Make(struct
+module Umap = Map.Make(struct
type t = substitution_domain
let compare = Pervasives.compare
end)
@@ -79,7 +79,7 @@ let map_mp mp1 mp2 = add_mp mp1 mp2 empty_subst
let subst_mp0 sub mp = (* 's like subst *)
let rec aux mp =
match mp with
- | MPself sid ->
+ | MPself sid ->
let mp',resolve = Umap.find (MSI sid) sub in
mp',resolve
| MPbound bid ->
@@ -87,17 +87,17 @@ let subst_mp0 sub mp = (* 's like subst *)
mp',resolve
| 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
@@ -148,84 +148,84 @@ let subst_con0 sub con =
let con' = make_con mp' dir l in
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 =
+let subst_mps sub =
map_kn (subst_kn0 sub) (subst_con0 sub)
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)
@@ -240,18 +240,18 @@ let replace_mp_in_con mpfrom mpto kn =
type 'a lazy_subst =
| LSval of 'a
| LSlazy of substitution * 'a
-
+
type 'a substituted = 'a lazy_subst ref
-
+
let from_val a = ref (LSval a)
-
-let force fsubst r =
+
+let force fsubst r =
match !r with
| LSval a -> a
- | LSlazy(s,a) ->
+ | LSlazy(s,a) ->
let a' = fsubst s a in
r := LSval a';
- a'
+ a'
@@ -265,9 +265,9 @@ let join (subst1 : substitution) (subst2 : substitution) =
let subst_key subst1 subst2 =
let replace_in_key key mp sub=
- let newkey =
+ let newkey =
match key with
- | MPI mp1 ->
+ | MPI mp1 ->
begin
match subst_mp0 subst1 mp1 with
| None -> None
@@ -283,24 +283,24 @@ let subst_key subst1 subst2 =
let update_subst_alias subst1 subst2 =
let subst_inv key (mp,_) sub =
- let newmp =
- match key with
+ 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
+ | 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
+ in
let subst_mbi = Umap.fold subst_inv subst2 empty_subst in
let alias_subst key (mp,_) sub=
- let newkey =
+ let newkey =
match key with
- | MPI mp1 ->
+ | MPI mp1 ->
begin
match subst_mp0 subst_mbi mp1 with
| None -> None
@@ -319,28 +319,28 @@ let join_alias (subst1 : substitution) (subst2 : substitution) =
match subst_mp0 sub mp with
None -> mp,None
| Some mp' -> mp',None in
- Umap.mapi (apply_subst subst2) subst1
+ Umap.mapi (apply_subst subst2) subst1
let update_subst subst1 subst2 =
let subst_inv key (mp,_) l =
- let newmp =
- match key with
+ let newmp =
+ match key with
| MBI msid -> MPbound msid
| MSI msid -> MPself msid
| MPI mp -> mp
in
- match mp with
+ match mp with
| MPbound mbid -> ((MBI mbid),newmp)::l
| MPself msid -> ((MSI msid),newmp)::l
| _ -> ((MPI mp),newmp)::l
- in
+ in
let subst_mbi = Umap.fold subst_inv subst2 [] in
let alias_subst key (mp,_) sub=
- let newsetkey =
+ let newsetkey =
match key with
- | MPI mp1 ->
- let compute_set_newkey l (k,mp') =
+ | MPI mp1 ->
+ let compute_set_newkey l (k,mp') =
let mp_from_key = match k with
| MBI msid -> MPbound msid
| MSI msid -> MPself msid
@@ -358,7 +358,7 @@ let update_subst subst1 subst2 =
in
match newsetkey with
| None -> sub
- | Some l ->
+ | Some l ->
List.fold_left (fun s k -> Umap.add k (mp,None) s)
sub l
in
@@ -372,7 +372,7 @@ let subst_substituted s r =
let s'' = join s' s in
ref (LSlazy(s'',a))
-let force_constr = force subst_mps
+let force_constr = force subst_mps
type constr_substituted = constr substituted
@@ -390,7 +390,7 @@ 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"
@@ -405,9 +405,9 @@ 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 *)|]
@@ -419,7 +419,7 @@ let subst_recarg sub r = match r with
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 +454,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
@@ -509,7 +509,7 @@ 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"
@@ -568,7 +568,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 ->
@@ -578,7 +578,7 @@ 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;
@@ -589,20 +589,20 @@ let subst_mind_packet sub mbp =
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 ;
@@ -612,7 +612,7 @@ let subst_mind sub mib =
(* 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
@@ -623,7 +623,7 @@ 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
+ | 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
@@ -633,15 +633,15 @@ and with_declaration_body =
With_module_body of identifier list * module_path *
struct_expr_body option * Univ.constraints
| With_definition_body of identifier list * constant_body
-
-and module_body =
+
+and module_body =
{ mod_expr : struct_expr_body option;
mod_type : struct_expr_body option;
mod_constraints : Univ.constraints;
mod_alias : substitution;
mod_retroknowledge : action list}
-and module_type_body =
+and module_type_body =
{ typ_expr : struct_expr_body;
typ_strength : module_path option;
typ_alias : substitution}
@@ -670,7 +670,7 @@ and val_module o = val_tuple "module_body"
and val_modtype o = val_tuple "module_type_body"
[|val_seb;val_opt val_mp;val_subst|] o
-
+
let rec subst_with_body sub = function
| With_module_body(id,mp,typ_opt,cst) ->
With_module_body(id,subst_mp sub mp,
@@ -683,18 +683,18 @@ and subst_modtype sub mtb =
if typ_expr'==mtb.typ_expr then
mtb
else
- { mtb with
+ { mtb with
typ_expr = typ_expr'}
-
-and subst_structure sub sign =
+
+and subst_structure sub sign =
let subst_body = function
- SFBconst cb ->
+ SFBconst cb ->
SFBconst (subst_const_body sub cb)
- | SFBmind mib ->
+ | SFBmind mib ->
SFBmind (subst_mind sub mib)
- | SFBmodule mb ->
+ | SFBmodule mb ->
SFBmodule (subst_module sub mb)
- | SFBmodtype mtb ->
+ | SFBmodtype mtb ->
SFBmodtype (subst_modtype sub mtb)
| SFBalias (mp,typ_opt ,cst) ->
SFBalias (subst_mp sub mp,
@@ -710,11 +710,11 @@ and subst_module sub mb =
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'
+ if mtb'==mb.mod_type && mb.mod_expr == me'
&& mb_alias == mb.mod_alias
then mb else
{ mod_expr = me';
- mod_type=mtb';
+ mod_type=mtb';
mod_constraints=mb.mod_constraints;
mod_alias = mb_alias;
mod_retroknowledge=mb.mod_retroknowledge}
@@ -722,7 +722,7 @@ and subst_module sub mb =
and subst_struct_expr sub = function
| SEBident mp -> SEBident (subst_mp sub mp)
- | SEBfunctor (msid, mtb, meb') ->
+ | SEBfunctor (msid, mtb, meb') ->
SEBfunctor(msid,subst_modtype sub mtb,subst_struct_expr sub meb')
| SEBstruct (msid,str)->
SEBstruct(msid, subst_structure sub str)
@@ -730,10 +730,10 @@ and subst_struct_expr sub = function
SEBapply(subst_struct_expr sub meb1,
subst_struct_expr sub meb2,
cst)
- | SEBwith (meb,wdb)->
+ | SEBwith (meb,wdb)->
SEBwith(subst_struct_expr sub meb,
subst_with_body sub wdb)
-
-let subst_signature_msid msid mp =
+
+let subst_signature_msid msid mp =
subst_structure (map_msid msid mp)
diff --git a/checker/declarations.mli b/checker/declarations.mli
index c5b676bda..3d061b4c2 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
@@ -109,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 = {
@@ -149,7 +149,7 @@ type mutual_inductive_body = {
type substitution
-type structure_field_body =
+type structure_field_body =
| SFBconst of constant_body
| SFBmind of mutual_inductive_body
| SFBmodule of module_body
@@ -160,7 +160,7 @@ 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
+ | 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
@@ -170,15 +170,15 @@ and with_declaration_body =
With_module_body of identifier list * module_path *
struct_expr_body option * Univ.constraints
| With_definition_body of identifier list * constant_body
-
-and module_body =
+
+and module_body =
{ mod_expr : struct_expr_body option;
mod_type : struct_expr_body option;
mod_constraints : Univ.constraints;
mod_alias : substitution;
mod_retroknowledge : action list}
-and module_type_body =
+and module_type_body =
{ typ_expr : struct_expr_body;
typ_strength : module_path option;
typ_alias : substitution}
diff --git a/checker/environ.ml b/checker/environ.ml
index 4bdbeee66..2d5ff3e43 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -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,11 +98,11 @@ 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 *)
@@ -111,17 +111,17 @@ let lookup_constant kn env =
Cmap.find kn env.env_globals.env_constants
let add_constant kn cs env =
- let new_constants =
+ 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_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
@@ -147,15 +147,15 @@ let evaluable_constant cst env =
let lookup_mind kn env =
KNmap.find kn env.env_globals.env_inductives
-let rec scrape_mind env kn =
+let rec scrape_mind env kn =
match (lookup_mind kn env).mind_equiv with
| None -> kn
| Some kn' -> scrape_mind env kn'
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
+ let new_globals =
+ { env.env_globals with
env_inductives = new_inds } in
{ env with env_globals = new_globals }
@@ -168,36 +168,36 @@ let rec mind_equiv env (kn1,i1) (kn2,i2) =
(* 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
+ let new_globals =
+ { env.env_globals with
env_alias = new_alias } in
{ env with env_globals = new_globals }
-let rec scrape_alias mp env =
+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/indtypes.ml b/checker/indtypes.ml
index 9ff21bc3f..3d4f6be79 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -119,17 +119,17 @@ 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
@@ -278,20 +278,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 =
@@ -312,7 +312,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
@@ -324,18 +324,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."
@@ -352,14 +352,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
@@ -367,7 +367,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)
@@ -377,7 +377,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 *)
@@ -389,7 +389,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) ->
@@ -400,7 +400,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
| _ -> ());
@@ -413,9 +413,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)
@@ -424,14 +424,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
@@ -440,30 +440,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
@@ -482,7 +482,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
@@ -505,9 +505,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
diff --git a/checker/inductive.ml b/checker/inductive.ml
index f1c8bea2a..e08efbe5b 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 =
@@ -258,12 +258,12 @@ 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
let build_dependent_inductive ind (_,mip) params =
let realargs,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
- applist
+ applist
(Ind ind,
List.map (lift mip.mind_nrealargs_ctxt) params
@ extended_rel_list 0 realargs)
@@ -272,11 +272,11 @@ let build_dependent_inductive ind (_,mip) params =
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
@@ -287,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;
@@ -299,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
@@ -336,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
@@ -361,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 *)
@@ -419,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 *)
@@ -443,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 }
@@ -455,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
@@ -465,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 }
@@ -504,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
@@ -521,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);
@@ -534,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) ->
@@ -549,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
@@ -572,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
@@ -586,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
@@ -598,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
@@ -626,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
@@ -672,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
@@ -686,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
@@ -699,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))
@@ -708,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
@@ -759,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
@@ -771,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))
@@ -822,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 *)
@@ -840,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)
@@ -858,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))
@@ -887,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 9e7a23363..99babe632 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,9 +58,9 @@ 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'
@@ -70,7 +70,7 @@ 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 +81,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
@@ -136,21 +136,21 @@ let lookup_modtype mp env =
failwith ("Unknown module type: "^string_of_mp mp)
-let rec check_with env mtb with_decl =
+let rec check_with env mtb with_decl =
match with_decl with
- | With_definition_body _ ->
+ | With_definition_body _ ->
check_with_aux_def env mtb with_decl;
empty_subst
- | With_module_body _ ->
+ | With_module_body _ ->
check_with_aux_mod env mtb with_decl
-and check_with_aux_def env mtb with_decl =
- let msid,sig_b = match (eval_struct env mtb) with
+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
| _ -> error_signature_expected mtb
in
- let id,idl = match with_decl with
+ 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
@@ -162,11 +162,11 @@ and check_with_aux_def env mtb with_decl =
let env' = Modops.add_signature (MPself msid) before 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
@@ -180,7 +180,7 @@ and check_with_aux_def env mtb with_decl =
With_definition_body (_,c) ->
With_definition_body (idl,c)
| With_module_body (_,c,t,cst) ->
- With_module_body (idl,c,t,cst) in
+ With_module_body (idl,c,t,cst) in
check_with_aux_def env' (type_of_mb env old) new_with_decl
| Some msb ->
error_a_generative_module_expected l
@@ -190,14 +190,14 @@ 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 =
+and check_with_aux_mod env mtb with_decl =
let initmsid,msid,sig_b =
- match eval_struct env mtb with
+ 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)
| _ -> error_signature_expected mtb in
- let id,idl = match with_decl with
+ 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
@@ -209,7 +209,7 @@ and check_with_aux_mod env mtb with_decl =
let rec mp_rec = function
| [] -> MPself initmsid
| i::r -> MPdot(mp_rec r,label_of_id i)
- in
+ in
let env' = Modops.add_signature (MPself msid) before env in
match with_decl with
| With_module_body ([],_,_,_) -> assert false
@@ -229,7 +229,7 @@ and check_with_aux_mod env mtb with_decl =
anomaly "Mod_typing:no implementation and no alias"
in
join (map_mp (mp_rec [id]) mp) mtb'.typ_alias
- | With_module_body (_::_,mp,_,_) ->
+ | With_module_body (_::_,mp,_,_) ->
let old = match spec with
SFBmodule msb -> msb
| _ -> error_not_a_module l
@@ -238,12 +238,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'
+ check_with_aux_mod env'
(type_of_mb env old) new_with_decl in
join (map_mp (mp_rec idl) mp) sub
| Some msb ->
@@ -263,15 +263,15 @@ and check_module_type env mty =
and check_module env mb =
let sub =
match mb.mod_expr, mb.mod_type with
- | None, None ->
+ | None, None ->
anomaly "Mod_typing.translate_module: empty type and expr in module entry"
| None, Some mtb -> check_modexpr env mtb
- | Some mexpr, _ ->
+ | Some mexpr, _ ->
let sub1 = check_modexpr env mexpr in
(match mb.mod_type with
| None -> sub1
- | Some mte ->
+ | Some mte ->
let sub2 = check_modexpr env mte in
check_subtypes env
{typ_expr = mexpr;
@@ -333,8 +333,8 @@ and check_modexpr env mse = match mse with
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
+ | SEBstruct (msid,sign) ->
+ join_alias
(subst_key (map_msid msid mp) mtb.typ_alias)
(map_msid msid mp)
| _ -> mtb.typ_alias in
@@ -356,12 +356,12 @@ and check_modexpr env mse = match mse with
let rec add_struct_expr_constraints env = function
| SEBident _ -> env
- | SEBfunctor (_,mtb,meb) ->
- add_struct_expr_constraints
+ | 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 +369,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 +390,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 498bd7753..a986e1898 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"
@@ -38,7 +38,7 @@ let error_no_such_label_sub l l1 l2 =
error (l1^" is not a subtype of "^l2^".\nThe field "^
string_of_label l^" is missing (or invisible) 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
@@ -57,7 +57,7 @@ let error_signature_expected mtb =
let error_application_to_not_path _ = error "Application to not path"
-let module_body_of_type mtb =
+let module_body_of_type mtb =
{ mod_type = Some mtb.typ_expr;
mod_expr = None;
mod_constraints = Constraint.empty;
@@ -65,12 +65,12 @@ let module_body_of_type mtb =
mod_retroknowledge = []}
let module_type_of_module mp mb =
- {typ_expr =
+ {typ_expr =
(match mb.mod_type with
| Some expr -> expr
| None -> (match mb.mod_expr with
| Some expr -> expr
- | None ->
+ | None ->
anomaly "Modops: empty expr and type"));
typ_alias = mb.mod_alias;
typ_strength = mp
@@ -95,24 +95,24 @@ let destr_functor env mtb =
| _ -> error_not_a_functor mtb
-let rec check_modpath_equiv env mp1 mp2 =
+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
+ else
error_not_equal mp1 mp2
-let strengthen_const env mp l cb =
+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
+ | true, Some _
+ | _, None ->
+ let const = Const (make_con mp empty_dirpath l) in
let const_subs = Some (Declarations.from_val const) in
- {cb with
+ {cb with
const_body = const_subs;
const_opaque = false
}
@@ -122,8 +122,8 @@ let strengthen_mind env mp l mib = match mib.mind_equiv with
| None -> {mib with mind_equiv = Some (make_kn mp empty_dirpath l)}
-let rec eval_struct env = function
- | SEBident mp ->
+let rec eval_struct env = function
+ | SEBident mp ->
begin
let mp = scrape_alias mp env in
let mtb =lookup_modtype mp env in
@@ -131,7 +131,7 @@ let rec eval_struct env = function
mtb,None -> eval_struct env mtb
| mtb,Some mp -> strengthen_mtb env mp (eval_struct env mtb)
end
- | SEBapply (seb1,seb2,_) ->
+ | 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
@@ -140,9 +140,9 @@ let rec eval_struct env = function
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
+ let sub_alias = update_subst_alias sub_alias
(map_mbid farg_id mp) in
- eval_struct env (subst_struct_expr
+ 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
@@ -150,24 +150,24 @@ let rec eval_struct env = function
let alias_in_mp =
(lookup_modtype mp env).typ_alias in
merge_with env mtb wdb alias_in_mp
-(* | SEBfunctor(mbid,mtb,body) ->
+(* | 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
+ | _,_ -> 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
+ 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
@@ -178,35 +178,35 @@ and merge_with env mtb with_decl alias=
let rec mp_rec = function
| [] -> MPself msid
| i::r -> MPdot(mp_rec r,label_of_id i)
- in
+ in
let new_spec,subst = match with_decl with
| With_definition_body ([],_)
| With_module_body ([],_,_,_) -> assert false
- | With_definition_body ([id],c) ->
+ | 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 (_::_,_,_,_) ->
+ | 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 =
+ 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 (idc,mp,t,cst) ->
With_module_body (idl,mp,t,cst),
- Some(map_mp (mp_rec idc) mp)
+ Some(map_mp (mp_rec idc) mp)
in
let subst = Option.fold_right join subst1 alias in
- let modtype =
+ 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_type = Some modtype;
mod_constraints = old.mod_constraints;
mod_alias = subst;
mod_retroknowledge = old.mod_retroknowledge}
@@ -218,35 +218,35 @@ and merge_with env mtb with_decl alias=
with
Not_found -> error_no_such_label l
-and add_signature mp sign env =
+and add_signature mp sign 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
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
+ | SFBmodule mb ->
+ add_module (MPdot (mp,l)) mb env
(* adds components as well *)
- | SFBalias (mp1,_,cst) ->
+ | SFBalias (mp1,_,cst) ->
Environ.register_alias (MPdot(mp,l)) mp1 env
- | SFBmodtype mtb -> Environ.add_modtype (MPdot(mp,l))
+ | SFBmodtype mtb -> Environ.add_modtype (MPdot(mp,l))
mtb env
in
List.fold_left add_one env sign
-and add_module mp mb env =
+and add_module mp mb env =
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) ->
+ | SEBstruct (msid,sign) ->
add_signature mp (subst_signature_msid msid mp sign) env
| SEBfunctor _ -> env
| _ -> anomaly "Modops:the evaluation of the structure failed "
-
+
and constants_of_specification env mp sign =
@@ -255,30 +255,30 @@ and constants_of_specification env mp sign =
| 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
+ 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
+ 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
+ | 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.
+ 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
+ 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
+ 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)
@@ -290,23 +290,23 @@ and constants_of_modtype env mp modtype =
(subst_signature_msid msid mp sign)
| SEBfunctor _ -> []
| _ -> anomaly "Modops:the evaluation of the structure failed "
-
+
and strengthen_mtb env mp mtb =
- let mtb1 = eval_struct env mtb in
+ let mtb1 = eval_struct env mtb in
match mtb1 with
| SEBfunctor _ -> mtb1
- | SEBstruct (msid,sign) ->
+ | SEBstruct (msid,sign) ->
SEBstruct (msid,strengthen_sig env msid sign mp)
| _ -> anomaly "Modops:the evaluation of the structure failed "
-and strengthen_mod env mp mb =
+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 ->
@@ -320,7 +320,7 @@ and strengthen_sig env msid sign mp = match sign with
| (l,SFBmodule mb) :: rest ->
let mp' = MPdot (mp,l) in
let item' = l,SFBmodule (strengthen_mod env mp' mb) in
- let env' = add_module
+ let env' = add_module
(MPdot (MPself msid,l)) mb env in
let rest' = strengthen_sig env' msid rest mp in
item':: rest'
@@ -328,21 +328,21 @@ and strengthen_sig env msid sign mp = match sign with
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))
+ | (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 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
+ | SEBstruct(msid,str) -> false, join_alias
(subst_key (map_msid msid mp) mb.mod_alias)
(map_msid msid mp)
| _ -> true, mb.mod_alias
diff --git a/checker/modops.mli b/checker/modops.mli
index 17b063e2a..d5c9f4de6 100644
--- a/checker/modops.mli
+++ b/checker/modops.mli
@@ -22,10 +22,10 @@ open Environ
(* make the environment entry out of type *)
val module_body_of_type : module_type_body -> module_body
-val module_type_of_module : module_path option -> module_body ->
- module_type_body
+val module_type_of_module : 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 *)
@@ -47,7 +47,7 @@ val strengthen : env -> struct_expr_body -> module_path -> struct_expr_body
val update_subst : env -> module_body -> module_path -> bool * substitution
-val error_incompatible_modtypes :
+val error_incompatible_modtypes :
module_type_body -> module_type_body -> 'a
val error_not_match : label -> structure_field_body -> 'a
@@ -63,7 +63,7 @@ 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 d81cfe352..612e7562f 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
@@ -148,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 =
@@ -211,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) *)
@@ -233,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) ->
@@ -281,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);
@@ -327,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
@@ -350,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
@@ -377,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));
())
@@ -391,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 *)
(********************************************************************)
@@ -413,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
@@ -426,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 47590edb3..81c93ee53 100644
--- a/checker/reduction.mli
+++ b/checker/reduction.mli
@@ -37,7 +37,7 @@ 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. *)
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index f4ffb302c..b0d683ff3 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -58,7 +58,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
@@ -72,21 +72,21 @@ let rec lighten_module mb =
mod_expr = Option.map lighten_modexpr mb.mod_expr;
mod_type = Option.map 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
| 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
@@ -95,17 +95,17 @@ and lighten_modexpr = function
| 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,7 +119,7 @@ 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
@@ -132,7 +132,7 @@ let import file (dp,mb,depends,engmt as vo) digest =
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) digest =
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 edf119c66..88989b32e 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -19,14 +19,14 @@ 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
@@ -37,11 +37,11 @@ type namedobject =
(* 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,8 +54,8 @@ 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)
@@ -74,11 +74,11 @@ 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 check_inductive env msid1 l info1 mib2 spec2 =
let kn = make_kn (MPself msid1) 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 ()
@@ -87,7 +87,7 @@ let check_inductive env msid1 l info1 mib2 spec2 =
(* 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,10 +155,10 @@ 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
@@ -168,17 +168,17 @@ let check_inductive env msid1 l info1 mib2 spec2 =
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 msid1 l info1 cb2 spec2 =
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
@@ -283,32 +283,32 @@ let rec check_modules env msid1 l msb1 msb2 =
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
-
-and check_signatures env (msid1,sig1) alias (msid2,sig2') =
+
+and check_signatures env (msid1,sig1) alias (msid2,sig2') =
let mp1 = MPself msid1 in
- let env = add_signature mp1 sig1 env 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
let map1 = make_label_map mp1 sig1 in
- let check_one_body (l,spec2) =
- let info1 =
- try
- Labmap.find l map1
- with
+ let check_one_body (l,spec2) =
+ let info1 =
+ try
+ Labmap.find l map1
+ with
Not_found -> error_no_such_label_sub l msid1 msid2
in
match spec2 with
| SFBconst cb2 ->
check_constant env msid1 l info1 cb2 spec2
- | SFBmind mib2 ->
+ | SFBmind mib2 ->
check_inductive env msid1 l info1 mib2 spec2
- | SFBmodule msb2 ->
+ | SFBmodule msb2 ->
begin
match info1 with
| Module msb -> check_modules env msid1 l msb msb2
- | Alias (mp,typ_opt) ->let msb =
+ | Alias (mp,typ_opt) ->let msb =
{mod_expr = Some (SEBident mp);
mod_type = typ_opt;
mod_constraints = Constraint.empty;
@@ -318,11 +318,11 @@ and check_signatures env (msid1,sig1) alias (msid2,sig2') =
| _ -> error_not_match l spec2
end
| SFBalias (mp,typ_opt,_) ->
- begin
+ begin
match info1 with
| Alias (mp1,_) -> check_modpath_equiv env mp mp1
- | Module msb ->
- let msb1 =
+ | Module msb ->
+ let msb1 =
{mod_expr = Some (SEBident mp);
mod_type = typ_opt;
mod_constraints = Constraint.empty;
@@ -332,7 +332,7 @@ and check_signatures env (msid1,sig1) alias (msid2,sig2') =
| _ -> error_not_match l spec2
end
| SFBmodtype mtb2 ->
- let mtb1 =
+ let mtb1 =
match info1 with
| Modtype mtb -> mtb
| _ -> error_not_match l spec2
@@ -341,7 +341,7 @@ and check_signatures env (msid1,sig1) alias (msid2,sig2') =
in
List.iter check_one_body sig2
-and check_modtypes env mtb1 mtb2 equiv =
+and check_modtypes env mtb1 mtb2 equiv =
if mtb1==mtb2 then () else (* just in case :) *)
let mtb1',mtb2'=
(match mtb1.typ_strength with
@@ -349,23 +349,23 @@ and check_modtypes env mtb1 mtb2 equiv =
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 =
+ let rec check_structure env str1 str2 equiv =
match str1, str2 with
- | SEBstruct (msid1,list1),
- SEBstruct (msid2,list2) ->
+ | 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),
+ check_signatures env
+ (msid2,list2) mtb2.typ_alias (msid1,list1)
+ | SEBfunctor (arg_id1,arg_t1,body_t1),
SEBfunctor (arg_id2,arg_t2,body_t2) ->
check_modtypes env arg_t2 arg_t1 equiv;
(* contravariant *)
- let env =
- add_module (MPbound arg_id2) (module_body_of_type arg_t2) env
+ let env =
+ add_module (MPbound arg_id2) (module_body_of_type arg_t2) env
in
- let body_t1' =
+ 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
@@ -375,14 +375,14 @@ and check_modtypes env mtb1 mtb2 equiv =
check_structure env (eval_struct env body_t1')
(eval_struct env body_t2) equiv
| _ , _ -> error_incompatible_modtypes mtb1 mtb2
- in
+ in
if mtb1'== mtb2' then ()
else check_structure env mtb1' mtb2' equiv
-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 check_equal env sup super =
(*if sup<>super then*)
check_modtypes env sup super true
diff --git a/checker/term.ml b/checker/term.ml
index f5b2496c8..92d898b31 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -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*******************************************************************)
@@ -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,7 +483,7 @@ 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
@@ -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 a96bba6a4..7c0141055 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 2d8f8ff22..0482f2f2a 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 1832ebec4..3a4f2f825 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
@@ -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
+ 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) ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 01:21:59 +0000