Setepenre pushed to branch master at Stefan / Typer

Commits: acbe9589 by Pierre Delaunay at 2016-04-17T20:09:54-04:00 minor changes

- - - - - 66678b3b by Pierre Delaunay at 2016-04-18T10:42:21-04:00 Merge branch 'master' of https://gitlab.com/monnier/typer

- - - - - f1ee2eb8 by Pierre Delaunay at 2016-04-19T12:40:55-04:00 new implementations lexp_p_decls

Changes to be committed: * src/lparse.ml: - added type of types - added a new implementation of lexp_p_decls but commented it out as it requires handling shifting

- - - - - 6a2ba53d by Pierre Delaunay at 2016-04-19T15:12:23-04:00 Merge branch 'master' of https://gitlab.com/monnier/typer

- - - - - de90e983 by Pierre Delaunay at 2016-04-20T02:46:34-04:00 Added macro handling in lparse.ml

Changes to be committed: * src/builtin.ml: added (expand_) * src/eval.ml: new function (from_lctx) * src/lparse.ml: handle the macro case in lexp_call

- - - - -

8 changed files:

- GNUmakefile - src/builtin.ml - src/debruijn.ml - src/env.ml - src/eval.ml - src/lparse.ml - src/subst.ml - tests/macro_test.ml

Changes:

===================================== GNUmakefile ===================================== --- a/GNUmakefile +++ b/GNUmakefile @@ -78,3 +78,6 @@ run/ityper:

run/tests: @./_build/tests/utests --verbose= 1 + +run/ityper-file: + @./_build/ityper ./samples/test__.typer

===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -75,9 +75,11 @@ let type_eq = let lv = (dloc, "l") in Arrow (Aexplicit, None, Var (tv, 1), dloc, type0))))

