Setepenre pushed to branch master at Stefan / Typer

Commits: bd6f086b by Pierre Delaunay at 2016-09-01T16:05:48-04:00 updated macro handling. implemented type_ macro. attributes are not working

Changes to be committed: * modified: btl/types.typer * modified: src/builtin.ml * modified: src/lparse.ml - updated macro handling * new file: samples/inductive.typer - type_ macro implementation

- - - - -

4 changed files:

- btl/types.typer - + samples/inductive.typer - src/builtin.ml - src/lparse.ml

Changes:

===================================== btl/types.typer ===================================== --- a/btl/types.typer +++ b/btl/types.typer @@ -139,16 +139,16 @@ bind = Built-in "bind" ( FileHandle = Built-in "FileHandle";

% define operation on file handle +%% runIO should have type IO Unit -> b -> b +%% or IO a -> b -> b, which means "run the IO, throw away the result, +%% and then return the second argument unchanged". The "dummy" b argument +%% is actually crucial to make sure the result of runIO is used, otherwise +%% the whole call would look like a dead function call and could be +%% optimized away! run-io = Built-in "run-io" ( - %% FIXME: runIO should have type IO Unit -> b -> b - %% or IO a -> b -> b, which means "run the IO, throw away the result, - %% and then return the second argument unchanged". The "dummy" b argument - %% is actually crucial to make sure the result of runIO is used, otherwise - %% the whole call would look like a dead function call and could be - %% optimized away! (a : Type) ≡> (b : Type) ≡> - IO a -> (a -> IO b) -> (IO b) -> Unit); + IO a -> b -> b);

open = Built-in "open" (String -> String -> IO FileHandle); write = Built-in "write" (FileHandle -> String -> IO Unit);

===================================== samples/inductive.typer ===================================== --- /dev/null +++ b/samples/inductive.typer @@ -0,0 +1,46 @@ +type-impl = lambda (x : List Sexp) -> + % x follow the mask -> (_|_ Nat zero (succ Nat)) + % Type name --^ ^------^ constructors + + % Get expression + let expr = head (a := Sexp) x in + let sexp_nil = nil (a := Sexp) in + + % Expression is node_ (symbol_ "|") (list) + % we only care about the list bit + + let get-list = (lambda (node : Sexp) -> + sexp_dispatch_ (a := List Sexp) node + (lambda (op : Sexp) -> (lambda (lst : List Sexp) -> lst)) % Nodes + (lambda (str : String) -> sexp_nil) % Symbol + (lambda (str : String) -> sexp_nil) % String + (lambda (int : Int) -> sexp_nil) % Integer + (lambda (float : Float) -> sexp_nil) % Float + (lambda (lst : List Sexp) -> sexp_nil)) in % List of Sexp + + let lst = get-list expr in + + let name = head (a := Sexp) lst in + let ctor = tail (a := Sexp) lst in + + % Create a forward declaration in case the declaration is recursive + let fdecl = node_ (symbol_ "_:_") + (cons (a := Sexp) name + (cons (a := Sexp) (symbol_ "Type") sexp_nil)) in + + % Create the inductive type definition + let inductive = node_ (symbol_ "inductive_") + (cons (a := Sexp) (symbol_ "dlabel") ctor) in + + let decl = node_ (symbol_ "_=_") + (cons (a := Sexp) name + (cons (a := Sexp) inductive sexp_nil)) in + + cons (a := Sexp) fdecl + (cons (a := Sexp) decl sexp_nil); + +type_ = Macro_ type-impl; + +type Nat + | zero + | succ Nat;

===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -56,28 +56,44 @@ let predef_name = [ "True"; "False"; "Bool"; + "Macro"; ]

let builtin_size = ref 0

-let predef_map : predef_table = +let default_predef_map : predef_table = (* add predef name, expr will be populated when parsing *) List.fold_left (fun m name -> SMap.add name (ref None) m) SMap.empty predef_name

+let predef_map = ref default_predef_map + let get_predef_raw (name: string) : lexp = - match !(SMap.find name predef_map) with + match !(SMap.find name (!predef_map)) with | Some exp -> exp | None -> builtin_error dloc "Try to access an empty predefined"

-let get_predef name ctx = - let r = (get_size ctx) - !builtin_size in - let v = mkSusp (get_predef_raw name) (S.shift r) in - v +let get_predef_option (name: string) ctx = + let r = (get_size ctx) - !builtin_size - 1 in + match !(SMap.find name (!predef_map)) with + | Some exp -> Some (mkSusp exp (S.shift r)) + | None -> None

+let get_predef (name: string) ctx = + let r = (get_size ctx) - !builtin_size - 1 in + let p = get_predef_raw name in + (mkSusp p (S.shift r))

let set_predef name lexp = - SMap.find name predef_map := lexp + SMap.find name (!predef_map) := lexp + +let dump_predef () = + let _ = SMap.iter (fun key item -> + print_string key; print_string " "; + let _ = match !item with + | Some lxp -> lexp_print lxp + | None -> print_string "None"; in + print_string "\n") !predef_map in ()

