diff options
| author | Alasdair Armstrong | 2017-10-23 18:31:05 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-10-23 18:31:05 +0100 |
| commit | 761c9bda82472b39d64416b6d4e25d21081fa261 (patch) | |
| tree | be6e0ff64a4a3a86e47704839cc5484a71c97d72 /src | |
| parent | a92a237fa23e6dd4b06f58615338a609c34d72be (diff) | |
Added effect set pretty printing for new parser
Also added some new utility functions in ast_util
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast_util.ml | 6 | ||||
| -rw-r--r-- | src/ast_util.mli | 6 | ||||
| -rw-r--r-- | src/pretty_print_sail2.ml | 5 |
3 files changed, 15 insertions, 2 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml index 99e19b04..71d783b9 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -576,6 +576,7 @@ module Id = struct | Id_aux (DeIid _, _), Id_aux (Id _, _) -> 1 end +module BESet = Set.Make(BE) module Bindings = Map.Make(Id) module IdSet = Set.Make(Id) module KBindings = Map.Make(Kid) @@ -708,4 +709,7 @@ let has_effect (Effect_aux (eff,_)) searched_for = match eff with List.exists (fun (BE_aux (be,_)) -> be = searched_for) effs | Effect_var _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown - "has_effect called on effect variable") + "has_effect called on effect variable") + +let effect_set (Effect_aux (eff,_)) = match eff with + | Effect_set effs -> BESet.of_list effs diff --git a/src/ast_util.mli b/src/ast_util.mli index 7ab7807a..189c272a 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -194,6 +194,10 @@ module IdSet : sig include Set.S with type elt = id end +module BESet : sig + include Set.S with type elt = base_effect +end + module KidSet : sig include Set.S with type elt = kid end @@ -225,3 +229,5 @@ val vector_typ_args_of : typ -> nexp * nexp * order * typ val is_order_inc : order -> bool val has_effect : effect -> base_effect_aux -> bool + +val effect_set : effect -> BESet.t diff --git a/src/pretty_print_sail2.ml b/src/pretty_print_sail2.ml index 3fa05132..5662fe1a 100644 --- a/src/pretty_print_sail2.ml +++ b/src/pretty_print_sail2.ml @@ -90,8 +90,11 @@ let rec doc_typ (Typ_aux (typ_aux, _)) = enclose (string "{|") (string "|}") (separate_map (string ", ") doc_int ints) | Typ_exist (kids, nc, typ) -> braces (separate_map space doc_kid kids ^^ comma ^^ space ^^ doc_nc nc ^^ dot ^^ space ^^ doc_typ typ) - | Typ_fn (typ1, typ2, eff) -> + | Typ_fn (typ1, typ2, Effect_aux (Effect_set [], _)) -> separate space [doc_typ typ1; string "->"; doc_typ typ2] + | Typ_fn (typ1, typ2, Effect_aux (Effect_set effs, _)) -> + let ocaml_eff = braces (separate (comma ^^ space) (List.map (fun be -> string (string_of_base_effect be)) effs)) in + separate space [doc_typ typ1; string "->"; doc_typ typ2; string "effect"; ocaml_eff] and doc_typ_arg (Typ_arg_aux (ta_aux, _)) = match ta_aux with | Typ_arg_typ typ -> doc_typ typ |