~subsetpark/pantagruel-web

pantagruel-web/index.pant -rw-r--r-- 1.7 KiB
f1039a14 — Zach Smith Update meta name. 2 months ago
                                                                                
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
Thought.
Specification = [String].

// Pantagruel is a language for writing *system specifications*.

pantagruel thoughts: [Thought] => Specification.
---

// It's a computer language, but not as you might think of it.

// The effects of evaluating a specification are *nil*---Pantagruel has no execution semantics.

eval spec = null.

;

eval spec: Specification.
check spec: Specification => Bool.
---

// However, Pantagruel specifications can be checked to ensure that certain conditions have been met.

// For instance, that you've defined all your terms by the end of your document.
(all s <: invoked_symbols spec =>
	first_invoked_in_head? s spec -> bound_as_of? s (first_appearance s spec)
	and
	first_invoked_in_body? s spec -> bound_as_of? s (next_chapter (first_appearance s spec))) -> check spec.

;

(Head, Body) = [String].
Chapter = (Head, Body).
Specification = [Chapter].

// This allows a structured form of description where terms can be explained in gradually greater detail.

first_invoked_in_head? symbol: String, spec: Specification => Bool.
first_invoked_in_body? symbol: String, spec: Specification => Bool.

//

invoked_symbols spec: Specification => {String}.
first_appearance symbol: String, spec: Specification => Nat.

//

bound_as_of? symbol: String, position: Nat => Bool.

next_chapter n: Nat => Nat.
---

invoked_symbols spec =
	[all chapter <: spec, head_s <: (chapter 0) => head_s] +
	[all chapter <: spec, body_s <: (chapter 1) => body_s].

;

Expression.

// Specifications can also be type-checked to ensure that your logic is consistent.
type_checks? expr: Expression => Bool.
---

(all expr <: expressions spec => type_checks? expr) -> check spec.

;

expressions spec: Specification => [Expression].
---