aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/abstraction.ml18
-rw-r--r--kernel/abstraction.mli1
-rw-r--r--kernel/closure.ml8
-rw-r--r--kernel/closure.mli2
-rw-r--r--kernel/environ.ml9
-rw-r--r--kernel/himsg.ml161
-rw-r--r--kernel/mach.ml4
-rw-r--r--kernel/mach.mli2
-rw-r--r--kernel/machops.ml25
-rw-r--r--kernel/machops.mli5
-rw-r--r--kernel/printer.mli16
-rw-r--r--kernel/reduction.ml11
-rw-r--r--kernel/sign.ml4
-rw-r--r--kernel/sosub.ml219
-rw-r--r--kernel/sosub.mli8
-rw-r--r--kernel/type_errors.ml72
-rw-r--r--kernel/type_errors.mli (renamed from kernel/himsg.mli)33
-rw-r--r--kernel/univ.ml368
-rw-r--r--kernel/univ.mli8
19 files changed, 744 insertions, 230 deletions
diff --git a/kernel/abstraction.ml b/kernel/abstraction.ml
new file mode 100644
index 000000000..e0b86dbf2
--- /dev/null
+++ b/kernel/abstraction.ml
@@ -0,0 +1,18 @@
+
+(* $Id$ *)
+
+open Util
+open Names
+open Generic
+open Term
+
+type abstraction_body = {
+ abs_kind : path_kind;
+ abs_arity : int array;
+ abs_rhs : constr }
+
+let contract_abstraction ab args =
+ if array_for_all2 (fun c i -> (count_dlam c) = i) args ab.abs_arity then
+ Sosub.soexecute (Array.fold_left sAPP ab.abs_rhs args)
+ else
+ failwith "contract_abstraction"
diff --git a/kernel/abstraction.mli b/kernel/abstraction.mli
index 5d71a1319..98fd86089 100644
--- a/kernel/abstraction.mli
+++ b/kernel/abstraction.mli
@@ -9,3 +9,4 @@ type abstraction_body = {
abs_arity : int array;
abs_rhs : constr }
+val contract_abstraction : abstraction_body -> constr array -> constr
diff --git a/kernel/closure.ml b/kernel/closure.ml
index f84b231d1..49be8a1a5 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -652,14 +652,6 @@ type fconstr = sorts oper freeze
let inject constr = freeze ESID constr
-(* trivial printer: prints the equivalent constr of a freeze,
- * just writing a "*" if it is in normal form
- *)
-let prfconstr v =
- let pv = Printer.pr_term (term_of_freeze v) in
- if v.norm then [< 'sTR"*"; pv >] else pv
-
-
(* Remove head lifts, applications and casts *)
let rec strip_frterm n v stack =
match v.term with
diff --git a/kernel/closure.mli b/kernel/closure.mli
index fb7431e4e..b64f2794b 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -139,8 +139,6 @@ val contract_subst : int -> 'a freeze -> 'a freeze -> 'a freeze
(* Calculus of Constructions *)
type fconstr = sorts oper freeze
val inject : constr -> fconstr
-(* A pseudo-printer for fconstr *)
-val prfconstr : fconstr -> std_ppcmds
val strip_frterm :
int -> fconstr -> fconstr array list -> int * fconstr * fconstr array
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 7086432ac..e84d8f296 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -156,13 +156,8 @@ let translucent_abst env = function
let abst_value env = function
| DOPN(Abst sp, args) ->
- let ab = lookup_abst sp env in
- if array_for_all2 (fun c i -> (count_dlam c) = i) args ab.abs_arity then
- (* Sosub.soexecute (Array.fold_left sAPP ab.abs_rhs args) *)
- failwith "todo: abstractions"
- else
- failwith "contract_abstraction"
- | _ -> invalid_arg "contract_abstraction"
+ contract_abstraction (lookup_abst sp env) args
+ | _ -> invalid_arg "abst_value"
let defined_constant env = function
| DOPN (Const sp, _) ->
diff --git a/kernel/himsg.ml b/kernel/himsg.ml
deleted file mode 100644
index 94ef46258..000000000
--- a/kernel/himsg.ml
+++ /dev/null
@@ -1,161 +0,0 @@
-
-(* $Id$ *)
-
-open Pp
-open Util
-open Printer
-open Generic
-open Term
-open Sign
-open Environ
-open Reduction
-
-let error_unbound_rel k env n =
- let ctx = context env in
- let pe = pr_ne_env [< 'sTR"in environment" >] k ctx in
- errorlabstrm "unbound rel"
- [< 'sTR"Unbound reference: "; pe; 'fNL;
- 'sTR"The reference "; 'iNT n; 'sTR" is free" >]
-
-let error_cant_execute k env c =
- let tc = gen_pr_term k env c in
- errorlabstrm "Cannot execute"
- [< 'sTR"Cannot execute term:"; 'bRK(1,1); tc >]
-
-let error_not_type k env c =
- let ctx = context env in
- let pe = pr_ne_env [< 'sTR"In environment" >] k ctx in
- let pc = gen_pr_term k env c in
- errorlabstrm "Not a type"
- [< pe; 'cUT; 'sTR "the term"; 'bRK(1,1); pc; 'sPC;
- 'sTR"should be typed by Set, Prop or Type." >];;
-
-let error_assumption k env c =
- let pc = gen_pr_term k env c in
- errorlabstrm "Bad assumption"
- [< 'sTR "Cannot declare a variable or hypothesis over the term";
- 'bRK(1,1); pc; 'sPC; 'sTR "because this term is not a type." >];;
-
-let error_reference_variables id =
- errorlabstrm "construct_reference"
- [< 'sTR "the constant"; 'sPC; pr_id id; 'sPC;
- 'sTR "refers to variables which are not in the context" >]
-
-let error_elim_expln env kp ki=
- if is_info_sort env kp && not (is_info_sort env ki) then
- "non-informative objects may not construct informative ones."
- else
- match (kp,ki) with
- | (DOP0(Sort (Type _)), DOP0(Sort (Prop _))) ->
- "strong elimination on non-small inductive types leads to paradoxes."
- | _ -> "wrong arity"
-
-let msg_bad_elimination env k = function
- | Some(ki,kp,explanation) ->
- let pki = gen_pr_term k env ki in
- let pkp = gen_pr_term k env kp in
- (hOV 0
- [< 'fNL; 'sTR "Elimination of an inductive object of sort : ";
- pki; 'bRK(1,0);
- 'sTR "is not allowed on a predicate in sort : "; pkp ;'fNL;
- 'sTR "because"; 'sPC; 'sTR explanation >])
- | None -> [<>]
-
-let error_elim_arity k env ind aritylst c p pt okinds =
- let pi = gen_pr_term k env ind in
- let ppar = prlist_with_sep pr_coma (gen_pr_term k env) aritylst in
- let pc = gen_pr_term k env c in
- let pp = gen_pr_term k env p in
- let ppt = gen_pr_term k env pt in
- errorlabstrm "incorrect elimimnation arity"
- [< 'sTR "Incorrect elimination of"; 'bRK(1,1); pc; 'sPC;
- 'sTR "in the inductive type"; 'bRK(1,1); pi; 'fNL;
- 'sTR "The elimination predicate"; 'bRK(1,1); pp; 'sPC;
- 'sTR "has type"; 'bRK(1,1); ppt; 'fNL;
- 'sTR "It should be one of :"; 'bRK(1,1) ; hOV 0 ppar; 'fNL;
- msg_bad_elimination env k okinds >]
-
-let error_case_not_inductive k env c ct =
- let pc = gen_pr_term k env c in
- let pct = gen_pr_term k env ct in
- errorlabstrm "Cases on non inductive type"
- [< 'sTR "In Cases expression"; 'bRK(1,1); pc; 'sPC;
- 'sTR "has type"; 'bRK(1,1); pct; 'sPC;
- 'sTR "which is not an inductive definition" >]
-
-let error_number_branches k env c ct expn =
- let pc = gen_pr_term k env c in
- let pct = gen_pr_term k env ct in
- errorlabstrm "Cases with wrong number of cases"
- [< 'sTR "Cases on term"; 'bRK(1,1); pc; 'sPC ;
- 'sTR "of type"; 'bRK(1,1); pct; 'sPC;
- 'sTR "expects "; 'iNT expn; 'sTR " branches" >]
-
-let error_ill_formed_branch k env c i actty expty =
- let pc = gen_pr_term k env c in
- let pa = gen_pr_term k env actty in
- let pe = gen_pr_term k env expty in
- errorlabstrm "Ill-formed branches"
- [< 'sTR "In Cases expression on term"; 'bRK(1,1); pc;
- 'sPC; 'sTR "the branch " ; 'iNT (i+1);
- 'sTR " has type"; 'bRK(1,1); pa ; 'sPC;
- 'sTR "which should be:"; 'bRK(1,1); pe >]
-
-let error_generalization k env (name,var) c =
- let pe = pr_ne_env [< 'sTR"in environment" >] k (context env) in
- let pv = gen_pr_term k env var.body in
- let pc = gen_pr_term k (push_rel (name,var) env) c in
- errorlabstrm "gen_rel"
- [< 'sTR"Illegal generalization: "; pe; 'fNL;
- 'sTR"Cannot generalize"; 'bRK(1,1); pv; 'sPC;
- 'sTR"over"; 'bRK(1,1); pc; 'sPC;
- 'sTR"which should be typed by Set, Prop or Type." >]
-
-let error_actual_type k env cj tj =
- let pe = pr_ne_env [< 'sTR"In environment" >] k (context env) in
- let pc = gen_pr_term k env cj.uj_val in
- let pct = gen_pr_term k env cj.uj_type in
- let pt = gen_pr_term k env tj.uj_val in
- errorlabstrm "Bad cast"
- [< pe; 'fNL;
- 'sTR"The term"; 'bRK(1,1); pc ; 'sPC ;
- 'sTR"does not have type"; 'bRK(1,1); pt; 'fNL;
- 'sTR"Actually, it has type" ; 'bRK(1,1); pct >]
-
-let error_cant_apply s k env rator randl =
- let pe = pr_ne_env [< 'sTR"in environment" >] k (context env) in
- let pr = gen_pr_term k env rator.uj_val in
- let prt = gen_pr_term k env rator.uj_type in
- let term_string = if List.length randl > 1 then "terms" else "term" in
- let appl =
- prlist_with_sep pr_fnl
- (fun c ->
- let pc = gen_pr_term k env c.uj_val in
- let pct = gen_pr_term k env c.uj_type in
- hOV 2 [< pc; 'sPC; 'sTR": " ; pct >]) randl
- in
- errorlabstrm "Illegal application"
- [< 'sTR"Illegal application ("; 'sTR s; 'sTR"): "; pe; 'fNL;
- 'sTR"The term"; 'bRK(1,1); pr; 'sPC;
- 'sTR"of type"; 'bRK(1,1); prt; 'sPC ;
- 'sTR("cannot be applied to the "^term_string); 'fNL;
- 'sTR" "; v 0 appl >]
-
-(* (co)fixpoints *)
-let error_ill_formed_rec_body str k env lna i vdefs =
- let pvd = gen_pr_term k env vdefs.(i) in
- errorlabstrm "Ill-formed rec body"
- [< str; 'fNL; 'sTR"The ";
- if Array.length vdefs = 1 then [<>] else [<'iNT (i+1); 'sTR "-th ">];
- 'sTR"recursive definition"; 'sPC ; pvd; 'sPC;
- 'sTR "is not well-formed" >]
-
-let error_ill_typed_rec_body k env i lna vdefj vargs =
- let pvd = gen_pr_term k env (vdefj.(i)).uj_val in
- let pvdt = gen_pr_term k env (vdefj.(i)).uj_type in
- let pv = gen_pr_term k env (body_of_type vargs.(i)) in
- errorlabstrm "Ill-typed rec body"
- [< 'sTR"The " ;
- if Array.length vdefj = 1 then [<>] else [<'iNT (i+1); 'sTR "-th">];
- 'sTR"recursive definition" ; 'sPC; pvd; 'sPC;
- 'sTR "has type"; 'sPC; pvdt;'sPC; 'sTR "it should be"; 'sPC; pv >]
diff --git a/kernel/mach.ml b/kernel/mach.ml
index c2817f5bf..2311fb999 100644
--- a/kernel/mach.ml
+++ b/kernel/mach.ml
@@ -7,10 +7,10 @@ open Names
open Univ
open Generic
open Term
-open Himsg
open Reduction
open Sign
open Environ
+open Type_errors
open Machops
(* Fonctions temporaires pour relier la forme castée de la forme jugement *)
@@ -232,6 +232,8 @@ let unsafe_type_of_type env c =
(*s Machines with information. *)
+type information = Logic | Inf of unsafe_judgment
+
(*i
let implicit_judgment = {body=mkImplicit;typ=implicit_sort}
diff --git a/kernel/mach.mli b/kernel/mach.mli
index fbf1a3ef7..9e37c4c79 100644
--- a/kernel/mach.mli
+++ b/kernel/mach.mli
@@ -30,6 +30,8 @@ val unsafe_type_of : 'a unsafe_env -> constr -> constr
(*s Machine with information. *)
+type information = Logic | Inf of unsafe_judgment
+
(*i
val infexemeta :
'a unsafe_env -> constr -> unsafe_judgment * information * universes
diff --git a/kernel/machops.ml b/kernel/machops.ml
index afeb7f3fa..23bac0b27 100644
--- a/kernel/machops.ml
+++ b/kernel/machops.ml
@@ -14,9 +14,7 @@ open Sign
open Environ
open Reduction
open Instantiate
-open Himsg
-
-type information = Logic | Inf of unsafe_judgment
+open Type_errors
let make_judge v tj =
{ uj_val = v;
@@ -82,12 +80,12 @@ let construct_reference id env hyps =
if hyps_inclusion env hyps hyps' then
Array.of_list (List.map (fun id -> VAR id) (ids_of_sign hyps))
else
- error_reference_variables id
+ error_reference_variables CCI env id
let check_hyps id env hyps =
let hyps' = get_globals (context env) in
if not (hyps_inclusion env hyps hyps') then
- error_reference_variables id
+ error_reference_variables CCI env id
(* Instantiation of terms on real arguments. *)
@@ -195,6 +193,15 @@ let make_arity_nodep env k =
in
mrec
+let error_elim_expln env kp ki =
+ if is_info_sort env kp && not (is_info_sort env ki) then
+ "non-informative objects may not construct informative ones."
+ else
+ match (kp,ki) with
+ | (DOP0(Sort (Type _)), DOP0(Sort (Prop _))) ->
+ "strong elimination on non-small inductive types leads to paradoxes."
+ | _ -> "wrong arity"
+
exception Arity of (constr * constr * string) option
let is_correct_arity env kd kn (c,p) =
@@ -419,9 +426,9 @@ let apply_rel_list env0 nocheck argjl funj =
let env' = set_universes g env in
apply_rec env' (subst1 hj.uj_val c2) restjl
| NotConvertible ->
- error_cant_apply "Type Error" CCI env funj argjl)
+ error_cant_apply CCI env "Type Error" funj argjl)
| _ ->
- error_cant_apply "Non-functional construction" CCI env funj argjl
+ error_cant_apply CCI env "Non-functional construction" funj argjl
in
apply_rec env0 funj.uj_type argjl
@@ -729,7 +736,7 @@ let check_fix env = function
try
let _ = check_subterm_rec_meta env nvect nvect.(i) vdefs.(i) in ()
with UserError (s,str) ->
- error_ill_formed_rec_body str CCI env lna i vdefs
+ error_ill_formed_rec_body CCI env str lna i vdefs
in
for i = 0 to ln-1 do check_type i done
@@ -873,7 +880,7 @@ let check_cofix env f =
(try
let _ = check_guard_rec_meta env nbfix vdefs.(i) varit.(i) in ()
with UserError (s,str) ->
- error_ill_formed_rec_body str CCI env lna i vdefs)
+ error_ill_formed_rec_body CCI env str lna i vdefs)
in
for i = 0 to nbfix-1 do check_type i done
| _ -> assert false
diff --git a/kernel/machops.mli b/kernel/machops.mli
index d0fa5eb5c..1a3b729c2 100644
--- a/kernel/machops.mli
+++ b/kernel/machops.mli
@@ -8,9 +8,8 @@ open Term
open Environ
(*i*)
-(* Typing judgments. *)
-type information = Logic | Inf of unsafe_judgment
+(* Base operations of the typing machine. *)
val make_judge : constr -> typed_type -> unsafe_judgment
@@ -18,8 +17,6 @@ val j_val_only : unsafe_judgment -> constr
val typed_type_of_judgment : 'a unsafe_env -> unsafe_judgment -> typed_type
-(* Base operations of the typing machine. *)
-
val relative : 'a unsafe_env -> int -> unsafe_judgment
val type_of_constant_or_existential : 'a unsafe_env -> constr -> typed_type
diff --git a/kernel/printer.mli b/kernel/printer.mli
deleted file mode 100644
index d9c2336bc..000000000
--- a/kernel/printer.mli
+++ /dev/null
@@ -1,16 +0,0 @@
-
-(* $Id$ *)
-
-open Pp
-open Names
-open Term
-open Sign
-open Environ
-
-val pr_id : identifier -> std_ppcmds
-val pr_sp : section_path -> std_ppcmds
-
-val gen_pr_term : path_kind -> 'a unsafe_env -> constr -> std_ppcmds
-val pr_term : constr -> std_ppcmds
-val pr_ne_env : std_ppcmds -> path_kind -> environment -> std_ppcmds
-
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index f1eb15998..c2309f8ed 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -169,11 +169,8 @@ let subst_term_occ locs c t =
else
let except = List.for_all (fun n -> n<0) locs in
let (nbocc,t') = substcheck except 1 1 c t in
- if List.exists (fun o -> o>=nbocc or o<= -nbocc) locs then
- errorlabstrm "subst_occ"
- [< 'sTR "Only "; 'iNT (nbocc-1); 'sTR " occurrences of";
- 'bRK(1,1); Printer.pr_term c; 'sPC;
- 'sTR "in"; 'bRK(1,1); Printer.pr_term t>]
+ if List.exists (fun o -> o >= nbocc or o <= -nbocc) locs then
+ failwith "subst_term_occ: too few occurences"
else
t'
@@ -752,9 +749,7 @@ type 'a conversion_function =
(* Conversion utility functions *)
let convert_of_constraint f u =
- match f u with
- | Consistent u' -> Convertible u'
- | Inconsistent -> NotConvertible
+ try Convertible (f u) with UniverseInconsistency -> NotConvertible
type conversion_test = universes -> conversion_result
diff --git a/kernel/sign.ml b/kernel/sign.ml
index 661f64042..c0e865812 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -24,7 +24,7 @@ let rev_sign (idl,tyl) = (List.rev idl, List.rev tyl)
let map_sign_typ f (idl,tyl) = (idl, List.map f tyl)
let concat_sign (idl1,tyl1) (idl2,tyl2) = (idl1@idl2, tyl1@tyl2)
let diff_sign (idl1,tyl1) (idl2,tyl2) =
- (subtract idl1 idl2, subtract tyl1 tyl2)
+ (list_subtract idl1 idl2, list_subtract tyl1 tyl2)
let nth_sign (idl,tyl) n = (List.nth idl (n-1), List.nth tyl (n-1))
let map_sign_graph f (ids,tys) = List.map2 f ids tys
@@ -134,7 +134,7 @@ let add_sign_replacing whereid (id,t) sign =
are distinct. *)
let prepend_sign gamma1 gamma2 =
- if [] = intersect (ids_of_sign gamma1) (ids_of_sign gamma2) then
+ if [] = list_intersect (ids_of_sign gamma1) (ids_of_sign gamma2) then
let (ids1,vals1) = gamma1
and (ids2,vals2) = gamma2 in
(ids1@ids2, vals1@vals2)
diff --git a/kernel/sosub.ml b/kernel/sosub.ml
new file mode 100644
index 000000000..e2f269899
--- /dev/null
+++ b/kernel/sosub.ml
@@ -0,0 +1,219 @@
+
+(* $Id$ *)
+
+open Util
+open Names
+open Generic
+open Term
+
+(* Given a term with variables in it, and second-order substitution,
+ this function will apply the substitution. The special
+ operator "XTRA[$SOAPP]" is used to represent the second-order
+ substitution.
+
+ (1) second-order substitutions: $SOAPP(SOLAM;... soargs ...)
+ This operation will take the term SOLAM, which must be
+ of the form [x1][x2]...[xn]B and replace the xi with the
+ soargs. If any of the soargs are variables, then we will
+ rename the binders for these variables to the name of the
+ xi.
+ *)
+
+let list_assign_1 l n e =
+ let rec assrec = function
+ | (1, h::t) -> e :: t
+ | (n, h::t) -> h :: (assrec (n-1,t))
+ | (_, []) -> failwith "list_assign_1"
+ in
+ assrec (n,l)
+
+
+(* [propagate_name spine_map argt new_na]
+ * if new_na is a real name, and argt is a (Rel idx)
+ * then the entry for idx in the spine_map
+ * is replaced with new_na. In any case, a new spine_map is returned.
+ *)
+let propagate_name smap argt new_na =
+ match argt,new_na with
+ | (Rel idx, (Name _ as na)) ->
+ (try list_assign_1 smap idx na with Failure _ -> smap)
+ | (_, _) -> smap
+
+let is_soapp_operator = function
+ | DOPN(XTRA("$SOAPP",[]),cl) -> true
+ | DOP2(XTRA("$SOAPP",[]),_,_) -> true
+ | _ -> false
+
+let dest_soapp_operator = function
+ | DOPN(XTRA("$SOAPP",[]),cl) -> (array_hd cl,array_list_of_tl cl)
+ | DOP2(XTRA("$SOAPP",[]),c1,c2) -> (c1,[c2])
+ | _ -> failwith "dest_soapp_operator"
+
+let solam_names =
+ let rec namrec acc = function
+ | DLAM(na,b) -> namrec (na::acc) b
+ | _ -> List.rev acc
+ in
+ namrec []
+
+let do_propsoapp smap (solam,soargs) =
+ let rec propsolam smap solam soargs =
+ match (solam,soargs) with
+ | ((DLAM(na,b)), (arg::argl)) ->
+ propsolam (propagate_name smap arg na) b argl
+ | ((DLAM _), []) -> error "malformed soapp"
+ | (_, (_::_)) -> error "malformed soapp"
+ | (_, []) -> smap
+ in
+ propsolam smap solam soargs
+
+let propsoapp smap t =
+ if is_soapp_operator t then
+ do_propsoapp smap (dest_soapp_operator t)
+ else
+ smap
+
+(* [propagate_names spine_map t]
+ * walks t, looking for second-order applications.
+ * Each time it finds one, it tries to propagate
+ * backwards any names that it can for arguments of
+ * the application which are debruijn references.
+ *)
+let propagate_names =
+ let rec proprec smap t =
+ let (smap,t) =
+ (match t with
+ | DOP0 oper -> (smap,t)
+ | DOP1(op,c) ->
+ let (smap',c') = proprec smap c in
+ (smap',DOP1(op,c'))
+ | DOP2(op,c1,c2) ->
+ let (smap',c1') = proprec smap c1 in
+ let (smap'',c2') = proprec smap c2 in
+ (smap'',DOP2(op,c1',c2'))
+ | DOPN(op,cl) ->
+ let cllist = Array.to_list cl in
+ let (smap',cl'list) =
+ List.fold_right
+ (fun c (smap,acc) ->
+ let (smap',c') = proprec smap c in (smap',c'::acc))
+ cllist (smap,[])
+ in
+ (smap',DOPN(op,Array.of_list cl'list))
+ | DOPL(op,cl) ->
+ let cllist = cl in
+ let (smap',cl'list) =
+ List.fold_right
+ (fun c (smap,acc) ->
+ let (smap',c') = proprec smap c in (smap',c'::acc))
+ cllist (smap,[])
+ in
+ (smap',DOPL(op,cl'list))
+ | DLAM(na,c) ->
+ let (lna', c') = proprec (na::smap) c in
+ (List.tl lna', DLAM(List.hd lna', c'))
+ | DLAMV(na,cl) ->
+ let cllist = Array.to_list cl in
+ let (lna',cl'list) =
+ List.fold_right
+ (fun c (smap,acc) ->
+ let (smap',c') = proprec smap c in (smap',c'::acc))
+ cllist (na::smap,[])
+ in
+ (List.tl lna',DLAMV(List.hd lna',Array.of_list cl'list))
+ | Rel i -> (smap,t)
+ | VAR id -> (smap,t))
+ in
+ (propsoapp smap t,t)
+ in
+ proprec
+
+let socontract =
+ let rec lamrec sigma x y =
+ match x,y with
+ | (h::t, DLAM(_,c)) -> lamrec (h::sigma) t c
+ | ([], t) -> substl sigma t
+ | ((_::_), _) -> error "second-order app with mismatched arguments"
+ in
+ lamrec []
+
+(* [soeval t]
+ * evaluates t, by contracting any second-order redexes
+ *)
+let rec soeval t=
+ match t with
+ | DOP0 _ -> t
+ | Rel _ -> t
+ | VAR _ -> t
+ | DOP1(op,c) -> DOP1(op,soeval c)
+ | DLAM(na,c) -> DLAM(na,soeval c)
+ | DLAMV(na,cl) -> DLAMV(na,Array.map soeval cl)
+ | DOP2(op,c1,c2) ->
+ let c1' = soeval c1
+ and c2' = soeval c2 in
+ if is_soapp_operator t then
+ socontract [c2'] c1'
+ else
+ DOP2(op,c1',c2')
+ | DOPN(op,cl) ->
+ let cl' = Array.map soeval cl in
+ if is_soapp_operator t then
+ let lam = array_hd cl' in
+ let args = Array.to_list (array_tl cl') in
+ socontract args lam
+ else
+ DOPN(op,cl')
+ | DOPL(op,cl) ->
+ let cl' = List.map soeval cl in
+ if is_soapp_operator t then
+ let lam = List.hd cl'
+ and args = List.tl cl' in
+ socontract args lam
+ else
+ DOPL(op,cl')
+
+let rec try_soeval t =
+ match t with
+ | DOP0 _ -> t
+ | Rel _ -> t
+ | VAR _ -> t
+ | DOP1(op,c) -> DOP1(op,try_soeval c)
+ | DLAM(na,c) -> DLAM(na,try_soeval c)
+ | DLAMV(na,cl) -> DLAMV(na,Array.map try_soeval cl)
+ | DOP2(op,c1,c2) ->
+ let c1' = try_soeval c1
+ and c2' = try_soeval c2 in
+ if is_soapp_operator t then
+ (try socontract [c2'] c1'
+ with (Failure _ | UserError _) -> DOP2(op,c1',c2'))
+ else
+ DOP2(op,c1',c2')
+ | DOPN(op,cl) ->
+ let cl' = Array.map try_soeval cl in
+ if is_soapp_operator t then
+ let lam = array_hd cl'
+ and args = Array.to_list (array_tl cl') in
+ (try socontract args lam
+ with (Failure _ | UserError _) -> DOPN(op,cl'))
+ else
+ DOPN(op,cl')
+ | DOPL(op,cl) ->
+ let cl' = List.map try_soeval cl in
+ if is_soapp_operator t then
+ let lam = List.hd cl'
+ and args = List.tl cl' in
+ (try socontract args lam
+ with (Failure _ | UserError _) -> DOPL(op,cl'))
+ else
+ DOPL(op,cl')
+
+let soexecute t =
+ let (_,t) = propagate_names [] t in
+ soeval t
+
+let try_soexecute t =
+ let (_,t) =
+ try propagate_names [] t
+ with (Failure _ | UserError _) -> ([],t)
+ in
+ try_soeval t
diff --git a/kernel/sosub.mli b/kernel/sosub.mli
new file mode 100644
index 000000000..c3093af73
--- /dev/null
+++ b/kernel/sosub.mli
@@ -0,0 +1,8 @@
+
+(* $Id$ *)
+
+open Term
+
+val soexecute : constr -> constr
+val try_soexecute : constr -> constr
+
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
new file mode 100644
index 000000000..6949940a4
--- /dev/null
+++ b/kernel/type_errors.ml
@@ -0,0 +1,72 @@
+
+(* $Id$ *)
+
+open Pp
+open Names
+open Term
+open Sign
+open Environ
+
+(* Type errors. *)
+
+type type_error =
+ | UnboundRel of int
+ | CantExecute of constr
+ | NotAType of constr
+ | BadAssumption of constr
+ | ReferenceVariables of identifier
+ | ElimArity of constr * constr list * constr * constr * constr
+ * (constr * constr * string) option
+ | CaseNotInductive of constr * constr
+ | NumberBranches of constr * constr * int
+ | IllFormedBranch of constr * int * constr * constr
+ | Generalization of (name * typed_type) * constr
+ | ActualType of unsafe_judgment * unsafe_judgment
+ | CantAply of string * unsafe_judgment * unsafe_judgment list
+ | IllFormedRecBody of std_ppcmds * name list * int * constr array
+ | IllTypedRecBody of int * name list * unsafe_judgment array
+ * typed_type array
+
+exception TypeError of path_kind * environment * type_error
+
+let error_unbound_rel k env n =
+ raise (TypeError (k, context env, UnboundRel n))
+
+let error_cant_execute k env c =
+ raise (TypeError (k, context env, CantExecute c))
+
+let error_not_type k env c =
+ raise (TypeError (k, context env, NotAType c))
+
+let error_assumption k env c =
+ raise (TypeError (k, context env, BadAssumption c))
+
+let error_reference_variables k env id =
+ raise (TypeError (k, context env, ReferenceVariables id))
+
+let error_elim_arity k env ind aritylst c p pt okinds =
+ raise (TypeError (k, context env, ElimArity (ind,aritylst,c,p,pt,okinds)))
+
+let error_case_not_inductive k env c ct =
+ raise (TypeError (k, context env, CaseNotInductive (c,ct)))
+
+let error_number_branches k env c ct expn =
+ raise (TypeError (k, context env, NumberBranches (c,ct,expn)))
+
+let error_ill_formed_branch k env c i actty expty =
+ raise (TypeError (k, context env, IllFormedBranch (c,i,actty,expty)))
+
+let error_generalization k env nvar c =
+ raise (TypeError (k, context env, Generalization (nvar,c)))
+
+let error_actual_type k env cj tj =
+ raise (TypeError (k, context env, ActualType (cj,tj)))
+
+let error_cant_apply k env s rator randl =
+ raise (TypeError (k, context env, CantAply (s,rator,randl)))
+
+let error_ill_formed_rec_body k env str lna i vdefs =
+ raise (TypeError (k, context env, IllFormedRecBody (str,lna,i,vdefs)))
+
+let error_ill_typed_rec_body k env i lna vdefj vargs =
+ raise (TypeError (k, context env, IllTypedRecBody (i,lna,vdefj,vargs)))
diff --git a/kernel/himsg.mli b/kernel/type_errors.mli
index 644bfe8be..cec8b7818 100644
--- a/kernel/himsg.mli
+++ b/kernel/type_errors.mli
@@ -1,13 +1,33 @@
(* $Id$ *)
-(*i*)
open Pp
open Names
open Term
open Sign
open Environ
-(*i*)
+
+(* Type errors. *)
+
+type type_error =
+ | UnboundRel of int
+ | CantExecute of constr
+ | NotAType of constr
+ | BadAssumption of constr
+ | ReferenceVariables of identifier
+ | ElimArity of constr * constr list * constr * constr * constr
+ * (constr * constr * string) option
+ | CaseNotInductive of constr * constr
+ | NumberBranches of constr * constr * int
+ | IllFormedBranch of constr * int * constr * constr
+ | Generalization of (name * typed_type) * constr
+ | ActualType of unsafe_judgment * unsafe_judgment
+ | CantAply of string * unsafe_judgment * unsafe_judgment list
+ | IllFormedRecBody of std_ppcmds * name list * int * constr array
+ | IllTypedRecBody of int * name list * unsafe_judgment array
+ * typed_type array
+
+exception TypeError of path_kind * environment * type_error
val error_unbound_rel : path_kind -> 'a unsafe_env -> int -> 'b
@@ -17,9 +37,7 @@ val error_not_type : path_kind -> 'a unsafe_env -> constr -> 'b
val error_assumption : path_kind -> 'a unsafe_env -> constr -> 'b
-val error_reference_variables : identifier -> 'a
-
-val error_elim_expln : 'a unsafe_env -> constr -> constr -> string
+val error_reference_variables : path_kind -> 'a unsafe_env -> identifier -> 'b
val error_elim_arity :
path_kind -> 'a unsafe_env -> constr -> constr list -> constr
@@ -41,14 +59,13 @@ val error_actual_type :
path_kind -> 'a unsafe_env -> unsafe_judgment -> unsafe_judgment -> 'b
val error_cant_apply :
- string -> path_kind -> 'a unsafe_env -> unsafe_judgment
+ path_kind -> 'a unsafe_env -> string -> unsafe_judgment
-> unsafe_judgment list -> 'b
val error_ill_formed_rec_body :
- std_ppcmds -> path_kind -> 'a unsafe_env
+ path_kind -> 'a unsafe_env -> std_ppcmds
-> name list -> int -> constr array -> 'b
val error_ill_typed_rec_body :
path_kind -> 'a unsafe_env -> int -> name list -> unsafe_judgment array
-> typed_type array -> 'b
-
diff --git a/kernel/univ.ml b/kernel/univ.ml
new file mode 100644
index 000000000..a5fa727ec
--- /dev/null
+++ b/kernel/univ.ml
@@ -0,0 +1,368 @@
+
+(* $Id$ *)
+
+(* Universes are stratified by a partial ordering $\ge$.
+ Let $\~{}$ be the associated equivalence. We also have a strict ordering
+ $>$ between equivalence classes, and we maintain that $>$ is acyclic,
+ and contained in $\ge$ in the sense that $[U]>[V]$ implies $U\ge V$.
+
+ At every moment, we have a finite number of universes, and we
+ maintain the ordering in the presence of assertions $U>V$ and $U\ge V$.
+
+ The equivalence $\~{}$ is represented by a tree structure, as in the
+ union-find algorithm. The assertions $>$ and $\ge$ are represented by
+ adjacency lists *)
+
+open Pp
+open Util
+open Names
+
+type universe = { u_sp : section_path; u_num : int }
+
+let universe_ord x y =
+ let c = x.u_num - y.u_num in
+ if c <> 0 then c else sp_ord x.u_sp y.u_sp
+
+module UniverseOrdered = struct
+ type t = universe
+ let compare = universe_ord
+end
+
+let pr_uni u = [< 'sTR(string_of_path u.u_sp) ; 'sTR"." ; 'iNT u.u_num >]
+
+let dummy_sp = make_path ["univ"] (id_of_string "dummy") OBJ
+let dummy_univ = {u_sp = dummy_sp; u_num = 0} (* for prover terms *)
+
+let new_univ =
+ let univ_gen = ref 0 in
+ (fun sp -> incr univ_gen; { u_sp = sp; u_num = !univ_gen })
+
+type relation =
+ | Greater of bool * universe * relation (* if bool then > else >= *)
+ | Equiv of universe
+ | Terminal
+
+module UniverseMap = Map.Make(UniverseOrdered)
+
+type arc = Arc of universe * relation
+
+type universes = arc UniverseMap.t
+
+exception UniverseInconsistency
+
+type constraint_function =
+ universe -> universe -> universes -> universes
+
+(* in Arc(u,Greater(b,v,r))::arcs, we have u>v if b, and u>=v if not b,
+ and r is the next relation pertaining to u; this relation may be
+ Greater or Terminal. *)
+
+let enter_arc a g =
+ let Arc(i,_) = a in
+ UniverseMap.add i a g
+
+let declare_univ u g =
+ if not (UniverseMap.mem u g) then
+ UniverseMap.add u (Arc(u,Terminal)) g
+ else
+ g
+
+(* The universes of Prop and Set: Type_0, Type_1 and Type_2, and the
+ resulting graph. *)
+let (initial_universes,prop_univ,prop_univ_univ,prop_univ_univ_univ) =
+ let prop_sp = make_path ["univ"] (id_of_string "prop_univ") OBJ in
+ let u = { u_sp = prop_sp; u_num = 0 } in
+ let su = { u_sp = prop_sp; u_num = 1 } in
+ let ssu = { u_sp = prop_sp; u_num = 2 } in
+ let g = enter_arc (Arc(u,Terminal)) UniverseMap.empty in
+ let g = enter_arc (Arc(su,Terminal)) g in
+ let g = enter_arc (Arc(ssu,Terminal)) g in
+ let g = enter_arc (Arc(su,Greater(true,u,Terminal))) g in
+ let g = enter_arc (Arc(ssu,Greater(true,su,Terminal))) g in
+ (g,u,su,ssu)
+
+(* Every universe has a unique canonical arc representative *)
+
+(* repr : universes -> universe -> arc *)
+(* canonical representative : we follow the Equiv links *)
+let repr g u =
+ let rec repr_rec u =
+ let arc =
+ try UniverseMap.find u g
+ with Not_found -> anomalylabstrm "Impuniv.repr"
+ [< 'sTR"Universe "; pr_uni u; 'sTR" undefined" >]
+ in
+ match arc with
+ | Arc(_,Equiv(v)) -> repr_rec v
+ | _ -> arc
+ in
+ repr_rec u
+
+let can g = List.map (repr g)
+
+(* transitive closure : we follow the Greater links *)
+(* close : relation -> universe list * universe list *)
+let close =
+ let rec closerec ((u,v) as pair) = function
+ | Terminal -> pair
+ | Greater(true,v_0,r) -> closerec (v_0::u,v) r
+ | Greater(false,v_0,r) -> closerec (u,v_0::v) r
+ | _ -> anomaly "Wrong universe structure"
+ in
+ closerec ([],[])
+
+(* reprgeq : arc -> arc list *)
+(* All canonical arcv such that arcu>=arcc with arcv#arcu *)
+let reprgeq g (Arc(_,ru) as arcu) =
+ let (_,v) = close ru in
+ let rec searchrec w = function
+ | [] -> w
+ | v_0 :: v ->
+ let arcv = repr g v_0 in
+ if List.memq arcv w || arcu=arcv then
+ searchrec w v
+ else
+ searchrec (arcv :: w) v
+ in
+ searchrec [] v
+
+(* collect : arc -> arc list * arc list *)
+(* collect u = (V,W) iff V={v canonical | u>v} W={w canonical | u>=w}-V *)
+(* i.e. collect does the transitive closure of what is known about u *)
+let collect g u =
+ let rec coll_rec v w = function
+ | [],[] -> (v,list_subtractq w v)
+ | (Arc(_,rv) as arcv)::v',w' ->
+ if List.memq arcv v then
+ coll_rec v w (v',w')
+ else
+ let (gt,geq) = close rv in
+ coll_rec (arcv::v) w ((can g (gt@geq))@v',w')
+ | [],(Arc(_,rw) as arcw)::w' ->
+ if (List.memq arcw v) or (List.memq arcw w) then
+ coll_rec v w ([],w')
+ else
+ let (gt,geq) = close rw in
+ coll_rec v (arcw::w) (can g gt, (can g geq)@w')
+ in
+ coll_rec [] [] ([],[u])
+
+type order = EQ | GT | GE | NGE
+
+(* compare : universe -> universe -> order *)
+let compare g u v =
+ let arcu = repr g u
+ and arcv = repr g v in
+ if arcu=arcv then
+ EQ
+ else
+ let (v,w) = collect g arcu in
+ if List.memq arcv v then
+ GT
+ else if List.memq arcv w then
+ GE
+ else
+ NGE
+
+(* Invariants : compare(u,v) = EQ <=> compare(v,u) = EQ
+ compare(u,v) = GT or GE => compare(v,u) = NGE
+ compare(u,v) = NGE => compare(v,u) = NGE or GE or GT
+
+ Adding u>=v is consistent iff compare(v,u) # GT
+ and then it is redundant iff compare(u,v) # NGE
+ Adding u>v is consistent iff compare(v,u) = NGE
+ and then it is redundant iff compare(u,v) = GT *)
+
+(* between : universe -> arc -> arc list *)
+(* we assume compare(u,v) = GE with v canonical *)
+(* between u v = {w|u>=w>=v, w canonical} *)
+let between g u arcv =
+ let rec explore (memo,l) arcu =
+ try
+ memo,list_unionq (List.assq arcu memo) l (* when memq arcu memo *)
+ with Not_found ->
+ let w = reprgeq g arcu in
+ let (memo',sols) = List.fold_left explore (memo,[]) w in
+ let sols' = if sols=[] then [] else arcu::sols in
+ ((arcu,sols')::memo', list_unionq sols' l)
+ in
+ snd (explore ([(arcv,[arcv])],[]) (repr g u))
+
+(* Note: hd(between u v) = repr u *)
+(* between is the most costly operation *)
+
+(* setgt : universe -> universe -> unit *)
+(* forces u > v *)
+let setgt g u v =
+ let Arc(u',ru) = repr g u in
+ enter_arc (Arc(u',Greater(true,v,ru))) g
+
+(* checks that non-redondant *)
+let setgt_if g u v = match compare g u v with
+ | GT -> g
+ | _ -> setgt g u v
+
+(* setgeq : universe -> universe -> unit *)
+(* forces u >= v *)
+let setgeq g u v =
+ let Arc(u',ru) = repr g u in
+ enter_arc (Arc(u',Greater(false,v,ru))) g
+
+
+(* checks that non-redondant *)
+let setgeq_if g u v = match compare g u v with
+ | NGE -> setgeq g u v
+ | _ -> g
+
+(* merge : universe -> universe -> unit *)
+(* we assume compare(u,v) = GE *)
+(* merge u v forces u ~ v with repr u as canonical repr *)
+let merge g u v =
+ match between g u (repr g v) with
+ | Arc(u',_)::v ->
+ let redirect (g,w,w') (Arc(v',rv)) =
+ let v,v'_0 = close rv in
+ let g' = enter_arc (Arc(v',Equiv(u'))) g in
+ (g',list_unionq v w,v'_0@w')
+ in
+ let (g',w,w') = List.fold_left redirect (g,[],[]) v in
+ let g'' = List.fold_left (fun g -> setgt_if g u') g' w in
+ let g''' = List.fold_left (fun g -> setgeq_if g u') g'' w' in
+ g'''
+ | [] -> anomaly "between"
+
+(* merge_disc : universe -> universe -> unit *)
+(* we assume compare(u,v) = compare(v,u) = NGE *)
+(* merge_disc u v forces u ~ v with repr u as canonical repr *)
+let merge_disc g u v =
+ let (Arc(u',_), Arc(v',rv)) = (repr g u, repr g v) in
+ let v,v'_0 = close rv in
+ let g' = enter_arc (Arc(v',Equiv(u'))) g in
+ let g'' = List.fold_left (fun g -> setgt_if g u') g' v in
+ let g''' = List.fold_left (fun g -> setgeq_if g u') g'' v'_0 in
+ g'''
+
+(* Universe inconsistency: error raised when trying to enforce a relation
+ that would create a cycle in the graph of universes. *)
+let error_inconsistency () =
+ raise UniverseInconsistency
+
+(* enforcegeq : universe -> universe -> unit *)
+(* enforcegeq u v will force u>=v if possible, will fail otherwise *)
+let enforce_geq u v g =
+ let g = declare_univ u g in
+ let g = declare_univ v g in
+ match compare g u v with
+ | NGE ->
+ (match compare g v u with
+ | GT -> error_inconsistency()
+ | GE -> merge g v u
+ | NGE -> setgeq g u v
+ | EQ -> anomaly "compare")
+ | _ -> g
+
+(* enforceq : universe -> universe -> unit *)
+(* enforceq u v will force u=v if possible, will fail otherwise *)
+let enforce_eq u v g =
+ let g = declare_univ u g in
+ let g = declare_univ v g in
+ match compare g u v with
+ | EQ -> g
+ | GT -> error_inconsistency()
+ | GE -> merge g u v
+ | NGE ->
+ (match compare g v u with
+ | GT -> error_inconsistency()
+ | GE -> merge g v u
+ | NGE -> merge_disc g u v
+ | EQ -> anomaly "compare")
+
+(* enforcegt u v will force u>v if possible, will fail otherwise *)
+let enforce_gt u v g =
+ let g = declare_univ u g in
+ let g = declare_univ v g in
+ match compare g u v with
+ | GT -> g
+ | GE -> setgt g u v
+ | EQ -> error_inconsistency()
+ | NGE ->
+ (match compare g v u with
+ | NGE -> setgt g u v
+ | _ -> error_inconsistency())
+
+let enforce_relation g u =
+ let rec enfrec g = function
+ | Terminal -> g
+ | Equiv v -> enforce_eq u v g
+ | Greater(false,v,r) -> enfrec (enforce_geq u v g) r
+ | Greater(true,v,r) -> enfrec (enforce_gt u v g) r
+ in
+ enfrec g
+
+
+(* Merging 2 universe graphs *)
+let merge_universes sp u1 u2 =
+ UniverseMap.fold (fun _ (Arc(u,r)) g -> enforce_relation g u r) u1 u2
+
+
+(* Returns the least upper bound of universes u and v. If they are not
+ constrained, then a new universe is created.
+ Used to type the products. *)
+let sup u v g =
+ let g = declare_univ u g in
+ let g = declare_univ v g in
+ match compare g u v with
+ | NGE ->
+ (match compare g v u with
+ | NGE ->
+ let w = new_univ u.u_sp in
+ let g' = setgeq g w u in
+ w, setgeq g' w v
+ | _ -> v, g)
+ | _ -> u, g
+
+(* Returns a fresh universe, juste above u. Does not create new universes
+ for Type_0 (the sort of Prop and Set).
+ Used to type the sort u. *)
+let super u g =
+ if u == prop_univ then
+ prop_univ_univ, g
+ else if u == prop_univ_univ then
+ prop_univ_univ_univ, g
+ else
+ let g = declare_univ u g in
+ let v = new_univ u.u_sp in
+ let g' = enter_arc (Arc(v,Greater(true,u,Terminal))) g in
+ v,g'
+
+(* Pretty-printing *)
+let num_universes g =
+ UniverseMap.fold (fun _ _ -> succ) g 0
+
+let num_edges g =
+ let reln_len =
+ let rec lenrec n = function
+ | Terminal -> n
+ | Equiv _ -> n+1
+ | Greater(_,_,r) -> lenrec (n+1) r
+ in
+ lenrec 0
+ in
+ UniverseMap.fold (fun _ (Arc(_,r)) n -> n + (reln_len r)) g 0
+
+let pr_reln u r =
+ let rec prec = function
+ | Greater(true,v,r) ->
+ [< pr_uni u ; 'sTR">" ; pr_uni v ; 'fNL ; prec r >]
+ | Greater(false,v,r) ->
+ [< pr_uni u ; 'sTR">=" ; pr_uni v ; 'fNL ; prec r >]
+ | Equiv v ->
+ [< pr_uni u ; 'sTR"=" ; pr_uni v >]
+ | Terminal -> [< >]
+ in
+ prec r
+
+let pr_universes g =
+ let graph = UniverseMap.fold (fun k a l -> (k,a)::l) g [] in
+ prlist_with_sep pr_fnl (function (_,Arc(u,r)) -> pr_reln u r) graph
+
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 203b0cbc6..1b47e00b4 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -11,6 +11,8 @@ val prop_univ : universe
val prop_univ_univ : universe
val prop_univ_univ_univ : universe
+val new_univ : section_path -> universe
+
type universes
val initial_universes : universes
@@ -19,12 +21,10 @@ val super : universe -> universes -> universe * universes
val sup : universe -> universe -> universes -> universe * universes
-type constraint_result =
- | Consistent of universes
- | Inconsistent
+exception UniverseInconsistency
type constraint_function =
- universe -> universe -> universes -> constraint_result
+ universe -> universe -> universes -> universes
val enforce_gt : constraint_function
val enforce_geq : constraint_function
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 13:27:48 +0000