From 60c439e7fdfc1c690a0c71195e90bef445d4e06e Mon Sep 17 00:00:00 2001 From: Teodoro Freund Date: Wed, 11 Sep 2019 16:34:47 +0200 Subject: [PATCH] Initial makam spec commit Quite limited for now --- .gitignore | 3 + makam-spec/README.md | 3 +- makam-spec/src/ast.makam | 70 +++++++++++++++++++++ makam-spec/src/eval.makam | 72 ++++++++++++++++++++++ makam-spec/src/examples.makam | 71 ++++++++++++++++++++++ makam-spec/src/init.makam | 12 ++++ makam-spec/src/syntax.makam | 108 +++++++++++++++++++++++++++++++++ makam-spec/src/typecheck.makam | 65 ++++++++++++++++++++ 8 files changed, 402 insertions(+), 2 deletions(-) create mode 100644 makam-spec/src/ast.makam create mode 100644 makam-spec/src/eval.makam create mode 100644 makam-spec/src/examples.makam create mode 100644 makam-spec/src/init.makam create mode 100644 makam-spec/src/syntax.makam create mode 100644 makam-spec/src/typecheck.makam diff --git a/.gitignore b/.gitignore index f42673af90..725815ec96 100644 --- a/.gitignore +++ b/.gitignore @@ -3,3 +3,6 @@ # rustfmt Backup file **/*.rs.bk + +# Makam cache +.makam-cache/ diff --git a/makam-spec/README.md b/makam-spec/README.md index 0298b0b402..7dc0bfb65e 100644 --- a/makam-spec/README.md +++ b/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 - diff --git a/makam-spec/src/ast.makam b/makam-spec/src/ast.makam new file mode 100644 index 0000000000..26eb8d89ee --- /dev/null +++ b/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. diff --git a/makam-spec/src/eval.makam b/makam-spec/src/eval.makam new file mode 100644 index 0000000000..f5aa80b030 --- /dev/null +++ b/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. diff --git a/makam-spec/src/examples.makam b/makam-spec/src/examples.makam new file mode 100644 index 0000000000..e7b7c4599b --- /dev/null +++ b/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 ? diff --git a/makam-spec/src/init.makam b/makam-spec/src/init.makam new file mode 100644 index 0000000000..90b0c9bc07 --- /dev/null +++ b/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). diff --git a/makam-spec/src/syntax.makam b/makam-spec/src/syntax.makam new file mode 100644 index 0000000000..3c1965eb2b --- /dev/null +++ b/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_FATARROW -> { } / { "> } +token_PROD -> { } / { } + +binop -> + (fun u => add) { } + / (fun u => sub) { } + / (fun u => mul) { } + +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_ -> ite + { "Ifte(" "," "," ")" } + / (fun id => fun body => lam (concrete.bindone id body)) + { "fun" token_FATARROW } + / clet + { "let" "in" } + / ebinop + { } + / eunop + { } + / app + { } + / { } + +baseexpr -> + promise + { "Promise(" "," ")"} + / fun ty => assume ty (label "Assume") + { "Assume(" "," ")"} + / ebool true { "true" } + / ebool false { "false" } + / estr { } + / concrete.var + { } + / eint + { } + / { "(" ")" } + +def -> tuple + { "(" "=" ")" } + +id -> concrete.name exprvar + { } + +baseTyp -> + tnum + { "Num" } + / tbool + { "Bool" } + / tdyn + { "Dyn" } + / tstr + { "String" } + / { "(" ")" } + +typ -> tarrow + { "->" } + / { } + +}} ). + +`( 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)). diff --git a/makam-spec/src/typecheck.makam b/makam-spec/src/typecheck.makam new file mode 100644 index 0000000000..69dabfa52d --- /dev/null +++ b/makam-spec/src/typecheck.makam @@ -0,0 +1,65 @@ +%use "ast". + +typecheck : expr -> typ -> prop. + +typecheck (let E (bind _ B)) T :- + typecheck E T', + (x: expr -> + typecheck x T' -> + typecheck (B x) T + ). + +typecheck (lam (bind _ B)) (tarrow S T) :- + (x: expr -> + typecheck x S -> + typecheck (B x) T + ). + +typecheck (app A B) T :- + typecheck A ATy, + typecheck B BTy, + ifte (eq ATy (tarrow S T')) + (ifte (eq BTy S) + (eq T' T) + (eq tdyn T)) + (eq tdyn T). + +typecheck (eint _) tnum. +typecheck (ebool _) tbool. +typecheck (estr _) tstr. + +typecheck (ite C T E) Ty :- + typecheck C CTy, + typecheck T TTy, + typecheck E ETy, + ifte (eq CTy tbool) + (ifte (eq TTy ETy) + (eq Ty TTy) + (eq Ty tdyn)) + (eq Ty tdyn). + +typecheck (eunop blame _) _. + +typecheck (eunop isNum _) tbool. +typecheck (eunop isBool _) tbool. +typecheck (eunop isFun _) tbool. + +typecheck (ebinop A _ B) Ty :- + typecheck A ATy, + typecheck B BTy, + ifte (eq ATy tnum) + (ifte (eq BTy tnum) + (eq Ty tnum) + (eq Ty tdyn)) + (eq Ty tdyn). + +typecheck (promise Ty E) T :- + ifte (typecheck E Ty) + (eq T Ty) + (and (log_error Ty `Couldnt check Promise(...)`) failure). + +(* The type of an Assume construct doesn't depend on the term *) +typecheck (assume Ty _ E) Ty :- + typecheck E _. + +typecheck (label _) tdyn.