From 46ff16eb8ccdc50fea0ae758aeacd998d6920a7a Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Thu, 9 Jan 2025 18:19:46 +0300 Subject: [PATCH] Add some documentation to Data.SOAS --- src/Data/SOAS.hs | 107 ++++++++++++++++++++++++++++++----------------- 1 file changed, 68 insertions(+), 39 deletions(-) diff --git a/src/Data/SOAS.hs b/src/Data/SOAS.hs index 3698cd8..dafaebb 100644 --- a/src/Data/SOAS.hs +++ b/src/Data/SOAS.hs @@ -31,47 +31,53 @@ import Generics.Kind.TH (deriveGenericK) import qualified Language.Lambda.Syntax.Abs as Raw import Unsafe.Coerce (unsafeCoerce) -data MetaAppSig metavar scope term = MetaAppSig metavar [term] +-- | Second-order signature for metavariable applications. +-- This way, metavariables can be added to any other signature using 'Sum'. +data MetaAppSig metavar scope term + = MetaAppSig metavar [term] -- ^ A metavariable is always fully applied to a list of arguments. deriving (Functor, Foldable, Traversable, GHC.Generic) - deriveBifunctor ''MetaAppSig deriveBifoldable ''MetaAppSig deriveBitraversable ''MetaAppSig - deriveGenericK ''MetaAppSig - instance (ZipMatchK a) => ZipMatchK (MetaAppSig a) --- >>> a = "λy.(λx.λy.X[x, y X[y, x]])y" :: MetaTerm Raw.MetaVarIdent Foil.VoidS --- >>> b = "λz.(λx.λy.X[x, y X[y, x]])z" :: MetaTerm Raw.MetaVarIdent Foil.VoidS --- >>> alphaEquiv Foil.emptyScope a b --- True - +-- | A second-order abstract syntax (SOAS) is generated from a signature +-- by adding parametrised metavariables. +-- +-- Note that here we also parametrise SOAS by the type of binders (patterns) @binder@. type SOAS binder metavar sig n = AST binder (Sum sig (MetaAppSig metavar)) n +-- | A scoped version of 'SOAS'. +-- 'ScopedSOAS' is to 'SOAS' what 'ScopedAST' is to 'AST'. type ScopedSOAS binder metavar sig n = ScopedAST binder (Sum sig (MetaAppSig metavar)) n +-- | A convenient pattern synonym for parametrised metavariables. pattern MetaApp :: metavar -> [SOAS binder metavar sig n] -> SOAS binder metavar sig n pattern MetaApp metavar args = Node (R2 (MetaAppSig metavar args)) +-- | A body of a metavariable substitution for one metavariable. data MetaAbs binder sig t where MetaAbs - :: Foil.NameBinderList Foil.VoidS n - -> Foil.NameMap n t - -> AST binder sig n + :: Foil.NameBinderList Foil.VoidS n -- ^ A list of binders corresponding to metavariable arguments. + -> Foil.NameMap n t -- ^ Types of parameters. + -> AST binder sig n -- ^ Term to substitute the metavariable with. -> MetaAbs binder sig t +-- | A metavariable substitution is a pair of a metavariable name and its body. newtype MetaSubst binder sig metavar ext t = MetaSubst { getMetaSubst :: (metavar, MetaAbs binder (Sum sig ext) t) } +-- | A collection of metavariable substitutions (for simultaneous substitution of multiple metavariables). newtype MetaSubsts binder sig metavar ext t = MetaSubsts { getMetaSubsts :: [MetaSubst binder sig metavar ext t] } +-- | Apply metavariable substitutions to a SOAS term. applyMetaSubsts :: ( Bifunctor sig , Eq metavar @@ -80,10 +86,10 @@ applyMetaSubsts , Foil.CoSinkable binder , Foil.SinkableK binder ) - => (metavar -> metavar') - -> Foil.Scope n - -> MetaSubsts binder sig metavar (MetaAppSig metavar') t - -> SOAS binder metavar sig n + => (metavar -> metavar') -- ^ Renaming of metavariables (normally, 'id' or some kind of injection). + -> Foil.Scope n -- ^ Scope of terms. + -> MetaSubsts binder sig metavar (MetaAppSig metavar') t -- ^ Metavariable substitutions. + -> SOAS binder metavar sig n -- ^ The original SOAS term. -> SOAS binder metavar' sig n applyMetaSubsts rename scope substs = \case Var x -> Var x @@ -129,9 +135,8 @@ applyMetaSubsts rename scope substs = \case where newScope = Foil.extendScopePattern binder scope' --- M[x, y] M[y, x] = x y --- M[x, y] M[x, y] = x y - +-- | Combine (compose) metavariable substitutions. +-- -- TODO: refactor combineMetaSubsts :: ( Eq metavar @@ -168,14 +173,21 @@ combineMetaSubsts = foldr go [] , m == m' ] --- | This function takes the following parameters: +-- | Match left-hand side (with metavariables) against the rigid right-hand side. +-- +-- If matching is successful, it produces metavariable substitutions that when applied to LHS make it syntactically equal to RHS. +-- For example, matching +-- M[f x, g]) = g (f x) +-- produces substitution +-- M[z₁, z₂] ↦ z₂ z₁ -- --- * `Scope n` - The current scope. --- * `SOAS binder metavar sig n` - The left-hand side (where we want to apply --- substitutions). --- * `AST binder sig' n` - The right-hand side (unchangeable). --- * `[MetaSubsts sig' metavar]` - The substitutions that turn the LHS into --- the RHS. +-- There may be more than one solution for matching, e.g. +-- M[f x, f x] = f x +-- can be solved with two different substitutions: +-- 1. M[z₁, z₂] ↦ z₁ +-- 2. M[z₁, z₂] ↦ z₂ +-- +-- Hence, this function produces a list of possible substitutions. match :: ( Bitraversable sig , ZipMatchK sig @@ -186,9 +198,9 @@ match , Bitraversable ext , ZipMatchK (Sum sig ext) ) - => Foil.Scope n - -> SOAS binder metavar sig n - -> AST binder (Sum sig ext) n + => Foil.Scope n -- ^ The current scope. + -> SOAS binder metavar sig n -- ^ The left-hand side (with metavariables that we solve for). + -> AST binder (Sum sig ext) n -- ^ The right hand side (rigid). -> [MetaSubsts binder sig metavar ext t] match scope lhs rhs = case (lhs, rhs) of @@ -233,6 +245,7 @@ match scope lhs rhs = (Var _, _) -> [] _ -> [] +-- | Same as 'match' but for scoped terms. matchScoped :: ( Bitraversable sig , ZipMatchK sig @@ -277,11 +290,18 @@ matchScoped scope (ScopedAST binder lhs) (ScopedAST binder' rhs) = in match scope' lhs' rhs' Foil.NotUnifiable -> trace "not unifiable" [] -closed :: AST binder sig n -> Maybe (AST binder sig Foil.VoidS) -closed term = Just (unsafeCoerce term) - --- M[x, x] = x + x --- ∀ x. M[λy:t. x, λa:t. λa:t. a] = λy:t. x +-- | A special case of 'match', when LHS is a parametrised metavariable. +-- +-- Note that here we do not have an explicit name for that metavariable, +-- and only consider its arguments. +-- This is helpful when recursively matching with fresh metavariables, +-- since we do not need to generate any actual fresh names for such metavariables, +-- saving in complexity and performance. +-- +-- For each possible solution, this function produces a pair of +-- +-- 1. Body of the metavariable substitution. +-- 2. Metavariable substitutions for the metavariables that occur in the parameters of the root metavariable on the LHS. matchMetavar :: forall metavar n m binder sig ext t . ( Eq metavar @@ -294,11 +314,11 @@ matchMetavar , ZipMatchK sig , ZipMatchK (Sum sig ext) ) - => Foil.Scope m - -> Foil.NameBinderList Foil.VoidS m - -> Foil.Scope n - -> [SOAS binder metavar sig n] - -> AST binder (Sum sig ext) n + => Foil.Scope m -- ^ Scope for the body of the metavariable substitution (at root of LHS). + -> Foil.NameBinderList Foil.VoidS m -- ^ List of binders for the metavariable parameters (size of the list should match the actual list of parameters). + -> Foil.Scope n -- ^ Current scope. + -> [SOAS binder metavar sig n] -- ^ A list of arguments of the parametrised metavariable on the left-hand side. + -> AST binder (Sum sig ext) n -- ^ The right-hand side term (rigid). -> [(AST binder (Sum sig ext) m, MetaSubsts binder sig metavar ext t)] matchMetavar metavarScope metavarNameBinders scope args rhs = let @@ -340,6 +360,7 @@ matchMetavar metavarScope metavarNameBinders scope args rhs = in map (term,) substs ++ project xs args' project _ _ = error "mismatched name list and argument list" +-- | Same as 'matchMetavar' but for scoped term. matchMetavarScoped :: forall n m metavar binder sig ext t . ( Foil.Distinct n @@ -374,6 +395,8 @@ matchMetavarScoped metavarScope metavarNameBinders scope args (ScopedAST binder result = matchMetavar metavarScope' metavarNameBinders' scope' args' rhs in map (first (ScopedAST metavarBinder)) result +-- | Generate fresh name binders for a list of things. +-- This is useful to generate proper name binders of metavariable parameters. withFreshNameBinderList :: (Foil.Distinct n) => [a] @@ -393,10 +416,16 @@ withFreshNameBinderList (_ : xs) scope binders cont = binders' = push binder binders in withFreshNameBinderList xs scope' binders' cont +-- | /O(n)/. Push a name binder into the end of a name binder list. +-- +-- /Should be in "Control.Monad.Foil"./ push :: Foil.NameBinder i l -> Foil.NameBinderList n i -> Foil.NameBinderList n l push x Foil.NameBinderListEmpty = Foil.NameBinderListCons x Foil.NameBinderListEmpty push x (Foil.NameBinderListCons y ys) = Foil.NameBinderListCons y (push x ys) +-- | /O(n)/. Concatenate name binder lists. +-- +-- Should be in "Control.Monad.Foil". concatNameBinderLists :: Foil.NameBinderList i l -> Foil.NameBinderList n i -> Foil.NameBinderList n l concatNameBinderLists lst Foil.NameBinderListEmpty = lst concatNameBinderLists lst (Foil.NameBinderListCons x xs) =