56 lines
1.8 KiB
Idris
56 lines
1.8 KiB
Idris
module Normalize
|
|
|
|
import Term
|
|
import Value
|
|
import Ctx
|
|
import Misc
|
|
|
|
import Data.Nat
|
|
|
|
%default total
|
|
|
|
-- There is some nasty assert_total here since I cannot solve the halting problem
|
|
|
|
public export
|
|
asTerm : NF -> Term 0
|
|
asTerm NType = TType
|
|
asTerm (NLam ty sc) = TLam (asTerm ty) sc
|
|
asTerm (NPi ty sc) = TPi (asTerm ty) sc
|
|
|
|
public export
|
|
fromNF : NF -> Glue
|
|
fromNF nf = MkGlue (asTerm nf) (const (pure nf))
|
|
|
|
substStep : {n,m : _} -> Term m -> LTE m n -> Term (S n) -> Term n
|
|
substStep {m = m} tr p tr' = case tr' of -- case somehow needed for idris not to loop over metavariable
|
|
TType => TType
|
|
(TLam ty sc) => TLam (substStep tr p ty) (substStep tr (lteSuccRight p) sc)
|
|
(TPi ty sc) => TPi (substStep tr p ty) (substStep tr (lteSuccRight p) sc)
|
|
(TApp f x) => TApp (substStep tr p f) (substStep tr p x)
|
|
(TVar i p) => case natEqDecid m i of
|
|
Left p => ?que1
|
|
Right p => ?que2
|
|
|
|
mutual
|
|
evalClosure : {n : Nat} -> Closure Term 0 -> PI (Term n)
|
|
evalClosure (MkClosure ctx term) = eval [] ctx term >>= pure . weaken0 . asTerm
|
|
|
|
public export
|
|
eval : {n : Nat} -> List (Closure Term 0) -> Ctx Term n -> Term n -> PI NF
|
|
eval stack env TType = pure NType
|
|
|
|
-- dirty
|
|
eval (thunk :: stack) env (TLam _ sc) = eval stack (!(assert_total (evalClosure thunk)) :: env) sc
|
|
|
|
eval stack env (TApp f x) = eval (MkClosure env x :: stack) env x
|
|
|
|
eval stack env (TVar m p) = assert_total $ eval stack (strengthenTo env minusLte) (lookup m env p)
|
|
|
|
eval stack env (TPi ty sc) = ?idk
|
|
|
|
eval [] env (TLam ty sc) = ?what
|
|
|
|
public export
|
|
fromTerm : Term 0 -> Glue
|
|
fromTerm term = MkGlue term (eval [] Nil)
|