diff options
| author | Jakob L. Kreuze | 2023-05-03 10:35:21 -0400 |
|---|---|---|
| committer | Jakob L. Kreuze | 2023-05-03 10:35:21 -0400 |
| commit | 725d02db071b79ab9007fdd9c38656b3eedd8edf (patch) | |
| tree | 88e00baa2f17a2431ccec87ea54b0cc95e719c5e | |
| parent | f33cf0df9d2902d43c53e38549234ec91508a0c4 (diff) | |
Recurse on <lean-compare>
| -rw-r--r-- | compiler/lean.scm | 9 | ||||
| -rw-r--r-- | compiler/passes/bool-to-prop.scm | 3 |
2 files changed, 11 insertions, 1 deletions
diff --git a/compiler/lean.scm b/compiler/lean.scm index fdbd235..6cd52b7 100644 --- a/compiler/lean.scm +++ b/compiler/lean.scm @@ -106,6 +106,15 @@ (right #:init-keyword #:right #:getter right)) +(define-method (tree-map (form <lean-compare>) f scope breadcrumb) + (match form + (($ <lean-compare> kind left right) + (let ((new (make <lean-compare> + #:kind kind + #:left (tree-map left f scope breadcrumb) + #:right (tree-map right f scope breadcrumb)))) + (f scope breadcrumb new))))) + ;; Expression arising from a call to computable Lean function (define-class <lean-funcall> (<lean-expression>) (name #:init-keyword #:name diff --git a/compiler/passes/bool-to-prop.scm b/compiler/passes/bool-to-prop.scm index 0dd81d5..6f82761 100644 --- a/compiler/passes/bool-to-prop.scm +++ b/compiler/passes/bool-to-prop.scm @@ -35,7 +35,8 @@ (make <lean-compare> #:kind 'eq #:left form - #:right (make <constant> #:value #t))))) + #:right (make <constant> #:value #t))) + (_ form))) (policy-map policy (lambda (scope breadcrumb form) |