diff options
| -rw-r--r-- | backends/hol4/divDefLibTestScript.sml | 7 | ||||
| -rw-r--r-- | backends/hol4/primitivesScript.sml | 521 | ||||
| -rw-r--r-- | backends/hol4/primitivesTheory.sig | 331 | ||||
| -rw-r--r-- | compiler/Config.ml | 5 | ||||
| -rw-r--r-- | compiler/Driver.ml | 5 | ||||
| -rw-r--r-- | compiler/Extract.ml | 1197 | ||||
| -rw-r--r-- | compiler/ExtractBase.ml | 22 | ||||
| -rw-r--r-- | compiler/PureUtils.ml | 2 | ||||
| -rw-r--r-- | compiler/StringUtils.ml | 5 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 2 | ||||
| -rw-r--r-- | compiler/Translate.ml | 466 | ||||
| -rw-r--r-- | tests/coq/betree/BetreeMain_Funs.v | 13 | ||||
| -rw-r--r-- | tests/coq/hashmap/Hashmap_Funs.v | 37 | ||||
| -rw-r--r-- | tests/coq/hashmap_on_disk/HashmapMain_Funs.v | 36 | ||||
| -rw-r--r-- | tests/coq/misc/Constants.v | 26 | ||||
| -rw-r--r-- | tests/coq/misc/External_Funs.v | 8 | ||||
| -rw-r--r-- | tests/coq/misc/Loops.v | 18 | ||||
| -rw-r--r-- | tests/coq/misc/NoNestedBorrows.v | 56 | ||||
| -rw-r--r-- | tests/coq/misc/Paper.v | 16 | ||||
| -rw-r--r-- | tests/hol4/Holmakefile.template | 3 | ||||
| -rw-r--r-- | tests/hol4/Makefile | 39 | ||||
| -rw-r--r-- | tests/lean/misc-no_nested_borrows/NoNestedBorrows.lean | 5 |
22 files changed, 2101 insertions, 719 deletions
diff --git a/backends/hol4/divDefLibTestScript.sml b/backends/hol4/divDefLibTestScript.sml index 80170b24..f5df6139 100644 --- a/backends/hol4/divDefLibTestScript.sml +++ b/backends/hol4/divDefLibTestScript.sml @@ -1,11 +1,6 @@ (* Examples which use divDefLib.DefineDiv *) -open HolKernel boolLib bossLib Parse -open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory - -open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory -open primitivesLib -open divDefTheory divDefLib +open primitivesLib divDefLib val _ = new_theory "divDefLibTest" diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml index 00511f00..5ef51f2e 100644 --- a/backends/hol4/primitivesScript.sml +++ b/backends/hol4/primitivesScript.sml @@ -17,37 +17,52 @@ End Type M = ``: 'a result`` -val bind_def = Define ` +Definition bind_def: (bind : 'a M -> ('a -> 'b M) -> 'b M) x f = case x of Return y => f y | Fail e => Fail e - | Diverge => Diverge`; + | Diverge => Diverge +End val bind_name = fst (dest_const “bind”) -val return_def = Define ` +Definition return_def: (return : 'a -> 'a M) x = - Return x`; + Return x +End -val massert_def = Define ‘massert b = if b then Return () else Fail Failure’ +Definition massert_def: + massert b = if b then Return () else Fail Failure +End Overload monad_bind = ``bind`` Overload monad_unitbind = ``\x y. bind x (\z. y)`` Overload monad_ignore_bind = ``\x y. bind x (\z. y)`` -val is_diverge_def = Define ‘ - is_diverge (r: 'a result) : bool = case r of Diverge => T | _ => F’ +Definition is_diverge_def: + is_diverge (r: 'a result) : bool = case r of Diverge => T | _ => F +End (* Allow the use of monadic syntax *) val _ = monadsyntax.enable_monadsyntax () +(*** For the globals *) +Definition get_return_value_def: + get_return_value (Return x) = x +End + (*** Misc *) Type char = “:char” Type string = “:string” -val mem_replace_fwd_def = Define ‘mem_replace_fwd (x : 'a) (y :'a) : 'a = x’ -val mem_replace_back_def = Define ‘mem_replace_back (x : 'a) (y :'a) : 'a = y’ +Definition mem_replace_fwd_def: + mem_replace_fwd (x : 'a) (y :'a) : 'a = x +End + +Definition mem_replace_back_def: + mem_replace_back (x : 'a) (y :'a) : 'a = y +End (*** Scalars *) (* Remark: most of the following code was partially generated *) @@ -343,6 +358,21 @@ val all_mk_int_defs = [ mk_u128_def ] +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))’ +val i32_neg_def = Define ‘i32_neg x = mk_i32 (- (i32_to_int x))’ +val i64_neg_def = Define ‘i64_neg x = mk_i64 (- (i64_to_int x))’ +val i128_neg_def = Define ‘i128_neg x = mk_i128 (- (i128_to_int x))’ + +val all_neg_defs = [ + isize_neg_def, + i8_neg_def, + i16_neg_def, + i32_neg_def, + i64_neg_def, + i128_neg_def +] val isize_add_def = Define ‘isize_add x y = mk_isize ((isize_to_int x) + (isize_to_int y))’ val i8_add_def = Define ‘i8_add x y = mk_i8 ((i8_to_int x) + (i8_to_int y))’ @@ -526,6 +556,71 @@ val all_rem_defs = [ val (asms,g) = top_goal () *) +fun prove_arith_unop_eq (asms, g) = + let + val rw_thms = List.concat [all_neg_defs, all_mk_int_defs, all_conversion_id_lemmas] + in + (rpt gen_tac >> + rpt disch_tac >> + assume_tac isize_bounds >> (* Only useful for isize of course *) + rw rw_thms) (asms, g) + end + +Theorem isize_neg_eq: + !x y. + isize_min ≤ - isize_to_int x ⇒ + - isize_to_int x ≤ isize_max ⇒ + ?y. isize_neg x = Return y /\ isize_to_int y = - isize_to_int x +Proof + prove_arith_unop_eq +QED + +Theorem i8_neg_eq: + !x y. + i8_min ≤ - i8_to_int x ⇒ + - i8_to_int x ≤ i8_max ⇒ + ?y. i8_neg x = Return y /\ i8_to_int y = - i8_to_int x +Proof + prove_arith_unop_eq +QED + +Theorem i16_neg_eq: + !x y. + i16_min ≤ - i16_to_int x ⇒ + - i16_to_int x ≤ i16_max ⇒ + ?y. i16_neg x = Return y /\ i16_to_int y = - i16_to_int x +Proof + prove_arith_unop_eq +QED + +Theorem i32_neg_eq: + !x y. + i32_min ≤ - i32_to_int x ⇒ + - i32_to_int x ≤ i32_max ⇒ + ?y. i32_neg x = Return y /\ i32_to_int y = - i32_to_int x +Proof + prove_arith_unop_eq +QED + +Theorem i64_neg_eq: + !x y. + i64_min ≤ - i64_to_int x ⇒ + - i64_to_int x ≤ i64_max ⇒ + ?y. i64_neg x = Return y /\ i64_to_int y = - i64_to_int x +Proof + prove_arith_unop_eq +QED + +Theorem i128_neg_eq: + !x y. + i128_min ≤ - i128_to_int x ⇒ + - i128_to_int x ≤ i128_max ⇒ + ?y. i128_neg x = Return y /\ i128_to_int y = - i128_to_int x +Proof + prove_arith_unop_eq +QED + + fun prove_arith_op_eq (asms, g) = let val (_, t) = (dest_exists o snd o strip_imp o snd o strip_forall) g; @@ -565,7 +660,7 @@ fun prove_arith_op_eq (asms, g) = Theorem u8_add_eq: !x y. - u8_to_int x + u8_to_int y <= u8_max ==> + u8_to_int x + u8_to_int y <= u8_max ⇒ ?z. u8_add x y = Return z /\ u8_to_int z = u8_to_int x + u8_to_int y Proof prove_arith_op_eq @@ -573,7 +668,7 @@ QED Theorem u16_add_eq: !(x y). - u16_to_int x + u16_to_int y <= u16_max ==> + u16_to_int x + u16_to_int y <= u16_max ⇒ ?(z). u16_add x y = Return z /\ u16_to_int z = u16_to_int x + u16_to_int y Proof prove_arith_op_eq @@ -581,7 +676,7 @@ QED Theorem u32_add_eq: !x y. - u32_to_int x + u32_to_int y <= u32_max ==> + u32_to_int x + u32_to_int y <= u32_max ⇒ ?z. u32_add x y = Return z /\ u32_to_int z = u32_to_int x + u32_to_int y Proof prove_arith_op_eq @@ -589,7 +684,7 @@ QED Theorem u64_add_eq: !x y. - u64_to_int x + u64_to_int y <= u64_max ==> + u64_to_int x + u64_to_int y <= u64_max ⇒ ?z. u64_add x y = Return z /\ u64_to_int z = u64_to_int x + u64_to_int y Proof prove_arith_op_eq @@ -597,7 +692,7 @@ QED Theorem u128_add_eq: !x y. - u128_to_int x + u128_to_int y <= u128_max ==> + u128_to_int x + u128_to_int y <= u128_max ⇒ ?z. u128_add x y = Return z /\ u128_to_int z = u128_to_int x + u128_to_int y Proof prove_arith_op_eq @@ -605,7 +700,7 @@ QED Theorem usize_add_eq: !x y. - (usize_to_int x + usize_to_int y <= u16_max) \/ (usize_to_int x + usize_to_int y <= usize_max) ==> + (usize_to_int x + usize_to_int y <= u16_max) \/ (usize_to_int x + usize_to_int y <= usize_max) ⇒ ?z. usize_add x y = Return z /\ usize_to_int z = usize_to_int x + usize_to_int y Proof prove_arith_op_eq @@ -613,8 +708,8 @@ QED Theorem i8_add_eq: !x y. - i8_min <= i8_to_int x + i8_to_int y ==> - i8_to_int x + i8_to_int y <= i8_max ==> + i8_min <= i8_to_int x + i8_to_int y ⇒ + i8_to_int x + i8_to_int y <= i8_max ⇒ ?z. i8_add x y = Return z /\ i8_to_int z = i8_to_int x + i8_to_int y Proof prove_arith_op_eq @@ -622,8 +717,8 @@ QED Theorem i16_add_eq: !x y. - i16_min <= i16_to_int x + i16_to_int y ==> - i16_to_int x + i16_to_int y <= i16_max ==> + i16_min <= i16_to_int x + i16_to_int y ⇒ + i16_to_int x + i16_to_int y <= i16_max ⇒ ?z. i16_add x y = Return z /\ i16_to_int z = i16_to_int x + i16_to_int y Proof prove_arith_op_eq @@ -631,8 +726,8 @@ QED Theorem i32_add_eq: !x y. - i32_min <= i32_to_int x + i32_to_int y ==> - i32_to_int x + i32_to_int y <= i32_max ==> + i32_min <= i32_to_int x + i32_to_int y ⇒ + i32_to_int x + i32_to_int y <= i32_max ⇒ ?z. i32_add x y = Return z /\ i32_to_int z = i32_to_int x + i32_to_int y Proof prove_arith_op_eq @@ -640,8 +735,8 @@ QED Theorem i64_add_eq: !x y. - i64_min <= i64_to_int x + i64_to_int y ==> - i64_to_int x + i64_to_int y <= i64_max ==> + i64_min <= i64_to_int x + i64_to_int y ⇒ + i64_to_int x + i64_to_int y <= i64_max ⇒ ?z. i64_add x y = Return z /\ i64_to_int z = i64_to_int x + i64_to_int y Proof prove_arith_op_eq @@ -649,8 +744,8 @@ QED Theorem i128_add_eq: !x y. - i128_min <= i128_to_int x + i128_to_int y ==> - i128_to_int x + i128_to_int y <= i128_max ==> + i128_min <= i128_to_int x + i128_to_int y ⇒ + i128_to_int x + i128_to_int y <= i128_max ⇒ ?z. i128_add x y = Return z /\ i128_to_int z = i128_to_int x + i128_to_int y Proof prove_arith_op_eq @@ -658,8 +753,8 @@ QED Theorem isize_add_eq: !x y. - (i16_min <= isize_to_int x + isize_to_int y \/ isize_min <= isize_to_int x + isize_to_int y) ==> - (isize_to_int x + isize_to_int y <= i16_max \/ isize_to_int x + isize_to_int y <= isize_max) ==> + (i16_min <= isize_to_int x + isize_to_int y \/ isize_min <= isize_to_int x + isize_to_int y) ⇒ + (isize_to_int x + isize_to_int y <= i16_max \/ isize_to_int x + isize_to_int y <= isize_max) ⇒ ?z. isize_add x y = Return z /\ isize_to_int z = isize_to_int x + isize_to_int y Proof prove_arith_op_eq @@ -667,7 +762,7 @@ QED Theorem u8_sub_eq: !x y. - 0 <= u8_to_int x - u8_to_int y ==> + 0 <= u8_to_int x - u8_to_int y ⇒ ?z. u8_sub x y = Return z /\ u8_to_int z = u8_to_int x - u8_to_int y Proof prove_arith_op_eq @@ -675,7 +770,7 @@ QED Theorem u16_sub_eq: !x y. - 0 <= u16_to_int x - u16_to_int y ==> + 0 <= u16_to_int x - u16_to_int y ⇒ ?z. u16_sub x y = Return z /\ u16_to_int z = u16_to_int x - u16_to_int y Proof prove_arith_op_eq @@ -683,7 +778,7 @@ QED Theorem u32_sub_eq: !x y. - 0 <= u32_to_int x - u32_to_int y ==> + 0 <= u32_to_int x - u32_to_int y ⇒ ?z. u32_sub x y = Return z /\ u32_to_int z = u32_to_int x - u32_to_int y Proof prove_arith_op_eq @@ -691,7 +786,7 @@ QED Theorem u64_sub_eq: !x y. - 0 <= u64_to_int x - u64_to_int y ==> + 0 <= u64_to_int x - u64_to_int y ⇒ ?z. u64_sub x y = Return z /\ u64_to_int z = u64_to_int x - u64_to_int y Proof prove_arith_op_eq @@ -699,7 +794,7 @@ QED Theorem u128_sub_eq: !x y. - 0 <= u128_to_int x - u128_to_int y ==> + 0 <= u128_to_int x - u128_to_int y ⇒ ?z. u128_sub x y = Return z /\ u128_to_int z = u128_to_int x - u128_to_int y Proof prove_arith_op_eq @@ -707,7 +802,7 @@ QED Theorem usize_sub_eq: !x y. - 0 <= usize_to_int x - usize_to_int y ==> + 0 <= usize_to_int x - usize_to_int y ⇒ ?z. usize_sub x y = Return z /\ usize_to_int z = usize_to_int x - usize_to_int y Proof prove_arith_op_eq @@ -715,8 +810,8 @@ QED Theorem i8_sub_eq: !x y. - i8_min <= i8_to_int x - i8_to_int y ==> - i8_to_int x - i8_to_int y <= i8_max ==> + i8_min <= i8_to_int x - i8_to_int y ⇒ + i8_to_int x - i8_to_int y <= i8_max ⇒ ?z. i8_sub x y = Return z /\ i8_to_int z = i8_to_int x - i8_to_int y Proof prove_arith_op_eq @@ -724,8 +819,8 @@ QED Theorem i16_sub_eq: !x y. - i16_min <= i16_to_int x - i16_to_int y ==> - i16_to_int x - i16_to_int y <= i16_max ==> + i16_min <= i16_to_int x - i16_to_int y ⇒ + i16_to_int x - i16_to_int y <= i16_max ⇒ ?z. i16_sub x y = Return z /\ i16_to_int z = i16_to_int x - i16_to_int y Proof prove_arith_op_eq @@ -733,8 +828,8 @@ QED Theorem i32_sub_eq: !x y. - i32_min <= i32_to_int x - i32_to_int y ==> - i32_to_int x - i32_to_int y <= i32_max ==> + i32_min <= i32_to_int x - i32_to_int y ⇒ + i32_to_int x - i32_to_int y <= i32_max ⇒ ?z. i32_sub x y = Return z /\ i32_to_int z = i32_to_int x - i32_to_int y Proof prove_arith_op_eq @@ -742,8 +837,8 @@ QED Theorem i64_sub_eq: !x y. - i64_min <= i64_to_int x - i64_to_int y ==> - i64_to_int x - i64_to_int y <= i64_max ==> + i64_min <= i64_to_int x - i64_to_int y ⇒ + i64_to_int x - i64_to_int y <= i64_max ⇒ ?z. i64_sub x y = Return z /\ i64_to_int z = i64_to_int x - i64_to_int y Proof prove_arith_op_eq @@ -751,8 +846,8 @@ QED Theorem i128_sub_eq: !x y. - i128_min <= i128_to_int x - i128_to_int y ==> - i128_to_int x - i128_to_int y <= i128_max ==> + i128_min <= i128_to_int x - i128_to_int y ⇒ + i128_to_int x - i128_to_int y <= i128_max ⇒ ?z. i128_sub x y = Return z /\ i128_to_int z = i128_to_int x - i128_to_int y Proof prove_arith_op_eq @@ -760,8 +855,8 @@ QED Theorem isize_sub_eq: !x y. - (i16_min <= isize_to_int x - isize_to_int y \/ isize_min <= isize_to_int x - isize_to_int y) ==> - (isize_to_int x - isize_to_int y <= i16_max \/ isize_to_int x - isize_to_int y <= isize_max) ==> + (i16_min <= isize_to_int x - isize_to_int y \/ isize_min <= isize_to_int x - isize_to_int y) ⇒ + (isize_to_int x - isize_to_int y <= i16_max \/ isize_to_int x - isize_to_int y <= isize_max) ⇒ ?z. isize_sub x y = Return z /\ isize_to_int z = isize_to_int x - isize_to_int y Proof prove_arith_op_eq @@ -769,7 +864,7 @@ QED Theorem u8_mul_eq: !x y. - u8_to_int x * u8_to_int y <= u8_max ==> + u8_to_int x * u8_to_int y <= u8_max ⇒ ?z. u8_mul x y = Return z /\ u8_to_int z = u8_to_int x * u8_to_int y Proof prove_arith_op_eq @@ -777,7 +872,7 @@ QED Theorem u16_mul_eq: !x y. - u16_to_int x * u16_to_int y <= u16_max ==> + u16_to_int x * u16_to_int y <= u16_max ⇒ ?z. u16_mul x y = Return z /\ u16_to_int z = u16_to_int x * u16_to_int y Proof prove_arith_op_eq @@ -785,7 +880,7 @@ QED Theorem u32_mul_eq: !x y. - u32_to_int x * u32_to_int y <= u32_max ==> + u32_to_int x * u32_to_int y <= u32_max ⇒ ?z. u32_mul x y = Return z /\ u32_to_int z = u32_to_int x * u32_to_int y Proof prove_arith_op_eq @@ -793,7 +888,7 @@ QED Theorem u64_mul_eq: !x y. - u64_to_int x * u64_to_int y <= u64_max ==> + u64_to_int x * u64_to_int y <= u64_max ⇒ ?z. u64_mul x y = Return z /\ u64_to_int z = u64_to_int x * u64_to_int y Proof prove_arith_op_eq @@ -801,7 +896,7 @@ QED Theorem u128_mul_eq: !x y. - u128_to_int x * u128_to_int y <= u128_max ==> + u128_to_int x * u128_to_int y <= u128_max ⇒ ?z. u128_mul x y = Return z /\ u128_to_int z = u128_to_int x * u128_to_int y Proof prove_arith_op_eq @@ -809,7 +904,7 @@ QED Theorem usize_mul_eq: !x y. - (usize_to_int x * usize_to_int y <= u16_max) \/ (usize_to_int x * usize_to_int y <= usize_max) ==> + (usize_to_int x * usize_to_int y <= u16_max) \/ (usize_to_int x * usize_to_int y <= usize_max) ⇒ ?z. usize_mul x y = Return z /\ usize_to_int z = usize_to_int x * usize_to_int y Proof prove_arith_op_eq @@ -817,8 +912,8 @@ QED Theorem i8_mul_eq: !x y. - i8_min <= i8_to_int x * i8_to_int y ==> - i8_to_int x * i8_to_int y <= i8_max ==> + i8_min <= i8_to_int x * i8_to_int y ⇒ + i8_to_int x * i8_to_int y <= i8_max ⇒ ?z. i8_mul x y = Return z /\ i8_to_int z = i8_to_int x * i8_to_int y Proof prove_arith_op_eq @@ -826,8 +921,8 @@ QED Theorem i16_mul_eq: !x y. - i16_min <= i16_to_int x * i16_to_int y ==> - i16_to_int x * i16_to_int y <= i16_max ==> + i16_min <= i16_to_int x * i16_to_int y ⇒ + i16_to_int x * i16_to_int y <= i16_max ⇒ ?z. i16_mul x y = Return z /\ i16_to_int z = i16_to_int x * i16_to_int y Proof prove_arith_op_eq @@ -835,8 +930,8 @@ QED Theorem i32_mul_eq: !x y. - i32_min <= i32_to_int x * i32_to_int y ==> - i32_to_int x * i32_to_int y <= i32_max ==> + i32_min <= i32_to_int x * i32_to_int y ⇒ + i32_to_int x * i32_to_int y <= i32_max ⇒ ?z. i32_mul x y = Return z /\ i32_to_int z = i32_to_int x * i32_to_int y Proof prove_arith_op_eq @@ -844,8 +939,8 @@ QED Theorem i64_mul_eq: !x y. - i64_min <= i64_to_int x * i64_to_int y ==> - i64_to_int x * i64_to_int y <= i64_max ==> + i64_min <= i64_to_int x * i64_to_int y ⇒ + i64_to_int x * i64_to_int y <= i64_max ⇒ ?z. i64_mul x y = Return z /\ i64_to_int z = i64_to_int x * i64_to_int y Proof prove_arith_op_eq @@ -853,8 +948,8 @@ QED Theorem i128_mul_eq: !x y. - i128_min <= i128_to_int x * i128_to_int y ==> - i128_to_int x * i128_to_int y <= i128_max ==> + i128_min <= i128_to_int x * i128_to_int y ⇒ + i128_to_int x * i128_to_int y <= i128_max ⇒ ?z. i128_mul x y = Return z /\ i128_to_int z = i128_to_int x * i128_to_int y Proof prove_arith_op_eq @@ -862,8 +957,8 @@ QED Theorem isize_mul_eq: !x y. - (i16_min <= isize_to_int x * isize_to_int y \/ isize_min <= isize_to_int x * isize_to_int y) ==> - (isize_to_int x * isize_to_int y <= i16_max \/ isize_to_int x * isize_to_int y <= isize_max) ==> + (i16_min <= isize_to_int x * isize_to_int y \/ isize_min <= isize_to_int x * isize_to_int y) ⇒ + (isize_to_int x * isize_to_int y <= i16_max \/ isize_to_int x * isize_to_int y <= isize_max) ⇒ ?z. isize_mul x y = Return z /\ isize_to_int z = isize_to_int x * isize_to_int y Proof prove_arith_op_eq @@ -871,7 +966,7 @@ QED Theorem u8_div_eq: !x y. - u8_to_int y <> 0 ==> + u8_to_int y <> 0 ⇒ ?z. u8_div x y = Return z /\ u8_to_int z = u8_to_int x / u8_to_int y Proof prove_arith_op_eq @@ -879,7 +974,7 @@ QED Theorem u16_div_eq: !x y. - u16_to_int y <> 0 ==> + u16_to_int y <> 0 ⇒ ?z. u16_div x y = Return z /\ u16_to_int z = u16_to_int x / u16_to_int y Proof prove_arith_op_eq @@ -887,7 +982,7 @@ QED Theorem u32_div_eq: !x y. - u32_to_int y <> 0 ==> + u32_to_int y <> 0 ⇒ ?z. u32_div x y = Return z /\ u32_to_int z = u32_to_int x / u32_to_int y Proof prove_arith_op_eq @@ -895,7 +990,7 @@ QED Theorem u64_div_eq: !x y. - u64_to_int y <> 0 ==> + u64_to_int y <> 0 ⇒ ?z. u64_div x y = Return z /\ u64_to_int z = u64_to_int x / u64_to_int y Proof prove_arith_op_eq @@ -903,7 +998,7 @@ QED Theorem u128_div_eq: !x y. - u128_to_int y <> 0 ==> + u128_to_int y <> 0 ⇒ ?z. u128_div x y = Return z /\ u128_to_int z = u128_to_int x / u128_to_int y Proof prove_arith_op_eq @@ -911,7 +1006,7 @@ QED Theorem usize_div_eq: !x y. - usize_to_int y <> 0 ==> + usize_to_int y <> 0 ⇒ ?z. usize_div x y = Return z /\ usize_to_int z = usize_to_int x / usize_to_int y Proof prove_arith_op_eq @@ -919,9 +1014,9 @@ QED Theorem i8_div_eq: !x y. - i8_to_int y <> 0 ==> - i8_min <= i8_to_int x / i8_to_int y ==> - i8_to_int x / i8_to_int y <= i8_max ==> + i8_to_int y <> 0 ⇒ + i8_min <= i8_to_int x / i8_to_int y ⇒ + i8_to_int x / i8_to_int y <= i8_max ⇒ ?z. i8_div x y = Return z /\ i8_to_int z = i8_to_int x / i8_to_int y Proof prove_arith_op_eq @@ -929,9 +1024,9 @@ QED Theorem i16_div_eq: !x y. - i16_to_int y <> 0 ==> - i16_min <= i16_to_int x / i16_to_int y ==> - i16_to_int x / i16_to_int y <= i16_max ==> + i16_to_int y <> 0 ⇒ + i16_min <= i16_to_int x / i16_to_int y ⇒ + i16_to_int x / i16_to_int y <= i16_max ⇒ ?z. i16_div x y = Return z /\ i16_to_int z = i16_to_int x / i16_to_int y Proof prove_arith_op_eq @@ -939,9 +1034,9 @@ QED Theorem i32_div_eq: !x y. - i32_to_int y <> 0 ==> - i32_min <= i32_to_int x / i32_to_int y ==> - i32_to_int x / i32_to_int y <= i32_max ==> + i32_to_int y <> 0 ⇒ + i32_min <= i32_to_int x / i32_to_int y ⇒ + i32_to_int x / i32_to_int y <= i32_max ⇒ ?z. i32_div x y = Return z /\ i32_to_int z = i32_to_int x / i32_to_int y Proof prove_arith_op_eq @@ -949,9 +1044,9 @@ QED Theorem i64_div_eq: !x y. - i64_to_int y <> 0 ==> - i64_min <= i64_to_int x / i64_to_int y ==> - i64_to_int x / i64_to_int y <= i64_max ==> + i64_to_int y <> 0 ⇒ + i64_min <= i64_to_int x / i64_to_int y ⇒ + i64_to_int x / i64_to_int y <= i64_max ⇒ ?z. i64_div x y = Return z /\ i64_to_int z = i64_to_int x / i64_to_int y Proof prove_arith_op_eq @@ -959,9 +1054,9 @@ QED Theorem i128_div_eq: !x y. - i128_to_int y <> 0 ==> - i128_min <= i128_to_int x / i128_to_int y ==> - i128_to_int x / i128_to_int y <= i128_max ==> + i128_to_int y <> 0 ⇒ + i128_min <= i128_to_int x / i128_to_int y ⇒ + i128_to_int x / i128_to_int y <= i128_max ⇒ ?z. i128_div x y = Return z /\ i128_to_int z = i128_to_int x / i128_to_int y Proof prove_arith_op_eq @@ -969,9 +1064,9 @@ QED Theorem isize_div_eq: !x y. - isize_to_int y <> 0 ==> - (i16_min <= isize_to_int x / isize_to_int y \/ isize_min <= isize_to_int x / isize_to_int y) ==> - (isize_to_int x / isize_to_int y <= i16_max \/ isize_to_int x / isize_to_int y <= isize_max) ==> + isize_to_int y <> 0 ⇒ + (i16_min <= isize_to_int x / isize_to_int y \/ isize_min <= isize_to_int x / isize_to_int y) ⇒ + (isize_to_int x / isize_to_int y <= i16_max \/ isize_to_int x / isize_to_int y <= isize_max) ⇒ ?z. isize_div x y = Return z /\ isize_to_int z = isize_to_int x / isize_to_int y Proof prove_arith_op_eq @@ -979,7 +1074,7 @@ QED Theorem u8_rem_eq: !x y. - u8_to_int y <> 0 ==> + u8_to_int y <> 0 ⇒ ?z. u8_rem x y = Return z /\ u8_to_int z = int_rem (u8_to_int x) (u8_to_int y) Proof prove_arith_op_eq @@ -987,7 +1082,7 @@ QED Theorem u16_rem_eq: !x y. - u16_to_int y <> 0 ==> + u16_to_int y <> 0 ⇒ ?z. u16_rem x y = Return z /\ u16_to_int z = int_rem (u16_to_int x) (u16_to_int y) Proof prove_arith_op_eq @@ -995,7 +1090,7 @@ QED Theorem u32_rem_eq: !x y. - u32_to_int y <> 0 ==> + u32_to_int y <> 0 ⇒ ?z. u32_rem x y = Return z /\ u32_to_int z = int_rem (u32_to_int x) (u32_to_int y) Proof prove_arith_op_eq @@ -1003,7 +1098,7 @@ QED Theorem u64_rem_eq: !x y. - u64_to_int y <> 0 ==> + u64_to_int y <> 0 ⇒ ?z. u64_rem x y = Return z /\ u64_to_int z = int_rem (u64_to_int x) (u64_to_int y) Proof prove_arith_op_eq @@ -1011,7 +1106,7 @@ QED Theorem u128_rem_eq: !x y. - u128_to_int y <> 0 ==> + u128_to_int y <> 0 ⇒ ?z. u128_rem x y = Return z /\ u128_to_int z = int_rem (u128_to_int x) (u128_to_int y) Proof prove_arith_op_eq @@ -1019,7 +1114,7 @@ QED Theorem usize_rem_eq: !x y. - usize_to_int y <> 0 ==> + usize_to_int y <> 0 ⇒ ?z. usize_rem x y = Return z /\ usize_to_int z = int_rem (usize_to_int x) (usize_to_int y) Proof prove_arith_op_eq @@ -1027,9 +1122,9 @@ QED Theorem i8_rem_eq: !x y. - i8_to_int y <> 0 ==> - i8_min <= int_rem (i8_to_int x) (i8_to_int y) ==> - int_rem (i8_to_int x) (i8_to_int y) <= i8_max ==> + i8_to_int y <> 0 ⇒ + i8_min <= int_rem (i8_to_int x) (i8_to_int y) ⇒ + int_rem (i8_to_int x) (i8_to_int y) <= i8_max ⇒ ?z. i8_rem x y = Return z /\ i8_to_int z = int_rem (i8_to_int x) (i8_to_int y) Proof prove_arith_op_eq @@ -1037,9 +1132,9 @@ QED Theorem i16_rem_eq: !x y. - i16_to_int y <> 0 ==> - i16_min <= int_rem (i16_to_int x) (i16_to_int y) ==> - int_rem (i16_to_int x) (i16_to_int y) <= i16_max ==> + i16_to_int y <> 0 ⇒ + i16_min <= int_rem (i16_to_int x) (i16_to_int y) ⇒ + int_rem (i16_to_int x) (i16_to_int y) <= i16_max ⇒ ?z. i16_rem x y = Return z /\ i16_to_int z = int_rem (i16_to_int x) (i16_to_int y) Proof prove_arith_op_eq @@ -1047,9 +1142,9 @@ QED Theorem i32_rem_eq: !x y. - i32_to_int y <> 0 ==> - i32_min <= int_rem (i32_to_int x) (i32_to_int y) ==> - int_rem (i32_to_int x) (i32_to_int y) <= i32_max ==> + i32_to_int y <> 0 ⇒ + i32_min <= int_rem (i32_to_int x) (i32_to_int y) ⇒ + int_rem (i32_to_int x) (i32_to_int y) <= i32_max ⇒ ?z. i32_rem x y = Return z /\ i32_to_int z = int_rem (i32_to_int x) (i32_to_int y) Proof prove_arith_op_eq @@ -1057,9 +1152,9 @@ QED Theorem i64_rem_eq: !x y. - i64_to_int y <> 0 ==> - i64_min <= int_rem (i64_to_int x) (i64_to_int y) ==> - int_rem (i64_to_int x) (i64_to_int y) <= i64_max ==> + i64_to_int y <> 0 ⇒ + i64_min <= int_rem (i64_to_int x) (i64_to_int y) ⇒ + int_rem (i64_to_int x) (i64_to_int y) <= i64_max ⇒ ?z. i64_rem x y = Return z /\ i64_to_int z = int_rem (i64_to_int x) (i64_to_int y) Proof prove_arith_op_eq @@ -1067,9 +1162,9 @@ QED Theorem i128_rem_eq: !x y. - i128_to_int y <> 0 ==> - i128_min <= int_rem (i128_to_int x) (i128_to_int y) ==> - int_rem (i128_to_int x) (i128_to_int y) <= i128_max ==> + i128_to_int y <> 0 ⇒ + i128_min <= int_rem (i128_to_int x) (i128_to_int y) ⇒ + int_rem (i128_to_int x) (i128_to_int y) <= i128_max ⇒ ?z. i128_rem x y = Return z /\ i128_to_int z = int_rem (i128_to_int x) (i128_to_int y) Proof prove_arith_op_eq @@ -1077,16 +1172,208 @@ QED Theorem isize_rem_eq: !x y. - isize_to_int y <> 0 ==> + isize_to_int y <> 0 ⇒ (i16_min <= int_rem (isize_to_int x) (isize_to_int y) \/ - isize_min <= int_rem (isize_to_int x) (isize_to_int y)) ==> + isize_min <= int_rem (isize_to_int x) (isize_to_int y)) ⇒ (int_rem (isize_to_int x) (isize_to_int y) <= i16_max \/ - int_rem (isize_to_int x) (isize_to_int y) <= isize_max) ==> + int_rem (isize_to_int x) (isize_to_int y) <= isize_max) ⇒ ?z. isize_rem x y = Return z /\ isize_to_int z = int_rem (isize_to_int x) (isize_to_int y) Proof prove_arith_op_eq QED +Definition u8_lt_def: + u8_lt x y = (u8_to_int x < u8_to_int y) +End + +Definition u16_lt_def: + u16_lt x y = (u16_to_int x < u16_to_int y) +End + +Definition u32_lt_def: + u32_lt x y = (u32_to_int x < u32_to_int y) +End + +Definition u64_lt_def: + u64_lt x y = (u64_to_int x < u64_to_int y) +End + +Definition u128_lt_def: + u128_lt x y = (u128_to_int x < u128_to_int y) +End + +Definition usize_lt_def: + usize_lt x y = (usize_to_int x < usize_to_int y) +End + +Definition i8_lt_def: + i8_lt x y = (i8_to_int x < i8_to_int y) +End + +Definition i16_lt_def: + i16_lt x y = (i16_to_int x < i16_to_int y) +End + +Definition i32_lt_def: + i32_lt x y = (i32_to_int x < i32_to_int y) +End + +Definition i64_lt_def: + i64_lt x y = (i64_to_int x < i64_to_int y) +End + +Definition i128_lt_def: + i128_lt x y = (i128_to_int x < i128_to_int y) +End + +Definition isize_lt_def: + isize_lt x y = (isize_to_int x < isize_to_int y) +End + +Definition u8_le_def: + u8_le x y = (u8_to_int x ≤ u8_to_int y) +End + +Definition u16_le_def: + u16_le x y = (u16_to_int x ≤ u16_to_int y) +End + +Definition u32_le_def: + u32_le x y = (u32_to_int x ≤ u32_to_int y) +End + +Definition u64_le_def: + u64_le x y = (u64_to_int x ≤ u64_to_int y) +End + +Definition u128_le_def: + u128_le x y = (u128_to_int x ≤ u128_to_int y) +End + +Definition usize_le_def: + usize_le x y = (usize_to_int x ≤ usize_to_int y) +End + +Definition i8_le_def: + i8_le x y = (i8_to_int x ≤ i8_to_int y) +End + +Definition i16_le_def: + i16_le x y = (i16_to_int x ≤ i16_to_int y) +End + +Definition i32_le_def: + i32_le x y = (i32_to_int x ≤ i32_to_int y) +End + +Definition i64_le_def: + i64_le x y = (i64_to_int x ≤ i64_to_int y) +End + +Definition i128_le_def: + i128_le x y = (i128_to_int x ≤ i128_to_int y) +End + +Definition isize_le_def: + isize_le x y = (isize_to_int x ≤ isize_to_int y) +End + +Definition u8_gt_def: + u8_gt x y = (u8_to_int x > u8_to_int y) +End + +Definition u16_gt_def: + u16_gt x y = (u16_to_int x > u16_to_int y) +End + +Definition u32_gt_def: + u32_gt x y = (u32_to_int x > u32_to_int y) +End + +Definition u64_gt_def: + u64_gt x y = (u64_to_int x > u64_to_int y) +End + +Definition u128_gt_def: + u128_gt x y = (u128_to_int x > u128_to_int y) +End + +Definition usize_gt_def: + usize_gt x y = (usize_to_int x > usize_to_int y) +End + +Definition i8_gt_def: + i8_gt x y = (i8_to_int x > i8_to_int y) +End + +Definition i16_gt_def: + i16_gt x y = (i16_to_int x > i16_to_int y) +End + +Definition i32_gt_def: + i32_gt x y = (i32_to_int x > i32_to_int y) +End + +Definition i64_gt_def: + i64_gt x y = (i64_to_int x > i64_to_int y) +End + +Definition i128_gt_def: + i128_gt x y = (i128_to_int x > i128_to_int y) +End + +Definition isize_gt_def: + isize_gt x y = (isize_to_int x > isize_to_int y) +End + +Definition u8_ge_def: + u8_ge x y = (u8_to_int x >= u8_to_int y) +End + +Definition u16_ge_def: + u16_ge x y = (u16_to_int x >= u16_to_int y) +End + +Definition u32_ge_def: + u32_ge x y = (u32_to_int x >= u32_to_int y) +End + +Definition u64_ge_def: + u64_ge x y = (u64_to_int x >= u64_to_int y) +End + +Definition u128_ge_def: + u128_ge x y = (u128_to_int x >= u128_to_int y) +End + +Definition usize_ge_def: + usize_ge x y = (usize_to_int x >= usize_to_int y) +End + +Definition i8_ge_def: + i8_ge x y = (i8_to_int x >= i8_to_int y) +End + +Definition i16_ge_def: + i16_ge x y = (i16_to_int x >= i16_to_int y) +End + +Definition i32_ge_def: + i32_ge x y = (i32_to_int x >= i32_to_int y) +End + +Definition i64_ge_def: + i64_ge x y = (i64_to_int x >= i64_to_int y) +End + +Definition i128_ge_def: + i128_ge x y = (i128_to_int x >= i128_to_int y) +End + +Definition isize_ge_def: + isize_ge x y = (isize_to_int x >= isize_to_int y) +End + (*** * Vectors @@ -1109,8 +1396,8 @@ QED Theorem update_spec: ∀ls i y. - 0 <= i ==> - i < len ls ==> + 0 <= i ⇒ + i < len ls ⇒ len (update ls i y) = len ls ∧ index i (update ls i y) = y ∧ ∀j. j < len ls ⇒ j ≠ i ⇒ index j (update ls i y) = index j ls @@ -1131,8 +1418,8 @@ QED Theorem index_update_same: ∀ls i j y. - 0 <= i ==> - i < len ls ==> + 0 <= i ⇒ + i < len ls ⇒ j < len ls ⇒ j ≠ i ⇒ index j (update ls i y) = index j ls Proof rpt strip_tac >> @@ -1142,8 +1429,8 @@ QED Theorem index_update_diff: ∀ls i j y. - 0 <= i ==> - i < len ls ==> + 0 <= i ⇒ + i < len ls ⇒ index i (update ls i y) = y Proof rpt strip_tac >> diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig index fdf28172..3b029c05 100644 --- a/backends/hol4/primitivesTheory.sig +++ b/backends/hol4/primitivesTheory.sig @@ -50,46 +50,77 @@ sig val error_CASE : thm val error_TY_DEF : thm val error_size_def : thm + val get_return_value_def : thm val i128_add_def : thm val i128_div_def : thm + val i128_ge_def : thm + val i128_gt_def : thm + val i128_le_def : thm + val i128_lt_def : thm val i128_max_def : thm val i128_min_def : thm val i128_mul_def : thm + val i128_neg_def : thm val i128_rem_def : thm val i128_sub_def : thm val i16_add_def : thm val i16_div_def : thm + val i16_ge_def : thm + val i16_gt_def : thm + val i16_le_def : thm + val i16_lt_def : thm val i16_max_def : thm val i16_min_def : thm val i16_mul_def : thm + val i16_neg_def : thm val i16_rem_def : thm val i16_sub_def : thm val i32_add_def : thm val i32_div_def : thm + val i32_ge_def : thm + val i32_gt_def : thm + val i32_le_def : thm + val i32_lt_def : thm val i32_max_def : thm val i32_min_def : thm val i32_mul_def : thm + val i32_neg_def : thm val i32_rem_def : thm val i32_sub_def : thm val i64_add_def : thm val i64_div_def : thm + val i64_ge_def : thm + val i64_gt_def : thm + val i64_le_def : thm + val i64_lt_def : thm val i64_max_def : thm val i64_min_def : thm val i64_mul_def : thm + val i64_neg_def : thm val i64_rem_def : thm val i64_sub_def : thm val i8_add_def : thm val i8_div_def : thm + val i8_ge_def : thm + val i8_gt_def : thm + val i8_le_def : thm + val i8_lt_def : thm val i8_max_def : thm val i8_min_def : thm val i8_mul_def : thm + val i8_neg_def : thm val i8_rem_def : thm val i8_sub_def : thm val int_rem_def : thm val is_diverge_def : thm val isize_add_def : thm val isize_div_def : thm + val isize_ge_def : thm + val isize_gt_def : thm + val isize_le_def : thm + val isize_lt_def : thm val isize_mul_def : thm + val isize_neg_def : thm val isize_rem_def : thm val isize_sub_def : thm val massert_def : thm @@ -113,36 +144,60 @@ sig val return_def : thm val u128_add_def : thm val u128_div_def : thm + val u128_ge_def : thm + val u128_gt_def : thm + val u128_le_def : thm + val u128_lt_def : thm val u128_max_def : thm val u128_mul_def : thm val u128_rem_def : thm val u128_sub_def : thm val u16_add_def : thm val u16_div_def : thm + val u16_ge_def : thm + val u16_gt_def : thm + val u16_le_def : thm + val u16_lt_def : thm val u16_max_def : thm val u16_mul_def : thm val u16_rem_def : thm val u16_sub_def : thm val u32_add_def : thm val u32_div_def : thm + val u32_ge_def : thm + val u32_gt_def : thm + val u32_le_def : thm + val u32_lt_def : thm val u32_max_def : thm val u32_mul_def : thm val u32_rem_def : thm val u32_sub_def : thm val u64_add_def : thm val u64_div_def : thm + val u64_ge_def : thm + val u64_gt_def : thm + val u64_le_def : thm + val u64_lt_def : thm val u64_max_def : thm val u64_mul_def : thm val u64_rem_def : thm val u64_sub_def : thm val u8_add_def : thm val u8_div_def : thm + val u8_ge_def : thm + val u8_gt_def : thm + val u8_le_def : thm + val u8_lt_def : thm val u8_max_def : thm val u8_mul_def : thm val u8_rem_def : thm val u8_sub_def : thm val usize_add_def : thm val usize_div_def : thm + val usize_ge_def : thm + val usize_gt_def : thm + val usize_le_def : thm + val usize_lt_def : thm val usize_mul_def : thm val usize_rem_def : thm val usize_sub_def : thm @@ -167,26 +222,31 @@ sig val i128_add_eq : thm val i128_div_eq : thm val i128_mul_eq : thm + val i128_neg_eq : thm val i128_rem_eq : thm val i128_sub_eq : thm val i16_add_eq : thm val i16_div_eq : thm val i16_mul_eq : thm + val i16_neg_eq : thm val i16_rem_eq : thm val i16_sub_eq : thm val i32_add_eq : thm val i32_div_eq : thm val i32_mul_eq : thm + val i32_neg_eq : thm val i32_rem_eq : thm val i32_sub_eq : thm val i64_add_eq : thm val i64_div_eq : thm val i64_mul_eq : thm + val i64_neg_eq : thm val i64_rem_eq : thm val i64_sub_eq : thm val i8_add_eq : thm val i8_div_eq : thm val i8_mul_eq : thm + val i8_neg_eq : thm val i8_rem_eq : thm val i8_sub_eq : thm val index_update_diff : thm @@ -194,6 +254,7 @@ sig val isize_add_eq : thm val isize_div_eq : thm val isize_mul_eq : thm + val isize_neg_eq : thm val isize_rem_eq : thm val isize_sub_eq : thm val num2error_11 : thm @@ -471,6 +532,10 @@ sig ⊢ ∀x. error_size x = 0 + [get_return_value_def] Definition + + ⊢ ∀x. get_return_value (Return x) = x + [i128_add_def] Definition ⊢ ∀x y. i128_add x y = mk_i128 (i128_to_int x + i128_to_int y) @@ -482,6 +547,22 @@ sig if i128_to_int y = 0 then Fail Failure else mk_i128 (i128_to_int x / i128_to_int y) + [i128_ge_def] Definition + + ⊢ ∀x y. i128_ge x y ⇔ i128_to_int x ≥ i128_to_int y + + [i128_gt_def] Definition + + ⊢ ∀x y. i128_gt x y ⇔ i128_to_int x > i128_to_int y + + [i128_le_def] Definition + + ⊢ ∀x y. i128_le x y ⇔ i128_to_int x ≤ i128_to_int y + + [i128_lt_def] Definition + + ⊢ ∀x y. i128_lt x y ⇔ i128_to_int x < i128_to_int y + [i128_max_def] Definition ⊢ i128_max = 170141183460469231731687303715884105727 @@ -494,6 +575,10 @@ sig ⊢ ∀x y. i128_mul x y = mk_i128 (i128_to_int x * i128_to_int y) + [i128_neg_def] Definition + + ⊢ ∀x. i128_neg x = mk_i128 (-i128_to_int x) + [i128_rem_def] Definition ⊢ ∀x y. @@ -516,6 +601,22 @@ sig if i16_to_int y = 0 then Fail Failure else mk_i16 (i16_to_int x / i16_to_int y) + [i16_ge_def] Definition + + ⊢ ∀x y. i16_ge x y ⇔ i16_to_int x ≥ i16_to_int y + + [i16_gt_def] Definition + + ⊢ ∀x y. i16_gt x y ⇔ i16_to_int x > i16_to_int y + + [i16_le_def] Definition + + ⊢ ∀x y. i16_le x y ⇔ i16_to_int x ≤ i16_to_int y + + [i16_lt_def] Definition + + ⊢ ∀x y. i16_lt x y ⇔ i16_to_int x < i16_to_int y + [i16_max_def] Definition ⊢ i16_max = 32767 @@ -528,6 +629,10 @@ sig ⊢ ∀x y. i16_mul x y = mk_i16 (i16_to_int x * i16_to_int y) + [i16_neg_def] Definition + + ⊢ ∀x. i16_neg x = mk_i16 (-i16_to_int x) + [i16_rem_def] Definition ⊢ ∀x y. @@ -550,6 +655,22 @@ sig if i32_to_int y = 0 then Fail Failure else mk_i32 (i32_to_int x / i32_to_int y) + [i32_ge_def] Definition + + ⊢ ∀x y. i32_ge x y ⇔ i32_to_int x ≥ i32_to_int y + + [i32_gt_def] Definition + + ⊢ ∀x y. i32_gt x y ⇔ i32_to_int x > i32_to_int y + + [i32_le_def] Definition + + ⊢ ∀x y. i32_le x y ⇔ i32_to_int x ≤ i32_to_int y + + [i32_lt_def] Definition + + ⊢ ∀x y. i32_lt x y ⇔ i32_to_int x < i32_to_int y + [i32_max_def] Definition ⊢ i32_max = 2147483647 @@ -562,6 +683,10 @@ sig ⊢ ∀x y. i32_mul x y = mk_i32 (i32_to_int x * i32_to_int y) + [i32_neg_def] Definition + + ⊢ ∀x. i32_neg x = mk_i32 (-i32_to_int x) + [i32_rem_def] Definition ⊢ ∀x y. @@ -584,6 +709,22 @@ sig if i64_to_int y = 0 then Fail Failure else mk_i64 (i64_to_int x / i64_to_int y) + [i64_ge_def] Definition + + ⊢ ∀x y. i64_ge x y ⇔ i64_to_int x ≥ i64_to_int y + + [i64_gt_def] Definition + + ⊢ ∀x y. i64_gt x y ⇔ i64_to_int x > i64_to_int y + + [i64_le_def] Definition + + ⊢ ∀x y. i64_le x y ⇔ i64_to_int x ≤ i64_to_int y + + [i64_lt_def] Definition + + ⊢ ∀x y. i64_lt x y ⇔ i64_to_int x < i64_to_int y + [i64_max_def] Definition ⊢ i64_max = 9223372036854775807 @@ -596,6 +737,10 @@ sig ⊢ ∀x y. i64_mul x y = mk_i64 (i64_to_int x * i64_to_int y) + [i64_neg_def] Definition + + ⊢ ∀x. i64_neg x = mk_i64 (-i64_to_int x) + [i64_rem_def] Definition ⊢ ∀x y. @@ -618,6 +763,22 @@ sig if i8_to_int y = 0 then Fail Failure else mk_i8 (i8_to_int x / i8_to_int y) + [i8_ge_def] Definition + + ⊢ ∀x y. i8_ge x y ⇔ i8_to_int x ≥ i8_to_int y + + [i8_gt_def] Definition + + ⊢ ∀x y. i8_gt x y ⇔ i8_to_int x > i8_to_int y + + [i8_le_def] Definition + + ⊢ ∀x y. i8_le x y ⇔ i8_to_int x ≤ i8_to_int y + + [i8_lt_def] Definition + + ⊢ ∀x y. i8_lt x y ⇔ i8_to_int x < i8_to_int y + [i8_max_def] Definition ⊢ i8_max = 127 @@ -630,6 +791,10 @@ sig ⊢ ∀x y. i8_mul x y = mk_i8 (i8_to_int x * i8_to_int y) + [i8_neg_def] Definition + + ⊢ ∀x. i8_neg x = mk_i8 (-i8_to_int x) + [i8_rem_def] Definition ⊢ ∀x y. @@ -663,10 +828,30 @@ sig if isize_to_int y = 0 then Fail Failure else mk_isize (isize_to_int x / isize_to_int y) + [isize_ge_def] Definition + + ⊢ ∀x y. isize_ge x y ⇔ isize_to_int x ≥ isize_to_int y + + [isize_gt_def] Definition + + ⊢ ∀x y. isize_gt x y ⇔ isize_to_int x > isize_to_int y + + [isize_le_def] Definition + + ⊢ ∀x y. isize_le x y ⇔ isize_to_int x ≤ isize_to_int y + + [isize_lt_def] Definition + + ⊢ ∀x y. isize_lt x y ⇔ isize_to_int x < isize_to_int y + [isize_mul_def] Definition ⊢ ∀x y. isize_mul x y = mk_isize (isize_to_int x * isize_to_int y) + [isize_neg_def] Definition + + ⊢ ∀x. isize_neg x = mk_isize (-isize_to_int x) + [isize_rem_def] Definition ⊢ ∀x y. @@ -810,6 +995,22 @@ sig if u128_to_int y = 0 then Fail Failure else mk_u128 (u128_to_int x / u128_to_int y) + [u128_ge_def] Definition + + ⊢ ∀x y. u128_ge x y ⇔ u128_to_int x ≥ u128_to_int y + + [u128_gt_def] Definition + + ⊢ ∀x y. u128_gt x y ⇔ u128_to_int x > u128_to_int y + + [u128_le_def] Definition + + ⊢ ∀x y. u128_le x y ⇔ u128_to_int x ≤ u128_to_int y + + [u128_lt_def] Definition + + ⊢ ∀x y. u128_lt x y ⇔ u128_to_int x < u128_to_int y + [u128_max_def] Definition ⊢ u128_max = 340282366920938463463374607431768211455 @@ -840,6 +1041,22 @@ sig if u16_to_int y = 0 then Fail Failure else mk_u16 (u16_to_int x / u16_to_int y) + [u16_ge_def] Definition + + ⊢ ∀x y. u16_ge x y ⇔ u16_to_int x ≥ u16_to_int y + + [u16_gt_def] Definition + + ⊢ ∀x y. u16_gt x y ⇔ u16_to_int x > u16_to_int y + + [u16_le_def] Definition + + ⊢ ∀x y. u16_le x y ⇔ u16_to_int x ≤ u16_to_int y + + [u16_lt_def] Definition + + ⊢ ∀x y. u16_lt x y ⇔ u16_to_int x < u16_to_int y + [u16_max_def] Definition ⊢ u16_max = 65535 @@ -870,6 +1087,22 @@ sig if u32_to_int y = 0 then Fail Failure else mk_u32 (u32_to_int x / u32_to_int y) + [u32_ge_def] Definition + + ⊢ ∀x y. u32_ge x y ⇔ u32_to_int x ≥ u32_to_int y + + [u32_gt_def] Definition + + ⊢ ∀x y. u32_gt x y ⇔ u32_to_int x > u32_to_int y + + [u32_le_def] Definition + + ⊢ ∀x y. u32_le x y ⇔ u32_to_int x ≤ u32_to_int y + + [u32_lt_def] Definition + + ⊢ ∀x y. u32_lt x y ⇔ u32_to_int x < u32_to_int y + [u32_max_def] Definition ⊢ u32_max = 4294967295 @@ -900,6 +1133,22 @@ sig if u64_to_int y = 0 then Fail Failure else mk_u64 (u64_to_int x / u64_to_int y) + [u64_ge_def] Definition + + ⊢ ∀x y. u64_ge x y ⇔ u64_to_int x ≥ u64_to_int y + + [u64_gt_def] Definition + + ⊢ ∀x y. u64_gt x y ⇔ u64_to_int x > u64_to_int y + + [u64_le_def] Definition + + ⊢ ∀x y. u64_le x y ⇔ u64_to_int x ≤ u64_to_int y + + [u64_lt_def] Definition + + ⊢ ∀x y. u64_lt x y ⇔ u64_to_int x < u64_to_int y + [u64_max_def] Definition ⊢ u64_max = 18446744073709551615 @@ -930,6 +1179,22 @@ sig if u8_to_int y = 0 then Fail Failure else mk_u8 (u8_to_int x / u8_to_int y) + [u8_ge_def] Definition + + ⊢ ∀x y. u8_ge x y ⇔ u8_to_int x ≥ u8_to_int y + + [u8_gt_def] Definition + + ⊢ ∀x y. u8_gt x y ⇔ u8_to_int x > u8_to_int y + + [u8_le_def] Definition + + ⊢ ∀x y. u8_le x y ⇔ u8_to_int x ≤ u8_to_int y + + [u8_lt_def] Definition + + ⊢ ∀x y. u8_lt x y ⇔ u8_to_int x < u8_to_int y + [u8_max_def] Definition ⊢ u8_max = 255 @@ -960,6 +1225,22 @@ sig if usize_to_int y = 0 then Fail Failure else mk_usize (usize_to_int x / usize_to_int y) + [usize_ge_def] Definition + + ⊢ ∀x y. usize_ge x y ⇔ usize_to_int x ≥ usize_to_int y + + [usize_gt_def] Definition + + ⊢ ∀x y. usize_gt x y ⇔ usize_to_int x > usize_to_int y + + [usize_le_def] Definition + + ⊢ ∀x y. usize_le x y ⇔ usize_to_int x ≤ usize_to_int y + + [usize_lt_def] Definition + + ⊢ ∀x y. usize_lt x y ⇔ usize_to_int x < usize_to_int y + [usize_mul_def] Definition ⊢ ∀x y. usize_mul x y = mk_usize (usize_to_int x * usize_to_int y) @@ -1078,6 +1359,15 @@ sig ∃z. i128_mul x y = Return z ∧ i128_to_int z = i128_to_int x * i128_to_int y + [i128_neg_eq] Theorem + + [oracles: DISK_THM] [axioms: i128_to_int_int_to_i128, isize_bounds] + [] + ⊢ ∀x y. + i128_min ≤ -i128_to_int x ⇒ + -i128_to_int x ≤ i128_max ⇒ + ∃y. i128_neg x = Return y ∧ i128_to_int y = -i128_to_int x + [i128_rem_eq] Theorem [oracles: DISK_THM] @@ -1131,6 +1421,14 @@ sig ∃z. i16_mul x y = Return z ∧ i16_to_int z = i16_to_int x * i16_to_int y + [i16_neg_eq] Theorem + + [oracles: DISK_THM] [axioms: i16_to_int_int_to_i16, isize_bounds] [] + ⊢ ∀x y. + i16_min ≤ -i16_to_int x ⇒ + -i16_to_int x ≤ i16_max ⇒ + ∃y. i16_neg x = Return y ∧ i16_to_int y = -i16_to_int x + [i16_rem_eq] Theorem [oracles: DISK_THM] @@ -1184,6 +1482,14 @@ sig ∃z. i32_mul x y = Return z ∧ i32_to_int z = i32_to_int x * i32_to_int y + [i32_neg_eq] Theorem + + [oracles: DISK_THM] [axioms: i32_to_int_int_to_i32, isize_bounds] [] + ⊢ ∀x y. + i32_min ≤ -i32_to_int x ⇒ + -i32_to_int x ≤ i32_max ⇒ + ∃y. i32_neg x = Return y ∧ i32_to_int y = -i32_to_int x + [i32_rem_eq] Theorem [oracles: DISK_THM] @@ -1237,6 +1543,14 @@ sig ∃z. i64_mul x y = Return z ∧ i64_to_int z = i64_to_int x * i64_to_int y + [i64_neg_eq] Theorem + + [oracles: DISK_THM] [axioms: i64_to_int_int_to_i64, isize_bounds] [] + ⊢ ∀x y. + i64_min ≤ -i64_to_int x ⇒ + -i64_to_int x ≤ i64_max ⇒ + ∃y. i64_neg x = Return y ∧ i64_to_int y = -i64_to_int x + [i64_rem_eq] Theorem [oracles: DISK_THM] @@ -1290,6 +1604,14 @@ sig ∃z. i8_mul x y = Return z ∧ i8_to_int z = i8_to_int x * i8_to_int y + [i8_neg_eq] Theorem + + [oracles: DISK_THM] [axioms: i8_to_int_int_to_i8, isize_bounds] [] + ⊢ ∀x y. + i8_min ≤ -i8_to_int x ⇒ + -i8_to_int x ≤ i8_max ⇒ + ∃y. i8_neg x = Return y ∧ i8_to_int y = -i8_to_int x + [i8_rem_eq] Theorem [oracles: DISK_THM] @@ -1365,6 +1687,15 @@ sig ∃z. isize_mul x y = Return z ∧ isize_to_int z = isize_to_int x * isize_to_int y + [isize_neg_eq] Theorem + + [oracles: DISK_THM] [axioms: isize_to_int_int_to_isize, isize_bounds] + [] + ⊢ ∀x y. + isize_min ≤ -isize_to_int x ⇒ + -isize_to_int x ≤ isize_max ⇒ + ∃y. isize_neg x = Return y ∧ isize_to_int y = -isize_to_int x + [isize_rem_eq] Theorem [oracles: DISK_THM] diff --git a/compiler/Config.ml b/compiler/Config.ml index 15818938..ce9b0e0c 100644 --- a/compiler/Config.ml +++ b/compiler/Config.ml @@ -3,9 +3,9 @@ (** {1 Backend choice} *) (** The choice of backend *) -type backend = FStar | Coq | Lean +type backend = FStar | Coq | Lean | HOL4 -let backend_names = [ "fstar"; "coq"; "lean" ] +let backend_names = [ "fstar"; "coq"; "lean"; "hol4" ] (** Utility to compute the backend from an input parameter *) let backend_of_string (b : string) : backend option = @@ -13,6 +13,7 @@ let backend_of_string (b : string) : backend option = | "fstar" -> Some FStar | "coq" -> Some Coq | "lean" -> Some Lean + | "hol4" -> Some HOL4 | _ -> None let opt_backend : backend option ref = ref None diff --git a/compiler/Driver.ml b/compiler/Driver.ml index d8418278..2ff9e295 100644 --- a/compiler/Driver.ml +++ b/compiler/Driver.ml @@ -158,6 +158,11 @@ let () = if !use_fuel then ( log#error "The Lean backend doesn't support the -use-fuel option"; fail ()) + | HOL4 -> + (* We don't support fuel for the HOL4 backend *) + if !use_fuel then ( + log#error "The HOL4 backend doesn't support the -use-fuel option"; + fail ()) in (* Retrieve and check the filename *) diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 03c256ec..0decbff1 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -16,7 +16,7 @@ module F = Format let int_name (int_ty : integer_type) = let isize, usize, i_format, u_format = match !backend with - | FStar | Coq -> + | FStar | Coq | HOL4 -> ("isize", "usize", format_of_string "i%d", format_of_string "u%d") | Lean -> ("Isize", "Usize", format_of_string "I%d", format_of_string "U%d") in @@ -37,14 +37,15 @@ let int_name (int_ty : integer_type) = (** Small helper to compute the name of a unary operation *) let unop_name (unop : unop) : string = match unop with - | Not -> ( match !backend with FStar | Lean -> "not" | Coq -> "negb") + | Not -> ( + match !backend with FStar | Lean -> "not" | Coq -> "negb" | HOL4 -> "~") | Neg (int_ty : integer_type) -> ( match !backend with Lean -> "-" | _ -> int_name int_ty ^ "_neg") | Cast _ -> raise (Failure "Unsupported") (** Small helper to compute the name of a binary operation (note that many binary operations like "less than" are extracted to primitive operations, - like [<]. + like [<]). *) let named_binop_name (binop : E.binop) (int_ty : integer_type) : string = let binop = @@ -54,12 +55,16 @@ let named_binop_name (binop : E.binop) (int_ty : integer_type) : string = | Add -> "add" | Sub -> "sub" | Mul -> "mul" + | Lt -> "lt" + | Le -> "le" + | Ge -> "ge" + | Gt -> "gt" | _ -> raise (Failure "Unreachable") in (* Remark: the Lean case is actually not used *) match !backend with | Lean -> int_name int_ty ^ "." ^ binop - | FStar | Coq -> int_name int_ty ^ "_" ^ binop + | FStar | Coq | HOL4 -> int_name int_ty ^ "_" ^ binop (** A list of keywords/identifiers used by the backend and with which we want to check collision. @@ -185,6 +190,28 @@ let keywords () = "with"; "opaque_defs"; ] + | HOL4 -> + [ + "Axiom"; + "case"; + "Definition"; + "else"; + "End"; + "fix"; + "fix_exec"; + "fn"; + "fun"; + "if"; + "in"; + "int"; + "Inductive"; + "let"; + "of"; + "Proof"; + "QED"; + "then"; + "Theorem"; + ] in List.concat [ named_unops; named_binops; misc ] @@ -215,6 +242,15 @@ let assumed_adts () : (assumed_ty * string) list = (Fuel, "nat"); (Option, "option"); (Vec, "vec"); + ] + | HOL4 -> + [ + (State, "state"); + (Result, "result"); + (Error, "error"); + (Fuel, "num"); + (Option, "OPTION"); + (Vec, "vec"); ]) let assumed_structs : (assumed_ty * string) list = [] @@ -253,6 +289,16 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list = (Option, option_some_id, "some"); (Option, option_none_id, "none"); ] + | HOL4 -> + [ + (Result, result_return_id, "Return"); + (Result, result_fail_id, "Fail"); + (Error, error_failure_id, "Failure"); + (* No Fuel::Zero on purpose *) + (* No Fuel::Succ on purpose *) + (Option, option_some_id, "SOME"); + (Option, option_none_id, "NONE"); + ] let assumed_llbc_functions : (A.assumed_fun_id * T.RegionGroupId.id option * string) list = @@ -288,6 +334,9 @@ let assumed_pure_functions () : (pure_assumed_fun_id * string) list = | Lean -> (* We don't provide [FuelDecrease] and [FuelEqZero] on purpose *) [ (Return, "return"); (Fail, "fail_"); (Assert, "massert") ] + | HOL4 -> + (* We don't provide [FuelDecrease] and [FuelEqZero] on purpose *) + [ (Return, "return"); (Fail, "fail"); (Assert, "massert") ] let names_map_init () : names_map_init = { @@ -310,37 +359,60 @@ let extract_unop (extract_expr : bool -> texpression -> unit) F.pp_print_space fmt (); extract_expr true arg; if inside then F.pp_print_string fmt ")" - | Cast (src, tgt) -> - (* The source type is an implicit parameter *) - if inside then F.pp_print_string fmt "("; - let cast_str = - match !backend with - | Coq | FStar -> "scalar_cast" - | Lean -> (* TODO: I8.cast, I16.cast, etc.*) "Scalar.cast" - in - F.pp_print_string fmt cast_str; - F.pp_print_space fmt (); - if !backend <> Lean then ( - F.pp_print_string fmt - (StringUtils.capitalize_first_letter - (PrintPure.integer_type_to_string src)); - F.pp_print_space fmt ()); - if !backend = Lean then F.pp_print_string fmt ("." ^ int_name tgt) - else - F.pp_print_string fmt - (StringUtils.capitalize_first_letter - (PrintPure.integer_type_to_string tgt)); - F.pp_print_space fmt (); - extract_expr true arg; - if inside then F.pp_print_string fmt ")" + | Cast (src, tgt) -> ( + (* HOL4 has a special treatment: because it doesn't support dependent + types, we don't have a specific operator for the cast *) + match !backend with + | HOL4 -> + (* Casting, say, an u32 to an i32 would be done as follows: + {[ + mk_i32 (u32_to_int x) + ]} + *) + if inside then F.pp_print_string fmt "("; + F.pp_print_string fmt ("mk_" ^ int_name tgt); + F.pp_print_space fmt (); + F.pp_print_string fmt "("; + F.pp_print_string fmt (int_name src ^ "_to_int"); + F.pp_print_space fmt (); + extract_expr true arg; + F.pp_print_string fmt ")"; + if inside then F.pp_print_string fmt ")" + | FStar | Coq | Lean -> + (* Rem.: the source type is an implicit parameter *) + if inside then F.pp_print_string fmt "("; + let cast_str = + match !backend with + | Coq | FStar -> "scalar_cast" + | Lean -> (* TODO: I8.cast, I16.cast, etc.*) "Scalar.cast" + | HOL4 -> raise (Failure "Unreachable") + in + F.pp_print_string fmt cast_str; + F.pp_print_space fmt (); + if !backend <> Lean then ( + F.pp_print_string fmt + (StringUtils.capitalize_first_letter + (PrintPure.integer_type_to_string src)); + F.pp_print_space fmt ()); + if !backend = Lean then F.pp_print_string fmt ("." ^ int_name tgt) + else + F.pp_print_string fmt + (StringUtils.capitalize_first_letter + (PrintPure.integer_type_to_string tgt)); + F.pp_print_space fmt (); + extract_expr true arg; + if inside then F.pp_print_string fmt ")") +(** [extract_expr] : the boolean argument is [inside] *) let extract_binop (extract_expr : bool -> texpression -> unit) (fmt : F.formatter) (inside : bool) (binop : E.binop) (int_ty : integer_type) (arg0 : texpression) (arg1 : texpression) : unit = if inside then F.pp_print_string fmt "("; (* Some binary operations have a special notation depending on the backend *) (match (!backend, binop) with - | _, (Eq | Lt | Le | Ne | Ge | Gt) | Lean, (Div | Rem | Add | Sub | Mul) -> + | HOL4, (Eq | Ne) + | (FStar | Coq | Lean), (Eq | Lt | Le | Ne | Ge | Gt) + | Lean, (Div | Rem | Add | Sub | Mul) -> let binop = match binop with | Eq -> "=" @@ -357,87 +429,99 @@ let extract_binop (extract_expr : bool -> texpression -> unit) | _ -> raise (Failure "Unreachable") in let binop = - match !backend with FStar | Lean -> binop | Coq -> "s" ^ binop + match !backend with FStar | Lean | HOL4 -> binop | Coq -> "s" ^ binop in extract_expr false arg0; F.pp_print_space fmt (); F.pp_print_string fmt binop; F.pp_print_space fmt (); extract_expr false arg1 - | _, (Div | Rem | Add | Sub | Mul) -> + | _, (Lt | Le | Ge | Gt | Div | Rem | Add | Sub | Mul) -> let binop = named_binop_name binop int_ty in F.pp_print_string fmt binop; F.pp_print_space fmt (); - extract_expr false arg0; + extract_expr true arg0; F.pp_print_space fmt (); - extract_expr false arg1 + extract_expr true arg1 | _, (BitXor | BitAnd | BitOr | Shl | Shr) -> raise Unimplemented); if inside then F.pp_print_string fmt ")" let type_decl_kind_to_qualif (kind : decl_kind) - (type_kind : type_decl_kind option) : string = + (type_kind : type_decl_kind option) : string option = match !backend with | FStar -> ( match kind with - | SingleNonRec -> "type" - | SingleRec -> "type" - | MutRecFirst -> "type" - | MutRecInner -> "and" - | MutRecLast -> "and" - | Assumed -> "assume type" - | Declared -> "val") + | SingleNonRec -> Some "type" + | SingleRec -> Some "type" + | MutRecFirst -> Some "type" + | MutRecInner -> Some "and" + | MutRecLast -> Some "and" + | Assumed -> Some "assume type" + | Declared -> Some "val") | Coq -> ( match (kind, type_kind) with - | SingleNonRec, Some Enum -> "Inductive" - | SingleNonRec, Some Struct -> "Record" - | (SingleRec | MutRecFirst), Some _ -> "Inductive" + | SingleNonRec, Some Enum -> Some "Inductive" + | SingleNonRec, Some Struct -> Some "Record" + | (SingleRec | MutRecFirst), Some _ -> Some "Inductive" | (MutRecInner | MutRecLast), Some _ -> (* Coq doesn't support groups of mutually recursive definitions which mix * records and inducties: we convert everything to records if this happens *) - "with" - | (Assumed | Declared), None -> "Axiom" + Some "with" + | (Assumed | Declared), None -> Some "Axiom" | _ -> raise (Failure "Unexpected")) | Lean -> ( match kind with | SingleNonRec -> - if type_kind = Some Struct then "structure" else "inductive" - | SingleRec -> "inductive" - | MutRecFirst -> "mutual inductive" - | MutRecInner -> "inductive" - | MutRecLast -> "inductive" (* TODO: need to print end afterwards *) - | Assumed -> "axiom" - | Declared -> "axiom") - -let fun_decl_kind_to_qualif (kind : decl_kind) = + if type_kind = Some Struct then Some "structure" else Some "inductive" + | SingleRec -> Some "inductive" + | MutRecFirst -> Some "inductive" + | MutRecInner -> Some "inductive" + | MutRecLast -> Some "inductive" + | Assumed -> Some "axiom" + | Declared -> Some "axiom") + | HOL4 -> None + +let fun_decl_kind_to_qualif (kind : decl_kind) : string option = match !backend with | FStar -> ( match kind with - | SingleNonRec -> "let" - | SingleRec -> "let rec" - | MutRecFirst -> "let rec" - | MutRecInner -> "and" - | MutRecLast -> "and" - | Assumed -> "assume val" - | Declared -> "val") + | SingleNonRec -> Some "let" + | SingleRec -> Some "let rec" + | MutRecFirst -> Some "let rec" + | MutRecInner -> Some "and" + | MutRecLast -> Some "and" + | Assumed -> Some "assume val" + | Declared -> Some "val") | Coq -> ( match kind with - | SingleNonRec -> "Definition" - | SingleRec -> "Fixpoint" - | MutRecFirst -> "Fixpoint" - | MutRecInner -> "with" - | MutRecLast -> "with" - | Assumed -> "Axiom" - | Declared -> "Axiom") + | SingleNonRec -> Some "Definition" + | SingleRec -> Some "Fixpoint" + | MutRecFirst -> Some "Fixpoint" + | MutRecInner -> Some "with" + | MutRecLast -> Some "with" + | Assumed -> Some "Axiom" + | Declared -> Some "Axiom") | Lean -> ( match kind with - | SingleNonRec -> "def" - | SingleRec -> "def" - | MutRecFirst -> "mutual def" - | MutRecInner -> "def" - | MutRecLast -> "def" (* TODO: need to print end afterwards *) - | Assumed -> "axiom" - | Declared -> "axiom") + | SingleNonRec -> Some "def" + | SingleRec -> Some "def" + | MutRecFirst -> Some "mutual def" + | MutRecInner -> Some "def" + | MutRecLast -> Some "def" + | Assumed -> Some "axiom" + | Declared -> Some "axiom") + | HOL4 -> None + +(** The type of types. + + TODO: move inside the formatter? + *) +let type_keyword () = + match !backend with + | FStar -> "Type0" + | Coq | Lean -> "Type" + | HOL4 -> raise (Failure "Unexpected") (** [ctx]: we use the context to lookup type definitions, to retrieve type names. @@ -514,7 +598,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) let name = List.map to_snake_case name in let name = String.concat "_" name in match !backend with - | FStar | Lean -> name + | FStar | Lean | HOL4 -> name | Coq -> capitalize_first_letter name in let type_name name = type_name_to_snake_case name ^ "_t" in @@ -533,7 +617,9 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) in let struct_constructor (basename : name) : string = let tname = type_name basename in - let prefix = match !backend with FStar -> "Mk" | Lean | Coq -> "mk" in + let prefix = + match !backend with FStar -> "Mk" | Lean | Coq | HOL4 -> "mk" + in prefix ^ tname in let get_fun_name = get_name in @@ -569,7 +655,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) match !Config.backend with | FStar -> "_decreases" | Lean -> "_terminates" - | Coq -> raise (Failure "Unexpected") + | Coq | HOL4 -> raise (Failure "Unexpected") in (* Concatenate *) fname ^ lp_suffix ^ suffix @@ -583,14 +669,16 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) let suffix = match !Config.backend with | Lean -> "_decreases" - | FStar | Coq -> raise (Failure "Unexpected") + | FStar | Coq | HOL4 -> raise (Failure "Unexpected") in (* Concatenate *) fname ^ lp_suffix ^ suffix in let opaque_pre () = - match !Config.backend with FStar | Coq -> "" | Lean -> "opaque_defs." + match !Config.backend with + | FStar | Coq | HOL4 -> "" + | Lean -> "opaque_defs." in let var_basename (_varset : StringSet.t) (basename : string option) (ty : ty) @@ -637,7 +725,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) (* TODO: use "t" also for F* *) match !backend with | FStar -> "x" (* lacking inspiration here... *) - | Coq | Lean -> "t" (* lacking inspiration here... *)) + | Coq | Lean | HOL4 -> "t" (* lacking inspiration here... *)) | Bool -> "b" | Char -> "c" | Integer _ -> "i" @@ -651,6 +739,9 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) | FStar -> (* This is *not* a no-op: this removes the capital letter *) to_snake_case basename + | HOL4 -> + (* In HOL4, type variable names must start with "'" *) + "'" ^ to_snake_case basename | Coq | Lean -> basename in let append_index (basename : string) (i : int) : string = @@ -663,14 +754,24 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) | Scalar sv -> ( match !backend with | FStar -> F.pp_print_string fmt (Z.to_string sv.PV.value) - | Coq -> - if inside then F.pp_print_string fmt "("; + | Coq | HOL4 -> + let print_brackets = inside && !backend = HOL4 in + if print_brackets then F.pp_print_string fmt "("; + (match !backend with + | Coq -> () + | HOL4 -> + F.pp_print_string fmt ("int_to_" ^ int_name sv.PV.int_ty); + F.pp_print_space fmt () + | _ -> raise (Failure "Unreachable")); (* We need to add parentheses if the value is negative *) if sv.PV.value >= Z.of_int 0 then F.pp_print_string fmt (Z.to_string sv.PV.value) else F.pp_print_string fmt ("(" ^ Z.to_string sv.PV.value ^ ")"); - F.pp_print_string fmt ("%" ^ int_name sv.PV.int_ty); - if inside then F.pp_print_string fmt ")" + (match !backend with + | Coq -> F.pp_print_string fmt ("%" ^ int_name sv.PV.int_ty) + | HOL4 -> () + | _ -> raise (Failure "Unreachable")); + if print_brackets then F.pp_print_string fmt ")" | Lean -> F.pp_print_string fmt "("; F.pp_print_string fmt (int_name sv.int_ty); @@ -694,6 +795,9 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) F.pp_print_string fmt b | Char c -> ( match !backend with + | HOL4 -> + (* [#"a"] is a notation for [CHR 97] (97 is the ASCII code for 'a') *) + F.pp_print_string fmt ("#\"" ^ String.make 1 c ^ "\"") | FStar | Lean -> F.pp_print_string fmt ("'" ^ String.make 1 c ^ "'") | Coq -> if inside then F.pp_print_string fmt "("; @@ -750,32 +854,183 @@ let mk_formatter_and_names_map (ctx : trans_ctx) (crate_name : string) let names_map = initialize_names_map fmt (names_map_init ()) in (fmt, names_map) +let is_single_opaque_fun_decl_group (dg : Pure.fun_decl list) : bool = + match dg with [ d ] -> d.body = None | _ -> false + +let is_single_opaque_type_decl_group (dg : Pure.type_decl list) : bool = + match dg with [ d ] -> d.kind = Opaque | _ -> false + +let is_empty_record_type_decl (d : Pure.type_decl) : bool = d.kind = Struct [] + +let is_empty_record_type_decl_group (dg : Pure.type_decl list) : bool = + match dg with [ d ] -> is_empty_record_type_decl d | _ -> false + (** In some provers, groups of definitions must be delimited. - in Coq, *every* group (including singletons) must end with "." - in Lean, groups of mutually recursive definitions must end with "end" + - in HOL4 (in most situations) the whole group must be within a `Define` command + + Calls to {!extract_fun_decl} should be inserted between calls to + {!start_fun_decl_group} and {!end_fun_decl_group}. + + TODO: maybe those [{start/end}_decl_group] functions are not that much a good + idea and we should merge them with the corresponding [extract_decl] functions. *) -let print_decl_end_delimiter (fmt : F.formatter) (kind : decl_kind) = - if !backend = Coq && decl_is_last_from_group kind then ( - F.pp_print_cut fmt (); - F.pp_print_string fmt ".") - else if !backend = Lean && kind = MutRecLast then ( - F.pp_print_cut fmt (); - F.pp_print_string fmt "end") +let start_fun_decl_group (ctx : extraction_ctx) (fmt : F.formatter) + (is_rec : bool) (dg : Pure.fun_decl list) = + match !backend with + | FStar | Coq | Lean -> () + | HOL4 -> + (* In HOL4, opaque functions have a special treatment *) + if is_single_opaque_fun_decl_group dg then () + else + let with_opaque_pre = false in + let compute_fun_def_name (def : Pure.fun_decl) : string = + ctx_get_local_function with_opaque_pre def.def_id def.loop_id + def.back_id ctx + ^ "_def" + in + let names = List.map compute_fun_def_name dg in + (* Add a break before *) + F.pp_print_break fmt 0 0; + (* Open the box for the delimiters *) + F.pp_open_vbox fmt 0; + (* Open the box for the definitions themselves *) + F.pp_open_vbox fmt ctx.indent_incr; + (* Print the delimiters *) + if is_rec then + F.pp_print_string fmt + ("val [" ^ String.concat ", " names ^ "] = DefineDiv ‘") + else ( + assert (List.length names = 1); + let name = List.hd names in + F.pp_print_string fmt ("val " ^ name ^ " = Define ‘")); + F.pp_print_cut fmt () + +(** See {!start_fun_decl_group}. *) +let end_fun_decl_group (fmt : F.formatter) (is_rec : bool) + (dg : Pure.fun_decl list) = + match !backend with + | FStar -> () + | Coq -> + (* For aesthetic reasons, we print the Coq end group delimiter directly + in {!extract_fun_decl}. *) + () + | Lean -> + (* We must add the "end" keyword to groups of mutually recursive functions *) + if is_rec && List.length dg > 1 then ( + F.pp_print_cut fmt (); + F.pp_print_string fmt "end"; + (* Add breaks to insert new lines between definitions *) + F.pp_print_break fmt 0 0) + else () + | HOL4 -> + (* In HOL4, opaque functions have a special treatment *) + if is_single_opaque_fun_decl_group dg then () + else ( + (* Close the box for the definitions *) + F.pp_close_box fmt (); + (* Print the end delimiter *) + F.pp_print_cut fmt (); + F.pp_print_string fmt "’"; + (* Close the box for the delimiters *) + F.pp_close_box fmt (); + (* Add breaks to insert new lines between definitions *) + F.pp_print_break fmt 0 0) -let unit_name () = match !backend with Lean -> "Unit" | Coq | FStar -> "unit" +(** See {!start_fun_decl_group}: similar usage, but for the type declarations. *) +let start_type_decl_group (ctx : extraction_ctx) (fmt : F.formatter) + (is_rec : bool) (dg : Pure.type_decl list) = + match !backend with + | FStar | Coq -> () + | Lean -> + if is_rec && List.length dg > 1 then ( + F.pp_print_space fmt (); + F.pp_print_string fmt "mutual"; + F.pp_print_space fmt ()) + | HOL4 -> + (* In HOL4, opaque types and empty records have a special treatment *) + if + is_single_opaque_type_decl_group dg + || is_empty_record_type_decl_group dg + then () + else ( + (* Add a break before *) + F.pp_print_break fmt 0 0; + (* Open the box for the delimiters *) + F.pp_open_vbox fmt 0; + (* Open the box for the definitions themselves *) + F.pp_open_vbox fmt ctx.indent_incr; + (* Print the delimiters *) + F.pp_print_string fmt "Datatype:"; + F.pp_print_cut fmt ()) + +(** See {!start_fun_decl_group}. *) +let end_type_decl_group (fmt : F.formatter) (is_rec : bool) + (dg : Pure.type_decl list) = + match !backend with + | FStar -> () + | Coq -> + (* For aesthetic reasons, we print the Coq end group delimiter directly + in {!extract_fun_decl}. *) + () + | Lean -> + (* We must add the "end" keyword to groups of mutually recursive functions *) + if is_rec && List.length dg > 1 then ( + F.pp_print_cut fmt (); + F.pp_print_string fmt "end"; + (* Add breaks to insert new lines between definitions *) + F.pp_print_break fmt 0 0) + else () + | HOL4 -> + (* In HOL4, opaque types and empty records have a special treatment *) + if + is_single_opaque_type_decl_group dg + || is_empty_record_type_decl_group dg + then () + else ( + (* Close the box for the definitions *) + F.pp_close_box fmt (); + (* Print the end delimiter *) + F.pp_print_cut fmt (); + F.pp_print_string fmt "End"; + (* Close the box for the delimiters *) + F.pp_close_box fmt (); + (* Add breaks to insert new lines between definitions *) + F.pp_print_break fmt 0 0) + +let unit_name () = + match !backend with Lean -> "Unit" | Coq | FStar | HOL4 -> "unit" (** [inside] constrols whether we should add parentheses or not around type applications (if [true] we add parentheses). + + [no_params_tys]: for all the types inside this set, do not print the type parameters. + This is used for HOL4. As polymorphism is uniform in HOL4, printing the + type parameters in the recursive definitions is useless (and actually + forbidden). + + For instance, where in F* we would write: + {[ + type list a = | Nil : list a | Cons : a -> list a -> list a + ]} + + In HOL4 we would simply write: + {[ + Datatype: + list = Nil 'a | Cons 'a list + End + ]} *) -let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) - (ty : ty) : unit = - let extract_rec = extract_ty ctx fmt in +let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) + (no_params_tys : TypeDeclId.Set.t) (inside : bool) (ty : ty) : unit = + let extract_rec = extract_ty ctx fmt no_params_tys in match ty with | Adt (type_id, tys) -> ( match type_id with | Tuple -> - (* This is a bit annoying, but in F*/Coq [()] is not the unit type: + (* This is a bit annoying, but in F*/Coq/HOL4 [()] is not the unit type: * we have to write [unit]... *) if tys = [] then F.pp_print_string fmt (unit_name ()) else ( @@ -784,23 +1039,54 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) (fun () -> F.pp_print_space fmt (); let product = - match !backend with FStar -> "&" | Coq -> "*" | Lean -> "×" + match !backend with + | FStar -> "&" + | Coq -> "*" + | Lean -> "×" + | HOL4 -> "#" in F.pp_print_string fmt product; F.pp_print_space fmt ()) (extract_rec true) tys; F.pp_print_string fmt ")") - | AdtId _ | Assumed _ -> - let print_paren = inside && tys <> [] in - if print_paren then F.pp_print_string fmt "("; - (* TODO: for now, only the opaque *functions* are extracted in the - opaque module. The opaque *types* are assumed. *) + | AdtId _ | Assumed _ -> ( + (* HOL4 behaves differently. Where in Coq/FStar/Lean we would write: + `tree a b` + + In HOL4 we would write: + `('a, 'b) tree` + *) let with_opaque_pre = false in - F.pp_print_string fmt (ctx_get_type with_opaque_pre type_id ctx); - if tys <> [] then F.pp_print_space fmt (); - Collections.List.iter_link (F.pp_print_space fmt) (extract_rec true) - tys; - if print_paren then F.pp_print_string fmt ")") + match !backend with + | FStar | Coq | Lean -> + let print_paren = inside && tys <> [] in + if print_paren then F.pp_print_string fmt "("; + (* TODO: for now, only the opaque *functions* are extracted in the + opaque module. The opaque *types* are assumed. *) + F.pp_print_string fmt (ctx_get_type with_opaque_pre type_id ctx); + if tys <> [] then ( + F.pp_print_space fmt (); + Collections.List.iter_link (F.pp_print_space fmt) + (extract_rec true) tys); + if print_paren then F.pp_print_string fmt ")" + | HOL4 -> + let print_tys = + match type_id with + | AdtId id -> not (TypeDeclId.Set.mem id no_params_tys) + | Assumed _ -> true + | _ -> raise (Failure "Unreachable") + in + if tys <> [] && print_tys then ( + let print_paren = List.length tys > 1 in + if print_paren then F.pp_print_string fmt "("; + Collections.List.iter_link + (fun () -> + F.pp_print_string fmt ","; + F.pp_print_space fmt ()) + (extract_rec true) tys; + if print_paren then F.pp_print_string fmt ")"; + F.pp_print_space fmt ()); + F.pp_print_string fmt (ctx_get_type with_opaque_pre type_id ctx))) | TypeVar vid -> F.pp_print_string fmt (ctx_get_type_var vid ctx) | Bool -> F.pp_print_string fmt ctx.fmt.bool_name | Char -> F.pp_print_string fmt ctx.fmt.char_name @@ -855,18 +1141,20 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) : (** Print the variants *) let extract_type_decl_variant (ctx : extraction_ctx) (fmt : F.formatter) - (type_name : string) (type_params : string list) (cons_name : string) - (fields : field list) : unit = + (type_decl_group : TypeDeclId.Set.t) (type_name : string) + (type_params : string list) (cons_name : string) (fields : field list) : + unit = F.pp_print_space fmt (); (* variant box *) F.pp_open_hvbox fmt ctx.indent_incr; (* [| Cons :] * Note that we really don't want any break above so we print everything * at once. *) - F.pp_print_string fmt ("| " ^ cons_name ^ " :"); - F.pp_print_space fmt (); + let opt_colon = if !backend <> HOL4 then " :" else "" in + F.pp_print_string fmt ("| " ^ cons_name ^ opt_colon); let print_field (fid : FieldId.id) (f : field) (ctx : extraction_ctx) : extraction_ctx = + F.pp_print_space fmt (); (* Open the field box *) F.pp_open_box fmt ctx.indent_incr; (* Print the field names, if the backend accepts it. @@ -888,16 +1176,17 @@ let extract_type_decl_variant (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_string fmt (field_name ^ " :"); F.pp_print_space fmt (); ctx) - | Coq | Lean -> ctx + | Coq | Lean | HOL4 -> ctx in (* Print the field type *) - extract_ty ctx fmt false f.field_ty; - (* Print the arrow [->]*) - F.pp_print_space fmt (); - F.pp_print_string fmt "->"; + let inside = !backend = HOL4 in + extract_ty ctx fmt type_decl_group inside f.field_ty; + (* Print the arrow [->] *) + if !backend <> HOL4 then ( + F.pp_print_space fmt (); + F.pp_print_string fmt "->"); (* Close the field box *) F.pp_close_box fmt (); - F.pp_print_space fmt (); (* Return *) ctx in @@ -907,21 +1196,23 @@ let extract_type_decl_variant (ctx : extraction_ctx) (fmt : F.formatter) List.fold_left (fun ctx (fid, f) -> print_field fid f ctx) ctx fields in (* Print the final type *) - F.pp_open_hovbox fmt 0; - F.pp_print_string fmt type_name; - List.iter - (fun type_param -> - F.pp_print_space fmt (); - F.pp_print_string fmt type_param) - type_params; - F.pp_close_box fmt (); + if !backend <> HOL4 then ( + F.pp_print_space fmt (); + F.pp_open_hovbox fmt 0; + F.pp_print_string fmt type_name; + List.iter + (fun type_param -> + F.pp_print_space fmt (); + F.pp_print_string fmt type_param) + type_params; + F.pp_close_box fmt ()); (* Close the variant box *) F.pp_close_box fmt () (* TODO: we don' need the [def_name] paramter: it can be retrieved from the context *) let extract_type_decl_enum_body (ctx : extraction_ctx) (fmt : F.formatter) - (def : type_decl) (def_name : string) (type_params : string list) - (variants : variant list) : unit = + (type_decl_group : TypeDeclId.Set.t) (def : type_decl) (def_name : string) + (type_params : string list) (variants : variant list) : unit = (* We want to generate a definition which looks like this (taking F* as example): {[ type list a = | Cons : a -> list a -> list a | Nil : list a @@ -959,15 +1250,16 @@ let extract_type_decl_enum_body (ctx : extraction_ctx) (fmt : F.formatter) id (in the case of Lean) *) let cons_name = ctx.fmt.variant_name def.name v.variant_name in let fields = v.fields in - extract_type_decl_variant ctx fmt def_name type_params cons_name fields + extract_type_decl_variant ctx fmt type_decl_group def_name type_params + cons_name fields in (* Print the variants *) let variants = VariantId.mapi (fun vid v -> (vid, v)) variants in List.iter (fun (vid, v) -> print_variant vid v) variants let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter) - (kind : decl_kind) (def : type_decl) (type_params : string list) - (fields : field list) : unit = + (type_decl_group : TypeDeclId.Set.t) (kind : decl_kind) (def : type_decl) + (type_params : string list) (fields : field list) : unit = (* We want to generate a definition which looks like this (taking F* as example): {[ type t = { x : int; y : bool; } @@ -1007,6 +1299,20 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter) expanded which introduces let bindings of the form: [let RecordCons ... = x in ...]. As a consequence, we never use the record projectors (unless we reconstruct them in the micro passes of course). + + HOL4: + ===== + Type definitions are written as follows: + {[ + Datatype: + tree = + TLeaf 'a + | TNode node ; + + node = + Node (tree list) + End + ]} *) (* Note that we already printed: [type t =] *) let is_rec = decl_is_from_rec_group kind in @@ -1026,12 +1332,15 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_string fmt (ctx_get_struct with_opaque_pre (AdtId def.def_id) ctx); F.pp_print_string fmt " "); - if !backend <> Lean then F.pp_print_string fmt "{"; + (match !backend with + | Lean -> () + | FStar | Coq -> F.pp_print_string fmt "{" + | HOL4 -> F.pp_print_string fmt "<|"); F.pp_print_break fmt 1 ctx.indent_incr; (* The body itself *) (* Open a box for the body *) (match !backend with - | Coq | FStar -> F.pp_open_hvbox fmt 0 + | Coq | FStar | HOL4 -> F.pp_open_hvbox fmt 0 | Lean -> F.pp_open_vbox fmt 0); (* Print the fields *) let print_field (field_id : FieldId.id) (f : field) : unit = @@ -1042,7 +1351,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_space fmt (); F.pp_print_string fmt ":"; F.pp_print_space fmt (); - extract_ty ctx fmt false f.field_ty; + extract_ty ctx fmt type_decl_group false f.field_ty; if !backend <> Lean then F.pp_print_string fmt ";"; (* Close the box for the field *) F.pp_close_box fmt () @@ -1053,9 +1362,14 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter) fields; (* Close the box for the body *) F.pp_close_box fmt (); - if !backend <> Lean then ( - F.pp_print_space fmt (); - F.pp_print_string fmt "}")) + match !backend with + | Lean -> () + | FStar | Coq -> + F.pp_print_space fmt (); + F.pp_print_string fmt "}" + | HOL4 -> + F.pp_print_space fmt (); + F.pp_print_string fmt "|>") else ( (* We extract for Coq or Lean, and we have a recursive record, or a record in a group of mutually recursive types: we extract it as an inductive type *) @@ -1063,14 +1377,15 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter) let with_opaque_pre = false in let cons_name = ctx_get_struct with_opaque_pre (AdtId def.def_id) ctx in let def_name = ctx_get_local_type with_opaque_pre def.def_id ctx in - extract_type_decl_variant ctx fmt def_name type_params cons_name fields) + extract_type_decl_variant ctx fmt type_decl_group def_name type_params + cons_name fields) in () (** Extract a nestable, muti-line comment *) let extract_comment (fmt : F.formatter) (s : string) : unit = match !backend with - | Coq | FStar -> + | Coq | FStar | HOL4 -> F.pp_print_string fmt "(** "; F.pp_print_string fmt s; F.pp_print_string fmt " *)" @@ -1081,16 +1396,16 @@ let extract_comment (fmt : F.formatter) (s : string) : unit = (** Extract a type declaration. - Note that all the names used for extraction should already have been - registered. + This function is for all type declarations and all backends **at the exception** + of opaque (assumed/declared) types format4 HOL4. + + See {!extract_type_decl}. *) -let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter) - (kind : decl_kind) (def : type_decl) : unit = - let extract_body = - match kind with - | SingleNonRec | SingleRec | MutRecFirst | MutRecInner | MutRecLast -> true - | Assumed | Declared -> false - in +let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) + (type_decl_group : TypeDeclId.Set.t) (kind : decl_kind) (def : type_decl) + (extract_body : bool) : unit = + (* Sanity check *) + assert (extract_body || !backend <> HOL4); let type_kind = if extract_body then match def.kind with @@ -1114,7 +1429,8 @@ let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter) * body translation (they are not top-level) *) let ctx_body, type_params = ctx_add_type_params def.type_params ctx in (* Add a break before *) - F.pp_print_break fmt 0 0; + if !backend <> HOL4 || not (decl_is_first_from_group kind) then + F.pp_print_break fmt 0 0; (* Print a comment to link the extracted type to its original rust definition *) extract_comment fmt ("[" ^ Print.name_to_string def.name ^ "]"); F.pp_print_break fmt 0 0; @@ -1122,18 +1438,17 @@ let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter) * one line. Note however that in the case of Lean line breaks are important * for parsing: we thus use a hovbox. *) (match !backend with - | Coq | FStar -> F.pp_open_hvbox fmt 0 + | Coq | FStar | HOL4 -> F.pp_open_hvbox fmt 0 | Lean -> F.pp_open_vbox fmt 0); (* Open a box for "type TYPE_NAME (TYPE_PARAMS) =" *) F.pp_open_hovbox fmt ctx.indent_incr; (* > "type TYPE_NAME" *) let qualif = ctx.fmt.type_decl_kind_to_qualif kind type_kind in - F.pp_print_string fmt (qualif ^ " " ^ def_name); + (match qualif with + | Some qualif -> F.pp_print_string fmt (qualif ^ " " ^ def_name) + | None -> F.pp_print_string fmt def_name); (* Print the type parameters *) - let type_keyword = - match !backend with FStar -> "Type0" | Coq | Lean -> "Type" - in - if def.type_params <> [] then ( + if def.type_params <> [] && !backend <> HOL4 then ( if use_forall then ( F.pp_print_space fmt (); F.pp_print_string fmt ":"; @@ -1149,7 +1464,7 @@ let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter) def.type_params; F.pp_print_string fmt ":"; F.pp_print_space fmt (); - F.pp_print_string fmt (type_keyword ^ ")")); + F.pp_print_string fmt (type_keyword () ^ ")")); (* Print the "=" if we extract the body*) if extract_body then ( F.pp_print_space fmt (); @@ -1160,32 +1475,107 @@ let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter) | Lean -> if type_kind = Some Struct && kind = SingleNonRec then "where" else ":=" + | HOL4 -> "=" in F.pp_print_string fmt eq) else ( - (* Otherwise print ": Type" *) + (* Otherwise print ": Type", unless it is the HOL4 backend (in + which case we declare the type with `new_type`) *) if use_forall then F.pp_print_string fmt "," else ( F.pp_print_space fmt (); F.pp_print_string fmt ":"); F.pp_print_space fmt (); - F.pp_print_string fmt type_keyword); + F.pp_print_string fmt (type_keyword ())); (* Close the box for "type TYPE_NAME (TYPE_PARAMS) =" *) F.pp_close_box fmt (); (if extract_body then - match def.kind with - | Struct fields -> - extract_type_decl_struct_body ctx_body fmt kind def type_params fields - | Enum variants -> - extract_type_decl_enum_body ctx_body fmt def def_name type_params - variants - | Opaque -> raise (Failure "Unreachable")); - (* If Coq: end the definition with a "." *) - print_decl_end_delimiter fmt kind; + match def.kind with + | Struct fields -> + extract_type_decl_struct_body ctx_body fmt type_decl_group kind def + type_params fields + | Enum variants -> + extract_type_decl_enum_body ctx_body fmt type_decl_group def def_name + type_params variants + | Opaque -> raise (Failure "Unreachable")); + (* Add the definition end delimiter *) + if !backend = HOL4 && decl_is_not_last_from_group kind then ( + F.pp_print_space fmt (); + F.pp_print_string fmt ";") + else if !backend = Coq && decl_is_last_from_group kind then ( + (* This is actually an end of group delimiter. For aesthetic reasons + we print it here instead of in {!end_type_decl_group}. *) + F.pp_print_cut fmt (); + F.pp_print_string fmt "."); (* Close the box for the definition *) F.pp_close_box fmt (); (* Add breaks to insert new lines between definitions *) - F.pp_print_break fmt 0 0 + if !backend <> HOL4 || decl_is_not_last_from_group kind then + F.pp_print_break fmt 0 0 + +(** Extract an opaque type declaration to HOL4. + + Remark (SH): having to treat this specific case separately is very annoying, + but I could not find a better way. + *) +let extract_type_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter) + (def : type_decl) : unit = + (* Retrieve the definition name *) + let with_opaque_pre = false in + let def_name = ctx_get_local_type with_opaque_pre def.def_id ctx in + (* Count the number of parameters *) + let num_params = List.length def.type_params in + (* Generate the declaration *) + F.pp_print_space fmt (); + F.pp_print_string fmt + ("val _ = new_type (\"" ^ def_name ^ ", " ^ string_of_int num_params ^ ")"); + F.pp_print_space fmt () + +(** Extract an empty record type declaration to HOL4. + + Empty records are not supported in HOL4, so we extract them as type + abbreviations to the unit type. + + Remark (SH): having to treat this specific case separately is very annoying, + but I could not find a better way. + *) +let extract_type_decl_hol4_empty_record (ctx : extraction_ctx) + (fmt : F.formatter) (def : type_decl) : unit = + (* Retrieve the definition name *) + let with_opaque_pre = false in + let def_name = ctx_get_local_type with_opaque_pre def.def_id ctx in + (* Sanity check *) + assert (def.type_params = []); + (* Generate the declaration *) + F.pp_print_space fmt (); + F.pp_print_string fmt ("Type " ^ def_name ^ " = “: unit”"); + F.pp_print_space fmt () + +(** Extract a type declaration. + + Note that all the names used for extraction should already have been + registered. + + This function should be inserted between calls to {!start_type_decl_group} + and {!end_type_decl_group}. + *) +let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter) + (type_decl_group : TypeDeclId.Set.t) (kind : decl_kind) (def : type_decl) : + unit = + let extract_body = + match kind with + | SingleNonRec | SingleRec | MutRecFirst | MutRecInner | MutRecLast -> true + | Assumed | Declared -> false + in + if extract_body then + if !backend = HOL4 && is_empty_record_type_decl def then + extract_type_decl_hol4_empty_record ctx fmt def + else extract_type_decl_gen ctx fmt type_decl_group kind def extract_body + else + match !backend with + | FStar | Coq | Lean -> + extract_type_decl_gen ctx fmt type_decl_group kind def extract_body + | HOL4 -> extract_type_decl_hol4_opaque ctx fmt def (** Auxiliary function. @@ -1370,7 +1760,9 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx) (* Close the inner box projector *) F.pp_close_box fmt (); (* If Coq: end the definition with a "." *) - print_decl_end_delimiter fmt kind; + if !backend = Coq then ( + F.pp_print_cut fmt (); + F.pp_print_string fmt "."); (* Close the outer box projector *) F.pp_close_box fmt (); (* Add breaks to insert new lines between definitions *) @@ -1401,7 +1793,9 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx) (* Close the inner box projector *) F.pp_close_box fmt (); (* If Coq: end the definition with a "." *) - print_decl_end_delimiter fmt kind; + if !backend = Coq then ( + F.pp_print_cut fmt (); + F.pp_print_string fmt "."); (* Close the outer box projector *) F.pp_close_box fmt (); (* Add breaks to insert new lines between definitions *) @@ -1424,7 +1818,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx) let extract_type_decl_extra_info (ctx : extraction_ctx) (fmt : F.formatter) (kind : decl_kind) (decl : type_decl) : unit = match !backend with - | FStar | Lean -> () + | FStar | Lean | HOL4 -> () | Coq -> extract_type_decl_coq_arguments ctx fmt kind decl; extract_type_decl_record_field_projectors ctx fmt kind decl @@ -1448,7 +1842,7 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx) match !backend with | Coq -> "Axiom" | Lean -> "axiom" - | FStar -> raise (Failure "Unexpected") + | FStar | HOL4 -> raise (Failure "Unexpected") in F.pp_print_string fmt axiom; F.pp_print_space fmt (); @@ -1475,6 +1869,8 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx) F.pp_print_string fmt ":"; F.pp_print_space fmt (); F.pp_print_string fmt "Type0" + | HOL4 -> + F.pp_print_string fmt ("val _ = new_type (" ^ state_name ^ ", 0)") | Coq | Lean -> print_axiom ()) | Declared -> ( match !backend with @@ -1486,12 +1882,24 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx) F.pp_print_string fmt ":"; F.pp_print_space fmt (); F.pp_print_string fmt "Type0" + | HOL4 -> + F.pp_print_string fmt ("val _ = new_type (" ^ state_name ^ ", 0)") | Coq | Lean -> print_axiom ())); (* Close the box for the definition *) F.pp_close_box fmt (); (* Add breaks to insert new lines between definitions *) F.pp_print_break fmt 0 0 +(** In some provers like HOL4, we don't print the type parameters when calling + functions (and the polymorphism is uniform...). + + TODO: we may want to check that the polymorphism is indeed uniform when + generating code for such backends, and print at least a warning to the + user when it is not the case. + *) +let print_fun_type_params () : bool = + match !backend with FStar | Coq | Lean -> true | HOL4 -> false + (** Compute the names for all the pure functions generated from a rust function (forward function and backward functions). *) @@ -1507,6 +1915,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx) (keep_fwd : bool) (* Add the decreases proof for Lean only *) match !Config.backend with | Coq | FStar -> ctx + | HOL4 -> raise (Failure "Unexpected") | Lean -> ctx_add_decreases_proof def ctx else ctx in @@ -1729,12 +2138,13 @@ and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter) let with_opaque_pre = ctx.use_opaque_pre in let fun_name = ctx_get_function with_opaque_pre fun_id ctx in F.pp_print_string fmt fun_name; - (* Print the type parameters *) - List.iter - (fun ty -> - F.pp_print_space fmt (); - extract_ty ctx fmt true ty) - type_args; + (* Print the type parameters, if the backend is not HOL4 *) + if !backend <> HOL4 then + List.iter + (fun ty -> + F.pp_print_space fmt (); + extract_ty ctx fmt TypeDeclId.Set.empty true ty) + type_args; (* Print the arguments *) List.iter (fun ve -> @@ -1787,9 +2197,8 @@ and extract_field_projector (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_string fmt "."; (* If in Coq, the field projection has to be parenthesized *) (match !backend with - | FStar -> F.pp_print_string fmt field_name - | Coq -> F.pp_print_string fmt ("(" ^ field_name ^ ")") - | Lean -> F.pp_print_string fmt field_name); + | FStar | Lean | HOL4 -> F.pp_print_string fmt field_name + | Coq -> F.pp_print_string fmt ("(" ^ field_name ^ ")")); (* Close the box *) F.pp_close_box fmt () | arg :: args -> @@ -1843,7 +2252,6 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) (re : texpression) : extraction_ctx = (* Open a box for the let-binding *) F.pp_open_hovbox fmt ctx.indent_incr; - let is_fstar_monadic = monadic && !backend = FStar in let ctx = (* There are two cases: * - do we use a notation like [x <-- y;] @@ -1861,7 +2269,7 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) let arrow = match !backend with | Coq -> "<-" - | FStar | Lean -> failwith "impossible" + | FStar | Lean | HOL4 -> raise (Failure "impossible") in F.pp_print_string fmt arrow; F.pp_print_space fmt (); @@ -1869,24 +2277,42 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) F.pp_print_string fmt ";"; ctx) else ( - F.pp_print_string fmt (if is_fstar_monadic then "let*" else "let"); - F.pp_print_space fmt (); + (* Print the "let" *) + if monadic then + match !backend with + | FStar -> + F.pp_print_string fmt "let*"; + F.pp_print_space fmt () + | Coq | Lean -> + F.pp_print_string fmt "let"; + F.pp_print_space fmt () + | HOL4 -> () + else ( + F.pp_print_string fmt "let"; + F.pp_print_space fmt ()); let ctx = extract_typed_pattern ctx fmt true lv in F.pp_print_space fmt (); let eq = match !backend with | FStar -> "=" | Coq -> ":=" - (* TODO: switch to ⟵ once issues are fixed *) - | Lean -> if monadic then "←" else ":=" + | Lean -> + (* TODO: switch to ⟵ once issues are fixed *) + if monadic then "←" else ":=" + | HOL4 -> if monadic then "<-" else "=" in F.pp_print_string fmt eq; F.pp_print_space fmt (); extract_texpression ctx fmt false re; - (* In Lean, monadic let-bindings don't require to end with "in" *) - if !backend <> Lean then ( - F.pp_print_space fmt (); - F.pp_print_string fmt "in"); + (* End the monadic let-binding *) + (match !backend with + | Lean -> + (* In Lean, monadic let-bindings don't require to end with anything *) + () + | Coq | FStar -> + F.pp_print_space fmt (); + F.pp_print_string fmt "in" + | HOL4 -> F.pp_print_string fmt ";"); ctx) in (* Close the box for the let-binding *) @@ -1896,10 +2322,10 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) ctx in let exists_monadic = List.exists (fun (m, _, _) -> m) lets in - (* If Lean, we rely on monadic blocks, so we insert a do and open a new box + (* If Lean and HOL4, we rely on monadic blocks, so we insert a do and open a new box immediately *) - if !backend = Lean && exists_monadic then ( - F.pp_open_vbox fmt ctx.indent_incr; + if (!backend = Lean || !backend = HOL4) && exists_monadic 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 ()); let ctx = @@ -1913,23 +2339,29 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) extract_texpression ctx fmt false next_e; (* Close the box for the next expression *) F.pp_close_box fmt (); - (* do-box (Lean only) *) - if !backend = Lean && exists_monadic then F.pp_close_box fmt (); + + (* do-box (Lean and HOL4 only) *) + if (!backend = Lean || !backend = HOL4) && exists_monadic then ( + if !backend = HOL4 then ( + F.pp_print_space fmt (); + F.pp_print_string fmt "od"); + F.pp_close_box fmt ()); (* Close parentheses *) if inside && !backend <> Lean then F.pp_print_string fmt ")"; (* Close the box for the whole expression *) F.pp_close_box fmt () -and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) +and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (_inside : bool) (scrut : texpression) (body : switch_body) : unit = + (* Remark: we don't use the [inside] parameter because we extract matches in + a conservative manner: we always make sure they are parenthesized/delimited + with keywords such as [end] *) (* Open a box for the whole expression. In the case of Lean, we rely on indentation to delimit the end of the branches, and need to insert line breaks: we thus use a vbox. *) if !Config.backend = Lean then F.pp_open_vbox fmt 0 else F.pp_open_hvbox fmt 0; - (* Open parentheses *) - if inside then F.pp_print_string fmt "("; (* Extract the switch *) (match body with | If (e_then, e_else) -> @@ -1961,7 +2393,7 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) F.pp_print_space fmt (); F.pp_print_string fmt "begin"; F.pp_print_space fmt - | Coq | Lean -> + | Coq | Lean | HOL4 -> F.pp_print_space fmt (); F.pp_print_string fmt "("; F.pp_print_cut fmt) @@ -1978,18 +2410,18 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) F.pp_close_box fmt (); (* Close the parenthesized expression *) (if parenth then - match !backend with - | FStar -> - F.pp_print_space fmt (); - F.pp_print_string fmt "end" - | Coq | Lean -> F.pp_print_string fmt ")"); + match !backend with + | FStar -> + F.pp_print_space fmt (); + F.pp_print_string fmt "end" + | Coq | Lean | HOL4 -> F.pp_print_string fmt ")"); (* Close the box for the then/else+branch *) F.pp_close_box fmt () in extract_branch true e_then; extract_branch false e_else - | Match branches -> + | Match branches -> ( (* Open a box for the [match ... with] *) F.pp_open_hovbox fmt ctx.indent_incr; (* Print the [match ... with] *) @@ -1998,13 +2430,19 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) | FStar -> "begin match" | Coq -> "match" | Lean -> "match h:" + | HOL4 -> + (* We're being extra safe in the case of HOL4 *) + "(case" in F.pp_print_string fmt match_begin; F.pp_print_space fmt (); let scrut_inside = PureUtils.texpression_requires_parentheses scrut in extract_texpression ctx fmt scrut_inside scrut; F.pp_print_space fmt (); - F.pp_print_string fmt "with"; + let match_scrut_end = + match !backend with FStar | Coq | Lean -> "with" | HOL4 -> "of" + in + F.pp_print_string fmt match_scrut_end; (* Close the box for the [match ... with] *) F.pp_close_box fmt (); @@ -2020,7 +2458,9 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) F.pp_print_space fmt (); let ctx = extract_typed_pattern ctx fmt false br.pat in F.pp_print_space fmt (); - let arrow = match !backend with FStar -> "->" | Coq | Lean -> "=>" in + let arrow = + match !backend with FStar -> "->" | Coq | Lean | HOL4 -> "=>" + in F.pp_print_string fmt arrow; (* Close the box for the pattern *) F.pp_close_box fmt (); @@ -2037,58 +2477,89 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) List.iter extract_branch branches; - (* End the match - we rely on indentation in Lean *) - if !backend <> Lean then ( - F.pp_print_space fmt (); - F.pp_print_string fmt "end")); - (* Close parentheses *) - if inside then F.pp_print_string fmt ")"; + (* End the match *) + match !backend with + | Lean -> (*We rely on indentation in Lean *) () + | FStar | Coq -> + F.pp_print_space fmt (); + F.pp_print_string fmt "end" + | HOL4 -> F.pp_print_string fmt ")")); (* Close the box for the whole expression *) F.pp_close_box fmt () and extract_StructUpdate (ctx : extraction_ctx) (fmt : F.formatter) - (_inside : bool) (supd : struct_update) : unit = + (inside : bool) (supd : struct_update) : unit = (* We can't update a subset of the fields in Coq (i.e., we can do [{| x:= 3; y := 4 |}], but there is no syntax for [{| s with x := 3 |}]) *) assert (!backend <> Coq || supd.init = None); - F.pp_open_hvbox fmt 0; - F.pp_open_hvbox fmt ctx.indent_incr; - let lb, rb = - match !backend with Lean | FStar -> ("{", "}") | Coq -> ("{|", "|}") + (* In the case of HOL4, records with no fields are not supported and are + thus extracted to unit. We need to check that by looking up the definition *) + let extract_as_unit = + if !backend = HOL4 then + let d = + TypeDeclId.Map.find supd.struct_id ctx.trans_ctx.type_context.type_decls + in + d.kind = Struct [] + else false in - F.pp_print_string fmt lb; - F.pp_print_space fmt (); - F.pp_open_hvbox fmt ctx.indent_incr; - if supd.init <> None then ( - let var_name = ctx_get_var (Option.get supd.init) ctx in - F.pp_print_string fmt var_name; - F.pp_print_space fmt (); - F.pp_print_string fmt "with"; - F.pp_print_space fmt ()); - F.pp_open_hvbox fmt 0; - let delimiter = match !backend with Lean -> "," | Coq | FStar -> ";" in - let assign = match !backend with Coq | Lean -> ":=" | FStar -> "=" in - Collections.List.iter_link - (fun () -> - F.pp_print_string fmt delimiter; - F.pp_print_space fmt ()) - (fun (fid, fe) -> - F.pp_open_hvbox fmt ctx.indent_incr; - let f = ctx_get_field (AdtId supd.struct_id) fid ctx in - F.pp_print_string fmt f; - F.pp_print_string fmt (" " ^ assign); + if extract_as_unit then + (* Remark: this is only valid for HOL4 (for instance the Coq unit value is [tt]) *) + F.pp_print_string fmt "()" + else ( + F.pp_open_hvbox fmt 0; + F.pp_open_hvbox fmt ctx.indent_incr; + let lb, rb = + 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 -> ()); + let need_paren = inside && !backend = HOL4 in + if need_paren then F.pp_print_string fmt "("; + F.pp_open_hvbox fmt ctx.indent_incr; + if supd.init <> None then ( + let var_name = ctx_get_var (Option.get supd.init) ctx in + F.pp_print_string fmt var_name; F.pp_print_space fmt (); - F.pp_open_hvbox fmt ctx.indent_incr; - extract_texpression ctx fmt true fe; - F.pp_close_box fmt (); - F.pp_close_box fmt ()) - supd.updates; - F.pp_close_box fmt (); - F.pp_close_box fmt (); - F.pp_close_box fmt (); - F.pp_print_space fmt (); - F.pp_print_string fmt rb; - F.pp_close_box fmt () + F.pp_print_string fmt "with"; + F.pp_print_space fmt ()); + F.pp_open_hvbox fmt 0; + let delimiter = + match !backend with Lean -> "," | Coq | FStar | HOL4 -> ";" + in + let assign = + match !backend with Coq | Lean | HOL4 -> ":=" | FStar -> "=" + in + Collections.List.iter_link + (fun () -> + F.pp_print_string fmt delimiter; + F.pp_print_space fmt ()) + (fun (fid, fe) -> + F.pp_open_hvbox fmt ctx.indent_incr; + let f = ctx_get_field (AdtId supd.struct_id) fid ctx in + F.pp_print_string fmt f; + F.pp_print_string fmt (" " ^ assign); + F.pp_print_space fmt (); + F.pp_open_hvbox fmt ctx.indent_incr; + extract_texpression ctx fmt true fe; + F.pp_close_box fmt (); + F.pp_close_box fmt ()) + supd.updates; + F.pp_close_box fmt (); + 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 -> ()); + F.pp_close_box fmt ()) (** Insert a space, if necessary *) let insert_req_space (fmt : F.formatter) (space : bool ref) : unit = @@ -2098,17 +2569,27 @@ let insert_req_space (fmt : F.formatter) (space : bool ref) : unit = We return two contexts: - the context augmented with bindings for the type parameters - - the previous context augmented with bindings for the input values + - the context augmented with bindings for the type parameters *and* + bindings for the input values + + TODO: do we really need the first one? We should probably always use + the second one. + It comes from the fact that when we print the input values for the + decrease clause, we introduce bindings in the context (because we print + patterns, not the variables). We should figure a cleaner way. *) let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx) (fmt : F.formatter) (def : fun_decl) : extraction_ctx * extraction_ctx = (* Add the type parameters - note that we need those bindings only for the * body translation (they are not top-level) *) let ctx, _ = ctx_add_type_params def.signature.type_params ctx in - (* Print the parameters - rk.: we should have filtered the functions + (* Print the parameters - rem.: we should have filtered the functions * with no input parameters *) - (* The type parameters *) - if def.signature.type_params <> [] then ( + (* The type parameters. + + Note that in HOL4 we don't print the type parameters. + *) + if def.signature.type_params <> [] && !backend <> HOL4 then ( (* Open a box for the type parameters *) F.pp_open_hovbox fmt 0; insert_req_space fmt space; @@ -2122,7 +2603,10 @@ let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx) F.pp_print_string fmt ":"; F.pp_print_space fmt (); let type_keyword = - match !backend with FStar -> "Type0" | Coq | Lean -> "Type" + match !backend with + | FStar -> "Type0" + | Coq | Lean -> "Type" + | HOL4 -> raise (Failure "Unreachable") in F.pp_print_string fmt (type_keyword ^ ")"); (* Close the box for the type parameters *) @@ -2142,7 +2626,7 @@ let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx) F.pp_print_space fmt (); F.pp_print_string fmt ":"; F.pp_print_space fmt (); - extract_ty ctx fmt false lv.ty; + extract_ty ctx fmt TypeDeclId.Set.empty false lv.ty; F.pp_print_string fmt ")"; (* Close the box for the input parameters *) F.pp_close_box fmt (); @@ -2161,7 +2645,7 @@ let extract_fun_input_parameters_types (ctx : extraction_ctx) (fmt : F.formatter) (def : fun_decl) : unit = let extract_param (ty : ty) : unit = let inside = false in - extract_ty ctx fmt inside ty; + extract_ty ctx fmt TypeDeclId.Set.empty inside ty; F.pp_print_space fmt (); F.pp_print_string fmt "->"; F.pp_print_space fmt () @@ -2171,7 +2655,9 @@ let extract_fun_input_parameters_types (ctx : extraction_ctx) let assert_backend_supports_decreases_clauses () = match !backend with | FStar | Lean -> () - | _ -> failwith "decreases clauses only supported for the Lean & F* backends" + | _ -> + raise + (Failure "decreases clauses only supported for the Lean & F* backends") (** Extract a decreases clause function template body. @@ -2346,14 +2832,12 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx) (** Extract a function declaration. - Note that all the names used for extraction should already have been - registered. + This function is for all function declarations and all backends **at the exception** + of opaque (assumed/declared) functions for HOL4. - We take the definition of the forward translation as parameter (which is - equal to the definition to extract, if we extract a forward function) because - it is useful for the decrease clause. + See {!extract_fun_decl}. *) -let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) +let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) (kind : decl_kind) (has_decreases_clause : bool) (def : fun_decl) : unit = assert (not def.is_global_decl_body); (* Retrieve the function name *) @@ -2363,7 +2847,8 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) ctx in (* Add a break before *) - F.pp_print_break fmt 0 0; + if !backend <> HOL4 || not (decl_is_first_from_group kind) then + F.pp_print_break fmt 0 0; (* Print a comment to link the extracted type to its original rust definition *) extract_comment fmt ("[" ^ Print.fun_name_to_string def.basename ^ "]"); F.pp_print_space fmt (); @@ -2371,6 +2856,9 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) * one line and indents are correct *) F.pp_open_hvbox fmt 0; F.pp_open_vbox fmt ctx.indent_incr; + (* For HOL4: we may need to put parentheses around the definition *) + let parenthesize = !backend = HOL4 && decl_is_not_last_from_group kind in + if parenthesize then F.pp_print_string fmt "("; (* Open a box for "let FUN_NAME (PARAMS) : EFFECT =" *) F.pp_open_hovbox fmt ctx.indent_incr; (* > "let FUN_NAME" *) @@ -2382,12 +2870,16 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) *) let is_opaque_coq = !backend = Coq && is_opaque in let use_forall = is_opaque_coq && def.signature.type_params <> [] in - (* *) - let qualif = ctx.fmt.fun_decl_kind_to_qualif kind in - (* For Lean: we generate a record of assumed functions *) - if not (!backend = Lean && (kind = Assumed || kind = Declared)) then ( - F.pp_print_string fmt qualif; - F.pp_print_space fmt ()); + (* Print the qualifier ("assume", etc.). + + For Lean: we generate a record of assumed functions *) + (if not (!backend = Lean && (kind = Assumed || kind = Declared)) then + let qualif = ctx.fmt.fun_decl_kind_to_qualif kind in + match qualif with + | Some qualif -> + F.pp_print_string fmt qualif; + F.pp_print_space fmt () + | None -> ()); F.pp_print_string fmt def_name; F.pp_print_space fmt (); if use_forall then ( @@ -2428,7 +2920,8 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) if !backend = FStar then ( F.pp_print_string fmt "Tot"; F.pp_print_space fmt ())); - extract_ty ctx fmt has_decreases_clause def.signature.output; + extract_ty ctx fmt TypeDeclId.Set.empty has_decreases_clause + def.signature.output; (* Close the box for the return type *) F.pp_close_box fmt (); (* Print the decrease clause - rk.: a function with a decreases clause @@ -2468,6 +2961,8 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) in Collections.List.prefix num_fwd_inputs all_inputs in + (* TODO: we should probably print the input variables, not the typed + patterns *) let _ = List.fold_left (fun ctx (lv : typed_pattern) -> @@ -2487,7 +2982,7 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) (* Print the "=" *) if not is_opaque then ( F.pp_print_space fmt (); - let eq = match !backend with FStar -> "=" | Coq | Lean -> ":=" in + let eq = match !backend with FStar | HOL4 -> "=" | Coq | Lean -> ":=" in F.pp_print_string fmt eq); (* Close the box for "(PARAMS) : EFFECT =" *) F.pp_close_box fmt (); @@ -2569,17 +3064,82 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) F.pp_close_box fmt (); (* Close the box for the [decreasing by ...] *) F.pp_close_box fmt ()); - (* Add the definition group end delimiter *) - print_decl_end_delimiter fmt kind; + (* Close the parentheses *) + if parenthesize then F.pp_print_string fmt ")"; + (* Add the definition end delimiter *) + if !backend = HOL4 && decl_is_not_last_from_group kind then ( + F.pp_print_space fmt (); + F.pp_print_string fmt "/\\") + else if !backend = Coq && decl_is_last_from_group kind then ( + (* This is actually an end of group delimiter. For aesthetic reasons + we print it here instead of in {!end_fun_decl_group}. *) + F.pp_print_cut fmt (); + F.pp_print_string fmt "."); (* Close the outer box for the definition *) F.pp_close_box fmt (); (* Add breaks to insert new lines between definitions *) - F.pp_print_break fmt 0 0 + if !backend <> HOL4 || decl_is_not_last_from_group kind then + F.pp_print_break fmt 0 0 + +(** Extract an opaque function declaration to HOL4. + + Remark (SH): having to treat this specific case separately is very annoying, + but I could not find a better way. + *) +let extract_fun_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter) + (def : fun_decl) : unit = + (* Retrieve the definition name *) + let with_opaque_pre = false in + let def_name = + ctx_get_local_function with_opaque_pre def.def_id None None ctx + in + (* Add the type parameters - note that we need those bindings only for the + * generation of the type (they are not top-level) *) + let ctx, _ = ctx_add_type_params def.signature.type_params ctx in + (* Open a box for the whole definition *) + F.pp_open_hovbox fmt ctx.indent_incr; + (* Generate: `val _ = new_constant ("...",` *) + F.pp_print_string fmt ("val _ = new_constant (\"" ^ def_name ^ ", "); + (* Open a box for the type *) + F.pp_open_hvbox fmt 0; + (* Generate the type *) + extract_fun_input_parameters_types ctx fmt def; + extract_ty ctx fmt TypeDeclId.Set.empty false def.signature.output; + (* Close the box for the type *) + F.pp_close_box fmt (); + (* Close the parenthesis opened for the inputs of `new_constant` *) + F.pp_print_string fmt ")"; + (* Close the box for the definition *) + F.pp_close_box fmt () + +(** Extract a function declaration. + + Note that all the names used for extraction should already have been + registered. + + We take the definition of the forward translation as parameter (which is + equal to the definition to extract, if we extract a forward function) because + it is useful for the decrease clause. + + This function should be inserted between calls to {!start_fun_decl_group} + and {!end_fun_decl_group}. + *) +let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) + (kind : decl_kind) (has_decreases_clause : bool) (def : fun_decl) : unit = + assert (not def.is_global_decl_body); + (* We treat HOL4 opaque functions in a specific manner *) + if !backend = HOL4 && Option.is_none def.body then + extract_fun_decl_hol4_opaque ctx fmt def + else extract_fun_decl_gen ctx fmt kind has_decreases_clause def (** Extract a global declaration body of the shape "QUALIF NAME : TYPE = BODY" - with a custom body extractor + with a custom body extractor. + + We introduce this helper because every (non opaque) global declaration gets + extracted to two declarations, and we can actually factor out the generation + of those declarations. See {!extract_global_decl} for more explanations. *) -let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter) +let extract_global_decl_body_gen (ctx : extraction_ctx) (fmt : F.formatter) (kind : decl_kind) (name : string) (ty : ty) (extract_body : (F.formatter -> unit) Option.t) : unit = let is_opaque = Option.is_none extract_body in @@ -2591,8 +3151,11 @@ let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter) (* Open "QUALIF NAME : TYPE =" box (depth=1) *) F.pp_open_hovbox fmt ctx.indent_incr; (* Print "QUALIF NAME " *) - F.pp_print_string fmt (ctx.fmt.fun_decl_kind_to_qualif kind); - F.pp_print_space fmt (); + (match ctx.fmt.fun_decl_kind_to_qualif kind with + | Some qualif -> + F.pp_print_string fmt qualif; + F.pp_print_space fmt () + | None -> ()); F.pp_print_string fmt name; F.pp_print_space fmt (); @@ -2605,14 +3168,14 @@ let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter) (* Open "TYPE" box (depth=3) *) F.pp_open_hovbox fmt ctx.indent_incr; (* Print "TYPE" *) - extract_ty ctx fmt false ty; + extract_ty ctx fmt TypeDeclId.Set.empty false ty; (* Close "TYPE" box (depth=3) *) F.pp_close_box fmt (); if not is_opaque then ( (* Print " =" *) F.pp_print_space fmt (); - let eq = match !backend with FStar -> "=" | Coq | Lean -> ":=" in + let eq = match !backend with FStar | HOL4 -> "=" | Coq | Lean -> ":=" in F.pp_print_string fmt eq); (* Close ": TYPE =" box (depth=2) *) F.pp_close_box fmt (); @@ -2632,22 +3195,52 @@ let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter) F.pp_close_box fmt (); (* Coq: add a "." *) - print_decl_end_delimiter fmt Declared; + if !backend = Coq then ( + F.pp_print_cut fmt (); + F.pp_print_string fmt "."); (* Close the outer definition box (depth=0) *) F.pp_close_box fmt () +(** Extract an opaque global declaration for HOL4. + + Remark (SH): having to treat this specific case separately is very annoying, + but I could not find a better way. + *) +let extract_global_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter) + (name : string) (ty : ty) : unit = + (* Open the definition boxe (depth=0) *) + F.pp_open_hvbox fmt ctx.indent_incr; + (* [val ..._def = new_constant ("...",] *) + F.pp_open_hovbox fmt 0; + F.pp_print_string fmt + ("val " ^ name ^ "_def = new_constant (\"" ^ name ^ "\", "); + F.pp_close_box fmt (); + (* Print the type *) + F.pp_open_hovbox fmt 0; + extract_ty ctx fmt TypeDeclId.Set.empty false ty; + F.pp_close_box fmt (); + (* Close the definition boxe *) F.pp_close_box fmt () + (** Extract a global declaration. - We generate the body which computes the global value separately from the + We generate the body which *computes* the global value separately from the value declaration itself. For example in Rust, [static X: u32 = 3;] will be translated to the following F*: - [let x_body : result u32 = Return 3] - [let x_c : u32 = eval_global x_body] + [let x_body : result u32 = Return 3] (* this has type [result u32] *) + [let x_c : u32 = eval_global x_body] (* this has type [u32] (no [result]!) *) + + This function generates the two declarations. + + Remark: because global declaration groups are always singletons (i.e., + there are no groups of mutually recursive global declarations), this function + doesn't need to be called between calls to functions of the shape + [{start,end}_gloabl_decl_group], contrary to {!extract_type_decl} + and {!extract_fun_decl}. *) let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) (global : A.global_decl) (body : fun_decl) (interface : bool) : unit = @@ -2677,13 +3270,19 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) in match body.body with | None -> + (* No body: only generate a [val x_c : u32] declaration *) let kind = if interface then Declared else Assumed in - extract_global_decl_body ctx fmt kind decl_name decl_ty None + if !backend = HOL4 then + extract_global_decl_hol4_opaque ctx fmt decl_name decl_ty + else extract_global_decl_body_gen ctx fmt kind decl_name decl_ty None | Some body -> - extract_global_decl_body ctx fmt SingleNonRec body_name body_ty + (* There is a body *) + (* Generate: [let x_body : result u32 = Return 3] *) + extract_global_decl_body_gen ctx fmt SingleNonRec body_name body_ty (Some (fun fmt -> extract_texpression ctx fmt false body.body)); F.pp_print_break fmt 0 0; - extract_global_decl_body ctx fmt SingleNonRec decl_name decl_ty + (* Generate: [let x_c : u32 = eval_global x_body] *) + extract_global_decl_body_gen ctx fmt SingleNonRec decl_name decl_ty (Some (fun fmt -> let body = @@ -2691,6 +3290,7 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) | FStar -> "eval_global " ^ body_name | Lean -> "eval_global " ^ body_name ^ " (by simp)" | Coq -> body_name ^ "%global" + | HOL4 -> "get_return_value " ^ body_name in F.pp_print_string fmt body)); (* Add a break to insert lines between declarations *) @@ -2790,7 +3390,22 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_string fmt "=="; F.pp_print_space fmt (); let success = ctx_get_variant (Assumed Result) result_return_id ctx in - F.pp_print_string fmt ("." ^ success ^ " ())")); + F.pp_print_string fmt ("." ^ success ^ " ())") + | HOL4 -> + F.pp_print_string fmt "val _ = assert_return ("; + F.pp_print_string fmt "“"; + (* Note that if the function is opaque, the unit test will fail + because the normalizer will get stuck *) + let with_opaque_pre = ctx.use_opaque_pre in + let fun_name = + ctx_get_local_function with_opaque_pre def.def_id def.loop_id + def.back_id ctx + in + F.pp_print_string fmt fun_name; + if sg.inputs <> [] then ( + F.pp_print_space fmt (); + F.pp_print_string fmt "()"); + F.pp_print_string fmt "”)"); (* Close the box for the test *) F.pp_close_box fmt (); (* Add a break after *) diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 81bdd202..0a5d7df2 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -98,6 +98,19 @@ let decl_is_from_mut_rec_group (kind : decl_kind) : bool = | SingleNonRec | SingleRec | Assumed | Declared -> false | MutRecFirst | MutRecInner | MutRecLast -> true +let decl_is_first_from_group (kind : decl_kind) : bool = + match kind with + | SingleNonRec | SingleRec | MutRecFirst | Assumed | Declared -> true + | MutRecLast | MutRecInner -> false + +(** Return [true] if the declaration is not the last from its group of declarations. + + We need this because in some provers (e.g., HOL4), we need to delimit + the inner declarations (with `/\` for instance). + *) +let decl_is_not_last_from_group (kind : decl_kind) : bool = + not (decl_is_last_from_group kind) + (* TODO: this should a module we give to a functor! *) type type_decl_kind = Enum | Struct @@ -118,15 +131,20 @@ type formatter = { char_name : string; int_name : integer_type -> string; str_name : string; - type_decl_kind_to_qualif : decl_kind -> type_decl_kind option -> string; + type_decl_kind_to_qualif : + decl_kind -> type_decl_kind option -> string option; (** Compute the qualified for a type definition/declaration. For instance: "type", "and", etc. + + Remark: can return [None] for some backends like HOL4. *) - fun_decl_kind_to_qualif : decl_kind -> string; + fun_decl_kind_to_qualif : decl_kind -> string option; (** Compute the qualified for a function definition/declaration. For instance: "let", "let rec", "and", etc. + + Remark: can return [None] for some backends like HOL4. *) field_name : name -> FieldId.id -> string option -> string; (** Inputs: diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml index 1f5d1ed8..9b768f3b 100644 --- a/compiler/PureUtils.ml +++ b/compiler/PureUtils.ml @@ -169,7 +169,7 @@ let rec let_group_requires_parentheses (e : texpression) : bool = let texpression_requires_parentheses e = match !Config.backend with | FStar | Lean -> false - | Coq -> let_group_requires_parentheses e + | Coq | HOL4 -> let_group_requires_parentheses e let is_var (e : texpression) : bool = match e.e with Var _ -> true | _ -> false diff --git a/compiler/StringUtils.ml b/compiler/StringUtils.ml index 0fd46136..161df27b 100644 --- a/compiler/StringUtils.ml +++ b/compiler/StringUtils.ml @@ -96,6 +96,11 @@ let capitalize_first_letter (s : string) : string = let s = match s with [] -> s | c :: s' -> uppercase_ascii c :: s' in string_of_chars s +let lowercase_first_letter (s : string) : string = + let s = string_to_chars s in + let s = match s with [] -> s | c :: s' -> lowercase_ascii c :: s' in + string_of_chars s + (** Unit tests *) let _ = assert (to_camel_case "hello_world" = "HelloWorld"); diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 5252495d..5dc8664a 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -2642,7 +2642,7 @@ let wrap_in_match_fuel (fuel0 : VarId.id) (fuel : VarId.id) (body : texpression) let match_ty = body.ty in let match_e = Switch (fuel0, Match [ fail_branch; success_branch ]) in { e = match_e; ty = match_ty } - | Lean -> + | Lean | HOL4 -> (* We should have checked the command line arguments before *) raise (Failure "Unexpected") diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 409fc5d3..709b54a4 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -407,10 +407,9 @@ let module_has_opaque_decls (ctx : gen_ctx) : bool * bool = the declaration, if both booleans are [true]). *) let export_type (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) - (kind : ExtractBase.decl_kind) (id : Pure.TypeDeclId.id) - (extract_decl : bool) (extract_extra_info : bool) : unit = - (* Retrieve the declaration *) - let def = Pure.TypeDeclId.Map.find id ctx.trans_types in + (type_decl_group : Pure.TypeDeclId.Set.t) (kind : ExtractBase.decl_kind) + (def : Pure.type_decl) (extract_decl : bool) (extract_extra_info : bool) : + unit = (* Update the kind, if the type is opaque *) let is_opaque, kind = match def.kind with @@ -427,7 +426,8 @@ let export_type (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) (is_opaque && config.extract_opaque) || ((not is_opaque) && config.extract_transparent) then ( - if extract_decl then Extract.extract_type_decl ctx.extract_ctx fmt kind def; + if extract_decl then + Extract.extract_type_decl ctx.extract_ctx fmt type_decl_group kind def; if extract_extra_info then Extract.extract_type_decl_extra_info ctx.extract_ctx fmt kind def) @@ -438,9 +438,11 @@ let export_type (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) *) let export_types_group (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) (is_rec : bool) (ids : Pure.TypeDeclId.id list) : unit = + assert (ids <> []); let export_type = export_type fmt config ctx in - let export_type_decl kind id = export_type kind id true false in - let export_type_extra_info kind id = export_type kind id false true in + let ids_set = Pure.TypeDeclId.Set.of_list ids in + let export_type_decl kind id = export_type ids_set kind id true false in + let export_type_extra_info kind id = export_type ids_set kind id false true in (* Rem.: we shouldn't have (mutually) recursive opaque types *) let num_decls = List.length ids in @@ -452,22 +454,51 @@ let export_types_group (fmt : Format.formatter) (config : gen_config) else if i = num_decls - 1 then ExtractBase.MutRecLast else ExtractBase.MutRecInner in - (* Extract the type declarations *) + + (* Retrieve the declarations *) + let defs = + List.map (fun id -> Pure.TypeDeclId.Map.find id ctx.trans_types) ids + in + + (* Extract the type declarations. + + Because some declaration groups are delimited, we wrap the declarations + between [{start,end}_type_decl_group]. + + Ex.: + ==== + When targeting HOL4, the calls to [{start,end}_type_decl_group] would generate + the [Datatype] and [End] delimiters in the snippet of code below: + + {[ + Datatype: + tree = + TLeaf 'a + | TNode node ; + + node = + Node (tree list) + End + ]} + *) + Extract.start_type_decl_group ctx.extract_ctx fmt is_rec defs; List.iteri - (fun i id -> + (fun i def -> let kind = kind_from_index i in - export_type_decl kind id) - ids; + export_type_decl kind def) + defs; + Extract.end_type_decl_group fmt is_rec defs; + (* Export the extra information (ex.: [Arguments] instructions in Coq) *) List.iteri - (fun i id -> + (fun i def -> let kind = kind_from_index i in - export_type_extra_info kind id) - ids + export_type_extra_info kind def) + defs (** Export a global declaration. - TODO: check correct behaviour with opaque globals. + TODO: check correct behavior with opaque globals. *) let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) (id : A.GlobalDeclId.id) : unit = @@ -485,6 +516,11 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) && (((not is_opaque) && config.extract_transparent) || (is_opaque && config.extract_opaque)) then + (* We don't wrap global declaration groups between calls to functions + [{start, end}_global_decl_group] (which don't exist): global declaration + groups are always singletons, so the [extract_global_decl] function + takes care of generating the delimiters. + *) Extract.extract_global_decl ctx.extract_ctx fmt global body config.interface (** Utility. @@ -519,6 +555,20 @@ let export_functions_group_scc (fmt : Format.formatter) (config : gen_config) let is_mut_rec = List.length decls > 1 in assert ((not is_mut_rec) || is_rec); let decls_length = List.length decls in + (* We open and close the declaration group with [{start, end}_fun_decl_group]. + + Some backends require the groups to be delimited. For instance, if we target + HOL4, the calls to [{start, end}_fun_decl_group] would generate the + [val ... = Define `] and [`] delimiters in the snippet of code below: + + {[ + val ... = Define ` + (even (i : num) : bool result = if i = 0 then Return T else odd (i - 1)) /\ + (odd (i : num) : bool result = if i = 0 then Return F else even (i - 1)) + ` + ]} + *) + Extract.start_fun_decl_group ctx.extract_ctx fmt is_rec decls; List.iteri (fun i def -> let is_opaque = Option.is_none def.Pure.body in @@ -545,7 +595,8 @@ let export_functions_group_scc (fmt : Format.formatter) (config : gen_config) ((not is_opaque) && config.extract_transparent) || (is_opaque && config.extract_opaque) then Extract.extract_fun_decl ctx.extract_ctx fmt kind has_decr_clause def) - decls + decls; + Extract.end_fun_decl_group fmt is_rec decls (** Export a group of function declarations. @@ -586,6 +637,9 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config) fmt decl | Coq -> raise (Failure "Coq doesn't have decreases/termination clauses") + | HOL4 -> + raise + (Failure "HOL4 doesn't have decreases/termination clauses") in extract_decrease fwd; List.iter extract_decrease loop_fwds) @@ -610,14 +664,14 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config) (* Extract the function definitions *) (if config.extract_fun_decls then - (* Group the mutually recursive definitions *) - let subgroups = ReorderDecls.group_reorder_fun_decls decls in + (* Group the mutually recursive definitions *) + let subgroups = ReorderDecls.group_reorder_fun_decls decls in - (* Extract the subgroups *) - let export_subgroup (is_rec : bool) (decls : Pure.fun_decl list) : unit = - export_functions_group_scc fmt config ctx is_rec decls - in - List.iter (fun (is_rec, decls) -> export_subgroup is_rec decls) subgroups); + (* Extract the subgroups *) + let export_subgroup (is_rec : bool) (decls : Pure.fun_decl list) : unit = + export_functions_group_scc fmt config ctx is_rec decls + in + List.iter (fun (is_rec, decls) -> export_subgroup is_rec decls) subgroups); (* Insert unit tests if necessary *) if config.test_trans_unit_functions then @@ -733,7 +787,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string) | Lean -> Printf.fprintf out "-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS\n"; Printf.fprintf out "-- [%s]%s\n" rust_module_name custom_msg - | Coq | FStar -> + | Coq | FStar | HOL4 -> Printf.fprintf out "(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)\n"; Printf.fprintf out "(** [%s]%s *)\n" rust_module_name custom_msg); @@ -769,7 +823,17 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string) (* Add the custom imports *) List.iter (fun m -> Printf.fprintf out "import %s\n" m) custom_imports; (* Add the custom includes *) - List.iter (fun m -> Printf.fprintf out "import %s\n" m) custom_includes); + List.iter (fun m -> Printf.fprintf out "import %s\n" m) custom_includes + | HOL4 -> + Printf.fprintf out "open primitivesLib divDefLib\n"; + (* Add the custom imports and includes *) + let imports = custom_imports @ custom_includes in + if imports <> [] then + let imports = String.concat " " imports in + Printf.fprintf out "open %s\n\n" imports + else Printf.fprintf out "\n"; + (* Initialize the theory *) + Printf.fprintf out "val _ = new_theory \"%s\"\n\n" module_name); (* From now onwards, we use the formatter *) (* Set the margin *) Format.pp_set_margin fmt 80; @@ -787,6 +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 | Coq -> Printf.fprintf out "End %s .\n" module_name); (* Some logging *) @@ -807,7 +872,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : let variant_concatenate_type_name = (* For Lean, we exploit the fact that the variant name should always be prefixed with the type name to prevent collisions *) - match !Config.backend with Coq | FStar -> true | Lean -> false + match !Config.backend with Coq | FStar | HOL4 -> true | Lean -> false in let mk_formatter_and_names_map = Extract.mk_formatter_and_names_map in let fmt, names_map = @@ -896,6 +961,11 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : let basename = Filename.basename filename in (* Convert the case *) let module_name = StringUtils.to_camel_case basename in + let module_name = + if !Config.backend = HOL4 then + StringUtils.lowercase_first_letter module_name + else module_name + in (* Concatenate *) (module_name, Filename.concat dest_dir module_name) in @@ -938,30 +1008,34 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : assert !Config.split_files; mkdir_if (dest_dir ^^ module_name ^^ "Clauses"))); - (* Copy the "Primitives" file *) + (* Copy the "Primitives" file, if necessary *) let _ = (* Retrieve the executable's directory *) let exe_dir = Filename.dirname Sys.argv.(0) in - let primitives_src, primitives_destname = + let primitives_src_dest = match !Config.backend with - | Config.FStar -> ("/backends/fstar/Primitives.fst", "Primitives.fst") - | Config.Coq -> ("/backends/coq/Primitives.v", "Primitives.v") - | Config.Lean -> ("/backends/lean/Primitives.lean", "Base/Primitives.lean") + | FStar -> Some ("/backends/fstar/Primitives.fst", "Primitives.fst") + | Coq -> Some ("/backends/coq/Primitives.v", "Primitives.v") + | Lean -> Some ("/backends/lean/Primitives.lean", "Base/Primitives.lean") + | HOL4 -> None in - let src = open_in (exe_dir ^ primitives_src) in - let tgt_filename = Filename.concat dest_dir primitives_destname in - let tgt = open_out tgt_filename in - (* Very annoying: I couldn't find a "cp" function in the OCaml libraries... *) - try - while true do - (* We copy line by line *) - let line = input_line src in - Printf.fprintf tgt "%s\n" line - done - with End_of_file -> - close_in src; - close_out tgt; - log#linfo (lazy ("Copied: " ^ tgt_filename)) + match primitives_src_dest with + | None -> () + | Some (primitives_src, primitives_destname) -> ( + let src = open_in (exe_dir ^ primitives_src) in + let tgt_filename = Filename.concat dest_dir primitives_destname in + let tgt = open_out tgt_filename in + (* Very annoying: I couldn't find a "cp" function in the OCaml libraries... *) + try + while true do + (* We copy line by line *) + let line = input_line src in + Printf.fprintf tgt "%s\n" line + done + with End_of_file -> + close_in src; + close_out tgt; + log#linfo (lazy ("Copied: " ^ tgt_filename))) in (* Extract the file(s) *) @@ -976,14 +1050,22 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : in let module_delimiter = - match !Config.backend with FStar -> "." | Coq -> "_" | Lean -> "." + match !Config.backend with + | FStar -> "." + | Coq -> "_" + | Lean -> "." + | HOL4 -> "_" in let file_delimiter = if !Config.backend = Lean then "/" else module_delimiter in (* File extension for the "regular" modules *) let ext = - match !Config.backend with FStar -> ".fst" | Coq -> ".v" | Lean -> ".lean" + match !Config.backend with + | FStar -> ".fst" + | Coq -> ".v" + | Lean -> ".lean" + | HOL4 -> "Script.sml" in (* File extension for the opaque module *) let opaque_ext = @@ -991,161 +1073,165 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : | FStar -> ".fsti" | Coq -> ".v" | Lean -> ".lean" + | HOL4 -> "Script.sml" in (* Extract one or several files, depending on the configuration *) (if !Config.split_files then ( - let base_gen_config = - { - extract_types = false; - extract_decreases_clauses = !Config.extract_decreases_clauses; - extract_template_decreases_clauses = false; - extract_fun_decls = false; - extract_transparent = true; - extract_opaque = false; - extract_state_type = false; - extract_globals = false; - interface = false; - test_trans_unit_functions = false; - } - in - - (* Check if there are opaque types and functions - in which case we need - * to split *) - let has_opaque_types, has_opaque_funs = module_has_opaque_decls gen_ctx in - let has_opaque_types = has_opaque_types || !Config.use_state in - - (* Extract the types *) - (* If there are opaque types, we extract in an interface *) - let types_filename_ext = - match !Config.backend with - | FStar -> if has_opaque_types then ".fsti" else ".fst" - | Coq -> ".v" - | Lean -> ".lean" - in - let types_filename = - extract_filebasename ^ file_delimiter ^ "Types" ^ types_filename_ext - in - let types_module = module_name ^ module_delimiter ^ "Types" in - let types_config = - { - base_gen_config with - extract_types = true; - extract_opaque = true; - extract_state_type = !Config.use_state; - interface = has_opaque_types; - } - in - extract_file types_config gen_ctx types_filename crate.A.name types_module - ": type definitions" [] []; - - (* Extract the template clauses *) - (if needs_clauses_module && !Config.extract_template_decreases_clauses then - let template_clauses_filename = - extract_filebasename ^ file_delimiter ^ "Clauses" ^ file_delimiter - ^ "Template" ^ ext - in - let template_clauses_module = - module_name ^ module_delimiter ^ "Clauses" ^ module_delimiter ^ "Template" - in - let template_clauses_config = - { base_gen_config with extract_template_decreases_clauses = true } - in - extract_file template_clauses_config gen_ctx template_clauses_filename - crate.A.name template_clauses_module - ": templates for the decreases clauses" [ types_module ] []); - - (* Extract the opaque functions, if needed *) - let opaque_funs_module = - if has_opaque_funs then ( - let opaque_filename = - extract_filebasename ^ file_delimiter ^ "Opaque" ^ opaque_ext - in - let opaque_module = module_name ^ module_delimiter ^ "Opaque" in - let opaque_imported_module = - (* In the case of Lean, we declare an interface (a record) containing - the opaque definitions, and we leave it to the user to provide an - instance of this module. - - TODO: do the same for Coq. - TODO: do the same for the type definitions. - *) - if !Config.backend = Lean then - module_name ^ module_delimiter ^ "ExternalFuns" - else opaque_module - in - let opaque_config = - { - base_gen_config with - extract_fun_decls = true; - extract_transparent = false; - extract_opaque = true; - interface = true; - } - in - let gen_ctx = - { - gen_ctx with - extract_ctx = { gen_ctx.extract_ctx with use_opaque_pre = false }; - } - in - extract_file opaque_config gen_ctx opaque_filename crate.A.name - opaque_module ": opaque function definitions" [] [ types_module ]; - [ opaque_imported_module ]) - else [] - in - - (* Extract the functions *) - let fun_filename = extract_filebasename ^ file_delimiter ^ "Funs" ^ ext in - let fun_module = module_name ^ module_delimiter ^ "Funs" in - let fun_config = - { - base_gen_config with - extract_fun_decls = true; - extract_globals = true; - test_trans_unit_functions = !Config.test_trans_unit_functions; - } - in - let clauses_module = - if needs_clauses_module then - let clauses_submodule = - if !Config.backend = Lean then module_delimiter ^ "Clauses" else "" - in - [ module_name ^ clauses_submodule ^ module_delimiter ^ "Clauses" ] - else [] - in - extract_file fun_config gen_ctx fun_filename crate.A.name fun_module - ": function definitions" [] - ([ types_module ] @ opaque_funs_module @ clauses_module)) - else - let gen_config = - { - extract_types = true; - extract_decreases_clauses = !Config.extract_decreases_clauses; - extract_template_decreases_clauses = - !Config.extract_template_decreases_clauses; - extract_fun_decls = true; - extract_transparent = true; - extract_opaque = true; - extract_state_type = !Config.use_state; - extract_globals = true; - interface = false; - test_trans_unit_functions = !Config.test_trans_unit_functions; - } - in - (* Add the extension for F* *) - let extract_filename = extract_filebasename ^ ext in - extract_file gen_config gen_ctx extract_filename crate.A.name module_name "" - [] []); + let base_gen_config = + { + extract_types = false; + extract_decreases_clauses = !Config.extract_decreases_clauses; + extract_template_decreases_clauses = false; + extract_fun_decls = false; + extract_transparent = true; + extract_opaque = false; + extract_state_type = false; + extract_globals = false; + interface = false; + test_trans_unit_functions = false; + } + in + + (* Check if there are opaque types and functions - in which case we need + * to split *) + let has_opaque_types, has_opaque_funs = module_has_opaque_decls gen_ctx in + let has_opaque_types = has_opaque_types || !Config.use_state in + + (* Extract the types *) + (* If there are opaque types, we extract in an interface *) + let types_filename_ext = + match !Config.backend with + | FStar -> if has_opaque_types then ".fsti" else ".fst" + | Coq -> ".v" + | Lean -> ".lean" + | HOL4 -> "Script.sml" + in + let types_filename = + extract_filebasename ^ file_delimiter ^ "Types" ^ types_filename_ext + in + let types_module = module_name ^ module_delimiter ^ "Types" in + let types_config = + { + base_gen_config with + extract_types = true; + extract_opaque = true; + extract_state_type = !Config.use_state; + interface = has_opaque_types; + } + in + extract_file types_config gen_ctx types_filename crate.A.name types_module + ": type definitions" [] []; + + (* Extract the template clauses *) + (if needs_clauses_module && !Config.extract_template_decreases_clauses then + let template_clauses_filename = + extract_filebasename ^ file_delimiter ^ "Clauses" ^ file_delimiter + ^ "Template" ^ ext + in + let template_clauses_module = + module_name ^ module_delimiter ^ "Clauses" ^ module_delimiter + ^ "Template" + in + let template_clauses_config = + { base_gen_config with extract_template_decreases_clauses = true } + in + extract_file template_clauses_config gen_ctx template_clauses_filename + crate.A.name template_clauses_module + ": templates for the decreases clauses" [ types_module ] []); + + (* Extract the opaque functions, if needed *) + let opaque_funs_module = + if has_opaque_funs then ( + let opaque_filename = + extract_filebasename ^ file_delimiter ^ "Opaque" ^ opaque_ext + in + let opaque_module = module_name ^ module_delimiter ^ "Opaque" in + let opaque_imported_module = + (* In the case of Lean, we declare an interface (a record) containing + the opaque definitions, and we leave it to the user to provide an + instance of this module. + + TODO: do the same for Coq. + TODO: do the same for the type definitions. + *) + if !Config.backend = Lean then + module_name ^ module_delimiter ^ "ExternalFuns" + else opaque_module + in + let opaque_config = + { + base_gen_config with + extract_fun_decls = true; + extract_transparent = false; + extract_opaque = true; + interface = true; + } + in + let gen_ctx = + { + gen_ctx with + extract_ctx = { gen_ctx.extract_ctx with use_opaque_pre = false }; + } + in + extract_file opaque_config gen_ctx opaque_filename crate.A.name + opaque_module ": opaque function definitions" [] [ types_module ]; + [ opaque_imported_module ]) + else [] + in + + (* Extract the functions *) + let fun_filename = extract_filebasename ^ file_delimiter ^ "Funs" ^ ext in + let fun_module = module_name ^ module_delimiter ^ "Funs" in + let fun_config = + { + base_gen_config with + extract_fun_decls = true; + extract_globals = true; + test_trans_unit_functions = !Config.test_trans_unit_functions; + } + in + let clauses_module = + if needs_clauses_module then + let clauses_submodule = + if !Config.backend = Lean then module_delimiter ^ "Clauses" else "" + in + [ module_name ^ clauses_submodule ^ module_delimiter ^ "Clauses" ] + else [] + in + extract_file fun_config gen_ctx fun_filename crate.A.name fun_module + ": function definitions" [] + ([ types_module ] @ opaque_funs_module @ clauses_module)) + else + let gen_config = + { + extract_types = true; + extract_decreases_clauses = !Config.extract_decreases_clauses; + extract_template_decreases_clauses = + !Config.extract_template_decreases_clauses; + extract_fun_decls = true; + extract_transparent = true; + extract_opaque = true; + extract_state_type = !Config.use_state; + extract_globals = true; + interface = false; + test_trans_unit_functions = !Config.test_trans_unit_functions; + } + in + (* Add the extension for F* *) + let extract_filename = extract_filebasename ^ ext in + extract_file gen_config gen_ctx extract_filename crate.A.name module_name + "" [] []); (* Generate the build file *) match !Config.backend with - | Coq | FStar -> + | Coq | FStar | HOL4 -> () (* Nothing to do - TODO: we might want to generate the _CoqProject file for Coq. But then we can't modify it if we want to add more files for the proofs for instance. But we might want to put the proofs elsewhere anyway. Remark: there is the same problem for Lean actually. + Maybe generate it if the user asks for it? *) | Lean -> (* diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v index dc97a9e9..940b8650 100644 --- a/tests/coq/betree/BetreeMain_Funs.v +++ b/tests/coq/betree/BetreeMain_Funs.v @@ -56,7 +56,7 @@ Definition betree_fresh_node_id_back (counter : u64) : result u64 := (** [betree_main::betree::NodeIdCounter::{0}::new] *) Definition betree_node_id_counter_new_fwd : result Betree_node_id_counter_t := - Return {| Betree_node_id_counter_next_node_id := (0%u64) |} + Return {| Betree_node_id_counter_next_node_id := 0%u64 |} . (** [betree_main::betree::NodeIdCounter::{0}::fresh_id] *) @@ -75,7 +75,7 @@ Definition betree_node_id_counter_fresh_id_back (** [core::num::u64::{10}::MAX] *) Definition core_num_u64_max_body : result u64 := - Return (18446744073709551615%u64) + Return 18446744073709551615%u64 . Definition core_num_u64_max_c : u64 := core_num_u64_max_body%global. @@ -86,7 +86,7 @@ Definition betree_upsert_update_fwd | None => match st with | BetreeUpsertFunStateAdd v => Return v - | BetreeUpsertFunStateSub i => Return (0%u64) + | BetreeUpsertFunStateSub i => Return 0%u64 end | Some prev0 => match st with @@ -94,7 +94,7 @@ Definition betree_upsert_update_fwd margin <- u64_sub core_num_u64_max_c prev0; if margin s>= v then u64_add prev0 v else Return core_num_u64_max_c | BetreeUpsertFunStateSub v => - if prev0 s>= v then u64_sub prev0 v else Return (0%u64) + if prev0 s>= v then u64_sub prev0 v else Return 0%u64 end end . @@ -107,7 +107,7 @@ Fixpoint betree_list_len_fwd | S n0 => match self with | BetreeListCons t tl => i <- betree_list_len_fwd T n0 tl; u64_add 1%u64 i - | BetreeListNil => Return (0%u64) + | BetreeListNil => Return 0%u64 end end . @@ -1061,8 +1061,7 @@ Definition betree_be_tree_new_fwd |}; Betree_be_tree_node_id_cnt := node_id_cnt0; Betree_be_tree_root := - (BetreeNodeLeaf - {| Betree_leaf_id := id; Betree_leaf_size := (0%u64) |}) + (BetreeNodeLeaf {| Betree_leaf_id := id; Betree_leaf_size := 0%u64 |}) |}) . diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v index 1245c654..6bc82677 100644 --- a/tests/coq/hashmap/Hashmap_Funs.v +++ b/tests/coq/hashmap/Hashmap_Funs.v @@ -49,7 +49,7 @@ Definition hash_map_new_with_capacity_fwd i0 <- usize_div i max_load_divisor; Return {| - Hash_map_num_entries := (0%usize); + Hash_map_num_entries := 0%usize; Hash_map_max_load_factor := (max_load_dividend, max_load_divisor); Hash_map_max_load := i0; Hash_map_slots := slots @@ -58,7 +58,7 @@ Definition hash_map_new_with_capacity_fwd (** [hashmap::HashMap::{0}::new] *) Definition hash_map_new_fwd (T : Type) (n : nat) : result (Hash_map_t T) := - hash_map_new_with_capacity_fwd T n (32%usize) (4%usize) (5%usize) + hash_map_new_with_capacity_fwd T n 32%usize 4%usize 5%usize . (** [hashmap::HashMap::{0}::clear] *) @@ -82,10 +82,10 @@ Fixpoint hash_map_clear_loop_fwd_back (** [hashmap::HashMap::{0}::clear] *) Definition hash_map_clear_fwd_back (T : Type) (n : nat) (self : Hash_map_t T) : result (Hash_map_t T) := - v <- hash_map_clear_loop_fwd_back T n self.(Hash_map_slots) (0%usize); + v <- hash_map_clear_loop_fwd_back T n self.(Hash_map_slots) 0%usize; Return {| - Hash_map_num_entries := (0%usize); + Hash_map_num_entries := 0%usize; Hash_map_max_load_factor := self.(Hash_map_max_load_factor); Hash_map_max_load := self.(Hash_map_max_load); Hash_map_slots := v @@ -186,7 +186,7 @@ Definition hash_map_insert_no_resize_fwd_back . (** [core::num::u32::{9}::MAX] *) -Definition core_num_u32_max_body : result u32 := Return (4294967295%u32). +Definition core_num_u32_max_body : result u32 := Return 4294967295%u32. Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global. (** [hashmap::HashMap::{0}::move_elements_from_list] *) @@ -259,8 +259,7 @@ Definition hash_map_try_resize_fwd_back i2 <- usize_mul capacity 2%usize; ntable <- hash_map_new_with_capacity_fwd T n i2 i i0; p <- - hash_map_move_elements_fwd_back T n ntable self.(Hash_map_slots) - (0%usize); + hash_map_move_elements_fwd_back T n ntable self.(Hash_map_slots) 0%usize; let (ntable0, _) := p in Return {| @@ -546,36 +545,36 @@ Definition hash_map_remove_back (** [hashmap::test1] *) Definition test1_fwd (n : nat) : result unit := hm <- hash_map_new_fwd u64 n; - hm0 <- hash_map_insert_fwd_back u64 n hm (0%usize) (42%u64); - hm1 <- hash_map_insert_fwd_back u64 n hm0 (128%usize) (18%u64); - hm2 <- hash_map_insert_fwd_back u64 n hm1 (1024%usize) (138%u64); - hm3 <- hash_map_insert_fwd_back u64 n hm2 (1056%usize) (256%u64); - i <- hash_map_get_fwd u64 n hm3 (128%usize); + hm0 <- hash_map_insert_fwd_back u64 n hm 0%usize 42%u64; + hm1 <- hash_map_insert_fwd_back u64 n hm0 128%usize 18%u64; + hm2 <- hash_map_insert_fwd_back u64 n hm1 1024%usize 138%u64; + hm3 <- hash_map_insert_fwd_back u64 n hm2 1056%usize 256%u64; + i <- hash_map_get_fwd u64 n hm3 128%usize; if negb (i s= 18%u64) then Fail_ Failure else ( - hm4 <- hash_map_get_mut_back u64 n hm3 (1024%usize) (56%u64); - i0 <- hash_map_get_fwd u64 n hm4 (1024%usize); + hm4 <- hash_map_get_mut_back u64 n hm3 1024%usize 56%u64; + i0 <- hash_map_get_fwd u64 n hm4 1024%usize; if negb (i0 s= 56%u64) then Fail_ Failure else ( - x <- hash_map_remove_fwd u64 n hm4 (1024%usize); + x <- hash_map_remove_fwd u64 n hm4 1024%usize; match x with | None => Fail_ Failure | Some x0 => if negb (x0 s= 56%u64) then Fail_ Failure else ( - hm5 <- hash_map_remove_back u64 n hm4 (1024%usize); - i1 <- hash_map_get_fwd u64 n hm5 (0%usize); + hm5 <- hash_map_remove_back u64 n hm4 1024%usize; + i1 <- hash_map_get_fwd u64 n hm5 0%usize; if negb (i1 s= 42%u64) then Fail_ Failure else ( - i2 <- hash_map_get_fwd u64 n hm5 (128%usize); + i2 <- hash_map_get_fwd u64 n hm5 128%usize; if negb (i2 s= 18%u64) then Fail_ Failure else ( - i3 <- hash_map_get_fwd u64 n hm5 (1056%usize); + i3 <- hash_map_get_fwd u64 n hm5 1056%usize; if negb (i3 s= 256%u64) then Fail_ Failure else Return tt))) end)) . diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v index 804f466a..2d1bcda6 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v @@ -51,7 +51,7 @@ Definition hashmap_hash_map_new_with_capacity_fwd i0 <- usize_div i max_load_divisor; Return {| - Hashmap_hash_map_num_entries := (0%usize); + Hashmap_hash_map_num_entries := 0%usize; Hashmap_hash_map_max_load_factor := (max_load_dividend, max_load_divisor); Hashmap_hash_map_max_load := i0; Hashmap_hash_map_slots := slots @@ -61,7 +61,7 @@ Definition hashmap_hash_map_new_with_capacity_fwd (** [hashmap_main::hashmap::HashMap::{0}::new] *) Definition hashmap_hash_map_new_fwd (T : Type) (n : nat) : result (Hashmap_hash_map_t T) := - hashmap_hash_map_new_with_capacity_fwd T n (32%usize) (4%usize) (5%usize) + hashmap_hash_map_new_with_capacity_fwd T n 32%usize 4%usize 5%usize . (** [hashmap_main::hashmap::HashMap::{0}::clear] *) @@ -89,10 +89,10 @@ Definition hashmap_hash_map_clear_fwd_back := v <- hashmap_hash_map_clear_loop_fwd_back T n self.(Hashmap_hash_map_slots) - (0%usize); + 0%usize; Return {| - Hashmap_hash_map_num_entries := (0%usize); + Hashmap_hash_map_num_entries := 0%usize; Hashmap_hash_map_max_load_factor := self.(Hashmap_hash_map_max_load_factor); Hashmap_hash_map_max_load := self.(Hashmap_hash_map_max_load); @@ -204,7 +204,7 @@ Definition hashmap_hash_map_insert_no_resize_fwd_back . (** [core::num::u32::{9}::MAX] *) -Definition core_num_u32_max_body : result u32 := Return (4294967295%u32). +Definition core_num_u32_max_body : result u32 := Return 4294967295%u32. Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global. (** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *) @@ -283,7 +283,7 @@ Definition hashmap_hash_map_try_resize_fwd_back ntable <- hashmap_hash_map_new_with_capacity_fwd T n i2 i i0; p <- hashmap_hash_map_move_elements_fwd_back T n ntable - self.(Hashmap_hash_map_slots) (0%usize); + self.(Hashmap_hash_map_slots) 0%usize; let (ntable0, _) := p in Return {| @@ -602,36 +602,36 @@ Definition hashmap_hash_map_remove_back (** [hashmap_main::hashmap::test1] *) Definition hashmap_test1_fwd (n : nat) : result unit := hm <- hashmap_hash_map_new_fwd u64 n; - hm0 <- hashmap_hash_map_insert_fwd_back u64 n hm (0%usize) (42%u64); - hm1 <- hashmap_hash_map_insert_fwd_back u64 n hm0 (128%usize) (18%u64); - hm2 <- hashmap_hash_map_insert_fwd_back u64 n hm1 (1024%usize) (138%u64); - hm3 <- hashmap_hash_map_insert_fwd_back u64 n hm2 (1056%usize) (256%u64); - i <- hashmap_hash_map_get_fwd u64 n hm3 (128%usize); + hm0 <- hashmap_hash_map_insert_fwd_back u64 n hm 0%usize 42%u64; + hm1 <- hashmap_hash_map_insert_fwd_back u64 n hm0 128%usize 18%u64; + hm2 <- hashmap_hash_map_insert_fwd_back u64 n hm1 1024%usize 138%u64; + hm3 <- hashmap_hash_map_insert_fwd_back u64 n hm2 1056%usize 256%u64; + i <- hashmap_hash_map_get_fwd u64 n hm3 128%usize; if negb (i s= 18%u64) then Fail_ Failure else ( - hm4 <- hashmap_hash_map_get_mut_back u64 n hm3 (1024%usize) (56%u64); - i0 <- hashmap_hash_map_get_fwd u64 n hm4 (1024%usize); + hm4 <- hashmap_hash_map_get_mut_back u64 n hm3 1024%usize 56%u64; + i0 <- hashmap_hash_map_get_fwd u64 n hm4 1024%usize; if negb (i0 s= 56%u64) then Fail_ Failure else ( - x <- hashmap_hash_map_remove_fwd u64 n hm4 (1024%usize); + x <- hashmap_hash_map_remove_fwd u64 n hm4 1024%usize; match x with | None => Fail_ Failure | Some x0 => if negb (x0 s= 56%u64) then Fail_ Failure else ( - hm5 <- hashmap_hash_map_remove_back u64 n hm4 (1024%usize); - i1 <- hashmap_hash_map_get_fwd u64 n hm5 (0%usize); + hm5 <- hashmap_hash_map_remove_back u64 n hm4 1024%usize; + i1 <- hashmap_hash_map_get_fwd u64 n hm5 0%usize; if negb (i1 s= 42%u64) then Fail_ Failure else ( - i2 <- hashmap_hash_map_get_fwd u64 n hm5 (128%usize); + i2 <- hashmap_hash_map_get_fwd u64 n hm5 128%usize; if negb (i2 s= 18%u64) then Fail_ Failure else ( - i3 <- hashmap_hash_map_get_fwd u64 n hm5 (1056%usize); + i3 <- hashmap_hash_map_get_fwd u64 n hm5 1056%usize; if negb (i3 s= 256%u64) then Fail_ Failure else Return tt))) end)) . diff --git a/tests/coq/misc/Constants.v b/tests/coq/misc/Constants.v index cd3880c2..6a5f2696 100644 --- a/tests/coq/misc/Constants.v +++ b/tests/coq/misc/Constants.v @@ -7,11 +7,11 @@ Local Open Scope Primitives_scope. Module Constants. (** [constants::X0] *) -Definition x0_body : result u32 := Return (0%u32). +Definition x0_body : result u32 := Return 0%u32. Definition x0_c : u32 := x0_body%global. (** [core::num::u32::{9}::MAX] *) -Definition core_num_u32_max_body : result u32 := Return (4294967295%u32). +Definition core_num_u32_max_body : result u32 := Return 4294967295%u32. Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global. (** [constants::X1] *) @@ -19,7 +19,7 @@ Definition x1_body : result u32 := Return core_num_u32_max_c. Definition x1_c : u32 := x1_body%global. (** [constants::X2] *) -Definition x2_body : result u32 := Return (3%u32). +Definition x2_body : result u32 := Return 3%u32. Definition x2_c : u32 := x2_body%global. (** [constants::incr] *) @@ -27,7 +27,7 @@ Definition incr_fwd (n : u32) : result u32 := u32_add n 1%u32. (** [constants::X3] *) -Definition x3_body : result u32 := incr_fwd (32%u32). +Definition x3_body : result u32 := incr_fwd 32%u32. Definition x3_c : u32 := x3_body%global. (** [constants::mk_pair0] *) @@ -48,11 +48,11 @@ Definition mk_pair1_fwd (x : u32) (y : u32) : result (Pair_t u32 u32) := . (** [constants::P0] *) -Definition p0_body : result (u32 * u32) := mk_pair0_fwd (0%u32) (1%u32). +Definition p0_body : result (u32 * u32) := mk_pair0_fwd 0%u32 1%u32. Definition p0_c : (u32 * u32) := p0_body%global. (** [constants::P1] *) -Definition p1_body : result (Pair_t u32 u32) := mk_pair1_fwd (0%u32) (1%u32). +Definition p1_body : result (Pair_t u32 u32) := mk_pair1_fwd 0%u32 1%u32. Definition p1_c : Pair_t u32 u32 := p1_body%global. (** [constants::P2] *) @@ -61,7 +61,7 @@ Definition p2_c : (u32 * u32) := p2_body%global. (** [constants::P3] *) Definition p3_body : result (Pair_t u32 u32) := - Return {| Pair_x := (0%u32); Pair_y := (1%u32) |} + Return {| Pair_x := 0%u32; Pair_y := 1%u32 |} . Definition p3_c : Pair_t u32 u32 := p3_body%global. @@ -77,7 +77,7 @@ Definition wrap_new_fwd (T : Type) (val : T) : result (Wrap_t T) := . (** [constants::Y] *) -Definition y_body : result (Wrap_t i32) := wrap_new_fwd i32 (2%i32). +Definition y_body : result (Wrap_t i32) := wrap_new_fwd i32 2%i32. Definition y_c : Wrap_t i32 := y_body%global. (** [constants::unwrap_y] *) @@ -89,7 +89,7 @@ Definition yval_body : result i32 := unwrap_y_fwd. Definition yval_c : i32 := yval_body%global. (** [constants::get_z1::Z1] *) -Definition get_z1_z1_body : result i32 := Return (3%i32). +Definition get_z1_z1_body : result i32 := Return 3%i32. Definition get_z1_z1_c : i32 := get_z1_z1_body%global. (** [constants::get_z1] *) @@ -101,7 +101,7 @@ Definition add_fwd (a : i32) (b : i32) : result i32 := i32_add a b. (** [constants::Q1] *) -Definition q1_body : result i32 := Return (5%i32). +Definition q1_body : result i32 := Return 5%i32. Definition q1_c : i32 := q1_body%global. (** [constants::Q2] *) @@ -109,7 +109,7 @@ Definition q2_body : result i32 := Return q1_c. Definition q2_c : i32 := q2_body%global. (** [constants::Q3] *) -Definition q3_body : result i32 := add_fwd q2_c (3%i32). +Definition q3_body : result i32 := add_fwd q2_c 3%i32. Definition q3_c : i32 := q3_body%global. (** [constants::get_z2] *) @@ -118,7 +118,7 @@ Definition get_z2_fwd : result i32 := . (** [constants::S1] *) -Definition s1_body : result u32 := Return (6%u32). +Definition s1_body : result u32 := Return 6%u32. Definition s1_c : u32 := s1_body%global. (** [constants::S2] *) @@ -130,7 +130,7 @@ Definition s3_body : result (Pair_t u32 u32) := Return p3_c. Definition s3_c : Pair_t u32 u32 := s3_body%global. (** [constants::S4] *) -Definition s4_body : result (Pair_t u32 u32) := mk_pair1_fwd (7%u32) (8%u32). +Definition s4_body : result (Pair_t u32 u32) := mk_pair1_fwd 7%u32 8%u32. Definition s4_c : Pair_t u32 u32 := s4_body%global. End Constants . diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v index b5476f25..05dd8f2e 100644 --- a/tests/coq/misc/External_Funs.v +++ b/tests/coq/misc/External_Funs.v @@ -46,7 +46,7 @@ Definition test_new_non_zero_u32_fwd (** [external::test_vec] *) Definition test_vec_fwd : result unit := - let v := vec_new u32 in _ <- vec_push_back u32 v (0%u32); Return tt + let v := vec_new u32 in _ <- vec_push_back u32 v 0%u32; Return tt . (** Unit test for [external::test_vec] *) @@ -89,15 +89,15 @@ Definition test_custom_swap_back (x : u32) (y : u32) (st : state) (st0 : state) : result (state * (u32 * u32)) := - custom_swap_back u32 x y st (1%u32) st0 + custom_swap_back u32 x y st 1%u32 st0 . (** [external::test_swap_non_zero] *) Definition test_swap_non_zero_fwd (x : u32) (st : state) : result (state * u32) := - p <- swap_fwd u32 x (0%u32) st; + p <- swap_fwd u32 x 0%u32 st; let (st0, _) := p in - p0 <- swap_back u32 x (0%u32) st st0; + p0 <- swap_back u32 x 0%u32 st st0; let (st1, p1) := p0 in let (x0, _) := p1 in if x0 s= 0%u32 then Fail_ Failure else Return (st1, x0) diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v index bcbfc8df..a5cb3688 100644 --- a/tests/coq/misc/Loops.v +++ b/tests/coq/misc/Loops.v @@ -19,7 +19,7 @@ Fixpoint sum_loop_fwd (n : nat) (max : u32) (i : u32) (s : u32) : result u32 := (** [loops::sum] *) Definition sum_fwd (n : nat) (max : u32) : result u32 := - sum_loop_fwd n max (0%u32) (0%u32) + sum_loop_fwd n max 0%u32 0%u32 . (** [loops::sum_with_mut_borrows] *) @@ -39,7 +39,7 @@ Fixpoint sum_with_mut_borrows_loop_fwd (** [loops::sum_with_mut_borrows] *) Definition sum_with_mut_borrows_fwd (n : nat) (max : u32) : result u32 := - sum_with_mut_borrows_loop_fwd n max (0%u32) (0%u32) + sum_with_mut_borrows_loop_fwd n max 0%u32 0%u32 . (** [loops::sum_with_shared_borrows] *) @@ -59,7 +59,7 @@ Fixpoint sum_with_shared_borrows_loop_fwd (** [loops::sum_with_shared_borrows] *) Definition sum_with_shared_borrows_fwd (n : nat) (max : u32) : result u32 := - sum_with_shared_borrows_loop_fwd n max (0%u32) (0%u32) + sum_with_shared_borrows_loop_fwd n max 0%u32 0%u32 . (** [loops::clear] *) @@ -72,7 +72,7 @@ Fixpoint clear_loop_fwd_back if i s< i0 then ( i1 <- usize_add i 1%usize; - v0 <- vec_index_mut_back u32 v i (0%u32); + v0 <- vec_index_mut_back u32 v i 0%u32; clear_loop_fwd_back n0 v0 i1) else Return v end @@ -80,7 +80,7 @@ Fixpoint clear_loop_fwd_back (** [loops::clear] *) Definition clear_fwd_back (n : nat) (v : vec u32) : result (vec u32) := - clear_loop_fwd_back n v (0%usize) + clear_loop_fwd_back n v 0%usize . (** [loops::List] *) @@ -201,7 +201,7 @@ Fixpoint get_elem_mut_loop_fwd (** [loops::get_elem_mut] *) Definition get_elem_mut_fwd (n : nat) (slots : vec (List_t usize)) (x : usize) : result usize := - l <- vec_index_mut_fwd (List_t usize) slots (0%usize); + l <- vec_index_mut_fwd (List_t usize) slots 0%usize; get_elem_mut_loop_fwd n x l . @@ -228,9 +228,9 @@ Definition get_elem_mut_back (n : nat) (slots : vec (List_t usize)) (x : usize) (ret : usize) : result (vec (List_t usize)) := - l <- vec_index_mut_fwd (List_t usize) slots (0%usize); + l <- vec_index_mut_fwd (List_t usize) slots 0%usize; l0 <- get_elem_mut_loop_back n x l ret; - vec_index_mut_back (List_t usize) slots (0%usize) l0 + vec_index_mut_back (List_t usize) slots 0%usize l0 . (** [loops::get_elem_shared] *) @@ -250,7 +250,7 @@ Fixpoint get_elem_shared_loop_fwd (** [loops::get_elem_shared] *) Definition get_elem_shared_fwd (n : nat) (slots : vec (List_t usize)) (x : usize) : result usize := - l <- vec_index_fwd (List_t usize) slots (0%usize); + l <- vec_index_fwd (List_t usize) slots 0%usize; get_elem_shared_loop_fwd n x l . diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v index 826b52b6..96d62711 100644 --- a/tests/coq/misc/NoNestedBorrows.v +++ b/tests/coq/misc/NoNestedBorrows.v @@ -87,8 +87,8 @@ Definition get_max_fwd (x : u32) (y : u32) : result u32 := (** [no_nested_borrows::test3] *) Definition test3_fwd : result unit := - x <- get_max_fwd (4%u32) (3%u32); - y <- get_max_fwd (10%u32) (11%u32); + x <- get_max_fwd 4%u32 3%u32; + y <- get_max_fwd 10%u32 11%u32; z <- u32_add x y; if negb (z s= 15%u32) then Fail_ Failure else Return tt . @@ -98,8 +98,7 @@ Check (test3_fwd )%return. (** [no_nested_borrows::test_neg1] *) Definition test_neg1_fwd : result unit := - y <- i32_neg (3%i32); - if negb (y s= (-3)%i32) then Fail_ Failure else Return tt + y <- i32_neg 3%i32; if negb (y s= (-3)%i32) then Fail_ Failure else Return tt . (** Unit test for [no_nested_borrows::test_neg1] *) @@ -162,7 +161,7 @@ Definition test_panic_fwd (b : bool) : result unit := (** [no_nested_borrows::test_copy_int] *) Definition test_copy_int_fwd : result unit := - y <- copy_int_fwd (0%i32); + y <- copy_int_fwd 0%i32; if negb (0%i32 s= y) then Fail_ Failure else Return tt . @@ -177,7 +176,7 @@ Definition is_cons_fwd (T : Type) (l : List_t T) : result bool := (** [no_nested_borrows::test_is_cons] *) Definition test_is_cons_fwd : result unit := let l := ListNil in - b <- is_cons_fwd i32 (ListCons (0%i32) l); + b <- is_cons_fwd i32 (ListCons 0%i32 l); if negb b then Fail_ Failure else Return tt . @@ -196,7 +195,7 @@ Definition split_list_fwd (** [no_nested_borrows::test_split_list] *) Definition test_split_list_fwd : result unit := let l := ListNil in - p <- split_list_fwd i32 (ListCons (0%i32) l); + p <- split_list_fwd i32 (ListCons 0%i32 l); let (hd, _) := p in if negb (hd s= 0%i32) then Fail_ Failure else Return tt . @@ -217,12 +216,12 @@ Definition choose_back (** [no_nested_borrows::choose_test] *) Definition choose_test_fwd : result unit := - z <- choose_fwd i32 true (0%i32) (0%i32); + z <- choose_fwd i32 true 0%i32 0%i32; z0 <- i32_add z 1%i32; if negb (z0 s= 1%i32) then Fail_ Failure else ( - p <- choose_back i32 true (0%i32) (0%i32) z0; + p <- choose_back i32 true 0%i32 0%i32 z0; let (x, y) := p in if negb (x s= 1%i32) then Fail_ Failure @@ -258,7 +257,7 @@ Arguments TreeNode {T} _ _ _. Fixpoint list_length_fwd (T : Type) (l : List_t T) : result u32 := match l with | ListCons t l1 => i <- list_length_fwd T l1; u32_add 1%u32 i - | ListNil => Return (0%u32) + | ListNil => Return 0%u32 end . @@ -317,34 +316,34 @@ Definition list_rev_fwd_back (T : Type) (l : List_t T) : result (List_t T) := (** [no_nested_borrows::test_list_functions] *) Definition test_list_functions_fwd : result unit := let l := ListNil in - let l0 := ListCons (2%i32) l in - let l1 := ListCons (1%i32) l0 in - i <- list_length_fwd i32 (ListCons (0%i32) l1); + let l0 := ListCons 2%i32 l in + let l1 := ListCons 1%i32 l0 in + i <- list_length_fwd i32 (ListCons 0%i32 l1); if negb (i s= 3%u32) then Fail_ Failure else ( - i0 <- list_nth_shared_fwd i32 (ListCons (0%i32) l1) (0%u32); + i0 <- list_nth_shared_fwd i32 (ListCons 0%i32 l1) 0%u32; if negb (i0 s= 0%i32) then Fail_ Failure else ( - i1 <- list_nth_shared_fwd i32 (ListCons (0%i32) l1) (1%u32); + i1 <- list_nth_shared_fwd i32 (ListCons 0%i32 l1) 1%u32; if negb (i1 s= 1%i32) then Fail_ Failure else ( - i2 <- list_nth_shared_fwd i32 (ListCons (0%i32) l1) (2%u32); + i2 <- list_nth_shared_fwd i32 (ListCons 0%i32 l1) 2%u32; if negb (i2 s= 2%i32) then Fail_ Failure else ( - ls <- list_nth_mut_back i32 (ListCons (0%i32) l1) (1%u32) (3%i32); - i3 <- list_nth_shared_fwd i32 ls (0%u32); + ls <- list_nth_mut_back i32 (ListCons 0%i32 l1) 1%u32 3%i32; + i3 <- list_nth_shared_fwd i32 ls 0%u32; if negb (i3 s= 0%i32) then Fail_ Failure else ( - i4 <- list_nth_shared_fwd i32 ls (1%u32); + i4 <- list_nth_shared_fwd i32 ls 1%u32; if negb (i4 s= 3%i32) then Fail_ Failure else ( - i5 <- list_nth_shared_fwd i32 ls (2%u32); + i5 <- list_nth_shared_fwd i32 ls 2%u32; if negb (i5 s= 2%i32) then Fail_ Failure else Return tt)))))) . @@ -448,7 +447,7 @@ Arguments Struct_with_pair_p {T1} {T2}. (** [no_nested_borrows::new_pair1] *) Definition new_pair1_fwd : result (Struct_with_pair_t u32 u32) := - Return {| Struct_with_pair_p := {| Pair_x := (1%u32); Pair_y := (2%u32) |} |} + Return {| Struct_with_pair_p := {| Pair_x := 1%u32; Pair_y := 2%u32 |} |} . (** [no_nested_borrows::test_constants] *) @@ -486,29 +485,26 @@ Check (test_weird_borrows1_fwd )%return. (** [no_nested_borrows::test_mem_replace] *) Definition test_mem_replace_fwd_back (px : u32) : result u32 := - let y := mem_replace_fwd u32 px (1%u32) in - if negb (y s= 0%u32) then Fail_ Failure else Return (2%u32) + let y := mem_replace_fwd u32 px 1%u32 in + if negb (y s= 0%u32) then Fail_ Failure else Return 2%u32 . (** [no_nested_borrows::test_shared_borrow_bool1] *) Definition test_shared_borrow_bool1_fwd (b : bool) : result u32 := - if b then Return (0%u32) else Return (1%u32) + if b then Return 0%u32 else Return 1%u32 . (** [no_nested_borrows::test_shared_borrow_bool2] *) Definition test_shared_borrow_bool2_fwd : result u32 := - Return (0%u32). + Return 0%u32. (** [no_nested_borrows::test_shared_borrow_enum1] *) Definition test_shared_borrow_enum1_fwd (l : List_t u32) : result u32 := - match l with - | ListCons i l0 => Return (1%u32) - | ListNil => Return (0%u32) - end + match l with | ListCons i l0 => Return 1%u32 | ListNil => Return 0%u32 end . (** [no_nested_borrows::test_shared_borrow_enum2] *) Definition test_shared_borrow_enum2_fwd : result u32 := - Return (0%u32). + Return 0%u32. End NoNestedBorrows . diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v index 8045222d..513bc749 100644 --- a/tests/coq/misc/Paper.v +++ b/tests/coq/misc/Paper.v @@ -12,7 +12,7 @@ Definition ref_incr_fwd_back (x : i32) : result i32 := (** [paper::test_incr] *) Definition test_incr_fwd : result unit := - x <- ref_incr_fwd_back (0%i32); + x <- ref_incr_fwd_back 0%i32; if negb (x s= 1%i32) then Fail_ Failure else Return tt . @@ -32,12 +32,12 @@ Definition choose_back (** [paper::test_choose] *) Definition test_choose_fwd : result unit := - z <- choose_fwd i32 true (0%i32) (0%i32); + z <- choose_fwd i32 true 0%i32 0%i32; z0 <- i32_add z 1%i32; if negb (z0 s= 1%i32) then Fail_ Failure else ( - p <- choose_back i32 true (0%i32) (0%i32) z0; + p <- choose_back i32 true 0%i32 0%i32 z0; let (x, y) := p in if negb (x s= 1%i32) then Fail_ Failure @@ -86,18 +86,18 @@ Fixpoint list_nth_mut_back Fixpoint sum_fwd (l : List_t i32) : result i32 := match l with | ListCons x tl => i <- sum_fwd tl; i32_add x i - | ListNil => Return (0%i32) + | ListNil => Return 0%i32 end . (** [paper::test_nth] *) Definition test_nth_fwd : result unit := let l := ListNil in - let l0 := ListCons (3%i32) l in - let l1 := ListCons (2%i32) l0 in - x <- list_nth_mut_fwd i32 (ListCons (1%i32) l1) (2%u32); + let l0 := ListCons 3%i32 l in + let l1 := ListCons 2%i32 l0 in + x <- list_nth_mut_fwd i32 (ListCons 1%i32 l1) 2%u32; x0 <- i32_add x 1%i32; - l2 <- list_nth_mut_back i32 (ListCons (1%i32) l1) (2%u32) x0; + l2 <- list_nth_mut_back i32 (ListCons 1%i32 l1) 2%u32 x0; i <- sum_fwd l2; if negb (i s= 7%i32) then Fail_ Failure else Return tt . diff --git a/tests/hol4/Holmakefile.template b/tests/hol4/Holmakefile.template new file mode 100644 index 00000000..c86fad70 --- /dev/null +++ b/tests/hol4/Holmakefile.template @@ -0,0 +1,3 @@ + +all: $(DEFAULT_TARGETS) +.PHONY: all diff --git a/tests/hol4/Makefile b/tests/hol4/Makefile new file mode 100644 index 00000000..fa2c5512 --- /dev/null +++ b/tests/hol4/Makefile @@ -0,0 +1,39 @@ +ALL_DIRS ?= $(filter-out %~ Makefile% Holmakefile%, $(wildcard *)) + +UPDATE_DIRS = $(addprefix update-,$(ALL_DIRS)) + +VERIFY_DIRS = $(addprefix verif-,$(ALL_DIRS)) + +CLEAN_DIRS = $(addprefix clean-,$(ALL_DIRS)) + +COPY_HOLMAKEFILE = $(addprefix copy-holmakefile-,$(ALL_DIRS)) + +# This allows to customize the INCLUDES variable of the Holmakefile - useful for Nix +HOLMAKEFILE_INCLUDES ?= ../../../backends/hol4 + +.PHONY: all +all: prepare-projects verify + +.PHONY: prepare-projects +prepare-projects: $(COPY_HOLMAKEFILE) + +.PHONY: prepare-projects +copy-holmakefile-%: + rm -f $*/Holmakefile + echo "# This file was automatically generated - modify ../Holmakefile.template instead" >> $*/Holmakefile + echo "INCLUDES = " $(HOLMAKEFILE_INCLUDES) >> $*/Holmakefile + cat Holmakefile.template >> $*/Holmakefile + +.PHONY: verify +verify: $(VERIFY_DIRS) + +.PHONY: verif-% +verif-%: + cd $* && Holmake + +.PHONY: clean +clean: $(CLEAN_DIRS) + +.PHONY: clean-% +clean-%: + cd $* && Holmake clean diff --git a/tests/lean/misc-no_nested_borrows/NoNestedBorrows.lean b/tests/lean/misc-no_nested_borrows/NoNestedBorrows.lean index a73848de..12c7d8f7 100644 --- a/tests/lean/misc-no_nested_borrows/NoNestedBorrows.lean +++ b/tests/lean/misc-no_nested_borrows/NoNestedBorrows.lean @@ -249,8 +249,10 @@ def choose_test_fwd : Result Unit := def test_char_fwd : Result Char := Result.ret 'a' +mutual + /- [no_nested_borrows::NodeElem] -/ -mutual inductive node_elem_t (T : Type) := +inductive node_elem_t (T : Type) := | Cons : tree_t T -> node_elem_t T -> node_elem_t T | Nil : node_elem_t T @@ -258,6 +260,7 @@ mutual inductive node_elem_t (T : Type) := inductive tree_t (T : Type) := | Leaf : T -> tree_t T | Node : T -> node_elem_t T -> tree_t T -> tree_t T + end /- [no_nested_borrows::list_length] -/ |