diff options
Diffstat (limited to 'backends/lean/Base/Diverge/Elab.lean')
| -rw-r--r-- | backends/lean/Base/Diverge/Elab.lean | 47 |
1 files changed, 40 insertions, 7 deletions
diff --git a/backends/lean/Base/Diverge/Elab.lean b/backends/lean/Base/Diverge/Elab.lean index ff680c07..6115b13b 100644 --- a/backends/lean/Base/Diverge/Elab.lean +++ b/backends/lean/Base/Diverge/Elab.lean @@ -17,6 +17,8 @@ syntax (name := divergentDef) open Lean Elab Term Meta Primitives Lean.Meta open Utils +def normalize_let_bindings := true + /- The following was copied from the `wfRecursion` function. -/ open WF in @@ -649,6 +651,15 @@ mutual -/ partial def proveExprIsValid (k_var kk_var : Expr) (e : Expr) : MetaM Expr := do trace[Diverge.def.valid] "proveExprIsValid: {e}" + -- Normalize to eliminate the lambdas - TODO: this is slightly dangerous. + let e ← do + if e.isLet ∧ normalize_let_bindings then do + let updt_config config := + { config with transparency := .reducible, zetaNonDep := false } + let e ← withConfig updt_config (whnf e) + trace[Diverge.def.valid] "e (after normalization): {e}" + pure e + else pure e match e with | .const _ _ => throwError "Unimplemented" -- Shouldn't get there? | .bvar _ @@ -659,6 +670,7 @@ partial def proveExprIsValid (k_var kk_var : Expr) (e : Expr) : MetaM Expr := do | .lam .. => throwError "Unimplemented" -- TODO | .forallE .. => throwError "Unreachable" -- Shouldn't get there | .letE .. => do + -- Remark: this branch is not taken if we normalize the expressions (above) -- Telescope all the let-bindings (remark: this also telescopes the lambdas) lambdaLetTelescope e fun xs body => do -- Note that we don't visit the bound values: there shouldn't be @@ -919,7 +931,7 @@ partial def proveAppIsValidApplyThms (k_var kk_var : Expr) (e : Expr) let updt_config config := { config with transparency := .reducible, zetaNonDep := false } withConfig updt_config (whnf e) - trace[Diverge.def.valid] "e (after reduction): {e}" + trace[Diverge.def.valid] "e (after normalization): {e}" let e_valid ← proveExprIsValid k_var kk_var e trace[Diverge.def.valid] "e_valid (for e): {e_valid}" let e_valid ← mkLambdaFVars forall_vars e_valid @@ -1018,6 +1030,7 @@ partial def proveSingleBodyIsValid let thmTy ← mkAppM ``FixII.is_valid_p #[k_var, bodyApp] trace[Diverge.def.valid] "thmTy: {thmTy}" -- Prove that the body is valid + trace[Diverge.def.valid] "body: {body}" let proof ← proveExprIsValid k_var kk_var body let proof ← mkLambdaFVars #[k_var, t_var, x_var] proof trace[Diverge.def.valid] "proveSingleBodyIsValid: proof:\n{proof}:\n{← inferType proof}" @@ -1599,10 +1612,6 @@ namespace Tests #check id2.unfold - --set_option trace.Diverge.def true - --set_option trace.Diverge.def.genBody true - --set_option trace.Diverge.def.valid true - --set_option trace.Diverge.def.genBody.visit true divergent def incr (t : Tree Nat) : Result (Tree Nat) := match t with | .leaf x => .ret (.leaf (x + 1)) @@ -1611,9 +1620,33 @@ namespace Tests let tl ← map incr tl .ret (.node tl) - --set_option trace.Diverge false + -- We handle this by inlining the let-binding + divergent def id3 (t : Tree Nat) : Result (Tree Nat) := + match t with + | .leaf x => .ret (.leaf (x + 1)) + | .node tl => + do + let f := id3 + let tl ← map f tl + .ret (.node tl) + + #check id3.unfold + + /- + -- This is not handled yet: we can only do it if we introduce "general" + -- relations for the input types and output types (result_rel should + -- be parameterized by something). + divergent def id4 (t : Tree Nat) : Result (Tree Nat) := + match t with + | .leaf x => .ret (.leaf (x + 1)) + | .node tl => + do + let f ← .ret id4 + let tl ← map f tl + .ret (.node tl) - #check incr.unfold + #check id4.unfold + -/ end HigherOrder |