summaryrefslogtreecommitdiff
path: root/src/Print.ml
diff options
context:
space:
mode:
authorSon Ho2022-05-15 16:49:24 +0200
committerSon Ho2022-05-15 16:49:24 +0200
commitdbd5af0c6c56ad95eb3654c588fa227737c645ad (patch)
tree9adc1d08a88241af7b9d842d694d4485ddc70123 /src/Print.ml
parent3cd74ec699e8c7eb2089b57c0a6768717c65d285 (diff)
Add AggregatedOption
Diffstat (limited to 'src/Print.ml')
-rw-r--r--src/Print.ml12
1 files changed, 9 insertions, 3 deletions
diff --git a/src/Print.ml b/src/Print.ml
index 8df3001f..0c4ef20a 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -12,7 +12,6 @@ let option_to_string (to_string : 'a -> string) (x : 'a option) : string =
match x with Some x -> "Some (" ^ to_string x ^ ")" | None -> "None"
let name_to_string (name : name) : string = Names.name_to_string name
-
let fun_name_to_string (name : fun_name) : string = name_to_string name
(** Pretty-printing for types *)
@@ -48,9 +47,7 @@ module Types = struct
}
type stype_formatter = T.RegionVarId.id T.region type_formatter
-
type rtype_formatter = T.RegionId.id T.region type_formatter
-
type etype_formatter = T.erased_region type_formatter
let integer_type_to_string = function
@@ -906,6 +903,15 @@ module LlbcAst = struct
let ops = List.map (operand_to_string fmt) ops in
match akind with
| E.AggregatedTuple -> "(" ^ String.concat ", " ops ^ ")"
+ | E.AggregatedOption (variant_id, _ty) ->
+ if variant_id == T.option_none_id then (
+ assert (ops == []);
+ "@Option::None")
+ else if variant_id == T.option_some_id then (
+ assert (List.length ops == 1);
+ let op = List.hd ops in
+ "@Option::Some(" ^ op ^ ")")
+ else raise (Failure "Unreachable")
| E.AggregatedAdt (def_id, opt_variant_id, _regions, _types) ->
let adt_name = fmt.type_decl_id_to_string def_id in
let variant_name =