Setepenre pushed to branch master at Stefan / Typer

Commits: 207f7226 by Pierre Delaunay at 2016-06-06T13:40:55-04:00 added Builtin attribute type

Changes to be committed: * btl/types.typer * src/builtin.ml * new function (new_attribute)

- - - - - 11191bb7 by Pierre Delaunay at 2016-06-09T12:41:18-04:00 Remove dead code

Changes to be committed: * src/debruijn.ml: dead code removal * src/elexp.ml: fix type print * src/env.ml: modified property env * src/eval.ml: monads are lazily evaluated

- - - - - 2fb51647 by Pierre Delaunay at 2016-06-14T16:56:18-04:00 New way of merging and detecting mutually recursive definition in lexp)decls

Changes to be committed: * src/debug_util.ml * src/env.ml * src/lparse.ml * src/REPL.ml: fix typer REPL

- - - - -

12 changed files:

- + - - GNUmakefile - btl/types.typer - samples/nat.typer - src/REPL.ml - src/builtin.ml - src/debruijn.ml - src/debug_util.ml - src/elexp.ml - src/env.ml - src/eval.ml - src/lparse.ml

Changes:

===================================== - ===================================== --- /dev/null +++ b/-

===================================== GNUmakefile ===================================== --- a/GNUmakefile +++ b/GNUmakefile @@ -9,17 +9,14 @@ OBFLAGS = -build-dir _build

all: typer debug tests-build

-ifeq ($(OS), Windows_NT) +# ifeq ($(OS), Windows_NT) # Windows need '-r' and building to native can be problematic (linking error) # So we build to byte instead -OBFLAGS = $(OBFLAGS) -r -endif +# OBFLAGS = $(OBFLAGS) -r +# endif

COMPILE_MODE = byte

- - - # debug file eval debug: # ============================

===================================== btl/types.typer ===================================== --- a/btl/types.typer +++ b/btl/types.typer @@ -114,7 +114,6 @@ sexp_dispatch_ = Built-in "sexp_dispatch_" (Sexp -> (List Sexp -> Sexp) -> Sexp);

- % ----------------------------------------------------- % Monads % ----------------------------------------------------- @@ -139,5 +138,20 @@ open = Built-in "open" (String -> String -> IO FileHandle); write = Built-in "write" (FileHandle -> String -> IO Unit); read = Built-in "read" (FileHandle -> Int -> IO String);

+% ----------------------------------------------------- +% Attributes +% ----------------------------------------------------- + +Attribute = Built-in "Attribute"; +new-attribute = Built-in "new-attribute" (Type -> Attribute); + + + + + + + + +

===================================== samples/nat.typer ===================================== --- a/samples/nat.typer +++ b/samples/nat.typer @@ -1,3 +1,4 @@ +Nat : Type; Nat = inductive_ (dNat) (zero) (succ Nat);

zero = inductive-cons Nat zero;

===================================== src/REPL.ml ===================================== --- a/src/REPL.ml +++ b/src/REPL.ml @@ -122,11 +122,11 @@ let ipexp_parse (sxps: sexp list): (pdecl list * pexp list) = _pxp_parse sxps [] []

-let ierase_type (lexps: (ldecl list * lexpr list)) = +let ierase_type (lexps: (ldecl list list * lexpr list)) = let (ldecls, lexprs) = lexps in - (EL.clean_decls ldecls), (List.map EL.erase_type lexprs) + (EL.clean_toplevel ldecls), (List.map EL.erase_type lexprs)

-let ilexp_parse pexps lctx: ((ldecl list * lexpr list) * lexp_context) = +let ilexp_parse pexps lctx: ((ldecl list list * lexpr list) * lexp_context) = let pdecls, pexprs = pexps in let ldecls, lctx = lexp_p_decls pdecls lctx in let lexprs = lexp_parse_all pexprs lctx in @@ -134,7 +134,7 @@ let ilexp_parse pexps lctx: ((ldecl list * lexpr list) * lexp_context) =

