--------------------------  plan-sorts.m  -----------------------------------

--- Date: Sat, 25 Aug 2001 00:44:24 -0700
--- From: Mark-Oliver Stehr <stehr@csl.sri.com>
--- Revised by CLT 01 Oct
--- Requires PLAN-LITERALS defined in plan-syntax.m
--- Defines PLAN-SORTS

fmod PLAN-SORTS is

including PLAN-LITERALS .

var a a' : Addr .

var bool bool' : Bool .
var str str' : String .
var int int' : Int .
var const const' : Const .
var var var' var'' : Var .
var cstr : Cstr .
var ncstr : NonCstr .


var id id' id'' : Id .
var idl idl' idl'' : IdList .

var type : PlanType .
var typel : PlanTypeList .

var ex ex' ex'' : Ex .
var exl exl' exl'' : ExList .


--- Values and NonValues

sort Val NonVal ValList .
subsort Val < Ex .
subsort NonVal < Ex .

subsort Const < Val .

subsort EmptyExList < ValList < ExList .
*** subsort EmptyExList < ExList .

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

var nval nval' nval'' : NonVal .
var val val' val'' : Val .
var val0 val0' val0'' : Val .
var val1 val1' val1'' : Val .
var vall vall' vall'' : ValList .

mb (Lam [idl : typel] ex) : Val .
mb (cstr vall) : Val .
mb (Raise val) : Val .

mb (val (exl,nval,exl')) : NonVal .
mb (nval exl) : NonVal .
mb (ncstr exl) : NonVal .
mb ((Lam [idl : typel] ex) exl) : NonVal .
mb (ex ; ex) : NonVal .
mb (If ex Then ex' Else ex'') : NonVal .
mb (Let [idl = exl] ex') : NonVal .
mb (LetRec [idl = exl] ex') : NonVal .
mb (Try ex Handle [id] ex') : NonVal .
mb (ex : type) : NonVal .

---------------------------
--- Subsorts of Values and Constants


sort PlanInt .
subsort PlanInt < Const .
mb (Int int) : PlanInt .

sort PlanBool .
subsort PlanBool < Const .
mb (Bool bool) : PlanBool .

sort PlanAddr .
subsort PlanAddr < Const .
mb (Addr a) : PlanAddr .

sort PlanKey .
subsort PlanKey < Const .
mb (Key int) : PlanKey .

sort PlanString .
subsort PlanString < Const .
mb (String str) : PlanString .

sort PlanPair .
subsort PlanPair < Val .
mb Pair (val, val') : PlanPair .

sort PlanFOPair .
subsort PlanFOPair < PlanPair Const .
mb Pair (const, const') : PlanFOPair .

sorts  PlanList PlanMtList .
subsorts PlanMtList < PlanList < Val .
sort PlanFOList .
subsorts PlanMtList < PlanFOList < Const PlanList .


vars pl pl' : PlanList .
vars pfl pfl' : PlanFOList .

mb Nil : PlanMtList .
mb Cons (val, pl) : PlanList .
mb Cons (const, pfl) : PlanFOList .

***(
sort PlanFOListAndConst . 
--- sort hierachy completion to obtain unique least sorts
subsort PlanFOListAndConst < PlanFOList .
subsort PlanFOListAndConst < Const .
mb Nil : PlanFOListAndConst .
)
endfm