programs: changed label syntax / absurd / cast

parent 606b4541
......@@ -328,11 +328,11 @@ test: bin/why.byte $(TOOLS)
@printf "*** Checking Coq compilation ***\\n"
@for i in output_coq/*.v; do printf "coq $$i\\n" && coqc $$i ; done
testl: bin/whyl.byte
ocamlrun -bt bin/whyl.byte -I theories/ src/programs/test.mlw
testl: bin/whyml.byte
ocamlrun -bt bin/whyml.byte -I theories/ src/programs/test.mlw
examples/programs/%: bin/whyl.byte
bin/whyl.byte -I theories examples/programs/$*.mlw
examples/programs/%: bin/whyml.byte
bin/whyml.byte -I theories examples/programs/$*.mlw
#tools
######
......
......@@ -49,6 +49,9 @@ val report : Format.formatter -> error -> unit
val specialize_fsymbol :
Ptree.qualid -> theory_uc -> lsymbol * Denv.dty list * Denv.dty
val specialize_tysymbol :
Loc.position -> Ptree.qualid -> theory_uc -> Ty.tysymbol * Denv.type_var list
type denv
val create_denv : theory_uc -> denv
......@@ -62,3 +65,6 @@ val add_var : string -> Denv.dty -> denv -> denv
val type_term : denv -> vsymbol Mstr.t -> Ptree.lexpr -> term
val type_fmla : denv -> vsymbol Mstr.t -> Ptree.lexpr -> fmla
val dty : denv -> Ptree.pty -> Denv.dty
......@@ -55,6 +55,7 @@
"if", IF;
"in", IN;
"invariant", INVARIANT;
"label", LABEL;
"let", LET;
"match", MATCH;
"not", NOT;
......
......@@ -52,6 +52,8 @@ let rec report fmt = function
Typing.report fmt e
| Pgm_typing.Error e ->
Pgm_typing.report fmt e
| Denv.Error e ->
Denv.report fmt e
| e ->
raise e
(* fprintf fmt "anomaly: %s" (Printexc.to_string e) *)
......
......@@ -97,7 +97,7 @@
/* keywords */
%token ABSURD AND AS ASSERT ASSUME BEGIN CHECK DO DONE ELSE END EXCEPTION FOR
%token FUN GHOST IF IN INVARIANT LET MATCH NOT RAISE RAISES READS REC
%token FUN GHOST IF IN INVARIANT LABEL LET MATCH NOT RAISE RAISES READS REC
%token RETURNS THEN TRY TYPE VARIANT VOID WHILE WITH WRITES
/* symbols */
......@@ -244,10 +244,14 @@ expr:
{ mk_expr (Elet ($2, $4, $6)) }
| GHOST expr
{ mk_expr (Eghost $2) }
| uident COLON expr
{ mk_expr (Elabel ($1, $3)) }
| LABEL uident COLON expr
{ mk_expr (Elabel ($2, $4)) }
| WHILE expr DO loop_annotation expr DONE
{ mk_expr (Ewhile ($2, $4, $5)) }
| ABSURD
{ mk_expr Eabsurd }
| expr COLON pure_type
{ mk_expr (Ecast ($1, $3)) }
;
simple_expr:
......@@ -299,7 +303,27 @@ constant:
{ Term.ConstReal $1 }
;
/*****
type_var:
| QUOTE ident { $2 }
;
pure_type:
| type_var
{ PPTtyvar $1 }
| lqualid
{ PPTtyapp ([], $1) }
| pure_type lqualid
{ PPTtyapp ([$1], $2) }
| LEFTPAR pure_type COMMA list1_pure_type_sep_comma RIGHTPAR lqualid
{ PPTtyapp ($2 :: $4, $6) }
;
list1_pure_type_sep_comma:
| pure_type { [$1] }
| pure_type COMMA list1_pure_type_sep_comma { $1 :: $3 }
;
/***********************************************************************
ident_rich:
| uident { $1 }
......
......@@ -38,6 +38,19 @@ type loop_annotation = {
loop_variant : lexpr option;
}
type type_v =
| Tpure of Ptree.pty
(* | Tarrow of (ident * type_v) list * type_c *)
(*
and type_c =
{ pc_result_name : Ident.t;
pc_result_type : ptype_v;
pc_effect : peffect;
pc_pre : assertion list;
pc_post : postcondition option }
*)
type expr = {
expr_desc : expr_desc;
expr_loc : loc;
......@@ -55,10 +68,12 @@ and expr_desc =
| Ewhile of expr * loop_annotation * expr
| Elazy of lazy_op * expr * expr
| Eskip
| Eabsurd
(* annotations *)
| Eassert of assertion_kind * lexpr
| Eghost of expr
| Elabel of ident * expr
| Ecast of expr * Ptree.pty
(* TODO: fun, rec, raise, try, absurd, any, post? *)
......
......@@ -29,6 +29,9 @@ type lazy_op = Pgm_ptree.lazy_op
(* phase 1: destructive typing *)
type dtype_v =
| DTpure of Denv.dty
type dexpr = {
dexpr_desc : dexpr_desc;
dexpr_denv : Typing.denv;
......@@ -47,7 +50,8 @@ and dexpr_desc =
| DEif of dexpr * dexpr * dexpr
| DEwhile of dexpr * Pgm_ptree.loop_annotation * dexpr
| DElazy of lazy_op * dexpr * dexpr
| DEskip
| DEskip
| DEabsurd
| DEassert of assertion_kind * Ptree.lexpr
| DEghost of dexpr
......@@ -78,6 +82,7 @@ and expr_desc =
| Ewhile of expr * loop_annotation * expr
| Elazy of lazy_op * expr * expr
| Eskip
| Eabsurd
| Eassert of assertion_kind * Term.fmla
| Eghost of expr
......
......@@ -68,9 +68,14 @@ let create_denv uc =
ty_bool = Tyapp (ns_find_ts ns ["bool"], []);
ty_unit = Tyapp (ns_find_ts ns ["unit"], []);
ts_arrow = ns_find_ts ns ["arrow"];
}
(*****************************************************************************)
let create_type_var loc =
let tv = Ty.create_tvsymbol (id_user "a" loc) in
Tyvar (create_ty_decl_var ~loc ~user:false tv)
let currying env tyl ty =
let make_arrow_type ty1 ty2 = Tyapp (env.ts_arrow, [ty1; ty2]) in
List.fold_right make_arrow_type tyl ty
......@@ -83,6 +88,11 @@ let expected_type e ty =
(* phase 1: typing programs (using destructive type inference) *)
let pure_type env = Typing.dty env.denv
let rec dtype_v env = function
| Pgm_ptree.Tpure pt -> DTpure (pure_type env pt)
let rec dexpr env e =
let d, ty = expr_desc env e.Pgm_ptree.expr_loc e.Pgm_ptree.expr_desc in
{ dexpr_desc = d; dexpr_loc = e.Pgm_ptree.expr_loc;
......@@ -143,6 +153,8 @@ and expr_desc env loc = function
DElazy (op, e1, e2), env.ty_bool
| Pgm_ptree.Eskip ->
DEskip, env.ty_unit
| Pgm_ptree.Eabsurd ->
DEabsurd, create_type_var loc
| Pgm_ptree.Eassert (k, le) ->
DEassert (k, le), env.ty_unit
......@@ -153,6 +165,11 @@ and expr_desc env loc = function
(* TODO: add label to env *)
let e1 = dexpr env e1 in
DElabel (l, e1), e1.dexpr_type
| Pgm_ptree.Ecast (e1, ty) ->
let e1 = dexpr env e1 in
let ty = pure_type env ty in
expected_type e1 ty;
e1.dexpr_desc, ty
(* phase 2: typing annotations *)
......@@ -192,6 +209,8 @@ and expr_desc env denv = function
Elazy (op, expr env e1, expr env e2)
| DEskip ->
Eskip
| DEabsurd ->
Eabsurd
| DEassert (k, f) ->
let f = Typing.type_fmla denv env f in
......
(* Parameters.
Without loss of generality, we can take [x1=0] and [y1=0].
Thus the line to draw joins [(0,0)] to [(x2,y2)]
and we have [deltax = x2] and [deltay = y2].
Moreover we assume being in the first octant, i.e.
[0 <= y2 <= x2] (see the Coq file). The seven other cases can be easily
deduced by symmetry. *)
{
logic x2 : int
logic y2 : int
axiom First_octant : 0 <= y2 and y2 <= x2
}
(* Global variables of the program. *)
(* The code.
[(best x y)] expresses that the point [(x,y)] is the best
possible point i.e. the closest to the real line (see the Coq file).
The invariant relates [x], [y] and [e] and
gives lower and upper bound for [e] (see the Coq file). *)
{
use import int.Abs
logic best(x:int, y:int) =
forall y':int. abs (x2 * y - x * y2) <= abs (x2 * y' - x * y2)
logic invariant(x:int, y:int, e:int) =
e = 2 * (x + 1) * y2 - (2 * y + 1) * x2 and
2 * (y2 - x2) <= e and e <= 2 * y2
lemma Invariant_is_ok : forall x,y,e:int. invariant(x,y,e) -> best(x,y)
}
let bresenham =
let p =
let x = ref 0 in
let y = ref 0 in
let e = ref (2 * y2 - x2) in
while !x <= x2 do
invariant {0 <= !x and !x <= x2 + 1 and invariant(!x, !y, !e) }
variant { x2 + 1 - !x }
(* here we would do (plot x y) *)
assert { best(!x, !y) };
if !e < 0 then
e := !e + 2 * y2
else begin
y := !y + 1;
e := !e + 2 * (y2 - x2)
end;
x := !x + 1
done
x := 1;
assert { !x = 1 };
absurd : int
(*
......
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