let ieval lexps rctx = let (ldecls, lexprs) = lexps in - let rctx = eval_decls ldecls rctx in + let rctx = eval_decls_toplevel ldecls rctx in let vals = eval_all lexprs rctx false in vals, rctx

@@ -158,8 +158,8 @@ let _raw_eval f str lctx rctx = let nods = sexp_parse_all_to_list default_grammar sxps (Some ";") in let pxps = pexp_decls_all nods in let lxps, lctx = lexp_p_decls pxps lctx in - let elxps = EL.clean_decls lxps in - let rctx = eval_decls elxps rctx in + let elxps = EL.clean_toplevel lxps in + let rctx = eval_decls_toplevel elxps rctx in (* This is for consistency with ieval *) [], lctx, rctx

===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -44,6 +44,9 @@ let builtin_error loc msg = msg_error "BUILT-IN" loc msg; raise (internal_error msg)

+let builtin_warning loc msg = + msg_warning "BUILT-IN" loc msg + type predef_table = (lexp option ref) SMap.t

let predef_name = [ @@ -264,7 +267,9 @@ let write_impl loc args_val ctx = fprintf channel "%s" msg; Vdummy

- +let new_attribute loc args_val ctx = + builtin_warning loc "new-attributes to be implemented"; + Vdummy

(* * Should we have a function that

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -55,7 +55,7 @@ module StringMap = Map.Make (struct type t = string let compare = String.compare end)

(* (* rev_dbi * Var name *) => (name * lexp) *) -type property_elem = lexp StringMap.t +type property_elem = lexp PropertyMap.t type property_env = property_elem PropertyMap.t

(* easier to debug with type annotations *) @@ -203,50 +203,3 @@ let replace_by ctx name by = let nenv = List.fold_left (fun ctx elem -> cons elem ctx) nenv decls in (a, nenv, b)

-(* shift an entire expression by n *) -let rec db_shift expr n = - let db_shift lxp = db_shift lxp n in - match expr with - (* Nothing to shift *) - | Imm _ -> expr - | SortLevel _ -> expr - | Sort _ -> expr - | Builtin _ -> expr - - | Var (s, idx) -> Var(s, idx + n) - | Susp(lxp, s) -> Susp(db_shift lxp, s) - | Cons((s, idx), t) -> Cons((s, idx + n), t) - - | Let(l, decls, lxp) -> - let decls = List.map (fun (var, lxp, ltp) -> - var, db_shift lxp, db_shift ltp) decls in - Let(l, decls, db_shift lxp) - - | Arrow(kind, var, ltp, l, lxp) -> - Arrow(kind, var, db_shift ltp, l, db_shift lxp) - - | Lambda(kind, var, ltp, lxp) -> - Lambda(kind, var, db_shift ltp, db_shift lxp) - - | Call(lxp, args) -> - let args = List.map (fun (kind, lxp) -> (kind, db_shift lxp)) args in - Call(db_shift lxp, args) - - | Inductive(l, nm, fargs, ctors) -> - let fargs = List.map (fun (kind, var, ltp) -> (kind, var, db_shift ltp)) - fargs in - let ctors = SMap.map (fun args -> - List.map (fun (kind, var, ltp) -> (kind, var, db_shift ltp)) args) - ctors in - Inductive(l, nm, fargs, ctors) - - | Case(l, tlxp, tltp, retltp, branch, dflt) -> - let dflt = match dflt with - | Some lxp -> Some (db_shift lxp) - | None -> None in - - let branch = SMap.map (fun (l, args, lxp) -> - (l, args, db_shift lxp)) branch in - Case(l, db_shift tlxp, db_shift tltp, db_shift retltp, branch, dflt) - -

===================================== src/debug_util.ml ===================================== --- a/src/debug_util.ml +++ b/src/debug_util.ml @@ -272,18 +272,55 @@ let main () = debug_pexp_decls pexps; print_string "\n"));

(* get lexp *) - let ctx = default_lctx in + let octx = default_lctx in

