Validate every inductive and constructor in an inductive block.
(
&mut self,
block: &KId<M>,
members: &[KId<M>],
)
| 96 | |
| 97 | /// Validate every inductive and constructor in an inductive block. |
| 98 | pub(crate) fn check_inductive_block( |
| 99 | &mut self, |
| 100 | block: &KId<M>, |
| 101 | members: &[KId<M>], |
| 102 | ) -> Result<(), TcError<M>> { |
| 103 | let mut ind_ids = Vec::new(); |
| 104 | let mut ctor_ids = Vec::new(); |
| 105 | |
| 106 | for member in members { |
| 107 | self.reset(); |
| 108 | self.begin_const(member); |
| 109 | let c = self.get_const(member)?; |
| 110 | self.validate_const_well_scoped(&c)?; |
| 111 | match c { |
| 112 | KConst::Indc { ty, .. } => { |
| 113 | let t = self.infer(&ty)?; |
| 114 | self.ensure_sort(&t)?; |
| 115 | ind_ids.push(member.clone()); |
| 116 | }, |
| 117 | KConst::Ctor { ty, .. } => { |
| 118 | let t = self.infer(&ty)?; |
| 119 | self.ensure_sort(&t)?; |
| 120 | ctor_ids.push(member.clone()); |
| 121 | }, |
| 122 | _ => { |
| 123 | return Err(TcError::Other(format!( |
| 124 | "check_inductive_block: non-inductive member {member} in block {block}" |
| 125 | ))); |
| 126 | }, |
| 127 | } |
| 128 | } |
| 129 | |
| 130 | for ind_id in &ind_ids { |
| 131 | self.reset(); |
| 132 | self.begin_const(ind_id); |
| 133 | self.check_inductive_member(ind_id)?; |
| 134 | } |
| 135 | for ctor_id in &ctor_ids { |
| 136 | let induct = match self.get_const(ctor_id)? { |
| 137 | KConst::Ctor { induct, .. } => induct, |
| 138 | _ => continue, |
| 139 | }; |
| 140 | self.reset(); |
| 141 | self.begin_const(ctor_id); |
| 142 | self.check_ctor_against_inductive_member(ctor_id, &induct)?; |
| 143 | } |
| 144 | Ok(()) |
| 145 | } |
| 146 | |
| 147 | /// Validate an inductive type and its constructors. |
| 148 | pub fn check_inductive_member( |
no test coverage detected