Tweak formatting in pretty printer, and resolve bugs.

Start specifying lem homs for rules.

2 files changed, 57 insertions, 83 deletions

diff --git a/language/l2_rules.ott b/language/l2_rules.ott
index 402f2d84..d865d0ed 100644
--- a/language/l2_rules.ott
+++ b/language/l2_rules.ott
@@ -16,17 +16,17 @@ k :: 'Ki_' ::=
    | K_infer                                           :: :: infer {{ com Representing an unknown kind, inferred by context }}
    | K_Abbrev t                                        :: :: abbrev {{ com Not really a kind, but a convenient way of tracking type abbreviations }}
 
-t , u :: 'T_' ::=                                {{ phantom }}
+t , u :: 'T_' ::=                                
 {{ com Internal types }}
    | id                                           :: :: id
    | kid                                          :: :: var
-   | t1 -> t2 effect tag S_N                     :: :: fn  {{ com [[S_N]] are constraints for the function, [[tag]] holds generation data }}
+   | t1 -> t2 effect tag S_N                      :: :: fn  {{ com [[S_N]] are constraints for the function, [[tag]] holds generation data }}
    | ( t1 * .... * tn )                           :: :: tup
    | id t_args                                    :: :: app 
    | register t_args                              :: :: reg_app
    | t [ t1 / id1 ... tn / idn ]		  :: :: subst
 
-tag :: 'Tag_' ::=                                 {{ phantom }}
+tag :: 'Tag_' ::=                                 
 {{ com Data indicating where the identifier arises and thus information necessary in compilation }}
    | None                                 :: :: empty 
    | Ctor                                 :: :: ctor {{ com Data constructor from a type union }}
@@ -77,51 +77,26 @@ ne :: 'Ne_' ::=
    | ne >= ne'           :: :: gteq
    | kid 'IN' { num1 , ... , numn } :: :: in
 
-%% %% embed
-%% %% {{ lem
-%% %% 
-%% %% val t_subst_t : list (tnv * t) -> t -> t 
-%% %% val t_subst_tnv : list (tnv * t) -> tnv -> t
-%% %% val ftv_t : t -> list tnv
-%% %% val ftv_tm : list t -> list tnv
-%% %% val ftv_s : list (p*tnv) -> list tnv
-%% %% val compatible_overlap : list (x*t) -> bool
-%% %% 
-%% %% (*TODO Should this normalize following the implementation? And blength and hlength need a means of implementation*)
-%% %% let normalize n = n
-%% %% 
-%% %% let blength (_,bit) = Ne_const 8
-%% %% let hlength (_,bit) = Ne_const 8
-%% %% 
+%%embed
+%%{{ lem
+%%
+%%let blength (bit) = Ne_const 8
+%%let hlength (bit) = Ne_const 8
+
 %% %% let rec sumation_nes nes = match nes with
 %% %%   | [ a; b] -> Ne_add a b 
 %% %%   | x :: y -> Ne_add x (sumation_nes y)
 %% %% end
 %% %% 
-%% %% }}
-%% %% 
-%% %% embed
-%% %% {{ hol
-%% %% load "fmaptreeTheory";
-%% %% val _ = 
-%% %%   Hol_datatype 
-%% %%     `env_body = <| env_p : x|->p; env_f : x|->f_desc; env_v : x|->v_desc |>`;
-%% %% 
-%% %% val _ = Define `
-%% %%   env_union e1 e2 =
-%% %%     let i1 = item e1 in
-%% %%     let m1 = map e1 in
-%% %%     let i2 = item e2 in
-%% %%     let m2 = map e2 in
-%% %%       FTNode <| env_p:=FUNION i1.env_p i2.env_p; 
-%% %%                 env_f:=FUNION i1.env_f i2.env_f;
-%% %%                 env_v:=FUNION i1.env_v i2.env_v |>
-%% %%              (FUNION m1 m2)`;
-%% %% }}
-%% %% {{ lem
-%% %% type env =
-%% %%   | EnvEmp 
-%% %%   | Env of (map x env) * (map x p) * (map x f_desc) * (map x v_desc)
+
+%% type definition_type =
+%%   | DenvEmp
+%%   | Denv of (map tid k_inf)  
+%%
+%% type env =
+%%   | EnvEmp 
+%%   | Env of (map x v_desc) * definition_type
+
 %% %% 
 %% %% val env_union : env -> env -> env
 %% %% let env_union e1 e2 =
@@ -131,9 +106,7 @@ ne :: 'Ne_' ::=
 %% %%    | ((Env Em1 Ep1 Ef1 Ev1),(Env Em2 Ep2 Ef2 Ev2)) ->
 %% %%      Env(union_map Em1 Em2) (union_map Ep1 Ep2) (union_map Ef1 Ef2) (union_map Ev1 Ev2)
 %% %% end
-%% %% 
-%% %% }}
-%% %% 
+%%}}
 
 S_N {{ tex {\Sigma^{\textsc{N} } } }} :: '' ::= {{ phantom }}
                                                                     {{ hol nec list }}
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 8a8b07cf..08eec393 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -54,7 +54,7 @@ let pp_format_id (Id_aux(i,_)) =
 
 let pp_id ppf id = base ppf (pp_format_id id)
 
