diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast_util.ml | 1 | ||||
| -rw-r--r-- | src/isail.ml | 4 | ||||
| -rw-r--r-- | src/ocaml_backend.ml | 8 | ||||
| -rw-r--r-- | src/pretty_print_sail.ml | 9 | ||||
| -rw-r--r-- | src/rewrites.ml | 13 | ||||
| -rw-r--r-- | src/sail.ml | 23 | ||||
| -rw-r--r-- | src/specialize.ml | 2 |
7 files changed, 39 insertions, 21 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml index 5746a242..11873690 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -1355,6 +1355,7 @@ and undefined_of_typ_args mwords l annot (A_aux (typ_arg_aux, _) as typ_arg) = match typ_arg_aux with | A_nexp n -> [E_aux (E_sizeof n, (l, annot (atom_typ n)))] | A_typ typ -> [undefined_of_typ mwords l annot typ] + | A_bool nc -> [E_aux (E_constraint nc, (l, annot (atom_bool_typ nc)))] | A_order _ -> [] let destruct_pexp (Pat_aux (pexp,ann)) = diff --git a/src/isail.ml b/src/isail.ml index 7d009791..4cfb2c6f 100644 --- a/src/isail.ml +++ b/src/isail.ml @@ -276,7 +276,7 @@ let load_session upto file = | Some upto_file when Filename.basename upto_file = file -> None | Some upto_file -> let (_, ast, env) = - load_files ~generate:false !Interactive.env [Filename.concat (Filename.dirname upto_file) file] + load_files ~check:true !Interactive.env [Filename.concat (Filename.dirname upto_file) file] in Interactive.ast := append_ast !Interactive.ast ast; Interactive.env := env; @@ -464,7 +464,7 @@ let handle_input' input = begin try load_into_session arg; - let (_, ast, env) = load_files !Interactive.env [arg] in + let (_, ast, env) = load_files ~check:true !Interactive.env [arg] in Interactive.ast := append_ast !Interactive.ast ast; interactive_state := initial_state !Interactive.ast Value.primops; Interactive.env := env; diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index d51aba75..05406413 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -710,13 +710,12 @@ let ocaml_pp_generators ctx defs orig_types required = and add_req_from_typarg required (A_aux (arg,_)) = match arg with | A_typ typ -> add_req_from_typ required typ - | A_nexp _ - | A_order _ - -> required + | A_nexp _ | A_order _ | A_bool _ -> required and add_req_from_td required (TD_aux (td,(l,_))) = match td with | TD_abbrev (_, _, A_aux (A_typ typ, _)) -> add_req_from_typ required typ + | TD_abbrev _ -> required | TD_record (_, _, fields, _) -> List.fold_left (fun req (typ,_) -> add_req_from_typ req typ) required fields | TD_variant (_, _, variants, _) -> @@ -787,7 +786,7 @@ let ocaml_pp_generators ctx defs orig_types required = | _ -> space ^^ separate space args_pp in string ("g.gen_" ^ typ_str) ^^ args_pp - and typearg (A_aux (arg,_)) = + and typearg (A_aux (arg,l)) = match arg with | A_nexp (Nexp_aux (nexp,l) as full_nexp) -> (match nexp with @@ -801,6 +800,7 @@ let ocaml_pp_generators ctx defs orig_types required = | Ord_inc -> string "true" | Ord_dec -> string "false") | A_typ typ -> parens (string "fun g -> " ^^ gen_type typ) + | A_bool nc -> raise (Reporting.err_todo l ("Unsupported constraint for generators: " ^ string_of_n_constraint nc)) in let make_subgen (Typ_aux (typ,l) as full_typ) = let typ_str, args_pp = diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index f30d5135..9a374275 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -619,8 +619,7 @@ let doc_typdef (TD_aux(td,_)) = match td with | TD_variant (id, TypQ_aux (TypQ_tq qs, _), unions, _) -> separate space [string "union"; doc_id id; doc_param_quants qs; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_union unions) rbrace] - | _ -> string "TYPEDEF" - + | TD_bitfield _ -> string "BITFIELD" (* should be rewritten *) let doc_spec ?comment:(comment=false) (VS_aux (v, annot)) = let doc_extern ext = @@ -656,6 +655,12 @@ let rec doc_scattered (SD_aux (sd_aux, _)) = string "scattered" ^^ space ^^ string "union" ^^ space ^^ doc_id id | SD_variant (id, TypQ_aux (TypQ_tq quants, _)) -> string "scattered" ^^ space ^^ string "union" ^^ space ^^ doc_id id ^^ doc_param_quants quants + | SD_mapcl (id, mapcl) -> + separate space [string "mapping clause"; doc_id id; equals; doc_mapcl mapcl] + | SD_mapping (id, Typ_annot_opt_aux (Typ_annot_opt_none, _)) -> + separate space [string "scattered mapping"; doc_id id] + | SD_mapping (id, Typ_annot_opt_aux (Typ_annot_opt_some (_, typ), _)) -> + separate space [string "scattered mapping"; doc_id id; string ":"; doc_typ typ] | SD_unioncl (id, tu) -> separate space [string "union clause"; doc_id id; equals; doc_union tu] diff --git a/src/rewrites.ml b/src/rewrites.ml index 5a70a721..31117f33 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -3525,7 +3525,11 @@ let rewrite_defs_mapping_patterns env = let mapping_in_typ = typ_of_annot p_annot in let x = Env.get_val_spec mapping_id env in - let (_, Typ_aux(Typ_bidir(typ1, typ2), _)) = x in + + let typ1, typ2 = match x with + | (_, Typ_aux(Typ_bidir(typ1, typ2), _)) -> typ1, typ2 + | (_, typ) -> raise (Reporting.err_unreachable (fst p_annot) __POS__ ("Must be bi-directional mapping: " ^ string_of_typ typ)) + in let mapping_direction = if mapping_in_typ = typ1 then @@ -4642,8 +4646,11 @@ let rec remove_clause_from_pattern ctx (P_aux (rm_pat,ann)) res_pat = rp' @ List.map (function [rp1;rp2] -> RP_cons (rp1,rp2) | _ -> assert false) res_pats end | P_record _ -> - raise (Reporting.err_unreachable (fst ann) __POS__ - "Record pattern not supported") + raise (Reporting.err_unreachable (fst ann) __POS__ "Record pattern not supported") + | P_or _ -> + raise (Reporting.err_unreachable (fst ann) __POS__ "Or pattern not supported") + | P_not _ -> + raise (Reporting.err_unreachable (fst ann) __POS__ "Negated pattern not supported") | P_vector _ | P_vector_concat _ | P_string_append _ -> diff --git a/src/sail.ml b/src/sail.ml index 06bd618e..28c5db0a 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -311,7 +311,7 @@ let _ = opt_file_arguments := (!opt_file_arguments) @ [s]) usage_msg -let load_files ?generate:(generate=true) type_envs files = +let load_files ?check:(check=false) type_envs files = if !opt_memo_z3 then Constraint.load_digests () else (); let t = Profile.start () in @@ -320,24 +320,27 @@ let load_files ?generate:(generate=true) type_envs files = List.fold_right (fun (_, Parse_ast.Defs ast_nodes) (Parse_ast.Defs later_nodes) -> Parse_ast.Defs (ast_nodes@later_nodes)) parsed (Parse_ast.Defs []) in let ast = Process_file.preprocess_ast options ast in - let ast = Initial_check.process_ast ~generate:generate ast in + let ast = Initial_check.process_ast ~generate:(not check) ast in Profile.finish "parsing" t; let t = Profile.start () in let (ast, type_envs) = check_ast type_envs ast in Profile.finish "type checking" t; - let ast = Scattered.descatter ast in - let ast = rewrite_ast type_envs ast in + if !opt_memo_z3 then Constraint.save_digests () else (); - let out_name = match !opt_file_out with - | None when parsed = [] -> "out.sail" - | None -> fst (List.hd parsed) - | Some f -> f ^ ".sail" in + if check then + ("out.sail", ast, type_envs) + else + let ast = Scattered.descatter ast in + let ast = rewrite_ast type_envs ast in - if !opt_memo_z3 then Constraint.save_digests () else (); + let out_name = match !opt_file_out with + | None when parsed = [] -> "out.sail" + | None -> fst (List.hd parsed) + | Some f -> f ^ ".sail" in - (out_name, ast, type_envs) + (out_name, ast, type_envs) let main() = if !opt_print_version then diff --git a/src/specialize.ml b/src/specialize.ml index 00357557..9f6af6d6 100644 --- a/src/specialize.ml +++ b/src/specialize.ml @@ -160,6 +160,8 @@ let string_of_instantiation instantiation = kid_name (mk_kopt K_int kid) ^ " in {" ^ Util.string_of_list ", " Big_int.to_string ns ^ "}" | NC_aux (NC_true, _) -> "true" | NC_aux (NC_false, _) -> "false" + | NC_aux (NC_var kid, _) -> kid_name (mk_kopt K_bool kid) + | NC_aux (NC_app (id, args), _) -> string_of_id id ^ "(" ^ Util.string_of_list ", " string_of_typ_arg args ^ ")" in let string_of_binding (kid, arg) = string_of_kid kid ^ " => " ^ string_of_typ_arg arg in |