diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-16 15:26:07 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-16 15:26:50 +0200 |
commit | 568aa9dff652d420e66cda7914d4bc265bb276e7 (patch) | |
tree | c493eaaa87636e304f5788136a5fd1c255816821 /checker | |
parent | bce318b6d991587773ef2fb18c83de8d24bc4a5f (diff) | |
parent | 2d4701b4d1bdb0fb4f64dec9ffbd9ad90506ba26 (diff) |
Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.
Diffstat (limited to 'checker')
-rw-r--r-- | checker/cic.mli | 15 | ||||
-rw-r--r-- | checker/values.ml | 11 |
2 files changed, 22 insertions, 4 deletions
diff --git a/checker/cic.mli b/checker/cic.mli index 00ac2f56c..469cf8d4c 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -212,6 +212,15 @@ type constant_def = type constant_universes = Univ.universe_context +(** The [typing_flags] are instructions to the type-checker which + modify its behaviour. The typing flags used in the type-checking + of a constant are tracked in their {!constant_body} so that they + can be displayed to the user. *) +type typing_flags = { + check_guarded : bool; (** If [false] then fixed points and co-fixed + points are assumed to be total. *) +} + type constant_body = { const_hyps : section_context; (** New: younger hyp at top *) const_body : constant_def; @@ -220,7 +229,9 @@ type constant_body = { const_polymorphic : bool; (** Is it polymorphic or not *) const_universes : constant_universes; const_proj : projection_body option; - const_inline_code : bool } + const_inline_code : bool; + const_typing_flags : typing_flags; +} (** {6 Representation of mutual inductive types } *) @@ -316,6 +327,8 @@ type mutual_inductive_body = { mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) + mind_checked_positive : bool; (** [false] when the mutual-inductive was assumed to be well-founded, bypassing the positivity checker. *) + (** {8 Data for native compilation } *) mind_native_name : native_name ref; (** status of the code (linked or not, and where) *) diff --git a/checker/values.ml b/checker/values.ml index 19cbb5060..dd29f6fbe 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -13,7 +13,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 9f7fd499f812b6548a55f7067e6a9d06 checker/cic.mli +MD5 7d7963269852d32324e10aa77beb938d checker/cic.mli *) @@ -213,6 +213,9 @@ let v_projbody = v_tuple "proj_eta" [|v_constr;v_constr|]; v_constr|] +let v_typing_flags = + v_tuple "typing_flags" [|v_bool|] + let v_cb = v_tuple "constant_body" [|v_section_ctxt; v_cst_def; @@ -221,7 +224,8 @@ let v_cb = v_tuple "constant_body" v_bool; v_context; Opt v_projbody; - v_bool|] + v_bool; + v_typing_flags|] let v_recarg = v_sum "recarg" 1 (* Norec *) [|[|v_ind|] (* Mrec *);[|v_ind|] (* Imbr *)|] @@ -270,7 +274,8 @@ let v_ind_pack = v_tuple "mutual_inductive_body" v_rctxt; v_bool; v_context; - Opt v_bool|] + Opt v_bool; + v_bool|] let v_with = Sum ("with_declaration_body",0, |