summaryrefslogtreecommitdiff
path: root/src/isail.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/isail.ml')
-rw-r--r--src/isail.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/isail.ml b/src/isail.ml
index 4cfb2c6f..252b21b8 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -358,7 +358,7 @@ let handle_input' input =
List.iter print_endline commands
| ":poly" ->
let is_kopt = match arg with
- | "Int" -> is_nat_kopt
+ | "Int" -> is_int_kopt
| "Type" -> is_typ_kopt
| "Order" -> is_order_kopt
| _ -> failwith "Invalid kind"
@@ -374,7 +374,7 @@ let handle_input' input =
| Arg.Bad message | Arg.Help message -> print_endline message
end;
| ":spec" ->
- let ast, env = Specialize.specialize !Interactive.ast !Interactive.env in
+ let ast, env = Specialize.(specialize int_specialization !Interactive.ast !Interactive.env) in
Interactive.ast := ast;
Interactive.env := env;
interactive_state := initial_state !Interactive.ast Value.primops
@@ -384,7 +384,7 @@ let handle_input' input =
let open PPrint in
let open C_backend in
let ast = Process_file.rewrite_ast_c !Interactive.env !Interactive.ast in
- let ast, env = Specialize.specialize ast !Interactive.env in
+ let ast, env = Specialize.(specialize typ_ord_specialization ast !Interactive.env) in
let ctx = initial_ctx env in
interactive_bytecode := bytecode_ast ctx (List.map flatten_cdef) ast
| ":ir" ->