Unity/mk_unity_prog.ml

   1 (*---------------------------------------------------------------------------*)
   2 (*
   3    File:         mk_unity_prog.sml
   4
   5    Description:
   6
   7    A back-end definition for the HOL-UNITY compiler programming language.
   8    =====================================================================
   9
  10    This file introduces general definitions for describing a program
  11    in HOL-UNITY.
  12
  13    Author:       (c) Copyright 1992-2008
  14                  by Flemming Andersen & Kim Dam Petersen
  15    Date:         August 3, 1992
  16    Updated:      May 4, 1995
  17    Updated:      March 22, 2006
  18    Last Update:  December 30, 2007
  19
  20      The functions below are based on the following representations:
  21
  22      type 'loc  =                               ``program variable location''
  23      type 'val  =                               ``program value''
  24      type state = ('loc -> 'val)                ``program state''
  25
  26      type t xpr = state -> t                    ``expression of type t''
  27      type t asg = t -> state -> state -> state  ``assignment of type t''
  28      type t var = (t xpr, t asg)                ``variable of type t''
  29
  30      type atom  = state -> state                ``atomic (singleton action)''
  31      type par   = state -> state -> state       ``parallel action''
  32      type int   = atom list                     ``interleaved action (program)''
  33      type seq   = var -> num -> (int list # num)``sequential action''
  34
  35
  36      Description of type representation: (Added: March 22, 2006)
  37      -----------------------------------------------------------
  38
  39      'loc    is an atomic (location) value that identifies a variable.
  40              Composite variables, such as arrays and lists has a
  41              single identifier. Assignment to a composite part is
  42              considered an assignment to the complete variable, that
  43              doesn't change the non-assigned parts of the variable.
  44
  45      'val    is a generic value type of all variables.
  46              It is constructed as a union of the types of the
  47              variables in the program. Each program will for each type
  48              of variable define a pair of functions to respectively
  49              encode and decode values of the type of the variable into
  50              and from the generic type 'val.
  51
  52      state   is a state that associates each variable (identified by it's
  53              'loc location) with it's current value (encoded in the
  54              generic type 'val of value).
  55              A state represents the values of every variable at a
  56              given moment.
  57              A state is implemented as a map from variable locations
  58              ('loc) to the generic value ('val) of the applied
  59              variable location.
  60
  61      -----
  62
  63      xpr     'val xpr - generic typed expression.
  64
  65      t xpr   is an expression of some (decoded) type t.
  66              An expression represents a state dependent value, ie. a
  67              value that depends on the values of variables.
  68              An expression is implemented as map from a state (in
  69              which the value is to be interpreted) to the value of the
  70              expression in that state.
  71
  72      t asg   is a assignment to a variable of type t.
  73              An assignment represents the change in state due to
  74              assignment of some variable to a value.  An assignment is
  75              implemented as a map from the value to be assigned, the
  76              original state and a previous state to the final state.
  77              The need for two parameter states: original and previous
  78              is due to the fact that assignment Consider the
  79              (high-level) assignment:
  80
  81              INITIALLY
  82                 a[0] = 0 /\ a[1] = 1
  83              ASSIGN
  84                 a[a[0]], a[a[1]] := 1, 0
  85
  86              The right-hand-side expression, and the left-hand-side
  87              index expression should be evaluated in the original
  88              state.
  89
  90              The parallel assignments of:
  91                 a[a[0]], a[a[1]] := 1, 0
  92              must be "transformed" into a single assignment of a:
  93                 a := a[a[i] => 1, a[j] => 0]
  94              If more variables are to be assigned we get:
  95                 i, j, a := 1, 0, a[a[i] => 1, a[j] => 0]
  96              A parallel assignment is evaluated in sequence; it is
  97              transformed into:
  98                 [ i := <1> ] ; [ j := <0> ] ; [ a := <a[a[i] => 1, a[j] => 0> ]
  99              It should be obvious that the expression in <>-braces has
 100              to be evaluated in the original state of the parallel
 101              assignment, whereas the sequential assignments has to be
 102              evaluated in the state that is the result of the previous
 103              assignment. This explains the need for two state
 104              parameters.
 105
 106              ** To Be Changed **
 107
 108      t var   is a variable of type t.
 109              A variable is represented by a pair that allow read- and
 110              write- access to the variable.
 111              ** To Be Changed **
 112
 113      atom    is an atomic action.
 114              An atomic action represents the state change associated
 115              with a single variable assignments.  An atomic action is
 116              implemented as a function, that given an initial state
 117              returns the state after executing the atomic action.  **
 118              To Be Changed **
 119
 120      par     is a parallel action.
 121              A parallel action represents the state change associated
 122              with multiple atomic actions, ex.
 123                (a[0] := a[1]) || (a[1] := a[0]).
 124              A parallel action is implemented as a function of an
 125              original- and previous state, that return a next
 126              state. The use of original- and previous state is
 127              explained above under section "t asg".
 128              ** To Be Changed **
 129
 130      int     is an interleaved action.
 131              An interleaved action represents the semantic of an
 132              interleaved action.  An interleaved action is implemented
 133              as a funtion that given an initial state returns the
 134              state after evaluating the interleaved action.
 135
 136      seq     is a sequential action.
 137              A sequential action is a sequence of interleaved
 138              actions. Each interleaved action is identified with a
 139              numeric label.  A sequential action is represented as a
 140              function that takes a program counter variable location,
 141              a NUM -encode and -decode function and an initial label
 142              for the action and returns a pair with a list of
 143              interleaved actions that implements the individual
 144              actions to be executed in sequence and a numeric label
 145              that represents the end of the sequential action.  This
 146              label is used as initial label for an optional sequential
 147              action that is compositionally added to the current.
 148
 149              Example: val s1 : seq = `` Computer generated seq '';
 150                       val s2 : seq = `` Computer generated seq '';
 151                       val s1s2 : seq = fn pc => mk => ds => l0 =>
 152                           let val (lst1, l1) = s1 pc mk ds l0 in
 153                           let val (lst2, l2) = s2 pc mk ds l1 in
 154                             (APPEND lst1 lst2, l2)
 155
 156
 157 [Flemming, May 1995:
 158
 159             Whereas we leave it for now due to the otherwize need for
 160             updating the compiler, assignment COULD BE CHANGED to the
 161             alternative below...]
 162
 163             An alternative way of implementing multiple parallel
 164             assignment exists:
 165
 166             1. Introduce a parallel variable assignment operator,
 167                which takes a list of locations and a list of evaluated
 168                generic typed expressions and performs the
 169                assignment. There will no problems with side-effects,
 170                due to the fact that all values has been evaluated.
 171
 172                define
 173                  ParAsg ([]: 'loc list) ([] : 'val list) (s : state) : state = s
 174                |  ParAsg (loc::locs) (val :: vals) =
 175                       ParAsg locs vals (fn l => (l == loc) ? val | s l))
 176                |  ParAsg _ _ = raise "ParAsg: location and value list differ in length";
 177
 178                The new type of ParAsg becomes:
 179
 180                ParAsg : 'loc list -> 'val list -> state -> state
 181
 182                If we redefine the type asg we get
 183
 184                ParAsg : 'loc list -> 'val list -> asg
 185
 186             2. Introduce a list evaluation operator:
 187
 188                define
 189                    EvalList ([] : (state -> 'val) list) (s : state) : 'val list = []
 190                 |  EvalList (genExp :: genExps) s = (genExp s) :: EvalList genExps s;
 191
 192             3. Compile a source parallel assignment into two lists:
 193                locs of the variables being assigned, and exps of
 194                component transformed expressions using decoded
 195                types. This process is part of the exisiting compiler.
 196
 197             4. Prepend each expression in exps with the proper encode
 198                function This produces a list genExps where every
 199                element is a generic typed expression.
 200
 201             5. The final representaion can now be expressed as:
 202
 203                ...
 204                val locs_123    : 'loc list = [ ``Generated by compiler'' ]
 205                val genExps_123 : 'val list = [ ``Generated by compiler'' ]
 206                val parAsg_123  : asg       = (ParAsg locs_123) o (EvalList genExps_123)
 207                ...
 208
 209             a)  A consequence of this is that VAR parameters should be
 210                 represented by their 'loc location.
 211             b)  A variable component can not be used as argument for a
 212                 VAR parameter, but still be used for a value parameter.
 213             c)  The assignment and update funtion will be deprecated.
 214             d)  The write part of a variable pair has to be replaced
 215                 with it's 'loc location.
 216             e)  The representation of an atomic action should be changed
 217                 such that it is based on the variable locations and the
 218                 assigned expressions. (How do we handle components???)
 219
 220 *)
 221 (*---------------------------------------------------------------------------*)
 222
 223
 224 let NUM     = `:num`;;
 225 let BOOL    = `:bool`;;
 226 let VAR_TP  = (fun s -> mk_vartype("'"^s));;
 227 let LST     = (fun t -> mk_type("list",[t]));;
 228 let PRD     = (fun (l,r) -> mk_type("prod",[l;r]));;
 229 let FUN     = (fun (l,r) -> mk_type("fun",[l;r]));;
 230 let rec FNC =
 231    function (l,[])      -> l
 232           | (l,(r::rs)) -> FUN(l,FNC(r,rs));;
 233
 234 let LOC = VAR_TP"loc";;
 235 let VAL = VAR_TP"val";;
 236 let STA = FUN(LOC,VAL);;
 237 let ACT = FUN(STA,STA);;
 238 let INT = LST(ACT);;
 239
 240 let XPR = (fun t -> FUN(STA,t));;
 241 let ASG = (fun t -> FNC(XPR t,[STA; STA; STA]));;
 242 let VAR = (fun t -> PRD(XPR t, ASG t));;
 243 let PAR = FNC(STA,[STA; STA]);;
 244 let SEQ = FUN(LOC, FUN(FUN(NUM,VAL), FUN(FUN(VAL,NUM), FUN(NUM, PRD(INT,NUM)))));;
 245
 246 (*---------------------------------------------------------------------------*)
 247 (*
 248   Defining Variable extraction functions
 249 *)
 250 (*---------------------------------------------------------------------------*)
 251
 252 let t   = mk_vartype"'t";;
 253 let v   = mk_var("v", VAR t);;
 254
 255 new_type_abbrev("stype",
 256    `:'loc->'val`);;
 257 new_type_abbrev("vtype",
 258    `:(stype->'t)#((stype->'t)->stype->stype->stype)`);;
 259 new_type_abbrev("vindex_type",
 260    `:(stype->'i->'t)#((stype->'i->'t)->stype->stype->stype)`);;
 261 new_type_abbrev("vpair_type",
 262    `:(stype->'a#'b)#((stype->'a#'b)->stype->stype->stype)`);;
 263 new_type_abbrev("seq_type",
 264    `:'loc->(num->'val)->('val->num)->num->(stype->stype)list#num`);;
 265
 266
 267 (*
 268  * Extraction expression of a variable
 269  *)
 270 let VAR_EXP = new_definition (`VAR_EXP (v:vtype) = FST v`);;
 271
 272 (*
 273  * Extraction assignment of a variable
 274  *)
 275 let VAR_ASG = new_definition (`VAR_ASG (v:vtype) = SND v`);;
 276
 277 (*---------------------------------------------------------------------------*)
 278 (*
 279   Location to variable translator functions
 280 *)
 281 (*---------------------------------------------------------------------------*)
 282
 283 let loc = mk_var("loc",LOC);;
 284 let s   = mk_var("s",  STA);;
 285 let s0  = mk_var("s0", STA);;
 286 let ds  = mk_var("ds", FUN(VAL,t));;
 287 let mk  = mk_var("mk", FUN(t,VAL));;
 288 let e   = mk_var("e", XPR t);;
 289
 290 (*
 291  * Translate a location to an expression
 292  *)
 293 let LOC_EXP = new_definition
 294   (`LOC_EXP loc (ds:'val->'t) (s:stype) = ds (s loc)`);;
 295
 296 (*
 297  * Translate a location to an assignment
 298  *)
 299 let LOC_ASG = new_definition
 300   (`LOC_ASG loc (mk:'t->'val) (e:stype->'t)
 301                              (s0:stype) (s:stype) l =
 302       (if (l = loc) then (mk (e s0)) else (s l))`);;
 303
 304 (*
 305  * Translate a location to a variable pair
 306  *)
 307 let LOC_VAR = new_definition
 308   (`LOC_VAR (loc:'loc) (mk:'t->'val) (ds:'val->'t) =
 309        (LOC_EXP loc ds, LOC_ASG loc mk)`);;
 310
 311 (*---------------------------------------------------------------------------*)
 312 (*
 313   Array (index) functions
 314 *)
 315 (*---------------------------------------------------------------------------*)
 316
 317 (*
 318  * Generate index expression
 319  *
 320  * IndexExp [(i,v),...] a
 321  *)
 322 let INDEX_EXP = new_definition
 323    (`(INDEX_EXP (a:stype->('i->'t)) (i:stype->'i) (s:stype) =
 324           (a s) (i s))`);;
 325
 326 (*
 327  * Generate updated index expression (index, exp and array are frozen)
 328  *
 329  * UpdIndex [(i,v),...] a
 330  *)
 331 let UPD_INDEX = new_definition
 332   (`(UPD_INDEX (i:'i) (c:'t) (a:'i->'t) j = (if (j = i) then c else (a j)))`);;
 333
 334 (*
 335  * Generate updated index expression (index and exp are frozen)
 336  *
 337  * UPD_INDEX_XPR [(i,v),...] a
 338  *)
 339 let UPD_INDEX_EXP = new_definition
 340   (`(UPD_INDEX_EXP (i:'i) (c:'t) (a:stype->'i->'t) (s:stype) =
 341        UPD_INDEX i c (a s))`);;
 342
 343 (*
 344  * Assignment part from Index of a variable
 345  *)
 346 let VAR_INDEX_ASG = new_definition
 347   (`VAR_INDEX_ASG
 348      (i:stype->'i) (v:vindex_type)
 349      (e:stype->'t) (s0:stype) (s:stype) =
 350          VAR_ASG v (UPD_INDEX_EXP (i s0) (e s0) (VAR_EXP v)) s0 s`);;
 351
 352 (*
 353  * Expression part from Index of a variable
 354  *)
 355 let VAR_INDEX_EXP = new_definition
 356   (`VAR_INDEX_EXP
 357      (i:stype->'i) (v:vindex_type) (s:stype) =
 358         (VAR_EXP v s) (i s)`);;
 359
 360 (*
 361  * Index variable
 362  *)
 363 let VAR_INDEXVAR = new_definition
 364   (`VAR_INDEXVAR (i:stype->'i) (v:vindex_type) =
 365          (VAR_INDEX_EXP i v, VAR_INDEX_ASG i v)`);;
 366
 367 (*---------------------------------------------------------------------------*)
 368 (*
 369   List functions (not complete)
 370 *)
 371 (*---------------------------------------------------------------------------*)
 372
 373 (*
 374  * List of expressions
 375  *)
 376 let LIST_EXP_term =
 377   (`(LIST_EXP [] (s:stype)               = []) /\
 378     (LIST_EXP (CONS (e:stype->'t) t) s = (CONS (e s) (LIST_EXP t s)))`);;
 379 let LIST_EXP = new_recursive_definition list_RECURSION LIST_EXP_term;;
 380
 381 (*---------------------------------------------------------------------------*)
 382 (*
 383   Record (pair,fst,snd) functions
 384 *)
 385 (*---------------------------------------------------------------------------*)
 386
 387 (*
 388  * State abstracted FST and SND
 389  *)
 390 let s_FST = new_definition
 391   (`s_FST (e:'sta->('a # 'b)) s = FST (e s)`);;
 392
 393 let s_SND = new_definition
 394   (`s_SND (e:'sta->('a # 'b)) s = SND (e s)`);;
 395
 396 (*
 397  * Update PAIR
 398  *)
 399 let UPD_FST = new_definition
 400   (`UPD_FST (c:'a) (p:'sta->('a#'b)) s = (c, SND(p s))`);;
 401
 402 let UPD_SND = new_definition
 403   (`UPD_SND (c:'b) (p:'sta->('a#'b)) s = (FST(p s),c)`);;
 404
 405 (*
 406  * Assignment to FST and SND
 407  *)
 408 let VAR_FST_ASG = new_definition
 409   (`VAR_FST_ASG (v:vpair_type) (e:stype->'a) (s0:stype) (s:stype) =
 410          VAR_ASG v (UPD_FST (e s0) (VAR_EXP v)) s0 s`);;
 411
 412 let VAR_SND_ASG = new_definition
 413   (`VAR_SND_ASG (v:vpair_type) (e:stype->'b) (s0:stype) (s:stype) =
 414          VAR_ASG v (UPD_SND (e s0) (VAR_EXP v)) s0 s`);;
 415
 416 (*
 417  * Variables of FST and SND
 418  *)
 419 let FST_VAR = new_definition
 420    (`FST_VAR (v:vpair_type) = (s_FST (VAR_EXP v), VAR_FST_ASG v)`);;
 421
 422 let SND_VAR = new_definition
 423    (`SND_VAR (v:vpair_type) = (s_SND (VAR_EXP v), VAR_SND_ASG v)`);;
 424
 425 (*---------------------------------------------------------------------------*)
 426 (*
 427   Parallel actions
 428 *)
 429 (*---------------------------------------------------------------------------*)
 430
 431 (*
 432  * Execute two parallel actions simultaneously
 433  *)
 434 let PAR_PAR = new_definition
 435   (`(PAR_PAR (p1:stype->stype->stype)
 436              (p2:stype->stype->stype)
 437              (s0:stype) (s:stype) =
 438         p2  s0 (p1 s0 s))`);;
 439
 440 (*
 441  * Execute a list of parallel actions
 442  *)
 443 let LIST_PAR_term =
 444   (`(LIST_PAR [] (s0:stype) (s:stype) = s) /\
 445     (LIST_PAR (CONS (h:stype->stype->stype) t) s0 s = LIST_PAR t s0 (h s0 s))`);;
 446 let LIST_PAR =  new_recursive_definition list_RECURSION LIST_PAR_term;;
 447
 448 (*
 449  * Translate a parallel action into an atomic action
 450  *)
 451 let PAR_ATOM = new_definition
 452  (`PAR_ATOM (p:stype->stype->stype) (s:stype) = p s s`);;
 453
 454 (*
 455  * Guard a parallel action
 456  *)
 457 let WHEN_PAR = new_definition
 458   (`WHEN_PAR (p:stype->stype->stype) g
 459              (s0:stype) (s:stype) =
 460         (if (g s0) then (p s0 s) else s)`);;
 461
 462 (*
 463  * Conditional parallel action
 464  *)
 465 let IF_PAR = new_definition
 466   (`IF_PAR (p1:stype->stype->stype)
 467            (p2:stype->stype->stype) g
 468            (s0:stype) (s:stype) =
 469      (if (g s0) then (p1 s0 s) else (p2 s0 s))`);;
 470
 471 (*
 472  * Identity parallel action
 473  *)
 474 let ID_PAR = new_definition (`ID_PAR (s0:stype) (s:stype) = s`);;
 475
 476 (*
 477  * Iterated parallel assignment
 478  *)
 479 let ITER_PAR0_term =
 480  (`(ITER_PAR0 (low:num) 0 (f:num->bool)
 481        (fi:num->stype->stype->stype) = ID_PAR) /\
 482    (ITER_PAR0 low (SUC n) f fi =
 483        (if (f low) then PAR_PAR (fi low) (ITER_PAR0 (SUC low) n f fi)
 484                    else (ITER_PAR0 (SUC low) n f fi)))`);;
 485 let ITER_PAR0 = new_recursive_definition num_RECURSION ITER_PAR0_term;;
 486
 487 let ITER_PAR = new_definition
 488   (`ITER_PAR low high (f:num->bool)
 489                       (fi:num->stype->stype->stype) =
 490       (ITER_PAR0 low ((1+high)-low) f fi)`);;
 491
 492 (*---------------------------------------------------------------------------*)
 493 (*
 494   Atomic actions
 495 *)
 496 (*---------------------------------------------------------------------------*)
 497
 498 (*
 499  * Translate a parallel action into an atomic action
 500  *)
 501
 502 (*
 503    K and S are removed from HOL Light.
 504    I and o are defined in trivia.ml
 505
 506    So I introduce K myself
 507 *)
 508 let K_DEF = new_definition (`K x y = x`);;
 509
 510 let ASG_ACT = new_definition
 511   (`ASG_ACT (par:stype->stype->stype)
 512             (pc:'loc) (mk:num->'val) (ds:'val->num) (l0:num) =
 513           PAR_ATOM
 514            (WHEN_PAR (LIST_PAR [par; LOC_ASG pc mk (K (SUC l0))])
 515                      (LOC_EXP pc ds =* (K l0)))`);;
 516
 517 (*
 518  * Test atomic action
 519  *)
 520 let TST_ACT = new_definition
 521   (`TST_ACT (g:stype->bool)
 522             (l:num) (pc:'loc) (mk:num->'val) (ds:'val->num) (l0:num) =
 523      (PAR_ATOM (WHEN_PAR (LOC_ASG pc mk ((g =>* K(SUC l0)) (K l)))
 524                     (LOC_EXP pc ds =* K l0)))`);;
 525
 526 (*
 527  * Goto atomic action
 528  *)
 529 let GTO_ACT = new_definition
 530   (`GTO_ACT (l:num) (pc:'loc) (mk:num->'val) (ds:'val->num) (l0:num) =
 531         PAR_ATOM (WHEN_PAR (LOC_ASG pc mk (K l))
 532                            (LOC_EXP pc ds =* K l0))`);;
 533
 534 (*---------------------------------------------------------------------------*)
 535 (*
 536   Sequential actions
 537 *)
 538 (*---------------------------------------------------------------------------*)
 539
 540 (*
 541  * Translate parallel to sequential action
 542  *)
 543 let PAR_SEQ = new_definition
 544   (`PAR_SEQ (par:stype->stype->stype)
 545             (pc:'loc) (mk:num->'val) (ds:'val->num) (l0:num) =
 546             ([ASG_ACT par pc mk ds l0], SUC l0)`);;
 547
 548 (*
 549  * Identity sequential action
 550  *)
 551 let ID_SEQ = new_definition
 552   (`ID_SEQ (pc:'loc) (mk:num->'val) (ds:'val->num) (l0:num) =
 553       ([], l0)`);;
 554
 555 (*
 556  * Execute two sequential actions in a row
 557  *)
 558 let SEQ_SEQ = new_definition
 559   (`SEQ_SEQ (s1:seq_type) (s2:seq_type)
 560             (pc:'loc) (mk:num->'val) (ds:'val->num) (l0:num) =
 561       let b1 = s1 pc mk ds l0 in
 562       let b2 = s2 pc mk ds (SND b1) in
 563         (APPEND (FST b1) (FST b2), (SND b2))`);;
 564
 565 (*
 566  * Iterated sequential actions
 567  *)
 568 let ITER_SEQ0_term =
 569  (`(ITER_SEQ0 (low:num) 0 (f:num->bool) (fi:num->seq_type) = ID_SEQ) /\
 570    (ITER_SEQ0 low (SUC n)  f             fi =
 571         (if (f low) then (SEQ_SEQ (fi low) (ITER_SEQ0 (SUC low) n f fi))
 572                     else (ITER_SEQ0 (SUC low) n f fi)))`);;
 573 let ITER_SEQ0 = new_recursive_definition num_RECURSION ITER_SEQ0_term;;
 574
 575 let ITER_SEQ = new_definition
 576   (`ITER_SEQ low high (f:num->bool) (fi:num->seq_type) =
 577         ITER_SEQ0 low ((1+high)-low) f fi`);;
 578
 579 (*
 580  * List of sequential actions
 581  *)
 582 let LIST_SEQ_term =
 583   (`(LIST_SEQ [] (pc:'loc) (mk:num->'val) (ds:'val->num) (l0:num) = ([], l0)) /\
 584     (LIST_SEQ (CONS (sa:seq_type) sas) pc mk ds l0 =
 585        let b1 = sa pc mk ds l0 in
 586        let bs = LIST_SEQ sas pc mk ds (SND b1) in
 587           (APPEND (FST b1) (FST bs), (SND bs)))`);;
 588 let LIST_SEQ = new_recursive_definition list_RECURSION LIST_SEQ_term;;
 589
 590 (*
 591  * Conditional sequential actions
 592  *)
 593 let IF1_SEQ = new_definition
 594   (`(IF1_SEQ (g:stype->bool)
 595              (sa:seq_type) (pc:'loc) (mk:num->'val) (ds:'val->num) (l0:num) =
 596        let b1 = sa pc mk ds (SUC l0) in
 597        let a1 = TST_ACT g (SND b1) pc mk ds l0 in
 598          (CONS a1 (FST b1), (SND b1)))`);;
 599
 600 (*
 601  * Conditional (else) sequential actions
 602  *)
 603 let IF2_SEQ = new_definition
 604  (`(IF2_SEQ (g:stype->bool) (sa1:seq_type) (sa2:seq_type)
 605              (pc:'loc) (mk:num->'val) (ds:'val->num) (l0:num) =
 606        let b1 = sa1 pc mk ds (SUC l0)                in
 607        let b2 = sa2 pc mk ds (SUC (SND b1))          in
 608        let a1 = TST_ACT g (SUC (SND b1)) pc mk ds l0 in
 609        let a2 = GTO_ACT (SND b2) pc mk ds (SND b1)   in
 610           (APPEND (CONS a1 (FST b1))
 611                   (CONS a2 (FST b2)), (SND b2)))`);;
 612
 613 (*
 614  * While loop sequential actions
 615  *)
 616 let WHL_SEQ = new_definition
 617  (`(WHL_SEQ (g:stype->bool) (sa:seq_type)
 618             (pc:'loc) (mk:num->'val) (ds:'val->num) (l0:num) =
 619       let b1 = sa pc mk ds (SUC l0)                 in
 620       let a1 = TST_ACT g (SUC (SND b1)) pc mk ds l0 in
 621       let a2 = GTO_ACT l0 pc mk ds (SND b1)         in
 622          (APPEND (CONS a1 (FST b1)) [a2], (SUC(SND b1))))`);;
 623
 624 (*---------------------------------------------------------------------------*)
 625 (*
 626   Interleaved actions
 627 *)
 628 (*---------------------------------------------------------------------------*)
 629
 630 (*
 631  * Translate a parallel action into an interleaved action
 632  *)
 633 let PAR_INT = new_definition
 634   (`PAR_INT (par:stype->stype->stype) = [PAR_ATOM par]`);;
 635
 636 (*
 637  * Composition of two interleaved actions
 638  *)
 639 let INT_INT = new_definition
 640   (`INT_INT (i1:(stype->stype)list) i2 = APPEND i1 i2`);;
 641
 642 (*
 643  * Translate a list of interleaved action into a single interleaved action
 644  *)
 645 let LIST_INT_term =
 646  (`(LIST_INT [] = ([]:(stype->stype)list)) /\
 647    (LIST_INT (CONS (h:(stype->stype)list) t) =
 648                      (APPEND h (LIST_INT t)))`);;
 649 let LIST_INT = new_recursive_definition list_RECURSION LIST_INT_term;;
 650
 651 (*
 652  * Translate a parallel action into an interleaved action
 653  *)
 654 let ID_INT = new_definition
 655   (`ID_INT = ([]:(stype->stype)list)`);;
 656
 657
 658 (*########################################################################
 659  #                                                                      #
 660  #      Iterated interleaving                                           #
 661  #                                                                      #
 662  #        << i : 1 <= i <= N :: Pr[i] >>                                #
 663  #                                                                      #
 664  #      is defined as:                                                  #
 665  #                                                                      #
 666  #        IteratedINTerleaving low n Pr[.] -->                          #
 667  #              Pr[low] [] ... [] Pr[low+n-1]                           #
 668  #                                                                      #
 669  ########################################################################*)
 670
 671 (*
 672  * Iterated interleaved assignment
 673  *)
 674 let ITER_INT0_term =
 675  (`(ITER_INT0 (low:num) 0 (f:num->bool) (fi:num->(stype->stype)list) = ID_INT) /\
 676    (ITER_INT0  low (SUC n) f             fi =
 677       (if (f low) then (INT_INT (fi low) (ITER_INT0 (SUC low) n f fi))
 678                   else (ITER_INT0 (SUC low) n f fi)))`);;
 679 let ITER_INT0 = new_recursive_definition num_RECURSION ITER_INT0_term;;
 680
 681 let ITER_INT = new_definition
 682   (`ITER_INT low high (f:num->bool) (fi:num->(stype->stype)list) =
 683            ITER_INT0 low ((1+high)-low) f fi`);;
 684
 685 (*#######################################################################
 686  #                                                                      #
 687  #      Absolute and relative Label predicates                          #
 688  #                                                                      #
 689  #      AT,AFTER      : At first, first following action                #
 690  #      IN            : Inside action                                   #
 691  #      BEFORE,FOLLOW : Strictly before,following action                #
 692  #                                                                      #
 693  ########################################################################*)
 694
 695 let AT_LBL = new_definition
 696   (`AT_LBL ds pc (label:num#num) =
 697       (LOC_EXP pc ds:stype->num) =* K (FST label)`);;
 698
 699 let AFTER_LBL = new_definition
 700   (`AFTER_LBL ds pc (label:num#num) =
 701       (LOC_EXP pc ds:stype->num) =* K (SND label)`);;
 702
 703 let BEFORE_LBL = new_definition
 704   (`BEFORE_LBL ds pc (label:num#num) =
 705        (LOC_EXP pc ds:stype->num) <* K (FST label)`);;
 706
 707 let INSIDE_LBL = new_definition
 708   (`INSIDE_LBL ds pc (label:num#num) =
 709       ((LOC_EXP pc ds:stype->num) >=* K (FST label)) /\*
 710       ((LOC_EXP pc ds:stype->num) <* K (SND label))`);;
 711
 712 let FOLLOW_LBL = new_definition
 713   (`FOLLOW_LBL ds pc (label:num#num) =
 714        (LOC_EXP pc ds:stype->num) >=* K (SND label)`);;
 715
 716 (* Absolute label handler *)
 717 let AT_ABS = new_definition
 718   (`AT_ABS (pc:stype->num) (l:num) (u:num) = (pc =* K l)`);;
 719
 720 let AT_REL = new_definition
 721   (`AT_REL (pc:(stype->num)#((stype->num)->stype->stype->stype))
 722            (label:(num#num)) =
 723       VAR_EXP pc =* K (FST label)`);;
 724
 725 let AFTER_ABS = new_definition
 726   (`AFTER_ABS (pc:stype->num) (l:num) (u:num) = (pc =* K u)`);;
 727
 728 let AFTER_REL = new_definition
 729   (`AFTER_REL (pc:(stype->num)#((stype->num)->stype->stype->stype))
 730               (label:(num#num)) =
 731        VAR_EXP pc =* K (SND label)`);;
 732
 733 let BEFORE_ABS = new_definition
 734   (`BeforeAbs (pc:stype->num) (l:num) (u:num) = (pc <* K l)`);;
 735
 736 let BEFORE_REL = new_definition
 737   (`BEFORE_REL (pc:(stype->num)#((stype->num)->stype->stype->stype))
 738                (label:(num#num)) =
 739           VAR_EXP pc <* K (FST label)`);;
 740
 741 let INSIDE_ABS = new_definition
 742   (`INSIDE_ABS (pc:stype->num) (l:num) (u:num) =
 743         (pc >=* K l) /\* (pc <* K u)`);;
 744
 745 let INSIDE_REL = new_definition
 746   (`INSIDE_REL (pc:(stype->num)#((stype->num)->stype->stype->stype))
 747                (label:(num#num)) =
 748          (VAR_EXP pc >=* K (FST label)) /\*
 749          (VAR_EXP pc  <* K (SND label))`);;
 750
 751 let FOLLOW_ABS = new_definition
 752   (`FollowAbs (pc:stype->num) (l:num) (u:num) = (pc >=* K l)`);;
 753
 754 let FOLLOW_REL = new_definition
 755   (`FOLLOW_REL (pc:(stype->num)#((stype->num)->stype->stype->stype))
 756                (label:(num#num)) =
 757        VAR_EXP pc >=* K (SND label)`);;
 758
 759 (*########################################################################
 760  #                                                                      #
 761  #      Restricted UNLESS                                               #
 762  #                                                                      #
 763  #        (p UNLESS{valid} q) Pr                                        #
 764  #                                                                      #
 765  #      is defined as:                                                  #
 766  #                                                                      #
 767  #        RESTRICTED_UNLESS valid p q Pr =                              #
 768  #              {p /\ valid /\ ~q)} Pr {p \/ q}                         #
 769  #                                                                      #
 770  ########################################################################*)
 771
 772 let RESTRICTED_UNLESS_STMT = new_definition
 773   (`RESTRICTED_UNLESS_STMT v p q st =
 774        (!s:'state. p s /\ v s /\ ~(q s) ==> p (st s) \/ q (st s))`);;
 775
 776 let RESTRICTED_UNLESS_term =
 777  (`(RESTRICTED_UNLESS (v:'state->bool) p q []           = T) /\
 778    (RESTRICTED_UNLESS (v:'state->bool) p q (CONS st Pr) =
 779      (RESTRICTED_UNLESS_STMT v p q st /\ RESTRICTED_UNLESS v p q Pr))`);;
 780 let RESTRICTED_UNLESS =
 781    new_recursive_definition list_RECURSION RESTRICTED_UNLESS_term;;
 782
 783 (*#######################################################################
 784  #                                                                      #
 785  #      RESTRICTED STABLE                                               #
 786  #                                                                      #
 787  #        (p STABLE{valid} q) Pr                                        #
 788  #                                                                      #
 789  #      is defined as:                                                  #
 790  #                                                                      #
 791  #        RESTRICTED_STABLE valid p q Pr =                              #
 792  #              {p /\ valid} Pr {p}                                     #
 793  #                                                                      #
 794  ########################################################################*)
 795 let RESTRICTED_STABLE_STMT = new_definition
 796   (`RESTRICTED_STABLE_STMT v p st =
 797        (!s:'state. p s /\ v s ==> p (st s))`);;
 798
 799 let RESTRICTED_STABLE_term =
 800  (`(RESTRICTED_STABLE (v:'state->bool) p [] = T) /\
 801    (RESTRICTED_STABLE (v:'state->bool) p (CONS st Pr) =
 802      (RESTRICTED_STABLE_STMT v p st /\ RESTRICTED_STABLE      v p Pr))`);;
 803 let RESTRICTED_STABLE =
 804    new_recursive_definition list_RECURSION RESTRICTED_STABLE_term;;
 805
 806 (*########################################################################
 807  #                                                                      #
 808  #      RESTRICTED EXISTS_TRANSITION                                    #
 809  #                                                                      #
 810  #        (p EXISTS_TRANSITION{valid} q) Pr                             #
 811  #                                                                      #
 812  #      is defined as:                                                  #
 813  #                                                                      #
 814  #        RESTRICTED_EXISTS_TRANSITION valid p q Pr =                   #
 815  #              ?st In Pr. {p /\ valid /\ ~q} Pr {q}                    #
 816  #                                                                      #
 817  ########################################################################*)
 818 let RESTRICTED_EXISTS_TRANSITION_STMT = new_definition
 819   (`RESTRICTED_EXISTS_TRANSITION_STMT v p q st =
 820        (!s:'state. p s /\ v s /\ ~(q s) ==> q (st s))`);;
 821
 822 let RESTRICTED_EXISTS_TRANSITION_term =
 823  (`(RESTRICTED_EXISTS_TRANSITION (v:'state->bool) p q [] = F) /\
 824    (RESTRICTED_EXISTS_TRANSITION (v:'state->bool) p q (CONS st Pr) =
 825       (RESTRICTED_EXISTS_TRANSITION_STMT v p q st \/
 826        RESTRICTED_EXISTS_TRANSITION      v p q Pr))`);;
 827 let RESTRICTED_EXISTS_TRANSITION =
 828    new_recursive_definition list_RECURSION RESTRICTED_EXISTS_TRANSITION_term;;
 829
 830 (*########################################################################
 831  #                                                                      #
 832  #      RESTRICTED ENSURES                                              #
 833  #                                                                      #
 834  #        (p ENSURES{valid} q) Pr                                       #
 835  #                                                                      #
 836  #      is defined as:                                                  #
 837  #                                                                      #
 838  #        RESTRICTED_ENSURES valid p q Pr =                             #
 839  #              RESTRICTED_UNLESS valid p q Pr /\                       #
 840  #              RESTRICTED_EXISTS_TRANSITION valid p q Pr               #
 841  #                                                                      #
 842  ########################################################################*)
 843 let RESTRICTED_ENSURES = new_definition
 844   (`RESTRICTED_ENSURES (v:'state->bool) p q Pr =
 845       (RESTRICTED_UNLESS            v p q Pr /\
 846        RESTRICTED_EXISTS_TRANSITION v p q Pr)`);;
 847
 848 (*########################################################################
 849  #                                                                      #
 850  #      RESTRICTED LEADSTO                                              #
 851  #                                                                      #
 852  #        (p LEADSTO{valid} q) Pr                                       #
 853  #                                                                      #
 854  #      is defined as:                                                  #
 855  #                                                                      #
 856  #        RESTRICTED_LEADSTO valid p q Pr =                             #
 857  #              (p /\ valid p) LEADSTO q Pr /\                          #
 858  #                                                                      #
 859  ########################################################################*)
 860 let RESTRICTED_LEADSTO = new_definition
 861   (`RESTRICTED_LEADSTO (v:'state->bool) p q Pr =
 862         (((p /\* v) LEADSTO q) Pr)`);;
 863
 864 (*########################################################################
 865  #                                                                      #
 866  #      Valid                                                           #
 867  #                                                                      #
 868  #        Valid p                                                       #
 869  #                                                                      #
 870  #      is defined as:                                                  #
 871  #                                                                      #
 872  #        Valid p =                                                     #
 873  #              !s. p s                                                 #
 874  #                                                                      #
 875  ########################################################################*)
 876 let VALID = new_definition
 877   (`VALID (p:'state->bool) = !s. p s`);;
 878
 879 let TRIPLE_term =
 880  (`(TRIPLE (p:'state->bool) q [] = T) /\
 881    (TRIPLE p q (CONS (st:'state->'state) Pr) =
 882      ((!s. p s ==> q(st s)) /\ TRIPLE p q Pr))`);;
 883 let RESTRICTED_TRIPLE =
 884    new_recursive_definition list_RECURSION TRIPLE_term;;
 885
 886 (*########################################################################
 887  #                                                                      #
 888  #      SUMMA lwb len filter body =                                     #
 889  #        Body(lwb) + ... Body(i) ... + Body(lwb+len-1) , when filter(i)#
 890  #                                                                      #
 891  #      SUMMA lwb 0 f b = 0                                             #
 892  #      SUMMA lwb (SUC n) f b = (f lwb => b lwb | 0) + SUMMA lwb n f b  #
 893  #                                                                      #
 894  ########################################################################*)
 895 let SUMMA0_term =
 896  (`(SUMMA0 lwb 0 f b = 0) /\
 897    (SUMMA0 lwb (SUC n) f b =
 898           ((if (f lwb) then (b lwb) else 0) + (SUMMA0 (SUC lwb) n f b)))`);;
 899 let SUMMA0 = new_recursive_definition num_RECURSION SUMMA0_term;;
 900
 901 let SUMMA = new_definition
 902   (`SUMMA lwb upb f b = SUMMA0 lwb ((1 + upb)-lwb) f b`);;
 903
 904 let SUMMA_S = new_definition
 905   (`SUMMA_S lwb upb f b (s:'state) =
 906           SUMMA (lwb s) (upb s) (\i. f i s) (\i. b i s)`);;
 907
 908 (*########################################################################
 909  #                                                                      #
 910  #      MULTA lwb len filter body =                                     #
 911  #        Body(lwb) * ... Body(i) ... * Body(lwb+len-1) , when filter(i)#
 912  #                                                                      #
 913  #      MULTA lwb 0 f b = 1                                             #
 914  #      MULTA lwb (SUC n) f b = (f lwb => b lwb | 1) * MULTA lwb n f b  #
 915  #                                                                      #
 916  ########################################################################*)
 917 let MULTA0_term =
 918  (`(MULTA0 lwb 0 f b = 1) /\
 919    (MULTA0 lwb (SUC n) f b =
 920       ((if (f lwb) then (b lwb) else 1) * (MULTA0 (SUC lwb) n f b)))`);;
 921 let MULTA0 = new_recursive_definition num_RECURSION MULTA0_term;;
 922
 923 let MULTA = new_definition
 924   (`MULTA lwb upb f b = MULTA0 lwb ((1 + upb)-lwb) f b`);;
 925
 926 let MULTA_S = new_definition
 927   (`MULTA_S lwb upb f b (s:'state) =
 928           MULTA (lwb s) (upb s) (\i. f i s) (\i. b i s)`);;
 929
 930 (*########################################################################
 931  #                                                                      #
 932  #      CONJA lwb len filter body =                                     #
 933  #        Body(lwb) & ... Body(i) ... & Body(lwb+len-1) , when filter(i)#
 934  #                                                                      #
 935  #      CONJA lwb 0 f b = T                                             #
 936  #      CONJA lwb (SUC n) f b = (f lwb => b lwb | 1) & CONJA lwb n f b  #
 937  #                                                                      #
 938  ########################################################################*)
 939 let CONJA0_term =
 940  (`(CONJA0 lwb 0 f b = T) /\
 941    (CONJA0 lwb (SUC n) f b =
 942      ((if (f lwb) then (b lwb) else T) /\ (CONJA0 (SUC lwb) n f b)))`);;
 943 let CONJA0 = new_recursive_definition num_RECURSION CONJA0_term;;
 944
 945 let CONJA = new_definition
 946   (`CONJA lwb upb f b = CONJA0 lwb ((1 + upb)-lwb) f b`);;
 947
 948 let CONJA_S = new_definition
 949   (`CONJA_S lwb upb f b (s:'state) =
 950           CONJA (lwb s) (upb s) (\i. f i s) (\i. b i s)`);;
 951
 952 (*########################################################################
 953  #                                                                      #
 954  #      DISJA lwb len filter body =                                     #
 955  #        Body(lwb) | ... Body(i) ... | Body(lwb+len-1) , when filter(i)#
 956  #                                                                      #
 957  #      DISJA lwb 0 f b = F                                             #
 958  #      DISJA lwb (SUC n) f b = (f lwb => b lwb | 1) | DISJA lwb n f b  #
 959  #                                                                      #
 960  ########################################################################*)
 961 let DISJA0_term =
 962  (`(DISJA0 lwb 0 f b = F) /\
 963    (DISJA0 lwb (SUC n) f b =
 964       ((if (f lwb) then (b lwb) else F) \/ (DISJA0 (SUC lwb) n f b)))`);;
 965 let DISJA0 = new_recursive_definition num_RECURSION DISJA0_term;;
 966
 967 let DISJA = new_definition
 968   (`DISJA lwb upb f b = DISJA0 lwb ((1 + upb)-lwb) f b`);;
 969
 970 let DISJA_S = new_definition
 971   (`DISJA_S lwb upb f b (s:'state) =
 972           DISJA (lwb s) (upb s) (\i. f i s) (\i. b i s)`);;
 973
 974 (*---------------------------------------------------------------------------*)
 975 (*
 976   Miscellaneous
 977 *)
 978 (*---------------------------------------------------------------------------*)
 979 (*
 980  * Test for list membership
 981  *)
 982 let MEMBER_term =
 983  (`(MEMBER (x:'a) []    = F) /\
 984    (MEMBER x (CONS h t) = ((x=h) \/ (MEMBER x t)))`);;
 985 let MEMBER = new_recursive_definition list_RECURSION MEMBER_term;;
 986
 987 (*
 988  * Test for unique elements in list
 989  *)
 990 let UNIQUE_term =
 991  (`(UNIQUE []              = T) /\
 992    (UNIQUE (CONS (h:'a) t) = ((~(MEMBER h t)) /\ UNIQUE t))`);;
 993 let UNIQUE = new_recursive_definition list_RECURSION UNIQUE_term;;