-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathhelp.ml
211 lines (211 loc) · 6.96 KB
/
help.ml
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
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
let help_text = [
" Chariot";
" =======";
"";
" A language with arbitrary nested inductive and coinductive types";
" ================================================================";
"";
"";
"Types";
"-----";
"";
"Types come in two flavors: strict/inductive or lazy/coinductive.";
"";
"A strict/inductive type is defined with";
" data tname(params)";
" where C1 : t0 -> t1 -> ... -> tn -> tname(params)";
" | C2 : ...";
" | ...";
"";
"Each Ci is a *constructor* and its type must end with tname(params).";
"(Each of the tj can also be tname(params) in order to define an";
"inductive type.)";
"";
"For example";
" data nat";
" where Zero : nat";
" | Succ : nat -> nat";
"";
" data list('a)";
" where Nil : list('a)";
" | Cons : 'a -> list('a) -> list('a)";
"";
" data empty";
" where";
" -- no constructor!";
"";
"";
"A lazy/coinductive type is defined with";
" codata tname(params)";
" where D1 : tname(params) -> t1 -> t2 -> ... -> tn";
" | D2 : ...";
" | ...";
"";
"Each Di is a *destructor* and its type must start with tname(params).";
"(Each of the tj can also be tname(params) in order to define a";
"coinductive type.)";
"There cannot be 'nullary' destructors D : tname(params).";
"";
"For example";
" codata stream('x)";
" where Head : stream('x) -> 'x";
" | Tail : stream('x) -> stream('x)";
"";
" codata prod('a,'b)";
" where Fst : prod('a,'b) -> 'a";
" | Snd : prod('a,'b) -> 'b";
"";
" codata one";
" where";
" -- no destructor!";
"";
" codata tree('b,'x) -- infinite trees branching on 'b with data in 'x";
" where Root : tree('b,'x) -> 'x";
" | Branch : tree('b,'x) -> 'b -> tree('b,'x)";
"";
"";
"Note: there can be at most one type with zero destructors (like 'one' above).";
"";
"";
"Note: to define a coinductive type with several 'constructors', we have";
"to define an auxiliary strict parametrized type:";
"";
" data colist_aux('x,'l)";
" where Nil : colist_aux('x,'l)";
" | Cons : 'x -> 'l -> colist_aux('x,'l)";
" codata colist('x)";
" where D : colist('x) -> colist_aux('x,colist('x))";
"";
"or";
"";
" data process_aux('p)";
" where End : process_aux('p)";
" | Out : nat -> process_aux('p)";
" | In : nat -> (nat -> 'p) -> process_aux('p)";
" codata process";
" where D : process -> process_aux(process)";
"";
"";
"Note: no two constructors / destructor may have the same name.";
"";
"";
"Note: comments are either";
" - single line comments started with '--'";
" - multiline comments delimited with '(*' and '*)'";
"";
"";
"Recursive Definitions";
"---------------------";
"";
"A definition is of the form";
" val f : t1 -> t2 -> ... -> tn";
" | clause0 = def0";
" | clause1 = def1";
" | ...";
"";
"Each clause is itself of the form";
" ((f cp ... cp).D cp ... cp).D ...";
"where each cp is a pattern (à la ML / Miranda).";
" cp ::= _ | var | C cp ... cp | { D = cp ; ... ; D = cp }";
"";
"Each def is a term:";
" term ::= var | (term) | term term | C | term.D | { D = term ; ... ; D = term }";
"";
"Some additionnal terms are";
" - ??? for a 'generic metavariable' (possibly shown as '✠' by the system)";
" - !!! for a 'generic looping term' (possibly show as 'Ω' by the system)";
"Those terms can take any type and differ only in how they behave during";
"evaluation / totality checking.";
" - ??? always terminates and the system assumes it decreases wrt to a parameter (optimistic)";
" - !!! always loops (pessimistic)";
"";
"";
"The type will be infered if not given. It is only necessary for";
"functions with 0 clause.";
"";
"For example:";
" val add n Zero = n";
" | add n (Succ m) = Succ (add n m)";
"";
" val bot : empty -> 'a";
"";
" val map : ('a -> 'b) -> list('a) -> list('b)";
" | map _ Nil = Nil";
" | map f (Cons x xs) = Cons (f x) (map f xs)";
"";
" val (map_stream f s).Head = f (s.Head)";
" | (map_stream f s).Tail = map_stream f (s.Tail)";
"";
" val branch : tree('b,'x) -> list('b) -> list('x)";
" | branch t Nil = t.Root";
" | branch t (Cons b bs) = Cons (t.Root) (branch (t.Branch b) bs)";
"";
"";
"Note that structures { D = ... ; ... ; D = ... } are never necessary and";
"can be replaced by auxiliary functions.";
"Structure are nevertheless necessary to avoid loosing too much";
"information for totality checking.";
"";
"";
"Syntactic sugar";
"---------------";
"";
"Several syntactic sugar are available:";
" - a decimal integer is expanded to Succ (Succ ... Zero)";
" - 'term + k' is expandend to Succ (Succ ... term)";
" - $ can be used for left-associative application";
" - a structure with a single label (destructor) D can be written as";
" with a #:";
" D # term instead of { D = term }";
" - lists can be given using Caml notation";
"";
" val fib 0 = 0";
" | fib 1 = 1";
" | fib (n+2) = add (fib (n+1)) (fib n)";
"";
" val rev_append [] l = l";
" | rev_append (x::xs) l = rev_append xs (x::l)";
"";
"";
"Toplevel and Commands";
"---------------------";
"";
"Each command to the toplevel needs to end with a ';' or a blank line.";
"";
"The top level interprets type definitions and recursive definitions and adds";
"them to the context.";
"";
"A single term given after the prompt is evaluated and the result is printed.";
"Structures are evaluated lazily and the system prints a 'hole' with a number:";
"";
" # arith 0 1;";
" >> term: arith 0 1";
" >> of type: stream(nat)";
" >> result: {";
" >> Head = <1> ;";
" >> Tail = <2> }";
"";
"Both <1> and <2> are such holes.";
"";
"To reduce them, we need to give the command";
"";
" # > 1,2";
"";
"If no hole is given, the system with evaluate all the holes...";
"";
"The other commands are";
" :help to display this help";
" :echo <string> to echo some statis message";
" :set to list the available options with their current value";
" :set <option> <value> to change the value of an optiond";
" :show <name> to show a function definition or a type definition";
" :show env to show the whole environment";
" :show types to show all the type definitions";
" :show functions to show all the recursive definitions";
" :reduce <term> to reduce a term and show the result";
" :type <term> to infer the type of a term and show the types of all its components";
" :unfold <term>, <depth> to reduce a term and unfold all its frozen components, up to a given depth";
" :quit to quit!";
"";
"";
]