Mlw: continue work on declarations and builtins

src/core/env.ml

@@ -234,7 +234,6 @@ let base_builtin path =
     if s = builtin_theory.th_name.id_string then builtin_theory else
     if s = highord_theory.th_name.id_string then highord_theory else
     if s = bool_theory.th_name.id_string then bool_theory else
-    if s = unit_theory.th_name.id_string then unit_theory else
     match tuple_theory_name s with
     | Some n -> tuple_theory n
     | None -> raise Not_found

src/core/theory.mli

@@ -202,8 +202,6 @@ val builtin_theory : theory
 
 val bool_theory : theory
 
-val unit_theory : theory
-
 val highord_theory : theory
 
 val tuple_theory : int -> theory

src/mlw/dexpr.ml

@@ -1246,11 +1246,6 @@ let let_defn ?(keep_loc=true) (id,ghost,kind,de) =
       let e = expr uloc env_empty de in
       if e_ghost e && not ghost then Loc.errorm ?loc:id.pre_loc
         "Variable %s must be explicitly marked ghost" id.pre_name;
-(* TODO: this must be done at the declaration level
-      if not (ity_closed e.e_ity) then Loc.errorm ?loc:id.pre_loc
-        "Top-level variables must have monomorphic type";
-      if not (Eexec (Cfun | Cany)) then Loc.errorm ?loc:id.pre_loc
-        "Top-level computations must carry a specification"; *)
       fst (let_var id ~ghost e)
   | RKlemma, ([], _) -> Loc.errorm ?loc:id.pre_loc
       "Lemma-functions must have parameters"

src/mlw/expr.ml

@@ -916,12 +916,6 @@ let print_variant fmt varl =
 
 let protect_on x s = if x then "(" ^^ s ^^ ")" else s
 
-let print_list_next sep print fmt = function
-  | [] -> ()
-  | [x] -> print true fmt x
-  | x :: r -> print true fmt x; sep fmt ();
-      Pp.print_list sep (print false) fmt r
-
 let debug_print_labels = Debug.register_info_flag "print_labels"
   ~desc:"Print@ labels@ of@ identifiers@ and@ expressions."
 
@@ -1096,7 +1090,7 @@ and print_let_defn fmt = function
         (print_cexp false 0 (*4*)) c
   | LDrec rdl ->
       List.iter (fun fd -> Hrs.replace ht_rs fd.rec_rsym fd.rec_sym) rdl;
-      print_list_next Pp.newline print_rec_fun fmt rdl;
+      Pp.print_list_next Pp.newline print_rec_fun fmt rdl;
       List.iter (fun fd -> Hrs.remove ht_rs fd.rec_rsym) rdl
 
 and print_rec_fun fst fmt fd =

src/mlw/pdecl.ml

@@ -12,6 +12,7 @@
 open Ident
 open Ty
 open Term
+open Decl
 open Ity
 open Expr
 
@@ -38,17 +39,17 @@ let check_field stv f =
   let loc = f.pv_vs.vs_name.id_loc in
   let ftv = ity_freevars Stv.empty f.pv_ity in
   if not (Stv.subset ftv stv) then Loc.error ?loc
-    (Ty.UnboundTypeVar (Stv.choose (Stv.diff ftv stv)));
+    (UnboundTypeVar (Stv.choose (Stv.diff ftv stv)));
   if not f.pv_ity.ity_pure then Loc.error ?loc
-    (Ity.ImpureField f.pv_ity)
+    (ImpureField f.pv_ity)
 
 let check_invariant stv svs p =
   let ptv = t_ty_freevars Stv.empty p in
   let pvs = t_freevars Mvs.empty p in
   if not (Stv.subset ptv stv) then Loc.error ?loc:p.t_loc
-    (Ty.UnboundTypeVar (Stv.choose (Stv.diff ptv stv)));
+    (UnboundTypeVar (Stv.choose (Stv.diff ptv stv)));
   if not (Mvs.set_submap pvs svs) then Loc.error ?loc:p.t_loc
-    (Decl.UnboundVar (fst (Mvs.choose (Mvs.set_diff pvs svs))))
+    (UnboundVar (fst (Mvs.choose (Mvs.set_diff pvs svs))))
 
 let check_pure_its s = not s.its_privmut &&
   s.its_mfields = [] && s.its_regions = [] &&
