diff options
author | Péter Diviánszky <divipp@gmail.com> | 2016-04-04 16:56:32 +0200 |
---|---|---|
committer | Péter Diviánszky <divipp@gmail.com> | 2016-04-04 16:56:32 +0200 |
commit | 3765e26fba68c8219b27fab9191ade7a845dddd7 (patch) | |
tree | 0eb8402a24074f77a1091f09d486f914ebf9af30 /doc/guide.pandoc | |
parent | a14705d13abf237c2e0a202612c3f600fa2a399f (diff) |
begin to document pattern match compilation
Diffstat (limited to 'doc/guide.pandoc')
-rw-r--r-- | doc/guide.pandoc | 141 |
1 files changed, 122 insertions, 19 deletions
diff --git a/doc/guide.pandoc b/doc/guide.pandoc index fb872712..9a4f8698 100644 --- a/doc/guide.pandoc +++ b/doc/guide.pandoc | |||
@@ -7,7 +7,7 @@ Main tasks of the compiler: | |||
7 | 7 | ||
8 | - find errors in source code | 8 | - find errors in source code |
9 | - code completion to avoid superfluous parts of source code | 9 | - code completion to avoid superfluous parts of source code |
10 | - eliminate abstractions (normalization, reduction) | 10 | - eliminate abstractions |
11 | 11 | ||
12 | Additional tasks of the compiler: | 12 | Additional tasks of the compiler: |
13 | 13 | ||
@@ -23,9 +23,10 @@ Additional tasks of the compiler: | |||
23 | 23 | ||
24 | Main design decisions | 24 | Main design decisions |
25 | 25 | ||
26 | - Semantics errors are ruled out by strong static typing. | 26 | - reuse Haskell syntax & semantics |
27 | - Use dependent types for more expressive power | 27 | - semantics errors are ruled out by strong static typing |
28 | - Use Haskell syntax & semantics with extensions | 28 | - code completion is done by type classes |
29 | - abstractions are eliminated by reduction | ||
29 | - Code generation is not part of the compiler; it is done during the reduction of the main expression. | 30 | - Code generation is not part of the compiler; it is done during the reduction of the main expression. |
30 | This helps to keep the compiler smaller and separate domain specific code. | 31 | This helps to keep the compiler smaller and separate domain specific code. |
31 | - The compiler has just two phases: | 32 | - The compiler has just two phases: |
@@ -284,6 +285,119 @@ Desugarer tasks | |||
284 | - desugar type classes and instances | 285 | - desugar type classes and instances |
285 | 286 | ||
286 | 287 | ||
288 | Pattern match compilation | ||
289 | ------------------------- | ||
290 | |||
291 | Main task: | ||
292 | |||
293 | - transform pattern matching and guards to case expressions | ||
294 | |||
295 | Other tasks: | ||
296 | |||
297 | - exhaustiveness check (is pattern matching total?) | ||
298 | - reachability check (are there superfluous expressions involved?) | ||
299 | - pattern guards desugaring | ||
300 | - view patterns desugaring | ||
301 | |||
302 | Design decisions: | ||
303 | |||
304 | - The same algorithm is used with different parameters to compile all syntactic structures which may use pattern matching: | ||
305 | - function alternatives | ||
306 | - case expressions | ||
307 | - lambda expressions | ||
308 | - closed type family alternatives | ||
309 | - open type family instances | ||
310 | - type class instances, type class instance heads (look at type class desugaring) | ||
311 | - A new data structure, *pattern guard trees* are used as intermediate representation. | ||
312 | Pattern match compilation is done in two steps: | ||
313 | 1. all syntax sugars (pattern matching, guards, view patterns, ...) are transformed to pattern guard trees | ||
314 | 2. pattern guard trees are optimized and compiled to case expressions | ||
315 | - Exhaustiveness and reachability checks are done also in step 2. | ||
316 | This approach is less error-prone then doing them in separate phase. | ||
317 | |||
318 | |||
319 | ### Pattern guard trees | ||
320 | |||
321 | Pattern guard trees is the simplest data structure which is general enough to express all pattern match related syntactic structures. | ||
322 | |||
323 | First we give a syntax of pattern guards trees which is used only in this documentation: | ||
324 | |||
325 | ----------- -- -------------------------------------------------------- ----------------------- | ||
326 | *guardtree* := *expression* **guard tree leaf** | ||
327 | | *guardtree* `|` *guardtree* **alternative patterns** | ||
328 | | *conname* (*parpat*)* `<-` *expression* `->` *guardtree* **pattern guard** | ||
329 | | `let` *bindings* `in` *guardtree* **let binding** | ||
330 | *parpat* := *pattern* | ||
331 | | *parpat* `,` *parpat* **parallel patterns** | ||
332 | *pattern* := *variable* **variable pattern** | ||
333 | | *conname* (*parpat*)* **constructor pattern** | ||
334 | | *expression* -> *parpat* **view pattern** | ||
335 | | *parpat* `::` *expression* **type annotation** | ||
336 | ----------- -- -------------------------------------------------------- ----------------------- | ||
337 | |||
338 | Remarks: | ||
339 | |||
340 | - A guard tree is an expression (it may appear whereever an expression may appear) | ||
341 | |||
342 | Examples: | ||
343 | |||
344 | 1. definition of `not` with pattern guard trees: | ||
345 | |||
346 | ~~~~~ {.haskell} | ||
347 | not x = (True <- x -> False) | (False <- x -> True) | ||
348 | ~~~~~ | ||
349 | |||
350 | The semantics of pattern guard trees is given by the `value`, `matchesP` and `matches` functions (pseudo code): | ||
351 | |||
352 | ~~~~~ {.haskell} | ||
353 | value :: GuardTree a -> Maybe a | ||
354 | value (Leaf e) = Just e | ||
355 | value (Alt x y) = value x <> value y | ||
356 | value (Let bs x) = value (let bs in x) | ||
357 | value (PatternGuard cn ps e x) = case PCon cn ps `matches` e of | ||
358 | Just bs -> value (let bs in x) | ||
359 | Nothing -> Nothing | ||
360 | |||
361 | matchesP :: ParPat a -> a -> Maybe [Binding] | ||
362 | Pat x `matchesP` v = x `matches' v | ||
363 | ParPat x y `matchesP` v = case x `matchesP` v of | ||
364 | Just bs -> case let bs in y `matchesP` v of | ||
365 | Just bs' -> Just (bs ++ bs') | ||
366 | Nothing -> Nothing | ||
367 | Nothing -> Nothing | ||
368 | |||
369 | matches :: Pattern a -> a -> Maybe [Binding] | ||
370 | Var n `matches` v = Just [n = v] | ||
371 | PCon cn ps `matches` v = case v of | ||
372 | cn vs -> mconcat (sequence (zipWith matchesP ps vs)) | ||
373 | _ -> Nothing | ||
374 | ViewPat f p `matches` v = p `matches` f v | ||
375 | TypeAnn p t `matches` v = p `matches` v | ||
376 | ~~~~~ | ||
377 | |||
378 | |||
379 | ### Desugaring to pattern guard trees | ||
380 | |||
381 | #### Function alternatives | ||
382 | |||
383 | |||
384 | |||
385 | |||
386 | |||
387 | |||
388 | #### View patterns | ||
389 | |||
390 | |||
391 | ### Compilation of pattern guard trees | ||
392 | |||
393 | |||
394 | ### TODO | ||
395 | |||
396 | - pattern matching on GADTs | ||
397 | - dependent pattern matching | ||
398 | |||
399 | |||
400 | |||
287 | Desugared source code | 401 | Desugared source code |
288 | --------------------- | 402 | --------------------- |
289 | 403 | ||
@@ -319,29 +433,17 @@ Tasks | |||
319 | - find semantic errors | 433 | - find semantic errors |
320 | - complete code | 434 | - complete code |
321 | - infer types | 435 | - infer types |
322 | - find out inferrable values | ||
323 | - construct witnesses for type class method invocation | 436 | - construct witnesses for type class method invocation |
437 | - possibly find out inferrable values | ||
324 | - normalize code | 438 | - normalize code |
325 | - reduce expressions (beta-reduction) | 439 | - reduce expressions (beta-reduction) |
326 | - avoid infinite recursion (termination checking) | 440 | - avoid infinite recursion (termination checking) |
327 | (this is not a priority at the moment) | 441 | (this is not a priority at the moment) |
328 | 442 | ||
329 | |||
330 | - code completion is base on supporting hidden arguments | ||
331 | |||
332 | |||
333 | - eliminate abstractions | ||
334 | - reduction, partial evaluation | ||
335 | - optimizations | ||
336 | - type erasure | ||
337 | |||
338 | |||
339 | - optimizations | ||
340 | - type erasure | ||
341 | |||
342 | Design decisions | 443 | Design decisions |
343 | 444 | ||
344 | - use a dependently typed core language (treat types as values) | 445 | - use a dependently typed core language (treat types as values) |
446 | This gives more expressive power to static typing and somewhat simplifies the compiler at the same time. | ||
345 | - all code completion task is done by inferring values of hidden variables in the following two intermangled phases: | 447 | - all code completion task is done by inferring values of hidden variables in the following two intermangled phases: |
346 | 1. make every hidden argument application explicit by inserting metavariables | 448 | 1. make every hidden argument application explicit by inserting metavariables |
347 | 2. gradually eliminate metavariables during type checking | 449 | 2. gradually eliminate metavariables during type checking |
@@ -358,6 +460,7 @@ Rich environment | |||
358 | 460 | ||
359 | 461 | ||
360 | 462 | ||
463 | |||
361 | Solving metavariables | 464 | Solving metavariables |
362 | --------------------- | 465 | --------------------- |
363 | 466 | ||