define.java

/*** 
An mm-ADT type has a signature and a definition.
  range<=domain[inst]
   \_________/  \__/
    signature  definition   
***/


// An mm-ADT type definition is always with respects to the type of objects that can be mapped.
// In the definition below, an int can be mapped to a nat by way of a predicate membership function.
mmlang> 1[define,nat<=int[is>0]][as,nat]
==>nat:1
mmlang> -1[define,nat<=int[is>0]][as,nat]


// In the definitions below, the second definition maps a str to a nat accordingly.
// Define a nat by way of an int or by way of a str.
mmlang> '1'[define,nat<=int[is>0]]
           [define,nat<=str[as,int][is>0]][as,nat]
==>nat:1
mmlang> '-1'[define,nat<=int[is>0]]
            [define,nat<=str[as,int][is>0]][as,nat]
mmlang>

// If the domain of the type definition matches the obj to be mapped, then its mapped.
// If not, then the type graph is searched further for a definition that can do the mapping.
// If no match is found, then an error -- as there is no way to move between the two type subgraphs.

/////////////////////
// examples with some ring axioms being defined relative to int
// subsequent compilations can reduce to values or types
// "compiling" is applying a type obj to a type (program)
// "evaluating" is applying a value obj to a type (program)
// if "compiling" yields a value, then there is no need for another pass to evaluate.

mmlang> int[define,_<=([plus,0])]               // a+0 = a
           [define,_<=([mult,1)]                // a*1 = a
           [define,_<=([neg][neg])]             // --a = a
           [define,([zero])<=([mult,0])]        // a*0 = 0
           [define,([plus,0])<=([plus,[neg]])]  // a-a = 0
mmlang> int+0
==>0
mmlang> int+1+36*0
==>0
mmlang> int+1+36[mult,int[mult,[mult,0]]]
==>0
mmlang> int*1+36+0[plus,*0][plus,int[neg]]
==>int[plus,36]
mmlang> int*1*0+36+0[plus,*0][plus,int[neg]]
==>36
mmlang> int*1*0+36+0[plus,*0][plus,int[neg][plus,0][neg][neg]]
==>36