From fa7e334938b9085687646b7335da615738041952 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Sun, 27 Oct 2024 10:59:35 +0300 Subject: [PATCH] Document MkFreeFoil and Language.SOAS.Impl --- .../Control/Monad/Free/Foil/TH/MkFreeFoil.hs | 100 +++++++++++++++--- .../soas/src/Language/SOAS/FreeFoilConfig.hs | 1 - haskell/soas/src/Language/SOAS/Impl.hs | 13 +++ 3 files changed, 100 insertions(+), 14 deletions(-) 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 index 6d178e56..4ce823e7 100644 --- a/haskell/free-foil/src/Control/Monad/Free/Foil/TH/MkFreeFoil.hs +++ b/haskell/free-foil/src/Control/Monad/Free/Foil/TH/MkFreeFoil.hs @@ -4,7 +4,13 @@ {-# LANGUAGE ViewPatterns #-} {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} {-# HLINT ignore "Use ++" #-} -module Control.Monad.Free.Foil.TH.MkFreeFoil where +-- | 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) @@ -20,30 +26,85 @@ 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 - } - -data FreeFoilConfig = FreeFoilConfig - { rawQuantifiedNames :: [Name] - , freeFoilTermConfigs :: [FreeFoilTermConfig] - , freeFoilNameModifier :: String -> String - , freeFoilScopeNameModifier :: String -> String - , signatureNameModifier :: String -> String - , freeFoilConNameModifier :: String -> String - , freeFoilConvertToName :: String -> String - , freeFoilConvertFromName :: String -> String - , ignoreNames :: [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 @@ -535,6 +596,13 @@ toFreeFoilClauseFromQuantified config rawRetType = go 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 @@ -629,6 +697,12 @@ reifyDataOrNewtype name = reify name >>= \case 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 diff --git a/haskell/soas/src/Language/SOAS/FreeFoilConfig.hs b/haskell/soas/src/Language/SOAS/FreeFoilConfig.hs index 55320e13..3a53e937 100644 --- a/haskell/soas/src/Language/SOAS/FreeFoilConfig.hs +++ b/haskell/soas/src/Language/SOAS/FreeFoilConfig.hs @@ -68,5 +68,4 @@ soasConfig = FreeFoilConfig , freeFoilConvertFromName = ("from" ++ ) , freeFoilConvertToName = ("to" ++ ) , signatureNameModifier = (++ "Sig") - , ignoreNames = [] } diff --git a/haskell/soas/src/Language/SOAS/Impl.hs b/haskell/soas/src/Language/SOAS/Impl.hs index 03c9e711..a0d30a61 100644 --- a/haskell/soas/src/Language/SOAS/Impl.hs +++ b/haskell/soas/src/Language/SOAS/Impl.hs @@ -13,6 +13,8 @@ {-# 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) @@ -33,13 +35,22 @@ import System.Exit (exitFailure) -- >>> 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)"] @@ -65,6 +76,8 @@ applySubsts scope substs term = 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