-let pp_format_var (Kid_aux(Var v,_)) = "'" ^ v
+let pp_format_var (Kid_aux(Var v,_)) = v
 
 let pp_var ppf var = base ppf (pp_format_var var)
 
@@ -81,7 +81,7 @@ let rec pp_format_typ (Typ_aux(t,_)) =
                             (parens is_atomic_typ pp_format_typ ret) ^ " effect " ^ 
                             (pp_format_effects efct) ^ ")"
   | Typ_tup(typs) -> "(" ^ (list_format " * " pp_format_typ typs) ^ ")"
-  | Typ_app(id,args) -> "(" ^ (pp_format_id id) ^ "<" ^ (list_format ", " pp_format_typ_arg args) ^ ">)"
+  | Typ_app(id,args) -> (pp_format_id id) ^ "<" ^ (list_format ", " pp_format_typ_arg args) ^ ">"
 and pp_format_nexp (Nexp_aux(n,_)) = 
   match n with
   | Nexp_var(var) -> pp_format_var var
@@ -170,7 +170,8 @@ let pp_format_lit (L_aux(l,_)) =
   | L_true -> "true"
   | L_false -> "false"
   | L_num(i) -> string_of_int i
-  | L_hex(n) | L_bin(n) -> n
+  | L_hex(n) -> "0x" ^ n
+  | L_bin(n) -> "0b" ^ n
   | L_undef -> "undefined"
   | L_string(s) -> "\"" ^ s ^ "\"" 
 
@@ -209,7 +210,7 @@ let rec pp_let ppf (LB_aux(lb,_)) =
 (* Need an is_atomic? check and insert parens otherwise *)
 and pp_exp ppf (E_aux(e,_)) = 
   match e with
-  | E_block(exps) -> fprintf ppf "@[<0>%a %a@ %a@]" 
+  | E_block(exps) -> fprintf ppf "@[<0>%a%a@ %a@]" 
                                  kwd "{" 
                                  (list_pp pp_semi_exp pp_exp) exps
                                  kwd "}"
@@ -219,47 +220,47 @@ and pp_exp ppf (E_aux(e,_)) =
   | E_app(f,args) -> fprintf ppf "@[<0>%a(%a)@]" pp_id f (list_pp pp_comma_exp pp_exp) args 
   | E_app_infix(l,op,r) -> fprintf ppf "@[<0>%a %a %a@]" pp_exp l pp_id op pp_exp r
   | E_tuple(exps) -> fprintf ppf "@[<0>%a %a %a@]" kwd "(" (list_pp pp_comma_exp pp_exp) exps kwd ")"
