diff options
| author | Alasdair Armstrong | 2019-02-19 17:02:19 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-02-19 17:02:19 +0000 |
| commit | fc7d360e9442ab2e945e0d2da97faaf0eefec66f (patch) | |
| tree | a823d0c949dde68bdf117c836c3c2e28f9cf9088 /src/isail.ml | |
| parent | 3c967f9075d890b8ba0e3fa1fb990a41a36ddd80 (diff) | |
Refactor specialization
specialize functions now take a 'specialization' parameter that
specifies how they will specialize the AST. typ_ord_specialization
gives the previous behaviour, whereas int_specialization allows
specializing on Int-kinded arguments. Note that this can loop forever
unless the appropriate case splits are inserted beforehand, presumably
by monomorphisation.
rename is_nat_kopt -> is_int_kopt for consistency
Diffstat (limited to 'src/isail.ml')
| -rw-r--r-- | src/isail.ml | 6 |
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" -> |