Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Declare implicit declarations in post-decode #3

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Declare implicit declarations in post-decode #3

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
21 changes: 12 additions & 9 deletions libASL/tcheck.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2102,6 +2102,16 @@ let addSetterFunction (env: GlobalEnv.t) (loc: AST.l) (qid: AST.ident) (tvs: Ide
(** {2 Typecheck instruction} *)
(****************************************************************)

let tc_body_with_implicits env b loc =
Env.nest_with_bindings (fun env' ->
let b' = List.map (tc_stmt env') b in
let imps = Env.getAllImplicits env in
List.iter (fun (v, ty) -> Env.addLocalVar env' loc v ty) imps;
let decls = declare_implicits loc imps in
if verbose && decls <> [] then Printf.printf "Implicit decls: %s %s" (pp_loc loc) (Utils.to_string (PP.pp_indented_block decls));
List.append decls b'
) env

(** Typecheck instruction encoding *)
let tc_encoding (env: Env.t) (x: encoding): (encoding * ((AST.ident * AST.ty) list)) =
(match x with
Expand All @@ -2112,14 +2122,7 @@ let tc_encoding (env: Env.t) (x: encoding): (encoding * ((AST.ident * AST.ty) li
) fields;
let guard' = check_expr env loc type_bool guard in
(* let (b', bs) = Env.nest_with_bindings (fun env' -> List.map (tc_stmt env') b) env in *)
let (b', bs) = Env.nest_with_bindings (fun env' ->
let b' = List.map (tc_stmt env') b in
let imps = Env.getAllImplicits env in
List.iter (fun (v, ty) -> Env.addLocalVar env' loc v ty) imps;
let decls = declare_implicits loc imps in
if verbose && decls <> [] then Printf.printf "Implicit decls: %s %s" (pp_loc loc) (Utils.to_string (PP.pp_indented_block decls));
List.append decls b'
) env in
let (b', bs) = tc_body_with_implicits env b loc in
(Encoding_Block (nm, iset, fields, opcode, guard', unpreds, b', loc), bs)
)

Expand Down Expand Up @@ -2371,7 +2374,7 @@ let tc_declaration (env: GlobalEnv.t) (d: AST.declaration): AST.declaration list

let (opost', pvs) = (match opost with
| Some b ->
let (b', vs) = Env.nest_with_bindings (fun env' -> List.map (tc_stmt env') b) locals in
let (b', vs) = tc_body_with_implicits locals b loc in
(Some b', vs)
| None ->
(None, []))
Expand Down