Skip to content

Commit 0f20f02

Browse files
AlasdairAlasdair
authored
Refactor short circuiting identifiers (#1439)
1 parent 24cecfa commit 0f20f02

23 files changed

Lines changed: 280 additions & 200 deletions

‎Makefile‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -15,8 +15,8 @@ libsail_coverage:
1515

1616
extraction:
1717
$(MAKE) -C src/lib/rocq
18-
cp src/lib/rocq/*.mli src/lib/extraction
19-
cp src/lib/rocq/*.ml src/lib/extraction
18+
mv src/lib/rocq/*.mli src/lib/extraction
19+
mv src/lib/rocq/*.ml src/lib/extraction
2020

2121
# Build binary tarball. The lib directory is very large and not needed
2222
# for running the compiler. TARBALL_EXTRA_BIN can be used to bundle z3.

‎src/lib/anf.ml‎

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -725,8 +725,7 @@ let rec anf (E_aux (e_aux, (l, tannot)) as exp) =
725725
let then_aexp = anf then_exp in
726726
let else_aexp = anf else_exp in
727727
wrap (mk_aexp (AE_if (cond_val, then_aexp, else_aexp, typ_of exp)))
728-
| E_app_infix (x, Id_aux (Id op, l), y) -> anf (E_aux (E_app (Id_aux (Operator op, l), [x; y]), (l, tannot)))
729-
| E_app_infix (x, Id_aux (Operator op, l), y) -> anf (E_aux (E_app (Id_aux (Id op, l), [x; y]), (l, tannot)))
728+
| E_app_infix (x, id, y) -> anf (E_aux (E_app (deinfix id, [x; y]), (l, tannot)))
730729
| E_vector exps ->
731730
let aexps = List.map anf exps in
732731
let avals = List.map to_aval aexps in
@@ -750,12 +749,12 @@ let rec anf (E_aux (e_aux, (l, tannot)) as exp) =
750749
let wrap = List.fold_left (fun f g x -> f (g x)) (fun x -> x) (List.map snd fexps) in
751750
let record = List.fold_left (fun r (id, aval) -> Bindings.add id aval r) Bindings.empty (List.map fst fexps) in
752751
exp_wrap (wrap (mk_aexp (AE_struct_update (aval, record, typ_of exp))))
753-
| E_app (id, [exp1; exp2]) when string_of_id id = "and_bool" ->
752+
| E_app (id, [exp1; exp2]) when is_and_bool id ->
754753
let aexp1 = anf exp1 in
755754
let aexp2 = anf exp2 in
756755
let aval1, wrap = to_aval aexp1 in
757756
wrap (mk_aexp (AE_short_circuit (SC_and, aval1, aexp2)))
758-
| E_app (id, [exp1; exp2]) when string_of_id id = "or_bool" ->
757+
| E_app (id, [exp1; exp2]) when is_or_bool id ->
759758
let aexp1 = anf exp1 in
760759
let aexp2 = anf exp2 in
761760
let aval1, wrap = to_aval aexp1 in

‎src/lib/ast_util.ml‎

Lines changed: 36 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -158,7 +158,11 @@ let is_order_inc = function Ord_aux (Ord_inc, _) -> true | Ord_aux (Ord_dec, _)
158158

159159
let is_order_dec o = not (is_order_inc o)
160160

161-
let string_of_id = function Id_aux (Id v, _) -> v | Id_aux (Operator v, _) -> "(operator " ^ v ^ ")"
161+
let string_of_id = function
162+
| Id_aux (And_bool, _) -> "and_bool"
163+
| Id_aux (Or_bool, _) -> "or_bool"
164+
| Id_aux (Id v, _) -> v
165+
| Id_aux (Operator v, _) -> "(operator " ^ v ^ ")"
162166

163167
let lvar_typ ?loc:(l = Parse_ast.Unknown) = function
164168
| Local (_, typ) -> typ
@@ -197,6 +201,13 @@ let rec is_gen_loc = function
197201
| Parse_ast.Hint (_, l1, l2) -> is_gen_loc l1 || is_gen_loc l2
198202
| Parse_ast.Range _ -> false
199203

204+
let mk_and_bool ?loc:(l = Parse_ast.Unknown) () = Id_aux (And_bool, l)
205+
let mk_or_bool ?loc:(l = Parse_ast.Unknown) () = Id_aux (Or_bool, l)
206+
207+
let is_and_bool = function Id_aux (And_bool, _) -> true | _ -> false
208+
209+
let is_or_bool = function Id_aux (Or_bool, _) -> true | _ -> false
210+
200211
let mk_id ?loc:(l = Parse_ast.Unknown) str = Id_aux (Id str, l)
201212

202213
let mk_nc ?loc:(l = Parse_ast.Unknown) nc_aux = NC_aux (nc_aux, l)
@@ -306,10 +317,16 @@ module Id = struct
306317
type t = id
307318
let compare id1 id2 =
308319
match (id1, id2) with
320+
| Id_aux (And_bool, _), Id_aux (And_bool, _) -> 0
321+
| Id_aux (Or_bool, _), Id_aux (Or_bool, _) -> 0
309322
| Id_aux (Id x, _), Id_aux (Id y, _) -> String.compare x y
310323
| Id_aux (Operator x, _), Id_aux (Operator y, _) -> String.compare x y
311-
| Id_aux (Id _, _), Id_aux (Operator _, _) -> -1
312-
| Id_aux (Operator _, _), Id_aux (Id _, _) -> 1
324+
| Id_aux (Id _, _), _ -> -1
325+
| _, Id_aux (Id _, _) -> 1
326+
| Id_aux (Operator _, _), _ -> -1
327+
| _, Id_aux (Operator _, _) -> 1
328+
| Id_aux (And_bool, _), _ -> -1
329+
| _, Id_aux (And_bool, _) -> 1
313330
end
314331

315332
let lex_ord f g x1 x2 y1 y2 = match f x1 x2 with 0 -> g y1 y2 | n -> n
@@ -1102,6 +1119,8 @@ type id_chunk = Id_chunk_int of int | Id_chunk_string of string
11021119
let split_id =
11031120
let open Ast in
11041121
function
1122+
| Id_aux (And_bool, _) -> [Id_chunk_string "and_bool"]
1123+
| Id_aux (Or_bool, _) -> [Id_chunk_string "or_bool"]
11051124
| Id_aux (Id id, _) ->
11061125
let pos = ref 0 in
11071126
let is_number = ref false in
@@ -1156,25 +1175,35 @@ let natural_sort_ids ids =
11561175
let ids = List.stable_sort (fun (n1, _) (n2, _) -> split_id_compare n1 n2) ids in
11571176
List.map snd ids
11581177

1159-
let deinfix = function Id_aux (Id v, l) -> Id_aux (Operator v, l) | Id_aux (Operator v, l) -> Id_aux (Operator v, l)
1178+
let deinfix = function Id_aux (Id v, l) -> Id_aux (Operator v, l) | id -> id
11601179

1161-
let infix_swap = function Id_aux (Id v, l) -> Id_aux (Operator v, l) | Id_aux (Operator v, l) -> Id_aux (Id v, l)
1180+
let infix_swap = function Id_aux (Operator v, l) -> Id_aux (Id v, l) | id -> deinfix id
11621181

11631182
let id_of_kid = function Kid_aux (Var v, l) -> Id_aux (Id (String.sub v 1 (String.length v - 1)), l)
11641183

1165-
let kid_of_id = function Id_aux (Id v, l) -> Kid_aux (Var ("'" ^ v), l) | Id_aux (Operator _, _) -> assert false
1184+
let kid_of_id = function Id_aux (Id v, l) -> Kid_aux (Var ("'" ^ v), l) | _ -> assert false
11661185

11671186
let prepend_id str = function
11681187
| Id_aux (Id v, l) -> Id_aux (Id (str ^ v), l)
11691188
| Id_aux (Operator v, l) -> Id_aux (Operator (str ^ v), l)
1189+
| Id_aux ((And_bool | Or_bool), l) ->
1190+
Reporting.unreachable l __POS__
1191+
"Attempted to construct prepended identifier from short-circuiting boolean operator"
11701192

11711193
let append_id id str =
1172-
match id with Id_aux (Id v, l) -> Id_aux (Id (v ^ str), l) | Id_aux (Operator v, l) -> Id_aux (Operator (v ^ str), l)
1194+
match id with
1195+
| Id_aux (Id v, l) -> Id_aux (Id (v ^ str), l)
1196+
| Id_aux (Operator v, l) -> Id_aux (Operator (v ^ str), l)
1197+
| Id_aux ((And_bool | Or_bool), l) ->
1198+
Reporting.unreachable l __POS__
1199+
"Attempted to construct appended identifier from short-circuiting boolean operator"
11731200

11741201
let remove_id_suffix id str =
11751202
match id with
11761203
| Id_aux (Id v, l) -> remove_suffix v str |> Option.map (fun s -> Id_aux (Id s, l))
11771204
| Id_aux (Operator v, l) -> remove_suffix v str |> Option.map (fun s -> Id_aux (Operator s, l))
1205+
| Id_aux ((And_bool | Or_bool), l) ->
1206+
Reporting.unreachable l __POS__ "Attempted to remove suffix from short-circuiting boolean operator"
11781207

11791208
let prepend_kid str = function
11801209
| Kid_aux (Var v, l) -> Kid_aux (Var ("'" ^ str ^ String.sub v 1 (String.length v - 1)), l)

‎src/lib/ast_util.mli‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -153,10 +153,15 @@ val lvar_typ : ?loc:l -> 'a lvar -> 'a
153153
val is_order_inc : order -> bool
154154
val is_order_dec : order -> bool
155155

156+
val is_and_bool : id -> bool
157+
val is_or_bool : id -> bool
158+
156159
(** {1 Functions for building and destructuring untyped AST elements} *)
157160

158161
(** {2 Functions for building untyped AST elements} *)
159162

163+
val mk_and_bool : ?loc:l -> unit -> id
164+
val mk_or_bool : ?loc:l -> unit -> id
160165
val mk_id : ?loc:l -> string -> id
161166
val mk_kid : ?loc:l -> string -> kid
162167
val mk_nc : ?loc:l -> n_constraint_aux -> n_constraint

‎src/lib/constant_fold.ml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -234,10 +234,10 @@ let rw_exp fixed target ok not_ok istate =
234234
| None -> E_aux (e_aux, annot)
235235
end
236236
(* Short-circuit boolean operators with constants *)
237-
| E_app (id, [(E_aux (E_lit (L_aux (L_false, _)), _) as false_exp); _]) when string_of_id id = "and_bool" ->
237+
| E_app (id, [(E_aux (E_lit (L_aux (L_false, _)), _) as false_exp); _]) when is_and_bool id ->
238238
ok ();
239239
false_exp
240-
| E_app (id, [(E_aux (E_lit (L_aux (L_true, _)), _) as true_exp); _]) when string_of_id id = "or_bool" ->
240+
| E_app (id, [(E_aux (E_lit (L_aux (L_true, _)), _) as true_exp); _]) when is_or_bool id ->
241241
ok ();
242242
true_exp
243243
| E_app (id, args) when List.for_all is_constant args ->

‎src/lib/extraction/Ast.ml‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -52,6 +52,8 @@ type kinded_id_aux =
5252
| KOpt_kind of kind * kid
5353

5454
type id_aux =
55+
| And_bool
56+
| Or_bool
5557
| Id of string
5658
| Operator of string
5759

‎src/lib/extraction/Ast.mli‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -52,6 +52,8 @@ type kinded_id_aux =
5252
| KOpt_kind of kind * kid
5353

5454
type id_aux =
55+
| And_bool
56+
| Or_bool
5557
| Id of string
5658
| Operator of string
5759

‎src/lib/extraction/Semantics.ml‎

Lines changed: 70 additions & 61 deletions
Original file line numberDiff line numberDiff line change
@@ -18,12 +18,13 @@ let id_eqb id1 id2 =
1818
let Id_aux (i2, _) = id2 in
1919
(match i2 with
2020
| Id s2 -> String.equal s1 s2
21-
| Operator _ -> false)
21+
| _ -> false)
2222
| Operator s1 ->
2323
let Id_aux (i2, _) = id2 in
2424
(match i2 with
25-
| Id _ -> false
26-
| Operator s2 -> String.equal s1 s2))
25+
| Operator s2 -> String.equal s1 s2
26+
| _ -> false)
27+
| _ -> false)
2728

2829
module IdMiniOrdered =
2930
struct
@@ -35,20 +36,30 @@ module IdMiniOrdered =
3536
let Id_aux (i, _) = x in
3637
let Id_aux (i0, _) = y in
3738
(match i with
39+
| And_bool ->
40+
(match i0 with
41+
| And_bool -> OrderedType.EQ
42+
| _ -> OrderedType.GT)
43+
| Or_bool ->
44+
(match i0 with
45+
| And_bool -> OrderedType.LT
46+
| Or_bool -> OrderedType.EQ
47+
| _ -> OrderedType.GT)
3848
| Id s ->
3949
(match i0 with
4050
| Id s0 ->
4151
if (fun s1 s2 -> String.compare s1 s2 < 0) s s0
4252
then OrderedType.LT
4353
else if String.equal s s0 then OrderedType.EQ else OrderedType.GT
44-
| Operator _ -> OrderedType.LT)
54+
| _ -> OrderedType.LT)
4555
| Operator s ->
4656
(match i0 with
4757
| Id _ -> OrderedType.GT
4858
| Operator s0 ->
4959
if (fun s1 s2 -> String.compare s1 s2 < 0) s s0
5060
then OrderedType.LT
51-
else if String.equal s s0 then OrderedType.EQ else OrderedType.GT))
61+
else if String.equal s s0 then OrderedType.EQ else OrderedType.GT
62+
| _ -> OrderedType.LT))
5263
end
5364

5465
module IdOrdered = OrderedType.MOT_to_OT(IdMiniOrdered)
@@ -375,10 +386,6 @@ module type SemanticExt =
375386

376387
val complete_value :
377388
((value * Nat_big_num.num) * Nat_big_num.num) list -> value
378-
379-
val is_and_bool : id -> bool
380-
381-
val is_or_bool : id -> bool
382389
end
383390

384391
module Make =
@@ -1204,58 +1211,60 @@ module Make =
12041211
wrap (E_internal_value v))
12051212
| E_typ (_, x) -> step0 x
12061213
| E_app (id0, args) ->
1207-
if T.is_or_bool id0
1208-
then (match args with
1209-
| [] -> Monad.Runtime_type_error (fst annot0)
1210-
| lhs :: l ->
1211-
(match l with
1212-
| [] -> Monad.Runtime_type_error (fst annot0)
1213-
| rhs :: l0 ->
1214-
(match l0 with
1215-
| [] ->
1216-
Monad.bind (get_bool lhs) (fun b ->
1217-
match b with
1218-
| Evaluated b0 ->
1219-
if b0
1220-
then wrap (E_internal_value (V_bool true))
1221-
else Monad.pure rhs
1222-
| Unevaluated ->
1223-
Monad.bind (step0 lhs) (fun lhs' ->
1224-
wrap (E_app (id0, (lhs' :: (rhs :: []))))))
1225-
| _ :: _ -> Monad.Runtime_type_error (fst annot0))))
1226-
else if T.is_and_bool id0
1227-
then (match args with
1228-
| [] -> Monad.Runtime_type_error (fst annot0)
1229-
| lhs :: l ->
1230-
(match l with
1231-
| [] -> Monad.Runtime_type_error (fst annot0)
1232-
| rhs :: l0 ->
1233-
(match l0 with
1234-
| [] ->
1235-
Monad.bind (get_bool lhs) (fun b ->
1236-
match b with
1237-
| Evaluated b0 ->
1238-
if b0
1239-
then Monad.pure rhs
1240-
else wrap (E_internal_value (V_bool false))
1241-
| Unevaluated ->
1242-
Monad.bind (step0 lhs) (fun lhs' ->
1243-
wrap (E_app (id0, (lhs' :: (rhs :: []))))))
1244-
| _ :: _ -> Monad.Runtime_type_error (fst annot0))))
1245-
else let filtered_var = left_to_right args in
1246-
let (evaluated0, unevaluated) = filtered_var in
1247-
(match unevaluated with
1248-
| [] ->
1249-
Monad.bind (Monad.Call (id0,
1250-
(all_evaluated evaluated0), Monad.pure)) (fun r ->
1251-
match r with
1252-
| Return_ok v -> wrap (E_internal_value v)
1253-
| Return_exception exn ->
1254-
wrap (E_throw (E_aux ((E_internal_value exn),
1255-
annot0))))
1256-
| u :: us ->
1257-
Monad.bind (step0 u) (fun u' ->
1258-
wrap (E_app (id0, (app evaluated0 (u' :: us))))))
1214+
let Id_aux (i, _) = id0 in
1215+
(match i with
1216+
| And_bool ->
1217+
(match args with
1218+
| [] -> Monad.Runtime_type_error (fst annot0)
1219+
| lhs :: l ->
1220+
(match l with
1221+
| [] -> Monad.Runtime_type_error (fst annot0)
1222+
| rhs :: l0 ->
1223+
(match l0 with
1224+
| [] ->
1225+
Monad.bind (get_bool lhs) (fun b ->
1226+
match b with
1227+
| Evaluated b0 ->
1228+
if b0
1229+
then Monad.pure rhs
1230+
else wrap (E_internal_value (V_bool false))
1231+
| Unevaluated ->
1232+
Monad.bind (step0 lhs) (fun lhs' ->
1233+
wrap (E_app (id0, (lhs' :: (rhs :: []))))))
1234+
| _ :: _ -> Monad.Runtime_type_error (fst annot0))))
1235+
| Or_bool ->
1236+
(match args with
1237+
| [] -> Monad.Runtime_type_error (fst annot0)
1238+
| lhs :: l ->
1239+
(match l with
1240+
| [] -> Monad.Runtime_type_error (fst annot0)
1241+
| rhs :: l0 ->
1242+
(match l0 with
1243+
| [] ->
1244+
Monad.bind (get_bool lhs) (fun b ->
1245+
match b with
1246+
| Evaluated b0 ->
1247+
if b0
1248+
then wrap (E_internal_value (V_bool true))
1249+
else Monad.pure rhs
1250+
| Unevaluated ->
1251+
Monad.bind (step0 lhs) (fun lhs' ->
1252+
wrap (E_app (id0, (lhs' :: (rhs :: []))))))
1253+
| _ :: _ -> Monad.Runtime_type_error (fst annot0))))
1254+
| _ ->
1255+
let filtered_var = left_to_right args in
1256+
let (evaluated0, unevaluated) = filtered_var in
1257+
(match unevaluated with
1258+
| [] ->
1259+
Monad.bind (Monad.Call (id0, (all_evaluated evaluated0),
1260+
Monad.pure)) (fun r ->
1261+
match r with
1262+
| Return_ok v -> wrap (E_internal_value v)
1263+
| Return_exception exn ->
1264+
wrap (E_throw (E_aux ((E_internal_value exn), annot0))))
1265+
| u :: us ->
1266+
Monad.bind (step0 u) (fun u' ->
1267+
wrap (E_app (id0, (app evaluated0 (u' :: us)))))))
12591268
| E_app_infix (lhs, id0, rhs) ->
12601269
let filtered_var = left_to_right2 lhs rhs in
12611270
(match filtered_var with

‎src/lib/extraction/Semantics.mli‎

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -273,10 +273,6 @@ module type SemanticExt =
273273

274274
val complete_value :
275275
((value * Nat_big_num.num) * Nat_big_num.num) list -> value
276-
277-
val is_and_bool : id -> bool
278-
279-
val is_or_bool : id -> bool
280276
end
281277

282278
module Make :

‎src/lib/initial_check.ml‎

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -211,7 +211,17 @@ let to_parse_kind = function
211211
let unaux_parse_kind (P.K_aux (aux, _)) = aux
212212

213213
let to_ast_id ctx (P.Id_aux (id, l)) =
214-
let to_ast_id' id = Id_aux ((match id with P.Id x -> Id x | P.Operator x -> Operator x), l) in
214+
let to_ast_id' id =
215+
Id_aux
216+
( ( match id with
217+
| P.Id "and_bool" -> And_bool
218+
| P.Id "or_bool" -> Or_bool
219+
| P.Id x -> Id x
220+
| P.Operator x -> Operator x
221+
),
222+
l
223+
)
224+
in
215225
if string_contains (string_of_parse_id_aux id) '#' then begin
216226
match Reporting.loc_file l with
217227
| Some file when !opt_magic_hash || StringSet.mem file ctx.internal_files -> to_ast_id' id

0 commit comments

Comments
 (0)