diff options
| -rw-r--r-- | backends/lean/Base/Diverge/Elab.lean | 25 |
1 files changed, 19 insertions, 6 deletions
diff --git a/backends/lean/Base/Diverge/Elab.lean b/backends/lean/Base/Diverge/Elab.lean index cf40ea8f..063480a2 100644 --- a/backends/lean/Base/Diverge/Elab.lean +++ b/backends/lean/Base/Diverge/Elab.lean @@ -378,17 +378,22 @@ mutual partial def proveExprIsValid (k_var kk_var : Expr) (e : Expr) : MetaM Expr := do trace[Diverge.def.valid] "proveValid: {e}" match e with + | .const _ _ => throwError "Unimplemented" -- Shouldn't get there? | .bvar _ | .fvar _ - | .mvar _ - | .sort _ | .lit _ - | .const _ _ => throwError "Unimplemented" + | .mvar _ + | .sort _ => throwError "Unreachable" | .lam .. => throwError "Unimplemented" | .forallE .. => throwError "Unreachable" -- Shouldn't get there - | .letE .. => throwError "TODO" - -- lambdaLetTelescope e fun xs b => mapVisitBinders xs do - -- mkLambdaFVars xs (← mapVisit k b) (usedLetOnly := false) + | .letE dName dTy dValue body _nonDep => do + -- Introduce a local declaration for the let-binding + withLetDecl dName dTy dValue fun decl => do + let isValid ← proveExprIsValid k_var kk_var body + -- Add the let-binding around (rem.: the let-binding should be + -- *inside* the `is_valid_p`, not outside, but because it reduces + -- in the end it doesn't matter) + mkLetFVars #[decl] isValid | .mdata _ b => proveExprIsValid k_var kk_var b | .proj _ _ _ => -- The projection shouldn't use the continuation @@ -963,4 +968,12 @@ mutual if i > 20 then foo (i / 20) else .ret 42 end +-- Testing dependent branching and let-bindings +-- TODO: why the linter warning? +divergent def is_non_zero (i : Int) : Result Bool := + if _h:i = 0 then return false + else + let b := true + return b + end Diverge |