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. --- checker/values.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'checker/values.ml') diff --git a/checker/values.ml b/checker/values.ml index bcac3014be..f2b961ef56 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -95,9 +95,9 @@ let v_cons = v_tuple "constructor" [|v_ind;Int|] (** kernel/univ *) let v_level_global = v_tuple "Level.Global.t" [|v_dp;Int|] -let v_raw_level = v_sum "raw_level" 2 (* Prop, Set *) +let v_raw_level = v_sum "raw_level" 3 (* SProp, Prop, Set *) [|(*Level*)[|v_level_global|]; (*Var*)[|Int|]|] -let v_level = v_tuple "level" [|Int;v_raw_level|] +let v_level = v_tuple "level" [|Int;v_raw_level|] let v_expr = v_tuple "levelexpr" [|v_level;Int|] let v_univ = List v_expr @@ -116,8 +116,8 @@ let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|] (** kernel/term *) -let v_sort = v_sum "sort" 2 (*Prop, Set*) [|[|v_univ(*Type*)|]|] -let v_sortfam = v_enum "sorts_family" 3 +let v_sort = v_sum "sort" 3 (*SProp, Prop, Set*) [|[|v_univ(*Type*)|]|] +let v_sortfam = v_enum "sorts_family" 4 let v_puniverses v = v_tuple "punivs" [|v;v_instance|] -- 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. --- checker/values.ml | 22 ++++++++++++++-------- 1 file changed, 14 insertions(+), 8 deletions(-) (limited to 'checker/values.ml') diff --git a/checker/values.ml b/checker/values.ml index f2b961ef56..5cbf0ff298 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -119,6 +119,9 @@ let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|] let v_sort = v_sum "sort" 3 (*SProp, Prop, Set*) [|[|v_univ(*Type*)|]|] let v_sortfam = v_enum "sorts_family" 4 +let v_relevance = v_sum "relevance" 2 [||] +let v_binder_annot x = v_tuple "binder_annot" [|x;v_relevance|] + let v_puniverses v = v_tuple "punivs" [|v;v_instance|] let v_boollist = List v_bool @@ -126,7 +129,7 @@ let v_boollist = List v_bool let v_caseinfo = let v_cstyle = v_enum "case_style" 5 in let v_cprint = v_tuple "case_printing" [|v_boollist;Array v_boollist;v_cstyle|] in - v_tuple "case_info" [|v_ind;Int;Array Int;Array Int;v_cprint|] + v_tuple "case_info" [|v_ind;Int;Array Int;Array Int;v_relevance;v_cprint|] let v_cast = v_enum "cast_kind" 4 @@ -141,9 +144,9 @@ let rec v_constr = [|Fail "Evar"|]; (* Evar *) [|v_sort|]; (* Sort *) [|v_constr;v_cast;v_constr|]; (* Cast *) - [|v_name;v_constr;v_constr|]; (* Prod *) - [|v_name;v_constr;v_constr|]; (* Lambda *) - [|v_name;v_constr;v_constr;v_constr|]; (* LetIn *) + [|v_binder_annot v_name;v_constr;v_constr|]; (* Prod *) + [|v_binder_annot v_name;v_constr;v_constr|]; (* Lambda *) + [|v_binder_annot v_name;v_constr;v_constr;v_constr|]; (* LetIn *) [|v_constr;Array v_constr|]; (* App *) [|v_puniverses v_cst|]; (* Const *) [|v_puniverses v_ind|]; (* Ind *) @@ -156,12 +159,13 @@ let rec v_constr = |]) and v_prec = Tuple ("prec_declaration", - [|Array v_name; Array v_constr; Array v_constr|]) + [|Array (v_binder_annot v_name); Array v_constr; Array v_constr|]) and v_fix = Tuple ("pfixpoint", [|Tuple ("fix2",[|Array Int;Int|]);v_prec|]) and v_cofix = Tuple ("pcofixpoint",[|Int;v_prec|]) -let v_rdecl = v_sum "rel_declaration" 0 [| [|v_name; v_constr|]; (* LocalAssum *) - [|v_name; v_constr; v_constr|] |] (* LocalDef *) +let v_rdecl = v_sum "rel_declaration" 0 + [| [|v_binder_annot v_name; v_constr|]; (* LocalAssum *) + [|v_binder_annot v_name; v_constr; v_constr|] |] (* LocalDef *) let v_rctxt = List v_rdecl let v_section_ctxt = v_enum "emptylist" 1 @@ -231,6 +235,7 @@ let v_cb = v_tuple "constant_body" [|v_section_ctxt; v_cst_def; v_constr; + v_relevance; Any; v_univs; Opt v_context_set; @@ -265,6 +270,7 @@ let v_one_ind = v_tuple "one_inductive_body" Array Int; Array Int; v_wfp; + v_relevance; Int; Int; Any|] @@ -273,7 +279,7 @@ let v_finite = v_enum "recursivity_kind" 3 let v_record_info = v_sum "record_info" 2 - [| [| Array (v_tuple "record" [| v_id; Array v_id; Array v_constr |]) |] |] + [| [| Array (v_tuple "record" [| v_id; Array v_id; Array v_relevance; Array v_constr |]) |] |] let v_ind_pack = v_tuple "mutual_inductive_body" [|Array v_one_ind; -- cgit v1.2.3