mm-model.java

// The mm model-ADT
//    The base model on which all other mm-ADT models are built.
//    ... a subset presented below.

mm:('type' -> (bool -> (bool),
               int  -> (int),
               real -> (real),
               str  -> (str),
               lst  -> (lst),
               rec  -> (rec)),
    'path' -> (_    -> ((_)<=([id])),
               int  -> ((int)<=(int[neg][neg]),
                        (int)<=(int[plus,0]),
                        (int)<=(int[mult,1]),
                        ([1])<=(int[one]),
                        ([0])<=(int[zero]),
                        ([0])<=(int[mult,0]))))
    
///////////////////////////////////////////////

/**
With no model, instructions can only be concatenated to types (the free inst monoid).
With a model (and respective path equivalences), the path int-->[one] is equivalent to the identity path 1.
**/

mmlang> int[one]
==>int[one]
mmlang> :[model,'model/mm.mm']
mmlang> int[one]
==>1
  
/**
A few more examples
**/
  
mmlang> int[neg][neg]
==>int
mmlang> int[plus,0]
==>int
mmlang> int[plus,0][id][mult,1]
==>int
mmlang> int[plus,0][id][mult,57]
==>int[mult,57]

The reason that path equivalence domain and ranges are wrapped in a poly is due to "lifting." poly (lst/rec) is the foundation of the metaprogramming theory of mm-ADT.