Define Declarative typing rules.

1 files changed, 148 insertions, 0 deletions

diff --git a/src/Core/Declarative.idr b/src/Core/Declarative.idr
new file mode 100644
index 0000000..2561797
--- /dev/null
+++ b/src/Core/Declarative.idr
@@ -0,0 +1,148 @@
+module Core.Declarative
+
+import Core.Context
+import Core.Name
+import Core.Term
+import Core.Term.Environment
+import Core.Term.Substitution
+import Core.Thinning
+import Core.Var
+
+import Data.Nat
+
+public export
+data EnvWf : Env sx -> Type
+public export
+data TypeWf : Env sx -> Term sx -> Type
+public export
+data TypeConv : Env sx -> Term sx -> Term sx -> Type
+public export
+data TermWf : Env sx -> Term sx -> Term sx -> Type
+public export
+data TermConv : Env sx -> Term sx -> Term sx -> Term sx -> Type
+
+data EnvWf where
+  Lin :
+    ---
+    EnvWf [<]
+  (:<) :
+    EnvWf env ->
+    TypeWf env a ->
+    ---
+    EnvWf (env :< a)
+
+data TypeWf where
+  SetType :
+    EnvWf env ->
+    ---
+    TypeWf env Set
+  PiType :
+    TypeWf env f ->
+    TypeWf (env :< f) g ->
+    ---
+    TypeWf env (Pi n f g)
+  LiftType :
+    TermWf env a Set ->
+    ---
+    TypeWf env a
+
+data TypeConv where
+  ReflType :
+    TypeWf env a ->
+    ---
+    TypeConv env a a
+  SymType :
+    TypeConv env a b ->
+    ---
+    TypeConv env b a
+  TransType :
+    TypeConv env a b ->
+    TypeConv env b c ->
+    ---
+    TypeConv env a c
+  PiTypeConv :
+    TypeWf env f ->
+    TypeConv env f h ->
+    TypeConv (env :< f) g e ->
+    ---
+    TypeConv env (Pi n f g) (Pi n h e)
+  LiftConv :
+    TermConv env a b Set ->
+    ---
+    TypeConv env a b
+
+data TermWf where
+  VarTerm :
+    EnvWf env ->
+    ---
+    TermWf env (Var i) (index env i)
+  PiTerm :
+    TermWf env f Set ->
+    TermWf (env :< f) g Set ->
+    ---
+    TermWf env (Pi n f g) Set
+  AbsTerm :
+    TypeWf env f ->
+    TermWf (env :< f) t g ->
+    ---
+    TermWf env (Abs n t) (Pi n f g)
+  AppTerm :
+    TermWf env t (Pi n f g) ->
+    TermWf env u f ->
+    ---
+    TermWf env (App t u) (subst g $ sub1 u)
+  ConvTerm :
+    TermWf env t a ->
+    TypeConv env a b ->
+    ---
+    TermWf env t b
+
+data TermConv where
+  ReflTerm :
+    TermWf env t a ->
+    ---
+    TermConv env t t a
+  SymTerm :
+    TermConv env t u a ->
+    ---
+    TermConv env u t a
+  TransTerm :
+    TermConv env t u a ->
+    TermConv env u v a ->
+    ---
+    TermConv env t v a
+  ConvTermConv :
+    TermConv env t u a ->
+    TypeConv env a b ->
+    ---
+    TermConv env t u b
+  PiTermConv :
+    TypeWf env f ->
+    TermConv env f h Set ->
+    TermConv (env :< f) g e Set ->
+    ---
+    TermConv env (Pi n f g) (Pi n h e) Set
+  PiBeta :
+    TypeWf env f ->
+    TermWf (env :< f) t g ->
+    TermWf env u f ->
+    ---
+    TermConv env (App (Abs n t) u) (subst t $ sub1 u) (subst g $ sub1 u)
+  PiEta :
+    TypeWf env f ->
+    TermWf env t (Pi n f g) ->
+    TermWf env u (Pi n f g) ->
+    TermConv (env :< f) (App (wkn t $ drop (id _) n) a) (App (wkn u $ drop (id _) n) a) g ->
+    ---
+    TermConv env t u (Pi n f g)
+  AppConv :
+    TermConv env t u (Pi n f g) ->
+    TermConv env a b f ->
+    ---
+    TermConv env (App t a) (App u b) (subst g $ sub1 a)
+
+%name EnvWf wf
+%name TypeWf wf
+%name TypeConv conv
+%name TermWf wf
+%name TermConv conv