Safe Haskell	None
Language	Haskell2010

Language.SOAS.Impl

Contents

Standard Types
Metavariable substitutions
Entrypoint

Description

Functions over Second-Order Abstract Syntax (SOAS) represented using scope-safe Haskell types (via Free Foil).

Synopsis

type Term = Term' BNFC'Position
type Type = Type' BNFC'Position
type Subst = Subst' BNFC'Position 'VoidS
type Constraint = Constraint' BNFC'Position 'VoidS
type OpTyping = OpTyping' BNFC'Position 'VoidS
lookupSubst :: MetaVarIdent -> [Subst] -> Maybe Subst
applySubsts :: forall (n :: S). Distinct n => Scope n -> [Subst] -> Term n -> Term n
isSolutionFor :: [Subst] -> [Constraint] -> Bool
defaultMain :: IO ()

Documentation

>>> :set -XOverloadedStrings
>>> :set -XDataKinds
>>> import qualified Control.Monad.Foil as Foil
>>> import Control.Monad.Free.Foil
>>> import Data.String (fromString)

Standard Types

type Term = Term' BNFC'Position Source #

Standard terms with source code location annotations.

type Type = Type' BNFC'Position Source #

Standard types with source code location annotations.

type Subst = Subst' BNFC'Position 'VoidS Source #

Standard metavariable substitutions with source code location annotations.

type Constraint = Constraint' BNFC'Position 'VoidS Source #

Standard unification constraints with source code location annotations.

type OpTyping = OpTyping' BNFC'Position 'VoidS Source #

Standard operator typings with source code location annotations.

Metavariable substitutions

lookupSubst :: MetaVarIdent -> [Subst] -> Maybe Subst Source #

Lookup a substitution by its MetaVarIdent.

>>> lookupSubst "?m" ["?n[] ↦ Zero()", "?m[x y] ↦ App(y, x)"]
Just ?m [x0 x1] ↦ App (x1, x0)

applySubsts :: forall (n :: S). Distinct n => Scope n -> [Subst] -> Term n -> Term n Source #

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, Lam (x2 . App (x2, App (x0, x0)))), x0))))

>>> applySubsts Foil.emptyScope ["?m[x y] ↦ App(y, x)"] "Lam(f. Lam(x. ?m[?m[x, f], f]))"
Lam (x0 . Lam (x1 . App (x0, App (x0, x1))))

isSolutionFor :: [Subst] -> [Constraint] -> Bool Source #

Check if a (simultaneous) substitution is a solution to a set of constraints:

>>> isSolutionFor ["?m[x y] ↦ App(y, x)"] ["∀ f x. ?m[?m[x, f], f] = App(f, App(f, x))"]
True
>>> isSolutionFor ["?m[x y] ↦ App(y, x)"] ["∀ f x y. ?m[?m[x, f], f] = App(f, App(f, y))"]
False

>>> isSolutionFor ["?m[x] ↦ Lam(f. App(f, x))"] ["∀ x. ?m[?m[x]] = Lam(f. App(f, Lam(f. App(f, x))))"]
True
>>> isSolutionFor ["?m[x] ↦ Lam(f. App(f, x))"] ["∀ y x. ?m[?m[x]] = Lam(f. App(f, Lam(f. App(f, y))))"]
False

Entrypoint

defaultMain :: IO () Source #

A SOAS interpreter implemented via the free foil.