diff options
| -rw-r--r-- | backends/hol4/primitivesScript.sml | 119 | ||||
| -rw-r--r-- | backends/hol4/primitivesTheory.sig | 99 | ||||
| -rw-r--r-- | compiler/Extract.ml | 93 | ||||
| -rw-r--r-- | compiler/PureUtils.ml | 24 | ||||
| -rw-r--r-- | compiler/Translate.ml | 2 |
5 files changed, 319 insertions, 18 deletions
diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml index e10ce7e5..4a1f5fdd 100644 --- a/backends/hol4/primitivesScript.sml +++ b/backends/hol4/primitivesScript.sml @@ -504,6 +504,33 @@ val all_mk_int_defs = [ mk_u128_def ] +(* Unfolding theorems for “mk_usize” and “mk_isize”: we need specific unfolding + theorems because the isize/usize bounds are opaque, and may make the evaluation + get stuck in the unit tests *) +Theorem mk_usize_unfold: + ∀ n. mk_usize n = + if 0 ≤ n ∧ (n ≤ u16_max ∨ n ≤ usize_max) then Return (int_to_usize n) + else Fail Failure +Proof + rw [mk_usize_def] >> fs [] >> + assume_tac usize_bounds >> + int_tac +QED +val _ = evalLib.add_unfold_thm "mk_usize_unfold" + +Theorem mk_isize_unfold: + ∀ n. mk_isize n = + if (i16_min ≤ n ∨ isize_min ≤ n) ∧ + (n ≤ i16_max ∨ n ≤ isize_max) + then Return (int_to_isize n) + else Fail Failure +Proof + rw [mk_isize_def] >> fs [] >> + assume_tac isize_bounds >> + int_tac +QED +val _ = evalLib.add_unfold_thm "mk_isize_unfold" + val isize_neg_def = Define ‘isize_neg x = mk_isize (- (isize_to_int x))’ val i8_neg_def = Define ‘i8_neg x = mk_i8 (- (i8_to_int x))’ val i16_neg_def = Define ‘i16_neg x = mk_i16 (- (i16_to_int x))’ @@ -1521,6 +1548,98 @@ Definition isize_ge_def: End +(* Equality theorems for the comparisons between integers - used by evalLib *) + +val prove_scalar_eq_equiv_tac = metis_tac all_scalar_to_int_to_scalar_lemmas + +Theorem isize_eq_equiv: + ∀x y. (x = y) = (isize_to_int x = isize_to_int y) +Proof + prove_scalar_eq_equiv_tac +QED + +Theorem i8_eq_equiv: + ∀x y. (x = y) = (i8_to_int x = i8_to_int y) +Proof + prove_scalar_eq_equiv_tac +QED + +Theorem i16_eq_equiv: + ∀x y. (x = y) = (i16_to_int x = i16_to_int y) +Proof + prove_scalar_eq_equiv_tac +QED + +Theorem i32_eq_equiv: + ∀x y. (x = y) = (i32_to_int x = i32_to_int y) +Proof + prove_scalar_eq_equiv_tac +QED + +Theorem i64_eq_equiv: + ∀x y. (x = y) = (i64_to_int x = i64_to_int y) +Proof + prove_scalar_eq_equiv_tac +QED + +Theorem i128_eq_equiv: + ∀x y. (x = y) = (i128_to_int x = i128_to_int y) +Proof + prove_scalar_eq_equiv_tac +QED + +Theorem usize_eq_equiv: + ∀x y. (x = y) = (usize_to_int x = usize_to_int y) +Proof + prove_scalar_eq_equiv_tac +QED + +Theorem u8_eq_equiv: + ∀x y. (x = y) = (u8_to_int x = u8_to_int y) +Proof + prove_scalar_eq_equiv_tac +QED + +Theorem u16_eq_equiv: + ∀x y. (x = y) = (u16_to_int x = u16_to_int y) +Proof + prove_scalar_eq_equiv_tac +QED + +Theorem u32_eq_equiv: + ∀x y. (x = y) = (u32_to_int x = u32_to_int y) +Proof + prove_scalar_eq_equiv_tac +QED + +Theorem u64_eq_equiv: + ∀x y. (x = y) = (u64_to_int x = u64_to_int y) +Proof + prove_scalar_eq_equiv_tac +QED + +Theorem u128_eq_equiv: + ∀x y. (x = y) = (u128_to_int x = u128_to_int y) +Proof + prove_scalar_eq_equiv_tac +QED + +(* Remark.: don't move this up, it will break some proofs *) +val _ = BasicProvers.export_rewrites [ + "isize_eq_equiv", + "i8_eq_equiv", + "i16_eq_equiv", + "i32_eq_equiv", + "i64_eq_equiv", + "i128_eq_equiv", + "usize_eq_equiv", + "u8_eq_equiv", + "u16_eq_equiv", + "u32_eq_equiv", + "u64_eq_equiv", + "u128_eq_equiv" +] + (*** * Vectors *) diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig index 1908cbcb..45caf234 100644 --- a/backends/hol4/primitivesTheory.sig +++ b/backends/hol4/primitivesTheory.sig @@ -221,6 +221,7 @@ sig val error_nchotomy : thm val i128_add_eq : thm val i128_div_eq : thm + val i128_eq_equiv : thm val i128_mul_eq : thm val i128_neg_eq : thm val i128_rem_eq : thm @@ -228,6 +229,7 @@ sig val i128_to_int_int_to_i128_unfold : thm val i16_add_eq : thm val i16_div_eq : thm + val i16_eq_equiv : thm val i16_mul_eq : thm val i16_neg_eq : thm val i16_rem_eq : thm @@ -235,6 +237,7 @@ sig val i16_to_int_int_to_i16_unfold : thm val i32_add_eq : thm val i32_div_eq : thm + val i32_eq_equiv : thm val i32_mul_eq : thm val i32_neg_eq : thm val i32_rem_eq : thm @@ -242,6 +245,7 @@ sig val i32_to_int_int_to_i32_unfold : thm val i64_add_eq : thm val i64_div_eq : thm + val i64_eq_equiv : thm val i64_mul_eq : thm val i64_neg_eq : thm val i64_rem_eq : thm @@ -249,6 +253,7 @@ sig val i64_to_int_int_to_i64_unfold : thm val i8_add_eq : thm val i8_div_eq : thm + val i8_eq_equiv : thm val i8_mul_eq : thm val i8_neg_eq : thm val i8_rem_eq : thm @@ -258,11 +263,14 @@ sig val index_update_same : thm val isize_add_eq : thm val isize_div_eq : thm + val isize_eq_equiv : thm val isize_mul_eq : thm val isize_neg_eq : thm val isize_rem_eq : thm val isize_sub_eq : thm val isize_to_int_int_to_isize_unfold : thm + val mk_isize_unfold : thm + val mk_usize_unfold : thm val mk_vec_unfold : thm val num2error_11 : thm val num2error_ONTO : thm @@ -277,30 +285,35 @@ sig val result_nchotomy : thm val u128_add_eq : thm val u128_div_eq : thm + val u128_eq_equiv : thm val u128_mul_eq : thm val u128_rem_eq : thm val u128_sub_eq : thm val u128_to_int_int_to_u128_unfold : thm val u16_add_eq : thm val u16_div_eq : thm + val u16_eq_equiv : thm val u16_mul_eq : thm val u16_rem_eq : thm val u16_sub_eq : thm val u16_to_int_int_to_u16_unfold : thm val u32_add_eq : thm val u32_div_eq : thm + val u32_eq_equiv : thm val u32_mul_eq : thm val u32_rem_eq : thm val u32_sub_eq : thm val u32_to_int_int_to_u32_unfold : thm val u64_add_eq : thm val u64_div_eq : thm + val u64_eq_equiv : thm val u64_mul_eq : thm val u64_rem_eq : thm val u64_sub_eq : thm val u64_to_int_int_to_u64_unfold : thm val u8_add_eq : thm val u8_div_eq : thm + val u8_eq_equiv : thm val u8_mul_eq : thm val u8_rem_eq : thm val u8_sub_eq : thm @@ -309,6 +322,7 @@ sig val update_spec : thm val usize_add_eq : thm val usize_div_eq : thm + val usize_eq_equiv : thm val usize_mul_eq : thm val usize_rem_eq : thm val usize_sub_eq : thm @@ -1366,6 +1380,11 @@ sig ∃z. i128_div x y = Return z ∧ i128_to_int z = i128_to_int x / i128_to_int y + [i128_eq_equiv] Theorem + + [oracles: DISK_THM] [axioms: int_to_i128_i128_to_int] [] + ⊢ ∀x y. x = y ⇔ i128_to_int x = i128_to_int y + [i128_mul_eq] Theorem [oracles: DISK_THM] @@ -1436,6 +1455,11 @@ sig ∃z. i16_div x y = Return z ∧ i16_to_int z = i16_to_int x / i16_to_int y + [i16_eq_equiv] Theorem + + [oracles: DISK_THM] [axioms: int_to_i16_i16_to_int] [] + ⊢ ∀x y. x = y ⇔ i16_to_int x = i16_to_int y + [i16_mul_eq] Theorem [oracles: DISK_THM] @@ -1505,6 +1529,11 @@ sig ∃z. i32_div x y = Return z ∧ i32_to_int z = i32_to_int x / i32_to_int y + [i32_eq_equiv] Theorem + + [oracles: DISK_THM] [axioms: int_to_i32_i32_to_int] [] + ⊢ ∀x y. x = y ⇔ i32_to_int x = i32_to_int y + [i32_mul_eq] Theorem [oracles: DISK_THM] @@ -1574,6 +1603,11 @@ sig ∃z. i64_div x y = Return z ∧ i64_to_int z = i64_to_int x / i64_to_int y + [i64_eq_equiv] Theorem + + [oracles: DISK_THM] [axioms: int_to_i64_i64_to_int] [] + ⊢ ∀x y. x = y ⇔ i64_to_int x = i64_to_int y + [i64_mul_eq] Theorem [oracles: DISK_THM] @@ -1643,6 +1677,11 @@ sig ∃z. i8_div x y = Return z ∧ i8_to_int z = i8_to_int x / i8_to_int y + [i8_eq_equiv] Theorem + + [oracles: DISK_THM] [axioms: int_to_i8_i8_to_int] [] + ⊢ ∀x y. x = y ⇔ i8_to_int x = i8_to_int y + [i8_mul_eq] Theorem [oracles: DISK_THM] @@ -1730,6 +1769,11 @@ sig ∃z. isize_div x y = Return z ∧ isize_to_int z = isize_to_int x / isize_to_int y + [isize_eq_equiv] Theorem + + [oracles: DISK_THM] [axioms: int_to_isize_isize_to_int] [] + ⊢ ∀x y. x = y ⇔ isize_to_int x = isize_to_int y + [isize_mul_eq] Theorem [oracles: DISK_THM] @@ -1787,6 +1831,24 @@ sig if i16_min ≤ n ∧ n ≤ i16_max then n else isize_to_int (int_to_isize n) + [mk_isize_unfold] Theorem + + [oracles: DISK_THM] [axioms: isize_bounds] [] + ⊢ ∀n. mk_isize n = + if + (i16_min ≤ n ∨ isize_min ≤ n) ∧ (n ≤ i16_max ∨ n ≤ isize_max) + then + Return (int_to_isize n) + else Fail Failure + + [mk_usize_unfold] Theorem + + [oracles: DISK_THM] [axioms: usize_bounds] [] + ⊢ ∀n. mk_usize n = + if 0 ≤ n ∧ (n ≤ u16_max ∨ n ≤ usize_max) then + Return (int_to_usize n) + else Fail Failure + [mk_vec_unfold] Theorem [oracles: DISK_THM] [axioms: mk_vec_axiom] [] @@ -1866,6 +1928,11 @@ sig ∃z. u128_div x y = Return z ∧ u128_to_int z = u128_to_int x / u128_to_int y + [u128_eq_equiv] Theorem + + [oracles: DISK_THM] [axioms: int_to_u128_u128_to_int] [] + ⊢ ∀x y. x = y ⇔ u128_to_int x = u128_to_int y + [u128_mul_eq] Theorem [oracles: DISK_THM] @@ -1923,6 +1990,11 @@ sig ∃z. u16_div x y = Return z ∧ u16_to_int z = u16_to_int x / u16_to_int y + [u16_eq_equiv] Theorem + + [oracles: DISK_THM] [axioms: int_to_u16_u16_to_int] [] + ⊢ ∀x y. x = y ⇔ u16_to_int x = u16_to_int y + [u16_mul_eq] Theorem [oracles: DISK_THM] @@ -1980,6 +2052,11 @@ sig ∃z. u32_div x y = Return z ∧ u32_to_int z = u32_to_int x / u32_to_int y + [u32_eq_equiv] Theorem + + [oracles: DISK_THM] [axioms: int_to_u32_u32_to_int] [] + ⊢ ∀x y. x = y ⇔ u32_to_int x = u32_to_int y + [u32_mul_eq] Theorem [oracles: DISK_THM] @@ -2037,6 +2114,11 @@ sig ∃z. u64_div x y = Return z ∧ u64_to_int z = u64_to_int x / u64_to_int y + [u64_eq_equiv] Theorem + + [oracles: DISK_THM] [axioms: int_to_u64_u64_to_int] [] + ⊢ ∀x y. x = y ⇔ u64_to_int x = u64_to_int y + [u64_mul_eq] Theorem [oracles: DISK_THM] @@ -2094,6 +2176,11 @@ sig ∃z. u8_div x y = Return z ∧ u8_to_int z = u8_to_int x / u8_to_int y + [u8_eq_equiv] Theorem + + [oracles: DISK_THM] [axioms: int_to_u8_u8_to_int] [] + ⊢ ∀x y. x = y ⇔ u8_to_int x = u8_to_int y + [u8_mul_eq] Theorem [oracles: DISK_THM] @@ -2164,6 +2251,11 @@ sig ∃z. usize_div x y = Return z ∧ usize_to_int z = usize_to_int x / usize_to_int y + [usize_eq_equiv] Theorem + + [oracles: DISK_THM] [axioms: int_to_usize_usize_to_int] [] + ⊢ ∀x y. x = y ⇔ usize_to_int x = usize_to_int y + [usize_mul_eq] Theorem [oracles: DISK_THM] @@ -2207,7 +2299,8 @@ sig [oracles: DISK_THM] [axioms: vec_to_list_num_bounds, usize_bounds, - usize_to_int_int_to_usize, usize_to_int_bounds, mk_vec_axiom] [] + int_to_usize_usize_to_int, usize_to_int_bounds, + usize_to_int_int_to_usize, mk_vec_axiom] [] ⊢ ∀v i x. usize_to_int i < usize_to_int (vec_len v) ⇒ ∃nv. @@ -2219,7 +2312,9 @@ sig [vec_len_spec] Theorem - [oracles: DISK_THM] [axioms: usize_bounds, vec_to_list_num_bounds] [] + [oracles: DISK_THM] + [axioms: int_to_usize_usize_to_int, usize_bounds, + vec_to_list_num_bounds] [] ⊢ ∀v. vec_len v = int_to_usize (len (vec_to_list v)) ∧ 0 ≤ len (vec_to_list v) ∧ len (vec_to_list v) ≤ usize_max diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 2f1898b3..7e4aeab4 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -2241,7 +2241,33 @@ and extract_Abs (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) (e : texpression) : unit = - let lets, next_e = destruct_lets e in + (* Destruct the lets. + + Note that in the case of HOL4, we stop destructing the lets if at some point + the "kind" (monadic or non-monadic) of the lets changes. + + We do this because in HOL4 the parsing is not very powerful: + if we mix monadic let-bindings and non monadic let-bindings, we have to + wrap the let-bindings inside a [do ... od] whenever we need to extract + a monadic let-binding non immediately inside a monadic let-binding. + + Ex.: + {[ + do + x <- ...; + let y = f x in + do + z <- g y; + ... + od + od + ]} + *) + let lets, next_e = + match !backend with + | HOL4 -> destruct_lets_no_interleave e + | FStar | Coq | Lean -> destruct_lets e + in (* Open a box for the whole expression. In the case of Lean, we use a vbox so that line breaks are inserted @@ -2325,10 +2351,21 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) (* Return *) ctx in - let exists_monadic = List.exists (fun (m, _, _) -> m) lets in (* If Lean and HOL4, we rely on monadic blocks, so we insert a do and open a new box immediately *) - if (!backend = Lean || !backend = HOL4) && exists_monadic then ( + let wrap_in_do_od = + match !backend with + | Lean -> + (* For Lean, we wrap in a block iff at least one of the let-bindings is monadic *) + List.exists (fun (m, _, _) -> m) lets + | HOL4 -> + (* HOL4 is similar to HOL4, but we add a sanity check *) + let wrap_in_do = List.exists (fun (m, _, _) -> m) lets in + if wrap_in_do then assert (List.for_all (fun (m, _, _) -> m) lets); + wrap_in_do + | FStar | Coq -> false + in + if wrap_in_do_od then ( F.pp_open_vbox fmt (if !backend = Lean then ctx.indent_incr else 0); F.pp_print_string fmt "do"; F.pp_print_space fmt ()); @@ -2345,7 +2382,7 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) F.pp_close_box fmt (); (* do-box (Lean and HOL4 only) *) - if (!backend = Lean || !backend = HOL4) && exists_monadic then ( + if wrap_in_do_od then ( if !backend = HOL4 then ( F.pp_print_space fmt (); F.pp_print_string fmt "od"); @@ -2512,17 +2549,45 @@ and extract_StructUpdate (ctx : extraction_ctx) (fmt : F.formatter) else ( F.pp_open_hvbox fmt 0; F.pp_open_hvbox fmt ctx.indent_incr; - let lb, rb = + (* Inner/outer brackets: there are several syntaxes for the field updates. + + For instance, in F*: + {[ + { x with f = ..., ... } + ]} + + In HOL4: + {[ + x with <| f = ..., ... |> + ]} + + In the above examples: + - in F*, the { } brackets are "outer" brackets + - in HOL4, the <| |> brackets are "inner" brackets + *) + (* Outer brackets *) + let olb, orb = match !backend with | Lean | FStar -> (Some "{", Some "}") | Coq -> (Some "{|", Some "|}") | HOL4 -> (None, None) in - (match lb with - | Some lb -> - F.pp_print_string fmt lb; - F.pp_print_space fmt () - | None -> ()); + (* Inner brackets *) + let ilb, irb = + match !backend with + | Lean | FStar | Coq -> (None, None) + | HOL4 -> (Some "<|", Some "|>") + in + (* Helper *) + let print_bracket (is_left : bool) b = + match b with + | Some b -> + if not is_left then F.pp_print_space fmt (); + F.pp_print_string fmt b; + if is_left then F.pp_print_space fmt () + | None -> () + in + print_bracket true olb; let need_paren = inside && !backend = HOL4 in if need_paren then F.pp_print_string fmt "("; F.pp_open_hvbox fmt ctx.indent_incr; @@ -2532,6 +2597,7 @@ and extract_StructUpdate (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_space fmt (); F.pp_print_string fmt "with"; F.pp_print_space fmt ()); + print_bracket true ilb; F.pp_open_hvbox fmt 0; let delimiter = match !backend with Lean -> "," | Coq | FStar | HOL4 -> ";" @@ -2555,14 +2621,11 @@ and extract_StructUpdate (ctx : extraction_ctx) (fmt : F.formatter) F.pp_close_box fmt ()) supd.updates; F.pp_close_box fmt (); + print_bracket false irb; F.pp_close_box fmt (); F.pp_close_box fmt (); if need_paren then F.pp_print_string fmt ")"; - (match rb with - | Some rb -> - F.pp_print_space fmt (); - F.pp_print_string fmt rb - | None -> ()); + print_bracket false orb; F.pp_close_box fmt ()) (** Insert a space, if necessary *) diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml index 9b768f3b..647678c1 100644 --- a/compiler/PureUtils.ml +++ b/compiler/PureUtils.ml @@ -220,6 +220,30 @@ let rec destruct_lets (e : texpression) : ((monadic, lv, re) :: lets, last_e) | _ -> ([], e) +(** Destruct an expression into a list of nested lets, where there + is no interleaving between monadic and non-monadic lets. + *) +let destruct_lets_no_interleave (e : texpression) : + (bool * typed_pattern * texpression) list * texpression = + (* Find the "kind" of the first let (monadic or non-monadic) *) + let m = + match e.e with + | Let (monadic, _, _, _) -> monadic + | _ -> raise (Failure "Unreachable") + in + (* Destruct the rest *) + let rec destruct_lets (e : texpression) : + (bool * typed_pattern * texpression) list * texpression = + match e.e with + | Let (monadic, lv, re, next_e) -> + if monadic = m then + let lets, last_e = destruct_lets next_e in + ((monadic, lv, re) :: lets, last_e) + else ([], e) + | _ -> ([], e) + in + destruct_lets e + (** Destruct an [App] expression into an expression and a list of arguments. We simply destruct the expression as long as it is of the form [App (f, x)]. diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 709b54a4..1107a123 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -851,7 +851,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string) (* Close the module *) (match !Config.backend with | FStar | Lean -> () - | HOL4 -> Printf.fprintf out "val _ = export_theory \"%s\"\n" module_name + | HOL4 -> Printf.fprintf out "val _ = export_theory ()\n" | Coq -> Printf.fprintf out "End %s .\n" module_name); (* Some logging *) |