summaryrefslogtreecommitdiff
path: root/checker/typeops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/typeops.ml')
-rw-r--r--checker/typeops.ml184
1 files changed, 83 insertions, 101 deletions
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 6b0c6eaf..9bc4b269 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -1,25 +1,25 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Errors
open Util
open Names
-open Univ
+open Cic
open Term
open Reduction
open Type_errors
-open Declarations
open Inductive
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
with NotConvertible -> raise (NotConvertibleVect i)); ())
@@ -27,6 +27,10 @@ let conv_leq_vecti env v1 v2 =
v1
v2
+let check_constraints cst env =
+ if Environ.check_constraints cst env then ()
+ else error_unsatisfied_constraints env cst
+
(* This should be a type (a priori without intension to be an assumption) *)
let type_judgment env (c,ty as j) =
match whd_betadeltaiota env ty with
@@ -48,11 +52,11 @@ let assumption_of_judgment env j =
(* Prop and Set *)
-let judge_of_prop = Sort (Type type1_univ)
+let judge_of_prop = Sort (Type Univ.type1_univ)
(* Type of Type(i). *)
-let judge_of_type u = Sort (Type (super u))
+let judge_of_type u = Sort (Type (Univ.super u))
(*s Type of a de Bruijn index. *)
@@ -63,53 +67,36 @@ let judge_of_relative env n =
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 ->
- error_unbound_var env id
-
-(* Management of context of variables. *)
-
-(* Checks if a context of variable can be instantiated by the
- variables of the current env *)
-(* TODO: check order? *)
-let rec check_hyps_inclusion env sign =
- fold_named_context
- (fun (id,_,ty1) () ->
- let ty2 = named_type id env in
- if not (eq_constr ty2 ty1) then
- error "types do not match")
- sign
- ~init:()
-
-
-let check_args env c hyps =
- try check_hyps_inclusion env hyps
- with UserError _ | Not_found ->
- error_reference_variables env c
-
(* Type of constants *)
-let type_of_constant_knowing_parameters env t paramtyps =
+
+let type_of_constant_type_knowing_parameters env t paramtyps =
match t with
- | NonPolymorphicType t -> t
- | PolymorphicArity (sign,ar) ->
+ | RegularArity t -> t
+ | TemplateArity (sign,ar) ->
let ctx = List.rev sign in
let ctx,s = instantiate_universes env ctx ar paramtyps in
mkArity (List.rev ctx,s)
+let type_of_constant_knowing_parameters env cst paramtyps =
+ let ty, cu = constant_type env cst in
+ type_of_constant_type_knowing_parameters env ty paramtyps, cu
+
let type_of_constant_type env t =
- type_of_constant_knowing_parameters env t [||]
+ type_of_constant_type_knowing_parameters env t [||]
-let judge_of_constant_knowing_parameters env cst paramstyp =
- let c = Const cst in
- let cb =
- try lookup_constant cst env
+let type_of_constant env cst =
+ type_of_constant_knowing_parameters env cst [||]
+
+let judge_of_constant_knowing_parameters env (kn,u as cst) paramstyp =
+ let _cb =
+ try lookup_constant kn env
with Not_found ->
- failwith ("Cannot find constant: "^string_of_con cst) in
- let _ = check_args env c cb.const_hyps in
- type_of_constant_knowing_parameters env cb.const_type paramstyp
+ failwith ("Cannot find constant: "^string_of_con kn)
+ in
+ let ty, cu = type_of_constant_knowing_parameters env cst paramstyp in
+ let () = check_constraints cu env in
+ ty
let judge_of_constant env cst =
judge_of_constant_knowing_parameters env cst [||]
@@ -146,13 +133,13 @@ let sort_of_product env domsort rangsort =
rangsort
else
(* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
- Type (sup u1 type0_univ)
+ Type (Univ.sup u1 Univ.type0_univ)
(* Product rule (Prop,Type_i,Type_i) *)
- | (Prop Pos, Type u2) -> Type (sup type0_univ u2)
+ | (Prop Pos, Type u2) -> Type (Univ.sup Univ.type0_univ u2)
(* Product rule (Prop,Type_i,Type_i) *)
| (Prop Null, Type _) -> rangsort
(* Product rule (Type_i,Type_i,Type_i) *)
- | (Type u1, Type u2) -> Type (sup u1 u2)
+ | (Type u1, Type u2) -> Type (Univ.sup u1 u2)
(* Type of a type cast *)
@@ -166,7 +153,7 @@ let sort_of_product env domsort rangsort =
let judge_of_cast env (c,cj) k tj =
let conversion =
match k with
- | VMcast -> vm_conv CUMUL
+ | VMcast | NATIVEcast -> vm_conv CUMUL
| DEFAULTcast -> conv_leq in
try
conversion env cj tj
@@ -187,31 +174,27 @@ let judge_of_cast env (c,cj) k tj =
the App case of execute; from this constraints, the expected
dynamic constraints of the form u<=v are enforced *)
-let judge_of_inductive_knowing_parameters env ind (paramstyp:constr array) =
- let c = Ind ind in
- let (mib,mip) =
+let judge_of_inductive_knowing_parameters env (ind,u) (paramstyp:constr array) =
+ let specif =
try lookup_mind_specif env ind
with Not_found ->
- failwith ("Cannot find inductive: "^string_of_mind (fst ind)) in
- check_args env c mib.mind_hyps;
- type_of_inductive_knowing_parameters env mip paramstyp
+ failwith ("Cannot find inductive: "^string_of_mind (fst ind))
+ in
+ type_of_inductive_knowing_parameters env (specif,u) paramstyp
let judge_of_inductive env ind =
judge_of_inductive_knowing_parameters env ind [||]
(* Constructors. *)
-let judge_of_constructor env c =
- let constr = Construct c in
- let _ =
- let ((kn,_),_) = c in
- let mib =
- try lookup_mind kn env
- with Not_found ->
- failwith ("Cannot find inductive: "^string_of_mind (fst (fst c))) in
- check_args env constr mib.mind_hyps in
- let specif = lookup_mind_specif env (inductive_of_constructor c) in
- type_of_constructor c specif
+let judge_of_constructor env (c,u) =
+ let ind = inductive_of_constructor c in
+ let specif =
+ try lookup_mind_specif env ind
+ with Not_found ->
+ failwith ("Cannot find inductive: "^string_of_mind (fst ind))
+ in
+ type_of_constructor (c,u) specif
(* Case. *)
@@ -227,11 +210,23 @@ let judge_of_case env ci pj (c,cj) lfj =
let indspec =
try find_rectype env cj
with Not_found -> error_case_not_inductive env (c,cj) in
- let _ = check_case_info env (fst indspec) ci in
+ let _ = check_case_info env (fst (fst indspec)) ci in
let (bty,rslty) = type_case_branches env indspec pj c in
check_branch_types env (c,cj) (lfj,bty);
rslty
+(* Projection. *)
+
+let judge_of_projection env p c ct =
+ let pb = lookup_projection p env in
+ let (ind,u), args =
+ try find_rectype env ct
+ with Not_found -> error_case_not_inductive env (c, ct)
+ in
+ assert(eq_mind pb.proj_ind (fst ind));
+ let ty = subst_instance_constr u pb.proj_type in
+ substl (c :: List.rev args) ty
+
(* Fixpoints. *)
(* Checks the type of a general (co)fixpoint, i.e. without checking *)
@@ -243,21 +238,21 @@ let type_fixpoint env lna lar lbody vdefj =
try
conv_leq_vecti env vdefj (Array.map (fun ty -> lift lt ty) lar)
with NotConvertibleVect i ->
- let vdefj = array_map2 (fun b ty -> b,ty) lbody vdefj in
+ let vdefj = Array.map2 (fun b ty -> b,ty) lbody vdefj in
error_ill_typed_rec_body env i lna vdefj lar
(************************************************************************)
(************************************************************************)
-let refresh_arity env ar =
- let ctxt, hd = decompose_prod_assum ar in
- match hd with
- Sort (Type u) when not (is_univ_variable u) ->
- let u' = fresh_local_univ() in
- let env' = add_constraints (enforce_geq u' u empty_constraint) env in
- env', mkArity (ctxt,Type u')
- | _ -> env, ar
+(* let refresh_arity env ar = *)
+(* let ctxt, hd = decompose_prod_assum ar in *)
+(* match hd with *)
+(* Sort (Type u) when not (is_univ_variable u) -> *)
+(* let u' = fresh_local_univ() in *)
+(* let env' = add_constraints (enforce_leq u u' empty_constraint) env in *)
+(* env', mkArity (ctxt,Type u') *)
+(* | _ -> env, ar *)
(* The typing machine. *)
@@ -270,7 +265,7 @@ let rec execute env cstr =
| Rel n -> judge_of_relative env n
- | Var id -> judge_of_variable env id
+ | Var _ -> anomaly (Pp.str "Section variable in Coqchk !")
| Const c -> judge_of_constant env c
@@ -292,9 +287,13 @@ let rec execute env cstr =
(* No sort-polymorphism *)
execute env f
in
- let jl = array_map2 (fun c ty -> c,ty) args jl in
+ let jl = Array.map2 (fun c ty -> c,ty) args jl in
judge_of_apply env (f,j) jl
+ | Proj (p, c) ->
+ let ct = execute env c in
+ judge_of_projection env p c ct
+
| Lambda (name,c1,c2) ->
let _ = execute_type env c1 in
let env1 = push_rel (name,None,c1) env in
@@ -312,7 +311,7 @@ let rec execute env cstr =
(* /!\ c2 can be an inferred type => refresh
(but the pushed type is still c2) *)
let _ =
- let env',c2' = refresh_arity env c2 in
+ let env',c2' = (* refresh_arity env *) env, c2 in
let _ = execute_type env' c2' in
judge_of_cast env' (c1,j1) DEFAULTcast c2' in
let env1 = push_rel (name,Some c1,c2) env in
@@ -350,10 +349,10 @@ let rec execute env cstr =
(* Partial proofs: unsupported by the kernel *)
| Meta _ ->
- anomaly "the kernel does not support metavariables"
+ anomaly (Pp.str "the kernel does not support metavariables")
| Evar _ ->
- anomaly "the kernel does not support existential variables"
+ anomaly (Pp.str "the kernel does not support existential variables")
and execute_type env constr =
let j = execute env constr in
@@ -361,7 +360,7 @@ and execute_type env constr =
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
+ let larj = Array.map2 (fun c ty -> c,ty) lar larj in
let lara = Array.map (assumption_of_judgment env) larj in
let env1 = push_rec_types (names,lara,vdef) env in
let vdefj = execute_array env1 vdef in
@@ -389,32 +388,15 @@ let check_ctxt env rels =
push_rel d env)
rels ~init:env
-let check_named_ctxt env ctxt =
- fold_named_context (fun (id,_,_ as d) env ->
- let _ =
- try
- let _ = lookup_named id env in
- failwith ("variable "^string_of_id id^" defined twice")
- with Not_found -> () in
- match d with
- (_,None,ty) ->
- let _ = infer_type env ty in
- push_named d env
- | (_,Some bd,ty) ->
- let j1 = infer env bd in
- let _ = infer env ty in
- conv_leq env j1 ty;
- push_named d env)
- ctxt ~init:env
-
(* Polymorphic arities utils *)
let check_kind env ar u =
- if snd (dest_prod env ar) = Sort(Type u) then ()
- else failwith "not the correct sort"
+ match (snd (dest_prod env ar)) with
+ | Sort (Type u') when Univ.Universe.equal u' (Univ.Universe.make u) -> ()
+ | _ -> failwith "not the correct sort"
let check_polymorphic_arity env params par =
- let pl = par.poly_param_levels in
+ let pl = par.template_param_levels in
let rec check_p env pl params =
match pl, params with
Some u::pl, (na,None,ty)::params ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 06:59:44 +0000