n-osborne/CoreTT - Change ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC

rewrite following chapman thesis ch2

Created by Fi16Ka6f4bget8foxQRWszq749Zub3y9dC3XmFoMpoqr on October 21, 2021

ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC

Dependencies

In channels

main

Change contents

Deletion in src/AST.hs at line 4 [2.951]
B:BD[2.999] → [2.999:1054]
```
import Data.Map (Map)
import qualified Data.Map as Map
```

Replacement in src/AST.hs at line 11 [2.951]

B:BD[2.1144] → [2.1144:1189]

data TermInf
  = Global Name
  | Local Index

[2.1144]

[2.1189]

data Term
  = Var Index
  | Pi Term Term
  | Lam Term
  | Term :$ Term
  | Ann Term Term

Deletion in src/AST.hs at line 18 [2.951]

B:BD[2.1198] → [2.1198:1291]

  | Ann TermChk TermChk
  | App TermChk TermInf
  | Pi TermChk TermChk
  deriving (Eq, Show)

Replacement in src/AST.hs at line 19 [2.951]

B:BD[2.1292] → [2.1292:1359]

data TermChk
  = Inf TermInf
  | Lam TermChk
  deriving (Eq, Show)

[2.1292]

[2.1359]

data Val
  = VLam Term Env
  | VPi Val Term Env
  | VStar
  | Ne Ne

Replacement in src/AST.hs at line 25 [2.951]

B:BD[2.1360] → [2.1360:1444]

data Value
  = VStar
  | VLam TermChk
  | VPi TermChk TermChk
  deriving (Eq, Show)

[2.1360]

[2.1444]

data Ne = NV Index | Ne :$$ Val

Replacement in src/AST.hs at line 27 [2.951]
B:BD[2.1445] → [2.1445:1471]
```
type Env = Map Name Value
```
[2.1445]
[2.1471]
```
type Env = [Val]
```
Replacement in src/AST.hs at line 29 [2.951]
B:BD[2.1472] → [2.1472:1503]
```
empty :: Env
empty = Map.empty
```
[2.1472]
[2.1503]
```
type Ctx = [Val]
```

Replacement in src/AST.hs at line 31 [2.951]

B:BD[2.1504] → [2.1504:1523]

type Ctx = [Value]

[2.1504]

[2.1523]

whnf :: Term -> Env -> Maybe Val
whnf (Var i) env = env !! i
whnf (Pi d r) env = do
  vd <- (whnf d env)
  Just $ VPi vd r env
whnf (Lam t) env = Just $ VLam t env
whnf (f :$ a) env = do
  vf <- whnf f env
  va <- whnf a env
  vf $$ va
whnf (Ann t _) env = whnf t env
whnf Star _ = Just VStar

Replacement in src/AST.hs at line 44 [2.951]

B:BD[2.1524] → [2.1524:1569]

type Eval t = Env -> Ctx -> t -> Maybe Value

[2.1524]

[2.1569]

($$) :: Val -> Val -> Maybe Val
(VLam r env) $$ a = whnf r (a : env)
Ne n $$ a = Just (Ne (n :$$ a))
_ $$ _ = Nothing

Replacement in src/AST.hs at line 49 [2.951]

B:BD[2.1570] → [2.1570:1999]

evalInf :: Eval TermInf
evalInf env ctx (Global n) = Map.lookup n env
evalInf env ctx (Local idx) = ctx !! idx
evalInf env ctx Star = Just VStar
evalInf env ctx (Ann t _) = evalChk env ctx t
evalInf env ctx (App f a) = do
  a <- evalInf env ctx a
  case evalChk env ctx f of
    Just (VLam b) -> evalChk env (a : ctx) b
    Just (VPi _ b) -> evalChk env (a : ctx) b
    _ -> Nothing
evalInf env ctx (Pi dom t) = Just (VPi dom t)

[2.1570]

[2.1999]

wk :: Val -> Val
wk (VLam t env) = VLam t (ewk env)
wk (VPi d r env) = VPi (wk d) r (ewk env)
wk VStar = VStar
wk (Ne ne) = Ne $ nwk ne
ewk :: Env -> Env
ewk = map wk
cwk :: Ctx -> Ctx
cwk = map wk

Replacement in src/AST.hs at line 61 [2.951]

B:BD[2.2000] → [2.2000:2120]

evalChk :: Eval TermChk
evalChk env ctx (Inf term) = evalInf env ctx term
evalChk env ctx (Lam body) = Just (VLam body)

[2.2000]

nwk :: Ne -> Ne
nwk (NV i) = NV (i + 1)
nwk (n :$$ v) = nwk n :$$ wk v
fresh :: Val
fresh = Ne (NV 0)
eq :: Ctx -> Val -> Val -> Val -> Maybe ()
eq _ VStar VStar VStar = return ()
eq ctx VStar (VPi d1 r1 env1) (VPi d2 r2 env2) = do
  eq ctx VStar d1 d2
  whnfr1 <- (whnf r1 ((Ne (NV 0)) : ewk env1))
  whnfr2 <- (whnf r2 ((Ne (NV 0)) : ewk env2))
  eq (fresh : cwk ctx) VStar whnfr1 whnfr2
eq ctx (VPi _ r env) f g = do
  vr <- whnf r ((Ne (NV 0)) : ewk env)
  vf <- wk f $$ (Ne (NV 0))
  vg <- wk g $$ (Ne (NV 0))
  eq (fresh : cwk ctx) vr vf vg
eq ctx _ (Ne n1) (Ne n2) = neq ctx n1 n2 >> return ()
eq _ _ _ _ = Nothing
neq :: Ctx -> Ne -> Ne -> Maybe Val
neq ctx (NV i) (NV j) = if i == j then ctx !! i else Nothing
neq ctx (n1 :$$ v1) (n2 :$$ v2) = do
  VPi d r env <- neq ctx n1 n2
  eq ctx d v1 v2
  whnf r (v1 : env)
neq _ _ _ = Nothing

Insertion in CoreTT.cabal at line 34 [3.926]

[3.1710]

    ghc-options:
        -Wall
        -Werror
        -fwarn-incomplete-uni-patterns