Update tutorial files

Author: mtzguido

tutorial/ParallelIncrement.fst

@@ -16,7 +16,6 @@
 
 module PulseByExample
 
-module PM = Pulse.Main
 open Pulse.Lib.Core
 
 (* 
@@ -27,30 +26,31 @@ open Pulse.Lib.Core
 *)
 
 //SNIPPET_START: five
+#lang-pulse
+
 let fstar_five : int = 5
 
-```pulse
 fn five ()
   requires emp
   returns n:int
   ensures pure (n == 5)
 { 
   fstar_five
 }
-```
+
 
 let pulse_five_in_fstar = five ()
 //SNIPPET_END: five
 
-```pulse
+
 fn five_alt ()
   requires emp
   returns n:(n:int { n == 5 })
   ensures emp
 { 
   5
 }
-```
+
 
 open Pulse.Lib.Reference
 module R = Pulse.Lib.Reference
@@ -62,7 +62,7 @@ module R = Pulse.Lib.Reference
   - default full permission
   - heap reference, read and write
 *)
-```pulse
+
 fn ref_swap (r1 r2:ref int)
   requires
     R.pts_to r1 'n1 **
@@ -77,7 +77,7 @@ fn ref_swap (r1 r2:ref int)
   r1 := v2;
   r2 := v1
 }
-```
+
 
 open Pulse.Lib.Array
 module A = Pulse.Lib.Array
@@ -91,7 +91,7 @@ open Pulse.Lib.BoundedIntegers
   - machine integers, ops on bounded integers
 *)
 
-```pulse
+
 fn arr_swap (#t:Type0) (n i j:SZ.t) (a:larray t (v n))
   requires
     A.pts_to a 's0 **
@@ -109,15 +109,15 @@ fn arr_swap (#t:Type0) (n i j:SZ.t) (a:larray t (v n))
   a.(i) <- vj;
   a.(j) <- vi;
 }
-```
+
 
 (* 
   Things to note:
   - control flow: while loop, if
   - mutable local reference, read and write
   - variable permission
 *)
-```pulse
+
 fn max (n:SZ.t) (a:larray nat (v n))
   requires
     A.pts_to a #'p 's **
@@ -156,10 +156,10 @@ fn max (n:SZ.t) (a:larray nat (v n))
   let vmax = !max;
   vmax
 }
-```
-// This option may become the default at some point
+
+//this option should become the default, once I shake out the handling of address-taking
 #push-options "--ext 'pulse:rvalues'"
-```pulse
+
 fn max_alt (n:SZ.t) (a:larray nat (v n))
   requires
     A.pts_to a #'p 's **
@@ -189,5 +189,18 @@ fn max_alt (n:SZ.t) (a:larray nat (v n))
   };
   max
 }
-```
-#pop-options
+
+#pop-options
+
+(* 
+- some more mature example (e.g. sorting alg)
+
+- some simple record data structure along with a library of functions on this DS
+  (e.g. library of functions on 2D points)
+
+- build up to explaining the pulse implementation of lpht? -- emphasis on connecting
+  pure implementation to imperative code
+- pulse linked list? -- more traditional sep logic example 
+
+- concurrency, e.g. par incr of a ctr
+*)

tutorial/PulseByExample.fst

@@ -1,22 +1,22 @@
 # Pulse By Example
 
 Pulse is a syntax extension and typechecker extension of F*. 
