diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/gen_lib/power_extras.lem | 2 | ||||
| -rw-r--r-- | src/gen_lib/sail_values.lem | 11 | ||||
| -rw-r--r-- | src/gen_lib/state.lem | 12 | ||||
| -rw-r--r-- | src/pretty_print.ml | 41 | ||||
| -rw-r--r-- | src/test/power.sail | 2 |
5 files changed, 44 insertions, 24 deletions
diff --git a/src/gen_lib/power_extras.lem b/src/gen_lib/power_extras.lem index 8515a406..2883c810 100644 --- a/src/gen_lib/power_extras.lem +++ b/src/gen_lib/power_extras.lem @@ -36,7 +36,7 @@ let EIEIO_Sync () = return () let recalculate_dependency () = return () -let trap () = () +let trap () = exit () (* this needs to change, but for that we'd have to make the type checker know about trap * as an effect *) diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index ace65b3b..fa2afe23 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -434,18 +434,25 @@ let eq (l,r) = bool_to_bit (l = r) let eq_vec_range (l,r) = eq (to_num false l,r) let eq_range_vec (l,r) = eq (l, to_num false r) let eq_vec_vec (l,r) = eq (to_num true l, to_num true r) - -let neq (l,r) = bitwise_not_bit (eq (l,r)) +(* +let neq (l,r) = bitwise_not_bit (eq (l,r)) *) let neq_vec (l,r) = bitwise_not_bit (eq_vec_vec (l,r)) let neq_vec_range (l,r) = bitwise_not_bit (eq_vec_range (l,r)) let neq_range_vec (l,r) = bitwise_not_bit (eq_range_vec (l,r)) +(* temporarily *) +val neq : forall 'a 'b. 'a * 'b -> bit +let neq _ = O + + let EXTS (v1,(V _ _ is_inc as v)) = to_vec is_inc (v1,signed v) let EXTZ = EXTS +let exts = EXTS + val make_indexed_vector_reg : list (integer * register) -> maybe register -> integer -> integer -> vector register let make_indexed_vector_reg entries default start length = diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem index b5b0c37f..983d14c6 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -130,23 +130,23 @@ let rec foreach_dec (i,stop,by) vars body = else ((),vars) -val foreachState_inc : forall 's 'e 'vars. (integer * integer * integer) -> 'vars -> +val foreachM_inc : forall 's 'e 'vars. (integer * integer * integer) -> 'vars -> (integer -> 'vars -> State 's 'e (unit * 'vars)) -> State 's 'e (unit * 'vars) -let rec foreachState_inc (i,stop,by) vars body = +let rec foreachM_inc (i,stop,by) vars body = if i <= stop then body i vars >>= fun (_,vars) -> - foreachState_inc (i + by,stop,by) vars body + foreachM_inc (i + by,stop,by) vars body else return ((),vars) -val foreachState_dec : forall 's 'e 'vars. (integer * integer * integer) -> 'vars -> +val foreachM_dec : forall 's 'e 'vars. (integer * integer * integer) -> 'vars -> (integer -> 'vars -> State 's 'e (unit * 'vars)) -> State 's 'e (unit * 'vars) -let rec foreachState_dec (i,stop,by) vars body = +let rec foreachM_dec (i,stop,by) vars body = if i >= stop then body i vars >>= fun (_,vars) -> - foreachState_dec (i - by,stop,by) vars body + foreachM_dec (i - by,stop,by) vars body else return ((),vars) val read_reg_field : forall 'e. register -> register_field -> State state 'e (vector bit) diff --git a/src/pretty_print.ml b/src/pretty_print.ml index 71b03c52..b31838d9 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -2063,17 +2063,18 @@ let doc_id_lem_type (Id_aux(i,_)) = * token in case of x ending with star. *) parens (separate space [colon; string x; empty]) -let doc_id_lem_ctor aexp_needed (Id_aux(i,_)) = +let doc_id_lem_ctor (Id_aux(i,_)) = match i with | Id("bit") -> string "bit" | Id("int") -> string "integer" | Id("nat") -> string "integer" + | Id("Some") -> string "Just" + | Id("None") -> string "Nothing" | Id i -> string (fix_id (String.capitalize i)) | DeIid x -> (* add an extra space through empty to avoid a closing-comment * token in case of x ending with star. *) - let epp = separate space [colon; string (String.capitalize x); empty] in - if aexp_needed then parens (align epp) else epp + separate space [colon; string (String.capitalize x); empty] let doc_typ_lem, doc_atomic_typ_lem = (* following the structure of parser for precedence *) @@ -2162,13 +2163,13 @@ let rec doc_pat_lem apat_needed regtypes (P_aux (p,(l,annot)) as pa) = match p w | P_app(id, ((_ :: _) as pats)) -> (match annot with | Base(_,(Constructor _ | Enum _),_,_,_,_) -> - let ppp = doc_unop (doc_id_lem_ctor true id) + let ppp = doc_unop (doc_id_lem_ctor id) (parens (separate_map comma (doc_pat_lem true regtypes) pats)) in if apat_needed then parens ppp else ppp | _ -> empty) | P_app(id,[]) -> (match annot with - | Base(_,(Constructor _| Enum _),_,_,_,_) -> doc_id_lem_ctor apat_needed id + | Base(_,(Constructor _| Enum _),_,_,_,_) -> doc_id_lem_ctor id | _ -> empty) | P_lit lit -> doc_lit_lem true lit annot | P_wild -> underscore @@ -2327,8 +2328,13 @@ let doc_exp_lem, doc_let_lem = | _ -> (match annot with | Base (_,Constructor _,_,_,_,_) -> - let epp = doc_id_lem f ^^ space ^^ - parens (separate_map comma (top_exp (regs,regtypes) true) args) in + let epp = + match args with + | [] -> doc_id_lem_ctor f + | [arg] -> doc_id_lem_ctor f ^^ space ^^ exp arg + | _ -> + doc_id_lem_ctor f ^^ space ^^ + parens (separate_map comma exp args) in if aexp_needed then parens (align epp) else epp | Base (_,External (Some "bitwise_not_bit"),_,_,_,_) -> let [a] = args in @@ -2339,7 +2345,7 @@ let doc_exp_lem, doc_let_lem = | Base(_,External (Some n),_,_,_,_) -> (match n with | _ -> string n) - | Base(_,Constructor _,_,_,_,_) -> doc_id_lem_ctor false f + | Base(_,Constructor _,_,_,_,_) -> doc_id_lem_ctor f | _ -> doc_id_lem f in let epp = align @@ -2389,9 +2395,12 @@ let doc_exp_lem, doc_let_lem = (match annot with | Base((_, ({t = Tapp("register",_)} | {t=Tabbrev(_,{t=Tapp("register",_)})})), External _,_,eff,_,_) -> + if has_rreg_effect eff then separate space [string "read_reg";doc_id_lem id] - | Base(_,(Constructor i |Enum i),_,_,_,_) -> doc_id_lem_ctor aexp_needed id - | Base((_,t),Alias alias_info,_,_,_,_) -> + else + doc_id_lem id + | Base(_,(Constructor i |Enum i),_,_,_,_) -> doc_id_lem_ctor id + | Base((_,t),Alias alias_info,_,eff,_,_) -> (match alias_info with | Alias_field(reg,field) -> let typ = match List.assoc reg regs with @@ -2408,7 +2417,11 @@ let doc_exp_lem, doc_let_lem = string (typ ^ "_" ^ field)] in if aexp_needed then parens (align epp) else epp | Alias_pair(reg1,reg2) -> - let epp = separate space [string "read_two_regs";string reg1;string reg2] in + let epp = + if has_rreg_effect eff then + separate space [string "read_two_regs";string reg1;string reg2] + else + separate space [string "RegisterPair";string reg1;string reg2] in if aexp_needed then parens (align epp) else epp | Alias_extract(reg,start,stop) -> let epp = @@ -2667,9 +2680,9 @@ let doc_exp_lem, doc_let_lem = (*TODO Upcase and downcase type and constructors as needed*) let doc_type_union_lem regtypes (Tu_aux(typ_u,_)) = match typ_u with - | Tu_ty_id(typ,id) -> separate space [pipe; doc_id_lem_ctor false id; string "of"; + | Tu_ty_id(typ,id) -> separate space [pipe; doc_id_lem_ctor id; string "of"; parens (doc_typ_lem regtypes typ)] - | Tu_id id -> separate space [pipe; doc_id_lem_ctor false id] + | Tu_id id -> separate space [pipe; doc_id_lem_ctor id] let rec doc_range_lem (BF_aux(r,_)) = match r with | BF_single i -> parens (doc_op comma (doc_int i) (doc_int i)) @@ -2693,7 +2706,7 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with (concat [string "type"; space; doc_id_lem_type id;]) (doc_typquant_lem typq ar_doc) | TD_enum(id,nm,enums,_) -> - let enums_doc = group (separate_map (break 1 ^^ pipe ^^ space) (doc_id_lem_ctor false) enums) in + let enums_doc = group (separate_map (break 1 ^^ pipe ^^ space) doc_id_lem_ctor enums) in doc_op equals (concat [string "type"; space; doc_id_lem_type id;]) (enums_doc) diff --git a/src/test/power.sail b/src/test/power.sail index 3c9a13e3..20e23cb9 100644 --- a/src/test/power.sail +++ b/src/test/power.sail @@ -490,7 +490,7 @@ function forall Nat 'n. (bit['n]) zero_or_undef ((bit['n]) x) = { scattered function unit execute scattered typedef ast = const union -val bit[32] -> ast effect pure decode +val bit[32] -> ast effect {escape} decode scattered function ast decode |