diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast_util.ml | 14 | ||||
| -rw-r--r-- | src/c_backend.ml | 34 | ||||
| -rw-r--r-- | src/initial_check.ml | 29 | ||||
| -rw-r--r-- | src/rewrites.ml | 11 | ||||
| -rw-r--r-- | src/type_check.ml | 132 |
5 files changed, 124 insertions, 96 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml index 97ce3896..09fc9fc9 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -486,7 +486,7 @@ let def_loc = function let string_of_id = function | Id_aux (Id v, _) -> v - | Id_aux (DeIid v, _) -> "(deinfix " ^ v ^ ")" + | Id_aux (DeIid v, _) -> "(operator " ^ v ^ ")" let id_of_kid = function | Kid_aux (Var v, l) -> Id_aux (Id (String.sub v 1 (String.length v - 1)), l) @@ -528,7 +528,7 @@ let string_of_base_effect_aux = function let string_of_base_kind_aux = function | BK_type -> "Type" - | BK_nat -> "Nat" + | BK_nat -> "Int" | BK_order -> "Order" let string_of_base_kind (BK_aux (bk, _)) = string_of_base_kind_aux bk @@ -567,11 +567,11 @@ and string_of_typ_aux = function | Typ_id id -> string_of_id id | Typ_var kid -> string_of_kid kid | Typ_tup typs -> "(" ^ string_of_list ", " string_of_typ typs ^ ")" - | Typ_app (id, args) -> string_of_id id ^ "<" ^ string_of_list ", " string_of_typ_arg args ^ ">" + | Typ_app (id, args) -> string_of_id id ^ "(" ^ string_of_list ", " string_of_typ_arg args ^ ")" | Typ_fn (typ_arg, typ_ret, eff) -> string_of_typ typ_arg ^ " -> " ^ string_of_typ typ_ret ^ " effect " ^ string_of_effect eff | Typ_exist (kids, nc, typ) -> - "exist " ^ string_of_list " " string_of_kid kids ^ ", " ^ string_of_n_constraint nc ^ ". " ^ string_of_typ typ + "{" ^ string_of_list " " string_of_kid kids ^ ", " ^ string_of_n_constraint nc ^ ". " ^ string_of_typ typ ^ "}" and string_of_typ_arg = function | Typ_arg_aux (typ_arg, l) -> string_of_typ_arg_aux typ_arg and string_of_typ_arg_aux = function @@ -588,7 +588,7 @@ and string_of_n_constraint = function | NC_aux (NC_and (nc1, nc2), _) -> "(" ^ string_of_n_constraint nc1 ^ " & " ^ string_of_n_constraint nc2 ^ ")" | NC_aux (NC_set (kid, ns), _) -> - string_of_kid kid ^ " IN {" ^ string_of_list ", " Big_int.to_string ns ^ "}" + string_of_kid kid ^ " in {" ^ string_of_list ", " Big_int.to_string ns ^ "}" | NC_aux (NC_true, _) -> "true" | NC_aux (NC_false, _) -> "false" @@ -599,7 +599,7 @@ let string_of_annot = function let string_of_quant_item_aux = function | QI_id (KOpt_aux (KOpt_none kid, _)) -> string_of_kid kid - | QI_id (KOpt_aux (KOpt_kind (k, kid), _)) -> string_of_kind k ^ " " ^ string_of_kid kid + | QI_id (KOpt_aux (KOpt_kind (k, kid), _)) -> "(" ^ string_of_kid kid ^ " :: " ^ string_of_kind k ^ ")" | QI_const constr -> string_of_n_constraint constr let string_of_quant_item = function @@ -641,7 +641,7 @@ let rec string_of_exp (E_aux (exp, _)) = | E_app_infix (x, op, y) -> "(" ^ string_of_exp x ^ " " ^ string_of_id op ^ " " ^ string_of_exp y ^ ")" | E_tuple exps -> "(" ^ string_of_list ", " string_of_exp exps ^ ")" | E_case (exp, cases) -> - "switch " ^ string_of_exp exp ^ " { case " ^ string_of_list " case " string_of_pexp cases ^ "}" + "match " ^ string_of_exp exp ^ " { " ^ string_of_list ", " string_of_pexp cases ^ " }" | E_try (exp, cases) -> "try " ^ string_of_exp exp ^ " catch { case " ^ string_of_list " case " string_of_pexp cases ^ "}" | E_let (letbind, exp) -> "let " ^ string_of_letbind letbind ^ " in " ^ string_of_exp exp diff --git a/src/c_backend.ml b/src/c_backend.ml index 398a0281..6e1083df 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -168,7 +168,7 @@ and sc_op = SC_and | SC_or and apat = | AP_tup of apat list - | AP_id of id + | AP_id of id * typ | AP_global of id * typ | AP_app of id * apat | AP_cons of apat * apat @@ -202,8 +202,8 @@ let rec frag_rename from_id to_id = function let rec apat_bindings = function | AP_tup apats -> List.fold_left IdSet.union IdSet.empty (List.map apat_bindings apats) - | AP_id id -> IdSet.singleton id - | AP_global (id, typ) -> IdSet.empty + | AP_id (id, _) -> IdSet.singleton id + | AP_global (id, _) -> IdSet.empty | AP_app (id, apat) -> apat_bindings apat | AP_cons (apat1, apat2) -> IdSet.union (apat_bindings apat1) (apat_bindings apat2) | AP_nil -> IdSet.empty @@ -211,8 +211,8 @@ let rec apat_bindings = function let rec apat_rename from_id to_id = function | AP_tup apats -> AP_tup (List.map (apat_rename from_id to_id) apats) - | AP_id id when Id.compare id from_id = 0 -> AP_id to_id - | AP_id id -> AP_id id + | AP_id (id, typ) when Id.compare id from_id = 0 -> AP_id (to_id, typ) + | AP_id (id, typ) -> AP_id (id, typ) | AP_global (id, typ) -> AP_global (id, typ) | AP_app (ctor, apat) -> AP_app (ctor, apat_rename from_id to_id apat) | AP_cons (apat1, apat2) -> AP_cons (apat_rename from_id to_id apat1, apat_rename from_id to_id apat2) @@ -430,7 +430,7 @@ let rec pp_aexp = function and pp_apat = function | AP_wild -> string "_" - | AP_id id -> pp_id id + | AP_id (id, typ) -> pp_annot typ (pp_id id) | AP_global (id, _) -> pp_id id | AP_tup apats -> parens (separate_map (comma ^^ space) pp_apat apats) | AP_app (id, apat) -> pp_id id ^^ parens (pp_apat apat) @@ -484,7 +484,7 @@ let rec split_block = function let rec anf_pat ?global:(global=false) (P_aux (p_aux, (l, _)) as pat) = match p_aux with | P_id id when global -> AP_global (id, pat_typ_of pat) - | P_id id -> AP_id id + | P_id id -> AP_id (id, pat_typ_of pat) | P_wild -> AP_wild | P_tup pats -> AP_tup (List.map (fun pat -> anf_pat ~global:global pat) pats) | P_app (id, [pat]) -> AP_app (id, anf_pat ~global:global pat) @@ -1544,8 +1544,9 @@ let compile_funcall ctx id args typ = (List.rev !setup, final_ctyp, call, !cleanup) let rec compile_match ctx apat cval case_label = + prerr_endline ("Compiling match " ^ Pretty_print_sail.to_string (pp_apat apat) ^ " cval " ^ Pretty_print_sail.to_string (pp_cval cval)); match apat, cval with - | AP_id pid, (frag, ctyp) when Env.is_union_constructor pid ctx.tc_env -> + | AP_id (pid, _), (frag, ctyp) when Env.is_union_constructor pid ctx.tc_env -> [ijump (F_op (F_field (frag, "kind"), "!=", F_lit (V_ctor_kind (string_of_id pid))), CT_bool) case_label], [] | AP_global (pid, typ), (frag, ctyp) -> @@ -1558,15 +1559,21 @@ let rec compile_match ctx apat cval case_label = [iconvert (CL_id pid) global_ctyp id ctyp], [] | _ -> c_error "Cannot compile global letbinding" end - | AP_id pid, (frag, ctyp) when is_ct_enum ctyp -> + | AP_id (pid, _), (frag, ctyp) when is_ct_enum ctyp -> begin match Env.lookup_id pid ctx.tc_env with | Unbound -> [idecl ctyp pid; icopy (CL_id pid) (frag, ctyp)], [] | _ -> [ijump (F_op (F_id pid, "!=", frag), CT_bool) case_label], [] end - | AP_id pid, _ -> + | AP_id (pid, typ), _ -> let ctyp = cval_ctyp cval in - let init, cleanup = if is_stack_ctyp ctyp then [], [] else [ialloc ctyp pid], [iclear ctyp pid] in - [idecl ctyp pid] @ init @ [icopy (CL_id pid) cval], cleanup + let id_ctyp = ctyp_of_typ ctx typ in + let init, cleanup = if is_stack_ctyp id_ctyp then [], [] else [ialloc id_ctyp pid], [iclear id_ctyp pid] in + if ctyp_equal id_ctyp ctyp then + [idecl ctyp pid] @ init @ [icopy (CL_id pid) cval], cleanup + else + let gs = gensym () in + let gs_init, gs_cleanup = if is_stack_ctyp ctyp then [], [] else [ialloc ctyp gs], [iclear ctyp gs] in + [idecl id_ctyp pid; idecl ctyp gs] @ init @ gs_init @ [icopy (CL_id gs) cval; iconvert (CL_id pid) id_ctyp gs ctyp] @ gs_cleanup, cleanup | AP_tup apats, (frag, ctyp) -> begin let get_tup n ctyp = (F_field (frag, "ztup" ^ string_of_int n), ctyp) in @@ -2170,6 +2177,7 @@ let rec compile_def ctx = function | DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, Pat_aux (Pat_exp (pat, exp), _)), _)]), _)) -> let aexp = map_functions (analyze_primop ctx) (c_literals ctx (no_shadow (pat_ids pat) (anf exp))) in + prerr_endline (Pretty_print_sail.to_string (pp_aexp aexp)); let setup, ctyp, call, cleanup = compile_aexp ctx aexp in let fundef_label = label "fundef_fail_" in let _, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in @@ -3333,7 +3341,7 @@ let codegen_def ctx def = let lists = List.map (fun ctyp -> codegen_list ctx (unlist ctyp)) lists in let vectors = List.filter is_ct_vector (cdef_ctyps ctx def) in let vectors = List.map (fun ctyp -> codegen_vector ctx (unvector ctyp)) vectors in - (* prerr_endline (Pretty_print_sail.to_string (pp_cdef def)); *) + prerr_endline (Pretty_print_sail.to_string (pp_cdef def)); concat tups ^^ concat lists ^^ concat vectors diff --git a/src/initial_check.ml b/src/initial_check.ml index 75668417..06ee1f65 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -1092,13 +1092,14 @@ let generate_initialize_registers vs_ids (Defs defs) = let generate_enum_functions vs_ids (Defs defs) = let rec gen_enums = function | DEF_type (TD_aux (TD_enum (id, _, elems, _), _)) as enum :: defs -> - let enum_val_spec name typ = - mk_val_spec (VS_val_spec (mk_typschm (mk_typquant []) typ, name, (fun _ -> None), !opt_enum_casts)) + let enum_val_spec name quants typ = + mk_val_spec (VS_val_spec (mk_typschm (mk_typquant quants) typ, name, (fun _ -> None), !opt_enum_casts)) in - let enum_range = range_typ (nint 0) (nint (List.length elems - 1)) in + let range_constraint kid = nc_and (nc_lteq (nint 0) (nvar kid)) (nc_lteq (nvar kid) (nint (List.length elems - 1))) in (* Create a function that converts a number to an enum. *) let to_enum = + let kid = mk_kid "e" in let name = append_id id "_of_num" in let pexp n id = let pat = @@ -1117,12 +1118,16 @@ let generate_enum_functions vs_ids (Defs defs) = let range = range_typ (nint 0) (nint (List.length elems - 1)) in if IdSet.mem name vs_ids then [] else - [ enum_val_spec name (function_typ enum_range (mk_typ (Typ_id id)) no_effect); + [ enum_val_spec name + [mk_qi_id BK_nat kid; mk_qi_nc (range_constraint kid)] + (function_typ (atom_typ (nvar kid)) (mk_typ (Typ_id id)) no_effect); mk_fundef [funcl] ] in (* Create a function that converts from an enum to a number. *) let from_enum = + let kid = mk_kid "e" in + let to_typ = mk_typ (Typ_exist ([kid], range_constraint kid, atom_typ (nvar kid))) in let name = prepend_id "num_of_" id in let pexp n id = mk_pexp (Pat_exp (mk_pat (P_id id), mk_lit_exp (L_num (Big_int.of_int n)))) in let funcl = @@ -1132,22 +1137,8 @@ let generate_enum_functions vs_ids (Defs defs) = in if IdSet.mem name vs_ids then [] else - [ enum_val_spec name (function_typ (mk_typ (Typ_id id)) enum_range no_effect); + [ enum_val_spec name [] (function_typ (mk_typ (Typ_id id)) to_typ no_effect); mk_fundef [funcl] ] - (* This is the simple way to generate this function, but the - rewriter and backends are all kinds of broken for function clause - patterns. - let name = prepend_id "num_of_" id in - let funcl n id = - mk_funcl name - (mk_pat (P_id id)) - (mk_lit_exp (L_num (Big_int.of_int n))) - in - if IdSet.mem name vs_ids then [] - else - [ enum_val_spec name (function_typ (mk_typ (Typ_id id)) enum_range no_effect); - mk_fundef (List.mapi funcl elems) ] - *) in enum :: to_enum @ from_enum @ gen_enums defs diff --git a/src/rewrites.ml b/src/rewrites.ml index 80c339e6..7ea0dadc 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -1961,15 +1961,23 @@ let rewrite_split_fun_constr_pats fun_name (Defs defs) = no_effect funcls in let fun_typ = function_typ args_typ ret_typ eff in + let quant_new_tyvars qis = + let quant_tyvars = List.fold_left KidSet.union KidSet.empty (List.map tyvars_of_quant_item qis) in + let typ_tyvars = tyvars_of_typ fun_typ in + let new_tyvars = KidSet.diff typ_tyvars quant_tyvars in + List.map (mk_qi_id BK_nat) (KidSet.elements new_tyvars) + in let typquant = match typquant with | TypQ_aux (TypQ_tq qis, l) -> let qis = List.filter (fun qi -> KidSet.subset (tyvars_of_quant_item qi) (tyvars_of_typ fun_typ)) qis + @ quant_new_tyvars qis in TypQ_aux (TypQ_tq qis, l) - | _ -> typquant + | _ -> + TypQ_aux (TypQ_tq (List.map (mk_qi_id BK_nat) (KidSet.elements (tyvars_of_typ fun_typ))), l) in let val_spec = VS_aux (VS_val_spec @@ -3216,6 +3224,7 @@ let rewrite_defs_ocaml = [ ("simple_assignments", rewrite_simple_assignments); ("remove_vector_concat", rewrite_defs_remove_vector_concat); ("remove_bitvector_pats", rewrite_defs_remove_bitvector_pats); + ("remove_numeral_pats", rewrite_defs_remove_numeral_pats); ("exp_lift_assign", rewrite_defs_exp_lift_assign); ("top_sort_defs", top_sort_defs); ("constraint", rewrite_constraint); diff --git a/src/type_check.ml b/src/type_check.ml index cc88c159..4b716ba8 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -167,6 +167,11 @@ let string_of_index_sort = function ^ string_of_list " & " (fun (x, y) -> string_of_nexp x ^ " <= " ^ string_of_nexp y) constraints ^ "}" +let is_atom (Typ_aux (typ_aux, _)) = + match typ_aux with + | Typ_app (f, [_]) when string_of_id f = "atom" -> true + | _ -> false + (**************************************************************************) (* 1. Substitutions *) (**************************************************************************) @@ -865,11 +870,13 @@ end = struct let get_constraints env = env.constraints - let add_constraint (NC_aux (_, l) as constr) env = + let add_constraint (NC_aux (nc_aux, l) as constr) env = wf_constraint env constr; begin typ_print ("Adding constraint " ^ string_of_n_constraint constr); - { env with constraints = constr :: env.constraints } + match nc_aux with + | NC_true -> env + | _ -> { env with constraints = constr :: env.constraints } end let get_ret_typ env = env.ret_typ @@ -942,7 +949,6 @@ end = struct } end - let add_typquant (quant : typquant) (env : Env.t) : Env.t = let rec add_quant_item env = function | QI_aux (qi, _) -> add_quant_item_aux env qi @@ -978,6 +984,12 @@ let destruct_exist env typ = Some (List.map snd fresh_kids, nc, typ) | _ -> None +let add_existential kids nc env = + let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env kids in + Env.add_constraint nc env + +let add_typ_vars kids env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env kids + let is_exist = function | Typ_aux (Typ_exist (_, _, _), _) -> true | _ -> false @@ -986,6 +998,41 @@ let exist_typ constr typ = let fresh_kid = fresh_existential () in mk_typ (Typ_exist ([fresh_kid], constr fresh_kid, typ fresh_kid)) +(** Destructure and canonicalise a numeric type into a list of type + variables, a constraint on those type variables, and an + N-expression that represents that numeric type in the + environment. For example: + - {'n, 'n <= 10. atom('n)} => ['n], 'n <= 10, 'n + - int => ['n], true, 'n (where x is fresh) + - atom('n) => [], true, 'n +**) +let destruct_numeric env typ = + let typ = Env.expand_synonyms env typ in + match destruct_exist env typ, typ with + | Some (kids, nc, Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp nexp, _)]), _)), _ when string_of_id id = "atom" -> + Some (kids, nc, nexp) + | None, Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp nexp, _)]), _) when string_of_id id = "atom" -> + Some ([], nc_true, nexp) + | None, Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp lo, _); Typ_arg_aux (Typ_arg_nexp hi, _)]), _) when string_of_id id = "range" -> + let kid = fresh_existential () in + Some ([kid], nc_and (nc_lteq lo (nvar kid)) (nc_lteq (nvar kid) hi), nvar kid) + | None, Typ_aux (Typ_id id, _) when string_of_id id = "nat" -> + let kid = fresh_existential () in + Some ([kid], nc_lteq (nint 0) (nvar kid), nvar kid) + | None, Typ_aux (Typ_id id, _) when string_of_id id = "int" -> + let kid = fresh_existential () in + Some ([kid], nc_true, nvar kid) + | _, _ -> None + +(** Pull an (potentially)-existentially qualified type into the global + typing environment **) +let bind_existential typ env = + match destruct_numeric env typ with + | Some (kids, nc, nexp) -> atom_typ nexp, add_existential kids nc env + | None -> match destruct_exist env typ with + | Some (kids, nc, typ) -> typ, add_existential kids nc env + | None -> typ, env + let destruct_vector env typ = let destruct_vector' = function | Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp n1, _); @@ -2432,6 +2479,7 @@ and bind_pat_no_guard env (P_aux (_,(l,_)) as pat) typ = | tpat, env, [] -> tpat, env and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) = + let (Typ_aux (typ_aux, _) as typ), env = bind_existential typ env in 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 pat typ = match pat with @@ -2458,34 +2506,8 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) | Enum enum -> subtyp l env enum typ; annot_pat (P_id v) typ, env, [] end | P_var (pat, typ_pat) -> - let typ = Env.expand_synonyms env typ in - let kid = Env.fresh_kid env in - let env, ex_typ = match destruct_exist env typ, typ with - | Some (kids, nc, ex_typ), _ -> - let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env kids in - let env = Env.add_constraint nc env in - env, ex_typ - | None, Typ_aux (Typ_id id, _) when string_of_id id = "int" -> - Env.add_typ_var kid BK_nat env, atom_typ (nvar kid) - | None, Typ_aux (Typ_id id, _) when string_of_id id = "nat" -> - let env = Env.add_typ_var kid BK_nat env in - let env = Env.add_constraint (nc_gt (nvar kid) (nint 0)) env in - env, atom_typ (nvar kid) - | None, Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp lo, _); Typ_arg_aux (Typ_arg_nexp hi, _)]), _) - when string_of_id id = "range" -> - let env = Env.add_typ_var kid BK_nat env in - let env = Env.add_constraint (nc_lteq lo (nvar kid)) env in - let env = Env.add_constraint (nc_lteq (nvar kid) hi) env in - env, atom_typ (nvar kid) - | None, Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp n, _)]), _) - when string_of_id id = "atom" -> - let env = Env.add_typ_var kid BK_nat env in - let env = Env.add_constraint (nc_eq (nvar kid) n) env in - env, atom_typ (nvar kid) - | None, _ -> typ_error l ("Cannot bind type variable against non existential or numeric type") - in - let env = bind_typ_pat env typ_pat ex_typ in - let typed_pat, env, guards = bind_pat env pat ex_typ in + let env = bind_typ_pat env typ_pat typ in + let typed_pat, env, guards = bind_pat env pat typ in annot_pat (P_var (typed_pat, typ_pat)) typ, env, guards | P_wild -> annot_pat P_wild typ, env, [] | P_cons (hd_pat, tl_pat) -> @@ -2566,10 +2588,14 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) | P_as (pat, id) -> let (typed_pat, env, guards) = bind_pat env pat typ in annot_pat (P_as (typed_pat, id)) (pat_typ_of typed_pat), Env.add_local id (Immutable, pat_typ_of typed_pat) env, guards + (* This is a special case for flow typing when we match a constant numeric literal. *) + | P_lit (L_aux (L_num n, _) as lit) when is_atom typ -> + let nexp = match destruct_atom_nexp env typ with Some n -> n | None -> assert false in + annot_pat (P_lit lit) (atom_typ (nconstant n)), Env.add_constraint (nc_eq nexp (nconstant n)) env, [] | _ -> let (inferred_pat, env, guards) = infer_pat env pat in - match subtyp l env (pat_typ_of inferred_pat) typ with - | () -> switch_typ inferred_pat typ, env, guards + match subtyp l env typ (pat_typ_of inferred_pat) with + | () -> switch_typ inferred_pat (pat_typ_of inferred_pat), env, guards | exception (Type_error _ as typ_exn) -> match pat_aux with | P_lit lit -> @@ -2979,27 +3005,17 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = let inferred_f = irule infer_exp env f in let inferred_t = irule infer_exp env t in let checked_step = crule check_exp env step int_typ in - match destruct_range (typ_of inferred_f), destruct_range (typ_of inferred_t) with - | None, _ -> typ_error l ("Type of " ^ string_of_exp f ^ " in foreach must be a range") - | _, None -> typ_error l ("Type of " ^ string_of_exp t ^ " in foreach must be a range") - (* | Some (l1, l2), Some (u1, u2) when prove env (nc_lteq l2 u1) -> - let loop_vtyp = exist_typ (fun e -> nc_and (nc_lteq l1 (nvar e)) (nc_lteq (nvar e) u2)) (fun e -> atom_typ (nvar e)) in + match destruct_numeric env (typ_of inferred_f), destruct_numeric env (typ_of inferred_t) with + | Some (kids1, nc1, nexp1), Some (kids2, nc2, nexp2) -> + let loop_kid = mk_kid ("loop_" ^ string_of_id v) in + let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env (loop_kid :: kids1 @ kids2) in + let env = Env.add_constraint (nc_and nc1 nc2) env in + let env = Env.add_constraint (nc_and (nc_lteq nexp1 (nvar loop_kid)) (nc_lteq (nvar loop_kid) nexp2)) env in + let loop_vtyp = atom_typ (nvar loop_kid) in let checked_body = crule check_exp (Env.add_local v (Immutable, loop_vtyp) env) body unit_typ in - annot_exp (E_for (v, inferred_f, inferred_t, checked_step, ord, checked_body)) unit_typ *) - | Some (l1, l2), Some (u1, u2) when prove env (nc_lteq l2 u1) -> - let kid = mk_kid ("loop_" ^ string_of_id v) in - if KBindings.mem kid (Env.get_typ_vars env) - then typ_error l "Nested loop variables cannot have the same name" - else - begin - let env = Env.add_typ_var kid BK_nat env in - let env = Env.add_constraint (nc_and (nc_lteq l1 (nvar kid)) (nc_lteq (nvar kid) u2)) env in - let loop_vtyp = atom_typ (nvar kid) in - let checked_body = crule check_exp (Env.add_local v (Immutable, loop_vtyp) env) body unit_typ in - if not is_dec (* undo reverse direction in annoteded ast for downto loop *) - then annot_exp (E_for (v, inferred_f, inferred_t, checked_step, ord, checked_body)) unit_typ - else annot_exp (E_for (v, inferred_t, inferred_f, checked_step, ord, checked_body)) unit_typ - end + if not is_dec (* undo reverse direction in annotated ast for downto loop *) + then annot_exp (E_for (v, inferred_f, inferred_t, checked_step, ord, checked_body)) unit_typ + else annot_exp (E_for (v, inferred_t, inferred_f, checked_step, ord, checked_body)) unit_typ | _, _ -> typ_error l "Ranges in foreach overlap" end | E_if (cond, then_branch, else_branch) -> @@ -3520,14 +3536,15 @@ and propagate_lexp_effect_aux = function (**************************************************************************) let check_letdef orig_env (LB_aux (letbind, (l, _))) = + typ_print "\nChecking top-level let"; begin match letbind with - | LB_val (P_aux (P_typ (typ_annot, pat), _), bind) -> + | LB_val (P_aux (P_typ (typ_annot, _), _) as pat, bind) -> let checked_bind = propagate_exp_effect (crule check_exp orig_env (strip_exp bind) typ_annot) in let tpat, env = bind_pat_no_guard orig_env (strip_pat pat) typ_annot in if (BESet.is_empty (effect_set (effect_of checked_bind)) || !opt_no_effects) then - [DEF_val (LB_aux (LB_val (P_aux (P_typ (typ_annot, tpat), (l, Some (orig_env, typ_annot, no_effect))), checked_bind), (l, None)))], env + [DEF_val (LB_aux (LB_val (tpat, checked_bind), (l, None)))], env else typ_error l ("Top-level definition with effects " ^ string_of_effect (effect_of checked_bind)) | LB_val (pat, bind) -> let inferred_bind = propagate_exp_effect (irule infer_exp orig_env (strip_exp bind)) in @@ -3650,7 +3667,10 @@ let check_val_spec env (VS_aux (vs, (l, _))) = let (id, quants, typ, env) = match vs with | VS_val_spec (TypSchm_aux (TypSchm_ts (quants, typ), _) as typschm, id, ext_opt, is_cast) -> typ_debug ("VS typschm: " ^ string_of_id id ^ ", " ^ string_of_typschm typschm); - let env = match ext_opt "smt" with Some op -> Env.add_smt_op id op env | None -> env in + let env = match (ext_opt "smt", ext_opt "#") with + | Some op, None -> Env.add_smt_op id op env + | _, _ -> env + in Env.wf_typ (add_typquant quants env) typ; typ_debug "CHECKED WELL-FORMED VAL SPEC"; let env = |