From d926ce9f2d1144f329598a30b3ed2e48899519b2 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Wed, 9 Oct 2024 16:57:47 +0100
Subject: Write a System T to Primrose program.

---
 program/syst-to-primrose.prim | 77 +++++++++++++++++++++++++++++++++++++++++++
 program/syst-to-primrose.pty  | 41 +++++++++++++++++++++++
 2 files changed, 118 insertions(+)
 create mode 100644 program/syst-to-primrose.prim
 create mode 100644 program/syst-to-primrose.pty

(limited to 'program')

diff --git a/program/syst-to-primrose.prim b/program/syst-to-primrose.prim
new file mode 100644
index 0000000..8ba1e6a
--- /dev/null
+++ b/program/syst-to-primrose.prim
@@ -0,0 +1,77 @@
+let Prim =
+(\X =>
+  [ Var: Nat
+  , Lit: Nat
+  , Suc: X
+  , Abs: X
+  , App: <Fun: X, Arg: X>
+  , Unit: <>
+  , Pair: <Fst: X, Snd: X>
+  , Fst: X
+  , Snd: X
+  , Absurd: <Target: X>
+  , Inl: X
+  , Inr: X
+  , Case: <Target: X, Left: X, Right: X>
+  , Expand: X
+  , Contract: X
+  , Fold: <Target: X, Body: X>
+  , Let: <Bound: X, Body: X>
+  , Annot:
+    < Term: X
+    , Type: (\Y =>
+      [ Var: Nat
+      , N: <>
+      , Arrow: <Dom: Y, Cod: Y>
+      , Unit: <>
+      , Pair: <Fst: Y, Snd: Y>
+      , Bottom: <>
+      , Sum: <Left: Y, Right: Y>
+      , Fix: Y
+      ])
+    >
+  ])
+in
+let lift (f : Nat -> Nat) (x : Nat) : Nat =
+  case !x of
+    { Z u => 0
+    ; S n => suc (f n)
+    }
+in
+let rename (t : Prim) : (Nat -> Nat) -> Prim =
+  foldcase t by
+    { Var n => \f => ~(Var (f n))
+    ; Lit n => \f => ~(Lit n)
+    ; Suc t => \f => ~(Suc (t f))
+    ; Abs t => \f => ~(Abs (t (lift f)))
+    ; App p => \f => ~(App <Fun: p.Fun f, Arg: p.Arg f>)
+    ; Unit u => \f => ~(Unit u)
+    ; Pair p => \f => ~(Pair <Fst: p.Fst f, Snd: p.Snd f>)
+    ; Fst t => \f => ~(Fst (t f))
+    ; Snd t => \f => ~(Snd (t f))
+    ; Absurd p => \f => ~(Absurd <Target: p.Target f>)
+    ; Inl t => \f => ~(Inl (t f))
+    ; Inr t => \f => ~(Inr (t f))
+    ; Case p => \f => ~(Case <Target: p.Target f, Left: p.Left (lift f), Right: p.Right (lift f)>)
+    ; Expand t => \f => ~(Expand (t f))
+    ; Contract t => \f => ~(Contract (t f))
+    ; Fold p => \f => ~(Fold <Target: p.Target f, Body: p.Body (lift f)>)
+    ; Let p => \f => ~(Let <Bound: p.Bound f, Body: p.Body (lift f)>)
+    ; Annot p => \f => ~(Annot <Term: p.Term f, Type: p.Type>)
+    }
+in
+\p => foldcase p by
+  { Var n => ~(Var n)
+  ; Zero u => ~(Lit 0)
+  ; Suc e => ~(Suc e)
+  ; Abs e => ~(Abs e)
+  ; App p => ~(App p)
+  ; Rec p => ~(Fold
+      < Target: p.Target
+      , Body: ~(Case
+        < Target: ~(Var 0)
+        , Left: rename p.Zero (\x => suc (suc x))
+        , Right: rename p.Suc (lift suc)
+        >)
+      >)
+  }
diff --git a/program/syst-to-primrose.pty b/program/syst-to-primrose.pty
new file mode 100644
index 0000000..4030642
--- /dev/null
+++ b/program/syst-to-primrose.pty
@@ -0,0 +1,41 @@
+(\X =>
+  [ Var: Nat
+  , Zero: <>
+  , Suc: X
+  , Rec: <Target: X, Zero: X, Suc: X>
+  , Abs: X
+  , App: <Fun: X, Arg: X>
+  ])
+->
+(\X =>
+  [ Var: Nat
+  , Lit: Nat
+  , Suc: X
+  , Abs: X
+  , App: <Fun: X, Arg: X>
+  , Unit: <>
+  , Pair: <Fst: X, Snd: X>
+  , Fst: X
+  , Snd: X
+  , Absurd: <Target: X>
+  , Inl: X
+  , Inr: X
+  , Case: <Target: X, Left: X, Right: X>
+  , Expand: X
+  , Contract: X
+  , Fold: <Target: X, Body: X>
+  , Let: <Bound: X, Body: X>
+  , Annot:
+    < Term: X
+    , Type: (\Y =>
+      [ Var: Nat
+      , N: <>
+      , Arrow: <Dom: Y, Cod: Y>
+      , Unit: <>
+      , Pair: <Fst: Y, Snd: Y>
+      , Bottom: <>
+      , Sum: <Left: Y, Right: Y>
+      , Fix: Y
+      ])
+    >
+  ])
-- 
cgit v1.2.3