summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/ast_util.ml48
-rw-r--r--src/ast_util.mli13
-rw-r--r--src/pretty_print_lem_new_tc.ml1385
-rw-r--r--src/rewriter_new_tc.ml304
-rw-r--r--src/rewriter_new_tc.mli1
-rw-r--r--src/type_check_new.ml29
-rw-r--r--src/type_check_new.mli2
7 files changed, 1596 insertions, 186 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml
index d8e1e7a6..3eb5ddf0 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -10,6 +10,7 @@
(* Christopher Pulte *)
(* Peter Sewell *)
(* Alasdair Armstrong *)
+(* Thomas Bauereiss *)
(* *)
(* All rights reserved. *)
(* *)
@@ -335,3 +336,50 @@ module Id = struct
| Id_aux (Id _, _), Id_aux (DeIid _, _) -> -1
| Id_aux (DeIid _, _), Id_aux (Id _, _) -> 1
end
+
+let rec is_number (Typ_aux (t,_)) =
+ match t with
+ | Typ_app (Id_aux (Id "range", _),_)
+ | Typ_app (Id_aux (Id "implicit", _),_)
+ | Typ_app (Id_aux (Id "atom", _),_) -> true
+ | _ -> false
+
+let rec is_vector_typ = function
+ | Typ_aux (Typ_app (Id_aux (Id "vector",_), [_;_;_;_]), _) -> true
+ | Typ_aux (Typ_app (Id_aux (Id "register",_), [Typ_arg_aux (Typ_arg_typ rtyp,_)]), _) ->
+ is_vector_typ rtyp
+ | _ -> false
+
+let typ_app_args_of = function
+ | Typ_aux (Typ_app (Id_aux (Id c,_), targs), l) ->
+ (c, List.map (fun (Typ_arg_aux (a,_)) -> a) targs, l)
+ | Typ_aux (_, l) -> raise (Reporting_basic.err_typ l "typ_app_args_of called on non-app type")
+
+let rec vector_typ_args_of typ = match typ_app_args_of typ with
+ | ("vector", [Typ_arg_nexp start; Typ_arg_nexp len; Typ_arg_order ord; Typ_arg_typ etyp], _) ->
+ (start, len, ord, etyp)
+ | ("register", [Typ_arg_typ rtyp], _) -> vector_typ_args_of rtyp
+ | (_, _, l) -> raise (Reporting_basic.err_typ l "vector_typ_args_of called on non-vector type")
+
+let is_order_inc = function
+ | Ord_aux (Ord_inc, _) -> true
+ | Ord_aux (Ord_dec, _) -> false
+ | Ord_aux (Ord_var _, l) ->
+ raise (Reporting_basic.err_unreachable l "is_order_inc called on vector with variable ordering")
+
+let is_bit_typ = function
+ | Typ_aux (Typ_id (Id_aux (Id "bit", _)), _) -> true
+ | _ -> false
+
+let is_bitvector_typ typ =
+ if is_vector_typ typ then
+ let (_,_,_,etyp) = vector_typ_args_of typ in
+ is_bit_typ etyp
+ else false
+
+let has_effect (Effect_aux (eff,_)) searched_for = match eff with
+ | Effect_set effs ->
+ List.exists (fun (BE_aux (be,_)) -> be = searched_for) effs
+ | Effect_var _ ->
+ raise (Reporting_basic.err_unreachable Parse_ast.Unknown
+ "has_effect called on effect variable")
diff --git a/src/ast_util.mli b/src/ast_util.mli
index 9d6c5653..8902c39c 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -10,6 +10,7 @@
(* Christopher Pulte *)
(* Peter Sewell *)
(* Alasdair Armstrong *)
+(* Thomas Bauereiss *)
(* *)
(* All rights reserved. *)
(* *)
@@ -94,3 +95,15 @@ module BE : sig
type t = base_effect
val compare : base_effect -> base_effect -> int
end
+
+val is_number : typ -> bool
+val is_vector_typ : typ -> bool
+val is_bit_typ : typ -> bool
+val is_bitvector_typ : typ -> bool
+
+val typ_app_args_of : typ -> string * typ_arg_aux list * Ast.l
+val vector_typ_args_of : typ -> nexp * nexp * order * typ
+
+val is_order_inc : order -> bool
+
+val has_effect : effect -> base_effect_aux -> bool
diff --git a/src/pretty_print_lem_new_tc.ml b/src/pretty_print_lem_new_tc.ml
new file mode 100644
index 00000000..443695d3
--- /dev/null
+++ b/src/pretty_print_lem_new_tc.ml
@@ -0,0 +1,1385 @@
+(**************************************************************************)
+(* Sail *)
+(* *)
+(* Copyright (c) 2013-2017 *)
+(* Kathyrn Gray *)
+(* Shaked Flur *)
+(* Stephen Kell *)
+(* Gabriel Kerneis *)
+(* Robert Norton-Wright *)
+(* Christopher Pulte *)
+(* Peter Sewell *)
+(* Thomas Bauereiss *)
+(* *)
+(* All rights reserved. *)
+(* *)
+(* This software was developed by the University of Cambridge Computer *)
+(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *)
+(* (REMS) project, funded by EPSRC grant EP/K008528/1. *)
+(* *)
+(* Redistribution and use in source and binary forms, with or without *)
+(* modification, are permitted provided that the following conditions *)
+(* are met: *)
+(* 1. Redistributions of source code must retain the above copyright *)
+(* notice, this list of conditions and the following disclaimer. *)
+(* 2. Redistributions in binary form must reproduce the above copyright *)
+(* notice, this list of conditions and the following disclaimer in *)
+(* the documentation and/or other materials provided with the *)
+(* distribution. *)
+(* *)
+(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *)
+(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *)
+(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *)
+(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *)
+(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *)
+(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *)
+(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *)
+(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *)
+(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *)
+(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *)
+(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *)
+(* SUCH DAMAGE. *)
+(**************************************************************************)
+
+open Type_check_new
+open Ast
+open Ast_util
+open Rewriter_new_tc
+open Big_int
+open PPrint
+open Pretty_print_common
+
+(****************************************************************************
+ * PPrint-based sail-to-lem pprinter
+****************************************************************************)
+
+let print_to_from_interp_value = ref false
+let langlebar = string "<|"
+let ranglebar = string "|>"
+let anglebars = enclose langlebar ranglebar
+
+let fix_id name = match name with
+ | "assert"
+ | "lsl"
+ | "lsr"
+ | "asr"
+ | "type"
+ | "fun"
+ | "function"
+ | "raise"
+ | "try"
+ | "match"
+ | "with"
+ | "field"
+ | "LT"
+ | "GT"
+ | "EQ"
+ | "integer"
+ -> name ^ "'"
+ | _ -> name
+
+let is_number char =
+ char = '0' || char = '1' || char = '2' || char = '3' || char = '4' || char = '5' ||
+ char = '6' || char = '7' || char = '8' || char = '9'
+
+let doc_id_lem (Id_aux(i,_)) =
+ match i with
+ | Id i ->
+ (* this not the right place to do this, just a workaround *)
+ if i.[0] = '\'' then
+ string ((String.sub i 1 (String.length i - 1)) ^ "'")
+ else if is_number(i.[0]) then
+ string ("v" ^ i ^ "'")
+ else
+ string (fix_id i)
+ | DeIid x ->
+ (* add an extra space through empty to avoid a closing-comment
+ * token in case of x ending with star. *)
+ parens (separate space [colon; string x; empty])
+
+let doc_id_lem_type (Id_aux(i,_)) =
+ match i with
+ | Id("int") -> string "ii"
+ | Id("nat") -> string "ii"
+ | Id("option") -> string "maybe"
+ | Id i -> string (fix_id i)
+ | DeIid x ->
+ (* add an extra space through empty to avoid a closing-comment
+ * token in case of x ending with star. *)
+ parens (separate space [colon; string x; empty])
+
+let doc_id_lem_ctor (Id_aux(i,_)) =
+ match i with
+ | Id("bit") -> string "bitU"
+ | 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. *)
+ separate space [colon; string (String.capitalize x); empty]
+
+let effectful_set =
+ List.exists
+ (fun (BE_aux (eff,_)) ->
+ match eff with
+ | BE_rreg | BE_wreg | BE_rmem | BE_rmemt | BE_wmem | BE_eamem
+ | BE_exmem | BE_wmv | BE_wmvt | BE_barr | BE_depend | BE_nondet
+ | BE_escape -> true
+ | _ -> false)
+
+let effectful (Effect_aux (eff,_)) =
+ match eff with
+ | Effect_var _ -> failwith "effectful: Effect_var not supported"
+ | Effect_set effs -> effectful_set effs
+
+let doc_typ_lem, doc_atomic_typ_lem =
+ (* following the structure of parser for precedence *)
+ let rec typ regtypes ty = fn_typ regtypes true ty
+ and typ' regtypes ty = fn_typ regtypes false ty
+ and fn_typ regtypes atyp_needed ((Typ_aux (t, _)) as ty) = match t with
+ | Typ_fn(arg,ret,efct) ->
+ (*let exc_typ = string "string" in*)
+ let ret_typ =
+ if effectful efct
+ then separate space [string "M";(*parens exc_typ;*) fn_typ regtypes true ret]
+ else separate space [fn_typ regtypes false ret] in
+ let tpp = separate space [tup_typ regtypes true arg; arrow;ret_typ] in
+ (* once we have proper excetions we need to know what the exceptions type is *)
+ if atyp_needed then parens tpp else tpp
+ | _ -> tup_typ regtypes atyp_needed ty
+ and tup_typ regtypes atyp_needed ((Typ_aux (t, _)) as ty) = match t with
+ | Typ_tup typs ->
+ let tpp = separate_map (space ^^ star ^^ space) (app_typ regtypes false) typs in
+ if atyp_needed then parens tpp else tpp
+ | _ -> app_typ regtypes atyp_needed ty
+ and app_typ regtypes atyp_needed ((Typ_aux (t, _)) as ty) = match t with
+ | Typ_app(Id_aux (Id "vector", _), [
+ Typ_arg_aux (Typ_arg_nexp n, _);
+ Typ_arg_aux (Typ_arg_nexp m, _);
+ Typ_arg_aux (Typ_arg_order ord, _);
+ Typ_arg_aux (Typ_arg_typ elem_typ, _)]) ->
+ let tpp = match elem_typ with
+ | Typ_aux (Typ_id (Id_aux (Id "bit",_)),_) ->
+ let len = match m with
+ | (Nexp_aux(Nexp_constant i,_)) -> string "ty" ^^ doc_int i
+ | _ -> doc_nexp m in
+ string "bitvector" ^^ space ^^ len
+ | _ -> string "vector" ^^ space ^^ typ regtypes elem_typ in
+ if atyp_needed then parens tpp else tpp
+ | Typ_app(Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ etyp, _)]) ->
+ (* TODO: Better distinguish register names and contents?
+ The former are represented in the Lem library using a type
+ "register" (without parameters), the latter just using the content
+ type (e.g. "bitvector ty64"). We assume the latter is meant here
+ and drop the "register" keyword. *)
+ fn_typ regtypes atyp_needed etyp
+ | Typ_app(Id_aux (Id "range", _),_) ->
+ (string "integer")
+ | Typ_app(Id_aux (Id "implicit", _),_) ->
+ (string "integer")
+ | Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux(Typ_arg_nexp n,_)]) ->
+ (string "integer")
+ | Typ_app(id,args) ->
+ let tpp = (doc_id_lem_type id) ^^ space ^^ (separate_map space (doc_typ_arg_lem regtypes) args) in
+ if atyp_needed then parens tpp else tpp
+ | _ -> atomic_typ regtypes atyp_needed ty
+ and atomic_typ regtypes atyp_needed ((Typ_aux (t, _)) as ty) = match t with
+ | Typ_id (Id_aux (Id "bool",_)) -> string "bitU"
+ | Typ_id (Id_aux (Id "boolean",_)) -> string "bitU"
+ | Typ_id (Id_aux (Id "bit",_)) -> string "bitU"
+ | Typ_id (id) ->
+ if List.exists ((=) (string_of_id id)) regtypes
+ then string "register"
+ else doc_id_lem_type id
+ | Typ_var v -> doc_var v
+ | Typ_wild -> underscore
+ | Typ_app _ | Typ_tup _ | Typ_fn _ ->
+ (* exhaustiveness matters here to avoid infinite loops
+ * if we add a new Typ constructor *)
+ let tpp = typ regtypes ty in
+ if atyp_needed then parens tpp else tpp
+ and doc_typ_arg_lem regtypes (Typ_arg_aux(t,_)) = match t with
+ | Typ_arg_typ t -> app_typ regtypes true t
+ | Typ_arg_nexp n -> empty
+ | Typ_arg_order o -> empty
+ | Typ_arg_effect e -> empty
+ in typ', atomic_typ
+
+let doc_tannot_lem regtypes eff typ =
+ let ta = doc_typ_lem regtypes typ in
+ if eff then string " : M " ^^ parens ta
+ else string " : " ^^ ta
+
+(* doc_lit_lem gets as an additional parameter the type information from the
+ * expression around it: that's a hack, but how else can we distinguish between
+ * undefined values of different types ? *)
+let doc_lit_lem in_pat (L_aux(lit,l)) a =
+ utf8string (match lit with
+ | L_unit -> "()"
+ | L_zero -> "B0"
+ | L_one -> "B1"
+ | L_false -> "B0"
+ | L_true -> "B1"
+ | L_num i ->
+ let ipp = string_of_int i in
+ if in_pat then "("^ipp^":nn)"
+ else if i < 0 then "((0"^ipp^"):ii)"
+ else "("^ipp^":ii)"
+ | L_hex n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0x" ^ n) ^ ")" (*shouldn't happen*)*)
+ | L_bin n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0b" ^ n) ^ ")" (*shouldn't happen*)*)
+ | L_undef ->
+ (match a with
+ | Some (_, Typ_aux (t,_), _) ->
+ (match t with
+ | Typ_id (Id_aux (Id "bit", _))
+ | Typ_app (Id_aux (Id "register", _),_) -> "UndefinedRegister 0"
+ | Typ_id (Id_aux (Id "string", _)) -> "\"\""
+ | _ -> "(failwith \"undefined value of unsupported type\")")
+ | _ -> "(failwith \"undefined value of unsupported type\")")
+ | L_string s -> "\"" ^ s ^ "\"")
+
+(* typ_doc is the doc for the type being quantified *)
+
+let doc_typquant_lem (TypQ_aux(tq,_)) typ_doc = typ_doc
+
+let doc_typschm_lem regtypes (TypSchm_aux(TypSchm_ts(tq,t),_)) =
+ (doc_typquant_lem tq (doc_typ_lem regtypes t))
+
+let is_ctor env id = match Env.lookup_id id env with
+| Enum _ | Union _ -> true
+| _ -> false
+
+(*Note: vector concatenation, literal vectors, indexed vectors, and record should
+ be removed prior to pp. The latter two have never yet been seen
+*)
+let rec doc_pat_lem regtypes apat_needed (P_aux (p,(l,annot)) as pa) = match p with
+ | P_app(id, ((_ :: _) as pats)) ->
+ (match annot with
+ | Some (env, _, _) when (is_ctor env id) ->
+ let ppp = doc_unop (doc_id_lem_ctor id)
+ (parens (separate_map comma (doc_pat_lem regtypes true) pats)) in
+ if apat_needed then parens ppp else ppp
+ | _ -> empty)
+ | P_app(id,[]) ->
+ (match annot with
+ | Some (env, _, _) when (is_ctor env id) -> doc_id_lem_ctor id
+ | _ -> empty)
+ | P_lit lit -> doc_lit_lem true lit annot
+ | P_wild -> underscore
+ | P_id id ->
+ begin match id with
+ | Id_aux (Id "None",_) -> string "Nothing" (* workaround temporary issue *)
+ | _ -> doc_id_lem id end
+ | P_as(p,id) -> parens (separate space [doc_pat_lem regtypes true p; string "as"; doc_id_lem id])
+ | P_typ(typ,p) -> doc_op colon (doc_pat_lem regtypes true p) (doc_typ_lem regtypes typ)
+ | P_vector pats ->
+ let ppp =
+ (separate space)
+ [string "Vector";brackets (separate_map semi (doc_pat_lem regtypes true) pats);underscore;underscore] in
+ if apat_needed then parens ppp else ppp
+ | P_vector_concat pats ->
+ let ppp =
+ (separate space)
+ [string "Vector";parens (separate_map (string "::") (doc_pat_lem regtypes true) pats);underscore;underscore] in
+ if apat_needed then parens ppp else ppp
+ | P_tup pats ->
+ (match pats with
+ | [p] -> doc_pat_lem regtypes apat_needed p
+ | _ -> parens (separate_map comma_sp (doc_pat_lem regtypes false) pats))
+ | P_list pats -> brackets (separate_map semi (doc_pat_lem regtypes false) pats) (*Never seen but easy in lem*)
+ | P_record (_,_) | P_vector_indexed _ -> empty (* TODO *)
+
+let rec contains_bitvector_typ (Typ_aux (t,_) as typ) = match t with
+ | Typ_tup ts -> List.exists contains_bitvector_typ ts
+ | Typ_app (_, targs) -> is_bitvector_typ typ || List.exists contains_bitvector_typ_arg targs
+ | Typ_fn (t1,t2,_) -> contains_bitvector_typ t1 || contains_bitvector_typ t2
+ | _ -> false
+and contains_bitvector_typ_arg (Typ_arg_aux (targ, _)) = match targ with
+ | Typ_arg_typ t -> contains_bitvector_typ t
+ | _ -> false
+
+let const_nexp (Nexp_aux (nexp,_)) = match nexp with
+ | Nexp_constant _ -> true
+ | _ -> false
+
+(* Check for variables in types that would be pretty-printed.
+ In particular, in case of vector types, only the element type and the
+ length argument are checked for variables, and the latter only if it is
+ a bitvector; for other types of vectors, the length is not pretty-printed
+ in the type, and the start index is never pretty-printed in vector types. *)
+let rec contains_t_pp_var (Typ_aux (t,a) as typ) = match t with
+ | Typ_wild -> true
+ | Typ_id _ -> false
+ | Typ_var _ -> true
+ | Typ_fn (t1,t2,_) -> contains_t_pp_var t1 || contains_t_pp_var t2
+ | Typ_tup ts -> List.exists contains_t_pp_var ts
+ | Typ_app (c,targs) ->
+ if is_bitvector_typ typ then
+ let (_,length,_,_) = vector_typ_args_of typ in
+ not (const_nexp ((*normalize_nexp*) length))
+ else List.exists contains_t_arg_pp_var targs
+and contains_t_arg_pp_var (Typ_arg_aux (targ, _)) = match targ with
+ | Typ_arg_typ t -> contains_t_pp_var t
+ | Typ_arg_nexp nexp -> not (const_nexp ((*normalize_nexp*) nexp))
+ | _ -> false
+
+let prefix_recordtype = true
+let report = Reporting_basic.err_unreachable
+let doc_exp_lem, doc_let_lem =
+ let rec top_exp regtypes (aexp_needed : bool) (E_aux (e, (l,annot)) as full_exp) =
+ let expY = top_exp regtypes true in
+ let expN = top_exp regtypes false in
+ let expV = top_exp regtypes in
+ match e with
+ | E_assign((LEXP_aux(le_act,tannot) as le), e) ->
+ (* can only be register writes *)
+ let t = typ_of_annot tannot in
+ (match le_act (*, t, tag*) with
+ | LEXP_vector_range (le,e2,e3) ->
+ (match le with
+ | LEXP_aux (LEXP_field (le,id), lannot) ->
+ if is_bit_typ (typ_of_annot lannot) then
+ raise (report l "indexing a register's (single bit) bitfield not supported")
+ else
+ (prefix 2 1)
+ (string "write_reg_field_range")
+ (align (doc_lexp_deref_lem regtypes le ^^ space^^
+ string_lit (doc_id_lem id) ^/^ expY e2 ^/^ expY e3 ^/^ expY e))
+ | _ ->
+ (prefix 2 1)
+ (string "write_reg_range")
+ (align (doc_lexp_deref_lem regtypes le ^^ space ^^ expY e2 ^/^ expY e3 ^/^ expY e))
+ )
+ | LEXP_vector (le,e2) when is_bit_typ t ->
+ (match le with
+ | LEXP_aux (LEXP_field (le,id), lannot) ->
+ if is_bit_typ (typ_of_annot lannot) then
+ raise (report l "indexing a register's (single bit) bitfield not supported")
+ else
+ (prefix 2 1)
+ (string "write_reg_field_bit")
+ (align (doc_lexp_deref_lem regtypes le ^^ space ^^ doc_id_lem id ^/^ expY e2 ^/^ expY e))
+ | _ ->
+ (prefix 2 1)
+ (string "write_reg_bit")
+ (doc_lexp_deref_lem regtypes le ^^ space ^^ expY e2 ^/^ expY e)
+ )
+ | LEXP_field (le,id) when is_bit_typ t ->
+ (prefix 2 1)
+ (string "write_reg_bitfield")
+ (doc_lexp_deref_lem regtypes le ^^ space ^^ string_lit(doc_id_lem id) ^/^ expY e)
+ | LEXP_field (le,id) ->
+ (prefix 2 1)
+ (string "write_reg_field")
+ (doc_lexp_deref_lem regtypes le ^^ space ^^
+ string_lit(doc_id_lem id) ^/^ expY e)
+ (* | (LEXP_id id | LEXP_cast (_,id)), t, Alias alias_info ->
+ (match alias_info with
+ | Alias_field(reg,field) ->
+ let f = match t with
+ | (Tid "bit" | Tabbrev (_,{t=Tid "bit"})) ->
+ string "write_reg_bitfield"
+ | _ -> string "write_reg_field" in
+ (prefix 2 1)
+ f
+ (separate space [string reg;string_lit(string field);expY e])
+ | Alias_pair(reg1,reg2) ->
+ string "write_two_regs" ^^ space ^^ string reg1 ^^ space ^^
+ string reg2 ^^ space ^^ expY e) *)
+ | _ ->
+ (prefix 2 1) (string "write_reg") (doc_lexp_deref_lem regtypes le ^/^ expY e))
+ | E_vector_append(le,re) ->
+ let t = typ_of_annot (l,annot) in
+ let (call,ta,aexp_needed) =
+ if is_bitvector_typ t then
+ if not (contains_t_pp_var t)
+ then ("bitvector_concat", doc_tannot_lem regtypes false t, true)
+ else ("bitvector_concat", empty, aexp_needed)
+ else ("vector_concat",empty,aexp_needed) in
+ let epp =
+ align (group (separate space [string call;expY le;expY re])) ^^ ta in
+ if aexp_needed then parens epp else epp
+ | E_cons(le,re) -> doc_op (group (colon^^colon)) (expY le) (expY re)
+ | E_if(c,t,e) ->
+ let (E_aux (_,(_,cannot))) = c in
+ let epp =
+ separate space [string "if";group (align (string "bitU_to_bool" ^//^ group (expY c)))] ^^
+ break 1 ^^
+ (prefix 2 1 (string "then") (expN t)) ^^ (break 1) ^^
+ (prefix 2 1 (string "else") (expN e)) in
+ if aexp_needed then parens (align epp) else epp
+ | E_for(id,exp1,exp2,exp3,(Ord_aux(order,_)),exp4) ->
+ raise (report l "E_for should have been removed till now")
+ | E_let(leb,e) ->
+ let epp = let_exp regtypes leb ^^ space ^^ string "in" ^^ hardline ^^ expN e in
+ if aexp_needed then parens epp else epp
+ | E_app(f,args) ->
+ begin match f with
+ (* temporary hack to make the loop body a function of the temporary variables *)
+ | Id_aux ((Id (("foreach_inc" | "foreach_dec" |
+ "foreachM_inc" | "foreachM_dec" ) as loopf),_)) ->
+ let [id;indices;body;e5] = args in
+ let varspp = match e5 with
+ | E_aux (E_tuple vars,_) ->
+ let vars = List.map (fun (E_aux (E_id (Id_aux (Id name,_)),_)) -> string name) vars in
+ begin match vars with
+ | [v] -> v
+ | _ -> parens (separate comma vars) end
+ | E_aux (E_id (Id_aux (Id name,_)),_) ->
+ string name
+ | E_aux (E_lit (L_aux (L_unit,_)),_) ->
+ string "_" in
+ parens (
+ (prefix 2 1)
+ ((separate space) [string loopf;group (expY indices);expY e5])
+ (parens
+ (prefix 1 1 (separate space [string "fun";expY id;varspp;arrow]) (expN body))
+ )
+ )
+ | Id_aux (Id "append",_) ->
+ let [e1;e2] = args in
+ let epp = align (expY e1 ^^ space ^^ string "++" ^//^ expY e2) in
+ if aexp_needed then parens (align epp) else epp
+ | Id_aux (Id "slice_raw",_) ->
+ let [e1;e2;e3] = args in
+ let t1 = typ_of e1 in
+ let eff1 = effect_of e1 in
+ let call = if is_bitvector_typ t1 then "bvslice_raw" else "slice_raw" in
+ let epp = separate space [string call;expY e1;expY e2;expY e3] in
+ let (taepp,aexp_needed) =
+ let t = typ_of full_exp in
+ let eff = effect_of full_exp in
+ if contains_bitvector_typ t && not (contains_t_pp_var t)
+ then (align epp ^^ (doc_tannot_lem regtypes (effectful eff) t), true)
+ else (epp, aexp_needed) in
+ if aexp_needed then parens (align taepp) else taepp
+ | Id_aux (Id "length",_) ->
+ let [arg] = args in
+ let targ = typ_of arg in
+ let call = if is_bitvector_typ targ then "bvlength" else "length" in
+ let epp = separate space [string call;expY arg] in
+ if aexp_needed then parens (align epp) else epp
+ | Id_aux (Id "bool_not", _) ->
+ let [a] = args in
+ let epp = align (string "~" ^^ expY a) in
+ if aexp_needed then parens (align epp) else epp
+ | _ ->
+ begin match annot with
+ | Some (env, _, _) when (is_ctor env f) ->
+ let argpp a_needed arg =
+ let t = typ_of arg in
+ if is_vector_typ t then
+ let call =
+ if is_bitvector_typ t then "reset_bitvector_start"
+ else "reset_vector_start" in
+ let epp = concat [string call;space;expY arg] in
+ if a_needed then parens epp else epp
+ else expV a_needed arg in
+ let epp =
+ match args with
+ | [] -> doc_id_lem_ctor f
+ | [arg] -> doc_id_lem_ctor f ^^ space ^^ argpp true arg
+ | _ ->
+ doc_id_lem_ctor f ^^ space ^^
+ parens (separate_map comma (argpp false) args) in
+ if aexp_needed then parens (align epp) else epp
+ | _ ->
+ let call = (*match annot with
+ | Base(_,External (Some n),_,_,_,_) -> string n
+ | _ ->*) doc_id_lem f in
+ let argpp a_needed arg =
+ let t = typ_of arg in
+ if is_vector_typ t then
+ let call =
+ if is_bitvector_typ t then "reset_bitvector_start"
+ else "reset_vector_start" in
+ let epp = concat [string call;space;expY arg] in
+ if a_needed then parens epp else epp
+ else expV a_needed arg in
+ let argspp = match args with
+ | [arg] -> argpp true arg
+ | args -> parens (align (separate_map (comma ^^ break 0) (argpp false) args)) in
+ let epp = align (call ^//^ argspp) in
+ let (taepp,aexp_needed) =
+ let t = typ_of full_exp in
+ let eff = effect_of full_exp in
+ if contains_bitvector_typ t && not (contains_t_pp_var t)
+ then (align epp ^^ (doc_tannot_lem regtypes (effectful eff) t), true)
+ else (epp, aexp_needed) in
+ if aexp_needed then parens (align taepp) else taepp
+ end
+ end
+ | E_vector_access (v,e) ->
+ let eff = effect_of full_exp in
+ let epp =
+ if has_effect eff BE_rreg then
+ separate space [string "read_reg_bit";expY v;expY e]
+ else
+ let tv = typ_of v in
+ let call = if is_bitvector_typ tv then "bvaccess" else "access" in
+ separate space [string call;expY v;expY e] in
+ if aexp_needed then parens (align epp) else epp
+ | E_vector_subrange (v,e1,e2) ->
+ let t = typ_of full_exp in
+ let eff = effect_of full_exp in
+ let (epp,aexp_needed) =
+ if has_effect eff BE_rreg then
+ let epp = align (string "read_reg_range" ^^ space ^^ expY v ^//^ expY e1 ^//^ expY e2) in
+ if contains_bitvector_typ t && not (contains_t_pp_var t)
+ then (epp ^^ doc_tannot_lem regtypes true t, true)
+ else (epp, aexp_needed)
+ else
+ if is_bitvector_typ t then
+ let bepp = string "bvslice" ^^ space ^^ expY v ^//^ expY e1 ^//^ expY e2 in
+ if not (contains_t_pp_var t)
+ then (bepp ^^ doc_tannot_lem regtypes false t, true)
+ else (bepp, aexp_needed)
+ else (string "slice" ^^ space ^^ expY v ^//^ expY e1 ^//^ expY e2, aexp_needed) in
+ if aexp_needed then parens (align epp) else epp
+ | E_field((E_aux(_,(l,fannot)) as fexp),id) ->
+ let ft = typ_of_annot (l,fannot) in
+ (match fannot with
+ | Some(env, (Typ_aux (Typ_id tid, _)), _) when Env.is_regtyp tid env ->
+ let t = typ_of full_exp in
+ let field_f = string
+ (if is_bit_typ t
+ then "read_reg_bitfield"
+ else "read_reg_field") in
+ let (ta,aexp_needed) =
+ if contains_bitvector_typ t && not (contains_t_pp_var t)
+ then (doc_tannot_lem regtypes true t, true)
+ else (empty, aexp_needed) in
+ let epp = field_f ^^ space ^^ (expY fexp) ^^ space ^^ string_lit (doc_id_lem id) in
+ if aexp_needed then parens (align epp ^^ ta) else (epp ^^ ta)
+ | Some(env, (Typ_aux (Typ_id tid, _)), _) when Env.is_record tid env ->
+ let fname =
+ if prefix_recordtype
+ then (string (string_of_id tid ^ "_")) ^^ doc_id_lem id
+ else doc_id_lem id in
+ expY fexp ^^ dot ^^ fname
+ | _ ->
+ raise (report l "E_field expression with no register or record type"))
+ | E_block [] -> string "()"
+ | E_block exps -> raise (report l "Blocks should have been removed till now.")
+ | E_nondet exps -> raise (report l "Nondet blocks not supported.")
+ | E_id id ->
+ let t = typ_of full_exp in
+ (match annot with
+ | Some (env, Typ_aux (Typ_id tid, _), eff) when Env.is_regtyp tid env ->
+ if has_effect eff BE_rreg then
+ let epp = separate space [string "read_reg";doc_id_lem id] in
+ if contains_bitvector_typ t && not (contains_t_pp_var t)
+ then parens (epp ^^ doc_tannot_lem regtypes true t)
+ else epp
+ else
+ doc_id_lem id
+ | Some (env, _, _) when (is_ctor env id) -> doc_id_lem_ctor id
+ (*| Base((_,t),Alias alias_info,_,eff,_,_) ->
+ (match alias_info with
+ | Alias_field(reg,field) ->
+ let call = match t.t with
+ | Tid "bit" | Tabbrev (_,{t=Tid "bit"}) -> "read_reg_bitfield"
+ | _ -> "read_reg_field" in
+ let ta =
+ if contains_bitvector_typ t && not (contains_t_pp_var t)
+ then doc_tannot_lem regtypes true t else empty in
+ let epp = separate space [string call;string reg;string_lit(string field)] ^^ ta in
+ if aexp_needed then parens (align epp) else epp
+ | Alias_pair(reg1,reg2) ->
+ let (call,ta) =
+ if has_effect eff BE_rreg then
+ let ta =
+ if contains_bitvector_typ t && not (contains_t_pp_var t)
+ then doc_tannot_lem regtypes true t else empty in
+ ("read_two_regs", ta)
+ else
+ ("RegisterPair", empty) in
+ let epp = separate space [string call;string reg1;string reg2] ^^ ta in
+ if aexp_needed then parens (align epp) else epp
+ | Alias_extract(reg,start,stop) ->
+ let epp =
+ if start = stop then
+ separate space [string "read_reg_bit";string reg;doc_int start]
+ else
+ let ta =
+ if contains_bitvector_typ t && not (contains_t_pp_var t)
+ then doc_tannot_lem regtypes true t else empty in
+ separate space [string "read_reg_range";string reg;doc_int start;doc_int stop] ^^ ta in
+ if aexp_needed then parens (align epp) else epp
+ )*)
+ | _ -> doc_id_lem id)
+ | E_lit lit -> doc_lit_lem false lit annot
+ | E_cast(typ,e) ->
+ if is_vector_typ typ then
+ let (start,_,_,_) = vector_typ_args_of typ in
+ let call =
+ if is_bitvector_typ typ then "set_bitvector_start"
+ else "set_vector_start" in
+ let epp = (concat [string call;space;doc_nexp start]) ^//^
+ expY e in
+ if aexp_needed then parens epp else epp
+ else
+ expV aexp_needed e (*
+ (match annot with
+ | Base((_,t),External _,_,_,_,_) ->
+ (* TODO: Does this case still exist with the new type checker? *)
+ let epp = string "read_reg" ^^ space ^^ expY e in
+ if contains_bitvector_typ t && not (contains_t_pp_var t)
+ then parens (epp ^^ doc_tannot_lem regtypes true t) else epp
+ | Base((_,t),_,_,_,_,_) ->
+ (match typ with
+ | Typ_app (Id_aux (Id "vector",_), [Typ_arg_aux (Typ_arg_nexp(Nexp_aux (Nexp_constant i,_)),_);_;_;_]) ->
+ let call =
+ if is_bitvector_typ t then "set_bitvector_start"
+ else "set_vector_start" in
+ let epp = (concat [string call;space;string (string_of_int i)]) ^//^
+ expY e in
+ if aexp_needed then parens epp else epp
+ (*
+ | Typ_var (Kid_aux (Var "length",_)) ->
+ (* TODO: Does this case still exist with the new type checker? *)
+ let call =
+ if is_bitvector_typ t then "set_bitvector_start_to_length"
+ else "set_vector_start_to_length" in
+ let epp = (string call) ^//^ expY e in
+ if aexp_needed then parens epp else epp
+ *)
+ | _ ->
+ expV aexp_needed e)) (*(parens (doc_op colon (group (expY e)) (doc_typ_lem typ)))) *)
+ *)
+ | E_tuple exps ->
+ (match exps with (*
+ | [e] -> expV aexp_needed e *)
+ | _ -> parens (separate_map comma expN exps))
+ | E_record(FES_aux(FES_Fexps(fexps,_),_)) ->
+ let recordtyp = match annot with
+ | Some (env, Typ_aux (Typ_id tid,_), _) when Env.is_record tid env ->
+ tid
+ | _ -> raise (report l "cannot get record type") in
+ let epp = anglebars (space ^^ (align (separate_map
+ (semi_sp ^^ break 1)
+ (doc_fexp regtypes recordtyp) fexps)) ^^ space) in
+ if aexp_needed then parens epp else epp
+ | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) ->
+ let recordtyp = match annot with
+ | Some (env, Typ_aux (Typ_id tid,_), _) when Env.is_record tid env ->
+ tid
+ | _ -> raise (report l "cannot get record type") in
+ anglebars (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp regtypes recordtyp) fexps))
+ | E_vector exps ->
+ let t = typ_of full_exp in
+ let (start, len, order, etyp) =
+ if is_vector_typ t then vector_typ_args_of t
+ else raise (Reporting_basic.err_unreachable l "E_vector of non-vector type") in
+ (*match annot with
+ | Base((_,t),_,_,_,_,_) ->
+ match t.t with
+ | Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; TA_typ etyp])
+ | Tabbrev(_,{t= Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; TA_typ etyp])}) ->*)
+ let dir,dir_out = if is_order_inc order then (true,"true") else (false, "false") in
+ let start = match start with
+ | Nexp_aux (Nexp_constant i, _) -> string_of_int i
+ | _ -> if dir then "0" else string_of_int (List.length exps) in
+ let expspp =
+ match exps with
+ | [] -> empty
+ | e :: es ->
+ let (expspp,_) =
+ List.fold_left
+ (fun (pp,count) e ->
+ (pp ^^ semi ^^ (if count = 20 then break 0 else empty) ^^
+ expN e),
+ if count = 20 then 0 else count + 1)
+ (expN e,0) es in
+ align (group expspp) in
+ let epp =
+ group (separate space [string "Vector"; brackets expspp;string start;string dir_out]) in
+ let (epp,aexp_needed) =
+ if is_bit_typ etyp then
+ let bepp = string "vec_to_bvec" ^^ space ^^ parens (align epp) in
+ if contains_t_pp_var t
+ then (bepp, aexp_needed)
+ else (bepp ^^ doc_tannot_lem regtypes false t, true)
+ else (epp,aexp_needed) in
+ if aexp_needed then parens (align epp) else epp
+ (* *)
+ | E_vector_indexed (iexps, (Def_val_aux (default,(dl,dannot)))) ->
+ let t = typ_of full_exp in
+ let (start, len, order, etyp) =
+ if is_vector_typ t then vector_typ_args_of t
+ else raise (Reporting_basic.err_unreachable l "E_vector_indexed of non-vector type") in
+ let dir,dir_out = if is_order_inc order then (true,"true") else (false, "false") in
+ let start = match start with
+ | Nexp_aux (Nexp_constant i, _) -> string_of_int i
+ | _ -> if dir then "0" else string_of_int (List.length iexps) in
+ let size = match len with
+ | Nexp_aux (Nexp_constant i, _)-> string_of_int i
+ | Nexp_aux (Nexp_exp (Nexp_aux (Nexp_constant i, _)), _) ->
+ string_of_int (Util.power 2 i)
+ | _ ->
+ raise (Reporting_basic.err_unreachable l
+ "trying to pretty-print indexed vector without constant size") in
+ let default_string =
+ match default with
+ | Def_val_empty ->
+ if is_bitvector_typ t then string "BU"
+ else failwith "E_vector_indexed of non-bitvector type without default argument"
+ | Def_val_dec e ->
+ (*let (Base ((_,{t = t}),_,_,_,_,_)) = dannot in
+ match t with
+ | Tapp ("register",
+ [TA_typ ({t = rt})]) ->
+ (* TODO: Does this case still occur with the new type checker? *)
+ let n = match rt with
+ | Tapp ("vector",TA_nexp {nexp = Nconst i} :: TA_nexp {nexp = Nconst j} ::_) ->
+ abs_big_int (sub_big_int i j)
+ | _ ->
+ raise ((Reporting_basic.err_unreachable dl)
+ ("not the right type information available to construct "^
+ "undefined register")) in
+ parens (string ("UndefinedRegister " ^ string_of_big_int n))
+ | _ ->*) expY e in
+ let iexp (i,e) = parens (doc_int i ^^ comma ^^ expN e) in
+ let expspp =
+ match iexps with
+ | [] -> empty
+ | e :: es ->
+ let (expspp,_) =
+ List.fold_left
+ (fun (pp,count) e ->
+ (pp ^^ semi ^^ (if count = 5 then break 1 else empty) ^^ iexp e),
+ if count = 5 then 0 else count + 1)
+ (iexp e,0) es in
+ align (expspp) in
+ let call = string "make_indexed_vector" in
+ let epp =
+ align (group (call ^//^ brackets expspp ^/^
+ separate space [default_string;string start;string size;string dir_out])) in
+ let (bepp, aexp_needed) =
+ if is_bitvector_typ t
+ then (string "vec_to_bvec" ^^ space ^^ parens (epp) ^^ doc_tannot_lem regtypes false t, true)
+ else (epp, aexp_needed) in
+ if aexp_needed then parens (align bepp) else bepp
+ | E_vector_update(v,e1,e2) ->
+ let t = typ_of full_exp in
+ let call = if is_bitvector_typ t then "bvupdate_pos" else "update_pos" in
+ let epp = separate space [string call;expY v;expY e1;expY e2] in
+ if aexp_needed then parens (align epp) else epp
+ | E_vector_update_subrange(v,e1,e2,e3) ->
+ let t = typ_of full_exp in
+ let call = if is_bitvector_typ t then "bvupdate" else "update" in
+ let epp = align (string call ^//^
+ group (group (expY v) ^/^ group (expY e1) ^/^ group (expY e2)) ^/^
+ group (expY e3)) in
+ if aexp_needed then parens (align epp) else epp
+ | E_list exps ->
+ brackets (separate_map semi (expN) exps)
+ | E_case(e,pexps) ->
+ let only_integers e =
+ let typ = typ_of e in
+ if Ast_util.is_number typ then
+ let e_pp = expY e in
+ align (string "toNatural" ^//^ e_pp)
+ else
+ (* TODO: Where does this come from?? *)
+ (match typ with
+ | Typ_aux (Typ_tup ([t1;t2;t3;t4;t5] as ts), _) when List.for_all Ast_util.is_number ts ->
+ let e_pp = expY e in
+ align (string "toNaturalFiveTup" ^//^ e_pp)
+ | _ -> expY e)
+ in
+
+ (* This is a hack, incomplete. It's because lem does not allow
+ pattern-matching on integers *)
+ let epp =
+ group ((separate space [string "match"; only_integers e; string "with"]) ^/^
+ (separate_map (break 1) (doc_case regtypes) pexps) ^/^
+ (string "end")) in
+ if aexp_needed then parens (align epp) else align epp
+ | E_exit e -> separate space [string "exit"; expY e;]
+ | E_assert (e1,e2) ->
+ let epp = separate space [string "assert'"; expY e1; expY e2] in
+ if aexp_needed then parens (align epp) else align epp
+ | E_app_infix (e1,id,e2) ->
+ (* TODO: Should have been removed by the new type checker; check with Alasdair *)
+ raise (Reporting_basic.err_unreachable l
+ "E_app_infix should have been rewritten before pretty-printing")
+ (*match annot with
+ | Base((_,t),External(Some name),_,_,_,_) ->
+ let argpp arg =
+ let (E_aux (_,(_,Base((_,t),_,_,_,_,_)))) = arg in
+ match t.t with
+ | Tapp("vector",_) ->
+ let call =
+ if is_bitvector_typ t then "reset_bitvector_start"
+ else "reset_vector_start" in
+ parens (concat [string call;space;expY arg])
+ | _ -> expY arg in
+ let epp =
+ let aux name = align (argpp e1 ^^ space ^^ string name ^//^ argpp e2) in
+ let aux2 name = align (string name ^//^ argpp e1 ^/^ argpp e2) in
+ align
+ (match name with
+ | "power" -> aux2 "pow"
+
+ | "bitwise_and_bit" -> aux "&."
+ | "bitwise_or_bit" -> aux "|."
+ | "bitwise_xor_bit" -> aux "+."
+ | "add" -> aux "+"
+ | "minus" -> aux "-"
+ | "multiply" -> aux "*"
+
+ | "quot" -> aux2 "quot"
+ | "quot_signed" -> aux2 "quot"
+ | "modulo" -> aux2 "modulo"
+ | "add_vec" -> aux2 "add_VVV"
+ | "add_vec_signed" -> aux2 "addS_VVV"
+ | "add_overflow_vec" -> aux2 "addO_VVV"
+ | "add_overflow_vec_signed" -> aux2 "addSO_VVV"
+ | "minus_vec" -> aux2 "minus_VVV"
+ | "minus_overflow_vec" -> aux2 "minusO_VVV"
+ | "minus_overflow_vec_signed" -> aux2 "minusSO_VVV"
+ | "multiply_vec" -> aux2 "mult_VVV"
+ | "multiply_vec_signed" -> aux2 "multS_VVV"
+ | "mult_overflow_vec" -> aux2 "multO_VVV"
+ | "mult_overflow_vec_signed" -> aux2 "multSO_VVV"
+ | "quot_vec" -> aux2 "quot_VVV"
+ | "quot_vec_signed" -> aux2 "quotS_VVV"
+ | "quot_overflow_vec" -> aux2 "quotO_VVV"
+ | "quot_overflow_vec_signed" -> aux2 "quotSO_VVV"
+ | "mod_vec" -> aux2 "mod_VVV"
+
+ | "add_vec_range" -> aux2 "add_VIV"
+ | "add_vec_range_signed" -> aux2 "addS_VIV"
+ | "minus_vec_range" -> aux2 "minus_VIV"
+ | "mult_vec_range" -> aux2 "mult_VIV"
+ | "mult_vec_range_signed" -> aux2 "multS_VIV"
+ | "mod_vec_range" -> aux2 "minus_VIV"
+
+ | "add_range_vec" -> aux2 "add_IVV"
+ | "add_range_vec_signed" -> aux2 "addS_IVV"
+ | "minus_range_vec" -> aux2 "minus_IVV"
+ | "mult_range_vec" -> aux2 "mult_IVV"
+ | "mult_range_vec_signed" -> aux2 "multS_IVV"
+
+ | "add_range_vec_range" -> aux2 "add_IVI"
+ | "add_range_vec_range_signed" -> aux2 "addS_IVI"
+ | "minus_range_vec_range" -> aux2 "minus_IVI"
+
+ | "add_vec_range_range" -> aux2 "add_VII"
+ | "add_vec_range_range_signed" -> aux2 "addS_VII"
+ | "minus_vec_range_range" -> aux2 "minus_VII"
+ | "add_vec_vec_range" -> aux2 "add_VVI"
+ | "add_vec_vec_range_signed" -> aux2 "addS_VVI"
+
+ | "add_vec_bit" -> aux2 "add_VBV"
+ | "add_vec_bit_signed" -> aux2 "addS_VBV"
+ | "add_overflow_vec_bit_signed" -> aux2 "addSO_VBV"
+ | "minus_vec_bit_signed" -> aux2 "minus_VBV"
+ | "minus_overflow_vec_bit" -> aux2 "minusO_VBV"
+ | "minus_overflow_vec_bit_signed" -> aux2 "minusSO_VBV"
+
+ | _ ->
+ string name ^//^ parens (expN e1 ^^ comma ^/^ expN e2)) in
+ let (epp,aexp_needed) =
+ if contains_bitvector_typ t && not (contains_t_pp_var t)
+ then (parens epp ^^ doc_tannot_lem regtypes false t, true)
+ else (epp, aexp_needed) in
+ if aexp_needed then parens (align epp) else epp
+ | _ ->
+ let epp =
+ align (doc_id_lem id ^//^ parens (expN e1 ^^ comma ^/^ expN e2)) in
+ if aexp_needed then parens (align epp) else epp*)
+ | E_internal_let(lexp, eq_exp, in_exp) ->
+ raise (report l "E_internal_lets should have been removed till now")
+ (* (separate
+ space
+ [string "let internal";
+ (match lexp with (LEXP_aux ((LEXP_id id | LEXP_cast (_,id)),_)) -> doc_id_lem id);
+ coloneq;
+ exp eq_exp;
+ string "in"]) ^/^
+ exp in_exp *)
+ | E_internal_plet (pat,e1,e2) ->
+ let epp =
+ let b = match e1 with E_aux (E_if _,_) -> true | _ -> false in
+ match pat with
+ | P_aux (P_wild,_) ->
+ (separate space [expV b e1; string ">>"]) ^^ hardline ^^ expN e2
+ | _ ->
+ (separate space [expV b e1; string ">>= fun";
+ doc_pat_lem regtypes true pat;arrow]) ^^ hardline ^^ expN e2 in
+ if aexp_needed then parens (align epp) else epp
+ | E_internal_return (e1) ->
+ separate space [string "return"; expY e1;]
+ | E_sizeof nexp ->
+ (match nexp with
+ | Nexp_aux (Nexp_constant i, _) -> doc_lit_lem false (L_aux (L_num i, l)) annot
+ | _ ->
+ raise (Reporting_basic.err_unreachable l
+ "pretty-printing non-constant sizeof expressions to Lem not yet supported"))
+ | E_return _ ->
+ raise (Reporting_basic.err_unreachable l
+ "pretty-printing early return statements not yet to Lem supported")
+ | E_comment _ | E_comment_struc _ -> empty
+ | E_internal_cast _ | E_internal_exp _ | E_sizeof_internal _ | E_internal_exp_user _ ->
+ raise (Reporting_basic.err_unreachable l
+ "unsupported internal expression encountered while pretty-printing")
+ and let_exp regtypes (LB_aux(lb,_)) = match lb with
+ | LB_val_explicit(_,pat,e)
+ | LB_val_implicit(pat,e) ->
+ prefix 2 1
+ (separate space [string "let"; doc_pat_lem regtypes true pat; equals])
+ (top_exp regtypes false e)
+
+ and doc_fexp regtypes recordtyp (FE_aux(FE_Fexp(id,e),_)) =
+ let fname =
+ if prefix_recordtype
+ then (string (string_of_id recordtyp ^ "_")) ^^ doc_id_lem id
+ else doc_id_lem id in
+ group (doc_op equals fname (top_exp regtypes true e))
+
+ and doc_case regtypes (Pat_aux(Pat_exp(pat,e),_)) =
+ group (prefix 3 1 (separate space [pipe; doc_pat_lem regtypes false pat;arrow])
+ (group (top_exp regtypes false e)))
+
+ and doc_lexp_deref_lem regtypes ((LEXP_aux(lexp,(l,annot))) as le) = match lexp with
+ | LEXP_field (le,id) ->
+ parens (separate empty [doc_lexp_deref_lem regtypes le;dot;doc_id_lem id])
+ | LEXP_vector(le,e) ->
+ parens ((separate space) [string "access";doc_lexp_deref_lem regtypes le;
+ top_exp regtypes true e])
+ | LEXP_id id -> doc_id_lem id
+ | LEXP_cast (typ,id) -> doc_id_lem id
+ | _ ->
+ raise (Reporting_basic.err_unreachable l ("doc_lexp_deref_lem: Shouldn't happen"))
+ (* expose doc_exp_lem and doc_let *)
+ in top_exp, let_exp
+
+(*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 id; string "of";
+ parens (doc_typ_lem regtypes typ)]
+ | 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))
+ | BF_range(i1,i2) -> parens (doc_op comma (doc_int i1) (doc_int i2))
+ | BF_concat(ir1,ir2) -> (doc_range ir1) ^^ comma ^^ (doc_range ir2)
+
+let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with
+ | TD_abbrev(id,nm,typschm) ->
+ doc_op equals (concat [string "type"; space; doc_id_lem_type id])
+ (doc_typschm_lem regtypes typschm)
+ | TD_record(id,nm,typq,fs,_) ->
+ let f_pp (typ,fid) =
+ let fname = if prefix_recordtype
+ then concat [doc_id_lem id;string "_";doc_id_lem_type fid;]
+ else doc_id_lem_type fid in
+ concat [fname;space;colon;space;doc_typ_lem regtypes typ; semi] in
+ let fs_doc = group (separate_map (break 1) f_pp fs) in
+ doc_op equals
+ (concat [string "type"; space; doc_id_lem_type id;])
+ (doc_typquant_lem typq (anglebars (space ^^ align fs_doc ^^ space)))
+ | TD_variant(id,nm,typq,ar,_) ->
+ (match id with
+ | Id_aux ((Id "read_kind"),_) -> empty
+ | Id_aux ((Id "write_kind"),_) -> empty
+ | Id_aux ((Id "barrier_kind"),_) -> empty
+ | Id_aux ((Id "trans_kind"),_) -> empty
+ | Id_aux ((Id "instruction_kind"),_) -> empty
+ | Id_aux ((Id "regfp"),_) -> empty
+ | Id_aux ((Id "niafp"),_) -> empty
+ | Id_aux ((Id "diafp"),_) -> empty
+ | _ ->
+ let ar_doc = group (separate_map (break 1) (doc_type_union_lem regtypes) ar) in
+ let typ_pp =
+
+ (doc_op equals)
+ (concat [string "type"; space; doc_id_lem_type id;])
+ (doc_typquant_lem typq ar_doc) in
+ let make_id pat id =
+ separate space [string "SIA.Id_aux";
+ parens (string "SIA.Id " ^^ string_lit (doc_id id));
+ if pat then underscore else string "SIA.Unknown"] in
+ let fromInterpValueF = concat [doc_id_lem_type id;string "FromInterpValue"] in
+ let toInterpValueF = concat [doc_id_lem_type id;string "ToInterpValue"] in
+ let fromInterpValuePP =
+ (prefix 2 1)
+ (separate space [string "let rec";fromInterpValueF;string "v";equals;string "match v with"])
+ (
+ ((separate_map (break 1))
+ (fun (Tu_aux (tu,_)) ->
+ match tu with
+ | Tu_ty_id (ty,cid) ->
+ (separate space)
+ [pipe;string "SI.V_ctor";parens (make_id true cid);underscore;underscore;string "v";
+ arrow;
+ doc_id_lem_ctor cid;
+ parens (string "fromInterpValue v")]
+ | Tu_id cid ->
+ (separate space)
+ [pipe;string "SI.V_ctor";parens (make_id true cid);underscore;underscore;string "v";
+ arrow;
+ doc_id_lem_ctor cid])
+ ar) ^/^
+
+ ((separate space) [pipe;string "SI.V_tuple [v]";arrow;fromInterpValueF;string "v"]) ^/^
+
+ let failmessage =
+ (string_lit
+ (concat [string "fromInterpValue";space;doc_id_lem_type id;colon;space;string "unexpected value. ";]))
+ ^^
+ (string " ^ Interp.debug_print_value v") in
+ ((separate space) [pipe;string "v";arrow;string "failwith";parens failmessage]) ^/^
+ string "end") in
+ let toInterpValuePP =
+ (prefix 2 1)
+ (separate space [string "let";toInterpValueF;equals;string "function"])
+ (
+ ((separate_map (break 1))
+ (fun (Tu_aux (tu,_)) ->
+ match tu with
+ | Tu_ty_id (ty,cid) ->
+ (separate space)
+ [pipe;doc_id_lem_ctor cid;string "v";arrow;
+ string "SI.V_ctor";
+ parens (make_id false cid);
+ parens (string "SIA.T_id " ^^ string_lit (doc_id id));
+ string "SI.C_Union";
+ parens (string "toInterpValue v")]
+ | Tu_id cid ->
+ (separate space)
+ [pipe;doc_id_lem_ctor cid;arrow;
+ string "SI.V_ctor";
+ parens (make_id false cid);
+ parens (string "SIA.T_id " ^^ string_lit (doc_id id));
+ string "SI.C_Union";
+ parens (string "toInterpValue ()")])
+ ar) ^/^
+ string "end") in
+ let fromToInterpValuePP =
+ ((prefix 2 1)
+ (concat [string "instance ";parens (string "ToFromInterpValue " ^^ doc_id_lem_type id)])
+ (concat [string "let toInterpValue = ";toInterpValueF;hardline;
+ string "let fromInterpValue = ";fromInterpValueF]))
+ ^/^ string "end" in
+ typ_pp ^^ hardline ^^ hardline ^^
+ if !print_to_from_interp_value then
+ toInterpValuePP ^^ hardline ^^ hardline ^^
+ fromInterpValuePP ^^ hardline ^^ hardline ^^
+ fromToInterpValuePP ^^ hardline
+ else empty)
+ | TD_enum(id,nm,enums,_) ->
+ (match id with
+ | Id_aux ((Id "read_kind"),_) -> empty
+ | Id_aux ((Id "write_kind"),_) -> empty
+ | Id_aux ((Id "barrier_kind"),_) -> empty
+ | Id_aux ((Id "trans_kind"),_) -> empty
+ | Id_aux ((Id "instruction_kind"),_) -> empty
+ | Id_aux ((Id "regfp"),_) -> empty
+ | Id_aux ((Id "niafp"),_) -> empty
+ | Id_aux ((Id "diafp"),_) -> empty
+ | _ ->
+ let rec range i j = if i > j then [] else i :: (range (i+1) j) in
+ let nats = range 0 in
+ let enums_doc = group (separate_map (break 1 ^^ pipe ^^ space) doc_id_lem_ctor enums) in
+ let typ_pp = (doc_op equals)
+ (concat [string "type"; space; doc_id_lem_type id;])
+ (enums_doc) in
+ let fromInterpValueF = concat [doc_id_lem_type id;string "FromInterpValue"] in
+ let toInterpValueF = concat [doc_id_lem_type id;string "ToInterpValue"] in
+ let make_id pat id =
+ separate space [string "SIA.Id_aux";
+ parens (string "SIA.Id " ^^ string_lit (doc_id id));
+ if pat then underscore else string "SIA.Unknown"] in
+ let fromInterpValuePP =
+ (prefix 2 1)
+ (separate space [string "let rec";fromInterpValueF;string "v";equals;string "match v with"])
+ (
+ ((separate_map (break 1))
+ (fun (cid) ->
+ (separate space)
+ [pipe;string "SI.V_ctor";parens (make_id true cid);underscore;underscore;string "v";
+ arrow;doc_id_lem_ctor cid]
+ )
+ enums
+ ) ^/^
+ (
+ (align
+ ((prefix 3 1)
+ (separate space [pipe;string ("SI.V_lit (SIA.L_aux (SIA.L_num n) _)");arrow])
+ (separate space [string "match";parens(string "natFromInteger n");string "with"] ^/^
+ (
+ ((separate_map (break 1))
+ (fun (cid,number) ->
+ (separate space)
+ [pipe;string (string_of_int number);arrow;doc_id_lem_ctor cid]
+ )
+ (List.combine enums (nats ((List.length enums) - 1)))
+ ) ^/^ string "end"
+ )
+ )
+ )
+ )
+ ) ^/^
+
+ ((separate space) [pipe;string "SI.V_tuple [v]";arrow;fromInterpValueF;string "v"]) ^/^
+
+ let failmessage =
+ (string_lit
+ (concat [string "fromInterpValue";space;doc_id_lem_type id;colon;space;string "unexpected value. ";]))
+ ^^
+ (string " ^ Interp.debug_print_value v") in
+ ((separate space) [pipe;string "v";arrow;string "failwith";parens failmessage]) ^/^
+
+ string "end") in
+ let toInterpValuePP =
+ (prefix 2 1)
+ (separate space [string "let";toInterpValueF;equals;string "function"])
+ (
+ ((separate_map (break 1))
+ (fun (cid,number) ->
+ (separate space)
+ [pipe;doc_id_lem_ctor cid;arrow;
+ string "SI.V_ctor";
+ parens (make_id false cid);
+ parens (string "SIA.T_id " ^^ string_lit (doc_id id));
+ parens (string ("SI.C_Enum " ^ string_of_int number));
+ parens (string "toInterpValue ()")])
+ (List.combine enums (nats ((List.length enums) - 1)))) ^/^
+ string "end") in
+ let fromToInterpValuePP =
+ ((prefix 2 1)
+ (concat [string "instance ";parens (string "ToFromInterpValue " ^^ doc_id_lem_type id)])
+ (concat [string "let toInterpValue = ";toInterpValueF;hardline;
+ string "let fromInterpValue = ";fromInterpValueF]))
+ ^/^ string "end" in
+ typ_pp ^^ hardline ^^ hardline ^^
+ if !print_to_from_interp_value
+ then toInterpValuePP ^^ hardline ^^ hardline ^^
+ fromInterpValuePP ^^ hardline ^^ hardline ^^
+ fromToInterpValuePP ^^ hardline
+ else empty)
+ | TD_register(id,n1,n2,rs) ->
+ match n1,n2 with
+ | Nexp_aux(Nexp_constant i1,_),Nexp_aux(Nexp_constant i2,_) ->
+ let doc_rid (r,id) = parens (separate comma_sp [string_lit (doc_id_lem id);
+ doc_range_lem r;]) in
+ let doc_rids = group (separate_map (semi ^^ (break 1)) doc_rid rs) in
+ (*let doc_rfield (_,id) =
+ (doc_op equals)
+ (string "let" ^^ space ^^ doc_id_lem id)
+ (string "Register_field" ^^ space ^^ string_lit(doc_id_lem id)) in*)
+ let dir_b = i1 < i2 in
+ let dir = string (if dir_b then "true" else "false") in
+ let size = if dir_b then i2-i1 +1 else i1-i2 + 1 in
+ (doc_op equals)
+ (concat [string "let";space;string "build_";doc_id_lem id;space;string "regname"])
+ (string "Register" ^^ space ^^
+ align (separate space [string "regname"; doc_int size; doc_int i1; dir;
+ break 0 ^^ brackets (align doc_rids)]))
+ (*^^ hardline ^^
+ separate_map hardline doc_rfield rs *)
+
+let doc_rec_lem (Rec_aux(r,_)) = match r with
+ | Rec_nonrec -> space
+ | Rec_rec -> space ^^ string "rec" ^^ space
+
+let doc_tannot_opt_lem regtypes (Typ_annot_opt_aux(t,_)) = match t with
+ | Typ_annot_opt_some(tq,typ) -> doc_typquant_lem tq (doc_typ_lem regtypes typ)
+
+let doc_funcl_lem regtypes (FCL_aux(FCL_Funcl(id,pat,exp),_)) =
+ group (prefix 3 1 ((doc_pat_lem regtypes false pat) ^^ space ^^ arrow)
+ (doc_exp_lem regtypes false exp))
+
+let get_id = function
+ | [] -> failwith "FD_function with empty list"
+ | (FCL_aux (FCL_Funcl (id,_,_),_))::_ -> id
+
+module StringSet = Set.Make(String)
+
+let rec doc_fundef_lem regtypes (FD_aux(FD_function(r, typa, efa, fcls),fannot)) =
+ match fcls with
+ | [] -> failwith "FD_function with empty function list"
+ | [FCL_aux (FCL_Funcl(id,pat,exp),_)] ->
+ (prefix 2 1)
+ ((separate space)
+ [(string "let") ^^ (doc_rec_lem r) ^^ (doc_id_lem id);
+ (doc_pat_lem regtypes true pat);
+ equals])
+ (doc_exp_lem regtypes false exp)
+ | _ ->
+ let id = get_id fcls in
+ (* let sep = hardline ^^ pipe ^^ space in *)
+ match id with
+ | Id_aux (Id fname,idl)
+ when fname = "execute" || fname = "initial_analysis" ->
+ let (_,auxiliary_functions,clauses) =
+ List.fold_left
+ (fun (already_used_fnames,auxiliary_functions,clauses) funcl ->
+ match funcl with
+ | FCL_aux (FCL_Funcl (Id_aux (Id _,l),pat,exp),annot) ->
+ let (P_aux (P_app (Id_aux (Id ctor,l),argspat),pannot)) = pat in
+ let rec pick_name_not_clashing_with already_used candidate =
+ if StringSet.mem candidate already_used then
+ pick_name_not_clashing_with already_used (candidate ^ "'")
+ else candidate in
+ let aux_fname = pick_name_not_clashing_with already_used_fnames (fname ^ "_" ^ ctor) in
+ let already_used_fnames = StringSet.add aux_fname already_used_fnames in
+ let fcl = FCL_aux (FCL_Funcl (Id_aux (Id aux_fname,l),
+ P_aux (P_tup argspat,pannot),exp),annot) in
+ let auxiliary_functions =
+ auxiliary_functions ^^ hardline ^^ hardline ^^
+ doc_fundef_lem regtypes (FD_aux (FD_function(r,typa,efa,[fcl]),fannot)) in
+ (* Bind complex patterns to names so that we can pass them to the
+ auxiliary function *)
+ let name_pat idx (P_aux (p,a)) = match p with
+ | P_as (pat,_) -> P_aux (p,a) (* already named *)
+ | P_lit _ -> P_aux (p,a) (* no need to name a literal *)
+ | P_id _ -> P_aux (p,a) (* no need to name an identifier *)
+ | _ -> P_aux (P_as (P_aux (p,a), Id_aux (Id ("arg" ^ string_of_int idx),l)),a) in
+ let named_argspat = List.mapi name_pat argspat in
+ let named_pat = P_aux (P_app (Id_aux (Id ctor,l),named_argspat),pannot) in
+ let doc_arg idx (P_aux (p,(l,a))) = match p with
+ | P_as (pat,id) -> doc_id_lem id
+ | P_lit lit -> doc_lit_lem false lit a
+ | P_id id -> doc_id_lem id
+ | _ -> string ("arg" ^ string_of_int idx) in
+ let clauses =
+ clauses ^^ (break 1) ^^
+ (separate space
+ [pipe;doc_pat_lem regtypes false named_pat;arrow;
+ string aux_fname;
+ parens (separate comma (List.mapi doc_arg named_argspat))]) in
+ (already_used_fnames,auxiliary_functions,clauses)
+ ) (StringSet.empty,empty,empty) fcls in
+
+ auxiliary_functions ^^ hardline ^^ hardline ^^
+ (prefix 2 1)
+ ((separate space) [string "let" ^^ doc_rec_lem r ^^ doc_id_lem id;equals;string "function"])
+ (clauses ^/^ string "end")
+ | _ ->
+ let clauses =
+ (separate_map (break 1))
+ (fun fcl -> separate space [pipe;doc_funcl_lem regtypes fcl]) fcls in
+ (prefix 2 1)
+ ((separate space) [string "let" ^^ doc_rec_lem r ^^ doc_id_lem id;equals;string "function"])
+ (clauses ^/^ string "end")
+
+
+
+let doc_dec_lem (DEC_aux (reg,(l,annot))) =
+ match reg with
+ | DEC_reg(typ,id) ->
+ (match typ with
+ | Typ_aux (Typ_app (r, [Typ_arg_aux (Typ_arg_typ rt, _)]), _)
+ when string_of_id r = "register" && is_vector_typ rt ->
+ let (start, size, order, etyp) = vector_typ_args_of rt in
+ (match is_bit_typ etyp, start, size with
+ | true, Nexp_aux (Nexp_constant start, _), Nexp_aux (Nexp_constant size, _) ->
+ let o = if is_order_inc order then "true" else "false" in
+ (doc_op equals)
+ (string "let" ^^ space ^^ doc_id_lem id)
+ (string "Register" ^^ space ^^
+ align (separate space [string_lit(doc_id_lem id);
+ doc_int (size);
+ doc_int (start);
+ string o;
+ string "[]"]))
+ ^/^ hardline
+ | _ ->
+ let (Id_aux (Id name,_)) = id in
+ failwith ("can't deal with register " ^ name))
+ | Typ_aux (Typ_app(r, [Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id idt, _)), _)]), _)
+ when string_of_id r = "register" ->
+ separate space [string "let";doc_id_lem id;equals;
+ string "build_" ^^ string (string_of_id idt);string_lit (doc_id_lem id)] ^/^ hardline
+ | Typ_aux (Typ_id idt, _) ->
+ separate space [string "let";doc_id_lem id;equals;
+ string "build_" ^^ string (string_of_id idt);string_lit (doc_id_lem id)] ^/^ hardline
+ |_-> empty)
+ | DEC_alias(id,alspec) -> empty
+ | DEC_typ_alias(typ,id,alspec) -> empty
+
+let doc_spec_lem regtypes (VS_aux (valspec,annot)) =
+ match valspec with
+ | VS_extern_no_rename _
+ | VS_extern_spec _ -> empty (* ignore these at the moment *)
+ | VS_val_spec (typschm,id) | VS_cast_spec (typschm,id) -> empty
+(* separate space [string "val"; doc_id_lem id; string ":";doc_typschm_lem regtypes typschm] ^/^ hardline *)
+
+
+let rec doc_def_lem regtypes def = match def with
+ | DEF_spec v_spec -> (doc_spec_lem regtypes v_spec,empty)
+ | DEF_overload _ -> (empty,empty)
+ | DEF_type t_def -> (group (doc_typdef_lem regtypes t_def) ^/^ hardline,empty)
+ | DEF_reg_dec dec -> (group (doc_dec_lem dec),empty)
+
+ | DEF_default df -> (empty,empty)
+ | DEF_fundef f_def -> (empty,group (doc_fundef_lem regtypes f_def) ^/^ hardline)
+ | DEF_val lbind -> (empty,group (doc_let_lem regtypes lbind) ^/^ hardline)
+ | DEF_scattered sdef -> failwith "doc_def_lem: shoulnd't have DEF_scattered at this point"
+
+ | DEF_kind _ -> (empty,empty)
+
+ | DEF_comm (DC_comm s) -> (empty,comment (string s))
+ | DEF_comm (DC_comm_struct d) ->
+ let (typdefs,vdefs) = doc_def_lem regtypes d in
+ (empty,comment (typdefs ^^ hardline ^^ vdefs))
+
+
+let doc_defs_lem regtypes (Defs defs) =
+ let (typdefs,valdefs) = List.split (List.map (doc_def_lem regtypes) defs) in
+ (separate empty typdefs,separate empty valdefs)
+
+let find_regtypes (Defs defs) =
+ List.fold_left
+ (fun acc def ->
+ match def with
+ | DEF_type (TD_aux(TD_register (Id_aux (Id tname, _),_,_,_),_)) -> tname :: acc
+ | _ -> acc
+ ) [] defs
+
+
+let typ_to_t env =
+ Type_check.typ_to_t env false false
+
+let pp_defs_lem (types_file,types_modules) (prompt_file,prompt_modules) (state_file,state_modules) d top_line =
+ let regtypes = find_regtypes d in
+ let (typdefs,valdefs) = doc_defs_lem regtypes d in
+ (print types_file)
+ (concat
+ [string "(*" ^^ (string top_line) ^^ string "*)";hardline;
+ (separate_map hardline)
+ (fun lib -> separate space [string "open import";string lib]) types_modules;hardline;
+ if !print_to_from_interp_value
+ then
+ concat
+ [(separate_map hardline)
+ (fun lib -> separate space [string " import";string lib]) ["Interp";"Interp_ast"];
+ string "open import Deep_shallow_convert";
+ hardline;
+ hardline;
+ string "module SI = Interp"; hardline;
+ string "module SIA = Interp_ast"; hardline;
+ hardline]
+ else empty;
+ typdefs]);
+ (print prompt_file)
+ (concat
+ [string "(*" ^^ (string top_line) ^^ string "*)";hardline;
+ (separate_map hardline)
+ (fun lib -> separate space [string "open import";string lib]) prompt_modules;hardline;
+ hardline;
+ valdefs]);
+ (print state_file)
+ (concat
+ [string "(*" ^^ (string top_line) ^^ string "*)";hardline;
+ (separate_map hardline)
+ (fun lib -> separate space [string "open import";string lib]) state_modules;hardline;
+ hardline;
+ valdefs]);
diff --git a/src/rewriter_new_tc.ml b/src/rewriter_new_tc.ml
index c76254f1..842ebdef 100644
--- a/src/rewriter_new_tc.ml
+++ b/src/rewriter_new_tc.ml
@@ -9,6 +9,7 @@
(* Robert Norton-Wright *)
(* Christopher Pulte *)
(* Peter Sewell *)
+(* Thomas Bauereiss *)
(* *)
(* All rights reserved. *)
(* *)
@@ -64,67 +65,32 @@ type 'a rewriters = {
let (>>) f g = fun x -> g(f(x))
-let raise_typ_err l m = raise (Reporting_basic.err_typ l m)
-
-let get_env_annot = function
+let env_of_annot = function
| (_,Some(env,_,_)) -> env
| (l,None) -> Env.empty
-let get_typ_annot = function
+let env_of (E_aux (_,a)) = env_of_annot a
+
+(*let typ_of_annot = function
| (_,Some(_,typ,_)) -> typ
- | (l,None) -> raise_typ_err l "no type information"
+ | (l,None) -> raise (Reporting_basic.err_typ l "no type information")
-let get_eff_annot = function
+let effect_of_annot = function
| (_,Some(_,_,eff)) -> eff
| (l,None) -> no_effect
-let get_env_exp (E_aux (_,a)) = get_env_annot a
-let get_typ_exp (E_aux (_,a)) = get_typ_annot a
-let get_eff_exp (E_aux (_,a)) = get_eff_annot a
-let get_eff_fpat (FP_aux (_,a)) = get_eff_annot a
-let get_eff_lexp (LEXP_aux (_,a)) = get_eff_annot a
-let get_eff_fexp (FE_aux (_,a)) = get_eff_annot a
-let get_eff_fexps (FES_aux (FES_Fexps (fexps,_),_)) =
- List.fold_left union_effects no_effect (List.map get_eff_fexp fexps)
-let get_eff_opt_default (Def_val_aux (_,a)) = get_eff_annot a
-let get_eff_pexp (Pat_aux (_,a)) = get_eff_annot a
-let get_eff_lb (LB_aux (_,a)) = get_eff_annot a
+let typ_of (E_aux (_,a)) = typ_of_annot a*)
+let effect_of_fpat (FP_aux (_,(_,a))) = effect_of_annot a
+let effect_of_lexp (LEXP_aux (_,(_,a))) = effect_of_annot a
+let effect_of_fexp (FE_aux (_,(_,a))) = effect_of_annot a
+let effect_of_fexps (FES_aux (FES_Fexps (fexps,_),_)) =
+ List.fold_left union_effects no_effect (List.map effect_of_fexp fexps)
+let effect_of_opt_default (Def_val_aux (_,(_,a))) = effect_of_annot a
+let effect_of_pexp (Pat_aux (_,(_,a))) = effect_of_annot a
+let effect_of_lb (LB_aux (_,(_,a))) = effect_of_annot a
let get_loc_exp (E_aux (_,(l,_))) = l
-let rec is_vector_typ = function
- | Typ_aux (Typ_app (Id_aux (Id "vector",_), [_;_;_;_]), _) -> true
- | Typ_aux (Typ_app (Id_aux (Id "register",_), [Typ_arg_aux (Typ_arg_typ rtyp,_)]), _) ->
- is_vector_typ rtyp
- | _ -> false
-
-let get_typ_app_args = function
- | Typ_aux (Typ_app (Id_aux (Id c,_), targs), l) ->
- (c, List.map (fun (Typ_arg_aux (a,_)) -> a) targs, l)
- | Typ_aux (_, l) -> raise (Reporting_basic.err_typ l "get_typ_app_args called on non-app type")
-
-let rec get_vector_typ_args typ = match get_typ_app_args typ with
- | ("vector", [Typ_arg_nexp start; Typ_arg_nexp len; Typ_arg_order ord; Typ_arg_typ etyp], _) ->
- (start, len, ord, etyp)
- | ("register", [Typ_arg_typ rtyp], _) -> get_vector_typ_args rtyp
- | (_, _, l) -> raise (Reporting_basic.err_typ l "get_vector_typ_args called on non-vector type")
-
-let order_is_inc = function
- | Ord_aux (Ord_inc, _) -> true
- | Ord_aux (Ord_dec, _) -> false
- | Ord_aux (Ord_var _, l) ->
- raise (Reporting_basic.err_unreachable l "order_is_inc called on vector with variable ordering")
-
-let is_bit_typ = function
- | Typ_aux (Typ_id (Id_aux (Id "bit", _)), _) -> true
- | _ -> false
-
-let is_bitvector_typ typ =
- if is_vector_typ typ then
- let (_,_,_,etyp) = get_vector_typ_args typ in
- is_bit_typ etyp
- else false
-
let simple_annot l typ = (Parse_ast.Generated l, Some (Env.empty, typ, no_effect))
let simple_num l n = E_aux (
E_lit (L_aux (L_num n, Parse_ast.Generated l)),
@@ -153,7 +119,7 @@ let fresh_id_pat pre ((l,annot)) =
P_aux (P_id id, (Parse_ast.Generated l, annot))
let union_eff_exps es =
- List.fold_left union_effects no_effect (List.map get_eff_exp es)
+ List.fold_left union_effects no_effect (List.map effect_of es)
let fix_eff_exp (E_aux (e,((l,_) as annot))) = match snd annot with
| Some (env, typ, eff) ->
@@ -162,7 +128,7 @@ let fix_eff_exp (E_aux (e,((l,_) as annot))) = match snd annot with
| E_nondet es -> union_eff_exps es
| E_id _
| E_lit _ -> no_effect
- | E_cast (_,e) -> get_eff_exp e
+ | E_cast (_,e) -> effect_of e
| E_app (_,es)
| E_tuple es -> union_eff_exps es
| E_app_infix (e1,_,e2) -> union_eff_exps [e1;e2]
@@ -171,7 +137,7 @@ let fix_eff_exp (E_aux (e,((l,_) as annot))) = match snd annot with
| E_vector es -> union_eff_exps es
| E_vector_indexed (ies,opt_default) ->
let (_,es) = List.split ies in
- union_effects (get_eff_opt_default opt_default) (union_eff_exps es)
+ union_effects (effect_of_opt_default opt_default) (union_eff_exps es)
| E_vector_access (e1,e2) -> union_eff_exps [e1;e2]
| E_vector_subrange (e1,e2,e3) -> union_eff_exps [e1;e2;e3]
| E_vector_update (e1,e2,e3) -> union_eff_exps [e1;e2;e3]
@@ -179,27 +145,27 @@ let fix_eff_exp (E_aux (e,((l,_) as annot))) = match snd annot with
| E_vector_append (e1,e2) -> union_eff_exps [e1;e2]
| E_list es -> union_eff_exps es
| E_cons (e1,e2) -> union_eff_exps [e1;e2]
- | E_record fexps -> get_eff_fexps fexps
+ | E_record fexps -> effect_of_fexps fexps
| E_record_update(e,fexps) ->
- union_effects (get_eff_exp e) (get_eff_fexps fexps)
- | E_field (e,_) -> get_eff_exp e
+ union_effects (effect_of e) (effect_of_fexps fexps)
+ | E_field (e,_) -> effect_of e
| E_case (e,pexps) ->
- List.fold_left union_effects (get_eff_exp e) (List.map get_eff_pexp pexps)
- | E_let (lb,e) -> union_effects (get_eff_lb lb) (get_eff_exp e)
- | E_assign (lexp,e) -> union_effects (get_eff_lexp lexp) (get_eff_exp e)
- | E_exit e -> get_eff_exp e
- | E_return e -> get_eff_exp e
+ List.fold_left union_effects (effect_of e) (List.map effect_of_pexp pexps)
+ | E_let (lb,e) -> union_effects (effect_of_lb lb) (effect_of e)
+ | E_assign (lexp,e) -> union_effects (effect_of_lexp lexp) (effect_of e)
+ | E_exit e -> effect_of e
+ | E_return e -> effect_of e
| E_sizeof _ | E_sizeof_internal _ -> no_effect
| E_assert (c,m) -> no_effect
| E_comment _ | E_comment_struc _ -> no_effect
- | E_internal_cast (_,e) -> get_eff_exp e
+ | E_internal_cast (_,e) -> effect_of e
| E_internal_exp _ -> no_effect
| E_internal_exp_user _ -> no_effect
| E_internal_let (lexp,e1,e2) ->
- union_effects (get_eff_lexp lexp)
- (union_effects (get_eff_exp e1) (get_eff_exp e2))
- | E_internal_plet (_,e1,e2) -> union_effects (get_eff_exp e1) (get_eff_exp e2)
- | E_internal_return e1 -> get_eff_exp e1)
+ union_effects (effect_of_lexp lexp)
+ (union_effects (effect_of e1) (effect_of e2))
+ | E_internal_plet (_,e1,e2) -> union_effects (effect_of e1) (effect_of e2)
+ | E_internal_return e1 -> effect_of e1)
in
E_aux (e, (l, Some (env, typ, effsum)))
| None ->
@@ -211,11 +177,11 @@ let fix_eff_lexp (LEXP_aux (lexp,((l,_) as annot))) = match snd annot with
| LEXP_id _ -> no_effect
| LEXP_cast _ -> no_effect
| LEXP_memory (_,es) -> union_eff_exps es
- | LEXP_vector (lexp,e) -> union_effects (get_eff_lexp lexp) (get_eff_exp e)
+ | LEXP_vector (lexp,e) -> union_effects (effect_of_lexp lexp) (effect_of e)
| LEXP_vector_range (lexp,e1,e2) ->
- union_effects (get_eff_lexp lexp)
- (union_effects (get_eff_exp e1) (get_eff_exp e2))
- | LEXP_field (lexp,_) -> get_eff_lexp lexp) in
+ union_effects (effect_of_lexp lexp)
+ (union_effects (effect_of e1) (effect_of e2))
+ | LEXP_field (lexp,_) -> effect_of_lexp lexp) in
LEXP_aux (lexp, (l, Some (env, typ, effsum)))
| None ->
LEXP_aux (lexp, (l, None))
@@ -223,7 +189,7 @@ let fix_eff_lexp (LEXP_aux (lexp,((l,_) as annot))) = match snd annot with
let fix_eff_fexp (FE_aux (fexp,((l,_) as annot))) = match snd annot with
| Some (env, typ, eff) ->
let effsum = union_effects eff (match fexp with
- | FE_Fexp (_,e) -> get_eff_exp e) in
+ | FE_Fexp (_,e) -> effect_of e) in
FE_aux (fexp, (l, Some (env, typ, effsum)))
| None ->
FE_aux (fexp, (l, None))
@@ -234,7 +200,7 @@ let fix_eff_opt_default (Def_val_aux (opt_default,((l,_) as annot))) = match snd
| Some (env, typ, eff) ->
let effsum = union_effects eff (match opt_default with
| Def_val_empty -> no_effect
- | Def_val_dec e -> get_eff_exp e) in
+ | Def_val_dec e -> effect_of e) in
Def_val_aux (opt_default, (l, Some (env, typ, effsum)))
| None ->
Def_val_aux (opt_default, (l, None))
@@ -242,7 +208,7 @@ let fix_eff_opt_default (Def_val_aux (opt_default,((l,_) as annot))) = match snd
let fix_eff_pexp (Pat_aux (pexp,((l,_) as annot))) = match snd annot with
| Some (env, typ, eff) ->
let effsum = union_effects eff (match pexp with
- | Pat_exp (_,e) -> get_eff_exp e) in
+ | Pat_exp (_,e) -> effect_of e) in
Pat_aux (pexp, (l, Some (env, typ, effsum)))
| None ->
Pat_aux (pexp, (l, None))
@@ -250,8 +216,8 @@ let fix_eff_pexp (Pat_aux (pexp,((l,_) as annot))) = match snd annot with
let fix_eff_lb (LB_aux (lb,((l,_) as annot))) = match snd annot with
| Some (env, typ, eff) ->
let effsum = union_effects eff (match lb with
- | LB_val_explicit (_,_,e) -> get_eff_exp e
- | LB_val_implicit (_,e) -> get_eff_exp e) in
+ | LB_val_explicit (_,_,e) -> effect_of e
+ | LB_val_implicit (_,e) -> effect_of e) in
LB_aux (lb, (l, Some (env, typ, effsum)))
| None ->
LB_aux (lb, (l, None))
@@ -266,7 +232,7 @@ let effectful_effs = function
) effs
| _ -> true
-let effectful eaux = effectful_effs (get_eff_exp eaux)
+let effectful eaux = effectful_effs (effect_of eaux)
let updates_vars_effs = function
| Effect_aux (Effect_set effs, _) ->
@@ -278,7 +244,7 @@ let updates_vars_effs = function
) effs
| _ -> true
-let updates_vars eaux = updates_vars_effs (get_eff_exp eaux)
+let updates_vars eaux = updates_vars_effs (effect_of eaux)
let id_to_string (Id_aux(id,l)) =
match id with
@@ -462,7 +428,7 @@ let rewrite_exp rewriters (E_aux (exp,(l,annot))) =
| E_assert(e1,e2) -> rewrap (E_assert(rewrite e1,rewrite e2))
| E_internal_cast (casted_annot,exp) ->
rewrap (E_internal_cast (casted_annot, rewrite exp))
- (* check_exp (get_env_exp exp) (strip_exp exp) (get_typ_annot casted_annot) *)
+ (* check_exp (env_of exp) (strip_exp exp) (typ_of_annot casted_annot) *)
(*let new_exp = rewrite exp in
(*let _ = Printf.eprintf "Removing an internal_cast with %s\n" (tannot_to_string casted_annot) in*)
(match casted_annot,exp with
@@ -1009,7 +975,7 @@ let remove_vector_concat_pat pat =
| Some j ->*) simple_num l j in
(*)| None ->
let length_app_exp = unit_exp l (E_app (Id_aux (Id "length",l),[root])) in
- (*let (_,length_root_nexp,_,_) = get_vector_typ_args (snd rannot) in
+ (*let (_,length_root_nexp,_,_) = vector_typ_args_of (snd rannot) in
let length_app_exp : tannot exp =
let typ = mk_atom_typ length_root_nexp in
let annot = (l,tag_annot typ (External (Some "length"))) in
@@ -1023,23 +989,23 @@ let remove_vector_concat_pat pat =
let letbind = fix_eff_lb (LB_aux (LB_val_implicit (P_aux (P_id child,cannot),subv),cannot)) in
(letbind,
- (fun body -> fix_eff_exp (E_aux (E_let (letbind,body), simple_annot l (get_typ_exp body)))),
+ (fun body -> fix_eff_exp (E_aux (E_let (letbind,body), simple_annot l (typ_of body)))),
(rootname,childname)) in
let p_aux = function
| ((P_as (P_aux (P_vector_concat pats,rannot'),rootid),decls),rannot) ->
- let (start,last_idx) = (match get_vector_typ_args (get_typ_annot rannot') with
+ let (start,last_idx) = (match vector_typ_args_of (typ_of_annot rannot') with
| (Nexp_aux (Nexp_constant start,_), Nexp_aux (Nexp_constant length,_), ord, _) ->
- (start, if order_is_inc ord then start + length - 1 else start - length + 1)
+ (start, if is_order_inc ord then start + length - 1 else start - length + 1)
| _ ->
raise (Reporting_basic.err_unreachable (fst rannot')
("unname_vector_concat_elements: vector of unspecified length in vector-concat pattern"))) in
let aux (pos,pat_acc,decl_acc) (P_aux (p,cannot),is_last) =
- let (_,length,ord,_) = get_vector_typ_args (get_typ_annot cannot) in
+ let (_,length,ord,_) = vector_typ_args_of (typ_of_annot cannot) in
(*)| (_,length,ord,_) ->*)
let (pos',index_j) = match length with
| Nexp_aux (Nexp_constant i,_) ->
- if order_is_inc ord then (pos+i, pos+i-1)
+ if is_order_inc ord then (pos+i, pos+i-1)
else (pos-i, pos-i+1)
| Nexp_aux (_,l) ->
if is_last then (pos,last_idx)
@@ -1065,7 +1031,7 @@ let remove_vector_concat_pat pat =
(Reporting_basic.err_unreachable
(fst cannot)
("unname_vector_concat_elements: Non-vector in vector-concat pattern:" ^
- string_of_typ (get_typ_annot cannot))
+ string_of_typ (typ_of_annot cannot))
)*) in
let pats_tagged = tag_last pats in
let (_,pats',decls') = List.fold_left aux (start,[],[]) pats_tagged in
@@ -1155,11 +1121,11 @@ let remove_vector_concat_pat pat =
let remove_vector_concats =
let p_vector_concat ps =
let aux acc (P_aux (p,annot),is_last) =
- let env = get_env_annot annot in
- let eff = get_eff_annot annot in
+ let env = env_of_annot annot in
+ let eff = effect_of_annot (snd annot) in
let (l,_) = annot in
let wild _ = P_aux (P_wild,(Parse_ast.Generated l, Some (env, bit_typ, eff))) in
- match p, get_vector_typ_args (get_typ_annot annot) with
+ match p, vector_typ_args_of (typ_of_annot annot) with
| P_vector ps,_ -> acc @ ps
| _, (_,Nexp_aux (Nexp_constant length,_),_,_) ->
acc @ (List.map wild (range 0 (length - 1)))
@@ -1168,10 +1134,10 @@ let remove_vector_concat_pat pat =
else raise
(Reporting_basic.err_unreachable l
("remove_vector_concats: Non-vector in vector-concat pattern " ^
- string_of_typ (get_typ_annot annot))) in
+ string_of_typ (typ_of_annot annot))) in
let has_length (P_aux (p,annot)) =
- match get_vector_typ_args (get_typ_annot annot) with
+ match vector_typ_args_of (typ_of_annot annot) with
| (_,Nexp_aux (Nexp_constant length,_),_,_) -> true
| _ -> false in
@@ -1250,7 +1216,7 @@ let rec contains_bitvector_pat (P_aux (pat,annot)) = match pat with
| P_lit _ | P_wild | P_id _ -> false
| P_as (pat,_) | P_typ (_,pat) -> contains_bitvector_pat pat
| P_vector _ | P_vector_concat _ | P_vector_indexed _ ->
- is_bitvector_typ (get_typ_annot annot)
+ is_bitvector_typ (typ_of_annot annot)
| P_app (_,pats) | P_tup pats | P_list pats ->
List.exists contains_bitvector_pat pats
| P_record (fpats,_) ->
@@ -1274,7 +1240,7 @@ let remove_bitvector_pat pat =
; p_list = (fun ps -> P_list (List.map (fun p -> p false) ps))
; p_aux =
(fun (pat,annot) contained_in_p_as ->
- let t = get_typ_annot annot in
+ let t = typ_of_annot annot in
let (l,_) = annot in
match pat, is_bitvector_typ t, contained_in_p_as with
| P_vector _, true, false
@@ -1305,10 +1271,10 @@ let remove_bitvector_pat pat =
Some (eqexp) in
let test_subvec_exp rootid l typ i j lits =
- let (start, length, ord, _) = get_vector_typ_args typ in
+ let (start, length, ord, _) = vector_typ_args_of typ in
let length' = nconstant (List.length lits) in
let start' =
- if order_is_inc ord then nconstant 0
+ if is_order_inc ord then nconstant 0
else nminus length' (nconstant 1) in
let typ' = vector_typ start' length' ord bit_typ in
let subvec_exp =
@@ -1355,9 +1321,9 @@ let remove_bitvector_pat pat =
(* Collect guards and let bindings *)
let guard_bitvector_pat =
let collect_guards_decls ps rootid t =
- let (start,_,ord,_) = get_vector_typ_args t in
+ let (start,_,ord,_) = vector_typ_args_of t in
let rec collect current (guards,dls) idx ps =
- let idx' = if order_is_inc ord then idx + 1 else idx - 1 in
+ let idx' = if is_order_inc ord then idx + 1 else idx - 1 in
(match ps with
| pat :: ps' ->
(match pat with
@@ -1434,7 +1400,7 @@ let remove_bitvector_pat pat =
; p_list = (fun ps -> let (ps,gdls) = List.split ps in
(P_list ps, flatten_guards_decls gdls))
; p_aux = (fun ((pat,gdls),annot) ->
- let t = get_typ_annot annot in
+ let t = typ_of_annot annot in
(match pat, is_bitvector_typ t with
| P_as (P_aux (P_vector ps, _), id), true ->
(P_aux (P_id id, annot), collect_guards_decls ps id t)
@@ -1480,11 +1446,11 @@ let rec subsumes_pat (P_aux (p1,annot1) as pat1) (P_aux (p2,annot2) as pat2) =
| _, P_typ (_,pat2) -> subsumes_pat pat1 pat2
| P_id (Id_aux (id1,_) as aid1), P_id (Id_aux (id2,_) as aid2) ->
if id1 = id2 then Some []
- else if Env.lookup_id aid1 (get_env_annot annot1) = Unbound &&
- Env.lookup_id aid2 (get_env_annot annot2) = Unbound
+ else if Env.lookup_id aid1 (env_of_annot annot1) = Unbound &&
+ Env.lookup_id aid2 (env_of_annot annot2) = Unbound
then Some [(id2,id1)] else None
| P_id id1, _ ->
- if Env.lookup_id id1 (get_env_annot annot1) = Unbound then Some [] else None
+ if Env.lookup_id id1 (env_of_annot annot1) = Unbound then Some [] else None
| P_wild, _ -> Some []
| P_app (Id_aux (id1,l1),args1), P_app (Id_aux (id2,_),args2) ->
if id1 = id2 then subsumes_list subsumes_pat args1 args2 else None
@@ -1544,8 +1510,8 @@ and fpat_to_fexp (FP_aux (FP_Fpat (id,pat),(l,annot))) =
let case_exp e t cs =
let pexp (pat,body,annot) = Pat_aux (Pat_exp (pat,body),annot) in
let ps = List.map pexp cs in
- (* let efr = union_effs (List.map get_eff_pexp ps) in *)
- fix_eff_exp (E_aux (E_case (e,ps), (get_loc_exp e, Some (get_env_exp e, t, no_effect))))
+ (* let efr = union_effs (List.map effect_of_pexp ps) in *)
+ fix_eff_exp (E_aux (E_case (e,ps), (get_loc_exp e, Some (env_of e, t, no_effect))))
let rewrite_guarded_clauses l cs =
let rec group clauses =
@@ -1590,7 +1556,7 @@ let rewrite_guarded_clauses l cs =
let else_exp =
if equiv_pats current_pat pat'
then if_exp current_pat (c' :: cs)
- else case_exp (pat_to_exp current_pat) (get_typ_annot annot') (group (c' :: cs)) in
+ else case_exp (pat_to_exp current_pat) (typ_of_annot annot') (group (c' :: cs)) in
fix_eff_exp (E_aux (E_if (exp,body,else_exp), annot))
| None -> body)
| [(pat,guard,body,annot)] -> body
@@ -1620,9 +1586,9 @@ let rewrite_exp_remove_bitvector_pat rewriters (E_aux (exp,(l,annot)) as full_ex
let exp_e' = E_aux (E_id fresh, gen_annot l (get_type e) pure_e) in
let pat_e' = P_aux (P_id fresh, gen_annot l (get_type e) pure_e) in *)
let letbind_e = LB_aux (LB_val_implicit (pat_e',e), (el,eannot)) in
- let exp' = case_exp exp_e' (get_typ_exp full_exp) clauses in
+ let exp' = case_exp exp_e' (typ_of full_exp) clauses in
rewrap (E_let (letbind_e, exp'))
- else case_exp e (get_typ_exp full_exp) clauses
+ else case_exp e (typ_of full_exp) clauses
| E_let (LB_aux (LB_val_explicit (typ,pat,v),annot'),body) ->
let (pat,(_,decls,_)) = remove_bitvector_pat pat in
rewrap (E_let (LB_aux (LB_val_explicit (typ,pat,rewrite_rec v),annot'),
@@ -1679,7 +1645,7 @@ let rewrite_defs_remove_bitvector_pats (Defs defs) =
let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as full_exp) =
let rewrap e = E_aux (e,annot) in
let rewrap_effects e eff =
- E_aux (e, (l,Some (get_env_annot annot, get_typ_annot annot, eff))) in
+ E_aux (e, (l,Some (env_of_annot annot, typ_of_annot annot, eff))) in
let rewrite_rec = rewriters.rewrite_exp rewriters in
let rewrite_base = rewrite_exp rewriters in
match exp with
@@ -1745,15 +1711,15 @@ let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as f
| E_assign(((LEXP_aux ((LEXP_id id | LEXP_cast (_,id)),lannot)) as le),e) ->
let le' = rewriters.rewrite_lexp rewriters le in
let e' = rewrite_base e in
- let effects = get_eff_exp e' in
- (match Env.lookup_id id (get_env_annot annot) with
+ let effects = effect_of e' in
+ (match Env.lookup_id id (env_of_annot annot) with
| Unbound ->
rewrap_effects
(E_internal_let(le', e', E_aux(E_block [], simple_annot l unit_typ)))
effects
| Local _ ->
- let effects' = union_effects effects (get_eff_annot lannot) in
- let annot' = Some (get_env_annot annot, unit_typ, effects') in
+ let effects' = union_effects effects (effect_of_annot (snd lannot)) in
+ let annot' = Some (env_of_annot annot, unit_typ, effects') in
E_aux((E_assign(le', e')),(l, annot'))
| _ -> rewrite_base full_exp)
| _ -> rewrite_base full_exp
@@ -1836,9 +1802,9 @@ let rewrite_defs_ocaml defs =
let rewrite_defs_remove_blocks =
let letbind_wild v body =
let (E_aux (_,(l,tannot))) = v in
- let annot_pat = (simple_annot l (get_typ_exp v)) in
+ let annot_pat = (simple_annot l (typ_of v)) in
let annot_lb = (Parse_ast.Generated l, tannot) in
- let annot_let = (Parse_ast.Generated l, Some (get_env_exp body, get_typ_exp body, union_eff_exps [v;body])) in
+ let annot_let = (Parse_ast.Generated l, Some (env_of body, typ_of body, union_eff_exps [v;body])) in
E_aux (E_let (LB_aux (LB_val_implicit (P_aux (P_wild,annot_pat),v),annot_lb),body),annot_let) in
let rec f l = function
@@ -1866,14 +1832,14 @@ let rewrite_defs_remove_blocks =
let letbind (v : 'a exp) (body : 'a exp -> 'a exp) : 'a exp =
(* body is a function : E_id variable -> actual body *)
- match get_typ_exp v with
+ match typ_of v with
| Typ_aux (Typ_id (Id_aux (Id "unit", _)), _) ->
let (E_aux (_,(l,annot))) = v in
let e = E_aux (E_lit (L_aux (L_unit,Parse_ast.Generated l)),(simple_annot l unit_typ)) in
let body = body e in
let annot_pat = simple_annot l unit_typ in
let annot_lb = annot_pat in
- let annot_let = (Parse_ast.Generated l, Some (get_env_exp body, get_typ_exp body, union_eff_exps [v;body])) in
+ let annot_let = (Parse_ast.Generated l, Some (env_of body, typ_of body, union_eff_exps [v;body])) in
let pat = P_aux (P_wild,annot_pat) in
E_aux (E_let (LB_aux (LB_val_implicit (pat,v),annot_lb),body),annot_let)
@@ -1883,9 +1849,9 @@ let letbind (v : 'a exp) (body : 'a exp -> 'a exp) : 'a exp =
let e_id = E_aux (E_id id, annot) in
let body = body e_id in
- let annot_pat = simple_annot l (get_typ_exp v) in
+ let annot_pat = simple_annot l (typ_of v) in
let annot_lb = annot_pat in
- let annot_let = (Parse_ast.Generated l, Some (get_env_exp body, get_typ_exp body, union_eff_exps [v;body])) in
+ let annot_let = (Parse_ast.Generated l, Some (env_of body, typ_of body, union_eff_exps [v;body])) in
let pat = P_aux (P_id id,annot_pat) in
E_aux (E_let (LB_aux (LB_val_implicit (pat,v),annot_lb),body),annot_let)
@@ -2077,7 +2043,7 @@ let rewrite_defs_letbind_effects =
| E_case (exp1,pexps) ->
let newreturn =
List.fold_left
- (fun b (Pat_aux (_,annot)) -> b || effectful_effs (get_eff_annot annot))
+ (fun b (Pat_aux (_,(_,annot))) -> b || effectful_effs (effect_of_annot annot))
false pexps in
n_exp_name exp1 (fun exp1 ->
n_pexpL newreturn pexps (fun pexps ->
@@ -2123,8 +2089,8 @@ let rewrite_defs_letbind_effects =
let rewrite_fun _ (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls),fdannot)) =
let newreturn =
List.fold_left
- (fun b (FCL_aux (FCL_Funcl(id,pat,exp),annot)) ->
- b || effectful_effs (get_eff_annot annot)) false funcls in
+ (fun b (FCL_aux (FCL_Funcl(id,pat,exp),(_,annot))) ->
+ b || effectful_effs (effect_of_annot annot)) false funcls in
let rewrite_funcl (FCL_aux (FCL_Funcl(id,pat,exp),annot)) =
let _ = reset_fresh_name_counter () in
FCL_aux (FCL_Funcl (id,pat,n_exp_term newreturn exp),annot)
@@ -2241,7 +2207,7 @@ let find_updated_vars exp =
; lEXP_aux =
(function
| ((Some id,ids,acc),(annot)) ->
- (match Env.lookup_id id (get_env_annot annot) with
+ (match Env.lookup_id id (env_of_annot annot) with
| Unbound | Local _ -> ((id,annot) :: ids,acc)
| _ -> (ids,acc))
| ((_,ids,acc),_) -> (ids,acc)
@@ -2272,22 +2238,22 @@ let mktup l es =
| [e] -> e
| e :: _ ->
let effs =
- List.fold_left (fun acc e -> union_effects acc (get_eff_exp e)) no_effect es in
- let typ = mk_typ (Typ_tup (List.map get_typ_exp es)) in
- E_aux (E_tuple es,(Parse_ast.Generated l, Some (get_env_exp e, typ, effs)))
+ List.fold_left (fun acc e -> union_effects acc (effect_of e)) no_effect es in
+ let typ = mk_typ (Typ_tup (List.map typ_of es)) in
+ E_aux (E_tuple es,(Parse_ast.Generated l, Some (env_of e, typ, effs)))
let mktup_pat l es =
match es with
| [] -> P_aux (P_wild,(simple_annot l unit_typ))
| [E_aux (E_id id,_) as exp] ->
- P_aux (P_id id,(simple_annot l (get_typ_exp exp)))
+ P_aux (P_id id,(simple_annot l (typ_of exp)))
| _ ->
- let typ = mk_typ (Typ_tup (List.map get_typ_exp es)) in
+ let typ = mk_typ (Typ_tup (List.map typ_of es)) in
let pats = List.map (function
| (E_aux (E_id id,_) as exp) ->
- P_aux (P_id id,(simple_annot l (get_typ_exp exp)))
+ P_aux (P_id id,(simple_annot l (typ_of exp)))
| exp ->
- P_aux (P_wild,(simple_annot l (get_typ_exp exp)))) es in
+ P_aux (P_wild,(simple_annot l (typ_of exp)))) es in
P_aux (P_tup pats,(simple_annot l typ))
@@ -2301,31 +2267,31 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
match expaux with
| E_let (lb,exp) ->
let exp = add_vars overwrite exp vars in
- E_aux (E_let (lb,exp),swaptyp (get_typ_exp exp) annot)
+ E_aux (E_let (lb,exp),swaptyp (typ_of exp) annot)
| E_internal_let (lexp,exp1,exp2) ->
let exp2 = add_vars overwrite exp2 vars in
- E_aux (E_internal_let (lexp,exp1,exp2), swaptyp (get_typ_exp exp2) annot)
+ E_aux (E_internal_let (lexp,exp1,exp2), swaptyp (typ_of exp2) annot)
| E_internal_plet (pat,exp1,exp2) ->
let exp2 = add_vars overwrite exp2 vars in
- E_aux (E_internal_plet (pat,exp1,exp2), swaptyp (get_typ_exp exp2) annot)
+ E_aux (E_internal_plet (pat,exp1,exp2), swaptyp (typ_of exp2) annot)
| E_internal_return exp2 ->
let exp2 = add_vars overwrite exp2 vars in
- E_aux (E_internal_return exp2,swaptyp (get_typ_exp exp2) annot)
+ E_aux (E_internal_return exp2,swaptyp (typ_of exp2) annot)
| _ ->
(* after rewrite_defs_letbind_effects there cannot be terms that have
effects/update local variables in "tail-position": check n_exp_term
and where it is used. *)
if overwrite then
- match get_typ_exp exp with
+ match typ_of exp with
| Typ_aux (Typ_id (Id_aux (Id "unit", _)), _) -> vars
| _ -> raise (Reporting_basic.err_unreachable l
"add_vars: trying to overwrite a non-unit expression in tail-position")
else
- let typ' = Typ_aux (Typ_tup [get_typ_exp exp;get_typ_exp vars], Parse_ast.Generated l) in
+ let typ' = Typ_aux (Typ_tup [typ_of exp;typ_of vars], Parse_ast.Generated l) in
E_aux (E_tuple [exp;vars],swaptyp typ' annot) in
let rewrite (E_aux (expaux,((el,_) as annot))) (P_aux (_,(pl,pannot)) as pat) =
- let overwrite = match get_typ_annot annot with
+ let overwrite = match typ_of_annot annot with
| Typ_aux (Typ_id (Id_aux (Id "unit", _)), _) -> true
| _ -> false in
match expaux with
@@ -2352,13 +2318,13 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
let loopvar =
(* Don't bother with creating a range type annotation, since the
Lem pretty-printing does not use it. *)
- (* let (bf,tf) = match get_typ_exp exp1 with
+ (* let (bf,tf) = match typ_of exp1 with
| {t = Tapp ("atom",[TA_nexp f])} -> (TA_nexp f,TA_nexp f)
| {t = Tapp ("reg", [TA_typ {t = Tapp ("atom",[TA_nexp f])}])} -> (TA_nexp f,TA_nexp f)
| {t = Tapp ("range",[TA_nexp bf;TA_nexp tf])} -> (TA_nexp bf,TA_nexp tf)
| {t = Tapp ("reg", [TA_typ {t = Tapp ("range",[TA_nexp bf;TA_nexp tf])}])} -> (TA_nexp bf,TA_nexp tf)
| {t = Tapp (name,_)} -> failwith (name ^ " shouldn't be here") in
- let (bt,tt) = match get_typ_exp exp2 with
+ let (bt,tt) = match typ_of exp2 with
| {t = Tapp ("atom",[TA_nexp t])} -> (TA_nexp t,TA_nexp t)
| {t = Tapp ("atom",[TA_typ {t = Tapp ("atom", [TA_nexp t])}])} -> (TA_nexp t,TA_nexp t)
| {t = Tapp ("range",[TA_nexp bt;TA_nexp tt])} -> (TA_nexp bt,TA_nexp tt)
@@ -2373,7 +2339,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
let pat =
if overwrite then mktup_pat el vars
else P_aux (P_tup [pat; mktup_pat pl vars],
- simple_annot pl (get_typ_exp v)) in
+ simple_annot pl (typ_of v)) in
Added_vars (v,pat)
| E_if (c,e1,e2) ->
let vars = List.map (fun (var,(l,t)) -> E_aux (E_id var,(l,t)))
@@ -2385,14 +2351,14 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
let e1 = rewrite_var_updates (add_vars overwrite e1 vartuple) in
let e2 = rewrite_var_updates (add_vars overwrite e2 vartuple) in
(* after rewrite_defs_letbind_effects c has no variable updates *)
- let env = get_env_annot annot in
- let typ = get_typ_exp e1 in
+ let env = env_of_annot annot in
+ let typ = typ_of e1 in
let eff = union_eff_exps [e1;e2] in
let v = E_aux (E_if (c,e1,e2), (Parse_ast.Generated el, Some (env, typ, eff))) in
let pat =
if overwrite then mktup_pat el vars
else P_aux (P_tup [pat; mktup_pat pl vars],
- (simple_annot pl (get_typ_exp v))) in
+ (simple_annot pl (typ_of v))) in
Added_vars (v,pat)
| E_case (e1,ps) ->
(* after rewrite_defs_letbind_effects e1 needs no rewriting *)
@@ -2407,25 +2373,25 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
let vartuple = mktup el vars in
let typ =
let (Pat_aux (Pat_exp (_,first),_)) = List.hd ps in
- get_typ_exp first in
+ typ_of first in
let (ps,typ,effs) =
let f (acc,typ,effs) (Pat_aux (Pat_exp (p,e),pannot)) =
- let etyp = get_typ_exp e in
+ let etyp = typ_of e in
let () = assert (string_of_typ etyp = string_of_typ typ) in
let e = rewrite_var_updates (add_vars overwrite e vartuple) in
- let pannot = simple_annot pl (get_typ_exp e) in
- let effs = union_effects effs (get_eff_exp e) in
+ let pannot = simple_annot pl (typ_of e) in
+ let effs = union_effects effs (effect_of e) in
let pat' = Pat_aux (Pat_exp (p,e),pannot) in
(acc @ [pat'],typ,effs) in
List.fold_left f ([],typ,no_effect) ps in
- let v = E_aux (E_case (e1,ps), (Parse_ast.Generated pl, Some (get_env_annot annot, typ, effs))) in
+ let v = E_aux (E_case (e1,ps), (Parse_ast.Generated pl, Some (env_of_annot annot, typ, effs))) in
let pat =
if overwrite then mktup_pat el vars
else P_aux (P_tup [pat; mktup_pat pl vars],
- (simple_annot pl (get_typ_exp v))) in
+ (simple_annot pl (typ_of v))) in
Added_vars (v,pat)
| E_assign (lexp,vexp) ->
- let effs = match get_eff_annot annot with
+ let effs = match effect_of_annot (snd annot) with
| Effect_aux (Effect_set effs, _) -> effs
| _ ->
raise (Reporting_basic.err_unreachable l
@@ -2435,23 +2401,23 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
else
(match lexp with
| LEXP_aux (LEXP_id id,annot) ->
- let pat = P_aux (P_id id, simple_annot pl (get_typ_exp vexp)) in
+ let pat = P_aux (P_id id, simple_annot pl (typ_of vexp)) in
Added_vars (vexp,pat)
| LEXP_aux (LEXP_cast (_,id),annot) ->
- let pat = P_aux (P_id id, simple_annot pl (get_typ_exp vexp)) in
+ let pat = P_aux (P_id id, simple_annot pl (typ_of vexp)) in
Added_vars (vexp,pat)
| LEXP_aux (LEXP_vector (LEXP_aux (LEXP_id id,((l2,_) as annot2)),i),((l1,_) as annot)) ->
- let eid = E_aux (E_id id, simple_annot l2 (get_typ_annot annot2)) in
+ let eid = E_aux (E_id id, simple_annot l2 (typ_of_annot annot2)) in
let vexp = E_aux (E_vector_update (eid,i,vexp),
- simple_annot l1 (get_typ_annot annot)) in
- let pat = P_aux (P_id id, simple_annot pl (get_typ_exp vexp)) in
+ simple_annot l1 (typ_of_annot annot)) in
+ let pat = P_aux (P_id id, simple_annot pl (typ_of vexp)) in
Added_vars (vexp,pat)
| LEXP_aux (LEXP_vector_range (LEXP_aux (LEXP_id id,((l2,_) as annot2)),i,j),
((l,_) as annot)) ->
- let eid = E_aux (E_id id, simple_annot l2 (get_typ_annot annot2)) in
+ let eid = E_aux (E_id id, simple_annot l2 (typ_of_annot annot2)) in
let vexp = E_aux (E_vector_update_subrange (eid,i,j,vexp),
- simple_annot l (get_typ_annot annot)) in
- let pat = P_aux (P_id id, simple_annot pl (get_typ_exp vexp)) in
+ simple_annot l (typ_of_annot annot)) in
+ let pat = P_aux (P_id id, simple_annot pl (typ_of vexp)) in
Added_vars (vexp,pat))
| _ ->
(* after rewrite_defs_letbind_effects this expression is pure and updates
@@ -2466,29 +2432,29 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
(match rewrite v pat with
| Added_vars (v,pat) ->
let (E_aux (_,(l,_))) = v in
- let lbannot = (simple_annot l (get_typ_exp v)) in
- (get_eff_exp v,LB_aux (LB_val_implicit (pat,v),lbannot))
- | Same_vars v -> (get_eff_exp v,LB_aux (LB_val_implicit (pat,v),lbannot)))
+ let lbannot = (simple_annot l (typ_of v)) in
+ (effect_of v,LB_aux (LB_val_implicit (pat,v),lbannot))
+ | Same_vars v -> (effect_of v,LB_aux (LB_val_implicit (pat,v),lbannot)))
| LB_aux (LB_val_explicit (typ,pat,v),lbannot) ->
(match rewrite v pat with
| Added_vars (v,pat) ->
let (E_aux (_,(l,_))) = v in
- let lbannot = (simple_annot l (get_typ_exp v)) in
- (get_eff_exp v,LB_aux (LB_val_implicit (pat,v),lbannot))
- | Same_vars v -> (get_eff_exp v,LB_aux (LB_val_explicit (typ,pat,v),lbannot))) in
- let tannot = Some (get_env_annot annot, get_typ_exp body, union_effects eff (get_eff_exp body)) in
+ let lbannot = (simple_annot l (typ_of v)) in
+ (effect_of v,LB_aux (LB_val_implicit (pat,v),lbannot))
+ | Same_vars v -> (effect_of v,LB_aux (LB_val_explicit (typ,pat,v),lbannot))) in
+ let tannot = Some (env_of_annot annot, typ_of body, union_effects eff (effect_of body)) in
E_aux (E_let (lb,body),(Parse_ast.Generated l,tannot))
| E_internal_let (lexp,v,body) ->
(* Rewrite E_internal_let into E_let and call recursively *)
let id = match lexp with
| LEXP_aux (LEXP_id id,_) -> id
| LEXP_aux (LEXP_cast (_,id),_) -> id in
- let env = get_env_annot annot in
- let vtyp = get_typ_exp v in
- let veff = get_eff_exp v in
- let bodyenv = get_env_exp body in
- let bodytyp = get_typ_exp body in
- let bodyeff = get_eff_exp body in
+ let env = env_of_annot annot in
+ let vtyp = typ_of v in
+ let veff = effect_of v in
+ let bodyenv = env_of body in
+ let bodytyp = typ_of body in
+ let bodyeff = effect_of body in
let pat = P_aux (P_id id, (simple_annot l vtyp)) in
let lbannot = (Parse_ast.Generated l, Some (env, vtyp, veff)) in
let lb = LB_aux (LB_val_implicit (pat,v),lbannot) in
@@ -2583,7 +2549,7 @@ let rewrite_defs_remove_superfluous_letbinds =
let rewrite_defs_remove_superfluous_returns =
- let has_unittype e = match get_typ_exp e with
+ let has_unittype e = match typ_of e with
| Typ_aux (Typ_id Id_aux (Id "unit", _), _) -> true
| _ -> false in
diff --git a/src/rewriter_new_tc.mli b/src/rewriter_new_tc.mli
index 3d80118a..584d33fa 100644
--- a/src/rewriter_new_tc.mli
+++ b/src/rewriter_new_tc.mli
@@ -9,6 +9,7 @@
(* Robert Norton-Wright *)
(* Christopher Pulte *)
(* Peter Sewell *)
+(* Thomas Bauereiss *)
(* *)
(* All rights reserved. *)
(* *)
diff --git a/src/type_check_new.ml b/src/type_check_new.ml
index 9aeded29..5e625112 100644
--- a/src/type_check_new.ml
+++ b/src/type_check_new.ml
@@ -1376,13 +1376,13 @@ let destructure_vec_typ l env typ =
in
destructure_vec_typ' l (Env.expand_synonyms env typ)
-let typ_of (E_aux (_, (_, tannot))) = match tannot with
+let typ_of_annot (l, tannot) = match tannot with
| Some (_, typ, _) -> typ
- | None -> assert false
+ | None -> raise (Reporting_basic.err_unreachable l "no type annotation")
-let pat_typ_of (P_aux (_, (_, tannot))) = match tannot with
- | Some (_, typ, _) -> typ
- | None -> assert false
+let typ_of (E_aux (_, (l, tannot))) = typ_of_annot (l, tannot)
+
+let pat_typ_of (P_aux (_, (l, tannot))) = typ_of_annot (l, tannot)
(* Flow typing *)
@@ -2190,30 +2190,25 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ =
(* 6. Effect system *)
(**************************************************************************)
-let effect_of (E_aux (exp, (l, annot))) =
- match annot with
- | Some (_, _, eff) -> eff
- | None -> no_effect
+let effect_of_annot = function
+| Some (_, _, eff) -> eff
+| None -> no_effect
+
+let effect_of (E_aux (exp, (l, annot))) = effect_of_annot annot
let add_effect (E_aux (exp, (l, annot))) eff1 =
match annot with
| Some (env, typ, eff2) -> E_aux (exp, (l, Some (env, typ, union_effects eff1 eff2)))
| None -> assert false
-let effect_of_lexp (LEXP_aux (exp, (l, annot))) =
- match annot with
- | Some (_, _, eff) -> eff
- | None -> no_effect
+let effect_of_lexp (LEXP_aux (exp, (l, annot))) = effect_of_annot annot
let add_effect_lexp (LEXP_aux (lexp, (l, annot))) eff1 =
match annot with
| Some (env, typ, eff2) -> LEXP_aux (lexp, (l, Some (env, typ, union_effects eff1 eff2)))
| None -> assert false
-let effect_of_pat (P_aux (exp, (l, annot))) =
- match annot with
- | Some (_, _, eff) -> eff
- | None -> no_effect
+let effect_of_pat (P_aux (exp, (l, annot))) = effect_of_annot annot
let add_effect_pat (P_aux (pat, (l, annot))) eff1 =
match annot with
diff --git a/src/type_check_new.mli b/src/type_check_new.mli
index 2989aa1d..757b6fe3 100644
--- a/src/type_check_new.mli
+++ b/src/type_check_new.mli
@@ -172,10 +172,12 @@ val check_exp : Env.t -> unit exp -> typ -> tannot exp
functions must be guaranteed to have tannots of the form Some (env,
typ) for these to work. *)
val typ_of : tannot exp -> typ
+val typ_of_annot : Ast.l * tannot -> typ
val pat_typ_of : tannot pat -> typ
val effect_of : tannot exp -> effect
+val effect_of_annot : tannot -> effect
val propagate_exp_effect : tannot exp -> tannot exp
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 18:35:11 +0000