--------------------------  plan-syntax.m  -----------------------------------

--- Date: Sat, 25 Aug 2001 00:44:24 -0700
--- From: Mark-Oliver Stehr <stehr@csl.sri.com>
--- Revised by CLT 01 Oct
--- Contains modules PLAN-SYNTAX PLAN-ADDR PLAN-LITERALS


fmod PLAN-SYNTAX is

protecting BOOL .
protecting INT .
protecting STRING .
protecting QID .

---------------------------
--- Lists of Identifiers

sort Id .
subsort String < Id .

sort IdList .
subsort Id < IdList .
op empty-idl : -> IdList .
op _,_ : IdList IdList -> IdList [ assoc id: empty-idl] .

---------------------------
--- Types

sort PlanType .

op TAny : -> PlanType .
op TUnit : -> PlanType .
op TBool : -> PlanType .
op TInt : -> PlanType .
op TString : -> PlanType .
op TAddr : -> PlanType .
op TKey : -> PlanType .
op TPair__ : PlanType PlanType -> PlanType [ gather (e E) ] .
op TList_ : PlanType -> PlanType  .
op TChunk_ : PlanType -> PlanType .
op TException : -> PlanType .

sort PlanTypeList .

subsort PlanType < PlanTypeList .
op empty-typel : -> PlanTypeList .
op _`,_ : PlanTypeList PlanTypeList -> PlanTypeList 
          [ assoc id: empty-typel ].

---------------------------
--- Indexed Variables

sort Var .

op _{_} : Id Nat -> Var [ prec 0 gather (E &) ] .

---------------------------
--- Constants

sort Cstr NonCstr Const .
subsort Cstr < Const .
subsort NonCstr < Const .

op  Dummy : -> Const .
op  Equal : -> NonCstr .
ops Not And Or : -> NonCstr .
ops Plus Minus Mul Div : -> NonCstr .
op  Pair : -> Cstr .
ops Fst Snd : -> NonCstr .
op  Cons  : -> Cstr .
op  Nil : -> Const .
ops Hd Tl : -> NonCstr .
ops Length Member Append Reverse : -> NonCstr .
ops Foldr Foldl : -> NonCstr .
op  Chunk : -> Cstr .

op  Print : -> NonCstr .
ops ThisHost ThisHostIs : -> NonCstr .
ops GetRB GetSrcDev GetSource : -> NonCstr .
ops GetNeighbors GetDevToHost : -> NonCstr .
ops Eval OnNeighbor  : -> NonCstr .
ops DefaultRoute OnRemote OnRemote' : -> NonCstr .
ops GenerateKey Exists Get Put Delete SetLT SetGT : -> NonCstr .

ops DivByZero ServiceNotPresent HdExcept TlExcept : -> Const .
ops NotEnoughRB HostNotLocal NoRouteEntry NotFound : -> Const .

---------------------------
--- Expressions

sort At Ex .
subsort Const < At < Ex .
subsort Var < At < Ex .

op __ : Ex ExList -> Ex [ prec 21 gather (E e) ] .
op _;_ : Ex Ex -> Ex [ prec 30 gather (e E) ] .
op If_Then_Else_ : Ex Ex Ex -> Ex .
op Let`[_=_`]_ : IdList ExList Ex -> Ex [ prec 30 gather (& & E) ] .
op LetRec`[_=_`]_ : IdList ExList Ex -> Ex [ prec 30 gather (& & E) ] .
op Lam`[_:_`]_ : IdList PlanTypeList Ex -> Ex [ prec 30 gather (& & E) ] .
op Try_Handle`[_`]_ : Ex Id Ex -> Ex [ prec 30 gather (E & E) ] .
op Raise_ : Ex -> Ex .
op _:_ : Ex PlanType -> Ex .

---------------------------
--- Lists of Expressions

sort EmptyExList ExList .

op empty-exl : -> EmptyExList .
subsort EmptyExList < ExList .

op _`,_ : EmptyExList EmptyExList -> EmptyExList 
          [ assoc id: empty-exl ] .

subsort Ex < ExList .
op _`,_ : ExList ExList -> ExList 
          [ assoc id: empty-exl ] .

endfm

------------------------  plan-addr.m -------------------------------
--- Date: Sat, 25 Aug 2001 00:44:24 -0700
--- From: Mark-Oliver Stehr <stehr@csl.sri.com>

fmod PLAN-ADDR is
protecting STRING .

--- Basic Network Sorts

sort Addr .  --- addresses (i.e. network interfaces)
op addr : String -> Addr .

endfm

------------------------  plan-literals.m -------------------------------
--- Date: Sat, 25 Aug 2001 00:44:24 -0700
--- From: Mark-Oliver Stehr <stehr@csl.sri.com>

fmod PLAN-LITERALS is

protecting STRING .
protecting PLAN-ADDR .
protecting PLAN-SYNTAX .

op Bool_ : Bool -> Const .
op Int_ : Int -> Const .
op String_ : String -> Const .
op Addr_ : Addr -> Const .
op Key_ : Int -> Const .

endfm