[Typer] [Git][monnier/typer][master] 4 commits: declaration fix bis

Setepenre pushed to branch master at Stefan / Typer

Commits: 2a292311 by Pierre Delaunay at 2016-03-11T10:17:24-05:00 declaration fix bis

- - - - - e594f7fe by Pierre Delaunay at 2016-03-13T12:49:23-04:00 Basic utest lib

- - - - - a37b8648 by Pierre Delaunay at 2016-03-13T14:31:28-04:00 tests

- - - - - 881f7888 by Pierre Delaunay at 2016-03-13T19:51:00-04:00 fix lexp_decl double decl

- - - - -

25 changed files:

- .gitignore - GNUmakefile - doc/Compiler Structure.md - − samples/case.typer - − samples/debug_test.typer - − samples/functions.typer - − samples/inductives.typer - − samples/let.typer - − samples/lexer_test.typer - − samples/lexp_test.typer - − samples/pretoken_test.typer - src/debruijn.ml - src/eval.ml - src/fmt.ml - src/lparse.ml - src/pexp.ml - tests/REPL.ml - tests/debug.ml - + tests/eval_test.ml - tests/full_debug.ml - − tests/let_test.ml - + tests/lexp_test.ml - + tests/pexp_test.ml - + tests/utest_lib.ml - tests/utest_main.ml

Changes:

===================================== .gitignore ===================================== --- a/.gitignore +++ b/.gitignore @@ -17,3 +17,4 @@ manual.?? #*# test__.ml _temp_hack +test__.typer

===================================== GNUmakefile ===================================== --- a/GNUmakefile +++ b/GNUmakefile @@ -1,6 +1,9 @@ RM=rm -f

