Setepenre pushed to branch master at Stefan / Typer
Commits: 1a4d46c6 by Pierre Delaunay at 2016-12-04T11:26:57-05:00 updated quote and type_ example
- - - - - 40a83aac by Pierre Delaunay at 2016-12-04T12:39:43-05:00 * src/eval.ml: fixed sexp_dispatch implementation (was evaluating with the wrong context) * Merging
- - - - -
4 changed files:
- samples/dependent.typer - samples/inductive.typer - samples/quote.typer - src/eval.ml
Changes:
===================================== samples/dependent.typer ===================================== --- a/samples/dependent.typer +++ b/samples/dependent.typer @@ -1,8 +1,8 @@
Reify = inductive_ (Reify (a : Type)) - (RInt (a = Int)) - (RFloat (a = Float)) - (RString (a = String)); + (RInt (Eq (t := Type) Int a)) + (RFloat (Eq (t := Type) Float a)) + (RString (Eq (t := Type) String a));
RInt = datacons Reify RInt; RFloat = datacons Reify RFloat;
===================================== samples/inductive.typer ===================================== --- a/samples/inductive.typer +++ b/samples/inductive.typer @@ -3,8 +3,8 @@ make-decl : Sexp -> Sexp -> Sexp; make-decl var-name value-expr = node_ (symbol_ "_=_") - (cons (a := Sexp) var-name - (cons (a := Sexp) value-expr (nil (a := Sexp)))); + (cons var-name + (cons value-expr nil));
% build datacons % ctor-name = datacons type-name ctor-name; @@ -12,33 +12,31 @@ make-cons : Sexp -> Sexp -> Sexp; make-cons ctor-name type-name = make-decl ctor-name (node_ (symbol_ "datacons") - (cons (a := Sexp) type-name - (cons (a := Sexp) ctor-name (nil (a := Sexp))))); + (cons type-name + (cons ctor-name nil)));
% buil type annotation % var-name : type-expr; make-ann : Sexp -> Sexp -> Sexp; make-ann var-name type-expr = node_ (symbol_ "_:_") - (cons (a := Sexp) var-name - (cons (a := Sexp) type-expr (nil (a := Sexp)))); + (cons var-name + (cons type-expr nil));
type-impl = lambda (x : List Sexp) -> % x follow the mask -> (_|_ Nat zero (succ Nat)) % Type name --^ ^------^ constructors
- let sexp_nil = (nil (a := Sexp)) in - % Return a list contained inside a node sexp let get-list : Sexp -> List Sexp; get-list node = sexp_dispatch_ (a := List Sexp) node (lambda op lst -> lst) % Nodes - (lambda _ -> sexp_nil) % Symbol - (lambda _ -> sexp_nil) % String - (lambda _ -> sexp_nil) % Integer - (lambda _ -> sexp_nil) % Float - (lambda _ -> sexp_nil) in % List of Sexp + (lambda _ -> nil) % Symbol + (lambda _ -> nil) % String + (lambda _ -> nil) % Integer + (lambda _ -> nil) % Float + (lambda _ -> nil) in % List of Sexp
% Get a name from a sexp % - (name t) -> name @@ -53,24 +51,28 @@ type-impl = lambda (x : List Sexp) -> (lambda _ -> symbol_ "error") % Float (lambda _ -> symbol_ "error") in % List of Sexp
+ let get-head : List Sexp -> Sexp; + get-head x = case x + | cons hd _ => hd + | nil => symbol_ "error" in + % Get expression - let expr = head (a := Sexp) x in + let expr = get-head x in
% Expression is node_ (symbol_ "|") (list) % we only care about the list bit let lst = get-list expr in
% head is (node_ type-name (arg list)) - let name = head (a := Sexp) lst; - ctor = tail (a := Sexp) lst in + let name = get-head lst; + ctor = tail lst in
let type-name = get-name name in
% Create the inductive type definition let inductive = node_ (symbol_ "inductive_") - (cons (a := Sexp) name ctor) in + (cons name ctor) in
- % Create a forward declaration in case the declaration is recursive let decl = make-decl type-name inductive in
% Add constructors @@ -78,40 +80,40 @@ type-impl = lambda (x : List Sexp) -> let for-each : List Sexp -> List Sexp -> List Sexp; for-each ctr acc = case ctr | cons hd tl => ( - let acc2 = cons (a := Sexp) (make-cons (get-name hd) type-name) acc in + let acc2 = cons (make-cons (get-name hd) type-name) acc in for-each tl acc2) | nil => acc - in for-each ctor (nil (a := Sexp)) in + in for-each ctor nil in
% return decls - (cons (a := Sexp) decl % inductive type declaration - ctors); % constructor declarations + (cons decl % inductive type declaration + ctors); % constructor declarations
-type_ = Macro_ type-impl; +type_ = DMacro_ type-impl;
% (type_ (_|_ (Either t1 t2) (either-first t1) (either-second t2))) -type Either t1 t2 - | either-first t1 - | either-second t2; +%type Either t1 t2 +% | either-first t1 +% | either-second t2;
-type Pair t1 t2 - | pair t1 t2; +%type Pair t1 t2 +% | pair t1 t2;
type Point t | point (x : t) (y : t);
-get-first : (a : Type) => (b : Type) => Pair -> a; -get-second : (a : Type) => (b : Type) => Pair -> b; +%get-first : (a : Type) => (b : Type) => Pair a b -> a; +%get-second : (a : Type) => (b : Type) => Pair a b -> b;
-get-first p = case p | pair a b => a; -get-second p = case p | pair a b => b; +%get-first p = case p | pair a b => a; +%get-second p = case p | pair a b => b;
-get-x : (a : Type) => Point -> a; -get-y : (a : Type) => Point -> a; -get-x p = case p | point x y => x; -get-y p = case p | point x y => y; +%get-x : (a : Type) => Point a -> a; +%get-y : (a : Type) => Point a -> a; +%get-x p = case p | point x y => x; +%get-y p = case p | point x y => y;
% transformed to:
===================================== samples/quote.typer ===================================== --- a/samples/quote.typer +++ b/samples/quote.typer @@ -1,13 +1,3 @@ -% those are name aliases -symbol = lambda (y : String) -> (symbol_ y) ; -string = lambda (y : String) -> (string_ y) ; -integer = lambda (y : Int) -> (integer_ y) ; -float = lambda (y : Float) -> (float_ y) ; -block = lambda (y : List Sexp) -> (block_ y) ; - -quote' : List Sexp -> List Sexp; - - % % f = (qquote (uquote x) * x) (node _*_ [(node_ unquote "x") "x"]) % @@ -16,19 +6,25 @@ quote' : List Sexp -> List Sexp; % % => x
-% the expression needs to be handled -has-uquote : List Sexp -> Sexp; -has-uquote = lambda y -> - head Sexp y; %node_ (symbol_ "node_") (quote' y); +get-head : List Sexp -> Sexp; +get-head x = case x + | cons hd _ => hd + | nil => symbol_ "error";
-% keep quoting the expression -hasnot-uquote : Sexp -> List Sexp -> List Sexp; -hasnot-uquote = lambda op -> - lambda y -> - case y - | nil => node_ op nil - | _ => node_ (quote' (cons op nil)) (quote' y); +symbol = lambda (y : String) -> (symbol_ y); +string = lambda (y : String) -> (string_ y); +integer = lambda (y : Int) -> (integer_ y); +float = lambda (y : Float) -> (float_ y); +block = lambda (y : List Sexp) -> (block_ y);
+quote' : List Sexp -> List Sexp; + +has-uquote : List Sexp -> Sexp; +has-uquote = lambda y -> + let expr = case y + | cons hd tl => hd + | nil => symbol_ "uquote expects one argument" in + expr;
% traverse nodes node : Sexp -> List Sexp -> Sexp; @@ -36,28 +32,62 @@ node = lambda (op : Sexp) -> lambda (y : List Sexp) -> case (sexp_eq op (symbol_ "uquote")) | true => has-uquote y - | false => hasnot-uquote op y; - + | false => node_ op (quote' y);
% tree traversal quote' = lambda (x : List Sexp) -> - let target = head Sexp x; - tl = tail Sexp x; + case x + | cons hd tl => ( + let nhd = sexp_dispatch_ (a := Sexp) hd node symbol string integer float block in + let ntl = quote' tl in + cons nhd ntl)
- rhd = sexp_dispatch_ (a := Sexp) target - node symbol string integer float block; + | nil => nil;
- rtl = case tl - | nil => nil - | _ => quote' tl; +% quote definition +qq = lambda (x : List Sexp) -> get-head (quote' x); +quote = Macro_ qq;
- in (cons rhd rtl); +% Raw +my_sqr = lambda (x : List Sexp) -> + let hd = (case x + | cons hd tl => hd + | nil => symbol_ "x") : Sexp in + (node_ (symbol_ "_*_") (cons hd (cons hd nil)));
+my_add = lambda (x : List Sexp) -> + let hd = (case x + | cons hd tl => hd + | nil => symbol_ "x") : Sexp in + (node_ (symbol_ "_=_") (cons hd (cons hd nil)));
-% quote definition -qq = lambda (x : List Sexp) -> head Sexp (quote' x); -quote = Macro_ qq; +sqr = Macro_ my_sqr; +add = Macro_ my_add; + +my_fun = lambda (arg : List Sexp) -> + let x = sqr 2 in + integer_ 2; + +fun = Macro_ my_fun; +main = fun 2; + + +% Quote +%my_fun = lambda (args : List Sexp) -> +% let hd : Sexp; +% hd = case args +% | cons hd tl => hd +% | nil => symbol_ "sqr expects a single argument" in +% +% quote ((uquote hd) * (uquote hd)); + +x = 2; +sqr = Macro_ my_fun;
-mn = quote (x * x); +% main = sqr 2; +% a = Macro_ (lambda x -> quote (2 + 2));
+% main = a Unit; +% main = let x = 2 in quote (x * x); +% main = let x = 2 in quote ((uquote x) * (uquote x));
===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -454,11 +454,18 @@ and run_io loc depth args_val = -> Sexp *) and sexp_dispatch loc depth args = let eval a b = _eval a b depth in - let sxp, nd, sym, str, it, flt, blk, rctx = match args with - | [sxp; Closure(_, nd, rctx); Closure(_, sym, _); - Closure(_, str, _); Closure(_, it, _); - Closure(_, flt, _); Closure(_, blk, _)] -> - sxp, nd, sym, str, it, flt, blk, rctx + let sxp, nd, ctx_nd, + sym, ctx_sym, + str, ctx_str, + it, ctx_it, + flt, ctx_flt, + blk, ctx_blk = match args with + + | [sxp; Closure(_, nd, ctx_nd); Closure(_, sym, ctx_sym); + Closure(_, str, ctx_str); Closure(_, it, ctx_it); + Closure(_, flt, ctx_flt); Closure(_, blk, ctx_blk)] -> + sxp, nd, ctx_nd, sym, ctx_sym, str, ctx_str, it, ctx_it, + flt, ctx_flt, blk, ctx_blk | _ -> error loc "sexp_dispatch expects 7 arguments" in
let sxp = match sxp with @@ -467,6 +474,7 @@ and sexp_dispatch loc depth args =
match sxp with | Node (op, s) ->( + let rctx = ctx_nd in let rctx = add_rte_variable None (Vsexp(op)) rctx in let rctx = add_rte_variable None (o2v_list s) rctx in match eval nd rctx with @@ -474,16 +482,22 @@ and sexp_dispatch loc depth args = | _ -> error loc "Node has 2 arguments")
| Symbol (_ , s) -> + let rctx = ctx_sym in eval sym (add_rte_variable None (Vstring(s)) rctx) | String (_ , s) -> + let rctx = ctx_str in eval str (add_rte_variable None (Vstring(s)) rctx) | Integer (_ , i) -> + let rctx = ctx_it in eval it (add_rte_variable None (Vint(i)) rctx) | Float (_ , f) -> + let rctx = ctx_flt in eval flt (add_rte_variable None (Vfloat(f)) rctx) (* | Block (_ , s, _) -> eval blk (add_rte_variable None (o2v_list s)) *) - | _ -> error loc "sexp_dispatch error" + | _ -> + print_string "match error\n"; flush stdout; + error loc "sexp_dispatch error"
(* -------------------------------------------------------------------------- *) and print_eval_result i lxp =
View it on GitLab: https://gitlab.com/monnier/typer/compare/411ba805c142bbc2407df977c4e5ea57468...
Afficher les réponses par date