From bf07a9fe3ee4ff06fe186e33221f7f91871b9217 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 6 Jun 2023 12:25:26 +0100
Subject: Write an encoding for data types.

---
 src/Level1.idr | 247 ---------------------------------------------------------
 1 file changed, 247 deletions(-)
 delete mode 100644 src/Level1.idr

(limited to 'src/Level1.idr')

diff --git a/src/Level1.idr b/src/Level1.idr
deleted file mode 100644
index d269eb6..0000000
--- a/src/Level1.idr
+++ /dev/null
@@ -1,247 +0,0 @@
-module Level1
-
-import Data.DPair
-import Data.SnocList.Elem
-import NormalForm
-import Term
-import Thinning
-
-%hide NormalForm.Normal
-
-data IsNormSubst : Subst ctx ctx' -> Type where
-  Base : IsNormSubst (Base thin)
-  (:<) : IsNormSubst sub -> IsNormal t -> IsNormSubst (sub :< t)
-
-%name IsNormSubst prf
-
-Normal : SnocList Ty -> Ty -> Type
-Normal ctx ty = Subset (Term ctx ty) IsNormal
-
-NormSubst : SnocList Ty -> SnocList Ty -> Type
-NormSubst ctx ctx' = Subset (Subst ctx ctx') IsNormSubst
-
-indexNormal : IsNormSubst sub -> (i : Elem ty ctx) -> IsNormal (index sub i)
-indexNormal Base i = Ntrl Var
-indexNormal (sub :< t) Here = t
-indexNormal (sub :< t) (There i) = indexNormal sub i
-
-index : NormSubst ctx' ctx -> Elem ty ctx -> Normal ctx' ty
-index sub i = Element (index (fst sub) i) (indexNormal (snd sub) i)
-
-restrictNormal : IsNormSubst sub -> (thin : ctx3 `Thins` ctx2) -> IsNormSubst (restrict sub thin)
-restrictNormal Base thin = Base
-restrictNormal (sub :< t) Id = sub :< t
-restrictNormal (sub :< t) (Drop thin) = restrictNormal sub thin
-restrictNormal (sub :< t) (Keep thin) = restrictNormal sub thin :< t
-
-restrict : NormSubst ctx1 ctx2 -> ctx3 `Thins` ctx2 -> NormSubst ctx1 ctx3
-restrict sub thin = Element (restrict (fst sub) thin) (restrictNormal (snd sub) thin)
-
-data Value : Type where
-  V : (ctx : SnocList Ty) -> (ty : Ty) -> Value
-  S : (ctx, ctx' : SnocList Ty) -> Value
-
-Raw : Value -> Type
-Raw (V ctx ty) = Term ctx ty
-Raw (S ctx ctx') = Subst ctx ctx'
-
-Norm : (a : Value) -> Raw a -> Type
-Norm (V _ _) = IsNormal
-Norm (S _ _) = IsNormSubst
-
-data Cont : Value -> Value -> Type where
-  EvalAbs1 : Term (ctx :< ty) ty' -> Cont (S (ctx' :< ty) ctx) (V ctx' (ty ~> ty'))
-  EvalAbs2 : Cont (V (ctx :< ty) ty') (V ctx (ty ~> ty'))
-  EvalApp1 : Term ctx ty -> NormSubst ctx' ctx -> Cont (V ctx' (ty ~> ty')) (V ctx' ty')
-  EvalApp2 : Normal ctx (ty ~> ty') -> Cont (V ctx ty) (V ctx ty')
-  EvalSucc1 : Cont (V ctx N) (V ctx N)
-  EvalRec1 :
-    Term ctx ty ->
-    Term (ctx :< ty) ty ->
-    NormSubst ctx' ctx ->
-    Cont (V ctx' N) (V ctx' ty)
-  EvalRec2 :
-    Normal ctx' N ->
-    Term (ctx :< ty) ty ->
-    NormSubst ctx' ctx ->
-    Cont (V ctx' ty) (V ctx' ty)
-  EvalRec3 :
-    Normal ctx' N ->
-    Normal ctx' ty ->
-    Term (ctx :< ty) ty ->
-    Cont (S (ctx' :< ty) ctx) (V ctx' ty)
-  EvalRec4 :
-    Normal ctx N ->
-    Normal ctx ty ->
-    Cont (V (ctx :< ty) ty) (V ctx ty)
-  EvalSub1 : Term ctx ty -> Cont (S ctx' ctx) (V ctx' ty)
-  EvalSnoc1 :
-    Term ctx ty ->
-    NormSubst ctx' ctx ->
-    Cont (S ctx' ctx'') (S ctx' (ctx'' :< ty))
-  EvalSnoc2 : NormSubst ctx' ctx -> Cont (V ctx' ty) (S ctx' (ctx :< ty))
-  RecSucc1 : Normal (ctx :< ty) ty -> Cont (V ctx ty) (V ctx ty)
-
-data Stack : Value -> Value -> Type where
-  Nil : Stack a a
-  (::) : Cont a b -> Stack b c -> Stack a c
-
-%name Cont k
-%name Stack stack
-
-data Case : Value -> Type where
-  Eval : Term ctx ty -> NormSubst ctx' ctx -> Case (V ctx' ty)
-  EvalSub : Subst ctx' ctx -> NormSubst ctx'' ctx' -> Case (S ctx'' ctx)
-  App : Normal ctx (ty ~> ty') -> Normal ctx ty -> Case (V ctx ty')
-  Rec : Normal ctx N -> Normal ctx ty -> Normal (ctx :< ty) ty -> Case (V ctx ty)
-  Run : Subset (Raw a) (Norm a) -> Case a
-
-%name Case c
-
-%prefix_record_projections off
-
-record Config (ret : Value) where
-  constructor On
-  {0 a : Value}
-  c : Case a
-  stack : Stack a ret
-
-data NotDone : Config ret -> Type where
-  EvalNotDone : NotDone (Eval t sub `On` stack)
-  EvalSubNotDone : NotDone (EvalSub sub sub' `On` stack)
-  AppNotDone : NotDone (App t u `On` stack)
-  RecNotDone : NotDone (Rec t u v `On` stack)
-  RunSomeNotDone : NotDone (Run x `On` step :: stack)
-
-step : (config : Config ret) -> {auto 0 _ : NotDone config} -> Config ret
-step (Eval (Var i) sub `On` stack) =
-  Run (index sub i) `On`
-  stack
-step (Eval (Abs t) sub `On` stack) =
-  EvalSub (fst sub) (Element (Base $ Drop Id) Base) `On`
-  EvalAbs1 t :: stack
-step (Eval (App t u) sub `On` stack) =
-  Eval t sub `On`
-  EvalApp1 u sub :: stack
-step (Eval Zero sub `On` stack) =
-  Run (Element Zero Zero) `On`
-  stack
-step (Eval (Succ t) sub `On` stack) =
-  Eval t sub `On`
-  EvalSucc1 :: stack
-step (Eval (Rec t u v) sub `On` stack) =
-  Eval t sub `On`
-  EvalRec1 u v sub :: stack
-step (Eval (Sub t sub') sub `On` stack) =
-  EvalSub sub' sub `On`
-  EvalSub1 t :: stack
-step (EvalSub (Base thin) sub' `On` stack) =
-  Run (restrict sub' thin) `On`
-  stack
-step (EvalSub (sub :< t) sub' `On` stack) =
-  EvalSub sub sub' `On`
-  EvalSnoc1 t sub' :: stack
-step (App (Element (Abs t) prf) u `On` stack) =
-  Eval t (Element (Base Id :< fst u) (Base :< snd u)) `On`
-  stack
-step (App (Element t@(Var _) prf) u `On` stack) =
-  Run (Element (App t (fst u)) (Ntrl $ App Var (snd u))) `On`
-  stack
-step (App (Element t@(App _ _) prf) u `On` stack) =
-  Run (Element (App t (fst u)) (Ntrl $ App (appNtrl prf) (snd u))) `On`
-  stack
-step (App (Element t@(Rec _ _ _) prf) u `On` stack) =
-  Run (Element (App t (fst u)) (Ntrl $ App (recNtrl prf) (snd u))) `On`
-  stack
-step (App (Element t@(Sub _ _) prf) u `On` stack) = void $ absurd prf
-step (Rec (Element Zero prf) u v `On` stack) =
-  Run u `On`
-  stack
-step (Rec (Element (Succ t) prf) u v `On` stack) =
-  Rec (Element t (predNorm prf)) u v `On`
-  RecSucc1 v :: stack
-step (Rec (Element t@(Var _) prf) u v `On` stack) =
-  Run (Element (Rec t (fst u) (fst v)) (Ntrl $ Rec Var (snd u) (snd v))) `On`
-  stack
-step (Rec (Element t@(App _ _) prf) u v `On` stack) =
-  Run (Element (Rec t (fst u) (fst v)) (Ntrl $ Rec (appNtrl prf) (snd u) (snd v))) `On`
-  stack
-step (Rec (Element t@(Rec _ _ _) prf) u v `On` stack) =
-  Run (Element (Rec t (fst u) (fst v)) (Ntrl $ Rec (recNtrl prf) (snd u) (snd v))) `On`
-  stack
-step (Rec (Element t@(Sub _ _) prf) u v `On` stack) = void $ absurd prf
-step (Run sub `On` EvalAbs1 t :: stack) =
-  Eval t (Element (fst sub :< Var Here) (snd sub :< Ntrl Var)) `On`
-  EvalAbs2 :: stack
-step (Run t `On` EvalAbs2 :: stack) =
-  Run (Element (Abs $ fst t) (Abs $ snd t)) `On`
-  stack
-step (Run t `On` EvalApp1 u sub :: stack) =
-  Eval u sub `On`
-  EvalApp2 t :: stack
-step (Run u `On` EvalApp2 t :: stack) =
-  App t u `On`
-  stack
-step (Run t `On` EvalSucc1 :: stack) =
-  Run (Element (Succ $ fst t) (Succ $ snd t)) `On`
-  stack
-step (Run t `On` EvalRec1 u v sub :: stack) =
-  Eval u sub `On`
-  EvalRec2 t v sub :: stack
-step (Run u `On` EvalRec2 t v sub :: stack) =
-  EvalSub (fst sub) (Element (Base $ Drop Id) Base) `On`
-  EvalRec3 t u v :: stack
-step (Run sub `On` EvalRec3 t u v :: stack) =
-  Eval v (Element (fst sub :< Var Here) (snd sub :< Ntrl Var)) `On`
-  EvalRec4 t u :: stack
-step (Run v `On` EvalRec4 t u :: stack) =
-  Rec t u v `On`
-  stack
-step (Run sub `On` EvalSub1 t :: stack) =
-  Eval t sub `On`
-  stack
-step (Run sub `On` EvalSnoc1 t sub' :: stack) =
-  Eval t sub' `On`
-  EvalSnoc2 sub :: stack
-step (Run t `On` EvalSnoc2 sub :: stack) =
-  Run (Element (fst sub :< fst t) (snd sub :< snd t)) `On`
-  stack
-step (Run val `On` RecSucc1 v :: stack) =
-  Eval (fst v) (Element (Base Id :< fst val) (Base :< snd val)) `On`
-  stack
-
-unwindStack : Raw a -> (stack : Stack a b) -> Raw b
-unwindStack x [] = x
-unwindStack sub (EvalAbs1 t :: stack) = unwindStack (Abs (Sub t (sub :< Var Here))) stack
-unwindStack t (EvalAbs2 :: stack) = unwindStack (Abs t) stack
-unwindStack t (EvalApp1 u sub :: stack) = unwindStack (App t (Sub u (fst sub))) stack
-unwindStack u (EvalApp2 t :: stack) = unwindStack (App (fst t) u) stack
-unwindStack t (EvalSucc1 :: stack) = unwindStack (Succ t) stack
-unwindStack t (EvalRec1 u v sub :: stack) =
-  unwindStack (Rec t (Sub u (fst sub)) (Sub v (Base (Drop Id) . fst sub :< Var Here))) stack
-unwindStack u (EvalRec2 t v sub :: stack) =
-  unwindStack (Rec (fst t) u (Sub v (Base (Drop Id) . fst sub :< Var Here))) stack
-unwindStack sub (EvalRec3 t u v :: stack) =
-  unwindStack (Rec (fst t) (fst u) (Sub v (sub :< Var Here))) stack
-unwindStack v (EvalRec4 t u :: stack) =
-  unwindStack (Rec (fst t) (fst u) v) stack
-unwindStack sub (EvalSub1 t :: stack) = unwindStack (Sub t sub) stack
-unwindStack sub (EvalSnoc1 t sub' :: stack) = unwindStack (sub :< Sub t (fst sub')) stack
-unwindStack t (EvalSnoc2 sub :: stack) = unwindStack (fst sub :< t) stack
-unwindStack val (RecSucc1 v :: stack) = unwindStack (Sub (fst v) (Base Id :< val)) stack
-
-unwind : Config a -> Raw a
-unwind (Eval t sub `On` stack) = unwindStack (Sub t $ fst sub) stack
-unwind (EvalSub sub sub' `On` stack) = unwindStack (fst sub' . sub) stack
-unwind (App t u `On` stack) = unwindStack (App (fst t) (fst u)) stack
-unwind (Rec t u v `On` stack) = unwindStack (Rec (fst t) (fst u) (fst v)) stack
-unwind (Run x `On` stack) = unwindStack (fst x) stack
-
-eval : Nat -> Config ret -> Raw ret
-eval 0 config = unwind config
-eval (S n) (Run x `On` []) = fst x
-eval (S n) config@(Run _ `On` _ :: _) = eval n (step config)
-eval (S n) config@(Eval _ _ `On` _) = eval n (step config)
-eval (S n) config@(EvalSub _ _ `On` _) = eval n (step config)
-eval (S n) config@(App _ _ `On` _) = eval n (step config)
-eval (S n) config@(Rec _ _ _ `On` _) = eval n (step config)
-- 
cgit v1.2.3