Commit b8a2ff2a authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

whyml: introduce create_let_(pv|ps)_defn

these return the newly created symbol, saving us a pattern matching
in let_defn.
parent 122f0b4c
......@@ -348,12 +348,7 @@ let d2 =
Mlw_expr.e_app e1 [c0]
in
(* building the first part of the let x = ref 0 *)
let letdef = Mlw_expr.create_let_defn (Ident.id_fresh "x") e in
(* get back the variable x *)
let var_x = match letdef.Mlw_expr.let_sym with
| Mlw_expr.LetV vs -> vs
| Mlw_expr.LetA _ -> assert false
in
let letdef, var_x = Mlw_expr.create_let_pv_defn (Ident.id_fresh "x") e in
(* building expression "!x" *)
let bang_x =
(* recall that "!" as type "ref 'a -> 'a" *)
......
......@@ -265,11 +265,7 @@ let create_var_full v =
let id = Ident.id_fresh v.vname in
let ty = ctype v.vtype in
let def = Mlw_expr.e_app (mk_ref ty) [any ty] in
let let_defn = Mlw_expr.create_let_defn id def in
let vs = match let_defn.Mlw_expr.let_sym with
| Mlw_expr.LetV vs -> vs
| Mlw_expr.LetA _ -> assert false
in
let let_defn, vs = Mlw_expr.create_let_pv_defn id def in
(*
Self.result "create program variable %s (%d)" v.vname v.vid;
*)
......
......@@ -499,6 +499,18 @@ let create_let_defn id e =
| VTvalue ity -> LetV (create_pvsymbol id ~ghost:e.e_ghost ity) in
{ let_sym = lv ; let_expr = e }
let create_let_pv_defn id e =
let ld = create_let_defn id e in
match ld.let_sym with
| LetA _ -> Loc.error ?loc:e.e_loc (ValueExpected e)
| LetV pv -> ld, pv
let create_let_ps_defn id e =
let ld = create_let_defn id e in
match ld.let_sym with
| LetV _ -> Loc.error ?loc:e.e_loc (ArrowExpected e)
| LetA ps -> ld, ps
let e_let ({ let_sym = lv ; let_expr = d } as ld) e =
let id = match lv with
| LetV pv -> pv.pv_vs.vs_name
......@@ -511,11 +523,7 @@ let e_let ({ let_sym = lv ; let_expr = d } as ld) e =
let on_value fn e = match e.e_node with
| Evalue pv -> fn pv
| _ ->
let id = id_fresh ?loc:e.e_loc "o" in
let ld = create_let_defn id e in
let pv = match ld.let_sym with
| LetA _ -> Loc.error ?loc:e.e_loc (ValueExpected e)
| LetV pv -> pv in
let ld,pv = create_let_pv_defn (id_fresh ?loc:e.e_loc "o") e in
e_let ld (fn pv)
(* application *)
......@@ -714,11 +722,7 @@ let on_fmla fn e = match e.e_node with
| Elogic t -> fn e (t_equ_simp t t_bool_true)
| Evalue pv -> fn e (t_equ_simp (t_var pv.pv_vs) t_bool_true)
| _ ->
let id = id_fresh ?loc:e.e_loc "o" in
let ld = create_let_defn id e in
let pv = match ld.let_sym with
| LetA _ -> Loc.error ?loc:e.e_loc (ValueExpected e)
| LetV pv -> pv in
let ld,pv = create_let_pv_defn (id_fresh ?loc:e.e_loc "o") e in
e_let ld (fn (e_value pv) (t_equ_simp (t_var pv.pv_vs) t_bool_true))
let e_not e =
......@@ -900,8 +904,7 @@ let rec expr_subst psm e = e_label_copy e (match e.e_node with
Loc.errorm "vty_value mismatch";
e_let { let_sym = LetV pv ; let_expr = nd } (expr_subst psm e)
| Elet ({ let_sym = LetA ps ; let_expr = d }, e) ->
let ld = create_let_defn (id_clone ps.ps_name) (expr_subst psm d) in
let ns = match ld.let_sym with LetA a -> a | LetV _ -> assert false in
let ld,ns = create_let_ps_defn (id_clone ps.ps_name) (expr_subst psm d) in
e_let ld (expr_subst (Mid.add ps.ps_name ns psm) e)
| Erec (fdl, e) ->
let conv lam = { lam with l_expr = expr_subst psm lam.l_expr } in
......
......@@ -210,7 +210,10 @@ val e_app : expr -> expr list -> expr
val e_lapp : lsymbol -> expr list -> ity -> expr
val e_plapp : plsymbol -> expr list -> ity -> expr
val create_let_defn : preid -> expr -> let_defn
val create_let_defn : preid -> expr -> let_defn
val create_let_pv_defn : preid -> expr -> let_defn * pvsymbol
val create_let_ps_defn : preid -> expr -> let_defn * psymbol
val create_fun_defn : preid -> lambda -> fun_defn
val create_rec_defn : (psymbol * lambda) list -> fun_defn list
......
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