-  | E_if(c,t,e) -> fprintf ppf "@[<0> %a %a @[<1> %a %a@] @[<1> %a@ %a@]@]" kwd "if " pp_exp c kwd "then" pp_exp t kwd "else" pp_exp e
+  | E_if(c,t,e) -> fprintf ppf "@[<0>%a %a @[<1>%a %a@] @[<1>%a@ %a@]@]" kwd "if " pp_exp c kwd "then" pp_exp t kwd "else" pp_exp e
   | E_for(id,exp1,exp2,exp3,exp4) ->
-    fprintf ppf "@[<0> %a %a %a %a %a %a %a %a@ @[<1> %a @] @]" 
+    fprintf ppf "@[<0> %a %a %a %a %a %a %a %a@ @[<1>%a@]@]" 
       kwd "foreach " pp_id id kwd " from " pp_exp exp1 kwd " to " pp_exp exp2 kwd "by " pp_exp exp3 pp_exp exp4
-  | E_vector(exps) -> fprintf ppf "@[<0> %a %a %a @]" kwd "[" (list_pp pp_comma_exp pp_exp) exps kwd "]"
+  | E_vector(exps) -> fprintf ppf "@[<0>%a%a%a@]" kwd "[" (list_pp pp_comma_exp pp_exp) exps kwd "]"
   | E_vector_indexed(iexps) -> 
-    let iformat ppf (i,e) = fprintf ppf "@[<1>%i %a %a %a@]" i kwd " = " pp_exp e kwd "," in
-    let lformat ppf (i,e) = fprintf ppf "@[<1>%i %a %a @]" i kwd " = " pp_exp e in
-    fprintf ppf "@[<0> %a %a %a @]" kwd "[" (list_pp iformat lformat) iexps kwd "]"
-  | E_vector_access(v,e) -> fprintf ppf "@[<0>%a %a %a %a@]" pp_exp v kwd "[" pp_exp e kwd "]"
-  | E_vector_subrange(v,e1,e2) -> fprintf ppf "@[<0> %a %a %a %a %a %a@]" pp_exp v kwd "[" pp_exp e1 kwd " : " pp_exp e1 kwd "]"
+    let iformat ppf (i,e) = fprintf ppf "@[<1>%i%a %a%a@]" i kwd " = " pp_exp e kwd "," in
+    let lformat ppf (i,e) = fprintf ppf "@[<1>%i%a %a@]" i kwd " = " pp_exp e in
+    fprintf ppf "@[<0> %a%a%a@]" kwd "[" (list_pp iformat lformat) iexps kwd "]"
+  | E_vector_access(v,e) -> fprintf ppf "@[<0>%a%a%a%a@]" pp_exp v kwd "[" pp_exp e kwd "]"
+  | E_vector_subrange(v,e1,e2) -> fprintf ppf "@[<0>%a%a%a%a%a%a@]" pp_exp v kwd "[" pp_exp e1 kwd " : " pp_exp e1 kwd "]"
   | E_vector_update(v,e1,e2) -> 
-    fprintf ppf "@[<0> %a %a %a %a %a %a %a@]" kwd "[" pp_exp v kwd "with" pp_exp e1 kwd " = " pp_exp e2 kwd "]"
+    fprintf ppf "@[<0>%a%a %a %a%a%a%a@]" kwd "[" pp_exp v kwd "with" pp_exp e1 kwd " = " pp_exp e2 kwd "]"
   | E_vector_update_subrange(v,e1,e2,e3) -> 
     fprintf ppf "@[<0>%a%a %a %a %a %a %a %a %a@]" kwd "[" pp_exp v kwd "with" pp_exp e1 kwd ":" pp_exp e2 kwd " = " pp_exp e3 kwd "]"
