From 11856fa96adeb35b73a360c11c4f260d81f270df Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sat, 25 Sep 2021 20:24:04 +0200
Subject: [PATCH] eval stuff

---
 src/Quox/Eval.idr | 134 ++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 129 insertions(+), 5 deletions(-)

diff --git a/src/Quox/Eval.idr b/src/Quox/Eval.idr
index ba1e892..e026814 100644
--- a/src/Quox/Eval.idr
+++ b/src/Quox/Eval.idr
@@ -2,11 +2,15 @@ module Quox.Eval
 
 -- todo list:
 -- - understand nbe and use it
--- - take a proof of well-typedness as an argument
+-- - take a proof of well-typedness as an argument,
+--   to reduce the number of eithers
+-- - remove the either if possible (should be???)
 
 import Quox.Syntax
+import Quox.Context
 
 import Data.DPair
+import Data.SortedMap
 
 %default total
 
@@ -14,17 +18,137 @@ import Data.DPair
 public export Exists2 : (ty1 -> ty2 -> Type) -> Type
 Exists2 t = Exists (\a => Exists (\b => t a b))
 
+parameters {0 t : ty -> Type}
+  private %inline some : t a -> Exists t
+  some t = Evidence _ t
+
+parameters {0 t : ty1 -> ty2 -> Type}
+  private %inline some2 : t a b -> Exists2 t
+  some2 t = some $ some t
+
+||| A term of some unknown scope sizes.
 public export SomeTerm : Type
 SomeTerm = Exists2 Term
 
+||| An elimination of some unknown scope sizes.
 public export SomeElim : Type
 SomeElim = Exists2 Elim
 
+||| A dimension of some unknown scope size.
 public export SomeDim : Type
 SomeDim = Exists Dim
 
-private some : {0 t : ty -> Type} -> t a -> Exists t
-some t = Evidence ? t
 
-private some2 : {0 t : ty1 -> ty2 -> Type} -> t a b -> Exists2 t
-some2 t = some $ some t
+public export
+record Global where
+  constructor G
+  val : forall d, n. NotCloElim d n
+
+public export Globals : Type
+Globals = SortedMap Name Global
+
+export (!!) : Globals -> Name -> Maybe (Elim d n)
+gs !! x = map (\g => g.val.fst) $ lookup x gs
+  -- just `map (fst . val)` fails?
+
+
+mutual
+  public export isValue : Term d n -> Bool
+  isValue (TYPE {})          = True
+  isValue (Pi {arg, res, _}) = isValue arg && isValue res
+  isValue (Lam {body, _})    = isValue body
+  isValue (E e)              = isNeutral e
+  isValue (CloT  {})         = False
+  isValue (DCloT {})         = False
+
+  public export isNeutral : Elim d n -> Bool
+  isNeutral (F {})       = False
+  isNeutral (B {})       = True
+  isNeutral (fun :@ arg) = isNeutral fun && isValue arg
+  isNeutral (_ :# _)     = False
+  isNeutral (CloE {})    = False
+  isNeutral (DCloE {})   = False
+
+public export IsValue : Term d n -> Type
+IsValue = So . isValue
+
+public export IsNeutral : Elim d n -> Type
+IsNeutral = So . isNeutral
+
+public export Value : Nat -> Nat -> Type
+Value d n = Subset (Term d n) IsValue
+
+public export Neutral : Nat -> Nat -> Type
+Neutral d n = Subset (Elim d n) IsNeutral
+
+public export valT : (t : Term d n) -> (0 _ : IsValue t) => Value d n
+valT t = Element t %search
+
+public export neuE : (e : Elim d n) -> (0 _ : IsNeutral e) => Neutral d n
+neuE e = Element e %search
+
+
+data EvalError =
+    NotInScope Name
+  | NonFunction SomeElim
+
+
+parameters (globals : Globals)
+  mutual
+    export covering %inline
+    evalT : Term d n -> Either EvalError (Value d n)
+    evalT = uncurry evalT' . pushSubstsT
+
+    export covering %inline
+    evalE : Elim d n -> Either EvalError (Neutral d n)
+    evalE = uncurry evalE' . pushSubstsE
+
+    export covering
+    evalT' : (t : Term d n) -> (0 prf : IsNotCloT t) ->
+             Either EvalError (Value d n)
+
+    export covering
+    evalE' : (e : Elim d n) -> (0 prf : IsNotCloE e) ->
+             Either EvalError (Neutral d n)
+
+
+public export
+data AlphaResult =
+    Ok
+  | Clash  SomeTerm SomeTerm
+  | DClash SomeDim  SomeDim
+  | QClash Qty      Qty
+
+export
+Semigroup AlphaResult where
+  Ok  <+> res = res
+  res <+> _   = res
+
+export Monoid AlphaResult where neutral = Ok
+
+private %inline clash : Term d1 n1 -> Term d2 n2 -> AlphaResult
+clash s t = Clash (some2 s) (some2 t)
+
+
+||| check two quantities are exactly equal and fail if not
+export %inline
+alphaQ : (pi, rh : Qty) -> AlphaResult
+alphaQ pi rh = if pi == rh then Ok else QClash pi rh
+
+export %inline
+alphaD : (al, be : Dim d) -> AlphaResult
+alphaD al be = if al == be then Ok else DClash (some al) (some be)
+
+mutual
+  private
+  alphaT : (s, t : Term d n) -> AlphaResult
+
+  private
+  alphaE : (e, f : Elim d n) -> AlphaResult
+
+
+export %inline alphaV : (u, v : Value d n) -> AlphaResult
+alphaV u v = alphaT u.fst v.fst
+
+export %inline alphaN : (p, q : Neutral d n) -> AlphaResult
+alphaN p q = alphaE p.fst q.fst