Setepenre pushed to branch master at Stefan / Typer

Commits: 29bde6e0 by Pierre Delaunay at 2016-04-21T17:36:03-04:00 -

Changes to be committed: * new file: samples/BTL.typer (list implementation) * new file: samples/autodiff.typer simple symbolic diff example * src/lparse.ml: - improved lexp_decls (lexp_decls now lexp_p_check when it can) - handle Phas_type - lexp_p_check: handle Plambda - moved macro handling to lexp_p_check * tests/eval_test.ml: - added list test - added necessary type annotations

- - - - -

9 changed files:

- + samples/BTL.typer - + samples/autodiff.typer - src/builtin.ml - src/eval.ml - src/lparse.ml - src/pexp.ml - src/typecheck.ml - tests/eval_test.ml - tests/macro_test.ml

Changes:

===================================== samples/BTL.typer ===================================== --- /dev/null +++ b/samples/BTL.typer @@ -0,0 +1,31 @@ + + +List : Type; +List = inductive_ (dList (a : Type)) (nil) (cons a (List a)); + +nil = inductive-cons List nil; +cons = inductive-cons List cons; + +% length : (a : Type) => List a -> Int; +% length = lambda a => +length : List a -> Int; +length = lambda (xs : List a) -> + case xs + | nil => 0 + | cons hd tl => (1 + length tl); + +% head : (a : Type) => List a -> a; +% head = lambda a => +head : List a -> a; +head = lambda (xs : List a) -> + case xs + | nil => nil + | cons hd tl => hd; + +% tail : (a : Type) => List a -> List a; +% tail = lambda a => +tail : List a -> List a; +tail = lambda (xs : List a) -> + case xs + | nil => nil + | cons hd tl => tl; \ No newline at end of file

