diff --git a/.gitignore b/.gitignore index 0916e47f..9d731f0c 100644 --- a/.gitignore +++ b/.gitignore @@ -1,9 +1,15 @@ -haskell/free-foil/src/Language/LambdaPi/Syntax/Lex.hs -haskell/free-foil/src/Language/LambdaPi/Syntax/Par.hs -haskell/free-foil/src/Language/LambdaPi/Syntax/Test -haskell/free-foil/src/Language/LambdaPi/Syntax/Test.hs -haskell/free-foil/src/Language/LambdaPi/Syntax/Skel.hs -haskell/free-foil/src/Language/LambdaPi/Syntax/ErrM.hs +haskell/lambda-pi/src/Language/LambdaPi/Syntax/Lex.hs +haskell/lambda-pi/src/Language/LambdaPi/Syntax/Par.hs +haskell/lambda-pi/src/Language/LambdaPi/Syntax/Test +haskell/lambda-pi/src/Language/LambdaPi/Syntax/Test.hs +haskell/lambda-pi/src/Language/LambdaPi/Syntax/Skel.hs +haskell/lambda-pi/src/Language/LambdaPi/Syntax/ErrM.hs +haskell/soas/src/Language/SOAS/Syntax/Lex.hs +haskell/soas/src/Language/SOAS/Syntax/Par.hs +haskell/soas/src/Language/SOAS/Syntax/Test +haskell/soas/src/Language/SOAS/Syntax/Test.hs +haskell/soas/src/Language/SOAS/Syntax/Skel.hs +haskell/soas/src/Language/SOAS/Syntax/ErrM.hs scala/free-foil/src/main/scala/.scala-build/ diff --git a/haskell/free-foil/free-foil.cabal b/haskell/free-foil/free-foil.cabal index 7258708c..9c0e1886 100644 --- a/haskell/free-foil/free-foil.cabal +++ b/haskell/free-foil/free-foil.cabal @@ -43,6 +43,7 @@ library Control.Monad.Free.Foil.Generic Control.Monad.Free.Foil.TH Control.Monad.Free.Foil.TH.Convert + Control.Monad.Free.Foil.TH.MkFreeFoil Control.Monad.Free.Foil.TH.PatternSynonyms Control.Monad.Free.Foil.TH.Signature Control.Monad.Free.Foil.TH.ZipMatch diff --git a/haskell/free-foil/src/Control/Monad/Foil.hs b/haskell/free-foil/src/Control/Monad/Foil.hs index 788c3c89..70831de2 100644 --- a/haskell/free-foil/src/Control/Monad/Foil.hs +++ b/haskell/free-foil/src/Control/Monad/Foil.hs @@ -47,7 +47,10 @@ module Control.Monad.Foil ( Substitution, lookupSubst, identitySubst, + voidSubst, addSubst, + addSubstPattern, + addSubstList, addRename, -- * Unification of binders UnifyNameBinders(..), @@ -66,6 +69,10 @@ module Control.Monad.Foil ( emptyNameMap, lookupName, addNameBinder, + nameMapToSubstitution, + addNameBinders, + addNameBinderList, + NameBinderList(..), -- * Constraints Ext, ExtEvidence(..), diff --git a/haskell/free-foil/src/Control/Monad/Foil/Internal.hs b/haskell/free-foil/src/Control/Monad/Foil/Internal.hs index 38086332..0378c4a4 100644 --- a/haskell/free-foil/src/Control/Monad/Foil/Internal.hs +++ b/haskell/free-foil/src/Control/Monad/Foil/Internal.hs @@ -708,6 +708,35 @@ class CoSinkable (pattern :: S -> S -> Type) where -- ^ Continuation, accepting result for the entire pattern and a (possibly refreshed) pattern. -> r +-- | Auxiliary data structure for collecting name binders. Used in 'nameBinderListOf'. +newtype WithNameBinderList r n l (o :: S) (o' :: S) = WithNameBinderList (NameBinderList l r -> NameBinderList n r) + +-- | Empty list of name binders (identity). +idWithNameBinderList :: DExt o o' => WithNameBinderList r n n o o' +idWithNameBinderList = WithNameBinderList id + +-- | Concatenating lists of name binders (compose). +compWithNameBinderList + :: (DExt o o', DExt o' o'') + => WithNameBinderList r n i o o' + -> WithNameBinderList r i l o' o'' + -> WithNameBinderList r n l o o'' +compWithNameBinderList (WithNameBinderList f) (WithNameBinderList g) = + WithNameBinderList (f . g) + +-- | Collect name binders of a generalized pattern into a name binder list, +-- which can be more easily traversed. +nameBinderListOf :: (CoSinkable binder) => binder n l -> NameBinderList n l +nameBinderListOf pat = withPattern + (\_scope' binder k -> + unsafeAssertFresh binder $ \binder' -> + k (WithNameBinderList (NameBinderListCons binder)) binder') + idWithNameBinderList + compWithNameBinderList + emptyScope + pat + (\(WithNameBinderList f) _ -> f NameBinderListEmpty) + instance CoSinkable NameBinder where coSinkabilityProof _rename (UnsafeNameBinder name) cont = cont unsafeCoerce (UnsafeNameBinder name) @@ -733,6 +762,10 @@ identitySubst :: InjectName e => Substitution e i i identitySubst = UnsafeSubstitution IntMap.empty +-- | An empty substitution from an empty scope. +voidSubst :: Substitution e VoidS n +voidSubst = UnsafeSubstitution IntMap.empty + -- | Extend substitution with a particular mapping. addSubst :: Substitution e i o @@ -742,6 +775,24 @@ addSubst addSubst (UnsafeSubstitution env) (UnsafeNameBinder (UnsafeName name)) ex = UnsafeSubstitution (IntMap.insert name ex env) +addSubstPattern + :: CoSinkable binder + => Substitution e i o + -> binder i i' + -> [e o] + -> Substitution e i' o +addSubstPattern subst pat = addSubstList subst (nameBinderListOf pat) + +addSubstList + :: Substitution e i o + -> NameBinderList i i' + -> [e o] + -> Substitution e i' o +addSubstList subst NameBinderListEmpty _ = subst +addSubstList subst (NameBinderListCons binder binders) (x:xs) = + addSubstList (addSubst subst binder x) binders xs +addSubstList _ _ [] = error "cannot add a binder to Substitution since the value list does not have enough elements" + -- | Add variable renaming to a substitution. -- This includes the performance optimization of eliding names mapped to themselves. addRename :: InjectName e => Substitution e i o -> NameBinder i i' -> Name o -> Substitution e i' o @@ -763,6 +814,29 @@ newtype NameMap (n :: S) a = NameMap { getNameMap :: IntMap a } emptyNameMap :: NameMap VoidS a emptyNameMap = NameMap IntMap.empty +-- | Convert a 'NameMap' of expressions into a 'Substitution'. +nameMapToSubstitution :: NameMap i (e o) -> Substitution e i o +nameMapToSubstitution (NameMap m) = (UnsafeSubstitution m) + +-- | Extend a map with multiple mappings (by repeatedly applying 'addNameBinder'). +-- +-- Note that the input list is expected to have __at least__ the same number of elements +-- as there are binders in the input pattern (generalized binder). +addNameBinders :: CoSinkable binder => binder n l -> [a] -> NameMap n a -> NameMap l a +addNameBinders pat = addNameBinderList (nameBinderListOf pat) + +-- | Extend a map with multiple mappings (by repeatedly applying 'addNameBinder'). +-- +-- Note that the input list is expected to have __at least__ the same number of elements +-- as there are binders in the input name binder list. +-- +-- See also 'addNameBinders' for a generalized version. +addNameBinderList :: NameBinderList n l -> [a] -> NameMap n a -> NameMap l a +addNameBinderList NameBinderListEmpty _ = id +addNameBinderList (NameBinderListCons binder binders) (x:xs) = + addNameBinderList binders xs . addNameBinder binder x +addNameBinderList _ [] = error "cannot add a binder to NameMap since the value list does not have enough elements" + -- | Looking up a name should always succeed. -- -- Note that since 'Name' is 'Sinkable', you can lookup a name from scope @n@ in a 'NameMap' for scope @l@ whenever @l@ extends @n@. diff --git a/haskell/free-foil/src/Control/Monad/Free/Foil.hs b/haskell/free-foil/src/Control/Monad/Free/Foil.hs index e4d4cfd7..f02b6e85 100644 --- a/haskell/free-foil/src/Control/Monad/Free/Foil.hs +++ b/haskell/free-foil/src/Control/Monad/Free/Foil.hs @@ -1,5 +1,4 @@ {-# LANGUAGE DataKinds #-} -{-# LANGUAGE RankNTypes #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleContexts #-} @@ -9,6 +8,7 @@ {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE UndecidableInstances #-} @@ -122,6 +122,20 @@ instance (Bifunctor sig, Foil.CoSinkable binder) => Foil.RelMonad Foil.Name (AST subst' = extendSubst subst in ScopedAST binder' (Foil.rbind scope' body subst') +-- | Substitution for a single generalized pattern. +substitutePattern + :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder', Foil.CoSinkable binder) + => Foil.Scope o -- ^ Resulting scope. + -> Foil.Substitution (AST binder sig) n o -- ^ Environment mapping names in scope @n@. + -> binder' n i -- ^ Binders that extend scope @n@ to scope @i@. + -> [AST binder sig o] -- ^ A list of terms intended to serve as + -> AST binder sig i + -> AST binder sig o +substitutePattern scope env binders args body = + substitute scope env' body + where + env' = Foil.addSubstPattern env binders args + -- * \(\alpha\)-equivalence -- | Refresh (force) all binders in a term, minimizing the used indices. @@ -338,7 +352,7 @@ convertFromAST -- ^ Peel back one layer of syntax. -> (rawIdent -> rawTerm) -- ^ Convert identifier into a raw variable term. - -> (forall x y. (Int -> rawIdent) -> binder x y -> rawPattern) + -> (forall x y. binder x y -> rawPattern) -- ^ Convert scope-safe pattern into a raw pattern. -> (rawTerm -> rawScopedTerm) -- ^ Wrap raw term into a scoped term. @@ -362,7 +376,7 @@ convertFromScopedAST -- ^ Peel back one layer of syntax. -> (rawIdent -> rawTerm) -- ^ Convert identifier into a raw variable term. - -> (forall x y. (Int -> rawIdent) -> binder x y -> rawPattern) + -> (forall x y. binder x y -> rawPattern) -- ^ Convert scope-safe pattern into a raw pattern. -> (rawTerm -> rawScopedTerm) -- ^ Wrap raw term into a scoped term. @@ -373,5 +387,5 @@ convertFromScopedAST -> (rawPattern, rawScopedTerm) convertFromScopedAST fromSig fromVar makePattern makeScoped f = \case ScopedAST binder body -> - ( makePattern f binder + ( makePattern binder , makeScoped (convertFromAST fromSig fromVar makePattern makeScoped f body)) diff --git a/haskell/free-foil/src/Control/Monad/Free/Foil/Generic.hs b/haskell/free-foil/src/Control/Monad/Free/Foil/Generic.hs index 46a645ee..16ae815e 100644 --- a/haskell/free-foil/src/Control/Monad/Free/Foil/Generic.hs +++ b/haskell/free-foil/src/Control/Monad/Free/Foil/Generic.hs @@ -1,13 +1,13 @@ {-# OPTIONS_GHC -Wno-missing-methods #-} {-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE InstanceSigs #-} -{-# LANGUAGE DefaultSignatures #-} -{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} +{-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE InstanceSigs #-} +{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} @@ -18,7 +18,7 @@ {-# LANGUAGE UndecidableInstances #-} module Control.Monad.Free.Foil.Generic where -import Data.Kind (Constraint, Type) +import Data.Kind (Constraint, Type) import Generics.Kind import Generics.Kind.Examples () import GHC.TypeError diff --git a/haskell/free-foil/src/Control/Monad/Free/Foil/TH/MkFreeFoil.hs b/haskell/free-foil/src/Control/Monad/Free/Foil/TH/MkFreeFoil.hs new file mode 100644 index 00000000..4ce823e7 --- /dev/null +++ b/haskell/free-foil/src/Control/Monad/Free/Foil/TH/MkFreeFoil.hs @@ -0,0 +1,1306 @@ +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE ViewPatterns #-} +{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} +{-# HLINT ignore "Use ++" #-} +-- | Template Haskell generation for Free Foil (generic scope-safe representation of syntax). +module Control.Monad.Free.Foil.TH.MkFreeFoil ( + FreeFoilConfig(..), + FreeFoilTermConfig(..), + mkFreeFoil, + mkFreeFoilConversions, +) where + +import Language.Haskell.TH +import Language.Haskell.TH.Syntax (addModFinalizer) + +import Control.Monad (forM, forM_, when) +import qualified Control.Monad.Foil as Foil +import Control.Monad.Foil.TH.Util +import qualified Control.Monad.Free.Foil as Foil +import Data.Bifunctor +import Data.List (find, unzip4, (\\), nub) +import Data.Maybe (catMaybes, mapMaybe) +import Data.Map (Map) +import qualified Data.Map as Map +import qualified GHC.Generics as GHC + +-- | Config for the Template Haskell generation of data types, +-- pattern synonyms, and conversion functions for the Free Foil representation, +-- based on a raw recursive representation. +data FreeFoilConfig = FreeFoilConfig + { rawQuantifiedNames :: [Name] + -- ^ Names of raw types that may include other binders and terms as components. + -- Some examples of syntax that might be suitable here: + -- + -- 1. a type scheme in HM-style type system (to explicitly disallow nested forall) + -- 2. defining equation of a function (which itself is not a term) + -- 3. data or type synonym declaration (which itself is not a type) + -- 4. unification constraints (quantified or not) + , freeFoilTermConfigs :: [FreeFoilTermConfig] + -- ^ Configurations for each term (e.g. expressions, types) group. + , freeFoilNameModifier :: String -> String + -- ^ Name modifier for the Free Foil conterpart of a raw type name. + -- Normally, this is just 'id'. + , freeFoilScopeNameModifier :: String -> String + -- ^ Name modifier for the scoped Free Foil conterpart of a raw type name. + -- Normally, this is something like @("Scoped" ++)@. + , signatureNameModifier :: String -> String + -- ^ Name modifier for the signature conterpart of a raw type name or raw constructor name. + -- Normally, this is something like @(++ "Sig")@. + , freeFoilConNameModifier :: String -> String + -- ^ Name modifier for the Free Foil conterpart (pattern synonym) of a raw constructor name. + -- Normally, this is just 'id'. + , freeFoilConvertToName :: String -> String + -- ^ Name of a conversion function (from raw to scope-safe) for a raw type name. + -- Normally, this is something like @("to" ++)@. + , freeFoilConvertFromName :: String -> String + -- ^ Name of a conversion function (from scope-safe to raw) for a raw type name. + -- Normally, this is something like @("from" ++)@. + } + +-- | Config for a single term group, +-- for the Template Haskell generation of data types, +-- pattern synonyms, and conversion functions for the Free Foil representation, +-- based on a raw recursive representation. +data FreeFoilTermConfig = FreeFoilTermConfig + { rawIdentName :: Name + -- ^ The type name for the identifiers. + -- When identifiers occur in a term, they are converted to 'Foil.Name' (with an appropriate type-level scope parameter). + -- When identifiers occur in a pattern, they are converted to 'Foil.NameBinder' (with appropriate type-level scope parameters). + , rawTermName :: Name + -- ^ The type name for the term. + -- This will be the main recursive type to be converted into an 'Foil.AST'. + , rawBindingName :: Name + -- ^ The type name for the binders (patterns). + -- This will be the main binder type to used in 'Foil.AST'-representation of the terms. + , rawScopeName :: Name + -- ^ The type name for the scoped term. + -- This will be replaced with either 'Foil.ScopedAST' (with outer scope) or 'Foil.AST' (with inner scope) + -- depending on its occurrence in a regular (sub)term or some quantified syntax. + , rawVarConName :: Name + -- ^ The constructor name for the variables in a term. + -- This constructor will be replaced with the standard 'Foil.Var'. + -- It is expected to have exactly one field of type 'rawIdentName'. + , rawSubTermNames :: [Name] + -- ^ Type names for subterm syntax. + -- This will rely on the main term type ('rawTermName') for recursive occurrences. + -- Template Haskell will also generate signatures for these. + , rawSubScopeNames :: [Name] + -- ^ Type names for scoped subterm syntax. + -- This will rely on the main term type ('rawTermName') for recursive occurrences. + -- Template Haskell will also generate signatures for these. + , intToRawIdentName :: Name + -- ^ Name of a function that converts 'Int' to a raw identifier. + -- Normally, this is something like @(\i -> VarIdent ("x" ++ show i))@. + -- This is required to generate standard conversions from scope-safe to raw representation. + , rawVarIdentToTermName :: Name + -- ^ Name of a function that converts a raw identifier into a raw term. + -- Normally, this is some kind of @Var@ or @TypeVar@ data constructor. + -- This is required to generate standard conversions from scope-safe to raw representation. + , rawTermToScopeName :: Name + -- ^ Name of a function that converts a raw term into a raw scoped term. + -- Normally, this is some kind of @ScopedTerm@ or @ScopedType@ data constructor. + , rawScopeToTermName :: Name + -- ^ Name of a function that extracts a raw term from a raw scoped term. + -- Normally, this is something like @(\(ScopedTerm term) -> term)@. + } + +toFreeFoilName :: FreeFoilConfig -> Name -> Name +toFreeFoilName FreeFoilConfig{..} name = mkName (freeFoilNameModifier (nameBase name)) + +toFreeFoilNameFrom :: FreeFoilConfig -> Name -> Name +toFreeFoilNameFrom FreeFoilConfig{..} name = mkName (freeFoilConvertFromName (nameBase name)) + +toFreeFoilNameTo :: FreeFoilConfig -> Name -> Name +toFreeFoilNameTo FreeFoilConfig{..} name = mkName (freeFoilConvertToName (nameBase name)) + +toFreeFoilScopedName :: FreeFoilConfig -> Name -> Name +toFreeFoilScopedName FreeFoilConfig{..} name = mkName (freeFoilScopeNameModifier (nameBase name)) + +toSignatureName :: FreeFoilConfig -> Name -> Name +toSignatureName FreeFoilConfig{..} name = mkName (signatureNameModifier (nameBase name)) + +toConName :: FreeFoilConfig -> Name -> Name +toConName FreeFoilConfig{..} name = mkName (freeFoilConNameModifier (nameBase name)) + +lookupIdentName :: Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig +lookupIdentName name = find (\FreeFoilTermConfig{..} -> rawIdentName == name) + +lookupTermName :: Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig +lookupTermName name = find (\FreeFoilTermConfig{..} -> rawTermName == name) + +lookupSubTermName :: Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig +lookupSubTermName name = find (\FreeFoilTermConfig{..} -> name `elem` rawSubTermNames) + +lookupSubScopeName :: Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig +lookupSubScopeName name = find (\FreeFoilTermConfig{..} -> name `elem` rawSubScopeNames) + +lookupBindingName :: Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig +lookupBindingName name = find (\FreeFoilTermConfig{..} -> rawBindingName == name) + +lookupScopeName :: Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig +lookupScopeName name = find (\FreeFoilTermConfig{..} -> rawScopeName == name) + +data Sort + = SortBinder | SortTerm | SortSubTerm + +toFreeFoilType :: Sort -> FreeFoilConfig -> Type -> Type -> Type -> Type +toFreeFoilType isBinder config@FreeFoilConfig{..} outerScope innerScope = go + where + go = \case + PeelConT typeName (map go -> typeParams) + | typeName `elem` rawQuantifiedNames -> + PeelConT (toFreeFoilName config typeName) (typeParams ++ [outerScope]) + | typeName `elem` map rawIdentName freeFoilTermConfigs -> + case isBinder of + SortBinder -> PeelConT ''Foil.NameBinder [outerScope, innerScope] + _ -> PeelConT ''Foil.Name [outerScope] + | Just _ <- lookupTermName typeName freeFoilTermConfigs -> + PeelConT (toFreeFoilName config typeName) (typeParams ++ [outerScope]) + | Just _ <- lookupBindingName typeName freeFoilTermConfigs -> + PeelConT (toFreeFoilName config typeName) (typeParams ++ [outerScope, innerScope]) + | Just FreeFoilTermConfig{..} <- lookupScopeName typeName freeFoilTermConfigs -> + PeelConT (toFreeFoilName config rawTermName) (typeParams ++ [innerScope]) + | Just _ <- lookupSubTermName typeName freeFoilTermConfigs -> + PeelConT (toFreeFoilName config typeName) (typeParams ++ [outerScope]) + | Just _ <- lookupSubScopeName typeName freeFoilTermConfigs -> + PeelConT (toFreeFoilName config typeName) (typeParams ++ [innerScope]) + ForallT bndrs ctx type_ -> ForallT bndrs ctx (go type_) + ForallVisT bndrs type_ -> ForallVisT bndrs (go type_) + AppT f x -> AppT (go f) (go x) + AppKindT f k -> AppKindT (go f) k + SigT t k -> SigT (go t) k + t@ConT{} -> t + t@VarT{} -> t + t@PromotedT{} -> t + InfixT l op r -> InfixT (go l) op (go r) + UInfixT l op r -> UInfixT (go l) op (go r) + PromotedInfixT l op r -> PromotedInfixT (go l) op (go r) + PromotedUInfixT l op r -> PromotedUInfixT (go l) op (go r) + ParensT t -> ParensT (go t) + t@TupleT{} -> t + t@UnboxedTupleT{} -> t + t@UnboxedSumT{} -> t + t@ArrowT{} -> t + t@MulArrowT{} -> t + t@EqualityT{} -> t + t@ListT{} -> t + t@PromotedTupleT{} -> t + t@PromotedNilT{} -> t + t@PromotedConsT{} -> t + t@StarT{} -> t + t@ConstraintT{} -> t + t@LitT{} -> t + t@WildCardT{} -> t + ImplicitParamT s t -> ImplicitParamT s (go t) + +toFreeFoilSigType :: Sort -> FreeFoilConfig -> Type -> Type -> Type -> Maybe Type +toFreeFoilSigType sort config@FreeFoilConfig{..} scope term = go + where + go :: Type -> Maybe Type + go = \case + PeelConT _typeName (mapM go -> Nothing) -> + error "bad type params" + PeelConT typeName (mapM go -> Just typeParams) + | Just _ <- lookupTermName typeName freeFoilTermConfigs -> + case sort of + SortSubTerm -> Just (PeelConT (toSignatureName config typeName) (typeParams ++ [scope, term])) + _ -> Just term + | Just _ <- lookupBindingName typeName freeFoilTermConfigs -> + Nothing + | Just _ <- lookupScopeName typeName freeFoilTermConfigs -> + Just scope + | Just _ <- lookupSubTermName typeName freeFoilTermConfigs -> + Just (PeelConT (toSignatureName config typeName) (typeParams ++ [scope, term])) + | Just _ <- lookupSubScopeName typeName freeFoilTermConfigs -> + Just (PeelConT (toSignatureName config typeName) (typeParams ++ [scope, term])) + ForallT bndrs ctx type_ -> ForallT bndrs ctx <$> go type_ + ForallVisT bndrs type_ -> ForallVisT bndrs <$> go type_ + AppT f x -> AppT <$> go f <*> go x + AppKindT f k -> AppKindT <$> go f <*> pure k + SigT t k -> SigT <$> go t <*> pure k + t@ConT{} -> pure t + t@VarT{} -> pure t + t@PromotedT{} -> pure t + InfixT l op r -> InfixT <$> go l <*> pure op <*> go r + UInfixT l op r -> UInfixT <$> go l <*> pure op <*> go r + PromotedInfixT l op r -> PromotedInfixT <$> go l <*> pure op <*> go r + PromotedUInfixT l op r -> PromotedUInfixT <$> go l <*> pure op <*> go r + ParensT t -> ParensT <$> go t + t@TupleT{} -> pure t + t@UnboxedTupleT{} -> pure t + t@UnboxedSumT{} -> pure t + t@ArrowT{} -> pure t + t@MulArrowT{} -> pure t + t@EqualityT{} -> pure t + t@ListT{} -> pure t + t@PromotedTupleT{} -> pure t + t@PromotedNilT{} -> pure t + t@PromotedConsT{} -> pure t + t@StarT{} -> pure t + t@ConstraintT{} -> pure t + t@LitT{} -> pure t + t@WildCardT{} -> pure t + ImplicitParamT s t -> ImplicitParamT s <$> go t + +toFreeFoilCon :: FreeFoilConfig -> Type -> Type -> Type -> Con -> Q Con +toFreeFoilCon config rawRetType outerScope innerScope = go + where + goType = toFreeFoilType SortTerm config outerScope innerScope + go = \case + GadtC conNames argTypes retType -> do + let newConNames = map (toConName config) conNames + forM_ (zip conNames newConNames) $ \(conName, newConName) -> + addModFinalizer $ putDoc (DeclDoc newConName) + ("Corresponds to '" ++ show conName ++ "'.") + return (GadtC newConNames (map (fmap goType) argTypes) (goType retType)) + NormalC conName types -> go (GadtC [conName] types rawRetType) + RecC conName types -> go (NormalC conName (map removeName types)) + InfixC l conName r -> go (GadtC [conName] [l, r] rawRetType) + ForallC params ctx con -> ForallC params ctx <$> go con + RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType) + +toFreeFoilSigCon :: FreeFoilConfig -> FreeFoilTermConfig -> Name -> Type -> Type -> Type -> Con -> Q (Maybe Con) +toFreeFoilSigCon config FreeFoilTermConfig{..} sigName rawRetType scope term = go + where + goType = toFreeFoilSigType SortTerm config scope term + go = \case + GadtC conNames argTypes retType + | null newConNames -> pure Nothing + | otherwise -> do + forM_ (zip conNames newConNames) $ \(conName, newConName) -> + addModFinalizer $ putDoc (DeclDoc newConName) + ("Corresponds to '" ++ show conName ++ "'.") + return (Just (GadtC newConNames newArgTypes theRetType)) + where + newArgTypes = mapMaybe (traverse goType) argTypes + newConNames = + [ toSignatureName config rawConName + | rawConName <- conNames + , rawConName /= rawVarConName ] + theRetType = + case retType of + PeelConT _rawTypeName (mapM goType -> Just params) -> + PeelConT sigName (params ++ [scope, term]) + _ -> error "unexpected return type!" + NormalC conName types -> go (GadtC [conName] types rawRetType) + RecC conName types -> go (NormalC conName (map removeName types)) + InfixC l conName r -> go (GadtC [conName] [l, r] rawRetType) + ForallC params ctx con -> fmap (ForallC params ctx) <$> go con + RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType) + +toFreeFoilBindingCon :: FreeFoilConfig -> Type -> Type -> Con -> Q Con +toFreeFoilBindingCon config rawRetType theOuterScope = go + where + goType = toFreeFoilType SortBinder config theOuterScope + + goTypeArgs :: Int -> Type -> [BangType] -> Q (Type, [BangType]) + goTypeArgs _ outerScope [] = pure (outerScope, []) + goTypeArgs i outerScope ((bang_, rawArgType) : rawArgs) = do + case rawArgType of + PeelConT rawTypeName _rawTypeParams + | rawTypeName `elem` map rawIdentName (freeFoilTermConfigs config) -> do + innerScope <- VarT <$> newName ("i" <> show i) + let argType = toFreeFoilType SortBinder config outerScope innerScope rawArgType + (theInnerScope, argTypes) <- goTypeArgs (i + 1) innerScope rawArgs + return (theInnerScope, ((bang_, argType) : argTypes)) + + | Just _ <- lookupBindingName rawTypeName (freeFoilTermConfigs config) -> do + innerScope <- VarT <$> newName ("i" <> show i) + let argType = toFreeFoilType SortBinder config outerScope innerScope rawArgType + (theInnerScope, argTypes) <- goTypeArgs (i + 1) innerScope rawArgs + return (theInnerScope, ((bang_, argType) : argTypes)) + + _ -> do + let argType = toFreeFoilType SortBinder config outerScope outerScope rawArgType + (theInnerScope, argTypes) <- goTypeArgs (i + 1) outerScope rawArgs + return (theInnerScope, ((bang_, argType) : argTypes)) + + go :: Con -> Q Con + go = \case + GadtC conNames argTypes retType -> do + (theInnerScope, newArgs) <- goTypeArgs 0 theOuterScope argTypes + let newConNames = map (toConName config) conNames + forM_ (zip conNames newConNames) $ \(conName, newConName) -> + addModFinalizer $ putDoc (DeclDoc newConName) + ("Corresponds to '" ++ show conName ++ "'.") + return (GadtC newConNames newArgs (goType theInnerScope retType)) + NormalC conName types -> go (GadtC [conName] types rawRetType) + RecC conName types -> go (NormalC conName (map removeName types)) + InfixC l conName r -> go (GadtC [conName] [l, r] rawRetType) + ForallC params ctx con -> ForallC params ctx <$> go con + RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType) + +termConToPat :: Name -> FreeFoilConfig -> FreeFoilTermConfig -> Con -> Q [([Name], Pat, Pat, [Exp])] +termConToPat rawTypeName config@FreeFoilConfig{..} FreeFoilTermConfig{..} = go + where + rawRetType = error "impossible happened!" + + fromArgType :: Type -> Q ([Name], [Pat], [Pat], [Exp]) + fromArgType = \case + PeelConT typeName _params + | Just _ <- lookupBindingName typeName freeFoilTermConfigs -> do + return ([], [], [], []) + | Just _ <- lookupScopeName typeName freeFoilTermConfigs -> do + binder <- newName "binder" + body <- newName "body" + return ([binder, body], [ConP 'Foil.ScopedAST [] [VarP binder, VarP body]], [TupP [VarP binder, VarP body]], [VarE binder, VarE body]) + | Just _ <- lookupSubTermName typeName freeFoilTermConfigs -> do + let rawSigName = toSignatureName config typeName + funName = toFreeFoilNameFrom config rawSigName + x <- newName "x" + return ([x], [VarP x], [VarP x], [AppE (VarE funName) (VarE x)]) + | Just _ <- lookupSubScopeName typeName freeFoilTermConfigs -> do + let rawSigName = toSignatureName config typeName + funName = toFreeFoilNameFrom config rawSigName + x <- newName "x" + return ([x], [VarP x], [VarP x], [AppE (VarE funName) (VarE x)]) + | typeName == '[] -> do + x <- newName "x" + return ([x], [VarP x], [VarP x], [ConE 'False]) + AppT _ (PeelConT typeName _params) + -- | Just _ <- lookupTermName typeName freeFoilTermConfigs -> do + -- let funName = toFreeFoilNameFrom config typeName + -- x <- newName "x" + -- return ([x], [VarP x], [VarP x], [AppE (AppE (VarE 'fmap) (VarE funName)) (VarE x)]) + | Just _ <- lookupSubTermName typeName freeFoilTermConfigs -> do + let rawSigName = toSignatureName config typeName + funName = toFreeFoilNameFrom config rawSigName + x <- newName "x" + return ([x], [VarP x], [VarP x], [AppE (AppE (VarE 'fmap) (VarE funName)) (VarE x)]) + | Just _ <- lookupSubScopeName typeName freeFoilTermConfigs -> do + let rawSigName = toSignatureName config typeName + funName = toFreeFoilNameFrom config rawSigName + x <- newName "x" + return ([x], [VarP x], [VarP x], [AppE (AppE (VarE 'fmap) (VarE funName)) (VarE x)]) + _ -> do + x <- newName "x" + return ([x], [VarP x], [VarP x], [VarE x]) + + go :: Con -> Q [([Name], Pat, Pat, [Exp])] + go = \case + GadtC conNames rawArgTypes _rawRetType -> concat <$> do + forM conNames $ \conName -> do + let newConName = toSignatureName config conName + (concat -> vars, concat -> pats, concat -> pats', concat -> exps) <- unzip4 <$> + mapM (fromArgType . snd) rawArgTypes + return $ + if rawTypeName == rawTermName + then [ (vars, ConP 'Foil.Node [] [ConP newConName [] pats], ConP newConName [] pats', exps) ] + else [ (vars, ConP newConName [] pats, ConP newConName [] pats', exps) ] + NormalC conName types -> go (GadtC [conName] types rawRetType) + RecC conName types -> go (NormalC conName (map removeName types)) + InfixC l conName r -> go (GadtC [conName] [l, r] rawRetType) + ForallC _params _ctx con -> go con + RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType) + +termConToPatBinding :: Name -> FreeFoilConfig -> FreeFoilTermConfig -> Con -> Q [([Name], Pat, Pat, [Exp])] +termConToPatBinding rawTypeName config@FreeFoilConfig{..} FreeFoilTermConfig{..} = go + where + rawRetType = error "impossible happened!" + + fromArgType :: Type -> Q ([Name], [Pat], [Pat], [Exp]) + fromArgType = \case + PeelConT typeName _params + | typeName == rawIdentName -> do + x <- newName "x" + return ([x], [VarP x], [VarP x], [VarE intToRawIdentName `AppE` (VarE 'Foil.nameId `AppE` (VarE 'Foil.nameOf `AppE` VarE x))]) + | Just _ <- lookupBindingName typeName freeFoilTermConfigs -> do + let funName = toFreeFoilNameFrom config typeName + x <- newName "x" + return ([x], [VarP x], [VarP x], [VarE funName `AppE` VarE x]) + | Just _ <- lookupScopeName typeName freeFoilTermConfigs -> do + binder <- newName "binder" + body <- newName "body" + return ([binder, body], [ConP 'Foil.ScopedAST [] [VarP binder, VarP body]], [TupP [VarP binder, VarP body]], [VarE binder, VarE body]) + | Just _ <- lookupSubTermName typeName freeFoilTermConfigs -> do + let rawSigName = toSignatureName config typeName + funName = toFreeFoilNameFrom config rawSigName + x <- newName "x" + return ([x], [VarP x], [VarP x], [AppE (VarE funName) (VarE x)]) + | Just _ <- lookupSubScopeName typeName freeFoilTermConfigs -> do + let rawSigName = toSignatureName config typeName + funName = toFreeFoilNameFrom config rawSigName + x <- newName "x" + return ([x], [VarP x], [VarP x], [AppE (VarE funName) (VarE x)]) + AppT _ (PeelConT typeName _params) + | Just _ <- lookupSubTermName typeName freeFoilTermConfigs -> do + let rawSigName = toSignatureName config typeName + funName = toFreeFoilNameFrom config rawSigName + x <- newName "x" + return ([x], [VarP x], [VarP x], [AppE (AppE (VarE 'fmap) (VarE funName)) (VarE x)]) + | Just _ <- lookupSubScopeName typeName freeFoilTermConfigs -> do + let rawSigName = toSignatureName config typeName + funName = toFreeFoilNameFrom config rawSigName + x <- newName "x" + return ([x], [VarP x], [VarP x], [AppE (AppE (VarE 'fmap) (VarE funName)) (VarE x)]) + _ -> do + x <- newName "x" + return ([x], [VarP x], [VarP x], [VarE x]) + + go :: Con -> Q [([Name], Pat, Pat, [Exp])] + go = \case + GadtC conNames rawArgTypes _rawRetType -> concat <$> do + forM conNames $ \conName -> do + let newConName = toFreeFoilName config conName + (concat -> vars, concat -> pats, concat -> pats', concat -> exps) <- unzip4 <$> + mapM (fromArgType . snd) rawArgTypes + return $ + if rawTypeName == rawTermName + then [ (vars, ConP 'Foil.Node [] [ConP newConName [] pats], ConP newConName [] pats', exps) ] + else [ (vars, ConP newConName [] pats, ConP newConName [] pats', exps) ] + NormalC conName types -> go (GadtC [conName] types rawRetType) + RecC conName types -> go (NormalC conName (map removeName types)) + InfixC l conName r -> go (GadtC [conName] [l, r] rawRetType) + ForallC _params _ctx con -> go con + RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType) + +termConToPatQuantified :: FreeFoilConfig -> Con -> Q [([Name], Pat, Pat, [Exp])] +termConToPatQuantified config@FreeFoilConfig{..} = go + where + rawRetType = error "impossible happened!" + + fromArgType :: Type -> Q ([Name], [Pat], [Pat], [Exp]) + fromArgType = \case + PeelConT typeName _params + | Just _ <- lookupTermName typeName freeFoilTermConfigs -> do + let funName = toFreeFoilNameFrom config typeName + x <- newName "x" + return ([x], [VarP x], [VarP x], [VarE funName `AppE` VarE x]) + | Just FreeFoilTermConfig{..} <- lookupScopeName typeName freeFoilTermConfigs -> do + let funName = toFreeFoilNameFrom config rawTermName + x <- newName "x" + return ([x], [VarP x], [VarP x], [VarE rawTermToScopeName `AppE` (VarE funName `AppE` VarE x)]) + | Just FreeFoilTermConfig{..} <- lookupIdentName typeName freeFoilTermConfigs -> do + x <- newName "x" + return ([x], [VarP x], [VarP x], [VarE intToRawIdentName `AppE` (VarE 'Foil.nameId `AppE` VarE x)]) + | Just _ <- lookupBindingName typeName freeFoilTermConfigs -> do + let funName = toFreeFoilNameFrom config typeName + x <- newName "x" + return ([x], [VarP x], [VarP x], [VarE funName `AppE` VarE x]) + | Just _ <- lookupSubTermName typeName freeFoilTermConfigs -> do + let rawSigName = toSignatureName config typeName + funName = toFreeFoilNameFrom config rawSigName + x <- newName "x" + return ([x], [VarP x], [VarP x], [AppE (VarE funName) (VarE x)]) + | Just _ <- lookupSubScopeName typeName freeFoilTermConfigs -> do + let rawSigName = toSignatureName config typeName + funName = toFreeFoilNameFrom config rawSigName + x <- newName "x" + return ([x], [VarP x], [VarP x], [AppE (VarE funName) (VarE x)]) + AppT _ (PeelConT typeName _params) + | Just _ <- lookupSubTermName typeName freeFoilTermConfigs -> do + let funName = toFreeFoilNameFrom config typeName + x <- newName "x" + return ([x], [VarP x], [VarP x], [AppE (AppE (VarE 'fmap) (VarE funName)) (VarE x)]) + | Just _ <- lookupSubScopeName typeName freeFoilTermConfigs -> do + let funName = toFreeFoilNameFrom config typeName + x <- newName "x" + return ([x], [VarP x], [VarP x], [AppE (AppE (VarE 'fmap) (VarE funName)) (VarE x)]) + | Just _ <- lookupTermName typeName freeFoilTermConfigs -> do + let funName = toFreeFoilNameFrom config typeName + x <- newName "x" + return ([x], [VarP x], [VarP x], [AppE (AppE (VarE 'fmap) (VarE funName)) (VarE x)]) + _ -> do + x <- newName "x" + return ([x], [VarP x], [VarP x], [VarE x]) + + go :: Con -> Q [([Name], Pat, Pat, [Exp])] + go = \case + GadtC conNames rawArgTypes _rawRetType -> concat <$> do + forM conNames $ \conName -> do + let newConName = toFreeFoilName config conName + (concat -> vars, concat -> pats, concat -> pats', concat -> exps) <- unzip4 <$> + mapM (fromArgType . snd) rawArgTypes + return [ (vars, ConP newConName [] pats, ConP newConName [] pats', exps) ] + NormalC conName types -> go (GadtC [conName] types rawRetType) + RecC conName types -> go (NormalC conName (map removeName types)) + InfixC l conName r -> go (GadtC [conName] [l, r] rawRetType) + ForallC _params _ctx con -> go con + RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType) + +mkPatternSynonym :: Name -> FreeFoilConfig -> FreeFoilTermConfig -> Type -> Con -> Q [Dec] +mkPatternSynonym rawTypeName config termConfig@FreeFoilTermConfig{..} rawRetType = go + where + go :: Con -> Q [Dec] + go = \case + GadtC conNames rawArgTypes _rawRetType -> concat <$> do + forM (conNames \\ [rawVarConName]) $ \conName -> do + let patName = toConName config conName + rawConType = foldr (\x y -> AppT (AppT ArrowT x) y) rawRetType (map snd rawArgTypes) + outerScope = VarT (mkName "o") + innerScope + | rawTypeName `elem` rawSubScopeNames = outerScope + | otherwise = VarT (mkName "i") + [(vars, pat, _, _)] <- termConToPat rawTypeName config termConfig (GadtC [conName] rawArgTypes rawRetType) -- FIXME: unsafe matching! + addModFinalizer $ putDoc (DeclDoc patName) + ("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. Pattern synonym for an '" ++ show ''Foil.AST ++ "' node of type '" ++ show conName ++ "'.") + return + [ PatSynSigD patName (toFreeFoilType SortTerm config outerScope innerScope rawConType) + , PatSynD patName (PrefixPatSyn vars) ImplBidir pat + ] + + NormalC conName types -> go (GadtC [conName] types rawRetType) + RecC conName types -> go (NormalC conName (map removeName types)) + InfixC l conName r -> go (GadtC [conName] [l, r] rawRetType) + ForallC _params _ctx con -> go con -- FIXME: params and ctx! + RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType) + +toFreeFoilClauseFrom :: Name -> FreeFoilConfig -> FreeFoilTermConfig -> Type -> Con -> Q [Clause] +toFreeFoilClauseFrom rawTypeName config termConfig@FreeFoilTermConfig{..} rawRetType = go + where + go = \case + GadtC conNames rawArgTypes rawRetType' -> concat <$> do + forM (conNames \\ [rawVarConName]) $ \conName -> do + [(_vars, _pat, pat, exps)] <- termConToPat rawTypeName config termConfig + (GadtC [conName] rawArgTypes rawRetType') -- FIXME: unsafe matching! + return [ Clause [pat] (NormalB (foldl AppE (ConE conName) exps)) [] ] + + NormalC conName types -> go (GadtC [conName] types rawRetType) + RecC conName types -> go (NormalC conName (map removeName types)) + InfixC l conName r -> go (GadtC [conName] [l, r] rawRetType) + ForallC _params _ctx con -> go con + RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType) + +toFreeFoilClauseFromBinding :: FreeFoilConfig -> FreeFoilTermConfig -> Type -> Con -> Q [Clause] +toFreeFoilClauseFromBinding config termConfig@FreeFoilTermConfig{..} rawRetType = go + where + go = \case + GadtC conNames rawArgTypes rawRetType' -> concat <$> do + forM (conNames \\ [rawVarConName]) $ \conName -> do + [(_vars, _pat, pat, exps)] <- termConToPatBinding rawBindingName config termConfig + (GadtC [conName] rawArgTypes rawRetType') -- FIXME: unsafe matching! + return [ Clause [pat] (NormalB (foldl AppE (ConE conName) exps)) [] ] + + NormalC conName types -> go (GadtC [conName] types rawRetType) + RecC conName types -> go (NormalC conName (map removeName types)) + InfixC l conName r -> go (GadtC [conName] [l, r] rawRetType) + ForallC _params _ctx con -> go con + RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType) + +toFreeFoilClauseFromQuantified :: FreeFoilConfig -> Type -> Con -> Q [Clause] +toFreeFoilClauseFromQuantified config rawRetType = go + where + go = \case + GadtC conNames rawArgTypes rawRetType' -> concat <$> do + forM conNames $ \conName -> do + [(_vars, _pat, pat, exps)] <- termConToPatQuantified config + (GadtC [conName] rawArgTypes rawRetType') -- FIXME: unsafe matching! + return [ Clause [pat] (NormalB (foldl AppE (ConE conName) exps)) [] ] + + NormalC conName types -> go (GadtC [conName] types rawRetType) + RecC conName types -> go (NormalC conName (map removeName types)) + InfixC l conName r -> go (GadtC [conName] [l, r] rawRetType) + ForallC _params _ctx con -> go con + RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType) + +-- | Generate scope-safe types and pattern synonyms for a given raw set of types: +-- +-- 1. Scope-safe quantified types (e.g. type schemas, defining equations of functions, unification constraints, data/type declarations) +-- 2. Scope-safe terms, scoped terms, subterms, scoped subterms. +-- 3. Scope-safe patterns. +-- 4. Signatures for terms, subterms, and scoped subterms. +-- 5. Pattern synonyms for terms, subterms, and scoped subterms. +mkFreeFoil :: FreeFoilConfig -> Q [Dec] +mkFreeFoil config@FreeFoilConfig{..} = concat <$> sequence + [ mapM mkQuantifiedType rawQuantifiedNames + , mapM mkBindingType freeFoilTermConfigs + , concat <$> mapM mkSignatureTypes freeFoilTermConfigs + , concat <$> mapM mkPatternSynonyms freeFoilTermConfigs + ] + where + scope = mkName "scope" + term = mkName "term" + outerScope = mkName "o" + innerScope = mkName "i" + + mkPatternSynonyms termConfig@FreeFoilTermConfig{..} = do + ds <- mkPatternSynonyms' termConfig rawTermName + ds' <- concat <$> mapM (mkPatternSynonyms' termConfig) (rawSubTermNames <> rawSubScopeNames) + return (ds <> ds') + + mkPatternSynonyms' FreeFoilTermConfig{..} rawName = do + (tvars, cons) <- reifyDataOrNewtype rawName + let rawRetType = PeelConT rawName (map (VarT . tvarName) tvars) + concat <$> mapM (mkPatternSynonym rawName config FreeFoilTermConfig{..} rawRetType) cons + + mkQuantifiedType rawName = do + (tvars, cons) <- reifyDataOrNewtype rawName + let name = toFreeFoilName config rawName + rawRetType = PeelConT rawName (map (VarT . tvarName) tvars) + newParams = tvars ++ [PlainTV outerScope BndrReq] + toCon = toFreeFoilCon config rawRetType (VarT outerScope) (VarT innerScope) + newCons <- mapM toCon cons + addModFinalizer $ putDoc (DeclDoc name) + ("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. A scope-safe version of '" ++ show rawName ++ "'.") + return (DataD [] name newParams Nothing newCons []) + + mkBindingType FreeFoilTermConfig{..} = do + (tvars, cons) <- reifyDataOrNewtype rawBindingName + let bindingName = toFreeFoilName config rawBindingName + rawRetType = PeelConT rawBindingName (map (VarT . tvarName) tvars) + newParams = tvars ++ [PlainTV outerScope BndrReq, PlainTV innerScope BndrReq] + toCon = toFreeFoilBindingCon config rawRetType (VarT outerScope) + newCons <- mapM toCon cons + addModFinalizer $ putDoc (DeclDoc bindingName) + ("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. A binding type, scope-safe version of '" ++ show rawBindingName ++ "'.") + return (DataD [] bindingName newParams Nothing newCons []) + + mkSignatureTypes termConfig@FreeFoilTermConfig{..} = do + sig <- mkSignatureType termConfig rawTermName + subsigs <- concat <$> mapM (mkSignatureType termConfig) (rawSubTermNames <> rawSubScopeNames) + return (sig ++ subsigs) + + mkSignatureType termConfig@FreeFoilTermConfig{..} rawName = do + (tvars, cons) <- reifyDataOrNewtype rawName + let sigName = toSignatureName config rawName + tvars' = map (VarT . tvarName) tvars + rawRetType = PeelConT rawName tvars' + newParams = tvars ++ [PlainTV scope BndrReq, PlainTV term BndrReq] + toCon = toFreeFoilSigCon config termConfig sigName rawRetType (VarT scope) (VarT term) + newCons <- catMaybes <$> mapM toCon cons + let bindingT = PeelConT (toFreeFoilName config rawBindingName) tvars' + sigNameT = PeelConT (toSignatureName config rawTermName) tvars' + astName = toFreeFoilName config rawName + scopeName = toFreeFoilScopedName config rawName + termAST = PeelConT ''Foil.AST [bindingT, sigNameT] + scopedTermAST = PeelConT ''Foil.ScopedAST [bindingT, sigNameT] + n = mkName "n" + addModFinalizer $ putDoc (DeclDoc sigName) + ("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. A signature based on '" ++ show rawName ++ "'.") + addModFinalizer $ putDoc (DeclDoc astName) + ("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. A scope-safe version of '" ++ show rawName ++ "'.") + when (rawTermName == rawName) $ do + addModFinalizer $ putDoc (DeclDoc scopeName) + ("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. A scoped (and scope-safe) version of '" ++ show rawName ++ "'.") + return $ concat + [ [ DataD [] sigName newParams Nothing newCons [DerivClause Nothing [ConT ''GHC.Generic, ConT ''Functor, ConT ''Foldable, ConT ''Traversable]] ] + , if rawTermName == rawName + then [ TySynD astName tvars termAST + , TySynD scopeName tvars scopedTermAST ] + else [ TySynD astName (tvars ++ [PlainTV n BndrReq]) + (PeelConT sigName + (tvars' ++ + [ AppT scopedTermAST (VarT n) + , AppT termAST (VarT n) ])) ] + ] + +infixr 3 --> +(-->) :: Type -> Type -> Type +a --> b = AppT (AppT ArrowT a) b + +reifyDataOrNewtype :: Name -> Q ([TyVarBndr BndrVis], [Con]) +reifyDataOrNewtype name = reify name >>= \case + TyConI (DataD _ctx _name tvars _kind cons _deriv) -> return (tvars, cons) + TyConI (NewtypeD _ctx _name tvars _kind con _deriv) -> return (tvars, [con]) + _ -> error ("not a data or newtype: " ++ show name) + +-- | Generate conversions to and from scope-safe representation: +-- +-- 1. Conversions for scope-safe quantified types (e.g. type schemas, defining equations of functions, unification constraints, data/type declarations) +-- 2. Conversions for scope-safe terms, scoped terms, subterms, scoped subterms. +-- 3. CPS-style conversions for scope-safe patterns. +-- 4. Helpers for signatures of terms, subterms, and scoped subterms. +mkFreeFoilConversions :: FreeFoilConfig -> Q [Dec] +mkFreeFoilConversions config@FreeFoilConfig{..} = concat <$> sequence + [ concat <$> mapM mkConvertFrom freeFoilTermConfigs + , concat <$> mapM mkConvertFromQuantified rawQuantifiedNames + , concat <$> mapM mkConvertTo freeFoilTermConfigs + , concat <$> mapM mkConvertToQuantified rawQuantifiedNames + ] + where + outerScope = mkName "o" + innerScope = mkName "i" + + mkConvertFrom termConfig@FreeFoilTermConfig{..} = concat <$> sequence + [ concat <$> mapM (mkConvertFromSig termConfig) (rawTermName : (rawSubTermNames <> rawSubScopeNames)) + , mkConvertFromBinding termConfig + , concat <$> mapM (mkConvertFromSubTerm termConfig) (rawSubTermNames <> rawSubScopeNames) + , mkConvertFromTerm termConfig + ] + + mkConvertFromSig termConfig@FreeFoilTermConfig{..} rawName = do + (tvars, cons) <- reifyDataOrNewtype rawName + let rawSigName = toSignatureName config rawName + funName = toFreeFoilNameFrom config rawSigName + rawRetType = PeelConT rawName (map (VarT . tvarName) tvars) + rawTermType = PeelConT rawTermName (map (VarT . tvarName) tvars) + rawScopedTermType = PeelConT rawScopeName (map (VarT . tvarName) tvars) + rawBindingType = PeelConT rawBindingName (map (VarT . tvarName) tvars) + rawScopeType = TupleT 2 `AppT` rawBindingType `AppT` rawScopedTermType + case toFreeFoilSigType SortSubTerm config rawScopeType rawTermType rawRetType of + Just termType -> do + clauses <- concat <$> mapM (toFreeFoilClauseFrom rawSigName config termConfig rawRetType) cons + addModFinalizer $ putDoc (DeclDoc funName) + ("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. A helper used to convert from scope-safe to raw representation.") + return + [ SigD funName (AppT (AppT ArrowT termType) rawRetType) + , FunD funName clauses ] + Nothing -> error "impossible happened" + + mkConvertFromTerm FreeFoilTermConfig{..} = do + (tvars, _cons) <- reifyDataOrNewtype rawTermName + let funName = toFreeFoilNameFrom config rawTermName + rawSigName = toSignatureName config rawTermName + funSigName = toFreeFoilNameFrom config rawSigName + funBindingName = toFreeFoilNameFrom config rawBindingName + rawTermType = PeelConT rawTermName (map (VarT . tvarName) tvars) + termType = toFreeFoilType SortTerm config (VarT outerScope) (VarT innerScope) rawTermType + addModFinalizer $ putDoc (DeclDoc funName) + ("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. Convert from scope-safe to raw representation.") + return + [ SigD funName (AppT (AppT ArrowT termType) rawTermType) + , FunD funName [ + Clause [] (NormalB + (VarE 'Foil.convertFromAST + `AppE` VarE funSigName + `AppE` VarE rawVarIdentToTermName + `AppE` VarE funBindingName + `AppE` VarE rawTermToScopeName + `AppE` VarE intToRawIdentName)) [] + ] + ] + + mkConvertFromSubTerm FreeFoilTermConfig{..} rawName = do + (tvars, _cons) <- reifyDataOrNewtype rawName + let funName = toFreeFoilNameFrom config rawName + funSigName = toFreeFoilNameFrom config (toSignatureName config rawName) + funTermName = toFreeFoilNameFrom config rawTermName + funBindingName = toFreeFoilNameFrom config rawBindingName + rawType = PeelConT rawName (map (VarT . tvarName) tvars) + safeType = toFreeFoilType SortTerm config (VarT outerScope) (VarT innerScope) rawType + binders <- newName "binders" + body <- newName "body" + addModFinalizer $ putDoc (DeclDoc funName) + ("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. Convert from scope-safe to raw representation.") + return + [ SigD funName (AppT (AppT ArrowT safeType) rawType) + , FunD funName [ + Clause [] (NormalB $ + InfixE + (Just (VarE funSigName)) + (VarE '(.)) + (Just (VarE 'bimap + `AppE` LamE [ConP 'Foil.ScopedAST [] [VarP binders, VarP body]] + (TupE [ Just (VarE funBindingName `AppE` VarE binders) + , Just (VarE rawTermToScopeName `AppE` (VarE funTermName `AppE` VarE body))]) + `AppE` VarE funTermName))) [] + ] + ] + + mkConvertFromQuantified rawName = do + (tvars, cons) <- reifyDataOrNewtype rawName + let funName = toFreeFoilNameFrom config rawName + rawType = PeelConT rawName (map (VarT . tvarName) tvars) + safeType = toFreeFoilType SortTerm config (VarT outerScope) (VarT innerScope) rawType + addModFinalizer $ putDoc (DeclDoc funName) + ("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. Convert from scope-safe to raw representation.") + clauses <- concat <$> mapM (toFreeFoilClauseFromQuantified config rawType) cons + return + [ SigD funName (AppT (AppT ArrowT safeType) rawType) + , FunD funName clauses + ] + + mkConvertFromBinding termConfig@FreeFoilTermConfig{..} = do + (tvars, cons) <- reifyDataOrNewtype rawBindingName + let funName = toFreeFoilNameFrom config rawBindingName + rawRetType = PeelConT rawBindingName (map (VarT . tvarName) tvars) + bindingType = toFreeFoilType SortBinder config (VarT outerScope) (VarT innerScope) rawRetType + clauses <- concat <$> mapM (toFreeFoilClauseFromBinding config termConfig rawRetType) cons + addModFinalizer $ putDoc (DeclDoc funName) + ("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. Convert a scope-safe to a raw binding.") + return + [ SigD funName (bindingType --> rawRetType) + , FunD funName clauses ] + + mkConvertTo termConfig@FreeFoilTermConfig{..} = concat <$> sequence + [ mkConvertToSig SortTerm termConfig rawTermName + , concat <$> mapM (mkConvertToSig SortSubTerm termConfig) (rawSubTermNames <> rawSubScopeNames) + , mkConvertToBinding termConfig + , concat <$> mapM (mkConvertToSubTerm termConfig) (rawSubTermNames <> rawSubScopeNames) + , mkConvertToTerm termConfig + ] + + mkConvertToSubTerm termConfig@FreeFoilTermConfig{..} rawName = do + (tvars, cons) <- reifyDataOrNewtype rawName + (itvars, _cons) <- reifyDataOrNewtype rawIdentName + let funName = toFreeFoilNameTo config rawName + rawIdentType = PeelConT rawIdentName (map (VarT . tvarName) (take (length itvars) tvars)) -- FIXME: undocumented hack :( + rawType = PeelConT rawName (map (VarT . tvarName) tvars) + safeType = toFreeFoilType SortTerm config (VarT outerScope) (VarT innerScope) rawType + clauses <- concat <$> mapM (subTermConToClause rawType config termConfig) cons + addModFinalizer $ putDoc (DeclDoc funName) + ("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. Convert from scope-safe to raw representation.") + let scope + | rawName `elem` rawSubTermNames = outerScope + | otherwise = innerScope + return + [ SigD funName $ + ForallT + (PlainTV scope SpecifiedSpec : map (SpecifiedSpec <$) tvars) + [ ConT ''Foil.Distinct `AppT` VarT scope + , ConT ''Ord `AppT` rawIdentType ] $ + (ConT ''Foil.Scope `AppT` VarT scope) + --> (ConT ''Map `AppT` rawIdentType `AppT` (ConT ''Foil.Name `AppT` VarT scope)) + --> rawType + --> safeType + , FunD funName clauses + ] + + mkConvertToTerm FreeFoilTermConfig{..} = do + (tvars, _cons) <- reifyDataOrNewtype rawTermName + (itvars, _cons) <- reifyDataOrNewtype rawIdentName + let funName = toFreeFoilNameTo config rawTermName + rawSigName = toSignatureName config rawTermName + rawIdentType = PeelConT rawIdentName (map (VarT . tvarName) (take (length itvars) tvars)) -- FIXME: undocumented hack :( + funSigName = toFreeFoilNameTo config rawSigName + funBindingName = toFreeFoilNameTo config rawBindingName + rawTermType = PeelConT rawTermName (map (VarT . tvarName) tvars) + termType = toFreeFoilType SortTerm config (VarT outerScope) (VarT innerScope) rawTermType + addModFinalizer $ putDoc (DeclDoc funName) + ("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. Convert from scope-safe to raw representation.") + return + [ SigD funName $ + ForallT + (PlainTV outerScope SpecifiedSpec : map (SpecifiedSpec <$) tvars) + [ ConT ''Foil.Distinct `AppT` VarT outerScope + , ConT ''Ord `AppT` rawIdentType ] $ + (ConT ''Foil.Scope `AppT` VarT outerScope) + --> (ConT ''Map `AppT` rawIdentType `AppT` (ConT ''Foil.Name `AppT` VarT outerScope)) + --> rawTermType + --> termType + , FunD funName [ + Clause [] (NormalB + (VarE 'Foil.convertToAST + `AppE` VarE funSigName + `AppE` VarE funBindingName + `AppE` VarE rawScopeToTermName)) [] + ] + ] + + mkConvertToSig sort termConfig@FreeFoilTermConfig{..} rawName = do + (tvars, cons) <- reifyDataOrNewtype rawName + (itvars, _cons) <- reifyDataOrNewtype rawIdentName + let rawSigName = toSignatureName config rawName + funName = toFreeFoilNameTo config rawSigName + rawType = PeelConT rawName (map (VarT . tvarName) tvars) + rawIdentType = PeelConT rawIdentName (map (VarT . tvarName) (take (length itvars) tvars)) -- FIXME: undocumented hack :( + rawTermType = PeelConT rawTermName (map (VarT . tvarName) tvars) + rawScopedTermType = PeelConT rawScopeName (map (VarT . tvarName) tvars) + rawBindingType = PeelConT rawBindingName (map (VarT . tvarName) tvars) + rawScopeType = TupleT 2 `AppT` rawBindingType `AppT` rawScopedTermType + case toFreeFoilSigType SortSubTerm config rawScopeType rawTermType rawType of + Just safeType -> do + let retType = case sort of + SortTerm -> ConT ''Either `AppT` rawIdentType `AppT` safeType + _ -> safeType + clauses <- concat <$> mapM (sigConToClause sort rawType config termConfig) cons + addModFinalizer $ putDoc (DeclDoc funName) + ("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. A helper used to convert from raw to scope-safe representation.") + return + [ SigD funName (AppT (AppT ArrowT rawType) retType) + , FunD funName clauses ] + Nothing -> error "impossible happened" + + mkConvertToBinding termConfig@FreeFoilTermConfig{..} = do + (tvars, cons) <- reifyDataOrNewtype rawBindingName + (itvars, _cons) <- reifyDataOrNewtype rawIdentName + let funName = toFreeFoilNameTo config rawBindingName + rawBindingType = PeelConT rawBindingName (map (VarT . tvarName) tvars) + rawIdentType = PeelConT rawIdentName (map (VarT . tvarName) (take (length itvars) tvars)) -- FIXME: undocumented hack :( + safeType = toFreeFoilType SortBinder config (VarT outerScope) (VarT innerScope) rawBindingType + clauses <- concat <$> mapM (bindingConToClause rawBindingType config termConfig) cons + r <- newName "r" + addModFinalizer $ putDoc (DeclDoc funName) + ("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. Convert from raw to scope-safe binding (CPS-style).") + return + [ SigD funName $ + ForallT + (PlainTV outerScope SpecifiedSpec : map (SpecifiedSpec <$) tvars ++ [PlainTV r SpecifiedSpec]) + [ ConT ''Foil.Distinct `AppT` VarT outerScope + , ConT ''Ord `AppT` rawIdentType ] $ + (ConT ''Foil.Scope `AppT` VarT outerScope) + --> (ConT ''Map `AppT` rawIdentType `AppT` (ConT ''Foil.Name `AppT` VarT outerScope)) + --> rawBindingType + --> ForallT [PlainTV innerScope SpecifiedSpec] + [ConT ''Foil.DExt `AppT` VarT outerScope `AppT` VarT innerScope] + (safeType + --> (ConT ''Map `AppT` rawIdentType `AppT` (ConT ''Foil.Name `AppT` VarT innerScope)) + --> VarT r) + --> VarT r + , FunD funName clauses ] + + mkConvertToQuantified rawName = do + (tvars, cons) <- reifyDataOrNewtype rawName + rawIdentNamesOfQuantifiedName rawName config >>= \case + [] -> error "unexpected: quantified type not connected to any known terms" + [rawIdentName'] -> do + (itvars, _cons) <- reifyDataOrNewtype rawIdentName' + let funName = toFreeFoilNameTo config rawName + rawIdentType = PeelConT rawIdentName' (map (VarT . tvarName) (take (length itvars) tvars)) -- FIXME: undocumented hack :( + rawType = PeelConT rawName (map (VarT . tvarName) tvars) + safeType = toFreeFoilType SortTerm config (VarT outerScope) (VarT innerScope) rawType + addModFinalizer $ putDoc (DeclDoc funName) + ("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. Convert from scope-safe to raw representation.") + clauses <- concat <$> mapM (quantifiedConToClause rawType config) cons + return + [ SigD funName $ + ForallT + (PlainTV outerScope SpecifiedSpec : map (SpecifiedSpec <$) tvars) + [ ConT ''Foil.Distinct `AppT` VarT outerScope + , ConT ''Ord `AppT` rawIdentType ] $ + (ConT ''Foil.Scope `AppT` VarT outerScope) + --> (ConT ''Map `AppT` rawIdentType `AppT` (ConT ''Foil.Name `AppT` VarT outerScope)) + --> rawType + --> safeType + , FunD funName clauses + ] + _ -> do + -- error ("unsupported: more than one known term connected to the quantified type: " <> show rawName) + return [] + +quantifiedConToClause :: Type -> FreeFoilConfig -> Con -> Q [Clause] +quantifiedConToClause rawType config@FreeFoilConfig{..} = go + where + goArgTypes :: Name -> Name -> Name -> Name -> [Type] -> Q ([Pat], [Exp], Exp -> Exp, Name, Name) + goArgTypes _theScope _theEnv scope env [] = return ([], [], id, scope, env) + goArgTypes theScope theEnv scope env (t:ts) = case t of + PeelConT typeName _params + | typeName `elem` map rawIdentName freeFoilTermConfigs -> do + x <- newName "_x" + (pats, exps, wrap, scope', env') <- goArgTypes theScope theEnv scope env ts + return (VarP x : pats, (InfixE (Just (VarE env)) (VarE '(Map.!)) (Just (VarE x))) : exps, wrap, scope', env') + | Just _ <- lookupBindingName typeName freeFoilTermConfigs -> do + x <- newName "_x" + x' <- newName "_x'" + scope' <- newName "_scope" + env' <- newName "_env" + let funName = toFreeFoilNameTo config typeName + (pats, exps, wrap, scope'', env'') <- goArgTypes theScope theEnv scope' env' ts + return (VarP x : pats, VarE x' : exps, \e -> + VarE funName `AppE` VarE scope `AppE` VarE env `AppE` VarE x `AppE` + LamE [VarP x', VarP env'] + (LetE [ ValD (VarP scope') (NormalB (VarE 'Foil.extendScopePattern `AppE` VarE x' `AppE` VarE scope)) []] + (wrap e)), scope'', env'') + | Just FreeFoilTermConfig{..} <- lookupScopeName typeName freeFoilTermConfigs -> do + x <- newName "_x" + let funName = toFreeFoilNameTo config rawTermName + (pats, exps, wrap, scope', env') <- goArgTypes theScope theEnv scope env ts + return (VarP x : pats, + (VarE funName `AppE` VarE scope' `AppE` VarE env' `AppE` (VarE rawScopeToTermName `AppE` VarE x)) : exps, + wrap, scope', env') + | Just _ <- lookupTermName typeName freeFoilTermConfigs -> do + let funName = toFreeFoilNameTo config typeName + x <- newName "x" + (pats, exps, wrap, scope', env') <- goArgTypes theScope theEnv scope env ts + return (VarP x : pats, (VarE funName `AppE` VarE scope' `AppE` VarE env' `AppE` VarE x) : exps, wrap, scope', env') + AppT _ (PeelConT typeName _params) + | Just _ <- lookupTermName typeName freeFoilTermConfigs -> do + let funName = toFreeFoilNameTo config typeName + x <- newName "x" + (pats, exps, wrap, scope', env') <- goArgTypes theScope theEnv scope env ts + return (VarP x : pats, AppE (AppE (VarE 'fmap) (VarE funName `AppE` VarE theScope `AppE` VarE theEnv)) (VarE x) : exps, wrap, scope', env') + | Just _ <- lookupSubTermName typeName freeFoilTermConfigs -> do + let funName = toFreeFoilNameTo config typeName + x <- newName "x" + (pats, exps, wrap, scope', env') <- goArgTypes theScope theEnv scope env ts + return (VarP x : pats, AppE (AppE (VarE 'fmap) (VarE funName `AppE` VarE theScope `AppE` VarE theEnv)) (VarE x) : exps, wrap, scope', env') + | Just _ <- lookupSubScopeName typeName freeFoilTermConfigs -> do + let funName = toFreeFoilNameTo config typeName + x <- newName "x" + (pats, exps, wrap, scope', env') <- goArgTypes theScope theEnv scope env ts + return (VarP x : pats, AppE (AppE (VarE 'fmap) (VarE funName `AppE` VarE scope' `AppE` VarE env')) (VarE x) : exps, wrap, scope', env') + | Just FreeFoilTermConfig{..} <- lookupScopeName typeName freeFoilTermConfigs -> do + let funName = toFreeFoilNameTo config rawTermName + x <- newName "x" + (pats, exps, wrap, scope', env') <- goArgTypes theScope theEnv scope env ts + return (VarP x : pats, AppE (AppE (VarE 'fmap) (VarE funName `AppE` VarE scope' `AppE` VarE env')) (VarE x) : exps, wrap, scope', env') + _ -> do + x <- newName "_x" + (pats, exps, wrap, scope', env') <- goArgTypes theScope theEnv scope env ts + return (VarP x : pats, VarE x : exps, wrap, scope', env') + + go :: Con -> Q [Clause] + go = \case + GadtC conNames rawArgTypes _rawRetType -> concat <$> do + scope <- newName "_scope" + env <- newName "_env" + forM conNames $ \conName -> do + let newConName = toConName config conName + (pats, exps, wrap, _scope', _env') <- goArgTypes scope env scope env (map snd rawArgTypes) + return + [ Clause [VarP scope, VarP env, ConP conName [] pats] + (NormalB (wrap (foldl AppE (ConE newConName) exps))) [] ] + NormalC conName types -> go (GadtC [conName] types rawType) + RecC conName types -> go (NormalC conName (map removeName types)) + InfixC l conName r -> go (GadtC [conName] [l, r] rawType) + ForallC _params _ctx con -> go con + RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType) + +subTermConToClause :: Type -> FreeFoilConfig -> FreeFoilTermConfig -> Con -> Q [Clause] +subTermConToClause rawType config FreeFoilTermConfig{..} = go + where + goArgTypes :: Name -> Name -> [Type] -> Q ([Pat], [Exp], Exp -> Exp, Name, Name) + goArgTypes scope env [] = return ([], [], id, scope, env) + goArgTypes scope env (t:ts) = case t of + PeelConT typeName _params + | typeName == rawBindingName -> do + x <- newName "_x" + x' <- newName "_x'" + scope' <- newName "_scope" + env' <- newName "_env" + let funName = toFreeFoilNameTo config typeName + (pats, exps, wrap, scope'', env'') <- goArgTypes scope' env' ts + return (VarP x : pats, VarE x' : exps, \e -> + VarE funName `AppE` VarE scope `AppE` VarE env `AppE` VarE x `AppE` + LamE [VarP x', VarP env'] + (LetE [ ValD (VarP scope') (NormalB (VarE 'Foil.extendScopePattern `AppE` VarE x' `AppE` VarE scope)) []] + (wrap e)), scope'', env'') + | typeName == rawScopeName -> do + x <- newName "_x" + let funName = toFreeFoilNameTo config rawTermName + (pats, exps, wrap, scope', env') <- goArgTypes scope env ts + return (VarP x : pats, + (VarE funName `AppE` VarE scope' `AppE` VarE env' `AppE` (VarE rawScopeToTermName `AppE` VarE x)) : exps, + wrap, scope', env') + | typeName == rawTermName -> do + x <- newName "_x" + let funName = toFreeFoilNameTo config rawTermName + (pats, exps, wrap, scope', env') <- goArgTypes scope env ts + return (VarP x : pats, + (VarE funName `AppE` VarE scope `AppE` VarE env `AppE` VarE x) : exps, + wrap, scope', env') + | typeName `elem` rawSubTermNames -> do + x <- newName "_x" + let funName = toFreeFoilNameTo config typeName + (pats, exps, wrap, scope', env') <- goArgTypes scope env ts + return (VarP x : pats, + (VarE funName `AppE` VarE scope `AppE` VarE env `AppE` VarE x) : exps, + wrap, scope', env') + AppT _ (PeelConT typeName _params) + | typeName == rawTermName -> do + let funName = toFreeFoilNameTo config typeName + x <- newName "_x" + (pats, exps, wrap, scope', env') <- goArgTypes scope env ts + return (VarP x : pats, + (VarE 'fmap `AppE` (VarE funName `AppE` VarE scope `AppE` VarE env) `AppE` VarE x) : exps, + wrap, scope', env') + | typeName `elem` rawSubTermNames -> do + let rawSigName = toSignatureName config typeName + funName = toFreeFoilNameTo config rawSigName + x <- newName "_x" + (pats, exps, wrap, scope', env') <- goArgTypes scope env ts + return (VarP x : pats, + (VarE 'fmap `AppE` (VarE funName `AppE` VarE scope `AppE` VarE env) `AppE` VarE x) : exps, + wrap, scope', env') + | typeName `elem` rawSubScopeNames -> do + let rawSigName = toSignatureName config typeName + funName = toFreeFoilNameTo config rawSigName + x <- newName "_x" + (pats, exps, wrap, scope', env') <- goArgTypes scope env ts + return (VarP x : pats, + (VarE 'fmap `AppE` (VarE funName `AppE` VarE scope' `AppE` VarE env') `AppE` VarE x) : exps, + wrap, scope', env') + _ -> do + x <- newName "_x" + (pats, exps, wrap, scope', env') <- goArgTypes scope env ts + return (VarP x : pats, VarE x : exps, wrap, scope', env') + + go :: Con -> Q [Clause] + go = \case + GadtC conNames rawArgTypes _rawRetType -> concat <$> do + scope <- newName "_scope" + env <- newName "_env" + forM conNames $ \conName -> do + let newConName = toConName config conName + (pats, exps, wrap, _scope', _env') <- goArgTypes scope env (map snd rawArgTypes) + return + [ Clause [VarP scope, VarP env, ConP conName [] pats] + (NormalB (wrap (foldl AppE (ConE newConName) exps))) [] ] + NormalC conName types -> go (GadtC [conName] types rawType) + RecC conName types -> go (NormalC conName (map removeName types)) + InfixC l conName r -> go (GadtC [conName] [l, r] rawType) + ForallC _params _ctx con -> go con + RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType) + +bindingConToClause :: Type -> FreeFoilConfig -> FreeFoilTermConfig -> Con -> Q [Clause] +bindingConToClause rawType config FreeFoilTermConfig{..} = go + where + goArgTypes :: Name -> Name -> [Type] -> Q ([Pat], [Exp], Exp -> Exp, Name) + goArgTypes _scope env [] = return ([], [], id, env) + goArgTypes scope env (t:ts) = case t of + PeelConT typeName _params + | typeName == rawIdentName -> do + x <- newName "_x" + x' <- newName "_x'" + scope' <- newName "_scope" + env' <- newName "_env" + (pats, exps, wrap, env'') <- goArgTypes scope' env' ts + return (VarP x : pats, VarE x' : exps, \e -> + VarE 'Foil.withFresh `AppE` VarE scope `AppE` + LamE [VarP x'] + (LetE [ ValD (VarP scope') (NormalB (VarE 'Foil.extendScope `AppE` VarE x' `AppE` VarE scope)) [] + , ValD (VarP env') (NormalB (VarE 'Map.insert `AppE` VarE x `AppE` (VarE 'Foil.nameOf `AppE` VarE x') `AppE` (VarE 'fmap `AppE` VarE 'Foil.sink `AppE` VarE env))) []] + (wrap e)), env'') + | typeName == rawBindingName -> do + x <- newName "_x" + x' <- newName "_x'" + scope' <- newName "_scope" + env' <- newName "_env" + let funName = toFreeFoilNameTo config typeName + (pats, exps, wrap, env'') <- goArgTypes scope' env' ts + return (VarP x : pats, VarE x' : exps, \e -> + VarE funName `AppE` VarE scope `AppE` VarE env `AppE` VarE x `AppE` + LamE [VarP x', VarP env'] + (LetE [ ValD (VarP scope') (NormalB (VarE 'Foil.extendScopePattern `AppE` VarE x' `AppE` VarE scope)) []] + (wrap e)), env'') + _ -> do + x <- newName "_x" + (pats, exps, wrap, env') <- goArgTypes scope env ts + return (VarP x : pats, VarE x : exps, wrap, env') + + go :: Con -> Q [Clause] + go = \case + GadtC conNames rawArgTypes _rawRetType -> concat <$> do + scope <- newName "_scope" + env <- newName "_env" + cont <- newName "_cont" + forM conNames $ \conName -> do + let newConName = toConName config conName + (pats, exps, wrap, env') <- goArgTypes scope env (map snd rawArgTypes) + return + [ Clause [VarP scope, VarP env, ConP conName [] pats, VarP cont] + (NormalB (wrap (VarE cont `AppE` foldl AppE (ConE newConName) exps `AppE` VarE env'))) [] ] + NormalC conName types -> go (GadtC [conName] types rawType) + RecC conName types -> go (NormalC conName (map removeName types)) + InfixC l conName r -> go (GadtC [conName] [l, r] rawType) + ForallC _params _ctx con -> go con + RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType) + + +sigConToClause :: Sort -> Type -> FreeFoilConfig -> FreeFoilTermConfig -> Con -> Q [Clause] +sigConToClause sort rawRetType config@FreeFoilConfig{..} FreeFoilTermConfig{..} = go + where + fromArgType :: Bool -> Name -> Type -> Q ([Pat], [Exp]) + fromArgType isVarCon theIdent = \case + PeelConT typeName _params + | typeName == rawIdentName, SortTerm <- sort, isVarCon -> do + return ([VarP theIdent], [VarE theIdent]) + | Just _ <- lookupBindingName typeName freeFoilTermConfigs -> do + return ([], []) + | Just _ <- lookupScopeName typeName freeFoilTermConfigs -> do + binder <- newName "binder" + body <- newName "body" + return ([VarP binder, VarP body], [TupE [Just (VarE binder), Just (VarE body)]]) + | Just _ <- lookupSubTermName typeName freeFoilTermConfigs -> do + let rawSigName = toSignatureName config typeName + funName = toFreeFoilNameTo config rawSigName + x <- newName "_x" + return ([VarP x], [AppE (VarE funName) (VarE x)]) + | Just _ <- lookupSubScopeName typeName freeFoilTermConfigs -> do + let rawSigName = toSignatureName config typeName + funName = toFreeFoilNameTo config rawSigName + x <- newName "_x" + return ([VarP x], [AppE (VarE funName) (VarE x)]) + AppT _ (PeelConT typeName _params) + | Just _ <- lookupSubTermName typeName freeFoilTermConfigs -> do + let rawSigName = toSignatureName config typeName + funName = toFreeFoilNameTo config rawSigName + x <- newName "_x" + return ([VarP x], [AppE (AppE (VarE 'fmap) (VarE funName)) (VarE x)]) + | Just _ <- lookupSubScopeName typeName freeFoilTermConfigs -> do + let rawSigName = toSignatureName config typeName + funName = toFreeFoilNameTo config rawSigName + x <- newName "_x" + return ([VarP x], [AppE (AppE (VarE 'fmap) (VarE funName)) (VarE x)]) + _ -> do + x <- newName "_x" + return ([VarP x], [VarE x]) + + go :: Con -> Q [Clause] + go = \case + GadtC conNames rawArgTypes _rawRetType -> concat <$> do + theIdent <- newName "_theRawIdent" + forM conNames $ \conName -> do + let newConName = toSignatureName config conName + isVarCon = conName == rawVarConName + (concat -> pats, concat -> exps) <- unzip <$> + mapM (fromArgType isVarCon theIdent . snd) rawArgTypes + case sort of + SortTerm + | isVarCon -> return + [ Clause [ConP conName [] pats] (NormalB (ConE 'Left `AppE` VarE theIdent)) [] ] -- FIXME! + | otherwise -> return + [ Clause [ConP conName [] pats] (NormalB (ConE 'Right `AppE` (foldl AppE (ConE newConName) exps))) [] ] + _ -> return + [ Clause [ConP conName [] pats] (NormalB (foldl AppE (ConE newConName) exps)) [] ] + NormalC conName types -> go (GadtC [conName] types rawRetType) + RecC conName types -> go (NormalC conName (map removeName types)) + InfixC l conName r -> go (GadtC [conName] [l, r] rawRetType) + ForallC _params _ctx con -> go con + RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType) + +rawIdentNamesOfQuantifiedName :: Name -> FreeFoilConfig -> Q [Name] +rawIdentNamesOfQuantifiedName rawName config = do + (_tvars, cons) <- reifyDataOrNewtype rawName + return (nub (concatMap go cons)) + where + rawRetType = error "impossible happened!" + + go :: Con -> [Name] + go = \case + GadtC _conNames rawArgTypes _rawRetType -> + concatMap (rawIdentNamesOfType config . snd) rawArgTypes + NormalC conName types -> go (GadtC [conName] types rawRetType) + RecC conName types -> go (NormalC conName (map removeName types)) + InfixC l conName r -> go (GadtC [conName] [l, r] rawRetType) + ForallC _params _ctx con -> go con + RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType) + +rawIdentNamesOfType :: FreeFoilConfig -> Type -> [Name] +rawIdentNamesOfType FreeFoilConfig{..} = go + where + go = \case + PeelConT typeName _params + | typeName `elem` rawQuantifiedNames -> [] + | typeName `elem` map rawIdentName freeFoilTermConfigs -> [typeName] + | Just FreeFoilTermConfig{..} <- lookupTermName typeName freeFoilTermConfigs -> + [rawIdentName] + | Just FreeFoilTermConfig{..} <- lookupBindingName typeName freeFoilTermConfigs -> + [rawIdentName] + | Just FreeFoilTermConfig{..} <- lookupScopeName typeName freeFoilTermConfigs -> + [rawIdentName] + | Just FreeFoilTermConfig{..} <- lookupSubTermName typeName freeFoilTermConfigs -> + [rawIdentName] + | Just FreeFoilTermConfig{..} <- lookupSubScopeName typeName freeFoilTermConfigs -> + [rawIdentName] + ForallT _bndrs _ctx type_ -> go type_ + ForallVisT _bndrs type_ -> go type_ + AppT f x -> go f <> go x + AppKindT f _k -> go f + SigT t _k -> go t + ConT{} -> [] + VarT{} -> [] + PromotedT{} -> [] + InfixT l _op r -> go l <> go r + UInfixT l _op r -> go l <> go r + PromotedInfixT l _op r -> go l <> go r + PromotedUInfixT l _op r -> go l <> go r + ParensT t -> go t + TupleT{} -> [] + UnboxedTupleT{} -> [] + UnboxedSumT{} -> [] + ArrowT{} -> [] + MulArrowT{} -> [] + EqualityT{} -> [] + ListT{} -> [] + PromotedTupleT{} -> [] + PromotedNilT{} -> [] + PromotedConsT{} -> [] + StarT{} -> [] + ConstraintT{} -> [] + LitT{} -> [] + WildCardT{} -> [] + ImplicitParamT _s t -> go t diff --git a/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoilTH.hs b/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoilTH.hs index 3acabf45..01040b19 100644 --- a/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoilTH.hs +++ b/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoilTH.hs @@ -1,16 +1,16 @@ {-# OPTIONS_GHC -fno-warn-orphans #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE DeriveTraversable #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE KindSignatures #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE PatternSynonyms #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeFamilies #-} -- | Free foil implementation of the \(\lambda\Pi\)-calculus (with pairs). -- -- Free foil provides __general__ definitions or implementations for the following: @@ -38,20 +38,20 @@ module Language.LambdaPi.Impl.FreeFoilTH where import qualified Control.Monad.Foil as Foil import Control.Monad.Foil.TH import Control.Monad.Free.Foil +import Control.Monad.Free.Foil.Generic import Control.Monad.Free.Foil.TH import Data.Bifunctor.TH import Data.Map (Map) import qualified Data.Map as Map import Data.String (IsString (..)) +import Generics.Kind.TH (deriveGenericK) +import qualified GHC.Generics as GHC import qualified Language.LambdaPi.Syntax.Abs as Raw import qualified Language.LambdaPi.Syntax.Layout as Raw import qualified Language.LambdaPi.Syntax.Lex as Raw import qualified Language.LambdaPi.Syntax.Par as Raw import qualified Language.LambdaPi.Syntax.Print as Raw import System.Exit (exitFailure) -import Control.Monad.Free.Foil.Generic -import Generics.Kind.TH (deriveGenericK) -import qualified GHC.Generics as GHC -- $setup @@ -138,9 +138,11 @@ fromTerm' :: Term' a n -> Raw.Term' a fromTerm' = convertFromAST convertFromTerm'Sig (Raw.Var (error "location missing")) - fromFoilPattern' + (fromFoilPattern' mkVarIdent) (Raw.AScopedTerm (error "location missing")) - (\n -> Raw.VarIdent ("x" ++ show n)) + mkVarIdent + where + mkVarIdent n = Raw.VarIdent ("x" ++ show n) -- | Parse scope-safe terms via raw representation. -- diff --git a/haskell/soas/LICENSE b/haskell/soas/LICENSE new file mode 100644 index 00000000..37685124 --- /dev/null +++ b/haskell/soas/LICENSE @@ -0,0 +1,28 @@ +BSD 3-Clause License + +Copyright (c) 2023, Nikolai Kudasov + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + +1. Redistributions of source code must retain the above copyright notice, this + list of conditions and the following disclaimer. + +2. Redistributions in binary form must reproduce the above copyright notice, + this list of conditions and the following disclaimer in the documentation + and/or other materials provided with the distribution. + +3. Neither the name of the copyright holder nor the names of its + contributors may be used to endorse or promote products derived from + this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" +AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE +IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE +DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE +FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL +DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR +SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER +CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, +OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/haskell/soas/README.md b/haskell/soas/README.md new file mode 100644 index 00000000..db617dfb --- /dev/null +++ b/haskell/soas/README.md @@ -0,0 +1,3 @@ +# soas + +Second-Order Abstract Syntax implemented via Free Foil (a version of SOAS). diff --git a/haskell/soas/Setup.hs b/haskell/soas/Setup.hs new file mode 100644 index 00000000..d944e79d --- /dev/null +++ b/haskell/soas/Setup.hs @@ -0,0 +1,59 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE QuasiQuotes #-} + +-- Source: https://github.com/haskell/cabal/issues/6726#issuecomment-918663262 + +-- | Custom Setup that runs bnfc to generate the language sub-libraries +-- for the parsers included in Ogma. +module Main (main) where + +import Data.List (intercalate) +import Distribution.Simple (defaultMainWithHooks, hookedPrograms, postConf, preBuild, simpleUserHooks) +import Distribution.Simple.Program (Program (..), findProgramVersion, simpleProgram) +import PyF (fmt) +import System.Exit (ExitCode (..)) +import System.Process (callCommand) + +-- | Run BNFC, happy, and alex on the grammar before the actual build step. +-- +-- All options for bnfc are hard-coded here. +main :: IO () +main = + defaultMainWithHooks $ + simpleUserHooks + { hookedPrograms = [bnfcProgram] + , postConf = \args flags packageDesc localBuildInfo -> do + let + isWindows = +#ifdef mingw32_HOST_OS + True +#else + False +#endif + -- See the details on the command in https://github.com/objectionary/normalizer/issues/347#issuecomment-2117097070 + command = intercalate "; " $ + [ "set -ex" ] <> + [ "chcp.com" | isWindows ] <> + [ "chcp.com 65001" | isWindows ] <> + [ "bnfc --haskell -d -p Language.SOAS --functor --generic -o src/ grammar/SOAS/Syntax.cf" + , "cd src/Language/SOAS/Syntax" + , "alex Lex.x" + , "happy Par.y" + , "true" + ] + + fullCommand = [fmt|bash -c ' {command} '|] + + putStrLn fullCommand + + _ <- callCommand fullCommand + + postConf simpleUserHooks args flags packageDesc localBuildInfo + } + +-- | NOTE: This should be in Cabal.Distribution.Simple.Program.Builtin. +bnfcProgram :: Program +bnfcProgram = + (simpleProgram "bnfc") + { programFindVersion = findProgramVersion "--version" id + } diff --git a/haskell/soas/app/SOAS.hs b/haskell/soas/app/SOAS.hs new file mode 100644 index 00000000..c48585d2 --- /dev/null +++ b/haskell/soas/app/SOAS.hs @@ -0,0 +1,6 @@ +module Main where + +import qualified Language.SOAS.Impl as Impl + +main :: IO () +main = Impl.defaultMain diff --git a/haskell/soas/grammar/SOAS/Syntax.cf b/haskell/soas/grammar/SOAS/Syntax.cf new file mode 100644 index 00000000..fb99a939 --- /dev/null +++ b/haskell/soas/grammar/SOAS/Syntax.cf @@ -0,0 +1,57 @@ +comment "--" ; +comment "{-" "-}" ; + +token VarIdent lower (letter | digit | '_' | '\'')* ; +token OpIdent upper (letter | digit | '_' | '\'')* ; +token MetaVarIdent '?' (letter | digit | '_' | '\'')* ; + +TermTyping. TermTyping ::= "∀" TypeBinders "." Context "⊢" ScopedTerm ":" ScopedType ; + +Context. Context ::= [MetaVarTyping] "|" [VarTyping] ; + +VarTyping. VarTyping ::= VarIdent ":" Type ; +separator VarTyping "," ; + +MetaVarTyping. MetaVarTyping ::= MetaVarIdent ":" "[" [Type] "]" Type ; +separator MetaVarTyping "," ; + +OpTyping. OpTyping ::= OpIdent ":" "∀" TypeBinders "." "(" [ScopedOpArgTyping] ")" "→" ScopedType ; + +ConstraintEq. Constraint ::= "∀" Binders "." ScopedTerm "=" ScopedTerm ; + +Unifier. Unifier ::= "[" [Subst] "]" ; + +Subst. Subst ::= MetaVarIdent "[" Binders "]" "↦" ScopedTerm ; +separator Subst "," ; + +Var. Term ::= VarIdent ; +Op. Term ::= OpIdent "(" [OpArg] ")" ; +MetaVar. Term ::= MetaVarIdent "[" [Term] "]" ; +separator Term "," ; + +OpArg. OpArg ::= Binders "." ScopedTerm ; +PlainOpArg. OpArg ::= Term ; +separator OpArg "," ; + +NoBinders. Binders ::= ; +-- OneBinder. Binders ::= VarIdent ; +SomeBinders. Binders ::= VarIdent Binders ; + +ScopedTerm. ScopedTerm ::= Term ; + +TypeFun. Type ::= Type1 "→" Type1 ; +TypeProduct. Type1 ::= Type1 "×" Type2 ; +TypeVar. Type2 ::= VarIdent ; +coercions Type 2 ; +separator Type "," ; + +NoTypeBinders. TypeBinders ::= ; +SomeTypeBinders. TypeBinders ::= VarIdent TypeBinders ; + +ScopedOpArgTyping. ScopedOpArgTyping ::= OpArgTyping ; +separator ScopedOpArgTyping "," ; + +OpArgTyping. OpArgTyping ::= [Type] "." Type ; + +ScopedType. ScopedType ::= Type ; +separator ScopedType "" ; diff --git a/haskell/soas/package.yaml b/haskell/soas/package.yaml new file mode 100644 index 00000000..1688c7f9 --- /dev/null +++ b/haskell/soas/package.yaml @@ -0,0 +1,106 @@ +name: soas +version: 0.1.0 +github: "fizruk/free-foil" +license: BSD3 +author: "Nikolai Kudasov" +maintainer: "nickolay.kudasov@gmail.com" +copyright: "2023–2024 Nikolai Kudasov, Renata Shakirova, Egor Shalagin, Karina Tyulebaeva" + +extra-source-files: + - README.md + - LICENSE + - grammar/SOAS/Syntax.cf + +synopsis: Second-Order Abstract Syntax implemented via Free Foil (a version of SOAS). +category: Language + +# To avoid duplicated efforts in documentation and dealing with the +# complications of embedding Haddock markup inside cabal files, it is +# common to point users to the README.md file. +description: Please see the README on GitHub at + +custom-setup: + dependencies: + base: ">= 4.11.0.0 && < 5.0" + Cabal: ">= 2.4.0.1 && < 4.0" + process: ">= 1.6.3.0" + PyF: + +build-tools: + alex: ">= 3.2.4" + happy: ">= 1.19.9" + BNFC:bnfc: ">= 2.9.4.1" + +dependencies: + array: ">= 0.5.3.0" + base: ">= 4.7 && < 5" + text: ">= 1.2.3.1" + containers: + bifunctors: + template-haskell: + deepseq: + free-foil: ">= 0.1.0" + kind-generics-th: + +ghc-options: + - -Wall + - -Wcompat + - -Widentities + - -Wincomplete-record-updates + - -Wincomplete-uni-patterns + # - -Wmissing-export-lists + - -Wmissing-home-modules + - -Wpartial-fields + - -Wredundant-constraints + - -optP-Wno-nonportable-include-path + +library: + source-dirs: src + when: + - condition: false + other-modules: + - Language.SOAS.Syntax.Test + - Language.SOAS.Syntax.ErrM + - Language.SOAS.Syntax.Skel + +executables: + soas: + main: SOAS.hs + source-dirs: app + ghc-options: + - -threaded + - -rtsopts + - -with-rtsopts=-N + dependencies: + - soas + +tests: + spec: + main: Spec.hs + source-dirs: test + ghc-options: + - -threaded + - -rtsopts + - -with-rtsopts=-N + dependencies: + - soas + - QuickCheck + - hspec + - hspec-discover + - mtl + + doctests: + source-dirs: + - src/ + - test/doctests + main: Main.hs + other-modules: [] + dependencies: + - soas + - doctest-parallel + when: + - condition: false + other-modules: + - Language.SOAS.Syntax.Test + - Language.SOAS.Syntax.ErrM + - Language.SOAS.Syntax.Skel diff --git a/haskell/soas/soas.cabal b/haskell/soas/soas.cabal new file mode 100644 index 00000000..94563f1c --- /dev/null +++ b/haskell/soas/soas.cabal @@ -0,0 +1,146 @@ +cabal-version: 1.24 + +-- This file has been generated from package.yaml by hpack version 0.37.0. +-- +-- see: https://github.com/sol/hpack + +name: soas +version: 0.1.0 +synopsis: Second-Order Abstract Syntax implemented via Free Foil (a version of SOAS). +description: Please see the README on GitHub at +category: Language +homepage: https://github.com/fizruk/free-foil#readme +bug-reports: https://github.com/fizruk/free-foil/issues +author: Nikolai Kudasov +maintainer: nickolay.kudasov@gmail.com +copyright: 2023–2024 Nikolai Kudasov, Renata Shakirova, Egor Shalagin, Karina Tyulebaeva +license: BSD3 +license-file: LICENSE +build-type: Custom +extra-source-files: + README.md + LICENSE + grammar/SOAS/Syntax.cf + +source-repository head + type: git + location: https://github.com/fizruk/free-foil + +custom-setup + setup-depends: + Cabal >=2.4.0.1 && <4.0 + , PyF + , base >=4.11.0.0 && <5.0 + , process >=1.6.3.0 + +library + exposed-modules: + Language.SOAS.FreeFoilConfig + Language.SOAS.Impl + Language.SOAS.Impl.Generated + Language.SOAS.Syntax.Abs + Language.SOAS.Syntax.Lex + Language.SOAS.Syntax.Par + Language.SOAS.Syntax.Print + other-modules: + Paths_soas + hs-source-dirs: + src + ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path + build-tools: + alex >=3.2.4 + , happy >=1.19.9 + build-tool-depends: + BNFC:bnfc >=2.9.4.1 + build-depends: + array >=0.5.3.0 + , base >=4.7 && <5 + , bifunctors + , containers + , deepseq + , free-foil >=0.1.0 + , kind-generics-th + , template-haskell + , text >=1.2.3.1 + default-language: Haskell2010 + +executable soas + main-is: SOAS.hs + other-modules: + Paths_soas + hs-source-dirs: + app + ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path -threaded -rtsopts -with-rtsopts=-N + build-tools: + alex >=3.2.4 + , happy >=1.19.9 + build-tool-depends: + BNFC:bnfc >=2.9.4.1 + build-depends: + array >=0.5.3.0 + , base >=4.7 && <5 + , bifunctors + , containers + , deepseq + , free-foil >=0.1.0 + , kind-generics-th + , soas + , template-haskell + , text >=1.2.3.1 + default-language: Haskell2010 + +test-suite doctests + type: exitcode-stdio-1.0 + main-is: Main.hs + hs-source-dirs: + src/ + test/doctests + ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path + build-tools: + alex >=3.2.4 + , happy >=1.19.9 + build-tool-depends: + BNFC:bnfc >=2.9.4.1 + build-depends: + array >=0.5.3.0 + , base >=4.7 && <5 + , bifunctors + , containers + , deepseq + , doctest-parallel + , free-foil >=0.1.0 + , kind-generics-th + , soas + , template-haskell + , text >=1.2.3.1 + default-language: Haskell2010 + +test-suite spec + type: exitcode-stdio-1.0 + main-is: Spec.hs + other-modules: + Paths_soas + hs-source-dirs: + test + ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path -threaded -rtsopts -with-rtsopts=-N + build-tools: + alex >=3.2.4 + , happy >=1.19.9 + build-tool-depends: + BNFC:bnfc >=2.9.4.1 + build-depends: + QuickCheck + , array >=0.5.3.0 + , base >=4.7 && <5 + , bifunctors + , containers + , deepseq + , free-foil >=0.1.0 + , hspec + , hspec-discover + , kind-generics-th + , mtl + , soas + , template-haskell + , text >=1.2.3.1 + default-language: Haskell2010 diff --git a/haskell/soas/src/Language/SOAS/FreeFoilConfig.hs b/haskell/soas/src/Language/SOAS/FreeFoilConfig.hs new file mode 100644 index 00000000..3a53e937 --- /dev/null +++ b/haskell/soas/src/Language/SOAS/FreeFoilConfig.hs @@ -0,0 +1,71 @@ +{-# LANGUAGE TemplateHaskell #-} +module Language.SOAS.FreeFoilConfig where + +import qualified Language.SOAS.Syntax.Abs as Raw +import Control.Monad.Free.Foil.TH.MkFreeFoil + +intToVarIdent :: Int -> Raw.VarIdent +intToVarIdent i = Raw.VarIdent ("x" <> show i) + +rawVar :: Raw.VarIdent -> Raw.Term' a +rawVar = Raw.Var (error "trying to access an erased annotation") + +rawTypeVar :: Raw.VarIdent -> Raw.Type' a +rawTypeVar = Raw.TypeVar (error "trying to access an erased annotation") + +rawScopedTerm :: Raw.Term' a -> Raw.ScopedTerm' a +rawScopedTerm = Raw.ScopedTerm (error "trying to access an erased annotation") + +rawScopedType :: Raw.Type' a -> Raw.ScopedType' a +rawScopedType = Raw.ScopedType (error "trying to access an erased annotation") + +rawScopeToTerm :: Raw.ScopedTerm' a -> Raw.Term' a +rawScopeToTerm (Raw.ScopedTerm _loc term) = term + +rawScopeToType :: Raw.ScopedType' a -> Raw.Type' a +rawScopeToType (Raw.ScopedType _loc type_) = type_ + +soasConfig :: FreeFoilConfig +soasConfig = FreeFoilConfig + { rawQuantifiedNames = + [ ''Raw.Subst' + , ''Raw.MetaVarTyping' + , ''Raw.OpTyping' + , ''Raw.Constraint' + , ''Raw.VarTyping' + , ''Raw.TermTyping' + ] + , freeFoilTermConfigs = + [ FreeFoilTermConfig + { rawIdentName = ''Raw.VarIdent + , rawTermName = ''Raw.Term' + , rawBindingName = ''Raw.Binders' + , rawScopeName = ''Raw.ScopedTerm' + , rawVarConName = 'Raw.Var + , rawSubTermNames = [ ''Raw.OpArg' ] + , rawSubScopeNames = [] + , intToRawIdentName = 'intToVarIdent + , rawVarIdentToTermName = 'rawVar + , rawTermToScopeName = 'rawScopedTerm + , rawScopeToTermName = 'rawScopeToTerm + } + , FreeFoilTermConfig + { rawIdentName = ''Raw.VarIdent + , rawTermName = ''Raw.Type' + , rawBindingName = ''Raw.TypeBinders' + , rawScopeName = ''Raw.ScopedType' + , rawVarConName = 'Raw.TypeVar + , rawSubTermNames = [ ''Raw.OpArgTyping' ] + , rawSubScopeNames = [ ''Raw.ScopedOpArgTyping' ] + , intToRawIdentName = 'intToVarIdent + , rawVarIdentToTermName = 'rawTypeVar + , rawTermToScopeName = 'rawScopedType + , rawScopeToTermName = 'rawScopeToType + } ] + , freeFoilNameModifier = id + , freeFoilScopeNameModifier = ("Scoped" ++ ) + , freeFoilConNameModifier = id + , freeFoilConvertFromName = ("from" ++ ) + , freeFoilConvertToName = ("to" ++ ) + , signatureNameModifier = (++ "Sig") + } diff --git a/haskell/soas/src/Language/SOAS/Impl.hs b/haskell/soas/src/Language/SOAS/Impl.hs new file mode 100644 index 00000000..a0d30a61 --- /dev/null +++ b/haskell/soas/src/Language/SOAS/Impl.hs @@ -0,0 +1,89 @@ +{-# OPTIONS_GHC -Wno-orphans -Wno-redundant-constraints -ddump-splices #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TemplateHaskell #-} +-- | Functions over Second-Order Abstract Syntax (SOAS) +-- represented using scope-safe Haskell types (via Free Foil). +module Language.SOAS.Impl where + +import Data.List (find) +import Data.Bifunctor +import qualified Control.Monad.Foil as Foil +import Control.Monad.Free.Foil +import Language.SOAS.Impl.Generated +import qualified Language.SOAS.Syntax.Abs as Raw +import qualified Language.SOAS.Syntax.Lex as Raw +import qualified Language.SOAS.Syntax.Par as Raw +import qualified Language.SOAS.Syntax.Print as Raw +import System.Exit (exitFailure) + +-- $setup +-- >>> :set -XOverloadedStrings +-- >>> :set -XDataKinds +-- >>> import qualified Control.Monad.Foil as Foil +-- >>> import Control.Monad.Free.Foil +-- >>> import Data.String (fromString) + +-- * Standard Types + +-- | Standard terms with source code location annotations. +type Term = Term' Raw.BNFC'Position +-- | Standard types with source code location annotations. +type Type = Type' Raw.BNFC'Position + +-- | Standard metavariable substitutions with source code location annotations. +type Subst = Subst' Raw.BNFC'Position Foil.VoidS +-- | Standard unification constraints with source code location annotations. +type Constraint = Constraint' Raw.BNFC'Position Foil.VoidS +-- | Standard operator typings with source code location annotations. +type OpTyping = OpTyping' Raw.BNFC'Position Foil.VoidS + +-- * Metavariable substitutions + +-- | Lookup a substitution by its 'Raw.MetaVarIdent'. +-- +-- >>> lookupSubst "?m" ["?n[] ↦ Zero()", "?m[x y] ↦ App(y, x)"] +-- Just ?m [x0 x1] ↦ App (x1, x0) +lookupSubst :: Raw.MetaVarIdent -> [Subst] -> Maybe Subst +lookupSubst m = find $ \(Subst _loc m' _ _) -> m == m' + +-- | Apply meta variable substitutions to a term. +-- +-- >>> applySubsts Foil.emptyScope ["?m[x y] ↦ Lam(z. App(z, App(x, y)))"] "Lam(x. ?m[App(x, ?m[x, x]), x])" +-- Lam (x0 . Lam (x2 . App (x2, App (App (x0, ?m [x0, x0]), x0)))) +applySubsts :: Foil.Distinct n => Foil.Scope n -> [Subst] -> Term n -> Term n +applySubsts scope substs term = + case term of + MetaVar _loc m args | Just (Subst _ _ binders body) <- lookupSubst m substs -> + substitutePattern scope Foil.voidSubst binders args body + Var{} -> term + Node node -> Node (bimap goScoped (applySubsts scope substs) node) + where + goScoped (ScopedAST binders body) = + case Foil.assertDistinct binders of + Foil.Distinct -> + let scope' = Foil.extendScopePattern binders scope + in ScopedAST binders (applySubsts scope' substs body) + +-- * Entrypoint + +-- | A SOAS interpreter implemented via the free foil. +defaultMain :: IO () +defaultMain = do + input <- getContents + case Raw.pTermTyping (Raw.tokens input) of + Left err -> do + putStrLn err + exitFailure + Right typing -> putStrLn (Raw.printTree typing) diff --git a/haskell/soas/src/Language/SOAS/Impl/Generated.hs b/haskell/soas/src/Language/SOAS/Impl/Generated.hs new file mode 100644 index 00000000..bdd0fb57 --- /dev/null +++ b/haskell/soas/src/Language/SOAS/Impl/Generated.hs @@ -0,0 +1,152 @@ +{-# OPTIONS_GHC -Wno-orphans -Wno-redundant-constraints #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TemplateHaskell #-} +module Language.SOAS.Impl.Generated where + +import Data.Bifunctor.TH +import qualified Data.Map as Map +import Data.String (IsString(..)) +import qualified Control.Monad.Foil as Foil +import Control.Monad.Free.Foil.TH.MkFreeFoil +import Control.Monad.Free.Foil +import qualified Language.SOAS.Syntax.Abs as Raw +import qualified Language.SOAS.Syntax.Lex as Raw +import qualified Language.SOAS.Syntax.Par as Raw +import qualified Language.SOAS.Syntax.Print as Raw +import Control.Monad.Free.Foil.Generic +import Generics.Kind.TH (deriveGenericK) +import Language.SOAS.FreeFoilConfig (soasConfig) + +-- $setup +-- >>> :set -XOverloadedStrings +-- >>> :set -XDataKinds +-- >>> import qualified Control.Monad.Foil as Foil +-- >>> import qualified Language.SOAS.Syntax.Abs as Raw +-- >>> import Control.Monad.Free.Foil +-- >>> import Data.String (fromString) + +-- * Generated code + +mkFreeFoil soasConfig + +deriveGenericK ''OpArg'Sig +deriveGenericK ''Term'Sig +deriveGenericK ''OpArgTyping'Sig +deriveGenericK ''Type'Sig + +deriveBifunctor ''OpArg'Sig +deriveBifunctor ''Term'Sig +deriveBifunctor ''OpArgTyping'Sig +deriveBifunctor ''ScopedOpArgTyping'Sig +deriveBifunctor ''Type'Sig + +-- FIXME: derive via GenericK +instance Foil.CoSinkable (Binders' a) where + coSinkabilityProof rename (NoBinders loc) cont = cont rename (NoBinders loc) + -- coSinkabilityProof rename (OneBinder loc binder) cont = + -- Foil.coSinkabilityProof rename binder $ \rename' binder' -> + -- cont rename' (OneBinder loc binder') + coSinkabilityProof rename (SomeBinders loc binder binders) cont = + Foil.coSinkabilityProof rename binder $ \rename' binder' -> + Foil.coSinkabilityProof rename' binders $ \rename'' binders' -> + cont rename'' (SomeBinders loc binder' binders') + + withPattern withBinder unit comp scope binders cont = + case binders of + NoBinders loc -> cont unit (NoBinders loc) + -- OneBinder loc binder -> + -- Foil.withPattern withBinder unit comp scope binder $ \f binder' -> + -- cont f (OneBinder loc binder') + SomeBinders loc binder moreBinders -> + Foil.withPattern withBinder unit comp scope binder $ \f binder' -> + let scope' = Foil.extendScopePattern binder' scope + in Foil.withPattern withBinder unit comp scope' moreBinders $ \g moreBinders' -> + cont (comp f g) (SomeBinders loc binder' moreBinders') + +-- FIXME: derive via GenericK +instance Foil.CoSinkable (TypeBinders' a) where + coSinkabilityProof rename (NoTypeBinders loc) cont = cont rename (NoTypeBinders loc) + coSinkabilityProof rename (SomeTypeBinders loc binder binders) cont = + Foil.coSinkabilityProof rename binder $ \rename' binder' -> + Foil.coSinkabilityProof rename' binders $ \rename'' binders' -> + cont rename'' (SomeTypeBinders loc binder' binders') + + withPattern withBinder unit comp scope binders cont = + case binders of + NoTypeBinders loc -> cont unit (NoTypeBinders loc) + SomeTypeBinders loc binder moreTypeBinders -> + Foil.withPattern withBinder unit comp scope binder $ \f binder' -> + let scope' = Foil.extendScopePattern binder' scope + in Foil.withPattern withBinder unit comp scope' moreTypeBinders $ \g moreTypeBinders' -> + cont (comp f g) (SomeTypeBinders loc binder' moreTypeBinders') + +mkFreeFoilConversions soasConfig + +-- | Ignore 'Raw.BNFC'Position' when matching terms. +instance ZipMatchK Raw.BNFC'Position where zipMatchWithK = zipMatchViaChooseLeft +-- | Match 'Raw.OpIdent' via 'Eq'. +instance ZipMatchK Raw.OpIdent where zipMatchWithK = zipMatchViaEq +-- | Match 'Raw.MetaVarIdent' via 'Eq'. +instance ZipMatchK Raw.MetaVarIdent where zipMatchWithK = zipMatchViaEq + +instance ZipMatchK a => ZipMatchK (Term'Sig a) +instance ZipMatchK a => ZipMatchK (OpArg'Sig a) +instance ZipMatchK a => ZipMatchK (Type'Sig a) + +instance ZipMatchK a => ZipMatch (Term'Sig a) where zipMatch = genericZipMatch2 +instance ZipMatchK a => ZipMatch (Type'Sig a) where zipMatch = genericZipMatch2 + +-- | +-- >>> "?m[App(Lam(x.x), Lam(y.y))]" :: Term' Raw.BNFC'Position Foil.VoidS +-- ?m [App (Lam (x0 . x0), Lam (x0 . x0))] +-- >>> "Lam(y. Let(Lam(x. x), f. ?m[y, App(f, y)]))" :: Term' Raw.BNFC'Position Foil.VoidS +-- Lam (x0 . Let (Lam (x1 . x1), x1 . ?m [x0, App (x1, x0)])) +instance IsString (Term' Raw.BNFC'Position Foil.VoidS) where + fromString = toTerm' Foil.emptyScope Map.empty . unsafeParse Raw.pTerm + +instance IsString (Type' Raw.BNFC'Position Foil.VoidS) where + fromString = toType' Foil.emptyScope Map.empty . unsafeParse Raw.pType + +-- | +-- >>> "Lam : ∀ a b. (a.b) → a→b" :: OpTyping' Raw.BNFC'Position Foil.VoidS +-- Lam : ∀ x0 x1 . (x0 . x1) → x0 → x1 +instance IsString (OpTyping' Raw.BNFC'Position Foil.VoidS) where + fromString = toOpTyping' Foil.emptyScope Map.empty . unsafeParse Raw.pOpTyping + +-- | +-- >>> "?m[x y] ↦ App(y, x)" :: Subst' Raw.BNFC'Position Foil.VoidS +-- ?m [x0 x1] ↦ App (x1, x0) +instance IsString (Subst' Raw.BNFC'Position Foil.VoidS) where + fromString = toSubst' Foil.emptyScope Map.empty . unsafeParse Raw.pSubst + +-- | +-- >>> "∀ x y. ?m[x, y] = App(y, x)" :: Constraint' Raw.BNFC'Position Foil.VoidS +-- ∀ x0 x1 . ?m [x0, x1] = App (x1, x0) +instance IsString (Constraint' Raw.BNFC'Position Foil.VoidS) where + fromString = toConstraint' Foil.emptyScope Map.empty . unsafeParse Raw.pConstraint + +instance Show (Term' a n) where show = Raw.printTree . fromTerm' +instance Show (Type' a n) where show = Raw.printTree . fromType' +instance Show (Subst' a n) where show = Raw.printTree . fromSubst' +instance Show (Constraint' a n) where show = Raw.printTree . fromConstraint' +instance Show (OpTyping' a n) where show = Raw.printTree . fromOpTyping' + +-- * User-defined helpers + +unsafeParse :: ([Raw.Token] -> Either String a) -> String -> a +unsafeParse parse input = + case parse (Raw.myLexer input) of + Left err -> error err + Right x -> x diff --git a/haskell/soas/src/Language/SOAS/Syntax/Abs.hs b/haskell/soas/src/Language/SOAS/Syntax/Abs.hs new file mode 100644 index 00000000..668087ab --- /dev/null +++ b/haskell/soas/src/Language/SOAS/Syntax/Abs.hs @@ -0,0 +1,204 @@ +-- File generated by the BNF Converter (bnfc 2.9.5). + +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE PatternSynonyms #-} + +-- | The abstract syntax of language Syntax. + +module Language.SOAS.Syntax.Abs where + +import Prelude (String) +import qualified Prelude as C + ( Eq, Ord, Show, Read + , Functor, Foldable, Traversable + , Int, Maybe(..) + ) +import qualified Data.String + +import qualified Data.Data as C (Data, Typeable) +import qualified GHC.Generics as C (Generic) + +type TermTyping = TermTyping' BNFC'Position +data TermTyping' a + = TermTyping a (TypeBinders' a) (Context' a) (ScopedTerm' a) (ScopedType' a) + deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic) + +type Context = Context' BNFC'Position +data Context' a = Context a [MetaVarTyping' a] [VarTyping' a] + deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic) + +type VarTyping = VarTyping' BNFC'Position +data VarTyping' a = VarTyping a VarIdent (Type' a) + deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic) + +type MetaVarTyping = MetaVarTyping' BNFC'Position +data MetaVarTyping' a + = MetaVarTyping a MetaVarIdent [Type' a] (Type' a) + deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic) + +type OpTyping = OpTyping' BNFC'Position +data OpTyping' a + = OpTyping a OpIdent (TypeBinders' a) [ScopedOpArgTyping' a] (ScopedType' a) + deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic) + +type Constraint = Constraint' BNFC'Position +data Constraint' a + = ConstraintEq a (Binders' a) (ScopedTerm' a) (ScopedTerm' a) + deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic) + +type Unifier = Unifier' BNFC'Position +data Unifier' a = Unifier a [Subst' a] + deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic) + +type Subst = Subst' BNFC'Position +data Subst' a = Subst a MetaVarIdent (Binders' a) (ScopedTerm' a) + deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic) + +type Term = Term' BNFC'Position +data Term' a + = Var a VarIdent + | Op a OpIdent [OpArg' a] + | MetaVar a MetaVarIdent [Term' a] + deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic) + +type OpArg = OpArg' BNFC'Position +data OpArg' a + = OpArg a (Binders' a) (ScopedTerm' a) | PlainOpArg a (Term' a) + deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic) + +type Binders = Binders' BNFC'Position +data Binders' a = NoBinders a | SomeBinders a VarIdent (Binders' a) + deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic) + +type ScopedTerm = ScopedTerm' BNFC'Position +data ScopedTerm' a = ScopedTerm a (Term' a) + deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic) + +type Type = Type' BNFC'Position +data Type' a + = TypeFun a (Type' a) (Type' a) + | TypeProduct a (Type' a) (Type' a) + | TypeVar a VarIdent + deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic) + +type TypeBinders = TypeBinders' BNFC'Position +data TypeBinders' a + = NoTypeBinders a | SomeTypeBinders a VarIdent (TypeBinders' a) + deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic) + +type ScopedOpArgTyping = ScopedOpArgTyping' BNFC'Position +data ScopedOpArgTyping' a = ScopedOpArgTyping a (OpArgTyping' a) + deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic) + +type OpArgTyping = OpArgTyping' BNFC'Position +data OpArgTyping' a = OpArgTyping a [Type' a] (Type' a) + deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic) + +type ScopedType = ScopedType' BNFC'Position +data ScopedType' a = ScopedType a (Type' a) + deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic) + +newtype VarIdent = VarIdent String + deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic, Data.String.IsString) + +newtype OpIdent = OpIdent String + deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic, Data.String.IsString) + +newtype MetaVarIdent = MetaVarIdent String + deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic, Data.String.IsString) + +-- | Start position (line, column) of something. + +type BNFC'Position = C.Maybe (C.Int, C.Int) + +pattern BNFC'NoPosition :: BNFC'Position +pattern BNFC'NoPosition = C.Nothing + +pattern BNFC'Position :: C.Int -> C.Int -> BNFC'Position +pattern BNFC'Position line col = C.Just (line, col) + +-- | Get the start position of something. + +class HasPosition a where + hasPosition :: a -> BNFC'Position + +instance HasPosition TermTyping where + hasPosition = \case + TermTyping p _ _ _ _ -> p + +instance HasPosition Context where + hasPosition = \case + Context p _ _ -> p + +instance HasPosition VarTyping where + hasPosition = \case + VarTyping p _ _ -> p + +instance HasPosition MetaVarTyping where + hasPosition = \case + MetaVarTyping p _ _ _ -> p + +instance HasPosition OpTyping where + hasPosition = \case + OpTyping p _ _ _ _ -> p + +instance HasPosition Constraint where + hasPosition = \case + ConstraintEq p _ _ _ -> p + +instance HasPosition Unifier where + hasPosition = \case + Unifier p _ -> p + +instance HasPosition Subst where + hasPosition = \case + Subst p _ _ _ -> p + +instance HasPosition Term where + hasPosition = \case + Var p _ -> p + Op p _ _ -> p + MetaVar p _ _ -> p + +instance HasPosition OpArg where + hasPosition = \case + OpArg p _ _ -> p + PlainOpArg p _ -> p + +instance HasPosition Binders where + hasPosition = \case + NoBinders p -> p + SomeBinders p _ _ -> p + +instance HasPosition ScopedTerm where + hasPosition = \case + ScopedTerm p _ -> p + +instance HasPosition Type where + hasPosition = \case + TypeFun p _ _ -> p + TypeProduct p _ _ -> p + TypeVar p _ -> p + +instance HasPosition TypeBinders where + hasPosition = \case + NoTypeBinders p -> p + SomeTypeBinders p _ _ -> p + +instance HasPosition ScopedOpArgTyping where + hasPosition = \case + ScopedOpArgTyping p _ -> p + +instance HasPosition OpArgTyping where + hasPosition = \case + OpArgTyping p _ _ -> p + +instance HasPosition ScopedType where + hasPosition = \case + ScopedType p _ -> p + diff --git a/haskell/soas/src/Language/SOAS/Syntax/Doc.txt b/haskell/soas/src/Language/SOAS/Syntax/Doc.txt new file mode 100644 index 00000000..d40cec0d --- /dev/null +++ b/haskell/soas/src/Language/SOAS/Syntax/Doc.txt @@ -0,0 +1,103 @@ +The Language Syntax +BNF Converter + + +%Process by txt2tags to generate html or latex + + + +This document was automatically generated by the //BNF-Converter//. It was generated together with the lexer, the parser, and the abstract syntax module, which guarantees that the document matches with the implementation of the language (provided no hand-hacking has taken place). + +==The lexical structure of Syntax== + +===Literals=== + + + + +VarIdent literals are recognized by the regular expression +`````lower (["'_"] | digit | letter)*````` + +OpIdent literals are recognized by the regular expression +`````upper (["'_"] | digit | letter)*````` + +MetaVarIdent literals are recognized by the regular expression +`````'?' (["'_"] | digit | letter)*````` + + +===Reserved words and symbols=== +The set of reserved words is the set of terminals appearing in the grammar. Those reserved words that consist of non-letter characters are called symbols, and they are treated in a different way from those that are similar to identifiers. The lexer follows rules familiar from languages like Haskell, C, and Java, including longest match and spacing conventions. + +The reserved words used in Syntax are the following: + +There are no reserved words in Syntax. + +The symbols used in Syntax are the following: + | ∀ | . | ⊢ | : + | | | , | [ | ] + | ( | ) | → | = + | ↦ | × | | + +===Comments=== +Single-line comments begin with --.Multiple-line comments are enclosed with {- and -}. + +==The syntactic structure of Syntax== +Non-terminals are enclosed between < and >. +The symbols -> (production), **|** (union) +and **eps** (empty rule) belong to the BNF notation. +All other symbols are terminals. + + | //TermTyping// | -> | ``∀`` //TypeBinders// ``.`` //Context// ``⊢`` //ScopedTerm// ``:`` //ScopedType// + | //Context// | -> | //[MetaVarTyping]// ``|`` //[VarTyping]// + | //VarTyping// | -> | //VarIdent// ``:`` //Type// + | //[VarTyping]// | -> | **eps** + | | **|** | //VarTyping// + | | **|** | //VarTyping// ``,`` //[VarTyping]// + | //MetaVarTyping// | -> | //MetaVarIdent// ``:`` ``[`` //[Type]// ``]`` //Type// + | //[MetaVarTyping]// | -> | **eps** + | | **|** | //MetaVarTyping// + | | **|** | //MetaVarTyping// ``,`` //[MetaVarTyping]// + | //OpTyping// | -> | //OpIdent// ``:`` ``∀`` //TypeBinders// ``.`` ``(`` //[ScopedOpArgTyping]// ``)`` ``→`` //ScopedType// + | //Constraint// | -> | ``∀`` //Binders// ``.`` //ScopedTerm// ``=`` //ScopedTerm// + | //Unifier// | -> | ``[`` //[Subst]// ``]`` + | //Subst// | -> | //MetaVarIdent// ``[`` //Binders// ``]`` ``↦`` //ScopedTerm// + | //[Subst]// | -> | **eps** + | | **|** | //Subst// + | | **|** | //Subst// ``,`` //[Subst]// + | //Term// | -> | //VarIdent// + | | **|** | //OpIdent// ``(`` //[OpArg]// ``)`` + | | **|** | //MetaVarIdent// ``[`` //[Term]// ``]`` + | //[Term]// | -> | **eps** + | | **|** | //Term// + | | **|** | //Term// ``,`` //[Term]// + | //OpArg// | -> | //Binders// ``.`` //ScopedTerm// + | | **|** | //Term// + | //[OpArg]// | -> | **eps** + | | **|** | //OpArg// + | | **|** | //OpArg// ``,`` //[OpArg]// + | //Binders// | -> | **eps** + | | **|** | //VarIdent// //Binders// + | //ScopedTerm// | -> | //Term// + | //Type// | -> | //Type1// ``→`` //Type1// + | | **|** | //Type1// + | //Type1// | -> | //Type1// ``×`` //Type2// + | | **|** | //Type2// + | //Type2// | -> | //VarIdent// + | | **|** | ``(`` //Type// ``)`` + | //[Type]// | -> | **eps** + | | **|** | //Type// + | | **|** | //Type// ``,`` //[Type]// + | //TypeBinders// | -> | **eps** + | | **|** | //VarIdent// //TypeBinders// + | //ScopedOpArgTyping// | -> | //OpArgTyping// + | //[ScopedOpArgTyping]// | -> | **eps** + | | **|** | //ScopedOpArgTyping// + | | **|** | //ScopedOpArgTyping// ``,`` //[ScopedOpArgTyping]// + | //OpArgTyping// | -> | //[Type]// ``.`` //Type// + | //ScopedType// | -> | //Type// + | //[ScopedType]// | -> | **eps** + | | **|** | //ScopedType// //[ScopedType]// + + + +%% File generated by the BNF Converter (bnfc 2.9.5). diff --git a/haskell/soas/src/Language/SOAS/Syntax/Lex.x b/haskell/soas/src/Language/SOAS/Syntax/Lex.x new file mode 100644 index 00000000..78690ca7 --- /dev/null +++ b/haskell/soas/src/Language/SOAS/Syntax/Lex.x @@ -0,0 +1,264 @@ +-- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.5). + +-- Lexer definition for use with Alex 3 +{ +{-# OPTIONS -fno-warn-incomplete-patterns #-} +{-# OPTIONS_GHC -w #-} + +{-# LANGUAGE PatternSynonyms #-} + +module Language.SOAS.Syntax.Lex where + +import Prelude + +import qualified Data.Bits +import Data.Char (ord) +import Data.Function (on) +import Data.Word (Word8) +} + +-- Predefined character classes + +$c = [A-Z\192-\221] # [\215] -- capital isolatin1 letter (215 = \times) FIXME +$s = [a-z\222-\255] # [\247] -- small isolatin1 letter (247 = \div ) FIXME +$l = [$c $s] -- letter +$d = [0-9] -- digit +$i = [$l $d _ '] -- identifier character +$u = [. \n] -- universal: any character + +-- Symbols and non-identifier-like reserved words + +@rsyms = \∀ | \. | \⊢ | \: | \| | \, | \[ | \] | \( | \) | \→ | \= | \↦ | \× + +:- + +-- Line comment "--" +"--" [.]* ; + +-- Block comment "{-" "-}" +\{ \- [$u # \-]* \- ([$u # [\- \}]] [$u # \-]* \- | \-)* \} ; + +-- Whitespace (skipped) +$white+ ; + +-- Symbols +@rsyms + { tok (eitherResIdent TV) } + +-- token VarIdent +$s ([\' \_]| ($d | $l)) * + { tok (eitherResIdent T_VarIdent) } + +-- token OpIdent +$c ([\' \_]| ($d | $l)) * + { tok (eitherResIdent T_OpIdent) } + +-- token MetaVarIdent +\? ([\' \_]| ($d | $l)) * + { tok (eitherResIdent T_MetaVarIdent) } + +-- Keywords and Ident +$l $i* + { tok (eitherResIdent TV) } + +{ +-- | Create a token with position. +tok :: (String -> Tok) -> (Posn -> String -> Token) +tok f p = PT p . f + +-- | Token without position. +data Tok + = TK {-# UNPACK #-} !TokSymbol -- ^ Reserved word or symbol. + | TL !String -- ^ String literal. + | TI !String -- ^ Integer literal. + | TV !String -- ^ Identifier. + | TD !String -- ^ Float literal. + | TC !String -- ^ Character literal. + | T_VarIdent !String + | T_OpIdent !String + | T_MetaVarIdent !String + deriving (Eq, Show, Ord) + +-- | Smart constructor for 'Tok' for the sake of backwards compatibility. +pattern TS :: String -> Int -> Tok +pattern TS t i = TK (TokSymbol t i) + +-- | Keyword or symbol tokens have a unique ID. +data TokSymbol = TokSymbol + { tsText :: String + -- ^ Keyword or symbol text. + , tsID :: !Int + -- ^ Unique ID. + } deriving (Show) + +-- | Keyword/symbol equality is determined by the unique ID. +instance Eq TokSymbol where (==) = (==) `on` tsID + +-- | Keyword/symbol ordering is determined by the unique ID. +instance Ord TokSymbol where compare = compare `on` tsID + +-- | Token with position. +data Token + = PT Posn Tok + | Err Posn + deriving (Eq, Show, Ord) + +-- | Pretty print a position. +printPosn :: Posn -> String +printPosn (Pn _ l c) = "line " ++ show l ++ ", column " ++ show c + +-- | Pretty print the position of the first token in the list. +tokenPos :: [Token] -> String +tokenPos (t:_) = printPosn (tokenPosn t) +tokenPos [] = "end of file" + +-- | Get the position of a token. +tokenPosn :: Token -> Posn +tokenPosn (PT p _) = p +tokenPosn (Err p) = p + +-- | Get line and column of a token. +tokenLineCol :: Token -> (Int, Int) +tokenLineCol = posLineCol . tokenPosn + +-- | Get line and column of a position. +posLineCol :: Posn -> (Int, Int) +posLineCol (Pn _ l c) = (l,c) + +-- | Convert a token into "position token" form. +mkPosToken :: Token -> ((Int, Int), String) +mkPosToken t = (tokenLineCol t, tokenText t) + +-- | Convert a token to its text. +tokenText :: Token -> String +tokenText t = case t of + PT _ (TS s _) -> s + PT _ (TL s) -> show s + PT _ (TI s) -> s + PT _ (TV s) -> s + PT _ (TD s) -> s + PT _ (TC s) -> s + Err _ -> "#error" + PT _ (T_VarIdent s) -> s + PT _ (T_OpIdent s) -> s + PT _ (T_MetaVarIdent s) -> s + +-- | Convert a token to a string. +prToken :: Token -> String +prToken t = tokenText t + +-- | Finite map from text to token organized as binary search tree. +data BTree + = N -- ^ Nil (leaf). + | B String Tok BTree BTree + -- ^ Binary node. + deriving (Show) + +-- | Convert potential keyword into token or use fallback conversion. +eitherResIdent :: (String -> Tok) -> String -> Tok +eitherResIdent tv s = treeFind resWords + where + treeFind N = tv s + treeFind (B a t left right) = + case compare s a of + LT -> treeFind left + GT -> treeFind right + EQ -> t + +-- | The keywords and symbols of the language organized as binary search tree. +resWords :: BTree +resWords = + b "]" 8 + (b "." 4 + (b ")" 2 (b "(" 1 N N) (b "," 3 N N)) + (b "=" 6 (b ":" 5 N N) (b "[" 7 N N))) + (b "\8614" 12 + (b "\215" 10 (b "|" 9 N N) (b "\8594" 11 N N)) + (b "\8866" 14 (b "\8704" 13 N N) N)) + where + b s n = B bs (TS bs n) + where + bs = s + +-- | Unquote string literal. +unescapeInitTail :: String -> String +unescapeInitTail = id . unesc . tail . id + where + unesc s = case s of + '\\':c:cs | elem c ['\"', '\\', '\''] -> c : unesc cs + '\\':'n':cs -> '\n' : unesc cs + '\\':'t':cs -> '\t' : unesc cs + '\\':'r':cs -> '\r' : unesc cs + '\\':'f':cs -> '\f' : unesc cs + '"':[] -> [] + c:cs -> c : unesc cs + _ -> [] + +------------------------------------------------------------------- +-- Alex wrapper code. +-- A modified "posn" wrapper. +------------------------------------------------------------------- + +data Posn = Pn !Int !Int !Int + deriving (Eq, Show, Ord) + +alexStartPos :: Posn +alexStartPos = Pn 0 1 1 + +alexMove :: Posn -> Char -> Posn +alexMove (Pn a l c) '\t' = Pn (a+1) l (((c+7) `div` 8)*8+1) +alexMove (Pn a l c) '\n' = Pn (a+1) (l+1) 1 +alexMove (Pn a l c) _ = Pn (a+1) l (c+1) + +type Byte = Word8 + +type AlexInput = (Posn, -- current position, + Char, -- previous char + [Byte], -- pending bytes on the current char + String) -- current input string + +tokens :: String -> [Token] +tokens str = go (alexStartPos, '\n', [], str) + where + go :: AlexInput -> [Token] + go inp@(pos, _, _, str) = + case alexScan inp 0 of + AlexEOF -> [] + AlexError (pos, _, _, _) -> [Err pos] + AlexSkip inp' len -> go inp' + AlexToken inp' len act -> act pos (take len str) : (go inp') + +alexGetByte :: AlexInput -> Maybe (Byte,AlexInput) +alexGetByte (p, c, (b:bs), s) = Just (b, (p, c, bs, s)) +alexGetByte (p, _, [], s) = + case s of + [] -> Nothing + (c:s) -> + let p' = alexMove p c + (b:bs) = utf8Encode c + in p' `seq` Just (b, (p', c, bs, s)) + +alexInputPrevChar :: AlexInput -> Char +alexInputPrevChar (p, c, bs, s) = c + +-- | Encode a Haskell String to a list of Word8 values, in UTF8 format. +utf8Encode :: Char -> [Word8] +utf8Encode = map fromIntegral . go . ord + where + go oc + | oc <= 0x7f = [oc] + + | oc <= 0x7ff = [ 0xc0 + (oc `Data.Bits.shiftR` 6) + , 0x80 + oc Data.Bits..&. 0x3f + ] + + | oc <= 0xffff = [ 0xe0 + (oc `Data.Bits.shiftR` 12) + , 0x80 + ((oc `Data.Bits.shiftR` 6) Data.Bits..&. 0x3f) + , 0x80 + oc Data.Bits..&. 0x3f + ] + | otherwise = [ 0xf0 + (oc `Data.Bits.shiftR` 18) + , 0x80 + ((oc `Data.Bits.shiftR` 12) Data.Bits..&. 0x3f) + , 0x80 + ((oc `Data.Bits.shiftR` 6) Data.Bits..&. 0x3f) + , 0x80 + oc Data.Bits..&. 0x3f + ] +} diff --git a/haskell/soas/src/Language/SOAS/Syntax/Par.y b/haskell/soas/src/Language/SOAS/Syntax/Par.y new file mode 100644 index 00000000..a5e599d1 --- /dev/null +++ b/haskell/soas/src/Language/SOAS/Syntax/Par.y @@ -0,0 +1,336 @@ +-- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.5). + +-- Parser definition for use with Happy +{ +{-# OPTIONS_GHC -fno-warn-incomplete-patterns -fno-warn-overlapping-patterns #-} +{-# LANGUAGE PatternSynonyms #-} + +module Language.SOAS.Syntax.Par + ( happyError + , myLexer + , pTermTyping + , pContext + , pVarTyping + , pListVarTyping + , pMetaVarTyping + , pListMetaVarTyping + , pOpTyping + , pConstraint + , pUnifier + , pSubst + , pListSubst + , pTerm + , pListTerm + , pOpArg + , pListOpArg + , pBinders + , pScopedTerm + , pType + , pType1 + , pType2 + , pListType + , pTypeBinders + , pScopedOpArgTyping + , pListScopedOpArgTyping + , pOpArgTyping + , pScopedType + , pListScopedType + ) where + +import Prelude + +import qualified Language.SOAS.Syntax.Abs +import Language.SOAS.Syntax.Lex + +} + +%name pTermTyping_internal TermTyping +%name pContext_internal Context +%name pVarTyping_internal VarTyping +%name pListVarTyping_internal ListVarTyping +%name pMetaVarTyping_internal MetaVarTyping +%name pListMetaVarTyping_internal ListMetaVarTyping +%name pOpTyping_internal OpTyping +%name pConstraint_internal Constraint +%name pUnifier_internal Unifier +%name pSubst_internal Subst +%name pListSubst_internal ListSubst +%name pTerm_internal Term +%name pListTerm_internal ListTerm +%name pOpArg_internal OpArg +%name pListOpArg_internal ListOpArg +%name pBinders_internal Binders +%name pScopedTerm_internal ScopedTerm +%name pType_internal Type +%name pType1_internal Type1 +%name pType2_internal Type2 +%name pListType_internal ListType +%name pTypeBinders_internal TypeBinders +%name pScopedOpArgTyping_internal ScopedOpArgTyping +%name pListScopedOpArgTyping_internal ListScopedOpArgTyping +%name pOpArgTyping_internal OpArgTyping +%name pScopedType_internal ScopedType +%name pListScopedType_internal ListScopedType +-- no lexer declaration +%monad { Err } { (>>=) } { return } +%tokentype {Token} +%token + '(' { PT _ (TS _ 1) } + ')' { PT _ (TS _ 2) } + ',' { PT _ (TS _ 3) } + '.' { PT _ (TS _ 4) } + ':' { PT _ (TS _ 5) } + '=' { PT _ (TS _ 6) } + '[' { PT _ (TS _ 7) } + ']' { PT _ (TS _ 8) } + '|' { PT _ (TS _ 9) } + '×' { PT _ (TS _ 10) } + '→' { PT _ (TS _ 11) } + '↦' { PT _ (TS _ 12) } + '∀' { PT _ (TS _ 13) } + '⊢' { PT _ (TS _ 14) } + L_VarIdent { PT _ (T_VarIdent _) } + L_OpIdent { PT _ (T_OpIdent _) } + L_MetaVarIdent { PT _ (T_MetaVarIdent _) } + +%% + +VarIdent :: { (Language.SOAS.Syntax.Abs.BNFC'Position, Language.SOAS.Syntax.Abs.VarIdent) } +VarIdent : L_VarIdent { (uncurry Language.SOAS.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.SOAS.Syntax.Abs.VarIdent (tokenText $1)) } + +OpIdent :: { (Language.SOAS.Syntax.Abs.BNFC'Position, Language.SOAS.Syntax.Abs.OpIdent) } +OpIdent : L_OpIdent { (uncurry Language.SOAS.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.SOAS.Syntax.Abs.OpIdent (tokenText $1)) } + +MetaVarIdent :: { (Language.SOAS.Syntax.Abs.BNFC'Position, Language.SOAS.Syntax.Abs.MetaVarIdent) } +MetaVarIdent : L_MetaVarIdent { (uncurry Language.SOAS.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.SOAS.Syntax.Abs.MetaVarIdent (tokenText $1)) } + +TermTyping :: { (Language.SOAS.Syntax.Abs.BNFC'Position, Language.SOAS.Syntax.Abs.TermTyping) } +TermTyping + : '∀' TypeBinders '.' Context '⊢' ScopedTerm ':' ScopedType { (uncurry Language.SOAS.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.SOAS.Syntax.Abs.TermTyping (uncurry Language.SOAS.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4) (snd $6) (snd $8)) } + +Context :: { (Language.SOAS.Syntax.Abs.BNFC'Position, Language.SOAS.Syntax.Abs.Context) } +Context + : ListMetaVarTyping '|' ListVarTyping { (fst $1, Language.SOAS.Syntax.Abs.Context (fst $1) (snd $1) (snd $3)) } + +VarTyping :: { (Language.SOAS.Syntax.Abs.BNFC'Position, Language.SOAS.Syntax.Abs.VarTyping) } +VarTyping + : VarIdent ':' Type { (fst $1, Language.SOAS.Syntax.Abs.VarTyping (fst $1) (snd $1) (snd $3)) } + +ListVarTyping :: { (Language.SOAS.Syntax.Abs.BNFC'Position, [Language.SOAS.Syntax.Abs.VarTyping]) } +ListVarTyping + : {- empty -} { (Language.SOAS.Syntax.Abs.BNFC'NoPosition, []) } + | VarTyping { (fst $1, (:[]) (snd $1)) } + | VarTyping ',' ListVarTyping { (fst $1, (:) (snd $1) (snd $3)) } + +MetaVarTyping :: { (Language.SOAS.Syntax.Abs.BNFC'Position, Language.SOAS.Syntax.Abs.MetaVarTyping) } +MetaVarTyping + : MetaVarIdent ':' '[' ListType ']' Type { (fst $1, Language.SOAS.Syntax.Abs.MetaVarTyping (fst $1) (snd $1) (snd $4) (snd $6)) } + +ListMetaVarTyping :: { (Language.SOAS.Syntax.Abs.BNFC'Position, [Language.SOAS.Syntax.Abs.MetaVarTyping]) } +ListMetaVarTyping + : {- empty -} { (Language.SOAS.Syntax.Abs.BNFC'NoPosition, []) } + | MetaVarTyping { (fst $1, (:[]) (snd $1)) } + | MetaVarTyping ',' ListMetaVarTyping { (fst $1, (:) (snd $1) (snd $3)) } + +OpTyping :: { (Language.SOAS.Syntax.Abs.BNFC'Position, Language.SOAS.Syntax.Abs.OpTyping) } +OpTyping + : OpIdent ':' '∀' TypeBinders '.' '(' ListScopedOpArgTyping ')' '→' ScopedType { (fst $1, Language.SOAS.Syntax.Abs.OpTyping (fst $1) (snd $1) (snd $4) (snd $7) (snd $10)) } + +Constraint :: { (Language.SOAS.Syntax.Abs.BNFC'Position, Language.SOAS.Syntax.Abs.Constraint) } +Constraint + : '∀' Binders '.' ScopedTerm '=' ScopedTerm { (uncurry Language.SOAS.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.SOAS.Syntax.Abs.ConstraintEq (uncurry Language.SOAS.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4) (snd $6)) } + +Unifier :: { (Language.SOAS.Syntax.Abs.BNFC'Position, Language.SOAS.Syntax.Abs.Unifier) } +Unifier + : '[' ListSubst ']' { (uncurry Language.SOAS.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.SOAS.Syntax.Abs.Unifier (uncurry Language.SOAS.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) } + +Subst :: { (Language.SOAS.Syntax.Abs.BNFC'Position, Language.SOAS.Syntax.Abs.Subst) } +Subst + : MetaVarIdent '[' Binders ']' '↦' ScopedTerm { (fst $1, Language.SOAS.Syntax.Abs.Subst (fst $1) (snd $1) (snd $3) (snd $6)) } + +ListSubst :: { (Language.SOAS.Syntax.Abs.BNFC'Position, [Language.SOAS.Syntax.Abs.Subst]) } +ListSubst + : {- empty -} { (Language.SOAS.Syntax.Abs.BNFC'NoPosition, []) } + | Subst { (fst $1, (:[]) (snd $1)) } + | Subst ',' ListSubst { (fst $1, (:) (snd $1) (snd $3)) } + +Term :: { (Language.SOAS.Syntax.Abs.BNFC'Position, Language.SOAS.Syntax.Abs.Term) } +Term + : VarIdent { (fst $1, Language.SOAS.Syntax.Abs.Var (fst $1) (snd $1)) } + | OpIdent '(' ListOpArg ')' { (fst $1, Language.SOAS.Syntax.Abs.Op (fst $1) (snd $1) (snd $3)) } + | MetaVarIdent '[' ListTerm ']' { (fst $1, Language.SOAS.Syntax.Abs.MetaVar (fst $1) (snd $1) (snd $3)) } + +ListTerm :: { (Language.SOAS.Syntax.Abs.BNFC'Position, [Language.SOAS.Syntax.Abs.Term]) } +ListTerm + : {- empty -} { (Language.SOAS.Syntax.Abs.BNFC'NoPosition, []) } + | Term { (fst $1, (:[]) (snd $1)) } + | Term ',' ListTerm { (fst $1, (:) (snd $1) (snd $3)) } + +OpArg :: { (Language.SOAS.Syntax.Abs.BNFC'Position, Language.SOAS.Syntax.Abs.OpArg) } +OpArg + : Binders '.' ScopedTerm { (fst $1, Language.SOAS.Syntax.Abs.OpArg (fst $1) (snd $1) (snd $3)) } + | Term { (fst $1, Language.SOAS.Syntax.Abs.PlainOpArg (fst $1) (snd $1)) } + +ListOpArg :: { (Language.SOAS.Syntax.Abs.BNFC'Position, [Language.SOAS.Syntax.Abs.OpArg]) } +ListOpArg + : {- empty -} { (Language.SOAS.Syntax.Abs.BNFC'NoPosition, []) } + | OpArg { (fst $1, (:[]) (snd $1)) } + | OpArg ',' ListOpArg { (fst $1, (:) (snd $1) (snd $3)) } + +Binders :: { (Language.SOAS.Syntax.Abs.BNFC'Position, Language.SOAS.Syntax.Abs.Binders) } +Binders + : {- empty -} { (Language.SOAS.Syntax.Abs.BNFC'NoPosition, Language.SOAS.Syntax.Abs.NoBinders Language.SOAS.Syntax.Abs.BNFC'NoPosition) } + | VarIdent Binders { (fst $1, Language.SOAS.Syntax.Abs.SomeBinders (fst $1) (snd $1) (snd $2)) } + +ScopedTerm :: { (Language.SOAS.Syntax.Abs.BNFC'Position, Language.SOAS.Syntax.Abs.ScopedTerm) } +ScopedTerm + : Term { (fst $1, Language.SOAS.Syntax.Abs.ScopedTerm (fst $1) (snd $1)) } + +Type :: { (Language.SOAS.Syntax.Abs.BNFC'Position, Language.SOAS.Syntax.Abs.Type) } +Type + : Type1 '→' Type1 { (fst $1, Language.SOAS.Syntax.Abs.TypeFun (fst $1) (snd $1) (snd $3)) } + | Type1 { (fst $1, (snd $1)) } + +Type1 :: { (Language.SOAS.Syntax.Abs.BNFC'Position, Language.SOAS.Syntax.Abs.Type) } +Type1 + : Type1 '×' Type2 { (fst $1, Language.SOAS.Syntax.Abs.TypeProduct (fst $1) (snd $1) (snd $3)) } + | Type2 { (fst $1, (snd $1)) } + +Type2 :: { (Language.SOAS.Syntax.Abs.BNFC'Position, Language.SOAS.Syntax.Abs.Type) } +Type2 + : VarIdent { (fst $1, Language.SOAS.Syntax.Abs.TypeVar (fst $1) (snd $1)) } + | '(' Type ')' { (uncurry Language.SOAS.Syntax.Abs.BNFC'Position (tokenLineCol $1), (snd $2)) } + +ListType :: { (Language.SOAS.Syntax.Abs.BNFC'Position, [Language.SOAS.Syntax.Abs.Type]) } +ListType + : {- empty -} { (Language.SOAS.Syntax.Abs.BNFC'NoPosition, []) } + | Type { (fst $1, (:[]) (snd $1)) } + | Type ',' ListType { (fst $1, (:) (snd $1) (snd $3)) } + +TypeBinders :: { (Language.SOAS.Syntax.Abs.BNFC'Position, Language.SOAS.Syntax.Abs.TypeBinders) } +TypeBinders + : {- empty -} { (Language.SOAS.Syntax.Abs.BNFC'NoPosition, Language.SOAS.Syntax.Abs.NoTypeBinders Language.SOAS.Syntax.Abs.BNFC'NoPosition) } + | VarIdent TypeBinders { (fst $1, Language.SOAS.Syntax.Abs.SomeTypeBinders (fst $1) (snd $1) (snd $2)) } + +ScopedOpArgTyping :: { (Language.SOAS.Syntax.Abs.BNFC'Position, Language.SOAS.Syntax.Abs.ScopedOpArgTyping) } +ScopedOpArgTyping + : OpArgTyping { (fst $1, Language.SOAS.Syntax.Abs.ScopedOpArgTyping (fst $1) (snd $1)) } + +ListScopedOpArgTyping :: { (Language.SOAS.Syntax.Abs.BNFC'Position, [Language.SOAS.Syntax.Abs.ScopedOpArgTyping]) } +ListScopedOpArgTyping + : {- empty -} { (Language.SOAS.Syntax.Abs.BNFC'NoPosition, []) } + | ScopedOpArgTyping { (fst $1, (:[]) (snd $1)) } + | ScopedOpArgTyping ',' ListScopedOpArgTyping { (fst $1, (:) (snd $1) (snd $3)) } + +OpArgTyping :: { (Language.SOAS.Syntax.Abs.BNFC'Position, Language.SOAS.Syntax.Abs.OpArgTyping) } +OpArgTyping + : ListType '.' Type { (fst $1, Language.SOAS.Syntax.Abs.OpArgTyping (fst $1) (snd $1) (snd $3)) } + +ScopedType :: { (Language.SOAS.Syntax.Abs.BNFC'Position, Language.SOAS.Syntax.Abs.ScopedType) } +ScopedType + : Type { (fst $1, Language.SOAS.Syntax.Abs.ScopedType (fst $1) (snd $1)) } + +ListScopedType :: { (Language.SOAS.Syntax.Abs.BNFC'Position, [Language.SOAS.Syntax.Abs.ScopedType]) } +ListScopedType + : {- empty -} { (Language.SOAS.Syntax.Abs.BNFC'NoPosition, []) } + | ScopedType ListScopedType { (fst $1, (:) (snd $1) (snd $2)) } + +{ + +type Err = Either String + +happyError :: [Token] -> Err a +happyError ts = Left $ + "syntax error at " ++ tokenPos ts ++ + case ts of + [] -> [] + [Err _] -> " due to lexer error" + t:_ -> " before `" ++ (prToken t) ++ "'" + +myLexer :: String -> [Token] +myLexer = tokens + +-- Entrypoints + +pTermTyping :: [Token] -> Err Language.SOAS.Syntax.Abs.TermTyping +pTermTyping = fmap snd . pTermTyping_internal + +pContext :: [Token] -> Err Language.SOAS.Syntax.Abs.Context +pContext = fmap snd . pContext_internal + +pVarTyping :: [Token] -> Err Language.SOAS.Syntax.Abs.VarTyping +pVarTyping = fmap snd . pVarTyping_internal + +pListVarTyping :: [Token] -> Err [Language.SOAS.Syntax.Abs.VarTyping] +pListVarTyping = fmap snd . pListVarTyping_internal + +pMetaVarTyping :: [Token] -> Err Language.SOAS.Syntax.Abs.MetaVarTyping +pMetaVarTyping = fmap snd . pMetaVarTyping_internal + +pListMetaVarTyping :: [Token] -> Err [Language.SOAS.Syntax.Abs.MetaVarTyping] +pListMetaVarTyping = fmap snd . pListMetaVarTyping_internal + +pOpTyping :: [Token] -> Err Language.SOAS.Syntax.Abs.OpTyping +pOpTyping = fmap snd . pOpTyping_internal + +pConstraint :: [Token] -> Err Language.SOAS.Syntax.Abs.Constraint +pConstraint = fmap snd . pConstraint_internal + +pUnifier :: [Token] -> Err Language.SOAS.Syntax.Abs.Unifier +pUnifier = fmap snd . pUnifier_internal + +pSubst :: [Token] -> Err Language.SOAS.Syntax.Abs.Subst +pSubst = fmap snd . pSubst_internal + +pListSubst :: [Token] -> Err [Language.SOAS.Syntax.Abs.Subst] +pListSubst = fmap snd . pListSubst_internal + +pTerm :: [Token] -> Err Language.SOAS.Syntax.Abs.Term +pTerm = fmap snd . pTerm_internal + +pListTerm :: [Token] -> Err [Language.SOAS.Syntax.Abs.Term] +pListTerm = fmap snd . pListTerm_internal + +pOpArg :: [Token] -> Err Language.SOAS.Syntax.Abs.OpArg +pOpArg = fmap snd . pOpArg_internal + +pListOpArg :: [Token] -> Err [Language.SOAS.Syntax.Abs.OpArg] +pListOpArg = fmap snd . pListOpArg_internal + +pBinders :: [Token] -> Err Language.SOAS.Syntax.Abs.Binders +pBinders = fmap snd . pBinders_internal + +pScopedTerm :: [Token] -> Err Language.SOAS.Syntax.Abs.ScopedTerm +pScopedTerm = fmap snd . pScopedTerm_internal + +pType :: [Token] -> Err Language.SOAS.Syntax.Abs.Type +pType = fmap snd . pType_internal + +pType1 :: [Token] -> Err Language.SOAS.Syntax.Abs.Type +pType1 = fmap snd . pType1_internal + +pType2 :: [Token] -> Err Language.SOAS.Syntax.Abs.Type +pType2 = fmap snd . pType2_internal + +pListType :: [Token] -> Err [Language.SOAS.Syntax.Abs.Type] +pListType = fmap snd . pListType_internal + +pTypeBinders :: [Token] -> Err Language.SOAS.Syntax.Abs.TypeBinders +pTypeBinders = fmap snd . pTypeBinders_internal + +pScopedOpArgTyping :: [Token] -> Err Language.SOAS.Syntax.Abs.ScopedOpArgTyping +pScopedOpArgTyping = fmap snd . pScopedOpArgTyping_internal + +pListScopedOpArgTyping :: [Token] -> Err [Language.SOAS.Syntax.Abs.ScopedOpArgTyping] +pListScopedOpArgTyping = fmap snd . pListScopedOpArgTyping_internal + +pOpArgTyping :: [Token] -> Err Language.SOAS.Syntax.Abs.OpArgTyping +pOpArgTyping = fmap snd . pOpArgTyping_internal + +pScopedType :: [Token] -> Err Language.SOAS.Syntax.Abs.ScopedType +pScopedType = fmap snd . pScopedType_internal + +pListScopedType :: [Token] -> Err [Language.SOAS.Syntax.Abs.ScopedType] +pListScopedType = fmap snd . pListScopedType_internal +} + diff --git a/haskell/soas/src/Language/SOAS/Syntax/Print.hs b/haskell/soas/src/Language/SOAS/Syntax/Print.hs new file mode 100644 index 00000000..4b4ef010 --- /dev/null +++ b/haskell/soas/src/Language/SOAS/Syntax/Print.hs @@ -0,0 +1,258 @@ +-- File generated by the BNF Converter (bnfc 2.9.5). + +{-# LANGUAGE CPP #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE LambdaCase #-} +#if __GLASGOW_HASKELL__ <= 708 +{-# LANGUAGE OverlappingInstances #-} +#endif + +-- | Pretty-printer for Language. + +module Language.SOAS.Syntax.Print where + +import Prelude + ( ($), (.) + , Bool(..), (==), (<) + , Int, Integer, Double, (+), (-), (*) + , String, (++) + , ShowS, showChar, showString + , all, elem, foldr, id, map, null, replicate, shows, span + ) +import Data.Char ( Char, isSpace ) +import qualified Language.SOAS.Syntax.Abs + +-- | The top-level printing method. + +printTree :: Print a => a -> String +printTree = render . prt 0 + +type Doc = [ShowS] -> [ShowS] + +doc :: ShowS -> Doc +doc = (:) + +render :: Doc -> String +render d = rend 0 False (map ($ "") $ d []) "" + where + rend + :: Int -- ^ Indentation level. + -> Bool -- ^ Pending indentation to be output before next character? + -> [String] + -> ShowS + rend i p = \case + "[" :ts -> char '[' . rend i False ts + "(" :ts -> char '(' . rend i False ts + "{" :ts -> onNewLine i p . showChar '{' . new (i+1) ts + "}" : ";":ts -> onNewLine (i-1) p . showString "};" . new (i-1) ts + "}" :ts -> onNewLine (i-1) p . showChar '}' . new (i-1) ts + [";"] -> char ';' + ";" :ts -> char ';' . new i ts + t : ts@(s:_) | closingOrPunctuation s + -> pending . showString t . rend i False ts + t :ts -> pending . space t . rend i False ts + [] -> id + where + -- Output character after pending indentation. + char :: Char -> ShowS + char c = pending . showChar c + + -- Output pending indentation. + pending :: ShowS + pending = if p then indent i else id + + -- Indentation (spaces) for given indentation level. + indent :: Int -> ShowS + indent i = replicateS (2*i) (showChar ' ') + + -- Continue rendering in new line with new indentation. + new :: Int -> [String] -> ShowS + new j ts = showChar '\n' . rend j True ts + + -- Make sure we are on a fresh line. + onNewLine :: Int -> Bool -> ShowS + onNewLine i p = (if p then id else showChar '\n') . indent i + + -- Separate given string from following text by a space (if needed). + space :: String -> ShowS + space t s = + case (all isSpace t, null spc, null rest) of + (True , _ , True ) -> [] -- remove trailing space + (False, _ , True ) -> t -- remove trailing space + (False, True, False) -> t ++ ' ' : s -- add space if none + _ -> t ++ s + where + (spc, rest) = span isSpace s + + closingOrPunctuation :: String -> Bool + closingOrPunctuation [c] = c `elem` closerOrPunct + closingOrPunctuation _ = False + + closerOrPunct :: String + closerOrPunct = ")],;" + +parenth :: Doc -> Doc +parenth ss = doc (showChar '(') . ss . doc (showChar ')') + +concatS :: [ShowS] -> ShowS +concatS = foldr (.) id + +concatD :: [Doc] -> Doc +concatD = foldr (.) id + +replicateS :: Int -> ShowS -> ShowS +replicateS n f = concatS (replicate n f) + +-- | The printer class does the job. + +class Print a where + prt :: Int -> a -> Doc + +instance {-# OVERLAPPABLE #-} Print a => Print [a] where + prt i = concatD . map (prt i) + +instance Print Char where + prt _ c = doc (showChar '\'' . mkEsc '\'' c . showChar '\'') + +instance Print String where + prt _ = printString + +printString :: String -> Doc +printString s = doc (showChar '"' . concatS (map (mkEsc '"') s) . showChar '"') + +mkEsc :: Char -> Char -> ShowS +mkEsc q = \case + s | s == q -> showChar '\\' . showChar s + '\\' -> showString "\\\\" + '\n' -> showString "\\n" + '\t' -> showString "\\t" + s -> showChar s + +prPrec :: Int -> Int -> Doc -> Doc +prPrec i j = if j < i then parenth else id + +instance Print Integer where + prt _ x = doc (shows x) + +instance Print Double where + prt _ x = doc (shows x) + +instance Print Language.SOAS.Syntax.Abs.VarIdent where + prt _ (Language.SOAS.Syntax.Abs.VarIdent i) = doc $ showString i +instance Print Language.SOAS.Syntax.Abs.OpIdent where + prt _ (Language.SOAS.Syntax.Abs.OpIdent i) = doc $ showString i +instance Print Language.SOAS.Syntax.Abs.MetaVarIdent where + prt _ (Language.SOAS.Syntax.Abs.MetaVarIdent i) = doc $ showString i +instance Print (Language.SOAS.Syntax.Abs.TermTyping' a) where + prt i = \case + Language.SOAS.Syntax.Abs.TermTyping _ typebinders context scopedterm scopedtype -> prPrec i 0 (concatD [doc (showString "\8704"), prt 0 typebinders, doc (showString "."), prt 0 context, doc (showString "\8866"), prt 0 scopedterm, doc (showString ":"), prt 0 scopedtype]) + +instance Print (Language.SOAS.Syntax.Abs.Context' a) where + prt i = \case + Language.SOAS.Syntax.Abs.Context _ metavartypings vartypings -> prPrec i 0 (concatD [prt 0 metavartypings, doc (showString "|"), prt 0 vartypings]) + +instance Print (Language.SOAS.Syntax.Abs.VarTyping' a) where + prt i = \case + Language.SOAS.Syntax.Abs.VarTyping _ varident type_ -> prPrec i 0 (concatD [prt 0 varident, doc (showString ":"), prt 0 type_]) + +instance Print [Language.SOAS.Syntax.Abs.VarTyping' a] where + prt _ [] = concatD [] + prt _ [x] = concatD [prt 0 x] + prt _ (x:xs) = concatD [prt 0 x, doc (showString ","), prt 0 xs] + +instance Print (Language.SOAS.Syntax.Abs.MetaVarTyping' a) where + prt i = \case + Language.SOAS.Syntax.Abs.MetaVarTyping _ metavarident types type_ -> prPrec i 0 (concatD [prt 0 metavarident, doc (showString ":"), doc (showString "["), prt 0 types, doc (showString "]"), prt 0 type_]) + +instance Print [Language.SOAS.Syntax.Abs.MetaVarTyping' a] where + prt _ [] = concatD [] + prt _ [x] = concatD [prt 0 x] + prt _ (x:xs) = concatD [prt 0 x, doc (showString ","), prt 0 xs] + +instance Print (Language.SOAS.Syntax.Abs.OpTyping' a) where + prt i = \case + Language.SOAS.Syntax.Abs.OpTyping _ opident typebinders scopedopargtypings scopedtype -> prPrec i 0 (concatD [prt 0 opident, doc (showString ":"), doc (showString "\8704"), prt 0 typebinders, doc (showString "."), doc (showString "("), prt 0 scopedopargtypings, doc (showString ")"), doc (showString "\8594"), prt 0 scopedtype]) + +instance Print (Language.SOAS.Syntax.Abs.Constraint' a) where + prt i = \case + Language.SOAS.Syntax.Abs.ConstraintEq _ binders scopedterm1 scopedterm2 -> prPrec i 0 (concatD [doc (showString "\8704"), prt 0 binders, doc (showString "."), prt 0 scopedterm1, doc (showString "="), prt 0 scopedterm2]) + +instance Print (Language.SOAS.Syntax.Abs.Unifier' a) where + prt i = \case + Language.SOAS.Syntax.Abs.Unifier _ substs -> prPrec i 0 (concatD [doc (showString "["), prt 0 substs, doc (showString "]")]) + +instance Print (Language.SOAS.Syntax.Abs.Subst' a) where + prt i = \case + Language.SOAS.Syntax.Abs.Subst _ metavarident binders scopedterm -> prPrec i 0 (concatD [prt 0 metavarident, doc (showString "["), prt 0 binders, doc (showString "]"), doc (showString "\8614"), prt 0 scopedterm]) + +instance Print [Language.SOAS.Syntax.Abs.Subst' a] where + prt _ [] = concatD [] + prt _ [x] = concatD [prt 0 x] + prt _ (x:xs) = concatD [prt 0 x, doc (showString ","), prt 0 xs] + +instance Print (Language.SOAS.Syntax.Abs.Term' a) where + prt i = \case + Language.SOAS.Syntax.Abs.Var _ varident -> prPrec i 0 (concatD [prt 0 varident]) + Language.SOAS.Syntax.Abs.Op _ opident opargs -> prPrec i 0 (concatD [prt 0 opident, doc (showString "("), prt 0 opargs, doc (showString ")")]) + Language.SOAS.Syntax.Abs.MetaVar _ metavarident terms -> prPrec i 0 (concatD [prt 0 metavarident, doc (showString "["), prt 0 terms, doc (showString "]")]) + +instance Print [Language.SOAS.Syntax.Abs.Term' a] where + prt _ [] = concatD [] + prt _ [x] = concatD [prt 0 x] + prt _ (x:xs) = concatD [prt 0 x, doc (showString ","), prt 0 xs] + +instance Print (Language.SOAS.Syntax.Abs.OpArg' a) where + prt i = \case + Language.SOAS.Syntax.Abs.OpArg _ binders scopedterm -> prPrec i 0 (concatD [prt 0 binders, doc (showString "."), prt 0 scopedterm]) + Language.SOAS.Syntax.Abs.PlainOpArg _ term -> prPrec i 0 (concatD [prt 0 term]) + +instance Print [Language.SOAS.Syntax.Abs.OpArg' a] where + prt _ [] = concatD [] + prt _ [x] = concatD [prt 0 x] + prt _ (x:xs) = concatD [prt 0 x, doc (showString ","), prt 0 xs] + +instance Print (Language.SOAS.Syntax.Abs.Binders' a) where + prt i = \case + Language.SOAS.Syntax.Abs.NoBinders _ -> prPrec i 0 (concatD []) + Language.SOAS.Syntax.Abs.SomeBinders _ varident binders -> prPrec i 0 (concatD [prt 0 varident, prt 0 binders]) + +instance Print (Language.SOAS.Syntax.Abs.ScopedTerm' a) where + prt i = \case + Language.SOAS.Syntax.Abs.ScopedTerm _ term -> prPrec i 0 (concatD [prt 0 term]) + +instance Print (Language.SOAS.Syntax.Abs.Type' a) where + prt i = \case + Language.SOAS.Syntax.Abs.TypeFun _ type_1 type_2 -> prPrec i 0 (concatD [prt 1 type_1, doc (showString "\8594"), prt 1 type_2]) + Language.SOAS.Syntax.Abs.TypeProduct _ type_1 type_2 -> prPrec i 1 (concatD [prt 1 type_1, doc (showString "\215"), prt 2 type_2]) + Language.SOAS.Syntax.Abs.TypeVar _ varident -> prPrec i 2 (concatD [prt 0 varident]) + +instance Print [Language.SOAS.Syntax.Abs.Type' a] where + prt _ [] = concatD [] + prt _ [x] = concatD [prt 0 x] + prt _ (x:xs) = concatD [prt 0 x, doc (showString ","), prt 0 xs] + +instance Print (Language.SOAS.Syntax.Abs.TypeBinders' a) where + prt i = \case + Language.SOAS.Syntax.Abs.NoTypeBinders _ -> prPrec i 0 (concatD []) + Language.SOAS.Syntax.Abs.SomeTypeBinders _ varident typebinders -> prPrec i 0 (concatD [prt 0 varident, prt 0 typebinders]) + +instance Print (Language.SOAS.Syntax.Abs.ScopedOpArgTyping' a) where + prt i = \case + Language.SOAS.Syntax.Abs.ScopedOpArgTyping _ opargtyping -> prPrec i 0 (concatD [prt 0 opargtyping]) + +instance Print [Language.SOAS.Syntax.Abs.ScopedOpArgTyping' a] where + prt _ [] = concatD [] + prt _ [x] = concatD [prt 0 x] + prt _ (x:xs) = concatD [prt 0 x, doc (showString ","), prt 0 xs] + +instance Print (Language.SOAS.Syntax.Abs.OpArgTyping' a) where + prt i = \case + Language.SOAS.Syntax.Abs.OpArgTyping _ types type_ -> prPrec i 0 (concatD [prt 0 types, doc (showString "."), prt 0 type_]) + +instance Print (Language.SOAS.Syntax.Abs.ScopedType' a) where + prt i = \case + Language.SOAS.Syntax.Abs.ScopedType _ type_ -> prPrec i 0 (concatD [prt 0 type_]) + +instance Print [Language.SOAS.Syntax.Abs.ScopedType' a] where + prt _ [] = concatD [] + prt _ (x:xs) = concatD [prt 0 x, prt 0 xs] diff --git a/haskell/soas/test/Spec.hs b/haskell/soas/test/Spec.hs new file mode 100644 index 00000000..a824f8c3 --- /dev/null +++ b/haskell/soas/test/Spec.hs @@ -0,0 +1 @@ +{-# OPTIONS_GHC -F -pgmF hspec-discover #-} diff --git a/haskell/soas/test/doctests/Main.hs b/haskell/soas/test/doctests/Main.hs new file mode 100644 index 00000000..28c562a8 --- /dev/null +++ b/haskell/soas/test/doctests/Main.hs @@ -0,0 +1,7 @@ +module Main where + +import System.Environment (getArgs) +import Test.DocTest (mainFromCabal) + +main :: IO () +main = mainFromCabal "soas" =<< getArgs diff --git a/stack.yaml b/stack.yaml index 237256c5..6a785a5b 100644 --- a/stack.yaml +++ b/stack.yaml @@ -2,6 +2,7 @@ resolver: nightly-2024-08-17 packages: - haskell/free-foil - haskell/lambda-pi + - haskell/soas # kind-generics-th is not on Stackage :( extra-deps: - kind-generics-th-0.2.3.3@sha256:fc5f3aee46725e048a0159d73612a5d86c30017cd24ebab764347b65cffbd1d4,1519