it works ! a lot has changed
parent
5790d22dcc
commit
40b089be6e
2
pi.ipkg
2
pi.ipkg
|
|
@ -2,11 +2,11 @@ package pi
|
|||
|
||||
modules = Term
|
||||
, Value
|
||||
, Ctx
|
||||
, Normalize
|
||||
, Convert
|
||||
, Check
|
||||
, Misc
|
||||
, Tests
|
||||
|
||||
options = "-p contrib --warnpartial"
|
||||
|
||||
|
|
|
|||
|
|
@ -0,0 +1,59 @@
|
|||
module Check
|
||||
|
||||
import Control.Monad.RWS
|
||||
import Control.Monad.Either
|
||||
import Control.Monad.Identity
|
||||
import Data.Vect
|
||||
import Data.Fin
|
||||
|
||||
import Term
|
||||
import Value
|
||||
import Normalize
|
||||
import Misc
|
||||
import Convert
|
||||
|
||||
|
||||
%default total
|
||||
|
||||
mutual
|
||||
public export
|
||||
-- terms types expected term
|
||||
check : Ctx n -> Ctx n -> Value -> Term n -> PI Bool
|
||||
check trs tys xpt' tr = do
|
||||
xpt <- whnf xpt'
|
||||
case tr of
|
||||
TLam sc => case xpt of
|
||||
VClos env (TPi a b) => do
|
||||
v <- VGen <$> fresh
|
||||
check (v :: trs) (VClos env a :: tys) (VClos (v :: env) b) sc
|
||||
_ => oops "expected pi"
|
||||
|
||||
TPi a b => case xpt of
|
||||
VType => do
|
||||
v <- VGen <$> fresh
|
||||
(&&) <$> check trs tys VType a
|
||||
<*> delay <$> check (v :: trs) (VClos trs a :: tys) VType b
|
||||
|
||||
|
||||
_ => oops "expected type"
|
||||
|
||||
_ => convert xpt =<< infer trs tys tr
|
||||
|
||||
-- terms types term
|
||||
infer : Ctx n -> Ctx n -> Term n -> PI Value
|
||||
infer trs tys (TVar i _) = pure (index (natToFinLT i) tys)
|
||||
infer trs tys TType = pure VType
|
||||
infer trs tys (TApp f x) = infer trs tys f >>= whnf >>=
|
||||
\case
|
||||
VClos env (TPi a b) => do
|
||||
if !(check trs tys (VClos env a) x)
|
||||
then pure (VClos (VClos trs x :: env) b)
|
||||
else oops "application"
|
||||
|
||||
_ => oops "expected infer pi"
|
||||
infer trs tys _ = oops "cannot infer type"
|
||||
|
||||
public export
|
||||
typecheck : Term 0 -> Term 0 -> Either String (Bool, List String)
|
||||
typecheck tr ty = resolve $ (&&) <$> check [] [] VType ty
|
||||
<*> delay <$> check [] [] (VClos [] ty) tr
|
||||
|
|
@ -0,0 +1,42 @@
|
|||
module Convert
|
||||
|
||||
import Term
|
||||
import Value
|
||||
import Misc
|
||||
import Normalize
|
||||
|
||||
import Control.Monad.RWS
|
||||
import Control.Monad.Identity
|
||||
import Control.Monad.Either
|
||||
|
||||
import Data.Nat
|
||||
import Data.Vect
|
||||
|
||||
%default total
|
||||
|
||||
public export
|
||||
convert : Value -> Value -> PI Bool
|
||||
convert u1 u2 = do
|
||||
u1' <- whnf u1
|
||||
u2' <- whnf u2
|
||||
logS ("checking equality of terms '" ++ show u1 ++ "' and '" ++ show u2 ++ "'.")
|
||||
logS ("with value representations '" ++ show u1' ++ "' and '" ++ show u2' ++ "'.")
|
||||
assert_total $ -- :(
|
||||
case (u1', u2') of
|
||||
(VType, VType) => pure True
|
||||
(VApp f1 x1, VApp f2 x2) => (&&) <$> convert f1 f2
|
||||
<*> delay <$> convert x1 x2
|
||||
(VGen k1, VGen k2) => pure (k1 == k2)
|
||||
|
||||
(VClos env1 (TLam sc1), VClos env2 (TLam sc2)) => do
|
||||
v <- VGen <$> fresh
|
||||
convert (VClos (v :: env1) sc1)
|
||||
(VClos (v :: env2) sc2)
|
||||
|
||||
(VClos env1 (TPi a1 b1), VClos env2 (TPi a2 b2)) => do
|
||||
v <- VGen <$> fresh
|
||||
(&&) <$> convert (VClos env1 a1)
|
||||
(VClos env2 a2)
|
||||
<*> delay <$> convert (VClos (v :: env1) b1)
|
||||
(VClos (v :: env2) b2)
|
||||
_ => pure False
|
||||
40
src/Ctx.idr
40
src/Ctx.idr
|
|
@ -1,40 +0,0 @@
|
|||
module Ctx
|
||||
|
||||
import Misc
|
||||
|
||||
import Data.Nat
|
||||
|
||||
%default total
|
||||
|
||||
infixr 7 ::
|
||||
|
||||
public export
|
||||
data Ctx : (Index -> Type) -> Index -> Type where
|
||||
Nil : Ctx ty 0
|
||||
(::) : {n : _} -> ty n -> Ctx ty n -> Ctx ty (S n)
|
||||
|
||||
-- indexed by amount of free variables
|
||||
public export
|
||||
data Closure : (Index -> Type) -> Index -> Type where
|
||||
MkClosure : {n : _} -> Ctx ty n -> ty (m + n) -> Closure ty m
|
||||
|
||||
public export
|
||||
enclose : {n : _} -> ty n -> Closure ty n
|
||||
enclose {n = n} ty = MkClosure Nil (rewrite plusZeroRightNeutral n in ty)
|
||||
|
||||
public export
|
||||
lookup : {m : _} -> (n : Nat) -> Ctx ty m -> LT n m -> ty (minus m (S n))
|
||||
lookup {m = S m} Z (x :: _) _ = rewrite minusZeroRight m in x
|
||||
lookup (S n) (_ :: ctx) (LTESucc p) = lookup n ctx p
|
||||
|
||||
public export
|
||||
strengthen : Ctx ty (S n) -> Ctx ty n
|
||||
strengthen (_ :: ctx) = ctx
|
||||
|
||||
public export
|
||||
strengthenTo : {n,m : _} -> Ctx ty m -> LTE n m -> Ctx ty n
|
||||
strengthenTo {n = Z} _ _ = Nil
|
||||
strengthenTo (x :: ctx) (LTESucc p)
|
||||
= case lteSplit p of
|
||||
Left Refl => x :: ctx
|
||||
Right p2 => strengthenTo ctx p2
|
||||
25
src/Misc.idr
25
src/Misc.idr
|
|
@ -1,5 +1,9 @@
|
|||
module Misc
|
||||
|
||||
import Control.Monad.RWS
|
||||
import Control.Monad.Identity
|
||||
import Control.Monad.Either
|
||||
|
||||
import Data.Nat
|
||||
|
||||
%default total
|
||||
|
|
@ -14,11 +18,28 @@ Name = String
|
|||
|
||||
public export
|
||||
PI : Type -> Type
|
||||
PI = Either String
|
||||
PI = EitherT String (RWS () (List String) Nat)
|
||||
|
||||
public export
|
||||
resolve : PI a -> Either String (a, List String)
|
||||
resolve a = case runRWS (runEitherT a) () 0 of
|
||||
(Left e, _) => Left e
|
||||
(Right r, _, s) => Right (r, s)
|
||||
|
||||
public export
|
||||
oops : String -> PI a
|
||||
oops = Left
|
||||
oops = left
|
||||
|
||||
public export
|
||||
fresh : PI Nat
|
||||
fresh = do
|
||||
i <- get
|
||||
put (S i)
|
||||
pure i
|
||||
|
||||
public export
|
||||
logS : String -> PI ()
|
||||
logS = tell . (:: [])
|
||||
|
||||
public export
|
||||
lteTransp : LTE a b -> a = c -> b = d -> LTE c d
|
||||
|
|
|
|||
|
|
@ -2,54 +2,38 @@ module Normalize
|
|||
|
||||
import Term
|
||||
import Value
|
||||
import Ctx
|
||||
import Misc
|
||||
|
||||
import Control.Monad.RWS
|
||||
import Control.Monad.Identity
|
||||
import Control.Monad.Either
|
||||
|
||||
import Data.Nat
|
||||
import Data.Vect
|
||||
|
||||
%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
|
||||
app : Value -> Value -> PI Value
|
||||
app (VClos env (TLam sc)) x = eval (x :: env) sc
|
||||
app f x = pure (VApp f x)
|
||||
|
||||
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
|
||||
eval : Ctx n -> Term n -> PI Value
|
||||
eval env (TVar i _) = pure (index (natToFinLT i) env)
|
||||
eval env (TApp f x) = do
|
||||
f' <- eval env f
|
||||
x' <- eval env x
|
||||
assert_total (app f' x') -- :(
|
||||
eval env TType = pure VType
|
||||
eval env tr = pure (VClos env tr)
|
||||
|
||||
public export
|
||||
fromTerm : Term 0 -> Glue
|
||||
fromTerm term = MkGlue term (eval [] Nil)
|
||||
whnf : Value -> PI Value
|
||||
whnf (VApp f x) = do
|
||||
f' <- whnf f
|
||||
x' <- whnf x
|
||||
app f' x'
|
||||
whnf (VClos env tr) = eval env tr
|
||||
whnf v = pure v
|
||||
|
|
|
|||
34
src/Term.idr
34
src/Term.idr
|
|
@ -12,17 +12,25 @@ import Misc
|
|||
-}
|
||||
public export
|
||||
data Term : (_ : Index) -> Type where
|
||||
TType : Term n -- Type of types
|
||||
TLam : Term n -> Term (S n) -> Term n -- Lambda abstraction (λ Type -> Scope)
|
||||
TPi : Term n -> Term (S n) -> Term n -- Pi type (∏ A -> B a )
|
||||
TApp : Term n -> Term n -> Term n -- Appliction
|
||||
TVar : (n : Nat) -> LT n m -> Term m -- Variable
|
||||
TType : Term n -- Type of types
|
||||
TLam : Term (S n) -> Term n -- Lambda abstraction (λ _ . Scope)
|
||||
TPi : Term n -> Term (S n) -> Term n -- Pi type (∏ _ : A . B _ )
|
||||
TApp : Term n -> Term n -> Term n -- Appliction
|
||||
TVar : (n : Nat) -> LT n m -> Term m -- Variable
|
||||
|
||||
public export
|
||||
Show (Term n) where
|
||||
show TType = "TType"
|
||||
show (TLam sc) = "TLam (" ++ show sc ++ ")"
|
||||
show (TPi ty sc) = "TPi (" ++ show ty ++ ") (" ++ show sc ++ ")"
|
||||
show (TApp f x) = "TApp (" ++ show f ++ ") (" ++ show x ++ ")"
|
||||
show (TVar i _) = "TVar " ++ show i
|
||||
|
||||
public export
|
||||
weaken : {p, q : _} -> LTE p q -> Term p -> Term q
|
||||
weaken _ TType = TType
|
||||
weaken p (TLam ty sc) = TLam (weaken p ty) (weaken (LTESucc p) sc)
|
||||
weaken p (TPi a bx) = TLam (weaken p a) (weaken (LTESucc p) bx)
|
||||
weaken p (TLam sc) = TLam (weaken (LTESucc p) sc)
|
||||
weaken p (TPi a bx) = TPi (weaken p a) (weaken (LTESucc p) bx)
|
||||
weaken p (TApp f x) = TApp (weaken p f) (weaken p x)
|
||||
{-
|
||||
Getting new index
|
||||
|
|
@ -50,11 +58,11 @@ weaken p (TApp f x) = TApp (weaken p f) (weaken p x)
|
|||
(r + q) - p < q ∎
|
||||
|
||||
-}
|
||||
weaken {p = S p} {q = S q} (LTESucc p1) (TVar r p2') =
|
||||
weaken {p = S p} {q = S q} (LTESucc p1) (TVar r p2' ) =
|
||||
case p2' of
|
||||
LTESucc p2 => TVar (minus (r + q) p)
|
||||
(LTESucc (lteTransp (minusLteMonotone (plusLteMonotoneRight q r p p2)) Refl (minusPlus p)))
|
||||
LTESucc p2 => TVar (minus (r + q) p)
|
||||
(LTESucc (lteTransp (minusLteMonotone (plusLteMonotoneRight q r p p2)) Refl (minusPlus p)))
|
||||
|
||||
|
||||
public export
|
||||
weaken0 : {n : _} -> Term 0 -> Term n
|
||||
weaken0 = weaken LTEZero
|
||||
weaken1 : {n : _} -> Term n -> Term (S n)
|
||||
weaken1 = weaken lteS
|
||||
|
|
|
|||
|
|
@ -0,0 +1,23 @@
|
|||
module Tests
|
||||
|
||||
import Term
|
||||
import Check
|
||||
import Check
|
||||
|
||||
import Data.Nat
|
||||
|
||||
%default total
|
||||
|
||||
a : {p, q : Nat} -> lt p q = True -> LT p q
|
||||
a {p} {q} eq = ltReflectsLT p q eq
|
||||
|
||||
test1 : Either String (Bool, List String)
|
||||
test1 = typecheck (TLam (TLam (TVar 0 (a Refl))))
|
||||
(TPi TType (TPi (TVar 0 (a Refl)) (TVar 1 (a Refl))))
|
||||
|
||||
test2 : Either String (Bool, List String)
|
||||
test2 = typecheck (TLam (TLam (TLam (TLam (TApp (TVar 1 (a Refl)) (TVar 0 (a Refl)))))))
|
||||
(TPi TType
|
||||
(TPi (TPi (TVar 0 (a Refl)) TType)
|
||||
(TPi (TPi (TVar 1 (a Refl)) (TApp (TVar 1 (a Refl)) (TVar 0 (a Refl))))
|
||||
(TPi (TVar 2 (a Refl)) (TApp (TVar 2 (a Refl)) (TVar 0 (a Refl)))))))
|
||||
|
|
@ -2,24 +2,26 @@ module Value
|
|||
|
||||
import Term
|
||||
import Misc
|
||||
import Ctx
|
||||
|
||||
import Data.Vect
|
||||
|
||||
%default total
|
||||
|
||||
public export
|
||||
data NF : Type where
|
||||
NType : NF -- Type of types
|
||||
NLam : NF -> Term 1 -> NF -- Lambda abstraction
|
||||
NPi : NF -> Term 1 -> NF -- Pi Type
|
||||
mutual
|
||||
public export
|
||||
data Value : Type where
|
||||
VType : Value
|
||||
VGen : Nat -> Value
|
||||
VApp : Value -> Value -> Value
|
||||
VClos : Ctx n -> Term n -> Value
|
||||
|
||||
public export
|
||||
Ctx : Index -> Type
|
||||
Ctx i = Vect i Value
|
||||
|
||||
public export
|
||||
data Glue : Type where
|
||||
MkGlue : Term 0 -> (Term 0 -> PI NF) -> Glue
|
||||
|
||||
public export
|
||||
getTerm : Glue -> Term 0
|
||||
getTerm (MkGlue term _) = term
|
||||
|
||||
public export
|
||||
getNF : Glue -> PI NF
|
||||
getNF (MkGlue term f) = f term
|
||||
Show Value where
|
||||
show VType = "VType"
|
||||
show (VGen i) = "VGen " ++ show i
|
||||
show (VApp f x) = "VApp (" ++ show f ++ ") (" ++ show x ++ ")"
|
||||
show (VClos e t) = "VClos (" ++ assert_total (show e) ++ ") (" ++ show t ++ ")"
|
||||
|
|
|
|||
Loading…
Reference in New Issue