cakeml/translator/okasaki-examples/PhysicistsQueueScript.sml at master · CakeML/cakeml · GitHub

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
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
(*
  This is an example of applying the translator to the Physicists
  Heap algorithm from Chris Okasaki's book.
*)
Theory PhysicistsQueue
Ancestors
  list arithmetic ListProg
Libs
  ml_translatorLib

val _ = translation_extends "ListProg";

(* implementation *)

Datatype:
  queue = QUEUE ('a list) num ('a list) num ('a list)
End

Definition empty_def:
  empty = QUEUE [] 0 [] 0 []
End
val r = translate empty_def;

Definition is_empty_def:
  is_empty (QUEUE _ lenf _ _ _) = (lenf = 0)
End
val r = translate is_empty_def;

Definition checkw_def:
  (checkw (QUEUE [] lenf f lenr r) = QUEUE f lenf f lenr r) /\
  (checkw q = q)
End
val r = translate checkw_def;

Definition check_def:
  check (QUEUE w lenf f lenr r) =
    if lenr <= lenf
      then checkw (QUEUE w lenf f lenr r)
      else checkw (QUEUE f (lenf + lenr) (f ++ REVERSE r) 0 [])
End
val r = translate check_def;

Definition snoc_def:
  snoc (QUEUE w lenf f lenr r) x =
    check (QUEUE w lenf f (lenr+1) (x::r))
End
val r = translate snoc_def;

Definition head_def:
  head (QUEUE (x::xs) lenf f lenr r) = x
End
val r = translate head_def;

Definition tail_def:
  tail (QUEUE (x::xs) lenf f lenr r) = check (QUEUE xs (lenf-1) (TL f) lenr r)
End
val r = translate tail_def;

(* verification proof *)

Definition queue_inv_def:
  queue_inv q (QUEUE w lenf f lenr r) <=>
    (q = f ++ REVERSE r) /\ (lenr = LENGTH r) /\ (lenf = LENGTH f) /\
    lenr <= lenf /\ ((w = []) ==> (q = [])) /\ isPREFIX w f
End

Theorem empty_thm[local]:
  !xs. queue_inv xs empty = (xs = [])
Proof
  EVAL_TAC THEN SIMP_TAC std_ss []
QED

Theorem is_empty_thm[local]:
  !q xs. queue_inv xs q ==> (is_empty q = (xs = []))
Proof
  Cases THEN Cases_on `l` THEN EVAL_TAC THEN SRW_TAC [] []
  THEN Cases_on `l0` THEN FULL_SIMP_TAC (srw_ss()) [APPEND_eq_NIL,LENGTH_NIL]
QED

Theorem isPREFIX_APPEND[local]:
  !xs ys. isPREFIX xs (xs ++ ys)
Proof
  Induct THEN FULL_SIMP_TAC (srw_ss()) [isPREFIX]
QED

Theorem isPREFIX_REFL[local]:
  !xs ys. isPREFIX xs xs
Proof
  Induct THEN FULL_SIMP_TAC (srw_ss()) [isPREFIX]
QED

Theorem snoc_thm[local]:
  !q xs x. queue_inv xs q ==> queue_inv (xs ++ [x]) (snoc q x)
Proof
  Cases THEN Cases_on `l`
  THEN FULL_SIMP_TAC (srw_ss()) [queue_inv_def,snoc_def,check_def,checkw_def]
  THEN SRW_TAC [] [] THEN FULL_SIMP_TAC (srw_ss())
    [queue_inv_def,snoc_def,check_def,checkw_def,ADD1]
  THEN Cases_on `l0` THEN FULL_SIMP_TAC (srw_ss())
    [queue_inv_def,snoc_def,check_def,checkw_def,ADD1]
  THEN FULL_SIMP_TAC std_ss [isPREFIX_APPEND,GSYM APPEND_ASSOC]
  THEN DECIDE_TAC
QED

Theorem head_thm[local]:
  !q x xs. queue_inv (x::xs) q ==> (head q = x)
Proof
  Cases THEN Cases_on `l` THEN EVAL_TAC THEN SRW_TAC [] []
  THEN Cases_on `l0` THEN FULL_SIMP_TAC (srw_ss()) [REVERSE_DEF,LENGTH_NIL]
QED

Theorem tail_thm[local]:
  !q x xs. queue_inv (x::xs) q ==> queue_inv xs (tail q)
Proof
  Cases THEN Cases_on `l`
  THEN FULL_SIMP_TAC (srw_ss()) [queue_inv_def,tail_def,check_def,checkw_def]
  THEN SRW_TAC [] [] THEN FULL_SIMP_TAC (srw_ss())
    [queue_inv_def,tail_def,check_def,checkw_def,ADD1] THEN Cases_on `l0`
  THEN FULL_SIMP_TAC (srw_ss()) [REVERSE_DEF,LENGTH_NIL,isPREFIX_REFL,checkw_def]
  THEN1 (Cases_on `t` THEN FULL_SIMP_TAC (srw_ss()) [LENGTH_NIL,checkw_def,queue_inv_def]
    THEN FULL_SIMP_TAC std_ss [queue_inv_def]
    THEN REPEAT STRIP_TAC THEN FULL_SIMP_TAC (srw_ss())
      [LENGTH_NIL,checkw_def,isPREFIX_REFL,isPREFIX_APPEND])
  THEN1 (Cases_on `t'` THEN FULL_SIMP_TAC (srw_ss()) [LENGTH_NIL,checkw_def,queue_inv_def]
    THEN FULL_SIMP_TAC std_ss [queue_inv_def]
    THEN REPEAT STRIP_TAC THEN FULL_SIMP_TAC (srw_ss())
      [LENGTH_NIL,checkw_def,isPREFIX_REFL,isPREFIX_APPEND] THEN DECIDE_TAC)
QED