Jonathan Graveline pushed to branch graveline at Stefan / Typer

Commits: abda0e39 by Jonathan Graveline at 2018-06-21T16:28:58Z macro do in pervasive; test for macro do; some change on macro case

- - - - - eb8acb50 by Jonathan Graveline at 2018-06-21T16:30:52Z Merge branch 'graveline' of https://gitlab.com/monnier/typer into graveline

- - - - - cec64f4a by Jonathan Graveline at 2018-06-21T16:57:44Z After last merge symbol "_" in macro do need to be declared

- - - - - a8a77d78 by Jonathan Graveline at 2018-06-22T20:45:23Z New type Elab_Context and functions Elab_getenv, Elab_isbound, Elab_isconstructor

- - - - -

11 changed files:

- btl/builtins.typer - btl/pervasive.typer - samples/case.typer - samples/do.typer - src/builtin.ml - src/debruijn.ml - src/elab.ml - src/env.ml - src/eval.ml - + tests/elabctx_test.ml - + tests/macro_do_test.ml

Changes:

===================================== btl/builtins.typer ===================================== @@ -242,4 +242,13 @@ Ref_write = Built-in "Ref.write" : (a : Type) ≡> a -> Ref a -> IO Unit;

gensym = Built-in "gensym" : Unit -> IO Sexp;

+%% Function on Elab_Context + +Elab_getenv = Built-in "Elab.getenv" : Unit -> IO Elab_Context; + +Elab_isbound = Built-in "Elab.isbound" : String -> Elab_Context -> IO Int; + +Elab_isconstructor = Built-in "Elab.isconstructor" + : String -> Elab_Context -> IO Int; + %%% builtins.typer ends here.

===================================== btl/pervasive.typer ===================================== @@ -413,4 +413,94 @@ test4 : Option Int; test4 = test1 : Option ?; test3 = test4;

+%%%% +%%%% Macro : do +%%%% + +assign = Sexp_symbol "<-"; + +get-sym : Sexp -> Sexp; +get-sym sexp = let + + dflt-sym = (lambda _ -> Sexp_symbol "(_ : IO Unit)"); + + in Sexp_dispatch sexp + + ( lambda s ss -> if_then_else_ (Sexp_eq (List_nth 0 ss Sexp_error) assign) + (s) + (dflt-sym ()) + ) + + dflt-sym dflt-sym dflt-sym + dflt-sym dflt-sym; % there must be a command + +get-op : Sexp -> Sexp; +get-op sexp = let + + as-is = lambda _ -> sexp; + + helper = (lambda sexp -> Sexp_dispatch sexp + + ( lambda s ss -> if_then_else_ (Sexp_eq (List_nth 0 ss Sexp_error) assign) + (Sexp_node (List_nth 1 ss Sexp_error) (List_tail (List_tail ss))) + (Sexp_node s ss) + ) + + as-is as-is as-is as-is as-is + ); + + op = (helper sexp); + +in if_then_else_ (Sexp_eq op (Sexp_symbol "")) Sexp_error op; + +get-decl : List Sexp -> List Sexp; +get-decl args = let + + err = lambda _ -> cons Sexp_error nil; + + % Expecting a Block of command separated by ";" + + node = Sexp_dispatch (List_nth 0 args Sexp_error) + + (lambda _ _ -> cons Sexp_error nil) err err err err + + (lambda l -> Parser_default l); + +in node; + +%% +%% The idea of the macro is : +%% +%% IO_bind a-op (lambda a-sym -> [next command or return a-sym]) +%% IO_bind a-op (lambda a-sym -> (IO_bind b-op (lambda b-sym -> [next command or return b-sym]))) +%% +%% this way a-sym is defined within b-op and so on +%% a-sym is now just `a` and not `IO a` +%% + +set-fun : List Sexp -> Sexp; +set-fun args = let + + helper : Sexp -> List Sexp -> Sexp; + helper lsym args = case args + | cons s ss => (let + + sym = get-sym s; + + op = get-op s; + + in Sexp_node (Sexp_symbol "IO_bind") (cons (op) + (cons (Sexp_node (Sexp_symbol "lambda_->_") (cons sym (cons (helper sym ss) nil))) nil)) + ) + + | nil => Sexp_node (Sexp_symbol "IO_return") (cons lsym nil); + +in helper (Sexp_symbol "") args; % return Unit if no command given + +%% Serie of command + +do = macro (lambda args -> + (IO_return (set-fun (get-decl args))) +); + %%% pervasive.typer ends here.

