(
&mut self,
id: &KId<M>,
c: &KConst<M>,
)
| 99 | } |
| 100 | |
| 101 | fn check_const_member( |
| 102 | &mut self, |
| 103 | id: &KId<M>, |
| 104 | c: &KConst<M>, |
| 105 | ) -> Result<(), TcError<M>> |
| 106 | where |
| 107 | M::MField<Vec<ix_common::env::Name>>: CheckDupLevelParams, |
| 108 | { |
| 109 | let phase_timing = *IX_PHASE_TIMING; |
| 110 | let overall = if phase_timing { Some(Instant::now()) } else { None }; |
| 111 | |
| 112 | let dup_start = overall.map(|_| Instant::now()); |
| 113 | if c.level_params().has_duplicate_level_params() { |
| 114 | return Err(TcError::Other("duplicate universe level parameter".into())); |
| 115 | } |
| 116 | let dup_elapsed = dup_start.map(|s| s.elapsed()); |
| 117 | |
| 118 | let mut validation_timing = ValidationTiming::default(); |
| 119 | let validate_start = overall.map(|_| Instant::now()); |
| 120 | if phase_timing { |
| 121 | self.validate_const_well_scoped_timed(c, Some(&mut validation_timing))?; |
| 122 | } else { |
| 123 | self.validate_const_well_scoped(c)?; |
| 124 | } |
| 125 | let validate_elapsed = validate_start.map(|s| s.elapsed()); |
| 126 | |
| 127 | match &c { |
| 128 | KConst::Axio { ty, .. } => { |
| 129 | let t = self.infer(ty)?; |
| 130 | self.ensure_sort(&t)?; |
| 131 | Ok(()) |
| 132 | }, |
| 133 | |
| 134 | KConst::Defn { ty, val, safety, kind, .. } => { |
| 135 | let t_infer_ty_start = overall.map(|_| Instant::now()); |
| 136 | let t = self.infer(ty)?; |
| 137 | let lvl = self.ensure_sort(&t)?; |
| 138 | let infer_ty_elapsed = t_infer_ty_start.map(|s| s.elapsed()); |
| 139 | |
| 140 | // Theorems must have types in Prop (Sort 0) |
| 141 | if *kind == DefKind::Theorem && !univ_eq(&lvl, &KUniv::zero()) { |
| 142 | return Err(TcError::Other( |
| 143 | "theorem type must be a proposition (Sort 0)".into(), |
| 144 | )); |
| 145 | } |
| 146 | |
| 147 | let t_infer_val_start = overall.map(|_| Instant::now()); |
| 148 | let val_ty = self.infer(val)?; |
| 149 | let infer_val_elapsed = t_infer_val_start.map(|s| s.elapsed()); |
| 150 | |
| 151 | let t_def_eq_start = overall.map(|_| Instant::now()); |
| 152 | let def_eq_ok = self.is_def_eq(&val_ty, ty)?; |
| 153 | let def_eq_elapsed = t_def_eq_start.map(|s| s.elapsed()); |
| 154 | |
| 155 | if !def_eq_ok { |
| 156 | if *IX_DECL_DIFF && self.debug_label_matches_env() { |
| 157 | // Post-whnf forms on both sides so we can see where |
| 158 | // reduction terminates and hence which reduction rule |
no test coverage detected