-
Notifications
You must be signed in to change notification settings - Fork 1
/
Scheme.idr
70 lines (56 loc) · 1.72 KB
/
Scheme.idr
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
module Scheme
import Data.Vect
import Data.String
import Data.SortedMap
import Derive.Prelude
import Language
%language ElabReflection
%default total
public export
data SchemeObj = Nil
| Symbol String
| ConsPair SchemeObj SchemeObj
| SymbolP | NilP | PairP
| Car | Cdr | Cons
| PartialCons SchemeObj
%runElab derive "SchemeObj" [Eq, Ord, Show]
export
FromString SchemeObj where
fromString = Symbol
export
FromChar SchemeObj where
fromChar = Symbol . String.singleton
export
Scheme : Language SchemeObj
Scheme = MkLanguage
([Nil, Car, Cdr, Cons] <+> letters)
$ SortedMap.fromList [("apply",
MkOperator 2 "apply"
$ \[op, arg] => !(denotation op) arg)]
where
symbolp : SchemeObj -> SchemeObj
symbolp (Symbol str) = 'T'
symbolp _ = Nil
nilp : SchemeObj -> SchemeObj
nilp [] = 'T'
nilp _ = Nil
pairp : SchemeObj -> SchemeObj
pairp (ConsPair _ _) = 'T'
pairp _ = Nil
car : SchemeObj -> Maybe SchemeObj
car (ConsPair a _) = Just a
car _ = Nothing
cdr : SchemeObj -> Maybe SchemeObj
cdr (ConsPair _ d) = Just d
cdr _ = Nothing
denotation : SchemeObj -> Maybe (SchemeObj -> Maybe SchemeObj)
denotation SymbolP = Just (Just . symbolp)
denotation NilP = Just (Just . nilp)
denotation PairP = Just (Just . pairp)
denotation Car = Just car
denotation Cdr = Just cdr
denotation Cons = Just (Just . PartialCons)
denotation (PartialCons a) = Just (Just . ConsPair a)
denotation _ = Nothing
letters : List SchemeObj
letters = fromChar <$> unpack "ABCDEFGHIJKLMNOPQRSTUVWXYZ"