From a385d1225d92fd7e342f1c1ba358e017c37a2def Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Sun, 14 Jul 2024 16:48:11 -0700
Subject: [PATCH] wip compile, drop let

---
 src/Lib/Check.idr   |  1 -
 src/Lib/Compile.idr | 26 ++++++++++++++++++++++++++
 src/Lib/TT.idr      |  1 -
 src/Lib/Types.idr   |  4 ----
 4 files changed, 26 insertions(+), 6 deletions(-)
 create mode 100644 src/Lib/Compile.idr

diff --git a/src/Lib/Check.idr b/src/Lib/Check.idr
index de4d836..10bf8ab 100644
--- a/src/Lib/Check.idr
+++ b/src/Lib/Check.idr
@@ -19,7 +19,6 @@ data PRen = PR Nat Nat (List Nat)
 -- IORef for metas needs IO
 
 forceMeta : Val -> M Val
--- TODO - need to look up metas
 forceMeta (VMeta ix sp) = case !(lookupMeta ix) of
   (Unsolved pos k xs) => pure (VMeta ix sp)
   (Solved k t) => vappSpine t sp
diff --git a/src/Lib/Compile.idr b/src/Lib/Compile.idr
new file mode 100644
index 0000000..ea7eca0
--- /dev/null
+++ b/src/Lib/Compile.idr
@@ -0,0 +1,26 @@
+module Lib.Compile
+
+import Lib.Types
+import Lib.Prettier
+
+-- turn Tm into javscript
+
+
+-- JS AST (or just write a Doc?)
+
+data JSExp : Type where
+
+data JSStmt : Type where
+
+compile : Nat -> Tm -> Doc
+-- Oh, we don't have local names...
+compile l (Bnd k) = text "_\{show k}"
+-- this is tied to Bnd
+-- And we probably want `{...}` with statements...
+compile l (Lam str t) = text "(_\{show l}) => " <+> compile (S l) t
+compile l (Ref str mt) = text str
+compile l (App t u) = compile l t <+> "(" <+> compile l u <+> ")"
+
+compile l U = "undefined"
+compile l (Pi str icit t u) = "undefined"
+compile l (Meta k) = ?fixme_zonk
diff --git a/src/Lib/TT.idr b/src/Lib/TT.idr
index 2b80673..f73c7fd 100644
--- a/src/Lib/TT.idr
+++ b/src/Lib/TT.idr
@@ -159,7 +159,6 @@ eval env mode (Meta i) =
         (Solved k t) => pure $ t
 eval env mode (Lam x t) = pure $ VLam x (MkClosure env t)
 eval env mode (Pi x icit a b) = pure $ VPi x icit !(eval env mode a) (MkClosure env b)
-eval env mode (Let x ty t u) = eval (!(eval env mode t) :: env) mode u
 eval env mode (Bnd i) = case getAt i env of
   Just rval => pure rval
   Nothing => error' "Bad deBruin index \{show i}"
diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr
index e910f71..86585bd 100644
--- a/src/Lib/Types.idr
+++ b/src/Lib/Types.idr
@@ -49,7 +49,6 @@ data Tm : Type where
   App : Tm -> Tm -> Tm
   U   : Tm
   Pi  : Name -> Icit -> Tm -> Tm -> Tm
-  Let : Name -> Tm -> Tm -> Tm -> Tm
 
 %name Tm t, u, v
 
@@ -63,7 +62,6 @@ Show Tm where
   show U = "U"
   show (Pi str Implicit t u) = "(Pi (\{str} : \{show t}) => \{show u})"
   show (Pi str Explicit t u) = "(Pi {\{str} : \{show t}} => \{show u})"
-  show (Let str t u v) = "let \{str} : \{show t} = \{show u} in \{show v}"
 
 -- I can't really show val because it's HOAS...
 
@@ -84,7 +82,6 @@ Eq (Tm) where
   (App t u) == App t' u' = t == t' && u == u'
   U == U = True
   (Pi n icit t u) == (Pi n' icit' t' u') = icit == icit' && t == t' && u == u'
-  (Let n t u v) == (Let n' t' u' v') = t == t' && u == u' && v == v'
   _ == _ = False
 
 public export
@@ -96,7 +93,6 @@ Pretty Tm where
   pretty (App t u) = text "(" <+> pretty t <+> pretty u <+> ")"
   pretty U = "U"
   pretty (Pi str icit t u) = text "(" <+> text str <+> ":" <+> pretty t <+> "=>" <+> pretty u <+> ")"
-  pretty (Let str t u v) = text "let" <+> text str <+> ":" <+> pretty t <+> "=" <+> pretty u
 
 -- public export
 -- data Closure : Nat -> Type