+SRC_FILES := $(wildcard ./src/*.ml) +CPL_FILES := $(wildcard ./_build/src/*.cmo) TEST_FILES := $(wildcard ./tests/*_test.ml) + # This is for windows: windows version is old ifeq ($(OS),Windows_NT) SHELL=C:/Windows/System32/cmd.exe @@ -21,12 +24,17 @@ debug: ityper: ocamlbuild tests/REPL.native -I src -cflag -rectypes mv _build/tests/REPL.native _build/ityper - -tests: - # Build tests + +tests-build: +# ============================ +# Build tests +# ============================ $(foreach test, $(TEST_FILES), ocamlbuild $(subst ./,,$(subst .ml,.native,$(test))) -I src -cflag -rectypes;)

- # Run tests +tests-run: +# ============================ +# Run tests +# ============================ ocamlbuild tests/utest_main.native ./_build/tests/utest_main.native

@@ -35,8 +43,8 @@ doc-tex: texi2pdf ./doc/manual.texi --pdf --build=clean

# Make implementation doc -#doc-ocaml: -# ocamldoc +doc-ocaml: + ocamldoc -html -d _build $(SRC_FILES)

.PHONY: ityper .PHONY: typer

===================================== doc/Compiler Structure.md ===================================== --- a/doc/Compiler Structure.md +++ b/doc/Compiler Structure.md @@ -45,7 +45,7 @@ Functions: sexp_parse sexp node_parse_string str

-* Sexp -> Pexp: ~ Check grammar +* Sexp -> Pexp: ~ Lexical Analysis

Identify nodes and transform them into language primitives

@@ -57,7 +57,7 @@ Functions: pexp_p_decls % For top level declaration pexp_p_toplevel % Parses using the appropriate parsing function

-* Pexp -> Lexp: ~ Check scopes/ declaration +* Pexp -> Lexp: ~ Semantic Analysis

Replace variable name by their (reverse) index in the environment. Lexps are very close to pexps

===================================== samples/case.typer deleted ===================================== --- a/samples/case.typer +++ /dev/null @@ -1,45 +0,0 @@ -% ------------------------------------------- -% Inductive type -% ------------------------------------------- - - -% -% Constructor with not args are not processed -% correctly in case . I need type info to differentiate them -% from variables -% - -% definition -inductive_ (dummy_Nat) (zero) (succ Nat); - -% declaration -% Nat : Type; % This line is not parsed -Nat = inductive_ (dummy_Nat) (zero) (succ Nat); % zero is not parsed - -% only inductive-cons is available -inductive-cons Nat succ; - -% Usage -zero = inductive-cons Nat zero; % those are aliases -succ = inductive-cons Nat succ; - -one = (succ (zero)); - -% Case test -% x = (succ zero); -x = (succ (succ zero)); - -% Simple -case x - | succ y => y - | _ => (2 + 4); - -% recursive -tonum = lambda x -> case x - | (succ y) => (1 + (tonum y)) - | _ => 0; - -(tonum x); - - - \ No newline at end of file

===================================== samples/debug_test.typer deleted ===================================== --- a/samples/debug_test.typer +++ /dev/null @@ -1,41 +0,0 @@ -% -% Pexp Debugging: Everything must work -% This is not meant to be correct Typer input -% - -{a => "This is a block"}; % Pimm: Block -"This is a String"; % Pimm: String -12; % Pimm: Integer -12.12; % Pimm: Float - -% Pvar -ab; - -% let_in -let a = b in - c = b -; - -% PCall -(function arg1 arg2 arg3); - -% Parrow -a -> 1; -a => 2; -a ≡> 1; - -% Lambda -a = lambda (x, y) -> x + y; -b = lambda (x, y) => x * y; -c = lambda (x, y) ≡> x / y; - -% case -case (a, b) - | (1, 2) => 1 - | (_, _) => 3 -; - -% inductive -% Nat : Type -Type = inductive_ (Type_Label) (zero) (succ Type); -inductive_ (Type_Label) (zero) (succ Type); \ No newline at end of file

===================================== samples/functions.typer deleted ===================================== --- a/samples/functions.typer +++ /dev/null @@ -1,32 +0,0 @@ -% ------------------------------------------- -% Function Calls -% ------------------------------------------- - -% define sqrt -sqr = lambda (x : Nat) -> x * x; - -(sqr 2); - -% define cube -cube = lambda (x : Nat) -> x * (sqr x); - -(cube 3); - -% explicit -mult = lambda (x : Nat) -> lambda (y : Nat) -> (y * x); - -(mult 2 3); - -% Not Working -% --------------------- - -% implicit (Type annotation introduce a bug) -% cube = lambda x y -> (x * y); - - -% partial application -partial_mul = (mult 2); - -(partial_mul 3); - -"FUNCTION END"; \ No newline at end of file

===================================== samples/inductives.typer deleted ===================================== --- a/samples/inductives.typer +++ /dev/null @@ -1,23 +0,0 @@ -% ------------------------------------------- -% Inductive type -% ------------------------------------------- - -% definition -inductive_ (dummy_Nat) (zero) (succ Nat); - - -% declaration -% Nat : Type; % This line is not parsed -Nat = inductive_ (dummy_Nat) (zero) (succ Nat); % zero is not parsed - - -% only inductive-cons is available -inductive-cons Nat succ; - -% Usage -zero = inductive-cons Nat zero; % those are aliases -succ = inductive-cons Nat succ; - -one = (succ (zero)); -one = (succ (zero)); -one = (succ (zero)); \ No newline at end of file

===================================== samples/let.typer deleted ===================================== --- a/samples/let.typer +++ /dev/null @@ -1,35 +0,0 @@ -% ------------------------------------------- -% Let -% ------------------------------------------- - - -let c = 1; a = 5; b = 10; d = 3; in - a + b; - - -a = 1; -b = 2; -c = 3; -d = 4; - - -let a = 3; g = 1; e = 1; f = 3; in - e + a + f + d; - - -% Not Implemented -% ---------------------- - - -% Type definition -Nat = inductive_ (dummy_Nat) (zero) (succ Nat); - -zero = inductive-cons Nat zero; -succ = inductive-cons Nat succ; - -v = (succ (succ zero)); - -% Recursive Let -let odd = lambda n -> case n | (zero) => false | (succ y) => (even y); - even = lambda n -> case n | (zero) => true | (succ y) => (odd y); in - (odd v) \ No newline at end of file

===================================== samples/lexer_test.typer deleted ===================================== --- a/samples/lexer_test.typer +++ /dev/null @@ -1,33 +0,0 @@ -%% This file check if typer recognize correctly tokens - -%% builtin types -%% ---------------- - -%% String -a => "The answer is 42"; - -%% Integer -b => 11; - -%% Float -c => 3.14; - -%% Something -C => 3.14.14; - -%% Case -%% ---------------- - -case (a,b) - | (Foo, Foo) => 3.14 - | (Bar, Bar) => 3.15 -; - - -%% Stuff -%% ---------------- - -%% Block -{ - a => "This is a Block"; -} \ No newline at end of file

===================================== samples/lexp_test.typer deleted ===================================== --- a/samples/lexp_test.typer +++ /dev/null @@ -1,18 +0,0 @@ - - - -% x : Nat; -x = 4; - -x + x + x; % 12 -x * x * x; % 64 - -sqr = lambda x -> x * x; -% cube = lambda x -> x * x * x; - -(sqr x); % 16 -%(cube x); - -cube = lambda x -> x * (sqr x); -(cube x); % 64 -

===================================== samples/pretoken_test.typer deleted ===================================== --- a/samples/pretoken_test.typer +++ /dev/null @@ -1,15 +0,0 @@ -%% This file check if typer recognize correctly pretokens - -%% Preblock -%% --> hum, hum - - -%% Prestring -%% --> String variable -b = "The answer is 42"; - - -%% Pretoken -%% --> Everything else - -a = 3; \ No newline at end of file

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -90,7 +90,7 @@ let _add_var_env variable ctx = let make_lexp_context = (_make_senv_type, _make_myers);;

(* return its current DeBruijn index *) -let rec senv_lookup (name: string) (ctx: lexp_context) = +let rec senv_lookup (name: string) (ctx: lexp_context): int = let ((n, map), _) = ctx in n - (StringMap.find name map) - 1 ;;

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -39,10 +39,6 @@ open Fmt open Debruijn open Grammar

-(* Value type *) -type value_type = - | Void - | Val of lexp

let _eval_error loc msg = msg_error "eval" loc msg; @@ -84,7 +80,7 @@ let get_function_name fname = let get_int lxp = match lxp with | Imm(Integer(_, l)) -> l - | _ -> lexp_print (Ltexp(lxp)); -40 + | _ -> lexp_print lxp; -40 ;;

(* Runtime Environ *) @@ -92,7 +88,11 @@ type runtime_env = (string option * lexp) myers let make_runtime_ctx = nil;; let add_rte_variable name x l = (cons (name, x) l);;

-let get_rte_variable idx l = let (_, x) = (nth (idx) l) in x;; +let get_rte_variable (idx: int) (l: runtime_env): lexp = + let (_, x) = (nth idx l) in x +;; + +let get_rte_size (l: runtime_env): int = length l;;

let print_rte_ctx l = print_myers_list l (fun (n, g) -> @@ -100,7 +100,7 @@ let print_rte_ctx l = print_myers_list l match n with | Some m -> lalign_print_string m 12; print_string " | " | None -> print_string (make_line ' ' 12); print_string " | " in - lexp_print (Ltexp(g)); print_string "\n") + lexp_print g; print_string "\n") ;;

@@ -113,29 +113,25 @@ let nfirst_rte_var n ctx = loop 0 [] ;;

-(* *) -let rec eval_toplevel ltop ctx: (value_type * runtime_env) = - global_trace := []; (* Clean up trace info *) - (* I have to use a sexp because declaration are not "carried" *) - match ltop with - (* Eval expression and return results *) - | Ltexp(x) -> - let a, b = _eval x ctx 0 in - Val(a), ctx - (* Add declaration to environment. return void *) - | Ltdecl(a, b, c) -> Void, (eval_decl (a, b, c) ctx) +(* currently, we don't do much *) +type value_type = lexp + +(* This is an internal definition + * 'i' is the recursion depth used to print the call trace *) +let rec _eval lxp ctx i: (value_type) =

-(* _eval is an internal definition you should use eval or eval_toplevel *) -and _eval lxp ctx i: (lexp * runtime_env) = + (if i > 255 then + raise (internal_error "Recursion Depth exceeded")); + add_call lxp i; match lxp with (* This is already a leaf *) - | Imm(v) -> lxp, ctx + | Imm(v) -> lxp

(* Return a value stored in the environ *) | Var((loc, name), idx) -> begin try - (get_rte_variable idx ctx), ctx + (get_rte_variable idx ctx) with Not_found -> print_string ("Variable: " ^ name ^ " was not found | "); @@ -144,13 +140,10 @@ and _eval lxp ctx i: (lexp * runtime_env) =

(* this works for non recursive let *) | Let(_, decls, inst) -> begin - (* First we _evaluate all declaration then we eval the instruction *) - + (* First we _evaluate all declaration *) let nctx = build_ctx decls ctx i in - - let value, nctx = _eval inst nctx (i + 1) in - (* return old context as we exit let's scope*) - value, ctx end + (* Then we eval the body *) + _eval inst nctx (i + 1) end

(* Function call *) | Call (lname, args) -> ( @@ -165,7 +158,7 @@ and _eval lxp ctx i: (lexp * runtime_env) =

let l = get_int (get_rte_variable 0 nctx) in let r = get_int (get_rte_variable 1 nctx) in - Imm(Integer(dloc, l + r)), ctx + Imm(Integer(dloc, l + r))

(* _*_ is reas as a single function with x args *) | Var((_, name), _) when name = "_*_" -> @@ -175,31 +168,35 @@ and _eval lxp ctx i: (lexp * runtime_env) = let varg = List.map (fun g -> get_int g) vint in let v = List.fold_left (fun a g -> a * g) 1 varg in

- Imm(Integer(dloc, v)), ctx + Imm(Integer(dloc, v))

(* This is a named function call *) - (* TODO: handle partial application *) | Var((_, name), idx) -> - + (* Check if the call is a constructor call *) + (* get function body *) let body = get_rte_variable idx ctx in + (* Add args in the scope *) let nctx = build_arg_list args ctx i in - let e, nctx = (_eval body nctx (i + 1)) in - - (* we exit function and send back old ctx *) - e, ctx + (* eval body *) + _eval body nctx (i + 1)

(* TODO Everything else *) (* Which includes a call to a lambda *) - | _ -> Imm(String(dloc, "Funct Not Implemented")), ctx) + | _ -> Imm(String(dloc, "Funct Not Implemented")))

+ (* Lambdas have one single mandatory argument *) + (* Nested lambda are collapsed then executed *) + (* I am thinking about building a 'get_free_variable' to be able to *) + (* handle partial application i.e build a new lambda if Partial App *) | Lambda(_, vr, _, body) -> begin let (loc, name) = vr in (* Get first arg *) let value = (get_rte_variable 0 ctx) in let nctx = add_rte_variable (Some name) value ctx in

+ (* Collapse nested lambdas *) let rec build_body bd idx nctx = match bd with | Lambda(_, vr, _, body) -> @@ -212,45 +209,61 @@ and _eval lxp ctx i: (lexp * runtime_env) = | _ -> bd, nctx in

let body, nctx = build_body body 1 nctx in - - let e, nctx = _eval body nctx (i + 1) in - e, ctx end + (* eval lambda body *) + _eval body nctx (i + 1) end

(* Inductive is a type declaration. We have nothing to eval *) - | Inductive (_, _, _, _) as e -> e, ctx + | Inductive (_, _, _, _) as e -> e

(* inductive-cons build a type too? *) - | Cons (_, _) as e -> e, ctx + | Cons (_, _) as e -> e

(* Case *) | Case (loc, target, _, pat, dflt) -> begin

(* Eval target *) - let v, nctx = _eval target ctx (i + 1) in + let v = _eval target ctx (i + 1) in + + let check_ctor ctor_name type_idx = + let info = get_rte_variable type_idx ctx in + match info with + | Inductive(_, _, _, ctor_def) -> SMap.find ctor_name ctor_def + | _ -> _eval_error loc "Target is not a Constructor" in + + (* 'v' must be a constructor *) + let ctor_name, args, idx = match v with

- (* V must be a constructor Call *) - let ctor_name, args = match v with + (* multi arg constructor are parsed as Call *) | Call(lname, args) -> (match lname with - | Var((_, ctor_name), _) -> ctor_name, args - | _ -> _eval_error loc "Target is not a Constructor" ) - (* - | Cons((_, idx), (_, cname)) -> begin - (* retrieve type definition *) - let info = get_rte_variable idx ctx in - let Inductive(_, _, _, ctor_def) = info in - try let args = SMap.find cname ctor_def in - cname, args - with - Not_found -> - _eval_error loc "Constructor does not exist" end *) + | Var((_, ctor_name), idx) -> + let offset = (get_rte_size ctx) - idx - 1 in + let tidx = idx + offset in + ctor_name, args, tidx + + | _ -> _eval_error loc "Target is not a Constructor" ) + + | Cons((_, idx), (_, cname)) -> + let offset = (get_rte_size ctx) - idx - 1 in + let tidx = idx + offset in + cname, [], tidx

- | _ -> lexp_print (Ltexp(target)); + | _ -> lexp_print v; _eval_error loc "Can't match expression" in + + (* Check if the constructor was defined *) + let targs = try check_ctor ctor_name idx + with Not_found -> _eval_error loc "Constructor does not exist" in

+ (* Check number of args *) + let n_targs = List.length targs in + let n_args = List.length args in + (if n_targs != n_args then + _eval_error loc "Wrong number of arguments"); + (* Check if a default is present *) let run_default df = match df with - | None -> Imm(String(loc, "Match Failure")), ctx + | None -> Imm(String(loc, "Match Failure")) | Some lxp -> _eval lxp ctx (i + 1) in

let ctor_n = List.length args in @@ -279,19 +292,16 @@ and _eval lxp ctx i: (lexp * runtime_env) = | Some (_, (_, name)) -> let (_, xp) = cl in add_rte_variable (Some name) xp nctx)

- nctx pat_args args in - - let r, nctx = _eval exp nctx (i + 1) in - (* return old context as we exist the case *) - r, ctx end + ctx pat_args args in + (* eval body *) + _eval exp ctx (i + 1) end

- | _ -> Imm(String(dloc, "eval Not Implemented")), ctx + | _ -> Imm(String(dloc, "eval Not Implemented"))

and build_arg_list args ctx i = (* _eval every args *) let arg_val = List.map ( - fun (k, e) -> - let (v, c) = _eval e ctx (i + 1) in v) + fun (k, e) -> _eval e ctx (i + 1)) args in

(* Add args inside context *) @@ -302,47 +312,35 @@ and build_ctx decls ctx i = | [] -> ctx | hd::tl -> let (v, exp, tp) = hd in - let (value, nctx) = _eval exp ctx (i + 1) in - let nctx = add_rte_variable None value nctx in - build_ctx tl nctx (i + 1) + let value = _eval exp ctx (i + 1) in + let nctx = add_rte_variable None value ctx in + build_ctx tl nctx i

and eval_decl ((l, n), lxp, ltp) ctx = add_rte_variable (Some n) lxp ctx + +(* Eval a declaration if a main is found it is returned *) +and eval_decls (decls: ((vdef * lexp * ltype) list)) + (ctx: runtime_env): runtime_env = + let rec loop decls ctx = + match decls with + | [] -> ctx + | hd::tl -> + let ((_, n), lxp, ltp) = hd in + let nctx = add_rte_variable (Some n) lxp ctx in + loop tl nctx in + + loop decls ctx

-and print_eval_result i tlxp = - match tlxp with - | Void -> () - | Val(lxp) -> +and print_eval_result i lxp = print_string " Out["; ralign_print_int i 2; print_string "] >> "; match lxp with | Imm(v) -> sexp_print v; print_string "\n" - | e -> lexp_print (Ltexp(e)); print_string "\n" -;; - - -let print_first n l f = - let rec loop i l = - match l with - | [] -> () - | hd::tl -> - if i < n then ((f i hd); loop (i + 1) tl;) - else () in - loop 0 l -;; + | e -> lexp_print e; print_string "\n"

-let _print_ct_tree i = - print_string " "; - let rec loop j = - if j = i then () else - match j with - | _ when (j mod 2) = 0 -> print_char '|'; loop (j + 1) - | _ -> print_char ':'; loop (j + 1) in - loop 0 -;; - -let print_call_trace () = +and print_call_trace () = print_string (make_title " CALL TRACE ");

let n = List.length !global_trace in @@ -350,63 +348,36 @@ let print_call_trace () = print_string (make_sep '-');

let racc = List.rev !global_trace in - print_first 20 racc (fun j (i, g) -> + print_first 50 racc (fun j (i, g) -> _print_ct_tree i; print_string "+- "; print_string (lexp_to_string g); print_string ": "; - lexp_print (Ltexp(g)); print_string "\n"); + lexp_print g; print_string "\n");

print_string (make_sep '='); ;;

+(* eval_expr *) let eval lxp ctx = try - let r, c = eval_toplevel lxp ctx in - (r, c) + (_eval lxp ctx 1) with e -> ( print_rte_ctx ctx; print_call_trace (); raise e) ;;

- - -let evalprint lxp ctx = - let v, ctx = (eval_toplevel lxp ctx) in - print_eval_result 0 v; - ctx -;; - (* Eval a list of lexp *) -let eval_all lxps rctx = - let rec _eval_all lxps acc rctx = - match lxps with - | [] -> (List.rev acc), rctx - | hd::tl -> - let lxp, rctx = eval hd rctx in - _eval_all tl (lxp::acc) rctx in - (_eval_all lxps [] rctx) -;; +let eval_all lxps rctx = List.map (fun g -> eval g rctx) lxps;;

-(* Eval a string given a context *) -let eval_string (str: string) tenv grm limit lxp_ctx rctx = - let lxps, lxp_ctx = lexp_parse_string str tenv grm limit lxp_ctx in - (eval_all lxps rctx), lxp_ctx +(* Eval String + * ---------------------- *) +let eval_expr_str str lctx rctx = + global_trace := []; + let lxps, lctx = lexp_expr_str str lctx in + (eval_all lxps rctx) ;;

-(* EVAL a string. Contexts are discarded *) -let easy_eval_string str = - let tenv = default_stt in - let grm = default_grammar in - let limit = (Some ";") in - let eval_string str clxp rctx = eval_string str tenv grm limit clxp rctx in - let clxp = make_lexp_context in - (* Those are hardcoded operation *) - let clxp = add_def "_+_" clxp in - let clxp = add_def "_*_" clxp in - let clxp = add_def "_=_" clxp in - - let rctx = make_runtime_ctx in - let (ret, rctx), clxp = (eval_string str clxp rctx) in - ret +let eval_decl_str str lctx rctx = + let lxps, lctx = lexp_decl_str str lctx in + (eval_decls lxps rctx), lctx ;; -

===================================== src/fmt.ml ===================================== --- a/src/fmt.ml +++ b/src/fmt.ml @@ -103,5 +103,27 @@ let make_rheader (head: (((char* int) option * string) list)) = let make_sep c = " " ^ (make_line c 76) ^ "\n";;

+(* used to help visualize the call trace *) +let _print_ct_tree i = + print_string " "; + let rec loop j = + if j = i then () else + match j with + | _ when (j mod 2) = 0 -> print_char '|'; loop (j + 1) + | _ -> print_char ':'; loop (j + 1) in + loop 0 +;; + +(* iterate of first n of a list l and apply f *) +let print_first n l f = + let rec loop i l = + match l with + | [] -> () + | hd::tl -> + if i < n then ((f i hd); loop (i + 1) tl;) + else () in + loop 0 l +;; +

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -68,18 +68,6 @@ type print_context = (bool * int * bool) (* Vdef is exactly similar to Pvar but need to modify our ctx *) let pvar_to_vdef p = p;;

-type ltop = - | Ltexp of lexp - | Ltdecl of vdef * lexp * ltype -;; - - -let lexp_location_toplevel ltp = - match ltp with - | Ltexp(x) -> lexp_location x - | Ltdecl((l, _), _, _) -> l -;; - (* PEXP is not giving SEXP types this is why types are always unknown *)

(* @@ -101,22 +89,8 @@ let lexp_location_toplevel ltp = * *)

-(* Process a top-level expression *) -let rec lexp_p_toplevel (p: ptop) (ctx: lexp_context) = - - (* Identify if the expression is a declaration *) - match p with - (* Declaration *) - | Ptdecl (x, p) -> - let (a, b, c), ctx = lexp_p_decls (x, p, None) ctx in - Ltdecl(a, b, c), ctx - - (* Everything else*) - | Ptexp (x) -> let x, ctx = lexp_parse x ctx in - Ltexp(x), ctx - -(**) -and lexp_parse (p: pexp) (ctx: lexp_context): (lexp * lexp_context) = + +let rec lexp_parse (p: pexp) (ctx: lexp_context): (lexp * lexp_context) = (* So I don't have to extract it *) let tloc = pexp_location p in match p with @@ -137,7 +111,7 @@ and lexp_parse (p: pexp) (ctx: lexp_context): (lexp * lexp_context) =

(* Let, Variable declaration + local scope *) | Plet(loc, decls, body) -> - let decl, nctx = lexp_parse_let decls ctx in + let decl, nctx = lexp_decls decls ctx in (* Body cannot modify context *) let bdy, _ = lexp_parse body nctx in (* Send back old context as we exit the inner scope *) @@ -159,25 +133,28 @@ and lexp_parse (p: pexp) (ctx: lexp_context): (lexp * lexp_context) = | Plambda (kind, var, Some ptype, body) -> (* Add argument to context *) let (loc, vname) = var in + let ltp, nctx = lexp_parse ptype ctx in (* Get Type *) + let nctx = senv_add_var vname loc ctx in - let ltp, nctx = lexp_parse ptype nctx in (* Get Type *) let nctx = env_add_var_info (0, (loc, vname), dlxp, ltp) nctx in

- let ltyp, nctx = lexp_parse ptype nctx in - let lbody, nctx = lexp_parse body nctx in + let lbody, _ = lexp_parse body nctx in

(* Return old context as we exit lambda scope*) - Lambda(kind, var, ltyp, lbody), ctx + Lambda(kind, var, ltp, lbody), ctx

| Plambda (kind, var, None, body) -> let (loc, vname) = var in + let nctx = senv_add_var vname loc ctx in let nctx = env_add_var_info (0, (loc, vname), dlxp, dltype) nctx in

- let lbody, ctx = lexp_parse body nctx in + let lbody, _ = lexp_parse body nctx in Lambda(kind, var, UnknownType(tloc), lbody), ctx

- | Pcall (fname, _args) -> lexp_call fname _args ctx + | Pcall (fname, _args) -> + let r, c = lexp_call fname _args ctx in + r, ctx

(* Pinductive *) | Pinductive (label, [], ctors) -> @@ -201,6 +178,7 @@ and lexp_parse (p: pexp) (ctx: lexp_context): (lexp * lexp_context) =

(* Pcase *) | Pcase (loc, target, patterns) -> + (* I need type info HERE *) let lxp, nctx = lexp_parse target ctx in let ltp = UnknownType(loc) in @@ -212,9 +190,10 @@ and lexp_parse (p: pexp) (ctx: lexp_context): (lexp * lexp_context) = | hd::tl -> let (pat, exp) = hd in (* Create pattern context *) - let (name, iloc, arg), nctx = lexp_read_pattern pat exp lxp nctx in + let (name, iloc, arg), nctx2 = + lexp_read_pattern pat exp lxp nctx in (* parse using pattern context *) - let exp, nctx = lexp_parse exp nctx in + let exp, _ = lexp_parse exp nctx2 in

if name = "_" then loop tl merged (Some exp) @@ -243,7 +222,7 @@ and lexp_call (fname: pexp) (_args: sexp list) ctx = | Pcons (_, (loc, nm)) -> nm, loc | _ -> raise Not_found in

- let largs, fctx = lexp_p_all pargs ctx in + let largs, fctx = lexp_parse_all pargs ctx in let new_args = List.map (fun g -> (Aexplicit, g)) largs in

try @@ -262,7 +241,7 @@ and lexp_call (fname: pexp) (_args: sexp list) ctx =

(* Call to a nameless function *) with Not_found -> - let largs, fctx = lexp_p_all pargs ctx in + let largs, fctx = lexp_parse_all pargs ctx in let new_args = List.map (fun g -> (Aexplicit, g)) largs in (* I think this should not modify context. * if so, funny things might happen when evaluating *) @@ -277,13 +256,19 @@ and lexp_read_pattern pattern exp target ctx: | Ppatany (loc) -> (* Catch all expression nothing to do *) ("_", loc, []), ctx

- | Ppatvar (loc, name) -> - (* FIXME What if it is a constructor with no arg ? *) - - (* Create a variable containing target *) - let nctx = senv_add_var name loc ctx in - let nctx = env_add_var_info (0, (loc, name), target, dltype) nctx in - (name, loc, []), nctx + | Ppatvar (loc, name) ->( + (* FIXME better check *) + try + let idx = senv_lookup name ctx in + (* constructor with no args *) + (name, loc, []), ctx + + (* would it not make a default match too? *) + with Not_found -> + (* Create a variable containing target *) + let nctx = senv_add_var name loc ctx in + let nctx = env_add_var_info (0, (loc, name), target, dltype) nctx in + ("_", loc, []), nctx)

| Ppatcons (ctor_name, args) -> let (loc, name) = ctor_name in @@ -294,7 +279,7 @@ and lexp_read_pattern pattern exp target ctx:

(* Read patterns inside a constructor *) and lexp_read_pattern_args args ctx: - (((arg_kind * vdef) option list) * lexp_context)= + (((arg_kind * vdef) option list) * lexp_context)=

let rec loop args acc ctx = match args with @@ -344,58 +329,24 @@ and lexp_parse_constructors ctors ctx = end in

loop ctors SMap.empty ctx - -(* Merge Type info and variable declaration together *) -(* Type info must be first then declaration else type will be inferred *) -and lexp_merge_info (decls: (pvar * pexp * bool) list) = - match decls with - | [] -> lexp_fatal dloc "Empty Declaration List" - | hd::tl -> (match hd with - (* Declaration without type info *) - | ((l, n1), expr, true) -> ( - match tl with - | [] -> lexp_fatal l "Unused Type info declaration"; - | ((_, _), expr2, true)::_ -> lexp_merge_info tl - | ((_, n2), expr2, _)::_ when n2 != n1 -> - (lexp_warning l "Unused Type info declaration"; - lexp_merge_info tl) - | ((_, _), expr2, _)::ttl -> - ((l, n1), expr2, Some expr), (ttl)) - - (* Declaration without type info *) - | (v, expr, false) -> (v, expr, None), tl) - -(* Add declaration in the environment *) -and lexp_p_decls (decl: (pvar * pexp * pexp option)) ctx = - let ((loc, vname), pxp, _) = decl in - - (* we should add the defined var to ctx *) - let nctx = senv_add_var vname loc ctx in - - (*let idx = senv_lookup vname nctx in *) - let lxp, ltp = lexp_p_infer pxp nctx in - - (* Add Var info*) - let nctx = env_add_var_info (0, (loc, vname), lxp, ltp) nctx in - - (* return processed var *) - ((loc, vname), lxp, ltp), nctx

(* Parse let declaration *) -and lexp_parse_let decls ctx = +and lexp_decls decls ctx: (((vdef * lexp * ltype) list) * lexp_context) =

(* Merge Type info and declaration together *) (* We use a list because order matters and Maps reorder elements *) + (* let rec is_equal target (p:(vdef * pexp option * pexp option)): bool = let ((_, name), _, _) = p in - if name == target then true else false in + if name == target then true else false in *)

- let rec merge_decls (decls: (pvar * pexp * bool) list) merged: - (vdef * pexp option * pexp option) list = + (* merge with a map to guarantee uniqueness. *) + let rec merge_decls (decls: (pvar * pexp * bool) list) merged acc: + ((location * pexp option * pexp option) SMap.t * string list) =

(* we cant evaluate here because variable are not in the environment *) match decls with - | [] -> List.rev merged + | [] -> merged, (List.rev acc) | hd::tl -> match hd with (* Type Info: Var:Type *) @@ -403,24 +354,35 @@ and lexp_parse_let decls ctx = try (* If found its means the instruction was declared * before the type info. Should we allow this? *) - let (vd, inst, _) = List.find (is_equal name) merged in - let new_decl = (vd, inst, Some type_info) in - (merge_decls tl (new_decl::merged)) + let (l, inst, _) = SMap.find name merged in + let new_decl = (l, inst, Some type_info) in + let nmerged = SMap.add name new_decl merged in + (merge_decls tl nmerged acc) with Not_found -> - let new_decl = (loc, name), None, Some type_info in - (merge_decls tl (new_decl::merged)) end + let new_decl = (loc, None, Some type_info) in + let nmerged = SMap.add name new_decl merged in + (merge_decls tl nmerged (name::acc)) end

(* Instruction: Var = expr *) | ((loc, name), inst, false) -> begin try - let (vd, _, ptyp) = List.find (is_equal name) merged in - let new_decl = (vd, Some inst, ptyp) in - (merge_decls tl (new_decl::merged)) + let (l, _, tp) = SMap.find name merged in + let new_decl = (l, Some inst, tp) in + let nmerged = SMap.add name new_decl merged in + (merge_decls tl nmerged acc) + with Not_found -> - let new_decl = ((loc, name), Some inst, None) in - (merge_decls tl (new_decl::merged)) end in + let new_decl = (loc, Some inst, None) in + let nmerged = SMap.add name new_decl merged in + (merge_decls tl nmerged (name::acc)) end in

- let decls = merge_decls decls [] in + let mdecls, ord = merge_decls decls SMap.empty [] in + + (* cast map to list*) + let decls = List.map (fun name -> + let (l, inst, tp) = SMap.find name mdecls in + ((l, name), inst, tp) ) ord + in

(* Add Each Variable to the environment *) let nctx = List.fold_left (fun ctx hd -> @@ -428,9 +390,11 @@ and lexp_parse_let decls ctx = | (_, None, _) -> ctx (* Unused variable: No Instruction *) | ((loc, name), _, _) -> senv_add_var name loc ctx) ctx decls in + + let n_decls = List.length decls in

(* Add Variable info *) - let rec process_var_info dcl_lst _ctx acc = + let rec process_var_info dcl_lst _ctx acc i = match dcl_lst with | [] -> (List.rev acc), _ctx | hd::tl -> @@ -438,33 +402,24 @@ and lexp_parse_let decls ctx = | ((loc, name), Some pinst, None) ->( let lxp, ltp = lexp_p_infer pinst _ctx in let nacc = ((loc, name), lxp, ltp)::acc in - let ctx2 = env_add_var_info (0, (loc, name), lxp, ltp) _ctx in - process_var_info tl ctx2 nacc) + let ctx2 = env_add_var_info (n_decls - i, (loc, name), lxp, ltp) _ctx in + process_var_info tl ctx2 nacc (i + 1))

| ((loc, name), Some pinst, Some ptype) ->( let linst, ctx1 = lexp_parse pinst _ctx in let ltyp, ctx2 = lexp_parse ptype ctx1 in let nacc = ((loc, name), linst, ltyp)::acc in - let ctx3 = env_add_var_info (0, (loc, name), linst, ltyp) ctx2 in - process_var_info tl ctx3 nacc) + let ctx3 = env_add_var_info (n_decls - i, (loc, name), linst, ltyp) ctx2 in + process_var_info tl ctx3 nacc (i + 1))

(* Skip the variable *) - | ((loc, name), None, _) -> (lexp_warning loc "Unused Variable"; - process_var_info tl _ctx acc) in + | ((loc, name), None, _) -> (lexp_warning loc ("Unused Variable: " ^ name); + process_var_info tl _ctx acc i) in

- let acc, ctx = process_var_info decls nctx [] in + let acc, ctx = process_var_info decls nctx [] 0 in acc, ctx

-and lexp_parse_all (p: ptop list) (ctx: lexp_context): - (ltop list * lexp_context) = - let rec loop (plst: ptop list) ctx (acc: ltop list) = - match plst with - | [] -> ((List.rev acc), ctx) - | _ -> let lxp, new_ctx = lexp_p_toplevel (List.hd plst) ctx in - (loop (List.tl plst) new_ctx (lxp::acc)) in - (loop p ctx []) - -and lexp_p_all (p: pexp list) (ctx: lexp_context): +and lexp_parse_all (p: pexp list) (ctx: lexp_context): (lexp list * lexp_context) = let rec loop (plst: pexp list) ctx (acc: lexp list) = match plst with @@ -472,7 +427,7 @@ and lexp_p_all (p: pexp list) (ctx: lexp_context): | _ -> let lxp, new_ctx = lexp_parse (List.hd plst) ctx in (loop (List.tl plst) new_ctx (lxp::acc)) in (loop p ctx []) - + (* * Type Inference * --------------------- *) @@ -506,6 +461,7 @@ and lexp_p_check (p : pexp) (t : ltype) (env : lexp_context): lexp = (* * Printing * --------------------- *) + (* Print back in CET (Close Enough Typer) easier to read *) (* So print can be called while parsing *) and lexp_print_adv opt exp = @@ -676,18 +632,22 @@ and lexp_print_var_info ctx = done; ;;

-let lexp_print e = - match e with - | Ltexp (x) -> lexp_print_adv (false, 0, true) x - | Ltdecl ((_, x), lxp, ltp) -> - print_string x; - print_string " = "; - lexp_print_adv (false, 0, true) lxp; - print_string " : "; - lexp_print_adv (false, 0, true) ltp -;; - -let lexp_parse_string (str: string) tenv grm limit ctx = +let lexp_print e = lexp_print_adv (false, 0, true) e;; + + +(* add dummy definition helper *) +let add_def name ctx = + let ctx = senv_add_var name dloc ctx in + env_add_var_info (0, (dloc, name), dlxp, dlxp) ctx +;; + + +(* String Parsing + * ------------------------ *) + +(* Lexp helper *) +let _lexp_expr_str (str: string) (tenv: bool array) + (grm: grammar) (limit: string option) (ctx: lexp_context) = let pretoks = prelex_string str in let toks = lex tenv pretoks in let sxps = sexp_parse_all_to_list grm toks limit in @@ -695,8 +655,22 @@ let lexp_parse_string (str: string) tenv grm limit ctx = lexp_parse_all pxps ctx ;;

-(* add dummy definition helper *) -let add_def name ctx = - let ctx = senv_add_var name dloc ctx in - env_add_var_info (0, (dloc, name), dlxp, dlxp) ctx +(* specialized version *) +let lexp_expr_str str lctx = + _lexp_expr_str str default_stt default_grammar (Some ";") lctx +;; + + +let _lexp_decl_str (str: string) tenv grm limit ctx = + let pretoks = prelex_string str in + let toks = lex tenv pretoks in + let sxps = sexp_parse_all_to_list grm toks limit in + let pxps = pexp_decls_all sxps in + lexp_decls pxps ctx ;; + +(* specialized version *) +let lexp_decl_str str lctx = + _lexp_decl_str str default_stt default_grammar (Some ";") lctx +;; +

===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -24,6 +24,7 @@ open Util open Sexp open Lexer open Prelexer +open Grammar

let pexp_error = msg_error "PEXP"

@@ -62,14 +63,6 @@ type pexp = | Pcons of pvar * symbol | Pcase of location * pexp * (ppat * pexp) list

-(* Top level expression annotation *) -type ptop = - | Ptexp of pexp - (* Declarations *) - | Ptann of pvar * pexp (* Type annotation *) - | Ptdecl of pvar * pexp (* Declaration *) - | Ptanndecl of pvar * pexp * pexp (* Annotated declaration *) - | Ptnone

let rec pexp_location e = match e with @@ -92,27 +85,9 @@ let rec pexp_pat_location e = match e with | Ppatcons ((l, _), _) -> l ;;

-let pexp_location_toplevel e = - match e with - | Ptexp (x) -> pexp_location x - | Ptdecl ((x, _), _) -> x - | Ptann ((x, _), _) -> x - | Ptanndecl((x, _), _, _) -> x -;; - -(* We use a list so we can merge 2 contiguous definitions *) -let rec pexp_p_toplevel (s : sexp): ptop = - - match s with - | Node (Symbol (_, "_:_"), _) -> - let (a, b, _)::_ = pexp_p_decls s in Ptann (a, b) - | Node (Symbol (_, "_=_"), _) -> - let (a, b, _)::_ = pexp_p_decls s in Ptdecl (a, b) - | _ -> Ptexp(pexp_parse s) - (* In the following "pexp_p" the prefix for "parse a sexp, returning a pexp" * and "pexp_u" is the prefix for "unparse a pexp, returning a sexp". *) -and pexp_parse (s : sexp) : pexp = +let rec pexp_parse (s : sexp) : pexp = match s with (* This is an internal error because Epsilon does not have any location * information so it needs to be caught elsewhere. *) @@ -378,23 +353,45 @@ and pexp_u_decls ds = let pexp_print e = sexp_print (pexp_unparse e)

-let pexp_print_toplevel e = - match e with - | Ptexp (x) -> pexp_print x - | Ptdecl ((_, n), e) -> print_string (n ^ " = "); pexp_print e; - | Ptann ((_, n), e) -> print_string (n ^ " : "); pexp_print e; - | Ptanndecl((_, n), e, t) -> print_string (n ^ " = "); pexp_print e; +let pexp_decls_all (nodes: sexp list): ((pvar * pexp * bool) list) = + let rec loop nodes acc = + match nodes with + | [] -> acc + | hd::tl -> + let r = pexp_p_decls hd in + let nacc = List.append acc r in + loop tl nacc in + loop nodes [] ;; - - + (* Parse All Pexp as a list *) let pexp_parse_all (nodes: sexp list) = - List.map pexp_p_toplevel nodes + List.map pexp_parse nodes ;;

-let pexp_parse_string (str: string) tenv grm limit = +(* Pexp String + * ------------------- *) +let _pexp_expr_str (str: string) tenv grm limit = let pretoks = prelex_string str in let toks = lex tenv pretoks in let sxps = sexp_parse_all_to_list grm toks limit in pexp_parse_all sxps ;; + +let pexp_expr_str str = + _pexp_expr_str str default_stt default_grammar (Some ";") +;; + + +let _pexp_decl_str (str: string) tenv grm limit = + let pretoks = prelex_string str in + let toks = lex tenv pretoks in + let sxps = sexp_parse_all_to_list grm toks limit in + pexp_decls_all sxps +;; + +let pexp_decl_str str = + _pexp_decl_str str default_stt default_grammar (Some ";") +;; + +

===================================== tests/REPL.ml ===================================== --- a/tests/REPL.ml +++ b/tests/REPL.ml @@ -45,7 +45,81 @@ let rec read_input i = loop "" 1 ;;

+(* Interactive mode is not usual typer + * It makes things easier to test out code *) +type ptop = + | Pdecl of pvar * pexp * bool + | Pexpr of pexp + +let ipexp_parse p = + match p with + (* Declaration *) + | Node (Symbol (_, "_=_"), [Symbol s; t]) -> + let (a, b, c)::_ = pexp_p_decls nod in + Pdecl(a, b, c) + | Node (Symbol (_, "_:_"), [Symbol s; t]) -> + let (a, b, c)::_ = pexp_p_decls nod in + Pdecl(a, b, c) + (* Expression *) + | _ -> let a = pexp_parse nod in Pexpr(a) +;; + +let ipexp_parse_all ps = List.map ipexp_parse ps;; + +type ltop = + | Ldecl of vdef * lexp * ltype + | Lexpr of lexp + +let ilexp_parse l lctx = + match l with + | Pdecl(_, _, _) -> let (a, b, c), d = lexp_decls [l] ctx in + Ldecl(a, b, c), d + | Pexpr(x) -> let v, c = lexp_parse x lctx in + Lexpr(v), c + +let ilexp_parse_all ls lctx = + let rec loop lst acc ctx = + match lst with + | [] -> List.rev acc, ctx + | hd::tl -> + let x, c = ilexp_parse hd ctx in + let nacc = acc::x in + loop tl nacc c in + loop ls [] lctx + +type ival = + | Ivoid + | Ival of lexp

+let ieval xpr rctx = + match xpr with + | Ldecl(_, _, _) -> let r = eval_decls xpr rctx in + Ivoid, rctx + | Lexpr(x) -> let v, _ = eval x rctx in + Ival(v), rctx + +let ieval_all xprs rctx = + let rec loop lst acc ctx = + match lst with + | [] -> List.rev acc, ctx + | hd::tl -> + let x, c = ieval hd ctx in + let nacc = acc::x in + loop tl nacc c in + loop xprs [] rctx + +let ieval_string str lctx rctx = + let pres = prelex_string str in + let sxps = lex default_stt pres in + let nods = sexp_parse_all_to_list default_grammar sxps (Some ";") in + + (* Different from usual typer *) + let pxps = ipexp_parse_all nods in + let lxps, ctx = ilexp_parse_all pxps lctx in + let v, rctx = ieval_all lxps rctx in + v, lctx, rctx +;; + (* Specials commands %[command-name] *) let rec repl () = let tenv = default_stt in @@ -71,9 +145,15 @@ let rec repl () = (print_call_trace (); loop (i + 1) clxp rctx) (* Else Process Typer code *) else - let (ret, rctx), clxp = (eval_string ipt clxp rctx) in - let print_e j v = print_eval_result i v in + let (ret, clxp, rctx) = (ieval_string ipt clxp rctx) in + + let print_e j v = + match b with + | Ivoid -> () + | Ival(x) -> print_eval_result i x in + List.iteri print_e ret; + loop (i + 1) clxp rctx in

loop 1 lxp_ctx rctx

===================================== tests/debug.ml ===================================== --- a/tests/debug.ml +++ b/tests/debug.ml @@ -42,6 +42,8 @@ open Lexp open Lparse open Debruijn open Fmt +open Grammar +open Eval

(* Print aPretokens *) let rec debug_pretokens_print pretoken = @@ -116,30 +118,37 @@ let debug_sexp_print_all tokens = (* Print a Pexp with debug info *) let debug_pexp_print ptop = print_string " "; - let l = pexp_location_toplevel ptop in + let l = pexp_location ptop in let print_info msg loc pex = print_string msg; print_string "["; print_loc loc; print_string "]\t"; - pexp_print_toplevel pex in + pexp_print pex in match ptop with - | Ptdecl((l, n), pexp) -> print_info "PDecl " l ptop - | Ptexp (pexp) -> ( - match pexp with - | Pimm _ -> print_info "Pimm " l ptop - | Pvar (_,_) -> print_info "Pvar " l ptop - | Phastype (_,_,_) -> print_info "Phastype " l ptop - | Pmetavar (_, _) -> print_info "Pmetavar " l ptop - | Plet (_, _, _) -> print_info "Plet " l ptop - | Parrow (_, _, _, _, _) -> print_info "Parrow " l ptop - | Plambda (_,_, _, _) -> print_info "Plambda " l ptop - | Pcall (_, _) -> print_info "Pcall " l ptop - | Pinductive (_, _, _) -> print_info "Pinductive " l ptop - | Pcons (_,_) -> print_info "Pcons " l ptop - | Pcase (_, _, _) -> print_info "Pcase " l ptop - | _ -> print_info "Not Impl " l ptop) + | Pimm _ -> print_info "Pimm " l ptop + | Pvar (_,_) -> print_info "Pvar " l ptop + | Phastype (_,_,_) -> print_info "Phastype " l ptop + | Pmetavar (_, _) -> print_info "Pmetavar " l ptop + | Plet (_, _, _) -> print_info "Plet " l ptop + | Parrow (_, _, _, _, _) -> print_info "Parrow " l ptop + | Plambda (_,_, _, _) -> print_info "Plambda " l ptop + | Pcall (_, _) -> print_info "Pcall " l ptop + | Pinductive (_, _, _) -> print_info "Pinductive " l ptop + | Pcons (_,_) -> print_info "Pcons " l ptop + | Pcase (_, _, _) -> print_info "Pcase " l ptop + | _ -> print_info "Not Impl " l ptop ;;

+let debug_pexp_decls decls = + List.iter (fun e -> + let ((_, name), pxp, tp) = e in + print_string name; + if tp then print_string " : " else print_string " = "; + pexp_print pxp; print_string "\n" + ) + decls + + (* Print a list of pexp *) let debug_pexp_print_all pexps = List.iter @@ -158,11 +167,8 @@ let debug_lexp_print tlxp = print_loc loc; print_string "]\t"; lexp_print lex in - let tloc = lexp_location_toplevel tlxp in + let tloc = lexp_location tlxp in match tlxp with - | Ltdecl ((_, x), lxp, ltp) -> print_info "Decl " tloc tlxp - | Ltexp(lxp) -> - match lxp with | Var((loc, _), _) -> print_info "Var " tloc tlxp | Imm(s) -> print_info "Imm " tloc tlxp | Let(loc, _, _) -> print_info "Let " tloc tlxp @@ -185,5 +191,34 @@ let debug_lexp_print_all lexps = lexps ;;

+let debug_lexp_decls decls = + List.iter (fun e -> + let ((_, name), lxp, ltp) = e in + print_string name; print_string " : "; + lexp_print ltp; + print_string " = "; + lexp_print lxp; + print_string ";\n" + ) + decls + + + + + + + + + + + + + + + + + + +

===================================== tests/eval_test.ml ===================================== --- /dev/null +++ b/tests/eval_test.ml @@ -0,0 +1,152 @@ +open Lparse (* add_def *) +open Debruijn (* make_lexp_context *) +open Eval (* make_rte_ctx *) +open Utest_lib + + +(* default environment *) +let lctx = make_lexp_context +let lctx = add_def "_+_" lctx +let lctx = add_def "_*_" lctx +let rctx = make_runtime_ctx + + +(* Let + * ------------------------ *) + +let _ = (add_test "EVAL" "Let" (fun () -> + (* Noise. Makes sure the correct variables are selected *) + let dcode = " + c = 3; a = 1; b = 2; d = 4;" in + let rctx, lctx = eval_decl_str dcode lctx rctx in + + let ecode = " + let a = 10; x = 50; y = 60; b = 20; in a + b;" in + + let ret = eval_expr_str ecode lctx rctx in + (* Expect a single result *) + match ret with + | [r] -> expect_equal_int 30 (get_int r) + | _ -> failure ()) +) +;; + + +(* Lambda + * ------------------------ *) +let _ = (add_test "EVAL" "Lambda" (fun () -> + (* Declare lambda *) + let rctx, lctx = eval_decl_str "sqr = lambda x -> x * x;" lctx rctx in + + (* Eval defined lambda *) + 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) + | _ -> failure ()) +) +;; + +let _ = (add_test "EVAL" "Nested Lambda" (fun () -> + let code = " + sqr = lambda x -> x * x; + cube = lambda x -> x * (sqr x); " in + + (* Declare lambda *) + let rctx, lctx = eval_decl_str code lctx rctx in + + (* Eval defined lambda *) + 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) + | _ -> failure ()) +) +;; + +(* Cases + Inductive types + * ------------------------ *) (* + +let _ = (add_test "EVAL" "Case" (fun () -> + (* Inductive type declaration *) + let code = " + idt = inductive_ (idtd) (ctr0) (ctr1 idt) (ctr2 idt) (ctr3 idt);\n + + ctr0 = inductive-cons idt ctr0;\n + ctr1 = inductive-cons idt ctr1;\n + ctr2 = inductive-cons idt ctr2;\n + ctr3 = inductive-cons idt ctr2;\n + + a = (ctr1 (ctr2 ctr0));\n + b = (ctr2 (ctr2 ctr0));\n + c = (ctr3 (ctr2 ctr0));\n + + test_fun = lambda x -> case x\n + | ctr1 y => 1\n + | ctr2 y => 2\n + | _ => 3;\n" in + + let rctx, lctx = eval_decl_str code lctx rctx in + + let rcode = "(test_fun a); (test_fun b); (test_fun c)"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) 1 in + let t2 = expect_equal_int (get_int b) 2 in + let t3 = expect_equal_int (get_int c) 3 in + if t1 = 0 && t2 = 0 && t3 = 0 then + success () + else + failure () + | _ -> failure ()) +) +;; *) + +let _ = (add_test "EVAL" "Recursive Call" (fun () -> + (* Inductive type declaration *) + let code = " + Nat = inductive_ (dNat) (zero) (succ Nat); + + zero = inductive-cons Nat zero; + succ = inductive-cons Nat succ; + + one = (succ zero); + two = (succ one); + three = (succ three); + + tonum = lambda x -> case x + | (succ y) => (1 + (tonum y)) + | _ => 0;" in + + let rctx, lctx = eval_decl_str code lctx rctx in + + let rcode = "(tonum one);"in + + (* Eval defined lambda *) + let ret = eval_expr_str rcode lctx rctx in + (* Expect a 3 results *) + match ret with + | [a] -> expect_equal_int (get_int a) 1 + + (*| [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 + if t1 = 0 && t2 = 0 && t3 = 0 then + success () + else + failure () *) + | _ -> failure ()) +) +;; + + + +(* run all tests *) +run_all () +;; +

===================================== tests/full_debug.ml ===================================== --- a/tests/full_debug.ml +++ b/tests/full_debug.ml @@ -47,14 +47,10 @@ open Lparse open Eval open Lexp

-(* pexp and lexp can be done together, one by one *) -let pexp_lexp_one node ctx = - let pxp = pexp_parse node in - lexp_parse pxp ctx -;; -

+let dummy_decl = Imm(String(dloc, "Dummy"));;

+(* let pexp_lexp_all nodes ctx =

let rec loop nodes ctx acc = @@ -66,7 +62,7 @@ let pexp_lexp_all nodes ctx = (loop nodes ctx []) ;;

-let dummy_decl = Imm(String(dloc, "Dummy"));; +

let add_rte_def name ctx = (add_rte_variable (Some name) dummy_decl ctx);; @@ -83,7 +79,9 @@ let eval_until_nth xpr n rctx = print_eval_result nb c; loop tl (nb + 1) rctx in loop xpr 0 rctx -;; +;; *) + +let discard v = ();;

let main () =

@@ -100,7 +98,6 @@ let main () = else begin let filename = Sys.argv.(1) in - (* Read additional Args if any *)

print_string (make_title " ERRORS "); @@ -113,8 +110,9 @@ let main () = (* get node sexp *) let nodes = sexp_parse_all_to_list default_grammar toks (Some ";") in

- (* get pexp *) - let pexps = pexp_parse_all nodes in + (* Parse All Declaration *) + let pexps = pexp_decls_all nodes in + (* let pexps = pexp_parse_all nodes in *)

(* get lexp *) let ctx = make_lexp_context in @@ -122,31 +120,53 @@ let main () = let ctx = add_def "_+_" ctx in let ctx = add_def "_*_" ctx in

- let lexps, new_ctx = lexp_parse_all pexps ctx in - + (* let lexps, new_ctx = lexp_parse_all pexps ctx in *) + let lexps, nctx = lexp_decls pexps ctx in + print_string "\n\n"; (* Printing *)(* print_title "PreTokens"; debug_pretokens_print_all pretoks; print_title "Base Sexp"; debug_sexp_print_all toks; *) - print_string (make_title " Node Sexp "); debug_sexp_print_all nodes; + print_string (make_title " Node Sexp "); debug_sexp_print_all nodes; print_string "\n"; - print_string (make_title " Pexp "); debug_pexp_print_all pexps; + print_string (make_title " Pexp "); debug_pexp_decls pexps; + (*debug_pexp_print_all pexps;*) print_string "\n"; - print_string (make_title " Lexp "); debug_lexp_print_all lexps; + print_string (make_title " Lexp "); debug_lexp_decls lexps; + (* debug_lexp_print_all lexps; *) + print_string "\n"; + + print_string "\n"; + lexp_context_print nctx; print_string "\n";

(* Eval Each Expression *) print_string (make_title " Eval Print ");

- (* Eval One *) + + (* Eval declaration *) let rctx = make_runtime_ctx in - let rctx = eval_until_nth lexps 500 rctx in - print_string "\n\n"; - print_rte_ctx rctx; + let rctx = eval_decls lexps rctx in + + let _ = + try + (* Check if main is present *) + let main = (senv_lookup "main" nctx) in + (* Push main args here if any *) + + (* get main body *) + let body = (get_rte_variable main rctx) in + (* eval main *) + let r = (eval body rctx) in + print_eval_result 0 r + + with + Not_found -> () in + + (* Print info *) + print_string "\n\n"; + print_rte_ctx rctx;

- print_string "\n"; - lexp_context_print new_ctx; - print_string "\n";

print_call_trace (); end @@ -154,4 +174,3 @@ let main () =

main () ;; -

===================================== tests/let_test.ml deleted ===================================== --- a/tests/let_test.ml +++ /dev/null @@ -1,30 +0,0 @@ - -open Eval - - -(* How to make macro in ocaml? *) - -(* -let EXPECT_EQUAL a b = - if a = b then(print_string "[ OK]\n"; SUCCESS) - else( print_string "[ FAIL]\n"; FAILURE) -;; - -let EXPECT_THROW a error = - try ((a); print_string "[ FAIL]\n"; FAILURE) - with (print_string "[ OK]\n"; SUCCESS) -;; *) - - -let main () = - - let ret = easy_eval_string "let a = 3; b = 5; in a + b;" in - match ret with - | [xpr] -> let v = get_int xpr in - if v = 8 then (exit 0) else (exit (-1)) - | _ -> exit (-1) - -;; - -main () -;; \ No newline at end of file

===================================== tests/lexp_test.ml ===================================== --- /dev/null +++ b/tests/lexp_test.ml @@ -0,0 +1,47 @@ +open Lparse +open Debruijn (* make_lexp_context *) +open Lexp +open Utest_lib + +(* default environment *) +let lctx = make_lexp_context +let lctx = add_def "_+_" lctx +let lctx = add_def "_*_" lctx + +(* Check if annotation are parsed and kept *) +(* Let and top level declarations are using the same code *) +(* We only have to check if let's type parsing is correct *) +let _ = (add_test "LEXP" "Type Parsing" (fun () -> + + (* This is garbage. I just want Nat to be defined *) + let dcode = " + Nat = inductive_ (dNat) (zero) (succ Nat);\n" in + + let _, lctx = lexp_decl_str dcode lctx in + + let ecode = " + let a : Nat; a = 1; b : Nat; b = 3; + in + a + b;" in + + let ret, _ = lexp_expr_str ecode lctx in + match ret with + | [expr] ->( + match expr with + | Let(_, arg, _) -> match arg with + | [] -> failure () + | (_, xp, tp)::_ ->( + (* tp must match Nat *) + match tp with + | Var((_, name), _) -> expect_equal_str name "Nat" + | _ -> failure () + ) + | _ -> failure ()) + | [] -> failure ()) +) +;; + + + +run_all () +;; \ No newline at end of file

===================================== tests/pexp_test.ml ===================================== --- /dev/null +++ b/tests/pexp_test.ml @@ -0,0 +1,29 @@ +open Pexp +open Utest_lib + + +let _ = (add_test "PEXP" "Type Parsing" (fun () -> + + let dcode = " + let a : Nat; a = 1; b : Nat; b = 3; in a + b;" in + + let ret = pexp_expr_str dcode in + match ret with + | [expr] ->( + match expr with + | Plet(_, arg, _) -> match arg with + | [] -> failure () + | (_, tp, bl)::_ ->( + if bl = true then + success () + else + failure ()) + | _ -> failure ()) + | [] -> failure ()) +) +;; + + + +run_all () +;; \ No newline at end of file

===================================== tests/utest_lib.ml ===================================== --- /dev/null +++ b/tests/utest_lib.ml @@ -0,0 +1,123 @@ +(* + * Typer Compiler + * + * --------------------------------------------------------------------------- + * + * Copyright (C) 2011-2016 Free Software Foundation, Inc. + * + * Author: Pierre Delaunay pierre.delaunay@hec.ca + * Keywords: languages, lisp, dependent types. + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any + * later version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for + * more details. + * + * You should have received a copy of the GNU General Public License along + * with this program. If not, see http://www.gnu.org/licenses/. + * + * --------------------------------------------------------------------------- + * + * Description: + * utest library utility. Tests register themselves + * + * --------------------------------------------------------------------------- *) + + + +module StringMap = + Map.Make (struct type t = string let compare = String.compare end) +;; + + +type test_fun = (unit -> int) +type tests = (test_fun) StringMap.t +type sections = (tests) StringMap.t + +let success () = 0;; +let failure () = (-1);; + +(* + * SECTION NAME - TEST NAME - FUNCTION (() -> int) + * "Let" - "Base Case" - (fun () -> success ) + * "Let" - "Recursive" + * "Lambda" - "Base Case" + * "Lambda" - "Nested" + *) +let _global_sections = ref StringMap.empty + + +(* USAGE *) +(* + * (add_test "LET" "Base Case" (fun () -> + * let r = eval_string "let a = 2; b = 3; in a + b;" in + * let v = (get_int r) in + * if v = 5 then success () else failure ())) + * + * sname: Section Name + * tname: Test Name + * dcode: Typer's Declarations + * ecode: expression to eval + * tfun : test function (unit -> int) + *) +let add_test sname tname tfun = + + (* Does Section Exists ? *) + let tmap = + try + StringMap.find sname (!_global_sections) + with + Not_found -> StringMap.empty in + + (* add test *) + let ntmap = StringMap.add tname tfun tmap in + _global_sections := StringMap.add sname ntmap (!_global_sections); +;; + +(* Run all *) +let run_all () = + (* iter over all sections *) + StringMap.iter (fun sk sv -> + print_string ("[RUN ] " ^ sk ^ " \n"); + (* iter over all tests in the current sections *) + StringMap.iter (fun tk tv -> + (* RUN TEST*) + let r = tv () in + if r = 0 then + (print_string ("[ OK] " ^ sk ^ " - " ^ tk ^ "\n")) + else + (print_string ("[ FAIL] " ^ sk ^ " - " ^ tk ^ "\n")) + ) + sv; + flush stdout; + ) + (!_global_sections) + + +let expect_equal_int value expect = + if value = expect then + success () + else( + print_string ("[ ] EXPECTED: " ^ (string_of_int expect)^ "\n"); + print_string ("[ ] GOT: " ^ (string_of_int value) ^ "\n"); + failure ()) +;; + + +let expect_equal_str value expect = + if value = expect then + success () + else( + print_string ("[ ] EXPECTED: " ^ expect ^ "\n"); + print_string ("[ ] GOT: " ^ value ^ "\n"); + failure ()) +;; + +

===================================== tests/utest_main.ml ===================================== --- a/tests/utest_main.ml +++ b/tests/utest_main.ml @@ -59,6 +59,7 @@ let main () = let root_folder = (if arg_n > 2 then Sys.argv.(2) else "./") in (* /_build/tests/ *)

for i = 0 to files_n - 1 do + flush stdout; (* Check if file is a test => if it is run it *) (if (Filename.check_suffix files.(i) "_test.byte") || (Filename.check_suffix files.(i) "_test.native") then @@ -66,17 +67,8 @@ let main () =

tests_n := !tests_n + 1;

- print_endline ("[RUN ] TEST: " ^ (cut_name files.(i))); - exit_code := Sys.command (folder ^ files.(i) ^ " " ^ root_folder);

- if !exit_code <> 0 then begin - print_string "[ FAIL]\n" ; - print_endline " =========== TEST FAILURE ==========="; - failed_test := !failed_test + 1; - end - else - print_string "[ OK]\n" ; end) done;

View it on GitLab: https://gitlab.com/monnier/typer/compare/772d85026102d81b874b60852ef71b5f299...