Skip to content

Instantly share code, notes, and snippets.

View okram's full-sized avatar
🏠
Working from home

Marko A. Rodriguez okram

🏠
Working from home
View GitHub Profile
mmlang> :[model,mm][define,tree<=[?0|(int;tree;int)]]
==>_[define,tree<=_[_{?}<=_[is,bool<=_[a,0]]|(int;tree;int)]]
mmlang> 0 => tree
==>tree:0
mmlang> 1 => tree
language error: 1 is not a tree
mmlang> (1;0;1) => tree
==>tree:(1;tree:0;1)
mmlang> (1;(2;0;2);1) => tree
==>tree:(1;tree:(2;tree:0;2);1)
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>
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]),(_[
{"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
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)
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
}
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
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)
@okram
okram / digraph.java
Last active September 8, 2020 07:49
/* 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))