diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-07-24 14:27:48 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-07-24 14:27:48 +0100 |
| commit | 5d5807f215805f1e235a0ad0546f995dd19a6767 (patch) | |
| tree | ca5a8cc4f7349e0ce3d595b05acfb73925f6d7b8 | |
| parent | 29a05f990dd945be30995c4f46b91b5f7c83abd9 (diff) | |
Compile to local constant function.
| -rw-r--r-- | src/Term/Compile.idr | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/src/Term/Compile.idr b/src/Term/Compile.idr index 2779ee3..dd423ae 100644 --- a/src/Term/Compile.idr +++ b/src/Term/Compile.idr @@ -15,7 +15,7 @@ import Term.Syntax %prefix_record_projections off const_ : Doc ann -const_ = "const" +const_ = "squid-const" rec_ : Doc ann rec_ = "squid-rec" @@ -62,15 +62,15 @@ parameters (names : Stream String) parens $ group $ hang 2 $ const_ <+> line <+> compileFullTerm t thin - -- compileFullTerm (Abs Var) thin = identity_ + compileFullTerm (Abs Var) thin = identity_ compileFullTerm (Abs t) thin = parens $ group $ hang 2 $ lambda <++> (parens $ pretty $ index (lenToNat len) names) <+> line <+> compileFullTerm t (Keep thin) - -- compileFullTerm (App (MakePair (Const t `Over` thin1) (u `Over` thin2) _)) thin = - -- compileFullTerm t (thin . thin1) - -- compileFullTerm (App (MakePair (Abs Var `Over` thin1) (u `Over` thin2) _)) thin = - -- compileFullTerm u (thin . thin2) + compileFullTerm (App (MakePair (Const t `Over` thin1) (u `Over` thin2) _)) thin = + compileFullTerm t (thin . thin1) + compileFullTerm (App (MakePair (Abs Var `Over` thin1) (u `Over` thin2) _)) thin = + compileFullTerm u (thin . thin2) compileFullTerm (App (MakePair (t `Over` thin1) (u `Over` thin2) _)) thin = parens $ group $ align $ compileFullTerm t (thin . thin1) <+> line <+> @@ -141,6 +141,7 @@ builtins = """ (define (squid-div m) (lambda (n) (euclidean-quotient m n))) (define (squid-mod m) (lambda (n) (euclidean-remainder m n))) (define (squid-identity x) x) + (define (squid-const x) (lambda (_) x)) """ wrap_main : Len ctx => Term ty ctx -> Doc ann |