@@ -144,7 +145,7 @@ let create_rec_variant_decl s cl =
 
 type pdecl = {
   pd_node : pdecl_node;
-  pd_pure : Decl.decl list;
+  pd_pure : decl list;
   pd_syms : Sid.t;
   pd_news : Sid.t;
   pd_tag  : int;
@@ -159,7 +160,7 @@ and pdecl_node =
 let pd_equal : pdecl -> pdecl -> bool = (==)
 
 let get_news node pure =
-  let news_id news id = Sid.add_new (Decl.ClashIdent id) id news in
+  let news_id news id = Sid.add_new (ClashIdent id) id news in
   let news_rs news s = news_id news s.rs_name in
   let news = match node with
     | PDtype dl ->
@@ -175,7 +176,7 @@ let get_news node pure =
         List.fold_left news_rd Sid.empty rdl
     | PDexn xs -> news_id Sid.empty xs.xs_name
     | PDpure -> Sid.empty in
-  let news_pure news d = Sid.union news d.Decl.d_news in
+  let news_pure news d = Sid.union news d.d_news in
   List.fold_left news_pure news pure
 
 let get_syms node pure =
@@ -183,7 +184,7 @@ let get_syms node pure =
   let syms_ls s ls = Sid.add ls.ls_name s in
   let syms_ty s ty = ty_s_fold syms_ts s ty in
   let syms_term s t = t_s_fold syms_ty syms_ls s t in
-  let syms_pure syms d = Sid.union syms d.Decl.d_syms in
+  let syms_pure syms d = Sid.union syms d.d_syms in
   let syms_vari syms (t,r) = Opt.fold syms_ls (syms_term syms t) r in
   let syms = List.fold_left syms_pure Sid.empty pure in
   let syms_its syms s = Sid.add s.its_ts.ts_name syms in
@@ -296,10 +297,42 @@ let mk_decl = let r = ref 0 in fun node pure ->
     pd_tag  = (incr r; !r) }
 
 let create_type_decl dl =
-  let ldl = assert false (* TODO *) in
-  mk_decl (PDtype dl) ldl
-
-let create_let_decl ld = let _ = PDlet ld in assert false (* TODO *)
+  let add_itd ({itd_its = s} as itd) (abst,defn,proj) =
+    match itd.itd_fields, itd.itd_constructors with
+    | fl, ([{rs_logic = RLnone}]|[]) ->
+        let get_ld s ldd = match s.rs_logic with
+          | RLls s -> create_param_decl s :: ldd | _ -> assert false in
+        create_ty_decl s.its_ts :: abst, defn, List.fold_right get_ld fl proj
+    | fl, cl ->
+        let add s f = Mpv.add (Opt.get f.rs_field) f s in
+        let mf = List.fold_left add Mpv.empty fl in
+        let get_fd s = match s.rs_logic with
+          | RLls s -> s | _ -> assert false in
+        let get_pj v = Opt.map get_fd (Mpv.find_opt v mf) in
+        let get_cs s = match s.rs_logic with
+          | RLls cs -> cs, List.map get_pj s.rs_cty.cty_args
+          | _ -> assert false in
+        abst, (s.its_ts, List.map get_cs cl) :: defn, proj in
+  let abst,defn,proj = List.fold_right add_itd dl ([],[],[]) in
+  let defn = if defn = [] then [] else [create_data_decl defn] in
+  mk_decl (PDtype dl) (abst @ defn @ proj)
+
+let create_let_decl ld =
+  let ls_of_rs s dl = match s.rs_logic with
+    | RLnone | RLlemma -> dl
+    | RLpv _ -> invalid_arg "Pdecl.create_let_decl"
+    | RLls s -> create_param_decl s :: dl in
+  let ldl = match ld with
+    | LDvar ({pv_vs = {vs_name = {id_loc = loc}}},e) ->
+        if not (ity_closed e.e_ity) then
+          Loc.errorm ?loc "Top-level variables must have monomorphic type";
+        if match e.e_node with Eexec _ -> false | _ -> true then
+          Loc.errorm ?loc "Top-level computations must carry a specification";
+        []
+    | LDrec rdl -> List.fold_right (fun d dl -> ls_of_rs d.rec_sym dl) rdl []
+    | LDsym (s,_) -> ls_of_rs s [] in
+  (* TODO: real function definitions and lemmas *)
+  mk_decl (PDlet ld) ldl
 
 let create_exn_decl xs =
   if not (ity_closed xs.xs_ity) then Loc.errorm ?loc:xs.xs_name.id_loc
