Merge branch 'bugfix/v0.87'

src/whyml/mlw_interp.ml

@@ -45,6 +45,8 @@ type value =
   | Vcase of value * term_branch list
 
 let array_cons_ls = ref ps_equ
+let ls_true = ref ps_equ
+let ls_false = ref ps_equ
 
 let rec print_value fmt v =
   match v with
@@ -228,6 +230,9 @@ let rec matching env (t:value) p =
         else
           if ls2.ls_constr > 0 then raise NoMatch
           else raise Undetermined
+      | Vbool b ->
+         let l = if b then !ls_true else !ls_false in
+         if ls_equal ls1 l then env else raise NoMatch
       | _ -> raise Undetermined
 
 
@@ -407,8 +412,8 @@ let eval_map_set ls_set l =
 
 let built_in_theories =
   [ ["bool"],"Bool", [],
-    [ "True", None, eval_true ;
-      "False", None, eval_false ;
+    [ "True", Some ls_true, eval_true ;
+      "False", Some ls_false, eval_false ;
     ] ;
     ["int"],"Int", [],
     [ "infix +", None, eval_int_op BigInt.add;

src/whyml/mlw_ocaml.ml

@@ -798,7 +798,7 @@ module Print = struct
         print_lident info fmt ts
     | Tapp (ts, [ty]) ->
         fprintf fmt (protect_on paren "%a@ %a")
-          (print_ty info) ty (print_lident info) ts
+          (print_ty ~paren:true info) ty (print_lident info) ts
     | Tapp (ts, tl) ->
         fprintf fmt (protect_on paren "(%a)@ %a")
           (print_list comma (print_ty info)) tl
@@ -969,7 +969,7 @@ module Print = struct
         fprintf fmt "%a.%a" (print_expr_p info) e (print_lident info) f
     | Esetfield (e1, f, e2) ->
         fprintf fmt (protect_on paren "%a.%a <- %a")
-        (print_expr info) e1 (print_lident info) f (print_expr info) e2
+        (print_expr_p info) e1 (print_lident info) f (print_expr info) e2
     | Eblock [] ->
         fprintf fmt "()"
     | Eblock [e] ->
@@ -1005,7 +1005,7 @@ module Print = struct
         fprintf fmt (protect_on paren "raise %a") (print_uident info) id
     | Eraise (Xident id, Some e1) ->
         fprintf fmt (protect_on paren "raise (%a %a)")
-              (print_uident info) id (print_expr info) e1
+              (print_uident info) id (print_expr ~paren:true info) e1
     | Etry (e1, bl) ->
         fprintf fmt
           "@[<v>@[<hv>@[<hov 2>begin@ try@ %a@]@ with@]@\n@[<hov>%a@]@\nend@]"
@@ -1069,7 +1069,7 @@ module Print = struct
        fprintf fmt "exception %a@\n@\n" (print_uident info) xs
     | Dexn (xs, Some ty) ->
        fprintf fmt "@[<hov 2>exception %a of %a@]@\n@\n"
-               (print_uident info) xs (print_ty info) ty
+               (print_uident info) xs (print_ty ~paren:true info) ty
 
 end