diff options
Diffstat (limited to 'kernel/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 70 |
1 files changed, 39 insertions, 31 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index fe82d85d5d..0ea68e2bcc 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -12,13 +12,13 @@ open Names open Univ open Term open Vars -open Context open Declarations open Environ open Entries open Reduction open Inductive open Type_errors +open Context.Rel.Declaration let conv_leq l2r env x y = default_conv CUMUL ~l2r env x y @@ -79,7 +79,7 @@ let judge_of_type u = let judge_of_relative env n = try - let (_,_,typ) = lookup_rel n env in + let typ = get_type (lookup_rel n env) in { uj_val = mkRel n; uj_type = lift n typ } with Not_found -> @@ -99,18 +99,20 @@ let judge_of_variable env id = variables of the current env. Order does not have to be checked assuming that all names are distinct *) let check_hyps_inclusion env c sign = - Context.fold_named_context - (fun (id,b1,ty1) () -> + Context.Named.fold_outside + (fun d1 () -> + let open Context.Named.Declaration in + let id = get_id d1 in try - let (_,b2,ty2) = lookup_named id env in - conv env ty2 ty1; - (match b2,b1 with - | None, None -> () - | None, Some _ -> + let d2 = lookup_named id env in + conv env (get_type d2) (get_type d1); + (match d2,d1 with + | LocalAssum _, LocalAssum _ -> () + | LocalAssum _, LocalDef _ -> (* This is wrong, because we don't know if the body is needed or not for typechecking: *) () - | Some _, None -> raise NotConvertible - | Some b2, Some b1 -> conv env b2 b1); + | LocalDef _, LocalAssum _ -> raise NotConvertible + | LocalDef (_,b2,_), LocalDef (_,b1,_) -> conv env b2 b1); with Not_found | NotConvertible | Option.Heterogeneous -> error_reference_variables env id c) sign @@ -125,19 +127,25 @@ let extract_level env p = match kind_of_term c with Sort (Type u) -> Univ.Universe.level u | _ -> None let extract_context_levels env l = - let fold l (_, b, p) = match b with - | None -> extract_level env p :: l - | _ -> l + let fold l = function + | LocalAssum (_,p) -> extract_level env p :: l + | LocalDef _ -> l in List.fold_left fold [] l let make_polymorphic_if_constant_for_ind env {uj_val = c; uj_type = t} = let params, ccl = dest_prod_assum env t in match kind_of_term ccl with - | Sort (Type u) when isInd (fst (decompose_app (whd_betadeltaiota env c))) -> - let param_ccls = extract_context_levels env params in - let s = { template_param_levels = param_ccls; template_level = u} in - TemplateArity (params,s) + | Sort (Type u) -> + let ind, l = decompose_app (whd_betadeltaiota env c) in + if isInd ind && List.is_empty l then + let mis = lookup_mind_specif env (fst (destInd ind)) in + let nparams = Inductive.inductive_params mis in + let paramsl = CList.lastn nparams params in + let param_ccls = extract_context_levels env paramsl in + let s = { template_param_levels = param_ccls; template_level = u} in + TemplateArity (params,s) + else RegularArity t | _ -> RegularArity t @@ -294,7 +302,7 @@ let judge_of_cast env cj k tj = match k with | VMcast -> mkCast (cj.uj_val, k, expected_type), - vm_conv CUMUL env cj.uj_type expected_type + Reduction.vm_conv CUMUL env cj.uj_type expected_type | DEFAULTcast -> mkCast (cj.uj_val, k, expected_type), default_conv ~l2r:false CUMUL env cj.uj_type expected_type @@ -304,7 +312,7 @@ let judge_of_cast env cj k tj = | NATIVEcast -> let sigma = Nativelambda.empty_evars in mkCast (cj.uj_val, k, expected_type), - native_conv CUMUL sigma env cj.uj_type expected_type + Nativeconv.native_conv CUMUL sigma env cj.uj_type expected_type in { uj_val = c; uj_type = expected_type } @@ -453,13 +461,13 @@ let rec execute env cstr = | Lambda (name,c1,c2) -> let varj = execute_type env c1 in - let env1 = push_rel (name,None,varj.utj_val) env in + let env1 = push_rel (LocalAssum (name,varj.utj_val)) env in let j' = execute env1 c2 in judge_of_abstraction env name varj j' | Prod (name,c1,c2) -> let varj = execute_type env c1 in - let env1 = push_rel (name,None,varj.utj_val) env in + let env1 = push_rel (LocalAssum (name,varj.utj_val)) env in let varj' = execute_type env1 c2 in judge_of_product env name varj varj' @@ -467,11 +475,11 @@ let rec execute env cstr = let j1 = execute env c1 in let j2 = execute_type env c2 in let _ = judge_of_cast env j1 DEFAULTcast j2 in - let env1 = push_rel (name,Some j1.uj_val,j2.utj_val) env in + let env1 = push_rel (LocalDef (name,j1.uj_val,j2.utj_val)) env in let j' = execute env1 c3 in judge_of_letin env name j1 j2 j' - | Cast (c,k, t) -> + | Cast (c,k,t) -> let cj = execute env c in let tj = execute_type env t in judge_of_cast env cj k tj @@ -543,18 +551,18 @@ let infer_v env cv = (* Typing of several terms. *) let infer_local_decl env id = function - | LocalDef c -> + | LocalDefEntry c -> let j = infer env c in - (Name id, Some j.uj_val, j.uj_type) - | LocalAssum c -> + LocalDef (Name id, j.uj_val, j.uj_type) + | LocalAssumEntry c -> let j = infer env c in - (Name id, None, assumption_of_judgment env j) + LocalAssum (Name id, assumption_of_judgment env j) let infer_local_decls env decls = let rec inferec env = function | (id, d) :: l -> let (env, l) = inferec env l in let d = infer_local_decl env id d in - (push_rel d env, add_rel_decl d l) - | [] -> (env, empty_rel_context) in + (push_rel d env, Context.Rel.add d l) + | [] -> (env, Context.Rel.empty) in inferec env decls |