Fix various boolean type-variable related issues

Remove some dead code in Pretty_print_common

Start thinking a bit about Minisail-esque syntactic sugar in initial_check

8 files changed, 33 insertions, 135 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index 8544700b..6c67e6e7 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -143,6 +143,10 @@ let is_typ_kopt = function
   | KOpt_aux (KOpt_kind (K_aux (K_type, _), _), _) -> true
   | _ -> false
 
+let is_bool_kopt = function
+  | KOpt_aux (KOpt_kind (K_aux (K_bool, _), _), _) -> true
+  | _ -> false
+       
 let string_of_kid = function
   | Kid_aux (Var v, _) -> v
 
@@ -321,6 +325,9 @@ let mk_infix_id str = Id_aux (DeIid str, Parse_ast.Unknown)
 
 let mk_id_typ id = Typ_aux (Typ_id id, Parse_ast.Unknown)
 
+let mk_kopt kind_aux id =
+  KOpt_aux (KOpt_kind (K_aux (kind_aux, Parse_ast.Unknown), id), Parse_ast.Unknown)
+
 let mk_ord ord_aux = Ord_aux (ord_aux, Parse_ast.Unknown)
 
 let unknown_typ = mk_typ Typ_internal_unknown
@@ -673,6 +680,7 @@ and string_of_typ_aux = function
   | Typ_var kid -> string_of_kid kid
   | Typ_tup typs -> "(" ^ string_of_list ", " string_of_typ typs ^ ")"
   | Typ_app (id, args) when Id.compare id (mk_id "atom") = 0 -> "int(" ^ string_of_list ", " string_of_typ_arg args ^ ")"
+  | Typ_app (id, args) when Id.compare id (mk_id "atom_bool") = 0 -> "bool(" ^ string_of_list ", " string_of_typ_arg args ^ ")"
   | Typ_app (id, args) -> string_of_id id ^ "(" ^ string_of_list ", " string_of_typ_arg args ^ ")"
   | Typ_fn ([typ_arg], typ_ret, eff) ->
      string_of_typ typ_arg ^ " -> " ^ string_of_typ typ_ret ^ " effect " ^ string_of_effect eff
diff --git a/src/ast_util.mli b/src/ast_util.mli
index fe36dfb6..c0123ce1 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -90,6 +90,7 @@ val mk_qi_nc : n_constraint -> quant_item
 val mk_qi_kopt : kinded_id -> quant_item
 val mk_fexp : id -> unit exp -> unit fexp
 val mk_letbind : unit pat -> unit exp -> unit letbind
+val mk_kopt : kind_aux -> kid -> kinded_id
 
 val unaux_exp : 'a exp -> 'a exp_aux
 val unaux_pat : 'a pat -> 'a pat_aux
@@ -110,7 +111,8 @@ val kopt_kid : kinded_id -> kid
 val is_nat_kopt : kinded_id -> bool
 val is_order_kopt : kinded_id -> bool
 val is_typ_kopt : kinded_id -> bool
-
+val is_bool_kopt : kinded_id -> bool
+  
 (* Some handy utility functions for constructing types. *)
 val mk_typ : typ_aux -> typ
 val mk_typ_arg : typ_arg_aux -> typ_arg
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 44f36892..da6c7b84 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -96,7 +96,7 @@ let to_ast_id (P.Id_aux(id, l)) =
              | P.DeIid x -> DeIid x),
             l)
 
-let to_ast_var (P.Kid_aux(P.Var v,l)) = Kid_aux(Var v,l)
+let to_ast_var (P.Kid_aux (P.Var v, l)) = Kid_aux (Var v, l)
 
 let to_ast_effects = function
   | P.ATyp_aux (P.ATyp_set effects, l) ->
@@ -161,6 +161,8 @@ let rec to_ast_typ ctx (P.ATyp_aux (aux, l)) =
        let kids = List.map to_ast_var kids in
        let ctx = { ctx with kinds = List.fold_left (fun kinds kid -> KBindings.add kid K_int kinds) ctx.kinds kids } in
        Typ_exist (kids, to_ast_constraint ctx nc, to_ast_typ ctx atyp)
+    | P.ATyp_base (id, kind, nc) ->
+       raise (Reporting.err_unreachable l __POS__ "TODO")
     | _ -> raise (Reporting.err_typ l "Invalid type")
   in
   Typ_aux (aux, l)
