impl: add more reductions to `normalOrderReduction`

diff --git a/src/Symantic/Semantics/Data.hs b/src/Symantic/Semantics/Data.hs
index 781a67f1365331fcfa79d1f486793ebe4725c53d..3016ed91b1fa880a6d4803d80dcf9565e7f2fc4c 100644 (file)
--- a/src/Symantic/Semantics/Data.hs
+++ b/src/Symantic/Semantics/Data.hs
@@ -108,26 +108,39 @@ normalOrderReduction ::
 normalOrderReduction = nor
   where
     nor :: SomeData sem b -> SomeData sem b
-    nor = \case
+    nor = expand Fun.$ \case
       Data (Lam f) -> lam (nor Fun.. f)
       Data (Lam1 f) -> lam1 (nor Fun.. f)
       Data (x :@ y) -> case whnf x of
         Data (Lam1 f) -> nor (f y)
         x' -> nor x' .@ nor y
-      Data (IfThenElse test ok ko) ->
-        case nor test of
-          Data (Constant b :: Data (Constantable Bool) sem Bool) ->
-            if b then nor ok else nor ko
-          t -> ifThenElse (nor t) (nor ok) (nor ko)
       x -> x
 
     whnf :: SomeData sem b -> SomeData sem b
-    whnf = \case
+    whnf = expand Fun.$ \case
       Data (x :@ y) -> case whnf x of
         Data (Lam1 f) -> whnf (f y)
         x' -> x' .@ y
       x -> x
 
+    expand :: (SomeData sem b -> SomeData sem b) -> SomeData sem b -> SomeData sem b
+    expand fct sd = fct Fun.$ case unSomeData sd of
+      Maybe.Just d -> case d of
+        Ap -> lam1 (\abc -> lam1 (\ab -> lam1 (\a -> abc .@ a .@ (ab .@ a))))
+        Const -> lam1 (\x -> lam1 (\_y -> x))
+        Id -> lam1 Fun.id
+        (:.) -> lam1 (\f -> lam1 (\g -> lam1 (\x -> f .@ (g .@ x))))
+        Flip -> lam1 (\f -> lam1 (\x -> lam1 (\y -> f .@ y .@ x)))
+        (:$) -> lam1 (\f -> lam1 (f .@))
+      Maybe.Nothing ->
+        case sd of
+          Data (IfThenElse test ok ko) ->
+            case nor test of
+              Data (Constant b :: Data (Constantable Bool) sem Bool) ->
+                if b then nor ok else nor ko
+              tst -> ifThenElse tst (nor ok) (nor ko)
+          _ -> sd
+
 -- Instantiable
 data instance Data Instantiable sem a where
   (:@) :: SomeData sem (a -> b) -> SomeData sem a -> Data Instantiable sem b

diff --git a/src/Symantic/Semantics/Viewer.hs b/src/Symantic/Semantics/Viewer.hs
index 5fb6d6bc5f18506c0582ce6aea5f74114f0546e0..a29af2cd12c0e703e903a5cf13e6504f9e2e1519 100644 (file)
--- a/src/Symantic/Semantics/Viewer.hs
+++ b/src/Symantic/Semantics/Viewer.hs
@@ -88,6 +88,21 @@ instance Abstractable Viewer where
                 }
     where
       op = infixN 0
+instance Abstractable1 Viewer where
+  lam1 f = Viewer Fun.$ \env ->
+    pairViewer env op Fun.$
+      let x = showString "u" Fun.. shows (viewEnv_lamDepth env)
+       in showString "\\"
+            Fun.. x
+            Fun.. showString " -> "
+            Fun.. runViewer
+              (f (Viewer (\_env -> x)))
+              env
+                { viewEnv_op = (op, SideL)
+                , viewEnv_lamDepth = Prelude.succ (viewEnv_lamDepth env)
+                }
+    where
+      op = infixN 0
 instance Instantiable Viewer where
   ViewerInfix op _name infixName .@ ViewerApp x y = Viewer Fun.$ \env ->
     pairViewer env op Fun.$
@@ -128,3 +143,6 @@ instance Listable Viewer where
 instance Maybeable Viewer where
   nothing = "Nothing"
   just = "Just"
+instance IfThenElseable Viewer where
+  ifThenElse test ok ko =
+    "if" .@ test .@ "then" .@ ok .@ "else" .@ ko