===================================== samples/case.typer ===================================== @@ -3,17 +3,28 @@ %%% %%% (pattern matching) %%% +%%% This file may not be up to date with version +%%% in pervasive.typer +%%%

%% -%% Match every variable in each pattern. +%% Match every variable in each pattern with a list of VarTest. +%% +%% VarTest : +%% +%% var_test is (var_test [ctor to match]) %% -%% var_test is (var_test ctor) +%% Push current var n_times for sub test +%% push_var is (push_var n_times) %% -%% Push current var n_times for sub test -%% push_var is (push_var n_times) +%% sub_test introduce a variable for testing sub pattern +%% sub_test is (sub_test [sup. var name] [ctor to match]) %% -%% sub_test introduce a variable for testing sub pattern -%% sub_test is (sub_test sup_var ctor) +%% Pattern : +%% +%% branch is (branch [list of var test] [user fun on match]) +%% +%% dflt_branch is (dflt_branch [user fun]) and always match %%

type VarTest @@ -26,24 +37,27 @@ type Pattern | dflt_branch Sexp;

%% -%% Get matched variable (e.g. case (var1,var2,...) | ...) +%% Get matched expression (e.g. case (var1,var2,...) | ...) +%% +%% Expression are separated by "," so it is useful for +%% case (expr1,expr2,...) ... +%% but also for +%% case ... | (expr3,expr4,...) => ... %%

-get_vars : Sexp -> List Sexp; -get_vars sexp = let +get_exprs : Sexp -> List Sexp; +get_exprs sexp = let

err = (lambda _ -> cons Sexp_error nil);

- get_vars_helper : List Sexp -> List Sexp; - get_vars_helper sexps = case sexps - | (cons s ss) => (case (Sexp_eq (Sexp_symbol "_,_") s) - | true => (ss) % tuple - % constructor or function called (only 1 pattern) - | false => (cons (Sexp_node s ss) nil)) - | nil => (cons (Sexp_symbol "_") nil); + get_exprs_helper : Sexp -> List Sexp -> List Sexp; + get_exprs_helper s ss = case (Sexp_eq (Sexp_symbol "_,_") s) + | true => (ss) % tuple + % constructor or function called (only 1 pattern) + | false => (cons (Sexp_node s ss) nil);

in Sexp_dispatch sexp - (lambda s ss -> (get_vars_helper (cons s ss))) + get_exprs_helper (lambda s -> (cons (Sexp_symbol s) nil)) err err err (lambda ss -> cons ss nil); % do nothing to Block @@ -79,7 +93,7 @@ get_cases sexps = let (lambda s ss -> case (Sexp_eq (Sexp_symbol "_=>_") s) % expecting a Sexp_node as second argument to _=>_ | true => (branch - (List_map (lambda ctor -> var_test ctor) (get_vars (List_nth 0 ss Sexp_error))) + (List_map (lambda ctor -> var_test ctor) (get_exprs (List_nth 0 ss Sexp_error))) (List_nth 1 ss Sexp_error)) | false => (dflt_branch (Sexp_node s ss)))

@@ -108,14 +122,15 @@ rename_nth n ctor sym = let | cons x xs => if_then_else_ (b x) (cons (f x i) (mapiif f b (i + 1) xs)) (cons x (mapiif f b i xs)); - - % cons (f x i) (mapiif f b (if_then_else_ (b x) i (i + 1)) xs);

err = (lambda _ -> Sexp_symbol "<not a ctor (0)>");

%% %% Is argument a variable or a ctor %% + %% (use keyword "ctor" if the ctor has no argument to + %% to differentiate with a variable) + %%

