github/semantic
1
1
Fork 0
mirror of https://github.com/github/semantic.git synced 2024-12-27 00:44:57 +03:00
Code Issues Projects Releases Wiki Activity

Define a smart constructor for Lam binding with Fin.

Browse Source
This commit is contained in:
Rob Rix 2019-11-04 16:29:08 -05:00
parent ea2b679049
commit 4811adddae
No known key found for this signature in database
GPG Key ID: F188A01508EA1CF7
1 changed files with 7 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
semantic-analysis/src/Analysis/Intro.hs
View File

@ -1,10 +1,11 @@
{-# LANGUAGE DeriveGeneric, DeriveTraversable, FlexibleContexts, GeneralizedNewtypeDeriving, QuantifiedConstraints, StandaloneDeriving #-} {-# LANGUAGE DataKinds, DeriveGeneric, DeriveTraversable, FlexibleContexts, GeneralizedNewtypeDeriving, QuantifiedConstraints, StandaloneDeriving #-}
module Analysis.Intro module Analysis.Intro
( unit ( unit
, bool , bool
, string , string
, record , record
, lam , lam
, lamFin
, lams , lams
, unlam , unlam
, Intro(..) , Intro(..)
@ -16,9 +17,11 @@ import Control.Effect.Carrier
import Data.String (IsString) import Data.String (IsString)
import Data.Text (Text) import Data.Text (Text)
import GHC.Generics (Generic1) import GHC.Generics (Generic1)
import Syntax.Fin
import Syntax.Module import Syntax.Module
import Syntax.Scope import Syntax.Scope
import Syntax.Term import Syntax.Term
import Syntax.Var
unit :: (Carrier sig m, Member Intro sig) => m a unit :: (Carrier sig m, Member Intro sig) => m a
unit = send Unit unit = send Unit
@ -35,6 +38,9 @@ record fs = send (Record fs)
lam :: (Eq a, Carrier sig m, Member Intro sig) => Maybe Name -> a -> m a -> m a lam :: (Eq a, Carrier sig m, Member Intro sig) => Maybe Name -> a -> m a -> m a
lam u n b = send (Lam u (abstract1 n b)) lam u n b = send (Lam u (abstract1 n b))
lamFin :: (Carrier sig m, Member Intro sig) => Maybe Name -> m (Var (Fin ('S n)) a) -> m (Var (Fin n) a)
lamFin u b = send (Lam u (toScopeFin b))
lams :: (Eq a, Foldable t, Carrier sig m, Member Intro sig) => t (Maybe Name, a) -> m a -> m a lams :: (Eq a, Foldable t, Carrier sig m, Member Intro sig) => t (Maybe Name, a) -> m a -> m a
lams names body = foldr (uncurry lam) body names lams names body = foldr (uncurry lam) body names