6 | module Language.IntrinsicScoping.TypeTheory

  8 | import Control.Monad.Error.Interface

  9 | import Decidable.Equality

 10 | import Data.SnocList

 11 | import Data.List.Quantifiers

 12 | import Data.SnocList.Quantifiers

 14 | import Language.IntrinsicScoping.Variables

 37 | public export

 38 | Scoped : Type

 39 | Scoped = LContext -> IContext -> Type

 42 | data Abs : Scoped -> Scoped where

 43 |   MkAbs : (x : Name) -> t f (g :< x) -> Abs t f g

 46 | data Infer : Scoped

 49 | data Check : Scoped

 52 | data Infer : Scoped where

 53 |   ||| A checkable term annotated with its expected type

 54 |   Ann : (t, ty : Check f g) -> Infer f g

 55 |   ||| The star kind is inferrable

 56 |   Star : Infer f g

 57 |   ||| The nat type is inferrable

 58 |   Nat : Infer f g

 59 |   ||| The nat induction principle is inferrable

 60 |   Rec : (pred, pz, ps : Check f g) -> (n : Check f g) -> Infer f g

 62 |   -- This is fairly unconventional: in order to support overloaded

 63 |   -- data constructors disambiguated in a type-direct manner, we would

 64 |   -- typically put zero, suc, & friends in `Check`.

 65 |   ||| The zero constructor is inferrable

 66 |   Zro : Infer f g

 67 |   ||| The successor constructor is inferrable

 68 |   Suc : Check f g -> Infer f g

 69 |   ||| Pi is inferrable

 70 |   Pi : (a : Check f g) -> (b : Abs Check f g) -> Infer f g

 71 |   ||| A bound variable

 72 |   Bnd : Index nm g -> Infer f g

 73 |   ||| A free variable

 74 |   Var : Level nm f -> Infer f g

 75 |   ||| The application of a function to its argument

 76 |   App : Infer f g -> Check f g -> Infer f g

 78 | export infixl 3 `App`

 80 | %name Infer e

 83 | data Check : Scoped where

 84 |   ||| Inferrable terms are trivially checkable

 85 |   Emb : Infer f g -> Check f g

 86 |   ||| A function binding its argument

 87 |   Lam : Abs Check f g -> Check f g

 89 | %name Check s, t

 94 | namespace Check

 95 |   -- here it's okay to use believe_me precisely because embedding

 96 |   -- terms in a wider LContext does not change any of their syntax

 97 |   export

 98 |   thin : (0 ext : _) -> Check f g -> Check (ext ++ f) g

 99 |   thin ext = believe_me

101 | namespace Infer

102 |   -- here it's okay to use believe_me precisely because embedding

103 |   -- terms in a wider LContext does not change any of their syntax

104 |   export

105 |   thin : (0 ext : _) -> Infer f g -> Infer (ext ++ f) g

106 |   thin ext = believe_me

108 |   -- here it's okay to use believe_me because there are no bound

109 |   -- variables

110 |   export

111 |   closed : (0 g : _) -> Infer f [<] -> Infer f g

112 |   closed g = believe_me

117 | (forall g. Eq (t f g)) => Eq (Abs t f g) where

