From 0ecd9e608ced18f70f465c986d6519e8e95b0b6b Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Wed, 20 Nov 2024 15:31:25 +0000
Subject: Improve syntactic sugar.

Sugar makes programs nicer to write.
---
 program/exp.prim     |  2 +-
 program/reducer.prim | 33 +++++++++++++++------------------
 2 files changed, 16 insertions(+), 19 deletions(-)

(limited to 'program')

diff --git a/program/exp.prim b/program/exp.prim
index 3c07ec1..8af7c3f 100644
--- a/program/exp.prim
+++ b/program/exp.prim
@@ -1,3 +1,3 @@
-let add (x : Nat) (y : Nat) : Nat = foldcase x by {Z u => y; S k => ~(S k)} in
+let add (x : Nat) (y : Nat) : Nat = foldcase x by {Z u => y; S k => suc k} in
 let mul (x : Nat) (y : Nat) : Nat = foldcase x by {Z u => 0; S k => add y k} in
 \x, y => foldcase y by {Z u => 1; S k => mul x k}
diff --git a/program/reducer.prim b/program/reducer.prim
index ead7fbc..0a0517e 100644
--- a/program/reducer.prim
+++ b/program/reducer.prim
@@ -31,7 +31,7 @@ let index (xs : List SysT) : Nat -> SysT =
     ; C p => \k => case !k of {Z u => p.H; S k => p.T k}
     }
 in
-let shift = map (\X => List X) SysT SysT (\t => rename t suc) in
+let shift = map (\X => List X) SysT SysT (\t => rename t (\x => suc x)) in
 let sub (t : SysT) : List SysT -> SysT =
   foldcase t by
     { Var n => \env => index env n
@@ -40,22 +40,23 @@ let sub (t : SysT) : List SysT -> SysT =
     ; Primrec p => \env =>
       ~(Primrec
          < Zero: p.Zero env
-         , Suc: p.Suc ~(C <H: ~(Var 0), T: shift env>)
+         , Suc: p.Suc (cons ~(Var 0) (shift env))
          , Target: p.Target env
          >)
-    ; Abs f => \env => ~(Abs (f ~(C <H: ~(Var 0), T: shift env>)))
+    ; Abs f => \env => ~(Abs (f (cons ~(Var 0) (shift env))))
     ; App p => \env => ~(App <Fun: p.Fun env, Arg: p.Arg env>)
     }
 in
 let app (fun : SysT) (arg : SysT) (smaller : Bool) : Stepped =
-  let default : Stepped = <Term: ~(App <Fun: fun, Arg: arg>), Smaller: smaller>
+  let default : Stepped =
+    <Term: ~(App <Fun: fun, Arg: arg>), Smaller: smaller>
   in
   case !fun of
     { Var n => default
     ; Zero u => default
     ; Suc t => default
     ; Primrec p => default
-    ; Abs t => <Term: sub t ~(C <H: arg, T: ~(N <>)>), Smaller: T <>>
+    ; Abs t => <Term: sub t [arg], Smaller: T <>>
     ; App t => default
     }
 in
@@ -67,10 +68,7 @@ let rec (z : SysT) (s : SysT) (target : SysT) (smaller : Bool) : Stepped =
     { Var n => default
     ; Zero u => <Term: z, Smaller: T <>>
     ; Suc t =>
-      < Term:
-          sub s ~(C <H: ~(Primrec <Zero: z, Suc: s, Target: t>), T: ~(N <>)>)
-      , Smaller: T <>
-      >
+      <Term: sub s [~(Primrec <Zero: z, Suc: s, Target: t>)], Smaller: T <>>
     ; Primrec p => default
     ; Abs t => default
     ; App t => default
@@ -91,13 +89,13 @@ let step (t : SysT) : Stepped =
             (or t.Zero.Smaller t.Suc.Smaller)
         ; T u =>
           < Term:
-              ~(Primrec
-                 (map
-                   (\X => <Zero: X, Suc: X, Target: X>)
-                   Stepped
-                   SysT
-                   (\p => p.Term)
-                   t))
+            ~(Primrec
+               (map
+                 (\X => <Zero: X, Suc: X, Target: X>)
+                 Stepped
+                 SysT
+                 (\p => p.Term)
+                 t))
           , Smaller: T <>
           >
         }
@@ -107,8 +105,7 @@ let step (t : SysT) : Stepped =
         { F u => app t.Fun.Term t.Arg.Term t.Fun.Smaller
         ; T u =>
           < Term:
-              ~(App
-                 (map (\X => <Fun: X, Arg: X>) Stepped SysT (\p => p.Term) t))
+            ~(App (map (\X => <Fun: X, Arg: X>) Stepped SysT (\p => p.Term) t))
           , Smaller: T <>
           >
         }
-- 
cgit v1.2.3