diff options
Diffstat (limited to 'kernel/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 240 |
1 files changed, 160 insertions, 80 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 19d76bfee6..f86c12e1f1 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -213,9 +213,20 @@ let type_of_apply env func funt argsv argstv = apply_rec 0 (inject funt) (* Type of primitive constructs *) -let type_of_prim_type _env = function - | CPrimitives.PT_int63 -> Constr.mkSet - | CPrimitives.PT_float64 -> Constr.mkSet +let type_of_prim_type _env u (type a) (prim : a CPrimitives.prim_type) = match prim with + | CPrimitives.PT_int63 -> + assert (Univ.Instance.is_empty u); + Constr.mkSet + | CPrimitives.PT_float64 -> + assert (Univ.Instance.is_empty u); + Constr.mkSet + | CPrimitives.PT_array -> + begin match Univ.Instance.to_array u with + | [|u|] -> + let ty = Constr.mkType (Univ.Universe.make u) in + Constr.mkProd(Context.anonR, ty , ty) + | _ -> anomaly Pp.(str"universe instance for array type should have length 1") + end let type_of_int env = match env.retroknowledge.Retroknowledge.retro_int63 with @@ -228,71 +239,11 @@ let type_of_float env = | None -> raise (Invalid_argument "Typeops.type_of_float: float64 not_defined") -let type_of_prim env t = - let int_ty () = type_of_int env in - let float_ty () = type_of_float env in - let bool_ty () = - match env.retroknowledge.Retroknowledge.retro_bool with - | Some ((ind,_),_) -> Constr.mkInd ind - | None -> CErrors.user_err Pp.(str"The type bool must be registered before this primitive.") - in - let compare_ty () = - match env.retroknowledge.Retroknowledge.retro_cmp with - | Some ((ind,_),_,_) -> Constr.mkInd ind - | None -> CErrors.user_err Pp.(str"The type compare must be registered before this primitive.") - in - let f_compare_ty () = - match env.retroknowledge.Retroknowledge.retro_f_cmp with - | Some ((ind,_),_,_,_) -> Constr.mkInd ind - | None -> CErrors.user_err Pp.(str"The type float_comparison must be registered before this primitive.") - in - let f_class_ty () = - match env.retroknowledge.Retroknowledge.retro_f_class with - | Some ((ind,_),_,_,_,_,_,_,_,_) -> Constr.mkInd ind - | None -> CErrors.user_err Pp.(str"The type float_class must be registered before this primitive.") - in - let pair_ty fst_ty snd_ty = - match env.retroknowledge.Retroknowledge.retro_pair with - | Some (ind,_) -> Constr.mkApp(Constr.mkInd ind, [|fst_ty;snd_ty|]) - | None -> CErrors.user_err Pp.(str"The type pair must be registered before this primitive.") - in - let carry_ty int_ty = - match env.retroknowledge.Retroknowledge.retro_carry with - | Some ((ind,_),_) -> Constr.mkApp(Constr.mkInd ind, [|int_ty|]) - | None -> CErrors.user_err Pp.(str"The type carry must be registered before this primitive.") - in - let open CPrimitives in - let tr_prim_type = function - | PT_int63 -> int_ty () - | PT_float64 -> float_ty () in - let tr_ind (type t) (i : t prim_ind) (a : t) = match i, a with - | PIT_bool, () -> bool_ty () - | PIT_carry, t -> carry_ty (tr_prim_type t) - | PIT_pair, (t1, t2) -> pair_ty (tr_prim_type t1) (tr_prim_type t2) - | PIT_cmp, () -> compare_ty () - | PIT_f_cmp, () -> f_compare_ty () - | PIT_f_class, () -> f_class_ty () in - let tr_type = function - | PITT_ind (i, a) -> tr_ind i a - | PITT_type t -> tr_prim_type t in - let rec nary_op = function - | [] -> assert false - | [ret_ty] -> tr_type ret_ty - | arg_ty :: r -> - let arg_ty = tr_type arg_ty in - Constr.mkProd(Context.nameR (Id.of_string "x"), arg_ty, nary_op r) in - nary_op (types t) - -let type_of_prim_or_type env = let open CPrimitives in - function - | OT_type t -> type_of_prim_type env t - | OT_op op -> type_of_prim env op - -let judge_of_int env i = - make_judge (Constr.mkInt i) (type_of_int env) - -let judge_of_float env f = - make_judge (Constr.mkFloat f) (type_of_float env) +let type_of_array env u = + assert (Univ.Instance.length u = 1); + match env.retroknowledge.Retroknowledge.retro_array with + | Some c -> mkConstU (c,u) + | None -> CErrors.user_err Pp.(str"The type array must be registered before this construction can be typechecked.") (* Type of product *) @@ -354,6 +305,18 @@ let check_cast env c ct k expected_type = with NotConvertible -> error_actual_type env (make_judge c ct) expected_type +let judge_of_int env i = + make_judge (Constr.mkInt i) (type_of_int env) + +let judge_of_float env f = + make_judge (Constr.mkFloat f) (type_of_float env) + +let judge_of_array env u tj defj = + let def = defj.uj_val in + let ty = defj.uj_type in + Array.iter (fun j -> check_cast env j.uj_val j.uj_type DEFAULTcast ty) tj; + make_judge (mkArray(u, Array.map j_val tj, def, ty)) (mkApp (type_of_array env u, [|ty|])) + (* Inductive types. *) (* The type is parametric over the uniform parameters whose conclusion @@ -407,7 +370,20 @@ let check_branch_types env (ind,u) c ct lft explft = | Invalid_argument _ -> error_number_branches env (make_judge c ct) (Array.length explft) -let type_of_case env ci p pt c ct _lf lft = +let should_invert_case env ci = + ci.ci_relevance == Sorts.Relevant && + let mib,mip = lookup_mind_specif env ci.ci_ind in + mip.mind_relevance == Sorts.Irrelevant && + (* NB: it's possible to have 2 ctors or arguments to 1 ctor by unsetting univ checks + but we don't do special reduction in such cases + + XXX Someday consider more carefully what happens with letin params and arguments + (currently they're squashed, see indtyping) + *) + Array.length mip.mind_nf_lc = 1 && + List.length (fst mip.mind_nf_lc.(0)) = List.length mib.mind_params_ctxt + +let type_of_case env ci p pt iv c ct _lf lft = let (pind, _ as indspec) = try find_rectype env ct with Not_found -> error_case_not_inductive env (make_judge c ct) in @@ -418,6 +394,14 @@ let type_of_case env ci p pt c ct _lf lft = else (warn_bad_relevance_ci (); {ci with ci_relevance=rp}) in let () = check_case_info env pind rp ci in + let () = + let is_inversion = match iv with + | NoInvert -> false + | CaseInvert _ -> true (* contents already checked *) + in + if not (is_inversion = should_invert_case env ci) + then error_bad_invert env + in let (bty,rslty) = type_case_branches env indspec (make_judge p pt) c in let () = check_branch_types env pind c ct lft bty in @@ -564,13 +548,22 @@ let rec execute env cstr = | Construct c -> cstr, type_of_constructor env c - | Case (ci,p,c,lf) -> + | Case (ci,p,iv,c,lf) -> let c', ct = execute env c in + let iv' = match iv with + | NoInvert -> NoInvert + | CaseInvert {univs;args} -> + let ct' = mkApp (mkIndU (ci.ci_ind,univs), args) in + let (ct', _) : constr * Sorts.t = execute_is_type env ct' in + let () = conv_leq false env ct ct' in + let _, args' = decompose_appvect ct' in + if args == args' then iv else CaseInvert {univs;args=args'} + in let p', pt = execute env p in let lf', lft = execute_array env lf in - let ci', t = type_of_case env ci p' pt c' ct lf' lft in - let cstr = if ci == ci' && c == c' && p == p' && lf == lf' then cstr - else mkCase(ci',p',c',lf') + let ci', t = type_of_case env ci p' pt iv' c' ct lf' lft in + let cstr = if ci == ci' && c == c' && p == p' && iv == iv' && lf == lf' then cstr + else mkCase(ci',p',iv',c',lf') in cstr, t @@ -591,6 +584,23 @@ let rec execute env cstr = (* Primitive types *) | Int _ -> cstr, type_of_int env | Float _ -> cstr, type_of_float env + | Array(u,t,def,ty) -> + (* ty : Type@{u} and all of t,def : ty *) + let ulev = match Univ.Instance.to_array u with + | [|u|] -> u + | _ -> assert false + in + let ty',tyty = execute env ty in + check_cast env ty' tyty DEFAULTcast (mkType (Universe.make ulev)); + let def', def_ty = execute env def in + check_cast env def' def_ty DEFAULTcast ty'; + let ta = type_of_array env u in + let t' = Array.Smart.map (fun x -> + let x', xt = execute env x in + check_cast env x' xt DEFAULTcast ty'; + x') t in + let cstr = if def'==def && t'==t && ty'==ty then cstr else mkArray(u, t',def',ty') in + cstr, mkApp(ta, [|ty'|]) (* Partial proofs: unsupported by the kernel *) | Meta _ -> @@ -710,14 +720,84 @@ let judge_of_inductive env indu = let judge_of_constructor env cu = make_judge (mkConstructU cu) (type_of_constructor env cu) -let judge_of_case env ci pj cj lfj = +let judge_of_case env ci pj iv cj lfj = let lf, lft = dest_judgev lfj in - let ci, t = type_of_case env ci pj.uj_val pj.uj_type cj.uj_val cj.uj_type lf lft in - make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val, lft)) t + let ci, t = type_of_case env ci pj.uj_val pj.uj_type iv cj.uj_val cj.uj_type lf lft in + make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, iv, cj.uj_val, lft)) t (* Building type of primitive operators and type *) -let check_primitive_type env op_t t = - let inft = type_of_prim_or_type env op_t in - try default_conv ~l2r:false CUMUL env inft t - with NotConvertible -> error_incorrect_primitive env (make_judge op_t inft) t +let type_of_prim_const env _u c = + let int_ty () = type_of_int env in + match c with + | CPrimitives.Arraymaxlength -> + int_ty () + +let type_of_prim env u t = + let int_ty () = type_of_int env in + let float_ty () = type_of_float env in + let array_ty u a = mkApp(type_of_array env u, [|a|]) in + let bool_ty () = + match env.retroknowledge.Retroknowledge.retro_bool with + | Some ((ind,_),_) -> Constr.mkInd ind + | None -> CErrors.user_err Pp.(str"The type bool must be registered before this primitive.") + in + let compare_ty () = + match env.retroknowledge.Retroknowledge.retro_cmp with + | Some ((ind,_),_,_) -> Constr.mkInd ind + | None -> CErrors.user_err Pp.(str"The type compare must be registered before this primitive.") + in + let f_compare_ty () = + match env.retroknowledge.Retroknowledge.retro_f_cmp with + | Some ((ind,_),_,_,_) -> Constr.mkInd ind + | None -> CErrors.user_err Pp.(str"The type float_comparison must be registered before this primitive.") + in + let f_class_ty () = + match env.retroknowledge.Retroknowledge.retro_f_class with + | Some ((ind,_),_,_,_,_,_,_,_,_) -> Constr.mkInd ind + | None -> CErrors.user_err Pp.(str"The type float_class must be registered before this primitive.") + in + let pair_ty fst_ty snd_ty = + match env.retroknowledge.Retroknowledge.retro_pair with + | Some (ind,_) -> Constr.mkApp(Constr.mkInd ind, [|fst_ty;snd_ty|]) + | None -> CErrors.user_err Pp.(str"The type pair must be registered before this primitive.") + in + let carry_ty int_ty = + match env.retroknowledge.Retroknowledge.retro_carry with + | Some ((ind,_),_) -> Constr.mkApp(Constr.mkInd ind, [|int_ty|]) + | None -> CErrors.user_err Pp.(str"The type carry must be registered before this primitive.") + in + let open CPrimitives in + let tr_prim_type (tr_type : ind_or_type -> constr) (type a) (ty : a prim_type) (t : a) = match ty with + | PT_int63 -> int_ty t + | PT_float64 -> float_ty t + | PT_array -> array_ty (fst t) (tr_type (snd t)) + in + let tr_ind (tr_type : ind_or_type -> constr) (type t) (i : t prim_ind) (a : t) = match i, a with + | PIT_bool, () -> bool_ty () + | PIT_carry, t -> carry_ty (tr_type t) + | PIT_pair, (t1, t2) -> pair_ty (tr_type t1) (tr_type t2) + | PIT_cmp, () -> compare_ty () + | PIT_f_cmp, () -> f_compare_ty () + | PIT_f_class, () -> f_class_ty () + in + let rec tr_type n = function + | PITT_ind (i, a) -> tr_ind (tr_type n) i a + | PITT_type (ty,t) -> tr_prim_type (tr_type n) ty t + | PITT_param i -> Constr.mkRel (n+i) + in + let rec nary_op n = function + | [] -> assert false + | [ret_ty] -> tr_type n ret_ty + | arg_ty :: r -> + Constr.mkProd(Context.nameR (Id.of_string "x"), tr_type n arg_ty, nary_op (n+1) r) + in + let params, sign = types t in + assert (AUContext.size (univs t) = Instance.length u); + Vars.subst_instance_constr u (Term.it_mkProd_or_LetIn (nary_op 0 sign) params) + +let type_of_prim_or_type env u = let open CPrimitives in + function + | OT_type t -> type_of_prim_type env u t + | OT_op op -> type_of_prim env u op + | OT_const c -> type_of_prim_const env u c |