From 75508769762372043387c67a9abe94e8f940e80a Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 27 Oct 2017 14:03:51 +0200 Subject: Add a non-cumulative impredicative universe SProp. Note currently it's impossible to define inductives in SProp because indtypes.ml and the pretyper aren't fully plugged. --- pretyping/typing.ml | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) (limited to 'pretyping/typing.ml') diff --git a/pretyping/typing.ml b/pretyping/typing.ml index ea6e52e1f8..ed020e243d 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -65,7 +65,7 @@ let judge_of_applied_inductive_knowing_parameters env sigma funj ind argjv = match EConstr.kind sigma (whd_all env sigma typ) with | Prod (_,c1,c2) -> sigma, (c1,c2) | Evar ev -> - let (sigma,t) = Evardefine.define_evar_as_product sigma ev in + let (sigma,t) = Evardefine.define_evar_as_product env sigma ev in let (_,c1,c2) = destProd sigma t in sigma, (c1,c2) | _ -> @@ -90,7 +90,7 @@ let judge_of_apply env sigma funj argjv = match EConstr.kind sigma (whd_all env sigma typ) with | Prod (_,c1,c2) -> sigma, (c1,c2) | Evar ev -> - let (sigma,t) = Evardefine.define_evar_as_product sigma ev in + let (sigma,t) = Evardefine.define_evar_as_product env sigma ev in let (_,c1,c2) = destProd sigma t in sigma, (c1,c2) | _ -> @@ -230,6 +230,10 @@ let check_cofix env sigma pcofix = (* The typing machine with universes and existential variables. *) +let judge_of_sprop = + { uj_val = EConstr.mkSProp; + uj_type = EConstr.type1 } + let judge_of_prop = { uj_val = EConstr.mkProp; uj_type = EConstr.mkSort Sorts.type1 } @@ -361,6 +365,9 @@ let rec execute env sigma cstr = | Sort s -> begin match ESorts.kind sigma s with + | SProp -> + if Environ.sprop_allowed env then sigma, judge_of_sprop + else error_disallowed_sprop env sigma | Prop -> sigma, judge_of_prop | Set -> sigma, judge_of_set | Type u -> sigma, judge_of_type u -- cgit v1.2.3 From 23f84f37c674a07e925925b7e0d50d7ee8414093 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 31 Oct 2017 17:04:02 +0100 Subject: Add relevance marks on binders. Kernel should be mostly correct, higher levels do random stuff at times. --- pretyping/typing.ml | 49 +++++++++++++++++++++++++++++-------------------- 1 file changed, 29 insertions(+), 20 deletions(-) (limited to 'pretyping/typing.ml') diff --git a/pretyping/typing.ml b/pretyping/typing.ml index ed020e243d..b660973cdd 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -15,6 +15,7 @@ open CErrors open Util open Term open Constr +open Context open Environ open EConstr open Vars @@ -122,7 +123,7 @@ let max_sort l = let is_correct_arity env sigma c pj ind specif params = let arsign = make_arity_signature env sigma true (make_ind_family (ind,params)) in let allowed_sorts = elim_sorts specif in - let error () = Pretype_errors.error_elim_arity env sigma ind allowed_sorts c pj None in + let error () = Pretype_errors.error_elim_arity env sigma ind c pj None in let rec srec env sigma pt ar = let pt' = whd_all env sigma pt in match EConstr.kind sigma pt', ar with @@ -136,11 +137,11 @@ let is_correct_arity env sigma c pj ind specif params = let s = ESorts.kind sigma s in if not (Sorts.List.mem (Sorts.family s) allowed_sorts) then error () - else sigma + else sigma, s | Evar (ev,_), [] -> let sigma, s = Evd.fresh_sort_in_family sigma (max_sort allowed_sorts) in let sigma = Evd.define ev (mkSort s) sigma in - sigma + sigma, s | _, (LocalDef _ as d)::ar' -> srec (push_rel d env) sigma (lift 1 pt') ar' | _ -> @@ -165,20 +166,20 @@ let type_case_branches env sigma (ind,largs) pj c = let (params,realargs) = List.chop nparams largs in let p = pj.uj_val in let params = List.map EConstr.Unsafe.to_constr params in - let sigma = is_correct_arity env sigma c pj ind specif params in + let sigma, ps = is_correct_arity env sigma c pj ind specif params in let lc = build_branches_type ind specif params (EConstr.to_constr ~abort_on_undefined_evars:false sigma p) in let lc = Array.map EConstr.of_constr lc in let n = (snd specif).Declarations.mind_nrealdecls in let ty = whd_betaiota sigma (lambda_applist_assum sigma (n+1) p (realargs@[c])) in - sigma, (lc, ty) + sigma, (lc, ty, Sorts.relevance_of_sort ps) let judge_of_case env sigma ci pj cj lfj = let ((ind, u), spec) = try find_mrectype env sigma cj.uj_type with Not_found -> error_case_not_inductive env sigma cj in let indspec = ((ind, EInstance.kind sigma u), spec) in - let _ = check_case_info env (fst indspec) ci in - let sigma, (bty,rslty) = type_case_branches env sigma indspec pj cj.uj_val in + let sigma, (bty,rslty,rci) = type_case_branches env sigma indspec pj cj.uj_val in + let () = check_case_info env (fst indspec) rci ci in let sigma = check_branch_types env sigma (fst indspec) cj (lfj,bty) in sigma, { uj_val = mkCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj); uj_type = rslty } @@ -203,11 +204,13 @@ let check_allowed_sort env sigma ind c p = let _, s = splay_prod env sigma pj.uj_type in let ksort = match EConstr.kind sigma s with | Sort s -> Sorts.family (ESorts.kind sigma s) - | _ -> error_elim_arity env sigma ind sorts c pj None in + | _ -> error_elim_arity env sigma ind c pj None in if not (List.exists ((==) ksort) sorts) then let s = inductive_sort_family (snd specif) in - error_elim_arity env sigma ind sorts c pj - (Some(ksort,s,Type_errors.error_elim_explain ksort s)) + error_elim_arity env sigma ind c pj + (Some(sorts,ksort,s,Type_errors.error_elim_explain ksort s)) + else + Sorts.relevance_of_sort_family ksort let judge_of_cast env sigma cj k tj = let expected_type = tj.utj_val in @@ -266,16 +269,19 @@ let judge_of_projection env sigma p cj = uj_type = ty} let judge_of_abstraction env name var j = - { uj_val = mkLambda (name, var.utj_val, j.uj_val); - uj_type = mkProd (name, var.utj_val, j.uj_type) } + let r = Sorts.relevance_of_sort var.utj_type in + { uj_val = mkLambda (make_annot name r, var.utj_val, j.uj_val); + uj_type = mkProd (make_annot name r, var.utj_val, j.uj_type) } let judge_of_product env name t1 t2 = + let r = Sorts.relevance_of_sort t1.utj_type in let s = sort_of_product env t1.utj_type t2.utj_type in - { uj_val = mkProd (name, t1.utj_val, t2.utj_val); + { uj_val = mkProd (make_annot name r, t1.utj_val, t2.utj_val); uj_type = mkSort s } let judge_of_letin env name defj typj j = - { uj_val = mkLetIn (name, defj.uj_val, typj.utj_val, j.uj_val) ; + let r = Sorts.relevance_of_sort typj.utj_type in + { uj_val = mkLetIn (make_annot name r, defj.uj_val, typj.utj_val, j.uj_val) ; uj_type = subst1 defj.uj_val j.uj_type } let check_hyps_inclusion env sigma f x hyps = @@ -353,7 +359,7 @@ let rec execute env sigma cstr = | Fix ((vn,i as vni),recdef) -> let sigma, (_,tys,_ as recdef') = execute_recdef env sigma recdef in - let fix = (vni,recdef') in + let fix = (vni,recdef') in check_fix env sigma fix; sigma, make_judge (mkFix fix) tys.(i) @@ -391,26 +397,29 @@ let rec execute env sigma cstr = | Lambda (name,c1,c2) -> let sigma, j = execute env sigma c1 in let sigma, var = type_judgment env sigma j in - let env1 = push_rel (LocalAssum (name, var.utj_val)) env in + let () = check_binder_annot env var.utj_type name in + let env1 = push_rel (LocalAssum (name, var.utj_val)) env in let sigma, j' = execute env1 sigma c2 in - sigma, judge_of_abstraction env1 name var j' + sigma, judge_of_abstraction env1 name.binder_name var j' | Prod (name,c1,c2) -> let sigma, j = execute env sigma c1 in let sigma, varj = type_judgment env sigma j in - let env1 = push_rel (LocalAssum (name, varj.utj_val)) env in + let () = check_binder_annot env varj.utj_type name in + let env1 = push_rel (LocalAssum (name, varj.utj_val)) env in let sigma, j' = execute env1 sigma c2 in let sigma, varj' = type_judgment env1 sigma j' in - sigma, judge_of_product env name varj varj' + sigma, judge_of_product env name.binder_name varj varj' | LetIn (name,c1,c2,c3) -> let sigma, j1 = execute env sigma c1 in let sigma, j2 = execute env sigma c2 in let sigma, j2 = type_judgment env sigma j2 in let sigma, _ = judge_of_cast env sigma j1 DEFAULTcast j2 in + let () = check_binder_annot env j2.utj_type name in let env1 = push_rel (LocalDef (name, j1.uj_val, j2.utj_val)) env in let sigma, j3 = execute env1 sigma c3 in - sigma, judge_of_letin env name j1 j2 j3 + sigma, judge_of_letin env name.binder_name j1 j2 j3 | Cast (c,k,t) -> let sigma, cj = execute env sigma c in -- cgit v1.2.3 From 06b29ed748a9d9b99c2c08a3788906dbad5417d2 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 11 Jun 2018 13:57:28 +0200 Subject: Repair relevance marks in-kernel. Prevent errors when under annotating binders. --- pretyping/typing.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'pretyping/typing.ml') diff --git a/pretyping/typing.ml b/pretyping/typing.ml index b660973cdd..89f72c874b 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -397,7 +397,7 @@ let rec execute env sigma cstr = | Lambda (name,c1,c2) -> let sigma, j = execute env sigma c1 in let sigma, var = type_judgment env sigma j in - let () = check_binder_annot env var.utj_type name in + let name = check_binder_annot var.utj_type name in let env1 = push_rel (LocalAssum (name, var.utj_val)) env in let sigma, j' = execute env1 sigma c2 in sigma, judge_of_abstraction env1 name.binder_name var j' @@ -405,7 +405,7 @@ let rec execute env sigma cstr = | Prod (name,c1,c2) -> let sigma, j = execute env sigma c1 in let sigma, varj = type_judgment env sigma j in - let () = check_binder_annot env varj.utj_type name in + let name = check_binder_annot varj.utj_type name in let env1 = push_rel (LocalAssum (name, varj.utj_val)) env in let sigma, j' = execute env1 sigma c2 in let sigma, varj' = type_judgment env1 sigma j' in @@ -416,7 +416,7 @@ let rec execute env sigma cstr = let sigma, j2 = execute env sigma c2 in let sigma, j2 = type_judgment env sigma j2 in let sigma, _ = judge_of_cast env sigma j1 DEFAULTcast j2 in - let () = check_binder_annot env j2.utj_type name in + let name = check_binder_annot j2.utj_type name in let env1 = push_rel (LocalDef (name, j1.uj_val, j2.utj_val)) env in let sigma, j3 = execute env1 sigma c3 in sigma, judge_of_letin env name.binder_name j1 j2 j3 -- cgit v1.2.3