Fixing case studies, pretty printing and html generation

examples/literate_beluga/0Beginner/Parallel_Reduction.bel

@@ -74,14 +74,14 @@ schema trCtx = some [t:tp] block x:tm, of_v: oft x t, pr_v: pr x x;
 %{{
 ## Substitution Lemma
 Beluga enjoys the usual substitution property for parametric and hypothetical derivations for free since substitutivity is just a by-product of
-hypothetical-parametric judgements. Strictly speaking, the substitution lemma does not need to be stated explicitly in order to prove type preservation for parallel reduction but we've encoded it regardless. While this is usually proved by induction on the first derivation, we show it as a corollary of the substitution principles.}}%
+hypothetical-parametric judgements. Strictly speaking, the substitution lemma does not need to be stated explicitly in order to prove type preservation for parallel reduction but we've encoded it regardless. While this is usually proved by induction on the first derivation, we show it as a corollary of the substitution principles. In stating the substitution lemma we explicitly state that the types <code>S</code> and <code>T</code> cannot depend on the context <code>g</code>, i.e. they are closed.}}%
 rec subst : (g:tCtx)
             [g,b: block x:tm, of_v: oft x T[] |- oft M[..,b.1] S[]]
 -> [g |-  oft N T[]]
 -> [g |-  oft M[..,N] S[]] =
 fn d1 => fn d2 =>
 let [g, b: block x:tm, of_v: oft x T |- D1[..,b.1,b.2]] = d1 in
-let [g |-  D2[..]] = d2 in
+let [g |-  D2] = d2 in
     [g |-  D1[..,_,D2]]
 ;
 
@@ -91,34 +91,34 @@ let [g |-  D2[..]] = d2 in
 % Type preservation for parallel reduction
 %{{
 ## Type Preservation for Parallel Reductions
-We prove type preservation for parallel reduction: when <code>M</code> steps to <code>N</code> and <code>M</code> has type <code>A</code> then <code>N</code> has the same type <code>A</code>. expressions to depend on the context since we may step terms containing variables. Substitution property for parametric and hypothetical derivations is free. }}% 
+We prove type preservation for parallel reduction: when <code>M</code> steps to <code>N</code> and <code>M</code> has type <code>A</code> then <code>N</code> has the same type <code>A</code>. expressions to depend on the context since we may step terms containing variables. Substitution property for parametric and hypothetical derivations is free. We do not enforce here that the type <code>A</code> is closed. Although this is possible by writing <code>A[]</code> the statement looks simpler if we do not enforce this extra invariant.}}% 
 
 rec tps : (g:trCtx)
-            [g |-  pr (M[..]) (N[..])] -> [g |-  oft (M[..]) A]
-          -> [g |-  oft (N[..]) A] =
+            [g |- pr M N] -> [g |- oft M A]
+          -> [g |- oft N A] =
 fn r => fn d => case r of
-| [g |-  #p.3[..] ] => d
-| [g |-  pr_b (\x.\pr_v. R1) (R2[..] ) ] =>
-    let [g |-  of_app (of_lam (\x.\of_v. D1)) (D2[..]) ] = d in
+| [g |- #p.3 ] => d
+| [g |- pr_b (\x.\pr_v. R1) R2 ] =>
+    let [g |-  of_app (of_lam (\x.\of_v. D1)) D2 ] = d in
     let [g, b: block x:tm, of_v: oft x T, pr_v: pr x x |- F1[..,b.1,b.2]] =
         tps [g, b: block x:tm, of_v: oft x _, pr_v: pr x x |- R1[..,b.1,b.3]]
 [g, b |- D1[..,b.1,b.2]] in
-    let [g |-  F2[..] ] = tps [g |-  R2[..]] [g |-  D2[..]] in
+    let [g |-  F2 ] = tps [g |-  R2] [g |-  D2] in
     [g |-  F1[..,_,F2]] % use substitution lemma directly
 
-| [g |-  pr_l \x.\pr_v. R] =>
+| [g |- pr_l \x.\pr_v. R] =>
     let [g |-  of_lam \x.\of_v. D] = d in
     let [g, b: block x:tm, of_v: oft x T, pr_v: pr x x |- F[..,b.1,b.2]] =
         tps [g, b: block x:tm, of_v: oft x _, pr_v: pr x x |- R[..,b.1,b.3]]
 [g, b |- D[..,b.1,b.2]] in
     [g |-  of_lam \x.\of_v. F]
 
-| [g |-  pr_a (R1[..]) (R2[..]) ] =>
-    let [g |-  of_app (D1[..]) (D2[..])] = d in
-    let [g |-  F1[..] ] = tps [g |-  R1[..]] [g |- D1[..]] in
-    let [g |-  F2[..] ] = tps [g |-  R2[..]] [g |- D2[..]] in
-    [g |-  of_app (F1[..]) (F2[..])]
+| [g |- pr_a R1 R2 ] =>
+    let [g |- of_app D1 D2] = d in
+    let [g |- F1] = tps [g |-  R1] [g |- D1] in
+    let [g |- F2] = tps [g |-  R2] [g |- D2] in
+    [g |- of_app F1 F2]
 ;
 %{{
-The &beta;-reduction case is perhaps the most note-worthy. We know by assumption that <code>d:[g |- oft (app (lam A (\x. M[..]x))(N[..])) (arr A B)</code> and by inversion that <code>d:[g |- of_a (of_l \x. \u. D1[..]x u)(D2[..]) ]</code> where <code>D1</code> stands for <code>oft (M[..]x) B</code> in the extended context <code>g, x:tm , u:oft x A</code>. Furthermore, <code>D2</code> describes a derivation <code>oft (N[..])A</code>. A recursive call on <code>D2</code> yields <code>F2:oft (N'[..])A</code>. Likewise, y the i.h. on <code>D1</code>, we obtain a derivation <code/>F1:oft (M'[..]x) B</code> in <code>g, b:block (x:tm , of_x:oft x A)</code>. We now want to substitute for <code>x</code> the term <code>N'</code>, and for the derivation <code>oft x A</code> the derivation <code>F2</code>. This is achieved by applying to <code>F1</code> the substitution <code>.. _ (F2[..])</code>. Since in the program above we do not have the name <code>N</code> available, we write an underscore and let Beluga's type reconstruction algorithm infer the appropriate name.
+The &beta;-reduction case is perhaps the most note-worthy. We know by assumption that <code>d:[g |- oft (app (lam A (\x. M x)) N)) (arr A B)</code> and by inversion that <code>d:[g |- of_a (of_l \x. \u. D1 x u)(D2) ]</code> where <code>D1</code> stands for <code>oft (M x) B</code> in the extended context <code>g, x:tm , u:oft x A</code>. Furthermore, <code>D2</code> describes a derivation <code>oft N A</code>. A recursive call on <code>D2</code> yields <code>F2:oft N' A</code>. Likewise, y the i.h. on <code>D1</code>, we obtain a derivation <code/>F1:oft M' B</code> in <code>g, b:block (x:tm , of_x:oft x A)</code>. We now want to substitute for <code>x</code> the term <code>N'</code>, and for the derivation <code>oft x A</code> the derivation <code>F2</code>. This is achieved by applying to <code>F1</code> the substitution <code>.., _ F2)</code>. Since in the program above we do not have the name <code>N</code> available, we write an underscore and let Beluga's type reconstruction algorithm infer the appropriate name.
 }}%