diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast_util.ml | 2 | ||||
| -rw-r--r-- | src/spec_analysis.ml | 2 | ||||
| -rw-r--r-- | src/test/pattern.sail | 4 | ||||
| -rw-r--r-- | src/type_check.ml | 23 | ||||
| -rw-r--r-- | src/type_check.mli | 5 |
5 files changed, 31 insertions, 5 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml index 2109175f..2f958507 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -319,6 +319,8 @@ and string_of_lexp (LEXP_aux (lexp, _)) = | LEXP_cast (typ, v) -> "(" ^ string_of_typ typ ^ ") " ^ string_of_id v | LEXP_tup lexps -> "(" ^ string_of_list ", " string_of_lexp lexps ^ ")" | LEXP_vector (lexp, exp) -> string_of_lexp lexp ^ "[" ^ string_of_exp exp ^ "]" + | LEXP_vector_range (lexp, exp1, exp2) -> + 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" diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml index fdd56ecc..1475da7a 100644 --- a/src/spec_analysis.ml +++ b/src/spec_analysis.ml @@ -238,7 +238,7 @@ let rec fv_of_typ consider_var bound used (Typ_aux (t,_)) : Nameset.t = | Typ_fn(arg,ret,_) -> fv_of_typ consider_var bound (fv_of_typ consider_var bound used arg) ret | Typ_tup ts -> List.fold_right (fun t n -> fv_of_typ consider_var bound n t) ts used | Typ_app(id,targs) -> - List.fold_right (fun ta n -> fv_of_targ consider_var bound n ta) targs (conditional_add_typ bound used id) + List.fold_right (fun ta n -> fv_of_targ consider_var bound n ta) targs (conditional_add_typ bound used id) and fv_of_targ consider_var bound used (Ast.Typ_arg_aux(targ,_)) : Nameset.t = match targ with | Typ_arg_typ t -> fv_of_typ consider_var bound used t diff --git a/src/test/pattern.sail b/src/test/pattern.sail index cabe7dad..97e5a0ef 100644 --- a/src/test/pattern.sail +++ b/src/test/pattern.sail @@ -4,9 +4,9 @@ register nat x register nat y typedef wordsize = forall Nat 'n, 'n IN {8,16,32}. [|'n|] -let forall Nat 'n. (wordsize<'n>) word = 8 +(* let forall Nat 'n. (wordsize<'n>) word = 8 *) -function nat main _ = { +function nat main () = { (* works - x and y are set to 42 *) n := 1; diff --git a/src/type_check.ml b/src/type_check.ml index 8f237411..4dc22b41 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -932,6 +932,21 @@ let is_exist = function | Typ_aux (Typ_exist (_, _, _), _) -> true | _ -> false +let exist_typ constr typ = + let fresh_kid = fresh_existential () in + mk_typ (Typ_exist ([fresh_kid], constr fresh_kid, typ fresh_kid)) + +let destruct_vector_typ env typ = + let destruct_vector_typ' = function + | Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp n1, _); + Typ_arg_aux (Typ_arg_nexp n2, _); + Typ_arg_aux (Typ_arg_order o, _); + Typ_arg_aux (Typ_arg_typ vtyp, _)] + ), _) when string_of_id id = "vector" -> Some (n1, n2, o, vtyp) + | typ -> None + in + destruct_vector_typ' (Env.expand_synonyms env typ) + (**************************************************************************) (* 3. Subtyping and constraint solving *) (**************************************************************************) @@ -2349,9 +2364,13 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = match is_range (typ_of inferred_f), is_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 checked_body = crule check_exp (Env.add_local v (Immutable, range_typ l1 u2) env) body unit_typ in + | 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 + 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 checked_body = crule check_exp (Env.add_local v (Immutable, range_typ l1 u2) env) body unit_typ in + annot_exp (E_for (v, inferred_f, inferred_t, checked_step, ord, checked_body)) unit_typ *) | _, _ -> typ_error l "Ranges in foreach overlap" end | E_if (cond, then_branch, else_branch) -> diff --git a/src/type_check.mli b/src/type_check.mli index 54352b68..ce66aba3 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -153,6 +153,8 @@ val npow2 : nexp -> nexp val nvar : kid -> nexp val nid : id -> nexp +val nc_gteq : nexp -> nexp -> n_constraint + (* Sail builtin types. *) val int_typ : typ val nat_typ : typ @@ -165,6 +167,7 @@ val string_typ : typ val real_typ : typ val vector_typ : nexp -> nexp -> order -> typ -> typ val list_typ : typ -> typ +val exist_typ : (kid -> n_constraint) -> (kid -> typ) -> typ val inc_ord : order val dec_ord : order @@ -212,6 +215,8 @@ val effect_of_annot : tannot -> effect val destructure_atom_nexp : typ -> nexp +val destruct_vector_typ : Env.t -> typ -> (nexp * nexp * order * typ) option + type uvar = | U_nexp of nexp | U_order of order |