From d9bc68446fe0cdf81b359e4fd33a8cf293e836dd Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Fri, 10 Mar 2023 21:52:29 +0100
Subject: [PATCH] more fromparser stuff

---
 lib/Quox/Parser/Syntax.idr  | 14 ++++--
 lib/Quox/Syntax/Dim.idr     | 12 ++---
 lib/Quox/Syntax/Var.idr     |  4 +-
 tests/TermImpls.idr         | 25 ++++------
 tests/Tests.idr             |  4 +-
 tests/Tests/FromPTerm.idr   | 93 +++++++++++++++++++++++++++++++++++++
 tests/Tests/Typechecker.idr |  9 +++-
 7 files changed, 130 insertions(+), 31 deletions(-)
 create mode 100644 tests/Tests/FromPTerm.idr

diff --git a/lib/Quox/Parser/Syntax.idr b/lib/Quox/Parser/Syntax.idr
index 126c962..c3cee48 100644
--- a/lib/Quox/Parser/Syntax.idr
+++ b/lib/Quox/Parser/Syntax.idr
@@ -176,6 +176,7 @@ data FromPTermError =
   | DuplicatesInEnum (List TagVal)
   | DimNotInScope Name
   | QtyNotGlobal PQty
+  | DimNameInTerm Name
 
 public export
 FromPTerm : (Type -> Type) -> Type
@@ -204,6 +205,11 @@ fromPDimWith : FromPTerm m =>
 fromPDimWith ds (K e) = pure $ K e
 fromPDimWith ds (V i) = fromBaseName (pure . B) (throwError . DimNotInScope) ds i
 
+private
+avoidDim : FromPTerm m => Context' BName d -> Name -> m (Term q d n)
+avoidDim ds x =
+  fromName (const $ throwError $ DimNameInTerm x) (pure . FT) ds x
+
 
 mutual
   export
@@ -263,7 +269,7 @@ mutual
       map E $ (:%) <$> fromPTermElim ds ns s <*> fromPDimWith ds p
 
     V x =>
