Setepenre pushed to branch master at Stefan / Typer

Commits: 2e53f40d by Pierre Delaunay at 2016-03-22T18:41:03-04:00 bound is inside lexp_ctx

- - - - - db4f6c1e by Pierre Delaunay at 2016-03-22T19:51:41-04:00 ityper can interpret files before REPL

- - - - - aa416638 by Pierre Delaunay at 2016-03-23T11:41:25-04:00 add arg parsing for ityper and full_debug

Changes to be committed: * GNUmakefile : new option "make tests", build tests and run them * tests/REPL.ml : files can be interpreted to populate environments * tests/full_debug.ml : we can choose how much info we want to print

- - - - -

10 changed files:

- GNUmakefile - src/debruijn.ml - src/eval.ml - src/lparse.ml - tests/REPL.ml - tests/debug.ml - tests/full_debug.ml - tests/lexp_test.ml - tests/pexp_test.ml - tests/utest_lib.ml

Changes:

===================================== GNUmakefile ===================================== --- a/GNUmakefile +++ b/GNUmakefile @@ -6,17 +6,14 @@ TEST_FILES := $(wildcard ./tests/*_test.ml)

CFLAG = -cflag -rectypes -build-dir _build

-# This is for windows: windows version is old - - all: ityper typer debug tests

-typer: +typer: ocamlbuild src/main.native $(CFLAG) @mv _build/src/main.native _build/typer

# debug file eval -debug: +debug: ocamlbuild tests/full_debug.native -I src $(CFLAG) @mv _build/tests/full_debug.native _build/full_debug

@@ -25,7 +22,7 @@ ityper: ocamlbuild tests/REPL.native -I src $(CFLAG) @mv _build/tests/REPL.native _build/ityper

-tests-build: +tests-build: # ============================ # Build tests # ============================ @@ -39,7 +36,9 @@ tests-run: # ============================ @./_build/tests/utests

-# Make language doc +tests: tests-build tests-run + +# Make language doc doc-tex: texi2pdf ./doc/manual.texi --pdf --build=clean

@@ -49,6 +48,6 @@ doc-ocaml:

# everything is expected to be compiled in the "./_build/" folder clean: - -rm -rf _build + -rm -rf _build

.PHONY: ityper typer debug tests

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -52,70 +52,71 @@ module StringMap = Map.Make (struct type t = string let compare = String.compare end) ;;

- (* Map matching variable name and its distance in the current scope *) type scope = (int) StringMap.t (* Map<String, int>*)

type senv_length = int (* it is not the map true length *) type senv_type = senv_length * scope

- (* name -> index * index -> info *) -type lexp_context = senv_type * env_type + (* name -> index * index -> info * (outer_size, r_offset) *) +type lexp_context = senv_type * env_type * (int * int)

-(* internal definitions: DO NOT USE +(* internal definitions * ---------------------------------- *)

let _make_scope = StringMap.empty;; let _make_senv_type = (0, _make_scope);; let _make_myers = nil +let _get_env(ctx: lexp_context): env_type = let (_, ev, _) = ctx in ev ;;

-let _get_senv (ctx: lexp_context) = - let (ct, _) = ctx in ct -;; +(* Public methods: DO USE + * ---------------------------------- *)

-let _get_scope(ctx: lexp_context): scope = - let ((_, ev), _) = ctx in ev -;; +let make_lexp_context = (_make_senv_type, _make_myers, (0, 0));;

-let _get_env(ctx: lexp_context): env_type = - let (_, ev) = ctx in ev -;; +let get_roffset ctx = let (_, _, (_, rof)) = ctx in rof;;

-let _add_var_env variable ctx = - let (a, env) = ctx in cons variable env +(* Enter a local scope such as let *) +let local_scope ctx pos = + let ((l, map), b, c) = ctx in + (* Check size *) + let n = (length b) in + ((l, map), b, (l, pos)) ;;

-(* Public methods: DO USE - * ---------------------------------- *) - -let make_lexp_context = (_make_senv_type, _make_myers);; +(* Enter a temporary scope such as Calls *) +let temp_scope ctx bound = let (a, b, c) = ctx in (a, b, bound)

(* return its current DeBruijn index *) let rec senv_lookup (name: string) (ctx: lexp_context): int = - let ((n, map), _) = ctx in - n - (StringMap.find name map) - 1 + let ((n, map), _, (csize, rof)) = ctx in + let raw_idx = n - (StringMap.find name map) - 1 in + if raw_idx > (n - csize) then + raw_idx - rof (* Shift if the variable is not bound *) + else + raw_idx ;;

(* We first add variable into our map. Later on, we will add them into * the environment. The reason for this is that the type info is * known after lexp parsing which need the index fist *) let senv_add_var name loc ctx = - let ((n, map), e) = ctx in + let ((n, map), e, f) = ctx in try - let idx = senv_lookup name ctx in + let _ = senv_lookup name ctx in debruijn_warning loc ("Variable Shadowing " ^ name); let nmap = StringMap.add name n map in - ((n + 1, nmap), e) + ((n + 1, nmap), e, f) with Not_found -> let nmap = StringMap.add name n map in - ((n + 1, nmap), e) + ((n + 1, nmap), e, f) ;;

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

let env_lookup_type_by_index index ctx = @@ -135,5 +136,7 @@ let env_lookup_type ctx (v : vref) = internal_error "DeBruijn index refers to wrong name!" with Not_found -> internal_error "DeBruijn index out of bounds!"

-let env_lookup_by_index index ctx = Myers.nth index (_get_env ctx);; +let env_lookup_by_index index (ctx: lexp_context): env_elem = + Myers.nth index (_get_env ctx) +;;

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -40,20 +40,19 @@ open Debruijn open Grammar

-let _eval_error loc msg = - msg_error "eval" loc msg; +let eval_error loc msg = + msg_error "EVAL" loc msg; raise (internal_error msg) ;;

let dloc = dummy_location -let _eval_warning = msg_warning "eval" +let eval_warning = msg_warning "EVAL"

type call_trace_type = (int * lexp) list let global_trace = ref []

let add_call cll i = global_trace := (i, cll)::!global_trace

-let reinit_call_trace () = global_trace := []

let print_myers_list l print_fun = let n = (length l) - 1 in @@ -71,12 +70,6 @@ let print_myers_list l print_fun = print_string (make_sep '='); ;;

-let get_function_name fname = - match fname with - | Var(v) -> let ((loc, name), idx) = v in name - | _ -> "Name Lookup failure" -;; - let get_int lxp = match lxp with | Imm(Integer(_, l)) -> l @@ -88,9 +81,16 @@ 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: int) (l: runtime_env): lexp = +let get_rte_variable (*name: string option*) (idx: int) (l: runtime_env): lexp = (* FIXME: Check that the variable's name is right! *) - let (_, x) = (nth idx l) in x + let (tn, x) = (nth idx l) in x + + (* + match (tn, name) with + | (Some n1, Some n2) -> + if n1 = n2 then x else (eval_error dloc + ("Variable lookup failure. Expected: " ^ n2 ^ " got " ^ n1); x) + | _ -> x (* can't check variable's name *) *) ;;

let get_rte_size (l: runtime_env): int = length l;; @@ -207,8 +207,8 @@ let rec _eval lxp ctx i: (value_type) = 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 = + (* Collapse nested lambdas. Returns body *) + let rec collapse bd idx nctx = match bd with | Lambda(_, vr, _, body) -> let (loc, name) = vr in @@ -216,10 +216,10 @@ let rec _eval lxp ctx i: (value_type) = let value = (get_rte_variable idx ctx) in (* Build lambda context *) let nctx = add_rte_variable (Some name) value nctx in - (build_body body (idx + 1) nctx) + (collapse body (idx + 1) nctx) | _ -> bd, nctx in

- let body, nctx = build_body body 1 nctx in + let body, nctx = collapse body 1 nctx in _eval body nctx (i + 1) end

(* Inductive is a type declaration. We have nothing to eval *) @@ -233,28 +233,30 @@ let rec _eval lxp ctx i: (value_type) =

(* Eval target *) let v = _eval target ctx (i + 1) in - let nctx = ctx in

(* V must be a constructor Call *) let ctor_name, args = match v with | Call(lname, args) -> (match lname with | Var((_, ctor_name), _) -> ctor_name, args - | _ -> _eval_error loc "Target is not a Constructor" ) + | _ -> eval_error loc "Target is not a Constructor" )

| Cons((_, idx), (_, cname)) -> begin (* retrieve type definition *) - print_int idx; + let info = get_rte_variable idx ctx in - let Inductive(_, _, _, ctor_def) = info in + let ctor_def = match info with + | Inductive(_, _, _, c) -> c + | _ -> eval_error loc "Not an Inductive Type" in + try let args = SMap.find cname ctor_def in cname, args with Not_found -> - _eval_error loc "Constructor does not exist" end + eval_error loc "Constructor does not exist" end

| _ -> lexp_print target; print_string "\n"; lexp_print v; print_string "\n"; - _eval_error loc "Can't match expression" in + eval_error loc "Can't match expression" in

(* Check if a default is present *) let run_default df = @@ -336,7 +338,8 @@ and print_call_trace () = print_string (make_title " CALL TRACE ");

let n = List.length !global_trace in - print_string " size = "; print_int n; print_string "\n"; + print_string " size = "; print_int n; + print_string (" max_printed = 50" ^ "\n"); print_string (make_sep '-');

let racc = List.rev !global_trace in @@ -358,12 +361,13 @@ let eval lxp ctx = ;;

(* Eval a list of lexp *) -let eval_all lxps rctx = List.map (fun g -> eval g rctx) lxps;; +let eval_all lxps rctx = + global_trace := []; + List.map (fun g -> eval g rctx) lxps;;

(* Eval String * ---------------------- *) let eval_expr_str str lctx rctx = - global_trace := []; let lxps = lexp_expr_str str lctx in (eval_all lxps rctx) ;;

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -105,18 +105,9 @@ let default_lctx = * possible for env to hold more variables than senv since senv is a map * which does not allow multiple definition while env does. * - * a = 1; - * let a = 3; b = 5 in a + b; - * *)

-let rec lexp_parse p ctx: lexp = - _lexp_parse p ctx (0, 0) - -(* bound is used to determine if the variable require shifting - * bound = (inner_size, r_offset) - *) -and _lexp_parse (p: pexp) (ctx: lexp_context) bound: lexp = +let rec lexp_parse (p: pexp) (ctx: lexp_context): lexp = (* So I don't have to extract it *) let tloc = pexp_location p in match p with @@ -127,12 +118,8 @@ and _lexp_parse (p: pexp) (ctx: lexp_context) bound: lexp = | Pvar (loc, name) -> begin try (* Send Variable loc *) - let (isize, rof) = bound in - let idx = senv_lookup name ctx in( - if idx > isize then - (make_var name (idx - rof) loc) - else - (make_var name idx loc)) + let idx = senv_lookup name ctx in + (make_var name idx loc)

with Not_found -> (lexp_error loc ("The Variable: " ^ name ^ " was not declared"); @@ -142,22 +129,19 @@ and _lexp_parse (p: pexp) (ctx: lexp_context) bound: lexp = (* Let, Variable declaration + local scope *) | Plet(loc, decls, body) -> let decl, nctx = lexp_decls decls ctx in - (* Body cannot modify context *) - let (_, rof) = bound in - let bound = ((List.length decl), rof) in - let bdy = _lexp_parse body nctx bound in + let bdy = lexp_parse body (local_scope nctx (get_roffset nctx)) in Let(tloc, decl, bdy)

(* ->/=> *) | Parrow (kind, Some var, tp, loc, expr) -> let nvar = var in (* /!\ HERE *) - let ltyp = _lexp_parse tp ctx bound in - let lxp = _lexp_parse expr ctx bound in + let ltyp = lexp_parse tp ctx in + let lxp = lexp_parse expr ctx in Arrow(kind, Some nvar, ltyp, tloc, lxp)

| Parrow (kind, None, tp, loc, expr) -> - let ltyp = _lexp_parse tp ctx bound in - let lxp = _lexp_parse expr ctx bound in + let ltyp = lexp_parse tp ctx in + let lxp = lexp_parse expr ctx in Arrow(kind, None, ltyp, tloc, lxp)

(* *) @@ -169,10 +153,10 @@ and _lexp_parse (p: pexp) (ctx: lexp_context) bound: lexp = let nctx = senv_add_var vname loc ctx in let nctx = env_add_var_info (0, (loc, vname), dlxp, ltp) nctx in

- let ltyp = _lexp_parse ptype nctx bound in - let (_, rof) = bound in - let bound = (1, rof) in - let lbody = _lexp_parse body nctx bound in + let ltyp = lexp_parse ptype nctx in + + let nctx = (local_scope nctx (get_roffset nctx)) in + let lbody = lexp_parse body nctx in Lambda(kind, var, ltyp, lbody)

| Plambda (kind, var, None, body) -> @@ -181,29 +165,27 @@ and _lexp_parse (p: pexp) (ctx: lexp_context) bound: lexp = let nctx = senv_add_var vname loc ctx in let nctx = env_add_var_info (0, (loc, vname), dlxp, dltype) nctx in

- let (_, rof) = bound in - let bound = (1, rof) in - let lbody = _lexp_parse body nctx bound in + let nctx = (local_scope nctx (get_roffset nctx)) in + let lbody = lexp_parse body nctx in Lambda(kind, var, UnknownType(tloc), lbody)

| Pcall (fname, _args) -> - lexp_call fname _args ctx bound + lexp_call fname _args ctx

(* Pinductive *) | Pinductive (label, [], ctors) -> - let map_ctor, nctx = lexp_parse_constructors ctors ctx bound in - Inductive(tloc, label, [], map_ctor) + let map_ctor, nctx = lexp_parse_constructors ctors ctx in + Inductive(tloc, label, [], map_ctor)

(* Pcons *) | Pcons(vr, sym) -> ( let (loc, type_name) = vr in let (_, ctor_name) = sym in - let (isize, rof) = bound in (* An inductive type named type_name must be in the environment *) try let idx = senv_lookup type_name ctx in (* Check if the constructor exists *) (* TODO *) - Cons((vr, idx - rof), sym) + Cons((vr, idx), sym) with Not_found -> lexp_error loc ("The inductive type: " ^ type_name ^ " was not declared"); @@ -213,7 +195,7 @@ and _lexp_parse (p: pexp) (ctx: lexp_context) bound: lexp = | Pcase (loc, target, patterns) ->

(* I need type info HERE *) - let lxp = _lexp_parse target ctx bound in + let lxp = lexp_parse target ctx in let ltp = UnknownType(loc) in

(* Read patterns one by one *) @@ -225,7 +207,7 @@ and _lexp_parse (p: pexp) (ctx: lexp_context) bound: lexp = (* Create pattern context *) let (name, iloc, arg), nctx = lexp_read_pattern pat exp lxp ctx in (* parse using pattern context *) - let exp = _lexp_parse exp nctx bound in + let exp = lexp_parse exp nctx in

if name = "_" then loop tl merged (Some exp) @@ -241,7 +223,7 @@ and _lexp_parse (p: pexp) (ctx: lexp_context) bound: lexp = -> UnknownType(tloc)

(* Identify Call Type and return processed call *) -and lexp_call (fname: pexp) (_args: sexp list) ctx bound = +and lexp_call (fname: pexp) (_args: sexp list) ctx = (* Process Arguments *) let pargs = List.map pexp_parse _args in

@@ -254,30 +236,29 @@ and lexp_call (fname: pexp) (_args: sexp list) ctx bound = | Pcons (_, (loc, nm)) -> nm, loc | _ -> raise Not_found in

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

try (* Check if the function was defined *) let idx = senv_lookup name ctx in let vf = (make_var name idx loc) in - - Call(vf, new_args) + Call(vf, new_args)

with Not_found -> (* 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) end + Call(vf, new_args) end

(* Call to a nameless function *) with Not_found -> - let largs = lexp_parse_all pargs ctx bound in + let largs = 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 *) - let fname = _lexp_parse fname ctx bound in + let fname = lexp_parse fname ctx in Call(fname, new_args) end

(* Read a pattern and create the equivalent representation *) @@ -333,7 +314,7 @@ and lexp_read_pattern_args args ctx: in loop args [] ctx

(* Parse inductive constructor *) -and lexp_parse_constructors ctors ctx bound = +and lexp_parse_constructors ctors ctx =

let make_args (args:(arg_kind * pvar option * pexp) list): (arg_kind * ltype) list * lexp_context = @@ -345,7 +326,7 @@ and lexp_parse_constructors ctors ctx bound = (* What does the optional Pvar do ? that expression does not exist in LEXP*) | (kind, _, exp) -> - let lxp = _lexp_parse exp ctx bound in + let lxp = lexp_parse exp ctx in loop tl ((kind, lxp)::acc) ctx end in loop args [] ctx in

@@ -427,18 +408,18 @@ and lexp_decls decls ctx: (((vdef * lexp * ltype) list) * lexp_context) = | hd::tl -> match hd with | ((loc, name), Some pinst, None) ->( - let bound = (0, m) in - let lxp, ltp = lexp_p_infer pinst _ctx bound in + let nctx = local_scope _ctx m in + let lxp, ltp = lexp_p_infer pinst nctx in let nacc = ((loc, name), lxp, ltp)::acc in - let ctx2 = env_add_var_info (0, (loc, name), lxp, ltp) _ctx in + let ctx2 = env_add_var_info (0, (loc, name), lxp, ltp) nctx in process_var_info tl ctx2 nacc (m - 1))

| ((loc, name), Some pinst, Some ptype) ->( - let bound = (0, m) in - let linst = _lexp_parse pinst _ctx bound in - let ltyp = _lexp_parse ptype _ctx bound in + let nctx = local_scope _ctx m in + let linst = lexp_parse pinst nctx in + let ltyp = lexp_parse ptype nctx in let nacc = ((loc, name), linst, ltyp)::acc in - let ctx3 = env_add_var_info (0, (loc, name), linst, ltyp) _ctx in + let ctx3 = env_add_var_info (0, (loc, name), linst, ltyp) nctx in process_var_info tl ctx3 nacc (m - 1))

(* Skip the variable *) @@ -448,12 +429,12 @@ and lexp_decls decls ctx: (((vdef * lexp * ltype) list) * lexp_context) = let acc, ctx = process_var_info decls nctx [] n in acc, ctx

-and lexp_parse_all (p: pexp list) (ctx: lexp_context) bound: lexp list = +and lexp_parse_all (p: pexp list) (ctx: lexp_context): lexp list =

let rec loop (plst: pexp list) ctx (acc: lexp list) = match plst with | [] -> (List.rev acc) - | _ -> let lxp = _lexp_parse (List.hd plst) ctx bound in + | _ -> let lxp = lexp_parse (List.hd plst) ctx in (loop (List.tl plst) ctx (lxp::acc)) in

(loop p ctx []) @@ -538,11 +519,11 @@ and free_variable pxp = * - use lexp_p_check whenever you can. *)

-and lexp_p_infer (p : pexp) (env : lexp_context) bound: lexp * ltype = +and lexp_p_infer (p : pexp) (env : lexp_context): lexp * ltype =

(* Parse expr *) let tloc = pexp_location p in - let lxp = _lexp_parse p env bound in + let lxp = lexp_parse p env in

(* determine type *) match lxp with @@ -555,7 +536,7 @@ and lexp_p_infer (p : pexp) (env : lexp_context) bound: lexp * ltype = (lxp, UnknownType(tloc)))

- (* Pcall lookup fname *) + (* Pcall lookup fname type *) (* Pinductive *) (* PCons return its Pinductive type *)

@@ -574,14 +555,13 @@ and lexp_p_infer (p : pexp) (env : lexp_context) bound: lexp * ltype = and lexp_p_check (p : pexp) (t : ltype) (env : lexp_context): lexp = match p with | _ - -> let (e, inferred_t) = lexp_p_infer p env (0, 0) in + -> let (e, inferred_t) = lexp_p_infer p env in (* FIXME: check that inferred_t = t! *) e (* * Printing * --------------------- *) - -(* Print back in CET (Close Enough Typer) easier to read *) +(* FIXME: transform to lexp_to_buffer *) and lexp_print_adv opt exp = let slexp_print = lexp_print_adv opt in (* short_lexp_print *) let (pty, indent, prtp) = opt in @@ -702,7 +682,7 @@ and lexp_print_decls opt decls =

(* Print context *) and lexp_context_print ctx = - let ((n, map), env) = ctx in + let ((n, map), env, f) = ctx in

print_string (make_title " LEXP CONTEXT ");

@@ -773,7 +753,7 @@ let _lexp_expr_str (str: string) (tenv: bool array) let toks = lex tenv pretoks in let sxps = sexp_parse_all_to_list grm toks limit in let pxps = pexp_parse_all sxps in - lexp_parse_all pxps ctx (0, 0) + lexp_parse_all pxps ctx ;;

(* specialized version *)

===================================== tests/REPL.ml ===================================== --- a/tests/REPL.ml +++ b/tests/REPL.ml @@ -5,7 +5,7 @@ * * Example: * - * $./_build/ityper + * $./_build/ityper [files] * In[ 1] >> sqr = lambda x -> x * x; * In[ 2] >> (sqr 4); * Out[ 2] >> 16 @@ -49,7 +49,7 @@ let rec read_input i = let line = input_line stdin in let s = String.length str in let n = String.length line in - if s = 0 && n = 0 then read_input (i + 1) else + if s = 0 && n = 0 then read_input i else (if n = 0 then ( print_string " . "; print_string (make_line ' ' (i * 4)); @@ -63,7 +63,7 @@ let rec read_input i = print_string (make_line ' ' (i * 4)); loop str (i + 1))) in

- loop "" 1 + loop "" i ;;

(* Interactive mode is not usual typer @@ -75,7 +75,7 @@ type ldecl = vdef * lexp * ltype type lexpr = lexp

(* Grouping declaration together will enable us to support mutually recursive - * declarations *) + * declarations while bringing us closer to normal typer *) let ipexp_parse (sxps: sexp list): (pdecl list * pexpr list) = let rec _pxp_parse sxps dacc pacc = match sxps with @@ -92,7 +92,7 @@ let ipexp_parse (sxps: sexp list): (pdecl list * pexpr list) = let ilexp_parse pexps lctx = let pdecls, pexprs = pexps in let ldecls, lctx = lexp_decls pdecls lctx in - let lexprs = lexp_parse_all pexprs lctx (0, 0) in + let lexprs = lexp_parse_all pexprs lctx in (ldecls, lexprs), lctx ;;

@@ -103,8 +103,8 @@ let ieval lexps rctx = vals, rctx ;;

-let ieval_string str lctx rctx = - let pres = prelex_string str in +let _ieval f str lctx rctx = + let pres = (f str) in let sxps = lex default_stt pres in let nods = sexp_parse_all_to_list default_grammar sxps (Some ";") in

@@ -115,33 +115,47 @@ let ieval_string str lctx rctx = v, lctx, rctx ;;

-(* Specials commands %[command-name] *) -let rec repl () = - let lxp_ctx = make_lexp_context in - let rctx = make_runtime_ctx in +let ieval_string = _ieval prelex_string +let ieval_file = _ieval prelex_file

- (* Those are hardcoded operation *) - let lxp_ctx = add_def "_+_" lxp_ctx in - let lxp_ctx = add_def "_*_" lxp_ctx in - - let rec loop i clxp rctx = - let ipt = read_input i in - match ipt with - (* Check special keywords *) - | "%quit" -> () - | "%who" -> (print_rte_ctx rctx; loop (i + 1) clxp rctx) - | "%info" -> (lexp_context_print clxp; loop (i + 1) clxp rctx) - | "%calltrace" -> (print_call_trace (); loop (i + 1) clxp rctx) - (* eval input *) - | _ -> let (ret, clxp, rctx) = (ieval_string ipt clxp rctx) in - - List.iter (print_eval_result i) ret; - loop (i + 1) clxp rctx in - - loop 1 lxp_ctx rctx +(* Specials commands %[command-name] *) +let rec repl i clxp rctx = + let ipt = read_input i in + match ipt with + (* Check special keywords *) + | "%quit" -> () + | "%who" -> (print_rte_ctx rctx; repl (i + 1) clxp rctx) + | "%info" -> (lexp_context_print clxp; repl (i + 1) clxp rctx) + | "%calltrace" -> (print_call_trace (); repl (i + 1) clxp rctx) + (* eval input *) + | _ -> let (ret, clxp, rctx) = (ieval_string ipt clxp rctx) in + List.iter (print_eval_result i) ret; + repl (i + 1) clxp rctx ;;

+let arg_files = ref [] + + +(* ./ityper [options] files *) +let arg_defs = [ + (*"-I", + Arg.String (fun f -> searchpath := f::!searchpath), + "Append a directory to the search path"*) +];; + +let parse_args () = + Arg.parse arg_defs (fun s -> arg_files:= s::!arg_files) "" + let main () = + parse_args (); + + let lctx = ref make_lexp_context in + let rctx = ref make_runtime_ctx in + + (* Those are hardcoded operation *) + lctx := add_def "_+_" !lctx; + lctx := add_def "_*_" !lctx; + print_string (make_title " TYPER REPL "); print_string " %quit : leave REPL\n"; print_string " %who : print runtime environment\n"; @@ -150,7 +164,25 @@ let main () = print_string (make_sep '-'); flush stdout;

- repl () + let nfiles = List.length !arg_files in + + (* Read specified files *) + List.iteri (fun i file -> + print_string " In["; ralign_print_int (i + 1) 2; print_string "] >> "; + print_string ("%readfile " ^ file); print_string "\n"; + + let (ret, lctx1, rctx1) = ieval_file file (!lctx) (!rctx) in + lctx := lctx1; + rctx := rctx1; + List.iter (print_eval_result i) ret; + ) + + !arg_files; + + flush stdout; + + (* Initiate REPL. This will allow us to inspect interpreted code *) + repl (nfiles + 1) (!lctx) (!rctx) ;;

===================================== tests/debug.ml ===================================== --- a/tests/debug.ml +++ b/tests/debug.ml @@ -26,9 +26,8 @@ * --------------------------------------------------------------------------- * * Description: - * Provide helper functions to print out - * extracted Pretoken - * extracted Sexp + * Provide helper functions to print out extracted + * Pretoken, Sexp, pexp and lexp * * --------------------------------------------------------------------------- *)

===================================== tests/full_debug.ml ===================================== --- a/tests/full_debug.ml +++ b/tests/full_debug.ml @@ -20,11 +20,11 @@ * 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/. + * 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: * print out each compilation' steps * @@ -38,136 +38,152 @@ open Grammar open Pexp open Util open Fmt - -let dloc = dummy_location;; - open Debruijn open Myers open Lparse open Eval open Lexp

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

-(* -let pexp_lexp_all nodes ctx = - - let rec loop nodes ctx acc = - match nodes with - | [] -> ((List.rev acc), ctx) - | hd::tl -> - let lxp, new_ctx = pexp_lexp_one hd ctx in - (loop tl new_ctx (lxp::acc)) in - (loop nodes ctx []) -;; +let discard v = ();;

+(* Argument parsing *) +let arg_print_options = ref SMap.empty;; +let arg_files = ref []

+let add_p_option name () = + arg_print_options := SMap.add name true (!arg_print_options);;

-let add_rte_def name ctx = - (add_rte_variable (Some name) dummy_decl ctx);; - +let get_p_option name = + try let _ = SMap.find name (!arg_print_options) in + true + with + Not_found -> false +;;

-let eval_until_nth xpr n rctx = +let arg_defs = [ + ("-pretok", + Arg.Unit (add_p_option "pretok"), " Print pretok debug info"); + ("-tok", + Arg.Unit (add_p_option "tok"), " Print tok debug info"); + ("-sexp", + Arg.Unit (add_p_option "sexp"), " Print sexp debug info"); + ("-pexp", + Arg.Unit (add_p_option "pexp"), " Print pexp debug info"); + ("-lexp", + Arg.Unit (add_p_option "lexp"), " Print lexp debug info"); + ("-all", + Arg.Unit (fun () -> + add_p_option "pretok" (); + add_p_option "tok" (); + add_p_option "sexp" (); + add_p_option "pexp" (); + add_p_option "lexp" ()), + " Print all compilation step with debug info"); +];; + +let parse_args () = + Arg.parse arg_defs (fun s -> arg_files:= s::!arg_files) "" + +let make_default () = + arg_print_options := SMap.empty; + add_p_option "sexp" (); + add_p_option "pexp" (); + add_p_option "lexp" () +;;

- let rec loop xpr nb rctx = - match xpr, nb with - | [], _ -> rctx - | _, nb when nb = n -> rctx - | hd::tl, _ -> - let c, rctx = eval_toplevel hd rctx in - print_eval_result nb c; - loop tl (nb + 1) rctx in - loop xpr 0 rctx -;; *) - -let discard v = ();; - -let main () = +let main () = + parse_args ();

let arg_n = Array.length Sys.argv in - let usage = - " Usage: \n " ^ Sys.argv.(0) ^ " <file_name> [options] \n\n" in - + + let usage = + "\n Usage: " ^ Sys.argv.(0) ^ " <file_name> [options]\n" in + (* Print Usage *) if arg_n == 1 then - begin - print_string usage; - print_string " Options:\n"; - end + (Arg.usage (Arg.align arg_defs) usage) else begin - let filename = Sys.argv.(1) in - (* Read additional Args if any *) + (if arg_n = 2 then make_default ()); + + let filename = List.hd (!arg_files) in

print_string (make_title " ERRORS "); (* get pretokens*) let pretoks = prelex_file filename in - + (* get sexp/tokens *) let toks = lex default_stt pretoks in - + (* get node sexp *) let nodes = sexp_parse_all_to_list default_grammar toks (Some ";") 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 (* Those are hardcoded operation *) let ctx = add_def "_+_" ctx in let ctx = add_def "_*_" 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 "\n"; - print_string (make_title " Pexp "); debug_pexp_decls pexps; - (*debug_pexp_print_all pexps;*) - print_string "\n"; - print_string (make_title " Lexp "); debug_lexp_decls lexps; - (* debug_lexp_print_all lexps; *) - print_string "\n"; + (* Printing *) + (if (get_p_option "pretok") then( + print_string (make_title " PreTokens"); + debug_pretokens_print_all pretoks; print_string "\n")); + + (if (get_p_option "tok") then( + print_string (make_title " Base Sexp"); + debug_sexp_print_all toks; print_string "\n")); + + (if (get_p_option "sexp") then( + print_string (make_title " Node Sexp "); + debug_sexp_print_all nodes; print_string "\n")); + + (if (get_p_option "pexp") then( + print_string (make_title " Pexp "); + debug_pexp_decls pexps; print_string "\n")); + + (if (get_p_option "lexp") then( + print_string (make_title " Lexp "); + debug_lexp_decls lexps; print_string "\n"));

print_string "\n"; lexp_context_print nctx; print_string "\n"; - + (* Eval Each Expression *) print_string (make_title " Eval Print "); - - + (* Eval declaration *) - let rctx = make_runtime_ctx in + let rctx = make_runtime_ctx in let rctx = eval_decls lexps rctx in - - let _ = + + 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 + + with Not_found -> () in - + (* Print info *) print_string "\n\n"; - print_rte_ctx rctx; - - + print_rte_ctx rctx; + print_call_trace (); end ;;

===================================== tests/lexp_test.ml ===================================== --- a/tests/lexp_test.ml +++ b/tests/lexp_test.ml @@ -1,6 +1,7 @@ open Lparse (* add_def *) open Debruijn (* make_lexp_context *) open Lexp +open Pexp open Utest_lib

(* default environment *) @@ -9,42 +10,42 @@ let lctx = add_def "_+_" lctx let lctx = add_def "_*_" lctx

-let _ = (add_test "LEXP" "Built-in Inference" (fun () -> +let _ = (add_test "LEXP" "Built-in type Inference" (fun () ->

let dcode = "a = 10; b = 1.12;" in

let ret, _ = lexp_decl_str dcode lctx in - + match ret with (* (vdef * lexp * ltype) *) - | [(_, _, Builtin(_, "Int", _)); - (_, _, Builtin(_, "Float", _))] -> + | [(_, _, Builtin(_, "Int", _)); + (_, _, Builtin(_, "Float", _))] -> success()

| _ -> failure ()) );;

-open Pexp -

let set_to_list s = StringSet.fold (fun g a -> g::a) s [] ;;

let _ = (add_test "LEXP" "Free Variable" (fun () -> - + let dcode = " a = 2; b = 3; f = lambda n -> (a + n); % a is a fv - g = lambda x -> ((f b) + a + x); % f,a,b is fv + g = lambda x -> ((f b) + a + x); % f,a,b are fv " in

let ret = pexp_decl_str dcode in - let (_, g, _)::_ = List.rev ret in + let g = match List.rev ret with + | (_, g, _)::_ -> g + | _ -> raise (Unexpected_result "Unexpected empty list") in

let (bound, free) = free_variable g in - + let bound = set_to_list bound in let (free, _) = free in

@@ -56,9 +57,7 @@ let _ = (add_test "LEXP" "Free Variable" (fun () -> | _ -> failure ()

));; - -

(* run all tests *) run_all () -;; \ No newline at end of file +;;

===================================== tests/pexp_test.ml ===================================== --- a/tests/pexp_test.ml +++ b/tests/pexp_test.ml @@ -1,25 +1,22 @@ -open Pexp -open Utest_lib +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 + | Plet(_, arg, _) -> (match arg with | [] -> failure () | (_, tp, bl)::_ ->( - if bl = true then - success () - else - failure ()) + if bl = true then success () else failure ())) | _ -> failure ()) - | [] -> failure ()) + | _ -> failure ()) ) ;;

===================================== tests/utest_lib.ml ===================================== --- a/tests/utest_lib.ml +++ b/tests/utest_lib.ml @@ -56,12 +56,15 @@ let _global_sections = ref StringMap.empty let _insertion_order = ref [] let _ret_code = ref 0

+(* Exception *) +exception Unexpected_result of string + (* Value Checking *) (* USAGE: expect_something_type value expected_value *) (* return success() if match else failure () *) let unexpected_throw sk tk e = print_string ("[ FAIL] " ^ sk ^ " - " ^ tk ^ "\n"); - print_string "[ ] UNEXPECTED THROW: \n"; + print_string "[ ] UNEXPECTED THROW:\n"; print_string "[ ] "; print_string ((Printexc.to_string e) ^ "\n"); ;;

@@ -101,7 +104,7 @@ let add_section sname = *) let add_test sname tname tfun =

- (* Does Section Exists ? *) + (* Does Section Exist ? *) let (tmap, lst) = add_section sname in

try let _ = StringMap.find tname tmap in @@ -124,8 +127,8 @@ let for_all_tests sk tmap tk = flush stdout; try let r = tv () in - if r = 0 then - (print_string ("[ OK] " ^ sk ^ " - " ^ tk ^ "\n")) + if r = 0 then( + print_string ("[ OK] " ^ sk ^ " - " ^ tk ^ "\n")) else( print_string ("[ FAIL] " ^ sk ^ " - " ^ tk ^ "\n"); _ret_code := failure ()) @@ -151,8 +154,3 @@ let run_all () = (* return success or failure *) exit !_ret_code ;; - - - - -

View it on GitLab: https://gitlab.com/monnier/typer/compare/74750a6624e99e6a45b0f766201b32ba4a8...