Skip to content

Commit

Permalink
fix
Browse files Browse the repository at this point in the history
  • Loading branch information
digama0 committed Nov 24, 2024
1 parent a1bdfbb commit 47aaf9a
Show file tree
Hide file tree
Showing 2 changed files with 13 additions and 25 deletions.
31 changes: 11 additions & 20 deletions mm0-rs/src/mmc/proof/compiler.rs
Original file line number Diff line number Diff line change
Expand Up @@ -916,38 +916,29 @@ impl ProcProver<'_> {
th
}

/// Returns `(ty, |- okReadHypVCtx vctx ty)`
fn read_hyp_vctx_var(&mut self, vctx: &VCtx, v: VarId) -> (ProofId, ProofId) {
/// Returns `(ty, |- okReadHyp tctx ty)`
fn read_hyp_tctx_var(&mut self, (tctx, l1): P<&TCtx>, v: VarId) -> (ProofId, ProofId) {
// eprintln!("get {:?} in\n{}", v,
// format_to_string(|s| vctx.pp(&self.thm, self.elab, &self.vctxs, s)));
let (_, val, h1) = vctx.get(&mut self.thm, &self.vctxs, v);
let (_, val, h1) = tctx.vctx.get(&mut self.thm, &self.vctxs, v);
app_match!(self.thm, let (mkTCtx vctx n mctx) = l1);
app_match!(self.thm, val => {
(vHyp ty) => (ty, thm!(self.thm, (okReadHypVCtx[vctx.e, ty]) =>
okReadHypVCtxI(ty, vctx.e, h1))),
(vVar v ty) => (ty, thm!(self.thm, (okReadHypVCtx[vctx.e, ty]) =>
okReadHypVar(ty, v, vctx.e, h1))),
(vHyp ty) => (ty, thm!(self.thm, okReadHypHyp(mctx, n, ty, vctx, h1): okReadHyp[l1, ty])),
(vVar v ty) =>
(ty, thm!(self.thm, okReadHypVar(mctx, n, ty, v, vctx, h1): okReadHyp[l1, ty])),
})
}

/// Returns `(ty, |- okReadHypVCtx vctx ty)`
fn read_hyp_vctx_place(&mut self, vctx: &VCtx, p: &Place) -> (ProofId, ProofId) {
/// Returns `(ty, |- okReadHyp tctx ty)`
fn read_hyp_tctx_place(&mut self, tctx: P<&TCtx>, p: &Place) -> (ProofId, ProofId) {
assert!(p.proj.is_empty()); // TODO
self.read_hyp_vctx_var(vctx, p.local)
}

/// Given `ty`, `|- okReadHypVCtx vctx ty`, returns `|- okReadHyp tctx ty`
fn read_hyp_from_vctx(&mut self, tctx: ProofId, ty: ProofId, th: ProofId) -> ProofId {
app_match!(self.thm, let (mkTCtx vctx n mctx) = tctx);
thm!(self.thm, okReadHypI(mctx, n, ty, vctx, th): okReadHyp[tctx, ty]) // TODO
self.read_hyp_tctx_var(tctx, p.local)
}

/// Returns `(ty, |- okReadHyp tctx ty)`
fn read_hyp_operand(&mut self, (tctx, l1): P<&TCtx>, op: &Operand) -> (ProofId, ProofId) {
match op.place() {
Ok(p) => {
let (ty, th) = self.read_hyp_vctx_place(&tctx.vctx, p);
(ty, self.read_hyp_from_vctx(l1, ty, th))
}
Ok(p) => self.read_hyp_tctx_place((tctx, l1), p),
Err(c) => match c.k {
ConstKind::Unit => {
let ty = app!(self.thm, (tyUnit));
Expand Down
7 changes: 2 additions & 5 deletions mm0-rs/src/mmc/proof/predefs.rs
Original file line number Diff line number Diff line change
Expand Up @@ -575,12 +575,9 @@ make_predefs! {
okPushHyp: TermId => "okPushHyp";
okPushHypI: ThmId => "okPushHypI";

okReadHypVCtx: TermId => "okReadHypVCtx";
okReadHypVCtxI: ThmId => "okReadHypVCtxI";
okReadHypVar: ThmId => "okReadHypVar";

okReadHyp: TermId => "okReadHyp";
okReadHypI: ThmId => "okReadHypI";
okReadHypHyp: ThmId => "okReadHypHyp";
okReadHypVar: ThmId => "okReadHypVar";
okReadHyp_unit: ThmId => "okReadHyp_unit";

okAssembled: TermId => "okAssembled";
Expand Down

0 comments on commit 47aaf9a

Please sign in to comment.