ref: 37c12e2cade08129c5004327aa0b9e4b231ab58e
parent: d4a9dd631f05e43868e457d00ebdf6d63397e433
parent: e1a569f2b532e6f37d1cb25a19a584814f89b59b
author: Lennart Augustsson <lennart.augustsson@epicgames.com>
date: Fri Oct 13 13:31:03 EDT 2023
Merge branch 'master' into class
--- a/comb/mhs.comb
+++ b/comb/mhs.comb
@@ -1,3 +1,3 @@
v4.0
-978
-((A :0 _862) ((A :1 ((B _908) _0)) ((A :2 (((S' _908) _0) I)) ((A :3 _832) ((A :4 (_3 "undefined")) ((A :5 I) ((A :6 (((C' B) _861) ((C _74) _5))) ((A :7 (((C' _6) (_879 _71)) ((_74 _877) _70))) ((A :8 ((B ((S _908) _877)) _3)) ((A :9 T) ((A :10 (T I)) ((A :11 ((B (_74 _188)) _10)) ((A :12 ((B (B (_73 _9))) (((C' B) ((B C) _10)) (B _10)))) ((A :13 ((B (B (_73 _9))) (((C' B) ((B C) _10)) (BK _10)))) ((A :14 ((B (_73 _9)) P)) ((A :15 ((B (B (_73 _9))) ((B ((C' C) _10)) (B P)))) ((A :16 _15) ((A :17 ((B (_73 _9)) (B (P _790)))) ((A :18 ((B (_73 _9)) (BK (P _790)))) ((A :19 ((_73 _9) ((S P) I))) ((A :20 ((B (_73 _9)) ((C (S' P)) I))) ((A :21 ((B Y) ((B (B (P (_14 _114)))) (((C' B) ((B (C' B)) (B _12))) (((C' (C' B)) (B _12)) ((B (B _14)) _115)))))) ((A :22 ((B Y) ((B (B (P (_14 _790)))) ((B (C' B)) (B _13))))) ((A :23 _3) ((A :24 (T (_14 _790))) ((A :25 (_21 _75)) ((A :26 ((C C) _33)) ((A :27 (T _32)) ((A :28 ((P _33) _32)) ((A :29 _33) ((A :30 ((C ((C S') _28)) I)) ((A :31 ((C S) _28)) ((A :32 K) ((A :33 A) ((A :34 _837) ((A :35 _838) ((A :36 (((S' _27) (_829 #97)) ((C _829) #122))) ((A :37 (((S' _27) (_829 #65)) ((C _829) #90))) ((A :38 (((S' _26) _36) _37)) ((A :39 (((S' _27) (_829 #48)) ((C _829) #57))) ((A :40 (((S' _27) (_829 #32)) ((C _829) #126))) ((A :41 _826) ((A :42 _827) ((A :43 _829) ((A :44 _828) ((A :45 (((S' _26) ((C _41) #32)) (((S' _26) ((C _41) #9)) ((C _41) #10)))) ((A :46 ((S ((S (((S' _27) (_43 #65)) ((C _43) #90))) (_33 (((_789 "lib/Data/Char.hs") #3) #8)))) ((B _34) (((C' _81) (((C' _82) _35) (_35 #65))) (_35 #97))))) ((A :47 ((S ((S (((S' _27) (_43 #97)) ((C _43) #97))) (_33 (((_789 "lib/Data/Char.hs") #3) #8)))) ((B _34) (((C' _81) (((C' _82) _35) (_35 #97))) (_35 #65))))) ((A :48 _797) ((A :49 _798) ((A :50 _799) ((A :51 _800) ((A :52 (_49 %0.0)) ((A :53 _48) ((A :54 _49) ((A :55 _50) ((A :56 _51) ((A :57 _801) ((A :58 _802) ((A :59 _57) ((A :60 _58) ((A :61 _803) ((A :62 _804) ((A :63 _805) ((A :64 _806) ((A :65 _61) ((A :66 _62) ((A :67 _63) ((A :68 _64) ((A :69 _807) ((A :70 ((B BK) T)) ((A :71 (BK T)) ((A :72 P) ((A :73 I) ((A :74 B) ((A :75 I) ((A :76 K) ((A :77 C) ((A :78 _833) ((A :79 ((C ((C S') _188)) _189)) ((A :80 (((C' (S' (C' B))) B) I)) ((A :81 _791) ((A :82 _792) ((A :83 _793) ((A :84 _794) ((A :85 _795) ((A :86 _796) ((A :87 (_82 #0)) ((A :88 _814) ((A :89 _815) ((A :90 _816) ((A :91 _817) ((A :92 _818) ((A :93 _819) ((A :94 _88) ((A :95 (BK K)) ((A :96 ((B BK) ((B (B BK)) P))) ((A :97 ((B (B (B BK))) ((B (B (B BK))) ((B (B (B C))) ((B (B C)) P))))) ((A :98 (((S' S) (((S' (S' C)) (((C' (C' S)) (((C' B) ((B (S' S')) (((C' B) ((B _26) (_91 #0))) (_88 #0)))) ((B (B ((C' P) (_86 #1)))) _81))) (C P))) _84)) _85)) ((A :99 _95) ((A :100 (((S' C) ((B (P _176)) (((C' (C' B)) (((C' C) _88) _176)) _177))) ((B ((C' (C' (C' C))) (((C' (C' (C' C))) (((C' (C' (C' (C' S')))) ((B (B (B (B C)))) ((B ((C' (C' (C' C))) ((B (B (B ((S' S') (_88 #0))))) ((B ((C' (C' C)) ((B (B ((S' S') (_88 #1)))) ((B ((C' C) ((B ((C' S') (_88 #2))) (C _100)))) (C _100))))) (C _100))))) (C _100)))) (T K))) (T A)))) ((C _98) #4)))) ((A :101 (_107 _76)) ((A :102 ((_122 (_79 _101)) _99)) ((A :103 ((C (((C' B) ((P _114) (((C' (C' O)) P) K))) (((S' (C' (C' (C' B)))) ((B (B (B (B _104)))) (((S' (C' (C' B))) ((B (B (B _104))) (((S' (C' B)) ((B (B _104)) (((C' B) ((B _120) (T #0))) _103))) (((C' B) ((B _120) (T #1))) _103)))) (((C' B) ((B _120) (T #2))) _103)))) (((C' B) ((B _120) (T #3))) _103)))) ((B T) ((B (B P)) ((C' _81) (_83 #4)))))) ((A :104 ((S S) ((B BK) ((B BK) (((S' S) T) ((B BK) ((B BK) ((C (((S' C') S) ((B (B (B (S B)))) ((B (B (B (B (B BK))))) ((B ((S' (C' B)) ((B B') B'))) ((B (B (B (B (B (S B)))))) ((B (B (B (B (B (B (B BK))))))) (((C' B) (B' (B' ((B (C' (C' (C' C)))) ((B ((C' B) (B' ((B C) _90)))) ((B ((C' B) _115)) _104)))))) ((B ((C' B) _115)) (C _104)))))))))) (((_789 "lib/Data/IntMap.hs") #3) #8))))))))) ((A :105 ((_74 (_120 _188)) _103)) ((A :106 (((C' C) (((C' C) (C _100)) (_3 "Data.IntMap.!"))) I)) ((A :107 ((B ((C' B) T)) ((B (B Y)) (((C' (C' (S' (S' C)))) ((B ((S' B) ((B (S' P)) (C _96)))) ((B (B ((C' (
\ No newline at end of file
+979
+((A :0 _863) ((A :1 ((B _909) _0)) ((A :2 (((S' _909) _0) I)) ((A :3 _833) ((A :4 (_3 "undefined")) ((A :5 I) ((A :6 (((C' B) _862) ((C _74) _5))) ((A :7 (((C' _6) (_880 _71)) ((_74 _878) _70))) ((A :8 ((B ((S _909) _878)) _3)) ((A :9 T) ((A :10 (T I)) ((A :11 ((B (_74 _189)) _10)) ((A :12 ((B (B (_73 _9))) (((C' B) ((B C) _10)) (B _10)))) ((A :13 ((B (B (_73 _9))) (((C' B) ((B C) _10)) (BK _10)))) ((A :14 ((B (_73 _9)) P)) ((A :15 ((B (B (_73 _9))) ((B ((C' C) _10)) (B P)))) ((A :16 _15) ((A :17 ((B (_73 _9)) (B (P _791)))) ((A :18 ((B (_73 _9)) (BK (P _791)))) ((A :19 ((_73 _9) ((S P) I))) ((A :20 ((B (_73 _9)) ((C (S' P)) I))) ((A :21 ((B Y) ((B (B (P (_14 _114)))) (((C' B) ((B (C' B)) (B _12))) (((C' (C' B)) (B _12)) ((B (B _14)) _115)))))) ((A :22 ((B Y) ((B (B (P (_14 _791)))) ((B (C' B)) (B _13))))) ((A :23 _3) ((A :24 (T (_14 _791))) ((A :25 (_21 _75)) ((A :26 (R _33)) ((A :27 (T _32)) ((A :28 ((P _33) _32)) ((A :29 _33) ((A :30 ((C ((C S') _28)) I)) ((A :31 ((C S) _28)) ((A :32 K) ((A :33 A) ((A :34 _838) ((A :35 _839) ((A :36 (((S' _27) (_830 #97)) ((C _830) #122))) ((A :37 (((S' _27) (_830 #65)) ((C _830) #90))) ((A :38 (((S' _26) _36) _37)) ((A :39 (((S' _27) (_830 #48)) ((C _830) #57))) ((A :40 (((S' _27) (_830 #32)) ((C _830) #126))) ((A :41 _827) ((A :42 _828) ((A :43 _830) ((A :44 _829) ((A :45 (((S' _26) ((C _41) #32)) (((S' _26) ((C _41) #9)) ((C _41) #10)))) ((A :46 ((S ((S (((S' _27) (_43 #65)) ((C _43) #90))) (_33 (((_790 "lib/Data/Char.hs") #3) #8)))) ((B _34) (((C' _81) (((C' _82) _35) (_35 #65))) (_35 #97))))) ((A :47 ((S ((S (((S' _27) (_43 #97)) ((C _43) #97))) (_33 (((_790 "lib/Data/Char.hs") #3) #8)))) ((B _34) (((C' _81) (((C' _82) _35) (_35 #97))) (_35 #65))))) ((A :48 _798) ((A :49 _799) ((A :50 _800) ((A :51 _801) ((A :52 (_49 %0.0)) ((A :53 _48) ((A :54 _49) ((A :55 _50) ((A :56 _51) ((A :57 _802) ((A :58 _803) ((A :59 _57) ((A :60 _58) ((A :61 _804) ((A :62 _805) ((A :63 _806) ((A :64 _807) ((A :65 _61) ((A :66 _62) ((A :67 _63) ((A :68 _64) ((A :69 _808) ((A :70 ((B BK) T)) ((A :71 (BK T)) ((A :72 P) ((A :73 I) ((A :74 B) ((A :75 I) ((A :76 K) ((A :77 C) ((A :78 _834) ((A :79 ((C ((C S') _189)) _190)) ((A :80 (((C' (S' (C' B))) B) I)) ((A :81 _792) ((A :82 _793) ((A :83 _794) ((A :84 _795) ((A :85 _796) ((A :86 _797) ((A :87 (_82 #0)) ((A :88 _815) ((A :89 _816) ((A :90 _817) ((A :91 _818) ((A :92 _819) ((A :93 _820) ((A :94 _88) ((A :95 (BK K)) ((A :96 ((B BK) ((B (B BK)) P))) ((A :97 ((B (B (B BK))) ((B (B (B BK))) ((B (B (B C))) ((B (B C)) P))))) ((A :98 (((S' S) (((S' (S' C)) (((C' (C' S)) (((C' B) ((B (S' S')) (((C' B) ((B _26) (_91 #0))) (_88 #0)))) ((B (B ((C' P) (_86 #1)))) _81))) (C P))) _84)) _85)) ((A :99 _95) ((A :100 (((S' C) ((B (P _177)) (((C' (C' B)) (((C' C) _88) _177)) _178))) ((B ((C' (C' (C' C))) (((C' (C' (C' C))) (((C' (C' (C' (C' S')))) ((B (B (B (B C)))) ((B ((C' (C' (C' C))) ((B (B (B ((S' S') (_88 #0))))) ((B ((C' (C' C)) ((B (B ((S' S') (_88 #1)))) ((B ((C' C) ((B ((C' S') (_88 #2))) (C _100)))) (C _100))))) (C _100))))) (C _100)))) (T K))) (T A)))) ((C _98) #4)))) ((A :101 (_107 _76)) ((A :102 ((_122 (_79 _101)) _99)) ((A :103 ((C (((C' B) ((P _114) (((C' (C' O)) P) K))) (((S' (C' (C' (C' B)))) ((B (B (B (B _104)))) (((S' (C' (C' B))) ((B (B (B _104))) (((S' (C' B)) ((B (B _104)) (((C' B) ((B _120) (T #0))) _103))) (((C' B) ((B _120) (T #1))) _103)))) (((C' B) ((B _120) (T #2))) _103)))) (((C' B) ((B _120) (T #3))) _103)))) ((B T) ((B (B P)) ((C' _81) (_83 #4)))))) ((A :104 ((S S) ((B BK) ((B BK) (((S' S) T) ((B BK) ((B BK) ((C (((S' C') S) ((B (B (B (S B)))) ((B (B (B (B (B BK))))) ((B ((S' (C' B)) ((B B') B'))) ((B (B (B (B (B (S B)))))) ((B (B (B (B (B (B (B BK))))))) (((C' B) (B' (B' ((B (C' (C' (C' C)))) ((B ((C' B) (B' ((B C) _90)))) ((B ((C' B) _115)) _104)))))) ((B ((C' B) _115)) (C _104)))))))))) (((_790 "lib/Data/IntMap.hs") #3) #8))))))))) ((A :105 ((_74 (_120 _189)) _103)) ((A :106 (((C' C) (((C' C) (C _100)) (_3 "Data.IntMap.!"))) I)) ((A :107 ((B ((C' B) T)) ((B (B Y)) (((C' (C' (S' (S' C)))) ((B ((S' B) ((B (S' P)) (C _96)))) ((B (B ((C' (S' C
\ No newline at end of file
--- a/lib/Data/List.hs
+++ b/lib/Data/List.hs
@@ -315,3 +315,6 @@
anySameBy :: forall a . (a -> a -> Bool) -> [a] -> Bool
anySameBy _ [] = False
anySameBy eq (x:xs) = elemBy eq x xs || anySameBy eq xs
+
+iterate :: forall a . (a -> a) -> a -> [a]
+iterate f x = x : iterate f (f x)
--- a/src/MicroHs/Exp.hs
+++ b/src/MicroHs/Exp.hs
@@ -1,8 +1,10 @@
{-# OPTIONS_GHC -Wno-unused-imports #-}+{-# LANGUAGE PatternSynonyms #-}-- Copyright 2023 Lennart Augustsson
-- See LICENSE file for full license.
module MicroHs.Exp(
compileOpt,
+-- compileOptX,
substExp,
Exp(..), showExp, eqExp, toStringP,
PrimOp,
@@ -22,6 +24,27 @@
type PrimOp = String
+--
+-- Used combinators
+-- * indicates that the implementation uses an indirection
+-- + indicates allocation in the implementation
+-- S x y z = x z (y z) +
+-- K x y = x *
+-- I x = x *
+-- B x y z = x (y z) +
+-- C x y z = x z y +
+-- S' x y z w = x (y w) (z w) +
+-- B' x y z w = x y (z w) +
+-- C' x y z w = x (y w) z +
+-- A x y = y *
+-- T x y = y x
+-- n@(Y x) = x n
+-- BK x y z = x y
+-- P x y z = z x y +
+-- R x y z = y z x +
+-- O x y z w = w x y +
+--
+
data Exp
= Var Ident
| App Exp Exp
@@ -103,6 +126,9 @@
cP :: Exp
cP = Lit (LPrim "P")
+--cR :: Exp
+--cR = Lit (LPrim "R")
+
{-eqExp :: Exp -> Exp -> Bool
eqExp ae1 ae2 =
@@ -255,6 +281,8 @@
cCC e1 e2 e3
else if isC bc && isI e1 then
app2 cP e2 e3
+-- else if isC bc && isC e1 then
+-- app2 cR e2 e3
else
r
@@ -273,6 +301,7 @@
cC (App (App CB e1) e2) e3 = cCC e1 e2 e3 -- C (B e1 e2) e3 = C' e1 e2 e3
cC (Var op) e2 | Just op' <- lookup op flipOps = App (Var op') e2 -- C op e = flip-op e
cC (App (App CC CI) e2) e3 = app2 CP e2 e3
+cC (App (App CC CC) e2) e3 = app2 CR e2 e3
cC e1 e2 = app2 CC e1 e2
-}
@@ -365,6 +394,8 @@
Lit (LPrim "T")
else if isB ff && isB aa then
Lit (LPrim "B'")
+ else if isC ff && isC aa then
+ Lit (LPrim "R")
else
let
def =
@@ -449,6 +480,7 @@
--------
-- Possible additions
--
+-- Added:
-- R = C C
-- R x y z = (C C x y) z = C y x z = y z x
--
@@ -484,3 +516,82 @@
-- C'C x y z w = C' C x y z w = C (x z) y w = x z w y
+---------------------------------------------------------------
+
+{-+data Peano = S Peano | Z
+ --Xderiving (Show)
+data DB = N Peano | L DB | A DB DB | Free Ident | K Lit
+ --Xderiving (Show)
+
+index :: Ident -> [Ident] -> Maybe Peano
+index x xs = lookupBy eqIdent x $ zip xs $ iterate S Z
+
+deBruijn :: Exp -> DB
+deBruijn = go [] where
+ go binds e =
+ case e of
+ Var x -> maybe (Free x) N $ index x binds
+ App t u -> A (go binds t) (go binds u)
+ Lam x t -> L $ go (x:binds) t
+ Lit l -> K l
+
+type CL = Exp
+type BCL = ([Bool], CL)
+
+com :: String -> Exp
+com s = Lit (LPrim s)
+(@@) :: Exp -> Exp -> Exp
+(@@) f a = App f a
+
+convertBool :: (BCL -> BCL -> CL) -> DB -> BCL
+convertBool (#) ee =
+ case ee of
+ N Z -> (True:[], com "I")
+ N (S e) -> (False:g, d) where (g, d) = rec $ N e
+ L e -> case rec e of
+ ([], d) -> ([], com "K" @@ d)
+ (False:g, d) -> (g, ([], com "K") # (g, d))
+ (True:g, d) -> (g, d)
+ A e1 e2 -> (zipWithDefault False (||) g1 g2, t1 # t2) where
+ t1@(g1, _) = rec e1
+ t2@(g2, _) = rec e2
+ Free s -> ([], Var s)
+ K l -> ([], Lit l)
+ where rec = convertBool (#)
+
+optEta :: DB -> BCL
+optEta = convertBool (#) where
+ (#) ([], d1) {- # -} ([], d2) = d1 @@ d2+ (#) ([], d1) {- # -} (True:[], Lit (LPrim "I")) = d1+ (#) ([], d1) {- # -} (True:g2, d2) = ([], com "B" @@ d1) # (g2, d2)+ (#) ([], d1) {- # -} (False:g2, d2) = ([], d1) # (g2, d2)+ (#) (True:[], Lit (LPrim "I")) {- # -} ([], d2) = com "T" @@ d2+ (#) (True:[], Lit (LPrim "I")) {- # -} (False:g2, d2) = ([], com "T") # (g2, d2)+ (#) (True:g1, d1) {- # -} ([], d2) = ([], com "R" @@ d2) # (g1, d1)+ (#) (True:g1, d1) {- # -} (True:g2, d2) = (g1, ([], com "S") # (g1, d1)) # (g2, d2)+ (#) (True:g1, d1) {- # -} (False:g2, d2) = (g1, ([], com "C") # (g1, d1)) # (g2, d2)+ (#) (False:g1, d1) {- # -} ([], d2) = (g1, d1) # ([], d2)+ (#) (False:_g1, d1) {- # -} (True:[], Lit (LPrim "I")) = d1+ (#) (False:g1, d1) {- # -} (True:g2, d2) = (g1, ([], com "B") # (g1, d1)) # (g2, d2)+ (#) (False:g1, d1) {- # -} (False:g2, d2) = (g1, d1) # (g2, d2)+
+zipWithDefault :: forall a b . a -> (a -> a -> b) -> [a] -> [a] -> [b]
+zipWithDefault d f [] ys = map (f d) ys
+zipWithDefault d f xs [] = map (flip f d) xs
+zipWithDefault d f (x:xt) (y:yt) = f x y : zipWithDefault d f xt yt
+
+compileOptX :: Exp -> Exp
+compileOptX = snd . optEta . deBruijn
+-}
+
+---------
+--
+-- C C x y z = C y x z = y z x
+-- C C == R
+-- R x y z = y z x
+--
+-- R True False x = False x True = K x A = x A
+-- not x = R True False x =
+-- False = K
+-- True = A
--- a/src/runtime/eval.c
+++ b/src/runtime/eval.c
@@ -147,7 +147,7 @@
#define ERR(s) do { fprintf(stderr, "ERR: %s\n", s); exit(1); } while(0) enum node_tag { T_FREE, T_IND, T_AP, T_INT, T_DOUBLE, T_HDL, T_S, T_K, T_I, T_B, T_C,- T_A, T_Y, T_SS, T_BB, T_CC, T_P, T_O, T_T, T_BK, T_ADD, T_SUB, T_MUL,
+ T_A, T_Y, T_SS, T_BB, T_CC, T_P, T_R, T_O, T_T, T_BK, T_ADD, T_SUB, T_MUL,
T_QUOT, T_REM, T_SUBR, T_UQUOT, T_UREM,
T_FADD, T_FSUB, T_FMUL, T_FDIV,
T_FEQ, T_FNE, T_FLT, T_FLE, T_FGT, T_FGE, T_FSHOW, T_FREAD,
@@ -632,6 +632,7 @@
{ "A", T_A }, { "S'", T_SS }, { "P", T_P },+ { "R", T_R }, { "I", T_I }, { "S", T_S }, { "T", T_T },@@ -1364,6 +1365,7 @@
case T_T: fprintf(f, "T"); break;
case T_Y: fprintf(f, "Y"); break;
case T_P: fprintf(f, "P"); break;
+ case T_R: fprintf(f, "R"); break;
case T_O: fprintf(f, "O"); break;
case T_SS: fprintf(f, "S'"); break;
case T_BB: fprintf(f, "B'"); break;
@@ -1808,6 +1810,7 @@
case T_C: GCCHECK(1); CHKARG3; GOAP(new_ap(x, z), y); /* C x y z = x z y */
case T_CC: GCCHECK(2); CHKARG4; GOAP(new_ap(x, new_ap(y, w)), z); /* C' x y z w = x (y w) z */
case T_P: GCCHECK(1); CHKARG3; GOAP(new_ap(z, x), y); /* P x y z = z x y */
+ case T_R: GCCHECK(1); CHKARG3; GOAP(new_ap(y, z), x); /* R x y z = y z x */
case T_O: GCCHECK(1); CHKARG4; GOAP(new_ap(w, x), y); /* O x y z w = w x y */
case T_ADD: ARITHBIN(+);
--
⑨