Setepenre pushed to branch master at Stefan / Typer

Commits: c36053c2 by Pierre at 2016-06-03T19:03:38+02:00 fix susp errors, added Monad type definition

- - - - - 053a0f36 by Pierre Delaunay at 2016-06-03T14:35:47-04:00 Added monads

Changes to be committed: * src/lparse.ml * src/eval.ml - added (bind impl) * src/builtin.ml - added (open/read/write _impl)

- - - - - d397b4c1 by Pierre at 2016-06-03T14:38:27-04:00 bugguy

- - - - - ac1f5998 by Pierre Delaunay at 2016-06-03T14:39:53-04:00 resolved file permission issue + merging

- - - - -

9 changed files:

- btl/types.typer - src/builtin.ml - src/debruijn.ml - src/debug_util.ml - src/env.ml - src/eval.ml - src/lparse.ml - tests/eval_test.ml - + w_file

Changes:

===================================== btl/types.typer ===================================== --- a/btl/types.typer +++ b/btl/types.typer @@ -39,6 +39,7 @@ Int = Built-in "Int"; Float = Built-in "Float"; String = Built-in "String"; Sexp = Built-in "Sexp"; +Unit = Built-in "Unit";

% Basic operators _+_ = Built-in "_+_" (Int -> Int -> Int); @@ -114,9 +115,29 @@ sexp_dispatch_ = Built-in "sexp_dispatch_" (Sexp -> Sexp);

+% ----------------------------------------------------- +% Monads +% ----------------------------------------------------- + +IO = Built-in "IO" (Type -> Type); + +% Builtin bind +bind = Built-in "bind" ( + (a : Type) ≡> + (b : Type) ≡> + IO a -> (a -> IO b) -> (IO b)); + +% return = Built-in "return" ((a : Type) ≡> a -> IO a);

+% File monad

+% define a dummy type that supposed to represent a file +FileHandle = Built-in "FileHandle";

+% define operation on file handle +open = Built-in "open" (String -> String -> IO FileHandle); +write = Built-in "write" (FileHandle -> String -> IO Unit); +read = Built-in "read" (FileHandle -> Int -> IO String);

===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -38,7 +38,7 @@ open Lexp

open Debruijn open Env (* get_rte_variable *) - +open Printf

let builtin_error loc msg = msg_error "BUILT-IN" loc msg; @@ -228,6 +228,44 @@ let sexp_eq loc args_val ctx = | _ -> tfalse) | _ -> builtin_error loc "int_eq expects 2 sexp"

+ +let open_impl loc args_val ctx = + + let file, mode = match args_val with + | [Vstring(file_name); Vstring(mode)] -> file_name, mode + | _ -> builtin_error loc "open expects 2 strings" in + + (* open file *) (* return a file handle *) + match mode with + | "r" -> Vin(open_in file) + | "w" -> Vout(open_out file) + | _ -> builtin_error loc "wrong open mode" + + +let read_impl loc args_val ctx = + + let channel = match args_val with + | [Vin(c); _] -> c + | _ -> + List.iter (fun v -> value_print v; print_string "\n") args_val; + builtin_error loc "read expects a in_channel" in + + let line = input_line channel in + Vstring(line) + +let write_impl loc args_val ctx = + + let channel, msg = match args_val with + | [Vout(c); Vstring(msg)] -> c, msg + | _ -> + List.iter (fun v -> value_print v) args_val; + builtin_error loc "read expects a out_channel" in + + fprintf channel "%s" msg; + Vdummy + + + (* * Should we have a function that * -> returns a new context inside typer ? (So we need to add a ctx type too) @@ -237,10 +275,6 @@ let sexp_eq loc args_val ctx = * -> ou seulement: 'eval expr ctx' *)

- - - - let is_lbuiltin idx ctx = let bsize = 1 in let csize = get_size ctx in

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -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 - (Susp (ltp, (S.shift (idx + 1)))) + mkSusp ltp (S.shift (idx + 1))

let env_lookup_expr ctx (v : vref): lexp = let (_, idx) = v in @@ -179,18 +179,7 @@ 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"; * ) - - )); *) - (*let idx = if r > 0 then idx - r else idx + 1 in *) - - (Susp (lxp, (S.shift (idx - r + 1)))) + mkSusp lxp (S.shift (idx + 1 - r))

