programs: less constructs in abstract syntax

parent 7ac0a5a7
......@@ -55,6 +55,7 @@ type env = {
ls_False: lsymbol;
ls_andb : lsymbol;
ls_orb : lsymbol;
ls_unit : lsymbol;
}
......@@ -141,6 +142,7 @@ let empty_env uc = {
ls_False = find_ls uc ["False"];
ls_andb = find_ls uc ["andb"];
ls_orb = find_ls uc ["orb"];
ls_unit = find_ls uc ["Tuple0"];
}
let make_arrow_type env tyl ty =
......
......@@ -51,6 +51,7 @@ type env = private {
ls_False: lsymbol;
ls_andb : lsymbol;
ls_orb : lsymbol;
ls_unit : lsymbol;
}
val empty_env : theory_uc -> env
......
......@@ -87,7 +87,6 @@ and dexpr_desc =
| DEloop of dloop_annotation * dexpr
| DElazy of lazy_op * dexpr * dexpr
| DEmatch of dexpr * (Denv.dpattern * dexpr) list
| DEskip
| DEabsurd
| DEraise of Term.lsymbol * dexpr option
| DEtry of dexpr * (Term.lsymbol * string option * dexpr) list
......@@ -142,12 +141,10 @@ and iexpr_desc =
| IElet of Term.vsymbol * iexpr * iexpr
| IEletrec of irecfun list * iexpr
| IEsequence of iexpr * iexpr
| IEif of iexpr * iexpr * iexpr
| IEloop of loop_annotation * iexpr
| IElazy of lazy_op * iexpr * iexpr
| IEmatch of Term.vsymbol * (Term.pattern * iexpr) list
| IEskip
| IEabsurd
| IEraise of Term.lsymbol * iexpr option
| IEtry of iexpr * (Term.lsymbol * Term.vsymbol option * iexpr) list
......@@ -180,11 +177,9 @@ and expr_desc =
| Elet of Term.vsymbol * expr * expr
| Eletrec of recfun list * expr
| Esequence of expr * expr
| Eif of expr * expr * expr
| Eloop of loop_annotation * expr
| Ematch of Term.vsymbol * (Term.pattern * expr) list
| Eskip
| Eabsurd
| Eraise of Term.lsymbol * expr option
| Etry of expr * (Term.lsymbol * Term.vsymbol option * expr) list
......
......@@ -390,7 +390,7 @@ and dexpr_desc env loc = function
let bl = List.map branch bl in
DEmatch (e1, bl), ty
| Pgm_ptree.Eskip ->
DEskip, (dty_unit env.env)
DElogic env.env.ls_unit, (dty_unit env.env)
| Pgm_ptree.Eabsurd ->
DEabsurd, create_type_var loc
| Pgm_ptree.Eraise (id, e) ->
......@@ -660,7 +660,8 @@ and iexpr_desc gl env loc ty = function
IEletrec (dl, e1)
| DEsequence (e1, e2) ->
IEsequence (iexpr gl env e1, iexpr gl env e2)
let vs = create_vsymbol (id_fresh "_") (ty_app gl.ts_unit []) in
IElet (vs, iexpr gl env e1, iexpr gl env e2)
| DEif (e1, e2, e3) ->
IEif (iexpr gl env e1, iexpr gl env e2, iexpr gl env e3)
| DEloop (la, e1) ->
......@@ -681,8 +682,6 @@ and iexpr_desc gl env loc ty = function
let bl = List.map branch bl in
let v = create_vsymbol (id_user "x" loc) e1.iexpr_type in
IElet (v, e1, mk_iexpr loc ty (IEmatch (v, bl)))
| DEskip ->
IEskip
| DEabsurd ->
IEabsurd
| DEraise (ls, e) ->
......@@ -798,9 +797,6 @@ let rec print_iexpr fmt e = match e.iexpr_desc with
fprintf fmt "@[let %a = %a in@ %a@]" print_vs v
print_iexpr e1 print_iexpr e2
| IEsequence (e1, e2) ->
fprintf fmt "@[%a;@\n%a@]" print_iexpr e1 print_iexpr e2
| _ ->
fprintf fmt "<other>"
......@@ -854,13 +850,13 @@ let without_exn_check f x =
let rec is_pure_expr e =
E.no_side_effect e.expr_effect &&
match e.expr_desc with
| Elocal _ | Elogic _ | Eskip -> true
| Elocal _ | Elogic _ -> true
| Eif (e1, e2, e3) -> is_pure_expr e1 && is_pure_expr e2 && is_pure_expr e3
| Elet (_, e1, e2) -> is_pure_expr e1 && is_pure_expr e2
| Elabel (_, e1) -> is_pure_expr e1
| Eany c -> E.no_side_effect c.c_effect
| Eassert _ | Etry _ | Eraise _ | Ematch _
| Eloop _ | Esequence _ | Eletrec _ | Efun _
| Eloop _ | Eletrec _ | Efun _
| Eglobal _ | Eabsurd -> false (* TODO: improve *)
let mk_expr loc ty ef d =
......@@ -939,11 +935,6 @@ and expr_desc gl env loc ty = function
let e1 = expr gl env e1 in
Eletrec (dl, e1), e1.expr_type_v, e1.expr_effect
| IEsequence (e1, e2) ->
let e1 = expr gl env e1 in
let e2 = expr gl env e2 in
let ef = E.union e1.expr_effect e2.expr_effect in
Esequence (e1, e2), e2.expr_type_v, ef
| IEif (e1, e2, e3) ->
let e1 = expr gl env e1 in
let e2 = expr gl env e2 in
......@@ -999,8 +990,6 @@ and expr_desc gl env loc ty = function
in
let ef, bl = map_fold_left branch E.empty bl in
Ematch (v, bl), Tpure ty, ef
| IEskip ->
Eskip, Tpure ty, E.empty
| IEabsurd ->
Eabsurd, Tpure ty, E.empty
| IEraise (x, e1) ->
......@@ -1109,9 +1098,6 @@ let rec fresh_expr gl ~term locals e = match e.expr_desc with
List.iter (fun (_, _, _, t) -> fresh_triple gl t) fl;
fresh_expr gl ~term locals e1
| Esequence (e1, e2) ->
fresh_expr gl ~term:false locals e1;
fresh_expr gl ~term locals e2
| Eif (e1, e2, e3) ->
fresh_expr gl ~term:false locals e1;
fresh_expr gl ~term locals e2;
......@@ -1121,7 +1107,7 @@ let rec fresh_expr gl ~term locals e = match e.expr_desc with
| Ematch (_, bl) ->
let branch (_, e1) = fresh_expr gl ~term locals e1 in
List.iter branch bl
| Eskip | Eabsurd | Eraise (_, None) ->
| Eabsurd | Eraise (_, None) ->
()
| Eraise (_, Some e1) ->
fresh_expr gl ~term:false locals e1
......@@ -1152,8 +1138,6 @@ let rec print_expr fmt e = match e.expr_desc with
fprintf fmt "@[let %a = %a in@ %a@]" print_vs v
print_expr e1 print_expr e2
| Esequence (e1, e2) ->
fprintf fmt "@[%a;@\n%a@]" print_expr e1 print_expr e2
| Eif (e1, e2, e3) ->
fprintf fmt "@[if %a@ then@ %a else@ %a@]"
print_expr e1 print_expr e2 print_expr e3
......
......@@ -284,10 +284,6 @@ and wp_desc env e q = match e.expr_desc with
let wl = List.map (wp_recfun env) dl in
wp_ands ~sym:true (w1 :: wl)
| Esequence (e1, e2) ->
let w2 = wp_expr env e2 (filter_post e2.expr_effect q) in
let q1 = saturate_post e1.expr_effect (v_result e1.expr_type, w2) q in
wp_expr env e1 q1
| Eif (e1, e2, e3) ->
let w2 = wp_expr env e2 (filter_post e2.expr_effect q) in
let w3 = wp_expr env e3 (filter_post e3.expr_effect q) in
......@@ -323,8 +319,6 @@ and wp_desc env e q = match e.expr_desc with
in
let t = t_var x in
f_case t (List.map branch bl)
| Eskip ->
let (_, q), _ = q in q
| Eabsurd ->
f_false
| Eraise (x, None) ->
......
......@@ -12,9 +12,11 @@ let f () =
assert { !r > 0 }
let foo () =
let x = any {} int {result=0} in
let y = any {} int {result=result+1} in
assert { false }
let x = ref 0 in
x := 1;
assert { !x = 1 };
x := !x + 1;
assert { !x > 1 }
(*
Local Variables:
......
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