tweak pp of initial type environment and l2.ott comments

4 files changed, 18 insertions, 14 deletions

diff --git a/language/l2.lem b/language/l2.lem
index 11d610b1..9691f21c 100644
--- a/language/l2.lem
+++ b/language/l2.lem
@@ -34,7 +34,7 @@ type base_kind =
  | BK_aux of base_kind_aux * l
 
 
-type kid_aux =  (* variables with kind, ticked to differntiate from program variables *)
+type kid_aux =  (* variables with kind, ticked to differentiate from program variables *)
  | Var of x
 
 
@@ -60,14 +60,14 @@ type kind =
 
 
 type nexp_aux =  (* expression of kind Nat, for vector sizes and origins *)
- | Nexp_id of id (* identifier, bound by def Nat x = nexp *)
+ | Nexp_id of id (* identifier, bound by \texttt{def Nat x = nexp} *)
  | Nexp_var of kid (* variable *)
  | Nexp_constant of integer (* constant *)
  | Nexp_times of nexp * nexp (* product *)
  | Nexp_sum of nexp * nexp (* sum *)
  | Nexp_minus of nexp * nexp (* subtraction *)
  | Nexp_exp of nexp (* exponential *)
- | Nexp_neg of nexp (* For internal use *)
+ | Nexp_neg of nexp (* for internal use only *)
 
 and nexp = 
  | Nexp_aux of nexp_aux * l
@@ -275,7 +275,7 @@ and exp 'a =
 
 and lexp_aux 'a =  (* lvalue expression *)
  | LEXP_id of id (* identifier *)
- | LEXP_memory of id * list (exp 'a) (* memory write via function call *)
+ | LEXP_memory of id * list (exp 'a) (* memory or register write via function call *)
  | LEXP_cast of typ * id
  | LEXP_tup of list (lexp 'a) (* set multiple at a time, a check will ensure it's not memory *)
  | LEXP_vector of (lexp 'a) * (exp 'a) (* vector element *)
@@ -297,7 +297,7 @@ and fexps_aux 'a =  (* Field-expression list *)
 and fexps 'a = 
  | FES_aux of (fexps_aux 'a) * annot 'a
 
-and opt_default_aux 'a =  (* Optional default value for indexed vectors, to define a defualt value for any unspecified positions in a sparse map *)
+and opt_default_aux 'a =  (* Optional default value for indexed vectors, to define a default value for any unspecified positions in a sparse map *)
  | Def_val_empty
  | Def_val_dec of (exp 'a)
 
diff --git a/language/l2.ml b/language/l2.ml
index bae88cab..fff2e420 100644
--- a/language/l2.ml
+++ b/language/l2.ml
@@ -31,7 +31,7 @@ id_aux =  (* Identifier *)
 
 
 type 
-kid_aux =  (* variables with kind, ticked to differntiate from program variables *)
+kid_aux =  (* variables with kind, ticked to differentiate from program variables *)
    Var of x
 
 
@@ -56,15 +56,15 @@ kind =
 
 
 type 
-nexp_aux =  (* expression of kind Nat, for vector sizes and origins *)
-   Nexp_id of id (* identifier, bound by def Nat x = nexp *)
+nexp_aux =  (* expression of kind _, for vector sizes and origins *)
+   Nexp_id of id (* identifier, bound by \texttt{def Nat x = nexp} *)
  | Nexp_var of kid (* variable *)
  | Nexp_constant of int (* constant *)
  | Nexp_times of nexp * nexp (* product *)
  | Nexp_sum of nexp * nexp (* sum *)
  | Nexp_minus of nexp * nexp (* subtraction *)
  | Nexp_exp of nexp (* exponential *)
- | Nexp_neg of nexp (* For internal use *)
+ | Nexp_neg of nexp (* for internal use only *)
 
 and nexp = 
    Nexp_aux of nexp_aux * l
@@ -289,7 +289,7 @@ and 'a exp =
 
 and 'a lexp_aux =  (* lvalue expression *)
    LEXP_id of id (* identifier *)
- | LEXP_memory of id * ('a exp) list (* memory write via function call *)
+ | LEXP_memory of id * ('a exp) list (* memory or register write via function call *)
  | LEXP_cast of typ * id
  | LEXP_tup of ('a lexp) list (* set multiple at a time, a check will ensure it's not memory *)
  | LEXP_vector of 'a lexp * 'a exp (* vector element *)
@@ -311,7 +311,7 @@ and 'a fexps_aux =  (* Field-expression list *)
 and 'a fexps = 
    FES_aux of 'a fexps_aux * 'a annot
 
-and 'a opt_default_aux =  (* Optional default value for indexed vectors, to define a defualt value for any unspecified positions in a sparse map *)
+and 'a opt_default_aux =  (* Optional default value for indexed vectors, to define a default value for any unspecified positions in a sparse map *)
    Def_val_empty
  | Def_val_dec of 'a exp
 
diff --git a/language/l2.ott b/language/l2.ott
index c3807f6a..f5bf73b7 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -1011,8 +1011,11 @@ terminals :: '' ::=
     {{ tex \ottkw{consistent\_increase}~ }}
   | consistent_decrease                 :: :: cd
     {{ tex \ottkw{consistent\_decrease}~ }}
- | == :: :: equiv
-   {{ tex \equiv }}
-
+  | == :: :: equiv
+    {{ tex \equiv }}
+%  | [|| :: :: list_start
+%    {{ tex \ottsym{[||} }}       
+%  | ||] :: :: list_end       
+%    {{ tex \ottsym{||]} }}       
 
 
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index d52e049f..451dee5e 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -810,6 +810,7 @@ let rec pp_format_annot_ascii = function
   | NoTyp -> "Nothing"
   | Base((targs,t),tag,nes,efct,efctsum,_) ->
     (*TODO print out bindings for use in pattern match in interpreter*)
+      (match tag with External (Some s) -> "("^s^") " | _ -> "") ^
      "forall " ^ list_format ", " (function (i,k) -> kind_to_string k ^" '"^ i) targs ^ 
   (match nes with [] -> "" | _ -> ", " ^ pp_format_nes_ascii nes)
   ^ ". "