is_ctor : Sexp -> Bool; is_ctor v = Sexp_dispatch v @@ -143,6 +158,7 @@ in IO_return (Sexp_dispatch ctor

%% %% Expand sub pattern into sub_test +%% and optionaly push_var when there's %%

expand_cases : List Pattern -> IO (List Pattern); @@ -191,6 +207,9 @@ expand_cases pats = let expand : VarTest -> IO (List VarTest); expand test = let

+ % I don't expect to use multiple not_unique_sym at the same time + % so the name may be reused + not_unique_sym : Sexp; not_unique_sym = Sexp_symbol " %not gensym% ";

@@ -233,7 +252,7 @@ expand_cases pats = let (IO_bind sub_case (lambda l -> IO_bind all (lambda all -> IO_return (List_concat all l))))

- in expand test); % (List_concat all (cons test nil)); + in expand test);

expand_all : Pattern -> IO Pattern; expand_all p = case p @@ -273,25 +292,25 @@ pattern_to_sexp vars pats = let | (cons v _) => push (n - 1) (cons v vars) | nil => nil);

- chain_ctors_fail : List Sexp -> List VarTest -> Sexp -> Sexp -> Sexp; - chain_ctors_fail vars tests succ fail = case vars + chain_ctors : List Sexp -> List VarTest -> Sexp -> Sexp -> Sexp; + chain_ctors vars tests succ fail = case vars | (cons v vv) => (case tests | (cons t tt) => (case t | (var_test t) => if_then_else_ (Sexp_eq t (Sexp_symbol "_")) - (to_case v t (chain_ctors_fail vv tt succ fail) none) - (to_case v t (chain_ctors_fail vv tt succ fail) (some fail)) + (to_case v t (chain_ctors vv tt succ fail) none) + (to_case v t (chain_ctors vv tt succ fail) (some fail)) | (sub_test v t) => if_then_else_ (Sexp_eq t (Sexp_symbol "_")) - (to_case v t (chain_ctors_fail vars tt succ fail) none) - (to_case v t (chain_ctors_fail vars tt succ fail) (some fail)) - | (push_var n) => (chain_ctors_fail (push n vars) tt succ fail)) + (to_case v t (chain_ctors vars tt succ fail) none) + (to_case v t (chain_ctors vars tt succ fail) (some fail)) + | (push_var n) => (chain_ctors (push n vars) tt succ fail)) | nil => Sexp_error) | nil => (case tests | (cons t tt) => (case t | (var_test _) => Sexp_error | (sub_test v t) => if_then_else_ (Sexp_eq t (Sexp_symbol "_")) - (to_case v t (chain_ctors_fail vars tt succ fail) none) - (to_case v t (chain_ctors_fail vars tt succ fail) (some fail)) - | (push_var n) => (chain_ctors_fail (push n vars) tt succ fail)) + (to_case v t (chain_ctors vars tt succ fail) none) + (to_case v t (chain_ctors vars tt succ fail) (some fail)) + | (push_var n) => (chain_ctors (push n vars) tt succ fail)) | nil => succ);

chain_ctors_nofail : List Sexp -> List VarTest -> Sexp -> Sexp; @@ -315,7 +334,7 @@ pattern_to_sexp vars pats = let one_to_sexp : List Sexp -> Pattern -> Sexp -> Sexp; one_to_sexp vars pat fail = case pat | (dflt_branch f) => f - | (branch tests f) => (chain_ctors_fail vars tests f fail); + | (branch tests f) => (chain_ctors vars tests f fail);

last_to_sexp : List Sexp -> Pattern -> Sexp; last_to_sexp vars pat = case pat @@ -330,6 +349,9 @@ pattern_to_sexp vars pats = let last_test_fun vars pat = (quote (lambda (_ : Unit) -> (uquote (last_to_sexp vars pat))));

+ % Same thing as not_unique_sym, I can reuse the name because + % only the last defined is important + fail_sym : Sexp; fail_sym = Sexp_symbol " %fail sym% ";

@@ -341,8 +363,6 @@ pattern_to_sexp vars pats = let (cons (Sexp_node (Sexp_symbol "_=_") (cons fail_sym (cons (helper vars pats) nil))) nil)) (cons (test_fun vars p fail_sym) nil)) - %(quote (let_in_ (_;_ (_=_ (uquote fail_sym) (uquote (helper vars pats)))) - %(uquote (test_fun vars p fail_sym)))) | nil => (last_test_fun vars p)) | nil => Sexp_error;