-      fromName (pure . E . B) (pure . FT) ns x
+      fromName (pure . E . B) (avoidDim ds) ns x
 
     s :# a =>
       map E $ (:#) <$> fromPTermWith ds ns s <*> fromPTermWith ds ns a
@@ -315,9 +321,9 @@ fromPTerm = fromPTermWith [<] [<]
 
 export
 globalPQty : FromPTerm m => (q : PQty) -> m (IsGlobal q)
-globalPQty Zero = pure GZero
-globalPQty One  = throwError $ QtyNotGlobal One
-globalPQty Any  = pure GAny
+globalPQty pi = case isGlobal pi of
+  Yes y => pure y
+  No  n => throwError $ QtyNotGlobal pi
 
 
 -- [todo] extend substitutions so they can do this injection. that's the sort of
diff --git a/lib/Quox/Syntax/Dim.idr b/lib/Quox/Syntax/Dim.idr
index 620903d..961e487 100644
--- a/lib/Quox/Syntax/Dim.idr
+++ b/lib/Quox/Syntax/Dim.idr
@@ -84,6 +84,12 @@ prettyDSubst th =
 
 public export FromVar Dim where fromVar = B
 
+
+export
+inject : Dim d -> Dim (d + inj)
+inject (K e) = K e
+inject (B i) = B $ inject i
+
 export
 CanShift Dim where
   K e // _  = K e
@@ -127,9 +133,3 @@ DecEq (Dim d) where
 public export %inline
 BV : (i : Nat) -> (0 _ : LT i d) => Dim d
 BV i = B $ V i
-
-
-export
-inject : {0 d' : Nat} -> Dim d -> Dim (d + d')
-inject (K e) = K e
-inject (B i) = B $ inject i
diff --git a/lib/Quox/Syntax/Var.idr b/lib/Quox/Syntax/Var.idr
index 95959fd..ef4197e 100644
--- a/lib/Quox/Syntax/Var.idr
+++ b/lib/Quox/Syntax/Var.idr
@@ -77,7 +77,7 @@ fromNatWith (S i) (LTESucc p) = VS $ fromNatWith i p
 
 public export %inline
 V : (i : Nat) -> {auto 0 p : i `LT` n} -> Var n
-V i {p} = fromNatWith i p
+V i = fromNatWith i p
 
 export %inline
 tryFromNat : Alternative f => (n : Nat) -> Nat -> f (Var n)
@@ -112,7 +112,7 @@ toFromNat (S k) (LTESucc x) = cong S $ toFromNat k x
 
 
 export
-inject : Var m -> Var (m + n)
+inject : Var m -> Var (m + inj)
 inject VZ     = VZ
 inject (VS i) = VS $ inject i
 
diff --git a/tests/TermImpls.idr b/tests/TermImpls.idr
index 116752d..a665870 100644
--- a/tests/TermImpls.idr
+++ b/tests/TermImpls.idr
@@ -25,13 +25,14 @@ mutual
     TYPE _ == _ = False
 
     Pi qty1 arg1 res1 == Pi qty2 arg2 res2 =
-      qty1 == qty2 && arg1 == arg2 && res1 == res2
+      qty1 == qty2 && arg1 == arg2 && res1.term == res2.term
     Pi {} == _ = False
 
-    Lam body1 == Lam body2 = body1 == body2
+    Lam body1 == Lam body2 = body1.term == body2.term
     Lam {} == _ = False
 
-    Sig fst1 snd1 == Sig fst2 snd2 = fst1 == fst2 && snd1 == snd2
+    Sig fst1 snd1 == Sig fst2 snd2 =
+      fst1 == fst2 && snd1.term == snd2.term
     Sig {} == _ = False
 
     Pair fst1 snd1 == Pair fst2 snd2 = fst1 == fst2 && snd1 == snd2
@@ -44,10 +45,10 @@ mutual
     Tag _ == _ = False
 
     Eq ty1 l1 r1 == Eq ty2 l2 r2 =
-      ty1 == ty2 && l1 == l2 && r1 == r2
+      ty1.term == ty2.term && l1 == l2 && r1 == r2
     Eq {} == _ = False
 
-    DLam body1 == DLam body2 = body1 == body2
+    DLam body1 == DLam body2 = body1.term == body2.term
     DLam {} == _ = False
 
     E e == E f = e == f
@@ -77,11 +78,11 @@ mutual
     (_ :@ _) == _ = False
 
     CasePair q1 p1 r1 b1 == CasePair q2 p2 r2 b2 =
-      q1 == q2 && p1 == p2 && r1 == r2 && b1 == b2
+      q1 == q2 && p1 == p2 && r1.term == r2.term && b1.term == b2.term
     CasePair {} == _ = False
 
     CaseEnum q1 t1 r1 a1 == CaseEnum q2 t2 r2 a2 =
-      q1 == q2 && t1 == t2 && r1 == r2 && a1 == a2
+      q1 == q2 && t1 == t2 && r1.term == r2.term && a1 == a2
     CaseEnum {} == _ = False
 
     (fun1 :% dim1) == (fun2 :% dim2) = fun1 == fun2 && dim1 == dim2
@@ -102,16 +103,6 @@ mutual
            Nothing   => False
     DCloE {} == _ = False
 
-  export covering
-  (forall n. Eq (f n)) => Eq (ScopedBody s f n) where
-    Y x == Y y = x == y
-    N x == N y = x == y
-    _   == _   = False
-
-  export covering
-  (forall n. Eq (f n)) => Eq (Scoped s f n) where
-    S _ x == S _ y = x == y
-
 export covering
 PrettyHL q => Show (Term q d n) where
   showPrec d t = showParens (d /= Open) $ prettyStr True t
diff --git a/tests/Tests.idr b/tests/Tests.idr
index bdd5124..c8c0ecf 100644
--- a/tests/Tests.idr
+++ b/tests/Tests.idr
@@ -6,6 +6,7 @@ import Tests.Equal
 import Tests.Typechecker
 import Tests.Lexer
 import Tests.Parser
+import Tests.FromPTerm
 import System
 
 
@@ -15,7 +16,8 @@ allTests = [
   Equal.tests,
   Typechecker.tests,
   Lexer.tests,
-  Parser.tests
+  Parser.tests,
+  FromPTerm.tests
 ]
 
 main : IO ()
diff --git a/tests/Tests/FromPTerm.idr b/tests/Tests/FromPTerm.idr
new file mode 100644
index 0000000..01d62b0
--- /dev/null
+++ b/tests/Tests/FromPTerm.idr
@@ -0,0 +1,93 @@
+module Tests.FromPTerm
+
+import Quox.Parser.Syntax
+import Quox.Parser
+import TermImpls
+import TAP
+
+import Derive.Prelude
+%language ElabReflection
+
+public export
+data Failure =
+    LexError Lexer.Error
+  | ParseError (List1 (ParsingError Token))
+  | FromPTermError FromPTermError
+  | WrongResult String
+  | ExpectedFail String
+
+%runElab derive "Syntax.FromPTermError" [Show]
+
+export
+ToInfo Failure where
+  toInfo (LexError err) =
+    [("type", "LexError"), ("info", show err)]
+  toInfo (ParseError errs) =
+    ("type", "ParseError") ::
+    map (bimap show show) ([1 .. length errs] `zip` toList errs)
+  toInfo (FromPTermError err) =
+    [("type", "FromPTermError"),
+     ("got", show err)]
+  toInfo (WrongResult got) =
+    [("type", "WrongResult"), ("got", got)]
+  toInfo (ExpectedFail got) =
+    [("type", "ExpectedFail"), ("got", got)]
+
+
+parameters {c : Bool} {auto _ : Show b}
+           (grm : Grammar c a) (fromP : a -> Either FromPTermError b)
+           (inp : String)
+  parameters {default (ltrim inp) label : String}
+    parsesWith : (b -> Bool) -> Test
+    parsesWith p = test label $ do
+      toks      <- mapFst LexError $ lex inp
+      (pres, _) <- mapFst ParseError $ parse (grm <* eof) toks
+      res       <- mapFst FromPTermError $ fromP pres
+      unless (p res) $ Left $ WrongResult $ show res
+
+    parses : Test
+    parses = parsesWith $ const True
+
+    parsesAs : Eq b => b -> Test
+    parsesAs exp = parsesWith (== exp)
+
+  parameters {default "\{ltrim inp}  # fails" label : String}
+    parseFails : Test
+    parseFails = test label $ do
+      toks      <- mapFst LexError $ lex inp
+      (pres, _) <- mapFst ParseError $ parse (grm <* eof) toks
+      either (const $ Right ()) (Left . ExpectedFail . show) $ fromP pres
+
+
+FromString BName where fromString = Just . fromString
+
+export
+tests : Test
+tests = "PTerm → Term" :- [
+  "dimensions" :-
+  let fromPDim = fromPDimWith [< "𝑖", "𝑗"]
+  in [
+    note "dim ctx: [𝑖, 𝑗]",
+    parsesAs dim fromPDim "𝑖" (BV 1),
+    parsesAs dim fromPDim "𝑗" (BV 0),
+    parseFails dim fromPDim "𝑘",
+    parsesAs dim fromPDim "0" (K Zero),
+    parsesAs dim fromPDim "1" (K One)
+  ],
+
+  "terms" :-
+  let fromPTerm' = fromPTermWith [< "𝑖", "𝑗"] [< "A", "x", "y", "z"]
+  in [
+    note "dim ctx: [𝑖, 𝑗]; term ctx: [A, x, y, z]",
+    parsesAs term fromPTerm' "x" $ BVT 2,
+    parseFails term fromPTerm' "𝑖",
+    parsesAs term fromPTerm' "f" $ FT "f",
+    parsesAs term fromPTerm' "λ w ⇒ w" $ ["w"] :\\ BVT 0,
+    parsesAs term fromPTerm' "λ w ⇒ x" $ ["w"] :\\ BVT 3,
+    parsesAs term fromPTerm' "λ x ⇒ x" $ ["x"] :\\ BVT 0,
+    parsesAs term fromPTerm' "λ a b ⇒ f a b" $
+      ["a", "b"] :\\ E (F "f" :@@ [BVT 1, BVT 0]),
+    parsesAs term fromPTerm' "f @𝑖" $
+      E $ F "f" :% BV 1
+  ]
+]
diff --git a/tests/Tests/Typechecker.idr b/tests/Tests/Typechecker.idr
index d139170..444d4ff 100644
--- a/tests/Tests/Typechecker.idr
+++ b/tests/Tests/Typechecker.idr
@@ -396,6 +396,13 @@ tests = "typechecker" :- [
           (Pi_ One "x" (FT "A")
             (Eq0 (E $ F "P" :@ BVT 0)
                  (E $ F "p" :@ BVT 0) (E $ F "q" :@ BVT 0)))
-          (Eq0 (Pi_ Any "x" (FT "A") $ E $ F "P" :@ BVT 0) (FT "p") (FT "q")))
+          (Eq0 (Pi_ Any "x" (FT "A") $ E $ F "P" :@ BVT 0) (FT "p") (FT "q"))),
+    todo "absurd (when coerce is in)"
+    -- absurd : (`true ≡ `false : {true, false}) ⇾ (0·A : ★₀) → A ≔
+    --   λ e ⇒
+    --     case coerce [i ⇒ case e @i return ★₀ of {`true ⇒ {tt}; `false ⇒ {}}]
+    --            @0 @1 `tt
+    --     return A
+    --     of { }
   ]
 ]