Commit e988b21d authored by MARCHE Claude's avatar MARCHE Claude

Test BV32

parent 305c620c
...@@ -181,7 +181,7 @@ test: bin/why.byte $(TOOLS) ...@@ -181,7 +181,7 @@ test: bin/why.byte $(TOOLS)
@printf "*** Checking Coq file generation ***\\n" @printf "*** Checking Coq file generation ***\\n"
@for i in int.Abs int.EuclideanDivision int.ComputerDivision \ @for i in int.Abs int.EuclideanDivision int.ComputerDivision \
real.Abs real.FromInt real.ExpLog real.Trigonometric \ real.Abs real.FromInt real.ExpLog real.Trigonometric \
floating_point.Test \ floating_point.Test array.TestBv32 \
; do \ ; do \
printf "Generate Coq file for $$i" && bin/why.byte \ printf "Generate Coq file for $$i" && bin/why.byte \
--driver drivers/coq.drv -I theories/ \ --driver drivers/coq.drv -I theories/ \
......
...@@ -17,6 +17,20 @@ theory BuiltIn ...@@ -17,6 +17,20 @@ theory BuiltIn
syntax logic (_<>_) "(%1 <> %2)" syntax logic (_<>_) "(%1 <> %2)"
end end
theory bool.Bool
syntax type bool "bool"
syntax logic True "true"
syntax logic False "false"
syntax logic andb "(andb %1 %2)"
syntax logic orb "(orb %1 %2)"
syntax logic xorb "(xorb %1 %2)"
syntax logic notb "(negb %1)"
end
theory int.Int theory int.Int
......
...@@ -170,7 +170,7 @@ and print_tnode opl opr drv fmt t = match t.t_node with ...@@ -170,7 +170,7 @@ and print_tnode opl opr drv fmt t = match t.t_node with
"(%s)%%R" "(%s * %s)%%R" "(%s / %s)%%R" fmt c "(%s)%%R" "(%s * %s)%%R" "(%s / %s)%%R" fmt c
| Tlet (t1,tb) -> | Tlet (t1,tb) ->
let v,t2 = t_open_bound tb in let v,t2 = t_open_bound tb in
fprintf fmt (protect_on opr "let %a =@ %a in@ %a") fprintf fmt (protect_on opr "let %a :=@ %a in@ %a")
print_vs v (print_opl_term drv) t1 (print_opl_term drv) t2; print_vs v (print_opl_term drv) t1 (print_opl_term drv) t2;
forget_var v forget_var v
| Tcase (tl,bl) -> | Tcase (tl,bl) ->
...@@ -211,7 +211,7 @@ and print_fnode opl opr drv fmt f = match f.f_node with ...@@ -211,7 +211,7 @@ and print_fnode opl opr drv fmt f = match f.f_node with
fprintf fmt (protect_on opr "~ %a") (print_opl_fmla drv) f fprintf fmt (protect_on opr "~ %a") (print_opl_fmla drv) f
| Flet (t,f) -> | Flet (t,f) ->
let v,f = f_open_bound f in let v,f = f_open_bound f in
fprintf fmt (protect_on opr "let %a =@ %a in@ %a") fprintf fmt (protect_on opr "let %a :=@ %a in@ %a")
print_vs v (print_opl_term drv) t (print_opl_fmla drv) f; print_vs v (print_opl_term drv) t (print_opl_fmla drv) f;
forget_var v forget_var v
| Fcase (tl,bl) -> | Fcase (tl,bl) ->
...@@ -272,7 +272,9 @@ let print_type_decl drv fmt d = ...@@ -272,7 +272,9 @@ let print_type_decl drv fmt d =
| Syntax _ -> () | Syntax _ -> ()
| _ -> print_type_decl drv fmt d; forget_tvs () | _ -> print_type_decl drv fmt d; forget_tvs ()
let print_ls_type drv fmt ls = match ls with let print_ls_type ?(arrow=false) drv fmt ls =
if arrow then fprintf fmt " ->@ ";
match ls with
| None -> fprintf fmt "Prop" | None -> fprintf fmt "Prop"
| Some ty -> print_ty drv fmt ty | Some ty -> print_ty drv fmt ty
...@@ -285,9 +287,9 @@ let print_logic_decl drv fmt (ls,ld) = match ld with ...@@ -285,9 +287,9 @@ let print_logic_decl drv fmt (ls,ld) = match ld with
(print_expr drv) e; (print_expr drv) e;
List.iter forget_var vl List.iter forget_var vl
| None -> | None ->
fprintf fmt "@[<hov 2>Parameter %a: %a@ -> %a.@]@\n@\n" fprintf fmt "@[<hov 2>Parameter %a: %a@ %a.@]@\n@\n"
print_ls ls (print_arrow_list (print_ty drv)) ls.ls_args print_ls ls (print_arrow_list (print_ty drv)) ls.ls_args
(print_ls_type drv) ls.ls_value (print_ls_type ~arrow:(List.length ls.ls_args > 0) drv) ls.ls_value
let print_logic_decl drv fmt d = let print_logic_decl drv fmt d =
match query_ident drv (fst d).ls_name with match query_ident drv (fst d).ls_name with
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment