Commit 4e0de3ee authored by Mário Pereira's avatar Mário Pereira

Extraction: new label [ocaml:remove]

New label can be used to avoid printing type definitions that are
only useful inside ghost, and so we do not want to get them in the
extracted code.

Labels [ocaml:named] and [ocaml:remove] moved into /src/mlw/ocaml_printer.ml
parent 7d82e6a1
......@@ -98,16 +98,6 @@ let get_model_trace_string ~labels =
| [_; t_str] -> t_str
| _ -> ""
(* functions for detecting optional and named arguments *)
let optional_arg = create_label "ocaml:optional"
let named_arg = create_label "ocaml:named"
let is_optional ~labels =
Slab.mem optional_arg labels
let is_named ~labels =
Slab.mem named_arg labels
(** Identifiers *)
type ident = {
......
......@@ -60,17 +60,6 @@ val get_model_trace_label : labels : Slab.t -> Slab.elt
(** Return a label of the form ["model_trace:*"].
Throws [Not_found] if there is no such label. *)
(* functions for detecting optional and named arguments *)
val optional_arg : label
val named_arg : label
val is_optional : labels:Slab.t -> bool
(** [is_optional sl] tests if the set [sl] contains [optional_arg]. *)
val is_named : labels:Slab.t -> bool
(** [is_named sl] tests if the set [sl] contains [named_arg]. *)
(** {2 Identifiers} *)
type ident = private {
......
......@@ -42,6 +42,20 @@ module Print = struct
open Mltree
open Compile.ML
(* extraction labels *)
let optional_arg = create_label "ocaml:optional"
let named_arg = create_label "ocaml:named"
let ocaml_remove = create_label "ocaml:remove"
let is_optional ~labels =
Slab.mem optional_arg labels
let is_named ~labels =
Slab.mem named_arg labels
let is_ocaml_remove ~labels =
Ident.Slab.mem ocaml_remove labels
let ocaml_keywords =
["and"; "as"; "assert"; "asr"; "begin";
"class"; "constraint"; "do"; "done"; "downto"; "else"; "end";
......@@ -263,7 +277,7 @@ module Print = struct
(* here [rs] refers to a [val] declaration *)
match query_syntax info.info_convert rs.rs_name,
query_syntax info.info_syn rs.rs_name with
| None, None when info.info_flat ->
| None, None (* when info.info_flat *) ->
(* FIXME? when extracting modularly, there are some functions we maybe do
not want to put in a drive, for instance mach.int.State63 *)
Loc.errorm ?loc "Function %a cannot be extracted" Expr.print_rs rs
......@@ -552,9 +566,11 @@ module Print = struct
| Some (Dalias ty) ->
fprintf fmt " =@ %a" (print_ty ~paren:false info) ty
in
fprintf fmt "@[<hov 2>%s %a%a%a@]"
(if fst then "type" else "and") print_tv_args its.its_args
(print_lident info) its.its_name print_def its.its_def
let labels = its.its_name.id_label in
if not (is_ocaml_remove ~labels) then
fprintf fmt "@[<hov 2>%s %a%a%a@]"
(if fst then "type" else "and") print_tv_args its.its_args
(print_lident info) its.its_name print_def its.its_def
let rec is_signature_decl info = function
| Dtype _ -> true
......
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