Require Import Coq.ZArith.ZArith. Require Import Coq.MSets.MSetPositive. Require Import Coq.FSets.FMapPositive. Require Import Coq.Strings.String. Require Import Coq.Strings.Ascii. Require Import Coq.Bool.Bool. Require Import Crypto.Util.ListUtil Coq.Lists.List. Require Crypto.Util.Strings.String. Require Import Crypto.Util.Strings.Decimal. Require Import Crypto.Util.Strings.HexString. Require Import Crypto.Util.Strings.Show. Require Import Crypto.Util.ZRange. Require Import Crypto.Util.ZRange.Operations. Require Import Crypto.Util.ZRange.Show. Require Import Crypto.Util.Option. Require Import Crypto.Util.OptionList. Require Import Crypto.Language. Require Import Crypto.AbstractInterpretation. Require Import Crypto.Util.Bool.Equality. Require Import Crypto.Util.Notations. Import Coq.Lists.List ListNotations. Local Open Scope zrange_scope. Local Open Scope Z_scope. Module Compilers. Local Set Boolean Equality Schemes. Local Set Decidable Equality Schemes. Export Language.Compilers. Export AbstractInterpretation.Compilers. Import invert_expr. Import defaults. Module ToString. Local Open Scope string_scope. Local Open Scope Z_scope. Module Import ZRange. Module Export type. Module Export base. Fixpoint show_interp {t} : Show (ZRange.type.base.interp t) := match t return bool -> ZRange.type.base.interp t -> string with | base.type.unit => @show unit _ | base.type.Z => @show zrange _ | base.type.bool => @show bool _ | base.type.nat => @show nat _ | base.type.zrange => @show zrange _ | base.type.prod A B => fun _ '(a, b) => "(" ++ @show_interp A false a ++ ", " ++ @show_interp B true b ++ ")" | base.type.list A => let SA := @show_interp A in @show (list (ZRange.type.base.interp A)) _ | base.type.option A => let SA := @show_interp A in @show (option (ZRange.type.base.interp A)) _ end%string. Global Existing Instance show_interp. Module Export option. Fixpoint show_interp {t} : Show (ZRange.type.base.option.interp t) := match t return bool -> ZRange.type.base.option.interp t -> string with | base.type.unit => @show unit _ | base.type.Z => @show (option zrange) _ | base.type.bool => @show (option bool) _ | base.type.nat => @show (option nat) _ | base.type.zrange => @show (option zrange) _ | base.type.prod A B => let SA := @show_interp A in let SB := @show_interp B in @show (ZRange.type.base.option.interp A * ZRange.type.base.option.interp B) _ | base.type.list A => let SA := @show_interp A in @show (option (list (ZRange.type.base.option.interp A))) _ | base.type.option A => let SA := @show_interp A in @show (option (option (ZRange.type.base.option.interp A))) _ end. Global Existing Instance show_interp. End option. End base. Module option. Global Instance show_interp {t} : Show (ZRange.type.option.interp t) := fun parens => match t return ZRange.type.option.interp t -> string with | type.base t => fun v : ZRange.type.base.option.interp t => show parens v | type.arrow s d => fun _ => "λ" end. End option. End type. End ZRange. Module PHOAS. Module type. Module base. Global Instance show_base : Show base.type.base := fun _ t => match t with | base.type.unit => "()" | base.type.Z => "ℤ" | base.type.bool => "𝔹" | base.type.nat => "ℕ" | base.type.zrange => "zrange" end. Fixpoint show_type (with_parens : bool) (t : base.type) : string := match t with | base.type.type_base t => show with_parens t | base.type.prod A B => maybe_wrap_parens with_parens (@show_type false A ++ " * " ++ @show_type true B) | base.type.list A => "[" ++ @show_type false A ++ "]" | base.type.option A => maybe_wrap_parens with_parens ("option " ++ @show_type true A) end. Fixpoint show_base_interp {t} : Show (base.base_interp t) := match t with | base.type.unit => @show unit _ | base.type.Z => @show Z _ | base.type.bool => @show bool _ | base.type.nat => @show nat _ | base.type.zrange => @show zrange _ end. Global Existing Instance show_base_interp. Fixpoint show_interp {t} : Show (base.interp t) := match t with | base.type.type_base t => @show (base.base_interp t) _ | base.type.prod A B => @show (base.interp A * base.interp B) _ | base.type.list A => @show (list (base.interp A)) _ | base.type.option A => @show (option (base.interp A)) _ end. Global Existing Instance show_interp. Global Instance show : Show base.type := show_type. End base. Fixpoint show_for_each_lhs_of_arrow {base_type} {f : type.type base_type -> Type} {show_f : forall t, Show (f t)} {t : type.type base_type} : Show (type.for_each_lhs_of_arrow f t) := match t return bool -> type.for_each_lhs_of_arrow f t -> string with | type.base t => @show unit _ | type.arrow s d => fun with_parens '((x, xs) : f s * type.for_each_lhs_of_arrow f d) => let _ : Show (f s) := show_f s in let _ : Show (type.for_each_lhs_of_arrow f d) := @show_for_each_lhs_of_arrow base_type f show_f d in match d with | type.base _ => show with_parens x | type.arrow _ _ => maybe_wrap_parens with_parens (show true x ++ ", " ++ show false xs) end end. Global Existing Instance show_for_each_lhs_of_arrow. Fixpoint show_type {base_type} {S : Show base_type} (with_parens : bool) (t : type.type base_type) : string := match t with | type.base t => S with_parens t | type.arrow s d => maybe_wrap_parens with_parens (@show_type base_type S true s ++ " → " ++ @show_type base_type S false d) end. Global Instance show {base_type} {S : Show base_type} : Show (type.type base_type) := show_type. End type. Definition bitwidth_to_string (v : Z) : string := (if v =? 2^Z.log2 v then "2^" ++ decimal_string_of_Z (Z.log2 v) else HexString.of_Z v). Definition show_range_or_ctype (v : zrange) : string := if (v.(lower) =? 0) && (v.(upper) =? 2^(Z.log2 (v.(upper) + 1)) - 1) then ("uint" ++ decimal_string_of_Z (Z.log2 (v.(upper) + 1)) ++ "_t")%string else let lg2 := 1 + Z.log2 (-v.(lower)) in if (v.(lower) =? -2^(lg2-1)) && (v.(upper) =? 2^(lg2-1)-1) then ("int" ++ decimal_string_of_Z lg2 ++ "_t")%string else show false v. Definition show_compact_Z (with_parens : bool) (v : Z) : string := let is_neg := v option string := match t with | base.type.Z => option_map show_range_or_ctype | base.type.type_base t => fun _ => None | base.type.prod A B => fun '(r1, r2) => match @make_castb A r1, @make_castb B r2 with | Some c1, Some c2 => Some (c1 ++ ", " ++ c2) | None, Some c => Some ("??, " ++ c) | Some c, None => Some (c ++ ", ??") | None, None => None end | base.type.list _ | base.type.option _ => fun _ => None end. Fixpoint make_cast {t} : ZRange.type.option.interp t -> option string := match t with | type.base t => @make_castb t | type.arrow _ _ => fun _ => None end. Definition maybe_wrap_cast (with_cast : bool) {t} (xr : (nat -> string) * ZRange.type.option.interp t) (lvl : nat) : string := match with_cast, make_cast (snd xr) with | true, Some c => "(" ++ c ++ ")" ++ fst xr 10%nat | _, _ => fst xr lvl end. Definition show_application (with_casts : bool) {t : type} (f : nat -> string) (args : type.for_each_lhs_of_arrow (fun t => (nat -> string) * ZRange.type.option.interp t)%type t) : nat -> string := match t return type.for_each_lhs_of_arrow (fun t => (nat -> string) * ZRange.type.option.interp t)%type t -> nat -> string with | type.base _ => fun 'tt lvl => f lvl | type.arrow s d => fun xs lvl => let _ : forall t, Show ((nat -> string) * ZRange.type.option.interp t)%type := (fun t with_parens x => maybe_wrap_cast with_casts x 10%nat) in maybe_wrap_parens (Nat.ltb lvl 11) (f 11%nat ++ show true xs) end args. Module ident. Definition show_ident_lvl (with_casts : bool) {t} (idc : ident.ident t) : type.for_each_lhs_of_arrow (fun t => (nat -> string) * ZRange.type.option.interp t)%type t -> (nat -> string) * ZRange.type.base.option.interp (type.final_codomain t) := match idc in ident.ident t return type.for_each_lhs_of_arrow (fun t => (nat -> string) * ZRange.type.option.interp t)%type t -> (nat -> string) * ZRange.type.base.option.interp (type.final_codomain t) with | ident.Literal base.type.Z v => fun 'tt => (fun lvl => show_compact_Z (Nat.eqb lvl 0) v, ZRange.type.base.option.None) | ident.Literal t v => fun 'tt => (fun lvl => show (Nat.eqb lvl 0) v, ZRange.type.base.option.None) | ident.Nat_succ => fun '((x, xr), tt) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 10) ((x 10%nat) ++ ".+1"), ZRange.type.base.option.None) | ident.Nat_pred => fun '((x, xr), tt) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 10) ((x 10%nat) ++ ".-1"), ZRange.type.base.option.None) | ident.Nat_max => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 10) ("Nat.max " ++ x 9%nat ++ " " ++ y 9%nat), ZRange.type.base.option.None) | ident.Nat_mul => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 40) (x 40%nat ++ " *ℕ " ++ y 39%nat), ZRange.type.base.option.None) | ident.Nat_add => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 50) (x 50%nat ++ " +ℕ " ++ y 49%nat), ZRange.type.base.option.None) | ident.Nat_sub => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 50) (x 50%nat ++ " -ℕ " ++ y 49%nat), ZRange.type.base.option.None) | ident.Nat_eqb => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 70) (x 69%nat ++ " =ℕ " ++ y 69%nat), ZRange.type.base.option.None) | ident.Some _ => fun args => (show_application with_casts (fun _ => "Some") args, ZRange.type.base.option.None) | ident.None _ => fun 'tt => (fun _ => "None", ZRange.type.base.option.None) | ident.nil t => fun 'tt => (fun _ => "[]", ZRange.type.base.option.None) | ident.cons t => fun '(x, ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 60) (maybe_wrap_cast with_casts x 59%nat ++ " :: " ++ y 60%nat), ZRange.type.base.option.None) | ident.pair A B => fun '(x, (y, tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 201) (maybe_wrap_cast with_casts x 201%nat ++ ", " ++ maybe_wrap_cast with_casts y 200%nat), ZRange.type.base.option.None) | ident.fst A B => fun '((x, xr), tt) => (fun _ => x 0%nat ++ "₁", fst xr) | ident.snd A B => fun '((x, xr), tt) => (fun _ => x 0%nat ++ "₂", snd xr) | ident.prod_rect A B T => fun '((f, fr), ((p, pr), tt)) => (fun _ => "match " ++ p 200%nat ++ " with " ++ f 200%nat ++ " end", ZRange.type.base.option.None) | ident.bool_rect T => fun '(t, (f, ((b, br), tt))) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 200) ("if " ++ b 200%nat ++ " then " ++ maybe_wrap_cast with_casts t 200%nat ++ " else " ++ maybe_wrap_cast with_casts f 200%nat), ZRange.type.base.option.None) | ident.nat_rect P => fun args => (show_application with_casts (fun _ => "nat_rect") args, ZRange.type.base.option.None) | ident.eager_nat_rect P => fun args => (show_application with_casts (fun _ => "eager_nat_rect") args, ZRange.type.base.option.None) | ident.eager_nat_rect_arrow P Q => fun args => (show_application with_casts (fun _ => "eager_nat_rect(→)") args, ZRange.type.base.option.None) | ident.nat_rect_arrow P Q => fun args => (show_application with_casts (fun _ => "nat_rect(→)") args, ZRange.type.base.option.None) | ident.option_rect A P => fun args => (show_application with_casts (fun _ => "option_rect") args, ZRange.type.base.option.None) | ident.list_rect A P => fun args => (show_application with_casts (fun _ => "list_rect") args, ZRange.type.base.option.None) | ident.eager_list_rect A P => fun args => (show_application with_casts (fun _ => "eager_list_rect") args, ZRange.type.base.option.None) | ident.list_rect_arrow A P Q => fun args => (show_application with_casts (fun _ => "list_rect(→)") args, ZRange.type.base.option.None) | ident.eager_list_rect_arrow A P Q => fun args => (show_application with_casts (fun _ => "eager_list_rect(→)") args, ZRange.type.base.option.None) | ident.list_case A P => fun args => (show_application with_casts (fun _ => "list_case") args, ZRange.type.base.option.None) | ident.List_length T => fun args => (show_application with_casts (fun _ => "len") args, ZRange.type.base.option.None) | ident.List_seq => fun args => (show_application with_casts (fun _ => "seq") args, ZRange.type.base.option.None) | ident.List_repeat A => fun args => (show_application with_casts (fun _ => "repeat") args, ZRange.type.base.option.None) | ident.List_firstn A => fun args => (show_application with_casts (fun _ => "firstn") args, ZRange.type.base.option.None) | ident.List_skipn A => fun args => (show_application with_casts (fun _ => "skipn") args, ZRange.type.base.option.None) | ident.List_combine A B => fun args => (show_application with_casts (fun _ => "combine") args, ZRange.type.base.option.None) | ident.List_map A B => fun args => (show_application with_casts (fun _ => "map") args, ZRange.type.base.option.None) | ident.List_app A => fun '((xs, xsr), ((ys, ysr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 60) (xs 59%nat ++ " ++ " ++ ys 60%nat), ZRange.type.base.option.None) | ident.List_rev A => fun args => (show_application with_casts (fun _ => "rev") args, ZRange.type.base.option.None) | ident.List_flat_map A B => fun args => (show_application with_casts (fun _ => "flat_map") args, ZRange.type.base.option.None) | ident.List_partition A => fun args => (show_application with_casts (fun _ => "partition") args, ZRange.type.base.option.None) | ident.List_fold_right A B => fun args => (show_application with_casts (fun _ => "fold_right") args, ZRange.type.base.option.None) | ident.List_update_nth T => fun args => (show_application with_casts (fun _ => "update_nth") args, ZRange.type.base.option.None) | ident.eager_List_nth_default T => fun '((d, dr), ((ls, lsr), ((i, ir), tt))) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 10) (ls 10%nat ++ "[[" ++ i 200%nat ++ "]]"), ZRange.type.base.option.None) | ident.List_nth_default T => fun '((d, dr), ((ls, lsr), ((i, ir), tt))) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 10) (ls 10%nat ++ "[" ++ i 200%nat ++ "]"), ZRange.type.base.option.None) | ident.Z_mul => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 40) (x 40%nat ++ " * " ++ y 39%nat), ZRange.type.base.option.None) | ident.Z_add => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 50) (x 50%nat ++ " + " ++ y 49%nat), ZRange.type.base.option.None) | ident.Z_sub => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 50) (x 50%nat ++ " - " ++ y 49%nat), ZRange.type.base.option.None) | ident.Z_pow => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 30) (x 30%nat ++ " ^ " ++ y 29%nat), ZRange.type.base.option.None) | ident.Z_opp => fun '((x, xr), tt) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 35) ("-" ++ x 35%nat), ZRange.type.base.option.None) | ident.Z_bneg => fun '((x, xr), tt) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 75) ("!" ++ x 75%nat), ZRange.type.base.option.None) | ident.Z_lnot_modulo => fun '((x, xr), ((m, mr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 75) ("~" ++ x 75%nat ++ (if with_casts then " (mod " ++ m 200%nat ++ ")" else "")), ZRange.type.base.option.None) | ident.Z_div => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 40) (x 40%nat ++ " / " ++ y 39%nat), ZRange.type.base.option.None) | ident.Z_modulo => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 40) (x 40%nat ++ " mod " ++ y 39%nat), ZRange.type.base.option.None) | ident.Z_eqb => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 70) (x 69%nat ++ " = " ++ y 69%nat), ZRange.type.base.option.None) | ident.Z_ltb => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 70) (x 69%nat ++ " < " ++ y 69%nat), ZRange.type.base.option.None) | ident.Z_leb => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 70) (x 69%nat ++ " ≤ " ++ y 69%nat), ZRange.type.base.option.None) | ident.Z_gtb => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 70) (x 69%nat ++ " > " ++ y 69%nat), ZRange.type.base.option.None) | ident.Z_geb => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 70) (x 69%nat ++ " ≥ " ++ y 69%nat), ZRange.type.base.option.None) | ident.Z_log2 => fun args => (show_application with_casts (fun _ => "Z.log2") args, ZRange.type.base.option.None) | ident.Z_log2_up => fun args => (show_application with_casts (fun _ => "Z.log2_up") args, ZRange.type.base.option.None) | ident.Z_of_nat => fun args => (show_application with_casts (fun _ => "(ℕ→ℤ)") args, ZRange.type.base.option.None) | ident.Z_to_nat => fun args => (show_application with_casts (fun _ => "(ℤ→ℕ)") args, ZRange.type.base.option.None) | ident.Z_min => fun args => (show_application with_casts (fun _ => "Z.min") args, ZRange.type.base.option.None) | ident.Z_max => fun args => (show_application with_casts (fun _ => "Z.max") args, ZRange.type.base.option.None) | ident.Z_shiftr => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 30) (x 30%nat ++ " >> " ++ y 29%nat), ZRange.type.base.option.None) | ident.Z_shiftl => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 30) (x 30%nat ++ " << " ++ y 29%nat), ZRange.type.base.option.None) | ident.Z_land => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 50) (x 50%nat ++ " & " ++ y 49%nat), ZRange.type.base.option.None) | ident.Z_lor => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 50) (x 50%nat ++ " | " ++ y 49%nat), ZRange.type.base.option.None) | ident.Z_mul_split => fun args => (show_application with_casts (fun _ => "Z.mul_split") args, ZRange.type.base.option.None) | ident.Z_add_get_carry => fun args => (show_application with_casts (fun _ => "Z.add_get_carry") args, ZRange.type.base.option.None) | ident.Z_add_with_carry => fun args => (show_application with_casts (fun _ => "Z.add_with_carry") args, ZRange.type.base.option.None) | ident.Z_add_with_get_carry => fun args => (show_application with_casts (fun _ => "Z.add_with_get_carry") args, ZRange.type.base.option.None) | ident.Z_sub_get_borrow => fun args => (show_application with_casts (fun _ => "Z.sub_get_borrow") args, ZRange.type.base.option.None) | ident.Z_sub_with_get_borrow => fun args => (show_application with_casts (fun _ => "Z.sub_with_get_borrow") args, ZRange.type.base.option.None) | ident.Z_zselect => fun args => (show_application with_casts (fun _ => "Z.zselect") args, ZRange.type.base.option.None) | ident.Z_add_modulo => fun args => (show_application with_casts (fun _ => "Z.add_modulo") args, ZRange.type.base.option.None) | ident.Z_rshi => fun args => (show_application with_casts (fun _ => "Z.rshi") args, ZRange.type.base.option.None) | ident.Z_cc_m => fun args => (show_application with_casts (fun _ => "Z.cc_m") args, ZRange.type.base.option.None) | ident.Z_combine_at_bitwidth => fun args => (show_application with_casts (fun _ => "Z.combine_at_bitwidth") args, ZRange.type.base.option.None) | ident.Z_cast range => fun '((x, xr), tt) => (x, Some range) | ident.Z_cast2 (r1, r2) => fun '((x, xr), tt) => (x, (Some r1, Some r2)) | ident.Build_zrange => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 0) ("r[" ++ x 60%nat ++ " ~> " ++ y 200%nat), ZRange.type.base.option.None) | ident.zrange_rect A => fun args => (show_application with_casts (fun _ => "zrange_rect") args, ZRange.type.base.option.None) | ident.fancy_add log2wordmax imm => fun args => (show_application with_casts (fun lvl' => maybe_wrap_parens (Nat.ltb lvl' 11) ("fancy.add 2^" ++ decimal_string_of_Z log2wordmax ++ " " ++ HexString.of_Z imm)) args, ZRange.type.base.option.None) | ident.fancy_addc log2wordmax imm => fun args => (show_application with_casts (fun lvl' => maybe_wrap_parens (Nat.ltb lvl' 11) ("fancy.addc 2^" ++ decimal_string_of_Z log2wordmax ++ " " ++ HexString.of_Z imm)) args, ZRange.type.base.option.None) | ident.fancy_sub log2wordmax imm => fun args => (show_application with_casts (fun lvl' => maybe_wrap_parens (Nat.ltb lvl' 11) ("fancy.sub 2^" ++ decimal_string_of_Z log2wordmax ++ " " ++ HexString.of_Z imm)) args, ZRange.type.base.option.None) | ident.fancy_subb log2wordmax imm => fun args => (show_application with_casts (fun lvl' => maybe_wrap_parens (Nat.ltb lvl' 11) ("fancy.subb 2^" ++ decimal_string_of_Z log2wordmax ++ " " ++ HexString.of_Z imm)) args, ZRange.type.base.option.None) | ident.fancy_mulll log2wordmax => fun args => (show_application with_casts (fun lvl' => maybe_wrap_parens (Nat.ltb lvl' 11) ("fancy.mulll 2^" ++ decimal_string_of_Z log2wordmax)) args, ZRange.type.base.option.None) | ident.fancy_mullh log2wordmax => fun args => (show_application with_casts (fun lvl' => maybe_wrap_parens (Nat.ltb lvl' 11) ("fancy.mullh 2^" ++ decimal_string_of_Z log2wordmax)) args, ZRange.type.base.option.None) | ident.fancy_mulhl log2wordmax => fun args => (show_application with_casts (fun lvl' => maybe_wrap_parens (Nat.ltb lvl' 11) ("fancy.mulhl 2^" ++ decimal_string_of_Z log2wordmax)) args, ZRange.type.base.option.None) | ident.fancy_mulhh log2wordmax => fun args => (show_application with_casts (fun lvl' => maybe_wrap_parens (Nat.ltb lvl' 11) ("fancy.mulhh 2^" ++ decimal_string_of_Z log2wordmax)) args, ZRange.type.base.option.None) | ident.fancy_rshi log2wordmax x => fun args => (show_application with_casts (fun lvl' => maybe_wrap_parens (Nat.ltb lvl' 11) ("fancy.rshi 2^" ++ decimal_string_of_Z log2wordmax ++ " " ++ decimal_string_of_Z x)) args, ZRange.type.base.option.None) | ident.fancy_selc => fun args => (show_application with_casts (fun _ => "fancy.selc") args, ZRange.type.base.option.None) | ident.fancy_selm log2wordmax => fun args => (show_application with_casts (fun lvl' => maybe_wrap_parens (Nat.ltb lvl' 11) ("fancy.selm 2^" ++ decimal_string_of_Z log2wordmax)) args, ZRange.type.base.option.None) | ident.fancy_sell => fun args => (show_application with_casts (fun _ => "fancy.sell") args, ZRange.type.base.option.None) | ident.fancy_addm => fun args => (show_application with_casts (fun _ => "fancy.addm") args, ZRange.type.base.option.None) end. Global Instance show_ident {t} : Show (ident.ident t) := fun with_parens idc => match idc with | ident.Literal base.type.Z v => show_compact_Z with_parens v | ident.Literal t v => show with_parens v | ident.Nat_succ => "Nat.succ" | ident.Nat_pred => "Nat.pred" | ident.Nat_max => "Nat.max" | ident.Nat_mul => "Nat.mul" | ident.Nat_add => "Nat.add" | ident.Nat_sub => "Nat.sub" | ident.Nat_eqb => "Nat.eqb" | ident.nil t => "[]" | ident.cons t => "(::)" | ident.pair A B => "(,)" | ident.fst A B => "fst" | ident.snd A B => "snd" | ident.prod_rect A B T => "prod_rect" | ident.bool_rect T => "bool_rect" | ident.nat_rect P => "nat_rect" | ident.eager_nat_rect P => "eager_nat_rect" | ident.nat_rect_arrow P Q => "nat_rect(→)" | ident.eager_nat_rect_arrow P Q => "eager_nat_rect(→)" | ident.list_rect A P => "list_rect" | ident.eager_list_rect A P => "eager_list_rect" | ident.list_rect_arrow A P Q => "list_rect(→)" | ident.eager_list_rect_arrow A P Q => "eager_list_rect(→)" | ident.list_case A P => "list_case" | ident.List_length T => "length" | ident.List_seq => "seq" | ident.List_repeat A => "repeat" | ident.List_firstn A => "firstn" | ident.List_skipn A => "skipn" | ident.List_combine A B => "combine" | ident.List_map A B => "map" | ident.List_app A => "(++)" | ident.List_rev A => "rev" | ident.List_flat_map A B => "flat_map" | ident.List_partition A => "partition" | ident.List_fold_right A B => "fold_right" | ident.List_update_nth T => "update_nth" | ident.List_nth_default T => "nth" | ident.eager_List_nth_default T => "eager_nth" | ident.Some _ => "Some" | ident.None _ => "None" | ident.option_rect _ _ => "option_rect" | ident.Z_add => "(+)" | ident.Z_mul => "( * )" | ident.Z_pow => "(^)" | ident.Z_sub => "(-)" | ident.Z_opp => "-" | ident.Z_div => "(/)" | ident.Z_modulo => "(mod)" | ident.Z_eqb => "(=)" | ident.Z_leb => "(≤)" | ident.Z_ltb => "(<)" | ident.Z_geb => "(≥)" | ident.Z_gtb => "(>)" | ident.Z_min => "min" | ident.Z_max => "max" | ident.Z_log2 => "log₂" | ident.Z_log2_up => "⌈log₂⌉" | ident.Z_of_nat => "(ℕ→ℤ)" | ident.Z_to_nat => "(ℤ→ℕ)" | ident.Z_shiftr => "(>>)" | ident.Z_shiftl => "(<<)" | ident.Z_land => "(&)" | ident.Z_lor => "(|)" | ident.Z_lnot_modulo => "~" | ident.Z_bneg => "!" | ident.Z_mul_split => "Z.mul_split" | ident.Z_add_get_carry => "Z.add_get_carry" | ident.Z_add_with_carry => "Z.add_with_carry" | ident.Z_add_with_get_carry => "Z.add_with_get_carry" | ident.Z_sub_get_borrow => "Z.sub_get_borrow" | ident.Z_sub_with_get_borrow => "Z.sub_with_get_borrow" | ident.Z_zselect => "Z.zselect" | ident.Z_add_modulo => "Z.add_modulo" | ident.Z_rshi => "Z.rshi" | ident.Z_cc_m => "Z.cc_m" | ident.Z_combine_at_bitwidth => "Z.combine_at_bitwidth" | ident.Z_cast range => "(" ++ show_range_or_ctype range ++ ")" | ident.Z_cast2 (r1, r2) => "(" ++ show_range_or_ctype r1 ++ ", " ++ show_range_or_ctype r2 ++ ")" | ident.Build_zrange => "Build_zrange" | ident.zrange_rect _ => "zrange_rect" | ident.fancy_add log2wordmax imm => maybe_wrap_parens with_parens ("fancy.add 2^" ++ decimal_string_of_Z log2wordmax ++ " " ++ HexString.of_Z imm) | ident.fancy_addc log2wordmax imm => maybe_wrap_parens with_parens ("fancy.addc 2^" ++ decimal_string_of_Z log2wordmax ++ " " ++ HexString.of_Z imm) | ident.fancy_sub log2wordmax imm => maybe_wrap_parens with_parens ("fancy.sub 2^" ++ decimal_string_of_Z log2wordmax ++ " " ++ HexString.of_Z imm) | ident.fancy_subb log2wordmax imm => maybe_wrap_parens with_parens ("fancy.subb 2^" ++ decimal_string_of_Z log2wordmax ++ " " ++ HexString.of_Z imm) | ident.fancy_mulll log2wordmax => maybe_wrap_parens with_parens ("fancy.mulll 2^" ++ decimal_string_of_Z log2wordmax) | ident.fancy_mullh log2wordmax => maybe_wrap_parens with_parens ("fancy.mullh 2^" ++ decimal_string_of_Z log2wordmax) | ident.fancy_mulhl log2wordmax => maybe_wrap_parens with_parens ("fancy.mulhl 2^" ++ decimal_string_of_Z log2wordmax) | ident.fancy_mulhh log2wordmax => maybe_wrap_parens with_parens ("fancy.mulhh 2^" ++ decimal_string_of_Z log2wordmax) | ident.fancy_rshi log2wordmax x => maybe_wrap_parens with_parens ("fancy.rshi 2^" ++ decimal_string_of_Z log2wordmax ++ " " ++ decimal_string_of_Z x) | ident.fancy_selc => "fancy.selc" | ident.fancy_selm log2wordmax => maybe_wrap_parens with_parens ("fancy.selm 2^" ++ decimal_string_of_Z log2wordmax) | ident.fancy_sell => "fancy.sell" | ident.fancy_addm => "fancy.addm" end. End ident. Module expr. Local Notation show_ident := ident.show_ident. Local Notation show_ident_lvl := ident.show_ident_lvl. Fixpoint get_eta_cps_args {A} (t : type) (idx : positive) {struct t} : (type.for_each_lhs_of_arrow (fun y => (nat -> string) * ZRange.type.option.interp y)%type t -> positive -> A) -> list string * A := match t with | type.arrow s d => fun k => let n := "x" ++ decimal_string_of_pos idx in let '(args, show_f) := @get_eta_cps_args A d (Pos.succ idx) (fun arglist => k (((fun _ => n), ZRange.type.option.None), arglist)) in (n :: args, show_f) | type.base _ => fun k => (nil, k tt idx) end. Section helper. Context (k : forall t, @expr.expr base.type ident (fun _ => string) t -> type.for_each_lhs_of_arrow (fun t => (nat -> string) * ZRange.type.option.interp t)%type t -> positive -> (positive * (nat -> list string)) * ZRange.type.base.option.interp (type.final_codomain t)). Fixpoint show_eta_abs_cps' {t} (idx : positive) (e : @expr.expr base.type ident (fun _ => string) t) : (positive * (list string * (nat -> list string))) * ZRange.type.base.option.interp (type.final_codomain t) := match e in expr.expr t return (unit -> _ * ZRange.type.base.option.interp (type.final_codomain t)) -> _ * ZRange.type.base.option.interp (type.final_codomain t) with | expr.Abs s d f => fun _ => let n := "x" ++ decimal_string_of_pos idx in let '(_, (args, show_f), r) := @show_eta_abs_cps' d (Pos.succ idx) (f n) in (idx, (n :: args, show_f), r) | _ => fun default => default tt end (fun _ => let '(args, (idx, show_f, r)) := get_eta_cps_args _ idx (@k _ e) in ((idx, (args, show_f)), r)). Definition show_eta_abs_cps (with_casts : bool) {t} (idx : positive) (e : @expr.expr base.type ident (fun _ => string) t) (extraargs : type.for_each_lhs_of_arrow (fun t => (nat -> string) * ZRange.type.option.interp t)%type t) : (positive * (nat -> list string)) * ZRange.type.base.option.interp (type.final_codomain t) := let '(idx, (args, show_f), r) := @show_eta_abs_cps' t idx e in let argstr := String.concat " " args in (idx, fun lvl => match show_f lvl with | nil => [show_application with_casts (fun _ => "(λ " ++ argstr ++ ", (* NOTHING‽ *))") extraargs 11%nat]%string | show_f::nil => [show_application with_casts (fun _ => "(λ " ++ argstr ++ ", " ++ show_f ++ ")") extraargs 11%nat]%string | show_f => ["(λ " ++ argstr ++ ","]%string ++ (List.map (fun v => String " " (String " " v)) show_f) ++ [")" ++ show_application with_casts (fun _ => "") extraargs 11%nat]%string end%list, r). Definition show_eta_cps {t} (idx : positive) (e : @expr.expr base.type ident (fun _ => string) t) : (positive * (nat -> list string)) * ZRange.type.option.interp t := let '(idx, (args, show_f), r) := @show_eta_abs_cps' t idx e in let argstr := String.concat " " args in (idx, (fun lvl => match args, show_f lvl with | nil, show_f => show_f | _, nil => ["(λ " ++ argstr ++ ", (* NOTHING‽ *))"]%string | _, show_f::nil => ["(λ " ++ argstr ++ ", " ++ show_f ++ ")"]%string | _, show_f => ["(λ " ++ argstr ++ ","]%string ++ (List.map (fun v => String " " (String " " v)) show_f) ++ [")"] end%list), match t return ZRange.type.base.option.interp (type.final_codomain t) -> ZRange.type.option.interp t with | type.base _ => fun r => r | type.arrow _ _ => fun _ => ZRange.type.option.None end r). End helper. Fixpoint show_expr_lines (with_casts : bool) {t} (e : @expr.expr base.type ident (fun _ => string) t) (args : type.for_each_lhs_of_arrow (fun t => (nat -> string) * ZRange.type.option.interp t)%type t) (idx : positive) {struct e} : (positive * (nat -> list string)) * ZRange.type.base.option.interp (type.final_codomain t) := match e in expr.expr t return type.for_each_lhs_of_arrow (fun t => (nat -> string) * ZRange.type.option.interp t)%type t -> (positive * (nat -> list string)) * ZRange.type.base.option.interp (type.final_codomain t) with | expr.Ident t idc => fun args => let '(v, r) := @show_ident_lvl with_casts t idc args in (idx, fun lvl => [v lvl], r) | expr.Var t v => fun args => (idx, fun lvl => [show_application with_casts (fun _ => v) args lvl], ZRange.type.base.option.None) | expr.Abs s d f as e => fun args => show_eta_abs_cps (fun t e args idx => let '(idx, v, r) := @show_expr_lines with_casts t e args idx in (idx, fun _ => v 200%nat, r)) with_casts idx e args | expr.App s d f x => fun args => let '(idx', x', xr) := show_eta_cps (fun t e args idx => @show_expr_lines with_casts t e args idx) idx x in @show_expr_lines with_casts _ f (((fun lvl => String.concat String.NewLine (x' lvl)), xr), args) idx | expr.LetIn A (type.base B) x f => fun 'tt => let n := "x" ++ decimal_string_of_pos idx in let '(_, show_x, xr) := show_eta_cps (fun t e args idx => @show_expr_lines with_casts t e args idx) idx x in let '(idx, show_f, fr) := show_eta_cps (fun t e args idx => @show_expr_lines with_casts t e args idx) (Pos.succ idx) (f n) in let ty_str := match make_cast xr with | Some c => " : " ++ c | None => "" end in let expr_let_line := "expr_let " ++ n ++ " := " in (idx, (fun lvl => match show_x 200%nat with | nil => [expr_let_line ++ "(* NOTHING‽ *) (*" ++ ty_str ++ " *) in"]%string ++ show_f 200%nat | show_x::nil => [expr_let_line ++ show_x ++ " (*" ++ ty_str ++ " *) in"]%string ++ show_f 200%nat | show_x::rest => ([expr_let_line ++ show_x]%string) ++ (List.map (fun l => String.of_list (List.repeat " "%char (String.length expr_let_line)) ++ l)%string rest) ++ ["(*" ++ ty_str ++ " *)"]%string ++ ["in"] ++ show_f 200%nat end%list), fr) | expr.LetIn A B x f => fun args => let n := "x" ++ decimal_string_of_pos idx in let '(_, show_x, xr) := show_eta_cps (fun t e args idx => @show_expr_lines with_casts t e args idx) idx x in let '(idx, show_f, fr) := show_eta_cps (fun t e args idx => @show_expr_lines with_casts t e args idx) (Pos.succ idx) (f n) in let ty_str := match make_cast xr with | Some c => " : " ++ c | None => "" end in let expr_let_line := "expr_let " ++ n ++ " := " in (idx, (fun lvl => (["("] ++ (map (String " ") match show_x 200%nat with | nil => [expr_let_line ++ "(* NOTHING‽ *) (*" ++ ty_str ++ " *) in"]%string ++ show_f 200%nat | show_x::nil => [expr_let_line ++ show_x ++ " (*" ++ ty_str ++ " *) in"]%string ++ show_f 200%nat | show_x::rest => ([expr_let_line ++ show_x]%string) ++ (List.map (fun l => String.of_list (List.repeat " "%char (String.length expr_let_line)) ++ l)%string rest) ++ ["(*" ++ ty_str ++ " *)"]%string ++ ["in"] ++ show_f 200%nat end%list) ++ [")"; show_application with_casts (fun _ => "") args 11%nat])%list), ZRange.type.base.option.None) end args. Fixpoint show_var_expr {var t} (with_parens : bool) (e : @expr.expr base.type ident var t) : string := match e with | expr.Ident t idc => show with_parens idc | expr.Var t v => maybe_wrap_parens with_parens ("VAR_(" ++ show false t ++ ")") | expr.Abs s d f => "λ_(" ++ show false t ++ ")" | expr.App s d f x => let show_f := @show_var_expr _ _ false f in let show_x := @show_var_expr _ _ true x in maybe_wrap_parens with_parens (show_f ++ " @ " ++ show_x) | expr.LetIn A B x f => let show_x := @show_var_expr _ _ false x in maybe_wrap_parens with_parens ("expr_let _ := " ++ show_x ++ " in _") end%string. Definition partially_show_expr {var t} : Show (@expr.expr base.type ident var t) := show_var_expr. Local Notation default_with_casts := false. Global Instance show_lines_expr {t} : ShowLines (@expr.expr base.type ident (fun _ => string) t) := fun with_parens e => let '(_, v, _) := show_eta_cps (fun t e args idx => @show_expr_lines default_with_casts t e args idx) 1%positive e in v (if with_parens then 0%nat else 201%nat). Global Instance show_lines_Expr {t} : ShowLines (@expr.Expr base.type ident t) := fun with_parens e => show_lines with_parens (e _). Global Instance show_expr {t} : Show (@expr.expr base.type ident (fun _ => string) t) := fun with_parens e => String.concat String.NewLine (show_lines with_parens e). Global Instance show_Expr {t} : Show (@expr.Expr base.type ident t) := fun with_parens e => show with_parens (e _). End expr. End PHOAS. Module C. Module type. Inductive primitive := Z | Zptr. Inductive type := type_primitive (t : primitive) | prod (A B : type) | unit. Module Export Notations. Global Coercion type_primitive : primitive >-> type. Delimit Scope Ctype_scope with Ctype. Bind Scope Ctype_scope with type. Notation "()" := unit : Ctype_scope. Notation "A * B" := (prod A B) : Ctype_scope. Notation type := type. End Notations. End type. Import type.Notations. Module int. Inductive type := signed (lgbitwidth : nat) | unsigned (lgbitwidth : nat). Definition lgbitwidth_of (t : type) : nat := match t with | signed lgbitwidth => lgbitwidth | unsigned lgbitwidth => lgbitwidth end. Definition bitwidth_of (t : type) : Z := 2^Z.of_nat (lgbitwidth_of t). Definition is_signed (t : type) : bool := match t with signed _ => true | unsigned _ => false end. Definition is_unsigned (t : type) : bool := negb (is_signed t). Definition to_zrange (t : type) : zrange := let bw := bitwidth_of t in if is_signed t then r[-2^(bw-1) ~> 2^(bw-1) - 1] else r[0 ~> 2^bw - 1]. Definition is_tighter_than (t1 t2 : type) := ZRange.is_tighter_than_bool (to_zrange t1) (to_zrange t2). Definition of_zrange_relaxed (r : zrange) : type := let lg2 := Z.log2_up ((upper r - lower r) + 1) in let lg2u := Z.log2_up (upper r + 1) in let lg2l := (if (lower r maybe_wrap_parens with_parens ((if is_unsigned t then "u" else "") ++ "int" ++ decimal_string_of_Z (bitwidth_of t)). Definition union (t1 t2 : type) : type := of_zrange_relaxed (ZRange.union (to_zrange t1) (to_zrange t2)). Definition union_zrange (r : zrange) (t : type) : type := of_zrange_relaxed (ZRange.union r (to_zrange t)). Fixpoint base_interp (t : base.type) : Set := match t with | base.type.Z => type | base.type.type_base _ => unit | base.type.prod A B => base_interp A * base_interp B | base.type.list A => list (base_interp A) | base.type.option A => option (base_interp A) end%type. Module option. Fixpoint interp (t : base.type) : Set := match t with | base.type.Z => option type | base.type.type_base _ => unit | base.type.prod A B => interp A * interp B | base.type.list A => option (list (interp A)) | base.type.option A => option (option (interp A)) end%type. Fixpoint None {t} : interp t := match t with | base.type.Z => Datatypes.None | base.type.type_base _ => tt | base.type.prod A B => (@None A, @None B) | base.type.list A => Datatypes.None | base.type.option A => Datatypes.None end. Fixpoint Some {t} : base_interp t -> interp t := match t with | base.type.Z => Datatypes.Some | base.type.type_base _ => fun tt => tt | base.type.prod A B => fun '(a, b) => (@Some A a, @Some B b) | base.type.list A => fun ls => Datatypes.Some (List.map (@Some A) ls) | base.type.option A => fun ls => Datatypes.Some (Option.map (@Some A) ls) end. End option. Module Export Notations. Notation _Bool := (unsigned 0). Notation uint8 := (unsigned 3). Notation int8 := (signed 3). Notation uint16 := (unsigned 4). Notation int16 := (signed 4). Notation uint32 := (unsigned 5). Notation int32 := (signed 5). Notation uint64 := (unsigned 6). Notation int64 := (signed 6). Notation uint128 := (unsigned 7). Notation int128 := (signed 7). End Notations. End int. Import int.Notations. Example of_zrange_int32 : int.of_zrange_relaxed r[-2^31 ~> 2^31-1] = int32 := eq_refl. Example of_zrange_int64 : int.of_zrange_relaxed r[-2^31-1 ~> 2^31-1] = int64 := eq_refl. Example of_zrange_int64' : int.of_zrange_relaxed r[-2^31 ~> 2^31] = int64 := eq_refl. Example of_zrange_uint32 : int.of_zrange_relaxed r[0 ~> 2^32-1] = uint32 := eq_refl. Example of_zrange_uint64 : int.of_zrange_relaxed r[0 ~> 2^32] = uint64 := eq_refl. Section ident. Import type. Inductive ident : type -> type -> Set := | literal (v : BinInt.Z) : ident unit Z | List_nth (n : Datatypes.nat) : ident Zptr Z | Addr : ident Z Zptr | Dereference : ident Zptr Z | Z_shiftr (offset : BinInt.Z) : ident Z Z | Z_shiftl (offset : BinInt.Z) : ident Z Z | Z_land : ident (Z * Z) Z | Z_lor : ident (Z * Z) Z | Z_add : ident (Z * Z) Z | Z_mul : ident (Z * Z) Z | Z_sub : ident (Z * Z) Z | Z_opp : ident Z Z | Z_lnot (ty:int.type) : ident Z Z | Z_bneg : ident Z Z | Z_mul_split (lgs:BinInt.Z) : ident ((Zptr * Zptr) * (Z * Z)) unit | Z_add_with_get_carry (lgs:BinInt.Z) : ident ((Zptr * Zptr) * (Z * Z * Z)) unit | Z_sub_with_get_borrow (lgs:BinInt.Z) : ident ((Zptr * Zptr) * (Z * Z * Z)) unit | Z_zselect (ty:int.type) : ident (Zptr * (Z * Z * Z)) unit | Z_add_modulo : ident (Z * Z * Z) Z | Z_static_cast (ty : int.type) : ident Z Z . End ident. Inductive arith_expr : type -> Set := | AppIdent {s d} (idc : ident s d) (arg : arith_expr s) : arith_expr d | Var (t : type.primitive) (v : string) : arith_expr t | Pair {A B} (a : arith_expr A) (b : arith_expr B) : arith_expr (A * B) | TT : arith_expr type.unit. Inductive stmt := | Call (val : arith_expr type.unit) | Assign (declare : bool) (t : type.primitive) (sz : option int.type) (name : string) (val : arith_expr t) | AssignZPtr (name : string) (sz : option int.type) (val : arith_expr type.Z) | DeclareVar (t : type.primitive) (sz : option int.type) (name : string) | AssignNth (name : string) (n : nat) (val : arith_expr type.Z). Definition expr := list stmt. Module Export Notations. Export int.Notations. Export type.Notations. Delimit Scope Cexpr_scope with Cexpr. Bind Scope Cexpr_scope with expr. Bind Scope Cexpr_scope with stmt. Bind Scope Cexpr_scope with arith_expr. Infix "@@" := AppIdent : Cexpr_scope. Notation "( x , y , .. , z )" := (Pair .. (Pair x%Cexpr y%Cexpr) .. z%Cexpr) : Cexpr_scope. Notation "( )" := TT : Cexpr_scope. Notation "()" := TT : Cexpr_scope. Notation "x ;; y" := (@cons stmt x%Cexpr y%Cexpr) (at level 70, right associativity, format "'[v' x ;; '/' y ']'") : Cexpr_scope. End Notations. Definition invert_literal {t} (e : arith_expr t) : option (BinInt.Z) := match e with | AppIdent s d (literal v) arg => Some v | _ => None end. Module OfPHOAS. Fixpoint base_var_data (t : base.type) : Set := match t with | base.type.unit => unit | base.type.nat | base.type.bool | base.type.zrange | base.type.option _ => Empty_set | base.type.Z => string * option int.type | base.type.prod A B => base_var_data A * base_var_data B | base.type.list A => string * option int.type * nat end. Definition var_data (t : Compilers.type.type base.type) : Set := match t with | type.base t => base_var_data t | type.arrow s d => Empty_set end. Fixpoint base_var_names (t : base.type) : Set := match t with | base.type.unit => unit | base.type.nat | base.type.bool | base.type.zrange | base.type.option _ => Empty_set | base.type.Z => string | base.type.prod A B => base_var_names A * base_var_names B | base.type.list A => string end. Definition var_names (t : Compilers.type.type base.type) : Set := match t with | type.base t => base_var_names t | type.arrow s d => Empty_set end. Fixpoint names_of_base_var_data {t} : base_var_data t -> base_var_names t := match t return base_var_data t -> base_var_names t with | base.type.unit | base.type.nat | base.type.bool | base.type.zrange | base.type.option _ => fun x => x | base.type.Z => @fst _ _ | base.type.prod A B => fun xy => (@names_of_base_var_data A (fst xy), @names_of_base_var_data B (snd xy)) | base.type.list A => fun x => fst (fst x) end. Definition names_of_var_data {t} : var_data t -> var_names t := match t with | type.base t => names_of_base_var_data | type.arrow _ _ => fun x => x end. Fixpoint arith_expr_for_base (t : base.type) : Set := match t with | base.type.Z => arith_expr type.Z * option int.type | base.type.prod A B => arith_expr_for_base A * arith_expr_for_base B | base.type.list A => list (arith_expr_for_base A) | base.type.option A => option (arith_expr_for_base A) | base.type.type_base _ as t => base.interp t end. Definition arith_expr_for (t : Compilers.type.type base.type) : Set := match t with | type.base t => arith_expr_for_base t | type.arrow s d => Empty_set end. (** Quoting http://en.cppreference.com/w/c/language/conversion: ** Integer promotions Integer promotion is the implicit conversion of a value of any integer type with rank less or equal to rank of int or of a bit field of type _Bool, int, signed int, unsigned int, to the value of type int or unsigned int If int can represent the entire range of values of the original type (or the range of values of the original bit field), the value is converted to type int. Otherwise the value is converted to unsigned int. *) (** We assume a 32-bit [int] type *) Definition integer_promote_type (t : int.type) : int.type := if int.is_tighter_than t int32 then int32 else t. (** Quoting http://en.cppreference.com/w/c/language/conversion: rank above is a property of every integer type and is defined as follows: 1) the ranks of all signed integer types are different and increase with their precision: rank of signed char < rank of short < rank of int < rank of long int < rank of long long int 2) the ranks of all signed integer types equal the ranks of the corresponding unsigned integer types 3) the rank of any standard integer type is greater than the rank of any extended integer type of the same size (that is, rank of __int64 < rank of long long int, but rank of long long < rank of __int128 due to the rule (1)) 4) rank of char equals rank of signed char and rank of unsigned char 5) the rank of _Bool is less than the rank of any other standard integer type 6) the rank of any enumerated type equals the rank of its compatible integer type 7) ranking is transitive: if rank of T1 < rank of T2 and rank of T2 < rank of T3 then rank of T1 < rank of T3 8) any aspects of relative ranking of extended integer types not covered above are implementation defined *) (** We define the rank to be the bitwidth, which satisfies (1), (2), (4), (5), and (7). Points (3) and (6) do not apply. *) Definition rank (r : int.type) : BinInt.Z := int.bitwidth_of r. Definition IMPOSSIBLE {T} (v : T) : T. exact v. Qed. (** Quoting http://en.cppreference.com/w/c/language/conversion: *) Definition common_type (t1 t2 : int.type) : int.type (** First of all, both operands undergo integer promotions (see below). Then *) := let t1 := integer_promote_type t1 in let t2 := integer_promote_type t2 in (** - If the types after promotion are the same, that type is the common type *) if int.type_beq t1 t2 then t1 (** - Otherwise, if both operands after promotion have the same signedness (both signed or both unsigned), the operand with the lesser conversion rank (see below) is implicitly converted to the type of the operand with the greater conversion rank *) else if bool_beq (int.is_signed t1) (int.is_signed t2) then (if rank t1 >=? rank t2 then t1 else t2) (** - Otherwise, the signedness is different: If the operand with the unsigned type has conversion rank greater or equal than the rank of the type of the signed operand, then the operand with the signed type is implicitly converted to the unsigned type *) else if int.is_unsigned t1 && (rank t1 >=? rank t2) then t1 else if int.is_unsigned t2 && (rank t2 >=? rank t1) then t2 (** - Otherwise, the signedness is different and the signed operand's rank is greater than unsigned operand's rank. In this case, if the signed type can represent all values of the unsigned type, then the operand with the unsigned type is implicitly converted to the type of the signed operand. *) else if int.is_signed t1 && int.is_tighter_than t2 t1 then t1 else if int.is_signed t2 && int.is_tighter_than t1 t2 then t2 (** - Otherwise, both operands undergo implicit conversion to the unsigned type counterpart of the signed operand's type. *) (** N.B. This case ought to be impossible in our code, where [rank] is the bitwidth. *) else if int.is_signed t1 then int.unsigned_counterpart_of t1 else int.unsigned_counterpart_of t2. Definition Zcast_down_if_needed : option int.type -> arith_expr_for_base base.type.Z -> arith_expr_for_base base.type.Z := fun desired_type '(e, known_type) => match desired_type, known_type with | None, _ => (e, known_type) | Some desired_type, Some known_type => if int.is_tighter_than known_type desired_type then (e, Some known_type) else (Z_static_cast desired_type @@ e, Some desired_type) | Some desired_type, None => (Z_static_cast desired_type @@ e, Some desired_type) end%core%Cexpr. Fixpoint cast_down_if_needed {t} : int.option.interp t -> arith_expr_for_base t -> arith_expr_for_base t := match t with | base.type.Z => Zcast_down_if_needed | base.type.type_base _ => fun _ x => x | base.type.prod A B => fun '(r1, r2) '(e1, e2) => (@cast_down_if_needed A r1 e1, @cast_down_if_needed B r2 e2) | base.type.list A => fun r1 ls => match r1 with | Some r1 => List.map (fun '(r, e) => @cast_down_if_needed A r e) (List.combine r1 ls) | None => ls end | base.type.option A => fun r1 ls => match r1 with | Some r1 => Option.map (fun '(r, e) => @cast_down_if_needed A r e) (Option.combine r1 ls) | None => ls end end. Definition Zcast_up_if_needed : option int.type -> arith_expr_for_base base.type.Z -> arith_expr_for_base base.type.Z := fun desired_type '(e, known_type) => match desired_type, known_type with | None, _ | _, None => (e, known_type) | Some desired_type, Some known_type => if int.is_tighter_than desired_type known_type then (e, Some known_type) else (Z_static_cast desired_type @@ e, Some desired_type)%core%Cexpr end. Fixpoint cast_up_if_needed {t} : int.option.interp t -> arith_expr_for_base t -> arith_expr_for_base t := match t with | base.type.Z => Zcast_up_if_needed | base.type.type_base _ => fun _ x => x | base.type.prod A B => fun '(r1, r2) '(e1, e2) => (@cast_up_if_needed A r1 e1, @cast_up_if_needed B r2 e2) | base.type.list A => fun r1 ls => match r1 with | Some r1 => List.map (fun '(r, e) => @cast_up_if_needed A r e) (List.combine r1 ls) | None => ls end | base.type.option A => fun r1 ls => match r1 with | Some r1 => Option.map (fun '(r, e) => @cast_up_if_needed A r e) (Option.combine r1 ls) | None => ls end end. Definition cast_bigger_up_if_needed (desired_type : option int.type) (args : arith_expr_for (base.type.Z * base.type.Z)) : arith_expr_for (base.type.Z * base.type.Z) := match desired_type with | None => args | Some _ => let '((e1, t1), (e2, t2)) := args in match t1, t2 with | None, _ | _, None => args | Some t1', Some t2' => if int.is_tighter_than t2' t1' then (Zcast_up_if_needed desired_type (e1, t1), (e2, t2)) else ((e1, t1), Zcast_up_if_needed desired_type (e2, t2)) end end. Definition arith_bin_arith_expr_of_PHOAS_ident (s:=(base.type.Z * base.type.Z)%etype) (d:=base.type.Z) (idc : ident (type.Z * type.Z) type.Z) : option int.type -> arith_expr_for s -> arith_expr_for d := fun desired_type '((e1, t1), (e2, t2)) => let t1 := option_map integer_promote_type t1 in let t2 := option_map integer_promote_type t2 in let '((e1, t1), (e2, t2)) := cast_bigger_up_if_needed desired_type ((e1, t1), (e2, t2)) in let ct := (t1 <- t1; t2 <- t2; Some (common_type t1 t2))%option in Zcast_down_if_needed desired_type ((idc @@ (e1, e2))%Cexpr, ct). Local Definition fakeprod (A B : Compilers.type.type base.type) : Compilers.type.type base.type := match A, B with | type.base A, type.base B => type.base (base.type.prod A B) | type.arrow _ _, _ | _, type.arrow _ _ => type.base (base.type.type_base base.type.unit) end. Definition arith_expr_for_uncurried_domain (t : Compilers.type.type base.type) := match t with | type.base t => unit | type.arrow s d => arith_expr_for (type.uncurried_domain fakeprod s d) end. Section with_bind. (* N.B. If we make the [bind*_err] notations, then Coq can't infer types correctly; if we make them [Local Definition]s or [Let]s, then [ocamlopt] fails with "Error: The type of this module, [...], contains type variables that cannot be generalized". We need to run [cbv] below to actually unfold them. >.< *) Local Notation ErrT T := (T + list string)%type. Local Notation ret v := (@inl _ (list string) v) (only parsing). Local Notation "x <- v ; f" := (match v with | inl x => f | inr err => inr err end). Reserved Notation "A1 ,, A2 <- X ; B" (at level 70, A2 at next level, right associativity, format "'[v' A1 ,, A2 <- X ; '/' B ']'"). Reserved Notation "A1 ,, A2 <- X1 , X2 ; B" (at level 70, A2 at next level, right associativity, format "'[v' A1 ,, A2 <- X1 , X2 ; '/' B ']'"). Reserved Notation "A1 ,, A2 ,, A3 <- X ; B" (at level 70, A2 at next level, A3 at next level, right associativity, format "'[v' A1 ,, A2 ,, A3 <- X ; '/' B ']'"). Reserved Notation "A1 ,, A2 ,, A3 <- X1 , X2 , X3 ; B" (at level 70, A2 at next level, A3 at next level, right associativity, format "'[v' A1 ,, A2 ,, A3 <- X1 , X2 , X3 ; '/' B ']'"). Reserved Notation "A1 ,, A2 ,, A3 ,, A4 <- X ; B" (at level 70, A2 at next level, A3 at next level, A4 at next level, right associativity, format "'[v' A1 ,, A2 ,, A3 ,, A4 <- X ; '/' B ']'"). Reserved Notation "A1 ,, A2 ,, A3 ,, A4 <- X1 , X2 , X3 , X4 ; B" (at level 70, A2 at next level, A3 at next level, A4 at next level, right associativity, format "'[v' A1 ,, A2 ,, A3 ,, A4 <- X1 , X2 , X3 , X4 ; '/' B ']'"). Reserved Notation "A1 ,, A2 ,, A3 ,, A4 ,, A5 <- X ; B" (at level 70, A2 at next level, A3 at next level, A4 at next level, A5 at next level, right associativity, format "'[v' A1 ,, A2 ,, A3 ,, A4 ,, A5 <- X ; '/' B ']'"). Reserved Notation "A1 ,, A2 ,, A3 ,, A4 ,, A5 <- X1 , X2 , X3 , X4 , X5 ; B" (at level 70, A2 at next level, A3 at next level, A4 at next level, A5 at next level, right associativity, format "'[v' A1 ,, A2 ,, A3 ,, A4 ,, A5 <- X1 , X2 , X3 , X4 , X5 ; '/' B ']'"). Let bind2_err {A B C} (v1 : ErrT A) (v2 : ErrT B) (f : A -> B -> ErrT C) : ErrT C := match v1, v2 with | inl x1, inl x2 => f x1 x2 | inr err, inl _ | inl _, inr err => inr err | inr err1, inr err2 => inr (List.app err1 err2) end. Local Notation "x1 ,, x2 <- v1 , v2 ; f" := (bind2_err v1 v2 (fun x1 x2 => f)). Local Notation "x1 ,, x2 <- v ; f" := (x1 ,, x2 <- fst v , snd v; f). Let bind3_err {A B C R} (v1 : ErrT A) (v2 : ErrT B) (v3 : ErrT C) (f : A -> B -> C -> ErrT R) : ErrT R := (x12 ,, x3 <- (x1 ,, x2 <- v1, v2; inl (x1, x2)), v3; let '(x1, x2) := x12 in f x1 x2 x3). Local Notation "x1 ,, x2 ,, x3 <- v1 , v2 , v3 ; f" := (bind3_err v1 v2 v3 (fun x1 x2 x3 => f)). Local Notation "x1 ,, x2 ,, x3 <- v ; f" := (let '(v1, v2, v3) := v in x1 ,, x2 ,, x3 <- v1 , v2 , v3; f). Let bind4_err {A B C D R} (v1 : ErrT A) (v2 : ErrT B) (v3 : ErrT C) (v4 : ErrT D) (f : A -> B -> C -> D -> ErrT R) : ErrT R := (x12 ,, x34 <- (x1 ,, x2 <- v1, v2; inl (x1, x2)), (x3 ,, x4 <- v3, v4; inl (x3, x4)); let '((x1, x2), (x3, x4)) := (x12, x34) in f x1 x2 x3 x4). Local Notation "x1 ,, x2 ,, x3 ,, x4 <- v1 , v2 , v3 , v4 ; f" := (bind4_err v1 v2 v3 v4 (fun x1 x2 x3 x4 => f)). Local Notation "x1 ,, x2 ,, x3 ,, x4 <- v ; f" := (let '(v1, v2, v3, v4) := v in x1 ,, x2 ,, x3 ,, x4 <- v1 , v2 , v3 , v4; f). Let bind5_err {A B C D E R} (v1 : ErrT A) (v2 : ErrT B) (v3 : ErrT C) (v4 : ErrT D) (v5 : ErrT E) (f : A -> B -> C -> D -> E -> ErrT R) : ErrT R := (x12 ,, x345 <- (x1 ,, x2 <- v1, v2; inl (x1, x2)), (x3 ,, x4 ,, x5 <- v3, v4, v5; inl (x3, x4, x5)); let '((x1, x2), (x3, x4, x5)) := (x12, x345) in f x1 x2 x3 x4 x5). Local Notation "x1 ,, x2 ,, x3 ,, x4 ,, x5 <- v1 , v2 , v3 , v4 , v5 ; f" := (bind5_err v1 v2 v3 v4 v5 (fun x1 x2 x3 x4 x5 => f)). Local Notation "x1 ,, x2 ,, x3 ,, x4 ,, x5 <- v ; f" := (let '(v1, v2, v3, v4, v5) := v in x1 ,, x2 ,, x3 ,, x4 ,, x5 <- v1 , v2 , v3 , v4 , v5; f). Definition maybe_log2 (s : Z) : option Z := if 2^Z.log2 s =? s then Some (Z.log2 s) else None. Definition maybe_loglog2 (s : Z) : option nat := (v <- maybe_log2 s; v <- maybe_log2 v; if Z.leb 0 v then Some (Z.to_nat v) else None). Definition arith_expr_of_PHOAS_ident {t} (idc : ident.ident t) : int.option.interp (type.final_codomain t) -> type.interpM_final (fun T => ErrT T) arith_expr_for_base t := match idc in ident.ident t return int.option.interp (type.final_codomain t) -> type.interpM_final (fun T => ErrT T) arith_expr_for_base t with | ident.Literal base.type.Z v => fun r => ret (cast_down_if_needed r (literal v @@ TT, Some (int.of_zrange_relaxed r[v~>v]))) | ident.nil t => fun _ => ret nil | ident.cons t => fun r x xs => ret (cast_down_if_needed r (cons x xs)) | ident.fst A B => fun r xy => ret (cast_down_if_needed r (@fst _ _ xy)) | ident.snd A B => fun r xy => ret (cast_down_if_needed r (@snd _ _ xy)) | ident.List_nth_default base.type.Z => fun r d ls n => List.nth_default (inr ["Invalid list index " ++ show false n]%string) (List.map (fun x => ret (cast_down_if_needed r x)) ls) n | ident.Z_shiftr => fun rout '(e, r) '(offset, roffset) => let rin := option_map integer_promote_type r in match invert_literal offset with | Some offset => (** N.B. We must cast the expression up to a large enough type to fit 2^offset (importantly, not just 2^offset-1), because C considers it to be undefined behavior to shift >= width of the type. We should probably figure out how to not generate these things in the first place... N.B. We must preserve signedness of the value being shifted, because shift does not commute with mod. *) let '(e', rin') := Zcast_up_if_needed (option_map (int.union_zrange r[0~>2^offset]%zrange) rin) (e, rin) in ret (cast_down_if_needed rout (Z_shiftr offset @@ e', rin')) | None => inr ["Invalid right-shift by a non-literal"]%string end | ident.Z_shiftl => fun rout '(e, r) '(offset, roffset) => let rin := option_map integer_promote_type r in match invert_literal offset with | Some offset => (** N.B. We must cast the expression up to a large enough type to fit 2^offset (importantly, not just 2^offset-1), because C considers it to be undefined behavior to shift >= width of the type. We should probably figure out how to not generate these things in the first place... N.B. We make sure that we only left-shift unsigned values, since shifting into the sign bit is undefined behavior. *) let rpre_out := match rout with | Some rout => Some (int.union_zrange r[0~>2^offset] (int.unsigned_counterpart_of rout)) | None => Some (int.of_zrange_relaxed r[0~>2^offset]%zrange) end in let '(e', rin') := Zcast_up_if_needed rpre_out (e, rin) in ret (cast_down_if_needed rout (Z_shiftl offset @@ e', rin')) | None => inr ["Invalid left-shift by a non-literal"]%string end | ident.Z_bneg => fun rout '(e, r) => (** N.B. We assume that C will implicitly cast the output of [!e] to whatever integer type it wants it in *) ret (Z_bneg @@ e, rout) | ident.Z_land => fun r x y => ret (arith_bin_arith_expr_of_PHOAS_ident Z_land r (x, y)) | ident.Z_lor => fun r x y => ret (arith_bin_arith_expr_of_PHOAS_ident Z_lor r (x, y)) | ident.Z_add => fun r x y => ret (arith_bin_arith_expr_of_PHOAS_ident Z_add r (x, y)) | ident.Z_mul => fun r x y => ret (arith_bin_arith_expr_of_PHOAS_ident Z_mul r (x, y)) | ident.Z_sub => fun r x y => ret (arith_bin_arith_expr_of_PHOAS_ident Z_sub r (x, y)) | ident.Z_lnot_modulo => fun rout '(e, r) '(modulus, _) => let rin := option_map integer_promote_type r in match invert_literal modulus with | Some modulus => match maybe_loglog2 modulus with | Some lgbitwidth => let ty := int.unsigned lgbitwidth in let rin' := Some ty in let '(e, _) := Zcast_up_if_needed rin' (e, r) in ret (cast_down_if_needed rout (cast_up_if_needed rout (Z_lnot ty @@ e, rin'))) | None => inr ["Invalid modulus for Z.lnot (not 2^(2^_)): " ++ show false modulus]%string end | None => inr ["Invalid non-literal modulus for Z.lnot"]%string end | ident.pair A B => fun _ _ _ => inr ["Invalid identifier in arithmetic expression " ++ show true idc]%string | ident.Z_opp (* we pretend this is [0 - _] *) => fun r y => let zero := (literal 0 @@ TT, Some (int.of_zrange_relaxed r[0~>0])) in ret (arith_bin_arith_expr_of_PHOAS_ident Z_sub r (zero, y)) | ident.Literal _ v => fun _ => ret v | ident.Nat_succ | ident.Nat_pred | ident.Nat_max | ident.Nat_mul | ident.Nat_add | ident.Nat_sub | ident.Nat_eqb | ident.prod_rect _ _ _ | ident.bool_rect _ | ident.nat_rect _ | ident.eager_nat_rect _ | ident.nat_rect_arrow _ _ | ident.eager_nat_rect_arrow _ _ | ident.Some _ | ident.None _ | ident.option_rect _ _ | ident.list_rect _ _ | ident.eager_list_rect _ _ | ident.list_rect_arrow _ _ _ | ident.eager_list_rect_arrow _ _ _ | ident.list_case _ _ | ident.List_length _ | ident.List_seq | ident.List_repeat _ | ident.List_firstn _ | ident.List_skipn _ | ident.List_combine _ _ | ident.List_map _ _ | ident.List_app _ | ident.List_rev _ | ident.List_flat_map _ _ | ident.List_partition _ | ident.List_fold_right _ _ | ident.List_update_nth _ | ident.List_nth_default _ | ident.eager_List_nth_default _ | ident.Z_pow | ident.Z_div | ident.Z_modulo | ident.Z_eqb | ident.Z_leb | ident.Z_ltb | ident.Z_geb | ident.Z_gtb | ident.Z_min | ident.Z_max | ident.Z_log2 | ident.Z_log2_up | ident.Z_of_nat | ident.Z_to_nat | ident.Z_zselect | ident.Z_mul_split | ident.Z_add_get_carry | ident.Z_add_with_carry | ident.Z_add_with_get_carry | ident.Z_sub_get_borrow | ident.Z_sub_with_get_borrow | ident.Z_add_modulo | ident.Z_rshi | ident.Z_cc_m | ident.Z_combine_at_bitwidth | ident.Z_cast _ | ident.Z_cast2 _ | ident.Build_zrange | ident.zrange_rect _ | ident.fancy_add _ _ | ident.fancy_addc _ _ | ident.fancy_sub _ _ | ident.fancy_subb _ _ | ident.fancy_mulll _ | ident.fancy_mullh _ | ident.fancy_mulhl _ | ident.fancy_mulhh _ | ident.fancy_rshi _ _ | ident.fancy_selc | ident.fancy_selm _ | ident.fancy_sell | ident.fancy_addm => fun _ => type.interpM_return _ _ _ (inr ["Invalid identifier in arithmetic expression " ++ show true idc]%string) end%core%Cexpr%option%zrange. Fixpoint collect_args_and_apply_unknown_casts {t} : (int.option.interp (type.final_codomain t) -> type.interpM_final (fun T => ErrT T) arith_expr_for_base t) -> type.interpM_final (fun T => ErrT T) (fun t => int.option.interp t -> ErrT (arith_expr_for_base t)) t := match t return ((int.option.interp (type.final_codomain t) -> type.interpM_final (fun T => ErrT T) arith_expr_for_base t) -> type.interpM_final (fun T => ErrT T) (fun t => int.option.interp t -> ErrT (arith_expr_for_base t)) t) with | type.base t => fun v => ret v | type.arrow (type.base s) d => fun f (x : (int.option.interp s -> ErrT (arith_expr_for_base s))) => match x int.option.None return _ with | inl x' => @collect_args_and_apply_unknown_casts d (fun rout => f rout x') | inr errs => type.interpM_return _ _ _ (inr errs) end | type.arrow (type.arrow _ _) _ => fun _ => type.interpM_return _ _ _ (inr ["Invalid higher-order function"]) end. Definition collect_args_and_apply_known_casts {t} (idc : ident.ident t) : ErrT (type.interpM_final (fun T => ErrT T) (fun t => int.option.interp t -> ErrT (arith_expr_for_base t)) t) := match idc in ident.ident t return ErrT (type.interpM_final (fun T => ErrT T) (fun t => int.option.interp t -> ErrT (arith_expr_for_base t)) t) with | ident.Z_cast r => inl (fun arg => inl (fun r' => arg <- arg (Some (int.of_zrange_relaxed r)); ret (Zcast_down_if_needed r' arg))) | ident.Z_cast2 (r1, r2) => inl (fun arg => inl (fun r' => arg <- (arg (Some (int.of_zrange_relaxed r1), Some (int.of_zrange_relaxed r2))); ret (cast_down_if_needed (t:=base.type.Z*base.type.Z) r' arg))) | ident.pair A B => inl (fun ea eb => inl (fun '(ra, rb) => ea' ,, eb' <- ea ra, eb rb; inl (ea', eb'))) | ident.nil _ => inl (inl (fun _ => inl nil)) | ident.cons t => inl (fun x xs => inl (fun rls => let mkcons (r : int.option.interp t) (rs : int.option.interp (base.type.list t)) := x ,, xs <- x r, xs rs; inl (cons x xs) in match rls with | Some (cons r rs) => mkcons r (Some rs) | Some nil | None => mkcons int.option.None int.option.None end)) | _ => inr ["Invalid identifier where cast or constructor was expected: " ++ show false idc]%string end. Definition collect_args_and_apply_casts {t} (idc : ident.ident t) (convert_no_cast : int.option.interp (type.final_codomain t) -> type.interpM_final (fun T => ErrT T) arith_expr_for_base t) : type.interpM_final (fun T => ErrT T) (fun t => int.option.interp t -> ErrT (arith_expr_for_base t)) t := match collect_args_and_apply_known_casts idc with | inl res => res | inr errs => collect_args_and_apply_unknown_casts convert_no_cast end. Fixpoint arith_expr_of_base_PHOAS_Var {t} : base_var_data t -> int.option.interp t -> ErrT (arith_expr_for_base t) := match t with | base.type.Z => fun '(n, r) r' => ret (cast_down_if_needed r' (Var type.Z n, r)) | base.type.prod A B => fun '(da, db) '(ra, rb) => (ea,, eb <- @arith_expr_of_base_PHOAS_Var A da ra, @arith_expr_of_base_PHOAS_Var B db rb; inl (ea, eb)) | base.type.list base.type.Z => fun '(n, r, len) r' => ret (List.map (fun i => (List_nth i @@ Var type.Zptr n, r))%core%Cexpr (List.seq 0 len)) | base.type.list _ | base.type.option _ | base.type.type_base _ => fun _ _ => inr ["Invalid type " ++ show false t]%string end. Fixpoint arith_expr_of_PHOAS {t} (e : @Compilers.expr.expr base.type ident.ident var_data t) : type.interpM_final (fun T => ErrT T) (fun t => int.option.interp t -> ErrT (arith_expr_for_base t)) t := match e in expr.expr t return type.interpM_final (fun T => ErrT T) (fun t => int.option.interp t -> ErrT (arith_expr_for_base t)) t with | expr.Var (type.base _) v => ret (arith_expr_of_base_PHOAS_Var v) | expr.Ident t idc => collect_args_and_apply_casts idc (arith_expr_of_PHOAS_ident idc) | expr.App (type.base s) d f x => let x' := @arith_expr_of_PHOAS s x in match x' with | inl x' => @arith_expr_of_PHOAS _ f x' | inr errs => type.interpM_return _ _ _ (inr errs) end | expr.Var (type.arrow _ _) _ => type.interpM_return _ _ _ (inr ["Invalid non-arithmetic let-bound Var of type " ++ show false t]%string) | expr.App (type.arrow _ _) _ _ _ => type.interpM_return _ _ _ (inr ["Invalid non-arithmetic let-bound App of type " ++ show false t]%string) | expr.LetIn _ _ _ _ => type.interpM_return _ _ _ (inr ["Invalid non-arithmetic let-bound LetIn of type " ++ show false t]%string) | expr.Abs _ _ _ => type.interpM_return _ _ _ (inr ["Invalid non-arithmetic let-bound Abs of type: " ++ show false t]%string) end. Definition arith_expr_of_base_PHOAS {t:base.type} (e : @Compilers.expr.expr base.type ident.ident var_data t) (rout : int.option.interp t) : ErrT (arith_expr_for_base t) := (e' <- arith_expr_of_PHOAS e; e' rout). Fixpoint make_return_assignment_of_base_arith {t} : base_var_data t -> @Compilers.expr.expr base.type ident.ident var_data t -> ErrT expr := match t return base_var_data t -> expr.expr t -> ErrT expr with | base.type.Z => fun '(n, r) e => (rhs <- arith_expr_of_base_PHOAS e r; let '(e, r) := rhs in ret [AssignZPtr n r e]) | base.type.type_base _ => fun _ _ => inr ["Invalid type " ++ show false t]%string | base.type.prod A B => fun '(rva, rvb) e => match invert_pair e with | Some (ea, eb) => ea',, eb' <- @make_return_assignment_of_base_arith A rva ea, @make_return_assignment_of_base_arith B rvb eb; ret (ea' ++ eb') | None => inr ["Invalid non-pair expr of type " ++ show false t]%string end | base.type.list base.type.Z => fun '(n, r, len) e => (ls <- arith_expr_of_base_PHOAS e (Some (repeat r len)); ret (List.map (fun '(i, (e, _)) => AssignNth n i e) (List.combine (List.seq 0 len) ls))) | base.type.list _ | base.type.option _ => fun _ _ => inr ["Invalid type of expr: " ++ show false t]%string end%list. Definition make_return_assignment_of_arith {t} : var_data t -> @Compilers.expr.expr base.type ident.ident var_data t -> ErrT expr := match t with | type.base t => make_return_assignment_of_base_arith | type.arrow s d => fun _ _ => inr ["Invalid type of expr: " ++ show false t]%string end. Definition report_type_mismatch (expected : defaults.type) (given : defaults.type) : string := ("Type mismatch; expected " ++ show false expected ++ " but given " ++ show false given ++ ".")%string. Fixpoint arith_expr_of_PHOAS_args {t} : type.for_each_lhs_of_arrow (@Compilers.expr.expr base.type ident.ident var_data) t -> ErrT (type.for_each_lhs_of_arrow (fun t => @Compilers.expr.expr base.type ident.ident var_data t * (arith_expr type.Z * option int.type)) t) := match t with | type.base t => fun 'tt => inl tt | type.arrow (type.base base.type.Z) d => fun '(arg, args) => arg' ,, args' <- arith_expr_of_base_PHOAS arg int.option.None , @arith_expr_of_PHOAS_args d args; inl ((arg, arg'), args') | type.arrow s d => fun '(arg, args) => arg' ,, args' <- @inr unit _ ["Invalid argument of non-ℤ type " ++ show false s]%string , @arith_expr_of_PHOAS_args d args; inr ["Impossible! (type error got lost somewhere)"] end. Let recognize_1ref_ident {t} (idc : ident.ident t) (rout : option int.type) : type.for_each_lhs_of_arrow (fun t => @Compilers.expr.expr base.type ident.ident var_data t * (arith_expr type.Z * option int.type))%type t -> ErrT (arith_expr type.Zptr -> expr) := let _ := @PHOAS.expr.partially_show_expr in match idc with | ident.Z_zselect => fun '((econdv, (econd, rcond)), ((e1v, (e1, r1)), ((e2v, (e2, r2)), tt))) => match rcond with | Some (int.unsigned 0) => let r1 := option_map integer_promote_type r1 in let r2 := option_map integer_promote_type r2 in let '((e1, r1), (e2, r2)) := cast_bigger_up_if_needed rout ((e1, r1), (e2, r2)) in let ct := (r1 <- r1; r2 <- r2; Some (common_type r1 r2))%option in ty <- match ct, rout with | Some ct, Some rout => if int.type_beq ct rout then inl ct else inr ["Casting the result of Z.zselect to a type other than the common type is not currently supported. (Cannot cast a pointer to " ++ show false rout ++ " to a pointer to " ++ show false ct ++ ".)"]%string | None, _ => inr ["Unexpected None result of common-type calculation for Z.zselect"] | _, None => inr ["Missing cast annotation on return of Z.zselect"] end; ret (fun retptr => [Call (Z_zselect ty @@ (retptr, (econd, e1, e2)))]%Cexpr) | _ => inr ["Invalid argument to Z.zselect not known to be 0 or 1: " ++ show false econdv]%string end | _ => fun _ => inr ["Unrecognized identifier (expecting a 1-pointer-returning function): " ++ show false idc]%string end. Definition bounds_check (do_bounds_check : bool) (descr : string) {t} (idc : ident.ident t) (s : BinInt.Z) {t'} (ev : @Compilers.expr.expr base.type ident.ident var_data t') (found : option int.type) : ErrT unit := if negb do_bounds_check then ret tt else let _ := @PHOAS.expr.partially_show_expr in match found with | None => inr ["Missing range on " ++ descr ++ " " ++ show true idc ++ ": " ++ show true ev]%string | Some ty => if int.is_tighter_than ty (int.of_zrange_relaxed r[0~>2^s-1]) then ret tt else inr ["Final bounds check failed on " ++ descr ++ " " ++ show false idc ++ "; expected an unsigned " ++ decimal_string_of_Z s ++ "-bit number (" ++ show false (int.of_zrange_relaxed r[0~>2^s-1]) ++ "), but found a " ++ show false ty ++ "."]%string end. Let round_up_to_split_type (lgs : Z) (t : option int.type) : option int.type := option_map (int.union (int.of_zrange_relaxed r[0~>2^lgs-1])) t. Let recognize_3arg_2ref_ident (do_bounds_check : bool) (t:=(base.type.Z -> base.type.Z -> base.type.Z -> base.type.Z * base.type.Z)%etype) (idc : ident.ident t) (rout : option int.type * option int.type) (args : type.for_each_lhs_of_arrow (fun t => @Compilers.expr.expr base.type ident.ident var_data t * (arith_expr type.Z * option int.type))%type t) : ErrT ((option int.type * option int.type) * (arith_expr (type.Zptr * type.Zptr) -> expr)) := let _ := @PHOAS.expr.partially_show_expr in let '((s, _), ((e1v, (e1, r1)), ((e2v, (e2, r2)), tt))) := args in match (s <- invert_Literal s; maybe_log2 s)%option, idc return ErrT ((option int.type * option int.type) * (arith_expr (type.Zptr * type.Zptr) -> expr)) with | Some s, ident.Z_mul_split => (_ ,, _ ,, _ ,, _ <- bounds_check do_bounds_check "first argument to" idc s e1v r1, bounds_check do_bounds_check "second argument to" idc s e2v r2, bounds_check do_bounds_check "first return value of" idc s e2v (fst rout), bounds_check do_bounds_check "second return value of" idc s e2v (snd rout); inl ((round_up_to_split_type s (fst rout), round_up_to_split_type s (snd rout)), fun retptr => [Call (Z_mul_split s @@ (retptr, (e1, e2)))%Cexpr])) | Some s, ident.Z_add_get_carry as idc | Some s, ident.Z_sub_get_borrow as idc => let idc' : ident _ _ := Option.invert_Some match idc with | ident.Z_add_get_carry => Some (Z_add_with_get_carry s) | ident.Z_sub_get_borrow => Some (Z_sub_with_get_borrow s) | _ => None end in (_ ,, _ ,, _ ,, _ <- bounds_check do_bounds_check "first argument to" idc s e1v r1, bounds_check do_bounds_check "second argument to" idc s e2v r2, bounds_check do_bounds_check "first return value of" idc s e2v (fst rout), bounds_check do_bounds_check "second return value of" idc 1 (* boolean carry/borrow *) e2v (snd rout); inl ((round_up_to_split_type s (fst rout), snd rout), fun retptr => [Call (idc' @@ (retptr, (literal 0 @@ TT, e1, e2)))%Cexpr])) | Some _, _ => inr ["Unrecognized identifier when attempting to construct an assignment with 2 arguments: " ++ show true idc]%string | None, _ => inr ["Expression is not a literal power of two of type ℤ: " ++ show true s ++ " (when trying to parse the first argument of " ++ show true idc ++ ")"]%string end. Let recognize_4arg_2ref_ident (do_bounds_check : bool) (t:=(base.type.Z -> base.type.Z -> base.type.Z -> base.type.Z -> base.type.Z * base.type.Z)%etype) (idc : ident.ident t) (rout : option int.type * option int.type) (args : type.for_each_lhs_of_arrow (fun t => @Compilers.expr.expr base.type ident.ident var_data t * (arith_expr type.Z * option int.type))%type t) : ErrT ((option int.type * option int.type) * (arith_expr (type.Zptr * type.Zptr) -> expr)) := let _ := @PHOAS.expr.partially_show_expr in let '((s, _), ((e1v, (e1, r1)), ((e2v, (e2, r2)), ((e3v, (e3, r3)), tt)))) := args in match (s <- invert_Literal s; maybe_log2 s)%option, idc return ErrT ((option int.type * option int.type) * (arith_expr (type.Zptr * type.Zptr) -> expr)) with | Some s, ident.Z_add_with_get_carry as idc | Some s, ident.Z_sub_with_get_borrow as idc => let idc' : ident _ _ := Option.invert_Some match idc with | ident.Z_add_with_get_carry => Some (Z_add_with_get_carry s) | ident.Z_sub_with_get_borrow => Some (Z_sub_with_get_borrow s) | _ => None end in (_ ,, _ ,, _ ,, _ ,, _ <- (bounds_check do_bounds_check "first (carry) argument to" idc 1 e1v r1, bounds_check do_bounds_check "second argument to" idc s e2v r2, bounds_check do_bounds_check "third argument to" idc s e2v r2, bounds_check do_bounds_check "first return value of" idc s e2v (fst rout), bounds_check do_bounds_check "second (carry) return value of" idc 1 (* boolean carry/borrow *) e2v (snd rout)); inl ((round_up_to_split_type s (fst rout), snd rout), fun retptr => [Call (idc' @@ (retptr, (e1, e2, e3)))%Cexpr])) | Some _, _ => inr ["Unrecognized identifier when attempting to construct an assignment with 2 arguments: " ++ show true idc]%string | None, _ => inr ["Expression is not a literal power of two of type ℤ: " ++ show true s ++ " (when trying to parse the first argument of " ++ show true idc ++ ")"]%string end. Let recognize_2ref_ident {t} : forall (do_bounds_check : bool) (idc : ident.ident t) (rout : option int.type * option int.type) (args : type.for_each_lhs_of_arrow (fun t => @Compilers.expr.expr base.type ident.ident var_data t * (arith_expr type.Z * option int.type))%type t), ErrT ((option int.type * option int.type) * (arith_expr (type.Zptr * type.Zptr) -> expr)) := match t with | (type.base base.type.Z -> type.base base.type.Z -> type.base base.type.Z -> type.base (base.type.Z * base.type.Z))%etype => recognize_3arg_2ref_ident | (type.base base.type.Z -> type.base base.type.Z -> type.base base.type.Z -> type.base base.type.Z -> type.base (base.type.Z * base.type.Z))%etype => recognize_4arg_2ref_ident | _ => fun do_bounds_check idc rout args => inr ["Unrecognized type for function call: " ++ show false t ++ " (when trying to handle the identifer " ++ show false idc ++ ")"]%string end. Definition declare_name (descr : string) (count : positive) (make_name : positive -> option string) (r : option int.type) : ErrT (expr * string * arith_expr type.Zptr) := (n ,, r <- (match make_name count with | Some n => ret n | None => inr ["Variable naming-function does not support the index " ++ show false count]%string end, match r with | Some r => ret r | None => inr ["Missing return type annotation for " ++ descr]%string end); ret ([DeclareVar type.Z (Some r) n], n, (Addr @@ Var type.Z n)%Cexpr)). Let make_assign_arg_1ref_opt (e : @Compilers.expr.expr base.type ident.ident var_data base.type.Z) (count : positive) (make_name : positive -> option string) : ErrT (expr * var_data base.type.Z) := let _ := @PHOAS.expr.partially_show_expr in let e1 := e in let '(rout, e) := match invert_Z_cast e with | Some (r, e) => (Some (int.of_zrange_relaxed r), e) | None => (None, e) end%core in let res_ref := match invert_AppIdent_curried e with | Some (existT _ (idc, args)) => args <- arith_expr_of_PHOAS_args args; idce <- recognize_1ref_ident idc rout args; v <- declare_name (show false idc) count make_name rout; let '(decls, n, retv) := v in ret ((decls ++ (idce retv))%list, (n, rout)) | None => inr ["Invalid assignment of non-identifier-application: " ++ show false e]%string end in match res_ref with | inl res => ret res | inr _ => e1 <- arith_expr_of_base_PHOAS e1 None; let '(e1, r1) := e1 in match make_name count with | Some n1 => ret ([Assign true type.Z r1 n1 e1], (n1, r1)) | None => inr ["Variable naming-function does not support the index " ++ show false count]%string end end. Let make_assign_arg_2ref (do_bounds_check : bool) (e : @Compilers.expr.expr base.type ident.ident var_data (base.type.Z * base.type.Z)) (count : positive) (make_name : positive -> option string) : ErrT (expr * var_data (base.type.Z * base.type.Z)) := let _ := @PHOAS.expr.partially_show_expr in let '((rout1, rout2), e) := match invert_Z_cast2 e with | Some ((r1, r2), e) => ((Some (int.of_zrange_relaxed r1), Some (int.of_zrange_relaxed r2)), e) | None => ((None, None), e) end%core in match invert_AppIdent_curried e with | Some (existT t (idc, args)) => args <- arith_expr_of_PHOAS_args args; idce <- recognize_2ref_ident do_bounds_check idc (rout1, rout2) args; let '((rout1, rout2), idce) := idce in v1,, v2 <- (declare_name (show false idc) count make_name rout1, declare_name (show false idc) (Pos.succ count) make_name rout2); let '(decls1, n1, retv1) := v1 in let '(decls2, n2, retv2) := v2 in ret (decls1 ++ decls2 ++ (idce (retv1, retv2)%Cexpr), ((n1, rout1), (n2, rout2)))%list | None => inr ["Invalid assignment of non-identifier-application: " ++ show false e]%string end. Let make_assign_arg_ref (do_bounds_check : bool) {t} : forall (e : @Compilers.expr.expr base.type ident.ident var_data t) (count : positive) (make_name : positive -> option string), ErrT (expr * var_data t) := let _ := @PHOAS.expr.partially_show_expr in match t with | type.base base.type.Z => make_assign_arg_1ref_opt | type.base (base.type.Z * base.type.Z)%etype => make_assign_arg_2ref do_bounds_check | _ => fun e _ _ => inr ["Invalid type of assignment expression: " ++ show false t ++ " (with expression " ++ show true e ++ ")"] end. Fixpoint size_of_type (t : base.type) : positive := match t with | base.type.type_base t => 1 | base.type.prod A B => size_of_type A + size_of_type B | base.type.list A => 1 | base.type.option A => 1 end%positive. Let make_uniform_assign_expr_of_PHOAS (do_bounds_check : bool) {s} (e1 : @Compilers.expr.expr base.type ident.ident var_data s) {d} (e2 : var_data s -> var_data d -> ErrT expr) (count : positive) (make_name : positive -> option string) (vd : var_data d) : ErrT expr := let _ := @PHOAS.expr.partially_show_expr in (* for TC resolution *) e1_vs <- make_assign_arg_ref do_bounds_check e1 count make_name; let '(e1, vs) := e1_vs in e2 <- e2 vs vd; ret (e1 ++ e2)%list. (* See above comment about extraction issues *) Definition make_assign_expr_of_PHOAS (do_bounds_check : bool) {s} (e1 : @Compilers.expr.expr base.type ident.ident var_data s) {s' d} (e2 : var_data s' -> var_data d -> ErrT expr) (count : positive) (make_name : positive -> option string) (v : var_data d) : ErrT expr := Eval cbv beta iota delta [bind2_err bind3_err bind4_err bind5_err recognize_1ref_ident recognize_3arg_2ref_ident recognize_4arg_2ref_ident recognize_2ref_ident make_assign_arg_1ref_opt make_assign_arg_2ref make_assign_arg_ref make_uniform_assign_expr_of_PHOAS make_uniform_assign_expr_of_PHOAS round_up_to_split_type] in match type.try_transport base.try_make_transport_cps _ _ s' e1 with | Some e1 => make_uniform_assign_expr_of_PHOAS do_bounds_check e1 e2 count make_name v | None => inr [report_type_mismatch s' s] end. Fixpoint expr_of_base_PHOAS (do_bounds_check : bool) {t} (e : @Compilers.expr.expr base.type ident.ident var_data t) (count : positive) (make_name : positive -> option string) {struct e} : forall (ret_val : var_data t), ErrT expr := match e in expr.expr t return var_data t -> ErrT expr with | expr.LetIn (type.base s) d e1 e2 => make_assign_expr_of_PHOAS do_bounds_check e1 (fun vs vd => @expr_of_base_PHOAS do_bounds_check d (e2 vs) (size_of_type s + count)%positive make_name vd) count make_name | expr.LetIn (type.arrow _ _) _ _ _ as e | expr.Var _ _ as e | expr.Ident _ _ as e | expr.App _ _ _ _ as e | expr.Abs _ _ _ as e => fun v => make_return_assignment_of_arith v e end%expr_pat%option. Fixpoint base_var_data_of_bounds {t} (count : positive) (make_name : positive -> option string) {struct t} : ZRange.type.base.option.interp t -> option (positive * var_data t) := match t return ZRange.type.base.option.interp t -> option (positive * var_data t) with | base.type.Z => fun r => (n <- make_name count; Some (Pos.succ count, (n, option_map int.of_zrange_relaxed r))) | base.type.prod A B => fun '(ra, rb) => (va <- @base_var_data_of_bounds A count make_name ra; let '(count, va) := va in vb <- @base_var_data_of_bounds B count make_name rb; let '(count, vb) := vb in Some (count, (va, vb))) | base.type.list base.type.Z => fun r => (ls <- r; n <- make_name count; Some (Pos.succ count, (n, match List.map (option_map int.of_zrange_relaxed) ls with | nil => None | cons x xs => List.fold_right (fun r1 r2 => r1 <- r1; r2 <- r2; Some (int.union r1 r2)) x xs end, length ls))) | base.type.unit => fun _ => Some (count, tt) | base.type.list _ | base.type.option _ | base.type.type_base _ => fun _ => None end%option. Definition var_data_of_bounds {t} (count : positive) (make_name : positive -> option string) : ZRange.type.option.interp t -> option (positive * var_data t) := match t with | type.base t => base_var_data_of_bounds count make_name | type.arrow s d => fun _ => None end. Fixpoint expr_of_PHOAS' (do_bounds_check : bool) {t} (e : @Compilers.expr.expr base.type ident.ident var_data t) (make_in_name : positive -> option string) (make_name : positive -> option string) (inbounds : type.for_each_lhs_of_arrow ZRange.type.option.interp t) (out_data : var_data (type.final_codomain t)) (count : positive) (in_to_body_count : positive -> positive) {struct t} : ErrT (type.for_each_lhs_of_arrow var_data t * var_data (type.final_codomain t) * expr) := let _ := @PHOAS.expr.partially_show_expr in (* for TC resolution *) match t return @Compilers.expr.expr base.type ident.ident var_data t -> type.for_each_lhs_of_arrow ZRange.type.option.interp t -> var_data (type.final_codomain t) -> ErrT (type.for_each_lhs_of_arrow var_data t * var_data (type.final_codomain t) * expr) with | type.base t => fun e tt vd => rv <- expr_of_base_PHOAS do_bounds_check e (in_to_body_count count) make_name vd; ret (tt, vd, rv) | type.arrow s d => fun e '(inbound, inbounds) vd => match var_data_of_bounds count make_in_name inbound, invert_Abs e with | Some (count, vs), Some f => retv <- @expr_of_PHOAS' do_bounds_check d (f vs) make_in_name make_name inbounds vd count in_to_body_count; let '(vss, vd, rv) := retv in ret (vs, vss, vd, rv) | None, _ => inr ["Unable to bind names for all arguments and bounds at type " ++ show false s]%string%list | _, None => inr ["Invalid non-λ expression of arrow type (" ++ show false t ++ "): " ++ show true e]%string%list end end%core%expr e inbounds out_data. Definition expr_of_PHOAS (do_bounds_check : bool) {t} (e : @Compilers.expr.expr base.type ident.ident var_data t) (make_in_name : positive -> option string) (make_out_name : positive -> option string) (make_name : positive -> option string) (inbounds : type.for_each_lhs_of_arrow ZRange.type.option.interp t) (outbounds : ZRange.type.option.interp (type.final_codomain t)) (count : positive) (in_to_body_count out_to_in_count : positive -> positive) : ErrT (type.for_each_lhs_of_arrow var_data t * var_data (type.final_codomain t) * expr) := match var_data_of_bounds count make_out_name outbounds with | Some vd => let '(count, vd) := vd in let count := out_to_in_count count in @expr_of_PHOAS' do_bounds_check t e make_in_name make_name inbounds vd count in_to_body_count | None => inr ["Unable to bind names for all return arguments and bounds at type " ++ show false (type.final_codomain t)]%string end. Definition ExprOfPHOAS (do_bounds_check : bool) {t} (e : @Compilers.expr.Expr base.type ident.ident t) (name_list : option (list string)) (inbounds : type.for_each_lhs_of_arrow ZRange.type.option.interp t) : ErrT (type.for_each_lhs_of_arrow var_data t * var_data (type.final_codomain t) * expr) := (let outbounds := partial.Extract e inbounds in let make_name_gen prefix := match name_list with | None => fun p => Some (prefix ++ decimal_string_of_Z (Zpos p)) | Some ls => fun p => List.nth_error ls (pred (Pos.to_nat p)) end in let make_in_name := make_name_gen "arg" in let make_out_name := make_name_gen "out" in let make_name := make_name_gen "x" in let reset_if_names_given := match name_list with | Some _ => fun p : positive => p | None => fun _ : positive => 1%positive end in expr_of_PHOAS do_bounds_check (e _) make_in_name make_out_name make_name inbounds outbounds 1 reset_if_names_given reset_if_names_given). End with_bind. End OfPHOAS. Module String. Definition typedef_header (prefix : string) (bitwidths_used : PositiveSet.t) : list string := (["#include "] ++ (if PositiveSet.mem 1 bitwidths_used then ["typedef unsigned char " ++ prefix ++ "uint1;"; "typedef signed char " ++ prefix ++ "int1;"]%string else []) ++ (if PositiveSet.mem 128 bitwidths_used then ["typedef signed __int128 " ++ prefix ++ "int128;"; "typedef unsigned __int128 " ++ prefix ++ "uint128;"]%string else []))%list. Definition stdint_bitwidths : list Z := [8; 16; 32; 64]. Definition is_special_bitwidth (bw : Z) := negb (existsb (Z.eqb bw) stdint_bitwidths). Module int. Module type. Definition to_string (prefix : string) (t : int.type) : string := ((if is_special_bitwidth (int.bitwidth_of t) then prefix else "") ++ (if int.is_unsigned t then "u" else "") ++ "int" ++ decimal_string_of_Z (int.bitwidth_of t) ++ (if is_special_bitwidth (int.bitwidth_of t) then "" else "_t"))%string. Definition to_literal_macro_string (t : int.type) : option string := if Z.ltb (int.bitwidth_of t) 8 then None else Some ((if int.is_unsigned t then "U" else "") ++ "INT" ++ decimal_string_of_Z (int.bitwidth_of t) ++ "_C")%string. End type. End int. Module type. Module primitive. Definition to_string (prefix : string) (t : type.primitive) (r : option int.type) : string := match r with | Some int_t => int.type.to_string prefix int_t | None => "ℤ" end ++ match t with | type.Zptr => "*" | type.Z => "" end. End primitive. End type. End String. Module primitive. Definition to_string (prefix : string) (t : type.primitive) (v : BinInt.Z) : string := match t, String.int.type.to_literal_macro_string (int.of_zrange_relaxed r[v ~> v]) with | type.Z, Some macro => macro ++ "(" ++ HexString.of_Z v ++ ")" | type.Z, None => HexString.of_Z v | type.Zptr, _ => "#error ""literal address " ++ HexString.of_Z v ++ """;" end. End primitive. Fixpoint arith_to_string (prefix : string) {t} (e : arith_expr t) : string := match e with | (literal v @@ _) => primitive.to_string prefix type.Z v | (List_nth n @@ Var _ v) => "(" ++ v ++ "[" ++ decimal_string_of_Z (Z.of_nat n) ++ "])" | (Addr @@ Var _ v) => "&" ++ v | (Dereference @@ e) => "( *" ++ @arith_to_string prefix _ e ++ " )" | (Z_shiftr offset @@ e) => "(" ++ @arith_to_string prefix _ e ++ " >> " ++ decimal_string_of_Z offset ++ ")" | (Z_shiftl offset @@ e) => "(" ++ @arith_to_string prefix _ e ++ " << " ++ decimal_string_of_Z offset ++ ")" | (Z_land @@ (e1, e2)) => "(" ++ @arith_to_string prefix _ e1 ++ " & " ++ @arith_to_string prefix _ e2 ++ ")" | (Z_lor @@ (e1, e2)) => "(" ++ @arith_to_string prefix _ e1 ++ " | " ++ @arith_to_string prefix _ e2 ++ ")" | (Z_add @@ (x1, x2)) => "(" ++ @arith_to_string prefix _ x1 ++ " + " ++ @arith_to_string prefix _ x2 ++ ")" | (Z_mul @@ (x1, x2)) => "(" ++ @arith_to_string prefix _ x1 ++ " * " ++ @arith_to_string prefix _ x2 ++ ")" | (Z_sub @@ (x1, x2)) => "(" ++ @arith_to_string prefix _ x1 ++ " - " ++ @arith_to_string prefix _ x2 ++ ")" | (Z_opp @@ e) => "(-" ++ @arith_to_string prefix _ e ++ ")" | (Z_lnot _ @@ e) => "(~" ++ @arith_to_string prefix _ e ++ ")" | (Z_bneg @@ e) => "(!" ++ @arith_to_string prefix _ e ++ ")" | (Z_mul_split lg2s @@ args) => prefix ++ "mulx_u" ++ decimal_string_of_Z lg2s ++ "(" ++ @arith_to_string prefix _ args ++ ")" | (Z_add_with_get_carry lg2s @@ args) => prefix ++ "addcarryx_u" ++ decimal_string_of_Z lg2s ++ "(" ++ @arith_to_string prefix _ args ++ ")" | (Z_sub_with_get_borrow lg2s @@ args) => prefix ++ "subborrowx_u" ++ decimal_string_of_Z lg2s ++ "(" ++ @arith_to_string prefix _ args ++ ")" | (Z_zselect ty @@ args) => prefix ++ "cmovznz_" ++ (if int.is_unsigned ty then "u" else "") ++ decimal_string_of_Z (int.bitwidth_of ty) ++ "(" ++ @arith_to_string prefix _ args ++ ")" | (Z_add_modulo @@ (x1, x2, x3)) => "#error addmodulo;" | (Z_static_cast int_t @@ e) => "(" ++ String.type.primitive.to_string prefix type.Z (Some int_t) ++ ")" ++ @arith_to_string prefix _ e | Var _ v => v | Pair A B a b => @arith_to_string prefix A a ++ ", " ++ @arith_to_string prefix B b | (List_nth _ @@ _) | (Addr @@ _) | (Z_add @@ _) | (Z_mul @@ _) | (Z_sub @@ _) | (Z_land @@ _) | (Z_lor @@ _) | (Z_add_modulo @@ _) => "#error bad_arg;" | TT => "#error tt;" end%core%Cexpr. Fixpoint stmt_to_string (prefix : string) (e : stmt) : string := match e with | Call val => arith_to_string prefix val ++ ";" | Assign true t sz name val => String.type.primitive.to_string prefix t sz ++ " " ++ name ++ " = " ++ arith_to_string prefix val ++ ";" | Assign false _ sz name val => name ++ " = " ++ arith_to_string prefix val ++ ";" | AssignZPtr name sz val => "*" ++ name ++ " = " ++ arith_to_string prefix val ++ ";" | DeclareVar t sz name => String.type.primitive.to_string prefix t sz ++ " " ++ name ++ ";" | AssignNth name n val => name ++ "[" ++ decimal_string_of_Z (Z.of_nat n) ++ "] = " ++ arith_to_string prefix val ++ ";" end. Definition to_strings (prefix : string) (e : expr) : list string := List.map (stmt_to_string prefix) e. Record ident_infos := { bitwidths_used : PositiveSet.t; addcarryx_lg_splits : PositiveSet.t; mulx_lg_splits : PositiveSet.t; cmovznz_bitwidths : PositiveSet.t }. Definition ident_info_empty : ident_infos := Build_ident_infos PositiveSet.empty PositiveSet.empty PositiveSet.empty PositiveSet.empty. Definition ident_info_union (x y : ident_infos) : ident_infos := let (x0, x1, x2, x3) := x in let (y0, y1, y2, y3) := y in Build_ident_infos (PositiveSet.union x0 y0) (PositiveSet.union x1 y1) (PositiveSet.union x2 y2) (PositiveSet.union x3 y3). Definition ident_info_of_bitwidths_used (v : PositiveSet.t) : ident_infos := {| bitwidths_used := v; addcarryx_lg_splits := PositiveSet.empty; mulx_lg_splits := PositiveSet.empty; cmovznz_bitwidths := PositiveSet.empty |}. Definition ident_info_of_addcarryx (v : PositiveSet.t) : ident_infos := {| bitwidths_used := PositiveSet.empty; addcarryx_lg_splits := v; mulx_lg_splits := PositiveSet.empty; cmovznz_bitwidths := PositiveSet.empty |}. Definition ident_info_of_mulx (v : PositiveSet.t) : ident_infos := {| bitwidths_used := PositiveSet.empty; addcarryx_lg_splits := PositiveSet.empty; mulx_lg_splits := v; cmovznz_bitwidths := PositiveSet.empty |}. Definition ident_info_of_cmovznz (v : PositiveSet.t) : ident_infos := {| bitwidths_used := PositiveSet.empty; addcarryx_lg_splits := PositiveSet.empty; mulx_lg_splits := PositiveSet.empty; cmovznz_bitwidths := v |}. Definition collect_bitwidths_of_int_type (t : int.type) : PositiveSet.t := PositiveSet.add (Z.to_pos (int.bitwidth_of t)) PositiveSet.empty. Definition collect_infos_of_ident {s d} (idc : ident s d) : ident_infos := match idc with | Z_static_cast ty => ident_info_of_bitwidths_used (collect_bitwidths_of_int_type ty) | Z_mul_split lg2s => ident_info_of_mulx (PositiveSet.add (Z.to_pos lg2s) PositiveSet.empty) | Z_add_with_get_carry lg2s | Z_sub_with_get_borrow lg2s => ident_info_of_addcarryx (PositiveSet.add (Z.to_pos lg2s) PositiveSet.empty) | Z_zselect ty => ident_info_of_cmovznz (collect_bitwidths_of_int_type ty) | literal _ | List_nth _ | Addr | Dereference | Z_shiftr _ | Z_shiftl _ | Z_land | Z_lor | Z_add | Z_mul | Z_sub | Z_opp | Z_bneg | Z_lnot _ | Z_add_modulo => ident_info_empty end. Fixpoint collect_infos_of_arith_expr {t} (e : arith_expr t) : ident_infos := match e with | AppIdent s d idc arg => ident_info_union (collect_infos_of_ident idc) (@collect_infos_of_arith_expr _ arg) | Var t v => ident_info_empty | Pair A B a b => ident_info_union (@collect_infos_of_arith_expr _ a) (@collect_infos_of_arith_expr _ b) | TT => ident_info_empty end. Fixpoint collect_infos_of_stmt (e : stmt) : ident_infos := match e with | Assign _ _ (Some sz) _ val | AssignZPtr _ (Some sz) val => ident_info_union (ident_info_of_bitwidths_used (collect_bitwidths_of_int_type sz)) (collect_infos_of_arith_expr val) | Call val | Assign _ _ None _ val | AssignZPtr _ None val | AssignNth _ _ val => collect_infos_of_arith_expr val | DeclareVar _ (Some sz) _ => ident_info_of_bitwidths_used (collect_bitwidths_of_int_type sz) | DeclareVar _ None _ => ident_info_empty end. Fixpoint collect_infos (e : expr) : ident_infos := fold_right ident_info_union ident_info_empty (List.map collect_infos_of_stmt e). Import OfPHOAS. Fixpoint to_base_arg_list (prefix : string) {t} : base_var_data t -> list string := match t return base_var_data t -> _ with | base.type.Z => fun '(n, r) => [String.type.primitive.to_string prefix type.Z r ++ " " ++ n] | base.type.prod A B => fun '(va, vb) => (@to_base_arg_list prefix A va ++ @to_base_arg_list prefix B vb)%list | base.type.list base.type.Z => fun '(n, r, len) => ["const " ++ String.type.primitive.to_string prefix type.Z r ++ " " ++ n ++ "[" ++ decimal_string_of_Z (Z.of_nat len) ++ "]"] | base.type.list _ => fun _ => ["#error ""complex list"";"] | base.type.option _ => fun _ => ["#error option;"] | base.type.unit => fun _ => ["#error unit;"] | base.type.nat => fun _ => ["#error ℕ;"] | base.type.bool => fun _ => ["#error bool;"] | base.type.zrange => fun _ => ["#error zrange;"] end. Definition to_arg_list (prefix : string) {t} : var_data t -> list string := match t return var_data t -> _ with | type.base t => to_base_arg_list prefix | type.arrow _ _ => fun _ => ["#error arrow;"] end. Fixpoint to_arg_list_for_each_lhs_of_arrow (prefix : string) {t} : type.for_each_lhs_of_arrow var_data t -> list string := match t return type.for_each_lhs_of_arrow var_data t -> _ with | type.base t => fun _ => nil | type.arrow s d => fun '(x, xs) => to_arg_list prefix x ++ @to_arg_list_for_each_lhs_of_arrow prefix d xs end%list. Fixpoint to_base_retarg_list prefix {t} : base_var_data t -> list string := match t return base_var_data t -> _ with | base.type.Z => fun '(n, r) => [String.type.primitive.to_string prefix type.Zptr r ++ " " ++ n] | base.type.prod A B => fun '(va, vb) => (@to_base_retarg_list prefix A va ++ @to_base_retarg_list prefix B vb)%list | base.type.list base.type.Z => fun '(n, r, len) => [String.type.primitive.to_string prefix type.Z r ++ " " ++ n ++ "[" ++ decimal_string_of_Z (Z.of_nat len) ++ "]"] | base.type.list _ => fun _ => ["#error ""complex list"";"] | base.type.option _ => fun _ => ["#error option;"] | base.type.unit => fun _ => ["#error unit;"] | base.type.nat => fun _ => ["#error ℕ;"] | base.type.bool => fun _ => ["#error bool;"] | base.type.zrange => fun _ => ["#error zrange;"] end. Definition to_retarg_list (prefix : string) {t} : var_data t -> list string := match t return var_data t -> _ with | type.base _ => to_base_retarg_list prefix | type.arrow _ _ => fun _ => ["#error arrow;"] end. Fixpoint bound_to_string {t : base.type} : var_data t -> ZRange.type.base.option.interp t -> list string := match t return var_data t -> ZRange.type.base.option.interp t -> list string with | base.type.Z => fun '(name, _) arg => [(name ++ ": ") ++ match arg with | Some arg => show false arg | None => show false arg end]%string | base.type.prod A B => fun '(va, vb) '(a, b) => @bound_to_string A va a ++ @bound_to_string B vb b | base.type.list A => fun '(name, _, _) arg => [(name ++ ": ") ++ match ZRange.type.base.option.lift_Some arg with | Some arg => show false arg | None => show false arg end]%string | base.type.option _ | base.type.unit | base.type.bool | base.type.nat | base.type.zrange => fun _ _ => nil end%list. Fixpoint input_bounds_to_string {t} : type.for_each_lhs_of_arrow var_data t -> type.for_each_lhs_of_arrow ZRange.type.option.interp t -> list string := match t return type.for_each_lhs_of_arrow var_data t -> type.for_each_lhs_of_arrow ZRange.type.option.interp t -> list string with | type.base t => fun _ _ => nil | type.arrow (type.base s) d => fun '(v, vs) '(arg, args) => (bound_to_string v arg) ++ @input_bounds_to_string d vs args | type.arrow s d => fun '(absurd, _) => match absurd : Empty_set with end end%list. Definition to_function_lines (static : bool) (prefix : string) (name : string) {t} (f : type.for_each_lhs_of_arrow var_data t * var_data (type.final_codomain t) * expr) : list string := let '(args, rets, body) := f in (((((if static then "static " else "") ++ "void " ++ name ++ "(" ++ (String.concat ", " (to_retarg_list prefix rets ++ to_arg_list_for_each_lhs_of_arrow prefix args)) ++ ") {")%string) :: (List.map (fun s => " " ++ s)%string (to_strings prefix body))) ++ ["}"])%list. Definition ToFunctionLines (do_bounds_check : bool) (static : bool) (prefix : string) (name : string) {t} (e : @Compilers.expr.Expr base.type ident.ident t) (comment : type.for_each_lhs_of_arrow var_data t -> var_data (type.final_codomain t) -> list string) (name_list : option (list string)) (inbounds : type.for_each_lhs_of_arrow ZRange.type.option.interp t) (outbounds : ZRange.type.base.option.interp (type.final_codomain t)) : (list string * ident_infos) + string := match ExprOfPHOAS do_bounds_check e name_list inbounds with | inl (indata, outdata, f) => inl ((["/*"] ++ (List.map (fun s => if (String.length s =? 0)%nat then " *" else (" * " ++ s))%string (comment indata outdata)) ++ [" * Input Bounds:"] ++ List.map (fun v => " * " ++ v)%string (input_bounds_to_string indata inbounds) ++ [" * Output Bounds:"] ++ List.map (fun v => " * " ++ v)%string (bound_to_string outdata outbounds) ++ [" */"] ++ to_function_lines static prefix name (indata, outdata, f))%list, collect_infos f) | inr nil => inr ("Unknown internal error in converting " ++ name ++ " to C")%string | inr [err] => inr ("Error in converting " ++ name ++ " to C:" ++ String.NewLine ++ err)%string | inr errs => inr ("Errors in converting " ++ name ++ " to C:" ++ String.NewLine ++ String.concat String.NewLine errs)%string end. Definition LinesToString (lines : list string) : string := String.concat String.NewLine lines. Definition ToFunctionString (do_bounds_check : bool) (static : bool) (prefix : string) (name : string) {t} (e : @Compilers.expr.Expr base.type ident.ident t) (comment : type.for_each_lhs_of_arrow var_data t -> var_data (type.final_codomain t) -> list string) (name_list : option (list string)) (inbounds : type.for_each_lhs_of_arrow ZRange.type.option.interp t) (outbounds : ZRange.type.option.interp (type.final_codomain t)) : (string * ident_infos) + string := match ToFunctionLines do_bounds_check static prefix name e comment name_list inbounds outbounds with | inl (ls, used_types) => inl (LinesToString ls, used_types) | inr err => inr err end. End C. Notation ToFunctionLines := C.ToFunctionLines. Notation ToFunctionString := C.ToFunctionString. Notation LinesToString := C.LinesToString. End ToString. End Compilers.