diff options
| author | Jon French | 2018-11-01 15:58:08 +0000 |
|---|---|---|
| committer | Jon French | 2018-11-01 15:58:08 +0000 |
| commit | 6bab4056ba7cd10e0dc633187b74b24a73bdd259 (patch) | |
| tree | 9d9b6fb1f26122b6fa1a1a86359737c928b9991b /src/initial_check.ml | |
| parent | d47313c00011be39ed1c2e411d401bb759ed65bf (diff) | |
| parent | 29f69b03602552d3ca1a29713527d21f5790e28a (diff) | |
Merge branch 'sail2' into rmem_interpreter
Diffstat (limited to 'src/initial_check.ml')
| -rw-r--r-- | src/initial_check.ml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml index 4e6e941d..36513ba1 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -370,6 +370,9 @@ and to_ast_nexp_constraint (k_env : kind Envmap.t) (c : Parse_ast.n_constraint) NC_or (to_ast_nexp_constraint k_env nc1, to_ast_nexp_constraint k_env nc2) | Parse_ast.NC_and (nc1, nc2) -> NC_and (to_ast_nexp_constraint k_env nc1, to_ast_nexp_constraint k_env nc2) + | Parse_ast.NC_app (id, typs) -> + let nexps = List.map (to_ast_nexp k_env) typs in + NC_app (to_ast_id id, nexps) | Parse_ast.NC_true -> NC_true | Parse_ast.NC_false -> NC_false ), l) @@ -907,6 +910,11 @@ let to_ast_def (names, k_env, def_ord) partial_defs def : def_progress envs_out | Parse_ast.DEF_reg_dec(dec) -> let d = to_ast_dec envs dec in ((Finished(DEF_reg_dec(d))),envs),partial_defs + | Parse_ast.DEF_constraint (id, kids, nc) -> + let id = to_ast_id id in + let kids = List.map to_ast_var kids in + let nc = to_ast_nexp_constraint k_env nc in + ((Finished (DEF_constraint (id, kids, nc))), envs), partial_defs | Parse_ast.DEF_pragma (_, _, l) -> typ_error l "Encountered preprocessor directive in initial check" None None None | Parse_ast.DEF_internal_mutrec _ -> |