@@ -359,12 +379,12 @@ case_ = macro (lambda args -> let | nil => o | cons x xs => foldi f (i + 1) (f x i o) xs;

- case0_ : List Sexp -> IO Sexp; - case0_ args = let + case0 : List Sexp -> IO Sexp; + case0 args = let

vars : List Sexp; vars = case args - | (cons s ss) => get_vars s + | (cons s ss) => get_exprs s | nil => nil;

pats : List Pattern; @@ -385,15 +405,23 @@ case_ = macro (lambda args -> let rvars = List_reverse vars nil;

nfun : Sexp; - nfun = (Sexp_node (foldi - (lambda v i fun -> (quote (lambda_->_ - ((uquote (List_nth i nvars Sexp_error)) : (decltype (uquote v))) - (uquote fun)))) - 0 fun fvars) (List_reverse fvars nil)); + nfun = fun; + + % + % I was using lambda_->_, then ##case_ needed a type so I added decltype, + % then decltype needed variable (rather than composed expression) + % so we end up with a let_in_ (thanks to gensym). + % + % nfun = (Sexp_node (foldi + % (lambda v i fun -> (quote (lambda_->_ + % ((uquote (List_nth i nvars Sexp_error)) : (decltype (uquote v))) + % (uquote fun)))) + % 0 fun fvars) (List_reverse fvars nil)); + %

in IO_return ( (foldi (lambda v i fun -> (quote ( - let (uquote (List_nth i fvars Sexp_error)) = (uquote v); in (uquote fun)))) + let (uquote (List_nth i nvars Sexp_error)) = (uquote v); in (uquote fun)))) 0 nfun vars)); % in IO_return nfun;

@@ -405,18 +433,15 @@ case_ = macro (lambda args -> let

% Only the Sexp after "_|_" are interesting

- case1_ : List Sexp -> IO Sexp; - case1_ args = case args - | (cons s ss) => if_then_else_ (Sexp_eq (Sexp_symbol "_|_") s) - (case0_ ss) - (IO_return Sexp_error) - | nil => IO_return Sexp_error; + case1 : Sexp -> List Sexp -> IO Sexp; + case1 s ss = if_then_else_ (Sexp_eq (Sexp_symbol "_|_") s) + (case0 ss) + (IO_return Sexp_error);

err = (lambda _ -> IO_return Sexp_error);

% Expecting only one Sexp_node containing a case with arguments

in (Sexp_dispatch (List_nth 0 args Sexp_error) - (lambda s ss -> (case1_ (cons s ss))) - err err err err err) + case1 err err err err err) );

===================================== samples/do.typer ===================================== @@ -1,11 +1,14 @@ %%% -%%% Macro : action +%%% Macro : do +%%% +%%% This file may not be up to date with version +%%% in pervasive.typer %%%

%% %% Here's an example : %% -%% fun = action { +%% fun = do { %% str <- return "\n\tHello world!\n\n"; %% print str; %% }; @@ -14,7 +17,7 @@ %% %% fun is a command, %% -%% action may contain action because it returns a command. +%% do may contain do because it returns a command. %%

assign = Sexp_symbol "<-"; @@ -22,7 +25,7 @@ assign = Sexp_symbol "<-"; get-sym : Sexp -> Sexp; get-sym sexp = let

- dflt-sym = (lambda _ -> Sexp_symbol "_"); + dflt-sym = (lambda _ -> Sexp_symbol "(_ : IO Unit)");

in Sexp_dispatch sexp

@@ -99,7 +102,7 @@ in helper (Sexp_symbol "") args; % return Unit if no command given

%% Serie of command

