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/e2a13504bc9dcd5154b26f63a51b0f8900d6...