| module Prime where | |
| open import Coinduction | |
| open import Data.Empty | |
| open import Data.Nat | |
| open import Data.Nat.Properties | |
| open import Data.Nat.Divisibility | |
| open import Data.Fin hiding (pred; _+_; _<_; _≤_; compare) | |
| open import Data.Fin.Props hiding (_≟_) |
Delimited continuations manipulate the control flow of programs. Similar to control structures like conditionals or loops they allow to deviate from a sequential flow of control.
We use exception handling as another example for control flow manipulation and later show how to implement it using delimited continuations. Finally, we show that nondeterminism can also be expressed using delimited continuations.
| ;; 1. place this in ~/.emacs.d/private/intero/packages.el | |
| ;; 2. add intero, syntax-checking and auto-completion to your | |
| ;; ~/.spacemacs layer configuration & remove the haskell layer | |
| ;; if you were using that before | |
| ;; 3. make sure you have stack installed http://haskellstack.org | |
| ;; 4. fire up emacs & open up a stack project's source files |
| {-# LANGUAGE DataKinds, TypeFamilies, TypeOperators, GADTs, | |
| ScopedTypeVariables, TypeOperators #-} | |
| -- | Type-level natural numbers and singletons, with proofs of | |
| -- a few basic properties. | |
| module BasicNat ( | |
| -- | Type-level natural numbers | |
| Nat (..) | |
| , type (+) |
Estimated time: 10 minutes
| {-# language TemplateHaskell, ScopedTypeVariables, RankNTypes, | |
| TypeFamilies, UndecidableInstances, DeriveFunctor, GADTs, | |
| TypeOperators, TypeApplications, AllowAmbiguousTypes, | |
| TypeInType, StandaloneDeriving #-} | |
| import Data.Singletons.TH -- singletons 2.4.1 | |
| import Data.Kind | |
| -- some standard stuff for later examples' sake |
| *** preview.el.orig 2018-06-11 14:08:50.000000000 -0400 | |
| --- preview.el 2018-06-11 15:35:38.000000000 -0400 | |
| *************** | |
| *** 180,186 **** | |
| (close preview-gs-close)) | |
| (tiff (open preview-gs-open) | |
| (place preview-gs-place) | |
| ! (close preview-gs-close))) | |
| "Define functions for generating images. | |
| These functions get called in the process of generating inline |
| {-# OPTIONS --cubical #-} | |
| open import Cubical.Core.Everything | |
| open import Cubical.Data.Maybe | |
| open import Cubical.Data.Nat | |
| open import Cubical.Foundations.Prelude | |
| open import Cubical.Foundations.Isomorphism | |
| data ω : Type₀ where |
| -- | This module defines a function that produces a complete binary tree | |
| -- from a breadth-first list of its (internal) node labels. It is an | |
| -- optimized version of an implementation by Will Ness that avoids | |
| -- any "impossible" cases. See | |
| -- | |
| -- https://stackoverflow.com/a/60561480/1477667 | |
| module Bftr (Tree (..), bft, list, deftest) where | |
| import Data.Function (fix) | |
| import Data.Monoid (Endo (..)) |