- print_string yellow; - let lexps, nctx = - try lexp_p_decls pexps ctx - with e -> ( - print_string reset; - print_lexp_ctx (!_global_lexp_ctx); - print_lexp_trace (); - raise e - ) in - print_string reset; + (* Debug declarations merging *) + + (** ) + let merged = lexp_detect_recursive pexps in + + let _ = List.iter (fun lst -> + print_string (make_line '-' 80); + print_string "\n"; + + List.iter (fun v -> + match v with + | Ldecl((l, s), pxp, ptp) -> ( + lalign_print_string s 20; + + let _ = match ptp with + | Some pxp -> pexp_print pxp; + | None -> print_string " " in + + print_string "\n"; + lalign_print_string s 20; + + let _ = match pxp with + | Some pxp -> pexp_print pxp; + | None -> print_string " " in + + print_string "\n") + | Lmcall((l, s), _ ) -> + print_string s; print_string "\n" + ) lst; + + ) merged in ( **) + + (* debug lexp parsing once merged *) + let lexps, nctx = _lexp_decls pexps octx 0 in + + (* + List.iter (fun ((l, s), lxp, ltp) -> + lalign_print_string s 20; + lexp_print ltp; print_string "\n"; + + lalign_print_string s 20; + lexp_print lxp; print_string "\n"; + + ) decls; *) + + (* use the new way of parsing expr *) + let ctx = nctx in let flexps = List.flatten lexps in

(* convert a lctx context into a typecheck context *)

===================================== src/elexp.ml ===================================== --- a/src/elexp.ml +++ b/src/elexp.ml @@ -205,6 +205,6 @@ and elexp_str lxp = | Inductive(_, (_, s)) -> "inductive_ " ^ s

- | _ -> "Why do you still have those ? " + | Type -> "Type "

===================================== src/env.ml ===================================== --- a/src/env.ml +++ b/src/env.ml @@ -61,6 +61,7 @@ type value_type = | Vdummy | Vin of in_channel | Vout of out_channel + | Vbind of elexp list

let rec value_print (vtp: value_type) = match vtp with @@ -80,6 +81,11 @@ let rec value_print (vtp: value_type) = | Vdummy -> print_string "value_print_dummy" | Vin _ -> print_string "in_channel" | Vout _ -> print_string "out_channel" + | Vbind [a; b] -> print_string "bind ("; + elexp_print a; print_string ") ("; + elexp_print b; print_string ")"; + + | Vbind _ -> print_string "bind" (* | _ -> print_string "debug print" *)

let value_location (vtp: value_type) = @@ -102,6 +108,7 @@ let value_name v = | Vdummy -> "Vdummy" | Vin _ -> "Vin" | Vout _ -> "Vout" + | Vbind _ -> "Vbind"

(* Runtime Environ *) type env_cell = (string option * value_type) ref

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -107,13 +107,13 @@ and eval_var ctx lxp v = let ((loc, name), idx) = v in try get_rte_variable (Some name) (idx) ctx with e -> - eval_error loc ("Variable: " ^ name ^ (str_idx idx) ^ " was not found ") + eval_error loc ("Variable: " ^ name ^ (str_idx idx) ^ " was not found ")

-and eval_call ctx i lname args = +and eval_call ctx i lname eargs = let loc = elexp_location lname in let args = List.map (fun e -> (* elexp_print e; print_string "\n"; *) - _eval e ctx (i + 1)) args in + _eval e ctx (i + 1)) eargs in let f = _eval lname ctx (i + 1) in

let rec eval_call f args ctx = @@ -128,6 +128,10 @@ and eval_call ctx i lname args = let ret = _eval lxp nctx (i + 1) in eval_call ret tl nctx

+ (* bind is lazily evaluated *) + | Vbuiltin ("bind"), _ -> + Vbind eargs + | Vbuiltin (str), args -> (* lookup the built-in implementation and call it *) (get_builtin_impl str loc) loc args ctx @@ -229,6 +233,7 @@ and typer_builtins_impl = [ ("bind" , bind_impl); ("read" , read_impl); ("write" , write_impl); + ("new-attribute" , new_attribute)

] and bind_impl loc args_val ctx = @@ -360,6 +365,7 @@ let from_lctx (ctx: lexp_context) rm: runtime_env = with e -> elexp_print lxp; print_string "\n"; raise e)

