diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Makefile | 1 | ||||
| -rw-r--r-- | src/_tags | 2 | ||||
| -rw-r--r-- | src/ast.sed | 2 | ||||
| -rw-r--r-- | src/ast_util.ml | 22 | ||||
| -rw-r--r-- | src/initial_check.ml | 12 | ||||
| -rw-r--r-- | src/interpreter.ml | 9 | ||||
| -rw-r--r-- | src/ocaml_backend.ml | 20 | ||||
| -rw-r--r-- | src/parser2.mly | 4 | ||||
| -rw-r--r-- | src/pretty_print_sail2.ml | 5 | ||||
| -rw-r--r-- | src/reporting_basic.ml | 6 | ||||
| -rw-r--r-- | src/type_check.ml | 142 | ||||
| -rw-r--r-- | src/type_check.mli | 3 | ||||
| -rw-r--r-- | src/value.ml | 15 |
13 files changed, 174 insertions, 69 deletions
diff --git a/src/Makefile b/src/Makefile index aa7c0f95..a39067b6 100644 --- a/src/Makefile +++ b/src/Makefile @@ -264,6 +264,7 @@ clean: -rm -rf lem lib -rm -rf sail.docdir -rm -f ast.ml + -rm -f ast.lem doc: ocamlbuild sail.docdir/index.html @@ -2,7 +2,7 @@ true: -traverse, debug, use_menhir <**/*.ml>: bin_annot, annot # <lem_interp> or <test>: include <sail.{byte,native}>: package(zarith), use_pprint, use_nums, use_unix, use_str, use_lem -<isail.{byte,native}>: package(linenoise), use_pprint, use_nums, use_unix, use_str, use_lem +<isail.{byte,native}>: package(zarith), package(linenoise), use_pprint, use_nums, use_unix, use_str, use_lem <isail.ml>: package(linenoise) <pprint> or <pprint/src>: include <*.m{l,li}>: use_lem diff --git a/src/ast.sed b/src/ast.sed new file mode 100644 index 00000000..39c58a50 --- /dev/null +++ b/src/ast.sed @@ -0,0 +1,2 @@ +s/type l = | Unknown/type l = Parse_ast.l/ +s/type value = | Val/open Value/ diff --git a/src/ast_util.ml b/src/ast_util.ml index 61b67c31..ec572bd4 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -142,6 +142,15 @@ module Nexp = struct | Nexp_id v1, Nexp_id v2 -> Id.compare v1 v2 | Nexp_var kid1, Nexp_var kid2 -> Kid.compare kid1 kid2 | Nexp_constant c1, Nexp_constant c2 -> Big_int.compare c1 c2 + | Nexp_app (op1, args1), Nexp_app (op2, args2) -> + let lex1 = Id.compare op1 op2 in + let lex2 = List.length args1 - List.length args2 in + let lex3 = + if lex2 = 0 then + List.fold_left2 (fun l n1 n2 -> if compare n1 n2 = 0 then 0 else compare n1 n2) 0 args1 args2 + else 0 + in + lex_ord (lex1, lex_ord (lex2, lex3)) | Nexp_times (n1a, n1b), Nexp_times (n2a, n2b) | Nexp_sum (n1a, n1b), Nexp_sum (n2a, n2b) | Nexp_minus (n1a, n1b), Nexp_minus (n2a, n2b) -> @@ -172,6 +181,7 @@ let rec is_nexp_constant (Nexp_aux (nexp, _)) = match nexp with | Nexp_times (n1, n2) | Nexp_sum (n1, n2) | Nexp_minus (n1, n2) -> is_nexp_constant n1 && is_nexp_constant n2 | Nexp_exp n | Nexp_neg n -> is_nexp_constant n + | Nexp_app (_, nexps) -> List.for_all is_nexp_constant nexps let rec nexp_simp (Nexp_aux (nexp, l)) = Nexp_aux (nexp_simp_aux nexp, l) and nexp_simp_aux = function @@ -365,6 +375,7 @@ and map_exp_annot_aux f = function | E_internal_exp_user (annot1, annot2) -> E_internal_exp_user (f annot1, f annot2) | E_comment str -> E_comment str | E_comment_struc exp -> E_comment_struc (map_exp_annot f exp) + | E_internal_value v -> E_internal_value v | E_internal_let (lexp, exp1, exp2) -> E_internal_let (map_lexp_annot f lexp, map_exp_annot f exp1, map_exp_annot f exp2) | E_internal_plet (pat, exp1, exp2) -> E_internal_plet (map_pat_annot f pat, map_exp_annot f exp1, map_exp_annot f exp2) | E_internal_return exp -> E_internal_return (map_exp_annot f exp) @@ -653,7 +664,6 @@ and string_of_lexp (LEXP_aux (lexp, _)) = string_of_lexp lexp ^ "[" ^ string_of_exp exp1 ^ ".." ^ string_of_exp exp2 ^ "]" | LEXP_field (lexp, id) -> string_of_lexp lexp ^ "." ^ string_of_id id | LEXP_memory (f, xs) -> string_of_id f ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")" - | _ -> "LEXP" and string_of_letbind (LB_aux (lb, l)) = match lb with | LB_val (pat, exp) -> string_of_pat pat ^ " = " ^ string_of_exp exp @@ -694,6 +704,7 @@ let rec nexp_frees (Nexp_aux (nexp, l)) = | Nexp_minus (n1, n2) -> KidSet.union (nexp_frees n1) (nexp_frees n2) | Nexp_exp n -> nexp_frees n | Nexp_neg n -> nexp_frees n + | Nexp_app (_, nexps) -> List.fold_left KidSet.union KidSet.empty (List.map nexp_frees nexps) let rec lexp_to_exp (LEXP_aux (lexp_aux, annot) as le) = let rewrap e_aux = E_aux (e_aux, annot) in @@ -783,13 +794,11 @@ let union_effects e1 e2 = | Effect_aux (Effect_set base_effs1, _), Effect_aux (Effect_set base_effs2, _) -> let base_effs3 = BESet.elements (BESet.of_list (base_effs1 @ base_effs2)) in Effect_aux (Effect_set base_effs3, Parse_ast.Unknown) - | _, _ -> assert false (* We don't do Effect variables *) let equal_effects e1 e2 = match e1, e2 with | Effect_aux (Effect_set base_effs1, _), Effect_aux (Effect_set base_effs2, _) -> BESet.compare (BESet.of_list base_effs1) (BESet.of_list base_effs2) = 0 - | _, _ -> assert false (* We don't do Effect variables *) let rec tyvars_of_nexp (Nexp_aux (nexp,_)) = match nexp with @@ -801,6 +810,7 @@ let rec tyvars_of_nexp (Nexp_aux (nexp,_)) = | Nexp_minus (n1,n2) -> KidSet.union (tyvars_of_nexp n1) (tyvars_of_nexp n2) | Nexp_exp n | Nexp_neg n -> tyvars_of_nexp n + | Nexp_app (_, nexps) -> List.fold_left KidSet.union KidSet.empty (List.map tyvars_of_nexp nexps) let rec tyvars_of_typ (Typ_aux (t,_)) = match t with @@ -835,7 +845,9 @@ let rec undefined_of_typ mwords l annot (Typ_aux (typ_aux, _) as typ) = wrap (E_sizeof i) typ | Typ_app (id, args) -> wrap (E_app (prepend_id "undefined_" id, - List.concat (List.map (undefined_of_typ_args mwords l annot) args))) typ + List.concat (List.map (undefined_of_typ_args mwords l annot) args))) typ + | Typ_tup typs -> + wrap (E_tuple (List.map (undefined_of_typ mwords l annot) typs)) typ | Typ_var kid -> (* Undefined monomorphism restriction in the type checker should guarantee that the typ_(kid) parameter was always one created @@ -843,7 +855,7 @@ let rec undefined_of_typ mwords l annot (Typ_aux (typ_aux, _) as typ) = initial_check.ml. i.e. the rewriter should only encounter this case when re-writing those functions. *) wrap (E_id (prepend_id "typ_" (id_of_kid kid))) typ - | Typ_fn _ -> assert false + | Typ_fn _ | Typ_exist _ -> assert false (* Typ_exist should be re-written *) and undefined_of_typ_args mwords l annot (Typ_arg_aux (typ_arg_aux, _) as typ_arg) = match typ_arg_aux with | Typ_arg_nexp n -> [E_aux (E_sizeof n, (l, annot (atom_typ n)))] diff --git a/src/initial_check.ml b/src/initial_check.ml index d5502d63..7ec0154e 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -131,7 +131,7 @@ let string_of_parse_id_aux = function | Parse_ast.DeIid v -> v let string_contains str char = - try (String.index str char; true) with + try (ignore (String.index str char); true) with | Not_found -> false let to_ast_id (Parse_ast.Id_aux(id, l)) = @@ -519,6 +519,7 @@ and to_ast_exp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l) | Parse_ast.E_throw exp -> E_throw (to_ast_exp k_env def_ord exp) | Parse_ast.E_return exp -> E_return(to_ast_exp k_env def_ord exp) | Parse_ast.E_assert(cond,msg) -> E_assert(to_ast_exp k_env def_ord cond, to_ast_exp k_env def_ord msg) + | _ -> raise (Reporting_basic.err_unreachable l "Unparsable construct in to_ast_exp") ), (l,())) and to_ast_lexp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) : unit lexp = @@ -747,7 +748,7 @@ let to_ast_fundef (names,k_env,def_ord) (Parse_ast.FD_aux(fd,l):Parse_ast.funde (*let _ = Printf.eprintf "to_ast_fundef\n" in*) let tannot_opt, k_env,_ = to_ast_tannot_opt k_env def_ord tannot_opt in FD_aux(FD_function(to_ast_rec rec_opt, tannot_opt, to_ast_effects_opt k_env effects_opt, List.map (to_ast_funcl (names, k_env, def_ord)) funcls), (l,())), (names,k_env,def_ord) - + type def_progress = No_def | Def_place_holder of id * Parse_ast.l @@ -823,6 +824,9 @@ 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_internal_mutrec _ -> + (* Should never occur because of remove_mutrec *) + typ_error Parse_ast.Unknown "Internal mutual block found when processing scattered defs" None None None | Parse_ast.DEF_scattered(Parse_ast.SD_aux(sd,l)) -> (match sd with | Parse_ast.SD_scattered_function(rec_opt, tannot_opt, effects_opt, id) -> @@ -887,8 +891,8 @@ let to_ast_def (names, k_env, def_ord) partial_defs def : def_progress envs_out ((Finished def), envs),partial_defs | _, true -> typ_error l "Scattered definition ended multiple times" (Some id) None None - | _ -> raise (Reporting_basic.err_unreachable l "Something in partial_defs other than fundef and type")))) - + | _ -> raise (Reporting_basic.err_unreachable l "Something in partial_defs other than fundef and type")))) + let rec to_ast_defs_helper envs partial_defs = function | [] -> ([],envs,partial_defs) | d::ds -> let ((d', envs), partial_defs) = to_ast_def envs partial_defs d in diff --git a/src/interpreter.ml b/src/interpreter.ml index 1a6e6393..3356b9dc 100644 --- a/src/interpreter.ml +++ b/src/interpreter.ml @@ -63,6 +63,7 @@ let value_of_lit (L_aux (l_aux, _)) = | L_true -> V_bool true | L_false -> V_bool false | L_string str -> V_string str + | _ -> failwith "Unimplemented value_of_lit" (* TODO *) let is_value = function | (E_aux (E_internal_value _, _)) -> true @@ -77,7 +78,9 @@ let is_false = function | _ -> false let exp_of_value v = (E_aux (E_internal_value v, (Parse_ast.Unknown, None))) -let value_of_exp (E_aux (E_internal_value v, _)) = v +let value_of_exp = function + | (E_aux (E_internal_value v, _)) -> v + | _ -> failwith "value_of_exp coerction failed" (**************************************************************************) (* 1. Interpreter Monad *) @@ -155,6 +158,7 @@ let rec subst id value (E_aux (e_aux, annot) as exp) = | E_id id' -> if Id.compare id id' = 0 then unaux_exp (exp_of_value value) else E_id id' | E_cast (typ, exp) -> E_cast (typ, subst id value exp) | E_app (fn, exps) -> E_app (fn, List.map (subst id value) exps) + | _ -> assert false (* TODO *) in wrap e_aux @@ -245,6 +249,8 @@ let rec step (E_aux (e_aux, annot)) = | E_sizeof _ | E_constraint _ -> assert false (* Must be re-written before interpreting *) + | _ -> assert false (* TODO *) + and combine _ v1 v2 = match (v1, v2) with | None, None -> None @@ -262,6 +268,7 @@ and pattern_match (P_aux (p_aux, _) as pat) value = matched, Bindings.add id value bindings | P_typ (_, pat) -> pattern_match pat value | P_id id -> true, Bindings.singleton id value + | P_var (pat, _) -> pattern_match pat value | P_app (id, pats) -> let (ctor, vals) = coerce_ctor value in if Id.compare id (mk_id ctor) = 0 then diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index aed736a7..b1a19482 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -181,7 +181,7 @@ let ocaml_lit (L_aux (lit_aux, _)) = | L_one -> string "B1" | L_true -> string "true" | L_false -> string "false" - | L_num n -> parens (string "Big_int.of_string" ^^ space ^^ string ("\"" ^ Big_int.to_string n ^ "\"")) + | L_num n -> parens (string "big_int_of_string" ^^ space ^^ string ("\"" ^ Big_int.to_string n ^ "\"")) | L_undef -> failwith "undefined should have been re-written prior to ocaml backend" | L_string str -> string_lit str | L_real str -> parens (string "real_of_string" ^^ space ^^ dquotes (string (String.escaped str))) @@ -285,11 +285,13 @@ let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) = match ord with | Ord_aux (Ord_inc, _) -> string "Big_int.add" ^^ space ^^ zencode ctx id ^^ space ^^ ocaml_atomic_exp ctx exp_step | Ord_aux (Ord_dec, _) -> string "Big_int.sub" ^^ space ^^ zencode ctx id ^^ space ^^ ocaml_atomic_exp ctx exp_step + | Ord_aux (Ord_var _, _) -> failwith "Cannot have variable loop order!" in let loop_compare = match ord with | Ord_aux (Ord_inc, _) -> string "Big_int.less_equal" | Ord_aux (Ord_dec, _) -> string "Big_int.greater" + | Ord_aux (Ord_var _, _) -> failwith "Cannot have variable loop order!" in let loop_body = separate space [string "if"; loop_compare; zencode ctx id; ocaml_atomic_exp ctx exp_to] @@ -442,7 +444,11 @@ let ocaml_funcls ctx = function | [] -> failwith "Ocaml: empty function" | [FCL_aux (FCL_Funcl (id, pexp),_)] -> - let Typ_aux (Typ_fn (typ1, typ2, _), _) = Bindings.find id ctx.val_specs in + let typ1, typ2 = + match Bindings.find id ctx.val_specs with + | Typ_aux (Typ_fn (typ1, typ2, _), _) -> (typ1, typ2) + | _ -> failwith "Found val spec which was not a function!" + in let pat_sym = gensym () in let pat, exp = match pexp with @@ -466,7 +472,11 @@ let ocaml_funcls ctx = ocaml_funcl call string_of_arg string_of_ret | funcls -> let id = funcls_id funcls in - let Typ_aux (Typ_fn (typ1, typ2, _), _) = Bindings.find id ctx.val_specs in + let typ1, typ2 = + match Bindings.find id ctx.val_specs with + | Typ_aux (Typ_fn (typ1, typ2, _), _) -> (typ1, typ2) + | _ -> failwith "Found val spec which was not a function!" + in let pat_sym = gensym () in let call_header = function_header () in let arg_sym, string_of_arg, ret_sym, string_of_ret = trace_info typ1 typ2 in @@ -599,7 +609,7 @@ let val_spec_typs (Defs defs) = | _ :: defs -> vs_typs defs | [] -> [] in - vs_typs defs; + ignore (vs_typs defs); !typs let ocaml_defs (Defs defs) = @@ -616,7 +626,7 @@ let ocaml_defs (Defs defs) = else empty in (string "open Sail_lib;;" ^^ hardline) - ^^ (string "module Big_int = Nat_big_num" ^^ ocaml_def_end) + ^^ (string "open Big_int" ^^ ocaml_def_end) ^^ concat (List.map (ocaml_def ctx) defs) ^^ empty_reg_init diff --git a/src/parser2.mly b/src/parser2.mly index 6021596f..140f1b86 100644 --- a/src/parser2.mly +++ b/src/parser2.mly @@ -75,7 +75,9 @@ let mk_kid str n m = Kid_aux (Var str, loc n m) let id_of_kid = function | Kid_aux (Var v, l) -> Id_aux (Id (String.sub v 1 (String.length v - 1)), l) -let deinfix (Id_aux (Id v, l)) = Id_aux (DeIid v, l) +let deinfix = function + | (Id_aux (Id v, l)) -> Id_aux (DeIid v, l) + | (Id_aux (DeIid v, l)) -> Id_aux (Id v, l) let mk_effect e n m = BE_aux (e, loc n m) let mk_typ t n m = ATyp_aux (t, loc n m) diff --git a/src/pretty_print_sail2.ml b/src/pretty_print_sail2.ml index 33743188..71fcd587 100644 --- a/src/pretty_print_sail2.ml +++ b/src/pretty_print_sail2.ml @@ -157,7 +157,7 @@ let doc_quants quants = | QI_id (KOpt_aux (KOpt_none kid, _)) -> [doc_kid kid] | QI_id kopt when is_nat_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Int"])] | QI_id kopt when is_typ_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Type"])] - | QI_id kopt when is_order_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Order"])] + | QI_id kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Order"])] | QI_const nc -> [] in let qi_nc (QI_aux (qi_aux, _)) = @@ -209,7 +209,6 @@ let rec doc_pat (P_aux (p_aux, _) as pat) = match p_aux with | P_id id -> doc_id id | P_tup pats -> lparen ^^ separate_map (comma ^^ space) doc_pat pats ^^ rparen - | P_app (id, pats) -> doc_id id ^^ lparen ^^ separate_map (comma ^^ space) doc_pat pats ^^ rparen | P_typ (typ, pat) -> separate space [doc_pat pat; colon; doc_typ typ] | P_lit lit -> doc_lit lit (* P_var short form sugar *) @@ -346,6 +345,7 @@ and doc_infix n (E_aux (e_aux, _) as exp) = | (InfixL, m) when m < n -> parens (separate space [doc_infix m l; doc_id op; doc_infix (m + 1) r]) | (InfixR, m) when m >= n -> separate space [doc_infix (m + 1) l; doc_id op; doc_infix m r] | (InfixR, m) when m < n -> parens (separate space [doc_infix (m + 1) l; doc_id op; doc_infix m r]) + | _ -> assert false with | Not_found -> separate space [doc_atomic_exp l; doc_id op; doc_atomic_exp r] @@ -510,7 +510,6 @@ let rec doc_def def = group (match def with | DEF_type t_def -> doc_typdef t_def | DEF_kind k_def -> doc_kind_def k_def | DEF_fundef f_def -> doc_fundef f_def - | DEF_internal_mutrec f_defs -> separate_map hardline doc_fundef f_defs | DEF_val lbind -> string "let" ^^ space ^^ doc_letbind lbind | DEF_internal_mutrec fundefs -> (string "mutual {" ^//^ separate_map (hardline ^^ hardline) doc_fundef fundefs) diff --git a/src/reporting_basic.ml b/src/reporting_basic.ml index 166e0517..af1f85d0 100644 --- a/src/reporting_basic.ml +++ b/src/reporting_basic.ml @@ -97,7 +97,7 @@ let rec skip_lines in_chan = function | n when n <= 0 -> () - | n -> input_line in_chan; skip_lines in_chan (n - 1) + | n -> ignore (input_line in_chan); skip_lines in_chan (n - 1) let rec read_lines in_chan = function | n when n <= 0 -> [] @@ -186,9 +186,9 @@ let read_from_file_pos2 p1 p2 = let ic = open_in p1.Lexing.pos_fname in let _ = seek_in ic s in let l = (e - s) in - let buf = String.create l in + let buf = Bytes.create l in let _ = input ic buf 0 l in - let _ = match multi with None -> () | Some sk -> String.fill buf 0 sk ' ' in + let _ = match multi with None -> () | Some sk -> Bytes.fill buf 0 sk ' ' in let _ = close_in ic in (buf, not (multi = None)) diff --git a/src/type_check.ml b/src/type_check.ml index ac5f19f8..c1390e84 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -106,6 +106,9 @@ let pp_type_error err = ^//^ string (string_of_list ", " string_of_n_constraint constrs) | Err_no_num_ident id -> string "No num identifier" ^^ space ^^ string (string_of_id id) + | Err_unresolved_quants (id, quants) -> + string "Could not resolve quantifiers for" ^^ space ^^ string (string_of_id id) + ^//^ group (separate_map hardline (fun quant -> string (string_of_quant_item quant)) quants) | Err_other str -> string str in pp_err err @@ -293,7 +296,8 @@ module Env : sig val is_union_constructor : id -> t -> bool val add_record : id -> typquant -> (typ * id) list -> t -> t val is_record : id -> t -> bool - val get_accessor : id -> id -> t -> typquant * typ + val get_accessor_fn : id -> id -> t -> typquant * typ + val get_accessor : id -> id -> t -> typquant * typ * typ * effect val add_local : id -> mut * typ -> t -> t val get_locals : t -> (mut * typ) Bindings.t val add_variant : id -> typquant * type_union list -> t -> t @@ -685,12 +689,18 @@ end = struct accessors = List.fold_left fold_accessors env.accessors fields } end - let get_accessor rec_id id env = + let get_accessor_fn rec_id id env = let freshen_bind bind = List.fold_left (fun bind (kid, _) -> freshen_kid env kid bind) bind (KBindings.bindings env.typ_vars) in try freshen_bind (Bindings.find (field_name rec_id id) env.accessors) with | Not_found -> typ_error (id_loc id) ("No accessor found for " ^ string_of_id (field_name rec_id id)) + let get_accessor rec_id id env = + match get_accessor_fn rec_id id env with + | (typq, Typ_aux (Typ_fn (rec_typ, field_typ, effect), _)) -> + (typq, rec_typ, field_typ, effect) + | _ -> typ_error (id_loc id) ("Accessor with non-function type found for " ^ string_of_id (field_name rec_id id)) + let is_mutable id env = try let (mut, _) = Bindings.find id env.locals in @@ -953,6 +963,9 @@ let add_typquant (quant : typquant) (env : Env.t) : Env.t = (* Create vectors with the default order from the environment *) +let default_order_error_string = + "No default Order (if you have set a default Order, move it earlier in the specification)" + let dvector_typ env n m typ = vector_typ n m (Env.get_default_order env) typ let lvector_typ env l typ = @@ -961,6 +974,8 @@ let lvector_typ env l typ = vector_typ (nint 0) l ord typ | Ord_aux (Ord_dec, _) as ord -> vector_typ (nminus l (nint 1)) l ord typ + | Ord_aux (Ord_var _, _) as ord -> + typ_error Parse_ast.Unknown default_order_error_string let ex_counter = ref 0 @@ -1272,6 +1287,7 @@ let rec typ_frees ?exs:(exs=KidSet.empty) (Typ_aux (typ_aux, l)) = | Typ_tup typs -> List.fold_left KidSet.union KidSet.empty (List.map (typ_frees ~exs:exs) typs) | Typ_app (f, args) -> List.fold_left KidSet.union KidSet.empty (List.map (typ_arg_frees ~exs:exs) args) | Typ_exist (kids, nc, typ) -> typ_frees ~exs:(KidSet.of_list kids) typ + | Typ_fn (typ1, typ2, _) -> KidSet.union (typ_frees ~exs:exs typ1) (typ_frees ~exs:exs typ2) and typ_arg_frees ?exs:(exs=KidSet.empty) (Typ_arg_aux (typ_arg_aux, l)) = match typ_arg_aux with | Typ_arg_nexp n -> nexp_frees ~exs:exs n @@ -1334,6 +1350,7 @@ let typ_identical env typ1 typ2 = | Typ_arg_nexp n1, Typ_arg_nexp n2 -> nexp_identical n1 n2 | Typ_arg_typ typ1, Typ_arg_typ typ2 -> typ_identical' typ1 typ2 | Typ_arg_order ord1, Typ_arg_order ord2 -> ord_identical ord1 ord2 + | _, _ -> false in typ_identical' (Env.expand_synonyms env typ1) (Env.expand_synonyms env typ2) @@ -1613,8 +1630,12 @@ let rec subtyp l env typ1 typ2 = when is_some (destruct_atom_kid env typ1) && is_some (destruct_atom_kid env typ2) -> let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env kids1 in let env = Env.add_constraint nc1 env in - let Some atom_kid1 = destruct_atom_kid env typ1 in - let Some atom_kid2 = destruct_atom_kid env typ2 in + + (* Guaranteed to succeed because of the guard *) + let destruct_some x = match x with Some y -> y | _ -> assert false in + let atom_kid1 = destruct_some (destruct_atom_kid env typ1) in + let atom_kid2 = destruct_some (destruct_atom_kid env typ2) in + let kids2 = List.filter (fun kid -> Kid.compare atom_kid2 kid <> 0) kids2 in let env = Env.add_typ_var atom_kid2 BK_nat env in let env = Env.add_constraint (nc_eq (nvar atom_kid1) (nvar atom_kid2)) env in @@ -1640,6 +1661,7 @@ let rec subtyp l env typ1 typ2 = let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env existential_kids in let env = List.fold_left uv_nexp_constraint env (KBindings.bindings unifiers) in Env.add_constraint enc env + | _, None -> assert false (* Cannot have existential_kids without existential_nc *) in if prove env nc then () else typ_error l ("Could not show " ^ string_of_typ typ1 ^ " is a subset of existential " ^ string_of_typ typ2) @@ -1683,6 +1705,8 @@ let infer_lit env (L_aux (lit_aux, l) as lit) = (nint (String.length str - 1)) (nint (String.length str)) (mk_typ (Typ_id (mk_id "bit"))) + | Ord_aux (Ord_var _, _) -> typ_error l default_order_error_string + end | L_hex str -> begin @@ -1694,6 +1718,8 @@ let infer_lit env (L_aux (lit_aux, l) as lit) = (nint (String.length str * 4 - 1)) (nint (String.length str * 4)) (mk_typ (Typ_id (mk_id "bit"))) + + | Ord_aux (Ord_var _, _) -> typ_error l default_order_error_string end | L_undef -> typ_error l "Cannot infer the type of undefined" @@ -1982,7 +2008,10 @@ let strip_lexp : 'a lexp -> unit lexp = function lexp -> map_lexp_annot (fun (l, let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ_aux, _) as typ) : tannot exp = let annot_exp_effect exp typ eff = E_aux (exp, (l, Some (env, typ, eff))) in - let add_effect (E_aux (exp, (l, Some (env, typ, _)))) eff = E_aux (exp, (l, Some (env, typ, eff))) in + let add_effect exp eff = match exp with + | (E_aux (exp, (l, Some (env, typ, _)))) -> E_aux (exp, (l, Some (env, typ, eff))) + | _ -> failwith "Tried to add effect to unannoted expression" + in let annot_exp exp typ = annot_exp_effect exp typ no_effect in match (exp_aux, typ_aux) with | E_block exps, _ -> @@ -2055,7 +2084,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ | _ -> typ_error l ("The type " ^ string_of_typ typ ^ " is not a record") in let check_fexp (FE_aux (FE_Fexp (field, exp), (l, ()))) = - let (typq, Typ_aux (Typ_fn (rectyp_q, field_typ, _), _)) = Env.get_accessor rectyp_id field env in + let (typq, rectyp_q, field_typ, _) = Env.get_accessor rectyp_id field env in let unifiers, _, _ (* FIXME *) = try unify l env rectyp_q typ with Unification_error (l, m) -> typ_error l ("Unification error: " ^ m) in let field_typ' = subst_unifiers unifiers field_typ in let checked_exp = crule check_exp env exp field_typ' in @@ -2070,7 +2099,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ | _ -> typ_error l ("The type " ^ string_of_typ typ ^ " is not a record") in let check_fexp (FE_aux (FE_Fexp (field, exp), (l, ()))) = - let (typq, Typ_aux (Typ_fn (rectyp_q, field_typ, _), _)) = Env.get_accessor rectyp_id field env in + let (typq, rectyp_q, field_typ, _) = Env.get_accessor rectyp_id field env in let unifiers, _, _ (* FIXME *) = try unify l env rectyp_q typ with Unification_error (l, m) -> typ_error l ("Unification error: " ^ m) in let field_typ' = subst_unifiers unifiers field_typ in let checked_exp = crule check_exp env exp field_typ' in @@ -2131,7 +2160,10 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ let checked_exp = crule check_exp env exp exc_typ in annot_exp_effect (E_throw checked_exp) typ (mk_effect [BE_escape]) | E_internal_let (lexp, bind, exp), _ -> - let E_aux (E_assign (lexp, bind), _), env = bind_assignment env lexp bind in + let lexp, bind, env = match bind_assignment env lexp bind with + | E_aux (E_assign (lexp, bind), _), env -> lexp, bind, env + | _, _ -> assert false + in let checked_exp = crule check_exp env exp typ in annot_exp (E_internal_let (lexp, bind, checked_exp)) typ | E_internal_return exp, _ -> @@ -2214,7 +2246,10 @@ and check_case env pat_typ pexp typ = and type_coercion env (E_aux (_, (l, _)) as annotated_exp) typ = let strip exp_aux = strip_exp (E_aux (exp_aux, (Parse_ast.Unknown, None))) in let annot_exp exp typ = E_aux (exp, (l, Some (env, typ, no_effect))) in - let switch_typ (E_aux (exp, (l, Some (env, _, eff)))) typ = E_aux (exp, (l, Some (env, typ, eff))) in + let switch_typ exp typ = match exp with + | (E_aux (exp, (l, Some (env, _, eff)))) -> E_aux (exp, (l, Some (env, typ, eff))) + | _ -> failwith "Cannot switch type for unannotated function" + in let rec try_casts trigger errs = function | [] -> typ_raise l (Err_no_casts (trigger, errs)) | (cast :: casts) -> begin @@ -2245,7 +2280,10 @@ and type_coercion env (E_aux (_, (l, _)) as annotated_exp) typ = and type_coercion_unify env (E_aux (_, (l, _)) as annotated_exp) typ = let strip exp_aux = strip_exp (E_aux (exp_aux, (Parse_ast.Unknown, None))) in let annot_exp exp typ = E_aux (exp, (l, Some (env, typ, no_effect))) in - let switch_typ (E_aux (exp, (l, Some (env, _, eff)))) typ = E_aux (exp, (l, Some (env, typ, eff))) in + let switch_typ exp typ = match exp with + | (E_aux (exp, (l, Some (env, _, eff)))) -> E_aux (exp, (l, Some (env, typ, eff))) + | _ -> failwith "Cannot switch type for unannotated expression" + in let rec try_casts = function | [] -> unify_error l "No valid casts resulted in unification" | (cast :: casts) -> begin @@ -2272,7 +2310,10 @@ and type_coercion_unify env (E_aux (_, (l, _)) as annotated_exp) typ = and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) = typ_print ("Binding " ^ string_of_pat pat ^ " to " ^ string_of_typ typ); let annot_pat pat typ = P_aux (pat, (l, Some (env, typ, no_effect))) in - let switch_typ (P_aux (pat_aux, (l, Some (env, _, eff)))) typ = P_aux (pat_aux, (l, Some (env, typ, eff))) in + let switch_typ pat typ = match pat with + | (P_aux (pat_aux, (l, Some (env, _, eff)))) -> P_aux (pat_aux, (l, Some (env, typ, eff))) + | _ -> failwith "Cannot switch type of unannotated pattern" + in let bind_tuple_pat (tpats, env) pat typ = let tpat, env = bind_pat env pat typ in tpat :: tpats, env in @@ -2411,7 +2452,7 @@ and infer_pat env (P_aux (pat_aux, (l, ())) as pat) = | P_id v -> begin match Env.lookup_id v env with - | Local (Immutable, _) | Unbound -> + | Local (Immutable, _) | Unbound | Union _ -> typ_error l ("Cannot infer identifier in pattern " ^ string_of_pat pat ^ " - try adding a type annotation") | Local (Mutable, _) | Register _ -> typ_error l ("Cannot shadow mutable local or register in switch statement pattern " ^ string_of_pat pat) @@ -2428,26 +2469,26 @@ and infer_pat env (P_aux (pat_aux, (l, ())) as pat) = let typed_pat, env = bind_pat env pat bit_typ in pats @ [typed_pat], env in - let ((typed_pat :: typed_pats) as pats), env = + let pats, env = List.fold_left fold_pats ([], env) (pat :: pats) in let len = nexp_simp (nint (List.length pats)) in - let etyp = pat_typ_of typed_pat in - List.map (fun pat -> typ_equality l env etyp (pat_typ_of pat)) pats; + let etyp = pat_typ_of (List.hd pats) in + List.iter (fun pat -> typ_equality l env etyp (pat_typ_of pat)) pats; annot_pat (P_vector pats) (lvector_typ env len etyp), env | P_vector_concat (pat :: pats) -> let fold_pats (pats, env) pat = let inferred_pat, env = infer_pat env pat in pats @ [inferred_pat], env in - let (inferred_pat :: inferred_pats), env = List.fold_left fold_pats ([], env) (pat :: pats) in - let (_, len, _, vtyp) = destruct_vec_typ l env (pat_typ_of inferred_pat) in + let inferred_pats, env = List.fold_left fold_pats ([], env) (pat :: pats) in + let (_, len, _, vtyp) = destruct_vec_typ l env (pat_typ_of (List.hd inferred_pats)) in let fold_len len pat = let (_, len', _, vtyp') = destruct_vec_typ l env (pat_typ_of pat) in typ_equality l env vtyp vtyp'; nsum len len' in - let len = nexp_simp (List.fold_left fold_len len inferred_pats) in - annot_pat (P_vector_concat (inferred_pat :: inferred_pats)) (lvector_typ env len vtyp), env + let len = nexp_simp (List.fold_left fold_len len (List.tl inferred_pats)) in + annot_pat (P_vector_concat inferred_pats) (lvector_typ env len vtyp), env | P_as (pat, id) -> let (typed_pat, env) = infer_pat env pat in annot_pat (P_as (typed_pat, id)) (pat_typ_of typed_pat), Env.add_local id (Immutable, pat_typ_of typed_pat) env @@ -2478,14 +2519,19 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as let is_immutable, vtyp, is_register = match Env.lookup_id v env with | Unbound -> typ_error l "Cannot assign to element of unbound vector" | Enum _ -> typ_error l "Cannot vector assign to enumeration element" + | Union _ -> typ_error l "Cannot vector assign to union element" | Local (Immutable, vtyp) -> true, vtyp, false | Local (Mutable, vtyp) -> false, vtyp, false | Register vtyp -> false, vtyp, true in let access = infer_exp (Env.enable_casts env) (E_aux (E_app (mk_id "vector_access", [E_aux (E_id v, (l, ())); exp]), (l, ()))) in - let E_aux (E_app (_, [_; inferred_exp]), _) = access in + let inferred_exp = match access with + | E_aux (E_app (_, [_; inferred_exp]), _) -> inferred_exp + | _ -> assert false + in typ_of access, LEXP_vector (annot_lexp (LEXP_id v) vtyp, inferred_exp), is_register end + | _ -> typ_error l "Field l-expression must be either a vector or an identifier" in let regtyp, inferred_flexp, is_register = infer_flexp flexp in typ_debug ("REGTYP: " ^ string_of_typ regtyp ^ " / " ^ string_of_typ (Env.expand_synonyms env regtyp)); @@ -2509,7 +2555,7 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as annot_assign (annot_lexp (LEXP_field (annot_lexp_effect inferred_flexp regtyp eff, field)) vec_typ) checked_exp, env | Typ_aux (Typ_id rectyp_id, _) | Typ_aux (Typ_app (rectyp_id, _), _) when Env.is_record rectyp_id env -> let eff = if is_register then mk_effect [BE_wreg] else no_effect in - let (typq, Typ_aux (Typ_fn (rectyp_q, field_typ, _), _)) = Env.get_accessor rectyp_id field env in + let (typq, rectyp_q, field_typ, _) = Env.get_accessor rectyp_id field env in let unifiers, _, _ (* FIXME *) = try unify l env rectyp_q regtyp with Unification_error (l, m) -> typ_error l ("Unification error: " ^ m) in let field_typ' = subst_unifiers unifiers field_typ in let checked_exp = crule check_exp env exp field_typ' in @@ -2541,8 +2587,8 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ = match lexp_aux with | LEXP_id v -> begin match Env.lookup_id v env with - | Local (Immutable, _) | Enum _ -> - typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v) + | Local (Immutable, _) | Enum _ | Union _ -> + typ_error l ("Cannot modify let-bound constant, union or enumeration constructor " ^ string_of_id v) | Local (Mutable, vtyp) -> subtyp l env typ vtyp; annot_lexp (LEXP_id v) typ, env | Register vtyp -> subtyp l env typ vtyp; annot_lexp_effect (LEXP_id v) typ (mk_effect [BE_wreg]), env | Unbound -> annot_lexp (LEXP_id v) typ, Env.add_local v (Mutable, typ) env @@ -2550,8 +2596,8 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ = | LEXP_cast (typ_annot, v) -> begin match Env.lookup_id v env with - | Local (Immutable, _) | Enum _ -> - typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v) + | Local (Immutable, _) | Enum _ | Union _ -> + typ_error l ("Cannot modify let-bound constant, union or enumeration constructor " ^ string_of_id v) | Local (Mutable, vtyp) -> begin subtyp l env typ typ_annot; @@ -2595,8 +2641,8 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ = | LEXP_aux (LEXP_id v, _) -> begin match Env.lookup_id v env with - | Local (Immutable, _) | Enum _ -> - typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v) + | Local (Immutable, _) | Enum _ | Union _ -> + typ_error l ("Cannot modify let-bound constant, union or enumeration constructor " ^ string_of_id v) | Unbound -> typ_error l "Unbound variable in vector tuple assignment" | Local (Mutable, vtyp) | Register vtyp -> @@ -2614,7 +2660,7 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ = | Register (Typ_aux (Typ_id rec_id, _)) -> rec_id | _ -> typ_error l (string_of_lexp lexp ^ " must be a record register here") in - let typq, (Typ_aux (Typ_fn (_, vtyp, _), _)) = Env.get_accessor rec_id fid env in + let typq, _, vtyp, _ = Env.get_accessor rec_id fid env in let llen' = match destruct_vector env vtyp with | Some (_, llen', _, _) -> llen' | None -> typ_error l "Variables in vector tuple assignment must be vectors" @@ -2636,12 +2682,16 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ = let is_immutable, is_register, vtyp = match Env.lookup_id v env with | Unbound -> typ_error l "Cannot assign to element of unbound vector" | Enum _ -> typ_error l "Cannot vector assign to enumeration element" + | Union _ -> typ_error l "Cannot vector assign to union element" | Local (Immutable, vtyp) -> true, false, vtyp | Local (Mutable, vtyp) -> false, false, vtyp | Register vtyp -> false, true, vtyp in let access = infer_exp (Env.enable_casts env) (E_aux (E_app (mk_id "vector_subrange", [E_aux (E_id v, (l, ())); exp1; exp2]), (l, ()))) in - let E_aux (E_app (_, [_; inferred_exp1; inferred_exp2]), _) = access in + let inferred_exp1, inferred_exp2 = match access with + | E_aux (E_app (_, [_; inferred_exp1; inferred_exp2]), _) -> inferred_exp1, inferred_exp2 + | _ -> assert false + in match typ_of access with | Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_typ deref_typ, _)]), _) when string_of_id id = "register" -> subtyp l env typ deref_typ; @@ -2660,12 +2710,16 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ = let is_immutable, is_register, vtyp = match Env.lookup_id v env with | Unbound -> typ_error l "Cannot assign to element of unbound vector" | Enum _ -> typ_error l "Cannot vector assign to enumeration element" + | Union _ -> typ_error l "Cannot vector assign to union element" | Local (Immutable, vtyp) -> true, false, vtyp | Local (Mutable, vtyp) -> false, false, vtyp | Register vtyp -> false, true, vtyp in let access = infer_exp (Env.enable_casts env) (E_aux (E_app (mk_id "vector_access", [E_aux (E_id v, (l, ())); exp]), (l, ()))) in - let E_aux (E_app (_, [_; inferred_exp]), _) = access in + let inferred_exp = match access with + | E_aux (E_app (_, [_; inferred_exp]), _) -> inferred_exp + | _ -> assert false + in match typ_of access with | Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_typ deref_typ, _)]), _) when string_of_id id = "register" -> subtyp l env typ deref_typ; @@ -2685,7 +2739,7 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ = | Register (Typ_aux (Typ_id rec_id, _)) -> rec_id | _ -> typ_error l (string_of_lexp lexp ^ " must be a record register here") in - let typq, (Typ_aux (Typ_fn (_, ret_typ, _), _)) = Env.get_accessor rec_id fid env in + let typq, _, ret_typ, _ = Env.get_accessor rec_id fid env in annot_lexp_effect (LEXP_field (annot_lexp (LEXP_id v) (mk_id_typ rec_id), fid)) ret_typ (mk_effect [BE_wreg]), env | _ -> typ_error l ("Unhandled l-expression " ^ string_of_lexp lexp) @@ -2743,7 +2797,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = (* Accessing a field of a record *) | Typ_aux (Typ_id rectyp, _) as typ when Env.is_record rectyp env -> begin - let inferred_acc, _ = infer_funapp' l (Env.no_casts env) field (Env.get_accessor rectyp field env) [strip_exp inferred_exp] None in + let inferred_acc, _ = infer_funapp' l (Env.no_casts env) field (Env.get_accessor_fn rectyp field env) [strip_exp inferred_exp] None in match inferred_acc with | E_aux (E_app (field, [inferred_exp]) ,_) -> annot_exp (E_field (inferred_exp, field)) (typ_of inferred_acc) | _ -> assert false (* Unreachable *) @@ -2764,7 +2818,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = | _ -> typ_error l ("The type " ^ string_of_typ typ ^ " is not a record") in let check_fexp (FE_aux (FE_Fexp (field, exp), (l, ()))) = - let (typq, Typ_aux (Typ_fn (rectyp_q, field_typ, _), _)) = Env.get_accessor rectyp_id field env in + let (typq, rectyp_q, field_typ, _) = Env.get_accessor rectyp_id field env in let unifiers, _, _ (* FIXME *) = try unify l env rectyp_q typ with Unification_error (l, m) -> typ_error l ("Unification error: " ^ m) in let field_typ' = subst_unifiers unifiers field_typ in let inferred_exp = crule check_exp env exp field_typ' in @@ -2797,6 +2851,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = let f, t, is_dec = match ord with | Ord_aux (Ord_inc, _) -> f, t, false | Ord_aux (Ord_dec, _) -> t, f, true (* reverse direction to typechecking downto as upto loop *) + | Ord_aux (Ord_var _, _) -> typ_error l "Cannot check a loop with variable direction!" (* This should never happen *) in let inferred_f = irule infer_exp env f in let inferred_t = irule infer_exp env t in @@ -2852,6 +2907,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = mk_typ_arg (Typ_arg_nexp (nint (List.length vec))); mk_typ_arg (Typ_arg_order (Env.get_default_order env)); mk_typ_arg (Typ_arg_typ (typ_of inferred_item))])) + | Ord_aux (Ord_var _, _) -> typ_error l default_order_error_string in annot_exp (E_vector (inferred_item :: checked_items)) vec_typ | E_assert (test, msg) -> @@ -2903,7 +2959,10 @@ and instantiation_of (E_aux (exp_aux, (l, _)) as exp) = and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ = let annot_exp exp typ eff = E_aux (exp, (l, Some (env, typ, eff))) in - let switch_annot env typ (E_aux (exp, (l, Some (_, _, eff)))) = E_aux (exp, (l, Some (env, typ, eff))) in + let switch_annot env typ = function + | (E_aux (exp, (l, Some (_, _, eff)))) -> E_aux (exp, (l, Some (env, typ, eff))) + | _ -> failwith "Cannot switch annot for unannotated function" + in let all_unifiers = ref KBindings.empty in let ex_goal = ref None in let prove_goal env = match !ex_goal with @@ -2961,6 +3020,7 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ = let enc = List.fold_left (fun nc kid -> nc_subst_nexp kid (Nexp_var (prepend_kid ex_tag kid)) nc) enc ex_kids in let env = List.fold_left (fun env kid -> Env.add_typ_var (prepend_kid ex_tag kid) BK_nat env) env ex_kids in Env.add_constraint enc env + | _, None -> assert false (* Cannot have ex_kids without ex_nc *) in let tag_unifier uvar = List.fold_left (fun uvar kid -> uvar_subst_nexp kid (Nexp_var (prepend_kid ex_tag kid)) uvar) uvar ex_kids in let unifiers = KBindings.map tag_unifier unifiers in @@ -3199,12 +3259,6 @@ and propagate_exp_effect_aux = function | E_field (exp, id) -> let p_exp = propagate_exp_effect exp in E_field (p_exp, id), effect_of p_exp - | E_internal_let (lexp, exp, body) -> - let p_lexp = propagate_lexp_effect lexp in - let p_exp = propagate_exp_effect exp in - let p_body = propagate_exp_effect body in - E_internal_let (p_lexp, p_exp, p_body), - union_effects (effect_of_lexp p_lexp) (collect_effects [p_exp; p_body]) | E_internal_plet (pat, exp, body) -> let p_pat = propagate_pat_effect pat in let p_exp = propagate_exp_effect exp in @@ -3322,7 +3376,6 @@ and propagate_lexp_effect_aux = function | LEXP_field (lexp, id) -> let p_lexp = propagate_lexp_effect lexp in LEXP_field (p_lexp, id),effect_of_lexp p_lexp - | _ -> typ_error Parse_ast.Unknown "Unimplemented: Cannot propagate effect in lexp" (**************************************************************************) (* 6. Checking toplevel definitions *) @@ -3411,12 +3464,16 @@ let check_fundef env (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls) | None -> typ_error l "funcl list is empty" in typ_print ("\nChecking function " ^ string_of_id id); - let have_val_spec, (quant, (Typ_aux (Typ_fn (vtyp_arg, vtyp_ret, declared_eff), vl) as typ)), env = + let have_val_spec, (quant, typ), env = try true, Env.get_val_spec id env, env with | Type_error (l, _) -> let (quant, typ) = infer_funtyp l env tannotopt funcls in false, (quant, typ), env in + let vtyp_arg, vtyp_ret, declared_eff, vl = match typ with + | Typ_aux (Typ_fn (vtyp_arg, vtyp_ret, declared_eff), vl) -> vtyp_arg, vtyp_ret, declared_eff, vl + | _ -> typ_error l "Function val spec was not a function type" + in check_tannotopt env quant vtyp_ret tannotopt; typ_debug ("Checking fundef " ^ string_of_id id ^ " has type " ^ string_of_bind (quant, typ)); let funcl_env = add_typquant quant env in @@ -3488,6 +3545,7 @@ let kinded_id_arg kind_id = typ_arg (Typ_arg_order (Ord_aux (Ord_var kid, Parse_ast.Unknown))) | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_type, _)], _), kid), _) -> typ_arg (Typ_arg_typ (mk_typ (Typ_var kid))) + | KOpt_aux (KOpt_kind (K_aux (K_kind kinds, _), kid), l) -> typ_error l "Badly formed kind" let fold_union_quant quants (QI_aux (qi, l)) = match qi with diff --git a/src/type_check.mli b/src/type_check.mli index 1931ce03..9a61f196 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -113,7 +113,8 @@ module Env : sig val is_record : id -> t -> bool - val get_accessor : id -> id -> t -> typquant * typ + (* Return type is: quantifier, argument type, return type, effect *) + val get_accessor : id -> id -> t -> typquant * typ * typ * effect (* If the environment is checking a function, then this will get the expected return type of the function. It's useful for checking or diff --git a/src/value.ml b/src/value.ml index 4974ca83..f49b230c 100644 --- a/src/value.ml +++ b/src/value.ml @@ -69,6 +69,7 @@ let rec string_of_value = function | V_bool false -> "false" | V_bit B0 -> "bitzero" | V_bit B1 -> "bitone" + | V_int n -> Big_int.to_string n | V_tuple vals -> "(" ^ Util.string_of_list ", " string_of_value vals ^ ")" | V_list vals -> "[" ^ Util.string_of_list ", " string_of_value vals ^ "]" | V_unit -> "()" @@ -89,9 +90,17 @@ let coerce_bool = function | V_bool b -> b | _ -> assert false -let and_bool [v1; v2] = V_bool (coerce_bool v1 && coerce_bool v2) -let or_bool [v1; v2] = V_bool (coerce_bool v1 || coerce_bool v2) -let print [v] = print_endline (string_of_value v |> Util.red |> Util.clear); V_unit +let and_bool = function + | [v1; v2] -> V_bool (coerce_bool v1 && coerce_bool v2) + | _ -> assert false + +let or_bool = function + | [v1; v2] -> V_bool (coerce_bool v1 || coerce_bool v2) + | _ -> assert false + +let print = function + | [v] -> print_endline (string_of_value v |> Util.red |> Util.clear); V_unit + | _ -> assert false let tuple_value (vs : value list) : value = V_tuple vs |