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

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
@@ -132,6 +138,7 @@ Located PTerm where
 export
 Located PCaseBody where
   (CasePair _ _     loc).loc = loc
+  (CaseW    _ _ _ _ loc).loc = loc
   (CaseEnum _       loc).loc = loc
   (CaseNat  _ _     loc).loc = loc
   (CaseBox  _ _     loc).loc = loc