+ (* Happen once *) | None -> eval_warning dloc ("Unable to eval expr: " ^ (maybe name)); Vdummy in

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -70,6 +70,12 @@ let _parsing_internals = ref false let _shift_glob = ref 0 let btl_folder = ref "./btl/"

+(* merged declaration, allow us to process declaration in multiple pass *) +(* first detect recursive decls then lexp decls*) +type mdecl = + | Ldecl of symbol * pexp option * pexp option + | Lmcall of symbol * sexp list + (* This is used to make Type annotation and inferred type having the same index *) (* since inferred type might need to parse a lambda var to infer the type *)

@@ -165,7 +171,7 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = | Plet(loc, decls, body) -> let decls, nctx = _lexp_decls decls ctx i in let bdy, ltp = lexp_infer body nctx in - (lexp_let_decls decls bdy nctx i), ltp + (lexp_let_decls decls bdy nctx i), ltp

(* ------------------------------------------------------------------ *) | Parrow (kind, ovar, tp, loc, expr) -> @@ -271,6 +277,13 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = | _ -> pexp_print p; print_string "\n"; lexp_fatal tloc "Unhandled Pexp"

+ +and lexp_let_decls decls (body: lexp) ctx i = + (* build the weird looking let *) + let decls = List.rev decls in + List.fold_left (fun lxp decls -> + Let(dloc, decls, lxp)) body decls + and lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context): lexp = _lexp_p_check p t ctx 1

@@ -701,12 +714,146 @@ and lexp_decls_macro (loc, mname) sargs ctx: pdecl list = (* Parse let declaration *) and lexp_p_decls decls ctx = _lexp_decls decls ctx 0

