summaryrefslogtreecommitdiff
path: root/src/specialize.mli
diff options
context:
space:
mode:
authorJon French2019-03-04 14:23:55 +0000
committerJon French2019-03-04 14:23:55 +0000
commit94d40fb68bb3d36159a006b93909fc3841c92d28 (patch)
tree219c6d0ae7daf47cd6c8897895d182916e8f3815 /src/specialize.mli
parenta7a3402ce155f13234d2d3e5198e5dbf6e0e8b82 (diff)
parent9ed89583d52ccff151fb75424975f2ac4e627a1b (diff)
Merge branch 'sail2' into rmem_interpreter
Diffstat (limited to 'src/specialize.mli')
-rw-r--r--src/specialize.mli7
1 files changed, 6 insertions, 1 deletions
diff --git a/src/specialize.mli b/src/specialize.mli
index 93dec239..6ec8c2aa 100644
--- a/src/specialize.mli
+++ b/src/specialize.mli
@@ -62,12 +62,15 @@ val typ_ord_specialization : specialization
(** (experimental) specialise Int-kinded definitions *)
val int_specialization : specialization
+(** (experimental) specialise Int-kinded definitions, including externs *)
+val int_specialization_with_externs : specialization
+
(** Returns an IdSet with the function ids that have X-kinded
parameters, e.g. val f : forall ('a : X). 'a -> 'a. The first
argument specifies what X should be - it should be one of:
[is_int_kopt], [is_order_kopt], or [is_typ_kopt] from [Ast_util],
or some combination of those. *)
-val polymorphic_functions : (kinded_id -> bool) -> 'a defs -> IdSet.t
+val polymorphic_functions : specialization -> 'a defs -> IdSet.t
(** specialize returns an AST with all the Order and Type polymorphism
removed, as well as the environment produced by type checking that
@@ -76,6 +79,8 @@ val polymorphic_functions : (kinded_id -> bool) -> 'a defs -> IdSet.t
which case specialize returns the AST unmodified. *)
val specialize : specialization -> tannot defs -> Env.t -> tannot defs * Env.t
+(** specialize' n performs at most n specialization passes. Useful for
+ int_specialization which is not guaranteed to terminate. *)
val specialize' : int -> specialization -> tannot defs -> Env.t -> tannot defs * Env.t
(** return all instantiations of a function id, with the