Initial makam spec commit

Quite limited for now

.gitignore

@@ -3,3 +3,6 @@
 
 # rustfmt Backup file
 **/*.rs.bk
+
+# Makam cache
+.makam-cache/

makam-spec/README.md

@@ -9,9 +9,8 @@ He distributes it through [NPM](https://www.npmjs.com/package/makam), and on the
 
 We use the `node2nix` helper, there's a [PR](https://github.com/NixOS/nixpkgs/pull/67703) to add it to nixpkgs, but for now this simple config should help.
 
-Just `nix-build -A makam` and have it on `result/bin/makam`
+Just `nix-build -A makam` and then `result/bin/makam ./src/init.makam -`. Or run `result/bin/makam src/init.makam src/examples.makam` to run the examples.
 
 ###### To update it
 
 Run `node2nix --nodejs-10 -c makam-composition.nix` on the `makam-spec` directory
-

makam-spec/src/ast.makam

@@ -0,0 +1,70 @@
+expr : type.
+typ : type.
+
+(* Lambda constructs *)
+let : expr -> bindone expr expr -> expr.
+lam : bindone expr expr -> expr.
+app : expr -> expr -> expr.
+
+(* Constants *)
+eint : int -> expr.
+ebool : bool -> expr.
+estr : string -> expr.
+
+(* Operations *)
+ite : expr -> expr -> expr -> expr.
+
+unop : type.
+eunop : unop -> expr -> expr.
+blame : unop.
+isNum : unop.
+isBool : unop.
+isStr : unop.
+isFun : unop.
+
+binop : type.
+ebinop : expr -> binop -> expr -> expr.
+add : binop.
+sub : binop.
+mul : binop.
+
+(* Typing *)
+promise : typ -> expr -> expr.
+assume : typ -> expr -> expr -> expr.
+
+(* Blaming *)
+label : string -> expr.
+
+(* Variables *)
+named : string -> expr.
+
+(* Types *)
+tdyn : typ.
+tnum : typ.
+tbool : typ.
+tstr : typ.
+tarrow : typ -> typ -> typ.
+
+(* Get the contract of a given type *)
+contract : typ -> expr -> prop.
+contract tdyn (lam (bind _ (fun l => lam (bind _ 
+  (fun t => t))))).
+contract tnum (lam (bind _ (fun l => lam (bind _ 
+  (fun t => ite (eunop isNum t) t (eunop blame l)))))).
+contract tbool (lam (bind _ (fun l => lam (bind _ 
+  (fun t => ite (eunop isBool t) t (eunop blame l)))))).
+contract tstr (lam (bind _ (fun l => lam (bind _ 
+  (fun t => ite (eunop isStr t) t (eunop blame l)))))).
+contract (tarrow S T) (lam (bind _ (fun l => lam (bind _ 
+  (fun t => ite (eunop isFun t) (lam (bind _ (fun x => app (app Ct l) (app t (app (app Cs l) x))))) (eunop blame l)))))) :-
+    contract S Cs,
+    contract T Ct.
+
+(* Other *)
+
+find : string -> list (tuple string A) -> A -> prop.
+find S [] _ :- log_error S `Not found in record ${S}`, failure.
+find S ((S, E) :: _) E.
+find S ((S', _) :: TL) E :-
+  not (eq S S'),
+  find S TL E.

makam-spec/src/eval.makam

@@ -0,0 +1,72 @@
+%use "ast".
+
+eval : expr -> expr -> prop.
+
+(* Lambda constructs *)
+eval (let E X_Body) V :-
+  bindone.apply X_Body E Body',
+  eval Body' V.
+
+eval (lam X_Body) (lam X_Body).
+
+eval (app E1 E2) V :-   (* Beta *)
+  eval E1 (lam X_Body),
+  bindone.apply X_Body E2 E',
+  eval E' V.
+
+(* Constants *)
+eval (eint N) (eint N).
+eval (ebool B) (ebool B).
+eval (estr S) (estr S).
+eval (label S) (label S).
+
+(* Operations *)
+eval (ite C T E) V :-
+  eval C (ebool true),
+  eval T V.
+eval (ite C T E) V :-
+  eval C (ebool false),
+  eval E V.
+
+eval_binop : binop -> expr -> expr -> expr -> prop.
+
+eval (ebinop E1 Op E2) V :-
+  map eval [E1, E2] [V1, V2],
+  eval_binop Op V1 V2 V.
+
+eval_binop add (eint N1) (eint N2) (eint N) :- plus N1 N2 N.
+eval_binop sub (eint N1) (eint N2) (eint N) :- plus N2 N N1, if (lessthan N 0 true) then (log_error _ `no negatives allowed`, failure) else success.
+eval_binop mul (eint N1) (eint N2) (eint N) :- mult N1 N2 N.
+
+eval_unop : unop -> expr -> expr -> prop.
+
+eval (eunop Op E) V :-
+  eval E E',
+  eval_unop Op E' V.
+
+eval_unop blame (label S) _ :- 
+  log_error S `Reached a blame with label ${S}`,
+  failure.
+
+eval_unop isNum (eint _) (ebool true).
+eval_unop isBool (ebool _) (ebool true).
+eval_unop isStr (estr _) (ebool true).
+eval_unop isFun (lam _) (ebool true).
+
+eval_unop isNum V (ebool false) :- not (eq V (eint _)).
+eval_unop isBool V (ebool false) :- not (eq V (ebool _)).
+eval_unop isStr V (ebool false) :- not (eq V (estr _)).
+eval_unop isFun V (ebool false) :- not (eq V (lam _)).
+
+(* Typing *)
+(* Promises don't perform any computation *)
+eval (promise _ T) V :-
+  eval T V.
+
+eval (assume Ty L T) V :-
+  contract Ty CTy,
+  eval (app (app CTy L) T) V.
+
+
+(* Variables *)
+eval (named X) _ :- log_error X `unknown variable ${X}`, failure.

makam-spec/src/examples.makam

@@ -0,0 +1,71 @@
+
+print "Simple example without let" ?
+
+interpreter "
+(fun x => x + x) 3
+" V T ?
+
+print "Promises are check before running, assumes after" ?
+
+interpreter "
+let ( id = fun t => t ) in
+
+Promise(Num,
+Ifte( ( Promise(Bool -> Bool, id) ) true, 3, Promise(Num, true))
+)
+" V T ?
+
+interpreter "
+let ( id = fun t => t ) in
+
+Promise(Num,
+Ifte( ( Promise(Bool -> Bool, id) ) true, 3, Assume(Num, true))
+)
+" V T ?
+
+interpreter "
+let ( id = fun t => t ) in
+
+Promise(Num,
+Ifte( ( Promise(Bool -> Bool, id) ) false, 3, Assume(Num, true))
+)
+" V T ?
+
+interpreter "
+let ( id = fun t => t ) in
+
+Promise(Num,
+Ifte( ( Promise(Bool -> Bool, id) ) false, 3, Assume(Num, 5))
+)
+" V T ?
+
+
+print " We don't have let polymorphism (any) " ?
+
+interpreter "
+let (id = fun x => x) in
+Ifte(true, Promise(Num, id 3), Promise(Bool, id true))
+" V T ?
+
+interpreter "
+let (id = fun x => x) in
+Ifte(true, Promise(Num, id 3), Assume(Bool, id true))
+" V T ?
+
+interpreter "
+let (id = fun x => x) in
+Ifte(false, Promise(Num, id 3), Assume(Bool, id true))
+" V T ?
+
+print "This is bad because order matters!!" ?
+interpreter "
+let (id = fun x => x) in
+Ifte(true, Assume(Bool, id true), Promise(Num, id 3))
+" V T ?
+
+print "We can still use Assume(...)s" ?
+
+interpreter "
+let (id = fun x => x) in
+Ifte(true, Promise( Num , id 3), Promise( Bool, Assume( Bool -> Bool , id ) true))
+" V T ?

makam-spec/src/init.makam

@@ -0,0 +1,12 @@
+%use "ast".
+%use "syntax".
+%use "eval".
+%use "typecheck".
+
+interpreter : string -> string -> string -> prop.
+interpreter S S' STy :-
+  either (isocast S (E: expr)) (log_error S `Parse error in Nickel program`),
+  either (typecheck E T) (and (log_error E `Could not typecheck`) (failure)),
+  eval E V,
+  isocast T (STy: string),
+  isocast V (S': string).

makam-spec/src/syntax.makam

@@ -0,0 +1,108 @@
+%use "ast".
+
+%open syntax.
+
+expr_, baseexpr : syntax expr.
+expr_concrete : syntax (concrete expr).
+id : syntax (concrete.name expr).
+def : syntax (concrete.name expr * expr).
+binop, binopC : syntax binop.
+unop, unopC : syntax unop.
+typ, baseTyp: syntax typ.
+
+exprvar : concrete.namespace expr.
+
+clet : (concrete.name expr * expr) -> expr -> expr.
+
+token_ARROW : syntax unit.
+token_FATARROW : syntax unit.
+token_PROD : syntax unit.
+
+`( syntax_rules {{
+
+token_ARROW -> { <token "→"> } / { <token "->"> }
+token_FATARROW -> { <token "⇒"> } / { <token "=>"> }
+token_PROD -> { <token "×"> } / { <token "*"> }
+
+binop ->
+        (fun u => add) { <token "+"> }
+      / (fun u => sub) { <token "-"> }
+      / (fun u => mul) { <token "*"> }
+
+unop ->
+        blame { "blame" }
+      / isNum { "isNum" }
+      / isBool { "isBool" }
+      / isStr { "isStr" }
+      / isFun { "isFun" }
+
+}} ).
+
+`( syntax.def_js binopC binop ).
+`( syntax.def_js unopC unop ).
+
+`( syntax_rules {{
+
+expr_concrete -> concrete { <expr_> }
+
+expr_ -> ite 
+        { "Ifte(" <expr_> "," <expr_> "," <expr_> ")" }
+      / (fun id => fun body => lam (concrete.bindone id body))
+        { "fun" <id> token_FATARROW <expr_> }
+      / clet
+        { "let" <def> "in" <expr_> }
+      / ebinop
+        { <baseexpr> <binopC> <baseexpr> }
+      / eunop
+        { <unopC> <baseexpr> }
+      / app
+        { <baseexpr>  <expr_> }
+      / { <baseexpr> }
+
+baseexpr ->
+        promise
+        { "Promise(" <typ> "," <expr_> ")"}
+      / fun ty => assume ty (label "Assume")
+        { "Assume(" <typ> "," <expr_> ")"}
+      / ebool true { "true" }
+      / ebool false { "false" }
+      / estr { <makam.string_literal> }
+      / concrete.var
+        { <id> }
+      / eint
+        { <makam.int_literal> }
+      / { "(" <expr_> ")" }
+
+def -> tuple
+        { "(" <id> "=" <expr_> ")" }
+
+id -> concrete.name exprvar
+        { <makam.ident> }
+
+baseTyp ->  
+        tnum 
+        { "Num" }
+      / tbool
+        { "Bool" }
+      / tdyn
+        { "Dyn" }
+      / tstr
+        { "String" }
+      / { "(" <typ> ")" }
+
+typ ->  tarrow
+        { <baseTyp> "->" <typ> }
+      / { <baseTyp> }
+
+}} ).
+
+`( syntax.def_toplevel_js expr_concrete ).
+`( syntax.def_toplevel_js typ ).
+
+concrete.pick_namespace_userdef (_: expr) exprvar.
+
+concrete.handle_unresolved_name (concrete.name exprvar ID) (named ID).
+
+concrete.resolve_conversion
+    (clet (Name, Def) Body)
+    (let Def (concrete.bindone Name Body)).