===================================== samples/autodiff.typer ===================================== --- /dev/null +++ b/samples/autodiff.typer @@ -0,0 +1,123 @@ +%* +%* Typer Compiler +%* +%* --------------------------------------------------------------------------- +%* +%(* Copyright (C) 2011-2016 Free Software Foundation, Inc. +%* +%* Author: Pierre Delaunay pierre.delaunay@hec.ca +%* Keywords: languages, lisp, dependent types. +%* +%* This file is part of Typer. +%* +%* Typer is free software; you can redistribute it and/or modify it under the +%* terms of the GNU General Public License as published by the Free Software +%* Foundation, either version 3 of the License, or (at your option) any +%* later version. +%* +%* Typer is distributed in the hope that it will be useful, but WITHOUT ANY +%* WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS +%* FOR A PARTICULAR PURPOSE. See the GNU General Public License for +%* more details. +%* +%* You should have received a copy of the GNU General Public License along +%* with this program. If not, see http://www.gnu.org/licenses/. +%* +%* --------------------------------------------------------------------------- +%* +%* Description: +%* Build a very basic symbolic differentiation library +%* +%* Limitations: +%* - Only (add) and (mult) +%* - Only a single unknown +%* - Only Integer operations +%* +%* ---------------------------------------------------------------------------*) + +Sym : Type; +Sym = inductive_ (dSym) + % leafs + (constant Int) + (placeholder String) + + % Nodes + (add Sym Sym) + (mult Sym Sym) + (inv Sym) + (neg Sym); + +constant = inductive-cons Sym constant; +placeholder = inductive-cons Sym placeholder; +add = inductive-cons Sym add; +mult = inductive-cons Sym mult; +inv = inductive-cons Sym inv; +neg = inductive-cons Sym neg; + +div : Sym -> Sym -> Sym; +div = lambda (up : Sym) -> + lambda (down : Sym) -> + (mult up (inv down)); + +sub : Sym -> Sym -> Sym; +sub = lambda (x : Sym) -> + lambda (y : Sym) -> + (add x (neg y)); + +sqr : Sym -> Sym; +sqr = lambda (x : Sym) -> + mult x x; + +zero = constant 0; +one = constant 1; +two = constant 2; + +% p should be even +%pow : Sym -> Int -> Sym; +%pow = lambda *x : Sym) -> lambda (p : Int) -> +% case p +% | 0 -> one +% | 1 -> x +% | _ -> mult (pow x (p / 2)) (pow x (p / 2)); + +eval : Int -> Sym -> Int; +eval = lambda (value : Int) -> + lambda (s : Sym) -> case s + | constant v => v + | placeholder _ => value + | add s1 s2 => ((eval value s1) + (eval value s2)) + | mult s1 s2 => (eval value s1) * (eval value s2); +% | inv s => (1 / (eval value s)) +% | neg s => (- (eval value s)) + +%print : Sym -> Type; +%print = lambda (s : Sym) -> +% case s +% | constant v => to-string v +% | placeholder n => to-string n +% | add s1 s2 => to-string s1 "+" s2 +% | mult s1 s2 => to-string s1 "*" s2; +% | inv s => to-string "1/" s +% | neg s => to-string "-" s; + +deriv : Sym -> Sym; +deriv = lambda (s : Sym) -> + case s + | constant v => zero + | placeholder _ => one + | add s1 s2 => (add (deriv s1) (deriv s2)) + | mult s1 s2 => let ds1 = (deriv s1); ds2 = (deriv s2); in + (add (mult ds1 s2) (mult ds2 s1)); +% | inv s => let up = (deriv s); down = (mult s s); in +% (neg (div up (sqr down))) +% | neg s => (- (deriv s)); + +y = placeholder "y"; +expr = mult y y; % y ^ 2 + +v1 = eval 4 expr; % 16 +main = eval 4 (deriv expr); % 8 + + + +

===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -40,7 +40,6 @@ open Debruijn open Env (* get_rte_variable *)

- let builtin_error loc msg = msg_error "BUILT-IN" loc msg; raise (internal_error msg) @@ -115,12 +114,14 @@ let _generic_binary_iop name f loc (args_val: value_type list) (ctx: runtime_env (* i.e we don't need to push x and y in the context. *) (* We don't even need the context *) let l, r = match args_val with - | [a; b] -> (get_int a), (get_int b) + | [a; b] -> a, b | _ -> builtin_error loc (name ^ " expects 2 arguments") in

- match l, r with + match (get_int l), (get_int r) with | Some v, Some w -> Value(Imm(Integer (loc, (f v w)))) - | _ -> builtin_error loc (name ^ " expects Integers as arguments") + | _ -> + value_print l; print_string " "; value_print r; + builtin_error loc (name ^ " expects Integers as arguments") ;;

let iadd_impl = _generic_binary_iop "Integer::add" (fun a b -> a + b) @@ -128,6 +129,13 @@ let isub_impl = _generic_binary_iop "Integer::sub" (fun a b -> a - b) let imult_impl = _generic_binary_iop "Integer::mult" (fun a b -> a * b) let idiv_impl = _generic_binary_iop "Integer::div" (fun a b -> a / b)

+(* +let eq_impl loc args_val ctx = + let l, r = match args_val with + | [a; b] -> a, b + | _ -> builtin_error loc "_=_ expects 2 arguments") in + + conv_p l r *)

(* loc is given by the compiler *) let none_fun = (fun loc args_val ctx -> @@ -197,10 +205,11 @@ let builtin_expand = Builtin (SexpType, "expand_", type_mexpand) (* Built-in list of types/functions *) (* Some of the information is redundant but it suppress a lot of warnings *) let typer_builtins = [ -(* NAME | LXP | Type | impl *) - ("Type" , type0 , type0, none_fun); - ("Int" , type_int , type0, none_fun); - ("Float", type_float, type0, none_fun); +(* NAME | LXP | Type | impl *) + ("Type" , type0 , type0, none_fun); + ("Int" , type_int , type0, none_fun); + ("Float" , type_float , type0, none_fun); + ("String", type_string, type0, none_fun);

(* Built-in Functions *) ("_=_" , builtin_eq, type_eq, none_fun); (* t -> t -> bool *)

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -127,8 +127,9 @@ and eval_call ctx i lname args call = (* first lambda *) | Value (lxp), hd::tl -> (match lxp with | Cons _ -> - let cons_args = List.map (fun g -> (Aexplicit, (get_value_lexp g))) args_val in - Value(Call(lname, (cons_args))) + let cons_args = List.map (fun g -> + (Aexplicit, (get_value_lexp g))) args_val in + Value(Call(lname, (cons_args))) | _ -> (* Push first arg *) let nctx = add_rte_variable None hd ctx in

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -117,8 +117,8 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = | Pimm value -> (Imm(value), match value with | Integer _ -> type_int - | Float _ -> type_float - | String _ -> lexp_error tloc "Could not find String"; dltype; + | Float _ -> type_float + | String _ -> type_string; | _ -> lexp_error tloc "Could not find type"; pexp_print p; print_string "\n"; dltype)

@@ -156,17 +156,27 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = v, type0

(* Pinductive *) - | Pinductive (label, [], ctors) -> + | Pinductive (label, formal_args, ctors) -> + let ctx = ref ctx in + (* (arg_kind * pvar * pexp option) list *) + let formal = List.map (fun (kind, var, opxp) -> + let ltp, _ = match opxp with + | Some pxp -> _lexp_p_infer pxp !ctx (i + 1) + | None -> dltype, dltype in + + ctx := env_extend !ctx var None dltype; + (kind, var, ltp) + ) formal_args in + (* (arg_kind * vdef * ltype) list *) + + let ctx = !ctx in let map_ctor = lexp_parse_inductive ctors ctx i in - let v = Inductive(tloc, label, [], map_ctor) in + let v = Inductive(tloc, label, formal, map_ctor) in v, type0

- (* *) - - | Plambda (kind, var, ptype, body) -> - let ltp, _ = match ptype with - | None -> dltype, dltype - | Some pt -> lexp_infer pt ctx in + (* This case can be inferred *) + | Plambda (kind, var, Some ptype, body) -> + let ltp, _ = lexp_infer ptype ctx in

let nctx = env_extend ctx var None ltp in let lbody, lbtp = lexp_infer body nctx in @@ -261,7 +271,12 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype =

Case(loc, tlxp, tltp, lpattern, dflt), (return_type)

- | _ -> lexp_fatal tloc "Unhandled Pexp" + | Phastype (_, pxp, ptp) -> + let ltp, _ = lexp_infer ptp ctx in + (_lexp_p_check pxp ltp ctx (i + 1)), ltp + + | _ -> pexp_print p; print_string "\n"; + lexp_fatal tloc "Unhandled Pexp"

and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = let tloc = pexp_location p in @@ -270,6 +285,35 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = _global_lexp_trace := (i, tloc, p)::!_global_lexp_trace;

match p with + (* This case cannot be inferred *) + | Plambda (kind, var, None, body) -> + (* Read var type from the provided type *) + let ltp, lbtp = match t with + | Arrow(kind, None, ltp, _, lbtp) -> ltp, lbtp + | _ -> lexp_error tloc "Type does not match"; dltype, dltype in + + let nctx = env_extend ctx var None ltp in + let lbody = _lexp_p_check body lbtp nctx (i + 1) in + + Lambda(kind, var, ltp, lbody) + + | Pcall (Pvar(_, "expand_"), _args) ->( + let pargs = List.map pexp_parse _args in + let largs = _lexp_parse_all pargs ctx i in + + let lxp = match largs with + | [lxp] -> lxp + | hd::tl -> lexp_error tloc "expand_ expects one lexp"; hd + | _ -> lexp_fatal tloc "expand_ expects one lexp" in + + (* eval argument *) + let sxp = match eval lxp (from_lctx ctx) with + | Vsexp(sxp) -> sxp + | _ -> lexp_fatal tloc "expand_ expects sexp" in + + let pxp = pexp_parse sxp in + _lexp_p_check pxp t ctx (i + 1)) + | _ -> let (e, inferred_t) = _lexp_p_infer p ctx (i + 1) in (* FIXME: check that inferred_t = t! *) e @@ -323,19 +367,9 @@ and lexp_call (fname: pexp) (_args: sexp list) ctx i = Call(vf, new_args), ret_type

(* Is it a macro ? *) - | Some Builtin (_, "expand_", _) ->( - let lxp = match largs with - | [lxp] -> lxp - | hd::tl -> lexp_error loc "expand_ one lexp"; hd - | _ -> lexp_fatal loc "expand_ one lexp" in - - (* eval argument *) - let sxp = match eval lxp (from_lctx ctx) with - | Vsexp(sxp) -> sxp - | _ -> lexp_fatal loc "expand_ expects sexp" in - - let pxp = pexp_parse sxp in - lexp_p_infer pxp ctx) + | Some Builtin (_, "expand_", _) -> + lexp_error loc "expand_ require type annotation"; + dltype, dltype

(* a builtin functions *) | Some e -> Call(e, new_args), ret_type @@ -499,40 +533,22 @@ and _lexp_decls decls ctx i: (((vdef * lexp * ltype) list) * lexp_context) = let rec merge_decls (decls: (pvar * pexp * bool) list) merged acc: ((location * pexp option * pexp option * int) SMap.t * string list) =

- (* we cant evaluate here because variable are not in the environment *) + (* we cant evaluate here because variables are not in the environment *) match decls with | [] -> merged, (List.rev acc) - | hd::tl -> - match hd with - (* Type Info: Var:Type *) - | ((loc, name), type_info, true) -> begin - try let (l, inst, _, i) = SMap.find name merged in - let new_decl = (l, inst, Some type_info, i) in - let nmerged = SMap.add name new_decl merged in - (merge_decls tl nmerged acc) - + | ((loc, name), pxp, bl)::tl -> + let (l, opxp, optp, i), acc = try (SMap.find name merged), acc with Not_found -> - (* add variable to ctx *) - let new_decl = (loc, None, Some type_info, !idx) in - let nmerged = SMap.add name new_decl merged in - idx := !idx + 1; - ctx := env_extend (!ctx) (loc, name) None dltype; - (merge_decls tl nmerged (name::acc)) end - - (* Instruction: Var = expr *) - | ((loc, name), inst, false) -> begin - try let (l, _, tp, i) = SMap.find name merged in - let new_decl = (l, Some inst, tp, i) in - let nmerged = SMap.add name new_decl merged in - (merge_decls tl nmerged acc) + idx := !idx + 1; + ctx := env_extend (!ctx) (loc, name) None dltype; + (loc, None, None, !idx - 1), (name::acc) in

- with Not_found -> - (* add variable to ctx *) - let new_decl = (loc, Some inst, None, !idx) in - let nmerged = SMap.add name new_decl merged in - idx := !idx + 1; - ctx := env_extend (!ctx) (loc, name) None dltype; - (merge_decls tl nmerged (name::acc)) end in + let new_decl = match bl with + | true -> (l, opxp, Some pxp, i) + | false -> (l, Some pxp, optp, i) in + + let nmerged = SMap.add name new_decl merged in + (merge_decls tl nmerged acc) in

let mdecls, ord = merge_decls decls SMap.empty [] in

@@ -572,9 +588,9 @@ and _lexp_decls decls ctx i: (((vdef * lexp * ltype) list) * lexp_context) = n := !n - 1;

match opxp, otpxp with - | Some pxp, Some _ -> + | Some pxp, Some ptp -> let ltp = env_lookup_type ctx vref in - let lxp, _ = _lexp_p_infer pxp ctx (i + 1) in + let lxp = _lexp_p_check pxp ltp ctx (i + 1) in (env_set_var_info ctx vref (Some lxp) ltp); lst := (vdef, lxp, ltp)::!lst

===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -187,6 +187,10 @@ and pexp_p_actual_arg arg : (arg_kind * pvar option * pexp) = | e -> (Aexplicit, None, pexp_parse e)

and pexp_p_formal_arg arg : (arg_kind * pvar * pexp option) = + (* FYI: None of the formal arg type work *) + (* (a ::: Type) -> (a ::: Type) instead of (::: a Type) + * (a :: Type) -> (a :: Type) instead of (:: a Type) + * (a : Type) -> (_:_ a Type) instead of (_:_ a Type) *) match arg with | Node (Symbol (_, ":::"), [Symbol s; e]) -> (Aerasable, s, Some (pexp_parse e)) @@ -194,8 +198,13 @@ and pexp_p_formal_arg arg : (arg_kind * pvar * pexp option) = -> (Aimplicit, s, Some (pexp_parse e)) | Node (Symbol (_, ":"), [Symbol s; e]) -> (Aexplicit, s, Some (pexp_parse e)) + (* ------ FIXME: temp FIX ------ *) + | Node (Symbol (_, "_:_"), [Symbol s; e]) + -> (Aexplicit, s, Some (pexp_parse e)) + (* ------ --------------- ------ *) | Symbol s -> (Aexplicit, s, None) - | _ -> (pexp_error (sexp_location arg) "Unrecognized formal arg"); + | _ -> sexp_print arg; + (pexp_error (sexp_location arg) "Unrecognized formal arg"); (Aexplicit, (sexp_location arg, "{arg}"), None)

and pexp_u_formal_arg (arg : arg_kind * pvar * pexp option) =

===================================== src/typecheck.ml ===================================== --- a/src/typecheck.ml +++ b/src/typecheck.ml @@ -28,7 +28,7 @@ open Sexp (* open Myers *) (* open Grammar *) open Lexp -open Builtin (* type_float *) + (* open Unify *) module S = Subst module L = List @@ -174,7 +174,7 @@ let rec unsusp e s = (* Push a suspension one level down. *) | Some e -> Some (mkSusp e s))

(********* Testing if a lexp is properly typed *********) - + type varbind = | Variable | ForwardRef @@ -288,4 +288,4 @@ let rec check ctx e = (* FIXME: If there are no branches nor default, then we have no * way to infer the type! *) (* FIXME: Check branches and default! *) - +

===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -97,8 +97,13 @@ let _ = (add_test "EVAL" "Let" (fun () -> let _ = (add_test "EVAL" "Lambda" (fun () -> reset_eval_trace ();

+ let dcode = " + sqr : Int -> Int; + sqr = lambda x -> x * x; + " in + (* Declare lambda *) - let rctx, lctx = eval_decl_str "sqr = lambda x -> x * x;" lctx rctx in + let rctx, lctx = eval_decl_str dcode lctx rctx in

(* Eval defined lambda *) let ret = eval_expr_str "(sqr 4);" lctx rctx in @@ -113,7 +118,10 @@ let _ = (add_test "EVAL" "Nested Lambda" (fun () -> reset_eval_trace ();

let code = " + sqr : Int -> Int; sqr = lambda x -> x * x; + + cube : Int -> Int; cube = lambda x -> x * (sqr x);" in

(* Declare lambda *) @@ -204,9 +212,9 @@ let nat_decl = " zero = inductive-cons Nat zero; succ = inductive-cons Nat succ;

- tonum : Nat -> Int; - tonum = lambda (x : Nat) -> case x - | (succ y) => (1 + (tonum y)) + to-num : Nat -> Int; + to-num = lambda (x : Nat) -> case x + | (succ y) => (1 + (to-num y)) | zero => 0;" ;;

@@ -226,7 +234,7 @@ let _ = (add_test "EVAL" "Inductive::Recursive Call" (fun () ->

let rctx, lctx = eval_decl_str code lctx rctx in

- let rcode = "(tonum zero); (tonum one); (tonum two);"in + let rcode = "(to-num zero); (to-num one); (to-num two);"in

(* Eval defined lambda *) let ret = eval_expr_str rcode lctx rctx in @@ -261,9 +269,9 @@ let _ = (add_test "EVAL" "Inductive::Nat Plus" (fun () -> let rctx, lctx = eval_decl_str code lctx rctx in

let rcode = " - (tonum (plus zero two)); - (tonum (plus two zero)); - (tonum (plus two one));"in + (to-num (plus zero two)); + (to-num (plus two zero)); + (to-num (plus two one));"in

(* Eval defined lambda *) let ret = eval_expr_str rcode lctx rctx in @@ -348,19 +356,66 @@ let _ = (add_test "EVAL" "Partial Application" (fun () -> | _ -> failure () ));;

-(* + +let list_decl = " +List : Type; List = inductive_ (dList (a : Type)) (nil) (cons a (List a));

nil = inductive-cons List nil; cons = inductive-cons List cons;

-length : (a : Type) => List a -> Nat; -length = lambda a => lambda (xs : List a) -> +% length : (a : Type) => List a -> Int; +% length = lambda a => +length : List a -> Int; +length = lambda (xs : List a) -> case xs - | nil => zero - | cons x xs => succ (length xs); -*) + | nil => 0 + | cons hd tl => (1 + length tl); + +% head : (a : Type) => List a -> a; +% head = lambda a => +head : List a -> a; +head = lambda (xs : List a) -> + case xs + | nil => nil + | cons hd tl => hd; + +% tail : (a : Type) => List a -> List a; +% tail = lambda a => +tail : List a -> List a; +tail = lambda (xs : List a) -> + case xs + | nil => nil + | cons hd tl => tl; +";; + +let _ = (add_test "EVAL" "List" (fun () -> + reset_eval_trace (); + + let dcode = list_decl ^ " + my_list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + " in + + let rctx, lctx = eval_decl_str dcode lctx rctx in + + let rcode = "(length my_list); + (head my_list); + (head (tail my_list));" in

+ (* Eval defined lambda *) + let ret = eval_expr_str rcode lctx rctx in + (* Expect a 3 results *) + match ret with + | [a; b; c] -> + let t1 = expect_equal_int (get_int a) 4 in + let t2 = expect_equal_int (get_int b) 1 in + let t3 = expect_equal_int (get_int c) 2 in + if t1 = 0 && t2 = 0 && t3 = 0 then + success () + else + failure () + | _ -> failure () +));;

(* run all tests *)

===================================== tests/macro_test.ml ===================================== --- a/tests/macro_test.ml +++ b/tests/macro_test.ml @@ -57,6 +57,7 @@ let _ = (add_test "MACROS" "macros base" (fun () -> sqr_sexp = (node_ (symbol_ "lambda_->_") (symbol_ "x") (node_ (symbol_ "_*_") (symbol_ "x") (symbol_ "x")));

+ sqr : Int -> Int; sqr = (expand_ sqr_sexp);" in

let rctx, lctx = eval_decl_str dcode lctx rctx in

View it on GitLab: https://gitlab.com/monnier/typer/commit/29bde6e0d32025100113463a0516a45e48ce...