summaryrefslogtreecommitdiff
path: root/program
diff options
context:
space:
mode:
Diffstat (limited to 'program')
-rw-r--r--program/reducer.prim123
-rw-r--r--program/reducer.pty17
-rw-r--r--program/syst-to-primrose.prim77
-rw-r--r--program/syst-to-primrose.pty41
4 files changed, 140 insertions, 118 deletions
diff --git a/program/reducer.prim b/program/reducer.prim
new file mode 100644
index 0000000..ead7fbc
--- /dev/null
+++ b/program/reducer.prim
@@ -0,0 +1,123 @@
+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>
+ ])
+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
+let rename (t : SysT) : (Nat -> Nat) -> SysT =
+ foldcase t by
+ { Var n => \f => ~(Var (f n))
+ ; 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>)
+ ; Abs r => \f => ~(Abs (r f))
+ ; App p => \f => ~(App <Fun: p.Fun f, Arg: p.Arg f>)
+ }
+in
+let index (xs : List SysT) : Nat -> SysT =
+ foldcase xs by
+ { N u => \k => ~(Var k)
+ ; 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 sub (t : SysT) : List SysT -> SysT =
+ foldcase t by
+ { Var n => \env => index env n
+ ; Zero u => \env => ~(Zero <>)
+ ; Suc f => \env => ~(Suc (f env))
+ ; Primrec p => \env =>
+ ~(Primrec
+ < Zero: p.Zero env
+ , Suc: p.Suc ~(C <H: ~(Var 0), T: shift env>)
+ , Target: p.Target env
+ >)
+ ; Abs f => \env => ~(Abs (f ~(C <H: ~(Var 0), T: 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>
+ 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 <>>
+ ; 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>
+ in
+ case !target of
+ { 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 <>
+ >
+ ; Primrec p => default
+ ; Abs t => default
+ ; App t => default
+ }
+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>
+ ; Primrec t =>
+ case t.Target.Smaller of
+ { F u =>
+ rec
+ t.Zero.Term
+ t.Suc.Term
+ t.Target.Term
+ (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))
+ , Smaller: T <>
+ >
+ }
+ ; 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 <>
+ >
+ }
+ }
+in
+\n =>
+ foldcase n by
+ { Z u => \t => t
+ ; S f => \t =>
+ let stepped = step t in
+ case stepped.Smaller of {F u => stepped.Term; T u => f stepped.Term}
+ }
diff --git a/program/reducer.pty b/program/reducer.pty
new file mode 100644
index 0000000..996541b
--- /dev/null
+++ b/program/reducer.pty
@@ -0,0 +1,17 @@
+Nat ->
+(\T =>
+ [ Var: Nat
+ , Zero: <>
+ , Suc: T
+ , Primrec: <Zero: T, Suc: T, Target: T>
+ , Abs: T
+ , App: <Fun: T, Arg: T>
+ ]) ->
+(\T =>
+ [ Var: Nat
+ , Zero: <>
+ , Suc: T
+ , Primrec: <Zero: T, Suc: T, Target: T>
+ , Abs: T
+ , App: <Fun: T, Arg: T>
+ ])
diff --git a/program/syst-to-primrose.prim b/program/syst-to-primrose.prim
deleted file mode 100644
index 8ba1e6a..0000000
--- a/program/syst-to-primrose.prim
+++ /dev/null
@@ -1,77 +0,0 @@
-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
deleted file mode 100644
index 4030642..0000000
--- a/program/syst-to-primrose.pty
+++ /dev/null
@@ -1,41 +0,0 @@
-(\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
- ])
- >
- ])
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 07:42:28 +0000