diff options
| author | Alasdair Armstrong | 2019-02-22 16:58:58 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-02-22 16:58:58 +0000 |
| commit | fc9e071bb633fd7c7241db79146934e4ab2b33b5 (patch) | |
| tree | 09348a1a3af899ef33630a74bd48ea8cee3e46e5 /src | |
| parent | a5bf7345a1d279d00f58820459ab4ea497749cc3 (diff) | |
Fix more bugs in int-specialization
Diffstat (limited to 'src')
| -rw-r--r-- | src/sail.ml | 1 | ||||
| -rw-r--r-- | src/specialize.ml | 12 |
2 files changed, 9 insertions, 4 deletions
diff --git a/src/sail.ml b/src/sail.ml index eaf96eb4..bd953992 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -407,6 +407,7 @@ let main() = then let ast_c = rewrite_ast_c type_envs ast in let ast_c, type_envs = Specialize.(specialize typ_ord_specialization ast_c type_envs) in + (* let ast_c, type_envs = Specialize.(specialize' 2 int_specialization ast_c type_envs) in *) (* let ast_c = Spec_analysis.top_sort_defs ast_c in *) Util.opt_warnings := true; C_backend.compile_ast (C_backend.initial_ctx type_envs) (!opt_includes_c) ast_c diff --git a/src/specialize.ml b/src/specialize.ml index f34dc85f..591a415a 100644 --- a/src/specialize.ml +++ b/src/specialize.ml @@ -380,10 +380,14 @@ let specialize_id_valspec spec instantiations id ast = let constraints = instantiate_constraints safe_instantiation constraints in let constraints = instantiate_constraints reverse constraints in let kopts = List.filter (fun kopt -> not (spec.is_polymorphic kopt)) kopts in - let typq = mk_typquant (List.map (mk_qi_id K_type) typ_frees - @ List.map (mk_qi_id K_int) int_frees - @ List.map mk_qi_kopt kopts - @ List.map mk_qi_nc constraints) in + let typq = + if List.length (typ_frees @ int_frees) = 0 && List.length kopts = 0 then + mk_typquant [] + else + mk_typquant (List.map (mk_qi_id K_type) typ_frees + @ List.map (mk_qi_id K_int) int_frees + @ List.map mk_qi_kopt kopts + @ List.map mk_qi_nc constraints) in let typschm = mk_typschm typq typ in let spec_id = id_of_instantiation id instantiation in |