-action = macro (lambda args -> +do = macro (lambda args -> (IO_return (set-fun (get-decl args))) );

@@ -116,13 +119,13 @@ tab = print "\t"; float2string v = IO_return (Float->String v);

%% -%% example0 = action { +%% example0 = do { %% str <- return "\n\tHello world!"; %% print str; %% return 0.0; %% }; %% -%% example1 = action { +%% example1 = do { %% flt <- example0; %% str <- float2string flt; %% newline;

===================================== src/builtin.ml ===================================== @@ -158,7 +158,8 @@ let register_builtin_csts () = add_builtin_cst "Int" DB.type_int; add_builtin_cst "Integer" DB.type_integer; add_builtin_cst "Float" DB.type_float; - add_builtin_cst "String" DB.type_string + add_builtin_cst "String" DB.type_string; + add_builtin_cst "Elab_Context" DB.type_elabctx

let register_builtin_types () = let _ = new_builtin_type "Sexp" DB.type0 in

===================================== src/debruijn.ml ===================================== @@ -92,6 +92,7 @@ let type_int = mkBuiltin ((dloc, "Int"), type0, None) let type_integer = mkBuiltin ((dloc, "Integer"), type0, None) let type_float = mkBuiltin ((dloc, "Float"), type0, None) let type_string = mkBuiltin ((dloc, "String"), type0, None) +let type_elabctx = mkBuiltin ((dloc, "Elab_Context"), type0, None)

(* easier to debug with type annotations *) type env_elem = (vname * varbind * ltype) @@ -311,13 +312,31 @@ let lctx_lookup (ctx : lexp_context) (v: vref): env_elem = ^ string_of_int dbi ^ " of `" ^ maybename oename ^ "` out of bounds!")

- +let lctx_olookup (ctx : lexp_context) (var : string) : (int * env_elem) option = + let rec _lctx_olookup ctx var idx = + try (let elem = M.car ctx in match elem with + | ((_,Some name),_,_) as elem -> (if (name = var) + then (Some (idx,elem)) + else _lctx_olookup (M.cdr ctx) var (idx + 1)) + | _ -> error dloc ("error in lctx_olookup")) + with Not_found -> None + in (_lctx_olookup ctx var 0)

let lctx_lookup_type (ctx : lexp_context) (vref : vref) : lexp = let (_, i) = vref in let (_, _, t) = lctx_lookup ctx vref in mkSusp t (S.shift (i + 1))

+let lctx_olookup_type (ctx : lexp_context) (var : string) : lexp option = + let oelem = lctx_olookup ctx var in match oelem with + | Some (i,(_, _, t)) -> Some (mkSusp t (S.shift (i + 1))) + | None -> None + +let lctx_olookup_value (ctx : lexp_context) (var : string) : lexp option = + let oelem = lctx_olookup ctx var in match oelem with + | Some (i,(_, LetDef (o, v), _)) -> Some (push_susp v (S.shift (i + 1))) + | None -> None + let lctx_lookup_value (ctx : lexp_context) (vref : vref) : lexp option = let (_, i) = vref in match lctx_lookup ctx vref with @@ -353,7 +372,6 @@ let rec lctx_view lctx = | Myers.Mcons ((loname, odef, t), lctx, _, _) -> CVlet (loname, odef, t, lctx)

- (** Sets of DeBruijn indices **)

type set = db_offset * unit IMap.t

===================================== src/elab.ml ===================================== @@ -999,6 +999,7 @@ and lexp_decls_1 (pending_defs : (symbol * sexp) list) (* Pending definitions. *) : (vname * lexp * ltype) list * sexp list * elab_context =

+ let rec _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs = match sdecls with | [] -> (if not (SMap.is_empty pending_decls) then let (s, l) = SMap.choose pending_decls in @@ -1008,10 +1009,10 @@ and lexp_decls_1 [], [], nctx

| Symbol (_, "") :: sdecls - -> lexp_decls_1 sdecls ectx nctx pending_decls pending_defs + -> _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs

| Node (Symbol (_, ("_;_" (* | "_;" | ";_" *))), sdecls') :: sdecls - -> lexp_decls_1 (List.append sdecls' sdecls) + -> _lexp_decls_1 (List.append sdecls' sdecls) ectx nctx pending_decls pending_defs

| Node (Symbol (l, "_:_"), args) :: sdecls @@ -1034,17 +1035,17 @@ and lexp_decls_1 ^ lexp_string ltp ^ "` incompatible with previous `" ^ lexp_string pt ^ "`") | Some [] -> () in - lexp_decls_1 sdecls ectx nctx pending_decls pending_defs + _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs else if List.exists (fun ((_, vname'), _) -> vname = vname') pending_defs then (error l ("Variable `" ^ vname ^ "` already defined!"); - lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) - else lexp_decls_1 sdecls ectx + _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) + else _lexp_decls_1 sdecls ectx (ectx_extend nctx (l, Some vname) ForwardRef ltp) (SMap.add vname l pending_decls) pending_defs | _ -> error l "Invalid type declaration syntax"; - lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) + _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs)

| Node (Symbol (l, "_=_") as head, args) :: sdecls (* FIXME: Move this to a "special form"! *) @@ -1070,15 +1071,15 @@ and lexp_decls_1 let decls, nctx = lexp_check_decls ectx nctx pending_defs in decls, sdecls, nctx else - lexp_decls_1 sdecls ectx nctx pending_decls pending_defs + _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs

else (error l ("`" ^ vname ^ "` defined but not declared!"); - lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) + _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs)

| [Node (Symbol s, args) as d; body] -> (* FIXME: Make it a macro (and don't hardcode `lambda_->_`)! *) - lexp_decls_1 ((Node (head, + _lexp_decls_1 ((Node (head, [Symbol s; Node (Symbol (sexp_location d, "lambda_->_"), [sexp_u_list args; body])])) @@ -1086,22 +1087,25 @@ and lexp_decls_1 ectx nctx pending_decls pending_defs

| _ -> error l "Invalid definition syntax"; - lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) + _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs)

| Node (Symbol (l, "define-operator"), args) :: sdecls (* FIXME: Move this to a "special form"! *) - -> lexp_decls_1 sdecls ectx (sdform_define_operator nctx l args None) + -> _lexp_decls_1 sdecls ectx (sdform_define_operator nctx l args None) pending_decls pending_defs

| Node (Symbol ((l, _) as v), sargs) :: sdecls -> (* expand macro and get the generated declarations *) let sdecl' = lexp_decls_macro v sargs nctx in - lexp_decls_1 (sdecl' :: sdecls) ectx nctx + _lexp_decls_1 (sdecl' :: sdecls) ectx nctx pending_decls pending_defs

| sexp :: sdecls -> error (sexp_location sexp) "Invalid declaration syntax"; - lexp_decls_1 sdecls ectx nctx pending_decls pending_defs + _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs + + in (EV.set_getenv nctx; + _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs)

and lexp_p_decls (sdecls : sexp list) (ctx : elab_context) : ((vname * lexp * ltype) list list * elab_context) =

===================================== src/env.ml ===================================== @@ -39,6 +39,7 @@ open Elexp module M = Myers module L = Lexp module BI = Big_int +module DB = Debruijn

let dloc = dummy_location

@@ -63,6 +64,7 @@ type value_type = | Vout of out_channel | Vcommand of (unit -> value_type) | Vref of (value_type ref) + | Velabctx of DB.elab_context

(* Runtime Environ *) and runtime_env = (vname * (value_type ref)) M.myers @@ -93,6 +95,8 @@ let rec value_equal a b =

| Vref (v1), Vref (v2) -> value_equal (!v1) (!v2)

+ | Velabctx (e1), Velabctx (e2) -> (e1 = e2) + | _ -> false

let rec value_eq_list a b = @@ -124,6 +128,7 @@ let rec value_name v = | Vbuiltin _ -> "Vbuiltin" | Vcommand _ -> "Vcommand" | Vref v -> ("Vref of "^(value_name (!v))) + | Velabctx _ -> ("Velabctx")

let rec value_string v = match v with @@ -145,6 +150,7 @@ let rec value_string v = "" lst in "(" ^ s ^ args ^ ")" | Vref (v) -> ("Ref of "^(value_string (!v))) + | Velabctx _ -> ("Velabctx")

let value_print (vtp: value_type) = print_string (value_string vtp)

===================================== src/eval.ml ===================================== @@ -723,6 +723,33 @@ let gensym = let count = ref 0 in Vsexp (Symbol (dloc,(" %gensym% no "^(string_of_int (!count))^" "))))) | _ -> error loc "gensym takes a Unit as argument")

