May 2016 - Typer - mailman.iro.umontreal.ca

[Git][monnier/typer][master] fix lexp_parse of mutually recursive def
by Setepenre 31 May '16

31 May '16

Setepenre pushed to branch master at Stefan / Typer Commits: 1d5459cf by Pierre Delaunay at 2016-05-31T18:19:26-04:00 fix lexp_parse of mutually recursive def Changes to be committed: * src/lparse.ml: modified lexp_p_decls - - - - - 4 changed files: - samples/quote.typer - src/builtin.ml - src/debruijn.ml - src/lparse.ml Changes: ===================================== samples/quote.typer ===================================== --- a/samples/quote.typer +++ b/samples/quote.typer @@ -55,8 +55,8 @@ quote' = lambda (x : List Sexp) -> % quote definition -quote = Macro_ (lambda (x : List Sexp) -> head Sexp (quote' x)); - +qq = lambda (x : List Sexp) -> head Sexp (quote' x); +quote = Macro_ qq; mn = quote (x * x); ===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -165,7 +165,7 @@ let make_node loc args_val ctx = | _ -> builtin_error loc "node_ expects one 'Sexp' and one 'List Sexp'" in - value_print tlist; print_string "\n"; + (* value_print tlist; print_string "\n"; *) let args = tlist2olist [] tlist in ===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -179,14 +179,15 @@ let env_lookup_expr ctx (v : vref): lexp = | LetDef lxp -> lxp | _ -> Sort (dummy_location, Stype (SortLevel (SLn 0))) in + (* (if (r != 1) then ( let s1 = (Susp (lxp, (S.shift (idx - r + 1)))) in let s2 = (Susp (lxp, (S.shift (idx + 1)))) in lexp_print (unsusp_all s1); print_string "\n"; - lexp_print (unsusp_all s2); print_string "\n"; + lexp_print (unsusp_all s2); print_string "\n"; * ) - )); + )); *) (*let idx = if r > 0 then idx - r else idx + 1 in *) (Susp (lxp, (S.shift (idx - r + 1)))) @@ -209,7 +210,7 @@ let replace_by ctx name by = (cons by tl1), acc else (* Skip some elements if possible *) - if idx < i then replace_by' tl1 by (elem::acc) + if idx <= i then replace_by' tl1 by (elem::acc) else replace_by' tl2 by (elem::acc) (* replace_by' tl1 by (elem::acc) *) in ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -467,7 +467,6 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = (* Build function to be called *) let arg = olist2tlist_lexp sargs ctx in - let lxp = Call(lxp, [(Aexplicit, arg)]) in let elexp = EL.erase_type lxp in let rctx = (from_lctx ctx 0) in @@ -481,9 +480,8 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = print_string "HERE2\n"; value_print body; *) - (* - EL.elexp_print elexp; + print_string "\n\n"; lexp_print lxp; print_string "\n\n"; *) @@ -493,15 +491,23 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = print_rte_ctx rctx; print_string "\n"; print_lexp_ctx ctx; print_string "\n";*) - let sxp = match eval elexp rctx with - | Vsexp(sxp) -> sxp - (* Those are sexp converted by the eval function *) - | Vint(i) -> Integer(dloc, i) - | Vstring(s) -> String(dloc, s) - | Vfloat(f) -> Float(dloc, f) - (* I have vdum here WHY *) - | v -> debug_msg (value_print v); - lexp_fatal loc "Macro_ expects '(List Sexp) -> Sexp'" in + _global_eval_trace := []; + + let vxp = try eval elexp rctx + with e -> + print_eval_trace (); + raise e in + + let sxp = match vxp with + | Vsexp(sxp) -> sxp + (* Those are sexp converted by the eval function *) + | Vint(i) -> Integer(dloc, i) + | Vstring(s) -> String(dloc, s) + | Vfloat(f) -> Float(dloc, f) + (* I have vdum here WHY *) + | v -> debug_msg (value_print v); + lexp_fatal loc "Macro_ expects '(List Sexp) -> Sexp'" in + let pxp = pexp_parse sxp in _lexp_p_infer pxp ctx (i + 1) in @@ -668,57 +674,91 @@ and _lexp_decls decls ctx i: (((vdef * lexp * ltype) list list) * lexp_context) let glob = ref SMap.empty in let mut = ref [] in let offset = ref 1 in + let last_decls = ref "" in + let recursive_mode = ref false in let ctx = List.fold_left (fun vctx expr -> _global_lexp_trace := []; match expr with - | Pexpr((l, s), pxp) ->( + | Pexpr((l, s), pxp) as e ->( try let idx = senv_lookup s vctx in let ltp = env_lookup_type vctx ((l, s), idx) in let lxp = lexp_p_check pxp ltp vctx in - let n = List.length !mut in - let idx = if n = 1 then ( - (* Simple recursive case *) - names := !mut::!names; - mut := []; - offset := 1; 1) else n - !offset in - - (* update declaration *) - glob := SMap.add s (l, s, Some lxp, ltp) !glob; - offset := !offset + 1; - - (* update context *) - replace_by vctx s (idx, Some (l, s), (LetDef lxp), ltp); + (* update declaration *) + glob := SMap.add s (l, s, Some lxp, ltp) !glob; + + (* check if recursive definition *) + (if !last_decls = s && !recursive_mode then + ( + (* print_string "RECURSIVE END\n"; *) + (* push every variable with the correct offset *) + let d = List.rev !mut in + let length = (List.length d) + 1 in + let j = ref 0 in + + let vctx = + List.fold_left (fun vctx n -> + let (l, s, lxp, ltp) = SMap.find n !glob in + let lxp = match lxp with + | Some lxp -> LetDef lxp + | None -> lexp_warning dloc "ForwardRef are not allowed"; + ForwardRef in + + j := !j + 1; + replace_by vctx s (length - !j, Some (l, s), lxp, ltp)) vctx d + + in + + (* Clean everything *) + mut := []; + last_decls := ""; + recursive_mode := false; + vctx + ) + else + ( + (if !recursive_mode then offset := !offset + 1); + (* update context *) + replace_by vctx s (1, Some (l, s), (LetDef lxp), ltp); + )); with Not_found -> - (* push mutually recursive definition *) - (if (List.length !mut) != 0 then - names := !mut::!names; - mut := []; - offset := 1); - (* Add dummy first *) let tctx = env_extend vctx (l, s) ForwardRef dltype in let lxp, ltp = lexp_p_infer pxp tctx in names := [s]::!names; + + (if !recursive_mode then ( + offset := !offset + 1; + mut := s::!mut)); + glob := SMap.add s (l, s, Some lxp, ltp) !glob; env_extend vctx (l, s) (LetDef lxp) ltp) - | Ptype((l, s), ptp) -> - (* this is a mutually recursive definition *) + | Ptype((l, s), ptp) as e -> + (if !recursive_mode then () else + last_decls := s; + offset := 1); + + recursive_mode := true; mut := s::!mut; - (* get type *) - let ltp, _ = lexp_p_infer ptp vctx in - (* push *) - glob := SMap.add s (l, s, None, ltp) !glob; - env_extend vctx (l, s) ForwardRef ltp - | _ -> vctx) ctx decls in + (* get type *) + let ltp, _ = lexp_p_infer ptp vctx in + (* push *) + glob := SMap.add s (l, s, None, ltp) !glob; + env_extend vctx (l, s) ForwardRef ltp + | Pmcall((l, n), sargs) -> + let pdecls = lexp_decls_macro (l, n) sargs vctx in + vctx + + | _ -> vctx) ctx decls in - (if List.length !mut != 0 then names := !mut::!names); + (* + (if List.length !mut != 0 then names := !mut::!names); *) (* return a list containing mutually recursive def *) let merge_list names = View it on GitLab: https://gitlab.com/monnier/typer/commit/1d5459cf478e1cb6ed0eefffb386128f4ed…

1 0

[Git][monnier/typer][master] Macro are passing.
by Setepenre 31 May '16

31 May '16

Setepenre pushed to branch master at Stefan / Typer Commits: 781a872a by Pierre Delaunay at 2016-05-31T15:39:54-04:00 Macro are passing. sqr = Macro_ (lambda (x : List Sexp) -> let hd = (head Sexp x) in (node_ (symbol_ "_*_") (cons hd (cons hd nil)))); This does not work, but if the lambda is declared separately, it works Changes to be committed: * src/builtin.ml * src/debug_util.ml * src/env.ml * src/eval.ml * src/lparse.ml * tests/macro_test.ml - - - - - 6 changed files: - src/builtin.ml - src/debug_util.ml - src/env.ml - src/eval.ml - src/lparse.ml - tests/macro_test.ml Changes: ===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -165,6 +165,8 @@ let make_node loc args_val ctx = | _ -> builtin_error loc "node_ expects one 'Sexp' and one 'List Sexp'" in + value_print tlist; print_string "\n"; + let args = tlist2olist [] tlist in let s = List.map (fun g -> match g with @@ -172,8 +174,11 @@ let make_node loc args_val ctx = (* eval transform sexp into those... *) | Vint (i) -> Integer(dloc, i) | Vstring (s) -> String(dloc, s) - | _ -> value_print g; - builtin_error loc ("node_ expects sexp as arguments")) args in + | _ -> + print_rte_ctx ctx; + print_string (value_name g); print_string "\n"; + value_print g; print_string "\n"; + builtin_error loc ("node_ expects 'List Sexp' second as arguments")) args in Vsexp(Node(op, s)) ===================================== src/debug_util.ml ===================================== --- a/src/debug_util.ml +++ b/src/debug_util.ml @@ -305,10 +305,16 @@ let main () = loop n env Myers.nil in *) (if (get_p_option "typecheck") then( + print_string (make_title " TYPECHECK "); + let cctx = lctx_to_cctx ctx in (* run type check *) List.iter (fun (_, lxp, _) -> - let _ = TC.check cctx lxp in ()) flexps)); + let _ = TC.check cctx lxp in ()) flexps; + + print_string (make_line '-' 76); + + )); (if (get_p_option "lexp") then( print_string (make_title " Lexp "); ===================================== src/env.ml ===================================== --- a/src/env.ml +++ b/src/env.ml @@ -55,14 +55,14 @@ type value_type = | Vcons of symbol * value_type list | Vbuiltin of string | Vfloat of float - | Closure of elexp * (((string option * value_type) ref myers) * (int * int)) + | Closure of string * elexp * (((string option * value_type) ref myers) * (int * int)) | Vsexp of sexp (* Values passed to macros. *) (* Unable to eval during macro expansion, only throw if the value is used *) | Vdummy let rec value_print (vtp: value_type) = match vtp with - | Closure (lxp, _) -> + | Closure (_, lxp, _) -> print_string ("Closure(" ^ (elexp_str lxp) ^ ")") | Vsexp sxp -> sexp_print sxp | Vint(i) -> print_int i @@ -80,7 +80,7 @@ let rec value_print (vtp: value_type) = let value_location (vtp: value_type) = match vtp with | Vcons ((loc, _), _) -> loc - | Closure (lxp, _) -> elexp_location lxp + | Closure (_, lxp, _) -> elexp_location lxp (* location info was lost or never existed *) | _ -> dloc ===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -80,11 +80,12 @@ let rec _eval lxp ctx i: (value_type) = | Imm(sxp) -> Vsexp(sxp) | Inductive (_, _) -> Vdummy | Cons (label) -> Vcons (label, []) - | Lambda (_, lxp) -> Closure(lxp, ctx) + | Lambda ((_, n), lxp) -> Closure(n, lxp, ctx) | Builtin ((_, str)) -> Vbuiltin(str) (* Return a value stored in env *) - | Var((loc, name), idx) as e -> eval_var ctx e ((loc, name), idx) + | Var((loc, name), idx) as e -> + eval_var ctx e ((loc, name), idx) (* Nodes *) (* ---------------- *) @@ -110,16 +111,20 @@ and eval_var ctx lxp v = and eval_call ctx i lname args = let loc = elexp_location lname in - let args = List.map (fun e -> _eval e ctx (i + 1)) args in + let args = List.map (fun e -> + (* elexp_print e; print_string "\n"; *) + _eval e ctx (i + 1)) args in let f = _eval lname ctx (i + 1) in let rec eval_call f args ctx = match f, args with - | Vcons (n, []), _ -> Vcons(n, args) + | Vcons (n, []), _ -> + let e = Vcons(n, args) in + (* value_print e; print_string "\n"; *) e (* we add an argument to the closure *) - | Closure (lxp, ctx), hd::tl -> - let nctx = add_rte_variable None hd ctx in + | Closure (n, lxp, ctx), hd::tl -> + let nctx = add_rte_variable (Some n) hd ctx in let ret = _eval lxp nctx (i + 1) in eval_call ret tl nctx @@ -229,7 +234,7 @@ and typer_eval loc args ctx = (* I need to be able to lexp sexp but I don't have lexp ctx *) match arg with (* Nodes that can be evaluated *) - | Closure (body, ctx) -> _eval body ctx 1 + | Closure (_, body, ctx) -> _eval body ctx 1 (* Leaf *) | _ -> arg @@ -251,9 +256,9 @@ and get_builtin_impl str loc = and sexp_dispatch loc args ctx = let eval a b = _eval a b 1 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; Closure(_, nd, rctx); Closure(_, sym, _); + Closure(_, str, _); Closure(_, it, _); + Closure(_, flt, _); Closure(_, blk, _)] -> sxp, nd, sym, str, it, flt, blk, rctx | _ -> eval_error loc "sexp_dispatch expects 7 arguments" in @@ -268,7 +273,7 @@ and sexp_dispatch loc args ctx = let rctx = add_rte_variable None (Vsexp(op)) rctx in let rctx = add_rte_variable None (olist2tlist_rte s) rctx in match eval nd rctx with - | Closure(nd, _) -> eval nd rctx + | Closure(_, nd, _) -> eval nd rctx | _ -> eval_error loc "Node has 2 arguments") | Symbol (_ , s) -> @@ -312,15 +317,18 @@ 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 maybe s = match s with Some v -> v | _ -> "" + +(* build a rctx from a lctx, rm is used to ignore the last 'rm' elements *) +let from_lctx (ctx: lexp_context) rm: runtime_env = let ((n, _), env, _) = ctx in let n = n - 1 in let rctx = ref make_runtime_ctx in - for i = 0 to n do + for i = 0 to (n - rm) do let name, exp = match (Myers.nth (n - i) env) with | (_, Some (_, name), LetDef exp, _) -> Some name, Some exp + | (_, Some (_, name), _, _) -> Some name, None | _ -> None, None in let vxp = match exp with @@ -331,7 +339,8 @@ let from_lctx (ctx: lexp_context): runtime_env = with e -> elexp_print lxp; print_string "\n"; raise e) - | None -> Vdummy in + | None -> eval_warning dloc ("Unable to eval expr: " ^ (maybe name)); + Vdummy in rctx := add_rte_variable name vxp (!rctx) done; ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -50,6 +50,7 @@ open Builtin module TC = Typecheck module EL = Elexp +module SU = Subst (* Shortcut => Create a Var *) let make_var name index loc = @@ -455,25 +456,50 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = lexp_fatal loc (name ^ " was found but " ^ (string_of_int idx) ^ " is not a correct index.") in - let lxp = match lxp with - | Call(Var((_, "Macro_"), _), [(Aexplicit, fct)]) -> fct - | _ -> lexp_fatal loc "Macro is ill formed" in + let lxp = match unsusp_all lxp with + | Call(Var((_, "Macro_"), _), [(_, fct)]) -> fct + | _ -> + print_string "\n"; + print_string (lexp_to_string lxp); print_string "\n"; + lexp_print lxp; print_string "\n"; + lexp_fatal loc "Macro is ill formed" in (* Build function to be called *) let arg = olist2tlist_lexp sargs ctx in + + let lxp = Call(lxp, [(Aexplicit, arg)]) in + let elexp = EL.erase_type lxp in + let rctx = (from_lctx ctx 0) in + + (* + let rargs = eval (EL.erase_type arg) rctx in + let rctx = add_rte_variable None rargs rctx in + + let lxp = Susp(lxp, (SU.shift 1)) in + let body = eval (EL.erase_type lxp) rctx in + + print_string "HERE2\n"; + value_print body; *) (* + EL.elexp_print elexp; print_string "\n\n"; lexp_print lxp; print_string "\n\n"; *) - let rctx = (from_lctx ctx) in - let sxp = match eval (EL.erase_type lxp) rctx with + (* print_string "DH: "; + value_print (eval (EL.erase_type arg) rctx); print_string "\n"; *) + (* + print_rte_ctx rctx; print_string "\n"; + print_lexp_ctx ctx; print_string "\n";*) + + let sxp = match eval elexp rctx with | Vsexp(sxp) -> sxp (* Those are sexp converted by the eval function *) | Vint(i) -> Integer(dloc, i) | Vstring(s) -> String(dloc, s) | Vfloat(f) -> Float(dloc, f) + (* I have vdum here WHY *) | v -> debug_msg (value_print v); lexp_fatal loc "Macro_ expects '(List Sexp) -> Sexp'" in @@ -644,6 +670,7 @@ and _lexp_decls decls ctx i: (((vdef * lexp * ltype) list list) * lexp_context) let offset = ref 1 in let ctx = List.fold_left (fun vctx expr -> + _global_lexp_trace := []; match expr with | Pexpr((l, s), pxp) ->( try let idx = senv_lookup s vctx in ===================================== tests/macro_test.ml ===================================== --- a/tests/macro_test.ml +++ b/tests/macro_test.ml @@ -42,15 +42,16 @@ open Env let lctx = default_lctx let rctx = default_rctx - let _ = (add_test "MACROS" "macros base" (fun () -> reset_eval_trace (); (* define 'lambda x -> x * x' using macros *) let dcode = " - sqr = Macro_ (lambda (x : List Sexp) -> + my_fun = lambda (x : List Sexp) -> let hd = head Sexp x in - (node_ (symbol_ \"_*_\") (cons hd (cons hd nil)))); + (node_ (symbol_ \"_*_\") (cons hd (cons hd nil))); + + sqr = Macro_ my_fun; " in let rctx, lctx = eval_decl_str dcode lctx rctx in View it on GitLab: https://gitlab.com/monnier/typer/commit/781a872a1c1873bbd8e57395b151a878661…

1 0

[Git][monnier/typer][master] All tests pass
by Setepenre 26 May '16

26 May '16

Setepenre pushed to branch master at Stefan / Typer Commits: 723db68b by Pierre Delaunay at 2016-05-26T16:24:59-04:00 All tests pass Changes to be committed: - src/eval.ml - src/lparse.ml - fix builtin parsing as (lctx -> rctx) is not as straight forward as it was - - - - - 2 changed files: - src/eval.ml - src/lparse.ml Changes: ===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -315,19 +315,43 @@ let eval_all lxps rctx silent = (* build a rctx from a lctx *) let from_lctx (ctx: lexp_context): runtime_env = let ((n, _), env, _) = ctx in + let n = n - 1 in + let rctx = ref make_runtime_ctx in + + for i = 0 to n do + let name, exp = match (Myers.nth (n - i) env) with + | (_, Some (_, name), LetDef exp, _) -> Some name, Some exp + | _ -> None, None in + + let vxp = match exp with + | Some lxp -> + let octx = add_rte_variable name Vdummy (!rctx) in + let lxp = (erase_type lxp) in + (try (eval lxp octx) + with e -> elexp_print lxp; + print_string "\n"; raise e) + + | None -> Vdummy in + + rctx := add_rte_variable name vxp (!rctx) + done; + + !rctx + + (* let ((n, _), env, _) = ctx in let rctx = ref make_runtime_ctx in let bsize = 0 in let csize = n - 1 in - (* add all variables *) + (* add all variables * ) for i = bsize to csize do let name = match (Myers.nth (csize - i) env) with | (_, Some (_, name), _, _) -> Some name | _ -> None in rctx := add_rte_variable name Vdummy (!rctx) - done; + done; *) let diff = csize - bsize in @@ -347,11 +371,11 @@ let from_lctx (ctx: lexp_context): runtime_env = print_string "\n"; raise e) | None -> Vdummy in - rctx := set_rte_variable j name vxp (!rctx) + rctx := add_rte_variable name vxp (!rctx) with Not_found -> print_int n; print_string " "; print_int (csize - i); print_string "\n "; raise Not_found done; - !rctx + !rctx *) ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -701,8 +701,9 @@ and _lexp_decls decls ctx i: (((vdef * lexp * ltype) list list) * lexp_context) | Some lxp -> lxp | None -> dltype in + (* let ltp = unsusp_all ltp in - let lxp = unsusp_all lxp in + let lxp = unsusp_all lxp in *) ((l, s), lxp, ltp)::acc) [] names in let decls = List.map (fun names -> @@ -893,9 +894,15 @@ let default_lctx = let pxps = pexp_decls_all nods in _parsing_internals := true; - let _, lctx = lexp_p_decls pxps lctx in + let d, lctx = lexp_p_decls pxps lctx in _parsing_internals := false; + (* dump grouped decls * ) + List.iter (fun decls -> + print_string "["; + List.iter (fun ((_, s), _, _) -> + print_string (s ^ ", ")) decls; print_string "] \n") d; *) + (* Once default builtin are set we can populate the predef table *) try List.iter (fun name -> @@ -911,11 +918,29 @@ let default_lctx = (* Make runtime context with built-in types *) let default_rctx = + (* Empty context *) + let lctx = make_lexp_context in + let lxp = Builtin((dloc, "Built-in"), type0) in + let lctx = env_extend lctx (dloc, "Built-in") (LetDef lxp) type0 in + + (* Read BTL files *) + let pres = prelex_file (!btl_folder ^ "types.typer") in + let sxps = lex default_stt pres in + let nods = sexp_parse_all_to_list default_grammar sxps (Some ";") in + let pxps = pexp_decls_all nods in + + _parsing_internals := true; + let d, lctx = lexp_p_decls pxps lctx in + _parsing_internals := false; + + let rctx = make_runtime_ctx in + eval_decls_toplevel (EL.clean_toplevel d) rctx + (* try (from_lctx (default_lctx)) with e ->( print_eval_trace (); lexp_error dloc "Could not convert lexp context into rte context"; - raise e) + raise e) *) (* String Parsing View it on GitLab: https://gitlab.com/monnier/typer/commit/723db68b317662ee4f962c847659bfc59f4…

1 0

[Git][monnier/typer][master] Trys to handle declaration parsing correctly.
by Setepenre 26 May '16

26 May '16

Setepenre pushed to branch master at Stefan / Typer Commits: e2a13504 by Pierre Delaunay at 2016-05-26T15:48:46-04:00 Trys to handle declaration parsing correctly. Function 'length' bug Changes to be committed: * src/eval.ml: - new function eval_decls_toplevel * src/lparse.ml: - new function lexep_decls_toplevel - - - - - 6 changed files: - btl/types.typer - src/debug_util.ml - src/elexp.ml - src/eval.ml - src/lparse.ml - tests/lexp_test.ml Changes: ===================================== btl/types.typer ===================================== --- a/btl/types.typer +++ b/btl/types.typer @@ -45,7 +45,73 @@ _+_ = Built-in "_+_" (Int -> Int -> Int); _*_ = Built-in "_*_" (Int -> Int -> Int); +Bool = inductive_ (Boolean) (True) (False); +True = inductive-cons Bool True; +False = inductive-cons Bool False; +%Option : Type -> Type; +Option = inductive_ (Option (a : Type)) (None) (Some a); +Some = inductive-cons Option Some; +None = inductive-cons Option None; + +string_eq = Built-in "string_eq" (String -> String -> Bool); +int_eq = Built-in "int_eq" (Int -> Int -> Bool); +sexp_eq = Built-in "sexp_eq" (Sexp -> Sexp -> Bool); + +% ----------------------------------------------------- +% List +% ----------------------------------------------------- + +List : Type -> 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 => + lambda xs -> + case xs + | nil => 0 + | cons hd tl => (1 + (length a tl)); + +head : (a : Type) => List a -> a; +head = lambda a => + lambda xs -> + case xs + | nil => nil + | cons hd tl => hd; + +tail : (a : Type) => List a -> List a; +tail = lambda a => + lambda xs -> + case xs + | nil => nil + | cons hd tl => tl; + +% ----------------------------------------------------- +% Macro +% ----------------------------------------------------- + +block_ = Built-in "block_" ((List Sexp) -> Sexp); +symbol_ = Built-in "symbol_" (String -> Sexp); +string_ = Built-in "string_" (String -> Sexp); +node_ = Built-in "node_" (Sexp -> (List Sexp) -> Sexp); +integer_ = Built-in "integer_" (Int -> Sexp); +float_ = Built-in "float_" (Float -> Sexp); + +% Macro : Type; +Macro = inductive_ (dMacro) (Macro_ ((List Sexp) -> Sexp)); +Macro_ = inductive-cons Macro Macro_ ; + +sexp_dispatch_ = Built-in "sexp_dispatch_" (Sexp + -> (Sexp -> List Sexp -> Sexp) + -> (String -> Sexp) + -> (String -> Sexp) + -> (Int -> Sexp) + -> (Float -> Sexp) + -> (List Sexp -> Sexp) + -> Sexp); ===================================== src/debug_util.ml ===================================== --- a/src/debug_util.ml +++ b/src/debug_util.ml @@ -201,7 +201,7 @@ let format_source () = print_string (make_sep '-'); print_string "\n"; - let result = _lexp_str_decls (!_ppctx) lexps in + let result = _lexp_str_decls (!_ppctx) (List.flatten lexps) in if (!_write_file) then ( print_string (" " ^ " Writing output file: " ^ (!_format_dest) ^ "\n"); @@ -284,6 +284,7 @@ let main () = raise e ) in print_string reset; + let flexps = List.flatten lexps in (* convert a lctx context into a typecheck context *) (* they will be the same in the future *) @@ -307,21 +308,21 @@ let main () = let cctx = lctx_to_cctx ctx in (* run type check *) List.iter (fun (_, lxp, _) -> - let _ = TC.check cctx lxp in ()) lexps)); + let _ = TC.check cctx lxp in ()) flexps)); (if (get_p_option "lexp") then( print_string (make_title " Lexp "); - debug_lexp_decls lexps; print_string "\n")); + debug_lexp_decls flexps; print_string "\n")); (if (get_p_option "lctx") then( print_lexp_ctx nctx; print_string "\n")); - let clean_lxp = EL.clean_decls lexps in + let clean_lxp = EL.clean_toplevel lexps in (* Eval declaration *) let rctx = default_rctx in print_string yellow; - let rctx = (try eval_decls clean_lxp rctx; + let rctx = (try eval_decls_toplevel clean_lxp rctx; with e -> print_string reset; print_rte_ctx (!_global_eval_ctx); ===================================== src/elexp.ml ===================================== --- a/src/elexp.ml +++ b/src/elexp.ml @@ -108,6 +108,10 @@ and filter_arg_list lst = and clean_decls decls = List.map (fun (v, lxp, _) -> (v, (erase_type lxp))) decls +(* toplevel is a list of value *) +and clean_toplevel decls = + List.map (fun v -> clean_decls v) decls + and clean_maybe lxp = match lxp with | Some lxp -> Some (erase_type lxp) ===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -183,30 +183,25 @@ and build_arg_list args ctx i = List.fold_left (fun c v -> add_rte_variable None v c) ctx arg_val and eval_decls decls ctx = _eval_decls decls ctx 0 -and _eval_decls (decls: ((vdef * elexp) list)) +and _eval_decls (decls: (vdef * elexp) list) (ctx: runtime_env) i: runtime_env = let n = (List.length decls) - 1 in (* Read declarations once and push them *) - List.fold_left (fun ctx ((_, name), lxp) -> - let ctx = add_rte_variable (Some name) Vdummy ctx in - let lxp = _eval lxp ctx (i + 1) in - set_rte_variable 0 (Some name) lxp ctx) - - ctx decls - - - - (* Read declarations once and push them * ) - let _, ctx = List.fold_left (fun (idx, ctx) ((_, name), lxp) -> - _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)) - (n, ctx) decls in - - ctx *) + let nctx = List.fold_left (fun ctx ((_, name), _) -> + add_rte_variable (Some name) Vdummy ctx) ctx decls in + + List.iteri (fun idx ((_, name), lxp) -> + let lxp = _eval lxp nctx (i + 1) in + let offset = n - idx in + ignore (set_rte_variable offset (Some name) lxp nctx)) decls; + + nctx +and eval_decls_toplevel (decls: (vdef * elexp) list list) ctx = + (* Add toplevel decls function *) + List.fold_left (fun ctx decls -> + eval_decls decls ctx) ctx decls (* -------------------------------------------------------------------------- *) (* Builtin Implementation (Some require eval) *) ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -162,9 +162,9 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = (* Let, Variable declaration + local scope *) | Plet(loc, decls, body) -> - let decl, nctx = _lexp_decls decls ctx i in + let decls, nctx = _lexp_decls decls ctx i in let bdy, ltp = lexp_infer body nctx in - Let(tloc, decl, bdy), ltp + (lexp_let_decls decls bdy nctx i), ltp (* ------------------------------------------------------------------ *) | Parrow (kind, ovar, tp, loc, expr) -> @@ -629,10 +629,94 @@ 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_decls decls ctx i: (((vdef * lexp * ltype) list) * lexp_context) = - let names = ref [] in + +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_decls decls ctx i: (((vdef * lexp * ltype) list list) * lexp_context) = + + let names = ref [] in (* decls name in correct order *) + let glob = ref SMap.empty in + let mut = ref [] in + let offset = ref 1 in + + let ctx = List.fold_left (fun vctx expr -> + match expr with + | Pexpr((l, s), pxp) ->( + try let idx = senv_lookup s vctx in + let ltp = env_lookup_type vctx ((l, s), idx) in + let lxp = lexp_p_check pxp ltp vctx in + let n = List.length !mut in + let idx = if n = 1 then ( + (* Simple recursive case *) + names := !mut::!names; + mut := []; + offset := 1; 1) else n - !offset in + + (* update declaration *) + glob := SMap.add s (l, s, Some lxp, ltp) !glob; + offset := !offset + 1; + + (* update context *) + replace_by vctx s (idx, Some (l, s), (LetDef lxp), ltp); + + with Not_found -> + (* push mutually recursive definition *) + (if (List.length !mut) != 0 then + names := !mut::!names; + mut := []; + offset := 1); + + (* Add dummy first *) + let tctx = env_extend vctx (l, s) ForwardRef dltype in + let lxp, ltp = lexp_p_infer pxp tctx in + + names := [s]::!names; + glob := SMap.add s (l, s, Some lxp, ltp) !glob; + + env_extend vctx (l, s) (LetDef lxp) ltp) + + | Ptype((l, s), ptp) -> + (* this is a mutually recursive definition *) + mut := s::!mut; + (* get type *) + let ltp, _ = lexp_p_infer ptp vctx in + (* push *) + glob := SMap.add s (l, s, None, ltp) !glob; + env_extend vctx (l, s) ForwardRef ltp + + | _ -> vctx) ctx decls in + + + (if List.length !mut != 0 then names := !mut::!names); + + (* return a list containing mutually recursive def *) + let merge_list names = + List.fold_left (fun acc key -> + let (l, s, lxp, ltp) = SMap.find key !glob in + let lxp = match lxp with + | Some lxp -> lxp + | None -> dltype in + + let ltp = unsusp_all ltp in + let lxp = unsusp_all lxp in + ((l, s), lxp, ltp)::acc) [] names in + + let decls = List.map (fun names -> + merge_list names) (List.rev !names) in + + decls, ctx + +and lexp_decls_toplevel decls ctx = + _lexp_decls decls ctx 1 + + (* let names = ref [] in let offset = ref 0 in let merged = ref SMap.empty in + let acc = ref [] in let ctx = List.fold_left (fun vctx expr -> match expr with @@ -674,7 +758,7 @@ and _lexp_decls decls ctx i: (((vdef * lexp * ltype) list) * lexp_context) = let lxp = unsusp_all lxp in ((l, s), lxp, ltp)::acc) [] !names in - decls, ctx + decls, ctx *) and _lexp_parse_all (p: pexp list) (ctx: lexp_context) i : lexp list = @@ -870,6 +954,6 @@ 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 - let elxps = (EL.clean_decls lxps) in - (eval_decls elxps rctx), lctx + let elxps = (EL.clean_toplevel lxps) in + (eval_decls_toplevel elxps rctx), lctx ===================================== tests/lexp_test.ml ===================================== --- a/tests/lexp_test.ml +++ b/tests/lexp_test.ml @@ -54,7 +54,7 @@ let _ = (add_test "LEXP" "lexp_print" (fun () -> let ret1, _ = lexp_decl_str dcode lctx in let to_str decls = - let str = _lexp_str_decls (!compact_ppctx) ret1 in + let str = _lexp_str_decls (!compact_ppctx) (List.flatten ret1) in List.fold_left (fun str lxp -> str ^ lxp) "" str in (* Cast to string *) View it on GitLab: https://gitlab.com/monnier/typer/commit/e2a13504bc9dcd5154b26f63a51b0f8900d…

1 0

[Git][monnier/typer][master] Fix recursive definition handling
by Setepenre 23 May '16

23 May '16

Setepenre pushed to branch master at Stefan / Typer Commits: 3335b48a by Pierre Delaunay at 2016-05-23T18:10:47-04:00 Fix recursive definition handling Changes to be committed: * src/debruijn.ml * src/lparse.ml - - - - - 3 changed files: - samples/nat.typer - src/debruijn.ml - src/lparse.ml Changes: ===================================== samples/nat.typer ===================================== --- a/samples/nat.typer +++ b/samples/nat.typer @@ -21,10 +21,22 @@ plus = lambda (x : Nat) -> | succ z => succ (plus z y); -n1 = (to-num zero); -n2 = (to-num one); -n3 = (to-num two); +odd : Nat -> Int; +even : Nat -> Int; +odd = lambda (n : Nat) -> case n + | zero => 0 + | succ y => (even y); -m1 = (to-num (plus zero two)); % 2 -m2 = (to-num (plus two zero)); % 2 -m3 = (to-num (plus two one)); % 3 \ No newline at end of file +even = lambda (n : Nat) -> case n + | zero => 1 + | succ y => (odd y); + +%n1 = (to-num zero); +%n2 = (to-num one); +%n3 = (to-num two); + +%m1 = (to-num (plus zero two)); % 2 +%m2 = (to-num (plus two zero)); % 2 +%m3 = (to-num (plus two one)); % 3 + +o1 = (even two); \ No newline at end of file ===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -176,7 +176,8 @@ let env_lookup_expr ctx (v : vref): lexp = let (r, _, lxp, _) = _env_lookup ctx v in let lxp = match lxp with - | LetDef lxp -> lxp in + | LetDef lxp -> lxp + | _ -> Sort (dummy_location, Stype (SortLevel (SLn 0))) in (if (r != 1) then ( let s1 = (Susp (lxp, (S.shift (idx - r + 1)))) in ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -234,7 +234,7 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = let inductive_type = Var((loc, type_name), idx) in (* Get constructor args *) - let formal, args = match idt with + let formal, args = match unsusp_all idt with | Inductive(_, _, formal, ctor_def) -> ( try formal, (SMap.find cname ctor_def) with Not_found -> @@ -542,7 +542,7 @@ and lexp_read_pattern pattern exp target ctx: | Ppatvar ((loc, name) as var) ->( try( let idx = senv_lookup name ctx in - match (env_lookup_expr ctx ((loc, name), idx)) with + match unsusp_all (env_lookup_expr ctx ((loc, name), idx)) with (* We are matching a constructor *) | Cons _ -> (name, loc, []), ctx View it on GitLab: https://gitlab.com/monnier/typer/commit/3335b48a67b752cbf208a59441031b21c12…

1 0

[Git][monnier/typer][master] fix eval order
by Setepenre 23 May '16

23 May '16

Setepenre pushed to branch master at Stefan / Typer Commits: 38d418dc by Pierre Delaunay at 2016-05-23T17:48:02-04:00 fix eval order Changes to be committed: * src/eval.ml * src/lparse.ml - add dummy type annotation if none present - - - - - 3 changed files: - src/debruijn.ml - src/eval.ml - src/lparse.ml Changes: ===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -126,7 +126,7 @@ let env_add_var_info var (ctx: lexp_context) = let env_extend (ctx: lexp_context) (def: vdef) (v: varbind) (t: lexp) = let ((n, map), e, f) = ctx in - env_add_var_info (0, Some def, v, t) (senv_add_var def ctx) + env_add_var_info (1, Some def, v, t) (senv_add_var def ctx) let _name_error loc estr str = @@ -169,7 +169,7 @@ let _env_lookup ctx (v: vref): env_elem = let env_lookup_type ctx (v : vref): lexp = let (_, idx) = v in let (_, _, _, ltp) = _env_lookup ctx v in - (* unsusp_all *) (Susp (ltp, (S.shift (idx + 1)))) + (Susp (ltp, (S.shift (idx + 1)))) let env_lookup_expr ctx (v : vref): lexp = let (_, idx) = v in @@ -178,7 +178,17 @@ let env_lookup_expr ctx (v : vref): lexp = let lxp = match lxp with | LetDef lxp -> lxp in - (* unsusp_all *) (Susp (lxp, (S.shift (idx - r + 1)))) + (if (r != 1) then ( + let s1 = (Susp (lxp, (S.shift (idx - r + 1)))) in + let s2 = (Susp (lxp, (S.shift (idx + 1)))) in + + lexp_print (unsusp_all s1); print_string "\n"; + lexp_print (unsusp_all s2); print_string "\n"; + + )); + (*let idx = if r > 0 then idx - r else idx + 1 in *) + + (Susp (lxp, (S.shift (idx - r + 1)))) let env_lookup_by_index index (ctx: lexp_context): env_elem = (Myers.nth index (_get_env ctx)) ===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -186,14 +186,19 @@ and eval_decls decls ctx = _eval_decls decls ctx 0 and _eval_decls (decls: ((vdef * elexp) list)) (ctx: runtime_env) i: runtime_env = - (* Read declarations once and push them *) - let ctx = List.fold_left (fun ctx ((_, name), lxp) -> - add_rte_variable (Some name) Vdummy ctx) - ctx decls in - let n = (List.length decls) - 1 in (* Read declarations once and push them *) + List.fold_left (fun ctx ((_, name), lxp) -> + let ctx = add_rte_variable (Some name) Vdummy ctx in + let lxp = _eval lxp ctx (i + 1) in + set_rte_variable 0 (Some name) lxp ctx) + + ctx decls + + + + (* Read declarations once and push them * ) let _, ctx = List.fold_left (fun (idx, ctx) ((_, name), lxp) -> _global_eval_trace := []; let lxp = _eval lxp ctx (i + 1) in @@ -201,7 +206,8 @@ and _eval_decls (decls: ((vdef * elexp) list)) (idx - 1, ctx)) (n, ctx) decls in - ctx + ctx *) + (* -------------------------------------------------------------------------- *) (* Builtin Implementation (Some require eval) *) ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -283,7 +283,7 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = (* This case cannot be inferred *) | Plambda (kind, var, None, body) ->( (* Read var type from the provided type *) - let ltp, lbtp = match t with + let ltp, lbtp = match unsusp_all t with | Arrow(kind, _, ltp, _, lbtp) -> ltp, lbtp | _ -> lexp_error tloc "Type does not match"; dltype, dltype in @@ -643,11 +643,14 @@ and _lexp_decls decls ctx i: (((vdef * lexp * ltype) list) * lexp_context) = let (_, _, _, ltp) = SMap.find s !merged in merged := SMap.add s (l, s, Some lxp, ltp) !merged; let r = !offset in + let r = if r = 0 then 1 else r in offset := 0; replace_by vctx s (r, Some (l, s), (LetDef lxp), ltp); with Not_found -> - let lxp, ltp = lexp_p_infer pxp vctx in + (* Add dummy first *) + let tctx = env_extend vctx (l, s) ForwardRef dltype in + let lxp, ltp = lexp_p_infer pxp tctx in names := s::!names; merged := SMap.add s (l, s, Some lxp, ltp) !merged; env_extend vctx (l, s) (LetDef lxp) ltp) @@ -694,7 +697,7 @@ and print_lexp_ctx (ctx : lexp_context) = (Some ('l', 7), "INDEX"); (Some ('l', 10), "NAME"); (Some ('l', 4), "OFF"); - (Some ('l', 32), "VALUE:TYPE")]; + (Some ('l', 29), "VALUE:TYPE")]; print_string (make_sep '-'); View it on GitLab: https://gitlab.com/monnier/typer/commit/38d418dca56f2b4bdf3b5254c75b6a89b4d…

1 0

[Git][monnier/typer][master] Use Susp to shift when required.
by Setepenre 21 May '16

21 May '16

Setepenre pushed to branch master at Stefan / Typer Commits: 9b332512 by Pierre Delaunay at 2016-05-21T09:11:50-04:00 Use Susp to shift when required. I don't understand why: sqr = lambda (x : Int) -> x * x; main = sqr 2; % sqr[0] 2; % failed to find sqr[0] found main is not processed correctly sqr is not shifted by one as it should have been. Changes to be committed: * src/lparse.ml * src/lexp.ml * src/debruijn.ml - - - - - 9 changed files: - .gitignore - GNUmakefile - btl/types.typer - src/debruijn.ml - src/elexp.ml - src/env.ml - src/eval.ml - src/lexp.ml - src/lparse.ml Changes: ===================================== .gitignore ===================================== --- a/.gitignore +++ b/.gitignore @@ -15,7 +15,7 @@ manual.?? *_build/ *~ \#*\# -test__.ml +test.ml _temp_hack test__.typer *.orig ===================================== GNUmakefile ===================================== --- a/GNUmakefile +++ b/GNUmakefile @@ -47,6 +47,10 @@ tests-build: tests-run: @./_build/tests/utests --verbose= 3 +test-file: + ocamlbuild src/test.$(COMPILE_MODE) -I src $(OBFLAGS) + @mv _build/src/test.$(COMPILE_MODE) _build/test + # There is nothing here. I use this to test if opam integration works install: tests @@ -80,3 +84,6 @@ run/tests: run/typer-file: @./_build/typer ./samples/test__.typer + +run/test-file: + @./_build/test ===================================== btl/types.typer ===================================== --- a/btl/types.typer +++ b/btl/types.typer @@ -44,78 +44,6 @@ Sexp = Built-in "Sexp"; _+_ = Built-in "_+_" (Int -> Int -> Int); _*_ = Built-in "_*_" (Int -> Int -> Int); -Bool = inductive_ (Boolean) (True) (False); -True = inductive-cons Bool True; -False = inductive-cons Bool False; - -%Option : Type -> Type; -Option = inductive_ (Option (a : Type)) (None) (Some a); -Some = inductive-cons Option Some; -None = inductive-cons Option None; - -string_eq = Built-in "string_eq" (String -> String -> Bool); -int_eq = Built-in "int_eq" (Int -> Int -> Bool); -sexp_eq = Built-in "sexp_eq" (Sexp -> Sexp -> Bool); - -% ----------------------------------------------------- -% List -% ----------------------------------------------------- - -List : Type -> 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 => - lambda xs -> - case xs - | nil => 0 - | cons hd tl => (1 + (length a tl)); - -head : (a : Type) => List a -> a; -head = lambda a => - lambda xs -> - case xs - | nil => nil - | cons hd tl => hd; - -tail : (a : Type) => List a -> List a; -tail = lambda a => - lambda xs -> - case xs - | nil => nil - | cons hd tl => tl; - -% ----------------------------------------------------- -% Macro -% ----------------------------------------------------- - -block_ = Built-in "block_" ((List Sexp) -> Sexp); -symbol_ = Built-in "symbol_" (String -> Sexp); -string_ = Built-in "string_" (String -> Sexp); -node_ = Built-in "node_" (Sexp -> (List Sexp) -> Sexp); -integer_ = Built-in "integer_" (Int -> Sexp); -float_ = Built-in "float_" (Float -> Sexp); - -% Macro : Type; -Macro = inductive_ (dMacro) (Macro_ ((List Sexp) -> Sexp)); -Macro_ = inductive-cons Macro Macro_ ; - -sexp_dispatch_ = Built-in "sexp_dispatch_" (Sexp - -> (Sexp -> List Sexp -> Sexp) - -> (String -> Sexp) - -> (String -> Sexp) - -> (Int -> Sexp) - -> (Float -> Sexp) - -> (List Sexp -> Sexp) - -> Sexp); - - - - - ===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -166,18 +166,19 @@ let _env_lookup ctx (v: vref): env_elem = Not_found -> debruijn_error loc "DeBruijn index out of bounds!" -let env_lookup_type ctx (v : vref) = - (* let ((csize, _), _, _) = ctx in *) - (* FIXME: We need to S.shift here, since `t` is valid in the context in - * which `vref` appeared, rather than in `ctx`. *) +let env_lookup_type ctx (v : vref): lexp = + let (_, idx) = v in + let (_, _, _, ltp) = _env_lookup ctx v in + (* unsusp_all *) (Susp (ltp, (S.shift (idx + 1)))) +let env_lookup_expr ctx (v : vref): lexp = + let (_, idx) = v in + let (r, _, lxp, _) = _env_lookup ctx v in - let (_, _, _, t) = _env_lookup ctx v in t + let lxp = match lxp with + | LetDef lxp -> lxp in -let env_lookup_expr ctx (v : vref) = - (* FIXME: We need S.shift here, since `lxp` is valid in the context in - * which `vref` appeared (plus recursion offset), rather than in `ctx`. *) - let (_, _, lxp, _) = _env_lookup ctx v in lxp + (* unsusp_all *) (Susp (lxp, (S.shift (idx - r + 1)))) let env_lookup_by_index index (ctx: lexp_context): env_elem = (Myers.nth index (_get_env ctx)) ===================================== src/elexp.ml ===================================== --- a/src/elexp.ml +++ b/src/elexp.ml @@ -140,6 +140,20 @@ let rec elexp_location e = | Inductive(l, _) -> l | Type -> U.dummy_location + +let elexp_name e = + match e with + | Imm _ -> "Imm" + | Builtin _ -> "Builtin" + | Var _ -> "Var" + | Let _ -> "Let" + | Lambda _ -> "Lambda" + | Call _ -> "Call" + | Cons _ -> "Cons" + | Case _ -> "Case" + | Type -> "Type" + | Inductive _ -> "Inductive" + let rec elexp_print lxp = print_string (elexp_str lxp) and elexp_to_string lxp = elexp_str lxp and elexp_str lxp = ===================================== src/env.ml ===================================== --- a/src/env.ml +++ b/src/env.ml @@ -84,6 +84,18 @@ let value_location (vtp: value_type) = (* location info was lost or never existed *) | _ -> dloc + +let value_name v = + match v with + | Vint _ -> "Vint" + | Vstring _ -> "Vstring" + | Vcons _ -> "Vcons" + | Vbuiltin _ -> "Sbuiltin" + | Vfloat _ -> "Vfloat" + | Closure _ -> "Closure" + | Vsexp _ -> "Vsexp" + | Vdummy -> "Vdummy" + (* Runtime Environ *) type env_cell = (string option * value_type) ref type runtime_env = (env_cell myers) * (int * int) ===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -291,10 +291,9 @@ and print_eval_result i lxp = and print_eval_trace () = - print_trace " EVAL TRACE " 50 elexp_to_string elexp_print !_global_eval_trace + print_trace " EVAL TRACE " 50 elexp_name elexp_print !_global_eval_trace let eval lxp ctx = - _global_eval_trace := []; _eval lxp ctx 1 let debug_eval lxp ctx = ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -322,7 +322,10 @@ let rec unsusp e s = (* Push a suspension one level down. *) | None -> default | Some e -> Some (mkSusp e s)) - +let unsusp_all e = + match e with + | Susp(e, s) -> unsusp e s + | _ -> e let lexp_to_string e = match e with @@ -665,6 +668,8 @@ and _lexp_to_str ctx exp = | Float (_, s) -> tval (string_of_float s) | e -> sexp_to_str e) + | Susp _ -> _lexp_to_str ctx (unsusp_all exp) + | Var ((loc, name), idx) -> name ^ (index idx) ; | Let (_, decls, body) -> @@ -711,7 +716,7 @@ and _lexp_to_str ctx exp = | _ -> "__", -1, true, true in let binop_str op (_, lhs) (_, rhs) = - (lexp_to_str lhs) ^ op ^ (lexp_to_str rhs) in + (lexp_to_str lhs) ^ op ^ (index idx) ^ " " ^ (lexp_to_str rhs) in let add_parens bl str = if bl then "(" ^ str ^ ")" else str in @@ -722,11 +727,11 @@ and _lexp_to_str ctx exp = * Either use the boring (_+_ e1 e2) notation, or check the * grammar to decide when we can use the infix notation and * when to add parenthese. *) - | ("_=_", [lhs; rhs]) -> binop_str " = " lhs rhs - | ("_+_", [lhs; rhs]) -> binop_str " + " lhs rhs - | ("_-_", [lhs; rhs]) -> binop_str " - " lhs rhs - | ("_/_", [lhs; rhs]) -> binop_str " / " lhs rhs - | ("_*_", [lhs; rhs]) -> binop_str " * " lhs rhs + | ("_=_", [lhs; rhs]) -> binop_str " =" lhs rhs + | ("_+_", [lhs; rhs]) -> binop_str " +" lhs rhs + | ("_-_", [lhs; rhs]) -> binop_str " -" lhs rhs + | ("_/_", [lhs; rhs]) -> binop_str " /" lhs rhs + | ("_*_", [lhs; rhs]) -> binop_str " *" lhs rhs (* not an operator *) | _ -> let args = List.fold_left ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -235,7 +235,7 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = (* Get constructor args *) let formal, args = match idt with - | LetDef Inductive(_, _, formal, ctor_def) -> ( + | Inductive(_, _, formal, ctor_def) -> ( try formal, (SMap.find cname ctor_def) with Not_found -> lexp_error loc @@ -388,7 +388,7 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = (* consume Arrows and args together *) let rec get_return_type name i ltp args = - match ltp, args with + match (unsusp_all ltp), args with | _, [] -> ltp | Arrow(_, _, _, _, ltp), hd::tl -> (get_return_type name (i + 1) ltp tl) | _, _ -> lexp_warning loc @@ -402,7 +402,7 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = (* retrieve function's body *) let body, ltp = _lexp_p_infer fun_name ctx (i + 1) in - (* let ret_type = get_return_type 0 ltp new_args in *) + let ltp = unsusp_all ltp in let handle_named_call (loc, name) = (* Process Arguments *) @@ -414,8 +414,8 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = let idx = senv_lookup name ctx in let vf = (make_var name idx loc) in - match env_lookup_expr ctx ((loc, name), idx) with - | LetDef Builtin((_, "Built-in"), _) ->( + match unsusp_all (env_lookup_expr ctx ((loc, name), idx)) with + | Builtin((_, "Built-in"), _) ->( (* ------ SPECIAL ------ *) match !_parsing_internals, largs with | true, [Imm(String (_, str))] -> @@ -432,7 +432,7 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = lexp_error loc "Use of \"Built-in\" in user code"; dlxp, dltype) - | _ -> + | e -> let ret_type = get_return_type name 0 ltp new_args in Call(vf, new_args), ret_type @@ -448,9 +448,9 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = lexp_fatal loc ("Could not find Variable: " ^ name) in (* Get the macro *) - let lxp = try match env_lookup_expr ctx ((loc, name), idx) with - | LetDef e -> e - | _ -> lexp_fatal loc "The macro cannot be expanded"; + let lxp = try env_lookup_expr ctx ((loc, name), idx) (* with + | e -> e + | _ -> lexp_fatal loc "The macro cannot be expanded"; *) with Not_found -> lexp_fatal loc (name ^ " was found but " ^ (string_of_int idx) ^ " is not a correct index.") in @@ -544,8 +544,7 @@ and lexp_read_pattern pattern exp target ctx: let idx = senv_lookup name ctx in match (env_lookup_expr ctx ((loc, name), idx)) with (* We are matching a constructor *) - | LetDef Cons _ -> - (name, loc, []), ctx + | Cons _ -> (name, loc, []), ctx (* name is defined but is not a constructor *) (* it technically could be ... (expr option) *) @@ -664,11 +663,13 @@ and _lexp_decls decls ctx i: (((vdef * lexp * ltype) list) * lexp_context) = (* merge type and expr *) let decls = List.fold_left (fun acc key -> - let (l, s, expr, ltp) = SMap.find key !merged in - let expr = match expr with - | Some expr -> expr + let (l, s, lxp, ltp) = SMap.find key !merged in + let lxp = match lxp with + | Some lxp -> lxp | None -> dltype in - ((l, s), expr, ltp)::acc) [] !names in + let ltp = unsusp_all ltp in + let lxp = unsusp_all lxp in + ((l, s), lxp, ltp)::acc) [] !names in decls, ctx @@ -786,31 +787,41 @@ let lexp_parse_all p ctx = _lexp_parse_all p ctx 1 * --------------------------------------------------------- *) (* Make lxp context with built-in types *) -let default_lctx = - (* Empty context *) +let empty_lctx = let lctx = make_lexp_context in let lxp = Builtin((dloc, "Built-in"), type0) in - let lctx = env_extend lctx (dloc, "Built-in") (LetDef lxp) type0 in - - (* Read BTL files *) - let pres = prelex_file (!btl_folder ^ "types.typer") in - let sxps = lex default_stt pres in - let nods = sexp_parse_all_to_list default_grammar sxps (Some ";") in - let pxps = pexp_decls_all nods in - - _parsing_internals := true; - let _, lctx = lexp_p_decls pxps lctx in - _parsing_internals := false; - - (* Once default builtin are set we can populate the predef table *) - List.iter (fun name -> - let idx = senv_lookup name lctx in - let v = Var((dloc, name), idx) in (* - let value = (env_lookup_expr lctx v) in *) - set_predef name (Some v)) predef_name; - (* -- DONE -- *) + env_extend lctx (dloc, "Built-in") (LetDef lxp) type0 + +let default_lctx = + + (* Empty context *) + let lctx = make_lexp_context in + let lxp = Builtin((dloc, "Built-in"), type0) in + let lctx = env_extend lctx (dloc, "Built-in") (LetDef lxp) type0 in + + (* Read BTL files *) + let pres = prelex_file (!btl_folder ^ "types.typer") in + let sxps = lex default_stt pres in + let nods = sexp_parse_all_to_list default_grammar sxps (Some ";") in + let pxps = pexp_decls_all nods in + + _parsing_internals := true; + let _, lctx = lexp_p_decls pxps lctx in + _parsing_internals := false; + + (* Once default builtin are set we can populate the predef table *) + try + List.iter (fun name -> + let idx = senv_lookup name lctx in + let v = Var((dloc, name), idx) in (* + let value = (env_lookup_expr lctx v) in *) + set_predef name (Some v)) predef_name; + (* -- DONE -- *) + lctx + with e -> lctx + (* Make runtime context with built-in types *) let default_rctx = try (from_lctx (default_lctx)) View it on GitLab: https://gitlab.com/monnier/typer/commit/9b3325124caca3c43ed83a2b152abb3f12e…

1 0

Re: [Typer] déclaration lexp_parsing
by Stefan Monnier 21 May '16

21 May '16

> Je ne comprends de quelle lookup il s'agit. Est-ce que cela devrait > ressembler à cela ? > let env_lookup_type ctx (v : vref): lexp = > let (_, idx) = v in > let (_, _, _, ltp) = _env_lookup ctx v in > unsusp_all (Susp (ltp, (S.shift (idx + 1)))) Plus ou moins, oui. Sauf que celui-ci est pour "lookup_type", où il n'y a pas le même problème de récursion, et donc c'est toujours "idx + 1" sans jamais avoir un "offset". Et que le unsusp devra aussi être fait ailleurs de toute façon, donc il n'est pas probablement pas nécessaire de le faire ici. Stefan > 2016-05-20 14:37 GMT-04:00 Stefan Monnier <monnier(a)iro.umontreal.ca>: >> > Voici l'état de l’environnement à l’évaluation: >> >> > | Position | roffset >> > | Nat | 13 | Nat | 1 | inductive_ (dNat) (succ >> > Nat[0]) (zero): Type[30] >> > | zero | 12 | zero | 0 | inductive-cons Nat[0] >> > zero: Nat[0] >> > | succ | 11 | succ | 0 | inductive-cons Nat[1] >> > succ: Nat[0] -> Nat[1] >> > | to-num | 10 | to-num | 1 | lambda (x : Nat[ >> > | one | 9 | one | 0 | (succ[1] zero[2]): >> Nat[1] >> > | two | 8 | two | 0 | (succ[2] one[0]): Nat[1] >> > | three | 7 | three | 0 | (succ[3] two[0]): Nat[1] >> > | plus | 6 | plus | 1 | lambda (x : Nat[7]) -> >> > | n1 | 5 | n1 | 0 | (to-num[4] zero[6]): >> > Int[32] >> > | n2 | 4 | n2 | 0 | (to-num[5] one[4]): >> Int[32] >> > | n3 | 3 | n3 | 0 | (to-num[6] two[4]): >> Int[32] >> > | m1 | 2 | m1 | 0 | (to-num[7] (plus[3] >> > zero[9] two[5])): Int[32] >> > | m2 | 1 | m2 | 0 | (to-num[8] (plus[4] >> two[6] >> > zero[10])): Int[32] >> > | m3 | 0 | m3 | 0 | (to-num[9] (plus[5] >> two[7] >> > one[8])): Int[32] >> >> J'ai pas regardé tout en détail, mais à première vue ça semble OK. >> >> > L'évaluation de `one = succ zero` ne marche pas (retourne l'item 2 du >> > contexte global) >> >> Hmm.. je ne suis pas sûr de comprendre ce que tu entends par >> "L'évaluation de `one = succ zero`". Si tu fait un `lookup "one"` >> (i.e. `lookup #9`) dans l'environnement ci-dessus, tu devrais obtenir >> qqch de la forme >> >> Susp (S.shift 10) (succ[1] zero[2]) >> >> Et si tu utilises "unsusp" assez de fois, cela devrait se réduire à >> >> (succ[11] zero[12]) >> >> > Pour résoudre le problème il faudrait garder en mémoire le chemin >> d’accès. >> > i.e one[9] -> (9 + zero[2]) + 1 = 12 >> >> Le "Susp" ajouté par le "lookup" devrait faire ce travail. >> >> >> Stefan >> > -- > Pierre Delaunay

1 0

déclaration lexp_parsing
by Pierre Delaunay 20 May '16

20 May '16

Bonjour, je viens d'ajouter le commit qui implémente le parsing des déclarations comme nous en avons parlé, aujourd'hui. Comme attendu, cela ne marche pas. Voici l'état de l’environnement à l’évaluation: | Position | roffset | Nat | 13 | Nat | 1 | inductive_ (dNat) (succ Nat[0]) (zero): Type[30] | zero | 12 | zero | 0 | inductive-cons Nat[0] zero: Nat[0] | succ | 11 | succ | 0 | inductive-cons Nat[1] succ: Nat[0] -> Nat[1] | to-num | 10 | to-num | 1 | lambda (x : Nat[ | one | 9 | one | 0 | (succ[1] zero[2]): Nat[1] | two | 8 | two | 0 | (succ[2] one[0]): Nat[1] | three | 7 | three | 0 | (succ[3] two[0]): Nat[1] | plus | 6 | plus | 1 | lambda (x : Nat[7]) -> | n1 | 5 | n1 | 0 | (to-num[4] zero[6]): Int[32] | n2 | 4 | n2 | 0 | (to-num[5] one[4]): Int[32] | n3 | 3 | n3 | 0 | (to-num[6] two[4]): Int[32] | m1 | 2 | m1 | 0 | (to-num[7] (plus[3] zero[9] two[5])): Int[32] | m2 | 1 | m2 | 0 | (to-num[8] (plus[4] two[6] zero[10])): Int[32] | m3 | 0 | m3 | 0 | (to-num[9] (plus[5] two[7] one[8])): Int[32] L'évaluation de `one = succ zero` ne marche pas (retourne l'item 2 du contexte global) Pour résoudre le problème il faudrait garder en mémoire le chemin d’accès. i.e one[9] -> (9 + zero[2]) + 1 = 12 Est-ce que vous avez des proposition pour faire cela ? -- Pierre Delaunay

2 1

[Git][monnier/typer][master] lexp_p_decls qui ne marche pas
by Setepenre 20 May '16

20 May '16

Setepenre pushed to branch master at Stefan / Typer Commits: 18d7aa8d by Pierre Delaunay at 2016-05-20T12:58:17-04:00 lexp_p_decls qui ne marche pas - - - - - 4 changed files: - samples/quote.typer - src/debruijn.ml - src/eval.ml - src/lparse.ml Changes: ===================================== samples/quote.typer ===================================== --- a/samples/quote.typer +++ b/samples/quote.typer @@ -5,19 +5,41 @@ 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"]) +% +% f = node_ "*" cons (x, cons (symbol_ "x") nil)) +% +% +% => x + +% the expression needs to be handled +has-uquote : List Sexp -> Sexp; +has-uquote = lambda y -> + head Sexp y; %node_ (symbol_ "node_") (quote' y); + +% 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); + + % traverse nodes node : Sexp -> List Sexp -> Sexp; -node = (lambda (op : Sexp) -> - lambda (y : List Sexp) -> - case y - | nil => node_ op nil - | _ => node_ (quote' (cons op nil)) (quote' y)); +node = lambda (op : Sexp) -> + lambda (y : List Sexp) -> + case (sexp_eq op (symbol_ "uquote")) + | True => has-uquote y + | False => hasnot-uquote op y; - | uquote => node_ (symbol_ "node_") (cons (quote' op) - (cons (reconstruire la liste en sexp) nil)) % tree traversal -quote' : List Sexp -> List Sexp; quote' = lambda (x : List Sexp) -> let target = head Sexp x; tl = tail Sexp x; @@ -36,13 +58,6 @@ quote' = lambda (x : List Sexp) -> quote = Macro_ (lambda (x : List Sexp) -> head Sexp (quote' x)); - -% Should it return -% (node_ (symbol_ "_*_") (cons (symbol_ x) (cons (symbol_ x) nil))) - -% OR -% x * x (Lexp, donc Call(_*_, [x x]) - -%main = quote (x * x); +mn = quote (x * x); ===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -126,7 +126,7 @@ let env_add_var_info var (ctx: lexp_context) = let env_extend (ctx: lexp_context) (def: vdef) (v: varbind) (t: lexp) = let ((n, map), e, f) = ctx in - env_add_var_info (n, Some def, v, t) (senv_add_var def ctx) + env_add_var_info (0, Some def, v, t) (senv_add_var def ctx) let _name_error loc estr str = @@ -167,8 +167,11 @@ let _env_lookup ctx (v: vref): env_elem = let env_lookup_type ctx (v : vref) = + (* let ((csize, _), _, _) = ctx in *) (* FIXME: We need to S.shift here, since `t` is valid in the context in * which `vref` appeared, rather than in `ctx`. *) + + let (_, _, _, t) = _env_lookup ctx v in t let env_lookup_expr ctx (v : vref) = @@ -179,4 +182,74 @@ let env_lookup_expr ctx (v : vref) = let env_lookup_by_index index (ctx: lexp_context): env_elem = (Myers.nth index (_get_env ctx)) +(* replace an expression by another *) +(* Most of the time it should be O(1) but it can be O(n) *) +let replace_by ctx name by = + let (a, env, b) = ctx in + let idx = senv_lookup name ctx in + (* lookup and replace *) + let rec replace_by' ctx by acc = + match ctx with + | Mnil -> debruijn_error dummy_location + ("Replace error. This expression does not exist: " ^ name) + | Mcons((_, Some (b, n), _, _) as elem, tl1, i, tl2) -> + if n = name then + (cons by tl1), acc + else + (* Skip some elements if possible *) + if idx < i then replace_by' tl1 by (elem::acc) + else replace_by' tl2 by (elem::acc) + (* replace_by' tl1 by (elem::acc) *) in + + let nenv, decls = replace_by' env by [] in + (* add old declarations *) + 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/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -317,7 +317,7 @@ let from_lctx (ctx: lexp_context): runtime_env = let ((n, _), env, _) = ctx in let rctx = ref make_runtime_ctx in - let bsize = 0 in (*skip the first Built-in function (useless) *) + let bsize = 0 in let csize = n - 1 in (* add all variables *) @@ -336,17 +336,18 @@ let from_lctx (ctx: lexp_context): runtime_env = try let j = diff - i (* - 1 *) in let name, exp = match Myers.nth (csize - i) env with - | (_, Some (_, name), LetDef exp, _) -> name, Some exp - | _ -> "", None in + | (_, Some (_, name), LetDef exp, _) -> Some name, Some exp + | _ -> None, None in let vxp = match exp with | Some lxp -> let lxp = (erase_type lxp) in (try (eval lxp !rctx) - with e -> elexp_print lxp; raise e) + with e -> elexp_print lxp; + print_string "\n"; raise e) | None -> Vdummy in - rctx := set_rte_variable j (Some name) vxp (!rctx) + rctx := set_rte_variable j name vxp (!rctx) with Not_found -> print_int n; print_string " "; ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -66,10 +66,12 @@ let lexp_fatal = msg_fatal "LPARSE" let _global_lexp_ctx = ref make_lexp_context let _global_lexp_trace = ref [] let _parsing_internals = ref false +let _shift_glob = ref 0 let btl_folder = ref "./btl/" (* 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 *) + let _type_shift tp i = match tp with | Var(v, idx) -> Var(v, idx) @@ -119,6 +121,9 @@ let build_var name ctx = let get_type0 ctx = build_var "Type" ctx let get_int ctx = build_var "Int" ctx +(* shift all variables by an offset *) +let senv_lookup name ctx = + senv_lookup name ctx + !_shift_glob let rec lexp_p_infer (p : pexp) (ctx : lexp_context): lexp * ltype = _lexp_p_infer p ctx 1 @@ -143,7 +148,7 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = (* Symbol i.e identifier *) | Pvar (loc, name) ->( - try let idx = senv_lookup name ctx in + try let idx = (senv_lookup name ctx) in let lxp = (make_var name idx loc) in (* search type *) @@ -376,8 +381,10 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = let loc = pexp_location fun_name in let from_lctx ctx = try (from_lctx ctx) - with e -> - lexp_fatal loc "Could not convert lexp context into rte context" in + with e ->( + lexp_error loc "Could not convert lexp context into rte context"; + print_eval_trace (); + raise e) in (* consume Arrows and args together *) let rec get_return_type name i ltp args = @@ -624,92 +631,46 @@ 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_decls decls ctx i: (((vdef * lexp * ltype) list) * lexp_context) = - let tctx = ctx in - let forw = SMap.empty in + let names = ref [] in + let offset = ref 0 in let merged = ref SMap.empty in - let acc = ref [] in - let idx = ref 0 in - - let rec process_decl tctx decl1 decl2 = - match decl1, decl2 with - (* identifier : type; - * identifier : expr; *) - | Ptype((l, s1), ptp), Some Pexpr((_, s2), pxp) when s1 = s2 -> - let ltp, _ = lexp_p_infer ptp tctx in - let octx = env_extend tctx (l, s1) ForwardRef ltp in - let lxp = lexp_p_check pxp ltp octx in - acc := (ref (s1, l, Some pxp, Some ptp))::!acc; - let tctx = env_extend tctx (l, s1) (LetDef lxp) ltp in - tctx, 2 - - (* Foward declaration *) - | Ptype((l, s), ptp), _ -> - let ltp, _ = lexp_p_infer ptp tctx in - acc := (ref (s, l, None, Some ptp))::!acc; - merged := SMap.add s (List.hd !acc) !merged; - let tctx = env_extend tctx (l, s) ForwardRef ltp in - tctx, 1 - - (* infer *) - | Pexpr((l, s), pxp), _ ->( - try let value = SMap.find s !merged in - let _ = (match !value with - | (s, l, None, Some ptp) -> - let ltp, _ = lexp_p_infer ptp tctx in - let lxp = lexp_p_check pxp ltp tctx in - value := (s, l, Some pxp, Some ptp); - | (s, l, Some _, _) -> - lexp_warning l "Declaration override are not allowed" - | _ -> typer_unreachable "Empty declaration") in - tctx, 1 - with Not_found -> - let lxp, ltp = lexp_p_infer pxp tctx in - acc := (ref (s, l, Some pxp, None))::!acc; - let tctx = env_extend tctx (l, s) (LetDef lxp) ltp in - tctx, 1) - - | Pmcall(s, sargs), _ -> - let decls = lexp_decls_macro s sargs tctx in - let tctx = foldvar tctx decls in - tctx, 1 - - and foldvar tctx decls = - match decls, decls with - | p1::p2::tl2, _::tl1 -> - let tctx, v = process_decl tctx p1 (Some p2) in - idx := !idx + 1; - if v = 2 then foldvar tctx tl2 else foldvar tctx tl1 - - | p1::[], _ -> - let tctx, v = process_decl tctx p1 None in - idx := !idx + 2; - tctx - | [], _ -> tctx in - - let tctx = foldvar tctx decls in - let merged_decls = List.rev !acc in - let acc, ctx = - List.fold_left (fun (acc, ctx) rf -> - let (s, l, opxp, optp) = ! rf in - match opxp, optp with - | Some pxp, Some ptp -> - let ltp, _ = lexp_p_infer ptp tctx in - let lxp = lexp_p_check pxp ltp tctx in - let acc = ((l, s), lxp, ltp)::acc in - acc, (env_extend ctx (l, s) (LetDef lxp) ltp) - - | Some pxp, _ -> - let lxp, ltp = lexp_p_infer pxp tctx in - ((l, s), lxp, ltp)::acc, (env_extend ctx (l, s) (LetDef lxp) ltp) - - | None, Some ptp -> - lexp_warning l "Unused variable"; - let ltp, _ = lexp_p_infer ptp tctx in - ((l, s), dlxp, ltp)::acc, (env_extend ctx (l, s) ForwardRef ltp) - - | _ -> typer_unreachable "No type no expression") ([], ctx) merged_decls in - List.rev acc, ctx + let ctx = List.fold_left (fun vctx expr -> + match expr with + | Pexpr ((l, s), pxp) ->( + try let idx = senv_lookup s vctx in + let ltp = env_lookup_type vctx ((l, s), idx) in + let lxp = lexp_p_check pxp ltp vctx in + let (_, _, _, ltp) = SMap.find s !merged in + merged := SMap.add s (l, s, Some lxp, ltp) !merged; + let r = !offset in + offset := 0; + replace_by vctx s (r, Some (l, s), (LetDef lxp), ltp); + + with Not_found -> + let lxp, ltp = lexp_p_infer pxp vctx in + names := s::!names; + merged := SMap.add s (l, s, Some lxp, ltp) !merged; + env_extend vctx (l, s) (LetDef lxp) ltp) + + | Ptype ((l, s), ptp) -> + offset := !offset + 1; + let ltp, _ = lexp_p_infer ptp vctx in + names := s::!names; + merged := SMap.add s (l, s, None, ltp) !merged; + env_extend vctx (l, s) ForwardRef ltp + + | _ -> vctx) ctx decls in + + (* merge type and expr *) + let decls = List.fold_left (fun acc key -> + let (l, s, expr, ltp) = SMap.find key !merged in + let expr = match expr with + | Some expr -> expr + | None -> dltype in + ((l, s), expr, ltp)::acc) [] !names in + + decls, ctx and _lexp_parse_all (p: pexp list) (ctx: lexp_context) i : lexp list = @@ -731,7 +692,8 @@ and print_lexp_ctx (ctx : lexp_context) = (Some ('l', 10), "NAME"); (Some ('l', 7), "INDEX"); (Some ('l', 10), "NAME"); - (Some ('l', 36), "VALUE:TYPE")]; + (Some ('l', 4), "OFF"); + (Some ('l', 32), "VALUE:TYPE")]; print_string (make_sep '-'); @@ -762,14 +724,16 @@ and print_lexp_ctx (ctx : lexp_context) = let ptr_str = "" in (*" | | | | " in *) - try let name, exp, tp = + try let r, name, exp, tp = match env_lookup_by_index (n - idx - 1) ctx with - | (_, Some (_, name), LetDef exp, tp) -> name, Some exp, tp - | _ -> "", None, dltype in + | (r, Some (_, name), LetDef exp, tp) -> r, name, Some exp, tp + | _ -> 0, "", None, dltype in (* Print env Info *) lalign_print_string name 10; (* name must match *) print_string " | "; + lalign_print_int r 4; + print_string " | "; let _ = (match exp with | None -> print_string "<var>" @@ -851,6 +815,7 @@ let default_lctx = let default_rctx = try (from_lctx (default_lctx)) with e ->( + print_eval_trace (); lexp_error dloc "Could not convert lexp context into rte context"; raise e) View it on GitLab: https://gitlab.com/monnier/typer/commit/18d7aa8dcbd5c04d7ad711ca2d1d3872055…

1 0