From f2490f5ca35b528c7332791c6932045eb9d5438b Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Tue, 7 Jan 2025 13:50:13 +0000
Subject: Add quotation to help metaprogramming.

---
 program/reducer.prim | 50 +++++++++++++++++++++++++-------------------------
 1 file changed, 25 insertions(+), 25 deletions(-)

(limited to 'program/reducer.prim')

diff --git a/program/reducer.prim b/program/reducer.prim
index 0a0517e..3abbc97 100644
--- a/program/reducer.prim
+++ b/program/reducer.prim
@@ -1,16 +1,16 @@
-let Bool = [T: <>, F: <>] in
+let Bool = [T: <>; F: <>] in
 let or (x : Bool) (y : Bool) : Bool = case x of {T u => T <>; F u => y} in
 let SysT =
   (\T =>
     [ Var: Nat
-    , Zero: <>
-    , Suc: T
-    , Primrec: <Zero: T, Suc: T, Target: T>
-    , Abs: T
-    , App: <Fun: T, Arg: T>
+    ; Zero: <>
+    ; Suc: T
+    ; Primrec: <Zero: T; Suc: T; Target: T>
+    ; Abs: T
+    ; App: <Fun: T; Arg: T>
     ])
 in
-let Stepped = <Term: SysT, Smaller: Bool> in
+let Stepped = <Term: SysT; Smaller: Bool> in
 let lift (f : Nat -> Nat) (n : Nat) : Nat =
   case !n of {Z u => 0; S k => suc (f k)}
 in
@@ -20,9 +20,9 @@ let rename (t : SysT) : (Nat -> Nat) -> SysT =
     ; Zero u => \f => ~(Zero <>)
     ; Suc r => \f => ~(Suc (r f))
     ; Primrec p => \f =>
-      ~(Primrec <Zero: p.Zero f, Suc: p.Suc (lift f), Target: p.Target f>)
+      ~(Primrec <Zero: p.Zero f; Suc: p.Suc (lift f); Target: p.Target f>)
     ; Abs r => \f => ~(Abs (r f))
-    ; App p => \f => ~(App <Fun: p.Fun f, Arg: p.Arg f>)
+    ; App p => \f => ~(App <Fun: p.Fun f; Arg: p.Arg f>)
     }
 in
 let index (xs : List SysT) : Nat -> SysT =
@@ -40,35 +40,35 @@ let sub (t : SysT) : List SysT -> SysT =
     ; Primrec p => \env =>
       ~(Primrec
          < Zero: p.Zero env
-         , Suc: p.Suc (cons ~(Var 0) (shift env))
-         , Target: p.Target env
+         ; Suc: p.Suc (cons ~(Var 0) (shift env))
+         ; Target: p.Target env
          >)
     ; Abs f => \env => ~(Abs (f (cons ~(Var 0) (shift env))))
-    ; App p => \env => ~(App <Fun: p.Fun env, Arg: p.Arg 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>
+    <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 [arg], Smaller: T <>>
+    ; Abs t => <Term: sub t [arg]; Smaller: T <>>
     ; App t => default
     }
 in
 let rec (z : SysT) (s : SysT) (target : SysT) (smaller : Bool) : Stepped =
   let default : Stepped =
-    <Term: ~(Primrec <Zero: z, Suc: s, Target: target>), Smaller: smaller>
+    <Term: ~(Primrec <Zero: z; Suc: s; Target: target>); Smaller: smaller>
   in
   case !target of
     { Var n => default
-    ; Zero u => <Term: z, Smaller: T <>>
+    ; Zero u => <Term: z; Smaller: T <>>
     ; Suc t =>
-      <Term: sub s [~(Primrec <Zero: z, Suc: s, Target: t>)], Smaller: T <>>
+      <Term: sub s [~(Primrec <Zero: z; Suc: s; Target: t>)]; Smaller: T <>>
     ; Primrec p => default
     ; Abs t => default
     ; App t => default
@@ -76,9 +76,9 @@ let rec (z : SysT) (s : SysT) (target : SysT) (smaller : Bool) : Stepped =
 in
 let step (t : SysT) : Stepped =
   foldcase t by
-    { Var n => <Term: ~(Var n), Smaller: F <>>
-    ; Zero u => <Term: ~(Zero <>), Smaller: F <>>
-    ; Suc t => <Term: ~(Suc t.Term), Smaller: t.Smaller>
+    { Var n => <Term: ~(Var n); Smaller: F <>>
+    ; Zero u => <Term: ~(Zero <>); Smaller: F <>>
+    ; Suc t => <Term: ~(Suc t.Term); Smaller: t.Smaller>
     ; Primrec t =>
       case t.Target.Smaller of
         { F u =>
@@ -91,22 +91,22 @@ let step (t : SysT) : Stepped =
           < Term:
             ~(Primrec
                (map
-                 (\X => <Zero: X, Suc: X, Target: X>)
+                 (\X => <Zero: X; Suc: X; Target: X>)
                  Stepped
                  SysT
                  (\p => p.Term)
                  t))
-          , Smaller: T <>
+          ; Smaller: T <>
           >
         }
-    ; Abs t => <Term: ~(Abs t.Term), Smaller: t.Smaller>
+    ; Abs t => <Term: ~(Abs t.Term); Smaller: t.Smaller>
     ; App t =>
       case t.Arg.Smaller of
         { 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))
-          , Smaller: T <>
+            ~(App (map (\X => <Fun: X; Arg: X>) Stepped SysT (\p => p.Term) t))
+          ; Smaller: T <>
           >
         }
     }
-- 
cgit v1.2.3