Setepenre pushed to branch master at Stefan / Typer

Commits: 36520963 by Pierre Delaunay at 2016-03-04T20:31:09-05:00 prelex_string hack

- - - - - e8c42357 by Pierre Delaunay at 2016-03-04T23:44:41-05:00 call + lambda eval

- - - - - b3a7eafb by Pierre Delaunay at 2016-03-06T13:13:10-05:00 simple repl for interactive testing

- - - - - cd150174 by Pierre Delaunay at 2016-03-06T15:06:10-05:00 fix inductive pexp parsing

- - - - - bbeff6f8 by Pierre Delaunay at 2016-03-06T16:47:12-05:00 eval case

- - - - - c6d73fd5 by Pierre Delaunay at 2016-03-06T21:16:28-05:00 env_info fix

- - - - -

15 changed files:

- .gitignore - GNUmakefile - + samples/case.typer - + samples/functions.typer - + samples/inductives.typer - + samples/let.typer - samples/lexp_test.typer - src/debruijn.ml - src/eval.ml - src/lexer.ml - src/lparse.ml - src/pexp.ml - src/prelexer.ml - + tests/REPL.ml - tests/full_debug.ml

Changes:

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

===================================== GNUmakefile ===================================== --- a/GNUmakefile +++ b/GNUmakefile @@ -1,21 +1,27 @@ RM=rm -f

