diff options
Diffstat (limited to 'src/Language.hs')
| -rw-r--r-- | src/Language.hs | 23 |
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) |