118 |   MkAbs x@_ b == MkAbs x' b' with (decEq x x')

119 |     _ | Yes Refl = b == b'

120 |     _ | No _ = False

122 | Eq (Infer f g)

123 | Eq (Check f g)

125 | Eq (Infer f g) where

126 |   Ann t ty == Ann t' ty' = t == t' && ty == ty'

127 |   Star == Star = True

128 |   Pi a b == Pi s t = a == s && b == t

129 |   Bnd k == Bnd l = case hetEqDec k l of

130 |     Yes _ => True

131 |     _ => False

132 |   Var m == Var n = case hetEqDec m n of

133 |     Yes _ => True

134 |     _ => False

135 |   App e s == App f t = e == f && s == t

136 |   _ == _ = False

138 | Eq (Check f g) where

139 |   Emb e == Emb f = assert_total (e == f)

140 |   Lam b == Lam t = assert_total (b == t)

141 |   _ == _ = False

149 | parameters {0 x : Name}

151 |   substAbs   : {g : _} -> Infer f [<] -> Abs Check f ([<x] <+> g) -> Abs Check f g

152 |   substCheck : {g : _} -> Infer f [<] -> Check f ([<x] <+> g) -> Check f g

153 |   substInfer : {g : _} -> Infer f [<] -> Infer f ([<x] <+> g)  -> Infer f g

155 |   substCheck u (Emb t) = Emb (substInfer u t)

156 |   substCheck u (Lam b) = Lam (substAbs u b)

158 |   substInfer u (Ann s a) = Ann (substCheck u s) (substCheck u a)

159 |   substInfer u Star = Star

160 |   substInfer u Nat = Nat

161 |   substInfer u Zro = Zro

162 |   substInfer u (Suc n) = Suc (substCheck u n)

163 |   substInfer u (Rec p pz ps n)

164 |     = Rec (substCheck u p) (substCheck u pz) (substCheck u ps) (substCheck u n)

165 |   substInfer u (Pi a b) = Pi (substCheck u a) (substAbs u b)

166 |   substInfer {g} u (Bnd k) = case isLast k of

167 |     Left _ => closed g u

168 |     Right k' => Bnd k'

169 |   substInfer u (Var nm) = Var nm

170 |   substInfer u (App e s) = App (substInfer u e) (substCheck u s)

172 |   substAbs u (MkAbs y t) = MkAbs y (substCheck u t)

184 | 0 Kripke : LContext -> Type

186 | data Value : LContext -> Type

187 | data Stuck : LContext -> Type

189 | data Value : LContext -> Type where

190 |   ||| Lambda abstractions become functions in the host language

191 |   VLam  : (b : Kripke f) -> Value f

192 |   ||| The Star kind is a value already

193 |   VStar : Value f

194 |   ||| The nat type is a value already

195 |   VNat : Value f

196 |   ||| The zero constructor is a value

197 |   VZro : Value f

198 |   ||| The successor constructor is a value constructor

199 |   VSuc : Value f -> Value f

200 |   ||| Pi constructors combine a value for their domain and

202 |   VPi   : (a : Value f) -> (b : Kripke f) -> Value f

203 |   ||| Stuck computations qualify as values

204 |   VEmb  : (e : Stuck f) -> Value f

206 | data Stuck : LContext -> Type where

207 |   ||| A variable is a stuck computation

208 |   NVar : Level nm f -> Stuck f

209 |   ||| An application whose function is stuck is also stuck

210 |   NApp : Stuck f -> Value f -> Stuck f

211 |   ||| An induction principle applied to a stuck natural numnber is stuck

212 |   NRec : (pred, pz, ps : Value f) -> Stuck f -> Stuck f

214 | Kripke f = (0 ext : _) -> Value (ext ++ f) -> Value (ext ++ f)

216 | namespace Value

217 |   -- here it's okay to use believe_me precisely because embedding

218 |   -- terms in a wider LContext does not change any of their syntax

219 |   export

220 |   thin : (0 ext : _) -> Value f -> Value (ext ++ f)

221 |   thin ext = believe_me

228 | vfree : Level nm f -> Value f

229 | vfree x = VEmb (NVar x)

231 | export infixl 5 `vapp`

237 | vapp : Value f -> Value f -> Value f

238 | vapp (VLam f) t = f [] t

239 | vapp (VEmb n) t = VEmb (NApp n t)

240 | vapp _ _ = idris_crash "Oops"

243 | Env : Scoped

244 | Env f g = All (const (Value f)) g

247 | evalIndex : Index nm g -> Env f g -> Value f

248 | evalIndex i@_ env with (view i)

249 |   evalIndex i@_ (_ :< v) | Z = v

250 |   evalIndex i@_ (env :< _) | S i' = evalIndex i' env

254 | evalInfer : Infer f g -> Env f g -> Value f

258 | evalCheck : Check f g -> Env f g -> Value f

261 | evalAbs : Abs Check f g -> Env f g -> Kripke f

263 | evalInfer (Ann t _) env = evalCheck t env

264 | evalInfer Star env = VStar

265 | evalInfer Nat env = VNat

266 | evalInfer Zro env = VZro

267 | evalInfer (Suc n) env = VSuc (evalCheck n env)

268 | evalInfer (Rec p pz ps n) env = go (evalCheck pz env) (evalCheck ps env) (evalCheck n env) where

270 |   go : (pz, ps, n : Value f) -> Value f

271 |   go pz ps VZro = pz

272 |   go pz ps (VSuc n) = ps `vapp` n `vapp` (go pz ps n)

273 |   go pz ps (VEmb n) = VEmb (NRec (evalCheck p env) pz ps n)

274 |   go _ _ _ = idris_crash "Oops"

276 | evalInfer (Pi a b) env = VPi (evalCheck a env) (evalAbs b env)

277 | evalInfer (Bnd i) env = evalIndex i env

278 | evalInfer (App f t) env = vapp (evalInfer f env) (evalCheck t env)

280 | evalCheck (Emb i) env = evalInfer i env

281 | evalCheck (Lam b) env = VLam (evalAbs b env)

283 | evalAbs {f} (MkAbs x b) env

284 |   -- here it's okay to use believe_me precisely because embedding

285 |   -- terms in a wider LContext does not change any of their syntax

286 |   = \ ext, v => evalCheck {f = ext ++ f, g = g :< x} (believe_me b) (believe_me env :< v)

292 | quoteStuckI : {f : _} -> Stuck f -> Infer [] (rev f)

293 | quoteAbsI   : {f : _} -> Kripke f -> Abs Check [] (rev f)

294 | quoteValueI : {f : _} -> Value f -> Check [] (rev f)

296 | quoteStuckI (NVar v) = Bnd (asIndex v)

297 | quoteStuckI (NApp e t) = quoteStuckI e `App` quoteValueI t

298 | quoteStuckI (NRec pred pz ps e)

299 |   = Rec (quoteValueI pred) (quoteValueI pz) (quoteValueI ps) (Emb (quoteStuckI e))

301 | quoteValueI VStar = Emb Star

302 | quoteValueI VNat = Emb Nat

303 | quoteValueI VZro = Emb Zro

304 | quoteValueI (VSuc n) = Emb (Suc (quoteValueI n))

305 | quoteValueI (VPi a b)

306 |   = let a = quoteValueI a in

307 |     let b = quoteAbsI b in

308 |     Emb (Pi a b)

309 | quoteValueI (VLam f) = Lam (quoteAbsI f)

310 | quoteValueI (VEmb e) = Emb (quoteStuckI e)

312 | quoteAbsI {f} b

313 |   = let nm = fromString "x_\{show (length f)}" in

314 |     MkAbs nm (quoteValueI (b [nm] (vfree fresh)))

316 | quoteValue : {f : _} -> Value f -> Check [] (rev f)

317 | quoteValue = quoteValueI

323 | normCheck : Check [] g -> Env [] g  -> Check [] [<]

324 | normCheck t env = quoteValue (evalCheck t env)

327 | normInfer : Infer [] g -> Env [] g -> Check [] [<]

328 | normInfer t env = quoteValue (evalInfer t env)

338 | Ty : LContext -> Type

339 | Ty = Value

342 | Context : LContext -> Type

343 | Context f = All (const (Ty f)) f

345 | parameters {0 m : Type -> Type} {auto _ : MonadError String m}

347 |   levelI : {f : _} -> All (const p) f -> Level nm f -> p

348 |   levelI vs lvl with (view lvl)

349 |     levelI (v :: vs) _ | Z = v

350 |     levelI (v :: vs) _ | S lvl' = levelI vs lvl'

352 |   inferI    : {f : _} -> Context f -> Infer f [<] -> m (Ty f)

353 |   checkAbsI : {f : _} -> Context f -> Ty f -> Kripke f -> Abs Check f [<] -> m ()

354 |   checkI    : {f : _} -> Context f -> Ty f -> Check f [<] -> m ()

356 |   inferI ctx (Ann t ty) = do

357 |     checkI ctx VStar ty

358 |     let ty = assert_total (evalCheck ty [<])

359 |     ty <$ checkI ctx ty t

360 |   inferI ctx Star = pure VStar

361 |   inferI ctx Nat = pure VStar

362 |   inferI ctx Zro = pure VNat

363 |   inferI ctx (Suc n) = VNat <$ checkI ctx VNat n

364 |   inferI ctx (Rec p pz ps n) = do

365 |     -- check & evaluate the predicate

366 |     checkI ctx (VPi VNat (\ _, _ => VStar)) p

367 |     let p = assert_total (evalCheck p [<])

368 |     -- check pz has type (p 0)

369 |     checkI ctx (assert_total (p `vapp` VZro)) pz

370 |     -- check ps has type (forall n. p n -> p (1+ n))

371 |     let psTy = VPi VNat $ \ ext, n =>

372 |                VPi (thin ext p `vapp` n) $

373 |                \ ext', _ => thin ext' (thin ext p `vapp` VSuc n)

374 |     checkI ctx psTy ps

375 |     -- check & evaluate the nat

376 |     checkI ctx VNat n

377 |     let n = assert_total (evalCheck n [<])

378 |     -- return (p n)

379 |     pure (assert_total (p `vapp` n))

380 |   inferI ctx (Pi a b) = do

381 |     checkI ctx VStar a

382 |     let a = assert_total (evalCheck a [<])

383 |     VStar <$ checkAbsI ctx a (\ _, _ => VStar) b

384 |   inferI ctx (Bnd k) =

385 |     -- unhandled in the original Haskell

386 |     throwError "Oops"

387 |   inferI ctx (Var v) = pure (levelI ctx v)

388 |   inferI ctx (App f t) = do

389 |     (VPi a b) <- inferI ctx f

390 |       | _ => throwError "illegal application"

391 |     checkI ctx a t

392 |     let t = assert_total (evalCheck t [<])

393 |     pure (b [] t)

396 |   checkI ctx ty (Emb t) = do

397 |     ty' <- inferI ctx t

398 |     unless (quoteValue ty == quoteValue ty') $ throwError "type mismatch"

399 |   checkI ctx ty (Lam t) = do

400 |     let VPi a b = ty

401 |       | _ => throwError "expected a function type"

402 |     checkAbsI ctx a b t

404 |   checkAbsI {f} ctx a b (MkAbs x t) = do

405 |     let b = b [x] (vfree fresh)

406 |     -- Here we turn the most local de Bruijn index into a level

407 |     let t = substCheck (Var fresh) (thin [x] t)

408 |     checkI (thin [x] a :: believe_me ctx) b t