-  | E_list(exps) -> fprintf ppf "@[<0> %a %a %a@]" kwd "[|" (list_pp pp_comma_exp pp_exp) exps kwd "|]"
-  | E_cons(e1,e2) -> fprintf ppf "@[<0> %a %a %a@]" pp_exp e1 kwd ":" pp_exp e2
-  | E_record(FES_aux(FES_Fexps(fexps,_),_)) -> fprintf ppf "@[<0> %a %a %a@]" kwd "{" (list_pp pp_semi_fexp pp_fexp) fexps kwd "}"
+  | E_list(exps) -> fprintf ppf "@[<0>%a%a%a@]" kwd "[||" (list_pp pp_comma_exp pp_exp) exps kwd "||]"
+  | E_cons(e1,e2) -> fprintf ppf "@[<0>%a%a%a@]" pp_exp e1 kwd ":" pp_exp e2
+  | E_record(FES_aux(FES_Fexps(fexps,_),_)) -> fprintf ppf "@[<0>%a%a%a@]" kwd "{" (list_pp pp_semi_fexp pp_fexp) fexps kwd "}"
   | E_record_update(exp,(FES_aux(FES_Fexps(fexps,_),_))) ->
-    fprintf ppf "@[<0> %a %a %a %a %a @]" kwd "{" pp_exp exp kwd " with " (list_pp pp_semi_fexp pp_fexp) fexps kwd "}"
-  | E_field(fexp,id) -> fprintf ppf "@[<0> %a%a%a@]" pp_exp fexp kwd "." pp_id id
-  | E_case(exp,pexps) -> fprintf ppf "@[<0> %a %a %a %a %a@]" kwd "switch " pp_exp exp kwd "{" (list_pp pp_case pp_case) pexps kwd "}"
-  | E_let(leb,exp) -> fprintf ppf "@[<0> %a@ %a@ %a @]" pp_let leb kwd "in" pp_exp exp
-  | E_assign(lexp,exp) -> fprintf ppf "@[<0> %a %a %a@]" pp_lexp lexp kwd " := " pp_exp exp
+    fprintf ppf "@[<0>%a%a %a %a%a@]" kwd "{" pp_exp exp kwd " with " (list_pp pp_semi_fexp pp_fexp) fexps kwd "}"
+  | E_field(fexp,id) -> fprintf ppf "@[<0>%a%a%a@]" pp_exp fexp kwd "." pp_id id
+  | E_case(exp,pexps) -> fprintf ppf "@[<0>%a %a %a %a %a@]" kwd "switch " pp_exp exp kwd "{" (list_pp pp_case pp_case) pexps kwd "}"
+  | E_let(leb,exp) -> fprintf ppf "@[<0>%a@ %a@ %a@]" pp_let leb kwd "in" pp_exp exp
+  | E_assign(lexp,exp) -> fprintf ppf "@[<0>%a%a%a@]" pp_lexp lexp kwd " := " pp_exp exp
 
-and pp_semi_exp ppf e = fprintf ppf "@[<1>%a %a@]" pp_exp e kwd ";"
+and pp_semi_exp ppf e = fprintf ppf "@[<1>%a%a@]" pp_exp e kwd ";"
 
-and pp_comma_exp ppf e = fprintf ppf "@[<1>%a %a@]" pp_exp e kwd ","
+and pp_comma_exp ppf e = fprintf ppf "@[<1>%a%a@]" pp_exp e kwd ","
 
 and pp_fexp ppf (FE_aux(FE_Fexp(id,exp),_)) = fprintf ppf "@[<1>%a %a %a@]" pp_id id kwd " = " pp_exp exp
-and pp_semi_fexp ppf fexp = fprintf ppf "@[<1>%a %a@]" pp_fexp fexp kwd ";"
+and pp_semi_fexp ppf fexp = fprintf ppf "@[<1>%a%a@]" pp_fexp fexp kwd ";"
 
 and pp_case ppf (Pat_aux(Pat_exp(pat,exp),_)) = 
