parameterise over qty semiring
This commit is contained in:
parent
961c8415b5
commit
c45a963ba0
16 changed files with 712 additions and 491 deletions
|
|
@ -5,6 +5,7 @@ import public Quox.Syntax
|
|||
import public Quox.Equal
|
||||
import public Quox.Pretty
|
||||
import public Quox.Typechecker
|
||||
import public Quox.Syntax.Qty.Three
|
||||
|
||||
import Data.Nat
|
||||
import Data.Vect
|
||||
|
|
@ -53,7 +54,7 @@ banner : PrettyOpts -> String
|
|||
banner opts = unlines $ zipWith (join1 opts) (qtuwu opts) (text opts)
|
||||
|
||||
export
|
||||
tm : Term 1 2
|
||||
tm : Term Three 1 2
|
||||
tm =
|
||||
(Pi One "a" (BVT 0) (TUsed $ E (F "F" :@@ [BVT 0, FT "w"]))
|
||||
`DCloT` (K One ::: id))
|
||||
|
|
|
|||
|
|
@ -2,49 +2,66 @@ module Quox.Definition
|
|||
|
||||
import public Quox.Syntax
|
||||
import public Data.SortedMap
|
||||
import public Control.Monad.State
|
||||
import public Control.Monad.Reader
|
||||
import Decidable.Decidable
|
||||
|
||||
|
||||
public export
|
||||
record AnyTerm where
|
||||
record AnyTerm q where
|
||||
constructor T
|
||||
get : forall d, n. Term d n
|
||||
get : forall d, n. Term q d n
|
||||
|
||||
public export
|
||||
record Definition where
|
||||
record Definition' q (isGlobal : q -> Type) where
|
||||
constructor MkDef'
|
||||
qty : Qty
|
||||
type : AnyTerm
|
||||
term : Maybe AnyTerm
|
||||
{auto 0 qtyGlobal : IsGlobal qty}
|
||||
qty : q
|
||||
type : AnyTerm q
|
||||
term : Maybe $ AnyTerm q
|
||||
{auto 0 qtyGlobal : isGlobal qty}
|
||||
|
||||
public export
|
||||
0 Definition : (q : Type) -> IsQty q => Type
|
||||
Definition q = Definition' q IsGlobal
|
||||
|
||||
public export %inline
|
||||
mkDef : (qty : Qty) -> (0 _ : IsGlobal qty) =>
|
||||
(type, term : forall d, n. Term d n) -> Definition
|
||||
mkDef : IsQty q => (qty : q) -> (0 _ : IsGlobal qty) =>
|
||||
(type, term : forall d, n. Term q d n) -> Definition q
|
||||
mkDef qty type term = MkDef' {qty, type = T type, term = Just (T term)}
|
||||
|
||||
public export %inline
|
||||
mkAbstract : (qty : Qty) -> (0 _ : IsGlobal qty) =>
|
||||
(type : forall d, n. Term d n) -> Definition
|
||||
mkAbstract : IsQty q => (qty : q) -> (0 _ : IsGlobal qty) =>
|
||||
(type : forall d, n. Term q d n) -> Definition q
|
||||
mkAbstract qty type = MkDef' {qty, type = T type, term = Nothing}
|
||||
|
||||
|
||||
public export %inline
|
||||
(.type0) : Definition -> Term 0 0
|
||||
(.type0) : Definition' q _ -> Term q 0 0
|
||||
g.type0 = g.type.get
|
||||
|
||||
public export %inline
|
||||
(.term0) : Definition -> Maybe (Term 0 0)
|
||||
(.term0) : Definition' q _ -> Maybe (Term q 0 0)
|
||||
g.term0 = map (\t => t.get) g.term
|
||||
|
||||
public export %inline
|
||||
(.qtyP) : Definition -> Subset Qty IsGlobal
|
||||
(.qtyP) : forall q, isGlobal. Definition' q isGlobal -> Subset q isGlobal
|
||||
g.qtyP = Element g.qty g.qtyGlobal
|
||||
|
||||
public export %inline
|
||||
isZero : Definition -> Bool
|
||||
isZero g = g.qty == Zero
|
||||
isZero : IsQty q => Definition q -> Bool
|
||||
isZero g = isYes $ isZero g.qty
|
||||
|
||||
public export
|
||||
Definitions : Type
|
||||
Definitions = SortedMap Name Definition
|
||||
0 Definitions' : (q : Type) -> (q -> Type) -> Type
|
||||
Definitions' q isGlobal = SortedMap Name $ Definition' q isGlobal
|
||||
|
||||
public export
|
||||
0 Definitions : (q : Type) -> IsQty q => Type
|
||||
Definitions q = Definitions' q IsGlobal
|
||||
|
||||
|
||||
public export
|
||||
0 HasDefs' : (q : Type) -> (q -> Type) -> (Type -> Type) -> Type
|
||||
HasDefs' q isGlobal = MonadReader (Definitions' q isGlobal)
|
||||
|
||||
0 HasDefs : (q : Type) -> IsQty q => (Type -> Type) -> Type
|
||||
HasDefs q = HasDefs' q IsGlobal
|
||||
|
|
|
|||
|
|
@ -9,194 +9,228 @@ import Data.Maybe
|
|||
|
||||
|
||||
private %inline
|
||||
ClashE : EqMode -> Elim d n -> Elim d n -> Error
|
||||
ClashE : EqMode -> Elim q d n -> Elim q d n -> Error q
|
||||
ClashE mode = ClashT mode `on` E
|
||||
|
||||
|
||||
public export
|
||||
record Env where
|
||||
record Env' q (isGlobal : q -> Type) where
|
||||
constructor MakeEnv
|
||||
defs : Definitions
|
||||
defs : Definitions' q isGlobal
|
||||
mode : EqMode
|
||||
|
||||
public export
|
||||
0 Env : (q : Type) -> IsQty q => Type
|
||||
Env q = Env' q IsGlobal
|
||||
|
||||
parameters {auto _ : MonadError Error m} {auto _ : MonadReader Env m}
|
||||
private %inline
|
||||
mode : m EqMode
|
||||
mode = asks mode
|
||||
public export
|
||||
0 HasEnv' : (q : Type) -> (q -> Type) -> (Type -> Type) -> Type
|
||||
HasEnv' q isGlobal = MonadReader (Env' q isGlobal)
|
||||
|
||||
private %inline
|
||||
clashT : Term d n -> Term d n -> m a
|
||||
clashT s t = throwError $ ClashT !mode s t
|
||||
|
||||
private %inline
|
||||
clashE : Elim d n -> Elim d n -> m a
|
||||
clashE e f = throwError $ ClashE !mode e f
|
||||
|
||||
private %inline
|
||||
defE : Name -> m (Maybe (Elim d n))
|
||||
defE x = asks $ \env => do
|
||||
g <- lookup x env.defs
|
||||
pure $ (!g.term).get :# g.type.get
|
||||
|
||||
private %inline
|
||||
defT : Name -> m (Maybe (Term d n))
|
||||
defT x = map E <$> defE x
|
||||
|
||||
export %inline
|
||||
compareU' : Universe -> Universe -> m Bool
|
||||
compareU' i j = pure $
|
||||
case !mode of Equal => i == j; Sub => i <= j
|
||||
|
||||
export %inline
|
||||
compareU : Universe -> Universe -> m ()
|
||||
compareU k l = unless !(compareU' k l) $
|
||||
throwError $ ClashU !mode k l
|
||||
|
||||
mutual
|
||||
private covering
|
||||
compareTN' : (s, t : Term 0 n) ->
|
||||
(0 _ : NotRedexT s) -> (0 _ : NotRedexT t) -> m ()
|
||||
|
||||
compareTN' (E e) (E f) ps pt = compareE0 e f
|
||||
-- if either term is a def, try to unfold it
|
||||
compareTN' s@(E (F x)) t ps pt = do
|
||||
Just s' <- defT x | Nothing => clashT s t
|
||||
compareT0 s' t
|
||||
compareTN' s t@(E (F y)) ps pt = do
|
||||
Just t' <- defT y | Nothing => clashT s t
|
||||
compareT0 s t'
|
||||
compareTN' s@(E _) t _ _ = clashT s t
|
||||
|
||||
compareTN' (TYPE k) (TYPE l) _ _ = compareU k l
|
||||
compareTN' s@(TYPE _) t _ _ = clashT s t
|
||||
|
||||
compareTN' (Pi qty1 _ arg1 res1) (Pi qty2 _ arg2 res2) _ _ = do
|
||||
unless (qty1 == qty2) $ throwError $ ClashQ qty1 qty2
|
||||
compareT0 arg2 arg1 -- reversed for contravariant domain
|
||||
compareTS0 res1 res2
|
||||
compareTN' s@(Pi {}) t _ _ = clashT s t
|
||||
|
||||
-- [todo] eta
|
||||
compareTN' (Lam _ body1) (Lam _ body2) _ _ =
|
||||
local {mode := Equal} $ compareTS0 body1 body2
|
||||
compareTN' s@(Lam {}) t _ _ = clashT s t
|
||||
|
||||
compareTN' (CloT {}) _ ps _ = void $ ps IsCloT
|
||||
compareTN' (DCloT {}) _ ps _ = void $ ps IsDCloT
|
||||
|
||||
private covering
|
||||
compareEN' : (e, f : Elim 0 n) ->
|
||||
(0 _ : NotRedexE e) -> (0 _ : NotRedexE f) -> m ()
|
||||
|
||||
compareEN' e@(F x) f@(F y) _ _ =
|
||||
if x == y then pure () else
|
||||
case (!(defE x), !(defE y)) of
|
||||
(Nothing, Nothing) => clashE e f
|
||||
(s', t') => compareE0 (fromMaybe e s') (fromMaybe f t')
|
||||
compareEN' e@(F x) f _ _ = do
|
||||
Just e' <- defE x | Nothing => clashE e f
|
||||
compareE0 e' f
|
||||
compareEN' e f@(F y) _ _ = do
|
||||
Just f' <- defE y | Nothing => clashE e f
|
||||
compareE0 e f'
|
||||
|
||||
compareEN' e@(B i) f@(B j) _ _ =
|
||||
unless (i == j) $ clashE e f
|
||||
compareEN' e@(B _) f _ _ = clashE e f
|
||||
|
||||
-- [todo] tracking variance of functions? maybe???
|
||||
-- probably not
|
||||
compareEN' (fun1 :@ arg1) (fun2 :@ arg2) _ _ =
|
||||
local {mode := Equal} $ do
|
||||
compareE0 fun1 fun2
|
||||
compareT0 arg1 arg2
|
||||
compareEN' e@(_ :@ _) f _ _ = clashE e f
|
||||
|
||||
-- [todo] is always checking the types are equal correct?
|
||||
compareEN' (tm1 :# ty1) (tm2 :# ty2) _ _ = do
|
||||
compareT0 tm1 tm2
|
||||
local {mode := Equal} $ compareT0 ty1 ty2
|
||||
compareEN' e@(_ :# _) f _ _ = clashE e f
|
||||
|
||||
compareEN' (CloE {}) _ pe _ = void $ pe IsCloE
|
||||
compareEN' (DCloE {}) _ pe _ = void $ pe IsDCloE
|
||||
public export
|
||||
0 HasEnv : (q : Type) -> IsQty q => (Type -> Type) -> Type
|
||||
HasEnv q = HasEnv' q IsGlobal
|
||||
|
||||
|
||||
private covering %inline
|
||||
compareTN : NonRedexTerm 0 n -> NonRedexTerm 0 n -> m ()
|
||||
compareTN s t = compareTN' s.fst t.fst s.snd t.snd
|
||||
public export
|
||||
0 CanEqual' : (q : Type) -> (q -> Type) -> (Type -> Type) -> Type
|
||||
CanEqual' q isGlobal m = (HasErr q m, HasEnv' q isGlobal m)
|
||||
|
||||
private covering %inline
|
||||
compareEN : NonRedexElim 0 n -> NonRedexElim 0 n -> m ()
|
||||
compareEN e f = compareEN' e.fst f.fst e.snd f.snd
|
||||
public export
|
||||
0 CanEqual : (q : Type) -> IsQty q => (Type -> Type) -> Type
|
||||
CanEqual q = CanEqual' q IsGlobal
|
||||
|
||||
|
||||
export covering %inline
|
||||
compareT : DimEq d -> Term d n -> Term d n -> m ()
|
||||
compareT eqs s t =
|
||||
for_ (splits eqs) $ \th => compareT0 (s /// th) (t /// th)
|
||||
|
||||
export covering %inline
|
||||
compareE : DimEq d -> Elim d n -> Elim d n -> m ()
|
||||
compareE eqs e f =
|
||||
for_ (splits eqs) $ \th => compareE0 (e /// th) (f /// th)
|
||||
private %inline
|
||||
mode : HasEnv' _ _ m => m EqMode
|
||||
mode = asks mode
|
||||
|
||||
private %inline
|
||||
clashT : CanEqual' q _ m => Term q d n -> Term q d n -> m a
|
||||
clashT s t = throwError $ ClashT !mode s t
|
||||
|
||||
private %inline
|
||||
clashE : CanEqual' q _ m => Elim q d n -> Elim q d n -> m a
|
||||
clashE e f = throwError $ ClashE !mode e f
|
||||
|
||||
private %inline
|
||||
defE : HasEnv' q _ m => Name -> m (Maybe (Elim q d n))
|
||||
defE x = asks $ \env => do
|
||||
g <- lookup x env.defs
|
||||
pure $ (!g.term).get :# g.type.get
|
||||
|
||||
private %inline
|
||||
defT : HasEnv' q _ m => Name -> m (Maybe (Term q d n))
|
||||
defT x = map E <$> defE x
|
||||
|
||||
export %inline
|
||||
compareU' : HasEnv' q _ m => Universe -> Universe -> m Bool
|
||||
compareU' i j = pure $
|
||||
case !mode of Equal => i == j; Sub => i <= j
|
||||
|
||||
export %inline
|
||||
compareU : CanEqual' q _ m => Universe -> Universe -> m ()
|
||||
compareU k l = unless !(compareU' k l) $
|
||||
throwError $ ClashU !mode k l
|
||||
|
||||
mutual
|
||||
private covering
|
||||
compareTN' : CanEqual' q _ m => Eq q =>
|
||||
(s, t : Term q 0 n) ->
|
||||
(0 _ : NotRedexT s) -> (0 _ : NotRedexT t) -> m ()
|
||||
|
||||
compareTN' (E e) (E f) ps pt = compareE0 e f
|
||||
-- if either term is a def, try to unfold it
|
||||
compareTN' s@(E (F x)) t ps pt = do
|
||||
Just s' <- defT x | Nothing => clashT s t
|
||||
compareT0 s' t
|
||||
compareTN' s t@(E (F y)) ps pt = do
|
||||
Just t' <- defT y | Nothing => clashT s t
|
||||
compareT0 s t'
|
||||
compareTN' s@(E _) t _ _ = clashT s t
|
||||
|
||||
compareTN' (TYPE k) (TYPE l) _ _ = compareU k l
|
||||
compareTN' s@(TYPE _) t _ _ = clashT s t
|
||||
|
||||
compareTN' (Pi qty1 _ arg1 res1) (Pi qty2 _ arg2 res2) _ _ = do
|
||||
unless (qty1 == qty2) $ throwError $ ClashQ qty1 qty2
|
||||
compareT0 arg2 arg1 -- reversed for contravariant domain
|
||||
compareTS0 res1 res2
|
||||
compareTN' s@(Pi {}) t _ _ = clashT s t
|
||||
|
||||
-- [todo] eta
|
||||
compareTN' (Lam _ body1) (Lam _ body2) _ _ =
|
||||
local {mode := Equal} $ compareTS0 body1 body2
|
||||
compareTN' s@(Lam {}) t _ _ = clashT s t
|
||||
|
||||
compareTN' (CloT {}) _ ps _ = void $ ps IsCloT
|
||||
compareTN' (DCloT {}) _ ps _ = void $ ps IsDCloT
|
||||
|
||||
private covering
|
||||
compareEN' : CanEqual' q _ m => Eq q =>
|
||||
(e, f : Elim q 0 n) ->
|
||||
(0 _ : NotRedexE e) -> (0 _ : NotRedexE f) -> m ()
|
||||
|
||||
compareEN' e@(F x) f@(F y) _ _ =
|
||||
if x == y then pure () else
|
||||
case (!(defE x), !(defE y)) of
|
||||
(Nothing, Nothing) => clashE e f
|
||||
(s', t') => compareE0 (fromMaybe e s') (fromMaybe f t')
|
||||
compareEN' e@(F x) f _ _ = do
|
||||
Just e' <- defE x | Nothing => clashE e f
|
||||
compareE0 e' f
|
||||
compareEN' e f@(F y) _ _ = do
|
||||
Just f' <- defE y | Nothing => clashE e f
|
||||
compareE0 e f'
|
||||
|
||||
compareEN' e@(B i) f@(B j) _ _ =
|
||||
unless (i == j) $ clashE e f
|
||||
compareEN' e@(B _) f _ _ = clashE e f
|
||||
|
||||
-- [todo] tracking variance of functions? maybe???
|
||||
-- probably not
|
||||
compareEN' (fun1 :@ arg1) (fun2 :@ arg2) _ _ =
|
||||
local {mode := Equal} $ do
|
||||
compareE0 fun1 fun2
|
||||
compareT0 arg1 arg2
|
||||
compareEN' e@(_ :@ _) f _ _ = clashE e f
|
||||
|
||||
-- [todo] is always checking the types are equal correct?
|
||||
compareEN' (tm1 :# ty1) (tm2 :# ty2) _ _ = do
|
||||
compareT0 tm1 tm2
|
||||
local {mode := Equal} $ compareT0 ty1 ty2
|
||||
compareEN' e@(_ :# _) f _ _ = clashE e f
|
||||
|
||||
compareEN' (CloE {}) _ pe _ = void $ pe IsCloE
|
||||
compareEN' (DCloE {}) _ pe _ = void $ pe IsDCloE
|
||||
|
||||
|
||||
export covering %inline
|
||||
compareT0 : Term 0 n -> Term 0 n -> m ()
|
||||
compareT0 s t = compareTN (whnfT s) (whnfT t)
|
||||
private covering %inline
|
||||
compareTN : CanEqual' q _ m => Eq q =>
|
||||
NonRedexTerm q 0 n -> NonRedexTerm q 0 n -> m ()
|
||||
compareTN s t = compareTN' s.fst t.fst s.snd t.snd
|
||||
|
||||
export covering %inline
|
||||
compareE0 : Elim 0 n -> Elim 0 n -> m ()
|
||||
compareE0 e f = compareEN (whnfE e) (whnfE f)
|
||||
|
||||
export covering %inline
|
||||
compareTS0 : ScopeTerm 0 n -> ScopeTerm 0 n -> m ()
|
||||
compareTS0 (TUnused body1) (TUnused body2) =
|
||||
compareT0 body1 body2
|
||||
compareTS0 body1 body2 =
|
||||
compareT0 (fromScopeTerm body1) (fromScopeTerm body2)
|
||||
|
||||
|
||||
parameters {auto _ : MonadError Error m} {auto _ : MonadReader Definitions m}
|
||||
private %inline
|
||||
into : EqMode ->
|
||||
(forall n. MonadError Error n => MonadReader Env n =>
|
||||
DimEq d -> a -> a -> n ()) ->
|
||||
DimEq d -> a -> a -> m ()
|
||||
into mode f eqs a b =
|
||||
runReaderT {m} (MakeEnv {mode, defs = !ask}) $ f eqs a b
|
||||
|
||||
export covering %inline
|
||||
equalTWith : DimEq d -> Term d n -> Term d n -> m ()
|
||||
equalTWith = into Equal compareT
|
||||
|
||||
export covering %inline
|
||||
equalEWith : DimEq d -> Elim d n -> Elim d n -> m ()
|
||||
equalEWith = into Equal compareE
|
||||
|
||||
export covering %inline
|
||||
subTWith : DimEq d -> Term d n -> Term d n -> m ()
|
||||
subTWith = into Sub compareT
|
||||
|
||||
export covering %inline
|
||||
subEWith : DimEq d -> Elim d n -> Elim d n -> m ()
|
||||
subEWith = into Sub compareE
|
||||
private covering %inline
|
||||
compareEN : CanEqual' q _ m => Eq q =>
|
||||
NonRedexElim q 0 n -> NonRedexElim q 0 n -> m ()
|
||||
compareEN e f = compareEN' e.fst f.fst e.snd f.snd
|
||||
|
||||
|
||||
export covering %inline
|
||||
equalT : {d : Nat} -> Term d n -> Term d n -> m ()
|
||||
equalT = equalTWith DimEq.new
|
||||
compareT : CanEqual' q _ m => Eq q =>
|
||||
DimEq d -> Term q d n -> Term q d n -> m ()
|
||||
compareT eqs s t =
|
||||
for_ (splits eqs) $ \th => compareT0 (s /// th) (t /// th)
|
||||
|
||||
export covering %inline
|
||||
equalE : {d : Nat} -> Elim d n -> Elim d n -> m ()
|
||||
equalE = equalEWith DimEq.new
|
||||
compareE : CanEqual' q _ m => Eq q =>
|
||||
DimEq d -> Elim q d n -> Elim q d n -> m ()
|
||||
compareE eqs e f =
|
||||
for_ (splits eqs) $ \th => compareE0 (e /// th) (f /// th)
|
||||
|
||||
|
||||
export covering %inline
|
||||
subT : {d : Nat} -> Term d n -> Term d n -> m ()
|
||||
subT = subTWith DimEq.new
|
||||
compareT0 : CanEqual' q _ m => Eq q => Term q 0 n -> Term q 0 n -> m ()
|
||||
compareT0 s t = compareTN (whnfT s) (whnfT t)
|
||||
|
||||
export covering %inline
|
||||
subE : {d : Nat} -> Elim d n -> Elim d n -> m ()
|
||||
subE = subEWith DimEq.new
|
||||
compareE0 : CanEqual' q _ m => Eq q => Elim q 0 n -> Elim q 0 n -> m ()
|
||||
compareE0 e f = compareEN (whnfE e) (whnfE f)
|
||||
|
||||
export covering %inline
|
||||
compareTS0 : CanEqual' q _ m => Eq q =>
|
||||
ScopeTerm q 0 n -> ScopeTerm q 0 n -> m ()
|
||||
compareTS0 (TUnused body1) (TUnused body2) =
|
||||
compareT0 body1 body2
|
||||
compareTS0 body1 body2 =
|
||||
compareT0 (fromScopeTerm body1) (fromScopeTerm body2)
|
||||
|
||||
|
||||
private %inline
|
||||
into : HasErr q m => HasDefs' q isg m => Eq q =>
|
||||
(forall n. HasErr q n => HasEnv' q isg n => d -> a -> a -> n ()) ->
|
||||
EqMode -> d -> a -> a -> m ()
|
||||
into f mode eqs a b =
|
||||
runReaderT {m} (MakeEnv {mode, defs = !ask}) $ f eqs a b
|
||||
|
||||
export covering %inline
|
||||
equalTWith : HasErr q m => HasDefs' q _ m => Eq q =>
|
||||
DimEq d -> Term q d n -> Term q d n -> m ()
|
||||
equalTWith = into compareT Equal
|
||||
|
||||
export covering %inline
|
||||
equalEWith : HasErr q m => HasDefs' q _ m => Eq q =>
|
||||
DimEq d -> Elim q d n -> Elim q d n -> m ()
|
||||
equalEWith = into compareE Equal
|
||||
|
||||
export covering %inline
|
||||
subTWith : HasErr q m => HasDefs' q _ m => Eq q =>
|
||||
DimEq d -> Term q d n -> Term q d n -> m ()
|
||||
subTWith = into compareT Sub
|
||||
|
||||
export covering %inline
|
||||
subEWith : HasErr q m => HasDefs' q _ m => Eq q =>
|
||||
DimEq d -> Elim q d n -> Elim q d n -> m ()
|
||||
subEWith = into compareE Sub
|
||||
|
||||
|
||||
export covering %inline
|
||||
equalT : HasErr q m => HasDefs' q _ m => Eq q =>
|
||||
{d : Nat} -> Term q d n -> Term q d n -> m ()
|
||||
equalT = equalTWith DimEq.new
|
||||
|
||||
export covering %inline
|
||||
equalE : HasErr q m => HasDefs' q _ m => Eq q =>
|
||||
{d : Nat} -> Elim q d n -> Elim q d n -> m ()
|
||||
equalE = equalEWith DimEq.new
|
||||
|
||||
export covering %inline
|
||||
subT : HasErr q m => HasDefs' q _ m => Eq q =>
|
||||
{d : Nat} -> Term q d n -> Term q d n -> m ()
|
||||
subT = subTWith DimEq.new
|
||||
|
||||
export covering %inline
|
||||
subE : HasErr q m => HasDefs' q _ m => Eq q =>
|
||||
{d : Nat} -> Elim q d n -> Elim q d n -> m ()
|
||||
subE = subEWith DimEq.new
|
||||
|
|
|
|||
|
|
@ -1,84 +1,78 @@
|
|||
module Quox.Syntax.Qty
|
||||
|
||||
import Quox.Pretty
|
||||
|
||||
import Data.Fin
|
||||
import Generics.Derive
|
||||
import Data.DPair
|
||||
|
||||
%default total
|
||||
%language ElabReflection
|
||||
|
||||
|
||||
public export
|
||||
data Qty = Zero | One | Any
|
||||
%name Qty.Qty pi, rh
|
||||
|
||||
%runElab derive "Qty" [Generic, Meta, Eq, Ord, DecEq, Show]
|
||||
|
||||
|
||||
export
|
||||
PrettyHL Qty where
|
||||
prettyM pi = hl Qty <$>
|
||||
case pi of
|
||||
Zero => ifUnicode "𝟬" "0"
|
||||
One => ifUnicode "𝟭" "1"
|
||||
Any => ifUnicode "𝛚" "*"
|
||||
|
||||
private
|
||||
commas : List (Doc HL) -> List (Doc HL)
|
||||
commas [] = []
|
||||
commas [x] = [x]
|
||||
commas [] = []
|
||||
commas [x] = [x]
|
||||
commas (x::xs) = (x <+> hl Delim ",") :: commas xs
|
||||
|
||||
export %inline
|
||||
prettyQtyBinds : Pretty.HasEnv m => List Qty -> m (Doc HL)
|
||||
prettyQtyBinds : Pretty.HasEnv m => PrettyHL q =>
|
||||
List q -> m (Doc HL)
|
||||
prettyQtyBinds =
|
||||
map ((hl Delim "@" <++>) . align . sep . commas) . traverse pretty0M
|
||||
|
||||
|
||||
public export
|
||||
plus : Qty -> Qty -> Qty
|
||||
plus Zero rh = rh
|
||||
plus pi Zero = pi
|
||||
plus _ _ = Any
|
||||
|
||||
public export
|
||||
times : Qty -> Qty -> Qty
|
||||
times Zero _ = Zero
|
||||
times _ Zero = Zero
|
||||
times One rh = rh
|
||||
times pi One = pi
|
||||
times Any Any = Any
|
||||
|
||||
infix 6 <=.
|
||||
public export
|
||||
compat : Qty -> Qty -> Bool
|
||||
compat pi rh = rh == Any || pi == rh
|
||||
|
||||
|
||||
public export
|
||||
interface IsQty q where
|
||||
interface Eq q => IsQty q where
|
||||
zero, one : q
|
||||
(+), (*) : q -> q -> q
|
||||
(<=.) : q -> q -> Bool
|
||||
|
||||
||| true if bindings of this quantity will be erased
|
||||
||| and must not be runtime relevant
|
||||
IsZero : q -> Type
|
||||
isZero : (pi : q) -> Dec (IsZero pi)
|
||||
zeroIsZero : IsZero zero
|
||||
|
||||
||| true if bindings of this quantity must be linear
|
||||
-- [fixme] is this needed for anything?
|
||||
IsOne : q -> Type
|
||||
isOne : (pi : q) -> Dec (IsOne pi)
|
||||
oneIsOne : IsOne one
|
||||
|
||||
||| ``p `Compat` q`` if it is ok for a binding of
|
||||
||| quantity `q` to be used exactly `p` times.
|
||||
||| e.g. ``1 `Compat` 1``, ``1 `Compat` ω``
|
||||
Compat : q -> q -> Type
|
||||
compat : (pi, rh : q) -> Dec (pi `Compat` rh)
|
||||
|
||||
||| true if it is ok for this quantity to appear for the
|
||||
||| subject of a typing judgement. this is about the
|
||||
||| subject reduction stuff in atkey
|
||||
IsSubj : q -> Type
|
||||
isSubj : (pi : q) -> Dec (IsSubj pi)
|
||||
zeroIsSubj : IsSubj zero
|
||||
oneIsSubj : IsSubj one
|
||||
|
||||
||| true if it is ok for a global definition to have this
|
||||
||| quantity. so not exact usage counts, maybe.
|
||||
IsGlobal : q -> Type
|
||||
isGlobal : (pi : q) -> Dec (IsGlobal pi)
|
||||
zeroIsGlobal : IsGlobal zero
|
||||
|
||||
public export
|
||||
IsQty Qty where
|
||||
zero = Zero; one = One
|
||||
(+) = plus; (*) = times
|
||||
(<=.) = compat
|
||||
0 SQty : (q : Type) -> IsQty q => Type
|
||||
SQty q = Subset q IsSubj
|
||||
|
||||
public export %inline
|
||||
szero : IsQty q => SQty q
|
||||
szero = Element zero zeroIsSubj
|
||||
|
||||
public export %inline
|
||||
sone : IsQty q => SQty q
|
||||
sone = Element one oneIsSubj
|
||||
|
||||
public export
|
||||
data IsSubj : Qty -> Type where
|
||||
SZero : IsSubj Zero
|
||||
SOne : IsSubj One
|
||||
0 GQty : (q : Type) -> IsQty q => Type
|
||||
GQty q = Subset q IsGlobal
|
||||
|
||||
export Uninhabited (IsSubj Any) where uninhabited _ impossible
|
||||
public export %inline
|
||||
gzero : IsQty q => GQty q
|
||||
gzero = Element zero zeroIsGlobal
|
||||
|
||||
public export
|
||||
data IsGlobal : Qty -> Type where
|
||||
GZero : IsGlobal Zero
|
||||
GAny : IsGlobal Any
|
||||
|
||||
export Uninhabited (IsGlobal One) where uninhabited _ impossible
|
||||
|
|
|
|||
111
lib/Quox/Syntax/Qty/Three.idr
Normal file
111
lib/Quox/Syntax/Qty/Three.idr
Normal file
|
|
@ -0,0 +1,111 @@
|
|||
module Quox.Syntax.Qty.Three
|
||||
|
||||
import Quox.Pretty
|
||||
import public Quox.Syntax.Qty
|
||||
import Generics.Derive
|
||||
|
||||
%default total
|
||||
%language ElabReflection
|
||||
|
||||
|
||||
public export
|
||||
data Three = Zero | One | Any
|
||||
%name Three pi, rh
|
||||
|
||||
%runElab derive "Three" [Generic, Meta, Eq, Ord, DecEq, Show]
|
||||
|
||||
|
||||
export
|
||||
PrettyHL Three where
|
||||
prettyM pi = hl Qty <$>
|
||||
case pi of
|
||||
Zero => ifUnicode "𝟬" "0"
|
||||
One => ifUnicode "𝟭" "1"
|
||||
Any => ifUnicode "𝛚" "*"
|
||||
|
||||
|
||||
public export
|
||||
plus : Three -> Three -> Three
|
||||
plus Zero rh = rh
|
||||
plus pi Zero = pi
|
||||
plus _ _ = Any
|
||||
|
||||
public export
|
||||
times : Three -> Three -> Three
|
||||
times Zero _ = Zero
|
||||
times _ Zero = Zero
|
||||
times One rh = rh
|
||||
times pi One = pi
|
||||
times Any Any = Any
|
||||
|
||||
public export
|
||||
data Compat3 : Three -> Three -> Type where
|
||||
CmpRefl : Compat3 pi pi
|
||||
CmpAny : Compat3 pi Any
|
||||
|
||||
public export
|
||||
compat3 : (pi, rh : Three) -> Dec (pi `Compat3` rh)
|
||||
compat3 pi rh with (decEq pi rh)
|
||||
compat3 pi pi | Yes Refl = Yes CmpRefl
|
||||
compat3 pi rh | No ne with (decEq rh Any)
|
||||
compat3 pi Any | No ne | Yes Refl = Yes CmpAny
|
||||
compat3 pi rh | No ne | No na = No $ \case
|
||||
CmpRefl => ne Refl
|
||||
CmpAny => na Refl
|
||||
|
||||
|
||||
public export
|
||||
data IsSubj3 : Three -> Type where
|
||||
SZero : IsSubj3 Zero
|
||||
SOne : IsSubj3 One
|
||||
|
||||
public export
|
||||
isSubj3 : (pi : Three) -> Dec (IsSubj3 pi)
|
||||
isSubj3 Zero = Yes SZero
|
||||
isSubj3 One = Yes SOne
|
||||
isSubj3 Any = No $ \case _ impossible
|
||||
|
||||
|
||||
public export
|
||||
data IsGlobal3 : Three -> Type where
|
||||
GZero : IsGlobal3 Zero
|
||||
GAny : IsGlobal3 Any
|
||||
|
||||
isGlobal3 : (pi : Three) -> Dec (IsGlobal3 pi)
|
||||
isGlobal3 Zero = Yes GZero
|
||||
isGlobal3 One = No $ \case _ impossible
|
||||
isGlobal3 Any = Yes GAny
|
||||
|
||||
|
||||
public export
|
||||
IsQty Three where
|
||||
zero = Zero
|
||||
one = One
|
||||
|
||||
(+) = plus
|
||||
(*) = times
|
||||
|
||||
IsZero = Equal Zero
|
||||
isZero = decEq Zero
|
||||
zeroIsZero = Refl
|
||||
|
||||
IsOne = Equal One
|
||||
isOne = decEq One
|
||||
oneIsOne = Refl
|
||||
|
||||
Compat = Compat3
|
||||
compat = compat3
|
||||
|
||||
IsSubj = IsSubj3
|
||||
isSubj = isSubj3
|
||||
zeroIsSubj = SZero
|
||||
oneIsSubj = SOne
|
||||
|
||||
IsGlobal = IsGlobal3
|
||||
isGlobal = isGlobal3
|
||||
zeroIsGlobal = GZero
|
||||
|
||||
|
||||
export Uninhabited (IsGlobal3 One) where uninhabited _ impossible
|
||||
|
||||
export Uninhabited (IsSubj3 Any) where uninhabited _ impossible
|
||||
|
|
@ -26,63 +26,67 @@ infixl 8 :#
|
|||
infixl 9 :@
|
||||
mutual
|
||||
public export
|
||||
TSubst : Nat -> Nat -> Nat -> Type
|
||||
TSubst d = Subst (\n => Elim d n)
|
||||
TSubst : Type -> Nat -> Nat -> Nat -> Type
|
||||
TSubst q d = Subst (\n => Elim q d n)
|
||||
|
||||
||| first argument `d` is dimension scope size, second `n` is term scope size
|
||||
public export
|
||||
data Term : (d, n : Nat) -> Type where
|
||||
data Term : (q : Type) -> (d, n : Nat) -> Type where
|
||||
||| type of types
|
||||
TYPE : (l : Universe) -> Term d n
|
||||
TYPE : (l : Universe) -> Term q d n
|
||||
|
||||
||| function type
|
||||
Pi : (qty : Qty) -> (x : Name) ->
|
||||
(arg : Term d n) -> (res : ScopeTerm d n) -> Term d n
|
||||
Pi : (qty : q) -> (x : Name) ->
|
||||
(arg : Term q d n) -> (res : ScopeTerm q d n) -> Term q d n
|
||||
||| function term
|
||||
Lam : (x : Name) -> (body : ScopeTerm d n) -> Term d n
|
||||
Lam : (x : Name) -> (body : ScopeTerm q d n) -> Term q d n
|
||||
|
||||
||| elimination
|
||||
E : (e : Elim d n) -> Term d n
|
||||
E : (e : Elim q d n) -> Term q d n
|
||||
|
||||
||| term closure/suspended substitution
|
||||
CloT : (tm : Term d from) -> (th : Lazy (TSubst d from to)) -> Term d to
|
||||
CloT : (tm : Term q d from) -> (th : Lazy (TSubst q d from to)) ->
|
||||
Term q d to
|
||||
||| dimension closure/suspended substitution
|
||||
DCloT : (tm : Term dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Term dto n
|
||||
DCloT : (tm : Term q dfrom n) -> (th : Lazy (DSubst dfrom dto)) ->
|
||||
Term q dto n
|
||||
|
||||
||| first argument `d` is dimension scope size, second `n` is term scope size
|
||||
public export
|
||||
data Elim : (d, n : Nat) -> Type where
|
||||
data Elim : (q : Type) -> (d, n : Nat) -> Type where
|
||||
||| free variable
|
||||
F : (x : Name) -> Elim d n
|
||||
F : (x : Name) -> Elim q d n
|
||||
||| bound variable
|
||||
B : (i : Var n) -> Elim d n
|
||||
B : (i : Var n) -> Elim q d n
|
||||
|
||||
||| term application
|
||||
(:@) : (fun : Elim d n) -> (arg : Term d n) -> Elim d n
|
||||
(:@) : (fun : Elim q d n) -> (arg : Term q d n) -> Elim q d n
|
||||
|
||||
||| type-annotated term
|
||||
(:#) : (tm, ty : Term d n) -> Elim d n
|
||||
(:#) : (tm, ty : Term q d n) -> Elim q d n
|
||||
|
||||
||| term closure/suspended substitution
|
||||
CloE : (el : Elim d from) -> (th : Lazy (TSubst d from to)) -> Elim d to
|
||||
CloE : (el : Elim q d from) -> (th : Lazy (TSubst q d from to)) ->
|
||||
Elim q d to
|
||||
||| dimension closure/suspended substitution
|
||||
DCloE : (el : Elim dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Elim dto n
|
||||
DCloE : (el : Elim q dfrom n) -> (th : Lazy (DSubst dfrom dto)) ->
|
||||
Elim q dto n
|
||||
|
||||
||| a scope with one more bound variable
|
||||
public export
|
||||
data ScopeTerm : (d, n : Nat) -> Type where
|
||||
data ScopeTerm : (q : Type) -> (d, n : Nat) -> Type where
|
||||
||| variable is used
|
||||
TUsed : (body : Term d (S n)) -> ScopeTerm d n
|
||||
TUsed : (body : Term q d (S n)) -> ScopeTerm q d n
|
||||
||| variable is unused
|
||||
TUnused : (body : Term d n) -> ScopeTerm d n
|
||||
TUnused : (body : Term q d n) -> ScopeTerm q d n
|
||||
|
||||
||| a scope with one more bound dimension variable
|
||||
public export
|
||||
data DScopeTerm : (d, n : Nat) -> Type where
|
||||
data DScopeTerm : (q : Type) -> (d, n : Nat) -> Type where
|
||||
||| variable is used
|
||||
DUsed : (body : Term (S d) n) -> DScopeTerm d n
|
||||
DUsed : (body : Term q (S d) n) -> DScopeTerm q d n
|
||||
||| variable is unused
|
||||
DUnused : (body : Term d n) -> DScopeTerm d n
|
||||
DUnused : (body : Term q d n) -> DScopeTerm q d n
|
||||
|
||||
%name Term s, t, r
|
||||
%name Elim e, f
|
||||
|
|
@ -90,21 +94,21 @@ mutual
|
|||
%name DScopeTerm body
|
||||
|
||||
public export %inline
|
||||
Arr : (qty : Qty) -> (arg, res : Term d n) -> Term d n
|
||||
Arr : (qty : q) -> (arg, res : Term q d n) -> Term q d n
|
||||
Arr {qty, arg, res} = Pi {qty, x = "_", arg, res = TUnused res}
|
||||
|
||||
||| same as `F` but as a term
|
||||
public export %inline
|
||||
FT : Name -> Term d n
|
||||
FT : Name -> Term q d n
|
||||
FT = E . F
|
||||
|
||||
||| abbreviation for a bound variable like `BV 4` instead of
|
||||
||| `B (VS (VS (VS (VS VZ))))`
|
||||
public export %inline
|
||||
BV : (i : Nat) -> (0 _ : LT i n) => Elim d n
|
||||
BV : (i : Nat) -> (0 _ : LT i n) => Elim q d n
|
||||
BV i = B $ V i
|
||||
|
||||
||| same as `BV` but as a term
|
||||
public export %inline
|
||||
BVT : (i : Nat) -> (0 _ : LT i n) => Term d n
|
||||
BVT : (i : Nat) -> (0 _ : LT i n) => Term q d n
|
||||
BVT i = E $ BV i
|
||||
|
|
|
|||
|
|
@ -28,7 +28,7 @@ colonD = hl Syntax ":"
|
|||
|
||||
mutual
|
||||
export covering
|
||||
PrettyHL (Term d n) where
|
||||
PrettyHL q => PrettyHL (Term q d n) where
|
||||
prettyM (TYPE l) =
|
||||
parensIfM App $ typeD <//> !(withPrec Arg $ prettyM l)
|
||||
prettyM (Pi qty x s t) =
|
||||
|
|
@ -49,7 +49,7 @@ mutual
|
|||
[|withPrec SApp (prettyM s) </> prettyDSubst th|]
|
||||
|
||||
export covering
|
||||
PrettyHL (Elim d n) where
|
||||
PrettyHL q => PrettyHL (Elim q d n) where
|
||||
prettyM (F x) =
|
||||
hl' Free <$> prettyM x
|
||||
prettyM (B i) =
|
||||
|
|
@ -70,15 +70,17 @@ mutual
|
|||
[|withPrec SApp (prettyM e) </> prettyDSubst th|]
|
||||
|
||||
export covering
|
||||
PrettyHL (ScopeTerm d n) where
|
||||
PrettyHL q => PrettyHL (ScopeTerm q d n) where
|
||||
prettyM body = prettyM $ fromScopeTerm body
|
||||
|
||||
export covering
|
||||
prettyTSubst : Pretty.HasEnv m => TSubst d from to -> m (Doc HL)
|
||||
prettyTSubst : Pretty.HasEnv m => PrettyHL q =>
|
||||
TSubst q d from to -> m (Doc HL)
|
||||
prettyTSubst s = prettySubstM prettyM (!ask).tnames TVar "[" "]" s
|
||||
|
||||
export covering
|
||||
prettyBinder : Pretty.HasEnv m => List Qty -> Name -> Term d n -> m (Doc HL)
|
||||
prettyBinder : Pretty.HasEnv m => PrettyHL q =>
|
||||
List q -> Name -> Term q d n -> m (Doc HL)
|
||||
prettyBinder pis x a =
|
||||
pure $ parens $ hang 2 $
|
||||
hsep [hl TVar !(prettyM x),
|
||||
|
|
|
|||
|
|
@ -7,43 +7,57 @@ import Quox.Syntax.Term.Subst
|
|||
|
||||
|
||||
mutual
|
||||
||| true if a term has a closure or dimension closure at the top level,
|
||||
||| or is `E` applied to such an elimination
|
||||
public export %inline
|
||||
topCloT : Term d n -> Bool
|
||||
topCloT (CloT _ _) = True
|
||||
topCloT (DCloT _ _) = True
|
||||
topCloT (E e) = topCloE e
|
||||
topCloT _ = False
|
||||
public export
|
||||
data NotCloT : Term {} -> Type where
|
||||
NCTYPE : NotCloT $ TYPE _
|
||||
NCPi : NotCloT $ Pi {}
|
||||
NCLam : NotCloT $ Lam {}
|
||||
NCE : NotCloE e -> NotCloT $ E e
|
||||
|
||||
||| true if an elimination has a closure or dimension closure at the top level
|
||||
public export %inline
|
||||
topCloE : Elim d n -> Bool
|
||||
topCloE (CloE _ _) = True
|
||||
topCloE (DCloE _ _) = True
|
||||
topCloE _ = False
|
||||
public export
|
||||
data NotCloE : Elim {} -> Type where
|
||||
NCF : NotCloE $ F _
|
||||
NCB : NotCloE $ B _
|
||||
NCApp : NotCloE $ _ :@ _
|
||||
NCAnn : NotCloE $ _ :# _
|
||||
|
||||
mutual
|
||||
export
|
||||
notCloT : (t : Term {}) -> Dec (NotCloT t)
|
||||
notCloT (TYPE _) = Yes NCTYPE
|
||||
notCloT (Pi {}) = Yes NCPi
|
||||
notCloT (Lam {}) = Yes NCLam
|
||||
notCloT (E e) with (notCloE e)
|
||||
notCloT (E e) | Yes nc = Yes $ NCE nc
|
||||
notCloT (E e) | No c = No $ \case NCE nc => c nc
|
||||
notCloT (CloT {}) = No $ \case _ impossible
|
||||
notCloT (DCloT {}) = No $ \case _ impossible
|
||||
|
||||
public export IsNotCloT : Term d n -> Type
|
||||
IsNotCloT = So . not . topCloT
|
||||
export
|
||||
notCloE : (e : Elim {}) -> Dec (NotCloE e)
|
||||
notCloE (F _) = Yes NCF
|
||||
notCloE (B _) = Yes NCB
|
||||
notCloE (_ :@ _) = Yes NCApp
|
||||
notCloE (_ :# _) = Yes NCAnn
|
||||
notCloE (CloE {}) = No $ \case _ impossible
|
||||
notCloE (DCloE {}) = No $ \case _ impossible
|
||||
|
||||
||| a term which is not a top level closure
|
||||
public export NotCloTerm : Nat -> Nat -> Type
|
||||
NotCloTerm d n = Subset (Term d n) IsNotCloT
|
||||
|
||||
public export IsNotCloE : Elim d n -> Type
|
||||
IsNotCloE = So . not . topCloE
|
||||
public export
|
||||
NotCloTerm : Type -> Nat -> Nat -> Type
|
||||
NotCloTerm q d n = Subset (Term q d n) NotCloT
|
||||
|
||||
||| an elimination which is not a top level closure
|
||||
public export NotCloElim : Nat -> Nat -> Type
|
||||
NotCloElim d n = Subset (Elim d n) IsNotCloE
|
||||
public export
|
||||
NotCloElim : Type -> Nat -> Nat -> Type
|
||||
NotCloElim q d n = Subset (Elim q d n) NotCloE
|
||||
|
||||
public export %inline
|
||||
ncloT : (t : Term d n) -> (0 _ : IsNotCloT t) => NotCloTerm d n
|
||||
ncloT : (t : Term q d n) -> (0 _ : NotCloT t) => NotCloTerm q d n
|
||||
ncloT t @{p} = Element t p
|
||||
|
||||
public export %inline
|
||||
ncloE : (t : Elim d n) -> (0 _ : IsNotCloE t) => NotCloElim d n
|
||||
ncloE : (e : Elim q d n) -> (0 _ : NotCloE e) => NotCloElim q d n
|
||||
ncloE e @{p} = Element e p
|
||||
|
||||
|
||||
|
|
@ -52,18 +66,18 @@ mutual
|
|||
||| if the input term has any top-level closures, push them under one layer of
|
||||
||| syntax
|
||||
export %inline
|
||||
pushSubstsT : Term d n -> NotCloTerm d n
|
||||
pushSubstsT : Term q d n -> NotCloTerm q d n
|
||||
pushSubstsT s = pushSubstsTWith id id s
|
||||
|
||||
||| if the input elimination has any top-level closures, push them under one
|
||||
||| layer of syntax
|
||||
export %inline
|
||||
pushSubstsE : Elim d n -> NotCloElim d n
|
||||
pushSubstsE : Elim q d n -> NotCloElim q d n
|
||||
pushSubstsE e = pushSubstsEWith id id e
|
||||
|
||||
export
|
||||
pushSubstsTWith : DSubst dfrom dto -> TSubst dto from to ->
|
||||
Term dfrom from -> NotCloTerm dto to
|
||||
pushSubstsTWith : DSubst dfrom dto -> TSubst q dto from to ->
|
||||
Term q dfrom from -> NotCloTerm q dto to
|
||||
pushSubstsTWith th ph (TYPE l) =
|
||||
ncloT $ TYPE l
|
||||
pushSubstsTWith th ph (Pi qty x a body) =
|
||||
|
|
@ -78,15 +92,15 @@ mutual
|
|||
pushSubstsTWith (ps . th) ph s
|
||||
|
||||
export
|
||||
pushSubstsEWith : DSubst dfrom dto -> TSubst dto from to ->
|
||||
Elim dfrom from -> NotCloElim dto to
|
||||
pushSubstsEWith : DSubst dfrom dto -> TSubst q dto from to ->
|
||||
Elim q dfrom from -> NotCloElim q dto to
|
||||
pushSubstsEWith th ph (F x) =
|
||||
ncloE $ F x
|
||||
pushSubstsEWith th ph (B i) =
|
||||
let res = ph !! i in
|
||||
case choose $ topCloE res of
|
||||
Left _ => assert_total pushSubstsE res
|
||||
Right _ => ncloE res
|
||||
case notCloE res of
|
||||
Yes _ => ncloE res
|
||||
No _ => assert_total pushSubstsE res
|
||||
pushSubstsEWith th ph (f :@ s) =
|
||||
ncloE $ subs f th ph :@ subs s th ph
|
||||
pushSubstsEWith th ph (s :# a) =
|
||||
|
|
@ -97,22 +111,22 @@ mutual
|
|||
pushSubstsEWith (ps . th) ph e
|
||||
|
||||
|
||||
parameters (th : DSubst dfrom dto) (ph : TSubst dto from to)
|
||||
parameters (th : DSubst dfrom dto) (ph : TSubst q dto from to)
|
||||
public export %inline
|
||||
pushSubstsTWith' : Term dfrom from -> Term dto to
|
||||
pushSubstsTWith' : Term q dfrom from -> Term q dto to
|
||||
pushSubstsTWith' s = (pushSubstsTWith th ph s).fst
|
||||
|
||||
public export %inline
|
||||
pushSubstsEWith' : Elim dfrom from -> Elim dto to
|
||||
pushSubstsEWith' : Elim q dfrom from -> Elim q dto to
|
||||
pushSubstsEWith' e = (pushSubstsEWith th ph e).fst
|
||||
|
||||
|
||||
public export %inline
|
||||
pushSubstsT' : Term d n -> Term d n
|
||||
pushSubstsT' : Term q d n -> Term q d n
|
||||
pushSubstsT' s = (pushSubstsT s).fst
|
||||
|
||||
public export %inline
|
||||
pushSubstsE' : Elim d n -> Elim d n
|
||||
pushSubstsE' : Elim q d n -> Elim q d n
|
||||
pushSubstsE' e = (pushSubstsE e).fst
|
||||
|
||||
|
||||
|
|
@ -159,41 +173,41 @@ pushSubstsE' e = (pushSubstsE e).fst
|
|||
|
||||
|
||||
public export %inline
|
||||
weakT : Term d n -> Term d (S n)
|
||||
weakT : Term q d n -> Term q d (S n)
|
||||
weakT t = t //. shift 1
|
||||
|
||||
public export %inline
|
||||
weakE : Elim d n -> Elim d (S n)
|
||||
weakE : Elim q d n -> Elim q d (S n)
|
||||
weakE t = t //. shift 1
|
||||
|
||||
|
||||
mutual
|
||||
public export
|
||||
data IsRedexT : Term d n -> Type where
|
||||
data IsRedexT : Term q d n -> Type where
|
||||
IsUpsilonT : IsRedexT $ E (_ :# _)
|
||||
IsCloT : IsRedexT $ CloT {}
|
||||
IsDCloT : IsRedexT $ DCloT {}
|
||||
IsERedex : IsRedexE e -> IsRedexT $ E e
|
||||
|
||||
public export %inline
|
||||
NotRedexT : Term d n -> Type
|
||||
NotRedexT : Term q d n -> Type
|
||||
NotRedexT = Not . IsRedexT
|
||||
|
||||
public export
|
||||
data IsRedexE : Elim d n -> Type where
|
||||
data IsRedexE : Elim q d n -> Type where
|
||||
IsUpsilonE : IsRedexE $ E _ :# _
|
||||
IsBetaLam : IsRedexE $ (Lam {} :# Pi {}) :@ _
|
||||
IsCloE : IsRedexE $ CloE {}
|
||||
IsDCloE : IsRedexE $ DCloE {}
|
||||
|
||||
public export %inline
|
||||
NotRedexE : Elim d n -> Type
|
||||
NotRedexE : Elim q d n -> Type
|
||||
NotRedexE = Not . IsRedexE
|
||||
|
||||
|
||||
mutual
|
||||
export %inline
|
||||
isRedexT : (t : Term d n) -> Dec (IsRedexT t)
|
||||
isRedexT : (t : Term {}) -> Dec (IsRedexT t)
|
||||
isRedexT (E (tm :# ty)) = Yes IsUpsilonT
|
||||
isRedexT (CloT {}) = Yes IsCloT
|
||||
isRedexT (DCloT {}) = Yes IsDCloT
|
||||
|
|
@ -201,7 +215,7 @@ mutual
|
|||
isRedexT (E (DCloE {})) = Yes $ IsERedex IsDCloE
|
||||
isRedexT (E e@(_ :@ _)) with (isRedexE e)
|
||||
_ | Yes yes = Yes $ IsERedex yes
|
||||
_ | No no = No \case IsERedex p => no p
|
||||
_ | No no = No $ \case IsERedex p => no p
|
||||
isRedexT (TYPE {}) = No $ \case _ impossible
|
||||
isRedexT (Pi {}) = No $ \case _ impossible
|
||||
isRedexT (Lam {}) = No $ \case _ impossible
|
||||
|
|
@ -209,7 +223,7 @@ mutual
|
|||
isRedexT (E (B _)) = No $ \case IsERedex _ impossible
|
||||
|
||||
export %inline
|
||||
isRedexE : (e : Elim d n) -> Dec (IsRedexE e)
|
||||
isRedexE : (e : Elim {}) -> Dec (IsRedexE e)
|
||||
isRedexE (E _ :# _) = Yes IsUpsilonE
|
||||
isRedexE ((Lam {} :# Pi {}) :@ _) = Yes IsBetaLam
|
||||
isRedexE (CloE {}) = Yes IsCloE
|
||||
|
|
@ -239,39 +253,38 @@ mutual
|
|||
|
||||
|
||||
public export %inline
|
||||
RedexTerm : Nat -> Nat -> Type
|
||||
RedexTerm d n = Subset (Term d n) IsRedexT
|
||||
RedexTerm : Type -> Nat -> Nat -> Type
|
||||
RedexTerm q d n = Subset (Term q d n) IsRedexT
|
||||
|
||||
public export %inline
|
||||
NonRedexTerm : Nat -> Nat -> Type
|
||||
NonRedexTerm d n = Subset (Term d n) NotRedexT
|
||||
|
||||
NonRedexTerm : Type -> Nat -> Nat -> Type
|
||||
NonRedexTerm q d n = Subset (Term q d n) NotRedexT
|
||||
|
||||
public export %inline
|
||||
RedexElim : Nat -> Nat -> Type
|
||||
RedexElim d n = Subset (Elim d n) IsRedexE
|
||||
RedexElim : Type -> Nat -> Nat -> Type
|
||||
RedexElim q d n = Subset (Elim q d n) IsRedexE
|
||||
|
||||
public export %inline
|
||||
NonRedexElim : Nat -> Nat -> Type
|
||||
NonRedexElim d n = Subset (Elim d n) NotRedexE
|
||||
NonRedexElim : Type -> Nat -> Nat -> Type
|
||||
NonRedexElim q d n = Subset (Elim q d n) NotRedexE
|
||||
|
||||
|
||||
||| substitute a term with annotation for the bound variable of a `ScopeTerm`
|
||||
export %inline
|
||||
substScope : (arg, argTy : Term d n) -> (body : ScopeTerm d n) -> Term d n
|
||||
substScope : (arg, argTy : Term q d n) -> (body : ScopeTerm q d n) -> Term q d n
|
||||
substScope arg argTy (TUsed body) = body // one (arg :# argTy)
|
||||
substScope arg argTy (TUnused body) = body
|
||||
|
||||
mutual
|
||||
export %inline
|
||||
stepT' : (s : Term d n) -> IsRedexT s -> Term d n
|
||||
stepT' : (s : Term q d n) -> IsRedexT s -> Term q d n
|
||||
stepT' (E (s :# _)) IsUpsilonT = s
|
||||
stepT' (CloT s th) IsCloT = pushSubstsTWith' id th s
|
||||
stepT' (DCloT s th) IsDCloT = pushSubstsTWith' th id s
|
||||
stepT' (E e) (IsERedex p) = E $ stepE' e p
|
||||
|
||||
export %inline
|
||||
stepE' : (e : Elim d n) -> IsRedexE e -> Elim d n
|
||||
stepE' : (e : Elim q d n) -> IsRedexE e -> Elim q d n
|
||||
stepE' (E e :# _) IsUpsilonE = e
|
||||
stepE' ((Lam {body, _} :# Pi {arg, res, _}) :@ s) IsBetaLam =
|
||||
substScope s arg body :# substScope s arg res
|
||||
|
|
@ -279,21 +292,21 @@ mutual
|
|||
stepE' (DCloE e th) IsDCloE = pushSubstsEWith' th id e
|
||||
|
||||
export %inline
|
||||
stepT : (s : Term d n) -> Either (NotRedexT s) (Term d n)
|
||||
stepT : (s : Term q d n) -> Either (NotRedexT s) (Term q d n)
|
||||
stepT s = case isRedexT s of Yes y => Right $ stepT' s y; No n => Left n
|
||||
|
||||
export %inline
|
||||
stepE : (e : Elim d n) -> Either (NotRedexE e) (Elim d n)
|
||||
stepE : (e : Elim q d n) -> Either (NotRedexE e) (Elim q d n)
|
||||
stepE e = case isRedexE e of Yes y => Right $ stepE' e y; No n => Left n
|
||||
|
||||
export covering
|
||||
whnfT : Term d n -> NonRedexTerm d n
|
||||
whnfT : Term q d n -> NonRedexTerm q d n
|
||||
whnfT s = case stepT s of
|
||||
Right s' => whnfT s'
|
||||
Left done => Element s done
|
||||
|
||||
export covering
|
||||
whnfE : Elim d n -> NonRedexElim d n
|
||||
whnfE : Elim q d n -> NonRedexElim q d n
|
||||
whnfE e = case stepE e of
|
||||
Right e' => whnfE e'
|
||||
Left done => Element e done
|
||||
|
|
|
|||
|
|
@ -9,74 +9,100 @@ import Data.Vect
|
|||
%default total
|
||||
|
||||
|
||||
public export %inline
|
||||
isLam : Term d n -> Bool
|
||||
isLam (Lam {}) = True
|
||||
isLam _ = False
|
||||
|
||||
public export
|
||||
NotLam : Term d n -> Type
|
||||
NotLam = So . not . isLam
|
||||
|
||||
data IsLam : Term {} -> Type where
|
||||
ItIsLam : IsLam $ Lam x body
|
||||
|
||||
public export %inline
|
||||
isApp : Elim d n -> Bool
|
||||
isApp ((:@) {}) = True
|
||||
isApp _ = False
|
||||
isLam : (s : Term {}) -> Dec (IsLam s)
|
||||
isLam (TYPE _) = No $ \case _ impossible
|
||||
isLam (Pi {}) = No $ \case _ impossible
|
||||
isLam (Lam {}) = Yes ItIsLam
|
||||
isLam (E _) = No $ \case _ impossible
|
||||
isLam (CloT {}) = No $ \case _ impossible
|
||||
isLam (DCloT {}) = No $ \case _ impossible
|
||||
|
||||
public export %inline
|
||||
NotLam : Term {} -> Type
|
||||
NotLam = Not . IsLam
|
||||
|
||||
|
||||
public export
|
||||
NotApp : Elim d n -> Type
|
||||
NotApp = So . not . isApp
|
||||
data IsApp : Elim {} -> Type where
|
||||
ItIsApp : IsApp $ f :@ s
|
||||
|
||||
public export %inline
|
||||
isApp : (e : Elim {}) -> Dec (IsApp e)
|
||||
isApp (F _) = No $ \case _ impossible
|
||||
isApp (B _) = No $ \case _ impossible
|
||||
isApp (_ :@ _) = Yes ItIsApp
|
||||
isApp (_ :# _) = No $ \case _ impossible
|
||||
isApp (CloE {}) = No $ \case _ impossible
|
||||
isApp (DCloE {}) = No $ \case _ impossible
|
||||
|
||||
public export
|
||||
NotApp : Elim {} -> Type
|
||||
NotApp = Not . IsApp
|
||||
|
||||
|
||||
infixl 9 :@@
|
||||
||| apply multiple arguments at once
|
||||
public export %inline
|
||||
(:@@) : Elim d n -> List (Term d n) -> Elim d n
|
||||
(:@@) : Elim q d n -> List (Term q d n) -> Elim q d n
|
||||
f :@@ ss = foldl (:@) f ss
|
||||
|
||||
public export
|
||||
record GetArgs (d, n : Nat) where
|
||||
record GetArgs q d n where
|
||||
constructor GotArgs
|
||||
fun : Elim d n
|
||||
args : List (Term d n)
|
||||
fun : Elim q d n
|
||||
args : List (Term q d n)
|
||||
0 notApp : NotApp fun
|
||||
|
||||
export
|
||||
getArgs' : Elim d n -> List (Term d n) -> GetArgs d n
|
||||
getArgs' fun args with (choose $ isApp fun)
|
||||
getArgs' (f :@ a) args | Left yes = getArgs' f (a :: args)
|
||||
_ | Right no = GotArgs {fun, args, notApp = no}
|
||||
getArgs' : Elim q d n -> List (Term q d n) -> GetArgs q d n
|
||||
getArgs' fun args with (isApp fun)
|
||||
getArgs' (f :@ a) args | Yes yes = getArgs' f (a :: args)
|
||||
getArgs' fun args | No no = GotArgs {fun, args, notApp = no}
|
||||
|
||||
||| splits an application into its head and arguments. if it's not an
|
||||
||| application then the list is just empty
|
||||
export %inline
|
||||
getArgs : Elim d n -> GetArgs d n
|
||||
getArgs : Elim q d n -> GetArgs q d n
|
||||
getArgs e = getArgs' e []
|
||||
|
||||
|
||||
infixr 1 :\\
|
||||
public export
|
||||
(:\\) : Vect m Name -> Term d (m + n) -> Term d n
|
||||
[] :\\ t = t
|
||||
x :: xs :\\ t = let t' = replace {p = Term _} (plusSuccRightSucc {}) t in
|
||||
Lam x $ TUsed $ xs :\\ t'
|
||||
absN : Vect m Name -> Term q d (m + n) -> Term q d n
|
||||
absN {m = 0} [] s = s
|
||||
absN {m = S m} (x :: xs) s = Lam x $ TUsed $ absN xs $
|
||||
rewrite sym $ plusSuccRightSucc m n in s
|
||||
|
||||
public export %inline
|
||||
(:\\) : Vect m Name -> Term q d (m + n) -> Term q d n
|
||||
(:\\) = absN
|
||||
|
||||
|
||||
public export
|
||||
record GetLams (d, n : Nat) where
|
||||
record GetLams q d n where
|
||||
constructor GotLams
|
||||
names : Vect lams Name
|
||||
body : Term d rest
|
||||
body : Term q d rest
|
||||
0 eq : lams + n = rest
|
||||
0 notLam : NotLam body
|
||||
|
||||
public export
|
||||
getLams : Term d n -> GetLams d n
|
||||
getLams s with (choose $ isLam s)
|
||||
getLams s@(Lam x body) | Left yes =
|
||||
let inner = getLams $ assert_smaller s $ fromScopeTerm body in
|
||||
GotLams {names = x :: inner.names,
|
||||
body = inner.body,
|
||||
eq = plusSuccRightSucc {} `trans` inner.eq,
|
||||
notLam = inner.notLam}
|
||||
_ | Right no = GotLams {names = [], body = s, eq = Refl, notLam = no}
|
||||
export
|
||||
getLams' : forall lams, rest.
|
||||
Vect lams Name -> Term q d rest -> lams + n = rest -> GetLams q d n
|
||||
getLams' xs s eq with (isLam s)
|
||||
getLams' xs (Lam x sbody) Refl | Yes ItIsLam =
|
||||
let 0 s = Lam x sbody
|
||||
body = assert_smaller s $ fromScopeTerm sbody
|
||||
in
|
||||
getLams' (x :: xs) body Refl
|
||||
getLams' xs s eq | No no =
|
||||
GotLams xs s eq no
|
||||
|
||||
export
|
||||
getLams : Term q d n -> GetLams q d n
|
||||
getLams s = getLams' [] s Refl
|
||||
|
|
|
|||
|
|
@ -5,8 +5,8 @@ import Quox.Syntax.Term.Base
|
|||
%default total
|
||||
|
||||
|
||||
export FromVar (Elim d) where fromVar = B
|
||||
export FromVar (Term d) where fromVar = E . fromVar
|
||||
export FromVar (Elim q d) where fromVar = B
|
||||
export FromVar (Term q d) where fromVar = E . fromVar
|
||||
|
||||
||| does the minimal reasonable work:
|
||||
||| - deletes the closure around a free name since it doesn't do anything
|
||||
|
|
@ -15,7 +15,7 @@ export FromVar (Term d) where fromVar = E . fromVar
|
|||
||| - immediately looks up a bound variable
|
||||
||| - otherwise, wraps in a new closure
|
||||
export
|
||||
CanSubst (Elim d) (Elim d) where
|
||||
CanSubst (Elim q d) (Elim q d) where
|
||||
F x // _ = F x
|
||||
B i // th = th !! i
|
||||
CloE e ph // th = assert_total CloE e $ ph . th
|
||||
|
|
@ -30,7 +30,7 @@ CanSubst (Elim d) (Elim d) where
|
|||
||| - goes inside `E` in case it is a simple variable or something
|
||||
||| - otherwise, wraps in a new closure
|
||||
export
|
||||
CanSubst (Elim d) (Term d) where
|
||||
CanSubst (Elim q d) (Term q d) where
|
||||
TYPE l // _ = TYPE l
|
||||
E e // th = E $ e // th
|
||||
CloT s ph // th = CloT s $ ph . th
|
||||
|
|
@ -39,13 +39,13 @@ CanSubst (Elim d) (Term d) where
|
|||
th => CloT s th
|
||||
|
||||
export
|
||||
CanSubst (Elim d) (ScopeTerm d) where
|
||||
CanSubst (Elim q d) (ScopeTerm q d) where
|
||||
TUsed body // th = TUsed $ body // push th
|
||||
TUnused body // th = TUnused $ body // th
|
||||
|
||||
export CanSubst Var (Term d) where s // th = s // map (B {d}) th
|
||||
export CanSubst Var (Elim d) where e // th = e // map (B {d}) th
|
||||
export CanSubst Var (ScopeTerm d) where s // th = s // map (B {d}) th
|
||||
export CanSubst Var (Term q d) where s // th = s // map (B {q, d}) th
|
||||
export CanSubst Var (Elim q d) where e // th = e // map (B {q, d}) th
|
||||
export CanSubst Var (ScopeTerm q d) where s // th = s // map (B {q, d}) th
|
||||
|
||||
|
||||
infixl 8 //., ///
|
||||
|
|
@ -53,13 +53,13 @@ mutual
|
|||
namespace Term
|
||||
||| applies a term substitution with a less ambiguous type
|
||||
export
|
||||
(//.) : Term d from -> TSubst d from to -> Term d to
|
||||
(//.) : Term q d from -> TSubst q d from to -> Term q d to
|
||||
t //. th = t // th
|
||||
|
||||
||| applies a dimension substitution with the same behaviour as `(//)`
|
||||
||| above
|
||||
export
|
||||
(///) : Term dfrom n -> DSubst dfrom dto -> Term dto n
|
||||
(///) : Term q dfrom n -> DSubst dfrom dto -> Term q dto n
|
||||
TYPE l /// _ = TYPE l
|
||||
E e /// th = E $ e /// th
|
||||
DCloT s ph /// th = DCloT s $ ph . th
|
||||
|
|
@ -68,20 +68,20 @@ mutual
|
|||
|
||||
||| applies a term and dimension substitution
|
||||
public export %inline
|
||||
subs : Term dfrom from -> DSubst dfrom dto -> TSubst dto from to ->
|
||||
Term dto to
|
||||
subs : Term q dfrom from -> DSubst dfrom dto -> TSubst q dto from to ->
|
||||
Term q dto to
|
||||
subs s th ph = s /// th // ph
|
||||
|
||||
namespace Elim
|
||||
||| applies a term substitution with a less ambiguous type
|
||||
export
|
||||
(//.) : Elim d from -> TSubst d from to -> Elim d to
|
||||
(//.) : Elim q d from -> TSubst q d from to -> Elim q d to
|
||||
e //. th = e // th
|
||||
|
||||
||| applies a dimension substitution with the same behaviour as `(//)`
|
||||
||| above
|
||||
export
|
||||
(///) : Elim dfrom n -> DSubst dfrom dto -> Elim dto n
|
||||
(///) : Elim q dfrom n -> DSubst dfrom dto -> Elim q dto n
|
||||
F x /// _ = F x
|
||||
B i /// _ = B i
|
||||
DCloE e ph /// th = DCloE e $ ph . th
|
||||
|
|
@ -90,46 +90,46 @@ mutual
|
|||
|
||||
||| applies a term and dimension substitution
|
||||
public export %inline
|
||||
subs : Elim dfrom from -> DSubst dfrom dto -> TSubst dto from to ->
|
||||
Elim dto to
|
||||
subs : Elim q dfrom from -> DSubst dfrom dto -> TSubst q dto from to ->
|
||||
Elim q dto to
|
||||
subs e th ph = e /// th // ph
|
||||
|
||||
namespace ScopeTerm
|
||||
||| applies a term substitution with a less ambiguous type
|
||||
export
|
||||
(//.) : ScopeTerm d from -> TSubst d from to -> ScopeTerm d to
|
||||
(//.) : ScopeTerm q d from -> TSubst q d from to -> ScopeTerm q d to
|
||||
body //. th = body // th
|
||||
|
||||
||| applies a dimension substitution with the same behaviour as `(//)`
|
||||
||| above
|
||||
export
|
||||
(///) : ScopeTerm dfrom n -> DSubst dfrom dto -> ScopeTerm dto n
|
||||
(///) : ScopeTerm q dfrom n -> DSubst dfrom dto -> ScopeTerm q dto n
|
||||
TUsed body /// th = TUsed $ body /// th
|
||||
TUnused body /// th = TUnused $ body /// th
|
||||
|
||||
||| applies a term and dimension substitution
|
||||
public export %inline
|
||||
subs : ScopeTerm dfrom from -> DSubst dfrom dto -> TSubst dto from to ->
|
||||
ScopeTerm dto to
|
||||
subs : ScopeTerm q dfrom from -> DSubst dfrom dto -> TSubst q dto from to ->
|
||||
ScopeTerm q dto to
|
||||
subs body th ph = body /// th // ph
|
||||
|
||||
export CanShift (Term d) where s // by = s //. Shift by
|
||||
export CanShift (Elim d) where e // by = e //. Shift by
|
||||
export CanShift (ScopeTerm d) where s // by = s //. Shift by
|
||||
export CanShift (Term q d) where s // by = s //. Shift by
|
||||
export CanShift (Elim q d) where e // by = e //. Shift by
|
||||
export CanShift (ScopeTerm q d) where s // by = s //. Shift by
|
||||
|
||||
|
||||
export %inline
|
||||
comp' : DSubst dfrom dto -> TSubst dfrom from mid -> TSubst dto mid to ->
|
||||
TSubst dto from to
|
||||
comp' : DSubst dfrom dto -> TSubst q dfrom from mid -> TSubst q dto mid to ->
|
||||
TSubst q dto from to
|
||||
comp' th ps ph = map (/// th) ps . ph
|
||||
|
||||
|
||||
export
|
||||
fromDScopeTerm : DScopeTerm d n -> Term (S d) n
|
||||
fromDScopeTerm : DScopeTerm q d n -> Term q (S d) n
|
||||
fromDScopeTerm (DUsed body) = body
|
||||
fromDScopeTerm (DUnused body) = body /// shift 1
|
||||
|
||||
export
|
||||
fromScopeTerm : ScopeTerm d n -> Term d (S n)
|
||||
fromScopeTerm : ScopeTerm q d n -> Term q d (S n)
|
||||
fromScopeTerm (TUsed body) = body
|
||||
fromScopeTerm (TUnused body) = body //. shift 1
|
||||
|
|
|
|||
|
|
@ -4,48 +4,50 @@ import public Quox.Syntax
|
|||
import public Quox.Typing
|
||||
import public Quox.Equal
|
||||
import public Control.Monad.Either
|
||||
import Decidable.Decidable
|
||||
|
||||
%default total
|
||||
|
||||
|
||||
private covering %inline
|
||||
expectTYPE : MonadError Error m => Term d n -> m Universe
|
||||
expectTYPE : HasErr q m => Term q d n -> m Universe
|
||||
expectTYPE s =
|
||||
case (whnfT s).fst of
|
||||
TYPE l => pure l
|
||||
_ => throwError $ ExpectedTYPE s
|
||||
|
||||
private covering %inline
|
||||
expectPi : MonadError Error m => Term d n ->
|
||||
m (Qty, Term d n, ScopeTerm d n)
|
||||
expectPi : HasErr q m => Term q d n ->
|
||||
m (q, Term q d n, ScopeTerm q d n)
|
||||
expectPi ty =
|
||||
case (whnfT ty).fst of
|
||||
Pi qty _ arg res => pure (qty, arg, res)
|
||||
_ => throwError $ ExpectedPi ty
|
||||
|
||||
private %inline
|
||||
expectEqualQ : MonadError Error m =>
|
||||
(expect, actual : Qty) -> m ()
|
||||
expectEqualQ : HasErr q m => Eq q =>
|
||||
(expect, actual : q) -> m ()
|
||||
expectEqualQ pi rh =
|
||||
unless (pi == rh) $ throwError $ ClashQ pi rh
|
||||
|
||||
|
||||
private %inline
|
||||
popQ : MonadError Error m => Qty -> QOutput (S n) -> m (QOutput n)
|
||||
popQ : HasErr q m => Eq q => q -> QOutput q (S n) -> m (QOutput q n)
|
||||
popQ pi (qctx :< rh) = expectEqualQ pi rh $> qctx
|
||||
|
||||
|
||||
private %inline
|
||||
tail : TyContext d (S n) -> TyContext d n
|
||||
tail : TyContext q d (S n) -> TyContext q d n
|
||||
tail = {tctx $= tail, qctx $= tail}
|
||||
|
||||
|
||||
private %inline
|
||||
weakI : InferResult d n -> InferResult d (S n)
|
||||
weakI : IsQty q => InferResult q d n -> InferResult q d (S n)
|
||||
weakI = {type $= weakT, qout $= (:< zero)}
|
||||
|
||||
private
|
||||
lookupBound : {n : Nat} -> Qty -> Var n -> TyContext d n -> InferResult d n
|
||||
lookupBound : IsQty q =>
|
||||
{n : Nat} -> q -> Var n -> TyContext q d n -> InferResult q d n
|
||||
lookupBound pi VZ (MkTyContext {tctx = _ :< ty, _}) =
|
||||
InfRes {type = weakT ty, qout = zero :< pi}
|
||||
lookupBound pi (VS i) ctx =
|
||||
|
|
@ -53,18 +55,22 @@ lookupBound pi (VS i) ctx =
|
|||
|
||||
|
||||
private %inline
|
||||
subjMult : Qty -> Qty -> Subset Qty IsSubj
|
||||
subjMult sg qty =
|
||||
if sg == Zero || qty == Zero
|
||||
then Element Zero %search
|
||||
else Element One %search
|
||||
subjMult : IsQty q => (sg : SQty q) -> q -> SQty q
|
||||
subjMult (Element sg subj) qty =
|
||||
if isYes (isZero sg) || isYes (isZero qty)
|
||||
then Element zero zeroIsSubj
|
||||
else Element sg subj
|
||||
|
||||
|
||||
public export
|
||||
CanTC : (Type -> Type) -> Type
|
||||
CanTC m = (MonadError Error m, MonadReader Definitions m)
|
||||
0 CanTC' : (q : Type) -> (q -> Type) -> (Type -> Type) -> Type
|
||||
CanTC' q isGlobal m = (HasErr q m, MonadReader (Definitions' q isGlobal) m)
|
||||
|
||||
parameters {auto _ : CanTC m}
|
||||
public export
|
||||
0 CanTC : (q : Type) -> IsQty q => (Type -> Type) -> Type
|
||||
CanTC q = CanTC' q IsGlobal
|
||||
|
||||
parameters {auto _ : IsQty q} {auto _ : CanTC q m}
|
||||
mutual
|
||||
-- [todo] it seems like the options here for dealing with substitutions are
|
||||
-- to either push them or parametrise the whole typechecker over ambient
|
||||
|
|
@ -73,76 +79,78 @@ parameters {auto _ : CanTC m}
|
|||
|
||||
export covering %inline
|
||||
check : {d, n : Nat} ->
|
||||
(ctx : TyContext d n) -> (sg : Qty) -> (0 _ : IsSubj sg) =>
|
||||
(subj : Term d n) -> (ty : Term d n) ->
|
||||
m (CheckResult n)
|
||||
(ctx : TyContext q d n) -> (sg : SQty q) ->
|
||||
(subj : Term q d n) -> (ty : Term q d n) ->
|
||||
m (CheckResult q n)
|
||||
check ctx sg subj ty = check' ctx sg (pushSubstsT subj) ty
|
||||
|
||||
export covering %inline
|
||||
infer : {d, n : Nat} ->
|
||||
(ctx : TyContext d n) -> (sg : Qty) -> (0 _ : IsSubj sg) =>
|
||||
(subj : Elim d n) ->
|
||||
m (InferResult d n)
|
||||
(ctx : TyContext q d n) -> (sg : SQty q) ->
|
||||
(subj : Elim q d n) ->
|
||||
m (InferResult q d n)
|
||||
infer ctx sg subj = infer' ctx sg (pushSubstsE subj)
|
||||
|
||||
|
||||
export covering
|
||||
check' : {d, n : Nat} ->
|
||||
(ctx : TyContext d n) -> (sg : Qty) -> (0 _ : IsSubj sg) =>
|
||||
(subj : NotCloTerm d n) -> (ty : Term d n) ->
|
||||
m (CheckResult n)
|
||||
(ctx : TyContext q d n) -> (sg : SQty q) ->
|
||||
(subj : NotCloTerm q d n) -> (ty : Term q d n) ->
|
||||
m (CheckResult q n)
|
||||
|
||||
check' ctx sg (Element (TYPE l) _) ty = do
|
||||
l' <- expectTYPE ty
|
||||
expectEqualQ zero sg
|
||||
expectEqualQ zero sg.fst
|
||||
unless (l < l') $ throwError $ BadUniverse l l'
|
||||
pure zero
|
||||
|
||||
check' ctx sg (Element (Pi qty x arg res) _) ty = do
|
||||
l <- expectTYPE ty
|
||||
expectEqualQ zero sg
|
||||
ignore $ check ctx zero arg (TYPE l)
|
||||
expectEqualQ zero sg.fst
|
||||
ignore $ check ctx szero arg (TYPE l)
|
||||
case res of
|
||||
TUsed res => ignore $ check (extendTy arg zero ctx) zero res (TYPE l)
|
||||
TUnused res => ignore $ check ctx zero res (TYPE l)
|
||||
TUsed res =>
|
||||
ignore $ check (extendTy arg zero ctx) szero res (TYPE l)
|
||||
TUnused res =>
|
||||
ignore $ check ctx szero res (TYPE l)
|
||||
pure zero
|
||||
|
||||
check' ctx sg (Element (Lam x body) _) ty = do
|
||||
(qty, arg, res) <- expectPi ty
|
||||
-- [todo] do this properly?
|
||||
let body = fromScopeTerm body; res = fromScopeTerm res
|
||||
qout <- check (extendTy arg (sg * qty) ctx) sg body res
|
||||
qout <- check (extendTy arg (sg.fst * qty) ctx) sg body res
|
||||
popQ qty qout
|
||||
|
||||
check' ctx sg (Element (E e) _) ty = do
|
||||
infres <- infer ctx sg e
|
||||
ignore $ check ctx zero ty (TYPE UAny)
|
||||
ignore $ check ctx szero ty (TYPE UAny)
|
||||
subT infres.type ty
|
||||
pure infres.qout
|
||||
|
||||
export covering
|
||||
infer' : {d, n : Nat} ->
|
||||
(ctx : TyContext d n) -> (sg : Qty) -> (0 _ : IsSubj sg) =>
|
||||
(subj : NotCloElim d n) ->
|
||||
m (InferResult d n)
|
||||
(ctx : TyContext q d n) -> (sg : SQty q) ->
|
||||
(subj : NotCloElim q d n) ->
|
||||
m (InferResult q d n)
|
||||
|
||||
infer' ctx sg (Element (F x) _) = do
|
||||
Just g <- asks $ lookup x | Nothing => throwError $ NotInScope x
|
||||
when (isZero g) $ expectEqualQ sg Zero
|
||||
when (isZero g) $ expectEqualQ sg.fst zero
|
||||
pure $ InfRes {type = g.type.get, qout = zero}
|
||||
|
||||
infer' ctx sg (Element (B i) _) =
|
||||
pure $ lookupBound sg i ctx
|
||||
pure $ lookupBound sg.fst i ctx
|
||||
|
||||
infer' ctx sg (Element (fun :@ arg) _) = do
|
||||
funres <- infer ctx sg fun
|
||||
(qty, argty, res) <- expectPi funres.type
|
||||
let Element sg' _ = subjMult sg qty
|
||||
let sg' = subjMult sg qty
|
||||
argout <- check ctx sg' arg argty
|
||||
pure $ InfRes {type = fromScopeTerm res //. ((arg :# argty) ::: id),
|
||||
qout = funres.qout + argout}
|
||||
|
||||
infer' ctx sg (Element (tm :# ty) _) = do
|
||||
ignore $ check ctx zero ty (TYPE UAny)
|
||||
ignore $ check ctx szero ty (TYPE UAny)
|
||||
qout <- check ctx sg tm ty
|
||||
pure $ InfRes {type = ty, qout}
|
||||
|
|
|
|||
|
|
@ -6,6 +6,7 @@ import public Quox.Definition
|
|||
|
||||
import Data.Nat
|
||||
import public Data.SortedMap
|
||||
import Control.Monad.Either
|
||||
import Control.Monad.Reader
|
||||
import Control.Monad.State
|
||||
import Generics.Derive
|
||||
|
|
@ -24,71 +25,72 @@ data DContext : Nat -> Type where
|
|||
DEq : Dim d -> Dim d -> DContext d -> DContext d
|
||||
|
||||
public export
|
||||
TContext : Nat -> Nat -> Type
|
||||
TContext d = Context (Term d)
|
||||
TContext : Type -> Nat -> Nat -> Type
|
||||
TContext q d = Context (Term q d)
|
||||
|
||||
public export
|
||||
QContext : Nat -> Type
|
||||
QContext = Context' Qty
|
||||
QContext : Type -> Nat -> Type
|
||||
QContext = Context'
|
||||
|
||||
public export
|
||||
QOutput : Nat -> Type
|
||||
QOutput : Type -> Nat -> Type
|
||||
QOutput = QContext
|
||||
|
||||
|
||||
public export
|
||||
record TyContext (d, n : Nat) where
|
||||
record TyContext q d n where
|
||||
constructor MkTyContext
|
||||
dctx : DContext d
|
||||
tctx : TContext d n
|
||||
qctx : QContext n
|
||||
tctx : TContext q d n
|
||||
qctx : QContext q n
|
||||
|
||||
%name TyContext ctx
|
||||
|
||||
|
||||
namespace TContext
|
||||
export
|
||||
pushD : TContext d n -> TContext (S d) n
|
||||
pushD : TContext q d n -> TContext q (S d) n
|
||||
pushD tel = map (/// shift 1) tel
|
||||
|
||||
|
||||
namespace TyContext
|
||||
export
|
||||
extendTy : Term d n -> Qty -> TyContext d n -> TyContext d (S n)
|
||||
extendTy : Term q d n -> q -> TyContext q d n -> TyContext q d (S n)
|
||||
extendTy s rho = {tctx $= (:< s), qctx $= (:< rho)}
|
||||
|
||||
export
|
||||
extendDim : TyContext d n -> TyContext (S d) n
|
||||
extendDim : TyContext q d n -> TyContext q (S d) n
|
||||
extendDim = {dctx $= DBind, tctx $= pushD}
|
||||
|
||||
export
|
||||
eqDim : Dim d -> Dim d -> TyContext d n -> TyContext d n
|
||||
eqDim : Dim d -> Dim d -> TyContext q d n -> TyContext q d n
|
||||
eqDim p q = {dctx $= DEq p q}
|
||||
|
||||
|
||||
namespace QOutput
|
||||
export
|
||||
(+) : QOutput n -> QOutput n -> QOutput n
|
||||
(+) = zipWith (+)
|
||||
parameters {auto _ : IsQty q}
|
||||
export
|
||||
(+) : QOutput q n -> QOutput q n -> QOutput q n
|
||||
(+) = zipWith (+)
|
||||
|
||||
export
|
||||
(*) : Qty -> QOutput n -> QOutput n
|
||||
(*) pi = map (pi *)
|
||||
export
|
||||
(*) : q -> QOutput q n -> QOutput q n
|
||||
(*) pi = map (pi *)
|
||||
|
||||
export
|
||||
zero : {n : Nat} -> QOutput n
|
||||
zero = pure Zero
|
||||
export
|
||||
zero : {n : Nat} -> QOutput q n
|
||||
zero = pure zero
|
||||
|
||||
|
||||
public export
|
||||
CheckResult : Nat -> Type
|
||||
CheckResult : Type -> Nat -> Type
|
||||
CheckResult = QOutput
|
||||
|
||||
public export
|
||||
record InferResult d n where
|
||||
record InferResult q d n where
|
||||
constructor InfRes
|
||||
type : Term d n
|
||||
qout : QOutput n
|
||||
type : Term q d n
|
||||
qout : QOutput q n
|
||||
|
||||
|
||||
public export
|
||||
|
|
@ -97,12 +99,16 @@ data EqMode = Equal | Sub
|
|||
|
||||
|
||||
public export
|
||||
data Error
|
||||
= ExpectedTYPE (Term d n)
|
||||
| ExpectedPi (Term d n)
|
||||
data Error q
|
||||
= ExpectedTYPE (Term q d n)
|
||||
| ExpectedPi (Term q d n)
|
||||
| BadUniverse Universe Universe
|
||||
|
||||
| ClashT EqMode (Term d n) (Term d n)
|
||||
| ClashU EqMode Universe Universe
|
||||
| ClashQ Qty Qty
|
||||
| ClashT EqMode (Term q d n) (Term q d n)
|
||||
| ClashU EqMode Universe Universe
|
||||
| ClashQ q q
|
||||
| NotInScope Name
|
||||
|
||||
public export
|
||||
0 HasErr : Type -> (Type -> Type) -> Type
|
||||
HasErr q = MonadError (Error q)
|
||||
|
|
|
|||
|
|
@ -16,6 +16,7 @@ modules =
|
|||
Quox.Syntax.Dim,
|
||||
Quox.Syntax.DimEq,
|
||||
Quox.Syntax.Qty,
|
||||
Quox.Syntax.Qty.Three,
|
||||
Quox.Syntax.Shift,
|
||||
Quox.Syntax.Subst,
|
||||
Quox.Syntax.Term,
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
module TermImpls
|
||||
|
||||
import Quox.Syntax
|
||||
import Quox.Pretty
|
||||
import public Quox.Pretty
|
||||
|
||||
|
||||
private
|
||||
|
|
@ -22,7 +22,7 @@ eqSubst (_ ::: _) (Shift _) = Nothing
|
|||
|
||||
mutual
|
||||
export covering
|
||||
Eq (Term d n) where
|
||||
Eq q => Eq (Term q d n) where
|
||||
TYPE k == TYPE l = k == l
|
||||
TYPE _ == _ = False
|
||||
|
||||
|
|
@ -49,7 +49,7 @@ mutual
|
|||
DCloT {} == _ = False
|
||||
|
||||
export covering
|
||||
Eq (Elim d n) where
|
||||
Eq q => Eq (Elim q d n) where
|
||||
F x == F y = x == y
|
||||
F _ == _ = False
|
||||
|
||||
|
|
@ -75,16 +75,16 @@ mutual
|
|||
DCloE {} == _ = False
|
||||
|
||||
export covering
|
||||
Eq (ScopeTerm d n) where
|
||||
Eq q => Eq (ScopeTerm q d n) where
|
||||
TUsed s == TUsed t = s == t
|
||||
TUnused s == TUnused t = s == t
|
||||
TUsed _ == TUnused _ = False
|
||||
TUnused _ == TUsed _ = False
|
||||
|
||||
export covering
|
||||
Show (Term d n) where
|
||||
PrettyHL q => Show (Term q d n) where
|
||||
showPrec d t = showParens (d /= Open) $ prettyStr True t
|
||||
|
||||
export covering
|
||||
Show (Elim d n) where
|
||||
PrettyHL q => Show (Elim q d n) where
|
||||
showPrec d e = showParens (d /= Open) $ prettyStr True e
|
||||
|
|
|
|||
|
|
@ -2,10 +2,11 @@ module Tests.Equal
|
|||
|
||||
import Quox.Equal as Lib
|
||||
import Quox.Pretty
|
||||
import Quox.Syntax.Qty.Three
|
||||
import TAP
|
||||
|
||||
export
|
||||
ToInfo Error where
|
||||
ToInfo (Error Three) where
|
||||
toInfo (NotInScope x) =
|
||||
[("type", "NotInScope"),
|
||||
("name", show x)]
|
||||
|
|
@ -35,10 +36,11 @@ ToInfo Error where
|
|||
("right", prettyStr True rh)]
|
||||
|
||||
|
||||
M = ReaderT Definitions (Either Error)
|
||||
0 M : Type -> Type
|
||||
M = ReaderT (Definitions Three) (Either (Error Three))
|
||||
|
||||
parameters (label : String) (act : Lazy (M ()))
|
||||
{default empty globals : Definitions}
|
||||
{default empty globals : Definitions Three}
|
||||
testEq : Test
|
||||
testEq = test label $ runReaderT globals act
|
||||
|
||||
|
|
@ -46,19 +48,19 @@ parameters (label : String) (act : Lazy (M ()))
|
|||
testNeq = testThrows label (const True) $ runReaderT globals act
|
||||
|
||||
|
||||
subT : {default 0 d, n : Nat} -> Term d n -> Term d n -> M ()
|
||||
subT : {default 0 d, n : Nat} -> Term Three d n -> Term Three d n -> M ()
|
||||
subT = Lib.subT
|
||||
%hide Lib.subT
|
||||
|
||||
equalT : {default 0 d, n : Nat} -> Term d n -> Term d n -> M ()
|
||||
equalT : {default 0 d, n : Nat} -> Term Three d n -> Term Three d n -> M ()
|
||||
equalT = Lib.equalT
|
||||
%hide Lib.equalT
|
||||
|
||||
subE : {default 0 d, n : Nat} -> Elim d n -> Elim d n -> M ()
|
||||
subE : {default 0 d, n : Nat} -> Elim Three d n -> Elim Three d n -> M ()
|
||||
subE = Lib.subE
|
||||
%hide Lib.subE
|
||||
|
||||
equalE : {default 0 d, n : Nat} -> Elim d n -> Elim d n -> M ()
|
||||
equalE : {default 0 d, n : Nat} -> Elim Three d n -> Elim Three d n -> M ()
|
||||
equalE = Lib.equalE
|
||||
%hide Lib.equalE
|
||||
|
||||
|
|
|
|||
|
|
@ -1,6 +1,7 @@
|
|||
module Tests.Reduce
|
||||
|
||||
import Quox.Syntax as Lib
|
||||
import Quox.Syntax.Qty.Three
|
||||
import TermImpls
|
||||
import TAP
|
||||
|
||||
|
|
@ -22,17 +23,18 @@ testNoStep step label e = test "\{label} (no step)" $
|
|||
Right e' => with Prelude.(::) Left [("reduced", e')]
|
||||
|
||||
|
||||
|
||||
parameters {default 0 d, n : Nat}
|
||||
testWhnfT : String -> Term d n -> Term d n -> Test
|
||||
testWhnfT : String -> Term Three d n -> Term Three d n -> Test
|
||||
testWhnfT = testWhnf whnfT
|
||||
|
||||
testWhnfE : String -> Elim d n -> Elim d n -> Test
|
||||
testWhnfE : String -> Elim Three d n -> Elim Three d n -> Test
|
||||
testWhnfE = testWhnf whnfE
|
||||
|
||||
testNoStepE : String -> Elim d n -> Test
|
||||
testNoStepE : String -> Elim Three d n -> Test
|
||||
testNoStepE = testNoStep stepE
|
||||
|
||||
testNoStepT : String -> Term d n -> Test
|
||||
testNoStepT : String -> Term Three d n -> Test
|
||||
testNoStepT = testNoStep stepT
|
||||
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue