pi-forall-0.1.1: src/Syntax.hs
{- PiForall language, OPLSS -}
{-# LANGUAGE TemplateHaskell,
FlexibleInstances,
MultiParamTypeClasses,
FlexibleContexts,
UndecidableInstances,
ViewPatterns,
EmptyDataDecls,
DeriveGeneric,
DeriveDataTypeable,
CPP #-}
{-# OPTIONS_GHC -Wall -fno-warn-unused-matches -fno-warn-orphans #-}
-- | The abstract syntax of the simple dependently typed language
-- See comment at the top of 'Parser' for the concrete syntax
module Syntax where
#ifdef MIN_VERSION_GLASGOW_HASKELL
#if MIN_VERSION_GLASGOW_HASKELL(7,10,3,0)
-- ghc >= 7.10.3
#else
-- older ghc versions, but MIN_VERSION_GLASGOW_HASKELL defined
#endif
#else
-- MIN_VERSION_GLASGOW_HASKELL not even defined yet (ghc <= 7.8.x)
-- both needed only on even earlier ghc's
-- import Control.Applicative (pure)
-- import Data.Monoid (mempty)
#endif
import GHC.Generics (Generic)
import Data.Typeable (Typeable)
import Unbound.Generics.LocallyNameless
import Unbound.Generics.LocallyNameless.Unsafe (unsafeUnbind)
import Unbound.Generics.LocallyNameless.TH (makeClosedAlpha)
import Text.ParserCombinators.Parsec.Pos
import Data.Set (Set)
import qualified Data.Set as S
import Data.Maybe (fromMaybe)
-----------------------------------------
-- * Variable names
-----------------------------------------
-- | term names, use unbound library to
-- automatically generate fv, subst, alpha-eq
type TName = Name Term
-- | module names
type MName = String
-- | type constructor names
type TCName = String
-- | data constructor names
type DCName = String
-----------------------------------------
-- * Core language
-----------------------------------------
-- Type abbreviation for documentation
type Type = Term
data Term =
-- basic language
Type -- ^ type of types
| Var TName -- ^ variables
| Lam (Bind (TName, Embed Annot) Term)
-- ^ abstraction
| App Term Term -- ^ application
| Pi (Bind (TName, Embed Term) Term) -- ^ function type
-- practical matters for surface language
| Ann Term Term -- ^ Annotated terms `( x : A )`
| Paren Term -- ^ parenthesized term, useful for printing
| Pos SourcePos Term -- ^ marked source position, for error messages
-- conveniences
| TrustMe Annot -- ^ an axiom 'TRUSTME', inhabits all types
-- unit
| TyUnit -- ^ The type with a single inhabitant `One`
| LitUnit -- ^ The inhabitant, written `tt`
-- homework: boolean expressions
| TyBool -- ^ The type with two inhabitants
| LitBool Bool -- ^ True and False
| If Term Term Term Annot -- ^ If expression for eliminating booleans
-- homework sigma types
| Sigma (Bind (TName, Embed Term) Term)
-- ^ sigma type `{ x : A | B }`
| Prod Term Term Annot
-- ^ introduction for sigmas `( a , b )`
| Pcase Term (Bind (TName, TName) Term) Annot
-- ^ elimination form `pcase p of (x,y) -> p`
-- homework let expression
| Let (Bind (TName, Embed Term) Term)
-- ^ let expression, introduces a new (potentially recursive)
-- definition in the ctx
-- propositional equality
| TyEq Term Term -- ^ Equality type `a = b`
| Refl Annot -- ^ Proof of equality
| Subst Term Term Annot
-- ^ equality elimination
| Contra Term Annot -- ^ witness to an equality contradiction
-- erasure
| ErasedLam (Bind (TName, Embed Annot) Term) -- ^ abstraction
| ErasedPi (Bind (TName, Embed Term) Term) -- ^ function type
| ErasedApp Term Term -- ^ application
-- datatypes
| TCon String [Term] -- ^ type constructors (fully applied)
| DCon String [Arg] Annot -- ^ term constructors
--- (fully applied, erased arguments first)
| Case Term [Match] Annot -- ^ case analysis
deriving (Show, Generic, Typeable)
-- | An 'Annot' is optional type information
newtype Annot = Annot (Maybe Term) deriving (Show, Generic, Typeable)
-- | A 'Match' represents a case alternative
data Match = Match (Bind Pattern Term) deriving (Show, Generic, Typeable)
-- | The patterns of case expressions bind all variables
-- in their respective branches.
data Pattern = PatCon DCName [(Pattern, Epsilon)]
| PatVar TName deriving (Show, Eq, Generic, Typeable)
-----------------------------------------
-- * Modules and declarations
-----------------------------------------
-- | A Module has a name, a list of imports, a list of declarations,
-- and a set of constructor names (which affect parsing).
data Module = Module { moduleName :: MName,
moduleImports :: [ModuleImport],
moduleEntries :: [Decl]
, moduleConstructors :: ConstructorNames
}
deriving (Show, Generic, Typeable)
newtype ModuleImport = ModuleImport MName
deriving (Show,Eq, Generic, Typeable)
data ConstructorNames = ConstructorNames {
tconNames :: Set String,
dconNames :: Set String
}
deriving (Show, Eq, Generic, Typeable)
-- | Declarations are the components of modules
data Decl = Sig TName Term
-- ^ Declaration for the type of a term
| Def TName Term
-- ^ The definition of a particular name, must
-- already have a type declaration in scope
| RecDef TName Term
-- ^ A potentially (recursive) definition of
-- a particular name, must be declared
| Data TCName Telescope [ConstructorDef]
-- ^ Declaration for a datatype including all of
-- its data constructors
| DataSig TCName Telescope
-- ^ An abstract view of a datatype. Does
-- not include any information about its data
-- constructors
deriving (Show, Generic, Typeable)
-- | A Data constructor has a name and a telescope of arguments
data ConstructorDef = ConstructorDef SourcePos DCName Telescope
deriving (Show, Generic, Typeable)
-------------
-- * Telescopes
-------------
-- | A telescope is like a first class context. It binds each name
-- in the rest of the telescope. For example
-- Delta = x:* , y:x, y = w, empty
data Telescope = Empty
| Cons Epsilon TName Term Telescope
| Constraint Term Term Telescope
deriving (Show, Generic, Typeable)
-- | Epsilon annotates the sort of a data constructor argument
data Epsilon =
Runtime
| Erased
deriving (Eq,Show,Read,Bounded,Ord,Generic,Typeable)
-- | An argument is tagged with whether it should be erased
data Arg = Arg Epsilon Term deriving (Show, Generic, Typeable)
-------------
-- * Auxiliary functions on syntax
-------------
-- | empty set of constructor names
emptyConstructorNames :: ConstructorNames
emptyConstructorNames = ConstructorNames S.empty S.empty
-- | Extract the term from an Arg
unArg :: Arg -> Term
unArg (Arg _ t) = t
-- | Default name for '_' occurring in patterns
wildcardName :: TName
wildcardName = string2Name "_"
-- | empty Annotation
noAnn :: Annot
noAnn = Annot Nothing
-- | Partial inverse of Pos
unPos :: Term -> Maybe SourcePos
unPos (Pos p _) = Just p
unPos _ = Nothing
-- | Tries to find a Pos anywhere inside a term
unPosDeep :: Term -> Maybe SourcePos
unPosDeep = unPos -- something (mkQ Nothing unPos) -- TODO: Generic version of this
-- | Tries to find a Pos inside a term, otherwise just gives up.
unPosFlaky :: Term -> SourcePos
unPosFlaky t = fromMaybe (newPos "unknown location" 0 0) (unPosDeep t)
-- | Is this the syntax of a literal (natural) number
isNumeral :: Term -> Maybe Int
isNumeral (Pos _ t) = isNumeral t
isNumeral (Paren t) = isNumeral t
isNumeral (DCon c [] _) | c== "Zero" = Just 0
isNumeral (DCon c [Arg _ t] _) | c== "Succ" =
do n <- isNumeral t ; return (n+1)
isNumeral _ = Nothing
-- | Is this pattern a variable
isPatVar :: Pattern -> Bool
isPatVar (PatVar _) = True
isPatVar _ = False
---------------------
-- * Erasure
---------------------
class Erase a where
-- | erase all computationally irrelevant parts of an expression
-- these include all typing annotations
-- irrelevant arguments are replaced by unit
erase :: a -> a
instance Erase Term where
erase (Var x) = Var x
erase (Lam bnd) = Lam (bind (x, embed noAnn) (erase body))
where ((x,unembed -> _), body) = unsafeUnbind bnd
erase (App a1 a2) = App (erase a1) (erase a2)
erase (Type) = Type
erase (Pi bnd) = Pi (bind (x, embed (erase tyA)) (erase tyB))
where ((x,unembed -> tyA), tyB) = unsafeUnbind bnd
erase (Ann t1 t2) = erase t1
erase (Paren t1) = erase t1
erase (Pos sp t) = erase t
erase (TrustMe _) = TrustMe noAnn
erase (TyUnit) = TyUnit
erase (LitUnit) = LitUnit
erase (TyBool) = TyBool
erase (LitBool b) = LitBool b
erase (If a b c _) = If (erase a) (erase b) (erase c) noAnn
erase (Let bnd) = Let (bind (x,embed (erase rhs)) (erase body))
where ((x,unembed -> rhs),body) = unsafeUnbind bnd
erase (TyEq a b) = TyEq (erase a) (erase b)
erase (Refl _) = Refl noAnn
erase (Subst tm pf _) = Subst (erase tm) (erase pf) noAnn
erase (Contra tm _) = Contra (erase tm) noAnn
erase (ErasedLam bnd) = ErasedLam (bind (x, embed noAnn) (erase body))
where ((x,unembed -> _), body) = unsafeUnbind bnd
erase (ErasedApp tm1 tm2) = ErasedApp (erase tm1) LitUnit
erase (ErasedPi bnd) = ErasedPi (bind (x, embed (erase tyA)) (erase tyB))
where ((x,unembed -> tyA), tyB) = unsafeUnbind bnd
erase (TCon n tms) = TCon n (map erase tms)
erase (DCon n args _) = DCon n (map erase args) noAnn
erase (Case tm ms _) = Case (erase tm) (map erase ms) noAnn
erase (Sigma bnd) = Sigma (bind (x, embed (erase tyA)) (erase tyB))
where ((x,unembed->tyA),tyB) = unsafeUnbind bnd
erase (Prod a b _) = Prod (erase a) (erase b) noAnn
erase (Pcase a bnd _) =
Pcase (erase a) (bind (x,y) (erase body)) noAnn where
((x,y),body) = unsafeUnbind bnd
instance Erase Match where
erase (Match bnd) = Match (bind p (erase t)) where
(p,t) = unsafeUnbind bnd
instance Erase Arg where
erase (Arg Runtime t) = Arg Runtime (erase t)
erase (Arg Erased t) = Arg Erased LitUnit
-----------------
-- * Alpha equivalence, free variables and substitution.
------------------
{- We use the unbound library to mark the binding occurrences of
variables in the syntax. That allows us to automatically derive
functions for alpha-equivalence, free variables and substitution
using the template haskell directives and default class instances
below.
-}
-- Defining SourcePos abstractly means that they get ignored
-- when comparing terms.
-- XXX need one with aeq' that always returns true.
$(makeClosedAlpha ''SourcePos)
-- instance Alpha SourcePos where
-- aeq' _ctx _ _ = True
-- fvAny' _ctx _nfn = pure
-- open _ _ = id
-- close _ _ = id
-- isPat _ = mempty
-- isTerm _ = True
-- nthPatFind _ _ = Left 0
-- namePatFind _ _ = Left 0
-- swaps' _ _ = id
-- freshen' _ x = return (x, mempty)
-- lfreshen' _ x cont = cont x mempty
instance Subst b SourcePos where subst _ _ = id ; substs _ = id
-- Among other things, the Alpha class enables the following
-- functions:
-- aeq :: Alpha a => a -> a -> Bool
-- fv :: Alpha a => a -> [Name a]
instance Alpha Term where
instance Alpha Match
instance Alpha Pattern
instance Alpha Epsilon
instance Alpha Telescope
instance Alpha Arg
instance Alpha ConstructorDef
instance Alpha Annot where
-- override default behavior so that type annotations are ignored
-- when comparing for alpha-equivalence
aeq' _ _ _ = True
-- The subst class derives capture-avoiding substitution
-- It has two parameters because the sort of thing we are substiting
-- for may not be the same as what we are substituting into:
-- class Subst b a where
-- subst :: Name b -> b -> a -> a -- single substitution
-- substs :: [(Name b, b)] -> a -> a -- multiple substitution
instance Subst Term Term where
isvar (Var x) = Just (SubstName x)
isvar _ = Nothing
instance Subst Term Epsilon
instance Subst Term Match
instance Subst Term Pattern
instance Subst Term Telescope
instance Subst Term Arg
instance Subst Term ConstructorDef
instance Subst Term Annot