Write a fuelled reducer for System T.

6 files changed, 195 insertions, 133 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
-      ])
-    >
-  ])
diff --git a/src/Inky/Term/Pretty.idr b/src/Inky/Term/Pretty.idr
index 79e8f6c..1ff0de0 100644
--- a/src/Inky/Term/Pretty.idr
+++ b/src/Inky/Term/Pretty.idr
@@ -66,7 +66,9 @@ prettyAllTerm [] d = []
 prettyAllTerm (t :: ts) d = prettyTerm t d :: prettyAllTerm ts d
 
 prettyTermCtx [<] d = [<]
-prettyTermCtx (ts :< (l :- t)) d = prettyTermCtx ts d :< (pretty l <+> ":" <++> prettyTerm t d)
+prettyTermCtx (ts :< (l :- t)) d =
+  prettyTermCtx ts d :<
+  (group $ hang 2 $ pretty l <+> ":" <+> line <+> prettyTerm t d)
 
 prettyCases [<] = [<]
 prettyCases (ts :< (l :- (x ** Abs _ (bound ** t)))) =
@@ -89,11 +91,43 @@ prettyLet binding term =
   term
 
 lessPrettyTerm (Annot _ t a) d =
-  group $ align $ hang 2 $ parenthesise (d < Annot) $
-    prettyTerm t App <++> ":" <+> line <+> prettyType a Open
+  group $ align $ parenthesise (d < Annot) $
+    prettyTerm t App <+> line <+>
+    ":" <++> prettyType a Open
 lessPrettyTerm (Var _ i) d = pretty (unVal $ nameOf i)
+lessPrettyTerm (Let _ (Annot _ (Abs _ (bound ** e)) a) (x ** t)) d =
+  let (binds, cod, rest) = groupBinds bound a in
+  let binds = map (\x => parens (pretty x.name <++> ":" <++> prettyType x.value Open)) binds in
+  group $ align $ parenthesise (d < Open) $
+  prettyLet
+    ( (group $ hang 2 $ flatAlt
+        ( pretty x <+> line <+>
+          concatWith (surround line) binds <+> line <+>
+          ":" <++> prettyType cod Open
+        )
+        (pretty x <++> concatWith (<++>) binds <++> ":" <++> prettyType cod Open)
+      ) <++> "=" <+>
+      ( if null rest
+        then neutral
+        else neutral <++> "\\" <+> concatWith (surround $ "," <++> neutral) (map pretty rest) <++> "=>")
+      <+> line <+> prettyTerm e Open
+    )
+    (prettyTerm t Open)
+  where
+  groupBinds : List String -> Ty tyCtx -> (List (Assoc $ Ty tyCtx), Ty tyCtx, List String)
+  groupBinds [] a = ([], a, [])
+  groupBinds (x :: xs) (TArrow a b) =
+    let (binds, cod, rest) = groupBinds xs b in
+    ((x :- a) :: binds, cod, rest)
+  groupBinds xs a = ([], a, xs)
+lessPrettyTerm (Let _ (Annot _ e a) (x ** t)) d =
+  group $ align $ parenthesise (d < Open) $
+  prettyLet
+    ( pretty x <++> ":" <++> prettyType a Open <++> "=" <+> line <+>
+      prettyTerm e Open
+    )
+    (prettyTerm t Open)
 lessPrettyTerm (Let _ e (x ** t)) d =
-  -- TODO: pretty print annotated abstraction
   group $ align $ parenthesise (d < Open) $
   prettyLet
     (pretty x <++> "=" <+> line <+> prettyTerm e Open)
@@ -105,7 +139,7 @@ lessPrettyTerm (LetTy _ a (x ** t)) d =
     (prettyTerm t Open)
 lessPrettyTerm (Abs _ (bound ** t)) d =
   group $ hang 2 $ parenthesise (d < Open) $
-    "\\" <+> concatWith (surround $ "," <+> line) (map pretty bound) <++> "=>" <+> line <+>
+    "\\" <+> concatWith (surround $ "," <++> neutral) (map pretty bound) <++> "=>" <+> line <+>
     prettyTerm t Open
 lessPrettyTerm (App _ (Map _ (x ** a) b c) ts) d =
   group $ align $ hang 2 $ parenthesise (d < App) $
