program declarations in modules

src/whyml/mlw_decl.ml

@@ -26,7 +26,9 @@ open Decl
 open Mlw_ty
 open Mlw_expr
 
-type pconstructor = psymbol * psymbol option list
+type ps_ls = { ps: psymbol; ls: lsymbol }
+
+type pconstructor = ps_ls * ps_ls option list
 
 type ity_defn =
   | ITabstract
@@ -82,7 +84,7 @@ let create_ity_decl tdl =
   let syms = ref Sid.empty in
   let add s (its,_) = news_id s its.its_pure.ts_name in
   let news = ref (List.fold_left add Sid.empty tdl) in
-  let projections = Hvs.create 17 in (* vs -> psymbol *)
+  let projections = Hvs.create 17 in (* vs -> ps_ls *)
   let build_constructor its (id, al) =
     (* check well-formedness *)
     let tvs = List.fold_right Stv.add its.its_args Stv.empty in
@@ -110,6 +112,7 @@ let create_ity_decl tdl =
     let arrow (pv,_) c = create_cty (vty_arrow pv c) in
     let v = (List.fold_right arrow al c).c_vty in
     let ps = create_psymbol id Stv.empty Sreg.empty v in
+    let ps_ls = { ps = ps; ls = ls } in
     news := Sid.add ps.p_name !news;
     (* build the projections, if any *)
     let build_proj pv id =
@@ -120,16 +123,17 @@ let create_ity_decl tdl =
       let effect = option_fold add_read eff_empty pv.pv_mutable in
       let vty = vty_arrow result (create_cty ~post ~effect (vty_value pv)) in
       let ps = create_psymbol id Stv.empty Sreg.empty vty in
+      let ps_ls = { ps = ps; ls = ls } in
       news := Sid.add ps.p_name !news;
-      Hvs.add projections pv.pv_vs ps;
-      ps
+      Hvs.add projections pv.pv_vs ps_ls;
+      ps_ls
     in
     let build_proj pv =
       try Hvs.find projections pv.pv_vs with Not_found -> build_proj pv id in
     let build_proj (pv, pj) =
       syms := ity_s_fold syms_its syms_ts !syms pv.pv_ity;
       if pj then Some (build_proj pv) else None in
-    ps, List.map build_proj al
+    ps_ls, List.map build_proj al
   in
   let build_type (its, defn) = its, match defn with
     | PITabstract -> ITabstract
@@ -155,7 +159,7 @@ let merge_known kn1 kn2 =
   in
   Mid.union check_known kn1 kn2
 
-let known_add_decl kn0 decl =
+let known_add_decl lkn0 kn0 decl =
   let kn = Mid.map (const decl) decl.pd_news in
   let check id decl0 _ =
     if pd_equal decl0 decl
@@ -164,5 +168,6 @@ let known_add_decl kn0 decl =
   in
   let kn = Mid.union check kn0 kn in
   let unk = Mid.set_diff decl.pd_syms kn in
+  let unk = Mid.set_diff unk lkn0 in
   if Sid.is_empty unk then kn
   else raise (UnknownIdent (Sid.choose unk))

src/whyml/mlw_decl.mli

@@ -20,12 +20,15 @@
 open Why3
 open Ident
 open Ty
+open Term
 open Mlw_ty
 open Mlw_expr
 
 (** {2 Type declaration} *)
 
-type pconstructor = psymbol * psymbol option list
+type ps_ls = private { ps: psymbol; ls: lsymbol }
+
+type pconstructor = ps_ls * ps_ls option list
 
 type ity_defn =
   | ITabstract
@@ -62,5 +65,5 @@ val create_ity_decl : pre_ity_decl list -> pdecl
 type known_map = pdecl Mid.t
 
 val known_id : known_map -> ident -> unit
-val known_add_decl : known_map -> pdecl -> known_map
+val known_add_decl : Decl.known_map -> known_map -> pdecl -> known_map
 val merge_known: known_map -> known_map -> known_map

src/whyml/mlw_module.ml

@@ -202,10 +202,48 @@ let create_module ?(path=[]) n =
 
 (** Program decls *)
 
-(*
-val add_pdecl : module_uc -> pdecl -> module_uc
-val add_pdecl_with_tuples : module_uc -> pdecl -> module_uc
-*)
+let add_symbol add id v uc =
+  match uc.muc_import, uc.muc_export with
+  | i0 :: sti, e0 :: ste -> { uc with
+      muc_import = add false id.id_string v i0 :: sti;
+      muc_export = add true  id.id_string v e0 :: ste }
+  | _ -> assert false
+
+let add_type uc (its,def) =
+  let add_ps uc {ps=ps} = add_symbol add_ps ps.p_name ps uc in
+  let add_proj = option_fold add_ps in
+  let add_constr uc (ps,pjl) = List.fold_left add_proj (add_ps uc ps) pjl in
+  let uc = add_symbol add_it its.its_pure.ts_name its uc in
+  match def with
+    | ITabstract -> uc
+    | ITalgebraic lfs -> List.fold_left add_constr uc lfs
+
+let add_pdecl uc d =
+  let uc =  { uc with
+    muc_decls = d :: uc.muc_decls;
+    muc_known = known_add_decl (Theory.get_known uc.muc_theory) uc.muc_known d;
+    muc_local = Sid.union uc.muc_local d.pd_news }
+  in
+  match d.pd_node with
+  | PDtype dl ->
+      let uc = List.fold_left add_type uc dl in
+      let constructor (ps, _) = ps.ls in
+      let defn = function
+        | ITabstract -> Decl.Tabstract
+        | ITalgebraic cl -> Decl.Talgebraic (List.map constructor cl)
+      in
+      let dl = List.map (fun (its, d) -> its.its_pure, defn d) dl in
+      add_to_theory Theory.add_ty_decl uc dl
+
+let add_pdecl_with_tuples uc d =
+  let ids = Mid.set_diff d.pd_syms uc.muc_known in
+  let ids = Mid.set_diff ids (Theory.get_known uc.muc_theory) in
+  let add id s = match is_ts_tuple_id id with
+    | Some n -> Sint.add n s
+    | None -> s in
+  let ixs = Sid.fold add ids Sint.empty in
+  let add n uc = use_export_theory uc (tuple_theory n) in
+  add_pdecl (Sint.fold add ixs uc) d
 
 (** Clone *)
 

src/whyml/mlw_module.mli

@@ -89,8 +89,9 @@ val add_meta : module_uc -> meta -> meta_arg list -> module_uc
 
 (** Program decls *)
 
-(*
-val add_ty_pdecl : module_uc -> ty_pdecl list -> module_uc
 val add_pdecl : module_uc -> pdecl -> module_uc
 val add_pdecl_with_tuples : module_uc -> pdecl -> module_uc
+
+(*
+val add_ty_pdecl : module_uc -> ty_pdecl list -> module_uc
 *)