diff options
| author | Gaëtan Gilbert | 2017-10-27 14:03:51 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-14 13:27:38 +0100 |
| commit | 75508769762372043387c67a9abe94e8f940e80a (patch) | |
| tree | 3f63e7790e9f3b6e7384b0a445d62cfa7edbe829 /checker | |
| parent | a0e16c9e5c3f88a8b72935dd4877f13388640f69 (diff) | |
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.
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/checker.ml | 2 | ||||
| -rw-r--r-- | checker/values.ml | 8 |
2 files changed, 6 insertions, 4 deletions
diff --git a/checker/checker.ml b/checker/checker.ml index d3f346d76b..205a3984d5 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -146,6 +146,7 @@ let make_senv () = let senv = Safe_typing.set_engagement !impredicative_set senv in let senv = Safe_typing.set_indices_matter !indices_matter senv in let senv = Safe_typing.set_VM false senv in + let senv = Safe_typing.set_allow_sprop true senv in (* be smarter later *) Safe_typing.set_native_compiler false senv let admit_list = ref ([] : object_file list) @@ -296,6 +297,7 @@ let explain_exn = function | IllFormedRecBody _ -> str"IllFormedRecBody" | IllTypedRecBody _ -> str"IllTypedRecBody" | UnsatisfiedConstraints _ -> str"UnsatisfiedConstraints" + | DisallowedSProp -> str"DisallowedSProp" | UndeclaredUniverse _ -> str"UndeclaredUniverse")) | InductiveError e -> 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|] |