-A pulse program is embedded in an F* program, delimited by the syntax extension notation ` ```pulse ... ``` `. 
+A pulse program is embedded in an F* program, delimited by the syntax extension notation `  ...  `. 
 The first code snippet demonstrates an embedded Pulse program `five`, which produces the integer 5. 
 The rest of the file is a normal F* program. 
 
 Pulse programs accept one or more arguments, where the `unit` type can be used to thunk a computation. 
 The specification of a Pulse program includes a precondition (`requires ...`), postcondition (`ensures ...`), and (optional) return type. 
 The pre- and post-conditions are propositions, like F* propositions but with a twise: Pulse leverages [separation logic](https://en.wikipedia.org/wiki/Separation_logic) to simplify reasoning about heap mutation. 
 
-Propositions in Pulse (called `vprop`s) enjoy separation logic operators like `**`, the separating conjunction. 
-A `vprop` may include a traditional F* `prop` by surrounding it with the `pure` keyword. 
-Generally, pure `prop`s are used to specify mathematical/logical constraints and anything having to do with references or memory sits outside in the surrounding `vprop`. 
+Propositions in Pulse (called `slprop`s) enjoy separation logic operators like `**`, the separating conjunction. 
+A `slprop` may include a traditional F* `prop` by surrounding it with the `pure` keyword. 
+Generally, pure `prop`s are used to specify mathematical/logical constraints and anything having to do with references or memory sits outside in the surrounding `slprop`. 
 
 Returning to our code snippet, the separation logic proposition `emp` means that the program does not own any resources or have any knowledge. 
 So the Pulse program `five` begins with no resources/knowledge and returns with the knowledge that the return value is logically equal to 5. 
 
-```ocaml
+ocaml
 module PM = Pulse.Main
 open Pulse.Lib.Core
 
@@ -31,7 +31,7 @@ fn five ()
   5
 }
 ``
-```
+
 
 Let's make things more interesting. 
 The next code snippet `ref_swap` swaps the values of two integer references. 
@@ -47,7 +47,7 @@ Pulse syntax spotlight: The program body demonstrates Pulse syntax for
 - reference read: `!r1`
 - reference write: `r1 := ...`
 
-```ocaml
+ocaml
 open Pulse.Lib.Reference
 module R = Pulse.Lib.Reference
 
@@ -64,12 +64,14 @@ fn ref_swap (r1 r2:ref int)
   r2 := v1
 }
 ``
-```
+
 
 You've seen references; now we'll introduce arrays. 
 But first, a note on integers. 
 In the following code snippet, we use non-primitive integers for the first time: `FStar.SizeT` is a module for machine integers of at least 16 bits, depending on the machine. 
+#lang-pulse
 The module `Pulse.Class.BoundedIntegers` offers arithmetic operations on various types of bounded integers, including `FStar.SizeT` and `FStar.U32`. 
+#lang-pulse
 The bounded integer class overloads arithmetic operators, like `<`, to allow, e.g., the comparison of `SizeT`s `i < n` on line X and comparison of `nat`s `k < v n` on line X (`v` elaborates to `SZ.v` and converts a `SizeT` to a nat). 
 
 Let's get back to arrays. 
@@ -85,7 +87,7 @@ Pulse syntax spotlight: The program body demonstrates Pulse syntax for
 - array read: `a.(i)`
 - array write: `a.(i) <- ...`
 
-```ocaml
+ocaml
 open Pulse.Lib.Array
 module A = Pulse.Lib.Array
 module SZ = FStar.SizeT
@@ -109,7 +111,7 @@ fn arr_swap (#t:Type0) (n i j:SZ.t) (a:larray t (v n))
   a.(j) <- vi;
 }
 ``
-```
+
 
 The last example introduces loops. 
 The Pulse program `max` computes the maximum value in an array of `nat`s. 
@@ -147,7 +149,7 @@ Pulse syntax spotlight: The program body demonstrates Pulse syntax for
 - loop invariant: `invariant b ...`
 - custom proof syntax: `with ... assert ...`
 
-```ocaml
+ocaml
 ``pulse
 fn max (n:SZ.t) (a:larray nat (v n))
   requires A.pts_to a #'p 's ** pure (Seq.length 's == v n)
@@ -185,7 +187,7 @@ fn max (n:SZ.t) (a:larray nat (v n))
   vmax
 }
 ``
-```
+
 
 In this tutorial, you have seen custom Pulse proof syntax:
 - `requires`, `ensures`