Remove build1

1 files changed, 16 insertions, 7 deletions

diff --git a/src/Language.hs b/src/Language.hs
index a1b3d8b..e8dc89f 100644
--- a/src/Language.hs
+++ b/src/Language.hs
@@ -3,6 +3,7 @@
 {-# LANGUAGE OverloadedLabels #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeApplications #-}
 module Language (
   fromNamed,
   NExpr,
@@ -65,7 +66,18 @@ constArr_ x =
        Dict -> NEConstArr knownNat ty x
 
 build1 :: NExpr env TIx -> (Var name TIx :-> NExpr ('(name, TIx) : env) t) -> NExpr env (TArr (S Z) t)
-build1 a (v :-> b) = NEBuild1 a v b
+build1 a (v :-> b) = NEBuild (SS SZ) (pair nil a) #idx (let_ v (snd_ #idx) (NEDrop (SS SZ) b))
+
+build2 :: NExpr env TIx -> NExpr env TIx
+       -> (Var name1 TIx :-> Var name2 TIx :-> NExpr ('(name2, TIx) : '(name1, TIx) : env) t)
+       -> NExpr env (TArr (S (S Z)) t)
+build2 a1 a2 (v1 :-> v2 :-> b) =
+  NEBuild (SS (SS SZ))
+          (pair (pair nil a1) a2)
+          #idx
+          (let_ v1 (snd_ (fst_ #idx)) $
+           let_ v2 (NEDrop SZ (snd_ #idx)) $
+             NEDrop (SS (SS SZ)) b)
 
 build :: SNat n -> NExpr env (Tup (Replicate n TIx)) -> (Var name (Tup (Replicate n TIx)) :-> NExpr ('(name, Tup (Replicate n TIx)) : env) t) -> NExpr env (TArr n t)
 build n a (v :-> b) = NEBuild n a v b
@@ -131,9 +143,6 @@ infix 4 .>=
 not_ :: NExpr env (TScal TBool) -> NExpr env (TScal TBool)
 not_ = oper ONot
 
--- | The "_" variables in scope are unusable and should be ignored. With a
--- weakening function on NExprs they could be hidden.
---
--- The first alternative is the True case; the second is the False case.
-if_ :: NExpr env (TScal TBool) -> NExpr ('("_", TNil) : env) t -> NExpr ('("_", TNil) : env) t -> NExpr env t
-if_ e a b = case_ (oper OIf e) (#_ :-> a) (#_ :-> b)
+-- | The first alternative is the True case; the second is the False case.
+if_ :: NExpr env (TScal TBool) -> NExpr env t -> NExpr env t -> NExpr env t
+if_ e a b = case_ (oper OIf e) (#_ :-> NEDrop SZ a) (#_ :-> NEDrop SZ b)