-
Notifications
You must be signed in to change notification settings - Fork 1
/
Template.language
160 lines (101 loc) · 4.69 KB
/
Template.language
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
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
# Hello! Welcome in the ALGT template/tutorial.
# Reading these comments will guide you through your first language
#
# Note that this tool is meant for programmers which have some experience, especially in the field of language design
# First of all, we start with imports. An imports you'll need practically every time, are the builtin values
# These contain some often used syntactic forms and functions to work with numbers (such as `plus`)
# Once you have some basic understandig of ALGT, you can head over to the source of this file and take a look to it
# You'll find it at: https://github.com/pietervdvn/ALGT2/blob/master/src/Assets/ALGT/Builtins.language
import ALGT.Builtins
# Next is the name of your language, followed by a line of stars:
Template
**********
# This is a template and tutorial language. Text that comes here is picked up by ALGT as documentation about your language
# Next, you'll want to declare the syntax of your language. This is done in a Syntax-section:
Syntax
========
# `a` is a simple example of an syntactic form
# Here, you define a simple syntactic form named 'a', which can be "T", can be "F", can be "(T)", "(F)", or even "(((T)))"
# Lines a whitespace insensitive by default, so `a` could be "(T )" or "(\tF )" as well
# Note that text above a syntactic form is considered documentation as well an can be queried from the REPL
a ::= "T" | "F" | "(" a ")"
# These are builtins offered by the import. You can remove this syntactic form
builtins ::= identifier | identifierUpper | string | unicodeChar
| upper | lower | digit | lineChar | wordChar
| number | integer
# If you don't want whitespace insensitivity by default, use `~~=` instead of `::=`
# This one would match `TT` and `TF`, but *not* `T T` or `T\tF`
whitespaceSensitiveLine ~~= a a
# This one does match `T T`
whitespaceInsensitiveLine ~~= a a
# A small language could contain following syntactic forms:
# A truth value
bool ::= "True" | "False"
# A value, which can be a bool or a number
value ::= bool
| integer # integer is defined within the builtins
# An expression, which is a value, an operator and another expression
expr ::= value "&" expr | value "+" expr | value "=" value | value
# The types that our language has
type ::= "Bool" | "Int"
Functions
===========
# Small helper functions go here. They serve to capture small reduction rules, which might be cumbersome to write as a full relation
# They start with the signature ( functionName ":" typeName "*" typeName "->" typeName)
# Clauses pattern match as in haskell
# As usual, the comments above a function count as docstring:
# The truth value resulting from the logical AND-operation
and : bool * bool -> bool
and("True", "True")
= "True"
and(_, _) = "False"
# Returns true if both arguments are the same
eqBool : bool * bool -> bool
eqBool("True", "True")
= "True"
eqBool("False", "False")
= "True"
eqBool(_, _) = "False"
# Compares two numbers for equality
eqInt : integer * integer -> bool
eqInt(i, i) = "True" # Here, we use the pattern matching to check for equality
eqInt(_, _) = "False"
# No plus for numbers, as this is a builtin function
Relations
============
# Next up are relations. Relations can be used for anything
# Most commonly, they are used for typecheckers and evaluators
# Here, relations are only declared.
# This is by giving a symbol between arrows, followed by what types it relates
# The mode `(in)` or `(out)` helps the algorithm. It is crucial to order the information flow through the rules
# Again, text above a rule is considered a docstring
# A single step in the evaluation
# (To produce → on linux: type Ctrl+U, release them, type 2192, press enter or space)
(→) : expr (in) * expr (out); Pronounced as "small step"
# Type the expression
(::) : expr (in) * type (out); Pronounced as "type as"
Rules
=======
# A rule is defined by dashes, followed by a rule name:
#
# -------------------- [Rule name goes here]
#
# Under the rule, a part of the relation is declared, e.g. that `a & b` will reduce to the logical AND of them: `and(a, b)`
#
# ---------------------[Eval And]
# (→) a "&" b, and(a, b)
# As we declared the first argument to be of mode in, this will be used as pattern match
# This can be seen in 
# Above the line, predicates can be given (seperated by tabs, not spaces):
a : bool b : bool
------------------------- [Eval And]
(→) a "&" b, and(a, b)
(::) a, "Bool" (::) b, "Bool"
-------------------------------------- [Type And]
(::) a "&" b, "Bool"
(::) a, "Int" (::) b, "Int"
-------------------------------------- [Type Plus]
(::) a "+" b, "Int"
(::) a, type (::) b, type
-------------------------------------- [Type Eq]
(::) a "=" b, type