@@ -763,6 +765,7 @@ let initial_ctx = {
           ("atom", [K_int]);
           ("implicit", [K_int]);
           ("itself", [K_int]);
+          ("not", [K_bool]);
         ];
     kinds = KBindings.empty;
     scattereds = Bindings.empty;
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index c57daa26..a5dbf66e 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -164,6 +164,7 @@ atyp_aux =  (* expressions of all kinds, to be translated to types, nats, orders
  | ATyp_tup of (atyp) list (* Tuple type *)
  | ATyp_app of id * (atyp) list (* type constructor application *)
  | ATyp_exist of kid list * atyp * atyp
+ | ATyp_base of id * atyp * atyp
 
 and atyp = 
    ATyp_aux of atyp_aux * l
diff --git a/src/parser.mly b/src/parser.mly
index 83e6936d..544438c0 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -555,6 +555,8 @@ atomic_typ:
     { mk_typ (ATyp_exist ($2, ATyp_aux (ATyp_lit (L_aux (L_true, loc $startpos $endpos)), loc $startpos $endpos), $4)) $startpos $endpos }
   | Lcurly kid_list Comma typ Dot typ Rcurly
     { mk_typ (ATyp_exist ($2, $4, $6)) $startpos $endpos }
+  | Lcurly id Colon typ Dot typ Rcurly
+    { mk_typ (ATyp_base ($2, $4, $6)) $startpos $endpos }
 
 typ_list:
   | typ
diff --git a/src/pretty_print_common.ml b/src/pretty_print_common.ml
index 0f1dee90..c01896ac 100644
--- a/src/pretty_print_common.ml
+++ b/src/pretty_print_common.ml
@@ -94,133 +94,5 @@ let rec doc_range (BF_aux(r,_)) = match r with
   | BF_range(i1,i2) -> doc_op dotdot (doc_int i1) (doc_int i2)
   | BF_concat(ir1,ir2) -> (doc_range ir1) ^^ comma ^^ (doc_range ir2)
 
-let doc_effect (BE_aux (e,_)) =
-  string (match e with
-  | BE_rreg -> "rreg"
-  | BE_wreg -> "wreg"
-  | BE_rmem -> "rmem"
-  | BE_rmemt -> "rmemt"
-  | BE_wmem -> "wmem"
-  | BE_wmv  -> "wmv"
-  | BE_wmvt  -> "wmvt"
-  (*| BE_lset -> "lset"
-  | BE_lret -> "lret"*)
-  | BE_eamem -> "eamem"
-  | BE_exmem -> "exmem"
-  | BE_barr -> "barr"
-  | BE_depend -> "depend"
-  | BE_escape -> "escape"
-  | BE_undef -> "undef"
-  | BE_unspec -> "unspec"
-  | BE_nondet -> "nondet"
-  | BE_config -> "config")
-
-let doc_effects (Effect_aux(e,_)) = match e with
-  | Effect_set [] -> string "pure"
-  | Effect_set s -> braces (separate_map comma_sp doc_effect s)
-
-let doc_ord (Ord_aux(o,_)) = match o with
-  | Ord_var v -> doc_var v
-  | Ord_inc -> string "inc"
-  | Ord_dec -> string "dec"
-
-let doc_typ, doc_atomic_typ, doc_nexp, doc_nexp_constraint =
-  (* following the structure of parser for precedence *)
-  let rec typ ty = fn_typ ty
-  and fn_typ ((Typ_aux (t, _)) as ty) = match t with
-  | Typ_fn(args,ret,efct) ->
-     separate space [parens (separate_map (comma ^^ space) tup_typ args); arrow; fn_typ ret; string "effect"; doc_effects efct]
-  | Typ_bidir (t1, t2) ->
-     separate space [tup_typ t1; bidir; tup_typ t2]
-  | _ -> tup_typ ty
-  and tup_typ ((Typ_aux (t, _)) as ty) = match t with
-  | Typ_exist (kids, nc, ty) ->
-     separate space [string "exist"; separate_map space doc_var kids ^^ comma; nexp_constraint nc ^^ dot; typ ty]
-  | Typ_tup typs -> parens (separate_map comma_sp app_typ typs)
-  | _ -> app_typ ty
-  and app_typ ((Typ_aux (t, _)) as ty) = match t with
-  | Typ_app(Id_aux (Id "range", _), [
-    A_aux(A_nexp (Nexp_aux(Nexp_constant n, _)), _);
-    A_aux(A_nexp m, _);]) ->
-    (squarebars (if Big_int.equal n Big_int.zero then nexp m else doc_op colon (doc_int n) (nexp m)))
-  | Typ_app(Id_aux (Id "atom", _), [A_aux(A_nexp n,_)]) ->
-     (squarecolons (nexp n))
-  | Typ_app(id,args) ->
-      (* trailing space to avoid >> token in case of nested app types *)
-      (doc_id id) ^^ (angles (separate_map comma_sp doc_typ_arg args)) ^^ space
-  | _ -> atomic_typ ty (* for simplicity, skip vec_typ - which is only sugar *)
-  and atomic_typ ((Typ_aux (t, _)) as ty) = match t with
-  | Typ_id id  -> doc_id id
-  | Typ_var v  -> doc_var v
-  | Typ_app _ | Typ_tup _ | Typ_fn _ | Typ_bidir _ | Typ_exist _ ->
-      (* exhaustiveness matters here to avoid infinite loops
-       * if we add a new Typ constructor *)
-     group (parens (typ ty))
-  | Typ_internal_unknown -> string "UNKNOWN"
-
-  and doc_typ_arg (A_aux(t,_)) = match t with
-  (* Be careful here because typ_arg is implemented as nexp in the
-   * parser - in practice falling through app_typ after all the proper nexp
-   * cases; so A_typ has the same precedence as a Typ_app *)
-  | A_typ t -> app_typ t
-  | A_nexp n -> nexp n
-  | A_order o -> doc_ord o
-
-  (* same trick to handle precedence of nexp *)
-  and nexp ne = sum_typ ne
-  and sum_typ ((Nexp_aux(n,_)) as ne) = match n with
-  | Nexp_sum(n1,n2) -> doc_op plus (sum_typ n1) (star_typ n2)
-  | Nexp_minus(n1,n2) -> doc_op minus (sum_typ n1) (star_typ n2)
-  | _ -> star_typ ne
-  and star_typ ((Nexp_aux(n,_)) as ne) = match n with
-  | Nexp_times(n1,n2) -> doc_op star (star_typ n1) (exp_typ n2)
-  | _ -> exp_typ ne
-  and exp_typ ((Nexp_aux(n,_)) as ne) = match n with
-  | Nexp_exp n1 -> doc_unop (string "2**") (atomic_nexp_typ n1)
-  | _ -> neg_typ ne
-  and neg_typ ((Nexp_aux(n,_)) as ne) = match n with
-  | Nexp_neg n1 ->
-      (* XXX this is not valid Sail, only an internal representation -
-       * work around by commenting it *)
-      let minus = concat [string "(*"; minus; string "*)"] in
-      minus ^^ (atomic_nexp_typ n1)
-  | _ -> atomic_nexp_typ ne
-  and atomic_nexp_typ ((Nexp_aux(n,_)) as ne) = match n with
-    | Nexp_var v -> doc_var v
-    | Nexp_id i  -> braces (doc_id i)
-    | Nexp_app (op, args) -> doc_id op ^^ parens (separate_map (comma ^^ space) nexp args)
-    | Nexp_constant i -> if Big_int.less i Big_int.zero then parens(doc_int i) else doc_int i
-    | Nexp_neg _ | Nexp_exp _ | Nexp_times _ | Nexp_sum _ | Nexp_minus _->
-      group (parens (nexp ne))
-
-  and nexp_constraint (NC_aux(nc,_)) = match nc with
-    | NC_equal(n1,n2) -> doc_op equals (nexp n1) (nexp n2)
-    | NC_not_equal (n1, n2) -> doc_op (string "!=") (nexp n1) (nexp n2)
-    | NC_bounded_ge(n1,n2) -> doc_op (string ">=") (nexp n1) (nexp n2)
-    | NC_bounded_le(n1,n2) -> doc_op (string "<=") (nexp n1) (nexp n2)
-    | NC_set(v,bounds) ->
-       doc_op (string "IN") (doc_var v)
-              (braces (separate_map comma_sp doc_int bounds))
-    | NC_or (nc1, nc2) ->
-       parens (separate space [nexp_constraint nc1; string "|"; nexp_constraint nc2])
-    | NC_and (nc1, nc2) ->
-       separate space [nexp_constraint nc1; string "&"; nexp_constraint nc2]
-    | NC_true -> string "true"
-    | NC_false -> string "false"
-
-  (* expose doc_typ, doc_atomic_typ, doc_nexp and doc_nexp_constraint *)
-  in typ, atomic_typ, nexp, nexp_constraint
-
-let pp_format_id (Id_aux(i,_)) =
-  match i with
-  | Id(i) -> i
-  | DeIid(x) -> "(deinfix " ^ x ^ ")"
-
-let rec list_format (sep : string) (fmt : 'a -> string) (ls : 'a list) : string =
-  match ls with
-  | [] -> ""
-  | [a] -> fmt a
-  | a::ls -> (fmt a) ^ sep ^ (list_format sep fmt ls)
-
 let print ?(len=100) channel doc = ToChannel.pretty 1. len channel doc
 let to_buf ?(len=100) buf doc = ToBuffer.pretty 1. len buf doc
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 94bcd54b..f756f3d2 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -113,7 +113,7 @@ let rec doc_nexp =
   in
   nexp0
 
-let doc_nc nc =
+let rec doc_nc nc =
   let nc_op op n1 n2 = separate space [doc_nexp n1; string op; doc_nexp n2] in
   let rec atomic_nc (NC_aux (nc_aux, _) as nc) =
     match nc_aux with
@@ -125,7 +125,10 @@ let doc_nc nc =
     | NC_bounded_le (n1, n2) -> nc_op "<=" n1 n2
     | NC_set (kid, ints) ->
        separate space [doc_kid kid; string "in"; braces (separate_map (comma ^^ space) doc_int ints)]
-    | _ -> nc0 ~parenthesize:true nc
+    | NC_app (id, args) ->
+       doc_id id ^^ parens (separate_map (comma ^^ space) doc_typ_arg args)
+    | NC_var kid -> doc_kid kid
+    | NC_or _ | NC_and _ -> nc0 ~parenthesize:true nc
   and nc0 ?parenthesize:(parenthesize=false) (NC_aux (nc_aux, _) as nc) =
     (* Rather than parens (nc0 x) we use nc0 ~parenthesize:true x, because if
        we rewrite a disjunction as a set constraint, then we can
@@ -151,7 +154,7 @@ let doc_nc nc =
   in
   atomic_nc (constraint_simp nc)
 
-let rec doc_typ ?(simple=false) (Typ_aux (typ_aux, l)) =
+and doc_typ ?(simple=false) (Typ_aux (typ_aux, l)) =
   match typ_aux with
   | Typ_id id -> doc_id id
   | Typ_app (id, []) -> doc_id id
@@ -186,6 +189,7 @@ and doc_typ_arg (A_aux (ta_aux, _)) =
   | A_typ typ -> doc_typ typ
   | A_nexp nexp -> doc_nexp nexp
   | A_order o -> doc_ord o
+  | A_bool nc -> doc_nc nc
 and doc_arg_typs = function
   | [typ] -> doc_typ typ
   | typs -> parens (separate_map (comma ^^ space) doc_typ typs)
diff --git a/src/type_check.ml b/src/type_check.ml
index 51625d4a..2f4561b5 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -449,7 +449,8 @@ end = struct
         ("real", []);
         ("list", [K_type]);
         ("string", []);
-        ("itself", [K_int])
+        ("itself", [K_int]);
+        ("atom_bool", [K_bool])
       ]
 
   let builtin_mappings =
@@ -499,6 +500,8 @@ end = struct
          subst_args kopts args
       | kopt :: kopts, A_aux (A_order arg, _) :: args when is_order_kopt kopt ->
          subst_args kopts args
+      | kopt :: kopts, A_aux (A_bool arg, _) :: args when is_bool_kopt kopt ->
+         subst_args kopts args
       | [], [] -> ncs
       | _, A_aux (_, l) :: _ -> typ_error l ("Error when processing type quantifer arguments " ^ string_of_typquant typq)
       | _, _ -> typ_error Parse_ast.Unknown ("Error when processing type quantifer arguments " ^ string_of_typquant typq)
@@ -1624,8 +1627,9 @@ let rec alpha_equivalent env typ1 typ2 =
     in
     Typ_aux (relabelled_aux, l)
   and relabel_arg (A_aux (aux, l) as arg) =
+    (* FIXME relabel constraint *)
     match aux with
-    | A_nexp _ | A_order _ -> arg
+    | A_nexp _ | A_order _ | A_bool _ -> arg
     | A_typ typ -> A_aux (A_typ (relabel typ), l)
   in
 
@@ -1729,6 +1733,8 @@ let rec subtyp l env typ1 typ2 =
   match typ_aux1, typ_aux2 with
   | _, Typ_internal_unknown when Env.allow_unknowns env -> ()
 
+  | Typ_app (id1, _), Typ_id id2 when string_of_id id1 = "atom_bool" && string_of_id id2 = "bool" -> ()
+                                                         
   | Typ_tup typs1, Typ_tup typs2 when List.length typs1 = List.length typs2 ->
      List.iter2 (subtyp l env) typs1 typs2