443 lines
23 KiB
OCaml
443 lines
23 KiB
OCaml
(** Resolved types: what [Ast.texpr] means once names are looked up.
|
|
|
|
The AST's type expressions are surface syntax — [Tname "Ptr"] and
|
|
[Tapp ("Option", ...)] are just names there. Here they are the real thing,
|
|
and two types are the same type exactly when they are structurally equal.
|
|
|
|
Milestone 2 has no generics, so there is no unification and no substitution:
|
|
a type variable is parsed, carried, and rejected the moment a value would
|
|
have to have it. That rejection lives in [Check]; this module only names
|
|
the shape. *)
|
|
|
|
(* Machine integer types. Signedness and width are both part of the type, and
|
|
two of them are the same type only when both halves match. A value may move
|
|
to a type that cannot lose it — see [widens_to] at the bottom of this file,
|
|
TODO.org, "Implicit numeric widening is legal; narrowing stays a hard error"
|
|
— and never the other way: narrowing is written or it does not happen. *)
|
|
type ikind = I8 | I16 | I32 | I64 | U8 | U16 | U32 | U64
|
|
|
|
type fkind = F32 | F64
|
|
|
|
(* Whether a slice may be stored through. [[const T]] is a view that can only
|
|
be read: [bytes-view] answers one, because its bytes are a string's and a
|
|
string literal's are in read-only memory. A [[T]] converts to a
|
|
[[const T]] implicitly and never back — see [const_widens] at the bottom of
|
|
this file — so every writable view is also a readable one, and a
|
|
read-only one cannot be laundered into a writable one. The const is
|
|
shallow: a [[const [u8]]] may not have its elements replaced, but each
|
|
element is a writable [[u8]] of its own. Both are the same two words at
|
|
run time; only the checker reads the flag. *)
|
|
type access = Mut | Const
|
|
|
|
type t =
|
|
| Int of ikind
|
|
| Float of fkind
|
|
| Bool
|
|
(* [char]: a Unicode scalar value, a u32 at run time and its own type here,
|
|
so a code point is never mistaken for a number. It compares, orders and
|
|
hashes; it does no arithmetic, and [i32 c] / [char n] convert. *)
|
|
| Char
|
|
| String
|
|
| Unit (* the zero-sized type, not C's void *)
|
|
| Never (* return, exit, error: no value at all *)
|
|
| Named of string (* a struct or data type, declared here *)
|
|
(* A C enum: an i32 at run time, but its own type, so a keyword at a call
|
|
site has something to resolve against and a plain integer does not fit. *)
|
|
| Enum of string
|
|
| Slice of access * t (* [T] [const T] ptr+len, non-owning *)
|
|
| Array of int64 * t (* [n T] inline, a value, copies *)
|
|
| Map of t * t (* (Map K V) *)
|
|
| Ptr of access * t (* (Ptr T) (Ptr const T) *)
|
|
(* [Allocator]: a builtin opaque type, the way [str] is a builtin
|
|
ptr+len. It is a [Types.t] case with no user-writable constructor, which
|
|
is what lets spec-memory.md's "procedure plus an opaque data pointer" be
|
|
expressed with none of milestone 5's function values — the procedure is a
|
|
C symbol the emitter names and no Flan type ever mentions it. At run time
|
|
it is two words: a pointer to the runtime's [flan_allocator], never a
|
|
copy of one — the capability set and the epoch have to be shared by every
|
|
container made from it — and the incarnation of it the value was made
|
|
for, which arena-destroy bumps so a stale value traps on use. *)
|
|
| Alloc
|
|
(* [(Vec T)]: ptr + len + cap + allocator, owning and move-only. One
|
|
type-erased runtime over (size, align) stands behind every instantiation,
|
|
so this is a container without generics — the concrete type is known only
|
|
at the call site, which is exactly where the two numbers are produced. *)
|
|
| Vec of t
|
|
| Option of t (* (Option T) *)
|
|
(* The two function types, and the difference between them is what a value
|
|
of each one *is* rather than what it may do.
|
|
|
|
[(Fn [T ...] R)] is a code address and the environment it is called
|
|
with: two words. It is the common case and keeps the short name, because
|
|
it is what almost every higher-order signature wants — a caller may pass
|
|
it a name, a non-capturing literal, or one that captured half the frame,
|
|
and the callee neither knows nor cares.
|
|
|
|
[(CFn [T ...] R)] is the bare address: one word, no environment, and
|
|
therefore nothing that can capture.
|
|
|
|
**The [C] is information, not decoration.** A value with no environment
|
|
is the only kind that could ever cross to C, and under the
|
|
[--no-conditions] direction TODO.org, "CFn and C's calling convention"
|
|
records — where a signature that cannot transfer drops the channel too —
|
|
one becomes literally a C
|
|
function pointer. The name points at what the type *is* and at where it
|
|
is going.
|
|
|
|
What it does **not** point at is a capability that exists now: a
|
|
[declare] cannot take a function type at all today, because a Flan
|
|
signature ends with the transfer channel and a C caller knows nothing
|
|
about one. Anyone reaching for [CFn] straight after writing a
|
|
[declare-c] is reaching too early, and [crossable] says so where they
|
|
will meet it.
|
|
|
|
The whole of the reason there are two: a uniform environment would tax
|
|
every function in every program for a feature most of them never use,
|
|
and the static side is not to pay for the dynamic side's existence. With
|
|
two types an ordinary [defn] keeps exactly the signature it always had.
|
|
|
|
**Nobody ever needs [CFn].** [Fn] accepts everything a [CFn] does, so
|
|
the narrow one is reached for on purpose, for one of four reasons:
|
|
handing a function to C (later, as above); a table of bare addresses;
|
|
forbidding capture at a boundary; and the one that is likeliest in
|
|
practice — a *named* function passed to an [Fn] parameter goes through
|
|
the widening thunk and pays an indirect hop per call, where a [CFn]
|
|
parameter is a direct call. [(map-in-place s double)] is the example.
|
|
|
|
One-way: a [CFn] value satisfies an [Fn] (paired with a null
|
|
environment), and an [Fn] does not satisfy a [CFn] — there is nowhere
|
|
for the environment to go. *)
|
|
| Fn of t list * t (* (Fn [T ...] R) *)
|
|
| CFn of t list * t (* (CFn [T ...] R) *)
|
|
| Var of string (* a type variable — milestone 5 *)
|
|
(* The two halves of a length parameter, and neither is the type of a value.
|
|
[Len] is a length standing where a generic struct's argument goes — the 8
|
|
in (Small 8 i32) — and what a length variable is bound to. [LArray] is a
|
|
fixed array whose length is a variable, [[$n $t]], and exists only in a
|
|
generic signature, as the pattern a call site binds [n] from. A generic
|
|
body is checked with its lengths at [Check.abstract_len], so neither ever
|
|
reaches a backend. *)
|
|
| Len of int64
|
|
| LArray of string * t
|
|
(* [dyn]: one machine word whose contents the runtime knows and this module
|
|
does not. It is a written type — [(defonce x dyn 5)] boxes the 5 — and it
|
|
is also what an unannotated [defn] parameter means, which is why it is a
|
|
case here and not a Named type the prelude declares: the checker has to
|
|
recognise it to choose the boxing and the dyn op lowering, and a name in a
|
|
table cannot be matched on.
|
|
|
|
Nothing about the representation is stated here on purpose. The word is
|
|
opaque to the compiler — runtime/flan_dyn.h owns which bits are a tag —
|
|
so that milestone 2 can change the encoding without touching Emit. *)
|
|
| Dyn
|
|
|
|
let signed = function
|
|
| I8 | I16 | I32 | I64 -> true
|
|
| U8 | U16 | U32 | U64 -> false
|
|
|
|
let bits = function
|
|
| I8 | U8 -> 8 | I16 | U16 -> 16 | I32 | U32 -> 32 | I64 | U64 -> 64
|
|
|
|
let bits_f = function F32 -> 32 | F64 -> 64
|
|
|
|
(* [int] and [float] are the two builtin aliases, and they are spelled here
|
|
rather than as prelude [defalias]es so that they are the machine type and
|
|
not a second name for it. The difference is visible at a cast: [Check]'s
|
|
[is_cast] asks these two functions whether a head names a primitive, and an
|
|
entry in the alias table is not consulted there — so a prelude alias would
|
|
give [(int x)] no reading while [(i32 x)] had one. Named here, every path
|
|
that already accepts [i32] accepts [int] without learning the word.
|
|
|
|
Only these two. The rest of the foreign spellings — [long], [double],
|
|
[uint], [string] — stay refusals that teach the Flan name; see
|
|
[Check.foreign_spelling] for why the line is drawn where it is.
|
|
|
|
The mapping is one-way on purpose: [ikind_name] and [fkind_name] below
|
|
still answer [i32] and [f32], so every message, every DWARF name and every
|
|
inspector line the user sees says the machine type, whichever spelling the
|
|
source used. *)
|
|
let ikind_of_name = function
|
|
| "i8" -> Some I8 | "i16" -> Some I16 | "i32" | "int" -> Some I32
|
|
| "i64" -> Some I64
|
|
| "u8" -> Some U8 | "u16" -> Some U16 | "u32" -> Some U32 | "u64" -> Some U64
|
|
| _ -> None
|
|
|
|
let fkind_of_name = function
|
|
| "f32" | "float" -> Some F32 | "f64" -> Some F64 | _ -> None
|
|
|
|
(* Every name the resolver accepts as a primitive type. The list exists so a
|
|
near-miss can be reported as the typo it is. [Unit] is on it because the
|
|
resolver still answers to that name -- [Cimport] builds [Tname "Unit"] for
|
|
C's void, and never goes through the parser -- but nobody writes it: unit
|
|
is spelled [()] in source, and [Parse.texpr] refuses the word.
|
|
|
|
[int] and [float] are on it for the same reason they are in the two
|
|
functions above: the places that ask this list — whether a [defonce]'s third
|
|
element is a type, whether [(vec-new int)] names an element type, whether a
|
|
[let] binding vector has an annotation wedged into it — must answer the
|
|
same for [int] as for [i32], or the alias is a type-position-only spelling
|
|
and the identity is a half one. *)
|
|
let primitive_names =
|
|
[ "i8"; "i16"; "i32"; "i64"; "u8"; "u16"; "u32"; "u64";
|
|
"f32"; "f64"; "bool"; "char"; "str"; "dyn"; "Unit"; "Never"; "Allocator";
|
|
"int"; "float" ]
|
|
|
|
let ikind_name k =
|
|
(if signed k then "i" else "u") ^ string_of_int (bits k)
|
|
|
|
let fkind_name = function F32 -> "f32" | F64 -> "f64"
|
|
|
|
(* Structural equality is the whole story for *identity*: no subtyping, no
|
|
variance, and nothing here bends to admit a conversion. Implicit widening
|
|
(below) is deliberately not expressed as a loosening of this function or of
|
|
[fits] — it is a separate predicate that every caller must pair with a
|
|
[Cast] on the value, so a node's type never lies about the bits it holds.
|
|
Written out rather than using [=] so that adding a case with a function or
|
|
a mutable field cannot silently break it. *)
|
|
let rec equal a b =
|
|
match a, b with
|
|
| Int x, Int y -> x = y
|
|
| Float x, Float y -> x = y
|
|
(* [Dyn] is equal to itself and to nothing else. Two dyn values may hold
|
|
different things at run time, which is the point of the type and is not
|
|
this function's question: this is identity of *static* types, and there is
|
|
one dyn type the way there is one string type. *)
|
|
| Bool, Bool | Char, Char | String, String | Unit, Unit | Never, Never | Dyn, Dyn -> true
|
|
| Named x, Named y | Enum x, Enum y -> String.equal x y
|
|
| Slice (a, x), Slice (b, y) -> a = b && equal x y
|
|
| Array (n, x), Array (m, y) -> Int64.equal n m && equal x y
|
|
| Map (k, v), Map (k', v') -> equal k k' && equal v v'
|
|
| Ptr (a, x), Ptr (b, y) -> a = b && equal x y
|
|
| Alloc, Alloc -> true
|
|
| Vec x, Vec y -> equal x y
|
|
| Option x, Option y -> equal x y
|
|
(* The two are *not* equal to each other, in either direction. One-way
|
|
coercion lives in [Check.expect], where it can build the value the
|
|
wider type needs; here there is only identity. *)
|
|
| Fn (ps, r), Fn (ps', r') | CFn (ps, r), CFn (ps', r') ->
|
|
List.length ps = List.length ps'
|
|
&& List.for_all2 equal ps ps'
|
|
&& equal r r'
|
|
| Var x, Var y -> String.equal x y
|
|
| Len x, Len y -> Int64.equal x y
|
|
| LArray (n, x), LArray (m, y) -> String.equal n m && equal x y
|
|
| _ -> false
|
|
|
|
(* How a generic struct's copy is spelled to a reader. The copy is an
|
|
ordinary struct under a symbol-safe key — [Small-8-i32] — and this is the
|
|
key's written form, [(Small 8 i32)], filled in as each copy is made. Global
|
|
rather than on a checker's env because every message that prints a type
|
|
comes through here with no env in hand. The key determines the spelling,
|
|
so an entry left from an earlier program in the same process is wrong only
|
|
for a struct that program's successor declares under a copy's key by hand,
|
|
and then only in how a message spells it. *)
|
|
let display : (string, string) Hashtbl.t = Hashtbl.create 16
|
|
|
|
(* The same copies as the template and its arguments, for [spell] to write
|
|
in either syntax. *)
|
|
let display_app : (string, string * t list) Hashtbl.t = Hashtbl.create 16
|
|
|
|
(* A struct's name as a printed value's head: its own name, or for a generic
|
|
struct's copy the template and its arguments, [Pair i32] — so a value
|
|
prints as [(Pair i32 {.a 1 .b 2})], the way its type is written. *)
|
|
let struct_head n =
|
|
match Hashtbl.find_opt display n with
|
|
| Some d when String.length d >= 2 && d.[0] = '(' ->
|
|
String.sub d 1 (String.length d - 2)
|
|
| _ -> n
|
|
|
|
(* A type as the code it is written in spells it: [(Fn [i32] bool)] in a
|
|
.flan file, [Fn(i32) -> bool] in a .fln one. Messages use it; a spelling
|
|
that is a key, a symbol or a runtime string stays [to_string]'s. *)
|
|
let rec spell ~indented t =
|
|
if not indented then to_string t
|
|
else
|
|
let sp = spell ~indented in
|
|
let call h args = h ^ "(" ^ String.concat ", " args ^ ")" in
|
|
match t with
|
|
| Named n ->
|
|
(match Hashtbl.find_opt display_app n with
|
|
| Some (g, args) -> call g (List.map sp args)
|
|
| None -> to_string t)
|
|
| Slice (Mut, t) -> "[" ^ sp t ^ "]"
|
|
| Slice (Const, t) -> "[const " ^ sp t ^ "]"
|
|
| Array (n, t) -> Printf.sprintf "[%Ld %s]" n (sp t)
|
|
| LArray (n, t) -> Printf.sprintf "[$%s %s]" n (sp t)
|
|
| Map (k, v) -> call "Map" [ sp k; sp v ]
|
|
| Ptr (Mut, t) -> call "Ptr" [ sp t ]
|
|
| Ptr (Const, t) -> call "Ptr" [ "const " ^ sp t ]
|
|
| Vec t -> call "Vec" [ sp t ]
|
|
| Option t -> call "Option" [ sp t ]
|
|
| Fn (ps, r) -> call "Fn" (List.map sp ps) ^ " -> " ^ sp r
|
|
| CFn (ps, r) -> call "CFn" (List.map sp ps) ^ " -> " ^ sp r
|
|
| _ -> to_string t
|
|
|
|
and to_string = function
|
|
| Int k -> ikind_name k
|
|
| Float k -> fkind_name k
|
|
| Bool -> "bool"
|
|
| Char -> "char"
|
|
| String -> "str"
|
|
| Unit -> "()"
|
|
| Never -> "Never"
|
|
| Named n -> (match Hashtbl.find_opt display n with Some d -> d | None -> n)
|
|
| Enum n -> n
|
|
| Slice (Mut, t) -> "[" ^ to_string t ^ "]"
|
|
| Slice (Const, t) -> "[const " ^ to_string t ^ "]"
|
|
| Array (n, t) -> Printf.sprintf "[%Ld %s]" n (to_string t)
|
|
| Map (k, v) -> Printf.sprintf "(Map %s %s)" (to_string k) (to_string v)
|
|
| Ptr (Mut, t) -> "(Ptr " ^ to_string t ^ ")"
|
|
| Ptr (Const, t) -> "(Ptr const " ^ to_string t ^ ")"
|
|
| Alloc -> "Allocator"
|
|
| Vec t -> "(Vec " ^ to_string t ^ ")"
|
|
| Option t -> "(Option " ^ to_string t ^ ")"
|
|
| Fn (ps, r) ->
|
|
Printf.sprintf "(Fn [%s] %s)"
|
|
(String.concat " " (List.map to_string ps)) (to_string r)
|
|
| CFn (ps, r) ->
|
|
Printf.sprintf "(CFn [%s] %s)"
|
|
(String.concat " " (List.map to_string ps)) (to_string r)
|
|
| Var n -> "$" ^ n
|
|
| Len n -> Int64.to_string n
|
|
| LArray (n, t) -> Printf.sprintf "[$%s %s]" n (to_string t)
|
|
| Dyn -> "dyn"
|
|
|
|
let is_numeric = function Int _ | Float _ -> true | _ -> false
|
|
|
|
(* Every integer kind, signed and unsigned, at every width — and nothing
|
|
else. This is [is-integer]'s question: the bound that admits a body written
|
|
with %, the bitwise operators or the shifts, and that keeps the same body
|
|
from ever being instantiated at a float, where those operations either do
|
|
not exist or mean something different. *)
|
|
let is_integer = function Int _ -> true | _ -> false
|
|
|
|
(* The key types the first Map implementation admits (spec-memory.md, "Maps —
|
|
first implementation"): integers, enums, strings, fixed arrays, and value
|
|
structs composed recursively from those. Equality and hashing for them are
|
|
compiler-provided structural operations, so this is the whole of what the
|
|
emitted hash and equality pair has to cover — there is no dispatch to design
|
|
and no type class anywhere.
|
|
|
|
A struct is [Named], and whether its fields qualify cannot be decided here:
|
|
this module has no field table. [Check] finishes the job by walking them,
|
|
which is also where it emits the pair. Everything this does say no to says
|
|
no for a reason that will not change with a milestone: a [Ptr] or a [Slice]
|
|
key would hash an address, and hashing an address is a different operation
|
|
from hashing what it points at. *)
|
|
let rec keyable = function
|
|
| Int _ | Enum _ | Bool | Char | String -> true
|
|
| Float _ -> false (* NaN /= NaN, and 0.0 and -0.0 differ bytewise *)
|
|
| Array (_, t) -> keyable t
|
|
| Named _ -> true (* [Check] decides, by walking the fields *)
|
|
| _ -> false
|
|
|
|
(* Ordering is defined on machine types and on nothing else — structs and
|
|
slices have no built-in [<], because an unconstrained type supports only
|
|
what every type supports (plan.org, Types). A string has no ordering
|
|
either: there is no true answer to whether one string is less than another
|
|
until the language picks a collation, and byte order is not it. *)
|
|
let is_comparable = function Enum _ | Char -> true | t -> is_numeric t
|
|
|
|
(* Equality admits one type ordering does not: a string, grown in by the M2
|
|
queue's item 5 — bytewise, by content and not by address, so two
|
|
separately built strings with the same bytes are equal. A bool is the
|
|
other: true and false are two values with no order between them. *)
|
|
let is_equatable = function String | Bool -> true | t -> is_comparable t
|
|
|
|
(* [Never] is the type of an expression that does not produce a value: return,
|
|
an early-returning `some`, exit. It fits anywhere, and that is the only
|
|
place anything resembling subtyping exists. *)
|
|
let fits ~expected ~actual =
|
|
match actual with Never -> true | _ -> equal expected actual
|
|
|
|
(* ── Implicit widening ───────────────────────────────────────────────
|
|
TODO.org, "Implicit numeric widening is legal; narrowing stays a hard
|
|
error".
|
|
Which numeric types a value may move to without the program saying so.
|
|
One rule decides every entry: the conversion is admitted exactly when no
|
|
value of the source type can come out the other side as a different number.
|
|
Narrowing is not on this list and never will be — [(u32 x)] is how an i64
|
|
becomes a u32, because that one can lose.
|
|
|
|
Read out of that rule:
|
|
|
|
- Same signedness, strictly wider: i8→i16→i32→i64, u8→u16→u32→u64.
|
|
- Unsigned into a strictly wider signed: u8→i16, u8/u16→i32, u8/u16/u32→i64.
|
|
Every u32 fits in an i64, so nothing is lost. The mirror never holds:
|
|
signed into unsigned drops the negatives, at any width.
|
|
- Equal width across signedness (i32→u32, u32→i32) is refused for the same
|
|
reason — one of the two halves of the range has nowhere to go.
|
|
- f32→f64.
|
|
- Integer into float only where the float's significand covers the integer
|
|
exactly: f64 has 53 bits, so i8/i16/i32/u8/u16/u32 reach it and i64/u64 do
|
|
not (2^53+1 is not an f64); f32 has 24, so only i8/i16/u8/u16 reach it.
|
|
Odin is looser here and lets any integer into any float. This is the
|
|
tighter rule on purpose: a program that wants the lossy one writes (f64 x)
|
|
and says so, and loosening later adds programs where tightening later
|
|
would break them.
|
|
|
|
Nothing else participates. [Bool] is not a number, an [Enum] is its own type
|
|
whose whole point is that a bare integer does not fit it, [Dyn] crosses by
|
|
boxing and unboxing rather than by this, and a container is invariant: a
|
|
[Vec i32] is not a [Vec i64] and a [[i32]] is not a [[i64]], because the
|
|
elements would each have to be rewritten and a slice does not own its
|
|
bytes. *)
|
|
let widens_to ~(from : t) ~(into : t) =
|
|
match from, into with
|
|
| Int a, Int b ->
|
|
if signed a = signed b then bits b > bits a
|
|
else (not (signed a)) && signed b && bits b > bits a
|
|
| Float F32, Float F64 -> true
|
|
| Int a, Float b -> bits a <= (match b with F64 -> 32 | F32 -> 16)
|
|
| _ -> false
|
|
|
|
(* The type a binary operator's two operands meet at: whichever of the pair the
|
|
other one widens into, and nothing otherwise. That is total and it is not a
|
|
real lattice — (i32, u32) has no answer here, and inventing i64 for it would
|
|
be picking a type neither operand was written at. Equal types answer
|
|
themselves, so a caller can use this without checking for that first. *)
|
|
let join a b =
|
|
if equal a b then Some a
|
|
else if widens_to ~from:a ~into:b then Some b
|
|
else if widens_to ~from:b ~into:a then Some a
|
|
else None
|
|
|
|
(* The one conversion between the two slice types, and it goes one way: a
|
|
[[T]] may be seen as a [[const T]], because a view that can only be read
|
|
asks less of its bytes than one that can be written. Under a const slice
|
|
the same holds one level down — [[[u8]]] reads as [[const [const u8]]] —
|
|
because nothing can be stored through the outer view to put a read-only
|
|
slice where the writable original expects a writable one. Under a writable
|
|
slice it does not: a [[[u8]]] seen as [[[const u8]]] could have a
|
|
read-only slice stored into it and read back out as a [[u8]]. Like
|
|
[widens_to] this is a predicate and not a loosening of [equal]; the
|
|
caller is [Check.expect], which retypes the value — the two words are the
|
|
same at run time. *)
|
|
let rec const_widens ~(from : t) ~(into : t) =
|
|
match from, into with
|
|
| Slice (_, a), Slice (Const, b) | Ptr (_, a), Ptr (Const, b) ->
|
|
equal a b || const_widens ~from:a ~into:b
|
|
| _ -> false
|
|
|
|
(* The one type two branches of an [if], or two arguments at one type
|
|
variable, meet at when they differ only in const: the read-only one,
|
|
whichever came first. *)
|
|
let const_join a b =
|
|
if equal a b then Some a
|
|
else if const_widens ~from:a ~into:b then Some b
|
|
else if const_widens ~from:b ~into:a then Some a
|
|
else None
|
|
|
|
(* A function of one signature standing where another is wanted, when the
|
|
two differ only in const. A parameter may be more permissive than asked —
|
|
a function that takes a [[const T]] only reads what it is handed, so a
|
|
caller handing it a [[T]] loses nothing — and a result may be less so: a
|
|
[[T]] returned where a [[const T]] is wanted is [const_widens]'s case. The
|
|
two words are the same either way, so [Check.expect] only retypes. *)
|
|
let fn_accepts ~(from : t list * t) ~(into : t list * t) =
|
|
let ps', r' = from and ps, r = into in
|
|
List.length ps = List.length ps'
|
|
&& List.for_all2
|
|
(fun p p' -> equal p p' || const_widens ~from:p ~into:p') ps ps'
|
|
&& (equal r r' || const_widens ~from:r' ~into:r)
|