Commit fd71d34a authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: type function declarations

parent 2c7397db
......@@ -42,6 +42,8 @@ type pdecl = {
and pdecl_node =
| PDtype of itysymbol
| PDdata of data_decl list
| PDlet of let_defn
| PDrec of rec_defn list
let pd_equal : pdecl -> pdecl -> bool = (==)
......@@ -121,6 +123,28 @@ let create_data_decl tdl =
let tdl = List.map build_type tdl in
mk_decl (PDdata tdl) !syms !news
let create_let_decl ld =
let id = match ld.let_var with
| LetV pv -> pv.pv_vs.vs_name
| LetA ps -> ps.ps_name in
let news = Sid.singleton id in
(* FIXME!!! This is not a correct way of counting symbols,
since it ignores type symbols and exception symbols, and
lsymbols inside specifications. We should either extend
varmap keeping in Mlw_expr to track all those symbols
(associating them to empty varsets), or use per-symbol maps
and folds in Mlw_ty and Mlw_expr, like we do in Ty and Term. *)
let syms = Mid.map (fun _ -> ()) ld.let_expr.e_vars in
mk_decl (PDlet ld) syms news
let create_rec_decl rdl =
if rdl = [] then raise Decl.EmptyDecl;
let add_rd s rd = news_id s rd.rec_ps.ps_name in
let news = List.fold_left add_rd Sid.empty rdl in
let add_rd s rd = Sid.union s (Mid.map (fun _ -> ()) rd.rec_vars) in
(* FIXME!!! See the comment in create_let_decl *)
let syms = List.fold_left add_rd Sid.empty rdl in
mk_decl (PDrec rdl) syms news
(** {2 Known identifiers} *)
......@@ -149,10 +173,10 @@ let known_add_decl lkn0 kn0 decl =
if Sid.is_empty unk then kn
else raise (UnknownIdent (Sid.choose unk))
(* TODO: known_add_decl must check pattern matches for exhaustiveness *)
let find_constructors kn its =
match (Mid.find its.its_pure.ts_name kn).pd_node with
| PDtype _ -> []
| PDdata dl -> List.assq its dl
(*
| _ -> assert false
*)
| PDlet _ | PDrec _ -> assert false
......@@ -44,6 +44,8 @@ type pdecl = private {
and pdecl_node = private
| PDtype of itysymbol
| PDdata of data_decl list
| PDlet of let_defn
| PDrec of rec_defn list
(** {2 Declaration constructors} *)
......@@ -55,6 +57,10 @@ val create_data_decl : pre_data_decl list -> pdecl
val create_ty_decl : itysymbol -> pdecl
val create_let_decl : let_defn -> pdecl
val create_rec_decl : rec_defn list -> pdecl
(** {2 Known identifiers} *)
type known_map = pdecl Mid.t
......
......@@ -235,6 +235,13 @@ let add_data uc (its,csl) =
let uc = add_symbol add_it its.its_pure.ts_name its uc in
List.fold_left add_constr uc csl
let add_let uc = function
| LetV pv -> add_symbol add_ps pv.pv_vs.vs_name (PV pv) uc
| LetA ps -> add_symbol add_ps ps.ps_name (PS ps) uc
let add_rec uc { rec_ps = ps } =
add_symbol add_ps ps.ps_name (PS ps) uc
let add_pdecl uc d =
let uc = { uc with
muc_decls = d :: uc.muc_decls;
......@@ -252,6 +259,10 @@ 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
| PDrec rdl ->
List.fold_left add_rec uc rdl
let add_pdecl_with_tuples uc d =
let ids = Mid.set_diff d.pd_syms uc.muc_known in
......
......@@ -160,6 +160,12 @@ let print_ppat fmt ppat = print_pat fmt ppat.ppat_pattern
(* expressions *)
let print_list_next sep print fmt = function
| [] -> ()
| [x] -> print true fmt x
| x :: r -> print true fmt x; sep fmt ();
print_list sep (print false) fmt r
let rec print_expr fmt e = print_lexpr 0 fmt e
and print_lexpr pri fmt e =
......@@ -219,21 +225,9 @@ and print_enode pri fmt e = match e.e_node with
print_lv lv (print_lexpr 4) e1 print_expr e2;
forget_lv lv
| Erec (rdl,e) ->
let print_and fmt () = fprintf fmt "@\nand@\n" in
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_rd fmt { rec_ps = ps ; rec_lambda = lam } =
fprintf fmt "(%a) %a =@ { %a }@ %a@ { %a }"
print_psty ps
(print_list space print_pvty) lam.l_args
print_term lam.l_pre
print_expr lam.l_expr
print_post lam.l_post
in
fprintf fmt (protect_on (pri > 0) "%a@ in@ %a")
(print_list_next newline print_rec) rdl print_expr e;
let forget_rd rd = forget_ps rd.rec_ps in
fprintf fmt (protect_on (pri > 0) "@[<hov 4>let rec %a@]@ in@ %a")
(print_list print_and print_rd) rdl print_expr e;
List.iter forget_rd rdl
| Eif (v,e1,e2) ->
fprintf fmt (protect_on (pri > 0) "if %a then %a@ else %a")
......@@ -251,6 +245,19 @@ and print_branch fmt ({ ppat_pattern = p }, e) =
fprintf fmt "@[<hov 4>| %a ->@ %a@]" print_pat p print_expr e;
Svs.iter forget_var p.pat_vars
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")
print_psty ps
(print_list space print_arg) lam.l_args
print_term lam.l_pre
print_expr lam.l_expr
print_post lam.l_post
(*
and print_tl fmt tl =
if tl = [] then () else fprintf fmt "@ [%a]"
......@@ -307,20 +314,31 @@ let print_data_decl fst fmt (ts,csl) =
(print_head fst) ts (print_list newline print_constr) csl;
forget_tvs_regs ()
(* Declarations *)
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 ()
let print_list_next sep print fmt = function
| [] -> ()
| [x] -> print true fmt x
| x :: r -> print true fmt x; sep fmt ();
print_list sep (print false) fmt r
let print_rec_decl fst fmt rd =
print_rec fst fmt rd;
forget_tvs_regs ()
(* Declarations *)
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
| PDlet ld -> print_let_decl fmt ld
| PDrec rdl -> print_list_next newline print_rec_decl fmt rdl
let print_next_data_decl = print_data_decl false
let print_data_decl = print_data_decl true
let print_next_data_decl = print_data_decl false
let print_data_decl = print_data_decl true
let print_next_rec_decl = print_rec_decl false
let print_rec_decl = print_rec_decl true
let print_module fmt m =
fprintf fmt "@[<hov 2>module %a%a@\n%a@]@\nend@."
......
......@@ -1005,11 +1005,18 @@ let add_module lib path mm mt m =
let uc = open_namespace uc in
let uc = List.fold_left add_decl uc dl in
Loc.try3 loc close_namespace uc import name
| Dlet (_id, e) ->
| Dlet (id, e) ->
let e = dexpr ~userloc:None (create_denv uc) e in
let e = expr Mstr.empty e in
Format.eprintf "@[%a@]@." Mlw_pretty.print_expr e;
uc
let pd = match e.dexpr_desc with
| DEfun (bl, tr) ->
let def = expr_fun Mstr.empty id bl tr in
create_rec_decl [def]
| _ ->
let e = expr Mstr.empty e in
let def = create_let_defn (id_user id) e in
create_let_decl def
in
Loc.try2 loc add_pdecl_with_tuples uc pd
| Dletrec _ | Dparam _ | Dexn _ ->
assert false (* TODO *)
| Duse _ ->
......
......@@ -25,12 +25,9 @@ module N
type myrec 'a = {| f1 : int ; ghost f2 : tree 'a |}
let h x =
let bang y = y.contents in
match x with
| {| f2 = Node x _ |} -> Node x Nil
| _ -> Leaf
end
let bang y = y.contents
let h () = bang
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