(*
    Author:      Norbert Schirmer
    Maintainer:  Norbert Schirmer, norbert.schirmer at web de

Copyright (C) 2006-2008 Norbert Schirmer
*)

(*<*)
theory SyntaxTest imports HeapList Vcg begin

record "globals" =
 alloc_' :: "ref list"
 free_':: nat
 GA_' :: "ref list list"
 next_' :: "ref → ref"
 cont_' :: "ref → nat"

record 'g vars = "'g state" +
  A_' :: "nat list"
  AA_' :: "nat list list"
  I_' :: nat
  M_' :: nat
  N_' :: nat
  R_' :: int
  S_' :: int
  B_' :: bool
  Abr_':: string
  p_' :: ref
  q_' :: ref

procedures Foo (p,I|p) = "🚫p :== 🚫p"

term "🚫I :==_g 3 - 1"
term "🚫R :==_g 3 - 1"
term "🚫I :==_g 🚫A!i"
term " 🚫A!i :== j"
term " 🚫AA :== 🚫AA!![i,j]"
term " 🚫AA!![i,j] :== 🚫AA"
term "🚫A!i :==_g j"
term "🚫p :==_g 🚫GA!i!j"
term "🚫GA!i!j :==_g 🚫p"
term "🚫p :==_g 🚫p → 🚫next"
term "🚫p → 🚫next :==_g 🚫p"
term "🚫p → 🚫next → 🚫next :==_g 🚫p"
term "🚫p :== NEW sz [🚫next :== Null,🚫cont :== 0]"
term "🚫p→🚫next :==_g NEW sz [🚫next :== Null,🚫cont :== 0]"
term "🚫p :== NNEW sz [🚫next :== Null,🚫cont :== 0]"
term "🚫p→🚫next :==_g NNEW sz [🚫next :== Null,🚫cont :== 0]"
term "🚫B :==_g 🚫N + 1 < 0 ∧ 🚫M + 🚫N < n"
term "🚫B :==_g 🚫N + 1 < 0 ∨ 🚫M + 🚫N < n"
term "🚫I :==_g 🚫N mod n"
term "🚫I :==_g 🚫N div n"
term "🚫R :==_g 🚫R div n"
term "🚫R :==_g 🚫R mod n"
term "🚫R :==_g 🚫R * n"
term "🚫I :==_g 🚫I - 🚫N"
term "🚫R :==_g 🚫R - 🚫S"
term "🚫R :==_g int 🚫I"
term "🚫I :==_g nat 🚫R"
term "🚫R :==_g -🚫R"
term "IF_g 🚫A!i < 🚫N THEN c1 ELSE c2 FI"
term "WHILE_g 🚫A!i < 🚫N DO c OD"
term "WHILE_g 🚫A!i < 🚫N INV {foo} DO c OD"
term "WHILE_g 🚫A!i < 🚫N INV {foo} VAR bar x DO c OD"
term "WHILE_g 🚫A!i < 🚫N INV {foo} VAR bar x DO c OD;;c"
term "c;;WHILE_g 🚫A!i < 🚫N INV {foo} VAR MEASURE 🚫N + 🚫M DO c;;c OD;;c"
context Foo_impl
begin
term "🚫q :== CALL Foo(🚫p,🚫M)"
term "🚫q :== CALL_g Foo(🚫p,🚫M + 1)"
term "🚫q :== CALL Foo(🚫p→🚫next,🚫M)"
term "🚫q → 🚫next :== CALL Foo(🚫p,🚫M)"
end

end

(*>*)