Setepenre pushed to branch master at Stefan / Typer
Commits: 6b432d51 by Pierre Delaunay at 2016-03-09T20:37:20-05:00 correct declaration handling
- - - - - 772d8502 by Pierre Delaunay at 2016-03-09T22:31:08-05:00 fix nested lambda offset
- - - - -
16 changed files:
- doc/Compiler Structure.md - samples/case.typer - samples/functions.typer - samples/let.typer - samples/lexp_test.typer - src/eval.ml - src/fmt.ml - src/lexp.ml - src/lparse.ml - src/pexp.ml - tests/REPL.ml - − tests/debruijn_test.ml - tests/debug.ml - tests/full_debug.ml - + tests/let_test.ml - tests/utest_main.ml
Changes:
===================================== doc/Compiler Structure.md ===================================== --- a/doc/Compiler Structure.md +++ b/doc/Compiler Structure.md @@ -1,5 +1,3 @@ -Stream.of_string - Typer Compiler Structure ========================
@@ -8,54 +6,79 @@ Read tests/full_debug.ml for ocaml usage
* in_channel -> PreLexer: PreToken
- Skips Blocks and identifies Strings - - Blocks : {this is a block} - String : "this is a string" - PreToken: a pretoken is everything else +Skips Blocks and identifies Strings
- Function: - prelex_file file - - TODO: - prelex_str "my code" - + Blocks : {this is a block} + String : "this is a string" + PreToken: a pretoken is everything else + +Code: "a => 3;" + Pretoken: ['a', '=>', '3;'] + +Functions: + prelex_file file + prelex_string str + * PreToken -> Lexer: Sexp
- Process PreToken. Cut them in smaller pieces according to [stt : token_env] - For example: +Process PreToken. Cut them in smaller pieces according to [stt : token_env] +For example: + + Code: "a => 3;" + Lexer => ['a', '=>', '3', ';']
- Code: "a => 3;" - - Pretoken: ['a', '=>', '3;'] - - Lexer ['a', '=>', '3;'] => ['a', '=>', '3', ';'] - - Here ';' is in stt which makes the '3;' pretoken to explode in two. +Here ';' is in stt which makes the '3;' pretoken to explode in two. + +Functions: + lex stt pretoken + lex_string str
- Function: - lex stt pretoken +* Sexp -> sexp_parse: Node Sexp
-* Sexp -> sexp_parse: Sexp +Group Sexp into Nodes according to the specified grammar. +Create the program tree. + + Code: "a => 3;" + sexp_parse => Node('_=>_', ['a', '3'])
- Group Sexp into Nodes according to the specified grammar. - Create the program tree. +Functions: + sexp_parse sexp + node_parse_string str + +* Sexp -> Pexp: ~ Check grammar
+Identify nodes and transform them into language primitives + Code: "a => 3;" - - Pretoken: ['a', '=>', '3;'] + Pexp: PArrow(kind='=>', a, 3) + +Functions: + pexp_parse sexp % For evaluable expression + pexp_p_decls % For top level declaration + pexp_p_toplevel % Parses using the appropriate parsing function
- Lexer ['a', '=>', '3;'] => ['a', '=>', '3', ';'] (Sexp) +* Pexp -> Lexp: ~ Check scopes/ declaration + +Replace variable name by their (reverse) index in the environment. +Lexps are very close to pexps + + Code: "a => 3;" + Lexp: Arrow(kind='=>', a, 3) + +Functions: + lexp_p_toplevel + lexp_parse + lexp_p_decls + lexp_parse_string
- sexp_parse ['a', '=>', '3', ';'] - => Node('_=>_', ['a', '3']) - - Function: - sexp_parse sexp - -* Sexp -> Lexp +* Lexp -> Value: ~ Evaluation + +Functions: + eval % Evals expression do not modify runtime + eval_decls % Evals declaration modify runtime env + eval_toplevel % uses the appropriate eval function + eval_string % uses eval_toplevel
- Replace variable name by their (reverse) index in the environment.
===================================== samples/case.typer ===================================== --- a/samples/case.typer +++ b/samples/case.typer @@ -2,6 +2,13 @@ % 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);
@@ -24,14 +31,13 @@ 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)); + | (succ y) => (1 + (tonum y)) + | _ => 0;
(tonum x);
===================================== samples/functions.typer ===================================== --- a/samples/functions.typer +++ b/samples/functions.typer @@ -3,12 +3,12 @@ % -------------------------------------------
% define sqrt -sqrt = lambda (x : Nat) -> x * x; +sqr = lambda (x : Nat) -> x * x;
-(sqrt 2); +(sqr 2);
% define cube -cube = lambda (x : Nat) -> x * (sqrt x); +cube = lambda (x : Nat) -> x * (sqr x);
(cube 3);
===================================== samples/let.typer ===================================== --- a/samples/let.typer +++ b/samples/let.typer @@ -20,4 +20,16 @@ let a = 3; g = 1; e = 1; f = 3; in % 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/lexp_test.typer ===================================== --- a/samples/lexp_test.typer +++ b/samples/lexp_test.typer @@ -1,15 +1,18 @@
-% Constructor -% ------------------------------------------- +% x : Nat; +x = 4;
+x + x + x; % 12 +x * x * x; % 64
+sqr = lambda x -> x * x; +% cube = lambda x -> x * x * x;
-% ------------------------------------------- -% Cases -% ------------------------------------------- +(sqr x); % 16 +%(cube x); + +cube = lambda x -> x * (sqr x); +(cube x); % 64
-case x - | zero => y - | succ x => succ (plus x y);
===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -36,39 +36,43 @@ open Lparse open Myers open Sexp 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; + 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) in + let n = (length l) - 1 in
- 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 (make_title " ENVIRONMENT "); + make_rheader [(None, "INDEX"); (None, "VARIABLE NAME"); (None, "VALUE")]; + print_string (make_sep '-');
- 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 + for i = 0 to n do print_string " | "; - ralign_print_int i 5; + ralign_print_int (n - i) 5; print_string " | "; - print_fun (nth i l); + print_fun (nth (n - i) l); done; - print_string sep; + print_string (make_sep '='); ;;
let get_function_name fname = @@ -79,8 +83,8 @@ let get_function_name fname =
let get_int lxp = match lxp with - | Imm(Integer(_, l)) -> l - | _ -> lexp_print lxp; -1 + | Imm(Integer(_, l)) -> l + | _ -> lexp_print (Ltexp(lxp)); -40 ;;
(* Runtime Environ *) @@ -96,12 +100,34 @@ 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 g; print_string "\n") + lexp_print (Ltexp(g)); print_string "\n") ;;
-(* _evaluation reduce an expression x to an Lexp.Imm *) -let rec _eval lxp ctx: (lexp * runtime_env) = - + +let nfirst_rte_var n ctx = + let rec loop i acc = + if i < n then + loop (i + 1) ((get_rte_variable i ctx)::acc) + else + List.rev acc in + 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) + +(* _eval is an internal definition you should use eval or eval_toplevel *) +and _eval lxp ctx i: (lexp * runtime_env) = + add_call lxp i; match lxp with (* This is already a leaf *) | Imm(v) -> lxp, ctx @@ -113,59 +139,54 @@ let rec _eval lxp ctx: (lexp * runtime_env) = with Not_found -> print_string ("Variable: " ^ name ^ " was not found | "); - print_int idx; print_string "\n"; + print_int idx; print_string "\n"; flush stdout; raise Not_found end
(* this works for non recursive let *) | Let(_, decls, inst) -> begin (* First we _evaluate all declaration then we eval the instruction *)
- let nctx = build_ctx decls ctx in + let nctx = build_ctx decls ctx i in
- (* - print_rte_ctx ctx; - print_rte_ctx nctx; *) - - let value, nctx = _eval inst nctx in + let value, nctx = _eval inst nctx (i + 1) in (* return old context as we exit let's scope*) value, ctx end
(* Function call *) | Call (lname, args) -> ( (* Try to extract name *) + let n = List.length args in 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 - (* Hardcoded functions *) + + (* + is read as a nested binary operator *) | Var((_, name), _) when name = "_+_" -> - let nctx = build_arg_list args ctx in + let nctx = build_arg_list args ctx i in + let l = get_int (get_rte_variable 0 nctx) in - let r = get_int (get_rte_variable 1 nctx) in + let r = get_int (get_rte_variable 1 nctx) in Imm(Integer(dloc, l + r)), ctx
+ (* _*_ is reas as a single function with x args *) | 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 + let nctx = build_arg_list args ctx i in + + let vint = (nfirst_rte_var n nctx) in + 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
(* This is a named function call *) (* TODO: handle partial application *) - | Var((_, _), idx) when idx >= 0 -> + | Var((_, name), idx) -> + (* 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 + 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
@@ -175,6 +196,7 @@ let rec _eval lxp ctx: (lexp * runtime_env) =
| 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
@@ -191,7 +213,7 @@ let rec _eval lxp ctx: (lexp * runtime_env) =
let body, nctx = build_body body 1 nctx in
- let e, nctx = _eval body nctx in + let e, nctx = _eval body nctx (i + 1) in e, ctx end
(* Inductive is a type declaration. We have nothing to eval *) @@ -204,7 +226,7 @@ let rec _eval lxp ctx: (lexp * runtime_env) = | Case (loc, target, _, pat, dflt) -> begin
(* Eval target *) - let v, nctx = _eval target ctx in + let v, nctx = _eval target ctx (i + 1) in
(* V must be a constructor Call *) let ctor_name, args = match v with @@ -222,14 +244,14 @@ let rec _eval lxp ctx: (lexp * runtime_env) = Not_found -> _eval_error loc "Constructor does not exist" end *)
- | _ -> lexp_print target; + | _ -> lexp_print (Ltexp(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 + | Some lxp -> _eval lxp ctx (i + 1) in
let ctor_n = List.length args in
@@ -259,60 +281,132 @@ let rec _eval lxp ctx: (lexp * runtime_env) =
nctx pat_args args in
- let r, nctx = _eval exp nctx in + let r, nctx = _eval exp nctx (i + 1) 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 = +and build_arg_list args ctx i = (* _eval every args *) - let arg_val = List.map (fun (k, e) -> let (v, c) = _eval e ctx in v) args in + let arg_val = List.map ( + fun (k, e) -> + let (v, c) = _eval e ctx (i + 1) in v) + args in + (* Add args inside context *) List.fold_left (fun c v -> add_rte_variable None v c) ctx arg_val
-and build_ctx decls ctx = +and build_ctx decls ctx i = match decls with | [] -> ctx | hd::tl -> let (v, exp, tp) = hd in - let (value, nctx) = _eval exp ctx in + let (value, nctx) = _eval exp ctx (i + 1) in let nctx = add_rte_variable None value nctx in - build_ctx tl nctx -;; - -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 = + build_ctx tl nctx (i + 1) + +and eval_decl ((l, n), lxp, ltp) ctx = + add_rte_variable (Some n) lxp ctx + +and print_eval_result i tlxp = + match tlxp with + | Void -> () + | Val(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 e; 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 +;; + +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 () = + print_string (make_title " CALL TRACE "); + + let n = List.length !global_trace in + print_string " size = "; print_int n; print_string "\n"; + print_string (make_sep '-'); + + let racc = List.rev !global_trace in + print_first 20 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"); + + print_string (make_sep '='); ;;
+let eval lxp ctx = + try + let r, c = eval_toplevel lxp ctx in + (r, c) + with e -> ( + print_rte_ctx ctx; + print_call_trace (); + raise e) +;; + + + let evalprint lxp ctx = - let v, ctx = (eval lxp ctx) in + 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) +;; + +(* Eval a string given a context *) 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 + let lxps, lxp_ctx = lexp_parse_string str tenv grm limit lxp_ctx in + (eval_all lxps rctx), lxp_ctx ;;
-*) +(* 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 +;;
===================================== src/fmt.ml ===================================== --- a/src/fmt.ml +++ b/src/fmt.ml @@ -76,3 +76,32 @@ let lalign_print_string = let lalign_print_int = lalign_generic str_size_int print_string print_int cut_int;;
+(* Table Printing helper *) +let make_title title = + let title_n = String.length title in + let p = title_n mod 2 in + let sep_n = (80 - title_n - 4) / 2 in + let lsep = (make_line '=' sep_n) in + let rsep = (make_line '=' (sep_n + p)) in + (" " ^ lsep ^ title ^ rsep ^ "\n") +;; + +let make_rheader (head: (((char* int) option * string) list)) = + print_string " | "; + + List.iter (fun (o, name) -> + let _ = match o with + | Some ('r', size) -> ralign_print_string name size + | Some ('r', size) -> lalign_print_string name size + | _ -> print_string name in + print_string " | ") + head; + + print_string "\n" +;; + +let make_sep c = " " ^ (make_line c 76) ^ "\n";; + + + +
===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -276,7 +276,21 @@ let rec lexp_location e = | Case (l,_,_,_,_) -> l (* | Susp (_, e) -> lexp_location e * | Metavar ((l,_),_,_) -> l *) - + + +let lexp_to_string e = + match e with + | Imm _ -> "Imm" + | Var _ -> "Var" + | Let _ -> "Let" + | Arrow _ -> "Arrow" + | Lambda _ -> "Lambda" + | Call _ -> "Call" + | Inductive _ -> "Inductive" + | Cons _ -> "Cons" + | Case _ -> "Case" +;; + let builtin_reduce b args arg = match b,args,arg with | IAdd, [(_,Imm (Integer (_, i1)))], (Imm (Integer (_, i2)))
===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -61,20 +61,24 @@ let lexp_fatal loc msg = raise (internal_error msg) ;;
-(* Print back in CET (Close Enough Typer) easier to read *) + (* pretty ? * indent level * print_type? *) type print_context = (bool * int * bool)
(* Vdef is exactly similar to Pvar but need to modify our ctx *) -let pvar_to_vdef p = - p +let pvar_to_vdef p = p;; + +type ltop = + | Ltexp of lexp + | Ltdecl of vdef * lexp * ltype ;;
-(* -let _ab = senv_add_var;; -let senv_add_var = - _ab name loc ctx -;;*) + +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 *)
@@ -97,7 +101,22 @@ let senv_add_var = * *)
-let rec lexp_parse (p: pexp) (ctx: lexp_context): (lexp * lexp_context) = +(* 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) = (* So I don't have to extract it *) let tloc = pexp_location p in match p with @@ -112,10 +131,9 @@ let rec lexp_parse (p: pexp) (ctx: lexp_context): (lexp * lexp_context) = (make_var name idx loc), ctx;
with Not_found -> - (* Add Variable *) - let ctx = senv_add_var name loc ctx in - let ctx = env_add_var_info (0, (loc, name), dlxp, dlxp) ctx in - (make_var name 0 loc), ctx; end + (lexp_error loc ("The Variable: " ^ name ^ " was not declared"); + (* Error recovery. The -1 index will raise an error later on *) + (make_var name (-1) loc), ctx) end
(* Let, Variable declaration + local scope *) | Plet(loc, decls, body) -> @@ -159,8 +177,7 @@ let rec lexp_parse (p: pexp) (ctx: lexp_context): (lexp * lexp_context) = let lbody, ctx = lexp_parse body nctx in Lambda(kind, var, UnknownType(tloc), lbody), ctx
- | Pcall (fname, _args) -> - lexp_call fname _args ctx + | Pcall (fname, _args) -> lexp_call fname _args ctx
(* Pinductive *) | Pinductive (label, [], ctors) -> @@ -184,7 +201,7 @@ let rec 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
@@ -211,11 +228,11 @@ let rec lexp_parse (p: pexp) (ctx: lexp_context): (lexp * lexp_context) =
| _ -> UnknownType(tloc), ctx - + (* Identify Call Type and return processed call *) -and lexp_call fname _args ctx = +and lexp_call (fname: pexp) (_args: sexp list) ctx = (* Process Arguments *) - let pargs = pexp_parse_all _args in + let pargs = List.map pexp_parse _args in
(* Call to named function which must have been defined earlier * * i.e they must be in the context *) @@ -225,34 +242,8 @@ and lexp_call fname _args ctx = | 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 largs, fctx = lexp_p_all pargs ctx in let new_args = List.map (fun g -> (Aexplicit, g)) largs in
try @@ -271,7 +262,7 @@ and lexp_call fname _args ctx =
(* Call to a nameless function *) with Not_found -> - let largs, fctx = lexp_parse_all pargs ctx in + let largs, fctx = lexp_p_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 *) @@ -281,15 +272,15 @@ and lexp_call fname _args ctx = (* Read a pattern and create the equivalent representation *) 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, []), ctx
- | Ppatvar (loc, name) -> (* Create a variable containing target *) + | 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 @@ -353,7 +344,43 @@ 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 =
@@ -428,7 +455,16 @@ and lexp_parse_let decls ctx = let acc, ctx = process_var_info decls nctx [] in acc, ctx
-and lexp_parse_all (p: pexp list) (ctx: lexp_context): +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): (lexp list * lexp_context) = let rec loop (plst: pexp list) ctx (acc: lexp list) = match plst with @@ -461,7 +497,7 @@ and lexp_p_infer (p : pexp) (env : lexp_context) : lexp * ltype = let lxp, nctx = lexp_parse p env in lxp, UnknownType(dummy_location)
-and lexp_p_check (env : lexp_context) (p : pexp) (t : ltype) : lexp = +and lexp_p_check (p : pexp) (t : ltype) (env : lexp_context): lexp = match p with | _ -> let (e, inferred_t) = lexp_p_infer p env in @@ -470,6 +506,7 @@ and lexp_p_check (env : lexp_context) (p : pexp) (t : ltype) : 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 = let slexp_print = lexp_print_adv opt in (* short_lexp_print *) @@ -589,15 +626,16 @@ and lexp_print_decls opt decls = (* Print context *) and lexp_context_print ctx = let ((n, map), env) = ctx in + + print_string (make_title " LEXP CONTEXT ");
- 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"); + make_rheader [ + (Some ('r', 10), "NAME"); + (Some ('r', 7), "INDEX"); + (Some ('r', 10), "NAME"); + (Some ('r', 20), "VALUE:TYPE")]; + + print_string (make_sep '-');
StringMap.iter (fun key idx -> (* Print senv info *) @@ -620,7 +658,7 @@ and lexp_context_print ctx =
map;
- print_string (" " ^ (make_line '=' 54) ^ "\n"); + print_string (make_sep '=');
(* Only print var info *) and lexp_print_var_info ctx = @@ -638,18 +676,26 @@ and lexp_print_var_info ctx = done; ;;
-let lexp_print = lexp_print_adv (false, 0, true) - +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 = +let lexp_parse_string (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 ctx = make_lexp_context in let pxps = pexp_parse_all sxps in 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
===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -61,6 +61,15 @@ type pexp = * (symbol * (arg_kind * pvar option * pexp) list) list | 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 @@ -81,11 +90,29 @@ let rec pexp_pat_location e = match e with | Ppatany l -> l | Ppatvar (l,_) -> l | 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". *) - -let rec pexp_parse (s : sexp) : pexp = +and 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. *) @@ -350,9 +377,19 @@ 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; +;; + + (* Parse All Pexp as a list *) let pexp_parse_all (nodes: sexp list) = - List.map pexp_parse nodes + List.map pexp_p_toplevel nodes ;;
let pexp_parse_string (str: string) tenv grm limit =
===================================== tests/REPL.ml ===================================== --- a/tests/REPL.ml +++ b/tests/REPL.ml @@ -23,37 +23,29 @@ let rec read_input i = print_input_line i; flush stdout;
- let rec loop str = + let rec loop str i = + flush stdout; 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 + if s = 0 && n = 0 then read_input (i + 1) else + (if n = 0 then ( + print_string " : "; + print_string (make_line ' ' (i * 4)); + loop str (i + 1)) + 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 + else ( + print_string " . "; + print_string (make_line ' ' (i * 4)); + loop str (i + 1))) in
- loop "" + loop "" 1 ;;
-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 @@ -64,7 +56,6 @@ let rec repl () = (* 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
@@ -76,24 +67,25 @@ let rec repl () = (print_rte_ctx rctx; loop (i + 1) clxp rctx) else if ipt = "%info" then (lexp_context_print clxp; loop (i + 1) clxp rctx) + else if ipt = "%calltrace" then + (print_call_trace (); 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"; + let print_e j v = print_eval_result i v in + List.iteri print_e ret; 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"); + print_string (make_title " TYPER REPL "); + print_string " %quit : leave REPL\n"; + print_string " %who : print runtime environment\n"; + print_string " %info : print elaboration environment\n"; + print_string " %calltrace : print call trace of last call \n"; + print_string (make_sep '='); flush stdout;
repl ()
===================================== tests/debruijn_test.ml deleted ===================================== --- a/tests/debruijn_test.ml +++ /dev/null @@ -1,32 +0,0 @@ -(* TODO make some real test *) -open Debruijn -open Util - -let main () = - (* Tests *) - (* Create a new scope: global scope *) - let loc = dummy_location in - let g0 = make_context in - let g1 = add_variable "a" loc g0 in - let g2 = add_variable "a" loc g1 in - let g3 = add_variable "b" loc g2 in - let g4 = add_variable "c" loc g3 in - let g5 = add_variable "d" loc g4 in - - (* we enter a let or whatever *) - let l0 = add_scope g5 in - let l1 = add_variable "a" loc l0 in - let l2 = add_variable "e" loc l1 in - - (* Testing is done *) - print_string "Inner Context\n"; - print_lexp_context l2; - - (* We exit the scope *) - print_string "Outer Context\n"; - print_lexp_context g5 -;; - - -main () -;; \ No newline at end of file
===================================== tests/debug.ml ===================================== --- a/tests/debug.ml +++ b/tests/debug.ml @@ -114,27 +114,30 @@ let debug_sexp_print_all tokens =
(* Print a Pexp with debug info *) -let debug_pexp_print pexp = +let debug_pexp_print ptop = print_string " "; - let l = pexp_location pexp in + let l = pexp_location_toplevel ptop in let print_info msg loc pex = print_string msg; print_string "["; print_loc loc; print_string "]\t"; - pexp_print pexp in - match pexp with - | Pimm _ -> print_info "Pimm " l pexp - | Pvar (_,_) -> print_info "Pvar " l pexp - | Phastype (_,_,_) -> print_info "Phastype " l pexp - | Pmetavar (_, _) -> print_info "Pmetavar " l pexp - | Plet (_, _, _) -> print_info "Plet " l pexp - | Parrow (_, _, _, _, _) -> print_info "Parrow " l pexp - | Plambda (_,_, _, _) -> print_info "Plambda " l pexp - | Pcall (_, _) -> print_info "Pcall " l pexp - | Pinductive (_, _, _) -> print_info "Pinductive " l pexp - | Pcons (_,_) -> print_info "Pcons " l pexp - | Pcase (_, _, _) -> print_info "Pcase " l pexp - | _ -> print_info "Not Impl " l pexp + pexp_print_toplevel 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) ;;
(* Print a list of pexp *) @@ -147,7 +150,7 @@ let debug_pexp_print_all pexps = ;;
(* Print lexp with debug info *) -let debug_lexp_print lxp = +let debug_lexp_print tlxp = print_string " "; let dloc = dummy_location in let print_info msg loc lex = @@ -155,18 +158,21 @@ let debug_lexp_print lxp = print_loc loc; print_string "]\t"; lexp_print lex in - let tloc = lexp_location lxp in + let tloc = lexp_location_toplevel 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 lxp - | Imm(s) -> print_info "Imm " tloc lxp - | Let(loc, _, _) -> print_info "Let " tloc lxp - | Arrow(_, _, _, loc, _) -> print_info "Arrow " tloc lxp - | Lambda(_, (loc, _), _, _) -> print_info "Lambda " tloc lxp - | Call(_, _) -> print_info "Call " tloc lxp - | Inductive(loc, _, _, _) -> print_info "Inductive " tloc lxp - | UnknownType(loc) -> print_info "UnknownType " tloc lxp - | Case(loc, _, _, _, _) -> print_info "Case " tloc lxp - | Cons (rf, sym) -> print_info "Cons " tloc lxp + | Var((loc, _), _) -> print_info "Var " tloc tlxp + | Imm(s) -> print_info "Imm " tloc tlxp + | Let(loc, _, _) -> print_info "Let " tloc tlxp + | Arrow(_, _, _, loc, _) -> print_info "Arrow " tloc tlxp + | Lambda(_, (loc, _), _, _) -> print_info "Lambda " tloc tlxp + | Call(_, _) -> print_info "Call " tloc tlxp + | Inductive(loc, _, _, _) -> print_info "Inductive " tloc tlxp + | UnknownType(loc) -> print_info "UnknownType " tloc tlxp + | Case(loc, _, _, _, _) -> print_info "Case " tloc tlxp + | Cons (rf, sym) -> print_info "Cons " tloc tlxp | _ -> print_string "Debug Printing Not Implemented"; ;;
===================================== tests/full_debug.ml ===================================== --- a/tests/full_debug.ml +++ b/tests/full_debug.ml @@ -36,11 +36,15 @@ open Lexer open Sexp open Grammar open Pexp +open Util +open Fmt + +let dloc = dummy_location;; + open Debruijn -open Lparse open Myers +open Lparse open Eval -open Util open Lexp
(* pexp and lexp can be done together, one by one *) @@ -49,7 +53,7 @@ let pexp_lexp_one node ctx = lexp_parse pxp ctx ;;
-let dloc = dummy_location;; +
let pexp_lexp_all nodes ctx =
@@ -75,11 +79,11 @@ let eval_until_nth xpr n rctx = | [], _ -> rctx | _, nb when nb = n -> rctx | hd::tl, _ -> - let c, rctx = eval hd rctx in + let c, rctx = eval_toplevel hd rctx in print_eval_result nb c; loop tl (nb + 1) rctx in loop xpr 0 rctx -;; +;;
let main () =
@@ -87,11 +91,6 @@ let main () = let usage = " Usage: \n " ^ Sys.argv.(0) ^ " <file_name> [options] \n\n" in
- let print_title msg = - print_string "\n\t====\n"; - print_string ("\t " ^ msg ^ "\n"); - print_string "\t=======================\n" in - (* Print Usage *) if arg_n == 1 then begin @@ -104,6 +103,7 @@ let main () =
(* Read additional Args if any *)
+ print_string (make_title " ERRORS "); (* get pretokens*) let pretoks = prelex_file filename in
@@ -121,28 +121,34 @@ let main () = (* 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 + let lexps, new_ctx = lexp_parse_all 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_title "Node Sexp"; debug_sexp_print_all nodes; - 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; + 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 "\n"; + print_string (make_title " Lexp "); debug_lexp_print_all lexps; + print_string "\n";
(* Eval Each Expression *) - print_title "Eval Print"; + print_string (make_title " Eval Print ");
(* Eval One *) let rctx = make_runtime_ctx in let rctx = eval_until_nth lexps 500 rctx in print_string "\n\n"; - print_rte_ctx rctx; + print_rte_ctx rctx; + + print_string "\n"; + lexp_context_print new_ctx; + print_string "\n"; + + print_call_trace (); end ;;
===================================== tests/let_test.ml ===================================== --- /dev/null +++ b/tests/let_test.ml @@ -0,0 +1,30 @@ + +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/utest_main.ml ===================================== --- a/tests/utest_main.ml +++ b/tests/utest_main.ml @@ -66,10 +66,7 @@ let main () =
tests_n := !tests_n + 1;
- print_string " " ; - print_int !tests_n; - print_endline (") " ^ (cut_name files.(i))); - print_endline "[RUN ]"; + print_endline ("[RUN ] TEST: " ^ (cut_name files.(i)));
exit_code := Sys.command (folder ^ files.(i) ^ " " ^ root_folder);
View it on GitLab: https://gitlab.com/monnier/typer/compare/c6d73fd58240616b5dd5c60c80b96d586eb...
Afficher les réponses par date
% define sqrt sqr = lambda (x : Nat) -> x * x;
(sqr 2);
Ce n'est pas du code Typer valide: le top-level d'un fichier doit contenir une liste de *déclarations* séparée par des ";".
sqr = lambda (x : Nat) -> x * x;
est une déclaration valide. Mais
(sqr 2);
ne l'est pas. C'est une expression. Il te faudrait qqch du genre:
result = sqr 2;
à la place.
Ce problème se retrouve dans beaucoup de tes fichiers d'exemples.
+let rec eval_toplevel ltop ctx: (value_type * runtime_env) =
"eval_toplevel" ne devrait jamais rien faire d'autre que d'évaluer des déclarations (vu que c'est la seule chose qu'il peut y avoir), donc il ne renvoie jamais de valeur.
Donc tu ne devrais pas avoir besoin de définir le type `value_type' ou `ltop'.
Bien sûr, il faut pouvoir exécuter du code d'une certaine manière. Pour ça, je pensais faire comme en C/Haskell/... et déclarer `main' comme un identificateur spécial qui contient le point d'entrée (i.e. l'exécution du programme se fait en appelant `main').
Stefan