diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast_util.ml | 1 | ||||
| -rw-r--r-- | src/ast_util.mli | 1 | ||||
| -rw-r--r-- | src/c_backend.ml | 6 | ||||
| -rw-r--r-- | src/initial_check.ml | 1 | ||||
| -rw-r--r-- | src/ocaml_backend.ml | 1 | ||||
| -rw-r--r-- | src/parser.mly | 3 | ||||
| -rw-r--r-- | src/type_check.ml | 13 |
7 files changed, 4 insertions, 22 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml index f872ac2f..cb500f08 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -286,7 +286,6 @@ let unit_typ = mk_id_typ (mk_id "unit") let bit_typ = mk_id_typ (mk_id "bit") let real_typ = mk_id_typ (mk_id "real") let app_typ id args = mk_typ (Typ_app (id, args)) -let ref_typ typ = mk_typ (Typ_app (mk_id "ref", [mk_typ_arg (Typ_arg_typ typ)])) let register_typ typ = mk_typ (Typ_app (mk_id "register", [mk_typ_arg (Typ_arg_typ typ)])) let atom_typ nexp = mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (Typ_arg_nexp (nexp_simp nexp))])) diff --git a/src/ast_util.mli b/src/ast_util.mli index 545e669d..affb857f 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -124,7 +124,6 @@ val range_typ : nexp -> nexp -> typ val bit_typ : typ val bool_typ : typ val app_typ : id -> typ_arg list -> typ -val ref_typ : typ -> typ val register_typ : typ -> typ val unit_typ : typ val string_typ : typ diff --git a/src/c_backend.ml b/src/c_backend.ml index 738f9748..265bb8d6 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -168,7 +168,7 @@ let rec ctyp_of_typ ctx typ = | Typ_id id when string_of_id id = "string" -> CT_string | Typ_id id when string_of_id id = "real" -> CT_real - | Typ_app (id, [Typ_arg_aux (Typ_arg_typ typ, _)]) when string_of_id id = "register" || string_of_id id = "ref" -> + | Typ_app (id, [Typ_arg_aux (Typ_arg_typ typ, _)]) when string_of_id id = "register" -> CT_ref (ctyp_of_typ ctx typ) | Typ_id id | Typ_app (id, _) when Bindings.mem id ctx.records -> CT_struct (id, Bindings.find id ctx.records |> Bindings.bindings) @@ -1534,8 +1534,6 @@ let rec compile_def ctx = function List.fold_left2 (fun ctx (id, _) (_, ctyp) -> { ctx with locals = Bindings.add id (Immutable, ctyp) ctx.locals }) ctx compiled_args compiled_args' in - if string_of_id id = "main" then c_verbosity := 1 else (); - (* Optimize and compile the expression *) let aexp = no_shadow (pat_ids pat) (anf exp) in c_debug (lazy (Pretty_print_sail.to_string (pp_aexp aexp))); @@ -1548,8 +1546,6 @@ let rec compile_def ctx = function compiled_args |> List.map snd |> combine_destructure_cleanup |> fix_destructure fundef_label in - c_verbosity := 0; - (* This better be true or something has gone badly wrong. *) let ret_ctyp = ctyp_of_typ ctx ret_typ in diff --git a/src/initial_check.ml b/src/initial_check.ml index bc0fe07a..2ab3cd98 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -1044,7 +1044,6 @@ let initial_kind_env = ("list", {k = K_Lam( [{k = K_Typ}], {k = K_Typ})}); ("reg", {k = K_Lam( [{k = K_Typ}], {k= K_Typ})}); ("register", {k = K_Lam( [{k = K_Typ}], {k= K_Typ})}); - ("ref", {k = K_Lam( [{k = K_Typ}], {k= K_Typ})}); ("range", {k = K_Lam( [ {k = K_Nat}; {k= K_Nat}], {k = K_Typ}) }); ("vector", {k = K_Lam( [{k = K_Nat}; {k= K_Ord} ; {k=K_Typ}], {k=K_Typ}) } ); ("atom", {k = K_Lam( [ {k=K_Nat} ], {k=K_Typ})}); diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index 236c4222..efbe63f3 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -131,7 +131,6 @@ let ocaml_typ_id ctx = function | id when Id.compare id (mk_id "real") = 0 -> string "Rational.t" | id when Id.compare id (mk_id "exception") = 0 -> string "exn" | id when Id.compare id (mk_id "register") = 0 -> string "ref" - | id when Id.compare id (mk_id "ref") = 0 -> string "ref" | id -> zencode ctx id let rec ocaml_typ ctx (Typ_aux (typ_aux, _)) = diff --git a/src/parser.mly b/src/parser.mly index 694a4669..4d2b6230 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -549,9 +549,6 @@ atomic_typ: | Register Lparen typ Rparen { let register_id = mk_id (Id "register") $startpos($1) $endpos($1) in mk_typ (ATyp_app (register_id, [$3])) $startpos $endpos } - | Ref Lparen typ Rparen - { let ref_id = mk_id (Id "ref") $startpos($1) $endpos($1) in - mk_typ (ATyp_app (ref_id, [$3])) $startpos $endpos } | Lparen typ Rparen { $2 } | Lparen typ Comma typ_list Rparen diff --git a/src/type_check.ml b/src/type_check.ml index e538bc36..84c21861 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -511,7 +511,6 @@ end = struct ("atom", [BK_int]); ("vector", [BK_int; BK_order; BK_type]); ("register", [BK_type]); - ("ref", [BK_type]); ("bit", []); ("unit", []); ("int", []); @@ -1143,8 +1142,7 @@ end = struct rewrap (Typ_fn (aux t1, aux t2, eff)) | Typ_tup ts -> rewrap (Typ_tup (List.map aux ts)) - | Typ_app (r, [Typ_arg_aux (Typ_arg_typ rtyp,_)]) - when string_of_id r = "register" || string_of_id r = "ref" -> + | Typ_app (r, [Typ_arg_aux (Typ_arg_typ rtyp,_)]) when string_of_id r = "register" -> aux rtyp | Typ_app (id, targs) -> rewrap (Typ_app (id, List.map aux_arg targs)) @@ -2788,7 +2786,7 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) end | _ -> typ_error l ("Mal-formed mapping " ^ string_of_id f) end - + | P_app (f, _) when (not (Env.is_union_constructor f env) && not (Env.is_mapping f env)) -> typ_error l (string_of_id f ^ " is not a union constructor or mapping in pattern " ^ string_of_pat pat) | P_as (pat, id) -> @@ -3011,12 +3009,10 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ = | LEXP_deref exp -> let inferred_exp = infer_exp env exp in begin match typ_of inferred_exp with - | Typ_aux (Typ_app (r, [Typ_arg_aux (Typ_arg_typ vtyp, _)]), _) when string_of_id r = "ref" -> - subtyp l env typ vtyp; annot_lexp (LEXP_deref inferred_exp) typ, env | Typ_aux (Typ_app (r, [Typ_arg_aux (Typ_arg_typ vtyp, _)]), _) when string_of_id r = "register" -> subtyp l env typ vtyp; annot_lexp_effect (LEXP_deref inferred_exp) typ (mk_effect [BE_wreg]), env | _ -> - typ_error l (string_of_typ typ ^ " must be a ref or register type in " ^ string_of_exp exp ^ ")") + typ_error l (string_of_typ typ ^ " must be a register type in " ^ string_of_exp exp ^ ")") end | LEXP_id v -> begin match Env.lookup_id ~raw:true v env with @@ -3309,9 +3305,6 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = let tpat, env = bind_pat_no_guard env pat ptyp in let inferred_exp = irule infer_exp env exp in annot_exp (E_let (LB_aux (LB_val (tpat, bind_exp), (let_loc, None)), inferred_exp)) (typ_of inferred_exp) - | E_ref id when Env.is_mutable id env -> - let (_, typ) = Bindings.find id (Env.get_locals env) in - annot_exp (E_ref id) (ref_typ typ) | E_ref id when Env.is_register id env -> let _, _, typ = Env.get_register id env in annot_exp (E_ref id) (register_typ typ) |