@@ -325,11 +358,6 @@ let pd_int, pd_real, pd_equ = match builtin_theory.th_decls with
       mk_decl PDpure [de]
   | _ -> assert false
 
-let pd_unit = match unit_theory.th_decls with
-  | [{td_node = Use _t0}; {td_node = Decl du}] ->
-      mk_decl (PDtype [mk_itd its_unit [] [] []]) [du]
-  | _ -> assert false
-
 let pd_func, pd_pred, pd_func_app = match highord_theory.th_decls with
   | [{td_node = Use _bo};
      {td_node = Decl df}; {td_node = Decl dp}; {td_node = Decl da}] ->
@@ -343,32 +371,88 @@ let pd_bool = match bool_theory.th_decls with
       mk_decl (PDtype [mk_itd its_bool [] [rs_true; rs_false] []]) [db]
   | _ -> assert false
 
-let pd_tuple _n = assert false (*TODO*)
+let pd_tuple = Stdlib.Hint.memo 17 (fun n ->
+  match (tuple_theory n).th_decls with
+  | [{td_node = Decl dt}] ->
+      mk_decl (PDtype [mk_itd (its_tuple n) [] [rs_tuple n] []]) [dt]
+  | _ -> assert false)
 
 (** {2 Known identifiers} *)
 
 type known_map = pdecl Mid.t
 
 let known_id kn id =
-  if not (Mid.mem id kn) then raise (Decl.UnknownIdent id)
+  if not (Mid.mem id kn) then raise (UnknownIdent id)
 
 let merge_known kn1 kn2 =
   let check_known id decl1 decl2 =
     if pd_equal decl1 decl2 then Some decl1
-    else raise (Decl.RedeclaredIdent id) in
+    else raise (RedeclaredIdent id) in
   Mid.union check_known kn1 kn2
 
 let known_add_decl kn0 d =
   let kn = Mid.map (Util.const d) d.pd_news in
   let check id decl0 _ =
     if pd_equal decl0 d
-    then raise (Decl.KnownIdent id)
-    else raise (Decl.RedeclaredIdent id) in
+    then raise (KnownIdent id)
+    else raise (RedeclaredIdent id) in
   let kn = Mid.union check kn0 kn in
   let unk = Mid.set_diff d.pd_syms kn in
   if Sid.is_empty unk then kn else
-    raise (Decl.UnknownIdent (Sid.choose unk))
+    raise (UnknownIdent (Sid.choose unk))
 
 (** {2 Pretty-printing} *)
 
