Setepenre pushed to branch master at Stefan / Typer

Commits: 5521e11a by Pierre Delaunay at 2016-04-27T11:02:03-04:00 fix little things

Changes to be committed: * GNUmakefile: compile to bytecote to avoid recompilation * src/pexp.ml: fix formal arg parsing * tests/sexp_test.ml: fix sexp_test

- - - - - 6967d92c by Pierre Delaunay at 2016-04-28T09:51:02-04:00 fix lexp_decls and Macro

Changes to be committed: * README.md: minor updates * src/lparse.ml: - add an error message when lambda does not habe type info - fix lexp.Arrow, its variable was not added to the environement * src/builtin.ml * btl/macro.typer: - added some ideas on how to define type built-in * src/lexp.ml: - fix lexp_print Inductive's formal args

- - - - -

15 changed files:

- GNUmakefile - README.md - samples/BTL.typer → btl/list.typer - + btl/macro.typer - + samples/macro.typer - src/builtin.ml - src/debruijn.ml - src/env.ml - src/eval.ml - src/lexp.ml - src/lparse.ml - src/pexp.ml - src/subst.ml - tests/macro_test.ml - tests/sexp_test.ml

Changes:

===================================== GNUmakefile ===================================== --- a/GNUmakefile +++ b/GNUmakefile @@ -5,18 +5,19 @@ CPL_FILES := $(wildcard ./_build/src/*.cmo) TEST_FILES := $(wildcard ./tests/*_test.ml)

OBFLAGS = -build-dir _build -COMPILE_MODE = native +# COMPILE_MODE = native

all: ityper typer debug tests-build

ifeq ($(OS), Windows_NT) # Windows need '-r' and building to native can be problematic (linking error) # So we build to byte instead - OBFLAGS = $(OBFLAGS) -r +endif + COMPILE_MODE = byte

-endif +

typer:

===================================== README.md ===================================== --- a/README.md +++ b/README.md @@ -12,19 +12,19 @@ Typer

By default ocamlbuild creates a '_build' folder which holds all the compiled files.

-* make typer: build typer interpreter 'typer' -* make debug: build typer with debug info 'debug' -* make tests: run interpreter's tests '/.tests/utest_main.byte' +* `make typer`: build typer interpreter './typer' +* `make debug`: build typer with debug info './debug_util' +* `make tests`: run interpreter's tests './tests/utests'

# Directory layout

-* src/ interpreter's source -* doc/ interpreter's doc files -* sample/ typer code sample for testing purposes -* tests/ ocaml test files - +* `src/` interpreter's source +* `doc/` interpreter's doc files +* `sample/` typer code sample for testing purposes +* `tests/` ocaml test files +* `btl/` builtin typer library + # Emacs files

/typer-mode.el - - \ No newline at end of file +

===================================== samples/BTL.typer → btl/list.typer ===================================== --- a/samples/BTL.typer +++ b/btl/list.typer @@ -6,26 +6,23 @@ 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 => -length : List a -> Int; -length = lambda (xs : List a) -> +length : (a : Type) => List a -> Int; +length = lambda a => + lambda xs -> case xs - | nil => 0 - | cons hd tl => (1 + length tl); + | nil => 0 + | cons hd tl => (1 + length tl);

-% head : (a : Type) => List a -> a; -% head = lambda a => -head : List a -> a; -head = lambda (xs : List a) -> +head : (a : Type) => List a -> a; +head = lambda a => + lambda xs -> case xs - | nil => nil - | cons hd tl => hd; + | nil => nil + | cons hd tl => hd;

-% tail : (a : Type) => List a -> List a; -% tail = lambda a => -tail : List a -> List a; -tail = lambda (xs : List a) -> +tail : (a : Type) => List a -> List a; +tail = lambda a => + lambda xs -> case xs - | nil => nil - | cons hd tl => tl; \ No newline at end of file + | nil => nil + | cons hd tl => tl; \ No newline at end of file

===================================== btl/macro.typer ===================================== --- /dev/null +++ b/btl/macro.typer @@ -0,0 +1,24 @@ + +% define Sexp constructor +Sexp : Type; +Sexp = inductive_ (built-in) (block_ Sexp) + (symbol_ string) (string_ string) (integer_ Int) (float_ Float) + (node_ Sexp List Sexp); + +Macro : Type; +Macro = inductive_ (built-in) (Macro_ sexp); + +%% Basic usage +% +% sqr = (Macro_ +% (node_ (symbol_ "lambda_->_") (symbol "x") +% (node_ "_*_" (symbol "x") (symbol "x")))); +% +% (sqr 4); % <=> 4 * 4 +% +% +%% Using Quasi Quote ` +% +% sqr = (Macro_ (qq (lambda x -> ,x * ,x))); +% +% (sqr 4); % <=> 4 * 4

===================================== samples/macro.typer ===================================== --- /dev/null +++ b/samples/macro.typer @@ -0,0 +1,14 @@ + +sqr_fun = node_ (symbol_ "lambda_->_") (symbol_ "x") + (node_ (symbol_ "_*_") (symbol_ "x") (symbol_ "x")); + +sqr_type = node_ (symbol_ "_->_") (symbol_ "Int") (symbol_ "Int"); + +give_type : Sexp -> Sexp -> Sexp; +give_type = lambda expr -> + lambda tp -> + node_ (symbol_ "_:_") expr tp; + +sqr = Macro_ (give_type sqr_fun sqr_type); + +main = (sqr 2); \ No newline at end of file

===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -56,9 +56,9 @@ let type_omega = Sort (dloc, StypeOmega) let type_level = Sort (dloc, StypeLevel) let type_level = Builtin (LevelType, "TypeLevel", type_level)

- -let type_int = Builtin (IntType, "Int", type0) +let type_int = Builtin (IntType, "Int", type0) let type_float = Builtin (FloatType, "Float", type0) +let type_sexp = Builtin (SexpType, "sexp", type0)

let op_binary t = Arrow (Aexplicit, None, t, dloc, Arrow (Aexplicit, None, t, dloc, t)) @@ -77,7 +77,7 @@ let type_eq = let lv = (dloc, "l") in let builtin_iadd = Builtin (IAdd, "_+_", iop_binary) let builtin_imult = Builtin (IMult, "_*_", iop_binary) let builtin_eq = Builtin (EqType, "_=_", type_eq) -let builtin_sexp = Builtin (SexpType, "sexp", type0) + (* let builtin_fadd = Builtin (FAdd, "_+_", fop_binary) let builtin_fmult = Builtin (FMult, "_*_", fop_binary) *) @@ -178,12 +178,12 @@ let make_float loc args_val ctx = Value(type0) let type_string = type0 let type_mblock = type0

-let type_msymbol = Arrow (Aexplicit, None, type_string, dloc, builtin_sexp) -let type_mstring = Arrow (Aexplicit, None, type_string, dloc, builtin_sexp) -let type_minteger = Arrow (Aexplicit, None, type_int, dloc, builtin_sexp) -let type_mfloat = Arrow (Aexplicit, None, type_float, dloc, builtin_sexp) -let type_mnode = Arrow (Aexplicit, None, builtin_sexp,dloc, builtin_sexp) -let type_mexpand = Arrow (Aexplicit, None, builtin_sexp,dloc, type0) +let type_msymbol = Arrow (Aexplicit, None, type_string, dloc, type_sexp) +let type_mstring = Arrow (Aexplicit, None, type_string, dloc, type_sexp) +let type_minteger = Arrow (Aexplicit, None, type_int , dloc, type_sexp) +let type_mfloat = Arrow (Aexplicit, None, type_float , dloc, type_sexp) +let type_mnode = Arrow (Aexplicit, None, type_sexp , dloc, type_sexp) +let type_mexpand = Arrow (Aexplicit, None, type_sexp , dloc, type0)

let builtin_block = Builtin (SexpType, "block_", type_mblock) let builtin_symbol = Builtin (SexpType, "symbol_", type_msymbol) @@ -191,8 +191,15 @@ let builtin_string = Builtin (SexpType, "string_", type_mstring) let builtin_integer = Builtin (SexpType, "integer_", type_minteger) let builtin_float = Builtin (SexpType, "float_", type_mfloat) let builtin_node = Builtin (SexpType, "node_", type_mnode) -let builtin_expand = Builtin (SexpType, "expand_", type_mexpand) +(* let builtin_expand = Builtin (SexpType, "expand_", type_mexpand) *)

+let type_macro = + let ctors = SMap.empty in + let ctors = SMap.add "Macro_" [(Aexplicit, None, type_sexp)] ctors in + Inductive (dloc, (dloc, "built-in"), [], ctors) + +let builtin_macro = Cons (((dloc, "Macro"), (-4)), (dloc, "Macro_")) +let macro_cons = Arrow (Aexplicit, None, type_sexp , dloc, type_macro) (* * Should we have a function that * -> returns a new context inside typer ? (So we need to add a ctx type too) @@ -210,12 +217,14 @@ let typer_builtins = [ ("Int" , type_int , type0, none_fun); ("Float" , type_float , type0, none_fun); ("String", type_string, type0, none_fun); + ("Sexp" , type_sexp , type0, none_fun); + ("Macro" , type_macro , type0, none_fun);

(* Built-in Functions *) - ("_=_" , builtin_eq, type_eq, none_fun); (* t -> t -> bool *) - ("_+_" , builtin_iadd, iop_binary, iadd_impl); (* int -> int -> int *) - ("_*_" , builtin_imult, iop_binary, imult_impl); (* int -> int -> int *) - + ("_=_" , builtin_eq, type_eq, none_fun); (* t -> t -> bool *) + ("_+_" , builtin_iadd, iop_binary, iadd_impl); (* int -> int -> int *) + ("_*_" , builtin_imult, iop_binary, imult_impl); (* int -> int -> int *) + ("Macro_", builtin_macro, macro_cons, none_fun); (* Macro primitives *) ("block_" , builtin_block , type_mblock , make_block); ("symbol_" , builtin_symbol , type_msymbol , make_symbol); @@ -223,7 +232,7 @@ let typer_builtins = [ ("integer_", builtin_integer, type_minteger, make_integer); ("float_" , builtin_float , type_mfloat , make_float); ("node_" , builtin_node , type_mnode , make_node); - ("expand_" , builtin_expand , type_mexpand , none_fun); + (* ("expand_" , builtin_expand , type_mexpand , none_fun); *)

(* Macros primitives type ? *)

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -119,7 +119,7 @@ let senv_add_var (loc, name) ctx =

let env_add_var_info var (ctx: lexp_context) = let (a, env, f) = ctx in - (a, cons (ref var) env, f) + (a, cons (ref var) env, f)

let env_extend (ctx: lexp_context) (def: vdef) (v: lexp option) (t: lexp) = let ((n, map), e, f) = ctx in

===================================== src/env.ml ===================================== --- a/src/env.ml +++ b/src/env.ml @@ -134,7 +134,7 @@ let set_rte_variable idx name (lxp: value_type) ctx = match (n, name) with | Some n1, Some n2 -> if (n1 != n2) then - env_error dloc ("Variable Name must Match:" ^ n1 ^ " " ^ n2) + env_error dloc ("Variable's Name must Match: " ^ n1 ^ " vs " ^ n2) else( ref_cell := (name, lxp); ctx)

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -90,6 +90,9 @@ let rec _eval lxp ctx i: (value_type) = let nctx = _eval_decls decls ctx i in _eval inst nctx (i + 1)

+ (* I don't really know why Built-in is ever evaluated... but it is sometimes *) + | Builtin _ -> Vdummy + (* Built-in Function *) | Call(Builtin(btype, str, ltp), args)-> (* built-in does not have location info. So we extract it from args *) @@ -105,13 +108,14 @@ let rec _eval lxp ctx i: (value_type) = (* Case *) | Case (loc, target, _, pat, dflt) -> (eval_case ctx i loc target pat dflt)

+ | _ -> print_string "debug catch-all eval: "; lexp_print lxp; Value(Imm(String(dloc, "eval Not Implemented")))

and eval_var ctx lxp v = let ((loc, name), idx) = v in try get_rte_variable (Some name) (idx) ctx - with Not_found -> + with e -> eval_error loc ("Variable: " ^ name ^ (str_idx idx) ^ " was not found ")

and eval_call ctx i lname args call = @@ -146,8 +150,9 @@ and eval_call ctx i lname args call =

(* No more arguments *) | Closure (_, _), [] -> body - | Value (lxp), [] -> body - | _ -> eval_error dloc "Cannot eval function" in + | _, [] -> body + | _ -> value_print body; + eval_error dloc "Cannot eval function" in

eval_call body args_val clean_ctx

@@ -331,16 +336,25 @@ let from_lctx (ctx: lexp_context): runtime_env = let bsize = List.length typer_builtins in let csize = get_size ctx in

+ (* add all variables *) for i = bsize to csize do - let (_, (_, name), exp, _) = !(Myers.nth (csize - i) env) in + let (_, (_, name), _, _) = !(Myers.nth (csize - i) env) in + rctx := add_rte_variable (Some name) Vdummy (!rctx) + done; + + let diff = csize - bsize in + + (* process all of them *) + for i = 0 to diff do + let j = diff - i (* - 1 *) in + let (_, (_, name), exp, _) = !(Myers.nth j env) in

let vxp = match exp with | Some lxp -> (eval lxp !rctx) | None -> Vdummy in

- rctx := add_rte_variable (Some name) vxp (!rctx) + rctx := set_rte_variable j (Some name) vxp (!rctx) done; - !rctx

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -54,6 +54,7 @@ type builtin = | IMult | EqType | LevelType + | MacroType

(* Pour la propagation des types bidirectionnelle, tout va dans `infer`, * sauf Lambda et Case qui vont dans `check`. Je crois. *) @@ -583,6 +584,10 @@ and _lexp_to_str ctx exp = match k with | Aexplicit -> "->" | Aimplicit -> "=>" | Aerasable -> "≡>" in

+ let kindp_str k = + match k with + | Aexplicit -> ":" | Aimplicit -> "::" | Aerasable -> ":::" in + match exp with | Imm(value) -> (match value with | String (_, s) -> tval (""" ^ s ^ """) @@ -640,8 +645,17 @@ and _lexp_to_str ctx exp =

"(" ^ (fun_call (lexp_to_str fname)) ^ args ^ ")")

- | Inductive (_, (_, name), _, ctors) -> - (keyword "inductive_") ^ " (" ^ name ^ ") " ^ (lexp_str_ctor ctx ctors) + | Inductive (_, (_, name), [], ctors) -> + (keyword "inductive_") ^ " (" ^ name ^") " ^ + (lexp_str_ctor ctx ctors) + + | Inductive (_, (_, name), args, ctors) -> + let args_str = List.fold_left (fun str (arg_kind, (_, name), ltype) -> + str ^ " (" ^ name ^ " " ^ (kindp_str arg_kind) ^ " " ^ (lexp_to_str ltype) ^ ")") + "" args in + + (keyword "inductive_") ^ " (" ^ name ^ args_str ^") " ^ + (lexp_str_ctor ctx ctors)

| Case (_, target, tpe, map, dflt) ->( let str = (keyword "case ") ^ (lexp_to_str target) ^ @@ -665,8 +679,10 @@ and _lexp_to_str ctx exp =

| Builtin (_, name, _) -> name

- | Sort (_, _) -> "Sort" - | SortLevel _ -> "SortLevel" + | Sort (_, Stype lvl) -> (match lvl with + | SortLevel (SLn 0) -> "Type" + | SortLevel (SLn v) -> "Type" ^ (string_of_int v) + | _ -> "Type")

| _ -> print_string "Printing Not Implemented"; ""

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -143,16 +143,14 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = Let(tloc, decl, bdy), ltp

(* ------------------------------------------------------------------ *) - | Parrow (kind, Some var, tp, loc, expr) -> - let ltyp, _ = lexp_infer tp ctx in - let lxp, _ = lexp_infer expr ctx in - let v = Arrow(kind, Some var, ltyp, tloc, lxp) in - v, type0 + | Parrow (kind, ovar, tp, loc, expr) -> + let ltp, _ = lexp_infer tp ctx in + let ctx = match ovar with + | None -> ctx + | Some var -> env_extend ctx var None ltp in

- | Parrow (kind, None, tp, loc, expr) -> - let ltyp, _ = lexp_infer tp ctx in let lxp, _ = lexp_infer expr ctx in - let v = Arrow(kind, None, ltyp, tloc, lxp) in + let v = Arrow(kind, ovar, ltp, tloc, lxp) in v, type0

(* Pinductive *) @@ -169,14 +167,25 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = ) formal_args in (* (arg_kind * vdef * ltype) list *)

+ (* -- Should I do that ?? --*) + let rec make_type args tp = + match args with + | (kind, (loc, n), ltp)::tl -> + make_type tl (Arrow(kind, Some (loc, n), ltp, loc, tp)) + | [] -> tp in + let ctx = !ctx in let map_ctor = lexp_parse_inductive ctors ctx i in let v = Inductive(tloc, label, formal, map_ctor) in - v, type0 + v, (make_type formal type0)

(* This case can be inferred *) - | Plambda (kind, var, Some ptype, body) -> - let ltp, _ = lexp_infer ptype ctx in + | Plambda (kind, var, optype, body) -> + let ltp, _ = match optype with + | Some ptype -> lexp_infer ptype ctx + (* This case must have been lexp_p_check *) + | None -> lexp_error tloc "Lambda require type annotation"; + dltype, dltype in

let nctx = env_extend ctx var None ltp in let lbody, lbtp = lexp_infer body nctx in @@ -267,6 +276,7 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = | hd::tl, Some _ -> hd | hd::tl, None -> hd | _, Some v -> v + (* This will change *) | _, None -> lexp_error loc "case with no branch ?"; dltype in

Case(loc, tlxp, tltp, lpattern, dflt), (return_type) @@ -289,7 +299,7 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = | Plambda (kind, var, None, body) -> (* Read var type from the provided type *) let ltp, lbtp = match t with - | Arrow(kind, None, ltp, _, lbtp) -> ltp, lbtp + | Arrow(kind, _, ltp, _, lbtp) -> ltp, lbtp | _ -> lexp_error tloc "Type does not match"; dltype, dltype in

let nctx = env_extend ctx var None ltp in @@ -297,6 +307,7 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp =

Lambda(kind, var, ltp, lbody)

+ (* | Pcall (Pvar(_, "expand_"), _args) ->( let pargs = List.map pexp_parse _args in let largs = _lexp_parse_all pargs ctx i in @@ -312,7 +323,7 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = | _ -> lexp_fatal tloc "expand_ expects sexp" in

let pxp = pexp_parse sxp in - _lexp_p_check pxp t ctx (i + 1)) + _lexp_p_check pxp t ctx (i + 1)) *)

| _ -> let (e, inferred_t) = _lexp_p_infer p ctx (i + 1) in (* FIXME: check that inferred_t = t! *) @@ -350,16 +361,18 @@ and lexp_call (fname: pexp) (_args: sexp list) ctx i = let vf = (make_var name idx loc) in

(* consume Arrows and args together *) - let rec get_return_type ltp args = + let rec get_return_type i ltp args = match ltp, args with | _, [] -> ltp - | Arrow(_, _, _, _, ltp), hd::tl -> (get_return_type ltp tl) - | _, _ -> lexp_warning loc "Too many args"; ltp in + | Arrow(_, _, _, _, ltp), hd::tl -> (get_return_type (i + 1) ltp tl) + | _, _ -> lexp_warning loc ("""^ name ^ + "" was provided with too many args. Expected: " ^ + (string_of_int i)); ltp in

- let ret_type = get_return_type ltp new_args in + let ret_type = get_return_type 0 ltp new_args in

(* Is the function built-in ? *) - (* built-in cannot be partially applied that us why we can get_return_type *) + (* built-in cannot be partially applied that is why we can get_return_type *) (* they can only if you redefine the operation *) if (is_lbuiltin idx ctx) then ( match env_lookup_expr ctx ((loc, name), idx) with @@ -367,9 +380,22 @@ and lexp_call (fname: pexp) (_args: sexp list) ctx i = Call(vf, new_args), ret_type

(* Is it a macro ? *) - | Some Builtin (_, "expand_", _) -> - lexp_error loc "expand_ require type annotation"; - dltype, dltype + | Some Cons (((_, "Macro"), _), (_, "Macro_")) -> + + let lxp = match largs with + | [lxp] -> lxp + | hd::tl -> lexp_error loc "Macro_ expects one lexp"; hd + | _ -> lexp_fatal loc "Macro_ expects one lexp" in + + let rctx = (from_lctx ctx) in + + (* eval argument *) + let sxp = match eval lxp rctx with + | Vsexp(sxp) -> sxp + | v -> lexp_fatal loc "Macro_ expects sexp" in + + let pxp = pexp_parse sxp in + _lexp_p_infer pxp ctx (i + 1)

(* a builtin functions *) | Some e -> Call(e, new_args), ret_type @@ -466,64 +492,9 @@ and lexp_parse_inductive ctors ctx i = SMap.empty ctors

(* Parse let declaration *) -and lexp_p_decls decls ctx = _lexp_decls decls ctx 1 +and lexp_p_decls decls ctx = _lexp_decls decls ctx 0 and _lexp_decls decls ctx i: (((vdef * lexp * ltype) list) * lexp_context) = - (* (pvar * pexp * bool) list * ) - - let ctx = ref ctx in - let mdecls = ref SMap.empty in - let order = ref [] in - let found = ref false in - - List.iter (fun ((loc, name), pxp, bl) -> - (* Check if variable was already defined *) - let (l, olxp, oltp, _) = try found := true; SMap.find name !mdecls - with Not_found -> - (* keep track of declaration order *) - order := (name::!order); - found := false; - (* create an empty element *) - (loc, None, None, 0) in - - (* create a dummy env for lexp_parse *) - let denv = env_extend (!ctx) (loc, name) None dltype in - - (* Do we already have a type ? *) - let lxp, ltp = match oltp with - (* We infer *) - | None -> _lexp_p_infer pxp denv (i + 1) - - (* We check *) - | Some ltp -> (_lexp_p_check pxp ltp denv (i + 1)), ltp in - - (* update declaration *) - (* FIXME: modify env when lxp is found *) - let new_decl = match bl with - | true -> (if !found then () else ctx := env_extend (!ctx) (loc, name) None lxp); - (l, olxp, Some lxp, i) - | false -> (if !found then () else ctx := env_extend (!ctx) (loc, name) (Some lxp) ltp); - (l, Some lxp, oltp, i) in - - (* Add Variable to the map *) - mdecls := SMap.add name new_decl !mdecls) - - decls; - - let ctx = !ctx in - let mdecls = !mdecls in - let order = !order in - (* Cast Map to list *) - let ndecls = List.map (fun name -> - let (l, inst, tp, _) = SMap.find name mdecls in - match inst, tp with - | Some lxp, Some ltp -> ((l, name), lxp, ltp) - | Some lxp, None -> ((l, name), lxp, dltype) - | None, Some ltp -> lexp_warning l "Type with no expression"; - ((l, name), dltype, ltp) - | None, None -> lexp_warning l "No expression, No Type"; - ((l, name), dltype, dltype)) order in - - (List.rev ndecls), ctx *) + (* (pvar * pexp * bool) list *)

let ctx = ref ctx in let idx = ref 0 in

===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -187,21 +187,13 @@ and pexp_p_actual_arg arg : (arg_kind * pvar option * pexp) = | e -> (Aexplicit, None, pexp_parse e)

and pexp_p_formal_arg arg : (arg_kind * pvar * pexp option) = - (* FYI: None of the formal arg type work *) - (* (a ::: Type) -> (a ::: Type) instead of (::: a Type) - * (a :: Type) -> (a :: Type) instead of (:: a Type) - * (a : Type) -> (_:_ a Type) instead of (_:_ a Type) *) match arg with - | Node (Symbol (_, ":::"), [Symbol s; e]) + | Node (Symbol (_, "_:::_"), [Symbol s; e]) -> (Aerasable, s, Some (pexp_parse e)) - | Node (Symbol (_, "::"), [Symbol s; e]) + | Node (Symbol (_, "_::_"), [Symbol s; e]) -> (Aimplicit, s, Some (pexp_parse e)) - | Node (Symbol (_, ":"), [Symbol s; e]) - -> (Aexplicit, s, Some (pexp_parse e)) - (* ------ FIXME: temp FIX ------ *) | Node (Symbol (_, "_:_"), [Symbol s; e]) -> (Aexplicit, s, Some (pexp_parse e)) - (* ------ --------------- ------ *) | Symbol s -> (Aexplicit, s, None) | _ -> sexp_print arg; (pexp_error (sexp_location arg) "Unrecognized formal arg");

===================================== src/subst.ml ===================================== --- a/src/subst.ml +++ b/src/subst.ml @@ -206,6 +206,7 @@ type 'a subst = (* lexp subst *) * context Δₛ₁ΔₜΔₛ₂ where Δₛ₂ has size N and Δₜ has size M. *) | Identity | Cons of 'a * 'a subst + (* we enter a let/lambda/case/inductive (with formal args) *) | Shift of 'a subst * db_offset (* | Lift of db_index * db_offset *)

===================================== tests/macro_test.ml ===================================== --- a/tests/macro_test.ml +++ b/tests/macro_test.ml @@ -54,11 +54,16 @@ let _ = (add_test "MACROS" "macros base" (fun () ->

(* define 'lambda x -> x * x' using macros *) let dcode = " - sqr_sexp = (node_ (symbol_ "lambda_->_") (symbol_ "x") - (node_ (symbol_ "_*_") (symbol_ "x") (symbol_ "x"))); + sqr_fun = node_ (symbol_ "lambda_->_") (symbol_ "x") + (node_ (symbol_ "_*_") (symbol_ "x") (symbol_ "x"));

- sqr : Int -> Int; - sqr = (expand_ sqr_sexp);" in + sqr_type = node_ (symbol_ "_->_") (symbol_ "Int") (symbol_ "Int"); + + has_type = lambda (expr : Sexp) -> + lambda (tp : Sexp) -> + node_ (symbol_ "_:_") expr tp; + + sqr = Macro_ (has_type sqr_fun sqr_type);" in

let rctx, lctx = eval_decl_str dcode lctx rctx in

===================================== tests/sexp_test.ml ===================================== --- a/tests/sexp_test.ml +++ b/tests/sexp_test.ml @@ -2,36 +2,19 @@ open Sexp open Lexer open Utest_lib

- -(* _+_ precedence is too low ? - * - * a = lambda x -> x + x + x - * is parsed to - * a = (_+_ (_+_ (lambda_->_ x x) x) x) <=> a = (lambda x -> x) + x + x - * instead of - * a = (lambda_->_ x (_+_ (_+_ x x) x)) *) let _ = (add_test "SEXP" "lambda x -> x + x" (fun () ->

- let dcode = "lambda x -> x + x;" in + let dcode = "lambda x -> x + x;" in

- let ret = sexp_parse_str dcode in - match ret with - | [n] ->(match n with - | Node(Symbol(_, "lambda"), [arg; body]) -> success () - (* arg = Symbol(_, "x") *) - (* body = Node(Symbol(_, "_+_"), [Symbol(_, "x"); Symbol(_, "x")]) *) - | _ -> failure ()) - | _ -> failure () + let ret = sexp_parse_str dcode in + match ret with + | [Node(lbd, [x; add])] -> (match lbd, x, add with + | (Symbol(_, "lambda_->_"), Symbol(_, "x"), + Node(Symbol(_, "_+_"), [Symbol(_, "x"); Symbol(_, "x")])) -> success () + | _ -> failure ()) + | _ -> failure () ));;

- -(* _*_ is not a binary operator - * - * b = lambda x -> (x * x * x); - * is parsed to - * b = (lambda_->_ x (_*_ x x x)) - * instead of - * b = (lambda_->_ x (_*_ (_*_ x x) x)) *) let _ = (add_test "SEXP" "x * x * x" (fun () ->

let dcode = "x * x * x;" in

View it on GitLab: https://gitlab.com/monnier/typer/compare/731e1482be1e361602378f9985250425663...