Commit 2ac5d569 authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: api for parameter declarations

parent afa16279
......@@ -42,6 +42,7 @@ type pdecl = {
and pdecl_node =
| PDtype of itysymbol
| PDdata of data_decl list
| PDval of val_decl
| PDlet of let_defn
| PDrec of rec_defn list
| PDexn of xsymbol
......@@ -147,6 +148,15 @@ let create_rec_decl rdl =
let syms = List.fold_left add_rd Sid.empty rdl in
mk_decl (PDrec rdl) syms news
let create_val_decl vd =
let id = match vd.val_name with
| LetV pv -> pv.pv_vs.vs_name
| LetA ps -> ps.ps_name in
let news = Sid.singleton id in
(* FIXME!!! See the comment in create_let_decl *)
let syms = Mid.map (fun _ -> ()) vd.val_vars in
mk_decl (PDval vd) syms news
let create_exn_decl xs =
let news = Sid.singleton xs.xs_name in
let syms = Sid.empty (* FIXME!!! *) in
......@@ -185,4 +195,4 @@ let find_constructors kn its =
match (Mid.find its.its_pure.ts_name kn).pd_node with
| PDtype _ -> []
| PDdata dl -> List.assq its dl
| PDlet _ | PDrec _ | PDexn _ -> assert false
| PDval _ | PDlet _ | PDrec _ | PDexn _ -> assert false
......@@ -44,6 +44,7 @@ type pdecl = private {
and pdecl_node = private
| PDtype of itysymbol
| PDdata of data_decl list
| PDval of val_decl
| PDlet of let_defn
| PDrec of rec_defn list
| PDexn of xsymbol
......@@ -58,6 +59,8 @@ val create_data_decl : pre_data_decl list -> pdecl
val create_ty_decl : itysymbol -> pdecl
val create_val_decl : val_decl -> pdecl
val create_let_decl : let_defn -> pdecl
val create_rec_decl : rec_defn list -> pdecl
......
......@@ -116,7 +116,7 @@ type let_var =
type val_decl = {
val_name : let_var;
val_decl : type_v;
val_spec : type_v;
val_vars : varset Mid.t;
}
......@@ -221,7 +221,7 @@ let create_val_decl id tyv =
let name = match build_v vars tyv with
| VTarrow vta -> LetA (create_psymbol id vta vars)
| VTvalue vtv -> LetV (create_pvsymbol id vtv) in
{ val_name = name; val_decl = tyv; val_vars = varm }
{ val_name = name; val_spec = tyv; val_vars = varm }
(** patterns *)
......
......@@ -110,7 +110,7 @@ type let_var =
type val_decl = private {
val_name : let_var;
val_decl : type_v;
val_spec : type_v;
val_vars : varset Mid.t;
}
......
......@@ -274,8 +274,8 @@ let add_pdecl uc d =
let defn cl = List.map constructor cl in
let dl = List.map (fun (its,cl) -> its.its_pure, defn cl) dl in
add_to_theory Theory.add_data_decl uc dl
| PDlet ld ->
add_let uc ld.let_var
| PDval { val_name = lv } | PDlet { let_var = lv } ->
add_let uc lv
| PDrec rdl ->
List.fold_left add_rec uc rdl
| PDexn xs ->
......
......@@ -156,10 +156,38 @@ let print_psty fmt ps =
print_regs (Mreg.set_diff vars.vars_reg ps.ps_subst.ity_subst_reg)
print_vta ps.ps_vta
let print_ppat fmt ppat = print_pat fmt ppat.ppat_pattern
(* specification *)
let print_post fmt post =
let vs,f = open_post post in
fprintf fmt "%a ->@ %a" print_vs vs print_term f
let print_lv fmt = function
| LetV pv -> print_pvty fmt pv
| LetA ps -> print_psty fmt ps
let forget_lv = function
| LetV pv -> forget_pv pv
| LetA ps -> forget_ps ps
let rec print_type_v fmt = function
| SpecV vtv -> print_vtv fmt vtv
| SpecA (pvl,tyc) ->
let print_arg fmt pv = fprintf fmt "(%a) ->@ " print_pvty pv in
fprintf fmt "%a%a" (print_list nothing print_arg) pvl print_type_c tyc
and print_type_c fmt tyc =
fprintf fmt "{ %a }@ %a%a@ { %a }@]"
print_term tyc.c_pre
print_effect tyc.c_effect
print_type_v tyc.c_result
print_post tyc.c_post
(* TODO: print_xpost *)
(* expressions *)
let print_ppat fmt ppat = print_pat fmt ppat.ppat_pattern
let print_ak fmt = function
| Aassert -> fprintf fmt "assert"
| Aassume -> fprintf fmt "assume"
......@@ -220,12 +248,6 @@ and print_enode pri fmt e = match e.e_node with
| Eapp (e,v) ->
fprintf fmt "(%a@ %a)" (print_lexpr pri) e print_pv v
| Elet ({ let_var = lv ; let_expr = e1 }, e2) ->
let print_lv fmt = function
| LetV pv -> print_pvty fmt pv
| LetA ps -> print_psty fmt ps in
let forget_lv = function
| LetV pv -> forget_pv pv
| LetA ps -> forget_ps ps in
fprintf fmt (protect_on (pri > 0) "let %a = @[%a@] in@ %a")
print_lv lv (print_lexpr 4) e1 print_expr e2;
forget_lv lv
......@@ -251,9 +273,11 @@ and print_enode pri fmt e = match e.e_node with
| Eabsurd ->
fprintf fmt "absurd"
| Eassert (ak,f) ->
fprintf fmt "%a@ (%a)" print_ak ak print_term f
| _ ->
fprintf fmt "<expr TODO>"
fprintf fmt "%a@ { %a }" print_ak ak print_term f
| Eghost e ->
fprintf fmt "ghost@ %a" print_expr e
| Eany tyc ->
fprintf fmt "any@ %a" print_type_c tyc
and print_branch fmt ({ ppat_pattern = p }, e) =
fprintf fmt "@[<hov 4>| %a ->@ %a@]" print_pat p print_expr e;
......@@ -264,9 +288,6 @@ and print_xbranch fmt (xs, pv, e) =
forget_pv pv
and print_rec fst fmt { rec_ps = ps ; rec_lambda = lam } =
let print_post fmt post =
let vs,f = open_post post in
fprintf fmt "%a ->@ %a" print_vs vs print_term f in
let print_arg fmt pv = fprintf fmt "(%a)" print_pvty pv in
fprintf fmt "@[<hov 2>%s (%a) %a =@ { %a }@ %a@ { %a }@]"
(if fst then "let rec" else "with")
......@@ -275,6 +296,7 @@ and print_rec fst fmt { rec_ps = ps ; rec_lambda = lam } =
print_term lam.l_pre
print_expr lam.l_expr
print_post lam.l_post
(* TODO: print_xpost *)
(*
and print_tl fmt tl =
......@@ -332,10 +354,12 @@ let print_data_decl fst fmt (ts,csl) =
(print_head fst) ts (print_list newline print_constr) csl;
forget_tvs_regs ()
let print_val_decl fmt { val_name = lv ; val_spec = tyv } =
fprintf fmt "@[<hov 2>val %a : @[%a@]@]" print_lv lv print_type_v tyv;
(* FIXME: don't forget global regions *)
forget_tvs_regs ()
let print_let_decl fmt { let_var = lv ; let_expr = e } =
let print_lv fmt = function
| LetV pv -> print_pvty fmt pv
| LetA ps -> print_psty fmt ps in
fprintf fmt "@[<hov 2>let %a = @[%a@]@]" print_lv lv print_expr e;
(* FIXME: don't forget global regions *)
forget_tvs_regs ()
......@@ -353,6 +377,7 @@ let print_exn_decl fmt xs =
let print_pdecl fmt d = match d.pd_node with
| PDtype ts -> print_ty_decl fmt ts
| PDdata tl -> print_list_next newline print_data_decl fmt tl
| PDval vd -> print_val_decl fmt vd
| PDlet ld -> print_let_decl fmt ld
| PDrec rdl -> print_list_next newline print_rec_decl fmt rdl
| PDexn xs -> print_exn_decl fmt xs
......
......@@ -54,6 +54,9 @@ val print_ppat : formatter -> ppattern -> unit (* program patterns *)
val print_expr : formatter -> expr -> unit (* expression *)
val print_type_c : formatter -> type_c -> unit
val print_type_v : formatter -> type_v -> unit
val print_ty_decl : formatter -> itysymbol -> unit
val print_data_decl : formatter -> data_decl -> unit
val print_next_data_decl : formatter -> data_decl -> unit
......
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