-let print_pdecl _fmt _d = assert false (* TODO *)
+open Format
+
+let print_its_defn fst fmt itd =
+  let s = itd.itd_its in
+  let print_args pr fmt tl = if tl <> [] then
+    fprintf fmt "@ %a" (Pp.print_list Pp.space pr) tl in
+  let print_regs pr fmt rl = if rl <> [] then
+    fprintf fmt "@ <%a>" (Pp.print_list Pp.comma pr) rl in
+  let print_field fmt f = fprintf fmt "%s%s%a%a : %a"
+    (if List.exists (pv_equal (Opt.get f.rs_field)) s.its_mfields
+      then "mutable " else "") (if rs_ghost f then "ghost " else "")
+    print_rs f Pretty.print_id_labels f.rs_name
+    print_ity f.rs_cty.cty_result in
+  let print_proj mf fmt f = match Mpv.find_opt f mf with
+    | Some f -> fprintf fmt "@ (%a)" print_field f
+    | _ when f.pv_ghost -> fprintf fmt "@ (ghost %a)" print_ity f.pv_ity
+    | _ -> fprintf fmt "@ %a" print_ity f.pv_ity in
+  let print_constr mf fmt c = fprintf fmt "@\n@[<hov 4}| %a%a%a@]"
+    print_rs c Pretty.print_id_labels c.rs_name
+    (Pp.print_list Pp.nothing (print_proj mf)) c.rs_cty.cty_args in
+  let print_defn fmt () =
+    match s.its_def, itd.itd_fields, itd.itd_constructors with
+    | Some ity, _, _ -> fprintf fmt " = %a" print_ity ity
+    | _, [], [] -> if s.its_privmut then fprintf fmt " = mutable {}"
+    | _, fl, [] -> fprintf fmt " = private%s { %a }"
+        (if s.its_privmut && s.its_mfields = [] then " mutable" else "")
+        (Pp.print_list Pp.semi print_field) fl
+    | _, fl, [_] when s.its_mfields <> [] || itd.itd_invariant <> [] ->
+        (* only records can have mutable fields or invariants *)
+        fprintf fmt " = { %a }"
+        (Pp.print_list Pp.semi print_field) fl
+    | _, fl, cl ->
+        let add s f = Mpv.add (Opt.get f.rs_field) f s in
+        let mf = List.fold_left add Mpv.empty fl in
+        Pp.print_list Pp.nothing (print_constr mf) fmt cl in
+  let print_inv fmt f = fprintf fmt
+    "@\n@  invariant { %a }" Pretty.print_term f in
+  fprintf fmt "@[<hov 2>%s %a%a%a%a%a%a@]"
+    (if fst then "type" else "with")
+    print_its s
+    Pretty.print_id_labels s.its_ts.ts_name
+    (print_args Pretty.print_tv) s.its_ts.ts_args
+    (print_regs print_reg) s.its_regions
+    print_defn ()
+    (Pp.print_list Pp.nothing print_inv) itd.itd_invariant
+
+let print_pdecl fmt d = match d.pd_node with
+  | PDtype dl -> Pp.print_list_next Pp.newline print_its_defn fmt dl
+  | PDlet ld -> print_let_defn fmt ld
+  | PDexn xs -> fprintf fmt
+      "@[<hov 2>exception %a%a of@ %a@]"
+        print_xs xs Pretty.print_id_labels xs.xs_name print_ity xs.xs_ity
+  | PDpure -> Pp.print_list Pp.newline2 Pretty.print_decl fmt d.pd_pure

src/mlw/pdecl.mli

@@ -69,7 +69,6 @@ val pd_int : pdecl
 val pd_real : pdecl
 val pd_equ : pdecl
 val pd_bool : pdecl
-val pd_unit : pdecl
 val pd_tuple : int -> pdecl
 val pd_func : pdecl
 val pd_pred : pdecl

src/mlw/pmodule.ml

@@ -264,52 +264,70 @@ let highord_module =
   let m = close_module uc in
   { m with mod_theory = highord_theory }
 
-let tuple_module _n = assert false (* TODO *)
-
-let tuple_module_name s = Theory.tuple_theory_name s
+let tuple_module = Hint.memo 17 (fun n ->
+  let nm = "Tuple" ^ string_of_int n in
+  let uc = empty_module None (id_fresh nm) ["why3";nm] in
+  let uc = add_pdecl uc (pd_tuple n) in
+  let m = close_module uc in
+  { m with mod_theory = tuple_theory n })
 
-(* TODO
 let unit_module =
   let uc = empty_module None (id_fresh "Unit") ["why3";"Unit"] in
   let uc = use_export uc (tuple_module 0) in
-  let uc = add_pdecl uc pd_unit in
-  let m = close_module uc in
-  { m with mod_theory = unit_theory }
-*)
+  let td = create_alias_decl (id_fresh "unit") [] ity_unit in
+  let uc = add_pdecl uc (create_type_decl [td]) in
+  close_module uc
 
 let create_module env ?(path=[]) n =
   let m = empty_module (Some env) n path in
   let m = use_export m builtin_module in
   let m = use_export m bool_module in
-(* TODO
   let m = use_export m unit_module in
-*)
-  let m = use_export m highord_module in
   m
 
 let add_pdecl ~wp uc d =
