rzk-0.8.0: src/Language/Rzk/Free/Syntax.hs
{-# OPTIONS_GHC -fno-warn-missing-pattern-synonym-signatures -fno-warn-missing-signatures -fno-warn-type-defaults #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeSynonymInstances #-}
module Language.Rzk.Free.Syntax where
import Data.Bifunctor.TH
import Data.Char (chr, ord)
import Data.Coerce
import Data.Function (on)
import Data.Functor (void)
import Data.List (intercalate, nub, (\\))
import Data.Maybe (fromMaybe)
import Data.String
import qualified Data.Text as T
import Free.Scoped
import Free.Scoped.TH
-- FIXME: use proper mechanisms for warnings
import Debug.Trace
import qualified Language.Rzk.Syntax as Rzk
data RzkPosition = RzkPosition
{ rzkFilePath :: Maybe FilePath
, rzkLineCol :: Rzk.BNFC'Position
}
ppRzkPosition :: RzkPosition -> String
ppRzkPosition RzkPosition{..} = intercalate ":" $ concat
[ [fromMaybe "<stdin>" rzkFilePath]
, foldMap (\(row, col) -> map show [row, col]) rzkLineCol]
newtype VarIdent = VarIdent { getVarIdent :: Rzk.VarIdent' RzkPosition }
instance Show VarIdent where
show = Rzk.printTree . getVarIdent
instance Eq VarIdent where
(==) = (==) `on` (void . getVarIdent)
instance IsString VarIdent where
fromString s = VarIdent (Rzk.VarIdent (RzkPosition Nothing Nothing) (fromString s))
ppVarIdentWithLocation :: VarIdent -> String
ppVarIdentWithLocation (VarIdent var@(Rzk.VarIdent pos _ident)) =
Rzk.printTree var <> " (" <> ppRzkPosition pos <> ")"
varIdent :: Rzk.VarIdent -> VarIdent
varIdent = varIdentAt Nothing
varIdentAt :: Maybe FilePath -> Rzk.VarIdent -> VarIdent
varIdentAt path (Rzk.VarIdent pos ident) = VarIdent (Rzk.VarIdent (RzkPosition path pos) ident)
fromVarIdent :: VarIdent -> Rzk.VarIdent
fromVarIdent (VarIdent (Rzk.VarIdent (RzkPosition _file pos) ident)) = Rzk.VarIdent pos ident
data TModality = Sharp | Flat | Op | Id deriving (Eq, Show)
toModality :: Rzk.Modality -> TModality
toModality Rzk.Sharp{} = Sharp
toModality Rzk.ASCII_Sharp{} = Sharp
toModality Rzk.Flat{} = Flat
toModality Rzk.ASCII_Flat{} = Flat
toModality Rzk.Op{} = Op
toModality Rzk.ASCII_Op{} = Op
toModality Rzk.Id{} = Id
modCompToMods :: Rzk.ModComp -> (TModality, TModality)
modCompToMods (Rzk.Single _ m) = (Id, toModality m)
modCompToMods (Rzk.Comp _ ext inn) = (toModality ext, toModality inn)
fromMod :: TModality -> Rzk.Modality
fromMod Sharp = Rzk.Sharp Nothing
fromMod Flat = Rzk.Flat Nothing
fromMod Op = Rzk.Op Nothing
fromMod Id = Rzk.Id Nothing
modsToModComp :: TModality -> TModality -> Rzk.ModComp
modsToModComp Id inn = Rzk.Single Nothing (fromMod inn)
modsToModComp ext inn = Rzk.Comp Nothing (fromMod ext) (fromMod inn)
data TermF scope term
= UniverseF
| UniverseCubeF
| UniverseTopeF
| CubeUnitF
| CubeUnitStarF
| Cube2F
| Cube2_0F
| Cube2_1F
| CubeProductF term term
| CubeFlipF term
| CubeUnflipF term
| TopeTopF
| TopeBottomF
| TopeEQF term term
| TopeLEQF term term
| TopeAndF term term
| TopeOrF term term
| TopeInvF term
| TopeUninvF term
| RecBottomF
| RecOrF [(term, term)]
| TypeFunF (Maybe VarIdent) term (Maybe scope) scope
| TypeSigmaF (Maybe VarIdent) term scope
| TypeIdF term (Maybe term) term
| AppF term term
| LetF (Maybe VarIdent) (Maybe term) term scope
| LambdaF (Maybe VarIdent) (Maybe (term, Maybe scope)) scope
| PairF term term
| FirstF term
| SecondF term
| ReflF (Maybe (term, Maybe term))
| IdJF term term term term term term
| UnitF
| TypeUnitF
| TypeAscF term term
| TypeRestrictedF term [(term, term)]
| TypeModalF TModality term
| ModAppF TModality term
| ModExtractF TModality TModality term
| LetModF (Maybe VarIdent) TModality TModality (Maybe term) term scope
deriving (Eq, Functor, Foldable, Traversable)
deriveBifunctor ''TermF
deriveBifoldable ''TermF
deriveBitraversable ''TermF
makePatternsAll ''TermF -- declare all patterns using Template Haskell
newtype Type term = Type { getType :: term }
deriving (Eq, Functor, Foldable, Traversable)
data TypeInfo term = TypeInfo
{ infoType :: term
, infoWHNF :: Maybe term
, infoNF :: Maybe term
} deriving (Eq, Functor, Foldable, Traversable)
type Term = FS TermF
type TermT = FS (AnnF TypeInfo TermF)
termIsWHNF :: TermT var -> TermT var
termIsWHNF t@Pure{} = t
termIsWHNF (Free (AnnF info f)) = t'
where
t' = Free (AnnF info { infoWHNF = Just t' } f)
termIsNF :: TermT var -> TermT var
termIsNF t@Pure{} = t
termIsNF (Free (AnnF info f)) = t'
where
t' = Free (AnnF info { infoWHNF = Just t', infoNF = Just t' } f)
invalidateWHNF :: TermT var -> TermT var
invalidateWHNF = transFS $ \(AnnF info f) ->
AnnF info { infoWHNF = Nothing, infoNF = Nothing } f
substituteT :: TermT var -> Scope TermT var -> TermT var
substituteT x = substitute x . invalidateWHNF
type Term' = Term VarIdent
type TermT' = TermT VarIdent
freeVars :: Term a -> [a]
freeVars = foldMap pure
-- FIXME: should be cached in TypeInfo?
partialFreeVarsT :: TermT a -> [a]
partialFreeVarsT (Pure x) = [x]
partialFreeVarsT UniverseT{} = []
partialFreeVarsT term@(Free (AnnF info _)) =
-- FIXME: check correctness (is it ok to use untyped here?)
foldMap (freeVars . untyped) [term, infoType info]
-- FIXME: should be cached in TypeInfo?
freeVarsT :: Eq a => (a -> TermT a) -> TermT a -> [a]
freeVarsT typeOfVar t = go [] (partialFreeVarsT t)
where
go vars latest
| null new = vars
| otherwise =
go (new <> vars)
(foldMap (partialFreeVarsT . typeOfVar) new)
where
new = nub latest \\ vars
toTerm' :: Rzk.Term -> Term'
toTerm' = toTerm Pure
toScope :: VarIdent -> (VarIdent -> Term a) -> Rzk.Term -> Scope Term a
toScope x bvars = toTerm $ \z -> if x == z then Pure Z else S <$> bvars z
toScopePattern :: Rzk.Pattern -> (VarIdent -> Term a) -> Rzk.Term -> Scope Term a
toScopePattern pat bvars = toTerm $ \z ->
case lookup z (bindings pat (Pure Z)) of
Just t -> t
Nothing -> S <$> bvars z
where
bindings (Rzk.PatternUnit _loc) _ = []
bindings (Rzk.PatternVar _loc (Rzk.VarIdent _ "_")) _ = []
bindings (Rzk.PatternVar _loc x) t = [(varIdent x, t)]
bindings (Rzk.PatternPair _loc l r) t = bindings l (First t) <> bindings r (Second t)
bindings (Rzk.PatternTuple loc p1 p2 ps) t = bindings (desugarTuple loc (reverse ps) p2 p1) t
desugarTuple loc ps p2 p1 =
case ps of
[] -> Rzk.PatternPair loc p1 p2
pLast : ps' -> Rzk.PatternPair loc (desugarTuple loc ps' p2 p1) pLast
toTerm :: (VarIdent -> Term a) -> Rzk.Term -> Term a
toTerm bvars = go
where
deprecated t t' = trace msg (go t')
where
msg = unlines
[ "[DEPRECATED]:" <> ppBNFC'Position (Rzk.hasPosition t)
, "the following notation is deprecated and will be removed from future version of rzk:"
, " " <> Rzk.printTree t
, "instead consider using the following notation:"
, " " <> Rzk.printTree t'
]
ppBNFC'Position Nothing = ""
ppBNFC'Position (Just (line_, col)) = " at line " <> show line_ <> " column " <> show col
lint orig suggestion = trace $ unlines
[ "[HINT]:" <> ppBNFC'Position (Rzk.hasPosition orig) <> " consider replacing"
, " " <> Rzk.printTree orig
, "with the following"
, " " <> Rzk.printTree suggestion
]
go = \case
-- Depracations
t@(Rzk.RecOrDeprecated loc psi phi a_psi a_phi) -> deprecated t
(Rzk.RecOr loc [Rzk.Restriction loc psi a_psi, Rzk.Restriction loc phi a_phi])
t@(Rzk.TypeExtensionDeprecated loc shape type_) -> deprecated t
(Rzk.TypeFun loc shape type_)
t@(Rzk.TypeFun loc (Rzk.ParamTermTypeDeprecated loc' pat type_) ret) -> deprecated t
(Rzk.TypeFun loc (Rzk.ParamTermType loc' (patternToTerm pat) type_) ret)
t@(Rzk.TypeFun loc (Rzk.ParamVarShapeDeprecated loc' pat cube tope) ret) -> deprecated t
(Rzk.TypeFun loc (Rzk.ParamTermShape loc' (patternToTerm pat) cube tope) ret)
t@(Rzk.Lambda loc ((Rzk.ParamPatternShapeDeprecated loc' pat cube tope):params) body) -> deprecated t
(Rzk.Lambda loc ((Rzk.ParamPatternShape loc' [pat] cube tope):params) body)
-- ASCII versions
Rzk.ASCII_CubeUnitStar loc -> go (Rzk.CubeUnitStar loc)
Rzk.ASCII_Cube2_0 loc -> go (Rzk.Cube2_0 loc)
Rzk.ASCII_Cube2_1 loc -> go (Rzk.Cube2_1 loc)
Rzk.ASCII_TopeTop loc -> go (Rzk.TopeTop loc)
Rzk.ASCII_TopeBottom loc -> go (Rzk.TopeBottom loc)
Rzk.ASCII_TopeEQ loc l r -> go (Rzk.TopeEQ loc l r)
Rzk.ASCII_TopeLEQ loc l r -> go (Rzk.TopeLEQ loc l r)
Rzk.ASCII_TopeAnd loc l r -> go (Rzk.TopeAnd loc l r)
Rzk.ASCII_TopeOr loc l r -> go (Rzk.TopeOr loc l r)
Rzk.ASCII_TypeFun loc param ret -> go (Rzk.TypeFun loc param ret)
Rzk.ASCII_TypeSigma loc pat ty ret -> go (Rzk.TypeSigma loc pat ty ret)
Rzk.ASCII_TypeSigmaModal _loc pat md ty body -> go (Rzk.TypeSigmaModal _loc pat md ty body)
Rzk.ASCII_TypeSigmaTuple loc p ps tN -> go (Rzk.TypeSigmaTuple loc p ps tN)
Rzk.ASCII_Lambda loc pat ret -> go (Rzk.Lambda loc pat ret)
Rzk.ASCII_TypeExtensionDeprecated loc shape type_ -> go (Rzk.TypeExtensionDeprecated loc shape type_)
Rzk.ASCII_First loc term -> go (Rzk.First loc term)
Rzk.ASCII_Second loc term -> go (Rzk.Second loc term)
Rzk.Var _loc x -> bvars (varIdent x)
Rzk.Universe _loc -> Universe
Rzk.UniverseCube _loc -> UniverseCube
Rzk.UniverseTope _loc -> UniverseTope
Rzk.CubeUnit _loc -> CubeUnit
Rzk.CubeUnitStar _loc -> CubeUnitStar
Rzk.Cube2 _loc -> Cube2
Rzk.Cube2_0 _loc -> Cube2_0
Rzk.Cube2_1 _loc -> Cube2_1
Rzk.CubeProduct _loc l r -> CubeProduct (go l) (go r)
Rzk.TopeTop _loc -> TopeTop
Rzk.TopeBottom _loc -> TopeBottom
Rzk.TopeEQ _loc l r -> TopeEQ (go l) (go r)
Rzk.TopeLEQ _loc l r -> TopeLEQ (go l) (go r)
Rzk.TopeAnd _loc l r -> TopeAnd (go l) (go r)
Rzk.TopeOr _loc l r -> TopeOr (go l) (go r)
Rzk.TopeInv _loc t -> TopeInv (go t)
Rzk.TopeUninv _loc t -> TopeUninv (go t)
Rzk.CubeFlip _loc t -> CubeFlip (go t)
Rzk.CubeUnflip _loc t -> CubeUnflip (go t)
Rzk.RecBottom _loc -> RecBottom
Rzk.RecOr _loc rs -> RecOr $ flip map rs $ \case
Rzk.Restriction _loc tope term -> (go tope, go term)
Rzk.ASCII_Restriction _loc tope term -> (go tope, go term)
Rzk.TypeId _loc x tA y -> TypeId (go x) (Just (go tA)) (go y)
Rzk.TypeIdSimple _loc x y -> TypeId (go x) Nothing (go y)
Rzk.TypeUnit _loc -> TypeUnit
Rzk.Unit _loc -> Unit
Rzk.App _loc f x -> App (go f) (go x)
Rzk.Pair _loc l r -> Pair (go l) (go r)
Rzk.Tuple _loc p1 p2 (p:ps) -> go (Rzk.Tuple _loc (Rzk.Pair _loc p1 p2) p ps)
Rzk.Tuple _loc p1 p2 [] -> go (Rzk.Pair _loc p1 p2)
Rzk.First _loc term -> First (go term)
Rzk.Second _loc term -> Second (go term)
Rzk.Refl _loc -> Refl Nothing
Rzk.ReflTerm _loc term -> Refl (Just (go term, Nothing))
Rzk.ReflTermType _loc x tA -> Refl (Just (go x, Just (go tA)))
Rzk.IdJ _loc a b c d e f -> IdJ (go a) (go b) (go c) (go d) (go e) (go f)
Rzk.TypeAsc _loc x t -> TypeAsc (go x) (go t)
Rzk.TypeFun _loc (Rzk.ParamTermModalType loc' patTerm md ty) ret ->
let pat = unsafeTermToPattern patTerm
letRet = Rzk.LetMod loc' (Rzk.Single loc' md)
(Rzk.BindPattern loc' pat) (patternToTerm pat) ret
in go (Rzk.TypeFun _loc (Rzk.ParamTermType loc' patTerm (Rzk.ModType loc' md ty)) letRet)
Rzk.TypeFun _loc (Rzk.ParamTermType _ patTerm arg) ret ->
let pat = unsafeTermToPattern patTerm
in TypeFun (patternVar pat) (go arg) Nothing (toScopePattern pat bvars ret)
t@(Rzk.TypeFun loc (Rzk.ParamTermShape loc' patTerm cube tope) ret) ->
let lint' = case tope of
Rzk.App _loc fun arg | void arg == void patTerm ->
lint t (Rzk.TypeFun loc (Rzk.ParamTermType loc' patTerm fun) ret)
_ -> id
pat = unsafeTermToPattern patTerm
in lint' $ TypeFun (patternVar pat) (go cube) (Just (toScopePattern pat bvars tope)) (toScopePattern pat bvars ret)
Rzk.TypeFun _loc (Rzk.ParamType _ arg) ret ->
TypeFun Nothing (go arg) Nothing (toTerm (fmap S <$> bvars) ret)
Rzk.TypeSigma _loc pat tA tB ->
TypeSigma (patternVar pat) (go tA) (toScopePattern pat bvars tB)
Rzk.TypeSigmaModal _loc pat md ty body ->
let letBody = Rzk.LetMod _loc (Rzk.Single _loc md)
(Rzk.BindPattern _loc pat) (patternToTerm pat) body
in go (Rzk.TypeSigma _loc pat (Rzk.ModType _loc md ty) letBody)
Rzk.TypeSigmaTuple _loc (Rzk.SigmaParamModal loc' pat md ty) rest body ->
let tailSigma = case rest of
[] -> body
[sp] -> sigmaParamToTypeSigma _loc sp body
(sp:sps) -> Rzk.TypeSigmaTuple _loc sp sps body
letTail = Rzk.LetMod loc' (Rzk.Single loc' md)
(Rzk.BindPattern loc' pat) (patternToTerm pat) tailSigma
in go (Rzk.TypeSigma _loc pat (Rzk.ModType loc' md ty) letTail)
Rzk.TypeSigmaTuple _loc (Rzk.SigmaParam _ patA tA) (mp@(Rzk.SigmaParamModal{}) : rest) body ->
go (Rzk.TypeSigma _loc patA tA (case rest of
[] -> sigmaParamToTypeSigma _loc mp body
_ -> Rzk.TypeSigmaTuple _loc mp rest body))
Rzk.TypeSigmaTuple _loc (Rzk.SigmaParam _ patA tA) ((Rzk.SigmaParam _ patB tB) : ps) tN ->
go (Rzk.TypeSigmaTuple _loc (Rzk.SigmaParam _loc patX tX) ps tN)
where
patX = Rzk.PatternPair _loc patA patB
tX = Rzk.TypeSigma _loc patA tA tB
Rzk.TypeSigmaTuple _loc (Rzk.SigmaParam _ pat tA) [] tB -> go (Rzk.TypeSigma _loc pat tA tB)
Rzk.Lambda _loc (Rzk.ParamPatternModalType _ [] _md _ty : params) body ->
go (Rzk.Lambda _loc params body)
Rzk.Lambda _loc (Rzk.ParamPatternModalType loc' (pat:pats) md ty : params) body ->
let inner = Rzk.Lambda _loc
(if null pats then params
else Rzk.ParamPatternModalType loc' pats md ty : params)
body
letBody = Rzk.LetMod loc' (Rzk.Single loc' md)
(Rzk.BindPattern loc' pat) (patternToTerm pat) inner
in go (Rzk.Lambda _loc [Rzk.ParamPatternType loc' [pat] (Rzk.ModType loc' md ty)] letBody)
Rzk.Lambda _loc [] body -> go body
Rzk.Lambda _loc (Rzk.ParamPattern _ pat : params) body ->
Lambda (patternVar pat) Nothing (toScopePattern pat bvars (Rzk.Lambda _loc params body))
Rzk.Lambda _loc (Rzk.ParamPatternType _ [] _ty : params) body ->
go (Rzk.Lambda _loc params body)
Rzk.Lambda _loc (Rzk.ParamPatternType _ (pat:pats) ty : params) body ->
Lambda (patternVar pat) (Just (go ty, Nothing))
(toScopePattern pat bvars (Rzk.Lambda _loc (Rzk.ParamPatternType _loc pats ty : params) body))
Rzk.Lambda _loc (Rzk.ParamPatternShape _ [] _cube _tope : params) body ->
go (Rzk.Lambda _loc params body)
t@(Rzk.Lambda _loc (Rzk.ParamPatternShape _loc' (pat:pats) cube tope : params) body) ->
let lint' = case tope of
Rzk.App _loc fun arg
| null pats && void arg == void (patternToTerm pat) ->
lint t (Rzk.Lambda _loc (Rzk.ParamPatternType _loc' [pat] fun : params) body)
_ -> id
in lint' $ Lambda (patternVar pat) (Just (go cube, Just (toScopePattern pat bvars tope)))
(toScopePattern pat bvars (Rzk.Lambda _loc (Rzk.ParamPatternShape _loc' pats cube tope : params) body))
Rzk.Let _loc (Rzk.BindPattern _ pat) val expr ->
Let (patternVar pat) Nothing (go val) (toScopePattern pat bvars expr)
Rzk.Let _loc (Rzk.BindPatternType _ pat ty) val expr ->
Let (patternVar pat) (Just (go ty)) (go val) (toScopePattern pat bvars expr)
Rzk.TypeRestricted _loc ty rs ->
TypeRestricted (go ty) $ flip map rs $ \case
Rzk.Restriction _loc tope term -> (go tope, go term)
Rzk.ASCII_Restriction _loc tope term -> (go tope, go term)
Rzk.Hole _loc _ident -> error "holes are not supported"
Rzk.ModApp _loc md body -> ModApp (toModality md) (go body)
Rzk.ModType _loc md ty -> TypeModal (toModality md) (go ty)
Rzk.ModExtract{} -> error "$extract$ is an internal term and cannot appear in source"
Rzk.LetMod _loc comp (Rzk.BindPattern _ pat) val body ->
let (ext, inn) = modCompToMods comp
in LetMod (patternVar pat) ext inn Nothing (go val) (toScopePattern pat bvars body)
Rzk.LetMod _loc comp (Rzk.BindPatternType _ pat ty) val body ->
let (ext, inn) = modCompToMods comp
in LetMod (patternVar pat) ext inn (Just (go ty)) (go val) (toScopePattern pat bvars body)
patternVar (Rzk.PatternVar _loc (Rzk.VarIdent _ "_")) = Nothing
patternVar (Rzk.PatternVar _loc x) = Just (varIdent x)
patternVar _ = Nothing
patternToTerm :: Rzk.Pattern -> Rzk.Term
patternToTerm = ptt
where
ptt = \case
Rzk.PatternVar loc x -> Rzk.Var loc x
Rzk.PatternPair loc l r -> Rzk.Pair loc (ptt l) (ptt r)
Rzk.PatternUnit loc -> Rzk.Unit loc
Rzk.PatternTuple loc p1 p2 ps -> patternToTerm (desugarTuple loc (reverse ps) p2 p1)
unsafeTermToPattern :: Rzk.Term -> Rzk.Pattern
unsafeTermToPattern = ttp
where
ttp = \case
Rzk.Unit loc -> Rzk.PatternUnit loc
Rzk.Var loc x -> Rzk.PatternVar loc x
Rzk.Pair loc l r -> Rzk.PatternPair loc (ttp l) (ttp r)
Rzk.Tuple loc t1 t2 ts -> Rzk.PatternTuple loc (ttp t1) (ttp t2) (map ttp ts)
term -> error ("ERROR: expected a pattern but got\n " ++ Rzk.printTree term)
sigmaParamToTypeSigma :: Rzk.BNFC'Position -> Rzk.SigmaParam -> Rzk.Term -> Rzk.Term
sigmaParamToTypeSigma loc sp body = case sp of
Rzk.SigmaParam _ pat ty -> Rzk.TypeSigma loc pat ty body
Rzk.SigmaParamModal _ pat md ty -> Rzk.TypeSigmaModal loc pat md ty body
fromTerm' :: Term' -> Rzk.Term
fromTerm' t = fromTermWith' vars (defaultVarIdents \\ vars) t
where vars = freeVars t
fromScope' :: VarIdent -> [VarIdent] -> [VarIdent] -> Scope Term VarIdent -> Rzk.Term
fromScope' x used xs = fromTermWith' (x : used) xs . (>>= f)
where
f Z = Pure x
f (S z) = Pure z
fromTermWith' :: [VarIdent] -> [VarIdent] -> Term' -> Rzk.Term
fromTermWith' used vars = go
where
withFresh Nothing f =
case vars of
x:xs -> f (x, xs)
_ -> error "not enough fresh variables!"
withFresh (Just z) f = f (z', filter (/= z') vars) -- FIXME: very inefficient filter
where
z' = refreshVar used z
loc = Nothing
goMod :: TModality -> Rzk.Modality
goMod Sharp = Rzk.Sharp loc
goMod Flat = Rzk.Flat loc
goMod Op = Rzk.Op loc
goMod Id = Rzk.Id loc
go :: Term' -> Rzk.Term
go = \case
Pure z -> Rzk.Var loc (fromVarIdent z)
Universe -> Rzk.Universe loc
UniverseCube -> Rzk.UniverseCube loc
UniverseTope -> Rzk.UniverseTope loc
CubeUnit -> Rzk.CubeUnit loc
CubeUnitStar -> Rzk.CubeUnitStar loc
Cube2 -> Rzk.Cube2 loc
Cube2_0 -> Rzk.Cube2_0 loc
Cube2_1 -> Rzk.Cube2_1 loc
CubeProduct l r -> Rzk.CubeProduct loc (go l) (go r)
TopeTop -> Rzk.TopeTop loc
TopeBottom -> Rzk.TopeBottom loc
TopeEQ l r -> Rzk.TopeEQ loc (go l) (go r)
TopeLEQ l r -> Rzk.TopeLEQ loc (go l) (go r)
TopeAnd l r -> Rzk.TopeAnd loc (go l) (go r)
TopeOr l r -> Rzk.TopeOr loc (go l) (go r)
TopeInv t -> Rzk.TopeInv loc (go t)
TopeUninv t -> Rzk.TopeUninv loc (go t)
CubeFlip t -> Rzk.CubeFlip loc (go t)
CubeUnflip t -> Rzk.CubeUnflip loc (go t)
RecBottom -> Rzk.RecBottom loc
RecOr rs -> Rzk.RecOr loc [ Rzk.Restriction loc (go tope) (go term) | (tope, term) <- rs ]
TypeFun z arg Nothing ret -> withFresh z $ \(x, xs) ->
Rzk.TypeFun loc (Rzk.ParamTermType loc (Rzk.Var loc (fromVarIdent x)) (go arg)) (fromScope' x used xs ret)
TypeFun z arg (Just tope) ret -> withFresh z $ \(x, xs) ->
Rzk.TypeFun loc (Rzk.ParamTermShape loc (Rzk.Var loc (fromVarIdent x)) (go arg) (fromScope' x used xs tope)) (fromScope' x used xs ret)
TypeSigma z a b -> withFresh z $ \(x, xs) ->
Rzk.TypeSigma loc (Rzk.PatternVar loc (fromVarIdent x)) (go a) (fromScope' x used xs b)
TypeId l (Just tA) r -> Rzk.TypeId loc (go l) (go tA) (go r)
TypeId l Nothing r -> Rzk.TypeIdSimple loc (go l) (go r)
App l r -> Rzk.App loc (go l) (go r)
Lambda z Nothing scope -> withFresh z $ \(x, xs) ->
Rzk.Lambda loc [Rzk.ParamPattern loc (Rzk.PatternVar loc (fromVarIdent x))] (fromScope' x used xs scope)
Lambda z (Just (ty, Nothing)) scope -> withFresh z $ \(x, xs) ->
Rzk.Lambda loc [Rzk.ParamPatternType loc [Rzk.PatternVar loc (fromVarIdent x)] (go ty)] (fromScope' x used xs scope)
Lambda z (Just (cube, Just tope)) scope -> withFresh z $ \(x, xs) ->
Rzk.Lambda loc [Rzk.ParamPatternShape loc [Rzk.PatternVar loc (fromVarIdent x)] (go cube) (fromScope' x used xs tope)] (fromScope' x used xs scope)
-- Lambda (Maybe (term, Maybe scope)) scope -> Rzk.Lambda loc (Maybe (term, Maybe scope)) scope
Let z Nothing val scope -> withFresh z $ \(x, xs) ->
Rzk.Let loc (Rzk.BindPattern loc (Rzk.PatternVar loc (fromVarIdent x))) (go val) (fromScope' x used xs scope)
Let z (Just ty) val scope -> withFresh z $ \(x, xs) ->
Rzk.Let loc (Rzk.BindPatternType loc (Rzk.PatternVar loc (fromVarIdent x)) (go ty)) (go val) (fromScope' x used xs scope)
Pair l r -> Rzk.Pair loc (go l) (go r)
First term -> Rzk.First loc (go term)
Second term -> Rzk.Second loc (go term)
TypeUnit -> Rzk.TypeUnit loc
Unit -> Rzk.Unit loc
Refl Nothing -> Rzk.Refl loc
Refl (Just (t, Nothing)) -> Rzk.ReflTerm loc (go t)
Refl (Just (t, Just ty)) -> Rzk.ReflTermType loc (go t) (go ty)
IdJ a b c d e f -> Rzk.IdJ loc (go a) (go b) (go c) (go d) (go e) (go f)
TypeAsc l r -> Rzk.TypeAsc loc (go l) (go r)
TypeRestricted ty rs ->
Rzk.TypeRestricted loc (go ty) (map (\(tope, term) -> (Rzk.Restriction loc (go tope) (go term))) rs)
TypeModal m ty -> Rzk.ModType loc (goMod m) (go ty)
ModApp m ty -> Rzk.ModApp loc (goMod m) (go ty)
ModExtract ma mb t -> Rzk.ModExtract loc (Rzk.Comp loc (goMod ma) (goMod mb)) (go t)
LetMod z ext inn Nothing val scope -> withFresh z $ \(x, xs) ->
Rzk.LetMod loc (modsToModComp ext inn)
(Rzk.BindPattern loc (Rzk.PatternVar loc (fromVarIdent x)))
(go val) (fromScope' x used xs scope)
LetMod z ext inn (Just ty) val scope -> withFresh z $ \(x, xs) ->
Rzk.LetMod loc (modsToModComp ext inn)
(Rzk.BindPatternType loc (Rzk.PatternVar loc (fromVarIdent x)) (go ty))
(go val) (fromScope' x used xs scope)
defaultVarIdents :: [VarIdent]
defaultVarIdents =
[ fromString name
| n <- [1..]
, let name = "x" <> map digitToSub (show n) ]
where
digitToSub c = chr ((ord c - ord '0') + ord '₀')
-- | Given a list of used variable names in the current context,
-- generate a unique fresh name based on a given one.
--
-- >>> print $ refreshVar ["x", "y", "x₁", "z"] "x"
-- x₂
refreshVar :: [VarIdent] -> VarIdent -> VarIdent
refreshVar vars x
| x `elem` vars = refreshVar vars (incVarIdentIndex x)
| otherwise = x
incVarIdentIndex :: VarIdent -> VarIdent
incVarIdentIndex (VarIdent (Rzk.VarIdent loc token)) =
VarIdent (Rzk.VarIdent loc (coerce incIndex token))
-- | Increment the subscript number at the end of the indentifier.
--
-- >>> putStrLn $ T.unpack $ incIndex "x"
-- x₁
-- >>> putStrLn $ T.unpack $ incIndex "x₁₉"
-- x₂₀
incIndex :: T.Text -> T.Text
incIndex s = T.pack $ name <> newIndex
where
digitsSub = "₀₁₂₃₄₅₆₇₈₉" :: String
isDigitSub = (`elem` digitsSub)
digitFromSub c = chr ((ord c - ord '₀') + ord '0')
digitToSub c = chr ((ord c - ord '0') + ord '₀')
(name, index) = break isDigitSub (T.unpack s)
oldIndexN = read ('0' : map digitFromSub index) -- FIXME: read
newIndex = map digitToSub (show (oldIndexN + 1))
instance Show Term' where
show = Rzk.printTree . fromTerm'
instance IsString Term' where
fromString = toTerm' . fromRight . Rzk.parseTerm . T.pack
where
fromRight (Left err) = error (T.unpack $ "Parse error: " <> err)
fromRight (Right t) = t
instance Show TermT' where
show var@Pure{} = Rzk.printTree (fromTerm' (untyped var))
show term@(Free (AnnF TypeInfo{..} _)) = termStr <> " : " <> typeStr
where
termStr = Rzk.printTree (fromTerm' (untyped term))
typeStr = Rzk.printTree (fromTerm' (untyped infoType))