97 lines
2.3 KiB
OCaml
97 lines
2.3 KiB
OCaml
(* This is an open-ended (non-recursive) version of the algebraic data type of
|
|
System F types. The ordinary, recursive version of this type is defined in
|
|
the module [F]. *)
|
|
|
|
type 'a structure =
|
|
| TyArrow of 'a * 'a
|
|
| TyProduct of 'a list
|
|
| TyConstr of Datatype.tyconstr_id * 'a list
|
|
|
|
(* -------------------------------------------------------------------------- *)
|
|
|
|
(* Traversals at arity 1. *)
|
|
|
|
(* We enforce the same traversal order for [iter], [fold], and [map].
|
|
In principle, this is not necessary. *)
|
|
|
|
let iter f t =
|
|
match t with
|
|
| TyArrow (t1, t2) ->
|
|
f t1; f t2
|
|
| TyProduct ts
|
|
| TyConstr (_, ts) ->
|
|
List.iter f ts
|
|
|
|
let fold f t accu =
|
|
match t with
|
|
| TyArrow (t1, t2) ->
|
|
let accu = f t1 accu in
|
|
let accu = f t2 accu in
|
|
accu
|
|
| TyProduct ts
|
|
| TyConstr (_, ts) ->
|
|
List.fold_left (fun accu t -> f t accu) accu ts
|
|
|
|
let map f t =
|
|
match t with
|
|
| TyArrow (t1, t2) ->
|
|
let t1 = f t1 in
|
|
let t2 = f t2 in
|
|
TyArrow (t1, t2)
|
|
| TyProduct ts ->
|
|
let ts = List.map f ts in
|
|
TyProduct ts
|
|
| TyConstr (tid, ts) ->
|
|
let ts = List.map f ts in
|
|
TyConstr (tid, ts)
|
|
|
|
(* -------------------------------------------------------------------------- *)
|
|
|
|
(* Traversals at arity 2. *)
|
|
|
|
exception Iter2
|
|
|
|
let list_iter2 f ts us =
|
|
if List.length ts <> List.length us then raise Iter2;
|
|
List.iter2 f ts us
|
|
|
|
let iter2 f t u =
|
|
match t, u with
|
|
| TyArrow (t1, t2), TyArrow (u1, u2) ->
|
|
f t1 u1;
|
|
f t2 u2
|
|
| TyProduct ts1, TyProduct ts2 ->
|
|
list_iter2 f ts1 ts2
|
|
| TyConstr (tid1, ts1), TyConstr (tid2, ts2) ->
|
|
if tid1 <> tid2 then raise Iter2;
|
|
list_iter2 f ts1 ts2
|
|
| TyArrow _, _
|
|
| TyProduct _, _
|
|
| TyConstr _, _ ->
|
|
raise Iter2
|
|
|
|
(* The function [conjunction] that is expected by the solver is essentially
|
|
[iter2], except it must return a structure, as opposed to a unit value. *)
|
|
|
|
exception InconsistentConjunction =
|
|
Iter2
|
|
|
|
let conjunction f t u =
|
|
iter2 f t u;
|
|
t
|
|
|
|
(* -------------------------------------------------------------------------- *)
|
|
|
|
(* Printing. *)
|
|
|
|
open PPrint
|
|
|
|
let pprint leaf s =
|
|
match s with
|
|
| TyArrow (t1, t2) ->
|
|
leaf t1 ^^ string " -> " ^^ leaf t2
|
|
| TyProduct ts ->
|
|
braces (separate_map (string " * ") leaf ts)
|
|
| TyConstr (Datatype.Type c, ts) ->
|
|
string c ^^ parens (separate_map (string ", ") leaf ts)
|