Mlw: use correct pure declarations in the builtins

src/mlw/pdecl.ml

@@ -159,24 +159,24 @@ and pdecl_node =
 let pd_equal : pdecl -> pdecl -> bool = (==)
 
 let get_news node pure =
-  let news_id s id = Sid.add_new (Decl.ClashIdent id) id s in
+  let news_id news id = Sid.add_new (Decl.ClashIdent id) id news in
   let news_rs news s = news_id news s.rs_name in
+  let news = match node with
+    | PDtype dl ->
+        let news_itd news d =
+          let news = news_id news d.itd_its.its_ts.ts_name in
+          let news = List.fold_left news_rs news d.itd_fields in
+          List.fold_left news_rs news d.itd_constructors in
+        List.fold_left news_itd Sid.empty dl
+    | PDlet (LDvar (v,_)) -> news_id Sid.empty v.pv_vs.vs_name
+    | PDlet (LDsym (s,_)) -> news_id Sid.empty s.rs_name
+    | PDlet (LDrec rdl) ->
+        let news_rd news d = news_id news d.rec_sym.rs_name in
+        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 = List.fold_left news_pure Sid.empty pure in
-  match node with
-  | PDtype dl ->
-      let news_itd news d =
-        let news = news_id news d.itd_its.its_ts.ts_name in
-        let news = List.fold_left news_rs news d.itd_fields in
-        List.fold_left news_rs news d.itd_constructors in
-      List.fold_left news_itd news dl
-  | PDlet (LDvar (v,_)) -> news_id news v.pv_vs.vs_name
-  | PDlet (LDsym (s,_)) -> news_id news s.rs_name
-  | PDlet (LDrec rdl) ->
-      let news_rd news d = news_id news d.rec_sym.rs_name in
-      List.fold_left news_rd news rdl
-  | PDexn xs -> news_id news xs.xs_name
-  | PDpure -> news
+  List.fold_left news_pure news pure
 
 let get_syms node pure =
   let syms_ts s ts = Sid.add ts.ts_name s in
@@ -312,21 +312,39 @@ let create_pure_decl d = mk_decl PDpure [d]
 
 (** {2 Built-in decls} *)
 
-let pd_int  = mk_decl (PDtype [mk_itd its_int  [] [] []]) [(*TODO*)]
-let pd_real = mk_decl (PDtype [mk_itd its_real [] [] []]) [(*TODO*)]
-let pd_unit = mk_decl (PDtype [mk_itd its_unit [] [] []]) [(*TODO*)]
-let pd_func = mk_decl (PDtype [mk_itd its_func [] [] []]) [(*TODO*)]
-let pd_pred = mk_decl (PDtype [mk_itd its_pred [] [] []]) [(*TODO*)]
-
-let pd_equ  = mk_decl PDpure [(*TODO*)]
-
-let pd_bool =
-  mk_decl (PDtype [mk_itd its_bool [] [rs_true; rs_false] []]) [(*TODO*)]
+open Theory
+
+(* We must keep the builtin modules in sync with the builtin theories.
+   Therefore we match the exact contents of th_decls, and crash if it
+   is not what we expect. *)
+
+let pd_int, pd_real, pd_equ = match builtin_theory.th_decls with
+  | [{td_node = Decl di}; {td_node = Decl dr}; {td_node = Decl de}] ->
+      mk_decl (PDtype [mk_itd its_int  [] [] []]) [di],
+      mk_decl (PDtype [mk_itd its_real [] [] []]) [dr],
+      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}] ->
+      mk_decl (PDtype [mk_itd its_func [] [] []]) [df],
+      mk_decl (PDtype [mk_itd its_pred [] [] []]) [dp],
+      mk_decl (PDlet ld_func_app) [da]
+  | _ -> assert false
+
+let pd_bool = match bool_theory.th_decls with
+  | [{td_node = Decl db}] ->
+      mk_decl (PDtype [mk_itd its_bool [] [rs_true; rs_false] []]) [db]
+  | _ -> assert false
 
 let pd_tuple _n = assert false (*TODO*)
 
-let pd_func_app = mk_decl (PDlet ld_func_app) [(*TODO*)]
-
 (** {2 Known identifiers} *)
 
 type known_map = pdecl Mid.t

src/mlw/pmodule.ml

@@ -12,6 +12,7 @@
 open Stdlib
 open Ident
 open Ty
+open Term
 open Theory
 open Ity
 open Expr
@@ -187,6 +188,9 @@ let use_export uc m =
   let th = Theory.use_export uc.muc_theory mth in
   add_to_module uc th m.mod_export
 
+let add_meta uc m al =
+  { uc with muc_theory = Theory.add_meta uc.muc_theory m al }
+
 let store_path, store_module, restore_path =
   let id_to_path = Wid.create 17 in
   let store_path uc path id =
