msyds/rlp
1
0
Fork 0
Code Issues 4 Pull Requests Actions Packages Projects Releases 2 Wiki Activity

implement corePrelude in core language

Browse Source
This commit is contained in:
crumbtoo
2023-11-24 14:59:21 -07:00
parent 0b72bc8f11
commit ec87ed49f8
1 changed files with 21 additions and 15 deletions
Download Patch File Download Diff File Expand all files Collapse all files

26
src/Core/Examples.hs
View File

@@ -107,18 +107,24 @@ listExample3 = [coreProg|
|] |]
corePrelude :: Module corePrelude :: Module
corePrelude = Module (Just ("Prelude", [])) $ Program corePrelude = Module (Just ("Prelude", [])) $
[ ScDef "id" ["x"] $ "x" -- non-primitive defs
, ScDef "k" ["x", "y"] $ "x" [coreProg|
, ScDef "k1" ["x", "y"] $ "y" id x = x;
, ScDef "succ" ["f", "g", "x"] $ "f" :$ "x" :$ ("g" :$ "x") k x y = x;
, ScDef "compose" ["f", "g", "x"] $ "f" :$ ("g" :$ "x") k1 x y = y;
, ScDef "twice" ["f", "x"] $ "f" :$ ("f" :$ "x") succ f g x = f x (g x);
, ScDef "False" [] $ Con 0 0 compose f g x = f (g x);
twice f x = f (f x);
fst p = casePair# p k;
snd p = casePair# p k1;
|]
<>
-- primitive constructors need some specialised wiring:
Program
[ ScDef "False" [] $ Con 0 0
, ScDef "True" [] $ Con 1 0 , ScDef "True" [] $ Con 1 0
, ScDef "MkPair" [] $ Con 0 2 , ScDef "MkPair" [] $ Con 0 2
, ScDef "fst" ["p"] $ "casePair#" :$ "p" :$ "k"
, ScDef "snd" ["p"] $ "casePair#" :$ "p" :$ "k1"
, ScDef "Nil" [] $ Con 1 0 , ScDef "Nil" [] $ Con 1 0
, ScDef "Cons" [] $ Con 2 2 , ScDef "Cons" [] $ Con 2 2
] ]