Skip to content

Instantly share code, notes, and snippets.

Avatar
🏠
Working from home

Marko A. Rodriguez okram

🏠
Working from home
View GitHub Profile
View autocoercion.java
mmlang> 1
==>1
mmlang> 1-<(_;_)
==>(1;1)
mmlang> 1-<(_;_)=(vertex;vertex)
==>(vertex:('id'->nat:1);vertex:('id'->nat:1))
mmlang> 1-<(_;_)=(vertex;vertex)=>edge
==>edge:('outV'->vertex:('id'->nat:1),'inV'->vertex:('id'->nat:1))
mmlang>
mmlang>
View gist:c8f783b10440748f3baba1920f81dc5d
List(edge<=(vertex;vertex)[split,('outV'->vertex<=(vertex;vertex)[get,0,_],'inV'->vertex<=(vertex;vertex)[get,1,_])])
List(cmplx:(real;real), <x>, cmplx<=cmplx:(real;real)<x>, [plus,cmplx<y>]{2}, [combine,(real;real){2}], cmplx:(real;real){2})
List(attr:('key'->_,'value'->_))
List(digraph#1105759305:('type'->([inst]->([inst]),attr->(attr:('key'->_,'value'->_),attr<=(str;_[id])[split,('key'->str<=(str;_[id])[get,0,_],'value'->_<=(str;_[id])[get,1,_])]),nat->(nat<=int[is,bool<=int[gt,0]]),cmplx:(real;real){2}->(cmplx{2}<=cmplx:(real;real)<x>[plus,cmplx<y>]{2}),bool->(bool),real->(real),str->(str),cmplx:(real;real)->(cmplx:(real;real)),rec->(rec),int->(int<=vertex[get,'id',_],int<=nat,int),edge->(edge:('outV'->vertex,'inV'->vertex),edge<=(vertex;vertex)[split,('outV'->vertex<=(vertex;vertex)[get,0,_],'inV'->vertex<=(vertex;vertex)[get,1,_])]),(_)->((_)<=(_[id]),(_)),(int)->((int)<=(int[neg][neg]),(int)<=(int[plus,0]),(int)<=(int[mult,1]),(int)),(_[1])->((_[1])<=(int[one]),(_[1])),(_[0])->((_[0])<=(int[zero]),(_[
View digraph.json
{"id":{"@type":"g:Int64","@value":0},"label":"type","properties":{"iso":[{"id":{"@type":"g:Int64","@value":3},"value":{"empty":true,"serial":false,"choice":false,"plus":false,"parallel":false}}],"obj":[{"id":{"@type":"g:Int64","@value":1},"value":{"empty":true,"serial":false,"choice":false,"plus":false,"parallel":false}}],"root":[{"id":{"@type":"g:Int64","@value":2},"value":true}]}}
{"id":{"@type":"g:Int64","@value":64},"label":"type","inE":{"noop":[{"id":{"@type":"g:Int64","@value":68},"outV":{"@type":"g:Int64","@value":17},"properties":{"iso":{"empty":true,"serial":false,"choice":false,"plus":false,"parallel":false},"obj":{"empty":true,"serial":false,"choice":false,"plus":false,"parallel":false}}}]},"properties":{"iso":[{"id":{"@type":"g:Int64","@value":67},"value":{}}],"obj":[{"id":{"@type":"g:Int64","@value":65},"value":{}}],"root":[{"id":{"@type":"g:Int64","@value":66},"value":false}]}}
{"id":{"@type":"g:Int64","@value":4},"label":"type","inE":{"split":[{"id":{"@type":"g:Int64","@value":16},"outV":{"@typ
View graph.java
mmlang> :[model,mm] // the base model (int,bool,real,str,lst,rec)
......> [define,
......> vertex<=rec, // a vertex is a sort of record
......> vertex<=int-<('id'->_), // a vertex can be constructed from an int
......> edge<=rec, // an edge is a sort of record
......> edge<=(vertex;vertex)-<('source'->.0,'target'->.1)] // an edge can be constructed from a vertex x vertex pair
==>_[define,vertex<=rec,vertex<=int[split,('id'->int)],edge<=rec,edge<=(vertex;vertex)[split,('source'->vertex<=(vertex;vertex)[get,0,_],'target'->vertex<=(vertex;vertex)[get,1,_])]]
mmlang> 5 => vertex // morph 5 into a vertex
==>vertex:('id'->5)
View mmParser.scala
lazy val cType:Parser[Obj] = (anonType | boolType | realType | intType | strType | instType | (not(inst) ~> (lstType | recType)) | tokenType) ~ opt(quantifier) ^^ (x => x._2.map(q => x._1.q(q)).getOrElse(x._1))
lazy val dtype:Parser[Obj] = cType ~ rep[Inst[Obj, Obj]](inst) ^^ (x => x._2.foldLeft(x._1.asInstanceOf[Obj])((x, y) => y.exec(x))) | anonTypeSugar
// the top definition of a type
lazy val aType:Parser[Obj] = opt(cType <~ Tokens.:<=) ~ dtype ^^ {
case Some(range) ~ domain => range <= domain
case None ~ domain => domain
}
View pg_2.java
pg_2:('type' -> (
graph -> (graph<=edge{*}),
vertex -> (vertex<=('id'->int),
vertex<=int-<('id'->_)),
edge -> (edge<=('outV'->vertex,'inV'->vertex),
edge<=(vertex;vertex)-<('outV'->.0,'inV'->.1)))) <= mm
View HoTT-mm-ADT.txt
HoTT and Sweaty with mm-ADT
---------------------------
http://mm-adt.org/vm
In homotopy type theory,
there is a space U, (universal set)
a is a point in U, (object)
b is a point in U. (object)
View digraph.java
/* MODEL: digraph (extends numbers and mm)
digraph:(
'type' -> (
vertex -> (vertex:('id'->nat,'attrs'->attr{*}),
vertex<=nat-<('id'->nat),
vertex<=(nat;attr)=(_)-<('id'->.0,'attrs'->.1),
vertex<=int[is<0]-<([neg];('no';'data'))),
attr -> (attr:('key'->_,'value'->_),
attr<=(str;_)-<('key'->.0,'value'->.1)),
edge -> (edge:(outV->vertex,inV->vertex))
View social.java
// 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]),