summaryrefslogtreecommitdiff
path: root/tests/hol4/external/external_FunsScript.sml
blob: f3692ee248865788df304a2286781dc8bd62b000 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
(** [external]: function definitions *)
open primitivesLib divDefLib
open external_TypesTheory external_OpaqueTheory

val _ = new_theory "external_Funs"


val swap_fwd_def = Define 
  (** [external::swap]: forward function *)
  swap_fwd (x : 't) (y : 't) (st : state) : (state # unit) result =
    do
    (st0, _) <- core_mem_swap_fwd x y st;
    (st1, _) <- core_mem_swap_back0 x y st st0;
    (st2, _) <- core_mem_swap_back1 x y st st1;
    Return (st2, ())
    od


val swap_back_def = Define 
  (** [external::swap]: backward function 0 *)
  swap_back
    (x : 't) (y : 't) (st : state) (st0 : state) : (state # ('t # 't)) result =
    do
    (st1, _) <- core_mem_swap_fwd x y st;
    (st2, x0) <- core_mem_swap_back0 x y st st1;
    (_, y0) <- core_mem_swap_back1 x y st st2;
    Return (st0, (x0, y0))
    od


val test_new_non_zero_u32_fwd_def = Define 
  (** [external::test_new_non_zero_u32]: forward function *)
  test_new_non_zero_u32_fwd
    (x : u32) (st : state) : (state # core_num_nonzero_non_zero_u32_t) result =
    do
    (st0, opt) <- core_num_nonzero_non_zero_u32_new_fwd x st;
    core_option_option_unwrap_fwd opt st0
    od


val test_vec_fwd_def = Define 
  (** [external::test_vec]: forward function *)
  test_vec_fwd : unit result =
    let v = vec_new in do
                       _ <- vec_push_back v (int_to_u32 0);
                       Return ()
                       od


(** Unit test for [external::test_vec] *)
val _ = assert_return (“test_vec_fwd”)

val custom_swap_fwd_def = Define 
  (** [external::custom_swap]: forward function *)
  custom_swap_fwd (x : 't) (y : 't) (st : state) : (state # 't) result =
    do
    (st0, _) <- core_mem_swap_fwd x y st;
    (st1, x0) <- core_mem_swap_back0 x y st st0;
    (st2, _) <- core_mem_swap_back1 x y st st1;
    Return (st2, x0)
    od


val custom_swap_back_def = Define 
  (** [external::custom_swap]: backward function 0 *)
  custom_swap_back
    (x : 't) (y : 't) (st : state) (ret : 't) (st0 : state) :
    (state # ('t # 't)) result
    =
    do
    (st1, _) <- core_mem_swap_fwd x y st;
    (st2, _) <- core_mem_swap_back0 x y st st1;
    (_, y0) <- core_mem_swap_back1 x y st st2;
    Return (st0, (ret, y0))
    od


val test_custom_swap_fwd_def = Define 
  (** [external::test_custom_swap]: forward function *)
  test_custom_swap_fwd
    (x : u32) (y : u32) (st : state) : (state # unit) result =
    do
    (st0, _) <- custom_swap_fwd x y st;
    Return (st0, ())
    od


val test_custom_swap_back_def = Define 
  (** [external::test_custom_swap]: backward function 0 *)
  test_custom_swap_back
    (x : u32) (y : u32) (st : state) (st0 : state) :
    (state # (u32 # u32)) result
    =
    custom_swap_back x y st (int_to_u32 1) st0


val test_swap_non_zero_fwd_def = Define 
  (** [external::test_swap_non_zero]: forward function *)
  test_swap_non_zero_fwd (x : u32) (st : state) : (state # u32) result =
    do
    (st0, _) <- swap_fwd x (int_to_u32 0) st;
    (st1, (x0, _)) <- swap_back x (int_to_u32 0) st st0;
    if x0 = int_to_u32 0 then Fail Failure else Return (st1, x0)
    od


val _ = export_theory ()