(* Builtin types *) let dloc = dummy_location @@ -164,13 +180,11 @@ let olist2tlist_rte lst = (* Typer list to Ocaml list *) let rec tlist2olist acc expr = match expr with - | Vcons((_, "cons"), [hd; tl]) -> - tlist2olist (hd::acc) tl + | Vcons((_, "cons"), [hd; tl]) -> tlist2olist (hd::acc) tl | Vcons((_, "nil"), []) -> List.rev acc | _ -> print_string (value_name expr); print_string "\n"; value_print expr; - builtin_error dloc "List conversion failure'"

let make_node loc depth args_val ctx = @@ -313,6 +327,8 @@ let has_attribute_impl loc largs ctx ftype =

let b = has_property ctx (vi, vn) (ai, an) in

+ + let rvar = if b then get_predef "True" ctx else get_predef "False" ctx in rvar, (get_predef "Bool" ctx)

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -446,7 +446,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = let ptp = pexp_parse stp in let ltp, _ = _lexp_p_infer ptp ctx (i + 1) in Builtin((loc, str), ltp), ltp - + | true, _ -> lexp_error loc "Wrong Usage of "Built-in""; dlxp, dltype @@ -454,65 +454,71 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = | false, _ -> lexp_error loc "Use of "Built-in" in user code"; dlxp, dltype) - + | e -> (* Process Arguments *) let largs, ret_type = handle_fun_args [] sargs ltp in Call (body, List.rev largs), ret_type in

- let handle_macro_call (loc, name) = - (* check for builtin *) - match is_builtin_macro name with - | true -> - let pargs = List.map pexp_parse sargs in - let largs = _lexp_parse_all pargs ctx i in - (get_macro_impl loc name) loc largs ctx ltp - - (* user defined macro *) - | false ->( - (* Get the macro *) - let lxp = match OL.lexp_whnf body ctx with - | Call(Var((_, "Macro_"), _), [(_, fct)]) -> fct - | lxp -> - 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 = OL.erase_type lxp in - let rctx = (from_lctx ctx 0) 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 + let handle_macro_call () = + (* Get the macro *) + let lxp = match OL.lexp_whnf body ctx with + | Call(Var((_, "Macro_"), _), [(_, fct)]) -> fct + | lxp -> + 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 = OL.erase_type lxp in + let rctx = (from_lctx ctx 0) 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 + + (* This is the builtin Macro type *) + let macro_type = match get_predef_option "Macro" ctx with + | Some lxp -> lxp + (* When type.typer is being parsed and the predef is not yet + * available *) + | None -> dltype in

(* determine function type *) match func, ltp with - (* FIXME: Rather than check a var name, define a builtin for it. *) - (* FIXME: Don't force func to be a Pvar. *) - | (Pvar (l, n), Var((_, "Macro"), _)) -> handle_macro_call (l, n) - (* FIXME: Handle special-forms here as well! *) - | _ -> handle_funcall () + | macro, _ when OL.conv_p ltp macro_type -> ( + match macro with + (* Special form *) + | Pvar(l, name) when is_builtin_macro name -> + let pargs = List.map pexp_parse sargs in + let largs = _lexp_parse_all pargs ctx i in + (get_macro_impl loc name) loc largs ctx ltp + + (* true macro *) + | _ -> handle_macro_call ()) + + (* FIXME: Handle special-forms here as well! *) + | _ -> handle_funcall ()

(* Read a pattern and create the equivalent representation *) @@ -645,6 +651,8 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * lexp_context) = (* get a list of declaration *) let decls = eval elexp rctx in

+ value_print decls; print_string "\n"; + (* convert typer list to ocaml *) let decls = tlist2olist [] decls in

@@ -652,7 +660,10 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * lexp_context) = let decls = List.map (fun g -> match g with | Vsexp(sxp) -> sxp - | _ -> lexp_fatal loc "Macro expects sexp list") decls in + | _ -> + print_string ((value_name g) ^ " : "); + value_print g; print_string "\n"; + lexp_fatal loc "Macro expects sexp list") decls in

(* read as pexp_declaraton *) pexp_decls_all decls, ctx) @@ -788,7 +799,7 @@ and _lexp_rec_decl decls ctx i = | 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 forward ref by its true value *) replace_by vctx s (n - !i, Some (l, s), LetDef lxp, ltp)

(* lexp check *) @@ -963,6 +974,7 @@ let default_lctx, default_rctx = (* -- DONE -- *) lctx with e -> + lexp_warning dloc "Predef not found"; lctx in let rctx = make_runtime_ctx in let rctx = eval_decls_toplevel (List.map OL.clean_decls d) rctx in

View it on GitLab: https://gitlab.com/monnier/typer/commit/bd6f086bd0d6749404c23a2dfc2cb1dd028d...