+  let ids = Mid.set_diff d.pd_syms uc.muc_known in
+  let uc = Sid.fold (fun id uc ->
+    if id_equal id ts_func.ts_name then
+      use_export uc highord_module
+    else match is_ts_tuple_id id with
+    | Some n -> use_export uc (tuple_module n)
+    | None -> uc) ids uc in
   ignore wp; (* TODO *)
   let uc = add_pdecl uc d in
   let th = List.fold_left Theory.add_decl uc.muc_theory d.pd_pure in
   { uc with muc_theory = th }
 
-let add_pdecl_with_tuples _uc _md = assert false (*TODO*)
-
 (** {2 WhyML language} *)
 
 type mlw_file = pmodule Mstr.t
 
-let mlw_language =
-  let conv mm = Mstr.map (fun m -> m.mod_theory) mm in
-  (Env.register_language Env.base_language conv : mlw_file Env.language)
-
-(* TODO
-let () = Env.add_builtin mlw_language (function
-  | [s] when s = mod_prelude.mod_theory.th_name.id_string ->
-      Mstr.singleton s mod_prelude,
-      Mstr.singleton s mod_prelude.mod_theory
-  | _ -> raise Not_found)
-*)
+let convert =
+  let dummy_env = Env.create_env [] in
+  let convert mm = Mstr.map (fun m -> m.mod_theory) mm in
+  fun mm -> if Mstr.is_empty mm then Mstr.empty else
+    match (snd (Mstr.choose mm)).mod_theory.th_path with
+    | ("why3" :: _) as path ->
+        begin try Env.read_library Env.base_language dummy_env path
+        with Env.LibraryNotFound _ -> convert mm end
+    | _ -> convert mm
+
+let mlw_language = Env.register_language Env.base_language convert
+
+open Theory
+
+let () =
+  let builtin s =
+    if s = unit_module.mod_theory.th_name.id_string then unit_module else
+    if s = builtin_theory.th_name.id_string then builtin_module else
+    if s = highord_theory.th_name.id_string then highord_module else
+    if s = bool_theory.th_name.id_string then bool_module else
+    match tuple_theory_name s with
+    | Some n -> tuple_module n
+    | None -> raise Not_found in
+  Env.add_builtin mlw_language (function
+    | [s] -> Mstr.singleton s (builtin s)
+    | _   -> raise Not_found)
 
 exception ModuleNotFound of Env.pathname * string
 

src/mlw/pmodule.mli

@@ -101,21 +101,11 @@ val add_pdecl : wp:bool -> pmodule_uc -> pdecl -> pmodule_uc
 (** {2 Builtin symbols} *)
 
 val builtin_module : pmodule
-
 val bool_module : pmodule
-
-(* TODO
 val unit_module : pmodule
-*)
-
 val highord_module : pmodule
-
 val tuple_module : int -> pmodule
 
-val tuple_module_name : string -> int option
-
-val add_pdecl_with_tuples : pmodule_uc -> pdecl -> pmodule_uc
-
 (** {2 WhyML language} *)
 
 open Env

src/tools/why3prove.ml

@@ -327,7 +327,7 @@ let do_theory env drv fname tname th glist elist =
       | None -> eprintf "Symbol '%s' has no definition in theory '%s'.@." x tname;
         exit 1
       | Some d ->
-        let l,t = Decl.open_ls_defn d in
+        let l,_t = Decl.open_ls_defn d in
         match l with
         | [] ->
 (* TODO

src/util/pp.ml

@@ -47,6 +47,12 @@ let print_list_delim ~start ~stop ~sep pr fmt = function
   | [] -> ()
   | l -> fprintf fmt "%a%a%a" start () (print_list sep pr) l stop ()
 
+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_iter1 iter sep print fmt l =
   let first = ref true in

src/util/pp.mli

@@ -31,6 +31,10 @@ val print_list_or_default :
 val print_list_par :
   (Format.formatter -> unit -> 'a) ->
   (Format.formatter -> 'b -> unit) -> Format.formatter -> 'b list -> unit
+val print_list_next :
+  (Format.formatter -> unit -> unit) ->
+  (bool -> Format.formatter -> 'a -> unit) ->
+  Format.formatter -> 'a list -> unit
 val print_list_delim :
   start:(Format.formatter -> unit -> unit) ->
   stop:(Format.formatter -> unit -> unit) ->