amelia
/
CCHM


{-# LANGUAGE ViewPatterns #-}

{-# LANGUAGE LambdaCase #-}

{-# LANGUAGE PatternSynonyms #-}

module Syntax where


import qualified Data.Map.Strict as Map

import qualified Data.Set as Set

import Data.Map.Strict (Map)

import Data.Set (Set)


import Presyntax (Formula)


import Systems


import Text.Show (showListWith)


type Space = Term


data Term

 = Var String

 | App Term Term

 | Lam String Term Term

 | Let String Term Term Term


 | Pi String Term Term

 | Type | Typeω


 | I

 | I0 | I1

 | IAnd Term Term

 | IOr Term Term

 | INot Term


 | Path Space Term Term

 | PathI Space Term Term String Term

 | PathP Space Term Term Term Term


 | Sigma String Term Term

 | Pair Term Term

 | Proj1 Term

 | Proj2 Term


 | System (System Term)

 | Partial Term Term

 | PartialP Term Term

 | Comp Term Term Term Term

 | Sub Term Term Term

 | InclSub Term Term Term Term


 | GlueTy

 Term -- Base type

 Term -- Extent

 Term -- Partial types

 Term -- Partial equivs

 | Glue

 Term -- Base

 Term -- Extent

 Term -- Partial types

 Term -- Partial equivs

 Term -- t

 Term -- a

 | Unglue

 Term -- Base

 Term -- Extent

 Term -- Partial types

 Term -- Partial equivs

 Term -- glued value


 | Bool

 | Tt | Ff

 | If Term Term Term Term

 deriving (Eq, Ord)


instance Show Term where

 showsPrec p =

 \case

 Var s -> showString s

 System fs -> showListWith showPE (Map.toList (getSystem fs))

 -- ew

 App (App (App (Lam _ _ (Lam _ _ (Lam _ _ Path{}))) a) x) y -> showsPrec p (Path a x y)

 App (App (App (Lam _ _ (Lam _ _ (Lam _ _ Sub{}))) a) x) y -> showsPrec p (Sub a x y)

 App (App (Lam _ _ (Lam _ _ Partial{})) phi) r -> showsPrec p (Partial phi r)

 App (App (Lam _ _ (Lam _ _ PartialP{})) phi) r -> showsPrec p (PartialP phi r)


 App (App (App (App (Lam _ _ (Lam _ _ (Lam _ _ (Lam _ _ Comp{})))) a) phi) u) a0 ->

 showsPrec p (Comp a phi u a0)


 App (App (App (App (Lam _ _ (Lam _ _ (Lam _ _ (Lam _ _ GlueTy{})))) a) phi) u) a0 ->

 showsPrec p (GlueTy a phi u a0)


 App f x -> showParen (p >= app_prec) $

 showsPrec fun_prec f

 . showChar ' '

 . showsPrec app_prec x


 Lam s t b ->

 let

 getLams (Lam s _ b) =

 let (as, b') = getLams b

 in (s:as, b')

 getLams (PathI _a _x _y s b) =

 let (as, b') = getLams b

 in (("(" ++ s ++ " : I)"):as, b')

 getLams t = ([], t)

 (args, bd) = getLams (Lam s t b)

 in showParen (p >= fun_prec) $

 showString ("λ " ++ unwords args ++ " -> ")

 . shows bd


 Let s t d b -> showParen (p > fun_prec) $

 showString "let\n "

 . showString s

 . showString " : "

 . shows t

 . showString " = "

 . shows d

 . showString " in "

 . shows b


 Pi "_" d r ->

 showParen (p >= domain_prec) $

 showsPrec domain_prec d

 . showString " -> "

 . shows r


 Pi v d r -> showParen (p >= domain_prec) $

 let

 showBinder (Pi "_" d r) =

 showsPrec domain_prec d

 . showString " -> "

 . shows r

 showBinder (Pi n d r) =

 let

 arr = case r of

 Pi n _ _ | n /= "_" -> " "

 _ -> " -> "

 in

 showParen True (showString n . showString " : " . shows d)

 . showString arr

 . showBinder r

 showBinder t = shows t

 in showBinder (Pi v d r)


 Type -> showString "Type"

 Typeω -> showString "Typeω"

 I -> showChar 'I'

 I0 -> showString "i0"

 I1 -> showString "i1"


 IAnd i j -> showParen (p >= and_prec) $

 showsPrec or_prec i

 . showString " && "

 . showsPrec or_prec j


 IOr i j -> showParen (p >= or_prec) $

 showsPrec app_prec i

 . showString " || "

 . showsPrec app_prec j


 INot s -> showChar '~' . showsPrec p s


 Path a x y -> showApps p (Var "Path") [a, x, y]

 Sub a x y -> showApps p (Var "Sub") [a, x, y]

 InclSub _a _phi _u0 a0 -> showsPrec p a0


 GlueTy a phi t e -> showApps p (Var "Glue") [a, phi, t, e]

 Glue base phi ty te t a ->

 showApps p (Var "glue") [phi, t, a]

 Unglue base phi ty te a ->

 showApps p (Var "unglue") [a]


 Partial r a -> showApps p (Var "Partial") [r, a]

 PartialP r a -> showApps p (Var "PartialP") [r, a]


 Comp a phi u a0 -> showApps p (Var "comp") [a, phi, u, a0]


 If _ Ff Tt d -> showApps p (Var "not") [d]

 If _ b c d -> showApps p (Var "if") [b, c, d]


 Bool -> showString "Bool"

 Tt -> showString "tt"

 Ff -> showString "ff"


 PathI a x y s b -> showParen (p >= fun_prec) $

 showString ("λ " ++ s ++ " -> ")

 . shows b

 PathP _a _x _y f i -> showsPrec p (App f i)


 Pair a b -> showParen True $

 shows a

 . showString ", "

 . shows b


 Proj1 b -> showsPrec p b . showString ".1"

 Proj2 b -> showsPrec p b . showString ".1"

 Sigma v d r ->

 showParen (p >= app_prec) $

 showParen True (showString v . showString " : " . shows d)

 . showString " × "

 . shows r

 where

 app_prec = 6

 domain_prec = 5

 and_prec = 4

 or_prec = 3

 fun_prec = 1


showApps :: Int -> Term -> [Term] -> ShowS

showApps p f xs = showsPrec p (foldl App f xs)


showPE :: (Formula, Term) -> String -> String

showPE (f, t) = shows f . showString " -> " . shows t


data Value

 = VNe String [Proj]

 | VLam String Value (Value -> Value)

 | VPi String Value (Value -> Value)

 | VType | VTypeω

 | VI | VI0 | VI1

 | VEqGlued Value Value -- e which is def. eq. to e'

 | VPair Value Value

 | VSigma String Value (Value -> Value)

 | VLine Value Value Value (Value -> Value)

 -- (λ i → ...) : Path A x y

 -- order: A x y k

 | VSystem (System Value)

 | VOfSub Value Value Value Value


 | VIAnd Value Value

 | VIOr Value Value

 | VINot Value


 | VPath Value Value Value

 | VSub Value Value Value

 | VPartial Value Value

 | VPartialP Value Value

 | VComp Value Value Value Value


 | VGlue Value Value Value Value

 | VGlueIntro Value Value Value Value Value Value

 | VGlueElim Value Value Value Value Value


 | VBool

 | VTrue

 | VFalse

 | VIf Value Value Value Value


data Proj

 = PApp Value

 | PPathP Value Value Value Value

 -- a x y i

 | PProj1

 | PProj2


pattern VVar :: String -> Value

pattern VVar x = VNe x []


quote :: Value -> Term

quote = go mempty where

 go :: Set String -> Value -> Term

 go scope (VNe hd spine) = foldl (goSpine scope) (Var hd) (reverse spine)

 go scope (VLam s a k) =

 let n = rename s scope

 in Lam n (go scope a) (go (Set.insert n scope) (k (VVar n)))

 go scope (VPi s d r) =

 let n = rename s scope

 in Pi n (go scope d) (go (Set.insert n scope) (r (VVar n)))

 go scope (VSigma s d r) =

 let n = rename s scope

 in Sigma n (go scope d) (go (Set.insert n scope) (r (VVar n)))


 go _ VType = Type

 go _ VI0 = I0

 go _ VI1 = I1

 go _ VI = I

 go _ VTypeω = Typeω


 go scope (VIAnd x y) = IAnd (go scope x) (go scope y)

 go scope (VIOr x y) = IOr (go scope x) (go scope y)

 go scope (VINot x) = INot (go scope x)


 go scope (VPath a x y) = Path (go scope a) (go scope x) (go scope y)

 go scope (VSub a x y) = Sub (go scope a) (go scope x) (go scope y)

 go scope (VPartial r a) = Partial (go scope r) (go scope a)

 go scope (VPartialP r a) = PartialP (go scope r) (go scope a)

 go scope (VComp a b c d) = Comp (go scope a) (go scope b) (go scope c) (go scope d)


 go scope (VEqGlued e _) = go scope e

 go scope (VPair a b) = Pair (go scope a) (go scope b)

 go scope (VLine a x y k) =

 let n = rename "i" scope

 in PathI (go scope a) (go scope x) (go scope y) n (go (Set.insert n scope) (k (VVar n)))

 go scope (VSystem (FMap fs)) = System (FMap (fmap (go scope) fs))

 go scope (VOfSub _ _ _ x) = go scope x


 go scope (VGlue a phi tys eqvs) = GlueTy (go scope a) (go scope phi) (go scope tys) (go scope eqvs)

 go scope (VGlueIntro base phi tys eqvs t a) =

 Glue (go scope base) (go scope phi) (go scope tys) (go scope eqvs) (go scope t) (go scope a)

 go scope (VGlueElim base phi tys eqvs a) =

 Unglue (go scope base) (go scope phi) (go scope tys) (go scope eqvs) (go scope a)


 go scope VBool = Bool

 go scope VTrue = Tt

 go scope VFalse = Ff

 go scope (VIf a b c d) = If (go scope a) (go scope b) (go scope c) (go scope d)


 goSpine :: Set String -> Term -> Proj -> Term

 goSpine scope t (PApp x) = App t (go scope x)

 goSpine scope t (PPathP a x y i) = PathP (go scope a) (go scope x) (go scope y) t (go scope i)

 goSpine scope t PProj1 = Proj1 t

 goSpine scope t PProj2 = Proj2 t


rename :: String -> Set String -> String

rename x s

 | x == "_" = x

 | x `Set.member` s = rename (x ++ "'") s

 | otherwise = x


instance Show Value where

 showsPrec p = showsPrec p . quote


data Env =

 Env { names :: Map String (Value, Value)

 }

 deriving (Show)