fixes issue #46

both constructor and projection names are now added to the mod_known from
Mltree.pmodule, pointing to the type declarations in which they are introduced.

src/mlw/compile.ml

@@ -44,7 +44,13 @@ module ML = struct
   open Mltree
 
   let rec get_decl_name = function
-    | Dtype itdefl -> List.map (fun {its_name = id} -> id) itdefl
+    | Dtype itdefl ->
+        let add_id = function
+          | Some (Ddata l)   -> List.map (fun (idc,    _) -> idc) l
+          | Some (Drecord l) -> List.map (fun (_, idp, _) -> idp) l
+          | _ -> [] in
+        let add_td_ids {its_name = id; its_def = def} = id :: (add_id def) in
+        List.flatten (List.map add_td_ids itdefl)
     | Dlet (Lrec rdef) -> List.map (fun {rec_sym = rs} -> rs.rs_name) rdef
     | Dlet (Lvar ({pv_vs={vs_name=id}}, _))
     | Dlet (Lsym ({rs_name=id}, _, _, _))
@@ -602,13 +608,11 @@ module Translate = struct
       List.map (fun ({rs_cty = cty} as rs) ->
           rs.rs_name,
           let args = List.filter pv_not_ghost cty.cty_args in
-          List.map (fun {pv_vs = vs} -> type_ vs.vs_ty) args)
-    in
+          List.map (fun {pv_vs = vs} -> type_ vs.vs_ty) args) in
     let drecord_fields ({rs_cty = cty} as rs) =
       (List.exists (pv_equal (fd_of_rs rs)) s.its_mfields),
       rs.rs_name,
-      mlty_of_ity cty.cty_mask cty.cty_result
-    in
+      mlty_of_ity cty.cty_mask cty.cty_result in
     let id = s.its_ts.ts_name in
     let is_private = s.its_private in
     let args = s.its_ts.ts_args in
@@ -636,11 +640,10 @@ module Translate = struct
           assert (args = []); (* a range type is not polymorphic *)
           ML.mk_its_defn id [] is_private (Some (Mltree.Drange r))
       | Float ff, [], [] ->
-          assert (args = []); (* a range type is not polymorphic *)
+          assert (args = []); (* a float type is not polymorphic *)
           ML.mk_its_defn id [] is_private (Some (Mltree.Dfloat ff))
       | (Range _ | Float _), _, _ ->
           assert false (* cannot have constructors or fields *)
-
     end
 
   (* exception ExtractionVal of rsymbol *)

src/mlw/ocaml_printer.ml

@@ -649,7 +649,7 @@ module Print = struct
       if query_syntax info.info_syn id = None &&
          not (Hashtbl.mem memo decl) then begin
         Hashtbl.add memo decl (); print_decl info fmt decl;
-        fprintf fmt "@." end in
+        fprintf fmt "@\n@." end in
     List.iter decide_print decl_name
 
 end

src/tools/why3extract.ml

@@ -158,7 +158,7 @@ let print_mdecls ?fname m mdecls =
     print_preludes m.mod_theory.Theory.th_name fmt pm;
     let flat = opt_modu_flat = Flat in
     let pr_decl fmt d = fprintf fmt "%a" (pr pargs ?old ?fname ~flat m) d in
-    Pp.print_list Pp.newline pr_decl fmt mdecls;
+    Pp.print_list Pp.nothing pr_decl fmt mdecls;
     if cout <> stdout then close_out cout end
 
 let find_module_path mm path m = match path with
@@ -353,7 +353,7 @@ let () =
       let idl = match opt_rec_single with
         | Single -> List.filter is_local idl
         | Recursive -> idl in
-      Pp.print_list Pp.newline extract fmt idl;
+      Pp.print_list Pp.nothing extract fmt idl;
       if cout <> stdout then close_out cout
   with e when not (Debug.test_flag Debug.stack_trace) ->
     eprintf "%a@." Exn_printer.exn_printer e;