@@ -216,53 +220,49 @@ let add_symbol add id v uc =
       muc_export = add true  id.id_string v e0 :: ste }
   | _ -> assert false
 
-let add_meta uc m al =
-  { uc with muc_theory = Theory.add_meta uc.muc_theory m al }
-
-let add_pdecl ~wp uc d =
+let add_pdecl uc d =
   let uc = { uc with
     muc_decls = d :: uc.muc_decls;
     muc_known = known_add_decl uc.muc_known d;
     muc_local = Sid.union uc.muc_local d.pd_news } in
-(* TODO
-  let uc = pdecl_ns uc d in
-  let uc = pdecl_vc ~wp uc d in
-*)
-  ignore wp; (* TODO *)
-  let th = List.fold_left Theory.add_decl uc.muc_theory d.pd_pure in
-  { uc with muc_theory = th }
+  let add_rs uc s = add_symbol add_ps s.rs_name (RS s) uc in
+  match d.pd_node with
+  | PDtype tdl ->
+      let add uc d =
+        let uc = List.fold_left add_rs uc d.itd_fields in
+        let uc = List.fold_left add_rs uc d.itd_constructors in
+        add_symbol add_ts d.itd_its.its_ts.ts_name d.itd_its uc in
+      List.fold_left add uc tdl
+  | PDlet (LDvar (v,_)) -> add_symbol add_ps v.pv_vs.vs_name (PV v) uc
+  | PDlet (LDsym (s,_)) -> add_rs uc s
+  | PDlet (LDrec l) -> List.fold_left (fun uc d -> add_rs uc d.rec_sym) uc l
+  | PDexn xs -> add_symbol add_ps xs.xs_name (XS xs) uc
+  | PDpure -> uc
 
 (** {2 Builtin symbols} *)
 
 let builtin_module =
-  let ns = empty_ns in
-  let ns = add_ts true its_int.its_ts.ts_name.id_string its_int ns in
-  let ns = add_ts true its_real.its_ts.ts_name.id_string its_real ns in
-  let kn = Mid.empty in
-  let kn = known_add_decl kn pd_int in
-  let kn = known_add_decl kn pd_real in
-  let kn = known_add_decl kn pd_equ in {
-    mod_theory = builtin_theory;
-    mod_decls  = [pd_int; pd_real; pd_equ];
-    mod_export = ns;
-    mod_known  = kn;
-    mod_local  = builtin_theory.th_local;
-    mod_used   = builtin_theory.th_used; }
+  let uc = empty_module None (id_fresh "BuiltIn") ["why3";"BuiltIn"] in
+  let uc = add_pdecl uc pd_int in
+  let uc = add_pdecl uc pd_real in
+  let uc = add_pdecl uc pd_equ in
+  let m = close_module uc in
+  { m with mod_theory = builtin_theory }
 
 let bool_module =
   let uc = empty_module None (id_fresh "Bool") ["why3";"Bool"] in
-  let uc = add_pdecl ~wp:false uc pd_bool in
-  let md = close_module uc in
-  { md with mod_theory = bool_theory }
+  let uc = add_pdecl uc pd_bool in
+  let m = close_module uc in
+  { m with mod_theory = bool_theory }
 
 let highord_module =
   let uc = empty_module None (id_fresh "HighOrd") ["why3";"HighOrd"] in
   let uc = use_export uc bool_module in
-  let uc = add_pdecl ~wp:false uc pd_func in
-  let uc = add_pdecl ~wp:false uc pd_pred in
-  let uc = add_pdecl ~wp:false uc pd_func_app in
-  let md = close_module uc in
-  { md with mod_theory = highord_theory }
+  let uc = add_pdecl uc pd_func in
+  let uc = add_pdecl uc pd_pred in
+  let uc = add_pdecl uc pd_func_app in
+  let m = close_module uc in
+  { m with mod_theory = highord_theory }
 
 let tuple_module _n = assert false (* TODO *)
 
@@ -272,13 +272,11 @@ let tuple_module_name s = Theory.tuple_theory_name s
 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 ~wp:false uc pd_unit in
-  let md = close_module uc in
-  { md with mod_theory = unit_theory }
+  let uc = add_pdecl uc pd_unit in
+  let m = close_module uc in
+  { m with mod_theory = unit_theory }
 *)
 
-let add_pdecl_with_tuples _uc _md = assert false (*TODO*)
-
 let create_module env ?(path=[]) n =
   let m = empty_module (Some env) n path in
   let m = use_export m builtin_module in
@@ -289,6 +287,14 @@ let create_module env ?(path=[]) n =
   let m = use_export m highord_module in
   m
 
+let add_pdecl ~wp uc d =
+  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 * theory Mstr.t