+(* I'm using a ref because I think register_builtin_functions + get called after the default_ctx is created in elab. + Another solution could be to define a function in elaboration step + and then undefine it. The thing is elab_context may not exist at runtime + so I must save it somewhere if the Elab.* function persist. *) +let _last_elab_context = ref empty_elab_context + +let getenv loc depth args_val = match args_val with + | [v] -> Vcommand (fun () -> Velabctx !_last_elab_context) + | _ -> error loc "getenv takes a single Unit as argument" + +let set_getenv (ectx : elab_context) = _last_elab_context := ectx + +let is_bound loc depth args_val = match args_val with + | [Vstring name; Velabctx ectx] -> Vcommand (fun () -> + let t = lctx_olookup (ectx_to_lctx ectx) name in match t with + | Some _ -> (Vint 1) + | _ -> (Vint 0) ) + | _ -> error loc "Elab.isbound takes an Elab_Context and a String as arguments" + +let is_constructor loc depth args_val = match args_val with + | [Vstring name; Velabctx ectx] -> Vcommand (fun () -> + let t = lctx_olookup_value (ectx_to_lctx ectx) name in match t with + | Some (Cons _) -> (Vint 1) + | _ -> (Vint 0) ) + | _ -> error loc "Elab.isconstructor takes an Elab_Context and a String as arguments" + let register_builtin_functions () = List.iter (fun (name, f, arity) -> add_builtin_function name f arity) [ @@ -755,6 +782,9 @@ let register_builtin_functions () = ("Ref.read" , ref_read, 1); ("Ref.write" , ref_write, 2); ("gensym" , gensym, 1); + ("Elab.getenv" , getenv, 1); + ("Elab.isbound" , is_bound, 2); + ("Elab.isconstructor", is_constructor, 2); ] let _ = register_builtin_functions ()

===================================== tests/elabctx_test.ml ===================================== @@ -0,0 +1,216 @@ + +open Util +open Utest_lib + +open Sexp +open Lexp + +open Eval (* reset_eval_trace *) + +open Builtin +open Env + +(* default environment *) +let ectx = Elab.default_ectx +let rctx = Elab.default_rctx + + +let _ = (add_test "ELABCTX" "Elab_getenv" (fun () -> + let dcode = " + return = IO_return; + + nop = (lambda _ -> return ()); + + action = do + { + env <- (Elab_getenv ()); + + return env; + };" in + + let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in + + let ecode = "action;" in + + let ret = Elab.eval_expr_str ecode ectx rctx in + + match ret with + | [Vcommand cmd] -> ( match (cmd ()) with + | (Velabctx _) -> success () + | _ -> failure () ) + | _ -> failure ()) +) + +let _ = (add_test "ELABCTX" "Elab_isbound" (fun () -> + let dcode = " + return = IO_return; + + nop = (lambda _ -> return ()); + + a = do + { + env <- (Elab_getenv ()); + + b <- (Elab_isbound "Int" env); + + return b; + }; + + b = do + { + env <- (Elab_getenv ()); + + b <- (Elab_isbound "List" env); + + return b; + }; + + c = do + { + env <- (Elab_getenv ()); + + b <- (Elab_isbound "Elab_isbound" env); + + return b; + }; + + d = do + { + env <- (Elab_getenv ()); + + b <- (Elab_isbound "do" env); + + return b; + }; + + e = do + { + env <- (Elab_getenv ()); + + b <- (Elab_isbound "randomunusednameabc123" env); + + return b; + };" in + + let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in + + let ecode = "a; b; c; d; e;" in + + let ret = Elab.eval_expr_str ecode ectx rctx in + + match ret with + | [Vcommand a; Vcommand b; Vcommand c; + Vcommand d; Vcommand e] -> + ( match (a (), b (), c (), d (), e ()) with + | (Vint 1, Vint 1, Vint 1, Vint 1, Vint 0) -> success () + | _ -> failure () ) + | _ -> failure ()) +) + +let _ = (add_test "ELABCTX" "Elab_isconstructor" (fun () -> + let dcode = " + return = IO_return; + + nop = (lambda _ -> return ()); + + af = do + { + env <- (Elab_getenv ()); + + b <- (Elab_isconstructor "Int" env); + + return b; + }; + + bf = do + { + env <- (Elab_getenv ()); + + b <- (Elab_isconstructor "List" env); + + return b; + }; + + cf = do + { + env <- (Elab_getenv ()); + + b <- (Elab_isconstructor "Elab_isbound" env); + + return b; + }; + + df = do + { + env <- (Elab_getenv ()); + + b <- (Elab_isconstructor "do" env); + + return b; + }; + + ef = do + { + env <- (Elab_getenv ()); + + b <- (Elab_isconstructor "randomunusednameabc123" env); + + return b; + }; + + at = do + { + env <- (Elab_getenv ()); + + b <- (Elab_isconstructor "cons" env); + + return b; + }; + + bt = do + { + env <- (Elab_getenv ()); + + b <- (Elab_isconstructor "nil" env); + + return b; + }; + + ct = do + { + env <- (Elab_getenv ()); + + b <- (Elab_isconstructor "true" env); + + return b; + }; + + dt = do + { + env <- (Elab_getenv ()); + + b <- (Elab_isconstructor "false" env); + + return b; + };" in + + let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in + + let ecode = "af; bf; cf; df; ef; at; bt; ct; dt;" in + + let ret = Elab.eval_expr_str ecode ectx rctx in + + match ret with + | [Vcommand af; Vcommand bf; Vcommand cf; Vcommand df; Vcommand ef; + Vcommand at; Vcommand bt; Vcommand ct; Vcommand dt] -> + ( match (af (), bf (), cf (), df (), ef (), + at (), bt (), ct (), dt ()) with + | (Vint 0, Vint 0, Vint 0, Vint 0, Vint 0, + Vint 1, Vint 1, Vint 1, Vint 1) -> success () + | _ -> failure () ) + | _ -> failure ()) +) + + +(* run all tests *) +let _ = run_all ()

===================================== tests/macro_do_test.ml ===================================== @@ -0,0 +1,118 @@ + +open Util +open Utest_lib + +open Sexp +open Lexp + +open Eval (* reset_eval_trace *) + +open Builtin +open Env + +(* default environment *) +let ectx = Elab.default_ectx +let rctx = Elab.default_rctx + +(* all tests use binded variable *) +(* I'm saying it in case everythings break *) + +(* there's a problem with string inside string when I use new line ("\n") *) + +(* mostly to check if no exception are thrown *) +let _ = (add_test "DO MACROS" "Hello, world!" (fun () -> + let dcode = " + return = IO_return; + + nop = (lambda _ -> return ()); + + action = do + { + str <- return "Hello, world!"; + + nop str; + };" in + + let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in + + let ecode = "action;" in + + let ret = Elab.eval_expr_str ecode ectx rctx in + + match ret with + | [Vcommand _] -> success () + | _ -> failure ()) +) + +(* check return value from do macro *) +let _ = (add_test "DO MACROS" "return value" (fun () -> + let dcode = " + return = IO_return; + + nop = (lambda _ -> return ()); + + action = do + { + nop "Doing random stuff before returning..."; + + n <- return 123456789; + + return n; + };" in + + let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in + + let ecode = "action;" in + + let ret = Elab.eval_expr_str ecode ectx rctx in + + match ret with + | [Vcommand cmd] -> ( match (cmd ()) with + | Vint v -> + if (123456789 = v) then success () else failure () + | _ -> failure() ) + + | _ -> failure ()) +) + +(* check if any problem when using do as command inside another do *) +let _ = (add_test "DO MACROS" "do inside do" (fun () -> + let dcode = " + return = IO_return; + + nop = (lambda _ -> return ()); + + action0 = do { return 123; }; + + action1 = do + { + x <- do { return (Float_+ 16.0 0.125); }; + + nop "Doing random stuff..."; + + str <- return (Float->String x); + + val123 <- action0; + + do { nop str; }; + + do { do { nop str; }; }; + + return str; + };" in + + let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in + + let ecode = "action1;" in + + let ret = Elab.eval_expr_str ecode ectx rctx in + + match ret with + | [Vcommand cmd] -> ( match (cmd ()) with + | Vstring str -> if ("16.125" = str) then success () else failure () + | _ -> failure () ) + | _ -> failure ()) +) + +(* run all tests *) +let _ = run_all ()

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