Skip to content

Instantly share code, notes, and snippets.

@mstewartgallus
Last active January 23, 2021 02:19
Show Gist options
  • Save mstewartgallus/c0f7dee98ee45539b822321640c2eb04 to your computer and use it in GitHub Desktop.
Save mstewartgallus/c0f7dee98ee45539b822321640c2eb04 to your computer and use it in GitHub Desktop.
Tried out makam (lambda Prolog dialect) http://astampoulis.github.io/makam/ . Remarkable velocity although poor tooling.
%open syntax.
expr : type.
id : expr.
compose : expr -> expr -> expr.
bang : expr.
v : (_ : string) -> expr.
kappa : string -> expr -> expr.
lift : expr -> expr.
z : (_ : int) -> expr.
add : expr.
var : syntax string.
expr, base : syntax expr.
`(syntax_rules <<
expr ->
compose { <base> "∘" <expr> }
/ lift { "lift" <expr> }
/ base ;
base ->
id { "id" }
/ bang { "!" }
/ add { "add" }
/ kappa { "κ" <var> "." <expr> }
/ z { <makam.int_literal> }
/ v { <var> }
/ { "(" <expr> ")" } ;
var -> { <makam.string_literal> }
>>).
`(syntax.def_toplevel_js expr ).
val : type.
bangval : val.
zval : (_ : int) -> val.
tupleval : (_ : val) (_ : val) -> val.
(* TODO figure out lists later *)
env : type.
nil : env.
bind : (_ : string) (_ : val) (_ : env) -> env.
search : (Env : env) (Key : string) (Val : val) -> prop.
search (bind Key Val _) Key Val.
(* FIXME is there a not equals constraint to maybe use here? *)
search (bind _ _ Tail) Key Val :-
search Tail Key Val.
eval : (_ : env) (_ : expr) (_ : val) (_ : val) -> prop.
eval _ id X X.
eval Env (compose F G) X Z :-
eval Env G X Y,
eval Env F Y Z.
eval _ bang _ bangval.
eval Env (v Var) bangval Y :-
search Env Var Y.
eval Env (lift F) T (tupleval H T) :-
eval Env F bangval H.
eval Env (kappa Var Body) (tupleval H T) Y :-
eval (bind Var H Env) Body T Y.
eval _ (z N) bangval (zval N).
eval _ add (tupleval (zval X) (tupleval (zval Y) bangval)) (zval Z) :-
plus X Y Z.
evalstr : (_ : string) (_ : val) -> prop.
evalstr Input Output :-
syntax.run expr Input Ast,
eval nil Ast bangval Output.
evalstr << (add ∘ (lift 3)) ∘ lift 5 >> Y ?
evalstr << (κ "x" . (add ∘ (lift "x")) ∘ lift "x") ∘ lift 4 >> Y ?
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment