(**************************************************************************) (* Sail *) (* *) (* Copyright (c) 2013-2017 *) (* Kathyrn Gray *) (* Shaked Flur *) (* Stephen Kell *) (* Gabriel Kerneis *) (* Robert Norton-Wright *) (* Christopher Pulte *) (* Peter Sewell *) (* Alasdair Armstrong *) (* Brian Campbell *) (* Thomas Bauereiss *) (* Anthony Fox *) (* Jon French *) (* Dominic Mulligan *) (* Stephen Kell *) (* Mark Wassell *) (* *) (* 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 open Ast open Ast_util open Reporting open Rewriter open PPrint open Pretty_print_common module StringSet = Set.Make(String) let opt_undef_axioms = ref false let opt_debug_on : string list ref = ref [] (**************************************************************************** * PPrint-based sail-to-coq pprinter ****************************************************************************) (* Data representation: * * In pure computations we keep values with top level existential types * (including ranges and nats) separate from the proofs of the accompanying * constraints, which keeps the terms shorter and more manageable. * Existentials embedded in types (e.g., in tuples or datatypes) are dependent * pairs. * * Monadic values always includes the proof in a dependent pair because the * constraint solving tactic won't see the term that defined the value, and * must rely entirely on the type (like the Sail type checker). *) type context = { early_ret : bool; kid_renames : kid KBindings.t; (* Plain tyvar -> tyvar renames *) kid_id_renames : id KBindings.t; (* tyvar -> argument renames *) bound_nvars : KidSet.t; build_at_return : string option; recursive_ids : IdSet.t; debug : bool; } let empty_ctxt = { early_ret = false; kid_renames = KBindings.empty; kid_id_renames = KBindings.empty; bound_nvars = KidSet.empty; build_at_return = None; recursive_ids = IdSet.empty; debug = false; } let debug_depth = ref 0 let rec indent n = match n with | 0 -> "" | n -> "| " ^ indent (n - 1) let debug ctxt m = if ctxt.debug then print_endline (indent !debug_depth ^ Lazy.force m) else () let langlebar = string "<|" let ranglebar = string "|>" let anglebars = enclose langlebar ranglebar let enclose_record = enclose (string "{| ") (string " |}") let enclose_record_update = enclose (string "{[ ") (string " ]}") let bigarrow = string "=>" let separate_opt s f l = separate s (Util.map_filter f l) let is_number_char c = c = '0' || c = '1' || c = '2' || c = '3' || c = '4' || c = '5' || c = '6' || c = '7' || c = '8' || c = '9' let is_enum env id = match Env.lookup_id id env with | Enum _ -> true | _ -> false let rec fix_id remove_tick name = match name with | "assert" | "lsl" | "lsr" | "asr" | "type" | "fun" | "function" | "raise" | "try" | "match" | "with" | "check" | "field" | "LT" | "GT" | "EQ" | "Z" | "O" | "S" | "mod" | "M" | "tt" -> name ^ "'" | _ -> if String.contains name '#' then fix_id remove_tick (String.concat "_" (Util.split_on_char '#' name)) else if String.contains name '?' then fix_id remove_tick (String.concat "_pat_" (Util.split_on_char '?' name)) else if String.contains name '^' then fix_id remove_tick (String.concat "__" (Util.split_on_char '^' name)) else if name.[0] = '\'' then let var = String.sub name 1 (String.length name - 1) in if remove_tick then fix_id remove_tick var else (var ^ "'") else if is_number_char(name.[0]) then ("v" ^ name ^ "'") else name let string_id (Id_aux(i,_)) = match i with | Id i -> fix_id false i | DeIid x -> Util.zencode_string ("op " ^ x) let doc_id id = string (string_id id) let doc_id_type (Id_aux(i,_)) = match i with | Id("int") -> string "Z" | Id("real") -> string "R" | Id i -> string (fix_id false i) | DeIid x -> string (Util.zencode_string ("op " ^ x)) let doc_id_ctor (Id_aux(i,_)) = match i with | Id i -> string (fix_id false i) | DeIid x -> string (Util.zencode_string ("op " ^ x)) let doc_var ctx kid = match KBindings.find kid ctx.kid_id_renames with | id -> doc_id id | exception Not_found -> string (fix_id true (string_of_kid (try KBindings.find kid ctx.kid_renames with Not_found -> kid))) let doc_docstring (l, _) = match l with | Parse_ast.Documented (str, _) -> string ("(*" ^ str ^ "*)") ^^ hardline | _ -> empty 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)), simple_annot (Parse_ast.Generated l) (atom_typ (Nexp_aux (Nexp_constant n, Parse_ast.Generated l)))) let effectful_set = function | [] -> false | _ -> true (*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 (Effect_set effs, _)) = effectful_set effs let is_regtyp (Typ_aux (typ, _)) env = match typ with | Typ_app(id, _) when string_of_id id = "register" -> true | _ -> false let doc_nexp ctx ?(skip_vars=KidSet.empty) nexp = (* Print according to Coq's precedence rules *) let rec plussub (Nexp_aux (n,l) as nexp) = match n with | Nexp_sum (n1, n2) -> separate space [plussub n1; plus; mul n2] | Nexp_minus (n1, n2) -> separate space [plussub n1; minus; mul n2] | _ -> mul nexp and mul (Nexp_aux (n,l) as nexp) = match n with | Nexp_times (n1, n2) -> separate space [mul n1; star; uneg n2] | _ -> uneg nexp and uneg (Nexp_aux (n,l) as nexp) = match n with | Nexp_neg n -> separate space [minus; uneg n] | _ -> exp nexp and exp (Nexp_aux (n,l) as nexp) = match n with | Nexp_exp n -> separate space [string "2"; caret; exp n] | _ -> app nexp and app (Nexp_aux (n,l) as nexp) = match n with | Nexp_app (Id_aux (Id "div",_), [n1;n2]) -> separate space [string "ZEuclid.div"; atomic n1; atomic n2] | Nexp_app (Id_aux (Id "mod",_), [n1;n2]) -> separate space [string "ZEuclid.modulo"; atomic n1; atomic n2] | Nexp_app (Id_aux (Id "abs_atom",_), [n1]) -> separate space [string "Z.abs"; atomic n1] | _ -> atomic nexp and atomic (Nexp_aux (n,l) as nexp) = match n with | Nexp_constant i -> string (Big_int.to_string i) | Nexp_var v when KidSet.mem v skip_vars -> string "_" | Nexp_var v -> doc_var ctx v | Nexp_id id -> doc_id id | Nexp_sum _ | Nexp_minus _ | Nexp_times _ | Nexp_neg _ | Nexp_exp _ | Nexp_app (Id_aux (Id ("div"|"mod"),_), [_;_]) | Nexp_app (Id_aux (Id "abs_atom",_), [_]) -> parens (plussub nexp) | _ -> raise (Reporting.err_unreachable l __POS__ ("cannot pretty-print nexp \"" ^ string_of_nexp nexp ^ "\"")) in atomic nexp (* Rewrite mangled names of type variables to the original names *) let rec orig_nexp (Nexp_aux (nexp, l)) = let rewrap nexp = Nexp_aux (nexp, l) in match nexp with | Nexp_var kid -> rewrap (Nexp_var (orig_kid kid)) | Nexp_times (n1, n2) -> rewrap (Nexp_times (orig_nexp n1, orig_nexp n2)) | Nexp_sum (n1, n2) -> rewrap (Nexp_sum (orig_nexp n1, orig_nexp n2)) | Nexp_minus (n1, n2) -> rewrap (Nexp_minus (orig_nexp n1, orig_nexp n2)) | Nexp_exp n -> rewrap (Nexp_exp (orig_nexp n)) | Nexp_neg n -> rewrap (Nexp_neg (orig_nexp n)) | _ -> rewrap nexp let rec orig_nc (NC_aux (nc, l) as full_nc) = let rewrap nc = NC_aux (nc, l) in match nc with | NC_equal (nexp1, nexp2) -> rewrap (NC_equal (orig_nexp nexp1, orig_nexp nexp2)) | NC_bounded_ge (nexp1, nexp2) -> rewrap (NC_bounded_ge (orig_nexp nexp1, orig_nexp nexp2)) | NC_bounded_le (nexp1, nexp2) -> rewrap (NC_bounded_le (orig_nexp nexp1, orig_nexp nexp2)) | NC_not_equal (nexp1, nexp2) -> rewrap (NC_not_equal (orig_nexp nexp1, orig_nexp nexp2)) | NC_set (kid,s) -> rewrap (NC_set (orig_kid kid, s)) | NC_or (nc1, nc2) -> rewrap (NC_or (orig_nc nc1, orig_nc nc2)) | NC_and (nc1, nc2) -> rewrap (NC_and (orig_nc nc1, orig_nc nc2)) | NC_app (f,args) -> rewrap (NC_app (f,List.map orig_typ_arg args)) | NC_var kid -> rewrap (NC_var (orig_kid kid)) | NC_true | NC_false -> full_nc and orig_typ_arg (A_aux (arg,l)) = let rewrap a = (A_aux (a,l)) in match arg with | A_nexp nexp -> rewrap (A_nexp (orig_nexp nexp)) | A_bool nc -> rewrap (A_bool (orig_nc nc)) | A_order _ | A_typ _ -> raise (Reporting.err_unreachable l __POS__ "Tried to pass Type or Order kind to SMT function") (* Returns the set of type variables that will appear in the Coq output, which may be smaller than those in the Sail type. May need to be updated with doc_typ *) let rec coq_nvars_of_typ (Typ_aux (t,l)) = let trec = coq_nvars_of_typ in match t with | Typ_id _ -> KidSet.empty | Typ_var kid -> tyvars_of_nexp (orig_nexp (nvar kid)) | Typ_fn (t1,t2,_) -> List.fold_left KidSet.union (trec t2) (List.map trec t1) | Typ_tup ts -> List.fold_left (fun s t -> KidSet.union s (trec t)) KidSet.empty ts | Typ_app(Id_aux (Id "register", _), [A_aux (A_typ etyp, _)]) -> trec etyp | Typ_app(Id_aux (Id "implicit", _),_) (* TODO: update when complex atom types are sorted out *) | Typ_app(Id_aux (Id "atom", _), _) -> KidSet.empty | Typ_app(Id_aux (Id "atom_bool", _), _) -> KidSet.empty | Typ_app (_,tas) -> List.fold_left (fun s ta -> KidSet.union s (coq_nvars_of_typ_arg ta)) KidSet.empty tas (* TODO: remove appropriate bound variables *) | Typ_exist (_,_,t) -> trec t | Typ_bidir _ -> unreachable l __POS__ "Coq doesn't support bidir types" | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown" and coq_nvars_of_typ_arg (A_aux (ta,_)) = match ta with | A_nexp nexp -> tyvars_of_nexp (orig_nexp nexp) | A_typ typ -> coq_nvars_of_typ typ | A_order _ -> KidSet.empty | A_bool nc -> tyvars_of_constraint (orig_nc nc) let maybe_expand_range_type (Typ_aux (typ,l) as full_typ) = match typ with | Typ_app(Id_aux (Id "range", _), [A_aux(A_nexp low,_); A_aux(A_nexp high,_)]) -> (* TODO: avoid name clashes *) let kid = mk_kid "rangevar" in let var = nvar kid in let nc = nc_and (nc_lteq low var) (nc_lteq var high) in Some (Typ_aux (Typ_exist ([mk_kopt K_int kid], nc, atom_typ var),Parse_ast.Generated l)) | Typ_id (Id_aux (Id "nat",_)) -> let kid = mk_kid "n" in let var = nvar kid in Some (Typ_aux (Typ_exist ([mk_kopt K_int kid], nc_gteq var (nconstant Nat_big_num.zero), atom_typ var), Parse_ast.Generated l)) | _ -> None let expand_range_type typ = Util.option_default typ (maybe_expand_range_type typ) let nice_and nc1 nc2 = match nc1, nc2 with | NC_aux (NC_true,_), _ -> nc2 | _, NC_aux (NC_true,_) -> nc1 | _,_ -> nc_and nc1 nc2 let nice_iff nc1 nc2 = match nc1, nc2 with | NC_aux (NC_true,_), _ -> nc2 | _, NC_aux (NC_true,_) -> nc1 | NC_aux (NC_false,_), _ -> nc_not nc2 | _, NC_aux (NC_false,_) -> nc_not nc1 | _,_ -> nc_or (nc_and nc1 nc2) (nc_and (nc_not nc1) (nc_not nc2)) (* n_constraint functions are currently just Z3 functions *) let doc_nc_fn_prop id = match string_of_id id with | "not" -> string "not" | s -> string s (* n_constraint functions are currently just Z3 functions *) let doc_nc_fn id = match string_of_id id with | "not" -> string "negb" | s -> string s (* When making changes here, check whether they affect coq_nvars_of_typ *) let rec doc_typ_fns ctx = (* following the structure of parser for precedence *) let rec typ ty = fn_typ true ty and typ' ty = fn_typ false ty and fn_typ atyp_needed ((Typ_aux (t, _)) as ty) = match t with | Typ_fn(args,ret,efct) -> let ret_typ = if effectful efct then separate space [string "M"; fn_typ true ret] else separate space [fn_typ false ret] in let arg_typs = List.map (app_typ false) args in let tpp = separate (space ^^ arrow ^^ space) (arg_typs @ [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 atyp_needed ty and tup_typ atyp_needed ((Typ_aux (t, _)) as ty) = match t with | Typ_tup typs -> parens (separate_map (space ^^ star ^^ space) (app_typ false) typs) | _ -> app_typ atyp_needed ty and app_typ atyp_needed ((Typ_aux (t, l)) as ty) = match t with | Typ_app(Id_aux (Id "vector", _), [ A_aux (A_nexp m, _); A_aux (A_order ord, _); A_aux (A_typ elem_typ, _)]) -> (* TODO: remove duplication with exists, below *) let tpp = match elem_typ with | Typ_aux (Typ_id (Id_aux (Id "bit",_)),_) -> (* TODO: coq-compatible simplification *) string "mword " ^^ doc_nexp ctx m | _ -> string "vec" ^^ space ^^ typ elem_typ ^^ space ^^ doc_nexp ctx m in if atyp_needed then parens tpp else tpp | Typ_app(Id_aux (Id "register", _), [A_aux (A_typ etyp, _)]) -> let tpp = string "register_ref regstate register_value " ^^ typ etyp in if atyp_needed then parens tpp else tpp | Typ_app(Id_aux (Id "range", _), _) | Typ_id (Id_aux (Id "nat", _)) -> (match maybe_expand_range_type ty with | Some typ -> atomic_typ atyp_needed typ | None -> raise (Reporting.err_unreachable l __POS__ "Bad range type")) | Typ_app(Id_aux (Id "implicit", _),_) -> (string "Z") | Typ_app(Id_aux (Id "atom", _), [A_aux(A_nexp n,_)]) -> (string "Z") | Typ_app(Id_aux (Id "atom_bool", _), [_]) -> string "bool" | Typ_app (Id_aux (Id "atom#bool",_), [A_aux (A_bool nc,_)]) -> let tpp = string "Bool" ^^ space ^^ doc_nc_prop ~top:false ctx nc in if atyp_needed then parens tpp else tpp | Typ_app(id,args) -> let tpp = (doc_id_type id) ^^ space ^^ (separate_map space doc_typ_arg args) in if atyp_needed then parens tpp else tpp | _ -> atomic_typ atyp_needed ty and atomic_typ atyp_needed ((Typ_aux (t, l)) as ty) = match t with | Typ_id (Id_aux (Id "bool",_)) -> string "bool" | 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_type id | Typ_var v -> doc_var ctx v | Typ_app _ | Typ_tup _ | Typ_fn _ -> (* exhaustiveness matters here to avoid infinite loops * if we add a new Typ constructor *) let tpp = typ ty in if atyp_needed then parens tpp else tpp (* TODO: handle non-integer kopts *) | Typ_exist (kopts,nc,ty') -> begin let kopts,nc,ty' = match maybe_expand_range_type ty' with | Some (Typ_aux (Typ_exist (kopts',nc',ty'),_)) -> kopts'@kopts,nc_and nc nc',ty' | _ -> kopts,nc,ty' in match ty' with | Typ_aux (Typ_app (Id_aux (Id "atom",_), [A_aux (A_nexp nexp,_)]),_) -> begin match nexp, kopts with | (Nexp_aux (Nexp_var kid,_)), [kopt] when Kid.compare kid (kopt_kid kopt) == 0 -> braces (separate space [doc_var ctx kid; colon; string "Z"; ampersand; doc_arithfact ctx nc]) | _ -> let var = mk_kid "_atom" in (* TODO collision avoid *) let nc = nice_and (nc_eq (nvar var) nexp) nc in braces (separate space [doc_var ctx var; colon; string "Z"; ampersand; doc_arithfact ctx ~exists:(List.map kopt_kid kopts) nc]) end | Typ_aux (Typ_app (Id_aux (Id "vector",_), [A_aux (A_nexp m, _); A_aux (A_order ord, _); A_aux (A_typ elem_typ, _)]),_) -> (* TODO: proper handling of m, complex elem type, dedup with above *) let var = mk_kid "_vec" in (* TODO collision avoid *) let kid_set = KidSet.of_list (List.map kopt_kid kopts) in let m_pp = doc_nexp ctx ~skip_vars:kid_set m in let tpp, len_pp = match elem_typ with | Typ_aux (Typ_id (Id_aux (Id "bit",_)),_) -> string "mword " ^^ m_pp, string "length_mword" | _ -> string "vec" ^^ space ^^ typ elem_typ ^^ space ^^ m_pp, string "vec_length" in let length_constraint_pp = if KidSet.is_empty (KidSet.inter kid_set (nexp_frees m)) then None else Some (separate space [len_pp; doc_var ctx var; equals; doc_nexp ctx m]) in braces (separate space [doc_var ctx var; colon; tpp; ampersand; doc_arithfact ctx ~exists:(List.map kopt_kid kopts) ?extra:length_constraint_pp nc]) | Typ_aux (Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]),_) -> let var = mk_kid "_bool" in (* TODO collision avoid *) let nc = nice_and (nice_iff (nc_var var) atom_nc) nc in braces (separate space [doc_var ctx var; colon; string "bool"; ampersand; doc_arithfact ctx ~exists:(List.map kopt_kid kopts) nc]) | _ -> raise (Reporting.err_todo l ("Non-atom existential type not yet supported in Coq: " ^ string_of_typ ty)) end (* let add_tyvar tpp kid = braces (separate space [doc_var ctx kid; colon; string "Z"; ampersand; tpp]) in match drop_duplicate_atoms kids ty with | Some ty -> let tpp = typ ty in let tpp = match nc with NC_aux (NC_true,_) -> tpp | _ -> braces (separate space [underscore; colon; parens (doc_arithfact ctx nc); ampersand; tpp]) in List.fold_left add_tyvar tpp kids | None -> match nc with (* | NC_aux (NC_true,_) -> List.fold_left add_tyvar (string "Z") (List.tl kids)*) | _ -> List.fold_left add_tyvar (doc_arithfact ctx nc) kids end*) | Typ_bidir _ -> unreachable l __POS__ "Coq doesn't support bidir types" | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown" and doc_typ_arg (A_aux(t,_)) = match t with | A_typ t -> app_typ true t | A_nexp n -> doc_nexp ctx n | A_order o -> empty | A_bool nc -> doc_nc_prop ~top:false ctx nc in typ', atomic_typ, doc_typ_arg and doc_typ ctx = let f,_,_ = doc_typ_fns ctx in f and doc_atomic_typ ctx = let _,f,_ = doc_typ_fns ctx in f and doc_typ_arg ctx = let _,_,f = doc_typ_fns ctx in f and doc_arithfact ctxt ?(exists = []) ?extra nc = let prop = doc_nc_prop ctxt nc in let prop = match extra with | None -> prop | Some pp -> separate space [pp; string "/\\"; prop] in let prop = match exists with | [] -> prop | _ -> separate space ([string "exists"]@(List.map (doc_var ctxt) exists)@[comma; prop]) in string "ArithFact" ^^ space ^^ parens prop (* Follows Coq precedence levels *) and doc_nc_prop ?(top = true) ctx nc = let rec l85 (NC_aux (nc,_) as nc_full) = match nc with | NC_or (nc1, nc2) -> doc_op (string "\\/") (doc_nc_prop ctx nc1) (doc_nc_prop ctx nc2) | _ -> l80 nc_full and l80 (NC_aux (nc,_) as nc_full) = match nc with | NC_and (nc1, nc2) -> doc_op (string "/\\") (doc_nc_prop ctx nc1) (doc_nc_prop ctx nc2) | _ -> l70 nc_full and l70 (NC_aux (nc,_) as nc_full) = match nc with | NC_equal (ne1, ne2) -> doc_op equals (doc_nexp ctx ne1) (doc_nexp ctx ne2) | NC_var kid -> doc_op equals (doc_nexp ctx (nvar kid)) (string "true") | NC_bounded_ge (ne1, ne2) -> doc_op (string ">=") (doc_nexp ctx ne1) (doc_nexp ctx ne2) | NC_bounded_le (ne1, ne2) -> doc_op (string "<=") (doc_nexp ctx ne1) (doc_nexp ctx ne2) | NC_not_equal (ne1, ne2) -> doc_op (string "<>") (doc_nexp ctx ne1) (doc_nexp ctx ne2) | _ -> l10 nc_full and l10 (NC_aux (nc,_) as nc_full) = match nc with | NC_set (kid, is) -> separate space [string "In"; doc_var ctx kid; brackets (separate (string "; ") (List.map (fun i -> string (Nat_big_num.to_string i)) is))] | NC_app (f,args) -> separate space (doc_nc_fn_prop f::List.map (doc_typ_arg ctx) args) | _ -> l0 nc_full and l0 (NC_aux (nc,_) as nc_full) = match nc with | NC_true -> string "True" | NC_false -> string "False" | NC_set _ | NC_app _ | NC_var _ | NC_or _ | NC_and _ | NC_equal _ | NC_bounded_ge _ | NC_bounded_le _ | NC_not_equal _ -> parens (l85 nc_full) in if top then l85 nc else l0 nc (* Follows Coq precedence levels *) let rec doc_nc_exp ctx env nc = let nc = Env.expand_constraint_synonyms env nc in let rec l70 (NC_aux (nc,_) as nc_full) = match nc with | NC_equal (ne1, ne2) -> doc_op (string "=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2) | NC_bounded_ge (ne1, ne2) -> doc_op (string ">=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2) | NC_bounded_le (ne1, ne2) -> doc_op (string "<=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2) | _ -> l50 nc_full and l50 (NC_aux (nc,_) as nc_full) = match nc with | NC_or (nc1, nc2) -> doc_op (string "||") (l50 nc1) (l40 nc2) | _ -> l40 nc_full and l40 (NC_aux (nc,_) as nc_full) = match nc with | NC_and (nc1, nc2) -> doc_op (string "&&") (l40 nc1) (l10 nc2) | _ -> l10 nc_full and l10 (NC_aux (nc,_) as nc_full) = match nc with | NC_not_equal (ne1, ne2) -> string "negb" ^^ space ^^ parens (doc_op (string "=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2)) | NC_set (kid, is) -> separate space [string "member_Z_list"; doc_var ctx kid; brackets (separate (string "; ") (List.map (fun i -> string (Nat_big_num.to_string i)) is))] | NC_true -> string "true" | NC_false -> string "false" | NC_app (f,args) -> separate space (doc_nc_fn f::List.map (doc_typ_arg_exp ctx env) args) | NC_var kid -> doc_nexp ctx (nvar kid) | NC_equal _ | NC_bounded_ge _ | NC_bounded_le _ | NC_or _ | NC_and _ -> parens (l70 nc_full) in l70 nc and doc_typ_arg_exp ctx env (A_aux (arg,l)) = match arg with | A_nexp nexp -> doc_nexp ctx nexp | A_bool nc -> doc_nc_exp ctx env nc | A_order _ | A_typ _ -> raise (Reporting.err_unreachable l __POS__ "Tried to pass Type or Order kind to SMT function") (* Check for variables in types that would be pretty-printed and are not bound in the val spec of the function. *) let contains_t_pp_var ctxt (Typ_aux (t,a) as typ) = KidSet.subset (coq_nvars_of_typ typ) ctxt.bound_nvars (* TODO: should we resurrect this? let replace_typ_size ctxt env (Typ_aux (t,a)) = match t with | Typ_app (Id_aux (Id "vector",_) as id, [A_aux (A_nexp size,_);ord;typ']) -> begin let mk_typ nexp = Some (Typ_aux (Typ_app (id, [A_aux (A_nexp nexp,Parse_ast.Unknown);ord;typ']),a)) in match Type_check.solve env size with | Some n -> mk_typ (nconstant n) | None -> let is_equal nexp = prove __POS__ env (NC_aux (NC_equal (size,nexp),Parse_ast.Unknown)) in match List.find is_equal (NexpSet.elements ctxt.bound_nexps) with | nexp -> mk_typ nexp | exception Not_found -> None end | _ -> None*) let doc_tannot ctxt env eff typ = let of_typ typ = let ta = doc_typ ctxt typ in if eff then if ctxt.early_ret then string " : MR " ^^ parens ta ^^ string " _" else string " : M " ^^ parens ta else string " : " ^^ ta in of_typ typ (* Only double-quotes need escaped - by doubling them. *) let coq_escape_string s = Str.global_replace (Str.regexp "\"") "\"\"" s let doc_lit (L_aux(lit,l)) = match lit with | L_unit -> utf8string "tt" | L_zero -> utf8string "B0" | L_one -> utf8string "B1" | L_false -> utf8string "false" | L_true -> utf8string "true" | L_num i -> let s = Big_int.to_string i in let ipp = utf8string s in if Big_int.less i Big_int.zero then parens ipp else ipp | 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 -> utf8string "(Fail \"undefined value of unsupported type\")" | L_string s -> utf8string ("\"" ^ (coq_escape_string s) ^ "\"") | L_real s -> (* Lem does not support decimal syntax, so we translate a string of the form "x.y" into the ratio (x * 10^len(y) + y) / 10^len(y). The OCaml library has a conversion function from strings to floats, but not from floats to ratios. ZArith's Q library does have the latter, but using this would require adding a dependency on ZArith to Sail. *) let parts = Util.split_on_char '.' s in let (num, denom) = match parts with | [i] -> (Big_int.of_string i, Big_int.of_int 1) | [i;f] -> let denom = Big_int.pow_int_positive 10 (String.length f) in (Big_int.add (Big_int.mul (Big_int.of_string i) denom) (Big_int.of_string f), denom) | _ -> raise (Reporting.Fatal_error (Reporting.Err_syntax_locn (l, "could not parse real literal"))) in parens (separate space (List.map string [ "realFromFrac"; Big_int.to_string num; Big_int.to_string denom])) let doc_quant_item_id ctx delimit (QI_aux (qi,_)) = match qi with | QI_id (KOpt_aux (KOpt_kind (K_aux (kind,_),kid),_)) -> begin if KBindings.mem kid ctx.kid_id_renames then None else match kind with | K_type -> Some (delimit (separate space [doc_var ctx kid; colon; string "Type"])) | K_int -> Some (delimit (separate space [doc_var ctx kid; colon; string "Z"])) | K_order -> None | K_bool -> Some (delimit (separate space [doc_var ctx kid; colon; string "bool"])) end | QI_const nc -> None let quant_item_id_name ctx (QI_aux (qi,_)) = match qi with | QI_id (KOpt_aux (KOpt_kind (K_aux (kind,_),kid),_)) -> begin if KBindings.mem kid ctx.kid_id_renames then None else match kind with | K_type -> Some (doc_var ctx kid) | K_int -> Some (doc_var ctx kid) | K_order -> None | K_bool -> Some (doc_var ctx kid) end | QI_const nc -> None let doc_quant_item_constr ctx delimit (QI_aux (qi,_)) = match qi with | QI_id _ -> None | QI_const nc -> Some (bquote ^^ braces (doc_arithfact ctx nc)) (* At the moment these are all anonymous - when used we rely on Coq to fill them in. *) let quant_item_constr_name ctx (QI_aux (qi,_)) = match qi with | QI_id _ -> None | QI_const nc -> Some underscore let doc_typquant_items ctx delimit (TypQ_aux (tq,_)) = match tq with | TypQ_tq qis -> separate_opt space (doc_quant_item_id ctx delimit) qis ^^ separate_opt space (doc_quant_item_constr ctx delimit) qis | TypQ_no_forall -> empty let doc_typquant_items_separate ctx delimit (TypQ_aux (tq,_)) = match tq with | TypQ_tq qis -> Util.map_filter (doc_quant_item_id ctx delimit) qis, Util.map_filter (doc_quant_item_constr ctx delimit) qis | TypQ_no_forall -> [], [] let typquant_names_separate ctx (TypQ_aux (tq,_)) = match tq with | TypQ_tq qis -> Util.map_filter (quant_item_id_name ctx) qis, Util.map_filter (quant_item_constr_name ctx) qis | TypQ_no_forall -> [], [] let doc_typquant ctx (TypQ_aux(tq,_)) typ = match tq with | TypQ_tq ((_ :: _) as qs) -> string "forall " ^^ separate_opt space (doc_quant_item_id ctx braces) qs ^/^ separate_opt space (doc_quant_item_constr ctx parens) qs ^^ string ", " ^^ typ | _ -> typ (* Produce Size type constraints for bitvector sizes when using machine words. Often these will be unnecessary, but this simple approach will do for now. *) let rec typeclass_nexps (Typ_aux(t,l)) = match t with | Typ_id _ | Typ_var _ -> NexpSet.empty | Typ_fn (t1,t2,_) -> List.fold_left NexpSet.union (typeclass_nexps t2) (List.map typeclass_nexps t1) | Typ_tup ts -> List.fold_left NexpSet.union NexpSet.empty (List.map typeclass_nexps ts) | Typ_app (Id_aux (Id "vector",_), [A_aux (A_nexp size_nexp,_); _;A_aux (A_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)]) | Typ_app (Id_aux (Id "itself",_), [A_aux (A_nexp size_nexp,_)]) -> let size_nexp = nexp_simp size_nexp in if is_nexp_constant size_nexp then NexpSet.empty else NexpSet.singleton (orig_nexp size_nexp) | Typ_app _ -> NexpSet.empty | Typ_exist (kids,_,t) -> NexpSet.empty (* todo *) | Typ_bidir _ -> unreachable l __POS__ "Coq doesn't support bidir types" | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown" let doc_typschm ctx quants (TypSchm_aux(TypSchm_ts(tq,t),_)) = let pt = doc_typ ctx t in if quants then doc_typquant ctx tq pt else pt let is_ctor env id = match Env.lookup_id id env with | Enum _ -> true | _ -> false let is_auto_decomposed_exist env typ = let typ = expand_range_type typ in match destruct_exist_plain (Env.expand_synonyms env typ) with | Some (_, _, typ') -> Some typ' | _ -> None (*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 ctxt apat_needed exists_as_pairs (P_aux (p,(l,annot)) as pat, typ) = let env = env_of_annot (l,annot) in let typ = Env.expand_synonyms env typ in match exists_as_pairs, is_auto_decomposed_exist env typ with | true, Some typ' -> let pat_pp = doc_pat ctxt true true (pat, typ') in let pat_pp = separate space [string "existT"; underscore; pat_pp; underscore] in if apat_needed then parens pat_pp else pat_pp | _ -> match p with (* Special case translation of the None constructor to remove the unit arg *) | P_app(id, _) when string_of_id id = "None" -> string "None" | P_app(id, ((_ :: _) as pats)) -> begin (* Following the type checker to get the subpattern types, TODO perhaps ought to persuade the type checker to output these somehow. *) let (typq, ctor_typ) = Env.get_val_spec id env in let arg_typs = match Env.expand_synonyms env ctor_typ with | Typ_aux (Typ_fn (arg_typs, ret_typ, _), _) -> let unifiers = unify l env (tyvars_of_typ ret_typ) ret_typ typ in List.map (subst_unifiers unifiers) arg_typs | _ -> assert false in (* Constructors that were specified without a return type might get an extra tuple in their type; expand that here if necessary. TODO: this should go away if we enforce proper arities. *) let arg_typs = match pats, arg_typs with | _::_::_, [Typ_aux (Typ_tup typs,_)] -> typs | _,_ -> arg_typs in let ppp = doc_unop (doc_id_ctor id) (parens (separate_map comma (doc_pat ctxt true true) (List.combine pats arg_typs))) in if apat_needed then parens ppp else ppp end | P_app(id, []) -> doc_id_ctor id | P_lit lit -> doc_lit lit | P_wild -> underscore | P_id id -> doc_id id | P_var(p,_) -> doc_pat ctxt true exists_as_pairs (p, typ) | P_as(p,id) -> parens (separate space [doc_pat ctxt true exists_as_pairs (p, typ); string "as"; doc_id id]) | P_typ(ptyp,p) -> let doc_p = doc_pat ctxt true exists_as_pairs (p, typ) in doc_p (* Type annotations aren't allowed everywhere in patterns in Coq *) (*parens (doc_op colon doc_p (doc_typ typ))*) | P_vector pats -> let el_typ = match destruct_vector env typ with | Some (_,_,t) -> t | None -> raise (Reporting.err_unreachable l __POS__ "vector pattern doesn't have vector type") in let ppp = brackets (separate_map semi (fun p -> doc_pat ctxt true exists_as_pairs (p,el_typ)) pats) in if apat_needed then parens ppp else ppp | P_vector_concat pats -> raise (Reporting.err_unreachable l __POS__ "vector concatenation patterns should have been removed before pretty-printing") | P_tup pats -> let typs = match typ with | Typ_aux (Typ_tup typs, _) -> typs | _ -> raise (Reporting.err_unreachable l __POS__ "tuple pattern doesn't have tuple type") in (match pats, typs with | [p], [typ'] -> doc_pat ctxt apat_needed true (p, typ') | [_], _ -> raise (Reporting.err_unreachable l __POS__ "tuple pattern length does not match tuple type length") | _ -> parens (separate_map comma_sp (doc_pat ctxt false true) (List.combine pats typs))) | P_list pats -> let el_typ = match typ with | Typ_aux (Typ_app (f, [A_aux (A_typ el_typ,_)]),_) when Id.compare f (mk_id "list") = 0 -> el_typ | _ -> raise (Reporting.err_unreachable l __POS__ "list pattern not a list") in brackets (separate_map semi (fun p -> doc_pat ctxt false true (p, el_typ)) pats) | P_cons (p,p') -> let el_typ = match typ with | Typ_aux (Typ_app (f, [A_aux (A_typ el_typ,_)]),_) when Id.compare f (mk_id "list") = 0 -> el_typ | _ -> raise (Reporting.err_unreachable l __POS__ "list pattern not a list") in doc_op (string "::") (doc_pat ctxt true true (p, el_typ)) (doc_pat ctxt true true (p', typ)) | P_string_append _ -> unreachable l __POS__ "string append pattern found in Coq backend, should have been rewritten" | P_not _ -> unreachable l __POS__ "Coq backend doesn't support not patterns" | P_or _ -> unreachable l __POS__ "Coq backend doesn't support or patterns yet" | P_record (_,_) -> empty (* TODO *) let contains_early_return exp = let e_app (f, args) = let rets, args = List.split args in (List.fold_left (||) (string_of_id f = "early_return") rets, E_app (f, args)) in fst (fold_exp { (Rewriter.compute_exp_alg false (||)) with e_return = (fun (_, r) -> (true, E_return r)); e_app = e_app } exp) let find_e_ids exp = let e_id id = IdSet.singleton id, E_id id in fst (fold_exp { (compute_exp_alg IdSet.empty IdSet.union) with e_id = e_id } exp) let typ_id_of (Typ_aux (typ, l)) = match typ with | Typ_id id -> id | Typ_app (register, [A_aux (A_typ (Typ_aux (Typ_id id, _)), _)]) when string_of_id register = "register" -> id | Typ_app (id, _) -> id | _ -> raise (Reporting.err_unreachable l __POS__ "failed to get type id") (* TODO: maybe Nexp_exp, division? *) (* Evaluation of constant nexp subexpressions, because Coq will be able to do those itself *) let rec nexp_const_eval (Nexp_aux (n,l) as nexp) = let binop f re l n1 n2 = match nexp_const_eval n1, nexp_const_eval n2 with | Nexp_aux (Nexp_constant c1,_), Nexp_aux (Nexp_constant c2,_) -> Nexp_aux (Nexp_constant (f c1 c2),l) | n1', n2' -> Nexp_aux (re n1' n2',l) in let unop f re l n1 = match nexp_const_eval n1 with | Nexp_aux (Nexp_constant c1,_) -> Nexp_aux (Nexp_constant (f c1),l) | n1' -> Nexp_aux (re n1',l) in match n with | Nexp_times (n1,n2) -> binop Big_int.mul (fun n1 n2 -> Nexp_times (n1,n2)) l n1 n2 | Nexp_sum (n1,n2) -> binop Big_int.add (fun n1 n2 -> Nexp_sum (n1,n2)) l n1 n2 | Nexp_minus (n1,n2) -> binop Big_int.sub (fun n1 n2 -> Nexp_minus (n1,n2)) l n1 n2 | Nexp_neg n1 -> unop Big_int.negate (fun n -> Nexp_neg n) l n1 | _ -> nexp (* Decide whether two nexps used in a vector size are similar; if not a cast will be inserted *) let similar_nexps ctxt env n1 n2 = let rec same_nexp_shape (Nexp_aux (n1,_)) (Nexp_aux (n2,_)) = match n1, n2 with | Nexp_id _, Nexp_id _ -> true (* TODO: this is really just an approximation to what we really want: will the Coq types have the same names? We could probably do better by tracking which existential kids are equal to bound kids. *) | Nexp_var k1, Nexp_var k2 -> Kid.compare k1 k2 == 0 || (prove __POS__ env (nc_eq (nvar k1) (nvar k2)) && ( not (KidSet.mem k1 ctxt.bound_nvars) || not (KidSet.mem k2 ctxt.bound_nvars))) | Nexp_constant c1, Nexp_constant c2 -> Nat_big_num.equal c1 c2 | Nexp_app (f1,args1), Nexp_app (f2,args2) -> Id.compare f1 f2 == 0 && List.for_all2 same_nexp_shape args1 args2 | Nexp_times (n1,n2), Nexp_times (n3,n4) | Nexp_sum (n1,n2), Nexp_sum (n3,n4) | Nexp_minus (n1,n2), Nexp_minus (n3,n4) -> same_nexp_shape n1 n3 && same_nexp_shape n2 n4 | Nexp_exp n1, Nexp_exp n2 | Nexp_neg n1, Nexp_neg n2 -> same_nexp_shape n1 n2 | _ -> false in if same_nexp_shape (nexp_const_eval n1) (nexp_const_eval n2) then true else false let constraint_fns = ["Z.leb"; "Z.geb"; "Z.ltb"; "Z.gtb"; "Z.eqb"; "neq_atom"] let condition_produces_constraint exp = (* Cheat a little - this isn't quite the right environment for subexpressions but will have all of the relevant functions in it. *) let env = env_of exp in Rewriter.fold_exp { (Rewriter.pure_exp_alg false (||)) with Rewriter.e_app = fun (f,bs) -> List.exists (fun x -> x) bs || (let name = if Env.is_extern f env "coq" then Env.get_extern f env "coq" else string_id f in List.exists (fun id -> String.compare name id == 0) constraint_fns) } exp (* For most functions whose return types are non-trivial atoms we return a dependent pair with a proof that the result is the expected integer. This is redundant for basic arithmetic functions and functions which we unfold in the constraint solver. *) let no_proof_fns = ["Z.add"; "Z.sub"; "Z.opp"; "Z.mul"; "length_mword"; "length"; "negb"; "andb"; "orb"; "Z.leb"; "Z.geb"; "Z.ltb"; "Z.gtb"; "Z.eqb"] let is_no_proof_fn env id = if Env.is_extern id env "coq" then let s = Env.get_extern id env "coq" in List.exists (fun x -> String.compare x s == 0) no_proof_fns else false let replace_atom_return_type ret_typ = (* TODO: more complex uses of atom *) match ret_typ with | Typ_aux (Typ_app (Id_aux (Id "atom",_), [A_aux (A_nexp nexp,_)]),l) -> let kid = mk_kid "_retval" in (* TODO: collision avoidance *) Some "build_ex", Typ_aux (Typ_exist ([mk_kopt K_int kid], nc_eq (nvar kid) nexp, atom_typ (nvar kid)),Parse_ast.Generated l) (* For informative booleans tweak the type name so that doc_typ knows that the constraint should be output. *) | Typ_aux (Typ_app (Id_aux (Id "atom_bool",il), ([A_aux (A_bool _,_)] as args)),l) -> Some "build_Bool", Typ_aux (Typ_app (Id_aux (Id "atom#bool",il), args),l) | _ -> None, ret_typ let is_range_from_atom env (Typ_aux (argty,_)) (Typ_aux (fnty,_)) = match argty, fnty with | Typ_app(Id_aux (Id "atom", _), [A_aux (A_nexp nexp,_)]), Typ_app(Id_aux (Id "range", _), [A_aux(A_nexp low,_); A_aux(A_nexp high,_)]) -> Type_check.prove __POS__ env (nc_and (nc_eq nexp low) (nc_eq nexp high)) | _ -> false (* Get a more general type for an annotation/expression - i.e., like typ_of but using the expected type if there was one *) let general_typ_of_annot annot = match expected_typ_of annot with | None -> typ_of_annot annot | Some typ -> typ let general_typ_of (E_aux (_,annot)) = general_typ_of_annot annot let is_prefix s s' = let l = String.length s in String.length s' >= l && String.sub s' 0 l = s let prefix_recordtype = true let report = Reporting.err_unreachable let doc_exp, doc_let = let rec top_exp (ctxt : context) (aexp_needed : bool) (E_aux (e, (l,annot)) as full_exp) = let top_exp c a e = let () = debug_depth := !debug_depth + 1 in let r = top_exp c a e in let () = debug_depth := !debug_depth - 1 in r in let expY = top_exp ctxt true in let expN = top_exp ctxt false in let expV = top_exp ctxt in let wrap_parens doc = if aexp_needed then parens (doc) else doc in let maybe_add_exist epp = let env = env_of full_exp in let typ = Env.expand_synonyms env (general_typ_of full_exp) in let () = debug ctxt (lazy ("Considering build_ex for " ^ string_of_exp full_exp)); debug ctxt (lazy (" at type " ^ string_of_typ typ)) in let typ = expand_range_type typ in match destruct_exist_plain typ with | None -> epp | Some _ -> let epp = string "build_ex" ^/^ epp in if aexp_needed then parens epp else epp in let rec construct_dep_pairs env = let rec aux want_parens (E_aux (e,_) as exp) (Typ_aux (t,_) as typ) = match e,t with | E_tuple exps, Typ_tup typs | E_cast (_, E_aux (E_tuple exps,_)), Typ_tup typs -> parens (separate (string ", ") (List.map2 (aux false) exps typs)) | _ -> let typ' = expand_range_type (Env.expand_synonyms (env_of exp) typ) in let build_ex, out_typ = match destruct_exist_plain typ' with | Some (_,_,t) -> true, t | None -> false, typ' in let in_typ = expand_range_type (Env.expand_synonyms (env_of exp) (typ_of exp)) in let in_typ = match destruct_exist_plain in_typ with Some (_,_,t) -> t | None -> in_typ in let autocast = (* Avoid using helper functions which simplify the nexps *) is_bitvector_typ in_typ && is_bitvector_typ out_typ && match in_typ, out_typ with | Typ_aux (Typ_app (_,[A_aux (A_nexp n1,_);_;_]),_), Typ_aux (Typ_app (_,[A_aux (A_nexp n2,_);_;_]),_) -> not (similar_nexps ctxt (env_of exp) n1 n2) | _ -> false in let exp_pp = expV (want_parens || autocast || build_ex) exp in let exp_pp = if autocast then let exp_pp = string "autocast" ^^ space ^^ exp_pp in if want_parens || build_ex then parens exp_pp else exp_pp else exp_pp in if build_ex then let exp_pp = string "build_ex" ^^ space ^^ exp_pp in if want_parens then parens exp_pp else exp_pp else exp_pp in aux in let liftR doc = if ctxt.early_ret && effectful (effect_of full_exp) then separate space [string "liftR"; parens (doc)] else doc in match e with | E_assign(_, _) when has_effect (effect_of full_exp) BE_config -> string "returnm tt" (* TODO *) | E_assign((LEXP_aux(le_act,tannot) as le), e) -> (* can only be register writes *) (match le_act (*, t, tag*) with | LEXP_vector_range (le,e2,e3) -> (match le with | LEXP_aux (LEXP_field ((LEXP_aux (_, lannot) as le),id), fannot) -> if is_bit_typ (typ_of_annot fannot) then raise (report l __POS__ "indexing a register's (single bit) bitfield not supported") else let field_ref = doc_id (typ_id_of (typ_of_annot lannot)) ^^ underscore ^^ doc_id id in liftR ((prefix 2 1) (string "write_reg_field_range") (align (doc_lexp_deref ctxt le ^/^ field_ref ^/^ expY e2 ^/^ expY e3 ^/^ expY e))) | _ -> let deref = doc_lexp_deref ctxt le in liftR ((prefix 2 1) (string "write_reg_range") (align (deref ^/^ expY e2 ^/^ expY e3) ^/^ expY e))) | LEXP_vector (le,e2) -> (match le with | LEXP_aux (LEXP_field ((LEXP_aux (_, lannot) as le),id), fannot) -> if is_bit_typ (typ_of_annot fannot) then raise (report l __POS__ "indexing a register's (single bit) bitfield not supported") else let field_ref = doc_id (typ_id_of (typ_of_annot lannot)) ^^ underscore ^^ doc_id id in let call = if is_bitvector_typ (Env.base_typ_of (env_of full_exp) (typ_of_annot fannot)) then "write_reg_field_bit" else "write_reg_field_pos" in liftR ((prefix 2 1) (string call) (align (doc_lexp_deref ctxt le ^/^ field_ref ^/^ expY e2 ^/^ expY e))) | LEXP_aux (_, lannot) -> let deref = doc_lexp_deref ctxt le in let call = if is_bitvector_typ (Env.base_typ_of (env_of full_exp) (typ_of_annot lannot)) then "write_reg_bit" else "write_reg_pos" in liftR ((prefix 2 1) (string call) (deref ^/^ expY e2 ^/^ expY e)) ) | LEXP_field ((LEXP_aux (_, lannot) as le),id) -> let field_ref = doc_id (typ_id_of (typ_of_annot lannot)) ^^ underscore ^^ doc_id id (*^^ dot ^^ string "set_field"*) in liftR ((prefix 2 1) (string "write_reg_field") (doc_lexp_deref ctxt le ^^ space ^^ field_ref ^/^ expY e)) | LEXP_deref re -> liftR ((prefix 2 1) (string "write_reg") (expY re ^/^ expY e)) | _ -> liftR ((prefix 2 1) (string "write_reg") (doc_lexp_deref ctxt le ^/^ expY e))) | E_vector_append(le,re) -> raise (Reporting.err_unreachable l __POS__ "E_vector_append should have been rewritten before pretty-printing") | E_cons(le,re) -> doc_op (group (colon^^colon)) (expY le) (expY re) | E_if(c,t,e) -> let epp = if_exp ctxt false c t e in if aexp_needed then parens (align epp) else epp | E_for(id,exp1,exp2,exp3,(Ord_aux(order,_)),exp4) -> raise (report l __POS__ "E_for should have been rewritten before pretty-printing") | E_loop _ -> raise (report l __POS__ "E_loop should have been rewritten before pretty-printing") | E_let(leb,e) -> let epp = let_exp ctxt leb ^^ space ^^ string "in" ^^ hardline ^^ expN e in if aexp_needed then parens epp else epp | E_app(f,args) -> begin match f with | Id_aux (Id "and_bool", _) | Id_aux (Id "or_bool", _) when effectful (effect_of full_exp) -> let call = doc_id (append_id f "M") in wrap_parens (hang 2 (flow (break 1) (call :: List.map expY args))) (* temporary hack to make the loop body a function of the temporary variables *) | Id_aux (Id "None", _) as none -> doc_id_ctor none | Id_aux (Id "foreach", _) -> begin match args with | [from_exp; to_exp; step_exp; ord_exp; vartuple; body] -> let loopvar, body = match body with | E_aux (E_if (_, E_aux (E_let (LB_aux (LB_val ( ((P_aux (P_typ (_, P_aux (P_var (P_aux (P_id id, _), _), _)), _)) | (P_aux (P_var (P_aux (P_id id, _), _), _)) | (P_aux (P_id id, _))), _), _), body), _), _), _) -> id, body | _ -> raise (Reporting.err_unreachable l __POS__ ("Unable to find loop variable in " ^ string_of_exp body)) in let dir = match ord_exp with | E_aux (E_lit (L_aux (L_false, _)), _) -> "_down" | E_aux (E_lit (L_aux (L_true, _)), _) -> "_up" | _ -> raise (Reporting.err_unreachable l __POS__ ("Unexpected loop direction " ^ string_of_exp ord_exp)) in let combinator = if effectful (effect_of body) then "foreach_ZM" else "foreach_Z" in let combinator = combinator ^ dir in let used_vars_body = find_e_ids body in let body_lambda = (* Work around indentation issues in Lem when translating tuple or literal unit patterns to Isabelle *) match fst (uncast_exp vartuple) with | E_aux (E_tuple _, _) when not (IdSet.mem (mk_id "varstup") used_vars_body)-> separate space [string "fun"; doc_id loopvar; string "_"; string "varstup"; bigarrow] ^^ break 1 ^^ separate space [string "let"; squote ^^ expY vartuple; string ":= varstup in"] | E_aux (E_lit (L_aux (L_unit, _)), _) when not (IdSet.mem (mk_id "unit_var") used_vars_body) -> separate space [string "fun"; doc_id loopvar; string "_"; string "unit_var"; bigarrow] | _ -> separate space [string "fun"; doc_id loopvar; string "_"; expY vartuple; bigarrow] in parens ( (prefix 2 1) ((separate space) [string combinator; expY from_exp; expY to_exp; expY step_exp; expY vartuple]) (parens (prefix 2 1 (group body_lambda) (expN body)) ) ) | _ -> raise (Reporting.err_unreachable l __POS__ "Unexpected number of arguments for loop combinator") end | Id_aux (Id (("while" | "until") as combinator), _) -> begin match args with | [cond; varstuple; body] -> let return (E_aux (e, a)) = E_aux (E_internal_return (E_aux (e, a)), a) in let csuffix, cond, body = match effectful (effect_of cond), effectful (effect_of body) with | false, false -> "", cond, body | false, true -> "M", return cond, body | true, false -> "M", cond, return body | true, true -> "M", cond, body in let used_vars_body = find_e_ids body in let lambda = (* Work around indentation issues in Lem when translating tuple or literal unit patterns to Isabelle *) match fst (uncast_exp varstuple) with | E_aux (E_tuple _, _) when not (IdSet.mem (mk_id "varstup") used_vars_body)-> separate space [string "fun varstup"; bigarrow] ^^ break 1 ^^ separate space [string "let"; squote ^^ expY varstuple; string ":= varstup in"] | E_aux (E_lit (L_aux (L_unit, _)), _) when not (IdSet.mem (mk_id "unit_var") used_vars_body) -> separate space [string "fun unit_var"; bigarrow] | _ -> separate space [string "fun"; expY varstuple; bigarrow] in parens ( (prefix 2 1) ((separate space) [string (combinator ^ csuffix); expY varstuple]) ((prefix 0 1) (parens (prefix 2 1 (group lambda) (expN cond))) (parens (prefix 2 1 (group lambda) (expN body)))) ) | _ -> raise (Reporting.err_unreachable l __POS__ "Unexpected number of arguments for loop combinator") end | Id_aux (Id "early_return", _) -> begin match args with | [exp] -> let exp_pp = match ctxt.build_at_return with | Some s -> parens (string s ^/^ expY exp) | None -> expY exp in let epp = separate space [string "early_return"; exp_pp] in let aexp_needed, tepp = if contains_t_pp_var ctxt (typ_of exp) || contains_t_pp_var ctxt (typ_of full_exp) then aexp_needed, epp else let tannot = separate space [string "MR"; doc_atomic_typ ctxt false (typ_of full_exp); doc_atomic_typ ctxt false (typ_of exp)] in true, doc_op colon epp tannot in if aexp_needed then parens tepp else tepp | _ -> raise (Reporting.err_unreachable l __POS__ "Unexpected number of arguments for early_return builtin") end | _ -> let env = env_of_annot (l,annot) in let () = debug ctxt (lazy ("Function application " ^ string_of_id f)) in let call, is_extern, is_ctor, is_rec = if Env.is_union_constructor f env then doc_id_ctor f, false, true, false else if Env.is_extern f env "coq" then string (Env.get_extern f env "coq"), true, false, false else if IdSet.mem f ctxt.recursive_ids then doc_id f, false, false, true else doc_id f, false, false, false in let (tqs,fn_ty) = Env.get_val_spec f env in (* Calculate the renaming *) let tqs_map = List.fold_left (fun m k -> let kid = kopt_kid k in KBindings.add (orig_kid kid) kid m) KBindings.empty (quant_kopts tqs) in let arg_typs, ret_typ, eff = match fn_ty with | Typ_aux (Typ_fn (arg_typs,ret_typ,eff),_) -> arg_typs, ret_typ, eff | _ -> raise (Reporting.err_unreachable l __POS__ "Function not a function type") in let inst = (* We attempt to get an instantiation of the function signature's type variables which agrees with Coq by 1. using dummy variables with the expected type of each argument (avoiding the inferred type, which might have (e.g.) stripped out an existential quantifier) 2. calculating the instantiation without using the expected return type, so that we can work out if we need a cast around the function call. *) let dummy_args = Util.list_mapi (fun i exp -> mk_id ("#coq#arg" ^ string_of_int i), general_typ_of exp) args in let dummy_exp = mk_exp (E_app (f, List.map (fun (id,_) -> mk_exp (E_id id)) dummy_args)) in let dummy_env = List.fold_left (fun env (id,typ) -> Env.add_local id (Immutable,typ) env) env dummy_args in let inst_exp = try infer_exp dummy_env dummy_exp with ex -> debug ctxt (lazy (" cannot infer dummy application " ^ Printexc.to_string ex)); full_exp in match instantiation_of_without_type inst_exp with | x -> x (* Not all function applications can be inferred, so try falling back to the type inferred when we know the target type. TODO: there are probably some edge cases where this won't pick up a need to cast. *) | exception _ -> instantiation_of full_exp in let inst = KBindings.fold (fun k u m -> KBindings.add (KBindings.find (orig_kid k) tqs_map) u m) inst KBindings.empty in let () = debug ctxt (lazy (" instantiations: " ^ String.concat ", " (List.map (fun (kid,tyarg) -> string_of_kid kid ^ " => " ^ string_of_typ_arg tyarg) (KBindings.bindings inst)))) in (* Insert existential packing of arguments where necessary *) let doc_arg want_parens arg typ_from_fn = let env = env_of arg in let typ_from_fn = subst_unifiers inst typ_from_fn in let typ_from_fn = Env.expand_synonyms env typ_from_fn in (* TODO: more sophisticated check *) let () = debug ctxt (lazy (" arg type found " ^ string_of_typ (typ_of arg))); debug ctxt (lazy (" arg type expected " ^ string_of_typ typ_from_fn)) in let typ_of_arg = Env.expand_synonyms env (typ_of arg) in let typ_of_arg = expand_range_type typ_of_arg in let typ_of_arg' = match typ_of_arg with Typ_aux (Typ_exist (_,_,t),_) -> t | t -> t in let typ_from_fn' = match typ_from_fn with Typ_aux (Typ_exist (_,_,t),_) -> t | t -> t in let autocast = (* Avoid using helper functions which simplify the nexps *) is_bitvector_typ typ_of_arg' && is_bitvector_typ typ_from_fn' && match typ_of_arg', typ_from_fn' with | Typ_aux (Typ_app (_,[A_aux (A_nexp n1,_);_;_]),_), Typ_aux (Typ_app (_,[A_aux (A_nexp n2,_);_;_]),_) -> not (similar_nexps ctxt env n1 n2) | _ -> false in (* If the argument is an integer that can be inferred from the context in a different form, let Coq fill it in. E.g., when "64" is really "8 * width". Avoid cases where the type checker has introduced a phantom type variable while calculating the instantiations. *) let vars_in_env n = let ekids = Env.get_typ_vars env in KidSet.for_all (fun kid -> KBindings.mem kid ekids) (nexp_frees n) in match typ_of_arg, typ_from_fn with | Typ_aux (Typ_app (Id_aux (Id "atom",_),[A_aux (A_nexp n1,_)]),_), Typ_aux (Typ_app (Id_aux (Id "atom",_),[A_aux (A_nexp n2,_)]),_) when vars_in_env n2 && not (similar_nexps ctxt env n1 n2) -> underscore | _ -> let want_parens1 = want_parens || autocast in let arg_pp = construct_dep_pairs env want_parens1 arg typ_from_fn in if autocast && false then let arg_pp = string "autocast" ^^ space ^^ arg_pp in if want_parens then parens arg_pp else arg_pp else arg_pp in let epp = if is_ctor then hang 2 (call ^^ break 1 ^^ parens (flow (comma ^^ break 1) (List.map2 (doc_arg false) args arg_typs))) else let main_call = call :: List.map2 (doc_arg true) args arg_typs in let all = if is_rec then main_call @ [parens (string "_limit_reduces _acc")] else match f with | Id_aux (Id x,_) when is_prefix "#rec#" x -> main_call @ [parens (string "Zwf_guarded _")] | _ -> main_call in hang 2 (flow (break 1) all) in (* Decide whether to unpack an existential result, pack one, or cast. To do this we compare the expected type stored in the checked expression with the inferred type. *) let ret_typ_inst = subst_unifiers inst ret_typ in let packeff,unpack,autocast,projbool = let ann_typ = Env.expand_synonyms env (general_typ_of_annot (l,annot)) in let ann_typ = expand_range_type ann_typ in let ret_typ_inst = expand_range_type (Env.expand_synonyms env ret_typ_inst) in let ret_typ_inst = if is_no_proof_fn env f then ret_typ_inst else snd (replace_atom_return_type ret_typ_inst) in let () = debug ctxt (lazy (" type returned " ^ string_of_typ ret_typ_inst)); debug ctxt (lazy (" type expected " ^ string_of_typ ann_typ)) in let unpack, in_typ = match ret_typ_inst with | Typ_aux (Typ_exist (_,_,t1),_) -> true,t1 | t1 -> false,t1 in let pack,out_typ = match ann_typ with | Typ_aux (Typ_exist (_,_,t1),_) -> true,t1 | t1 -> false,t1 in let autocast = (* Avoid using helper functions which simplify the nexps *) is_bitvector_typ in_typ && is_bitvector_typ out_typ && match in_typ, out_typ with | Typ_aux (Typ_app (_,[A_aux (A_nexp n1,_);_;_]),_), Typ_aux (Typ_app (_,[A_aux (A_nexp n2,_);_;_]),_) -> not (similar_nexps ctxt env n1 n2) | _ -> false in let projbool = match in_typ with | Typ_aux (Typ_app (Id_aux (Id "atom#bool",_),_),_) -> true | _ -> false in pack,unpack,autocast,projbool in let autocast_id, proj_id = if effectful eff then "autocast_m", "projT1_m" else "autocast", "projT1" in let epp = if unpack && not (effectful eff) then string proj_id ^^ space ^^ parens epp else epp in let epp = if projbool && not (effectful eff) then string "projBool" ^^ space ^^ parens epp else epp in let epp = if autocast then string autocast_id ^^ space ^^ parens epp else epp in let epp = if effectful eff && packeff && not unpack then string "build_ex_m" ^^ space ^^ parens epp else epp in liftR (if aexp_needed then parens (align epp) else epp) end | E_vector_access (v,e) -> raise (Reporting.err_unreachable l __POS__ "E_vector_access should have been rewritten before pretty-printing") | E_vector_subrange (v,e1,e2) -> raise (Reporting.err_unreachable l __POS__ "E_vector_subrange should have been rewritten before pretty-printing") | E_field((E_aux(_,(l,fannot)) as fexp),id) -> (match destruct_tannot fannot with | Some(env, (Typ_aux (Typ_id tid, _)), _) | Some(env, (Typ_aux (Typ_app (tid, _), _)), _) when Env.is_record tid env -> let fname = if prefix_recordtype && string_of_id tid <> "regstate" then (string (string_of_id tid ^ "_")) ^^ doc_id id else doc_id id in expY fexp ^^ dot ^^ parens fname | _ -> raise (report l __POS__ "E_field expression with no register or record type")) | E_block [] -> string "tt" | E_block exps -> raise (report l __POS__ "Blocks should have been removed till now.") | E_nondet exps -> raise (report l __POS__ "Nondet blocks not supported.") | E_id id | E_ref id -> let env = env_of full_exp in let typ = typ_of full_exp in let eff = effect_of full_exp in let base_typ = Env.base_typ_of env typ in if has_effect eff BE_rreg then let epp = separate space [string "read_reg";doc_id (append_id id "_ref")] in if is_bitvector_typ base_typ then wrap_parens (align (group (prefix 0 1 (parens (liftR epp)) (doc_tannot ctxt env true base_typ)))) else liftR epp else if Env.is_register id env && is_regtyp typ env then doc_id (append_id id "_ref") else if is_ctor env id then doc_id_ctor id else begin match Env.lookup_id id env with | Local (_,typ) -> let exp_typ = expand_range_type (Env.expand_synonyms env typ) in let ann_typ = general_typ_of full_exp in let ann_typ = expand_range_type (Env.expand_synonyms env ann_typ) in let () = debug ctxt (lazy ("Variable " ^ string_of_id id ^ " with type " ^ string_of_typ typ)); debug ctxt (lazy (" expected type " ^ string_of_typ ann_typ)) in doc_id id | _ -> doc_id id end | E_lit lit -> doc_lit lit | E_cast(typ,e) -> let epp = expV true e in let env = env_of_annot (l,annot) in let outer_typ = Env.expand_synonyms env (general_typ_of_annot (l,annot)) in let outer_typ = expand_range_type outer_typ in let cast_typ = expand_range_type (Env.expand_synonyms env typ) in let inner_typ = Env.expand_synonyms env (general_typ_of e) in let inner_typ = expand_range_type inner_typ in let () = debug ctxt (lazy ("Cast of type " ^ string_of_typ cast_typ)); debug ctxt (lazy (" on expr of type " ^ string_of_typ inner_typ)); debug ctxt (lazy (" where type expected is " ^ string_of_typ outer_typ)) in let outer_ex,outer_typ' = match outer_typ with | Typ_aux (Typ_exist (_,_,t1),_) -> true,t1 | t1 -> false,t1 in let cast_ex,cast_typ' = match cast_typ with | Typ_aux (Typ_exist (_,_,t1),_) -> true,t1 | t1 -> false,t1 in let inner_ex,inner_typ' = match inner_typ with | Typ_aux (Typ_exist (_,_,t1),_) -> true,t1 | t1 -> false,t1 in let autocast = (* Avoid using helper functions which simplify the nexps *) is_bitvector_typ outer_typ' && is_bitvector_typ cast_typ' && match outer_typ', cast_typ' with | Typ_aux (Typ_app (_,[A_aux (A_nexp n1,_);_;_]),_), Typ_aux (Typ_app (_,[A_aux (A_nexp n2,_);_;_]),_) -> not (similar_nexps ctxt env n1 n2) | _ -> false in let effects = effectful (effect_of e) in let epp = if effects then if inner_ex then if cast_ex (* If the types are the same use the cast as a hint to Coq, otherwise derive the new type from the old one. *) then if alpha_equivalent env inner_typ cast_typ then epp else string "derive_m" ^^ space ^^ epp else string "projT1_m" ^^ space ^^ epp else if cast_ex then string "build_ex_m" ^^ space ^^ epp else epp else if cast_ex then string "build_ex" ^^ space ^^ epp else epp in let epp = epp ^/^ doc_tannot ctxt (env_of e) effects typ in let epp = if effects then if cast_ex && not outer_ex then string "projT1_m" ^^ space ^^ parens epp else epp else if cast_ex then string "projT1" ^^ space ^^ parens epp else epp in let epp = if autocast then string (if effects then "autocast_m" else "autocast") ^^ space ^^ parens epp else epp in if aexp_needed then parens epp else epp | E_tuple exps -> construct_dep_pairs (env_of_annot (l,annot)) true full_exp (general_typ_of full_exp) | E_record fexps -> let recordtyp = match destruct_tannot annot with | Some (env, Typ_aux (Typ_id tid,_), _) | Some (env, Typ_aux (Typ_app (tid, _), _), _) -> (* when Env.is_record tid env -> *) tid | _ -> raise (report l __POS__ ("cannot get record type from annot " ^ string_of_tannot annot ^ " of exp " ^ string_of_exp full_exp)) in let epp = enclose_record (align (separate_map (semi_sp ^^ break 1) (doc_fexp ctxt recordtyp) fexps)) in if aexp_needed then parens epp else epp | E_record_update(e, fexps) -> let recordtyp, env = match destruct_tannot annot with | Some (env, Typ_aux (Typ_id tid,_), _) | Some (env, Typ_aux (Typ_app (tid, _), _), _) when Env.is_record tid env -> tid, env | _ -> raise (report l __POS__ ("cannot get record type from annot " ^ string_of_tannot annot ^ " of exp " ^ string_of_exp full_exp)) in if List.length fexps > 1 then let _,fields = Env.get_record recordtyp env in let var, let_pp = match e with | E_aux (E_id id,_) -> id, empty | _ -> let v = mk_id "_record" in (* TODO: collision avoid *) v, separate space [string "let "; doc_id v; coloneq; top_exp ctxt true e; string "in"] ^^ break 1 in let doc_field (_,id) = match List.find (fun (FE_aux (FE_Fexp (id',_),_)) -> Id.compare id id' == 0) fexps with | fexp -> doc_fexp ctxt recordtyp fexp | exception Not_found -> let fname = if prefix_recordtype && string_of_id recordtyp <> "regstate" then (string (string_of_id recordtyp ^ "_")) ^^ doc_id id else doc_id id in doc_op coloneq fname (doc_id var ^^ dot ^^ parens fname) in let_pp ^^ enclose_record (align (separate_map (semi_sp ^^ break 1) doc_field fields)) else enclose_record_update (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp ctxt recordtyp) fexps)) | E_vector exps -> let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in let start, (len, order, etyp) = if is_vector_typ t then vector_start_index t, vector_typ_args_of t else raise (Reporting.err_unreachable l __POS__ "E_vector of non-vector type") in let dir,dir_out = if is_order_inc order then (true,"true") else (false, "false") 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 = brackets expspp in let (epp,aexp_needed) = if is_bit_typ etyp then let bepp = string "vec_of_bits" ^^ space ^^ align epp in (align (group (prefix 0 1 bepp (doc_tannot ctxt (env_of full_exp) false t))), true) else let vepp = string "vec_of_list_len" ^^ space ^^ align epp in (vepp,aexp_needed) in if aexp_needed then parens (align epp) else epp | E_vector_update(v,e1,e2) -> raise (Reporting.err_unreachable l __POS__ "E_vector_update should have been rewritten before pretty-printing") | E_vector_update_subrange(v,e1,e2,e3) -> raise (Reporting.err_unreachable l __POS__ "E_vector_update should have been rewritten before pretty-printing") | E_list exps -> brackets (separate_map semi (expN) exps) | E_case(e,pexps) -> let only_integers e = expY e in let epp = group ((separate space [string "match"; only_integers e; string "with"]) ^/^ (separate_map (break 1) (doc_case ctxt (typ_of e)) pexps) ^/^ (string "end")) in if aexp_needed then parens (align epp) else align epp | E_try (e, pexps) -> if effectful (effect_of e) then let try_catch = if ctxt.early_ret then "try_catchR" else "try_catch" in let epp = (* TODO capture avoidance for __catch_val *) group ((separate space [string try_catch; expY e; string "(fun __catch_val => match __catch_val with "]) ^/^ (separate_map (break 1) (doc_case ctxt exc_typ) pexps) ^/^ (string "end)")) in if aexp_needed then parens (align epp) else align epp else raise (Reporting.err_todo l "Warning: try-block around pure expression") | E_throw e -> let epp = liftR (separate space [string "throw"; expY e]) in if aexp_needed then parens (align epp) else align epp | E_exit e -> liftR (separate space [string "exit"; expY e]) | E_assert (e1,e2) -> let epp = liftR (separate space [string "assert_exp"; expY e1; expY e2]) in if aexp_needed then parens (align epp) else align epp | E_app_infix (e1,id,e2) -> raise (Reporting.err_unreachable l __POS__ "E_app_infix should have been rewritten before pretty-printing") | E_var(lexp, eq_exp, in_exp) -> raise (report l __POS__ "E_vars should have been removed before pretty-printing") | E_internal_plet (pat,e1,e2) -> begin let () = debug ctxt (lazy ("Internal plet, pattern " ^ string_of_pat pat)); debug ctxt (lazy (" type of e1 " ^ string_of_typ (typ_of e1))) in match pat, e1, e2 with | (P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _)), (E_aux (E_assert (assert_e1,assert_e2),_)), _ -> let epp = liftR (separate space [string "assert_exp'"; expY assert_e1; expY assert_e2]) in let epp = infix 0 1 (string ">>= fun _ =>") epp (expN e2) in if aexp_needed then parens (align epp) else align epp (* Special case because we don't handle variables with nested existentials well yet. TODO: check that id1 is not used in e2' *) | ((P_aux (P_id id1,_)) | P_aux (P_typ (_, P_aux (P_id id1,_)),_)), _, (E_aux (E_let (LB_aux (LB_val (pat', E_aux (E_cast (typ', E_aux (E_id id2,_)),_)),_), e2'),_)) when Id.compare id1 id2 == 0 -> let m_str, tail_pp = if ctxt.early_ret then "MR",[string "_"] else "M",[] in let e1_pp = parens (separate space ([expY e1; colon; string m_str; parens (doc_typ ctxt typ')]@tail_pp)) in let middle = match pat' with | P_aux (P_id id,_) when Util.is_none (is_auto_decomposed_exist (env_of e1) (typ_of e1)) && not (is_enum (env_of e1) id) -> separate space [string ">>= fun"; doc_id id; bigarrow] | P_aux (P_typ (typ, P_aux (P_id id,_)),_) when Util.is_none (is_auto_decomposed_exist (env_of e1) typ) && not (is_enum (env_of e1) id) -> separate space [string ">>= fun"; doc_id id; colon; doc_typ ctxt typ; bigarrow] | _ -> separate space [string ">>= fun"; squote ^^ doc_pat ctxt true true (pat', typ'); bigarrow] in infix 0 1 middle e1_pp (expN e2') | _ -> let epp = let middle = match pat with | P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _) -> string ">>" | P_aux (P_id id,_) when Util.is_none (is_auto_decomposed_exist (env_of e1) (typ_of e1)) && not (is_enum (env_of e1) id) -> separate space [string ">>= fun"; doc_id id; bigarrow] | P_aux (P_typ (typ, P_aux (P_id id,_)),_) when Util.is_none (is_auto_decomposed_exist (env_of e1) typ) && not (is_enum (env_of e1) id) -> separate space [string ">>= fun"; doc_id id; colon; doc_typ ctxt typ; bigarrow] | P_aux (P_typ (typ, P_aux (P_id id,_)),_) | P_aux (P_typ (typ, P_aux (P_var (P_aux (P_id id,_),_),_)),_) | P_aux (P_var (P_aux (P_typ (typ, P_aux (P_id id,_)),_),_),_) when not (is_enum (env_of e1) id) -> let full_typ = (expand_range_type typ) in let binder = match destruct_exist_plain (Env.expand_synonyms (env_of e1) full_typ) with | Some _ -> squote ^^ parens (separate space [string "existT"; underscore; doc_id id; underscore; colon; doc_typ ctxt typ]) | _ -> parens (separate space [doc_id id; colon; doc_typ ctxt typ]) in separate space [string ">>= fun"; binder; bigarrow] | _ -> separate space [string ">>= fun"; squote ^^ doc_pat ctxt true true (pat, typ_of e1); bigarrow] in infix 0 1 middle (expY e1) (expN e2) in if aexp_needed then parens (align epp) else epp end | E_internal_return (e1) -> let exp_typ = typ_of e1 in let ret_typ = general_typ_of full_exp in let () = debug ctxt (lazy ("Monad return of " ^ string_of_exp e1)); debug ctxt (lazy (" with type " ^ string_of_typ exp_typ)); debug ctxt (lazy (" at type " ^ string_of_typ ret_typ)) in let valpp = let env = env_of e1 in construct_dep_pairs env true e1 ret_typ in wrap_parens (align (separate space [string "returnm"; valpp])) | E_sizeof nexp -> (match nexp_simp nexp with | Nexp_aux (Nexp_constant i, _) -> doc_lit (L_aux (L_num i, l)) | _ -> raise (Reporting.err_unreachable l __POS__ "pretty-printing non-constant sizeof expressions to Lem not supported")) | E_return r -> let ret_monad = " : MR" in let exp_pp = match ctxt.build_at_return with | Some s -> parens (string s ^/^ expY r) | None -> expY r in let ta = if contains_t_pp_var ctxt (typ_of full_exp) || contains_t_pp_var ctxt (typ_of r) then empty else separate space [string ret_monad; parens (doc_typ ctxt (typ_of full_exp)); parens (doc_typ ctxt (typ_of r))] in align (parens (string "early_return" ^//^ exp_pp ^//^ ta)) | E_constraint nc -> wrap_parens (doc_nc_exp ctxt (env_of full_exp) nc) | E_internal_value _ -> raise (Reporting.err_unreachable l __POS__ "unsupported internal expression encountered while pretty-printing") and if_exp ctxt (elseif : bool) c t e = let if_pp = string (if elseif then "else if" else "if") in let else_pp = match e with | E_aux (E_if (c', t', e'), _) | E_aux (E_cast (_, E_aux (E_if (c', t', e'), _)), _) -> if_exp ctxt true c' t' e' | _ -> prefix 2 1 (string "else") (top_exp ctxt false e) in (prefix 2 1 (soft_surround 2 1 if_pp ((if condition_produces_constraint c then string "sumbool_of_bool" ^^ space else empty) ^^ parens (top_exp ctxt true c)) (string "then")) (top_exp ctxt false t)) ^^ break 1 ^^ else_pp and let_exp ctxt (LB_aux(lb,_)) = match lb with (* Prefer simple lets over patterns, because I've found Coq can struggle to work out return types otherwise *) | LB_val(P_aux (P_id id,_),e) when Util.is_none (is_auto_decomposed_exist (env_of e) (typ_of e)) && not (is_enum (env_of e) id) -> prefix 2 1 (separate space [string "let"; doc_id id; coloneq]) (top_exp ctxt false e) | LB_val(P_aux (P_typ (typ,P_aux (P_id id,_)),_),e) when Util.is_none (is_auto_decomposed_exist (env_of e) typ) && not (is_enum (env_of e) id) -> prefix 2 1 (separate space [string "let"; doc_id id; colon; doc_typ ctxt typ; coloneq]) (top_exp ctxt false e) | LB_val(P_aux (P_typ (typ,pat),_),(E_aux (_,e_ann) as e)) -> prefix 2 1 (separate space [string "let"; squote ^^ doc_pat ctxt true false (pat, typ); coloneq]) (top_exp ctxt false (E_aux (E_cast (typ,e),e_ann))) | LB_val(pat,e) -> prefix 2 1 (separate space [string "let"; squote ^^ doc_pat ctxt true false (pat, typ_of e); coloneq]) (top_exp ctxt false e) and doc_fexp ctxt recordtyp (FE_aux(FE_Fexp(id,e),_)) = let fname = if prefix_recordtype && string_of_id recordtyp <> "regstate" then (string (string_of_id recordtyp ^ "_")) ^^ doc_id id else doc_id id in group (doc_op coloneq fname (top_exp ctxt true e)) and doc_case ctxt typ = function | Pat_aux(Pat_exp(pat,e),_) -> group (prefix 3 1 (separate space [pipe; doc_pat ctxt false false (pat,typ);bigarrow]) (group (top_exp ctxt false e))) | Pat_aux(Pat_when(_,_,_),(l,_)) -> raise (Reporting.err_unreachable l __POS__ "guarded pattern expression should have been rewritten before pretty-printing") and doc_lexp_deref ctxt ((LEXP_aux(lexp,(l,annot)))) = match lexp with | LEXP_field (le,id) -> parens (separate empty [doc_lexp_deref ctxt le;dot;doc_id id]) | LEXP_id id -> doc_id (append_id id "_ref") | LEXP_cast (typ,id) -> doc_id (append_id id "_ref") | LEXP_tup lexps -> parens (separate_map comma_sp (doc_lexp_deref ctxt) lexps) | _ -> raise (Reporting.err_unreachable l __POS__ ("doc_lexp_deref: Unsupported lexp")) (* expose doc_exp and doc_let *) in top_exp, let_exp (* FIXME: A temporary definition of List.init until 4.06 is more standard *) let list_init n f = Array.to_list (Array.init n f) let types_used_with_generic_eq defs = let rec add_typ idset (Typ_aux (typ,_)) = match typ with | Typ_id id -> IdSet.add id idset | Typ_app (id,args) -> List.fold_left add_typ_arg (IdSet.add id idset) args | Typ_tup ts -> List.fold_left add_typ idset ts | _ -> idset and add_typ_arg idset (A_aux (ta,_)) = match ta with | A_typ typ -> add_typ idset typ | _ -> idset in let alg = { (Rewriter.compute_exp_alg IdSet.empty IdSet.union) with Rewriter.e_aux = fun ((typs,exp),annot) -> let typs' = match exp with | E_app (f,[arg1;_]) -> if Env.is_extern f (env_of_annot annot) "coq" then let f' = Env.get_extern f (env_of_annot annot) "coq" in if f' = "generic_eq" || f' = "generic_neq" then add_typ typs (Env.expand_synonyms (env_of arg1) (typ_of arg1)) else typs else typs | _ -> typs in typs', E_aux (exp,annot) } in let typs_req_funcl (FCL_aux (FCL_Funcl (_,pexp), _)) = fst (Rewriter.fold_pexp alg pexp) in let typs_req_fundef (FD_aux (FD_function (_,_,_,fcls),_)) = List.fold_left IdSet.union IdSet.empty (List.map typs_req_funcl fcls) in let rec typs_req_def = function | DEF_type _ | DEF_spec _ | DEF_fixity _ | DEF_overload _ | DEF_default _ | DEF_pragma _ | DEF_reg_dec _ -> IdSet.empty | DEF_fundef fd -> typs_req_fundef fd | DEF_mapdef (MD_aux (_,(l,_))) | DEF_scattered (SD_aux (_,(l,_))) | DEF_measure (Id_aux (_,l),_,_) -> unreachable l __POS__ "Internal definition found in the Coq back-end" | DEF_internal_mutrec fds -> List.fold_left IdSet.union IdSet.empty (List.map typs_req_fundef fds) | DEF_val lb -> fst (Rewriter.fold_letbind alg lb) in List.fold_left IdSet.union IdSet.empty (List.map typs_req_def defs) let doc_type_union ctxt typ_name (Tu_aux(Tu_ty_id(typ,id),_)) = separate space [doc_id_ctor id; colon; doc_typ ctxt typ; arrow; typ_name] (* let rec doc_range ctxt (BF_aux(r,_)) = match r with | BF_single i -> parens (doc_op comma (doc_nexp ctxt i) (doc_nexp ctxt i)) | BF_range(i1,i2) -> parens (doc_op comma (doc_nexp ctxt i1) (doc_nexp ctxt i2)) | BF_concat(ir1,ir2) -> (doc_range ctxt ir1) ^^ comma ^^ (doc_range ctxt ir2) *) let doc_typdef generic_eq_types (TD_aux(td, (l, annot))) = match td with | TD_abbrev(id,typq,A_aux (A_typ typ, _)) -> let typschm = TypSchm_aux (TypSchm_ts (typq, typ), l) in doc_op coloneq (separate space [string "Definition"; doc_id_type id; doc_typquant_items empty_ctxt parens typq; colon; string "Type"]) (doc_typschm empty_ctxt false typschm) ^^ dot | TD_abbrev _ -> empty (* TODO? *) | TD_bitfield _ -> empty (* TODO? *) | TD_record(id,typq,fs,_) -> let fname fid = if prefix_recordtype && string_of_id id <> "regstate" then concat [doc_id id;string "_";doc_id_type fid;] else doc_id_type fid in let f_pp (typ,fid) = concat [fname fid;space;colon;space;doc_typ empty_ctxt typ; semi] in let rectyp = match typq with | TypQ_aux (TypQ_tq qs, _) -> let quant_item = function | QI_aux (QI_id (KOpt_aux (KOpt_kind (_, kid), _)), l) -> [A_aux (A_nexp (Nexp_aux (Nexp_var kid, l)), l)] | _ -> [] in let targs = List.concat (List.map quant_item qs) in mk_typ (Typ_app (id, targs)) | TypQ_aux (TypQ_no_forall, _) -> mk_id_typ id in let fs_doc = group (separate_map (break 1) f_pp fs) in let doc_update_field (_,fid) = let idpp = fname fid in let otherfield (_,fid') = if Id.compare fid fid' == 0 then empty else let idpp = fname fid' in separate space [semi; idpp; string ":="; idpp; string "r"] in string "Notation \"{[ r 'with' '" ^^ idpp ^^ string "' := e ]}\" := ({| " ^^ idpp ^^ string " := e" ^^ concat (List.map otherfield fs) ^^ space ^^ string "|})." in let updates_pp = separate hardline (List.map doc_update_field fs) in let id_pp = doc_id_type id in let numfields = List.length fs in let intros_pp s = string " intros [" ^^ separate space (list_init numfields (fun n -> string (s ^ string_of_int n))) ^^ string "]." ^^ hardline in let eq_pp = if IdSet.mem id generic_eq_types then string "Instance Decidable_eq_" ^^ id_pp ^^ space ^^ colon ^/^ string "forall (x y : " ^^ id_pp ^^ string "), Decidable (x = y)." ^^ hardline ^^ intros_pp "x" ^^ intros_pp "y" ^^ separate hardline (list_init numfields (fun n -> let ns = string_of_int n in string ("cmp_record_field x" ^ ns ^ " y" ^ ns ^ "."))) ^^ hardline ^^ string "refine (Build_Decidable _ true _). subst. split; reflexivity." ^^ hardline ^^ string "Defined." ^^ hardline else empty in doc_op coloneq (separate space [string "Record"; id_pp; doc_typquant_items empty_ctxt parens typq]) ((*doc_typquant typq*) (braces (space ^^ align fs_doc ^^ space))) ^^ dot ^^ hardline ^^ eq_pp ^^ updates_pp | TD_variant(id,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 *) | Id_aux ((Id "option"),_) -> empty | _ -> let id_pp = doc_id_type id in let typ_nm = separate space [id_pp; doc_typquant_items empty_ctxt braces typq] in let ar_doc = group (separate_map (break 1 ^^ pipe ^^ space) (doc_type_union empty_ctxt id_pp) ar) in let typ_pp = (doc_op coloneq) (concat [string "Inductive"; space; typ_nm]) ((*doc_typquant typq*) ar_doc) in (* We declared the type parameters as implicit so that they're implicit in the constructors. Currently Coq also makes them implicit in the type, so undo that here. *) let resetimplicit = separate space [string "Arguments"; id_pp; colon; string "clear implicits."] in typ_pp ^^ dot ^^ hardline ^^ resetimplicit ^^ hardline ^^ hardline) | TD_enum(id,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 enums_doc = group (separate_map (break 1 ^^ pipe ^^ space) doc_id_ctor enums) in let id_pp = doc_id_type id in let typ_pp = (doc_op coloneq) (concat [string "Inductive"; space; id_pp]) (enums_doc) in let eq1_pp = string "Scheme Equality for" ^^ space ^^ id_pp ^^ dot in let eq2_pp = string "Instance Decidable_eq_" ^^ id_pp ^^ space ^^ colon ^/^ string "forall (x y : " ^^ id_pp ^^ string "), Decidable (x = y) :=" ^/^ string "Decidable_eq_from_dec " ^^ id_pp ^^ string "_eq_dec." in typ_pp ^^ dot ^^ hardline ^^ eq1_pp ^^ hardline ^^ eq2_pp ^^ hardline) let args_of_typ l env typs = let arg i typ = let id = mk_id ("arg" ^ string_of_int i) in (P_aux (P_id id, (l, mk_tannot env typ no_effect)), typ), E_aux (E_id id, (l, mk_tannot env typ no_effect)) in List.split (List.mapi arg typs) (* Sail currently has a single pattern to match against a list of argument types. We need to tweak everything to match up, especially so that the function is presented in curried form. In particular, if there's a single binder for multiple arguments (which rewriting can currently introduce) then we need to turn it into multiple binders and reconstruct it in the function body. *) let rec untuple_args_pat typs (P_aux (paux, ((l, _) as annot)) as pat) = let env = env_of_annot annot in let identity = (fun body -> body) in match paux, typs with | P_tup [], _ -> let annot = (l, mk_tannot Env.empty unit_typ no_effect) in [P_aux (P_lit (mk_lit L_unit), annot), unit_typ], identity | P_tup pats, _ -> List.combine pats typs, identity | P_wild, _ -> let wild typ = P_aux (P_wild, (l, mk_tannot env typ no_effect)), typ in List.map wild typs, identity | P_typ (_, pat), _ -> untuple_args_pat typs pat | P_as _, _::_::_ | P_id _, _::_::_ -> let argpats, argexps = args_of_typ l env typs in let argexp = E_aux (E_tuple argexps, annot) in let bindargs (E_aux (_, bannot) as body) = E_aux (E_let (LB_aux (LB_val (pat, argexp), annot), body), bannot) in argpats, bindargs | _, [typ] -> [pat,typ], identity | _, _ -> unreachable l __POS__ "Unexpected pattern/type combination" let doc_fun_body ctxt exp = let doc_exp = doc_exp ctxt false exp in if ctxt.early_ret then align (string "catch_early_return" ^//^ parens (doc_exp)) else doc_exp (* Coq doesn't support "as" patterns well in Definition binders, so we push them over to the r.h.s. of the := *) let demote_as_pattern i (P_aux (_,p_annot) as pat,typ) = let open Rewriter in if fst (fold_pat ({ (compute_pat_alg false (||)) with p_as = (fun ((_,p),id) -> true, P_as (p,id)) }) pat) then let id = mk_id ("arg" ^ string_of_int i) in (* TODO: name conflicts *) (P_aux (P_id id, p_annot),typ), fun (E_aux (_,e_ann) as e) -> E_aux (E_let (LB_aux (LB_val (pat, E_aux (E_id id, p_annot)),p_annot),e),e_ann) else (pat,typ), fun e -> e let pat_is_plain_binder env (P_aux (p,_)) = match p with | P_id id | P_typ (_,P_aux (P_id id,_)) when not (is_enum env id) -> Some id | _ -> None let demote_all_patterns env i (P_aux (p,p_annot) as pat,typ) = match pat_is_plain_binder env pat with | Some id -> if Util.is_none (is_auto_decomposed_exist env typ) then (pat,typ), fun e -> e else (P_aux (P_id id, p_annot),typ), fun (E_aux (_,e_ann) as e) -> E_aux (E_let (LB_aux (LB_val (pat, E_aux (E_id id, p_annot)),p_annot),e),e_ann) | None -> let id = mk_id ("arg" ^ string_of_int i) in (* TODO: name conflicts *) (P_aux (P_id id, p_annot),typ), fun (E_aux (_,e_ann) as e) -> E_aux (E_let (LB_aux (LB_val (pat, E_aux (E_id id, p_annot)),p_annot),e),e_ann) (* Add equality constraints between arguments and nexps, except in the case that they've been merged. *) let rec atom_constraint ctxt (pat, typ) = let typ = Env.base_typ_of (env_of_pat pat) typ in match pat, typ with | P_aux (P_id id, _), Typ_aux (Typ_app (Id_aux (Id "atom",_), [A_aux (A_nexp nexp,_)]),_) -> (match nexp with (* When the kid is mapped to the id, we don't need a constraint *) | Nexp_aux (Nexp_var kid,_) when (try Id.compare (KBindings.find kid ctxt.kid_id_renames) id == 0 with _ -> false) -> None | _ -> Some (bquote ^^ braces (string "ArithFact" ^^ space ^^ parens (doc_op equals (doc_id id) (doc_nexp ctxt nexp))))) | P_aux (P_typ (_,p),_), _ -> atom_constraint ctxt (p, typ) | _ -> None let all_ids pexp = let open Rewriter in fold_pexp ( { (pure_exp_alg IdSet.empty IdSet.union) with e_id = (fun id -> IdSet.singleton id); e_ref = (fun id -> IdSet.singleton id); e_app = (fun (id,ids) -> List.fold_left IdSet.union (IdSet.singleton id) ids); e_app_infix = (fun (ids1,id,ids2) -> IdSet.add id (IdSet.union ids1 ids2)); e_for = (fun (id,ids1,ids2,ids3,_,ids4) -> IdSet.add id (IdSet.union ids1 (IdSet.union ids2 (IdSet.union ids3 ids4)))); lEXP_id = IdSet.singleton; lEXP_memory = (fun (id,ids) -> List.fold_left IdSet.union (IdSet.singleton id) ids); lEXP_cast = (fun (_,id) -> IdSet.singleton id); pat_alg = { (pure_pat_alg IdSet.empty IdSet.union) with p_as = (fun (ids,id) -> IdSet.add id ids); p_id = IdSet.singleton; p_app = (fun (id,ids) -> List.fold_left IdSet.union (IdSet.singleton id) ids); } }) pexp let tyvars_of_typquant (TypQ_aux (tq,_)) = match tq with | TypQ_no_forall -> KidSet.empty | TypQ_tq qs -> List.fold_left KidSet.union KidSet.empty (List.map tyvars_of_quant_item qs) let mk_kid_renames ids_to_avoid kids = let map_id = function | Id_aux (Id i, _) -> Some (fix_id false i) | Id_aux (DeIid _, _) -> None in let ids = StringSet.of_list (Util.map_filter map_id (IdSet.elements ids_to_avoid)) in let rec check_kid kid (newkids,rebindings) = let rec check kid1 = let kid_string = fix_id true (string_of_kid kid1) in if StringSet.mem kid_string ids then let kid2 = match kid1 with Kid_aux (Var x,l) -> Kid_aux (Var (x ^ "0"),l) in check kid2 else KidSet.add kid1 newkids, KBindings.add kid kid1 rebindings in check kid in snd (KidSet.fold check_kid kids (kids, KBindings.empty)) let merge_kids_atoms pats = let try_eliminate (gone,map,seen) = function | P_aux (P_id id, ann), typ | P_aux (P_typ (_,P_aux (P_id id, ann)),_), typ -> begin let merge kid l = if KidSet.mem kid seen then let () = Reporting.print_err l "merge_kids_atoms" ("want to merge tyvar and argument for " ^ string_of_kid kid ^ " but rearranging arguments isn't supported yet") in gone,map,seen else KidSet.add kid gone, KBindings.add kid id map, KidSet.add kid seen in match Type_check.destruct_atom_nexp (env_of_annot ann) typ with | Some (Nexp_aux (Nexp_var kid,l)) -> merge kid l | _ -> match Type_check.destruct_atom_bool (env_of_annot ann) typ with | Some (NC_aux (NC_var kid,l)) -> merge kid l | _ -> gone,map,KidSet.union seen (tyvars_of_typ typ) end | _, typ -> gone,map,KidSet.union seen (tyvars_of_typ typ) in let gone,map,_ = List.fold_left try_eliminate (KidSet.empty, KBindings.empty, KidSet.empty) pats in gone,map let merge_var_patterns map pats = let map,pats = List.fold_left (fun (map,pats) (pat, typ) -> match pat with | P_aux (P_var (P_aux (P_id id,_), TP_aux (TP_var kid,_)),ann) -> KBindings.add kid id map, (P_aux (P_id id,ann), typ) :: pats | _ -> map, (pat,typ)::pats) (map,[]) pats in map, List.rev pats type mutrec_pos = NotMutrec | FirstFn | LaterFn let doc_funcl mutrec rec_opt (FCL_aux(FCL_Funcl(id, pexp), annot)) = let env = env_of_annot annot in let (tq,typ) = Env.get_val_spec_orig id env in let (arg_typs, ret_typ, eff) = match typ with | Typ_aux (Typ_fn (arg_typs, ret_typ, eff),_) -> arg_typs, ret_typ, eff | _ -> failwith ("Function " ^ string_of_id id ^ " does not have function type") in let build_ex, ret_typ = replace_atom_return_type ret_typ in let build_ex = match destruct_exist_plain (Env.expand_synonyms env (expand_range_type ret_typ)) with | Some _ -> Some "build_ex" | _ -> build_ex in let ids_to_avoid = all_ids pexp in let bound_kids = tyvars_of_typquant tq in let pat,guard,exp,(l,_) = destruct_pexp pexp in let pats, bind = untuple_args_pat arg_typs pat in (* Fixpoint definitions can only use simple binders, but even Definitions can't handle as patterns *) let pattern_elim = match rec_opt with | Rec_aux (Rec_nonrec,_) -> demote_as_pattern | _ -> demote_all_patterns env in let pats, binds = List.split (Util.list_mapi pattern_elim pats) in let eliminated_kids, kid_to_arg_rename = merge_kids_atoms pats in let kid_to_arg_rename, pats = merge_var_patterns kid_to_arg_rename pats in let kids_used = KidSet.diff bound_kids eliminated_kids in let is_measured, recursive_ids = match rec_opt with (* No mutual recursion in this backend yet; only change recursive definitions where we have a measure *) | Rec_aux (Rec_measure _,_) -> true, IdSet.singleton id | _ -> false, IdSet.empty in let ctxt = { early_ret = contains_early_return exp; kid_renames = mk_kid_renames ids_to_avoid kids_used; kid_id_renames = kid_to_arg_rename; bound_nvars = bound_kids; build_at_return = if effectful eff then build_ex else None; recursive_ids = recursive_ids; debug = List.mem (string_of_id id) (!opt_debug_on) } in let () = debug ctxt (lazy ("Function " ^ string_of_id id)); debug ctxt (lazy (" return type " ^ string_of_typ ret_typ)); debug ctxt (lazy (" build_ex " ^ match build_ex with Some s -> s ^ " needed" | _ -> "not needed")); debug ctxt (lazy (if effectful eff then " effectful" else " pure")); debug ctxt (lazy (" kid_id_renames " ^ String.concat ", " (List.map (fun (kid,id) -> string_of_kid kid ^ " |-> " ^ string_of_id id) (KBindings.bindings kid_to_arg_rename)))) in (* Put the constraints after pattern matching so that any type variable that's been replaced by one of the term-level arguments is bound. *) let quantspp, constrspp = doc_typquant_items_separate ctxt braces tq in let exp = List.fold_left (fun body f -> f body) (bind exp) binds in let used_a_pattern = ref false in let doc_binder (P_aux (p,ann) as pat, typ) = let env = env_of_annot ann in let exp_typ = Env.expand_synonyms env typ in let () = debug ctxt (lazy (" pattern " ^ string_of_pat pat)); debug ctxt (lazy (" with expanded type " ^ string_of_typ exp_typ)) in match pat_is_plain_binder env pat with | Some id -> if Util.is_none (is_auto_decomposed_exist env exp_typ) then parens (separate space [doc_id id; colon; doc_typ ctxt typ]) else begin let full_typ = (expand_range_type exp_typ) in match destruct_exist_plain (Env.expand_synonyms env full_typ) with | Some ([kopt], NC_aux (NC_true,_), Typ_aux (Typ_app (Id_aux (Id "atom",_), [A_aux (A_nexp (Nexp_aux (Nexp_var kid,_)),_)]),_)) when Kid.compare (kopt_kid kopt) kid == 0 -> parens (separate space [doc_id id; colon; string "Z"]) | Some ([kopt], nc, Typ_aux (Typ_app (Id_aux (Id "atom",_), [A_aux (A_nexp (Nexp_aux (Nexp_var kid,_)),_)]),_)) when Kid.compare (kopt_kid kopt) kid == 0 && not is_measured -> (used_a_pattern := true; squote ^^ parens (separate space [string "existT"; underscore; doc_id id; underscore; colon; doc_typ ctxt typ])) | _ -> parens (separate space [doc_id id; colon; doc_typ ctxt typ]) end | None -> (used_a_pattern := true; squote ^^ parens (separate space [doc_pat ctxt true true (pat, exp_typ); colon; doc_typ ctxt typ])) in let patspp = flow_map (break 1) doc_binder pats in let atom_constrs = Util.map_filter (atom_constraint ctxt) pats in let atom_constr_pp = separate space atom_constrs in let retpp = if effectful eff then string "M" ^^ space ^^ parens (doc_typ ctxt ret_typ) else doc_typ ctxt ret_typ in let idpp = doc_id id in let intropp, accpp, measurepp, fixupspp = match rec_opt with | Rec_aux (Rec_measure _,_) -> let fixupspp = Util.map_filter (fun (pat,typ) -> match pat_is_plain_binder env pat with | Some id -> begin match destruct_exist_plain (Env.expand_synonyms env (expand_range_type typ)) with | Some (_, NC_aux (NC_true,_), _) -> None | Some ([KOpt_aux (KOpt_kind (_, kid), _)], nc, Typ_aux (Typ_app (Id_aux (Id "atom",_), [A_aux (A_nexp (Nexp_aux (Nexp_var kid',_)),_)]),_)) when Kid.compare kid kid' == 0 -> Some (string "let " ^^ doc_id id ^^ string " := projT1 " ^^ doc_id id ^^ string " in") | _ -> None end | None -> None) pats in string "Fixpoint", [parens (string "_acc : Acc (Zwf 0) _reclimit")], [string "{struct _acc}"], fixupspp | Rec_aux (r,_) -> let d = match r with Rec_nonrec -> "Definition" | _ -> "Fixpoint" in string d, [], [], [] in let intropp = match mutrec with | NotMutrec -> intropp | FirstFn -> string "Fixpoint" | LaterFn -> string "with" in let terminalpp = match mutrec with NotMutrec -> dot | _ -> empty in (* Work around Coq bug 7975 about pattern binders followed by implicit arguments *) let implicitargs = if !used_a_pattern && List.length constrspp + List.length atom_constrs > 0 then break 1 ^^ separate space ([string "Arguments"; idpp;] @ List.map (fun _ -> string "{_}") quantspp @ List.map (fun _ -> string "_") pats @ List.map (fun _ -> string "{_}") constrspp @ List.map (fun _ -> string "{_}") atom_constrs) ^^ dot else empty in let _ = match guard with | None -> () | _ -> raise (Reporting.err_unreachable l __POS__ "guarded pattern expression should have been rewritten before pretty-printing") in let bodypp = doc_fun_body ctxt exp in let bodypp = if effectful eff then bodypp else match build_ex with Some s -> string s ^^ parens bodypp | None -> bodypp in let bodypp = separate (break 1) fixupspp ^/^ bodypp in group (prefix 3 1 (flow (break 1) ([intropp; idpp] @ quantspp @ [patspp] @ constrspp @ [atom_constr_pp] @ accpp) ^/^ flow (break 1) (measurepp @ [colon; retpp; coloneq])) (bodypp ^^ terminalpp)) ^^ implicitargs let get_id = function | [] -> failwith "FD_function with empty list" | (FCL_aux (FCL_Funcl (id,_),_))::_ -> id (* Coq doesn't support multiple clauses for a single function joined by "and". However, all the funcls should have been merged by the merge_funcls rewrite now. *) let doc_fundef_rhs ?(mutrec=NotMutrec) (FD_aux(FD_function(r, typa, efa, funcls),(l,_))) = match funcls with | [] -> unreachable l __POS__ "function with no clauses" | [funcl] -> doc_funcl mutrec r funcl | (FCL_aux (FCL_Funcl (id,_),_))::_ -> unreachable l __POS__ ("function " ^ string_of_id id ^ " has multiple clauses in backend") let doc_mutrec = function | [] -> failwith "DEF_internal_mutrec with empty function list" | fundef::fundefs -> doc_fundef_rhs ~mutrec:FirstFn fundef ^^ hardline ^^ separate_map hardline (doc_fundef_rhs ~mutrec:LaterFn) fundefs ^^ dot let rec doc_fundef (FD_aux(FD_function(r, typa, efa, fcls),fannot)) = match fcls with | [] -> failwith "FD_function with empty function list" | [FCL_aux (FCL_Funcl(id,_),annot) as funcl] when not (Env.is_extern id (env_of_annot annot) "coq") -> doc_funcl NotMutrec r funcl | [_] -> empty (* extern *) | _ -> failwith "FD_function with more than one clause" let doc_dec (DEC_aux (reg, ((l, _) as annot))) = match reg with | DEC_reg(_,_,typ,id) -> empty (* let env = env_of_annot annot in let rt = Env.base_typ_of env typ in if is_vector_typ rt then let start, (size, order, etyp) = vector_start_index rt, vector_typ_args_of rt in if is_bit_typ etyp && is_nexp_constant start && is_nexp_constant size then let o = if is_order_inc order then "true" else "false" in (doc_op equals) (string "let" ^^ space ^^ doc_id id) (string "Register" ^^ space ^^ align (separate space [string_lit(doc_id id); doc_nexp (size); doc_nexp (start); string o; string "[]"])) ^/^ hardline else raise (Reporting.err_unreachable l __POS__ ("can't deal with register type " ^ string_of_typ typ)) else raise (Reporting.err_unreachable l __POS__ ("can't deal with register type " ^ string_of_typ typ)) *) | DEC_config(id, typ, exp) -> separate space [string "Definition"; doc_id id; coloneq; doc_exp empty_ctxt false exp] ^^ dot ^^ hardline | DEC_alias(id,alspec) -> empty | DEC_typ_alias(typ,id,alspec) -> empty let is_field_accessor regtypes fdef = let is_field_of regtyp field = List.exists (fun (tname, (_, _, fields)) -> tname = regtyp && List.exists (fun (_, fid) -> string_of_id fid = field) fields) regtypes in match Util.split_on_char '_' (string_of_id (id_of_fundef fdef)) with | [access; regtyp; field] -> (access = "get" || access = "set") && is_field_of regtyp field | _ -> false let int_of_field_index tname fid nexp = match int_of_nexp_opt nexp with | Some i -> i | None -> raise (Reporting.err_typ Parse_ast.Unknown ("Non-constant bitfield index in field " ^ string_of_id fid ^ " of " ^ tname)) let doc_regtype_fields (tname, (n1, n2, fields)) = let const_int fid idx = int_of_field_index tname fid idx in let i1, i2 = match n1, n2 with | Nexp_aux(Nexp_constant i1,_),Nexp_aux(Nexp_constant i2,_) -> i1, i2 | _ -> raise (Reporting.err_typ Parse_ast.Unknown ("Non-constant indices in register type " ^ tname)) in let dir_b = i1 < i2 in let dir = (if dir_b then "true" else "false") in let doc_field (fr, fid) = let i, j = match fr with | BF_aux (BF_single i, _) -> let i = const_int fid i in (i, i) | BF_aux (BF_range (i, j), _) -> (const_int fid i, const_int fid j) | _ -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ ("Unsupported type in field " ^ string_of_id fid ^ " of " ^ tname)) in let fsize = Big_int.succ (Big_int.abs (Big_int.sub i j)) in (* TODO Assumes normalised, decreasing bitvector slices; however, since start indices or indexing order do not appear in Lem type annotations, this does not matter. *) let ftyp = vector_typ (nconstant fsize) dec_ord bit_typ in let reftyp = mk_typ (Typ_app (Id_aux (Id "field_ref", Parse_ast.Unknown), [mk_typ_arg (A_typ (mk_id_typ (mk_id tname))); mk_typ_arg (A_typ ftyp)])) in let rfannot = doc_tannot empty_ctxt Env.empty false reftyp in doc_op equals (concat [string "let "; parens (concat [string tname; underscore; doc_id fid; rfannot])]) (concat [ space; langlebar; string " field_name = \"" ^^ doc_id fid ^^ string "\";"; hardline; space; space; space; string (" field_start = " ^ Big_int.to_string i ^ ";"); hardline; space; space; space; string (" field_is_inc = " ^ dir ^ ";"); hardline; space; space; space; string (" get_field = get_" ^ tname ^ "_" ^ string_of_id fid ^ ";"); hardline; space; space; space; string (" set_field = set_" ^ tname ^ "_" ^ string_of_id fid ^ " "); ranglebar]) in separate_map hardline doc_field fields (* Remove some type variables in a similar fashion to merge_kids_atoms *) let doc_axiom_typschm typ_env (TypSchm_aux (TypSchm_ts (tqs,typ),l) as ts) = let typ_env = add_typquant l tqs typ_env in match typ with | Typ_aux (Typ_fn (typs, ret_ty, eff),l') -> let check_typ (args,used) typ = match Type_check.destruct_atom_nexp typ_env typ with | Some (Nexp_aux (Nexp_var kid,_)) -> if KidSet.mem kid used then args,used else KidSet.add kid args, used | Some _ -> args, used | _ -> args, KidSet.union used (tyvars_of_typ typ) in let args, used = List.fold_left check_typ (KidSet.empty, KidSet.empty) typs in let used = if is_number ret_ty then used else KidSet.union used (tyvars_of_typ ret_ty) in let tqs = match tqs with | TypQ_aux (TypQ_tq qs,l) -> TypQ_aux (TypQ_tq (List.filter (function | QI_aux (QI_id kopt,_) when is_nat_kopt kopt -> let kid = kopt_kid kopt in KidSet.mem kid used && not (KidSet.mem kid args) | _ -> true) qs),l) | _ -> tqs in let doc_typ' typ = match Type_check.destruct_atom_nexp typ_env typ with | Some (Nexp_aux (Nexp_var kid,_)) when KidSet.mem kid args -> parens (doc_var empty_ctxt kid ^^ string " : Z") | _ -> parens (underscore ^^ string " : " ^^ doc_typ empty_ctxt typ) in let arg_typs_pp = separate space (List.map doc_typ' typs) in let _, ret_ty = replace_atom_return_type ret_ty in let ret_typ_pp = doc_typ empty_ctxt ret_ty in let ret_typ_pp = if effectful eff then string "M" ^^ space ^^ parens ret_typ_pp else ret_typ_pp in let tyvars_pp, constrs_pp = doc_typquant_items_separate empty_ctxt braces tqs in string "forall" ^/^ separate space tyvars_pp ^/^ arg_typs_pp ^/^ separate space constrs_pp ^^ comma ^/^ ret_typ_pp | _ -> doc_typschm empty_ctxt true ts let doc_val_spec unimplemented (VS_aux (VS_val_spec(tys,id,_,_),ann)) = if !opt_undef_axioms && IdSet.mem id unimplemented then let typ_env = env_of_annot ann in group (separate space [string "Axiom"; doc_id id; colon; doc_axiom_typschm typ_env tys] ^^ dot) ^/^ hardline else empty (* Type signatures appear in definitions *) (* If a top-level value is declared with an existential type, we turn it into a type annotation expression instead (unless it duplicates an existing one). *) let doc_val pat exp = let (id,pat_typ) = match pat with | P_aux (P_typ (typ, P_aux (P_id id,_)),_) -> id, Some typ | P_aux (P_id id, _) -> id, None | P_aux (P_var (P_aux (P_id id, _), TP_aux (TP_var kid, _)),_) when Id.compare id (id_of_kid kid) == 0 -> id, None | P_aux (P_typ (typ, P_aux (P_var (P_aux (P_id id, _), TP_aux (TP_var kid, _)),_)),_) when Id.compare id (id_of_kid kid) == 0 -> id, Some typ | _ -> raise (Reporting.err_todo (pat_loc pat) "Top-level value definition with complex pattern not supported for Coq yet") in let typpp = match pat_typ with | None -> empty | Some typ -> space ^^ colon ^^ space ^^ doc_typ empty_ctxt typ in let env = env_of exp in let ctxt = { empty_ctxt with debug = List.mem (string_of_id id) (!opt_debug_on) } in let typpp, exp = match pat_typ with | None -> typpp, exp | Some typ -> let typ = expand_range_type (Env.expand_synonyms env typ) in match destruct_exist_plain typ with | None -> typpp, exp | Some _ -> empty, match exp with | E_aux (E_cast (typ',_),_) when alpha_equivalent env typ typ' -> exp | _ -> E_aux (E_cast (typ,exp), (Parse_ast.Unknown, mk_tannot env typ (effect_of exp))) in let idpp = doc_id id in let base_pp = doc_exp ctxt false exp ^^ dot in group (string "Definition" ^^ space ^^ idpp ^^ typpp ^^ space ^^ coloneq ^/^ base_pp) ^^ hardline ^^ group (separate space [string "Hint Unfold"; idpp; colon; string "sail."]) ^^ hardline let rec doc_def unimplemented generic_eq_types def = (* let _ = Pretty_print_sail.pp_defs stderr (Defs [def]) in *) match def with | DEF_spec v_spec -> doc_val_spec unimplemented v_spec | DEF_fixity _ -> empty | DEF_overload _ -> empty | DEF_type t_def -> group (doc_typdef generic_eq_types t_def) ^/^ hardline | DEF_reg_dec dec -> group (doc_dec dec) | DEF_default df -> empty | DEF_fundef fdef -> group (doc_fundef fdef) ^/^ hardline | DEF_internal_mutrec fundefs -> doc_mutrec fundefs ^/^ hardline | DEF_val (LB_aux (LB_val (pat, exp), _)) -> doc_val pat exp | DEF_scattered sdef -> failwith "doc_def: shoulnd't have DEF_scattered at this point" | DEF_mapdef (MD_aux (_, (l,_))) -> unreachable l __POS__ "Coq doesn't support mappings" | DEF_pragma _ -> empty let find_exc_typ defs = let is_exc_typ_def = function | DEF_type td -> string_of_id (id_of_type_def td) = "exception" | _ -> false in if List.exists is_exc_typ_def defs then "exception" else "unit" let find_unimplemented defs = let adjust_fundef unimplemented (FD_aux (FD_function (_,_,_,funcls),_)) = match funcls with | [] -> unimplemented | (FCL_aux (FCL_Funcl (id,_),_))::_ -> IdSet.remove id unimplemented in let adjust_def unimplemented = function | DEF_spec (VS_aux (VS_val_spec (_,id,ext,_),_)) -> begin match ext "coq" with | Some _ -> unimplemented | None -> IdSet.add id unimplemented end | DEF_internal_mutrec fds -> List.fold_left adjust_fundef unimplemented fds | DEF_fundef fd -> adjust_fundef unimplemented fd | _ -> unimplemented in List.fold_left adjust_def IdSet.empty defs let pp_defs_coq (types_file,types_modules) (defs_file,defs_modules) (Defs defs) top_line = try (* let regtypes = find_regtypes d in *) let state_ids = State.generate_regstate_defs true defs |> Initial_check.val_spec_ids in let is_state_def = function | DEF_spec vs -> IdSet.mem (id_of_val_spec vs) state_ids | DEF_fundef fd -> IdSet.mem (id_of_fundef fd) state_ids | _ -> false in let is_typ_def = function | DEF_type _ -> true | _ -> false in let exc_typ = find_exc_typ defs in let typdefs, defs = List.partition is_typ_def defs in let statedefs, defs = List.partition is_state_def defs in let register_refs = State.register_refs_coq (State.find_registers defs) in let unimplemented = find_unimplemented defs in let generic_eq_types = types_used_with_generic_eq defs in let doc_def = doc_def unimplemented generic_eq_types in let () = if !opt_undef_axioms || IdSet.is_empty unimplemented then () else Reporting.print_err Parse_ast.Unknown "Warning" ("The following functions were declared but are undefined:\n" ^ String.concat "\n" (List.map string_of_id (IdSet.elements unimplemented))) in (print types_file) (concat [string "(*" ^^ (string top_line) ^^ string "*)";hardline; (separate_map hardline) (fun lib -> separate space [string "Require Import";string lib] ^^ dot) types_modules;hardline; separate empty (List.map doc_def typdefs); hardline; hardline; separate empty (List.map doc_def statedefs); hardline; hardline; register_refs; hardline; concat [ string ("Definition MR a r := monadR register_value a r " ^ exc_typ ^ "."); hardline; string ("Definition M a := monad register_value a " ^ exc_typ ^ "."); hardline ] ]); (print defs_file) (concat [string "(*" ^^ (string top_line) ^^ string "*)";hardline; (separate_map hardline) (fun lib -> separate space [string "Require Import";string lib] ^^ dot) defs_modules;hardline; string "Import ListNotations."; hardline; string "Open Scope string."; hardline; string "Open Scope bool."; hardline; (* Put the body into a Section so that we can define some values with Let to put them into the local context, where tactics can see them *) string "Section Content."; hardline; hardline; separate empty (List.map doc_def defs); hardline; string "End Content."; hardline]) with Type_check.Type_error (env,l,err) -> let extra = "\nError during Coq printing\n" ^ if Printexc.backtrace_status () then "\n" ^ Printexc.get_backtrace () else "(backtracing unavailable)" in raise (Reporting.err_typ l (Type_error.string_of_type_error err ^ extra))