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

@@ -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
+

btl/list.typer

+
+
+List : 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 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;
\ No newline at end of file

btl/macro.typer

+
+% 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/BTL.typer

-
-
-List : 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 =>
-length : List a -> Int;
-length = lambda (xs : List a) ->
-    case xs
-        | 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) ->
-    case xs
-        | 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) ->
-    case xs
-        | nil => nil
-        | cons hd tl => tl;
\ No newline at end of file

samples/macro.typer

+
+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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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