@@ -141,20 +175,26 @@ lessPrettyTerm (Case _ e (MkRow ts _)) d =
   let parts = prettyCases ts <>> [] in
   group $ align $ hang 2 $ parenthesise (d < Open) $
     (group $ hang (-2) $ "case" <++> prettyTerm e Open <+> line <+> "of") <+> line <+>
-    (braces $
-      flatAlt
-        (neutral <++> concatWith (surround $ line' <+> ";" <++> neutral) parts <+> line)
-        (concatWith (surround $ ";" <++> neutral) parts))
+    (braces $ flatAlt
+      (neutral <++> concatWith (surround $ line' <+> ";" <++> neutral) parts <+> line)
+      (concatWith (surround $ ";" <++> neutral) parts))
 lessPrettyTerm (Roll _ t) d =
   pretty "~" <+>
   parenthesise (d < Prefix) (group $ align $ hang 2 $ prettyTerm t Prefix)
 lessPrettyTerm (Unroll _ e) d =
   pretty "!" <+>
-  parenthesise (d > Prefix) (group $ align $ hang 2 $ prettyTerm e Prefix)
+  parenthesise (d < Prefix) (group $ align $ hang 2 $ prettyTerm e Prefix)
+lessPrettyTerm (Fold _ e ("__tmp" ** Case _ (Var _ ((%%) "__tmp" {pos = Here})) (MkRow ts _))) d =
+  let parts = prettyCases ts <>> [] in
+  -- XXX: should check for usage of "__tmp" in ts
+  group $ align $ hang 2 $ parenthesise (d < Open) $
+    (group $ hang (-2) $ "foldcase" <++> prettyTerm e Open <+> line <+> "by") <+> line <+>
+    (braces $ flatAlt
+      (neutral <++> concatWith (surround $ line' <+> ";" <++> neutral) parts <+> line)
+      (concatWith (surround $ ";" <++> neutral) parts))
 lessPrettyTerm (Fold _ e (x ** t)) d =
-  -- TODO: foldcase
   group $ align $ hang 2 $ parenthesise (d < Open) $
-    "fold" <++> prettyTerm e Open <++> "by" <+> hardline <+>
+    (group $ hang (-2) $ "fold" <++> prettyTerm e Open <++> "by") <+> line <+>
     (group $ align $ hang 2 $ parens $
       "\\" <+> pretty x <++> "=>" <+> line <+> prettyTerm t Open)
 lessPrettyTerm (Map _ (x ** a) b c) d =
diff --git a/src/Inky/Type/Pretty.idr b/src/Inky/Type/Pretty.idr
index ae80125..2785b87 100644
--- a/src/Inky/Type/Pretty.idr
+++ b/src/Inky/Type/Pretty.idr
@@ -55,13 +55,13 @@ lessPrettyType (TProd (MkRow as _)) d =
   let parts = lessPrettyTypeCtx as Open <>> [] in
   group $ align $ enclose "<" ">" $
     flatAlt
-      (neutral <++> concatWith (surround $ line' <+> "," <++> neutral) parts <+> line)
+      (neutral <++> concatWith (surround $ line <+> "," <++> neutral) parts <+> line)
       (concatWith (surround $ "," <++> neutral) parts)
 lessPrettyType (TSum (MkRow as _)) d =
   let parts = lessPrettyTypeCtx as Open <>> [] in
   group $ align $ enclose "[" "]" $
     flatAlt
-      (neutral <++> concatWith (surround $ line' <+> "," <++> neutral) parts <+> line)
+      (neutral <++> concatWith (surround $ line <+> "," <++> neutral) parts <+> line)
       (concatWith (surround $ "," <++> neutral) parts)
 lessPrettyType (TFix x a) d =
   group $ align $ hang 2 $ parens $
@@ -71,4 +71,4 @@ lessPrettyType (TFix x a) d =
 lessPrettyTypeCtx [<] d = [<]
 lessPrettyTypeCtx (as :< (x :- a)) d =
   lessPrettyTypeCtx as d :<
-  (group $ align $ hang 2 $ pretty x <+> ":" <+> line <+> prettyType a d)
+  (group $ align $ pretty x <+> ":" <+> line <+> prettyType a d)