summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/initial_check.ml2
-rw-r--r--src/lem_interp/interp.lem11
-rw-r--r--src/pretty_print.ml29
-rw-r--r--src/process_file.ml2
-rw-r--r--src/test/pattern.sail10
-rw-r--r--src/type_check.ml21
-rw-r--r--src/type_internal.ml6
-rw-r--r--src/type_internal.mli3
8 files changed, 64 insertions, 20 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 2a80ff37..78e44bf0 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -482,7 +482,7 @@ let to_ast_typedef (names,k_env,t_env) (td:Parse_ast.type_def) : (tannot type_de
| Parse_ast.TD_abbrev(id,name_scm_opt,typschm) ->
let id = to_ast_id id in
let key = id_to_string id in
- let typschm,_,_ = to_ast_typschm k_env typschm in
+ let typschm,k_env,_ = to_ast_typschm k_env typschm in
let td_abrv = TD_aux(TD_abbrev(id,to_ast_namescm name_scm_opt,typschm),(l,None)) in
let typ = (match typschm with
| TypSchm_aux(TypSchm_ts(tq,typ), _) ->
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 8a9ebfe5..50d84556 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -621,7 +621,7 @@ and interp_main t_level l_env l_mem (E_aux exp (l,annot)) =
| E_lit lit ->
if is_lit_vector lit then (Value (litV_to_vec lit) Tag_empty,l_mem,l_env)
else (Value (V_lit lit) Tag_empty, l_mem,l_env)
- | E_cast typ exp ->
+ | E_cast ((Typ_aux typ _) as ctyp) exp ->
resolve_outcome (interp_main t_level l_env l_mem exp)
(fun v lm le ->
match (tag,v) with
@@ -629,8 +629,15 @@ and interp_main t_level l_env l_mem (E_aux exp (l,annot)) =
(Action (Read_reg regform Nothing)
(Frame (id_of_string "0")
(E_aux (E_id (id_of_string "0")) (Unknown, (val_annot (reg_to_t regform)))) le lm Top), lm,le)
+ | (_,V_vector start inc items) ->
+ (match typ with
+ | Typ_app (Id_aux (Id "vector") _) [Typ_arg_aux (Typ_arg_nexp(Nexp_aux (Nexp_constant i) _)) _;_;_;_] ->
+ if start = i
+ then (Value v tag,lm,le)
+ else (Value (V_vector i inc items) tag,lm,le)
+ | _ -> (Value v tag,lm,le) end)
| _ -> (Value v Tag_empty,lm,le) end)
- (fun a -> update_stack a (add_to_top_frame (fun e -> (E_aux (E_cast typ e) (l,annot)))))
+ (fun a -> update_stack a (add_to_top_frame (fun e -> (E_aux (E_cast ctyp e) (l,annot)))))
(* TODO introduce coercions to change offset of vectors *)
| E_id id ->
let name = get_id id in
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 84efbf56..e78f3a09 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -210,7 +210,7 @@ let rec pp_let ppf (LB_aux(lb,_)) =
| LB_val_implicit(pat,exp) -> fprintf ppf "@[<0>%a %a %a@ %a@]" kwd "let" pp_pat_atomic pat kwd " =" pp_exp exp
(* Need an is_atomic? check and insert parens otherwise *)
-and pp_exp ppf (E_aux(e,_)) =
+and pp_exp ppf (E_aux(e,(_,annot))) =
match e with
| E_block(exps) -> fprintf ppf "@[<0>%a%a@ %a@]"
kwd "{"
@@ -220,9 +220,14 @@ and pp_exp ppf (E_aux(e,_)) =
| E_lit(lit) -> pp_lit ppf lit
| E_cast(typ,exp) -> fprintf ppf "@[<0>%a%a%a %a@]" kwd "(" pp_typ typ kwd ")" pp_exp exp
| E_internal_cast((_,None),e) -> pp_exp ppf e
- | E_internal_cast((_,Some((_,t),_,_,_)), exp) ->
- (*check if the internal exp has the same vector start as the annot, and if so, drop *)
- fprintf ppf "@[<0>%a%a%a %a@]" kwd "(" pp_typ (t_to_typ t) kwd ")" pp_exp exp
+ | E_internal_cast((_,Some((_,t),_,_,_)), (E_aux(_,(_,eannot)) as exp)) ->
+ (match t.t,eannot with
+ | Tapp("vector",[TA_nexp n1;_;_;_]),Some((_,{t=Tapp("vector",[TA_nexp n2;_;_;_])}),_,_,_) ->
+ if nexp_eq n1 n2
+ then pp_exp ppf exp
+ else
+ fprintf ppf "@[<0>%a%a%a %a@]" kwd "(" pp_typ (t_to_typ t) kwd ")" pp_exp exp
+ | _ -> fprintf ppf "@[<0>%a%a%a %a@]" kwd "(" pp_typ (t_to_typ t) kwd ")" pp_exp exp)
| E_app(f,args) -> fprintf ppf "@[<0>%a(%a)@]" pp_id f (list_pp pp_comma_exp pp_exp) args
| E_app_infix(l,op,r) -> fprintf ppf "@[<0>%a %a %a@]" pp_exp l pp_id op pp_exp r
| E_tuple(exps) -> fprintf ppf "@[<0>%a %a %a@]" kwd "(" (list_pp pp_comma_exp pp_exp) exps kwd ")"
@@ -536,7 +541,7 @@ let rec pp_format_t t =
| Ttup(tups) -> "(T_tup [" ^ (list_format "; " pp_format_t tups) ^ "])"
| Tapp(i,args) -> "(T_app (Id_aux (Id \"" ^ i ^ "\") Unknown) (T_args [" ^ list_format "; " pp_format_targ args ^ "]))"
| Tabbrev(ti,ta) -> "(T_abbrev " ^ (pp_format_t ti) ^ " " ^ (pp_format_t ta) ^ ")"
- | Tuvar(_) -> "(T_var (Kid_aux (Var \"fresh_v\") Unknown))"
+ | Tuvar(_) -> assert false (*"(T_var (Kid_aux (Var \"fresh_v\") Unknown))"*)
and pp_format_targ = function
| TA_typ t -> "(T_arg_typ " ^ pp_format_t t ^ ")"
| TA_nexp n -> "(T_arg_nexp " ^ pp_format_n n ^ ")"
@@ -550,7 +555,7 @@ and pp_format_n n =
| Nmult(n1,n2) -> "(Ne_mult " ^ (pp_format_n n1) ^ " " ^ (pp_format_n n2) ^ ")"
| N2n n -> "(Ne_exp " ^ (pp_format_n n) ^ ")"
| Nneg n -> "(Ne_unary " ^ (pp_format_n n) ^ ")"
- | Nuvar(_) -> "(Ne_var (Kid_aux (Var \"fresh_v\") Unknown))"
+ | Nuvar _ -> "(Ne_var (Kid_aux (Var \"fresh_v_" ^ string_of_int (get_index n) ^ "\") Unknown))"
and pp_format_e e =
"(Effect_aux " ^
(match e.effect with
@@ -633,7 +638,7 @@ let rec pp_lem_let ppf (LB_aux(lb,(l,annot))) =
fprintf ppf "@[<0>(LB_aux %a (%a, %a))@]" print_lb lb pp_lem_l l pp_annot annot
and pp_lem_exp ppf (E_aux(e,(l,annot))) =
- let print_e ppf e =
+ let rec print_e ppf e =
match e with
| E_block(exps) -> fprintf ppf "@[<0>%a [%a] %a@]"
kwd "(E_block"
@@ -643,9 +648,13 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) =
| E_lit(lit) -> fprintf ppf "(%a %a)" kwd "E_lit" pp_lem_lit lit
| E_cast(typ,exp) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_cast" pp_lem_typ typ pp_lem_exp exp
| E_internal_cast((_,None),e) -> pp_lem_exp ppf e
- | E_internal_cast((_,Some((_,t),_,_,_)), exp) ->
- (*check if the internal exp has the same vector start as the annot, and if so, drop *)
- fprintf ppf "@[<0>(E_cast %a %a)@]" pp_lem_typ (t_to_typ t) pp_lem_exp exp
+ | E_internal_cast((_,Some((_,t),_,_,_)), (E_aux(ec,(_,eannot)) as exp)) ->
+ (match t.t,eannot with
+ | Tapp("vector",[TA_nexp n1;_;_;_]),Some((_,{t=Tapp("vector",[TA_nexp n2;_;_;_])}),_,_,_) ->
+ if nexp_eq n1 n2
+ then print_e ppf ec
+ else fprintf ppf "@[<0>(E_cast %a %a)@]" pp_lem_typ (t_to_typ t) pp_lem_exp exp
+ | _ -> fprintf ppf "@[<0>(E_cast %a %a)@]" pp_lem_typ (t_to_typ t) pp_lem_exp exp)
| E_app(f,args) -> fprintf ppf "@[<0>(%a %a [%a])@]" kwd "E_app" pp_lem_id f (list_pp pp_semi_lem_exp pp_lem_exp) args
| E_app_infix(l,op,r) -> fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "E_app_infix" pp_lem_exp l pp_lem_id op pp_lem_exp r
| E_tuple(exps) -> fprintf ppf "@[<0>%a [%a] %a@]" kwd "(E_tuple" (list_pp pp_semi_lem_exp pp_lem_exp) exps kwd ")"
diff --git a/src/process_file.ml b/src/process_file.ml
index 57024bb4..26fc1f22 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -112,7 +112,7 @@ let close_output_with_check (o, temp_file_name, file_name) =
()
let generated_line f =
- Printf.sprintf "Generated by XX from %s." f
+ Printf.sprintf "Generated by Sail from %s." f
(*let tex_preamble =
"\\documentclass{article}\n" ^
diff --git a/src/test/pattern.sail b/src/test/pattern.sail
index bc04590d..7bbfebf9 100644
--- a/src/test/pattern.sail
+++ b/src/test/pattern.sail
@@ -3,6 +3,9 @@ register nat n
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
+
function nat main _ = {
(* works - x and y are set to 42 *)
@@ -14,7 +17,12 @@ function nat main _ = {
case z -> { x := 99; x }
});
- (* doesn't work - main returns 1 instead of 99 *)
+ switch word {
+ case 8 -> { x:= 32; }
+ case 16 -> { x:= 64; }
+ case 32 -> { x:= 128; }
+ };
+
n := 3;
switch n {
case 0 -> { 21 }
diff --git a/src/type_check.ml b/src/type_check.ml
index b3836761..d9c38a08 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -391,11 +391,16 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
let tannot = Some(([],t),Emp_local,cs,ef) in
let t',cs',e' = type_coerce l d_env t' (rebuild tannot) expect_t' in
(e',t,t_env,cs@cs',ef)
- | Tapp("register",[TA_typ(t')]),_ ->
+ | Tapp("register",[TA_typ(t')]),Tuvar _ ->
let ef' = add_effect (BE_aux(BE_rreg,l)) ef in
let tannot = Some(([],t),External (Some i),cs,ef') in
let t',cs',e' = type_coerce l d_env t' (rebuild tannot) expect_actual in
(e',t,t_env,cs@cs',ef)
+ | Tapp("register",[TA_typ(t')]),_ ->
+ let ef' = add_effect (BE_aux(BE_rreg,l)) ef in
+ let tannot = Some(([],t),External (Some i),cs,ef') in
+ let t',cs',e' = type_coerce l d_env t' (rebuild tannot) expect_actual in
+ (e',t',t_env,cs@cs',ef)
| Tapp("reg",[TA_typ(t')]),_ ->
let tannot = Some(([],t),Emp_local,cs,pure_e) in
let t',cs',e' = type_coerce l d_env t' (rebuild tannot) expect_actual in
@@ -832,9 +837,15 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
| records -> typ_error l ("Multiple structs contain field " ^ fi ^ ", try adding a cast to disambiguate"))
| _ -> typ_error l ("Expected a struct or register for access but found an expression of type " ^ t_to_string t'))
| E_case(exp,pexps) ->
- let check_t = new_t() in
- let (e',t',_,cs,ef) = check_exp envs check_t exp in
- let (pexps',t,cs',ef') = check_cases envs check_t expect_t pexps in
+ (*let check_t = new_t() in*)
+ let (e',t',_,cs,ef) = check_exp envs (new_t()) exp in
+ (*let _ = Printf.printf "Type of pattern after expression check %s\n" (t_to_string t') in*)
+ let t' =
+ match t'.t with
+ | Tapp("register",[TA_typ t]) -> t
+ | _ -> t' in
+ (*let _ = Printf.printf "Type of pattern after register check %s\n" (t_to_string t') in*)
+ let (pexps',t,cs',ef') = check_cases envs t' expect_t pexps in
(E_aux(E_case(e',pexps'),(l,Some(([],t),Emp_local,[],pure_e))),t,t_env,cs@cs',union_effects ef ef')
| E_let(lbind,body) ->
let (lb',t_env',cs,ef) = (check_lbind envs Emp_local lbind) in
@@ -866,7 +877,7 @@ and check_cases envs check_t expect_t pexps : ((tannot pexp) list * typ * nexp_r
let (e,t,_,cs2,ef2) = check_exp (Env(d_env,Envmap.union_merge (tannot_merge l d_env) t_env env)) expect_t exp in
[Pat_aux(Pat_exp(pat',e),(l,Some(([],t),Emp_local,cs_p@cs_p'@cs2,ef2)))],t,cs_p@cs_p'@cs2,ef2
| ((Pat_aux(Pat_exp(pat,exp),(l,annot)))::pexps) ->
- let pat',env,cs_p,u = check_pattern envs Emp_local (new_t ()) pat in
+ let pat',env,cs_p,u = check_pattern envs Emp_local check_t pat in
let t',cs_p' = type_consistent l d_env u check_t in
let (e,t,_,cs2,ef2) = check_exp (Env(d_env,Envmap.union_merge (tannot_merge l d_env) t_env env)) expect_t exp in
let (pes,t'',csl,efl) = check_cases envs check_t expect_t pexps in
diff --git a/src/type_internal.ml b/src/type_internal.ml
index f958803a..45b89f3b 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -92,6 +92,11 @@ type def_envs = {
type exp = tannot Ast.exp
+let get_index n =
+ match n.nexp with
+ | Nuvar {nindex = i} -> i
+ | _ -> assert false
+
let rec string_of_list sep string_of = function
| [] -> ""
| [x] -> string_of x
@@ -772,6 +777,7 @@ let nexp_eq n1 n2 =
When considering two range type applications, will check for consistency instead of equality*)
(*TODOTODO when t1 range and t2 a tuvar or t2 an range with nuvars, need to not copy directly but issue bound (not eq) constraints for pattern matching against multiple constants ... possibly an in constraint for constants, and then when considering constraints, merge various in statements for same variable *)
let rec type_consistent_internal l d_env t1 cs1 t2 cs2 =
+ (*let _ = Printf.printf "type_consistent_internal called with %s and %s\n" (t_to_string t1) (t_to_string t2) in*)
let t1,cs1',_ = get_abbrev d_env t1 in
let t2,cs2',_ = get_abbrev d_env t2 in
let cs1,cs2 = cs1@cs1',cs2@cs2' in
diff --git a/src/type_internal.mli b/src/type_internal.mli
index eec077d6..71b72856 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -118,6 +118,7 @@ val subst : (string * kind) list -> t -> nexp_range list -> effect -> t * nexp_r
val get_abbrev : def_envs -> t -> (t * nexp_range list * effect)
val eval_nexp : nexp -> nexp
+val get_index : nexp -> int (*TEMPORARILY expose nindex through this for debugging purposes*)
(*May raise an exception if a contradiction is found*)
val resolve_constraints : nexp_range list -> nexp_range list
@@ -125,6 +126,8 @@ val resolve_constraints : nexp_range list -> nexp_range list
(*May raise an exception if effects do not match tannot effects, will lift unification variables to fresh type variables *)
val check_tannot : Parse_ast.l -> tannot -> nexp_range list -> effect -> tannot
+val nexp_eq : nexp -> nexp -> bool
+
(* type_consistent is similar to a standard type equality, except in the case of [[consistent t1 t2]] where
t1 and t2 are both enum types and t1 is contained within the range of t2: i.e.
enum 2 5 is consistent with enum 0 10, but not vice versa.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 11:12:55 +0000