Commit 17e8ab2a authored by MARCHE Claude's avatar MARCHE Claude
Browse files

new construction 'abstract e { q }' (unfinished)

parent 9d3b3853
......@@ -1190,6 +1190,8 @@ expr:
{ mk_expr (Etry ($2, $5)) }
| ANY simple_type_c
{ mk_expr (Eany $2) }
| ABSTRACT expr post
{ mk_expr (Eabstract($2, $3)) }
| label expr %prec prec_named
{ mk_expr (Enamed ($1, $2)) }
;
......
......@@ -241,6 +241,7 @@ and expr_desc =
| Emark of ident * expr
| Ecast of expr * pty
| Eany of type_c
| Eabstract of expr * post
| Enamed of label * expr
(* TODO: ghost *)
......
......@@ -483,6 +483,8 @@ let rec print_expr fmt e = match e.expr_desc with
fprintf fmt "<todo: Eletrec>"
| Eabsurd ->
fprintf fmt "assert false (* absurd *)"
| Eabstract(e, _) ->
fprintf fmt "@[%a (* abstract *)@]" print_expr e
and print_lexpr fmt e =
print_expr fmt e
......
......@@ -58,6 +58,8 @@ let rec print_expr fmt e = match e.expr_desc with
| Eany c ->
fprintf fmt "@[[any %a]@]" print_type_c c
| Eabstract(e1,q) ->
fprintf fmt "@[abstract %a %a]@]" print_expr e1 print_post q
| Emark (_, _) ->
fprintf fmt "<todo: Emark>"
......
......@@ -104,6 +104,7 @@ and dexpr_desc =
| DEassert of assertion_kind * Ptree.lexpr
| DEmark of string * dexpr
| DEany of dutype_c
| DEabstract of dexpr * dpost
and drecfun = (ident * Denv.dty) * dubinder list * dvariant option * dtriple
......@@ -205,6 +206,7 @@ and iexpr_desc =
| IEassert of assertion_kind * Term.term
| IEmark of mark * iexpr
| IEany of itype_c
| IEabstract of iexpr * ipost
and irecfun = ivsymbol * ibinder list * irec_variant option * itriple
......@@ -261,6 +263,7 @@ and expr_desc =
| Eassert of assertion_kind * Term.term
| Emark of mark * expr
| Eany of type_c
| Eabstract of expr * post
and recfun = pvsymbol * pvsymbol list * triple * E.t
......
......@@ -710,6 +710,10 @@ and dexpr_desc ~ghost ~userloc env loc = function
| Ptree.Eany c ->
let c = dutype_c env c in
DEany c, dpurify_utype_v c.duc_result_type
| Ptree.Eabstract(e1,q) ->
let e1 = dexpr ~ghost ~userloc env e1 in
let q = dpost env.uc q in
DEabstract(e1, q), e1.dexpr_type
| Ptree.Enamed _ ->
assert false
......@@ -1339,6 +1343,11 @@ and iexpr_desc env loc ty = function
| DEany c ->
let c = iutype_c env c in
IEany c
| DEabstract(e1, q) ->
let e1 = iexpr env e1 in
let ty = e1.iexpr_type in
let q = iupost env ty q in
IEabstract(e1,q)
and decompose_app env e args = match e.dexpr_desc with
| DEapply (e1, e2) ->
......@@ -1550,6 +1559,7 @@ let rec is_pure_expr e =
| 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
| Eabstract (e1, _)
| Emark (_, e1) -> is_pure_expr e1
| Eany c -> E.no_side_effect c.c_effect
| Eassert _ | Etry _ | Efor _ | Eraise _ | Ematch _
......@@ -1785,6 +1795,13 @@ and expr_desc gl env loc ty = function
| IEany c ->
let c = type_c env c in
Eany c, c.c_result_type, c.c_effect
| IEabstract(e1, q) ->
let e1 = expr gl env e1 in
let q = saturation e1.expr_loc e1.expr_effect q in
let ef = e1.expr_effect in
let ef, q = post_effect ef q in
let e1 = { e1 with expr_effect = ef } in
Eabstract(e1,q), e1.expr_type_v, ef
and triple ?(sat_exn=true) gl env (p, e, q) =
let e = expr gl env e in
......@@ -1916,7 +1933,7 @@ let rec fresh_expr gl ~term locals e = match e.expr_desc with
List.iter (fun (_, _, e2) -> fresh_expr gl ~term locals e2) hl
| Efor (_, _, _, _, _, e1) ->
fresh_expr gl ~term:false locals e1
| Eabstract(e, _)
| Emark (_, e) ->
fresh_expr gl ~term locals e
| Eassert _ | Eany _ ->
......
......@@ -640,6 +640,10 @@ and wp_desc env rm e q = match e.expr_desc with
let p = wp_label e (wp_expl "precondition" c.c_pre) in
let p = t_label ~loc:e.expr_loc p.t_label p in
wp_and p w
| Eabstract(e1,((_normal,_exns) as post)) ->
let w1 = wp_expr env rm e1 post in
let w2 = t_false (* TODO *) in
wp_and ~sym:true w1 w2
and wp_triple env rm bl (p, e, q) =
let rm = add_binders bl rm in
......
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