let env_lookup_by_index index (ctx: lexp_context): env_elem = (Myers.nth index (_get_env ctx))

===================================== src/debug_util.ml ===================================== --- a/src/debug_util.ml +++ b/src/debug_util.ml @@ -323,8 +323,20 @@ let main () = (if (get_p_option "lctx") then( print_lexp_ctx nctx; print_string "\n"));

+ + (* + List.iter (fun ((_, n), lxp, _) -> + print_string n; print_string "\n") + (List.flatten lexps); *) + let clean_lxp = EL.clean_toplevel lexps in

+ (* + List.iter (fun ((_, n), lxp) -> + print_string n; print_string "\n"; + ) (List.flatten clean_lxp); + *) + (* Eval declaration *) let rctx = default_rctx in print_string yellow;

===================================== src/env.ml ===================================== --- a/src/env.ml +++ b/src/env.ml @@ -59,6 +59,8 @@ type value_type = | Vsexp of sexp (* Values passed to macros. *) (* Unable to eval during macro expansion, only throw if the value is used *) | Vdummy + | Vin of in_channel + | Vout of out_channel

let rec value_print (vtp: value_type) = match vtp with @@ -76,6 +78,9 @@ let rec value_print (vtp: value_type) =

| Vbuiltin(str) -> print_string str | Vdummy -> print_string "value_print_dummy" + | Vin _ -> print_string "in_channel" + | Vout _ -> print_string "out_channel" + | _ -> print_string "debug print"

let value_location (vtp: value_type) = match vtp with

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -225,7 +225,28 @@ and typer_builtins_impl = [ ("int_eq" , int_eq); ("sexp_eq" , sexp_eq); ("eval_" , typer_eval); + ("open" , open_impl); + ("bind" , bind_impl); + ("read" , read_impl); + ("write" , write_impl); + ] +and bind_impl loc args_val ctx = + + let io, cb = match args_val with + | [io; callback] -> io, callback + | _ -> builtin_error loc "bind expects two arguments" in + + (* get callback *) + let body, ctx = match cb with + | Closure(_, body, ctx) -> body, ctx + | _ -> builtin_error loc "A Closure was expected" in + + (* add evaluated IO to arg list *) + let nctx = add_rte_variable None io ctx in + + (* eval callback *) + _eval body nctx 0

and typer_eval loc args ctx = let arg = match args with @@ -248,7 +269,7 @@ and get_builtin_impl str loc =

try SMap.find str !_builtin_lookup with Not_found -> - eval_error loc "Requested Built-in does not exist" + eval_error loc ("Requested Built-in "" ^ str ^ "" does not exist")

(* Sexp -> (Sexp -> List Sexp -> Sexp) -> (String -> Sexp) -> (String -> Sexp) -> (Int -> Sexp) -> (Float -> Sexp) -> (List Sexp -> Sexp)

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -560,7 +560,17 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = (* Constructor. This case is rarely used *) | (Pcons(_, v), _) -> handle_named_call v

- | e, _ -> lexp_fatal (pexp_location e) "This expression cannot be called" + | Pcall(fct, sargs2), ltp -> + let pargs = List.map pexp_parse sargs in + let largs = _lexp_parse_all pargs ctx i in + let new_args = List.map (fun g -> (Aexplicit, g)) largs in + let body, ltp = lexp_call fct sargs2 ctx (i + 1) in + Call(body, new_args), ltp + + | e, _ -> + pexp_print e; print_string "\n"; + print_string ((pexp_to_string e) ^ "\n"); + lexp_fatal (pexp_location e) "This expression cannot be called"

(* Read a pattern and create the equivalent representation *) @@ -743,6 +753,7 @@ and _lexp_decls decls ctx i: (((vdef * lexp * ltype) list list) * lexp_context) offset := 1);

recursive_mode := true; + names := [s]::!names; mut := s::!mut;

(* get type *)

===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -286,7 +286,6 @@ let _ = (add_test "EVAL" "Mutually Recursive Definition" (fun () -> two = (succ one); three = (succ two);

- odd : Nat -> Int; even : Nat -> Int; odd = lambda (n : Nat) -> case n | zero => 0

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

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