Setepenre pushed to branch master at Stefan / Typer

Commits: 4af18f1c by Pierre Delaunay at 2016-04-28T16:45:35-04:00 Continued Stefan `value_type` changes (Broke Macro Handling)

Changes to be committed: * src/env.ml : value_type definition - no more `Value of lexp`

- Adapted Files * src/eval.ml * src/builtin.ml * tests/*

- - - - -

8 changed files:

- + samples/nat.typer - src/builtin.ml - src/env.ml - src/eval.ml - src/lparse.ml - tests/env_test.ml - tests/eval_test.ml - tests/macro_test.ml

Changes:

===================================== samples/nat.typer ===================================== --- /dev/null +++ b/samples/nat.typer @@ -0,0 +1,32 @@ +Nat = inductive_ (dNat) (zero) (succ Nat); + +zero = inductive-cons Nat zero; +succ = inductive-cons Nat succ; + +to-num : Nat -> Int; +to-num = lambda (x : Nat) -> + case x + | (succ y) => (1 + (to-num y)) + | zero => 0; + +one = (succ zero); +two = (succ one); +three = (succ two); + +plus : Nat -> Nat -> Nat; +plus = lambda (x : Nat) -> + lambda (y : Nat) -> + case x + | zero => y + | succ z => succ (plus z y); + + +n1 = (to-num zero); +n2 = (to-num one); +n3 = (to-num two); + + + +m1 = (to-num (plus zero two)); % 2 +m2 = (to-num (plus two zero)); % 2 +m3 = (to-num (plus two one)); % 3 \ No newline at end of file

===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -82,26 +82,6 @@ let builtin_eq = Builtin (EqType, "_=_", type_eq) let builtin_fadd = Builtin (FAdd, "_+_", fop_binary) let builtin_fmult = Builtin (FMult, "_*_", fop_binary) *)

-(* Math Functions *) -let get_int (lxp: value_type): (int option) = - let lxp = get_value_lexp lxp in - match lxp with - | Imm(Integer(_, l)) -> Some l - | _ -> None -;; - -let get_string (lxp: value_type): (string option) = - let lxp = get_value_lexp lxp in - match lxp with - | Imm(String(_, l)) -> Some l - | _ -> None -;; - -let get_sexp (lxp: value_type): (sexp option) = - match lxp with - | Vsexp l -> Some l - | _ -> None -;;

(* Builtin of builtin * string * ltype *) let _generic_binary_iop name f loc (args_val: value_type list) (ctx: runtime_env) = @@ -117,8 +97,8 @@ let _generic_binary_iop name f loc (args_val: value_type list) (ctx: runtime_env | [a; b] -> a, b | _ -> builtin_error loc (name ^ " expects 2 arguments") in

- match (get_int l), (get_int r) with - | Some v, Some w -> Value(Imm(Integer (loc, (f v w)))) + match l, r with + | Vint(v), Vint(w) -> Vint(f v w) | _ -> value_print l; print_string " "; value_print r; builtin_error loc (name ^ " expects Integers as arguments") @@ -147,33 +127,29 @@ let make_symbol loc args_val ctx = | [r] -> r | _ -> builtin_error loc ("symbol_ expects 1 argument") in

- let s = get_string lxp in - match s with - | Some str -> Vsexp(Symbol(loc, str)) + match lxp with + | Vstring(str) -> Vsexp(Symbol(loc, str)) | _ -> builtin_error loc ("symbol_ expects one string as argument")

let make_node loc args_val ctx =

- let head, args = match args_val with - | hd::tl -> (get_sexp hd), tl + let op, args = match args_val with + | Vsexp(s)::tl -> s, tl + | _::tl -> builtin_error loc ("node_ expects sexp as operator") | _ -> builtin_error loc ("node_ expects at least 2 arguments") in

- let op = match head with - | Some sxp -> sxp - | None -> builtin_error loc ("node_ expects sexp as operator") in - - let s = List.map (fun g -> match get_sexp g with - | Some sxp -> sxp - | None -> builtin_error loc ("node_ expects sexp as arguments")) args in + let s = List.map (fun g -> match g with + | Vsexp(sxp) -> sxp + | _ -> builtin_error loc ("node_ expects sexp as arguments")) args in

Vsexp(Node(op, s))

-let make_block loc args_val ctx = Value(type0) -let make_string loc args_val ctx = Value(type0) -let make_integer loc args_val ctx = Value(type0) -let make_float loc args_val ctx = Value(type0) +let make_block loc args_val ctx = Vdummy +let make_string loc args_val ctx = Vdummy +let make_integer loc args_val ctx = Vdummy +let make_float loc args_val ctx = Vdummy

let type_string = type0 let type_mblock = type0 @@ -272,7 +248,7 @@ let default_rctx () = (* populate ctx *) List.fold_left (fun ctx (name, lxp, ltp, f) -> - add_rte_variable (Some name) (Value(lxp)) ctx) + add_rte_variable (Some name) (Vdummy) ctx) rctx typer_builtins ;;

===================================== src/env.ml ===================================== --- a/src/env.ml +++ b/src/env.ml @@ -51,31 +51,42 @@ let str_idx idx = "[" ^ (string_of_int idx) ^ "]"

(* currently, we don't do much *) type value_type = - | Value of lexp + | Vint of int + | Vstring of string + | Vcons of symbol * value_type list + | Vbuiltin | Closure of lexp * (((string option * value_type) ref myers) * (int * int)) (* Macro type *) | Vsexp of sexp (* Unable to eval during macro expansion, only throw if the value is used *) | Vdummy

-let get_value_lexp (vtp: value_type) = - match vtp with - | Value s -> s - | Closure (s, _) -> s - | _ -> env_error dloc "Does not hold a lexp" - -let value_print (vtp: value_type) = +let rec value_print (vtp: value_type) = match vtp with | Closure (lxp, _) -> print_string ("Closure(" ^ (_lexp_to_str (!debug_ppctx) lxp) ^ ")") - | Value s -> lexp_print s | Vsexp sxp -> sexp_print sxp - | _ -> print_string "value_print_dummy" + | Vint(i) -> print_int i; + | Vstring(s) -> print_string (""" ^ s ^ """) + | Vcons ((_, n), []) -> print_string n + | Vcons ((_, n), args) -> + print_string ("(" ^ n); + List.iter (fun arg -> print_string " "; value_print arg) args; + print_string ")";

-let value_location (vtp: value_type) = lexp_location (get_value_lexp vtp) + | Vdummy -> print_string "value_print_dummy" + | Vbuiltin -> print_string "value_print_builtin" + | _ -> print_string "value_print_bug"

+let value_location (vtp: value_type) = + match vtp with + | Vcons ((loc, _), _) -> loc + | Closure (lxp, _) -> lexp_location lxp + (* location info was lost or never existed *) + | _ -> dloc + (* Runtime Environ *) type env_cell = (string option * value_type) ref type runtime_env = (env_cell myers) * (int * int) @@ -161,6 +172,8 @@ let select_n (ctx: runtime_env) n: runtime_env =

((!r), a)

+(* This removes temporary variables from the environment *) +(* and create a clean context free of function arguments *) let temp_ctx (ctx: runtime_env): runtime_env = let (l, (osize, _)) = ctx in let tsize = length l in

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -74,12 +74,12 @@ let rec _eval lxp ctx i: (value_type) = match lxp with (* Leafs *) (* ---------------- *) - | Imm(v) -> Value(lxp) - | Inductive (_, _, _, _) as e -> Value(e) - | Cons (_, _) as e -> Value(e) - - (* Lambda's body is evaluated when called *) - | Lambda (_, _, _, lxp) -> Closure(lxp, ctx) + | Imm(Integer (_, i)) -> Vint(i) + | Imm(String (_, s)) -> Vstring(s) + | Inductive (_, _, _, _) -> Vdummy + | Cons (_, label) -> Vcons (label, []) + | Lambda (_, _, _, lxp) -> Closure(lxp, ctx) + | Builtin _ -> Vbuiltin

(* Return a value stored in the env *) | Var((loc, name), idx) as e -> eval_var ctx e ((loc, name), idx) @@ -90,9 +90,6 @@ 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 *) @@ -110,7 +107,7 @@ let rec _eval lxp ctx i: (value_type) =

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

and eval_var ctx lxp v = let ((loc, name), idx) = v in @@ -128,19 +125,7 @@ and eval_call ctx i lname args call =

let rec eval_call body args ctx = match body, args with - (* first lambda *) - | Value (lxp), hd::tl -> (match lxp with - | Cons _ -> - let cons_args = List.map (fun g -> - (Aexplicit, (get_value_lexp g))) args_val in - Value(Call(lname, (cons_args))) - | _ -> - (* Push first arg *) - let nctx = add_rte_variable None hd ctx in - (* eval first lambda *) - let ret = _eval lxp nctx (i + 1) in - - eval_call ret tl nctx) + | Vcons (n, []), _ -> Vcons(n, args)

(* we add an argument to the closure *) | Closure (lxp, ctx), hd::tl -> @@ -150,7 +135,10 @@ and eval_call ctx i lname args call =

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

@@ -158,114 +146,61 @@ and eval_call ctx i lname args call =

and eval_case ctx i loc target pat dflt = (* Eval target *) - let v = (get_value_lexp (_eval target ctx (i + 1))) in - - let (_, (osize, _)) = ctx in (* number of variable declared outside *) - let csize = get_rte_size ctx in (* current size *) - let offset = csize - osize in - - (* Get inductive type from a constructor *) - let get_inductive_ref lxp = - match lxp with - | Cons(((_, vname), idx), (_, cname)) ->( - let info = (get_value_lexp - (get_rte_variable (Some vname) (idx + offset) ctx)) in - let ctor_def = match info with - | Inductive(_, _, _, c) -> c - | _ -> eval_error loc "Not an Inductive Type" in - info, ctor_def) - | _ -> eval_error loc "Target is not a Constructor" in - - (* I think checks should be in lexp not done during eval *) - (* check if a constructor 'cname' exist *) - let check_ctor cname cargs ctor_def = - try let targs = (SMap.find cname ctor_def) in - let n_targs = List.length targs in - let n_cargs = List.length cargs in - - match (n_targs - n_cargs) with - | 0 -> cname, cargs - | _ -> eval_error loc ("Constructor not applied. " ^ - cname ^ " expected " ^ (string_of_int n_targs) ^ " arg(s)." ^ - " Given " ^ (string_of_int n_cargs) ^ " arg(s).") - - with Not_found -> - eval_error loc ("Constructor "" ^ cname ^ "" does not exist") in - - (* extract constructor name and check its validity *) - let ctor_name, args = match v with - | Call(Var((_, cname), tp), args) ->( - (* Don't check the constructor this job will be done in lexping *) - cname, args) - - (* get constructor * ) - try let ctor = get_rte_variable None (tp + offset) ctx in - let idt, ctor_def = get_inductive_ref ctor in - check_ctor cname args ctor_def - - (* currently we have a little bug with ctor checking *) - with e -> cname, args) *) - - | Cons(((_, vname), idx), (_, cname)) as ctor -> - let idt, ctor_def = get_inductive_ref ctor in - check_ctor cname [] ctor_def + let v = _eval target ctx (i + 1) in

- | _ -> lexp_print target; print_string "\n"; - lexp_print v; print_string "\n"; + (* extract constructor name and arguments *) + let ctor_name, args = match v with + (* | Call(Var((_, cname), tp), args) -> cname, args *) + | Vcons((_, cname), args) -> cname, args + + | _ -> + (* -- Debug print -- *) + lexp_print target; print_string "\n"; + value_print v; print_string "\n"; + (* -- Crash -- *) eval_error loc "Target is not a Constructor" in

+ let ctor_n = List.length args in + (* Check if a default is present *) let run_default df = match df with - | None -> eval_error loc "Match Failure" - | Some lxp -> _eval lxp ctx (i + 1) in - - let ctor_n = List.length args in + | Some lxp -> _eval lxp ctx (i + 1) + | None -> + (* -- Debug print -- *) + lexp_print target; print_string "\n"; + value_print v; print_string "\n"; + (* -- Crash -- *) + eval_error loc "Match Failure" in

(* Build a filter option *) - let is_true key value = - let (_, pat_args, _) = value in - let pat_n = List.length pat_args in - (* FIXME: Shouldn't pat_n != ctor_n cause an error ? *) - if pat_n = ctor_n && ctor_name = key then - true - else - false in - - (* if the argument is a reference to a variable its index need to be - * shifted *) - let arg_shift xp offset = - match xp with - | Var(a, idx) -> Var(a, idx + offset) - | _ -> xp in + let is_true key (_, pat_args, _) = + (*let pat_n = List.length pat_args in (pat_n = ctor_n) && *) + (ctor_name = key) in

(* Search for the working pattern *) let sol = SMap.filter is_true pat in - if SMap.is_empty sol then - run_default dflt - else - (* Get working pattern *) - let key, (_, pat_args, exp) = SMap.min_binding sol in - - (* count the number of declared variables *) - let case_offset = List.fold_left (fun i g -> - match g with None -> i | _ -> i + 1) - 0 pat_args in - - let toffset = case_offset + offset in - - (* build context *) - let nctx = List.fold_left2 (fun nctx pat arg -> - match pat with - | None -> nctx - | Some (_, (_, name)) -> - let (_, xp) = arg in - let xp = (arg_shift xp toffset) in - add_rte_variable (Some name) (Value(xp)) nctx) - - ctx pat_args args in - (* eval body *) - _eval exp nctx (i + 1) + if SMap.is_empty sol then + run_default dflt + else( + (* Get working pattern *) + let key, (_, pat_args, exp) = SMap.min_binding sol in + + (* build context (List.fold2 has problem with some cases) *) + let rec fold2 nctx pats args = + match pats, args with + | (Some (_, (_, name)))::pats, arg::args -> + let nctx = add_rte_variable (Some name) arg nctx in + fold2 nctx pats args + | None::pats, arg::args -> fold2 nctx pats args + (* Errors *) + | _::_, [] -> eval_warning loc "a) Eval::Case Pattern Error"; nctx + | [], _::_ -> eval_warning loc "b) Eval::Case Pattern Error"; nctx + (* Normal case *) + | [], [] -> nctx in + + let nctx = fold2 ctx pat_args args in + _eval exp nctx (i + 1))

and build_arg_list args ctx i = (* _eval every args *) @@ -274,13 +209,13 @@ and build_arg_list args ctx i = (* Add args inside context *) List.fold_left (fun c v -> add_rte_variable None v c) ctx arg_val

-and eval_decls decls ctx = _eval_decls decls ctx 1 +and eval_decls decls ctx = _eval_decls decls ctx 0 and _eval_decls (decls: ((vdef * lexp * ltype) list)) (ctx: runtime_env) i: runtime_env =

(* Read declarations once and push them *) let ctx = List.fold_left (fun ctx ((_, name), lxp, ltp) -> - add_rte_variable (Some name) (Value(lxp)) ctx) + add_rte_variable (Some name) Vdummy ctx) ctx decls in

(* local ctx saves the number of declared variable inside ctx *) @@ -290,7 +225,7 @@ and _eval_decls (decls: ((vdef * lexp * ltype) list))

(* Read declarations once and push them *) let _, ctx = List.fold_left (fun (idx, ctx) ((_, name), lxp, ltp) -> - + _global_eval_trace := []; let lxp = _eval lxp ctx (i + 1) in let ctx = set_rte_variable idx (Some name) lxp ctx in (idx - 1, ctx)) @@ -310,10 +245,12 @@ and print_eval_trace () = ;;

let eval lxp ctx = + _global_eval_trace := []; _eval lxp ctx 1

let debug_eval lxp ctx = try + _global_eval_trace := []; eval lxp ctx with e -> ( print_rte_ctx (!_global_eval_ctx); @@ -350,7 +287,9 @@ let from_lctx (ctx: lexp_context): runtime_env = let (_, (_, name), exp, _) = !(Myers.nth j env) in

let vxp = match exp with - | Some lxp -> (eval lxp !rctx) + | Some lxp -> (try (eval lxp !rctx) + with e -> lexp_print lxp; raise e) + | None -> Vdummy in

rctx := set_rte_variable j (Some name) vxp (!rctx)

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -167,17 +167,17 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = ) formal_args in (* (arg_kind * vdef * ltype) list *)

- (* -- Should I do that ?? --*) + (* -- 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 + | [] -> 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, (make_type formal type0) + v, type0

(* This case can be inferred *) | Plambda (kind, var, optype, body) -> @@ -330,7 +330,96 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = e

(* Identify Call Type and return processed call *) -and lexp_call (fname: pexp) (_args: sexp list) ctx i = +and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = + let loc = pexp_location fun_name in + + (* Process Arguments *) + 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 + + (* consume Arrows and args together *) + let rec get_return_type i ltp args = + match ltp, args with + | _, [] -> ltp + | Arrow(_, _, _, _, ltp), hd::tl -> (get_return_type (i + 1) ltp tl) + | _, _ -> lexp_warning loc + ("Function was provided with too many args. Expected: " ^ + (string_of_int i)); ltp in + + (* Vanilla : sqr is inferred and (lambda x -> x * x) is returned + * Macro : sqr is returned + * Constructor : a constructor is returned + * Anonymous : lambda *) + + (* retrieve function's body *) + let body, ltp = _lexp_p_infer fun_name ctx (i + 1) in + let ret_type = get_return_type 0 ltp new_args in + + (* handle named functions*) + let named_call (loc, name) = + try (* Check if the function was defined *) + let idx = senv_lookup name ctx in + let vf = (make_var name idx loc) in + + (* Replace a built-in name by builtin so they can be recognized + * during eval *) + if (is_lbuiltin idx ctx) then ( + match env_lookup_expr ctx ((loc, name), idx) with + | None -> lexp_error loc "Unknown builtin"; + Call(vf, new_args), ret_type + + (* a builtin functions *) + | Some e -> Call(e, new_args), ret_type + ) + else Call(vf, new_args), ret_type + with Not_found -> + lexp_error loc ("The function "" ^ name ^ "" was not defined"); + let vf = (make_var name (-1) loc) in + Call(vf, new_args), ltp in + + (* determine function type *) + match fun_name, ltp with + (* Anonymous *) + | ((Plambda _), _) -> Call(body, new_args), ltp + + (* Call to a macro *) + | (Pvar (loc, name), Inductive _) -> + (* look up for definition *) + let idx = senv_lookup name ctx in + let vf = (make_var name idx loc) in + + (* Get the macro *) + let lxp = match env_lookup_expr ctx ((loc, name), idx) with + | None -> lexp_fatal loc "The macro cannot be expanded"; + | Some e -> e in + + print_string "HERE"; + + let rctx = (from_lctx ctx) in + + print_string "HERE"; + + let sxp = match eval lxp rctx with + | Vsexp(sxp) -> sxp + | v -> value_print v; + lexp_fatal loc "Macro_ expects sexp" in + + let pxp = pexp_parse sxp in + (* Generated Code *) + let lxp, ltp = _lexp_p_infer pxp ctx (i + 1) in + Call(lxp, new_args), ltp + + (* Call to Vanilla or constructor *) + | (Pvar v, _) -> named_call v + + (* Constructor. This case is rarely used *) + | (Pcons(_, v), _) -> named_call v + + | e, _ -> lexp_fatal (pexp_location e) "This expression cannot be called" + + + (* (* Process Arguments *) let pargs = List.map pexp_parse _args in let largs = _lexp_parse_all pargs ctx i in @@ -354,6 +443,11 @@ and lexp_call (fname: pexp) (_args: sexp list) ctx i = (* retrieve function body *) let body, ltp = _lexp_p_infer fname ctx (i + 1) in

+ (* Check if macro *) + let _ = match ltp with + | Inductive (_, (_, "built-in"), [], _) -> lexp_print body; print_string "\n"; + | _ -> () in + try

(* Check if the function was defined *) @@ -381,7 +475,8 @@ and lexp_call (fname: pexp) (_args: sexp list) ctx i =

(* Is it a macro ? *) | Some Cons (((_, "Macro"), _), (_, "Macro_")) -> - + Call(vf, new_args), type_macro + (* let lxp = match largs with | [lxp] -> lxp | hd::tl -> lexp_error loc "Macro_ expects one lexp"; hd @@ -395,7 +490,7 @@ and lexp_call (fname: pexp) (_args: sexp list) ctx i = | v -> lexp_fatal loc "Macro_ expects sexp" in

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

(* a builtin functions *) | Some e -> Call(e, new_args), ret_type @@ -406,7 +501,7 @@ and lexp_call (fname: pexp) (_args: sexp list) ctx i = (* Don't stop even if an error was found *) lexp_error loc ("The function "" ^ name ^ "" was not defined"); let vf = (make_var name (-1) loc) in - Call(vf, new_args), ltp end + Call(vf, new_args), ltp end *)

(* Read a pattern and create the equivalent representation *) and lexp_read_pattern pattern exp target ctx:

===================================== tests/env_test.ml ===================================== --- a/tests/env_test.ml +++ b/tests/env_test.ml @@ -37,7 +37,7 @@ open Env

let rctx = default_rctx ()

-let make_val value = Imm(String(dloc, value)) +let make_val value = Vstring(value)

let _ = (add_test "ENV" "Set Variables" (fun () -> @@ -55,13 +55,13 @@ let _ = (add_test "ENV" "Set Variables" (fun () -> let n = (List.length var) - 1 in

let rctx = List.fold_left (fun ctx (n, t, _) -> - add_rte_variable n (Value(t)) ctx) + add_rte_variable n (Vdummy) ctx) rctx var in

print_rte_ctx rctx;

let rctx, _ = List.fold_left (fun (ctx, idx) (n, _, v) -> - ((set_rte_variable idx n (Value(v)) ctx), idx - 1)) + ((set_rte_variable idx n (Vdummy) ctx), idx - 1)) (rctx, n) var in

print_rte_ctx rctx;

===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -37,13 +37,6 @@ open Eval (* reset_eval_trace *) open Builtin open Env

-let get_int lxp = - let lxp = get_value_lexp lxp in - match lxp with - | Imm(Integer(_, l)) -> l - | _ -> (-40); -;; - (* default environment *) let lctx = default_lctx () let rctx = default_rctx () @@ -64,7 +57,7 @@ let _ = (add_test "EVAL" "Variable Cascade" (fun () -> let ret = eval_expr_str ecode lctx rctx in

match ret with - | [r] -> expect_equal_int (get_int r) 10 + | [Vint(r)] -> expect_equal_int r 10 | _ -> failure ()) );;

@@ -86,7 +79,7 @@ let _ = (add_test "EVAL" "Let" (fun () -> let ret = eval_expr_str ecode lctx rctx in (* Expect a single result *) match ret with - | [r] -> expect_equal_int (get_int r) 30 + | [Vint(r)] -> expect_equal_int r 30 | _ -> failure ()) ) ;; @@ -109,7 +102,7 @@ let _ = (add_test "EVAL" "Lambda" (fun () -> let ret = eval_expr_str "(sqr 4);" lctx rctx in (* Expect a single result *) match ret with - | [r] -> expect_equal_int (get_int r) (4 * 4) + | [Vint(r)] -> expect_equal_int r (4 * 4) | _ -> failure ()) ) ;; @@ -131,7 +124,7 @@ let _ = (add_test "EVAL" "Nested Lambda" (fun () -> let ret = eval_expr_str "(cube 4);" lctx rctx in (* Expect a single result *) match ret with - | [r] -> expect_equal_int (get_int r) (4 * 4 * 4) + | [Vint(r)] -> expect_equal_int r (4 * 4 * 4) | _ -> failure ()) ) ;; @@ -175,7 +168,7 @@ let _ = (add_test "EVAL" "Inductive::Case" (fun () -> ctr0 = inductive-cons idt ctr0; e = 20; ctr1 = inductive-cons idt ctr1; f = 30; ctr2 = inductive-cons idt ctr2; g = 40; - ctr3 = inductive-cons idt ctr2; h = 50; + ctr3 = inductive-cons idt ctr3; h = 50;

a = (ctr1 (ctr2 ctr0)); y = 2; b = (ctr2 (ctr2 ctr0)); z = 3; @@ -194,10 +187,10 @@ let _ = (add_test "EVAL" "Inductive::Case" (fun () -> let ret = eval_expr_str rcode lctx rctx in (* Expect 3 results *) match ret with - | [a; b; c] -> - let t1 = expect_equal_int (get_int a) 1 in - let t2 = expect_equal_int (get_int b) 2 in - let t3 = expect_equal_int (get_int c) 3 in + | [Vint(a); Vint(b); Vint(c)] -> + let t1 = expect_equal_int a 1 in + let t2 = expect_equal_int b 2 in + let t3 = expect_equal_int c 3 in if t1 = 0 && t2 = 0 && t3 = 0 then success () else @@ -240,10 +233,10 @@ let _ = (add_test "EVAL" "Inductive::Recursive Call" (fun () -> let ret = eval_expr_str rcode lctx rctx in (* Expect a 3 results *) match ret with - | [a; b; c] -> - let t1 = expect_equal_int (get_int a) 0 in - let t2 = expect_equal_int (get_int b) 1 in - let t3 = expect_equal_int (get_int c) 2 in + | [Vint(a); Vint(b); Vint(c)] -> + let t1 = expect_equal_int a 0 in + let t2 = expect_equal_int b 1 in + let t3 = expect_equal_int c 2 in if t1 = 0 && t2 = 0 && t3 = 0 then success () else @@ -277,10 +270,10 @@ let _ = (add_test "EVAL" "Inductive::Nat Plus" (fun () -> let ret = eval_expr_str rcode lctx rctx in (* Expect a 3 results *) match ret with - | [a; b; c] -> - let t1 = expect_equal_int (get_int a) 2 in - let t2 = expect_equal_int (get_int b) 2 in - let t3 = expect_equal_int (get_int c) 3 in + | [Vint(a); Vint(b); Vint(c)] -> + let t1 = expect_equal_int a 2 in + let t2 = expect_equal_int b 2 in + let t3 = expect_equal_int c 3 in if t1 = 0 && t2 = 0 && t3 = 0 then success () else @@ -314,11 +307,11 @@ let _ = (add_test "EVAL" "Mutually Recursive Definition" (fun () -> let ret = eval_expr_str rcode lctx rctx in (* Expect a 3 results *) match ret with - | [a; b; c; d] -> - let t1 = expect_equal_int (get_int a) 1 in - let t2 = expect_equal_int (get_int b) 0 in - let t3 = expect_equal_int (get_int c) 0 in - let t4 = expect_equal_int (get_int d) 1 in + | [Vint(a); Vint(b); Vint(c); Vint(d)] -> + let t1 = expect_equal_int a 1 in + let t2 = expect_equal_int b 0 in + let t3 = expect_equal_int c 0 in + let t4 = expect_equal_int d 1 in if t1 = 0 && t2 = 0 && t3 = 0 && t4 = 0 then success () else @@ -345,10 +338,10 @@ let _ = (add_test "EVAL" "Partial Application" (fun () -> let ret = eval_expr_str rcode lctx rctx in (* Expect a 3 results *) match ret with - | [a; b; c] -> - let t1 = expect_equal_int (get_int a) 2 in - let t2 = expect_equal_int (get_int b) 3 in - let t3 = expect_equal_int (get_int c) 4 in + | [Vint(a); Vint(b); Vint(c)] -> + let t1 = expect_equal_int a 2 in + let t2 = expect_equal_int b 3 in + let t3 = expect_equal_int c 4 in if t1 = 0 && t2 = 0 && t3 = 0 then success () else @@ -364,29 +357,26 @@ 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 a 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; + | nil => nil + | cons hd tl => tl; ";;

let _ = (add_test "EVAL" "List" (fun () -> @@ -398,18 +388,18 @@ let _ = (add_test "EVAL" "List" (fun () ->

let rctx, lctx = eval_decl_str dcode lctx rctx in

- let rcode = "(length my_list); - (head my_list); - (head (tail my_list));" in + let rcode = "(length Int my_list); + (head Int my_list); + (head Int (tail Int my_list));" in

(* Eval defined lambda *) let ret = eval_expr_str rcode lctx rctx in (* Expect a 3 results *) match ret with - | [a; b; c] -> - let t1 = expect_equal_int (get_int a) 4 in - let t2 = expect_equal_int (get_int b) 1 in - let t3 = expect_equal_int (get_int c) 2 in + | [Vint(a); Vint(b); Vint(c)] -> + let t1 = expect_equal_int a 4 in + let t2 = expect_equal_int b 1 in + let t3 = expect_equal_int c 2 in if t1 = 0 && t2 = 0 && t3 = 0 then success () else

===================================== tests/macro_test.ml ===================================== --- a/tests/macro_test.ml +++ b/tests/macro_test.ml @@ -37,12 +37,6 @@ open Eval (* reset_eval_trace *) open Builtin open Env

-let get_int lxp = - let lxp = get_value_lexp lxp in - match lxp with - | Imm(Integer(_, l)) -> l - | _ -> (-40); -;;

(* default environment *) let lctx = default_lctx () @@ -72,7 +66,7 @@ let _ = (add_test "MACROS" "macros base" (fun () -> let ret = eval_expr_str ecode lctx rctx in

match ret with - | [r] -> expect_equal_int (get_int r) (3 * 3) + | [Vint(r)] -> expect_equal_int r (3 * 3) | _ -> failure ()) );;

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