Commit f112a95c authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

removed theory unit.Unit; programs: type unit is now alias for tuple0

parent d41cca42
...@@ -252,7 +252,7 @@ clean:: ...@@ -252,7 +252,7 @@ clean::
# test target # test target
%: %.mlw bin/whyml.byte %: %.mlw bin/whyml.byte
bin/whyml.byte -P alt-ergo --debug $*.mlw bin/whyml.byte -P alt-ergo $*.mlw
############### ###############
# proof manager # proof manager
......
...@@ -54,6 +54,7 @@ programs () { ...@@ -54,6 +54,7 @@ programs () {
if ! $pgml $pgml_options $f > /dev/null 2>&1; then if ! $pgml $pgml_options $f > /dev/null 2>&1; then
echo echo
echo "$pgml $pgml_options $f" echo "$pgml $pgml_options $f"
$pgml $pgml_options $f
echo "FAILED!" echo "FAILED!"
exit 1 exit 1
else else
...@@ -81,6 +82,8 @@ valid_goals () { ...@@ -81,6 +82,8 @@ valid_goals () {
echo -n " "$f"... " echo -n " "$f"... "
if $pgml -P alt-ergo $f | grep -q -v Valid; then if $pgml -P alt-ergo $f | grep -q -v Valid; then
echo "valid test $f failed!" echo "valid test $f failed!"
echo "$pgml -P alt-ergo $f"
$pgml -P alt-ergo $f
exit 1 exit 1
else else
echo "ok" echo "ok"
......
...@@ -104,9 +104,9 @@ theory bool.Bool ...@@ -104,9 +104,9 @@ theory bool.Bool
syntax logic False "false" syntax logic False "false"
end end
theory unit.Unit theory Tuple0
syntax type unit "unit" syntax type tuple0 "unit"
syntax logic Unit "void" syntax logic Tuple0 "void"
end end
theory algebra.AC theory algebra.AC
......
...@@ -20,18 +20,11 @@ let rec f91 (n:int) : int variant { 101-n } = ...@@ -20,18 +20,11 @@ let rec f91 (n:int) : int variant { 101-n } =
logic iter_f (n x:int) : int = logic iter_f (n x:int) : int =
if n = 0 then x else iter_f (n-1) (f x) if n = 0 then x else iter_f (n-1) (f x)
(*
clone import relations.Lex with type t1 = int, type t2 = int, clone import relations.Lex with type t1 = int, type t2 = int,
logic r1 = lt_nat, logic r2 = lt_int logic rel1 = lt_nat, logic rel2 = lt_nat
*)
inductive lex (int,int) (int,int) =
| Lex_1: forall x1 y1 x2 y2 : int.
lt_nat x1 x2 -> lex (x1,y1) (x2,y2)
| Lex_2: forall x y1 y2 : int.
lt_nat y1 y2 -> lex (x,y1) (x,y2)
} }
let f91_nonrec (n:ref int) (x:ref int) = let f91_nonrec (n x : ref int) =
{ !n >= 1 } { !n >= 1 }
label L: label L:
while !n > 0 do while !n > 0 do
......
(* How many integers 0 <= n < 10^18 have the property that the sum
of the digits of n equals the sum of digits of 137n? *)
(* answer: 20444710234716473 *)
{ {
use import int.EuclideanDivision use import int.EuclideanDivision
...@@ -7,12 +11,18 @@ ...@@ -7,12 +11,18 @@
if n = 0 then 0 else sum_digits (div n 10) + mod n 10 if n = 0 then 0 else sum_digits (div n 10) + mod n 10
logic p (n:int) = sum_digits(n) = sum_digits(137 * n) logic p (n:int) = sum_digits(n) = sum_digits(137 * n)
clone int.NumOf as P with logic p = p clone int.NumOf as P with logic pr = p
type int2 = (int,int) type int2 = (int,int)
logic q (d:int2) (n:int) = logic q (d:int2) (n:int) =
let (a,b) = d in sum_digits(n) = sum_digits(137 * n + a) = b let (a,b) = d in sum_digits(n) = sum_digits(137 * n + a) = b
clone int.NumOfDep as Q with type dep = int2, logic p = q clone int.NumOfParam as Q with type param = int2, logic pr = q
type int3 = (int,int,int)
logic r (d:int3) (n:int) =
let (a,b,c) = d in
0 <= mod n 10 < c and sum_digits(n) = sum_digits(137 * n + a) = b
clone int.NumOfParam as R with type param = int3, logic pr = r
goal Test : forall n:int. 0 <= n < power 10 0 -> n = 0 goal Test : forall n:int. 0 <= n < power 10 0 -> n = 0
} }
...@@ -27,7 +37,7 @@ let rec sd n = ...@@ -27,7 +37,7 @@ let rec sd n =
{ result = sum_digits n } { result = sum_digits n }
(* f(m,a,b) = the number of 0 <= n < 10^m such that (* f(m,a,b) = the number of 0 <= n < 10^m such that
digitsum(n) = digitsum(137n+a)+b. *) digitsum(n) = digitsum(137n+a) + b. *)
let rec f m a b = let rec f m a b =
{ 0 <= m } { 0 <= m }
if m = 0 then begin if m = 0 then begin
......
...@@ -39,8 +39,12 @@ let create_env = ...@@ -39,8 +39,12 @@ let create_env =
env_memo = Hashtbl.create 17; env_memo = Hashtbl.create 17;
env_tag = !r } env_tag = !r }
in in
let th = builtin_theory in let add th m = Mnm.add th.th_name.id_string th m in
let m = Mnm.add th.th_name.id_string th Mnm.empty in let m = Mnm.empty in
let m = add builtin_theory m in
let m = add (tuple_theory 0) m in
let m = add (tuple_theory 1) m in
let m = add (tuple_theory 2) m in
Hashtbl.add env.env_memo [] m; Hashtbl.add env.env_memo [] m;
env env
......
...@@ -114,8 +114,10 @@ let report fmt = function ...@@ -114,8 +114,10 @@ let report fmt = function
let () = Exn_printer.register let () = Exn_printer.register
(fun fmt exn -> match exn with (fun fmt exn -> match exn with
| Error error -> report fmt error | Error error ->
| _ -> raise exn) report fmt error
| _ ->
raise exn)
(** Environments *) (** Environments *)
......
...@@ -132,7 +132,7 @@ let empty_env uc = { ...@@ -132,7 +132,7 @@ let empty_env uc = {
ts_label = find_ts uc ["label"]; ts_label = find_ts uc ["label"];
ts_ref = find_ts uc ["ref"]; ts_ref = find_ts uc ["ref"];
ts_exn = find_ts uc ["exn"]; ts_exn = find_ts uc ["exn"];
ts_unit = find_ts uc ["unit"]; ts_unit = find_ts uc ["tuple0"];
(* functions *) (* functions *)
ls_at = find_ls uc ["at"]; ls_at = find_ls uc ["at"];
ls_bang = find_ls uc ["prefix !"]; ls_bang = find_ls uc ["prefix !"];
......
...@@ -42,7 +42,7 @@ type env = private { ...@@ -42,7 +42,7 @@ type env = private {
ts_bool : tysymbol; ts_bool : tysymbol;
ts_label: tysymbol; ts_label: tysymbol;
ts_ref : tysymbol; ts_ref : tysymbol;
ts_exn: tysymbol; ts_exn : tysymbol;
ts_unit : tysymbol; ts_unit : tysymbol;
ls_at : lsymbol; ls_at : lsymbol;
ls_bang : lsymbol; ls_bang : lsymbol;
......
...@@ -488,6 +488,8 @@ type_v: ...@@ -488,6 +488,8 @@ type_v:
{ Tarrow ([id_anonymous (), Some $1], $3) } { Tarrow ([id_anonymous (), Some $1], $3) }
| lident COLON simple_type_v ARROW type_c | lident COLON simple_type_v ARROW type_c
{ Tarrow ([$1, Some $3], $5) } { Tarrow ([$1, Some $3], $5) }
/* TODO: we could alllow lidents instead, e.g. x y : int -> ... */
/*{ Tarrow (List.map (fun x -> x, Some $3) $1, $5) }*/
; ;
simple_type_v: simple_type_v:
......
...@@ -77,9 +77,11 @@ let lexpr (loc, s) = parse_string Lexer.parse_lexpr loc s ...@@ -77,9 +77,11 @@ let lexpr (loc, s) = parse_string Lexer.parse_lexpr loc s
(* phase 1: typing programs (using destructive type inference) **************) (* phase 1: typing programs (using destructive type inference) **************)
let dty_bool gl = Tyapp (gl.ts_bool, []) let dty_app (ts, tyl) = assert (ts.ts_def = None); Tyapp (ts, tyl)
let dty_unit gl = Tyapp (gl.ts_unit, [])
let dty_label gl = Tyapp (gl.ts_label, []) let dty_bool gl = dty_app (gl.ts_bool, [])
let dty_unit gl = dty_app (gl.ts_unit, [])
let dty_label gl = dty_app (gl.ts_label, [])
(* note: local variables are sqimultaneously in locals (to type programs) (* note: local variables are sqimultaneously in locals (to type programs)
and in denv (to type logic elements) *) and in denv (to type logic elements) *)
...@@ -153,7 +155,7 @@ let create_type_var loc = ...@@ -153,7 +155,7 @@ let create_type_var loc =
Tyvar (create_ty_decl_var ~loc ~user:false tv) Tyvar (create_ty_decl_var ~loc ~user:false tv)
let dcurrying gl tyl ty = let dcurrying gl tyl ty =
let make_arrow_type ty1 ty2 = Tyapp (gl.ts_arrow, [ty1; ty2]) in let make_arrow_type ty1 ty2 = dty_app (gl.ts_arrow, [ty1; ty2]) in
List.fold_right make_arrow_type tyl ty List.fold_right make_arrow_type tyl ty
let uncurrying gl ty = let uncurrying gl ty =
...@@ -181,7 +183,7 @@ let rec dpurify env = function ...@@ -181,7 +183,7 @@ let rec dpurify env = function
(dpurify env c.dc_result_type) (dpurify env c.dc_result_type)
let check_reference_type gl loc ty = let check_reference_type gl loc ty =
let ty_ref = Tyapp (gl.ts_ref, [create_type_var loc]) in let ty_ref = dty_app (gl.ts_ref, [create_type_var loc]) in
if not (Denv.unify ty ty_ref) then if not (Denv.unify ty ty_ref) then
errorm ~loc "this expression has type %a, but is expected to be a reference" errorm ~loc "this expression has type %a, but is expected to be a reference"
print_dty ty print_dty ty
...@@ -200,7 +202,7 @@ let dreference env id = ...@@ -200,7 +202,7 @@ let dreference env id =
let dexception env id = let dexception env id =
let _, _, ty as r = specialize_exception id.id_loc id.id env.env in let _, _, ty as r = specialize_exception id.id_loc id.id env.env in
let ty_exn = Tyapp (env.env.ts_exn, []) in let ty_exn = dty_app (env.env.ts_exn, []) in
if not (Denv.unify ty ty_exn) then if not (Denv.unify ty ty_exn) then
errorm ~loc:id.id_loc errorm ~loc:id.id_loc
"this expression has type %a, but is expected to be an exception" "this expression has type %a, but is expected to be an exception"
...@@ -284,9 +286,9 @@ let rec dexpr env e = ...@@ -284,9 +286,9 @@ let rec dexpr env e =
and dexpr_desc env loc = function and dexpr_desc env loc = function
| Pgm_ptree.Econstant (ConstInt _ as c) -> | Pgm_ptree.Econstant (ConstInt _ as c) ->
DEconstant c, Tyapp (Ty.ts_int, []) DEconstant c, dty_app (Ty.ts_int, [])
| Pgm_ptree.Econstant (ConstReal _ as c) -> | Pgm_ptree.Econstant (ConstReal _ as c) ->
DEconstant c, Tyapp (Ty.ts_real, []) DEconstant c, dty_app (Ty.ts_real, [])
| Pgm_ptree.Eident (Qident {id=x}) when Mstr.mem x env.locals -> | Pgm_ptree.Eident (Qident {id=x}) when Mstr.mem x env.locals ->
(* local variable *) (* local variable *)
let tyv = Mstr.find x env.locals in let tyv = Mstr.find x env.locals in
...@@ -302,7 +304,7 @@ and dexpr_desc env loc = function ...@@ -302,7 +304,7 @@ and dexpr_desc env loc = function
let e1 = dexpr env e1 in let e1 = dexpr env e1 in
let e2 = dexpr env e2 in let e2 = dexpr env e2 in
let ty2 = create_type_var loc and ty = create_type_var loc in let ty2 = create_type_var loc and ty = create_type_var loc in
if not (Denv.unify e1.dexpr_type (Tyapp (env.env.ts_arrow, [ty2; ty]))) if not (Denv.unify e1.dexpr_type (dty_app (env.env.ts_arrow, [ty2; ty])))
then then
errorm ~loc:e1.dexpr_loc "this expression is not a function"; errorm ~loc:e1.dexpr_loc "this expression is not a function";
expected_type e2 ty2; expected_type e2 ty2;
...@@ -327,7 +329,7 @@ and dexpr_desc env loc = function ...@@ -327,7 +329,7 @@ and dexpr_desc env loc = function
let n = List.length el in let n = List.length el in
let s = Typing.fs_tuple n in let s = Typing.fs_tuple n in
let tyl = List.map (fun _ -> create_type_var loc) el in let tyl = List.map (fun _ -> create_type_var loc) el in
let ty = Tyapp (Typing.ts_tuple n, tyl) in let ty = dty_app (Typing.ts_tuple n, tyl) in
let create d ty = let create d ty =
{ dexpr_desc = d; dexpr_denv = env.denv; { dexpr_desc = d; dexpr_denv = env.denv;
dexpr_type = ty; dexpr_loc = loc } dexpr_type = ty; dexpr_loc = loc }
...@@ -337,7 +339,7 @@ and dexpr_desc env loc = function ...@@ -337,7 +339,7 @@ and dexpr_desc env loc = function
assert (Denv.unify e2.dexpr_type ty2); assert (Denv.unify e2.dexpr_type ty2);
let ty = create_type_var loc in let ty = create_type_var loc in
assert (Denv.unify e1.dexpr_type assert (Denv.unify e1.dexpr_type
(Tyapp (env.env.ts_arrow, [ty2; ty]))); (dty_app (env.env.ts_arrow, [ty2; ty])));
create (DEapply (e1, e2)) ty create (DEapply (e1, e2)) ty
in in
let e = create (DElogic s) (dcurrying env.env tyl ty) in let e = create (DElogic s) (dcurrying env.env tyl ty) in
......
let rec foo (x:int) variant {x} = {
{ x >= 0 } type t = (int, int)
if x = 0 then 0 else foo (x-1) logic x : t = (1, 2) : t
{ result = 0 } }
let test () = {} foo 4 {result=0} let test (x : ref int) = x := 0; 1
(* (*
Local Variables: Local Variables:
......
...@@ -94,48 +94,49 @@ theory Power ...@@ -94,48 +94,49 @@ theory Power
end end
theory NumOf theory NumOfParam
type param
use import Int use import Int
logic p int logic pr param int
(* number of n st a <= n < b and p(n) *) (* number of n st a <= n < b and pr(p,n) *)
logic num_of (a b : int) : int logic num_of (p : param) (a b : int) : int
axiom Num_of_empty : axiom Num_of_empty :
forall a b : int. b <= a -> num_of a b = 0 forall p : param, a b : int.
axiom Num_of_zero : b <= a -> num_of p a b = 0
forall a b : int. a < b -> not p a -> num_of a b = num_of (a+1) b
axiom Num_of_one : axiom Num_of_left_no_add :
forall a b : int. a < b -> p a -> num_of a b = 1 + num_of (a+1) b forall p : param, a b : int.
a < b -> not pr p a -> num_of p a b = num_of p (a+1) b
axiom Num_of_left_add :
forall p : param, a b : int.
a < b -> pr p a -> num_of p a b = 1 + num_of p (a+1) b
axiom Num_of_right_no_add :
forall p : param, a b : int.
a < b -> not pr p (b-1) -> num_of p a b = num_of p a (b-1)
axiom Num_of_right_add :
forall p : param, a b : int.
a < b -> pr p (b-1) -> num_of p a b = 1 + num_of p a (b-1)
axiom Num_of_append : axiom Num_of_append :
forall a b c : int. a < b < c -> num_of a c = num_of a b + num_of b c forall p : param, a b c : int.
a <= b <= c -> num_of p a c = num_of p a b + num_of p b c
end end
theory NumOfDep theory NumOf
type dep
use import Int logic pr int
logic p dep int logic pr0 () (n : int) = pr n
(* number of n st a <= n < b and p(d,n) *) clone NumOfParam as N with type param = tuple0, logic pr = pr0
logic num_of dep (a b : int) : int
axiom Num_of_empty : logic num_of (a b : int) : int = N.num_of () a b
forall d : dep, a b : int.
b <= a -> num_of d a b = 0
axiom Num_of_zero :
forall d : dep, a b : int.
a < b -> not p d a -> num_of d a b = num_of d (a+1) b
axiom Num_of_one :
forall d : dep, a b : int.
a < b -> p d a -> num_of d a b = 1 + num_of d (a+1) b
axiom Num_of_append :
forall d : dep, a b c : int.
a < b < c -> num_of d a c = num_of d a b + num_of d b c
end end
...@@ -17,7 +17,7 @@ theory Prelude ...@@ -17,7 +17,7 @@ theory Prelude
axiom Ge_bool_def : forall x y:int. ge_bool x y = True <-> x>=y axiom Ge_bool_def : forall x y:int. ge_bool x y = True <-> x>=y
axiom Gt_bool_def : forall x y:int. gt_bool x y = True <-> x> y axiom Gt_bool_def : forall x y:int. gt_bool x y = True <-> x> y
use export unit.Unit type unit = ()
logic ignore 'a : unit logic ignore 'a : unit
type arrow 'a 'b type arrow 'a 'b
......
...@@ -162,23 +162,21 @@ theory TotalOrder ...@@ -162,23 +162,21 @@ theory TotalOrder
end end
*) *)
(*
theory Lex theory Lex
type t1 type t1
type t2 type t2
logic r1 t1 t1 logic rel1 t1 t1
logic r2 t2 t2 logic rel2 t2 t2
inductive lex (t1, t2) (t1, t2) = inductive lex (t1, t2) (t1, t2) =
| Lex_1: forall (x1 x2 : t1) (y1 y2 : t2). | Lex_1: forall x1 x2 : t1, y1 y2 : t2.
r1 x1 x2 -> lex (x1,y1) (x2,y2) rel1 x1 x2 -> lex (x1,y1) (x2,y2)
| Lex_2: forall (x : t1) (y1 y2 : t2). | Lex_2: forall x : t1, y1 y2 : t2.
r2 y1 y2 -> lex (x,y1) (x,y2) rel2 y1 y2 -> lex (x,y1) (x,y2)
end end
*)
(* (*
theory MinMax theory MinMax
......
theory Unit
type unit = Unit
end
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