-  fprintf ppf "@[<1>%a %a@ @[<1> %a @] @]" pp_pat_atomic pat kwd "-> " pp_exp exp 
+  fprintf ppf "@[<1>%a %a@@[<1>%a@]@]" pp_pat_atomic pat kwd "-> " pp_exp exp 
 
 and pp_lexp ppf (LEXP_aux(lexp,_)) =
   match lexp with
   | LEXP_id(id) -> pp_id ppf id
   | LEXP_memory(id,args) -> fprintf ppf "@[%a(%a)@]" pp_id id (list_pp pp_exp pp_exp) args
-  | LEXP_vector(v,exp) -> fprintf ppf "@[%a %a %a %a@]" pp_lexp v kwd "[" pp_exp exp kwd "]"
-  | LEXP_vector_range(v,e1,e2) -> fprintf ppf "@[%a %a %a %a %a %a@]" pp_lexp v kwd "[" pp_exp e1 kwd ":" pp_exp e2 kwd "]"
+  | LEXP_vector(v,exp) -> fprintf ppf "@[%a%a%a%a@]" pp_lexp v kwd "[" pp_exp exp kwd "]"
+  | LEXP_vector_range(v,e1,e2) -> fprintf ppf "@[%a%a%a%a%a%a@]" pp_lexp v kwd "[" pp_exp e1 kwd ":" pp_exp e2 kwd "]"
   | LEXP_field(v,id) -> fprintf ppf "@[%a%a%a@]" pp_lexp v kwd "." pp_id id
 
 let pp_default ppf (DT_aux(df,_)) =
@@ -281,8 +282,8 @@ let pp_namescm ppf (Name_sect_aux(ns,_)) =
 let rec pp_range ppf (BF_aux(r,_)) =
   match r with 
   | BF_single(i) -> fprintf ppf "%i" i
-  | BF_range(i1,i2) -> fprintf ppf "%i .. %i" i1 i2
-  | BF_concat(ir1,ir2) -> fprintf ppf "%a %a %a" pp_range ir1 kwd ", " pp_range ir2
+  | BF_range(i1,i2) -> fprintf ppf "%i..%i" i1 i2
+  | BF_concat(ir1,ir2) -> fprintf ppf "%a%a %a" pp_range ir1 kwd ", " pp_range ir2
 
 let pp_typdef ppf (TD_aux(td,_)) =
   match td with
@@ -291,7 +292,7 @@ let pp_typdef ppf (TD_aux(td,_)) =
   | TD_record(id,nm,typq,fs,_) -> 
     let f_pp ppf (typ,id) =
       fprintf ppf "@[<1>%a %a%a@]" pp_typ typ pp_id id kwd ";" in
-    fprintf ppf "@[<0>%a %a %a %a %a %a %a %a@[<1>%a@] %a]@\n" 
+    fprintf ppf "@[<0>%a %a %a%a %a %a %a%a@[<1>%a@]%a@]@\n" 
       kwd "typedef" pp_id id pp_namescm nm kwd "=" kwd "const" kwd "struct" pp_typquant typq kwd "{" (list_pp f_pp f_pp) fs kwd "}"
   | TD_variant(id,nm,typq,ar,_) ->
     let a_pp ppf (Tu_aux(typ_u,_)) = 
@@ -299,16 +300,16 @@ let pp_typdef ppf (TD_aux(td,_)) =
       | Tu_ty_id(typ,id) -> fprintf ppf "@[<1>%a %a%a@]" pp_typ typ pp_id id kwd ";" 
       | Tu_id(id) -> fprintf ppf "@[<1>%a%a@]" pp_id id kwd ";"
     in
-    fprintf ppf "@[<0>%a %a %a %a %a %a %a %a@[<1>%a@] %a]@\n" 
+    fprintf ppf "@[<0>%a %a %a %a %a %a %a %a@[<1>%a@] %a@]@\n" 
       kwd "typedef" pp_id id pp_namescm nm kwd "=" kwd "const" kwd "union" pp_typquant typq kwd "{" (list_pp a_pp a_pp) ar kwd "}"
   | TD_enum(id,ns,enums,_) ->
     let pp_id_semi ppf id = fprintf ppf "%a%a " pp_id id kwd ";" in
     fprintf ppf "@[<0>%a %a %a %a %a %a%a %a@]@\n"
       kwd "typedef" pp_id id pp_namescm ns kwd "=" kwd "enumerate" kwd "{" (list_pp pp_id_semi pp_id) enums kwd "}"
   | TD_register(id,n1,n2,rs) -> 
-    let pp_rid ppf (r,id) = fprintf ppf "%a %a %a%a " pp_range r kwd ":" pp_id id kwd ";" in
+    let pp_rid ppf (r,id) = fprintf ppf "%a%a%a%a " pp_range r kwd ":" pp_id id kwd ";" in
     let pp_rids = (list_pp pp_rid pp_rid) in
-    fprintf ppf "@[<0>%a %a %a %a %a %a %a %a %a %a %a %a%a@]@\n"
+    fprintf ppf "@[<0>%a %a %a %a %a %a%a%a%a%a %a%a%a@]@\n"
      kwd "typedef" pp_id id kwd "=" kwd "register" kwd "bits" kwd "[" pp_nexp n1 kwd ":" pp_nexp n2 kwd "]" kwd "{" pp_rids rs kwd "}"
 
 let pp_rec ppf (Rec_aux(r,_)) =
@@ -318,7 +319,7 @@ let pp_rec ppf (Rec_aux(r,_)) =
 
 let pp_tannot_opt ppf (Typ_annot_opt_aux(t,_)) =
   match t with
-  | Typ_annot_opt_some(tq,typ) -> fprintf ppf "%a %a " pp_typquant tq pp_typ typ
+  | Typ_annot_opt_some(tq,typ) -> fprintf ppf "%a%a " pp_typquant tq pp_typ typ
 
 let pp_effects_opt ppf (Effect_opt_aux(e,_)) =
   match e with
@@ -326,11 +327,11 @@ let pp_effects_opt ppf (Effect_opt_aux(e,_)) =
   | Effect_opt_effect e -> fprintf ppf "effect %a" pp_effects e
 
 let pp_funcl ppf (FCL_aux(FCL_Funcl(id,pat,exp),_)) =
-  fprintf ppf "@[<0>%a %a %a @[<1>%a@] @]@\n" pp_id id pp_pat_atomic pat kwd "=" pp_exp exp 
+  fprintf ppf "%a %a %a @[<1>%a@]@\n" pp_id id pp_pat_atomic pat kwd "=" pp_exp exp 
 
 let pp_fundef ppf (FD_aux(FD_function(r, typa, efa, fcls),_)) =
   let pp_funcls ppf funcl = fprintf ppf "%a %a" kwd "and" pp_funcl funcl in
-  fprintf ppf "@[<0>%a %a%a%a %a@ @[<1>%a@] @]@\n"
+  fprintf ppf "@[<0>%a %a%a%a @[<1>%a@] @[<1>%a@] @]@\n"
     kwd "function" pp_rec r pp_tannot_opt typa pp_effects_opt efa pp_funcl (List.hd fcls) (list_pp pp_funcls pp_funcls) (List.tl fcls)
 
 let pp_def ppf (DEF_aux(d,(l,_))) =
@@ -339,7 +340,7 @@ let pp_def ppf (DEF_aux(d,(l,_))) =
   | DEF_spec(v_spec) -> pp_spec ppf v_spec
   | DEF_type(t_def) -> pp_typdef ppf t_def
   | DEF_fundef(f_def) -> pp_fundef ppf f_def
-  | DEF_val(lbind) -> pp_let ppf lbind
+  | DEF_val(lbind) -> fprintf ppf "@[<0>%a@]@\n" pp_let lbind
   | DEF_reg_dec(typ,id) -> fprintf ppf "@[<0>%a %a %a@]@\n" kwd "register" pp_typ typ pp_id id
   | _ -> raise (Reporting_basic.err_unreachable l "initial_check didn't remove all scattered Defs")