-and lexp_let_decls decls (body: lexp) ctx i = - (* build the weird looking let *) - let decls = List.rev decls in - List.fold_left (fun lxp decls -> - Let(dloc, decls, lxp)) body decls +and lexp_detect_recursive pdecls = + (* Pack mutually recursive declarations *) + (* mutually recursive def must use forward declarations *) + + let decls = ref [] in + let pending = ref [] in + let merged = ref [] in + + List.iter (fun expr -> + match expr with + | Pexpr((l, s), pxp) ->( + let was_forward = (List.exists + (fun (Ldecl((_, p), _, _)) -> p = s) !pending) in + + let is_empty = (List.length !pending) = 0 in + let is_one = (List.length !pending) = 1 in + + (* This is a standard declaration: not forwarded *) + if (was_forward = false) && is_empty then( + decls := [Ldecl((l, s), Some pxp, None)]::!decls; + ) + (* This is an annotated expression + * or the last element of a mutually rec definition *) + else if (was_forward && is_one) then ( + + (* we know that names match already *) + let ptp = (match (!pending) with + | Ldecl(_, _, ptp)::[] -> ptp + (* we already checked that len(pending) == 1*) + | Ldecl(_, _, ptp)::_ -> lexp_fatal l "Unreachable" + | [] -> lexp_fatal l "Unreachable" + | Lmcall _ :: _ -> lexp_fatal l "Unreachable") in + + (* add declaration to merged decl *) + merged := Ldecl((l, s), Some pxp, ptp)::(!merged); + + (* append decls *) + decls := (List.rev !merged)::!decls; + + (* Reset State *) + pending := []; + merged := []; + ) + (* This is a mutually recursive definition *) + else ( + (* get pending element and remove it from the list *) + let elem, lst = List.partition + (fun (Ldecl((_, n), _, _)) -> n = s) !pending in + + let _ = (match elem with + (* nothing to merge *) + | [] -> + merged := Ldecl((l, s), Some pxp, None)::!merged; + + (* append new element to merged list *) + | Ldecl((l, s), _, Some ptp)::[] -> + merged := Ldecl((l, s), Some pxp, (Some ptp))::!merged; + + (* s should be unique *) + | _ -> lexp_error l "declaration must be unique") in + + (* element is not pending anymore *) + pending := lst; + )) + + | Ptype((l, s), ptp) -> + pending := Ldecl((l, s), None, Some ptp)::!pending + + (* macro will be handled later *) + | Pmcall(a, sargs) -> + decls := [Lmcall(a, sargs)]::!decls;

+ ) pdecls; + + (List.rev !decls) + + +and _lexp_decls decls ctx i: ((vdef * lexp * ltype) list list * lexp_context) = + (* detect mutually recursive def and merge definition *) + let decls = lexp_detect_recursive decls in + let all = ref [] in + + let ctx = List.fold_left (fun ctx decl -> + let d, ctx = _lexp_rec_decl decl ctx i in + all := d::!all; + ctx) ctx decls in + + (List.rev !all), ctx + +and _lexp_rec_decl decls ctx i = + (* parse a groupe of mutually recursive definition + * i.e let decl parsing *) + + (* to compute recursive offset *) + let n = (List.length decls) + 1 in + let lst = ref [] in + + (* add all elements to the environment *) + let tctx = List.fold_left (fun vctx expr -> + match expr with + | Ldecl((l, s), _, None) -> + env_extend vctx (l, s) ForwardRef dltype + + | Ldecl((l, s), _, Some ptp) -> + let lxp, _ = lexp_p_infer ptp vctx in + env_extend vctx (l, s) ForwardRef lxp + + | Lmcall _ -> + lexp_fatal dloc "use lexp_decl_macro to parse macro decls") ctx decls in + + let i = ref 0 in + let ctx = List.fold_left (fun vctx expr -> + i := !i + 1; + match expr with + (* lexp infer *) + | Ldecl ((l, s), Some pxp, None) -> + let lxp, ltp = lexp_p_infer pxp vctx in + lst := ((l, s), lxp, ltp)::!lst; + (* replace forward ref by its true value *) + replace_by vctx s (n - !i, Some (l, s), LetDef lxp, ltp) + + (* lexp check *) + | Ldecl ((l, s), Some pxp, Some ptp) -> + let ltp, _ = lexp_p_infer ptp vctx in + let lxp = lexp_p_check pxp ltp vctx in + lst := ((l, s), lxp, ltp)::!lst; + replace_by vctx s (n - !i, Some (l, s), LetDef lxp, ltp) + + (* macros *) + | Lmcall (a, sargs) -> + lexp_fatal dloc "use lexp_decl_macro to parse macro decls" + + (* unused arg *) + | Ldecl ((l, s), None, _) -> + lexp_error l ("Variable "" ^ s ^ "" is unused!"); + vctx) tctx decls in + + (List.rev !lst), ctx + + (* and _lexp_decls decls ctx i: (((vdef * lexp * ltype) list list) * lexp_context) =

let names = ref [] in (* decls name in correct order *) @@ -794,6 +941,7 @@ and _lexp_decls decls ctx i: (((vdef * lexp * ltype) list list) * lexp_context) | Pmcall((l, n), sargs) -> ( let pdecls = lexp_decls_macro (l, n) sargs vctx in let _, _ =_lexp_decls pdecls vctx (i + 1) in + vctx)

(* | _ -> vctx*)) ctx decls in @@ -818,6 +966,7 @@ and _lexp_decls decls ctx i: (((vdef * lexp * ltype) list list) * lexp_context) merge_list names) (List.rev !names) in

decls, ctx +*)

and lexp_decls_toplevel decls ctx = _lexp_decls decls ctx 1 @@ -1042,7 +1191,9 @@ let default_rctx = _parsing_internals := false;

let rctx = make_runtime_ctx in - eval_decls_toplevel (EL.clean_toplevel d) rctx + let rctx = eval_decls_toplevel (EL.clean_toplevel d) rctx in + _global_eval_trace := []; + rctx (* try (from_lctx (default_lctx)) with e ->( @@ -1073,7 +1224,6 @@ let lexp_decl_str str lctx = _lexp_decl_str str default_stt default_grammar (Some ";") lctx

- (* Eval String * --------------------------------------------------------- *) (* Because we cant include lparse in eval.ml *)

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