Attention une mise à jour du service Gitlab va être effectuée le mardi 30 novembre entre 17h30 et 18h00. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes. Cette mise à jour intermédiaire en version 14.0.12 nous permettra de rapidement pouvoir mettre à votre disposition une version plus récente.

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

programs: raising exceptions

parent d7b92194
......@@ -183,7 +183,7 @@ logic inv_succ2(src:vertex, s:vertex S.t, q: vertex S.t,
let shortest_path_code (src:vertex) (dst:vertex) =
{ S.mem(src,v) and S.mem(dst,v) }
init src;
while not (q_is_empty Unit) do
while not (q_is_empty ()) do
invariant { inv(src, !visited, !q, !d) and inv_succ(src, !visited, !q) }
variant { S.cardinal(v) - S.cardinal(!visited) }
let u = q_extract_min () in
......
......@@ -59,6 +59,7 @@
"let", LET;
"match", MATCH;
"not", NOT;
"of", OF;
"parameter", PARAMETER;
"raise", RAISE;
"raises", RAISES;
......
......@@ -68,6 +68,7 @@
let id = { id = prefix op; id_loc = loc_i 1 } in
mk_expr (mk_apply_id id [e1])
let id_unit () = { id = "Unit"; id_loc = loc () }
let id_result () = { id = "result"; id_loc = loc () }
let id_anonymous () = { id = "_"; id_loc = loc () }
......@@ -107,7 +108,7 @@
%token ABSURD AND AS ASSERT ASSUME BEGIN CHECK DO DONE ELSE END
%token EXCEPTION FOR
%token FUN GHOST IF IN INVARIANT LABEL LET MATCH NOT PARAMETER
%token FUN GHOST IF IN INVARIANT LABEL LET MATCH NOT OF PARAMETER
%token RAISE RAISES READS REC
%token THEN TRY TYPE VARIANT WHILE WITH WRITES
......@@ -189,6 +190,10 @@ decl:
{ Dletrec $3 }
| PARAMETER lident COLON type_v
{ Dparam ($2, $4) }
| EXCEPTION uident
{ Dexn ($2, None) }
| EXCEPTION uident OF pure_type
{ Dexn ($2, Some $4) }
;
list1_recfun_sep_and:
......@@ -288,6 +293,10 @@ expr:
{ mk_expr Eabsurd }
| expr COLON pure_type
{ mk_expr (Ecast ($1, $3)) }
| RAISE uident
{ mk_expr (Eraise ($2, None)) }
| RAISE LEFTPAR uident expr RIGHTPAR
{ mk_expr (Eraise ($3, Some $4)) }
;
triple:
......
......@@ -80,13 +80,14 @@ and expr_desc =
| Ematch of expr list * (Ptree.pattern list * expr) list
| Eskip
| Eabsurd
| Eraise of ident * expr option
(* annotations *)
| Eassert of assertion_kind * lexpr
| Eghost of expr
| Elabel of ident * expr
| Ecast of expr * Ptree.pty
(* TODO: raise, try, any, post?, ghost *)
(* TODO: try, any, post?, ghost *)
and triple = lexpr * expr * lexpr
......@@ -95,6 +96,7 @@ type decl =
| Dletrec of (ident * binder list * variant option * triple) list
| Dlogic of Ptree.decl list
| Dparam of ident * type_v
| Dexn of ident * Ptree.pty option
type file = decl list
......@@ -81,6 +81,7 @@ and dexpr_desc =
| DEmatch of dexpr list * (Typing.dpattern list * dexpr) list
| DEskip
| DEabsurd
| DEraise of Term.lsymbol * dexpr option
| DEassert of assertion_kind * Ptree.lexpr
| DEghost of dexpr
......@@ -142,6 +143,7 @@ and expr_desc =
| Ematch of expr list * (Term.pattern list * expr) list
| Eskip
| Eabsurd
| Eraise of Term.lsymbol * expr option
| Eassert of assertion_kind * Term.fmla
| Eghost of expr
......
......@@ -56,11 +56,16 @@ let id_result = "result"
(* environments *)
let dty_bool uc = Tyapp (ns_find_ts (get_namespace uc) ["bool"], [])
let dty_unit uc = Tyapp (ns_find_ts (get_namespace uc) ["unit"], [])
let dty_label uc = Tyapp (ns_find_ts (get_namespace uc) ["label"], [])
let ts_unit uc = ns_find_ts (get_namespace uc) ["unit"]
let ts_ref uc = ns_find_ts (get_namespace uc) ["ref"]
let ts_arrow uc = ns_find_ts (get_namespace uc) ["arrow"]
let ts_exn uc = ns_find_ts (get_namespace uc) ["exn"]
let ls_Unit uc = ns_find_ls (get_namespace uc) ["Unit"]
let dty_bool uc = Tyapp (ns_find_ts (get_namespace uc) ["bool"], [])
let dty_unit uc = Tyapp (ts_unit uc, [])
let dty_label uc = Tyapp (ns_find_ts (get_namespace uc) ["label"], [])
type denv = {
uc : theory_uc;
......@@ -104,28 +109,40 @@ let rec dpurify env = function
dcurrying env.uc (List.map (fun (_,ty) -> dpurify env ty) bl)
(dpurify env c.dc_result_type)
let check_reference _loc _ty =
() (*TODO*)
let check_reference_type uc loc ty =
let ty_ref =Tyapp (ts_ref uc, [create_type_var loc]) in
if not (Denv.unify ty ty_ref) then
errorm ~loc "this expression has type %a, but is expected to be a reference"
print_dty ty
let dreference env id =
if Typing.mem_var id.id env.denv then
(* local variable *)
let ty = Typing.find_var id.id env.denv in
check_reference id.id_loc ty;
check_reference_type env.uc id.id_loc ty;
DRlocal id.id
else
let p = Qident id in
let s, _tyl, ty = Typing.specialize_fsymbol p env.uc in
check_reference id.id_loc ty;
let s, _, ty = Typing.specialize_fsymbol p env.uc in
check_reference_type env.uc id.id_loc ty;
DRglobal s
let dexception _env _id =
assert false (*TODO*)
let dexception env id =
let p = Qident id in
let _, _, ty as r = Typing.specialize_fsymbol p env.uc in
let ty_exn = Tyapp (ts_exn env.uc, []) in
if not (Denv.unify ty ty_exn) then
errorm ~loc:id.id_loc
"this expression has type %a, but is expected to be an exception"
print_dty ty;
r
let deffect env e =
{ de_reads = List.map (dreference env) e.Pgm_ptree.pe_reads;
de_writes = List.map (dreference env) e.Pgm_ptree.pe_writes;
de_raises = List.map (dexception env) e.Pgm_ptree.pe_raises; }
de_raises =
List.map (fun id -> let ls,_,_ = dexception env id in ls)
e.Pgm_ptree.pe_raises; }
let rec dtype_v env = function
| Pgm_ptree.Tpure pt ->
......@@ -239,6 +256,24 @@ and dexpr_desc env loc = function
DEskip, (dty_unit env.uc)
| Pgm_ptree.Eabsurd ->
DEabsurd, create_type_var loc
| Pgm_ptree.Eraise (id, e) ->
let ls, tyl, _ = dexception env id in
let e = match e, tyl with
| None, [] ->
None
| Some _, [] ->
errorm ~loc "expection %s has no argument" id.id
| None, [ty] ->
errorm ~loc "exception %s is expecting an argument of type %a"
id.id print_dty ty;
| Some e, [ty] ->
let e = dexpr env e in
expected_type e ty;
Some e
| _ ->
assert false
in
DEraise (ls, e), create_type_var loc
| Pgm_ptree.Eassert (k, le) ->
DEassert (k, le), (dty_unit env.uc)
......@@ -389,6 +424,8 @@ and expr_desc uc env denv = function
Eskip
| DEabsurd ->
Eabsurd
| DEraise (ls, e) ->
Eraise (ls, option_map (expr uc env) e)
| DEassert (k, f) ->
let f = Typing.type_fmla denv env f in
......@@ -433,6 +470,11 @@ let type_expr uc e =
let e = dexpr denv e in
expr uc Mstr.empty e
let type_type uc ty =
let denv = create_denv uc in
let dty = Typing.dty denv.denv ty in
Denv.ty_of_dty dty
let add_decl uc ls =
try
Theory.add_decl uc (Decl.create_logic_decl [ls, None])
......@@ -475,6 +517,15 @@ let file env uc dl =
let ls = create_lsymbol (id_user id.id id.id_loc) tyl (Some ty) in
let uc = add_decl uc ls in
uc, Dparam (ls, tyv) :: acc
| Pgm_ptree.Dexn (id, ty) ->
let tyl = match ty with
| None -> []
| Some ty -> [type_type uc ty]
in
let exn = ty_app (ts_exn uc) [] in
let ls = create_lsymbol (id_user id.id id.id_loc) tyl (Some exn) in
let uc = add_decl uc ls in
uc, acc
)
(uc, []) dl
in
......@@ -491,6 +542,5 @@ End:
TODO:
- mutually recursive functions: check variants are all present or all absent
- variant: check type int or relation order specified
- typing exceptions in effects (raises)
*)
......@@ -4,6 +4,11 @@ use import list.List
logic c : int
}
exception Not_found
exception Found of int
let test_raise (x:bool) = raise Not_found : int
let test (n:int) =
let rec is_even (x:int) =
{true}
......
......@@ -23,4 +23,6 @@ theory Prelude
type label
logic at ('a, label) : 'a
logic old ('a) : 'a
end
\ No newline at end of file
type exn
end
theory Base
theory Set
type 'a t
......@@ -17,9 +17,6 @@ theory Base
forall x, y : 'a. forall s : 'a t.
mem(x, add(y, s)) <-> (x = y or mem(x, s))
logic add'(x:'a, s:'a t) : 'a t =
epsilon res:'a t. forall y:'a. mem(y, res) <-> (y = x or mem(y, s))
logic remove('a, 'a t) : 'a t
axiom Remove_def1 :
......@@ -53,7 +50,7 @@ end
(* finite sets *)
theory Fset
use import int.Int
clone export Base
clone export Set
logic cardinal('a t) : int
......@@ -74,6 +71,3 @@ theory Fset
end
theory Set
clone export Base
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