Add bool in default environment

src/bin/expect_tests/contract_tests.ml

@@ -1425,7 +1425,7 @@ let%expect_test _ =
 let%expect_test _ =
   run_ligo_bad [ "compile-contract" ; bad_contract "redundant_constructors.mligo" ; "main" ] ;
   [%expect {|
-    ligo: redundant constructor:  {"constructor":"Add","environment":"- E[]\tT[union_a -> sum[Add -> int , Remove -> int]] ]"}
+    ligo: redundant constructor:  {"constructor":"Add","environment":"- E[]\tT[union_a -> sum[Add -> int , Remove -> int]]\n- E[]\tT[bool -> sum[false -> unit , true -> unit]]]"}
 
 
      If you're not sure how to fix this error, you can
@@ -1465,7 +1465,7 @@ ligo: in file "create_contract_var.mligo", line 6, character 35 to line 10, char
 
   run_ligo_bad [ "compile-contract" ; bad_contract "create_contract_no_inline.mligo" ; "main" ] ;
   [%expect {|
-    ligo: in file "create_contract_no_inline.mligo", line 3, characters 40-46. unbound type variable:  {"variable":"return","location":"in file \"create_contract_no_inline.mligo\", line 3, characters 40-46","in":"- E[foo -> int]\tT[] ]","did_you_mean":"no suggestion"}
+    ligo: in file "create_contract_no_inline.mligo", line 3, characters 40-46. unbound type variable:  {"variable":"return","location":"in file \"create_contract_no_inline.mligo\", line 3, characters 40-46","in":"- E[foo -> int]\tT[] - E[]\tT[bool -> sum[false -> unit , true -> unit]]]","did_you_mean":"no suggestion"}
 
 
      If you're not sure how to fix this error, you can

src/bin/expect_tests/typer_error_tests.ml

@@ -93,7 +93,7 @@ let%expect_test _ =
 
   run_ligo_bad [ "compile-contract" ; "../../test/contracts/negative/error_typer_3.mligo" ; "main" ] ;
   [%expect {|
-    ligo: in file "error_typer_3.mligo", line 3, characters 34-53. tuples have different sizes: Expected these two types to be the same, but they're different (both are tuples, but with a different number of arguments) {"a":"( int * string * bool )","b":"( int * string )"}
+    ligo: in file "error_typer_3.mligo", line 3, characters 34-53. tuples have different sizes: Expected these two types to be the same, but they're different (both are tuples, but with a different number of arguments) {"a":"( int * string * sum[false -> unit , true -> unit] )","b":"( int * string )"}
 
 
      If you're not sure how to fix this error, you can
@@ -106,7 +106,7 @@ let%expect_test _ =
 
   run_ligo_bad [ "compile-contract" ; "../../test/contracts/negative/error_typer_4.mligo" ; "main" ] ;
   [%expect {|
-    ligo: in file "error_typer_4.mligo", line 4, characters 17-56. different keys in records:  {"key_a":"c","key_b":"b","a":"record[a -> int , c -> bool , d -> string]","b":"record[a -> int , b -> string , c -> bool]"}
+    ligo: in file "error_typer_4.mligo", line 4, characters 17-56. different keys in records:  {"key_a":"c","key_b":"b","a":"record[a -> int , c -> sum[false -> unit , true -> unit] , d -> string]","b":"record[a -> int , b -> string , c -> sum[false -> unit , true -> unit]]"}
 
 
      If you're not sure how to fix this error, you can
@@ -119,7 +119,7 @@ let%expect_test _ =
 
   run_ligo_bad [ "compile-contract" ; "../../test/contracts/negative/error_typer_5.mligo" ; "main" ] ;
   [%expect {|
-    ligo: in file "error_typer_5.mligo", line 1, characters 10-17. unbound type variable:  {"variable":"boolean","location":"in file \"error_typer_5.mligo\", line 1, characters 10-17","in":"- E[]\tT[] ]","did_you_mean":"bool"}
+    ligo: in file "error_typer_5.mligo", line 1, characters 10-17. unbound type variable:  {"variable":"boolean","location":"in file \"error_typer_5.mligo\", line 1, characters 10-17","in":"- E[]\tT[] - E[]\tT[bool -> sum[false -> unit , true -> unit]]]","did_you_mean":"bool"}
 
 
      If you're not sure how to fix this error, you can
@@ -132,7 +132,7 @@ let%expect_test _ =
 
   run_ligo_bad [ "compile-contract" ; "../../test/contracts/negative/error_typer_6.mligo" ; "main" ] ;
   [%expect {|
-    ligo: in file "error_typer_6.mligo", line 1, characters 30-64. different type constructors: Expected these two constant type constructors to be the same, but they're different {"a":"string","b":"bool"}
+    ligo: in file "error_typer_6.mligo", line 1, characters 30-64. different kinds:  {"a":"string","b":"sum[false -> unit , true -> unit]"}
 
 
      If you're not sure how to fix this error, you can
@@ -145,7 +145,7 @@ let%expect_test _ =
 
   run_ligo_bad [ "compile-contract" ; "../../test/contracts/negative/error_typer_7.mligo" ; "main" ] ;
   [%expect {|
-    ligo: in file "error_typer_7.mligo", line 4, characters 18-48. records have different sizes: Expected these two types to be the same, but they're different (both are records, but with a different number of arguments) {"a":"record[a -> int , b -> string]","b":"record[a -> int , b -> string , c -> bool]"}
+    ligo: in file "error_typer_7.mligo", line 4, characters 18-48. records have different sizes: Expected these two types to be the same, but they're different (both are records, but with a different number of arguments) {"a":"record[a -> int , b -> string]","b":"record[a -> int , b -> string , c -> sum[false -> unit , true -> unit]]"}
 
 
      If you're not sure how to fix this error, you can

src/environment/bool.ml

@@ -1,3 +1,4 @@
 open Ast_typed
+open Stage_common.Constant
 
-let environment = env_sum_type ~type_name:(Var.of_name "bool") @@ [(Constructor "true",t_unit ());(Constructor "false",t_unit ())]
+let environment = env_sum_type ~type_name:t_bool @@ [(Constructor "true",{ctor_type=t_unit ();michelson_annotation=None});(Constructor "false",{ctor_type=t_unit ();michelson_annotation=None})]

src/environment/dune

@@ -5,6 +5,7 @@
     simple-utils
     tezos-utils
     ast_typed
+    stage_common
   )
   (preprocess
     (pps ppx_let bisect_ppx --conditional)

src/passes/10-interpreter/interpreter.ml

@@ -255,7 +255,6 @@ C_STEPS_TO_QUOTA
 (*interpreter*)
 and eval_literal : Ast_typed.literal -> value result = function
   | Literal_unit        -> ok @@ V_Ct (C_unit)
-  | Literal_bool b      -> ok @@ V_Ct (C_bool b)
   | Literal_int i       -> ok @@ V_Ct (C_int i)
   | Literal_nat n       -> ok @@ V_Ct (C_nat n)
   | Literal_timestamp i -> ok @@ V_Ct (C_timestamp i)
@@ -329,6 +328,8 @@ and eval : Ast_typed.expression -> env -> value result
         arguments in
       apply_operator cons_name operands'
     )
+    | E_constructor { constructor = Constructor c ; element } when (c = "true" || c = "false")
+     && element.expression_content = Ast_typed.e_unit () -> ok @@ V_Ct (C_bool (bool_of_string c))
     | E_constructor { constructor = Constructor c ; element } ->
       let%bind v' = eval element env in
       ok @@ V_Construct (c,v')

src/passes/10-transpiler/transpiler.ml

@@ -76,7 +76,7 @@ them. please report this to the developers." in
     error ~data title content
 
   let wrong_mini_c_value expected_type actual =
-    let title () = "illed typed intermediary value" in
+    let title () = "transpiler: illed typed intermediary value" in
     let content () = "type of intermediary value doesn't match what was expected" in
     let data = [
       ("expected_type" , fun () -> expected_type) ;
@@ -231,22 +231,23 @@ let transpile_constant' : AST.constant' -> constant' = function
 
 let rec transpile_type (t:AST.type_expression) : type_value result =
   match t.type_content with
+  | T_variable (name) when Var.equal name Stage_common.Constant.t_bool -> ok (T_base TB_bool)
+  | T_sum (m) when m = (AST.CMap.of_list [(Constructor "true", AST.{ctor_type=t_unit();michelson_annotation=None});(Constructor "false", AST.{ctor_type=t_unit ();michelson_annotation=None})])-> ok (T_base TB_bool)
   | T_variable (name) -> fail @@ no_type_variable @@ name
-  | T_constant (TC_bool) -> ok (T_base TC_bool)
+  | T_constant (TC_int)       -> ok (T_base TB_int)
-  | T_constant (TC_int) -> ok (T_base TC_int)
+  | T_constant (TC_nat)       -> ok (T_base TB_nat)
-  | T_constant (TC_nat) -> ok (T_base TC_nat)
+  | T_constant (TC_mutez)     -> ok (T_base TB_mutez)
-  | T_constant (TC_mutez) -> ok (T_base TC_mutez)
+  | T_constant (TC_string)    -> ok (T_base TB_string)
-  | T_constant (TC_string) -> ok (T_base TC_string)
+  | T_constant (TC_bytes)     -> ok (T_base TB_bytes)
-  | T_constant (TC_bytes) -> ok (T_base TC_bytes)
+  | T_constant (TC_address)   -> ok (T_base TB_address)
-  | T_constant (TC_address) -> ok (T_base TC_address)
+  | T_constant (TC_timestamp) -> ok (T_base TB_timestamp)
-  | T_constant (TC_timestamp) -> ok (T_base TC_timestamp)
+  | T_constant (TC_unit)      -> ok (T_base TB_unit)
-  | T_constant (TC_unit) -> ok (T_base TC_unit)
+  | T_constant (TC_operation) -> ok (T_base TB_operation)
-  | T_constant (TC_operation) -> ok (T_base TC_operation)
+  | T_constant (TC_signature) -> ok (T_base TB_signature)
-  | T_constant (TC_signature) -> ok (T_base TC_signature)
+  | T_constant (TC_key)       -> ok (T_base TB_key)
-  | T_constant (TC_key) -> ok (T_base TC_key)
+  | T_constant (TC_key_hash)  -> ok (T_base TB_key_hash)
-  | T_constant (TC_key_hash) -> ok (T_base TC_key_hash)
+  | T_constant (TC_chain_id)  -> ok (T_base TB_chain_id)
-  | T_constant (TC_chain_id) -> ok (T_base TC_chain_id)
+  | T_constant (TC_void)      -> ok (T_base TB_void)
-  | T_constant (TC_void)     -> ok (T_base TC_void)
   | T_operator (TC_contract x) ->
       let%bind x' = transpile_type x in
       ok (T_contract x')
@@ -362,7 +363,6 @@ let record_access_to_lr : type_value -> type_value AST.label_map -> AST.label ->
   ok lst
 
 let rec transpile_literal : AST.literal -> value = fun l -> match l with
-  | Literal_bool b -> D_bool b
   | Literal_int n -> D_int n
   | Literal_nat n -> D_nat n
   | Literal_timestamp n -> D_timestamp n
@@ -411,6 +411,8 @@ and transpile_annotated_expression (ae:AST.expression) : expression result =
       let%bind a = transpile_annotated_expression lamb in
       let%bind b = transpile_annotated_expression args in
       return @@ E_application (a, b)
+  | E_constructor {constructor=Constructor name;element} when (name="true"||name="false") && element.expression_content = AST.e_unit () ->
+    return @@ E_literal (D_bool (bool_of_string name))
   | E_constructor {constructor;element} -> (
       let%bind param' = transpile_annotated_expression element in
       let (param'_expr , param'_tv) = Combinators.Expression.(get_content param' , get_type param') in

src/passes/10-transpiler/untranspiler.ml

@@ -19,7 +19,7 @@ them. please report this to the developers." in
     error ~data title content
 
   let wrong_mini_c_value expected_type actual =
-    let title () = "illed typed intermediary value" in
+    let title () = "untranspiler: illed typed intermediary value" in
     let content () = "type of intermediary value doesn't match what was expected" in
     let data = [
       ("expected_type" , fun () -> expected_type) ;
@@ -44,6 +44,18 @@ let rec untranspile (v : value) (t : AST.type_expression) : AST.expression resul
   let open! AST in
   let return e = ok (make_a_e_empty e t) in
   match t.type_content with
+  | T_variable (name) when Var.equal name Stage_common.Constant.t_bool -> (
+        let%bind b =
+          trace_strong (wrong_mini_c_value "bool" v) @@
+          get_bool v in
+        return (e_bool b Environment.full_empty)
+      )
+  | T_sum m when m = CMap.of_list [(Constructor "true",{ctor_type=t_unit ();michelson_annotation=None});(Constructor "false",{ctor_type=t_unit ();michelson_annotation=None})] -> (
+        let%bind b =
+          trace_strong (wrong_mini_c_value "bool" v) @@
+          get_bool v in
+        return (e_bool b Environment.full_empty)
+      )
   | T_constant type_constant -> (
     match type_constant with
     | TC_unit -> (
@@ -52,12 +64,6 @@ let rec untranspile (v : value) (t : AST.type_expression) : AST.expression resul
           get_unit v in
         return (E_literal Literal_unit)
       )
-    | TC_bool -> (
-        let%bind b =
-          trace_strong (wrong_mini_c_value "bool" v) @@
-          get_bool v in
-        return (E_literal (Literal_bool b))
-      )
     | TC_int -> (
         let%bind n =
           trace_strong (wrong_mini_c_value "int" v) @@

src/passes/11-self_mini_c/subst.ml

@@ -117,7 +117,7 @@ let rec subst_expression : body:expression -> x:var_name -> expr:expression -> e
   (* hack to avoid reimplementing subst_binder for 2-ary binder in E_if_cons:
      intuitively, we substitute in \hd tl. expr' as if it were \hd. \tl. expr *)
   let subst_binder2 y z expr' =
-    let dummy = T_base TC_unit in
+    let dummy = T_base TB_unit in
     let hack = { content = E_closure { binder = z ; body = expr' } ;
                  type_value = dummy } in
     match subst_binder y hack with
@@ -199,7 +199,7 @@ let rec subst_expression : body:expression -> x:var_name -> expr:expression -> e
   )
 
 let%expect_test _ =
-  let dummy_type = T_base TC_unit in
+  let dummy_type = T_base TB_unit in
   let wrap e = { content = e ; type_value = dummy_type } in
 
   let show_subst ~body ~x ~expr =

src/passes/12-compiler/compiler_type.ml

@@ -59,24 +59,24 @@ module Ty = struct
   let not_comparable name () = error (thunk "not a comparable type") (fun () -> name) ()
   let not_compilable_type name () = error (thunk "not a compilable type") (fun () -> name) ()
 
-  let comparable_type_base : type_constant -> ex_comparable_ty result = fun tb ->
+  let comparable_type_base : type_base -> ex_comparable_ty result = fun tb ->
     let return x = ok @@ Ex_comparable_ty x in
     match tb with
-    | TC_unit -> fail (not_comparable "unit")
+    | TB_unit -> fail (not_comparable "unit")
-    | TC_void -> fail (not_comparable "void")
+    | TB_void -> fail (not_comparable "void")
-    | TC_bool -> return bool_k
+    | TB_bool -> return bool_k
-    | TC_nat -> return nat_k
+    | TB_nat -> return nat_k
-    | TC_mutez -> return tez_k
+    | TB_mutez -> return tez_k
-    | TC_int -> return int_k
+    | TB_int -> return int_k
-    | TC_string -> return string_k
+    | TB_string -> return string_k
-    | TC_address -> return address_k
+    | TB_address -> return address_k
-    | TC_timestamp -> return timestamp_k
+    | TB_timestamp -> return timestamp_k
-    | TC_bytes -> return bytes_k
+    | TB_bytes -> return bytes_k
-    | TC_operation -> fail (not_comparable "operation")
+    | TB_operation -> fail (not_comparable "operation")
-    | TC_signature -> fail (not_comparable "signature")
+    | TB_signature -> fail (not_comparable "signature")
-    | TC_key -> fail (not_comparable "key")
+    | TB_key -> fail (not_comparable "key")
-    | TC_key_hash -> return key_hash_k
+    | TB_key_hash -> return key_hash_k
-    | TC_chain_id -> fail (not_comparable "chain_id")
+    | TB_chain_id -> fail (not_comparable "chain_id")
 
   let comparable_leaf : type a. (a, _) comparable_struct -> (a , leaf) comparable_struct result =
       fun a ->
@@ -109,24 +109,24 @@ module Ty = struct
     | T_option _ -> fail (not_comparable "option")
     | T_contract _ -> fail (not_comparable "contract")
 
-  let base_type : type_constant -> ex_ty result = fun b ->
+  let base_type : type_base -> ex_ty result = fun b ->
     let return x = ok @@ Ex_ty x in
    match b with
-    | TC_unit -> return unit
+    | TB_unit -> return unit
-    | TC_void -> fail (not_compilable_type "void")
+    | TB_void -> fail (not_compilable_type "void")
-    | TC_bool -> return bool
+    | TB_bool -> return bool
-    | TC_int -> return int
+    | TB_int -> return int
-    | TC_nat -> return nat
+    | TB_nat -> return nat
-    | TC_mutez -> return tez
+    | TB_mutez -> return tez
-    | TC_string -> return string
+    | TB_string -> return string
-    | TC_address -> return address
+    | TB_address -> return address
-    | TC_timestamp -> return timestamp
+    | TB_timestamp -> return timestamp
-    | TC_bytes -> return bytes
+    | TB_bytes -> return bytes
-    | TC_operation -> return operation
+    | TB_operation -> return operation
-    | TC_signature -> return signature
+    | TB_signature -> return signature
-    | TC_key -> return key
+    | TB_key -> return key
-    | TC_key_hash -> return key_hash
+    | TB_key_hash -> return key_hash
-    | TC_chain_id -> return chain_id
+    | TB_chain_id -> return chain_id
 
   let rec type_ : type_value -> ex_ty result =
     function
@@ -195,23 +195,23 @@ module Ty = struct
 end
 
 
-let base_type : type_constant -> O.michelson result =
+let base_type : type_base -> O.michelson result =
   function
-  | TC_unit -> ok @@ O.prim T_unit
+  | TB_unit -> ok @@ O.prim T_unit
-  | TC_void -> fail (Ty.not_compilable_type "void")
+  | TB_void -> fail (Ty.not_compilable_type "void")
-  | TC_bool -> ok @@ O.prim T_bool
+  | TB_bool -> ok @@ O.prim T_bool
-  | TC_int -> ok @@ O.prim T_int
+  | TB_int -> ok @@ O.prim T_int
-  | TC_nat -> ok @@ O.prim T_nat
+  | TB_nat -> ok @@ O.prim T_nat
-  | TC_mutez -> ok @@ O.prim T_mutez
+  | TB_mutez -> ok @@ O.prim T_mutez
-  | TC_string -> ok @@ O.prim T_string
+  | TB_string -> ok @@ O.prim T_string
-  | TC_address -> ok @@ O.prim T_address
+  | TB_address -> ok @@ O.prim T_address
-  | TC_timestamp -> ok @@ O.prim T_timestamp
+  | TB_timestamp -> ok @@ O.prim T_timestamp
-  | TC_bytes -> ok @@ O.prim T_bytes
+  | TB_bytes -> ok @@ O.prim T_bytes
-  | TC_operation -> ok @@ O.prim T_operation
+  | TB_operation -> ok @@ O.prim T_operation
-  | TC_signature -> ok @@ O.prim T_signature
+  | TB_signature -> ok @@ O.prim T_signature
-  | TC_key -> ok @@ O.prim T_key
+  | TB_key -> ok @@ O.prim T_key
-  | TC_key_hash -> ok @@ O.prim T_key_hash
+  | TB_key_hash -> ok @@ O.prim T_key_hash
-  | TC_chain_id -> ok @@ O.prim T_chain_id
+  | TB_chain_id -> ok @@ O.prim T_chain_id
 
 let rec type_ : type_value -> O.michelson result =
   function

src/passes/2-concrete_to_imperative/cameligo.ml

@@ -768,11 +768,11 @@ and compile_logic_expression ?te_annot (t:Raw.logic_expr) : expr result =
   match t with
   | BoolExpr (False reg) -> (
       let loc = Location.lift reg in
-      return @@ e_literal ~loc (Literal_bool false)
+      return @@ e_bool ~loc false
     )
   | BoolExpr (True reg) -> (
       let loc = Location.lift reg in
-      return @@ e_literal ~loc (Literal_bool true)
+      return @@ e_bool ~loc true
     )
   | BoolExpr (Or b) ->
       compile_binop "OR" b

src/passes/2-concrete_to_imperative/pascaligo.ml

@@ -487,11 +487,11 @@ and compile_logic_expression (t:Raw.logic_expr) : expression result =
   match t with
   | BoolExpr (False reg) -> (
       let loc = Location.lift reg in
-      return @@ e_literal ~loc (Literal_bool false)
+      return @@ e_bool ~loc false
     )
   | BoolExpr (True reg) -> (
       let loc = Location.lift reg in
-      return @@ e_literal ~loc (Literal_bool true)
+      return @@ e_bool ~loc true
     )
   | BoolExpr (Or b) ->
       compile_binop "OR" b

src/passes/8-typer-new/PP.ml

@@ -14,7 +14,6 @@ let type_constraint : _ -> type_constraint_simpl -> unit = fun ppf ->
       | Solver.Core.C_list         -> "list"
       | Solver.Core.C_set          -> "set"
       | Solver.Core.C_unit         -> "unit"
-      | Solver.Core.C_bool         -> "bool"
       | Solver.Core.C_string       -> "string"
       | Solver.Core.C_nat          -> "nat"
       | Solver.Core.C_mutez        -> "mutez"

src/passes/8-typer-new/dune

@@ -8,6 +8,7 @@
     ast_typed
     operators
     UnionFind
+    environment
   )
   (preprocess
     (pps ppx_let)

src/passes/8-typer-new/solver.ml

@@ -387,93 +387,89 @@ let compare_simple_c_constant = function
   | C_arrow -> (function
       (* N/A -> 1 *)
       | C_arrow -> 0
-      | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
+      | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit  | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
   | C_option -> (function
       | C_arrow -> 1
       | C_option -> 0
-      | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
+      | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit  | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
   | C_record -> (function
       | C_arrow | C_option  -> 1
       | C_record -> 0
-      | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
+      | C_variant | C_map | C_big_map | C_list | C_set | C_unit  | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
   | C_variant -> (function
       | C_arrow | C_option  | C_record -> 1
       | C_variant -> 0
-      | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
+      | C_map | C_big_map | C_list | C_set | C_unit  | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
   | C_map -> (function
       | C_arrow | C_option  | C_record | C_variant -> 1
       | C_map -> 0
-      | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
+      | C_big_map | C_list | C_set | C_unit  | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
   | C_big_map -> (function
       | C_arrow | C_option  | C_record | C_variant | C_map -> 1
       | C_big_map -> 0
-      | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
+      | C_list | C_set | C_unit  | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
   | C_list -> (function
       | C_arrow | C_option  | C_record | C_variant | C_map | C_big_map -> 1
       | C_list -> 0
-      | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
+      | C_set | C_unit  | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
   | C_set -> (function
       | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list -> 1
       | C_set -> 0
-      | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
+      | C_unit  | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
   | C_unit -> (function
       | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set -> 1
       | C_unit -> 0
-      | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
-  | C_bool -> (function
-      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit -> 1
-      | C_bool -> 0
        | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
   | C_string -> (function
-      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool -> 1
+      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit  -> 1
       | C_string -> 0
       | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
   | C_nat -> (function
-      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string -> 1
+      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit  | C_string -> 1
       | C_nat -> 0
       | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
   | C_mutez -> (function
-      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat -> 1
+      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit  | C_string | C_nat -> 1
       | C_mutez -> 0
       | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
   | C_timestamp -> (function
-      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez -> 1
+      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit  | C_string | C_nat | C_mutez -> 1
       | C_timestamp -> 0
       | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
   | C_int -> (function
-      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp -> 1
+      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit  | C_string | C_nat | C_mutez | C_timestamp -> 1
       | C_int -> 0
       | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
   | C_address -> (function
-      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int -> 1
+      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit  | C_string | C_nat | C_mutez | C_timestamp | C_int -> 1
       | C_address -> 0
       | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
   | C_bytes -> (function
-      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address -> 1
+      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit  | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address -> 1
       | C_bytes -> 0
       | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
   | C_key_hash -> (function
-      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes -> 1
+      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit  | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes -> 1
       | C_key_hash -> 0
       | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
   | C_key -> (function
-      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash -> 1
+      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit  | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash -> 1
       | C_key -> 0
       | C_signature | C_operation | C_contract | C_chain_id -> -1)
   | C_signature -> (function
-      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key -> 1
+      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit  | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key -> 1
       | C_signature -> 0
       | C_operation | C_contract | C_chain_id -> -1)
   | C_operation -> (function
-      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature -> 1
+      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit  | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature -> 1
       | C_operation -> 0
       | C_contract | C_chain_id -> -1)
   | C_contract -> (function
-      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation -> 1
+      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit  | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation -> 1
       | C_contract -> 0
       | C_chain_id -> -1)
   | C_chain_id -> (function
-      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> 1
+      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit  | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> 1
       | C_chain_id -> 0
       (* N/A -> -1 *)
     )
@@ -492,7 +488,6 @@ let debug_pp_constant : _ -> constant_tag -> unit = fun ppf c_tag ->
       | Core.C_list      -> "list"
       | Core.C_set       -> "set"
       | Core.C_unit      -> "unit"
-      | Core.C_bool      -> "bool"
       | Core.C_string    -> "string"
       | Core.C_nat       -> "nat"
       | Core.C_mutez     -> "mutez"

src/passes/8-typer-new/todo_use_fold_generator.ml

@@ -10,7 +10,6 @@ let convert_type_constant : I.type_constant -> O.type_constant = function
     | TC_nat -> TC_nat
     | TC_int -> TC_int
     | TC_mutez -> TC_mutez
-    | TC_bool -> TC_bool
     | TC_operation -> TC_operation
     | TC_address -> TC_address
     | TC_key -> TC_key

src/passes/8-typer-new/typer.ml

@@ -2,6 +2,7 @@ open Trace
 module I = Ast_core
 module O = Ast_typed
 open O.Combinators
+module DEnv = Environment
 module Environment = O.Environment
 module Solver = Solver
 type environment = Environment.t
@@ -233,9 +234,6 @@ and type_expression : environment -> Solver.state -> ?tv_opt:O.type_expression -
       return expr' state constraints expr_type
     )
 
-  | E_literal (Literal_bool b) -> (
-      return_wrapped (e_bool b) state @@ Wrap.literal (t_bool ())
-    )
   | E_literal (Literal_string s) -> (
       return_wrapped (e_string s) state @@ Wrap.literal (t_string ())
     )
@@ -481,7 +479,7 @@ let type_and_subst_xyz (env_state_node : environment * Solver.state * 'a) (apply
   ok (program, state)
 
 let type_program (p : I.program) : (O.program * Solver.state) result =
-  let empty_env = Ast_typed.Environment.full_empty in
+  let empty_env = DEnv.default in
   let empty_state = Solver.initial_state in
   type_and_subst_xyz (empty_env , empty_state , p) Typesystem.Misc.Substitution.Pattern.s_program type_program_returns_state
 

src/passes/8-typer-new/untyper.ml

@@ -13,7 +13,6 @@ let unconvert_type_constant : O.type_constant -> I.type_constant = function
     | TC_nat -> TC_nat
     | TC_int -> TC_int
     | TC_mutez -> TC_mutez
-    | TC_bool -> TC_bool
     | TC_operation -> TC_operation
     | TC_address -> TC_address
     | TC_key -> TC_key
@@ -219,7 +218,6 @@ let untype_literal (l:O.literal) : I.literal result =
   match l with
   | Literal_unit -> ok Literal_unit
   | Literal_void -> ok Literal_void
-  | Literal_bool b -> ok (Literal_bool b)
   | Literal_nat n -> ok (Literal_nat n)
   | Literal_timestamp n -> ok (Literal_timestamp n)
   | Literal_mutez n -> ok (Literal_mutez n)

src/passes/8-typer-new/wrap.ml

@@ -47,7 +47,6 @@ let rec type_expression_to_type_value : T.type_expression -> O.type_value = fun
   | T_constant (type_name) ->
      let csttag = Core.(match type_name with
                         | TC_unit      -> C_unit
-                        | TC_bool      -> C_bool
                         | TC_string    -> C_string
                         | TC_nat       -> C_nat
                         | TC_mutez     -> C_mutez
@@ -94,7 +93,6 @@ let rec type_expression_to_type_value_copypasted : I.type_expression -> O.type_v
   | T_constant (type_name) ->
      let csttag = Core.(match type_name with
                         | TC_unit   -> C_unit
-                        | TC_bool   -> C_bool
                         | TC_string -> C_string
                         | _        -> failwith "unknown type constructor")
      in
@@ -278,7 +276,7 @@ let loop : T.type_expression -> T.type_expression -> (constraints * T.type_varia
   let body' = type_expression_to_type_value body in
   let whole_expr = Core.fresh_type_variable () in
   O.[
-      C_equation (expr'                 , P_constant (C_bool , [])) ;
+      C_equation (expr'                 , P_variable (Stage_common.Constant.t_bool)) ;
       C_equation (body'                 , P_constant (C_unit , [])) ;
       C_equation (P_variable whole_expr , P_constant (C_unit , []))
   ] , whole_expr

src/passes/8-typer-old/dune

@@ -8,6 +8,7 @@
     ast_typed
     typer_new
     operators
+    environment
   )
   (preprocess
     (pps ppx_let)

src/passes/8-typer-old/typer.ml

@@ -4,6 +4,7 @@ module I = Ast_core
 module O = Ast_typed
 open O.Combinators
 
+module DEnv = Environment
 module Environment = O.Environment
 
 module Solver = Typer_new.Solver
@@ -226,7 +227,6 @@ let convert_type_constant : I.type_constant -> O.type_constant = function
     | TC_nat -> TC_nat
     | TC_int -> TC_int
     | TC_mutez -> TC_mutez
-    | TC_bool -> TC_bool
     | TC_operation -> TC_operation
     | TC_address -> TC_address
     | TC_key -> TC_key
@@ -477,7 +477,7 @@ let rec type_program (p:I.program) : (O.program * Solver.state) result =
   in
   let%bind (_, lst) =
     trace (fun () -> program_error p ()) @@
-    bind_fold_list aux (Environment.full_empty, []) p in
+    bind_fold_list aux (DEnv.default, []) p in
   ok @@ (List.rev lst , (Solver.placeholder_for_state_of_new_typer ()))
 
 and type_declaration env (_placeholder_for_state_of_new_typer : Solver.state) : I.declaration -> (environment * Solver.state * O.declaration option) result = function
@@ -689,8 +689,6 @@ and type_expression' : environment -> ?tv_opt:O.type_expression -> I.expression
         trace_option (unbound_variable e name ae.location)
         @@ Environment.get_opt name e in
       return (E_variable name) tv'.type_value
-  | E_literal (Literal_bool b) ->
-      return (E_literal (Literal_bool b)) (t_bool ())
   | E_literal Literal_unit ->
       return (E_literal (Literal_unit)) (t_unit ())
   | E_literal Literal_void -> return (E_literal (Literal_void)) (t_unit ()) (* TODO : IS this really a t_unit ?*)
@@ -1015,7 +1013,6 @@ let untype_literal (l:O.literal) : I.literal result =
   match l with
   | Literal_unit -> ok Literal_unit
   | Literal_void -> ok Literal_void
-  | Literal_bool b -> ok (Literal_bool b)
   | Literal_nat n -> ok (Literal_nat n)
   | Literal_timestamp n -> ok (Literal_timestamp n)
   | Literal_mutez n -> ok (Literal_mutez n)

src/passes/operators/operators.ml

@@ -43,7 +43,6 @@ module Concrete_to_imperative = struct
     | "nat"       -> Some TC_nat
     | "int"       -> Some TC_int
     | "tez"       -> Some TC_mutez
-    | "bool"      -> Some TC_bool
     | "operation" -> Some TC_operation
     | "address"   -> Some TC_address
     | "key"       -> Some TC_key

src/stages/1-ast_imperative/combinators.ml

@@ -21,7 +21,7 @@ open Errors
 
 let make_t ?(loc = Location.generated) type_content = {type_content; location=loc}
 
-let t_bool ?loc ()        : type_expression = make_t ?loc @@ T_constant (TC_bool)
+let t_bool ?loc ()        : type_expression = make_t ?loc @@ T_variable (Stage_common.Constant.t_bool)
 let t_string ?loc ()      : type_expression = make_t ?loc @@ T_constant (TC_string)
 let t_bytes ?loc ()       : type_expression = make_t ?loc @@ T_constant (TC_bytes)
 let t_int ?loc ()         : type_expression = make_t ?loc @@ T_constant (TC_int)
@@ -88,7 +88,6 @@ let e_nat_z ?loc n : expression = make_e ?loc @@ E_literal (Literal_nat n)
 let e_nat ?loc n : expression = e_nat_z ?loc @@ Z.of_int n
 let e_timestamp_z ?loc n : expression = make_e ?loc @@ E_literal (Literal_timestamp n)
 let e_timestamp ?loc n : expression = e_timestamp_z ?loc @@ Z.of_int n
-let e_bool ?loc   b : expression = make_e ?loc @@ E_literal (Literal_bool b)
 let e_string ?loc s : expression = make_e ?loc @@ E_literal (Literal_string s)
 let e_address ?loc s : expression = make_e ?loc @@ E_literal (Literal_address s)
 let e_mutez_z ?loc s : expression = make_e ?loc @@ E_literal (Literal_mutez s)
@@ -148,6 +147,8 @@ let e_while ?loc condition body = make_e ?loc @@ E_while {condition; body}
 let e_for ?loc binder start final increment body = make_e ?loc @@ E_for {binder;start;final;increment;body}
 let e_for_each ?loc binder collection collection_type body = make_e ?loc @@ E_for_each {binder;collection;collection_type;body}
 
+let e_bool ?loc   b : expression = e_constructor ?loc (string_of_bool b) (e_unit ())
+
 let ez_match_variant (lst : ((string * string) * 'a) list) =
   let lst = List.map (fun ((c,n),a) -> ((Constructor c, Var.of_name n), a) ) lst in
   Match_variant (lst,())

src/stages/1-ast_imperative/misc.ml

@@ -34,9 +34,6 @@ open Errors
 
 let assert_literal_eq (a, b : literal * literal) : unit result =
   match (a, b) with
-  | Literal_bool a, Literal_bool b when a = b -> ok ()
-  | Literal_bool _, Literal_bool _ -> fail @@ different_literals "different bools" a b
-  | Literal_bool _, _ -> fail @@ different_literals_because_different_types "bool vs non-bool" a b
   | Literal_int a, Literal_int b when a = b -> ok ()
   | Literal_int _, Literal_int _ -> fail @@ different_literals "different ints" a b
   | Literal_int _, _ -> fail @@ different_literals_because_different_types "int vs non-int" a b

src/stages/2-ast_sugar/combinators.ml

@@ -27,7 +27,7 @@ let tuple_to_record lst =
   let (_, lst ) = List.fold_left aux (0,[]) lst in
   lst
 
-let t_bool ?loc ()        : type_expression = make_t ?loc @@ T_constant (TC_bool)
+let t_bool ?loc ()        : type_expression = make_t ?loc @@ T_variable (Stage_common.Constant.t_bool)
 let t_string ?loc ()      : type_expression = make_t ?loc @@ T_constant (TC_string)
 let t_bytes ?loc ()       : type_expression = make_t ?loc @@ T_constant (TC_bytes)
 let t_int ?loc ()         : type_expression = make_t ?loc @@ T_constant (TC_int)
@@ -90,7 +90,6 @@ let e_unit ?loc () : expression = make_e ?loc @@ E_literal (Literal_unit)
 let e_int ?loc n : expression = make_e ?loc @@ E_literal (Literal_int n)
 let e_nat ?loc n : expression = make_e ?loc @@ E_literal (Literal_nat n)
 let e_timestamp ?loc n : expression = make_e ?loc @@ E_literal (Literal_timestamp n)
-let e_bool ?loc   b : expression = make_e ?loc @@ E_literal (Literal_bool b)
 let e_string ?loc s : expression = make_e ?loc @@ E_literal (Literal_string s)
 let e_address ?loc s : expression = make_e ?loc @@ E_literal (Literal_address s)
 let e_mutez ?loc s : expression = make_e ?loc @@ E_literal (Literal_mutez s)
@@ -142,6 +141,8 @@ let e_map ?loc lst : expression = make_e ?loc @@ E_map lst
 let e_big_map ?loc lst : expression = make_e ?loc @@ E_big_map lst
 let e_look_up ?loc a b : expression = make_e ?loc @@ E_look_up (a,b)
 
+let e_bool ?loc   b : expression = e_constructor ?loc (Constructor (string_of_bool b)) (e_unit ())
+
 let make_option_typed ?loc e t_opt =
   match t_opt with
   | None -> e

src/stages/2-ast_sugar/misc.ml

@@ -34,9 +34,6 @@ open Errors
 
 let assert_literal_eq (a, b : literal * literal) : unit result =
   match (a, b) with
-  | Literal_bool a, Literal_bool b when a = b -> ok ()
-  | Literal_bool _, Literal_bool _ -> fail @@ different_literals "different bools" a b
-  | Literal_bool _, _ -> fail @@ different_literals_because_different_types "bool vs non-bool" a b
   | Literal_int a, Literal_int b when a = b -> ok ()
   | Literal_int _, Literal_int _ -> fail @@ different_literals "different ints" a b
   | Literal_int _, _ -> fail @@ different_literals_because_different_types "int vs non-int" a b

src/stages/3-ast_core/combinators.ml

@@ -27,7 +27,7 @@ let tuple_to_record lst =
   let (_, lst ) = List.fold_left aux (0,[]) lst in
   lst
 
-let t_bool ?loc ()        : type_expression = make_t ?loc @@ T_constant (TC_bool)
+let t_bool ?loc ()        : type_expression = make_t ?loc @@ T_variable (Stage_common.Constant.t_bool)
 let t_string ?loc ()      : type_expression = make_t ?loc @@ T_constant (TC_string)
 let t_bytes ?loc ()       : type_expression = make_t ?loc @@ T_constant (TC_bytes)
 let t_int ?loc ()         : type_expression = make_t ?loc @@ T_constant (TC_int)
@@ -87,7 +87,6 @@ let e_unit ?loc () : expression = make_e ?loc @@ E_literal (Literal_unit)
 let e_int ?loc n : expression = make_e ?loc @@ E_literal (Literal_int n)
 let e_nat ?loc n : expression = make_e ?loc @@ E_literal (Literal_nat n)
 let e_timestamp ?loc n : expression = make_e ?loc @@ E_literal (Literal_timestamp n)
-let e_bool ?loc   b : expression = make_e ?loc @@ E_literal (Literal_bool b)
 let e_string ?loc s : expression = make_e ?loc @@ E_literal (Literal_string s)
 let e_address ?loc s : expression = make_e ?loc @@ E_literal (Literal_address s)
 let e_mutez ?loc s : expression = make_e ?loc @@ E_literal (Literal_mutez s)
@@ -126,6 +125,8 @@ let e_record_update ?loc record path update = make_e ?loc @@ E_record_update {re
 
 let e_annotation ?loc anno_expr ty = make_e ?loc @@ E_ascription {anno_expr; type_annotation = ty}
 
+let e_bool ?loc   b : expression = e_constructor ?loc (string_of_bool b) (e_unit ())
+
 let make_option_typed ?loc e t_opt =
   match t_opt with
   | None -> e

src/stages/3-ast_core/misc.ml

@@ -34,9 +34,6 @@ open Errors
 
 let assert_literal_eq (a, b : literal * literal) : unit result =
   match (a, b) with
-  | Literal_bool a, Literal_bool b when a = b -> ok ()
-  | Literal_bool _, Literal_bool _ -> fail @@ different_literals "different bools" a b
-  | Literal_bool _, _ -> fail @@ different_literals_because_different_types "bool vs non-bool" a b
   | Literal_int a, Literal_int b when a = b -> ok ()
   | Literal_int _, Literal_int _ -> fail @@ different_literals "different ints" a b
   | Literal_int _, _ -> fail @@ different_literals_because_different_types "int vs non-int" a b

src/stages/4-ast_typed/PP.ml

@@ -180,7 +180,6 @@ let literal ppf (l : literal) =
   match l with
   | Literal_unit -> fprintf ppf "unit"
   | Literal_void -> fprintf ppf "void"
-  | Literal_bool b -> fprintf ppf "%b" b
   | Literal_int z -> fprintf ppf "%a" Z.pp_print z
   | Literal_nat z -> fprintf ppf "+%a" Z.pp_print z
   | Literal_timestamp z -> fprintf ppf "+%a" Z.pp_print z
@@ -205,7 +204,6 @@ let s =
     | TC_nat -> "nat"
     | TC_int -> "int"
     | TC_mutez -> "mutez"
-    | TC_bool -> "bool"
     | TC_operation -> "operation"
     | TC_address -> "address"
     | TC_key -> "key"

src/stages/4-ast_typed/combinators.ml

@@ -34,7 +34,6 @@ let make_n_t type_name type_value = { type_name ; type_value }
 
 let t_signature ?loc ?s ()  : type_expression = make_t ?loc (T_constant TC_signature) s
 let t_chain_id ?loc ?s ()   : type_expression = make_t ?loc (T_constant TC_chain_id) s
-let t_bool ?loc ?s ()       : type_expression = make_t ?loc (T_constant TC_bool) s
 let t_string ?loc ?s ()     : type_expression = make_t ?loc (T_constant TC_string) s
 let t_bytes ?loc ?s ()      : type_expression = make_t ?loc (T_constant TC_bytes) s
 let t_key ?loc ?s ()        : type_expression = make_t ?loc (T_constant TC_key) s
@@ -67,10 +66,13 @@ let t_big_map ?loc k v ?s () = make_t ?loc (T_operator (TC_big_map { k ; v })) s
 let t_map_or_big_map ?loc k v ?s () = make_t ?loc (T_operator (TC_map_or_big_map { k ; v })) s
 
 let t_sum m ?loc ?s () : type_expression = make_t ?loc (T_sum m) s
-let make_t_ez_sum ?loc (lst:(constructor' * ctor_content) list) : type_expression =
+let make_t_ez_sum ?loc ?s (lst:(constructor' * ctor_content) list) : type_expression =
   let aux prev (k, v) = CMap.add k v prev in
   let map = List.fold_left aux CMap.empty lst in
-  make_t ?loc (T_sum map) None
+  make_t ?loc (T_sum map) s
+
+let t_bool ?loc ?s ()       : type_expression = make_t_ez_sum ?loc ?s
+  [(Constructor "true", {ctor_type=t_unit ();michelson_annotation=None});(Constructor "false", {ctor_type=t_unit ();michelson_annotation=None})]
 
 let t_function param result ?loc ?s () : type_expression = make_t ?loc (T_arrow {type1=param; type2=result}) s
 let t_shallow_closure param result ?loc ?s () : type_expression = make_t ?loc (T_arrow {type1=param; type2=result}) s
@@ -90,7 +92,8 @@ let get_lambda_with_type e =
   | _ -> simple_fail "not a lambda with functional type"
 
 let get_t_bool (t:type_expression) : unit result = match t.type_content with
-  | T_constant (TC_bool) -> ok ()
+  | T_variable v when Var.equal v Stage_common.Constant.t_bool -> ok ()
+  | T_sum m when m = CMap.of_list [(Constructor "true", {ctor_type=t_unit();michelson_annotation=None});(Constructor "false",{ctor_type=t_unit();michelson_annotation=None})] -> ok ()
   | _ -> fail @@ Errors.not_a_x_type "bool" t ()
 
 let get_t_int (t:type_expression) : unit result = match t.type_content with
@@ -286,7 +289,6 @@ let e_unit () : expression_content =     E_literal (Literal_unit)
 let e_int n : expression_content = E_literal (Literal_int n)
 let e_nat n : expression_content = E_literal (Literal_nat n)
 let e_mutez n : expression_content = E_literal (Literal_mutez n)
-let e_bool b : expression_content = E_literal (Literal_bool b)
 let e_string s : expression_content = E_literal (Literal_string s)
 let e_bytes s : expression_content = E_literal (Literal_bytes s)
 let e_timestamp s : expression_content = E_literal (Literal_timestamp s)
@@ -302,11 +304,15 @@ let e_application lamb args : expression_content = E_application {lamb;args}
 let e_variable v : expression_content = E_variable v
 let e_let_in let_binder inline rhs let_result = E_let_in { let_binder ; rhs ; let_result; inline }
 
+let e_constructor constructor element: expression_content = E_constructor {constructor;element}
+
+let e_bool b env : expression_content = e_constructor (Constructor (string_of_bool b)) (make_e (e_unit ())(t_unit()) env)
+
 let e_a_unit = make_e (e_unit ()) (t_unit ())
 let e_a_int n = make_e (e_int n) (t_int ())
 let e_a_nat n = make_e (e_nat n) (t_nat ())
 let e_a_mutez n = make_e (e_mutez n) (t_mutez ())
-let e_a_bool b = make_e (e_bool b) (t_bool ())
+let e_a_bool b = fun env -> make_e (e_bool b env) (t_bool ()) env
 let e_a_string s = make_e (e_string s) (t_string ())
 let e_a_address s = make_e (e_address s) (t_address ())
 let e_a_pair a b = make_e (e_pair a b)
@@ -326,6 +332,7 @@ let ez_e_a_record r = make_e (ez_e_record r) (ez_t_record (List.map (fun (x, y)
 let e_a_let_in binder expr body attributes = make_e (e_let_in binder expr body attributes) (get_type_expression body)
 
 
+
 let get_a_int (t:expression) =
   match t.expression_content with
   | E_literal (Literal_int n) -> ok n
@@ -338,7 +345,7 @@ let get_a_unit (t:expression) =
 
 let get_a_bool (t:expression) =
   match t.expression_content with
-  | E_literal (Literal_bool b) -> ok b
+  | E_constructor {constructor=Constructor name;element} when (name = "true" || name = "false") && element.expression_content = e_unit () -> ok (bool_of_string name)
   | _ -> simple_fail "not a bool"
 
 

src/stages/4-ast_typed/combinators.mli

@@ -33,7 +33,7 @@ val t_map : ?loc:Location.t -> type_expression -> type_expression -> ?s:S.type_e
 val t_big_map : ?loc:Location.t -> type_expression -> type_expression -> ?s:S.type_expression -> unit -> type_expression
 val t_map_or_big_map : ?loc:Location.t -> type_expression -> type_expression ->  ?s:S.type_expression -> unit -> type_expression
 val t_sum : Types.te_cmap -> ?loc:Location.t -> ?s:S.type_expression -> unit -> type_expression
-val make_t_ez_sum : ?loc:Location.t -> ( constructor' * ctor_content ) list -> type_expression
+val make_t_ez_sum : ?loc:Location.t -> ?s:S.type_expression -> ( constructor' * ctor_content ) list -> type_expression
 val t_function : type_expression -> type_expression -> ?loc:Location.t -> ?s:S.type_expression -> unit -> type_expression
 val t_shallow_closure : type_expression -> type_expression -> ?loc:Location.t -> ?s:S.type_expression -> unit -> type_expression
 val get_type_expression : expression -> type_expression
@@ -114,7 +114,7 @@ val e_unit : unit -> expression_content
 val e_int : Z.t -> expression_content
 val e_nat : Z.t -> expression_content
 val e_mutez : Z.t -> expression_content
-val e_bool : bool -> expression_content
+val e_bool : bool -> full_environment -> expression_content
 val e_string : string -> expression_content
 val e_bytes : bytes -> expression_content
 val e_timestamp : Z.t -> expression_content

src/stages/4-ast_typed/helpers.ml

@@ -47,7 +47,6 @@ let type_expression'_of_string = function
   | "TC_nat"       , [] -> ok @@ T_constant(TC_nat)
   | "TC_int"       , [] -> ok @@ T_constant(TC_int)
   | "TC_mutez"     , [] -> ok @@ T_constant(TC_mutez)
-  | "TC_bool"      , [] -> ok @@ T_constant(TC_bool)
   | "TC_operation" , [] -> ok @@ T_constant(TC_operation)
   | "TC_address"   , [] -> ok @@ T_constant(TC_address)
   | "TC_key"       , [] -> ok @@ T_constant(TC_key)
@@ -77,7 +76,6 @@ let string_of_type_constant = function
   | TC_nat       -> "TC_nat", []
   | TC_int       -> "TC_int", []
   | TC_mutez     -> "TC_mutez", []
-  | TC_bool      -> "TC_bool", []
   | TC_operation -> "TC_operation", []
   | TC_address   -> "TC_address", []
   | TC_key       -> "TC_key", []

src/stages/4-ast_typed/misc.ml

@@ -407,9 +407,6 @@ let type_expression_eq ab = Trace.to_bool @@ assert_type_expression_eq ab
 
 let assert_literal_eq (a, b : literal * literal) : unit result =
   match (a, b) with
-  | Literal_bool a, Literal_bool b when a = b -> ok ()
-  | Literal_bool _, Literal_bool _ -> fail @@ different_literals "booleans" a b
-  | Literal_bool _, _ -> fail @@ different_literals_because_different_types "bool vs non-bool" a b
   | Literal_int a, Literal_int b when a = b -> ok ()
   | Literal_int _, Literal_int _ -> fail @@ different_literals "different ints" a b
   | Literal_int _, _ -> fail @@ different_literals_because_different_types "int vs non-int" a b

src/stages/4-ast_typed/types.ml

@@ -9,7 +9,6 @@ type type_constant =
     | TC_nat
     | TC_int
     | TC_mutez
-    | TC_bool
     | TC_operation
     | TC_address
     | TC_key
@@ -77,7 +76,6 @@ and type_expression = {
 
 type literal =
   | Literal_unit
-  | Literal_bool of bool
   | Literal_int of z
   | Literal_nat of z
   | Literal_timestamp of z

src/stages/5-mini_c/PP.ml

@@ -29,23 +29,23 @@ and environment_element ppf ((n, tv) : environment_element) =
 and environment ppf (x:environment) =
   fprintf ppf "Env[%a]" (list_sep_d environment_element) x
 
-and type_constant ppf (tc:type_constant) : unit =
+and type_constant ppf (tb:type_base) : unit =
-  let s = match tc with 
+  let s = match tb with 
-    | TC_unit      -> "unit"
+    | TB_unit      -> "unit"
-    | TC_string    -> "string"
+    | TB_string    -> "string"
-    | TC_bytes     -> "bytes"
+    | TB_bytes     -> "bytes"
-    | TC_nat       -> "nat"
+    | TB_nat       -> "nat"
-    | TC_int       -> "int"
+    | TB_int       -> "int"
-    | TC_mutez     -> "mutez"
+    | TB_mutez     -> "mutez"
-    | TC_bool      -> "bool"
+    | TB_bool      -> "bool"
-    | TC_operation -> "operation"
+    | TB_operation -> "operation"
-    | TC_address   -> "address"
+    | TB_address   -> "address"
-    | TC_key       -> "key"
+    | TB_key       -> "key"
-    | TC_key_hash  -> "key_hash"
+    | TB_key_hash  -> "key_hash"
-    | TC_signature -> "signature"
+    | TB_signature -> "signature"
-    | TC_timestamp -> "timestamp"
+    | TB_timestamp -> "timestamp"
-    | TC_chain_id  -> "chain_id"
+    | TB_chain_id  -> "chain_id"
-    | TC_void      -> "void"
+    | TB_void      -> "void"
     in
   fprintf ppf "(TC %s)" s
 
@@ -255,7 +255,7 @@ let%expect_test _ =
 
 let%expect_test _ =
   let pp = expression' Format.std_formatter in
-  let dummy_type = T_base TC_unit in
+  let dummy_type = T_base TB_unit in
   let wrap e = { content = e ; type_value = dummy_type } in
   pp @@ E_closure { binder = Var.of_name "y" ; body = wrap (E_variable (Var.of_name "y")) } ;
   [%expect{|

src/stages/5-mini_c/combinators.ml

@@ -152,7 +152,7 @@ let get_t_contract t = match t with
   | _ -> fail @@ wrong_type "contract" t
 
 let get_t_operation t = match t with
-  | T_base TC_operation -> ok t
+  | T_base TB_operation -> ok t
   | _ -> fail @@ wrong_type "operation" t
 
 let get_operation (v:value) = match v with
@@ -160,9 +160,9 @@ let get_operation (v:value) = match v with
   | _ -> simple_fail "not an operation"
 
 
-let t_int : type_value = T_base TC_int
+let t_int  : type_value = T_base TB_int
-let t_unit : type_value = T_base TC_unit
+let t_unit : type_value = T_base TB_unit
-let t_nat : type_value = T_base TC_nat
+let t_nat  : type_value = T_base TB_nat
 
 let t_function x y : type_value = T_function ( x , y )
 let t_pair x y : type_value = T_pair ( x , y )

src/stages/5-mini_c/types.ml

@@ -1,4 +1,3 @@
-
 include Stage_common.Types
 
 type 'a annotated = string option * 'a
@@ -7,7 +6,7 @@ type type_value =
   | T_pair of (type_value annotated * type_value annotated)
   | T_or of (type_value annotated * type_value annotated)
   | T_function of (type_value * type_value)
-  | T_base of type_constant
+  | T_base of type_base
   | T_map of (type_value * type_value)
   | T_big_map of (type_value * type_value)
   | T_list of type_value
@@ -15,6 +14,23 @@ type type_value =
   | T_contract of type_value
   | T_option of type_value
 
+and type_base =
+  | TB_unit
+  | TB_bool
+  | TB_string
+  | TB_bytes
+  | TB_nat
+  | TB_int
+  | TB_mutez
+  | TB_operation
+  | TB_address
+  | TB_key
+  | TB_key_hash
+  | TB_chain_id
+  | TB_signature
+  | TB_timestamp
+  | TB_void
+
 and environment_element = expression_variable * type_value
 
 and environment = environment_element list

src/stages/common/PP.ml

@@ -130,7 +130,6 @@ let literal ppf (l : literal) =
   match l with
   | Literal_unit -> fprintf ppf "unit"
   | Literal_void -> fprintf ppf "void"
-  | Literal_bool b -> fprintf ppf "%b" b
   | Literal_int z -> fprintf ppf "%a" Z.pp_print z
   | Literal_nat z -> fprintf ppf "+%a" Z.pp_print z
   | Literal_timestamp z -> fprintf ppf "+%a" Z.pp_print z
@@ -155,7 +154,6 @@ let s =
     | TC_nat -> "nat"
     | TC_int -> "int"
     | TC_mutez -> "mutez"
-    | TC_bool -> "bool"
     | TC_operation -> "operation"
     | TC_address -> "address"
     | TC_key -> "key"

src/stages/common/constant.ml

@@ -0,0 +1,2 @@
+open Types
+let t_bool : type_variable = Var.of_name "bool"

src/stages/common/types.ml

@@ -20,7 +20,6 @@ type 'a constructor_map = 'a CMap.t
     | TC_nat
     | TC_int
     | TC_mutez
-    | TC_bool
     | TC_operation
     | TC_address
     | TC_key
@@ -112,7 +111,6 @@ module Ast_generic_type (PARAMETER : AST_PARAMETER_TYPE) = struct
     | "TC_nat"       , [] -> ok @@ T_constant(TC_nat)
     | "TC_int"       , [] -> ok @@ T_constant(TC_int)
     | "TC_mutez"     , [] -> ok @@ T_constant(TC_mutez)
-    | "TC_bool"      , [] -> ok @@ T_constant(TC_bool)
     | "TC_operation" , [] -> ok @@ T_constant(TC_operation)
     | "TC_address"   , [] -> ok @@ T_constant(TC_address)
     | "TC_key"       , [] -> ok @@ T_constant(TC_key)
@@ -142,7 +140,6 @@ module Ast_generic_type (PARAMETER : AST_PARAMETER_TYPE) = struct
     | TC_nat       -> "TC_nat", []
     | TC_int       -> "TC_int", []
     | TC_mutez     -> "TC_mutez", []
-    | TC_bool      -> "TC_bool", []
     | TC_operation -> "TC_operation", []
     | TC_address   -> "TC_address", []
     | TC_key       -> "TC_key", []
@@ -162,7 +159,6 @@ end
 
 type literal =
   | Literal_unit
-  | Literal_bool of bool
   | Literal_int of Z.t
   | Literal_nat of Z.t
   | Literal_timestamp of Z.t

src/stages/typesystem/core.ml

@@ -18,7 +18,6 @@ type constant_tag =
   | C_list      (* * -> * *)
   | C_set       (* * -> * *)
   | C_unit      (* * *)
-  | C_bool      (* * *)
   | C_string    (* * *)
   | C_nat       (* * *)
   | C_mutez     (* * *)
@@ -87,7 +86,6 @@ let type_expression'_of_simple_c_constant = function
   | C_nat       , [] -> ok @@ Ast_typed.T_constant(TC_nat)
   | C_int       , [] -> ok @@ Ast_typed.T_constant(TC_int)
   | C_mutez     , [] -> ok @@ Ast_typed.T_constant(TC_mutez)
-  | C_bool      , [] -> ok @@ Ast_typed.T_constant(TC_bool)
   | C_operation , [] -> ok @@ Ast_typed.T_constant(TC_operation)
   | C_address   , [] -> ok @@ Ast_typed.T_constant(TC_address)
   | C_key       , [] -> ok @@ Ast_typed.T_constant(TC_key)
@@ -95,5 +93,5 @@ let type_expression'_of_simple_c_constant = function
   | C_chain_id  , [] -> ok @@ Ast_typed.T_constant(TC_chain_id)
   | C_signature , [] -> ok @@ Ast_typed.T_constant(TC_signature)
   | C_timestamp , [] -> ok @@ Ast_typed.T_constant(TC_timestamp)
-  | (C_unit | C_string | C_bytes | C_nat | C_int | C_mutez | C_bool | C_operation | C_address | C_key | C_key_hash | C_chain_id | C_signature | C_timestamp), _::_ ->
+  | (C_unit | C_string | C_bytes | C_nat | C_int | C_mutez | C_operation | C_address | C_key | C_key_hash | C_chain_id | C_signature | C_timestamp), _::_ ->
      failwith "internal error: wrong number of arguments for type constant"

src/stages/typesystem/misc.ml

@@ -119,7 +119,6 @@ module Substitution = struct
       | T.Literal_void ->
         let () = ignore @@ substs in
         ok @@ T.Literal_void
-      | (T.Literal_bool _ as x)
       | (T.Literal_int _ as x)
       | (T.Literal_nat _ as x)
       | (T.Literal_timestamp _ as x)

src/stages/typesystem/shorthands.ml

@@ -53,7 +53,7 @@ let map  k v  = P_constant (C_map   , [k; v])
 let unit      = P_constant (C_unit    , [])
 let list   t  = P_constant (C_list    , [t])
 let set    t  = P_constant (C_set     , [t])
-let bool      = P_constant (C_bool    , [])
+let bool      = P_variable (Stage_common.Constant.t_bool)
 let string    = P_constant (C_string  , [])
 let nat       = P_constant (C_nat     , [])
 let mutez     = P_constant (C_mutez  , [])

src/test/typer_tests.ml

@@ -20,7 +20,7 @@ let int () : unit result =
   ok ()
 
 module TestExpressions = struct
-  let test_expression ?(env = Typer.Environment.full_empty)
+  let test_expression ?(env = Environment.default)
                       ?(state = Typer.Solver.initial_state)
                       (expr : expression)
                       (test_expected_ty : Typed.type_expression) =