| <!DOCTYPE html> | |
| <html lang="en"> | |
| <head> | |
| <meta charset="utf-8" /> | |
| <meta name="viewport" content="width=device-width, initial-scale=1" /> | |
| <title>*scratch*</title> | |
| <style> | |
| body { | |
| font-family: Hack, Menlo, Monaco, 'Droid Sans Mono', 'Courier New', monospace; | |
| white-space: pre; |
| (define reduce | |
| (lambda (subject complete-rules rules generation-id) | |
| (if (null? rules) | |
| subject | |
| (let* ((rule-pair (car rules)) | |
| (rest-of-rules (cdr rules)) | |
| (pattern (car rule-pair)) | |
| (replacements (cdr rule-pair)) | |
| (new-gen-id (+ generation-id 1)) | |
| (new-subject (apply-rule subject pattern replacements generation-id))) |
| -- A simply-typed lambda calculus, and a definition of normalisation by | |
| -- evaluation for it. | |
| -- | |
| -- The NBE implementation is based on a presentation by Sam Lindley from 2016: | |
| -- http://homepages.inf.ed.ac.uk/slindley/nbe/nbe-cambridge2016.pdf | |
| -- | |
| -- Adapted to handle terms with explicitly typed contexts (Sam's slides only | |
| -- consider open terms with the environments left implicit/untyped). This was a | |
| -- pain in the ass to figure out. |
| open import Level | |
| -- "Wok" stands for "weak omega kategory". | |
| mutual | |
| record Wok {i} (Obj : Set i) : Set (suc i) where | |
| coinductive | |
| constructor Wok: | |
| infix 1 Hom | |
| infixr 9 compo | |
| field Arr : (a b : Obj) -> Set i | |
| field Hom : (a b : Obj) -> Wok (Arr a b) |
Mini projects by Maxime Euzière (xem), subzey, Martin Kleppe (aemkei), Mathieu Henri (p01), Litterallylara, Tommy Hodgins (innovati), Veu(beke), Anders Kaare, Keith Clark, Addy Osmani, bburky, rlauck, cmoreau, maettig, thiemowmde, ilesinge, adlq, solinca, xen_the,...
(For more info and other projects, visit http://xem.github.io)
(Official Slack room: http://jsgolf.club / join us on http://register.jsgolf.club)
| while { | |
| let x = foo(); | |
| bar(x); | |
| x != 0 | |
| } {} | |
