--- Standard ML/CML specification --- [rule-based / mixfix phrases] version
--- version 1.0 by Fabricio Chalub Barbosa do Rosário <frosario@ic.uff.br> and
---                Christiano Braga <cbraga@ic.uff.br>
--- based on Peter Mosses' Standard ML/CML MSOS specification
--- as described in `Fundamental Concepts and Formal Semantics
---      of Programming Languages, an introductory course', 
---      version 0.1 <URL:http://wiki.daimi.au.dk/dSprogSem-01>
--- and on the MRS of the bc programming languages, as described
---      on BRAGA, C. & MESEGUER, J. `Modular Rewriting Semantics 
---      in Practice'

--- The latest version of this file is always available at:
---     http://www.ic.uff.br/~cbraga/losd/specs/cml.maude

fmod RECORD is 
 sorts Index Component Field PreRecord Record .
 subsort Field < PreRecord .

 op null : -> PreRecord [ctor] .
 op _,_ : PreRecord PreRecord -> PreRecord [ctor assoc comm id: null] .
 op _:_ : [Index] [Component] -> [Field] [ctor] .
 op {_} : [PreRecord] -> [Record] [ctor] .
 op duplicated : [PreRecord] -> [Bool] .
 var I : Index . vars C C' : Component . var pr : PreRecord .
 eq duplicated((I : C),(I : C'), pr) = true .
 cmb {pr} : Record if duplicated(pr) =/= true .
endfm

fmod CONF is 
 protecting RECORD .
 sorts Program Conf .
 op <_,_> : Program Record -> Conf [ctor] .
endfm

mod RCONF is extending CONF .
 op {_,_} : [Program] [Record] -> [Conf] [ctor] .
 op [_,_] : [Program] [Record] -> [Conf] [ctor] .
 vars P P' : Program .
 vars R R' : Record .
 crl [step] : < P , R > => < P' , R' > if { P , R } => [ P' , R' ] .
endm

fmod EMPTY-LIST is
 sort EmptyList .
 op empty-list : -> EmptyList [ctor] .
 op _,_ : EmptyList EmptyList -> 
          EmptyList [assoc id: empty-list prec 45] .
endfm

fmod VALUE is 
 sorts Value NzValue . 
 op no-value : -> [Value] . 

 op isTrue : Value -> Bool .
 op isEqualTo : Value Value -> Value .
 op lessThan : Value Value -> Value .    
 op greaterThan : Value Value -> Value . 
endfm

fmod VALUE-LIST is
 pr VALUE . 
 pr EMPTY-LIST .
 sort ValueList .
 subsorts Value EmptyList < ValueList .
 op _,_ : ValueList ValueList -> ValueList [ctor ditto] . 
endfm


fmod IDE is 
 sort Ide .
 ops true false : -> Ide [ctor] .
endfm

fmod LABEL is
 sort Label .
endfm

fmod CML-VALUES is
 including VALUE-LIST .
 including LABEL .
 including IDE .
 protecting RAT .

 op constr : Ide -> Value [ctor] .
 op constr : Ide Value -> Value [ctor] .

 sorts Tuple List Rec NumberConstant .

 op rat : Rat -> NumberConstant [ctor] .
 op unrat : NumberConstant -> Rat [ctor] .
 eq unrat(rat(r:Rat)) = r:Rat .

 subsort NumberConstant < Value .
 --- subsort NzNumberConstant < NzValue .
 subsort Tuple < Value .
 subsort List < Value .
 subsort Rec < Value .

 var v : Value .

 --- tuples
 op tuple() : -> Tuple [ctor] .
 op tuple(_) : ValueList -> Tuple [ctor] .
 op tuple-select : Int Tuple -> [Value] .

 eq tuple-select (1, tuple(v:Value, vl:ValueList)) = v .
 eq tuple-select (s(i:Int), tuple(v:Value, vl:ValueList)) =
    tuple-select (i:Int, tuple(vl:ValueList)) [owise] .

 --- records
 op row : Label Value -> Rec [ctor] .
 op rec : Rec Rec -> Rec [ctor assoc comm] .
 op row-select : Label Rec -> [Value] .
 eq row-select (a:Label, rec(row (a:Label, v), r:Rec)) = v .
endfm

fmod EXPR-SYNTAX is
 extending IDE .
 extending LABEL .
 extending CML-VALUES .
 protecting INT .

 sorts Exp ExpList ExpRow .

 subsorts Ide Value < Exp .
 subsort Exp < ExpList .
 subsorts ValueList EmptyList < ExpList < ExpRow .

 op _,_ : ExpList ExpList -> ExpList [ditto] .
 op _;_ : Exp Exp -> Exp [assoc] .
 op if_then_else_ : Exp Exp Exp -> Exp [prec 60] .
 op _andalso_ : Exp Exp -> Value .
 op _orelse_ : Exp Exp -> Value .

 op __ : Exp Exp -> Exp [prec 15] .

 op .() : -> Exp .
 op .(_) : ExpList -> Exp  .

 op #_ : Int -> Exp [prec 43] .
 op select : Int -> Value .
 op [] : -> Exp .
 op [_] : ExpList -> Exp .

 op nil : -> List .
 op _::_ : Exp Exp -> List [assoc] .

 op {} : -> Exp [prec 48] .
 op {_} : ExpRow -> Exp [prec 48] .
 op _=_ : Label Exp -> ExpRow [prec 44] .
 op _,_ : ExpRow ExpRow -> ExpRow [ditto] .
 op #_ : Label -> Exp [prec 48] .

 op _'=_ : Exp Exp -> Exp [prec 58] .
 op _'+_ : Exp Exp -> Exp [prec 58] .
 op _'-_ : Exp Exp -> Exp [prec 58] .
 op _'*_ : Exp Exp -> Exp [prec 58] .
 op _'/_ : Exp Exp -> Exp [prec 58] .
 op _'>_ : Exp Exp -> Exp [prec 58] .
 op _'<_ : Exp Exp -> Exp [prec 58] .
 op _'%_ : Exp Exp -> Exp [prec 58] .

 op select : Label -> Value .
endfm

mod EXPR-SEMANTICS is
 extending RCONF .
 including EXPR-SYNTAX .
 protecting CML-VALUES .

 subsorts Exp ExpList ExpRow < Program .

 vars e e' e1 e2 e3 e'1 e'2 e'3 : Exp .
 vars el el' : ExpList .
 vars r r' : Record .
 vars pr pr' : PreRecord .
 vars v v' v1 v2 v'1 v'2 : Value .
 var vl : ValueList .

 crl { e1 ; e2, r } => [ e'1 ; e2, r' ] 
  if { e1, r } => [ e'1, r' ] .

  rl {  v ; e2, r } => [ e2, r ] .

 crl { if e1 then e2 else e3, r } => 
     [ if e'1 then e2 else e3, r' ] 
  if { e1, r } => [ e'1, r' ] .

  rl { if constr(true) then e2 else e3, r } => 
     [ e2, r ] .
  rl { if constr(false) then e2 else e3, r } => 
     [ e3, r ] .

 crl { e1 andalso e2, r } => [ e'1 andalso e2, r' ]
   if { e1, r } => [ e'1, r' ] .

  rl { constr(true) andalso e2, r } => 
     [ e2, r ] .
  rl { constr(false) andalso e2, r } => 
     [ constr(false), r ] .

 crl { e1 orelse e2, r } => 
     [ e'1 orelse e2, r' ]
  if { e1, r } => [ e'1, r' ] .

  rl { constr(true) orelse e2, r } => 
     [ constr(true), r ] .
  rl { constr(false) orelse e2, r } => [ e2, r ] .

 crl { e1 e2, r } => [ e'1 e2, r' ]
  if { e1, r } => [ e'1, r' ] .

 crl { v e2, r } => [ v e'2, r' ]
  if { e2, r } => [ e'2, r' ] .

  rl { # I:Int, r } => [ select(I:Int), r ] .
  rl { # L:Label, r } => [ select(L:Label), r ] .

  crl { e1 '> e2, r } => [ e'1 '> e2, r' ] 
    if { e1, r } => [ e'1, r' ] .
  crl { v '> e2, r } => [ v '> e'2, r' ] 
    if { e2, r } => [ e'2, r' ] .
   rl { v1 '> v2, r } => 
      [ if unrat(v1) > unrat(v2) then constr(true) 
                   else constr(false) fi, r ] .

  crl { e1 '< e2, r } => [ e'1 '< e2, r' ] 
    if { e1, r } => [ e'1, r' ] .
  crl { v '< e2, r } => [ v '< e'2, r' ] 
    if { e2, r } => [ e'2, r' ] .
   rl { v1 '< v2, r } => 
      [ if unrat(v1) < unrat(v2) then constr(true) 
                   else constr(false) fi, r ] .

  crl { e1 '+ e2, r } => [ e'1 '+ e2, r' ] 
    if { e1, r } => [ e'1, r' ] .
  crl { v '+ e2, r } => [ v '+ e'2, r' ] 
    if { e2, r } => [ e'2, r' ] .
   rl { v1 '+ v2, r } => [ rat(unrat(v1) + unrat(v2)), r ] .

  crl { e1 '/ e2, r } => [ e'1 '/ e2, r' ] 
    if { e1, r } => [ e'1, r' ] .
  crl { v '/ e2, r } => [ v '/ e'2, r' ] 
    if { e2, r } => [ e'2, r' ] .
   rl { v1 '/ v2, r } => [ rat(unrat(v1) / unrat(v2)), r ] .

  crl { e1 '- e2, r } => [ e'1 '- e2, r' ] 
    if { e1, r } => [ e'1, r' ] .
  crl { v '- e2, r } => [ v '- e'2, r' ] 
    if { e2, r } => [ e'2, r' ] .
   rl { v1 '- v2, r } => [ rat(unrat(v1) - unrat(v2)), r ] .

  crl { e1 '* e2, r } => [ e'1 '* e2, r' ] 
    if { e1, r } => [ e'1, r' ] .
  crl { v '* e2, r } => [ v '* e'2, r' ] 
    if { e2, r } => [ e'2, r' ] .
   rl { v1 '* v2, r } => [ rat(unrat(v1) * unrat(v2)), r ] .

  crl { e1 '= e2, r } => [ e'1 '= e2, r' ] 
    if { e1, r } => [ e'1, r' ] .
  crl { v '= e2, r } => [ v '= e'2, r' ] 
    if { e2, r } => [ e'2, r' ] .
   rl { v1 '= v2, r } => 
      [ if unrat(v1) == unrat(v2) then constr(true)
                    else constr(false) fi, r ] .

  crl { e1 '% e2, r } => [ e'1 '% e2, r' ] 
    if { e1, r } => [ e'1, r' ] .
  crl { v '% e2, r } => [ v '% e'2, r' ] 
    if { e2, r } => [ e'2, r' ] .
   rl { v1 '% v2, r } => [ rat(unrat(v1) rem unrat(v2)), r ] .

  rl { .(), r } => [ tuple(), r ] .
 crl { .(e, el), r } => [ .(e', el), r' ] 
   if { e, r } => [ e', r' ] .

 --- This is required in order to reduce spurious 
 --- matching of single expressions against any (Exp, empty-list)

 op eval-explist : ExpList -> ExpList .

 crl { .(v, el), r } => [ .(v, el'), r' ]
   if { eval-explist(el), r } => 
      [ eval-explist(el'), r' ] .

 crl { eval-explist(e, el), r } => 
     [ eval-explist(e', el), r' ] 
   if { e, r } => [ e', r' ] .

 crl { eval-explist(v, el), r } => 
     [ eval-explist(v, el'), r' ]
   if { eval-explist(el), r } => 
      [ eval-explist(el'), r' ] .

 rl { .(v, vl), r } => 
    [ tuple(v, vl), r ] .

 rl { select(i:Int) t:Tuple, r } =>
     [ tuple-select(i:Int, t:Tuple), r ] .

  rl { select(L:Label) r:Rec, r } 
     => [ row-select(L:Label, r:Rec), r ] .
 
  rl { [], r } => [ nil, r ] .
  rl { [e], r } => [ e :: nil, r ] .

 crl { [e, el], r } => [ e :: [el], r ] 
     if el =/= empty-list .

 crl { e1 :: e2, r } => [ e'1 :: e2, r']
     if { e1, r } => [ e'1, r' ] .

 crl { v :: e, r } => [ v :: e', r']
     if { e, r } => [ e', r' ] .

  vars er er' er1 er2 er'1 er'2 : ExpRow .

  op eval-exprow : ExpRow -> ExpRow .

  crl { {er}, r } => [ {er'}, r' ]
   if { eval-exprow(er), r } => 
      [ eval-exprow(er'), r' ] .

  rl { { r:Rec }, r } => [ r:Rec, r ] .

 crl { eval-exprow(L:Label = e), r } => 
     [ eval-exprow(L:Label = e'), r' ] 
   if { e, r } => [ e', r' ] .

  rl { eval-exprow(L:Label = v), r } => 
     [ eval-exprow(row(L:Label, v)), r ] .

 crl { eval-exprow(er1, er2), r } => 
     [ eval-exprow(er'1, er2), r' ] 
   if er1 =/= empty-list /\ er2 =/= empty-list /\
      { eval-exprow(er1), r } => 
      [ eval-exprow(er'1), r' ] .

 crl { eval-exprow(r:Rec, er), r } => 
     [ eval-exprow(r:Rec, er'), r' ]
   if { eval-exprow(er), r }  => 
      [ eval-exprow(er'), r' ] .

 rl { eval-exprow(r1:Rec, r2:Rec), r } =>
    [ eval-exprow(rec(r1:Rec, r2:Rec)), r ] .
endm

--- The LOCATION module is an abstract interface for memory locations.
fmod LOCATION is
 sort Loc .
endfm

--- BASIC-ENVIRONMENT is an abstract interface for environment components.
fmod BASIC-ENVIRONMENT is
 ex RECORD .
 pr IDE .
 pr VALUE .

 sorts Env BVal .
 subsort Env < Component .
 subsort BVal < Value .

 op env : -> Index [ctor] .

 op find : Env Ide -> [BVal] .

 --- override an environment with a single binding
 op override : Env Ide BVal -> Env .

 --- override an environment with the bindings of another environment
 op override-env : Env Env -> Env .

 op new-env : Ide BVal -> Env [ctor] .

 --- `failure' is a type of binding
 op failure : -> Env [ctor] .

 op union : Env Env -> Env .
 ceq union (e1:Env, e2:Env) = override-env (e1:Env, e2:Env) 
     if e1:Env =/= failure /\ e2:Env =/= failure .
 ceq union (e1:Env, e2:Env) = failure if e1:Env == failure .
 ceq union (e1:Env, e2:Env) = failure if e2:Env == failure .

 op env-id : -> Env [ctor] .

 op get-ide : Env -> Ide .
 op get-val : Env -> BVal .

 mb env : E:Env : Field .
endfm

--- STORE is an abstract interface for memory components.
fmod STORE is
 ex RECORD .
 pr VALUE .
 inc LOCATION .

 sorts Store SVal .
 subsort Store < Component .
 subsort SVal < Value .

 op st : -> Index [ctor] .
 op lookup : Store Loc -> [SVal] .
 op update : Store Loc SVal -> Store .
 op newLoc : Store -> Loc .

 mb st : S:Store : Field .
endfm

fmod VAL is
 protecting RECORD .
 protecting VALUE .

 sorts Val ValContent .

 subsort Val < Component .
 subsort ValContent < Value .

 op val-id : -> ValContent [ctor] .

 op set_ : ValContent -> Val .
 op get_ : Val -> ValContent .

 op val : -> Index .
 mb val : v:Val : Field .
endfm

fmod DECLARATIONS-SYNTAX is
 extending EXPR-SYNTAX .

 sorts ValueBind Decl . 
 sorts Pat PatList PatRow Match .

 subsorts Pat EmptyList < PatList < PatRow .
 subsort ValueBind < Decl .

 op _,_  : PatList PatList -> PatList [ditto] .

 op p()  : -> Pat .
 op p(_) : PatList -> Pat .

 op p[]  : -> Pat .
 op p[_] : PatList -> Pat [ctor] .
 op p{_} : PatRow  -> Pat [ctor prec 48] .

 op _::_ : Pat Pat -> Pat [assoc] .

 op pat : Ide -> Pat .
 op pat : Value -> Pat .

 op _,_  : PatRow PatRow -> PatRow [ditto] .
 op _=_  : Label Pat -> PatRow [ditto] .

 op val_ : ValueBind -> Decl [prec 65] .
 op _and_ : ValueBind ValueBind -> ValueBind [prec 64 assoc] .
 op _seq_ : Decl Decl -> Decl [prec 66 assoc] .

 op _=_ : Pat Exp -> ValueBind .

 op let_in_end : Decl Exp -> Exp [prec 70] .

 op _=>_ : Pat Exp -> Match [prec 64] .
 op _.|_ : Match Match -> Match [assoc] .

 op case_of_ : Exp Match -> Exp .
endfm

mod DECLARATIONS-SEMANTICS is
 including DECLARATIONS-SYNTAX .
 extending EXPR-SEMANTICS .
 extending BASIC-ENVIRONMENT . 
 protecting VAL .

 subsort Env < ValueBind .
 subsorts PatRow Decl Match < Program .

 vars r r' : Record .
 vars pr pr' : PreRecord .
 vars e e' : Exp . 
 vars v v' : Value .
 var vl : ValueList .
 vars vb vb' vb1 vb2 vb'1 vb'2 : ValueBind .
 vars b b' b1 b2 : Env .
 vars rho rho' : Env .
 vars m m1 m2 : Match .
 var i : Ide .

 --- `empty' is just another name for the environment
 --- abstract identity constructor, env-id.
 op empty-binding   : -> Env .
 eq empty-binding = env-id .
 
  rl { i, { (env : rho), pr} } => 
     [ find(rho, i), { (env : rho), pr} ] .

 crl { val vb, r } => [ val vb', r' ] 
   if { vb, r } => [ vb', r' ] .

 crl { vb1 and vb2, r }  => [ vb'1 and vb2, r' ]
  if { vb1, r } => [ vb'1, r' ] .

 crl { b and vb2, r } => [ b and vb'2, r' ]
  if { vb2, r } => [ vb'2, r' ] .
 
  rl { b1 and b2, r } => [ override-env (b1, b2), r ] .

  rl { val b, r } => [ b, r ] .

 vars d1 d2 d'1 d'2 d d' : Decl .

 crl { let d in e end, r } => [ let d' in e end, r' ]
   if { d, r } => [ d', r' ] .

 crl { let b in e end, { (env : rho), pr} } 
     => [ let b in e' end, { (env : rho), pr' } ] 
  if rho' := override-env (rho, b)  /\
     { e, { (env : rho'), pr} } => 
     [ e', { (env : rho'), pr' } ] .

 rl { let b in v end, r } => [ v, r ] .

 --- sequential declarations
 vars pt pt' : Pat .
 var ptl : PatList .

 crl { d1 seq d2, r } => [ d'1 seq d2, r' ] 
   if { d1, r } => [ d'1, r' ] .

 crl { b seq d2, {(env : rho), pr} } =>
     [ b seq d'2, {(env : rho), pr'} ]
  if rho' := override-env (rho, b) /\
     { d2, {(env : rho'), pr} } =>
     [ d'2, {(env : rho'), pr'} ] .

  rl { b1 seq b2, r } => [ override-env(b1,b2), r ] .

 crl { pat(v), {(val : val:Val), pr} } => 
     [ failure, {(val : val:Val), pr} ] 
   if v' := get val:Val /\ v =/= v' .

 --- this rule is needed to expand a pattern like p[X,Y,Z] into X :: Y :: Z :: nil
 crl { pt = e, r } => [ pt' = e, r' ]
   if { pt, r } => [ pt', r' ] .

 crl { pt = e, r } => [ pt = e', r' ]
   if { e, r } => [ e', r' ] .

 crl { pt = v, {(val : val:Val), pr} } => [ b, {(val : val:Val), pr} ]
   if val1:Val := set v /\ { pt, {(val : val1:Val), pr} } => 
      [ b, {(val : val1:Val), pr} ] .

 crl { pat(i), {(val : val:Val), pr} } => 
     [ new-env (i, v), {(val : val:Val), pr} ] if v := get val:Val .

 crl { pat(v), {(val : val:Val), pr} } => 
     [ empty-binding, {(val : val:Val), pr} ] 
   if v' := get val:Val /\ v == v' .

 --- tuple matching
  rl { p(), {(val : val:Val), pr} }
    => [ env-id, {(val : val:Val), pr} ] .

 crl { p(pt), {(val : val:Val), pr} }
    => [ b, {(val : val:Val), pr} ] 
   if tuple(v) := get val:Val /\ val1:Val := set v /\
      { pt, {(val : val1:Val), pr} } => 
      [ b, {(val : val1:Val), pr} ] .

 op eval-patlist : PatList -> PatList .

 crl { p(pt, ptl), {(val : val:Val), pr} }
    => [ b, {(val : val:Val), pr} ] 
   if tuple(v, vl) := get val:Val /\
      val1:Val := set v /\ val2:Val := set vl /\
      { pt, {(val : val1:Val), pr} } => 
      [ b1, {(val : val1:Val), pr} ] /\ 
      { eval-patlist(ptl), {(val : val2:Val), pr} } => 
      [ b2, {(val : val2:Val), pr} ] /\
      b := union (b1, b2) .

 crl { eval-patlist(pt, ptl), {(val : val:Val), pr} } => 
     [ override-env(b1,b2), {(val : val:Val), pr} ]
   if (v, vl) := get val:Val /\ val1:Val := set v /\ val2:Val := set vl /\
      { pt, {(val : val1:Val), pr} } => 
      [ b1, {(val : val1:Val), pr} ] /\ 
      { eval-patlist(ptl), {(val : val2:Val), pr} } => 
      [ b2, {(val : val2:Val), pr} ] .

 --- new rule, due to EVAL-PATLIST eventually boiling
 --- down to a EVAL-PATLIST(P, EMPTY-LIST)
 crl { eval-patlist(pt), {(val : val:Val), pr} } => 
     [ b, {(val : val:Val), pr} ]
   if { pt, {(val : val:Val), pr} } => 
      [ b, {(val : val:Val), pr} ] .

 --- list matching
 --- The idea is to first expand both patterns and expressions into their equivalent forms
 --- [1,2,3] ==> 1 :: 2 :: 3 :: nil, for example, and then do the pattern matching.
 vars pt1 pt2 pt'2 : Pat .
 vars v1 v2 : Value .
  rl { p[], r } => [ pat(nil), r ] .
  rl { p[pt], r } => [ pt :: pat(nil), r ] .
 crl { p[pt, ptl], r } => [ pt :: p[ptl], r ] if ptl =/= empty-list .
 crl { pt1 :: pt2, r } => [ pt1 :: pt'2, r' ] if { pt2, r } => [ pt'2, r' ] .

 crl { pat(nil), {(val : val:Val), pr} } => [ env-id, {(val : val:Val), pr} ] if val:Val := set nil .

 crl { pt1 :: pt2, {(val : val:Val), pr} } => [ b, {(val : val:Val), pr} ]
  if (v1 :: v2) := get val:Val /\ val1:Val := set v1 /\ val2:Val := set v2 /\
     { pt1, {(val : val1:Val), pr} } => [ b1, {(val : val1:Val), pr} ] /\
     { pt2, {(val : val2:Val), pr} } => [ b2, {(val : val2:Val), pr} ] /\
     b := union(b1,b2) .

 --- Rec matching
 var rec : Rec .
 var patr patr1 patr2 : PatRow .

 op eval-patrow : PatRow -> PatRow .

 crl { p{ patr }, {(val : val:Val), pr} } => 
     [ b, {(val : val:Val), pr} ] 
   if { eval-patrow(patr),  {(val : val:Val), pr} } => 
      [ b, {(val : val:Val), pr} ] .

 crl { eval-patrow(patr1, patr2), {(val : val:Val), pr} } 
     => [ b, {(val : val:Val), pr} ] 
   if patr1 =/= empty-list /\
      patr2 =/= empty-list /\
      { eval-patrow(patr1), {(val : val:Val), pr} } => 
      [ b1, {(val : val:Val), pr} ] /\
      { eval-patrow(patr2), {(val : val:Val), pr} } => 
      [ b2, {(val : val:Val), pr} ] /\
      b := union (b1, b2) .

 crl { eval-patrow(L:Label = pt), {(val : val:Val), pr} } => 
     [ b, {(val : val:Val), pr} ]
   if rec := get val:Val /\
      v := row-select(L:Label, rec) /\
      val':Val := set v /\
      { pt, {(val : val':Val), pr} } =>  
      [ b, {(val : val':Val), pr} ] .

 sort MatchValue .
 op match-value : Env Exp -> MatchValue [ctor] .
 subsort MatchValue < Program .
 
 crl { case e of m, r } => [ case e' of m, r' ]
   if { e, r } => [ e', r' ] .

 crl { case v of m, {(val : val:Val), pr} } => 
     [ let b in e end, {(val : val:Val), pr} ]
   if val':Val := set v /\
      { m, {(val : val':Val), pr} } => 
      [ match-value (b, e), {(val : val':Val), pr} ] .

 crl { pt => e, r } => [ match-value(b, e), r ]
   if { pt, r } => [ b, r ] /\ b =/= failure .

 crl { pt => e, r } => [ failure, r ]
     if { pt, r } => [ failure, r ] .

 crl { m1 .| m2, r } => [ match-value (b, e), r ]
   if { m1, r } => [ match-value (b, e), r ] .

 crl { m1 .| m2, r } => [ match-value (b, e), r ]
   if { m1, r } => [ failure, r ] /\ 
      { m2, r } => [ match-value (b, e), r ] .
endm

mod ABSTRACTIONS-SYNTAX is
 extending DECLARATIONS-SYNTAX .

 op fn_ : Match -> Exp [prec 65] .
 op fun_(_)=_ : Ide Ide Exp -> Decl [prec 65] .
endm

mod ABSTRACTIONS-SEMANTICS is
 including ABSTRACTIONS-SYNTAX . 
 extending DECLARATIONS-SEMANTICS .

 sorts Closure Reclosure .

 subsorts Closure Reclosure < BVal .
 subsorts Closure Reclosure < ValContent .

 op closure : Match Env -> Closure .
 op reclosure : Match Env Env -> Reclosure .
 op unfold : Ide Value -> Env .
 op reclose(_,_)(_,_) : Ide Value Ide Value -> Env .

 vars r r' : Record . 
 vars pr pr' : PreRecord .
 vars rho rho' : Env .
 vars b b' b'' b1 b2 : Env .
 vars i i' : Ide .
 var m : Match .
 var v v' : Value .
 var e : Exp .

  eq unfold(i,v) = reclose(i,v)(i,v) .
  eq reclose(i,v)(i, closure(m, b')) 
     = new-env (i, reclosure (m, b', new-env(i,v))) .
  eq reclose(i,v)(i, reclosure(m, b', b'')) 
     = new-env (i, reclosure (m, b', new-env(i,v))) .

  rl { fn M:Match, { (env : rho), pr} } 
     => [ closure(M:Match, rho), { (env : rho), pr} ] .

  rl { closure(M:Match, rho) v, r } 
     => [ let rho in case v of M:Match end, r ] .

  rl { fun i (i') = e, { (env : rho), pr} } 
     => [ unfold(i, closure(pat(i') => e, rho)), 
          { (env : rho), pr} ] .

 crl { reclosure(pat(i) => e, b', b) v, { (env : rho), pr} } 
     => [ let b2 in e end, { (env : rho), pr} ]
  if b1 := override-env (b', unfold (get-ide(b), get-val(b))) /\ 
     b2 := override (b1, i, v) . 
endm

mod IMPERATIVES-SYNTAX is
 extending ABSTRACTIONS-SYNTAX .
 including STORE .

 op while_do_ : Exp Exp -> Exp .
 op _:=_ : Exp Exp -> Exp [prec 40] .
 ops ! ref : -> Value [ctor] .
endm

mod IMPERATIVES-SEMANTICS is
 including IMPERATIVES-SYNTAX .
 extending ABSTRACTIONS-SEMANTICS .

 vars sigma sigma' : Store .
 var l : Loc .
 var v : Value .
 var pr : PreRecord .
 vars e1 e2 e'1 e'2 e e' : Exp .
 vars r r' : Record .

 subsort Loc < Value .

  crl { ref v, { (st : sigma), pr} } => 
      [ l, { (st : sigma'), pr} ]
   if l := newLoc(sigma) /\ 
      sigma' := update (sigma, l, v) .

 crl { ! l, { (st : sigma), pr}  } => 
     [ v, { (st : sigma), pr}  ]
   if v := lookup(sigma, l) .

 crl { e1 := e2, r } => [ e'1 := e2, r' ] 
   if { e1, r } => [ e'1, r' ] .
 crl { l := e2, r } => [ l := e'2, r' ] 
   if { e2, r } => [ e'2, r' ] .
 crl { l := v, {(st : sigma), pr}  } => 
     [ tuple(), {(st : sigma'), pr}  ]
   if sigma' := update (sigma, l, v) .

 rl { while e1 do e2, r } => 
    [ (if e1 then (e2 ; (while e1 do e2)) else tuple()), r ] .
endm

fmod EXCEPTION is 
 sort Exc .
endfm

fmod EXCS is
 extending RECORD .
 protecting INT . 
 including EXCEPTION .

 sorts Excs .
 subsort Excs < Component .
 
 op excs : -> Index [ctor] .

 op new-exc : Excs -> Exc .
 op add-exc : Excs Exc -> Excs .

 mb excs : E:Excs : Field .
endfm

fmod RAISING is
 protecting RECORD .
 including EXCEPTION .
 
 sorts Raising RVal .

 subsort Raising < Component .

 op raising-id : -> Raising [ctor] .

 op set_ : RVal -> Raising .
 op get_ : Raising -> RVal .

 eq get set rv:RVal = rv:RVal .

 op raising : -> Index .
 mb raising : r:Raising : Field .
endfm

fmod EXCEPTIONS-SYNTAX is
 extending IMPERATIVES-SYNTAX .

 op exception_ : Ide -> Decl .
 op raise_ : Exp -> Exp .
 op _handle_ : Exp Match -> Exp .
endfm

mod EXCEPTIONS-SEMANTICS is
 including EXCEPTIONS-SYNTAX .
 extending IMPERATIVES-SEMANTICS .
 including EXCS .
 including RAISING .

 var i : Ide .
 var b : Env .
 vars r r' : Record .
 vars pr pr' : PreRecord .
 vars ex ex' : Excs .
 var m : Match .
 var e e' e'' : Exp .
 var v : Value .
 var rs rs' : Raising .

 --- Exc may appear on environments or vals (pattern matching)
 subsort Exc < BVal .
 subsort Exc < ValContent .

 *** boxing of Exc into RVal
 *** setting Exc < RVal gives us: `operator set_ has been imported
 *** from [...] with no common ancestor', so we coerce it
 op rval : Exc -> RVal [ctor] .

 crl { exception i, { (excs : ex), pr } } => 
     [ new-env(i, e:Exc), { (excs : add-exc(ex, e:Exc)), pr } ]
   if e:Exc := new-exc (ex) .

 crl { raise e, r } => [ raise e', r' ]
   if { e, r } => [ e', r' ] .

 rl { raise e:Exc, { (raising : rs), pr } } => 
    [ tuple(),  { (raising : set rval(e:Exc)), pr } ] .

 crl { e handle m, { (raising : rs), pr } } => 
     [ e' handle m, { (raising : rs), pr' } ]
   if { e, { (raising : raising-id), pr } } => 
      [ e', { (raising : raising-id), pr' } ] .

  rl { v handle m, r } => [ v, r ] .

 crl { e handle m, { (val : val:Val), (raising : rs), pr } } => 
     [ let b in e'' end, { (val : val:Val), (raising : rs), pr' } ]
   if { e, {(val : val:Val), (raising : rs), pr} } => 
      [ e', {(val : val:Val), (raising : rs'), pr'} ] /\
      rval(e:Exc) := get rs' /\ val':Val := set e:Exc /\
      { m, {(val : val':Val), (raising : rs), pr} } => 
      [ match-value(b, e''), { (val : val':Val), (raising : rs), pr'} ] .

 crl { e handle m, {(val : val:Val), (raising : rs), pr} } => 
     [ e', {(val : val:Val), (raising : rs), pr'} ]
   if { e, {(val : val:Val), (raising : rs), pr} } => 
      [ e', {(val : val:Val), (raising : rs'), pr'} ] /\
      rval(e:Exc) := get rs' /\ val':Val := set e:Exc /\
      { m, {(raising : rs), (val : val':Val), pr} } => 
      [ failure, {(raising : rs), (val : val':Val), pr'} ] .
endm

fmod ACTS is
 extending RECORD .
 extending VALUE .
 
 sorts Acts Act .
 subsort Acts < Component .

 op ac : -> Index [ctor] .

 op concat : Acts Act -> Acts . 
 op last   : Acts -> Act .

 mb ac : A:Acts : Field .
endfm

fmod PID is 
 sort Pid .
endfm

fmod PIDS is
 extending RECORD .
 including PID .

 sorts Pids .
 subsort Pids < Component .

 op pids : -> Index [ctor] .

 op new-pid : Pids -> Pid .
 op add-pid : Pids Pid -> Pids .

 mb pids : P:Pids : Field .
endfm

fmod CHANNEL is 
 sort Chan .
endfm

fmod CHANS is
 extending RECORD .
 including CHANNEL .

 sorts Chans .
 subsort Chans < Component .
 
 op chans : -> Index [ctor] .

 op new-chn : Chans -> Chan .
 op add-chn : Chans Chan -> Chans .

 mb chans : C:Chans : Field .
endfm

fmod TRACE is
 protecting RECORD .
 protecting PID .

 sorts Trace TOp .
 subsort Trace < Component .

 op tr : -> Index [ctor] .

 op tr-id : -> Trace [ctor] .

 op new-tr : TOp -> Trace .
 op prc-run : Pid -> TOp [ctor] .

 mb tr : T:Trace : Field .
endfm

fmod OFFER is
 protecting RECORD .
 protecting VALUE .
 protecting CHANNEL .

 sorts Offers Offer .

 subsort Offers < Component .

 op offer-id : -> Offers [ctor] .

 op snd : Chan Value -> Offer .
 op rcv : Chan -> Offer .

 op agree : Offer Offer -> Bool .
 op agree-value : Offer Offer -> [Value] .

 eq agree (snd(ch:Chan, v:Value), rcv(ch:Chan)) = true .
 eq agree (snd(ch:Chan, v:Value), rcv(ch':Chan)) = false [owise] .

 eq agree-value (snd(ch:Chan, v:Value), rcv(ch:Chan)) = v:Value .
 
 op set_ : Offer -> Offers .

 op offer : -> Index .
 mb offer : o:Offers : Field .
endfm

fmod CONCURRENCY-SYNTAX is
 extending EXCEPTIONS-SYNTAX .
 including PID .

 sorts Prog Proc Procs  .

 op cml_ : Procs -> Prog .
 op prc : Pid Exp -> Proc .

 subsort Proc < Procs .

 op _||_ : Procs Procs -> Procs [comm assoc] .
 ops spawn channel send recv : -> Value [ctor] .
endfm

mod CONCURRENCY-SEMANTICS is
 including CONCURRENCY-SYNTAX .
 extending EXCEPTIONS-SEMANTICS .
 extending RCONF .
 including ACTS .
 including PIDS .
 including CHANS .
 including OFFER .
 including TRACE .
 including META-LEVEL .

 subsorts Prog Procs < Program .

 *** concrete sort coercion
 op act : Proc -> Act [ctor] .

 vars p1 p2 p'1 p'2 : Proc .
 var PS1 PS2 PS : Procs .

 var r r' : Record .
 var pr pr' : PreRecord . 
 var v : Value .
 var a a' : Acts .
 var pi pi1 pi2 : Pid .
 var pc : Procs .
 var pg : Prog .
 var e1 e2 e'1 : Exp .
 var ps : Pids .

 subsort Pid < BVal . 
 subsort Chan < BVal .

 var c : Chans .
 var ch : Chan .
 vars o o' o1 o2 : Offer .

 *** we can't use these rules, originally from MSOS, since
 *** Maude doesn't do unification of free variables (v,
 *** in this particular case)
 ***
 *** `v' remains a free variable until it is unified
 *** on the [SYNCH] rule.

 crl { channel tuple(), {(chans : c), pr} } => 
     [ ch, {(chans : add-chn(c, ch)), pr} ] 
   if ch := new-chn (c) .

 rl { send tuple(ch, v), {(offer : o:Offers),pr} } =>
     [ tuple(), {(offer : set snd(ch,v)), pr} ] .

 op recv-ph : Chan -> Value [ctor] .

 rl { recv ch, {(offer : o:Offers),pr} } =>
     [ recv-ph(ch), {(offer : set rcv(ch)), pr} ] .

 op meta-update-recv : TermList Value -> TermList .

 eq meta-update-recv (q:Qid[tl1:TermList,tl2:TermList], v:Value) =
       q:Qid[meta-update-recv (tl1:TermList, v:Value), 
             meta-update-recv (tl2:TermList, v:Value)] .

 eq meta-update-recv ((tl1:TermList,tl2:TermList), v:Value) =
             (meta-update-recv (tl1:TermList, v:Value), 
              meta-update-recv (tl2:TermList, v:Value)) .

 eq meta-update-recv ('recv-ph['chn[t:Term]], v:Value) = upTerm(v:Value) .
 eq meta-update-recv (t:TermList, v:Value) = t:TermList [owise].

 op update-recv : Procs Value -> Procs .
 op update-recv-exp : -> Procs [ctor] .
 eq update-recv(p:Procs, v:Value) = 
    downTerm(meta-update-recv(upTerm(p:Procs),v:Value), update-recv-exp) .

 crl { p1 || p2, {(offer : o:Offers), pr} } => [ p'1 || update-recv (p'2, v), {(offer : o:Offers), pr} ]
   if { p1, {(offer : o:Offers),pr} } => [ p'1, {(offer : set o1), pr} ] /\
      { p2, {(offer : o:Offers),pr} } => [ p'2, {(offer : set o2), pr} ] /\
      agree(o1, o2) /\ v := agree-value (o1, o2) .

---(
 crl { cml P:Procs, {(offer : offer-id), pr} } => [ cml P:Procs, {(offer : offer-id), pr'} ]
   if { P:Procs,  {(offer : offer-id), pr} } =>
      [ P':Procs, {(offer : offer-id), pr'} ] .
)
 
 crl { prc(pi1, e1:Exp), {(ac : a), pr} } => 
     [ (prc(pi1, e'1:Exp) || p1), {(ac : a), pr'} ]
     if { e1,  {(ac : a), pr} } => 
        [ e'1, {(ac : a'), pr' } ] /\ act(p1) := last(a') .

---(
 crl { prc(pi1, e1:Exp), {(ac : a), (tr : t:Trace), pr} } => 
     [ prc(pi1, e'1:Exp), {(ac : a), (tr : new-tr (prc-run(pi1))), pr' } ]
     if { e1,  {(ac : a), (tr : t:Trace), pr} } => 
        [ e'1, {(ac : a), (tr : t':Trace), pr' } ] .
)

 crl { prc(pi1, e1:Exp), {(ac : a), pr} } => 
     [ prc(pi1, e'1:Exp), {(ac : a), pr' } ]
     if { e1,  {(ac : a), pr} } => 
        [ e'1, {(ac : a), pr' } ] .

  crl { spawn v, {(pids : ps), (ac : a), pr} } => 
      [ pi, {(pids : add-pid(ps,pi)), 
             (ac : concat(a, act(prc(pi, (v tuple()))))), pr} ] 
     if pi := new-pid(ps) .

  crl { p1 || PS2, r } => [ PS1 || PS2, r' ] 
    if { p1, r } => [ PS1, r' ] .
endm

--- Concrete components

fmod CML-LOCATION is
 including LOCATION .
 protecting NAT .

 op loc : Nat -> Loc [ctor] .
endfm

fmod CML-STORE is
 including STORE .
 protecting CML-LOCATION .
 protecting CML-VALUES .

 sort Cell CStore .
 subsort Cell < CStore .
 subsort NumberConstant < SVal .

 op mt-st : -> CStore [ctor] .
 op [[_,_]] : Loc SVal -> Cell [ctor] .
 op __ : CStore CStore -> CStore [ctor assoc comm id: mt-st] .
 op _[_|->_] : CStore Loc SVal -> CStore .
 op _(_) : CStore Loc -> SVal .
 op <_> : [CStore] -> [Store] .
 op dupl : [CStore] -> [Bool] .

 eq dupl([[ L:Loc,SV:SVal ]] [[ L:Loc,SV1:SVal ]] 
         CS:CStore) = true .
 cmb < CS:CStore > : Store if dupl(CS:CStore) =/= true .  

 eq lookup(< CS:CStore >, L:[Loc]) = CS:CStore ( L:[Loc] ) .
 eq update(< CS:CStore >, L:Loc, SV:SVal) = 
	< CS:CStore [ L:Loc |-> SV:SVal ] > . 

 eq ([[ L:Loc,SV:SVal ]] CS:CStore)(L:Loc) = SV:SVal .
 eq CS:CStore ( L:Loc ) = rat(0) [owise] .

 eq ([[ L:Loc , SV:SVal ]] CS:CStore)[ L:Loc |-> SV':SVal ] = 
        ([[ L:Loc , SV':SVal ]] CS:CStore)  .
 eq CS:CStore [ L:Loc |-> SV':SVal ] = 
	[[ L:Loc , SV':SVal ]] CS:CStore [owise] .

 var s : Store .
 var cs : CStore .
 var sv : SVal .

 op newLocAux : Store Nat -> Loc .
 eq newLoc(s) = newLocAux(s, 0) .
 ceq newLocAux(< cs [[loc(N:Nat), sv]] >, M:Nat) =
     newLocAux(< cs >, N:Nat) if N:Nat > M:Nat .
 eq newLocAux(s,M:Nat) = loc(s(M:Nat)) [owise] .
endfm

fmod CML-BASIC-ENVIRONMENT is
 including BASIC-ENVIRONMENT .
 protecting CML-VALUES .
 protecting CML-LOCATION .

 sort Bind CEnv .
 subsort Bind < CEnv .
 subsorts Loc Tuple List Rec NumberConstant < BVal .

 op mt-env : -> CEnv [ctor] .
 op [_,_] : Ide BVal -> Bind [ctor] .
 op __ : CEnv CEnv -> CEnv [ctor assoc comm id: mt-env] .
 op <_> : [CEnv] -> [Env] . 
 op dupl : [CEnv] -> [Bool] .
 
 eq env-id = < mt-env > .

 var i : Ide .
 vars bv bv' bv1 : BVal .
 var e : Env .
 var ce : CEnv .

 eq dupl([i,bv] [i,bv1] ce) = true .
 cmb < ce > : Env if dupl(ce) =/= true .  

 eq find(< [i, bv] ce >,i) = bv .
 eq find(e,i) = no-value [owise] .

 eq new-env (i, bv) = < [i,bv] > .

 eq override-env(e, < mt-env >) = e .
 eq override-env(e, < [i, bv] ce >) = 
    override-env (override (e, i, bv), < ce >) .


 eq get-ide (< [i, bv] >) = i .
 eq get-val (< [i, bv] >) = bv .

 eq override(< [i,bv] ce >,i,bv') = 
    < [i,bv'] ce > .
 eq override(< ce >, i, bv') = 
    < [i, bv'] ce > [owise] .
endfm

fmod CML-VAL is
 including VAL .
 protecting CML-VALUES .
 protecting CML-LOCATION .

 sorts CVal CValContent .
 subsort CValContent < CVal .

 subsorts Loc Tuple List Rec NumberConstant < ValContent .

 op <_> : CVal -> Val [ctor] .
 op mt-val : -> CVal [ctor] .

 op cval[_] : ValContent -> CValContent [ctor] .

 eq set vc:ValContent = < cval[vc:ValContent] > .
 eq get < cval[vc:ValContent] > = vc:ValContent .

endfm

fmod CML-EXCEPTION is
 including EXCEPTION .
 protecting NAT .

 op exc : Nat -> Exc [ctor] .
endfm

fmod CML-EXCS is
 including EXCS .
 protecting CML-EXCEPTION .
 
 sort CExcs EVal .
 subsort EVal < CExcs .

 op mt-excs : -> CExcs [ctor] .

 op <_> : CExcs -> Excs .
 op _x_ : CExcs CExcs -> CExcs [ctor assoc id: mt-excs] .

 --- boxing of Exc into EVal
 op e[_] : Exc -> EVal [ctor] .

 eq new-exc (< mt-excs >) = exc(1) .
 eq new-exc (< C:CExcs x e[exc(i:Int)] >) = exc(s(i:Int)) .
 eq add-exc (< C:CExcs >, p:Exc) = < C:CExcs x e[p:Exc] > .
endfm

fmod CML-RAISING is
 including RAISING .
 protecting CML-EXCEPTION .

 sorts CRaising .
 subsort RVal < CRaising .
 op mt-raising : -> CRaising [ctor] .

 op <_> : CRaising -> Raising .
endfm

fmod CML-ACTS is
 including ACTS .

 sort CActs .
 subsort Act < CActs .

 op mt-ac : -> CActs [ctor] .

 op <_> : CActs -> Acts .

 op _x_ : CActs CActs -> CActs [ctor assoc id: mt-ac] .
 eq concat (< C:CActs >, A:Act) = < C:CActs x A:Act > .
 eq last (< C:CActs x A:Act >) = A:Act .
endfm

fmod CML-PID is
 including PID .
 protecting NAT .

 op pid : Nat -> Pid [ctor] .
endfm

fmod CML-PIDS is
 including PIDS .
 including CML-PID .

 sort CPids PVal .
 subsort PVal < CPids .
 
 op mt-pids : -> CPids [ctor] .

 op <_> : CPids -> Pids .
 op _x_ : CPids CPids -> CPids [ctor assoc id: mt-pids] .

 --- boxing of pid into pval
 op pval[_] : Pid -> PVal [ctor] .

 eq add-pid (< C:CPids >, p:Pid) = < C:CPids x pval[p:Pid] > .
 eq new-pid (< C:CPids x pval[pid(n:Nat)] >) = pid(s(n:Nat)) .
endfm

fmod CML-CHANNEL is
 including CHANNEL .
 protecting NAT .

 op chn : Nat -> Chan [ctor] .
endfm

fmod CML-CHANS is
 including CHANS .
 including CML-CHANNEL .

 sorts CChans CChan .
 subsort CChan < CChans .

 op mt-chans : -> CChans [ctor] .

 op <_> : CChans -> Chans .
 op _x_ : CChans CChans -> CChans [ctor assoc id: mt-chans] .

 --- boxing of Chan into CChan
 op c[_] : Chan -> CChan .

 eq add-chn (< C:CChans >, c:Chan) = < C:CChans x c[c:Chan] > .
 eq new-chn (< C:CChans x c[chn(n:Nat)] >) = chn(s(n:Nat)) .
 eq new-chn (< mt-chans >) = chn(1) .
endfm

fmod CML-OFFER is
 including OFFER .
endfm

fmod CML-TRACE is
 including TRACE .
 protecting PID .

 sorts CTrace CTVal .
 subsort CTVal < CTrace .

 op mt-tr : -> CTrace [ctor] .

 op t[_] : TOp -> CTVal [ctor] . 

 eq new-tr (o:TOp) = < t[o:TOp] > .

 op <_> : CTrace -> Trace .
endfm

fmod CML-SEMANTICS is
 protecting CML-BASIC-ENVIRONMENT .
 protecting CML-STORE .
 protecting CML-VAL .
 protecting CML-EXCS .
 protecting CML-RAISING .
 protecting CML-PIDS .
 protecting CML-ACTS .
 protecting CML-CHANS .
 protecting CML-OFFER .
 protecting CML-TRACE .
 protecting CONCURRENCY-SEMANTICS .
 protecting CML-VALUES .
endfm