TEST_FILES := $(wildcard ./tests/*_test.ml) -# This is for windows: Make windows version is old +# This is for windows: windows version is old ifeq ($(OS),Windows_NT) SHELL=C:/Windows/System32/cmd.exe endif

-all: typer debug tests +all: ityper typer debug tests

typer: ocamlbuild src/main.byte -cflag -rectypes mv _build/src/main.byte _build/typer # move and rename executable

+# debug file eval debug: ocamlbuild tests/full_debug.native -I src -cflag -rectypes mv _build/tests/full_debug.native _build/full_debug

+# interactive typer +ityper: + ocamlbuild tests/REPL.native -I src -cflag -rectypes + mv _build/tests/REPL.native _build/ityper + tests: # Build tests $(foreach test, $(TEST_FILES), ocamlbuild $(subst ./,,$(subst .ml,.native,$(test))) -I src -cflag -rectypes;) @@ -29,9 +35,10 @@ doc-tex: texi2pdf ./doc/manual.texi --pdf --build=clean

# Make implementation doc -doc-ocaml: - ocamldoc +#doc-ocaml: +# ocamldoc

+.PHONY: ityper .PHONY: typer .PHONY: debug .PHONY: tests

===================================== samples/case.typer ===================================== --- /dev/null +++ b/samples/case.typer @@ -0,0 +1,39 @@ +% ------------------------------------------- +% 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)); + +% Case test +% x = (succ zero); +x = (succ (succ zero)); + +% Simple +case x + | zero => 0 + | succ y => y + | _ => (2 + 4); + +% recursive +tonum = lambda x -> case x + | zero => 0 + | (succ y) => (1 + (tonum y)); + +(tonum x); + + + \ No newline at end of file

===================================== samples/functions.typer ===================================== --- /dev/null +++ b/samples/functions.typer @@ -0,0 +1,32 @@ +% ------------------------------------------- +% Function Calls +% ------------------------------------------- + +% define sqrt +sqrt = lambda (x : Nat) -> x * x; + +(sqrt 2); + +% define cube +cube = lambda (x : Nat) -> x * (sqrt 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 ===================================== --- /dev/null +++ b/samples/inductives.typer @@ -0,0 +1,23 @@ +% ------------------------------------------- +% 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 ===================================== --- /dev/null +++ b/samples/let.typer @@ -0,0 +1,23 @@ +% ------------------------------------------- +% 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 +% ---------------------- + +% Recursive Let

===================================== samples/lexp_test.typer ===================================== --- a/samples/lexp_test.typer +++ b/samples/lexp_test.typer @@ -1,47 +1,10 @@ -% Eval test

-let c = 1; a = 5; b = 10; d = 3; in - a + b; - -% ------------------------------------------- -% Function Calls -% ------------------------------------------- - -% define sqrt -sqrt = lambda (x : Nat) -> x * x; - -% define cube -cube = lambda (x : Nat) -> x * (sqrt x); - -% explicit -mult = lambda (x : Nat) -> lambda (y : Nat) -> (y * x); - -% implicit (Type annotation introduce a bug) -cube = lambda x y -> (x * y);

-% ------------------------------------------- -% Inductive type -% ------------------------------------------- - -inductive_ (dummy_Nat) (zero) (succ Nat); - -% Usage -Nat : Type % This line is not parsed -Nat = inductive_ (dummy_Nat) (zero) (succ Nat); % zero is not parsed - % Constructor % -------------------------------------------

-% 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));

% ------------------------------------------- % Cases

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -113,10 +113,8 @@ let senv_add_var name loc ctx =

(* *) let env_add_var_info var (ctx: lexp_context) = - let (a, _) = ctx in - (* let (rof, (loc, name), value, ltyp) = var in *) - let nenv = _add_var_env var ctx in - (a, nenv) + let (a, env) = ctx in + (a, cons var env) ;;

let env_lookup_type_by_index index ctx =

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -36,29 +36,39 @@ open Lparse open Myers open Sexp open Fmt +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"

let print_myers_list l print_fun = let n = (length l) in

- print_string "-------------------\n"; - print_string " Environement: \n"; - print_string "-------------------\n"; + let title = " EVAL ENVIRONMENT " in + let title_n = String.length title in + let sep_n = (80 - title_n - 4) / 2 in + let sep_t = 80 - 4 in + let psep = (make_line '=' sep_n) in + let fsep = (make_line '=' sep_t) in + let sep = " " ^ fsep ^ "\n" in + + print_string (" " ^ psep ^ title ^ psep ^ "\n"); + print_string " | INDEX | VARIABLE NAME | VALUE \n"; + print_string (" " ^ (make_line '-' sep_t) ^ "\n");

for i = 0 to n - 1 do - ralign_print_int (i + 1) 4; - print_string ") "; + print_string " | "; + ralign_print_int i 5; + print_string " | "; print_fun (nth i l); done; - print_string "-------------------\n"; + print_string sep; ;;

let get_function_name fname = @@ -74,17 +84,23 @@ let get_int lxp = ;;

(* Runtime Environ *) -type runtime_env = lexp myers +type runtime_env = (string option * lexp) myers let make_runtime_ctx = nil;; -let add_rte_variable x l = (cons x l);; -let get_rte_variable idx l = (nth (idx) l);; +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 print_rte_ctx l = print_myers_list l - (fun g -> lexp_print g; print_string "\n") + (fun (n, g) -> + let _ = + match n with + | Some m -> lalign_print_string m 12; print_string " | " + | None -> print_string (make_line ' ' 12); print_string " | " in + lexp_print g; print_string "\n") ;;

-(* Evaluation reduce an expression x to an Lexp.Imm *) -let rec eval lxp ctx: (lexp * runtime_env) = +(* _evaluation reduce an expression x to an Lexp.Imm *) +let rec _eval lxp ctx: (lexp * runtime_env) =

match lxp with (* This is already a leaf *) @@ -102,80 +118,201 @@ let rec eval lxp ctx: (lexp * runtime_env) =

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

(* Function call *) - | Call (lname, args) -> - (* Try to extract name *)(* - let tname = match lname with - | Var((loc, name), _) -> name - | _ -> lexp_print lname; eval_error "Incorrect Function Name" in - - (* Save declaration in environment *) - let n = List.length args in - if tname = "_=_" && n == 2 then - let (((_, name), _), expr) = args in - let nctx = add_rte_variable *) - - - (* Add args in the scope *) - print_rte_ctx ctx; - let nctx = build_arg_list args ctx in - print_rte_ctx nctx; - - (* We need to seek out the function declaration and eval the body *) - (* but currently we cannot declare functions so I hardcoded + *) - (* let bdy = get_body fname in - eval bdy nctx *) - - (* fname is currently a var *) - let name = get_function_name lname in - (* Hardcoded function for now *) - if name = "_+_" then begin + | Call (lname, args) -> ( + (* Try to extract name *) + match lname with + (* Function declaration *) + | Var((loc, name), _) when name = "_=_" -> + (* Save declaration in environment *) + let (vr, body) = match args with + | [(_, a); (_, b)] -> a, b + | _ -> _eval_error loc "Wrong number of Args" in + + let vname = get_function_name vr in + let nctx = add_rte_variable (Some vname) body ctx in + body, nctx

- (* Get the two args *) + (* Hardcoded functions *) + | Var((_, name), _) when name = "_+_" -> + let nctx = build_arg_list args ctx in 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

- (*print_int l; print_string " "; - print_int r; print_string "\n"; *) + | Var((_, name), _) when name = "_*_" -> + let nctx = build_arg_list args ctx in + 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 + + (* This is a named function call *) + (* TODO: handle partial application *) + | Var((_, _), idx) when idx >= 0 -> + (* get function body *) + let body = get_rte_variable idx ctx in + (* Add args in the scope *) + let nctx = build_arg_list args ctx in + let e, nctx = (_eval body nctx) in + (* we exit function and send back old ctx *) + e, ctx + + (* TODO Everything else *) + (* Which includes a call to a lambda *) + | _ -> Imm(String(dloc, "Funct Not Implemented")), ctx) + + | Lambda(_, vr, _, body) -> begin + let (loc, name) = vr in + let value = (get_rte_variable 0 ctx) in + let nctx = add_rte_variable (Some name) value ctx in + + let rec build_body bd idx nctx = + match bd with + | Lambda(_, vr, _, body) -> + let (loc, name) = vr in + (* Get Variable from call context *) + 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) + | _ -> bd, nctx in

- Imm(Integer(dummy_location, l + r)), ctx end + let body, nctx = build_body body 1 nctx in + + let e, nctx = _eval body nctx in + e, ctx end + + (* Inductive is a type declaration. We have nothing to eval *) + | Inductive (_, _, _, _) as e -> e, ctx + + (* inductive-cons build a type too? *) + | Cons (_, _) as e -> e, ctx + + (* Case *) + | Case (loc, target, _, pat, dflt) -> begin + + (* Eval target *) + let v, nctx = _eval target 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" ) + (* + | 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 *) + + | _ -> lexp_print target; + _eval_error loc "Can't match expression" in + + (* Check if a default is present *) + let run_default df = + match df with + | None -> Imm(String(loc, "Match Failure")), ctx + | Some lxp -> _eval lxp ctx in + + let ctor_n = List.length args in + + (* Build a filter option *) + let is_true key value = + let (_, pat_args, _) = value in + let pat_n = List.length pat_args in + if pat_n = ctor_n && ctor_name = key then + true + else + false in + + (* Search for the working pattern *) + let sol = SMap.filter is_true pat in + if SMap.is_empty sol then + run_default dflt else - Imm(String(dummy_location, "Funct Not Implemented")), ctx - - | _ -> Imm(String(dummy_location, "Eval Not Implemented")), ctx + (* Get working pattern *) + let key, (_, pat_args, exp) = SMap.min_binding sol in + + (* build context *) + let nctx = List.fold_left2 (fun nctx pat cl -> + match pat with + | None -> nctx + | Some (_, (_, name)) -> let (_, xp) = cl in + add_rte_variable (Some name) xp nctx) + + nctx pat_args args in + + let r, nctx = _eval exp nctx in + (* return old context as we exist the case *) + r, ctx end + + | _ -> Imm(String(dloc, "eval Not Implemented")), ctx

and build_arg_list args ctx = - (* Eval every args *) - let arg_val = List.map (fun (k, e) -> let (v, c) = eval e ctx in v) args in + (* _eval every args *) + let arg_val = List.map (fun (k, e) -> let (v, c) = _eval e ctx in v) args in (* Add args inside context *) - List.fold_left (fun c v -> add_rte_variable v c) ctx arg_val + List.fold_left (fun c v -> add_rte_variable None v c) ctx arg_val

and build_ctx decls ctx = match decls with | [] -> ctx | hd::tl -> let (v, exp, tp) = hd in - let (value, nctx) = eval exp ctx in - let nctx = add_rte_variable value nctx in + let (value, nctx) = _eval exp ctx in + let nctx = add_rte_variable None value nctx in build_ctx tl nctx ;;

-let print_eval_result lxp = - print_string " >> "; +let eval lxp ctx = + try + _eval lxp ctx + with + e -> print_rte_ctx ctx; + Imm(String(dloc, "Evaluation Failed")), ctx +;; + +let 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" - | _ -> print_string "Evaluation Failed\n" + | e -> lexp_print e; print_string "\n" ;;

let evalprint lxp ctx = let v, ctx = (eval lxp ctx) in - print_eval_result v; + print_eval_result 0 v; ctx ;;

+(* +let eval_string (str: string) tenv grm limit lxp_ctx rctx = + 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_parse_all sxps in + let lxp, lxp_ctx = lexp_parse_all pxps lxp_ctx in + (eval lxp rctx), lxp_ctx +;; + +*) +

===================================== src/lexer.ml ===================================== --- a/src/lexer.ml +++ b/src/lexer.ml @@ -117,4 +117,16 @@ let lex tenv (pts : pretoken list) : sexp list = | _ -> let (tok, pts, bpos, cpos) = nexttoken tenv pts bpos cpos in gettokens pts bpos cpos (tok :: acc) in gettokens pts 0 0 [] +;; + +let lex_string (str: string) tenv = + let pretoks = prelex_string str in + lex tenv pretoks +;; + +let node_parse_string (str: string) tenv grm limit = + let pretoks = prelex_string str in + let toks = lex tenv pretoks in + sexp_parse_all_to_list grm toks limit +;;

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -38,6 +38,9 @@ open Grammar open Debruijn open Fmt

+open Lexer +open Prelexer + (* Shortcut => Create a Var *) let make_var name index loc = Var(((loc, name), index)) @@ -47,6 +50,8 @@ let not_implemented_error () = internal_error "not implemented" ;;

+let dlxp = UnknownType(dloc) +let dltype = UnknownType(dloc) let dloc = dummy_location

let lexp_warning = msg_warning "LEXP" @@ -64,11 +69,32 @@ type print_context = (bool * int * bool) let pvar_to_vdef p = p ;; + +(* +let _ab = senv_add_var;; +let senv_add_var = + _ab name loc ctx +;;*) + (* PEXP is not giving SEXP types this is why types are always unknown *)

(* * The main job of lexp (currently) is to determine variable name (index) * and to regroup type specification with their variable + * + * lexp_context is composed of two environment: senv and env. + * the senv environment is used to find the correct debruijn index + * while the env environment is used to save variable information. + * the env environment look a lot like the runtime environment that will be + * used in the eval section. + * + * While most of the time senv and env will be synchronised it is + * 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: pexp) (ctx: lexp_context): (lexp * lexp_context) = @@ -88,13 +114,14 @@ let rec lexp_parse (p: pexp) (ctx: lexp_context): (lexp * lexp_context) = with Not_found -> (* Add Variable *) let ctx = senv_add_var name loc ctx in - (make_var name 0 loc), ctx; end + let ctx = env_add_var_info (0, (loc, name), dlxp, dlxp) ctx in + (make_var name 0 loc), ctx; end

(* Let, Variable declaration + local scope *) | Plet(loc, decls, body) -> let decl, nctx = lexp_parse_let decls ctx in - lexp_context_print nctx; - let bdy, nctx = lexp_parse body nctx in + (* Body cannot modify context *) + let bdy, _ = lexp_parse body nctx in (* Send back old context as we exit the inner scope *) Let(tloc, decl, bdy), ctx

@@ -112,79 +139,66 @@ let rec lexp_parse (p: pexp) (ctx: lexp_context): (lexp * lexp_context) =

(* *) | Plambda (kind, var, Some ptype, body) -> - let nvar = pvar_to_vdef var in (* /!\ HERE *) - let ltyp, ctx = lexp_parse ptype ctx in - let lbody, ctx = lexp_parse body ctx in - Lambda(kind, nvar, ltyp, lbody), ctx + (* Add argument to context *) + let (loc, vname) = var in + 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 + + (* Return old context as we exit lambda scope*) + Lambda(kind, var, ltyp, lbody), ctx

| Plambda (kind, var, None, body) -> - let nvar = pvar_to_vdef var in (* /!\ HERE *)(* /!\ Missing Type *) - let lbody, ctx = lexp_parse body ctx in - Lambda(kind, nvar, UnknownType(tloc), lbody), ctx + 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 + Lambda(kind, var, UnknownType(tloc), lbody), ctx

| Pcall (fname, _args) -> - (* Process Arguments *) - let pargs = pexp_parse_all _args in - let largs, fctx = lexp_parse_all pargs ctx in - (* Make everything explicit for now *) - let new_args = List.map (fun g -> (Aexplicit, g)) largs in - - (* Call to named function which must have been defined earlier * - * i.e they must be in the context *) - begin try begin - (* Get function name *) - let name, loc = match fname with - | Pvar(loc, nm) -> nm, loc - | Pcons (_, (loc, nm)) -> nm, loc - | _ -> raise Not_found 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), ctx - - 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), ctx end - - (* Call to a nameless function *) - with Not_found -> - (* I think this should not modify context. - * if so, funny things might happen when evaluating *) - let fname, ctx = lexp_parse fname ctx in - Call(fname, new_args), ctx end + lexp_call fname _args ctx

(* Pinductive *) - | Pinductive (label, _, ctors) -> - let dummy = (Aexplicit, (dummy_location, "a"), UnknownType(tloc))::[] in + | Pinductive (label, [], ctors) -> let map_ctor, nctx = lexp_parse_constructors ctors ctx in - (* We exit current context, return old context *) - Inductive(tloc, label, dummy, map_ctor), ctx + Inductive(tloc, label, [], map_ctor), nctx

(* Pcons *) - | Pcons(var, sym) -> (* vref, symbol*) - let (loc, name) = var in - let idx = 0 in - Cons(((pvar_to_vdef var), idx), sym), ctx + | Pcons(vr, sym) -> ( + let (loc, type_name) = vr in + let (_, ctor_name) = sym 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), sym), ctx + with Not_found -> + lexp_error loc + ("The inductive type: " ^ type_name ^ " was not declared"); + Cons((vr, -1), sym), ctx)

(* Pcase *) | Pcase (loc, target, patterns) ->

- let lxp, ltp = lexp_p_infer target ctx in - + let lxp, nctx = lexp_parse target ctx in + let ltp = UnknownType(loc) in + (* Read patterns one by one *) let rec loop ptrns merged dflt = match ptrns with | [] -> merged, dflt | hd::tl -> let (pat, exp) = hd in - (* Parse the pattern first then parse the expr *) - let (name, iloc, arg) = lexp_read_pattern pat exp lxp in - let exp, nctx = lexp_parse exp ctx in + (* Create pattern context *) + let (name, iloc, arg), nctx = lexp_read_pattern pat exp lxp nctx in + (* parse using pattern context *) + let exp, nctx = lexp_parse exp nctx in + if name = "_" then loop tl merged (Some exp) else @@ -192,53 +206,123 @@ let rec lexp_parse (p: pexp) (ctx: lexp_context): (lexp * lexp_context) = loop tl merged dflt in

let (lpattern, dflt) = loop patterns SMap.empty None in + (* Exit case, send back old context *) Case(loc, lxp, ltp, lpattern, dflt), ctx

| _ -> UnknownType(tloc), ctx + +(* Identify Call Type and return processed call *) +and lexp_call fname _args ctx = + (* Process Arguments *) + let pargs = pexp_parse_all _args in + + (* Call to named function which must have been defined earlier * + * i.e they must be in the context *) + begin try begin + (* Get function name *) + let name, loc = match fname with + | Pvar(loc, nm) -> nm, loc + | Pcons (_, (loc, nm)) -> nm, loc + | _ -> raise Not_found in + + (* _=_ is a special function *) (**) + let n = List.length pargs in + if name = "_=_" && n = 2 then( + let (var, inst) = match pargs with + | [a; b] -> a, b + (* This was added to remove a warning but will never be true *) + | _ -> lexp_fatal loc "Wrong Number of Args" in + + let vname = match var with Pvar(loc, name) -> name + | e -> pexp_print var; "str" 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, ltyp = lexp_p_infer inst nctx in + + (* Add Var info*) + let nctx = env_add_var_info (0, (loc, vname), lxp, ltyp) nctx in + + (* _=_ is the only function with -2 index *) + let vf = (make_var "_=_" (-2) loc) in + let vr = (make_var vname idx loc) in + + Call(vf, [(Aexplicit, vr); (Aexplicit, lxp)]), nctx) + else(**) + let largs, fctx = 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), ctx + + 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), ctx end + + (* Call to a nameless function *) + with Not_found -> + 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 *) + let fname, ctx = lexp_parse fname ctx in + Call(fname, new_args), ctx end + (* Read a pattern and create the equivalent representation *) -and lexp_read_pattern pattern exp target: - (string * location * (arg_kind * vdef) option list) = +and lexp_read_pattern pattern exp target ctx: + ((string * location * (arg_kind * vdef) option list) * lexp_context) =

(* lookup target val if its a var and extract its args *) (* TODO *)

match pattern with | Ppatany (loc) -> (* Catch all expression nothing to do *) - ("_", loc, []) + ("_", loc, []), ctx

| Ppatvar (loc, name) -> (* Create a variable containing target *) - (*let nctx = add_variable name loc ctx in - let idx = get_var_index name nctx in - let info = (idx, (loc, name), target, UnknownType(loc)) in - let nctx = add_variable_info info nctx in *) - (name, loc, []) + 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

| Ppatcons (ctor_name, args) -> let (loc, name) = ctor_name in

(* read pattern args *) - let args = lexp_read_pattern_args args in - (name, loc, args) + let args, nctx = lexp_read_pattern_args args ctx in + (name, loc, args), nctx

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

- let rec loop args acc = + let rec loop args acc ctx = match args with - | [] -> (List.rev acc) - | hd::tl -> + | [] -> (List.rev acc), ctx + | hd::tl -> ( let (_, pat) = hd in match pat with (* Nothing to do *) - | Ppatany (loc) -> loop tl (None::acc) + | Ppatany (loc) -> loop tl (None::acc) ctx | Ppatvar (loc, name) -> + (* Add var *) + let nctx = senv_add_var name loc ctx in + let nctx = env_add_var_info (0, (loc, name), dlxp, dltype) nctx in let nacc = (Some (Aexplicit, (loc, name)))::acc in - loop tl nacc - | _ -> lexp_fatal dloc "Constructor inside a Constructor"; + loop tl nacc nctx + | _ -> lexp_error dloc "Constructor inside a Constructor"; + loop tl (None::acc) ctx)

- in loop args [] + in loop args [] ctx

(* Parse inductive constructor *) and lexp_parse_constructors ctors ctx = @@ -279,7 +363,7 @@ and lexp_parse_let decls ctx = let ((_, name), _, _) = p in if name == target then true else false in

- let rec loop (decls: (pvar * pexp * bool) list) merged: + let rec merge_decls (decls: (pvar * pexp * bool) list) merged: (vdef * pexp option * pexp option) list =

(* we cant evaluate here because variable are not in the environment *) @@ -294,22 +378,22 @@ and lexp_parse_let decls ctx = * 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 - (loop tl (new_decl::merged)) + (merge_decls tl (new_decl::merged)) with Not_found -> let new_decl = (loc, name), None, Some type_info in - (loop tl (new_decl::merged)) end + (merge_decls tl (new_decl::merged)) 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 - (loop tl (new_decl::merged)) + (merge_decls tl (new_decl::merged)) with Not_found -> let new_decl = ((loc, name), Some inst, None) in - (loop tl (new_decl::merged)) end in + (merge_decls tl (new_decl::merged)) end in

- let decls = loop decls [] in + let decls = merge_decls decls [] in

(* Add Each Variable to the environment *) let nctx = List.fold_left (fun ctx hd -> @@ -318,32 +402,32 @@ and lexp_parse_let decls ctx = | ((loc, name), _, _) -> senv_add_var name loc ctx) ctx decls in

- (* lexp_parse instruction and types *) - let rec parse_decls decls ctx acc = - match decls with - | [] -> (List.rev acc), ctx - | hd::tl -> begin - match hd with - | ((loc, name), Some pinst, Some ptype) -> - let linst, nctx = lexp_parse pinst ctx in - let ltyp, nctx = lexp_parse ptype nctx in - let nacc = ((loc, name), linst, ltyp)::acc in - let nctx = - env_add_var_info (0, (loc, name), linst, ltyp) nctx in - (parse_decls tl nctx nacc) - | ((loc, name), Some pinst, None) -> - let lxp, ltp = lexp_p_infer pinst ctx in + (* Add Variable info *) + let rec process_var_info dcl_lst _ctx acc = + match dcl_lst with + | [] -> (List.rev acc), _ctx + | hd::tl -> + match hd with + | ((loc, name), Some pinst, None) ->( + let lxp, ltp = lexp_p_infer pinst _ctx in let nacc = ((loc, name), lxp, ltp)::acc in - let nctx = - env_add_var_info (0, (loc, name), lxp, ltp) nctx in - (parse_decls tl nctx nacc) + let ctx2 = env_add_var_info (0, (loc, name), lxp, ltp) _ctx in + process_var_info tl ctx2 nacc) + + | ((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) + (* Skip the variable *) - | ((loc, name), None, _) -> - lexp_warning loc "Unused Variable"; - (parse_decls tl ctx acc) end in - - parse_decls decls nctx [] - + | ((loc, name), None, _) -> (lexp_warning loc "Unused Variable"; + process_var_info tl _ctx acc) in + + let acc, ctx = process_var_info decls nctx [] in + acc, ctx + and lexp_parse_all (p: pexp list) (ctx: lexp_context): (lexp list * lexp_context) = let rec loop (plst: pexp list) ctx (acc: lexp list) = @@ -394,8 +478,7 @@ and lexp_print_adv opt exp = | Imm(value) -> sexp_print value | Var ((loc, name), idx) -> print_string name; - if idx > 0 then begin - print_string "("; print_int idx; print_string ")"; end + print_string "["; print_int idx; print_string "]"

| Let (_, decls, body) -> print_string "let"; lexp_print_decls (pty, indent + 1, prtp) decls; @@ -416,13 +499,14 @@ and lexp_print_adv opt exp = | Cons(vf, symbol) -> let (loc, name) = symbol in let ((loc, vname), idx) = vf in - print_string (name ^ "("); print_string (vname ^ ")"); + print_string (name ^ "("); print_string vname; + print_string "["; print_int idx; print_string "])"

| Call(fname, args) -> begin (* /!\ Partial Print *) (* get function name *) - let str = match fname with - | Var((_, name), _) -> name - | _ -> "unkwn" in + let str, idx = match fname with + | Var((_, name), idx) -> name, idx + | _ -> "unkwn", -1 in

let print_arg arg = match arg with | (kind, lxp) -> lexp_print_adv (pty, 0, prtp) lxp in @@ -439,7 +523,7 @@ and lexp_print_adv opt exp = | ("_*_", [lhs; rhs]) -> print_binop " * " lhs rhs (* not an operator *) | _ -> - print_string ("(" ^ str); + print_string ("(" ^ str ^ "["); print_int idx; print_string "]"; List.iter (fun arg -> print_string " "; print_arg arg) args; print_string ")" end

@@ -506,26 +590,67 @@ and lexp_print_decls opt decls = and lexp_context_print ctx = let ((n, map), env) = ctx in

+ print_string (" " ^ (make_line '=' 20) ^ " LEXP CONTEXT " ^ (make_line '=' 20) ^ "\n"); + print_string " | "; + ralign_print_string "NAME" 10; print_string " | "; + ralign_print_string "INDEX" 7; print_string " | "; + ralign_print_string "NAME" 10; print_string " | "; + ralign_print_string "VALUE" 7; print_string ": "; + print_string "TYPE"; print_string "\n"; + print_string (" " ^ (make_line '-' 54) ^ "\n"); + StringMap.iter (fun key idx -> (* Print senv info *) - print_string " "; - ralign_print_string key 20; - print_string " => "; - ralign_print_int idx 4; - print_string " => "; + print_string " | "; + ralign_print_string key 10; + print_string " | "; + ralign_print_int (n - idx - 1) 7; + print_string " | ";

(* Print env Info *) - try let (_, (_, name), exp, tp) = env_lookup_by_index (n - idx) ctx in - print_string name; (* name must match *) - print_string " = "; + try let (_, (_, name), exp, tp) = env_lookup_by_index (n - idx - 1) ctx in + ralign_print_string name 10; (* name must match *) + print_string " | "; lexp_print_adv (false, 0, true) exp; print_string ": "; lexp_print_adv (false, 0, true) tp; print_string "\n" with Not_found -> print_string "Not_found \n") - map + + map; + + print_string (" " ^ (make_line '=' 54) ^ "\n"); + +(* Only print var info *) +and lexp_print_var_info ctx = + let ((_, _), env) = ctx in + let n = Myers.length env in + + for i = 0 to n - 1 do ( + let (_, (_, name), exp, tp) = Myers.nth i env in + print_string name; (* name must match *) + print_string " = "; + lexp_print_adv (false, 0, true) exp; + print_string ": "; + lexp_print_adv (false, 0, true) tp; + print_string "\n") + done; ;;

let lexp_print = lexp_print_adv (false, 0, true) - + + +let lexp_parse_string (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 + let ctx = make_lexp_context in + let pxps = pexp_parse_all sxps in + lexp_parse_all pxps ctx +;; + +let add_def name ctx = + let ctx = senv_add_var name dloc ctx in + env_add_var_info (0, (dloc, name), dlxp, dlxp) ctx +;;

===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -22,6 +22,8 @@ this program. If not, see http://www.gnu.org/licenses/. *)

open Util open Sexp +open Lexer +open Prelexer

let pexp_error = msg_error "PEXP"

@@ -142,6 +144,9 @@ let rec pexp_parse (s : sexp) : pexp = (* read Constructor name + args => Type ((Symbol * args) list) *) | Node (Symbol s, cases) -> (s, List.map pexp_p_ind_arg cases)::pcases + (* This is a constructor with no args *) + | Symbol s -> (s, [])::pcases + | _ -> pexp_error (sexp_location case) "Unrecognized constructor declaration"; pcases) cases [] in @@ -349,3 +354,10 @@ let pexp_print e = sexp_print (pexp_unparse e) let pexp_parse_all (nodes: sexp list) = List.map pexp_parse nodes ;; + +let pexp_parse_string (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 +;;

===================================== src/prelexer.ml ===================================== --- a/src/prelexer.ml +++ b/src/prelexer.ml @@ -140,8 +140,17 @@ let prelex_file file = let fin = open_in file in prelex file fin 1 [] [] (* Traditionally, line numbers start at 1 :-( *)

+(* Since current implementation is not compatible with stream * + * we write a temporary file and use this file as input. * + * This is a terrible solution but for the things we do it does not * + * really matters. Plus it will make testing easier *) let prelex_string str = - prelex "string" str 1 [] [] + let fin = open_out "_temp_hack" in + output_string fin str; + (flush_all); + close_out fin; + let fin = open_in "_temp_hack" in + prelex "string" fin 1 [] []

let rec pretokens_print pretokens = List.iter (fun pt -> @@ -153,3 +162,8 @@ let rec pretokens_print pretokens = | Prestring(_, str) -> print_string """; print_string str; print_string """) pretokens + + + + + \ No newline at end of file

===================================== tests/REPL.ml ===================================== --- /dev/null +++ b/tests/REPL.ml @@ -0,0 +1,104 @@ +open Debug +open Prelexer +open Lexer +open Sexp +open Grammar +open Pexp +open Debruijn +open Lparse +open Myers +open Eval +open Util +open Lexp +open Fmt + +let print_input_line i = + print_string " In["; + ralign_print_int i 2; + print_string "] >> " +;; + +(* Read stdin for input. Returns only when the last char is ';' *) +let rec read_input i = + print_input_line i; + flush stdout; + + let rec loop str = + let line = input_line stdin in + let s = String.length str in + let n = String.length line in + if n = 0 then loop str else + let str = if s > 0 then String.concat "\n" [str; line] else line in + if line.[n - 1] = ';' || line.[0] = '%' then + str + else + (print_string " "; loop str) in + + loop "" +;; + + +let eval_string (str: string) tenv grm limit lxp_ctx 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 + + 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_parse_all sxps in + let lxp, lxp_ctx = lexp_parse_all pxps lxp_ctx in + (eval_all lxp [] rctx), lxp_ctx +;; + +(* Specials commands %[command-name] *) +let rec repl () = + 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 lxp_ctx = make_lexp_context in + (* Those are hardcoded operation *) + let lxp_ctx = add_def "_+_" lxp_ctx in + let lxp_ctx = add_def "_*_" lxp_ctx in + let lxp_ctx = add_def "_=_" lxp_ctx in + + let rctx = make_runtime_ctx in + + let rec loop i clxp rctx = + let ipt = read_input i in + (* Check special keywords *) + if ipt = "%quit" then () (* Stop REPL *) + else if ipt = "%who" then (* Print environment *) + (print_rte_ctx rctx; loop (i + 1) clxp rctx) + else if ipt = "%info" then + (lexp_context_print clxp; loop (i + 1) clxp rctx) + (* Else Process Typer code *) + else + let (ret, rctx), clxp = (eval_string ipt clxp rctx) in + let printe j v = print_eval_result i v in + List.iteri printe ret; + print_string "\n"; + loop (i + 1) clxp rctx in + + loop 1 lxp_ctx rctx +;; + +let main () = + print_string ((make_line '-' 80) ^ "\n"); + print_string " Typer REPL \n"; + print_string " %quit : to leave\n"; + print_string " %who : to print runtime environment\n"; + print_string " %info : to print elaboration environment\n"; + print_string ((make_line '-' 80) ^ "\n\n"); + flush stdout; + + repl () +;; + + +main () +;; \ No newline at end of file

===================================== tests/full_debug.ml ===================================== --- a/tests/full_debug.ml +++ b/tests/full_debug.ml @@ -41,6 +41,7 @@ open Lparse open Myers open Eval open Util +open Lexp

(* pexp and lexp can be done together, one by one *) let pexp_lexp_one node ctx = @@ -48,6 +49,8 @@ let pexp_lexp_one node ctx = lexp_parse pxp ctx ;;

+let dloc = dummy_location;; + let pexp_lexp_all nodes ctx =

let rec loop nodes ctx acc = @@ -58,6 +61,25 @@ let pexp_lexp_all nodes ctx = (loop tl new_ctx (lxp::acc)) in (loop nodes ctx []) ;; + +let dummy_decl = Imm(String(dloc, "Dummy"));; + +let add_rte_def name ctx = + (add_rte_variable (Some name) dummy_decl ctx);; + + +let eval_until_nth xpr n rctx = + + let rec loop xpr nb rctx = + match xpr, nb with + | [], _ -> rctx + | _, nb when nb = n -> rctx + | hd::tl, _ -> + let c, rctx = eval hd rctx in + print_eval_result nb c; + loop tl (nb + 1) rctx in + loop xpr 0 rctx +;;

let main () =

@@ -96,6 +118,11 @@ let main () =

(* 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 ctx = add_def "_=_" ctx in + let lexps, new_ctx = lexp_parse_all pexps ctx in

(* Printing *)(* @@ -105,14 +132,17 @@ let main () = print_title "Pexp"; debug_pexp_print_all pexps; print_title "Lexp"; debug_lexp_print_all lexps;

+ print_string "\n\n"; + lexp_context_print new_ctx; + (* Eval Each Expression *) print_title "Eval Print";

(* Eval One *) - let rctx = make_runtime_ctx in - let c, rctx = eval (List.hd lexps) rctx in - print_eval_result c - + let rctx = make_runtime_ctx in + let rctx = eval_until_nth lexps 500 rctx in + print_string "\n\n"; + print_rte_ctx rctx; end ;;

View it on GitLab: https://gitlab.com/monnier/typer/compare/02f84cd7fba45500f403b339740adf92778...