okram

// the social.mm model-ADT is something I plan to build up to be the primary model used for the documentation.
// nat    -- natural positive integer
// date   -- 3 element list month/day/year
// moday  -- 2 element list with a default year provided
// person -- a person has an id, name, and age.
// badge  -- a badge has an id-code and a date

social:('type' -> (nat    -> (nat<=int[is,bool<=int[gt,0]]),
                   date   -> (date:(nat<=nat[is=<12];nat<=nat[is=<31];nat),
                              date<=(nat<=nat[is=<12];nat<=nat[is=<31])[put,2,2009]),

okram

mmlang> (1,2,3)>--<(int{3};[mult,10];-<(-<([is>20];-<(+70,+170,+270)>-)>-,
......>                                 -<([is>10];-<(*10,*20,*30)>-  )>-,
......>                                 -<(_;{0})>-                       )>-;[plus,100])>-
==>500
==>200
==>300{2}
==>400{2}
==>700{2}
==>1000

okram

mmlang> :[define,list<=lst[[is,>-[count]==0]|
......>                    [is,[and,[head]?int],[tail]?list]]]
mmlang> ()[a,list]
==>true
mmlang> (1)[a,list]
==>true
mmlang> ('a')[a,list]
==>false
mmlang> (1;2;3;4;5;6)[a,list]
==>true

okram

// 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)),

okram

mmlang> 1=>int[plus,1][plus,2][plus,3]
==>7
mmlang> 1=>int[plus,1][plus,2][plus,3][path]
==>(1;[plus,1];2;[plus,2];4;[plus,3];7)
mmlang> 1=>int[plus,1][plus,2][plus,3][path]=(_,_{0},_)
==>(1,,2)
mmlang> 1=>int[plus,1][plus,2][plus,3][path]=(_,_{0},_)>-
==>1
==>2
mmlang> 1=>int[plus,1][plus,2][plus,3][path]=(_,_{0},_)>-[sum]

okram

ex:('type' -> (nat    -> (nat<=int[is>0]),
               large  -> (large<=int[is>99],
                          large<=nat[is>99]),
               names  -> (names:(str,str)),
               user   -> (user:('id'->int,'login'->str),
                          user<=person[put,'id',.age][put,'login',.name]),
               person -> (person:('name'->str,'age'->nat),
                          person<=('name'->str,'age'->int),
                          person<=('name'->str)[put,'age',1],
                          person<=names-<('name'-><y>.0+<.y>.1,'age'->1),

okram

The mm-ADT ;-poly

mmlang> 5-<(+1;+2;+3;+4;+5)
==>(6;8;11;15;20)
mmlang> 5-<(+1+2;+3;+4+5)
==>(8;11;20)
mmlang> 5-<(+1+2+3+4+5)
==>(20)
mmlang> 5-<(+1;+2;+3;+4;+5)>-
==>20

okram

// kv-ADT
[define,kvstore<=kv{*},kv:('k'->obj,'v'->obj)]

// tp3-ADT
[define,graph:('V'->vertex{*},'E'->edge{*}),
  vertex:('id'->obj,'label'->str,'properties'->property{*},'outE'->edge{*},'inE'->edge{*}),
  edge:('id'->obj,'label'->str,'properties'->property{*},'outV'->vertex,'inV'->vertex),
  property:([is,!['id'|'label']]->obj)]
  

okram

mm-ADT: An Algebraic Overview for the Category Theory Meetup
  by Dr. Marko A. Rodriguez (collaborator: Dr. Ryan Wisnesky)

  http://mm-adt.org
  https://www.mm-adt.org/vm (draft)

https://www.meetup.com/Category-Theory/events/vmkkjrybckbkb/
------------------------------------------------------
------------------------------------------------------
            mm-ADT

okram

@scala.annotation.tailrec
  def fetchOption[A <: Obj](obj: Obj, label: String): Option[A] = {
    obj match {
      case x if x.root => None
      case x if x.via._2.op == Tokens.to && x.via._2.arg0[StrValue].g == label => obj match {
        case _: Value[Obj] => Some(x.via._1.asInstanceOf[A])
        case _: Type[Obj] => Some(x.via._1.range.from(label).asInstanceOf[A])
      }
      case x if x.via._2.op == Tokens.rewrite && x.via._2.arg0[Obj].name == label => Some(Inst.resolveArg(obj, x.via._2.arg0[A]))
      case x if x.via._2.op == Tokens.define && x.via._2.arg0[Obj].name == label => Some(Inst.resolveArg(obj, x.via._2.arg0[A].named(baseName(x.via._2.arg0[A]))))