-let builtin_iadd = Builtin (IAdd, "_+_", iop_binary) +let builtin_iadd = Builtin (IAdd, "_+_", iop_binary) let builtin_imult = Builtin (IMult, "_*_", iop_binary) -let builtin_eq = Builtin (EqType, "_=_", type_eq) (* +let builtin_eq = Builtin (EqType, "_=_", type_eq) +let builtin_sexp = Builtin (SexpType, "sexp", type0) +(* let builtin_fadd = Builtin (FAdd, "_+_", fop_binary) let builtin_fmult = Builtin (FMult, "_*_", fop_binary) *)

@@ -135,12 +137,12 @@ let make_symbol loc args_val ctx = (* symbol is a simple string *) let lxp = match args_val with | [r] -> r - | _ -> builtin_error loc ("symbol_ expects 1 arguments") in + | _ -> builtin_error loc ("symbol_ expects 1 argument") in

let s = get_string lxp in match s with | Some str -> Vsexp(Symbol(loc, str)) - | _ -> builtin_error loc ("symbol_ expects sexp as arguments") + | _ -> builtin_error loc ("symbol_ expects one string as argument")

let make_node loc args_val ctx = @@ -159,17 +161,29 @@ let make_node loc args_val ctx =

Vsexp(Node(op, s))

+ let make_block loc args_val ctx = Value(type0) let make_string loc args_val ctx = Value(type0) let make_integer loc args_val ctx = Value(type0) let make_float loc args_val ctx = Value(type0)

-let builtin_block = Builtin (SexpType, "block_", type0) -let builtin_symbol = Builtin (SexpType, "symbol_", type0) -let builtin_string = Builtin (SexpType, "string_", type0) -let builtin_integer = Builtin (SexpType, "integer_", type0) -let builtin_float = Builtin (SexpType, "float_", type0) -let builtin_node = Builtin (SexpType, "node_", type0) +let type_string = type0 +let type_mblock = type0 + +let type_msymbol = Arrow (Aexplicit, None, type_string, dloc, builtin_sexp) +let type_mstring = Arrow (Aexplicit, None, type_string, dloc, builtin_sexp) +let type_minteger = Arrow (Aexplicit, None, type_int, dloc, builtin_sexp) +let type_mfloat = Arrow (Aexplicit, None, type_float, dloc, builtin_sexp) +let type_mnode = Arrow (Aexplicit, None, builtin_sexp,dloc, builtin_sexp) +let type_mexpand = Arrow (Aexplicit, None, builtin_sexp,dloc, type0) + +let builtin_block = Builtin (SexpType, "block_", type_mblock) +let builtin_symbol = Builtin (SexpType, "symbol_", type_msymbol) +let builtin_string = Builtin (SexpType, "string_", type_mstring) +let builtin_integer = Builtin (SexpType, "integer_", type_minteger) +let builtin_float = Builtin (SexpType, "float_", type_mfloat) +let builtin_node = Builtin (SexpType, "node_", type_mnode) +let builtin_expand = Builtin (SexpType, "expand_", type_mexpand)

(* * Should we have a function that @@ -194,12 +208,13 @@ let typer_builtins = [ ("_*_" , builtin_imult, iop_binary, imult_impl); (* int -> int -> int *)

(* Macro primitives *) - ("block_" , builtin_block , type0, make_block); - ("symbol_" , builtin_symbol , type0, make_symbol); - ("string_" , builtin_string , type0, make_string); - ("integer_", builtin_integer, type0, make_integer); - ("float_" , builtin_float , type0, make_float); - ("node_" , builtin_node , type0, make_node); + ("block_" , builtin_block , type_mblock , make_block); + ("symbol_" , builtin_symbol , type_msymbol , make_symbol); + ("string_" , builtin_string , type_mstring , make_string); + ("integer_", builtin_integer, type_minteger, make_integer); + ("float_" , builtin_float , type_mfloat , make_float); + ("node_" , builtin_node , type_mnode , make_node); + ("expand_" , builtin_expand , type_mexpand , none_fun);

(* Macros primitives type ? *)

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -122,7 +122,8 @@ let env_add_var_info var (ctx: lexp_context) = (a, cons (ref var) env, f)

let env_extend (ctx: lexp_context) (def: vdef) (v: lexp option) (t: lexp) = - env_add_var_info (0, def, v, t) (senv_add_var def ctx) + let ((n, map), e, f) = ctx in + env_add_var_info (n, def, v, t) (senv_add_var def ctx)

let _name_error loc estr str =

===================================== src/env.ml ===================================== --- a/src/env.ml +++ b/src/env.ml @@ -37,7 +37,7 @@ open Sexp open Lexp (* lexp_print *)

open Myers - +open Debruijn

let dloc = dummy_location @@ -55,6 +55,8 @@ type value_type = | Closure of lexp * (((string option * value_type) ref myers) * (int * int)) (* Macro type *) | Vsexp of sexp + (* Unable to eval during macro expansion, only throw if the value is used *) + | Vdummy

let get_value_lexp (vtp: value_type) = match vtp with @@ -65,9 +67,10 @@ let get_value_lexp (vtp: value_type) = let value_print (vtp: value_type) = match vtp with | Closure (lxp, _) -> - print_string ("Closure(" ^ (_lexp_to_str (!debug_ppctx) lxp)) + print_string ("Closure(" ^ (_lexp_to_str (!debug_ppctx) lxp) ^ ")") | Value s -> lexp_print s | Vsexp sxp -> sexp_print sxp + | _ -> print_string "value_print_dummy"

let value_location (vtp: value_type) = lexp_location (get_value_lexp vtp) @@ -108,6 +111,16 @@ let get_rte_variable (name: string option) (idx: int) (ctx: runtime_env): value_ n ^ "" idx: " ^ (str_idx idx)) ;;

+let rte_shift vref ctx = + let (_, (osize, _)) = ctx in (* number of variable declared outside *) + let csize = get_rte_size ctx in (* current size *) + let offset = csize - osize in + let ((loc, name), idx) = vref in + (* check if variable is free *) + let offset = if idx > offset then offset else 0 in + (* shift idx *) + idx + offset + let add_rte_variable name (x: value_type) (ctx: runtime_env): runtime_env = let (l, b) = ctx in let lst = (cons (ref (name, x)) l) in @@ -198,3 +211,4 @@ let print_rte_ctx (ctx: runtime_env) =

value_print g; print_string "\n") ;; +

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -105,11 +105,12 @@ let rec _eval lxp ctx i: (value_type) = (* Case *) | Case (loc, target, _, pat, dflt) -> (eval_case ctx i loc target pat dflt)

- | _ -> lexp_print lxp; Value(Imm(String(dloc, "eval Not Implemented"))) + | _ -> print_string "debug catch-all eval: "; + lexp_print lxp; Value(Imm(String(dloc, "eval Not Implemented")))

and eval_var ctx lxp v = let ((loc, name), idx) = v in - try get_rte_variable (Some name) idx ctx + try get_rte_variable (Some name) (idx) ctx with Not_found -> eval_error loc ("Variable: " ^ name ^ (str_idx idx) ^ " was not found ")

@@ -283,7 +284,7 @@ and _eval_decls (decls: ((vdef * lexp * ltype) list))

(* Read declarations once and push them *) let _, ctx = List.fold_left (fun (idx, ctx) ((_, name), lxp, ltp) -> - _global_eval_trace := []; + let lxp = _eval lxp ctx (i + 1) in let ctx = set_rte_variable idx (Some name) lxp ctx in (idx - 1, ctx)) @@ -303,7 +304,6 @@ and print_eval_trace () = ;;

let eval lxp ctx = - _global_eval_trace := []; _eval lxp ctx 1

let debug_eval lxp ctx = @@ -321,3 +321,27 @@ let eval_all lxps rctx silent = List.map (fun g -> evalfun g rctx) lxps;;

+(* build a rctx from a lctx *) +let from_lctx (ctx: lexp_context): runtime_env = + let ((_, _), env, _) = ctx in + let rctx = ref (default_rctx ()) in + + (* Skip builtins *) + let bsize = List.length typer_builtins in + let csize = get_size ctx in + + for i = bsize to csize do + let (_, (_, name), exp, _) = !(Myers.nth (csize - i) env) in + + let vxp = match exp with + | Some lxp -> (eval lxp !rctx) + | None -> Vdummy in + + rctx := add_rte_variable (Some name) vxp (!rctx) + done; + + !rctx + + + +

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -38,6 +38,7 @@ open Sexp open Pexp open Lexp

+open Env open Debruijn open Eval

@@ -141,19 +142,26 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = let bdy, ltp = lexp_infer body nctx in Let(tloc, decl, bdy), ltp

- (* ->/=> *) + (* ------------------------------------------------------------------ *) | Parrow (kind, Some var, tp, loc, expr) -> - let nvar = var in (* /!\ HERE *) let ltyp, _ = lexp_infer tp ctx in let lxp, _ = lexp_infer expr ctx in - let v = Arrow(kind, Some nvar, ltyp, tloc, lxp) in - v, v + let v = Arrow(kind, Some var, ltyp, tloc, lxp) in + v, type0

| Parrow (kind, None, tp, loc, expr) -> let ltyp, _ = lexp_infer tp ctx in let lxp, _ = lexp_infer expr ctx in let v = Arrow(kind, None, ltyp, tloc, lxp) in - v, v + v, type0 + + (* Pinductive *) + | Pinductive (label, [], ctors) -> + let map_ctor = lexp_parse_inductive ctors ctx i in + let v = Inductive(tloc, label, [], map_ctor) in + v, type0 + + (* *)

| Plambda (kind, var, ptype, body) -> let ltp, _ = match ptype with @@ -169,12 +177,6 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = | Pcall (fname, _args) -> lexp_call fname _args ctx i

- (* Pinductive *) - | Pinductive (label, [], ctors) -> - let map_ctor = lexp_parse_inductive ctors ctx i in - let v = Inductive(tloc, label, [], map_ctor) in - v, v - (* Pcons *) | Pcons(vr, sym) -> ( let (loc, type_name) = vr in @@ -183,14 +185,14 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = (* An inductive type named type_name must be in the environment *) try let idx = senv_lookup type_name ctx in (* Check if the constructor exists *) - let idt = env_lookup_type ctx (vr, idx) in + let idt = env_lookup_expr ctx (vr, idx) in

(* make Base type *) let inductive_type = Var((loc, type_name), idx) in

(* Get constructor args *) let args = match idt with - | Inductive(_, _, _, ctor_def) -> ( + | Some Inductive(_, _, _, ctor_def) -> ( try (SMap.find cname ctor_def) with Not_found -> lexp_error loc @@ -261,7 +263,7 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype =

| _ -> lexp_fatal tloc "Unhandled Pexp"

-and lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = +and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = let tloc = pexp_location p in

_global_lexp_ctx := ctx; @@ -319,6 +321,23 @@ and lexp_call (fname: pexp) (_args: sexp list) ctx i = match env_lookup_expr ctx ((loc, name), idx) with | None -> lexp_error loc "Unknown builtin"; 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) + + (* a builtin functions *) | Some e -> Call(e, new_args), ret_type ) else Call(vf, new_args), ret_type @@ -415,6 +434,62 @@ and lexp_parse_inductive ctors ctx i = (* Parse let declaration *) and lexp_p_decls decls ctx = _lexp_decls decls ctx 1 and _lexp_decls decls ctx i: (((vdef * lexp * ltype) list) * lexp_context) = + (* (pvar * pexp * bool) list * ) + + let ctx = ref ctx in + let mdecls = ref SMap.empty in + let order = ref [] in + let found = ref false in + + List.iter (fun ((loc, name), pxp, bl) -> + (* Check if variable was already defined *) + let (l, olxp, oltp, _) = try found := true; SMap.find name !mdecls + with Not_found -> + (* keep track of declaration order *) + order := (name::!order); + found := false; + (* create an empty element *) + (loc, None, None, 0) in + + (* create a dummy env for lexp_parse *) + let denv = env_extend (!ctx) (loc, name) None dltype in + + (* Do we already have a type ? *) + let lxp, ltp = match oltp with + (* We infer *) + | None -> _lexp_p_infer pxp denv (i + 1) + + (* We check *) + | Some ltp -> (_lexp_p_check pxp ltp denv (i + 1)), ltp in + + (* update declaration *) + (* FIXME: modify env when lxp is found *) + let new_decl = match bl with + | true -> (if !found then () else ctx := env_extend (!ctx) (loc, name) None lxp); + (l, olxp, Some lxp, i) + | false -> (if !found then () else ctx := env_extend (!ctx) (loc, name) (Some lxp) ltp); + (l, Some lxp, oltp, i) in + + (* Add Variable to the map *) + mdecls := SMap.add name new_decl !mdecls) + + decls; + + let ctx = !ctx in + let mdecls = !mdecls in + let order = !order in + (* Cast Map to list *) + let ndecls = List.map (fun name -> + let (l, inst, tp, _) = SMap.find name mdecls in + match inst, tp with + | Some lxp, Some ltp -> ((l, name), lxp, ltp) + | Some lxp, None -> ((l, name), lxp, dltype) + | None, Some ltp -> lexp_warning l "Type with no expression"; + ((l, name), dltype, ltp) + | None, None -> lexp_warning l "No expression, No Type"; + ((l, name), dltype, dltype)) order in + + (List.rev ndecls), ctx *)

let ctx = ref ctx in let idx = ref 0 in @@ -469,35 +544,52 @@ and _lexp_decls decls ctx i: (((vdef * lexp * ltype) list) * lexp_context) = (* This is required for later *) let ctx = !ctx in let lst = ref [] in - let n = ref ((List.length ndecls) - 1) in - (* for each declaration lexp their rhs *) - List.iter (fun ((loc, name), opxp, otpxp) -> - let vdef = (loc, name) in - let vref = (vdef, !n) in - n := !n - 1; - - match opxp, otpxp with - | Some pxp, Some tpxp -> - (* Add type first (for recursive definition) *) - let ltp, _ = _lexp_p_infer tpxp ctx (i + 1) in - (env_set_var_info ctx vref None ltp);

- let lxp, _ = _lexp_p_infer pxp ctx (i + 1) in - (env_set_var_info ctx vref (Some lxp) ltp); + (* Doing types and expressions separately allow us to use *) + (* all typing information when lexp_parsing recursive definition *) + (* The price of this is iterating twice over declarations *) + (* + now we need to lookup type info *)

- lst := (vdef, lxp, ltp)::!lst - - | Some pxp, None -> - let lxp, ltp = _lexp_p_infer pxp ctx (i + 1) in - (env_set_var_info ctx vref (Some lxp) ltp); - lst := (vdef, lxp, ltp)::!lst + (* Process types once *) + let n = ref ((List.length ndecls) - 1) in + (* for each declaration lexp their types *) + List.iter (fun ((loc, name), opxp, otpxp) -> + let vdef = (loc, name) in + let vref = (vdef, !n) in + n := !n - 1; + + match opxp, otpxp with + | _, Some tpxp -> let ltp, _ = _lexp_p_infer tpxp ctx (i + 1) in + (env_set_var_info ctx vref None ltp); + | _ -> ()) + ndecls;

- | None, _ -> lexp_warning loc "Unused Variable" + (* Process declaration in itself*) + let n = ref ((List.length ndecls) - 1) in + List.iter (fun ((loc, name), opxp, otpxp) -> + let vdef = (loc, name) in + let vref = (vdef, !n) in + n := !n - 1; + + match opxp, otpxp with + | Some pxp, Some _ -> + let ltp = env_lookup_type ctx vref in + let lxp, _ = _lexp_p_infer pxp ctx (i + 1) in + (env_set_var_info ctx vref (Some lxp) ltp); + lst := (vdef, lxp, ltp)::!lst + + | Some pxp, None -> + let lxp, ltp = _lexp_p_infer pxp ctx (i + 1) in + (env_set_var_info ctx vref (Some lxp) ltp); + lst := (vdef, lxp, ltp)::!lst + + | None, _ -> lexp_warning loc "Unused Variable" ) ndecls;

List.rev (!lst), ctx

+ and _lexp_parse_all (p: pexp list) (ctx: lexp_context) i : lexp list =

let rec loop (plst: pexp list) ctx (acc: lexp list) = @@ -640,4 +732,4 @@ let eval_expr_str str lctx rctx = _eval_expr_str str lctx rctx false let eval_decl_str str lctx rctx = let lxps, lctx = lexp_decl_str str lctx in (eval_decls lxps rctx), lctx -;; \ No newline at end of file +;;

===================================== src/subst.ml ===================================== --- a/src/subst.ml +++ b/src/subst.ml @@ -21,6 +21,40 @@ this program. If not, see http://www.gnu.org/licenses/. *)

module U = Util

+ +(* Suspensions definitions. + * + * ol: old embedding level ('associate' level, length with environement) + * nl: new .... + * + * n: A Natural Number + * i: A positive integer + * + * t ::= c : + * #i : Debruijn Index variable bound by the ith abstraction + * (t, t) : Applications + * (λ t) : Abstractions + * [t, n, n, e] : Suspensions + * + * length level + * e ::= nil : 0 : 0 + * (t, n)::e : n + len(e) : n + * {e1, nl, ol, e2} : len(e1) + len(e2) - nl : lev(e1) + nl - ol + * + * level is the dbi index ? + * + * Substitutions Compositions definitions. + * + * a ::= 1 + * a b + * (λ a) : + * a[s] : + * + * s ::= id : identity + * a . s : cons replace dbi_idx = 0 by a use s for the rest + * s o t : Composition + * shift : dbi_index + 1 + *) (* Substitutions. * * There are many different ways to implement a calculus with explicit @@ -40,7 +74,7 @@ module U = Util * The normal beta rule is: * * (λ t₁) t₂ ==> [t₁, 1, 0, (t₂,0) :: nil] - * + * * which would be instantiated to * * (λ [t₁, ol, nl, e]) t₂ ==> [[t₁, ol, nl, e], 1, 0, (t₂,0) :: nil] @@ -168,7 +202,7 @@ type db_offset = int (* DeBruijn index offset. *) * In practice, 'a is always lexp, but we keep it as a paramter: * - for better modularity of the code. * - to break a mutual dependency between the Lexp and the Subst modules. *) -type 'a subst = +type 'a subst = (* lexp subst *) (* Lift (n,m) increases indices≥N by M. * IOW, it takes variables from a source context Δₛ₁Δₛ₂ to a destination * context Δₛ₁ΔₜΔₛ₂ where Δₛ₂ has size N and Δₜ has size M. *)

===================================== tests/macro_test.ml ===================================== --- a/tests/macro_test.ml +++ b/tests/macro_test.ml @@ -54,17 +54,19 @@ let _ = (add_test "MACROS" "macros base" (fun () ->

(* define 'lambda x -> x * x' using macros *) let dcode = " - sqrt_sexp = (node_ (symbol_ "lambda_->_") (symbol_ "x") - (node_ (symbol_ "_*_") (symbol_ "x") (symbol_ "x"))); " in + sqr_sexp = (node_ (symbol_ "lambda_->_") (symbol_ "x") + (node_ (symbol_ "_*_") (symbol_ "x") (symbol_ "x"))); + + sqr = (expand_ sqr_sexp);" in

let rctx, lctx = eval_decl_str dcode lctx rctx in

- let ecode = "(sqrt_sexp);" in + let ecode = "(sqr 3);" in

let ret = eval_expr_str ecode lctx rctx in

match ret with - | [r] -> value_print r; print_string "\n"; success (); + | [r] -> expect_equal_int (get_int r) (3 * 3) | _ -> failure ()) );;

View it on GitLab: https://gitlab.com/monnier/typer/compare/ccb4d1aa4a79f15f6fa26f92885f1b79db7...