From 3cebc7b9b27f5a496d34e045701927d15f18d7b5 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Tue, 8 Aug 2023 06:39:52 +0200
Subject: [PATCH] add W to parser syntax

---
 lib/Quox/Parser/FromParser.idr | 31 ++++++++++++++++++++++++-------
 lib/Quox/Parser/Syntax.idr     | 15 +++++++++++----
 2 files changed, 35 insertions(+), 11 deletions(-)

diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr
index 7ca26e5..4514245 100644
--- a/lib/Quox/Parser/FromParser.idr
+++ b/lib/Quox/Parser/FromParser.idr
@@ -150,6 +150,23 @@ mutual
     Pair s t loc =>
       Pair <$> fromPTermWith ds ns s <*> fromPTermWith ds ns t <*> pure loc
 
+    W x s t loc =>
+      W <$> fromPTermWith ds ns s
+        <*> fromPTermTScope ds ns [< x] t
+        <*> pure loc
+
+    Sup s t loc =>
+      Sup <$> fromPTermWith ds ns s
+          <*> fromPTermWith ds ns t
+          <*> pure loc
+
+    Case pi tree (r, ret) (CaseW x y (rh, ih) body _) loc =>
+      map E $ CaseW (fromPQty pi) (fromPQty rh)
+        <$> fromPTermElim ds ns tree
+        <*> fromPTermTScope ds ns [< r] ret
+        <*> fromPTermTScope ds ns [< x, y, ih] body
+        <*> pure loc
+
     Case pi pair (r, ret) (CasePair (x, y) body _) loc =>
       map E $ CasePair (fromPQty pi)
         <$> fromPTermElim ds ns pair
@@ -157,13 +174,6 @@ mutual
         <*> fromPTermTScope ds ns [< x, y] body
         <*> pure loc
 
-    Case pi tag (r, ret) (CaseEnum arms _) loc =>
-      map E $ CaseEnum (fromPQty pi)
-        <$> fromPTermElim ds ns tag
-        <*> fromPTermTScope ds ns [< r] ret
-        <*> assert_total fromPTermEnumArms ds ns arms
-        <*> pure loc
-
     Nat loc => pure $ Nat loc
     Zero loc => pure $ Zero loc
     Succ n loc => [|Succ (fromPTermWith ds ns n) (pure loc)|]
@@ -185,6 +195,13 @@ mutual
 
     Tag str loc => pure $ Tag str loc
 
+    Case pi tag (r, ret) (CaseEnum arms _) loc =>
+      map E $ CaseEnum (fromPQty pi)
+        <$> fromPTermElim ds ns tag
+        <*> fromPTermTScope ds ns [< r] ret
+        <*> assert_total fromPTermEnumArms ds ns arms
+        <*> pure loc
+
     Eq (i, ty) s t loc =>
       Eq <$> fromPTermDScope ds ns [< i] ty
          <*> fromPTermWith ds ns s
diff --git a/lib/Quox/Parser/Syntax.idr b/lib/Quox/Parser/Syntax.idr
index 335eb49..d08ab65 100644
--- a/lib/Quox/Parser/Syntax.idr
+++ b/lib/Quox/Parser/Syntax.idr
@@ -74,6 +74,9 @@ namespace PTerm
       | Pair PTerm PTerm Loc
       | Case PQty PTerm (PatVar, PTerm) PCaseBody Loc
 
+      | W PatVar PTerm PTerm Loc
+      | Sup PTerm PTerm Loc
+
       | Enum (List TagVal) Loc
       | Tag TagVal Loc
 
@@ -98,6 +101,7 @@ namespace PTerm
     public export
     data PCaseBody =
         CasePair (PatVar, PatVar) PTerm Loc
+      | CaseW PatVar PatVar (PQty, PatVar) PTerm Loc
       | CaseEnum (List (PTagVal, PTerm)) Loc
       | CaseNat PTerm (PatVar, PQty, PatVar, PTerm) Loc
       | CaseBox PatVar PTerm Loc
@@ -114,6 +118,8 @@ Located PTerm where
   (Sig  _ _ _         loc).loc = loc
   (Pair _ _           loc).loc = loc
   (Case _ _ _ _       loc).loc = loc
+  (W    _ _ _         loc).loc = loc
+  (Sup  _ _           loc).loc = loc
   (Enum _             loc).loc = loc
   (Tag  _             loc).loc = loc
   (Eq   _ _ _         loc).loc = loc
@@ -131,10 +137,11 @@ Located PTerm where
 
 export
 Located PCaseBody where
-  (CasePair _ _ loc).loc = loc
-  (CaseEnum _   loc).loc = loc
-  (CaseNat  _ _ loc).loc = loc
-  (CaseBox  _ _ loc).loc = loc
+  (CasePair _ _     loc).loc = loc
+  (CaseW    _ _ _ _ loc).loc = loc
+  (CaseEnum _       loc).loc = loc
+  (CaseNat  _ _     loc).loc = loc
+  (CaseBox  _ _     loc).loc = loc
 
 
 public export