Setepenre pushed to branch master at Stefan / Typer
Commits: 7cfabe06 by Pierre Delaunay at 2016-03-31T00:43:05-04:00 Fix mutually recursive definition lexp parsing
Changes to be committed: * src/lparse.ml: - rollback to old lexp_decls implementation - renamed (lexp_decls) to (lexp_p_decls) * tests/eval_test.ml: minor fixes * src/eval.ml: - new functions (eval_call)/(eval_case) - modified eval_call to support partial application
renamed: src/full_debug.ml -> src/debug_util.ml * GNUmakefile: adapted to renamed files
- - - - -
8 changed files:
- GNUmakefile - doc/Compiler Structure.md - src/REPL.ml - src/debruijn.ml - src/full_debug.ml → src/debug_util.ml - src/eval.ml - src/lparse.ml - tests/eval_test.ml
Changes:
===================================== GNUmakefile ===================================== --- a/GNUmakefile +++ b/GNUmakefile @@ -20,8 +20,8 @@ debug: # ============================ # Build debug utils # ============================ - ocamlbuild src/full_debug.native -I src $(CFLAG) - @mv _build/src/full_debug.native _build/full_debug + ocamlbuild src/debug_util.native -I src $(CFLAG) + @mv _build/src/debug_util.native _build/debug_util
# interactive typer ityper:
===================================== doc/Compiler Structure.md ===================================== --- a/doc/Compiler Structure.md +++ b/doc/Compiler Structure.md @@ -5,48 +5,48 @@ 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
Code: "a => 3;" Pretoken: ['a', '=>', '3;'] - + Functions: prelex_file file prelex_string str - -* PreToken -> Lexer: Sexp - + +* PreToken -> Lexer: Sexp + Process PreToken. Cut them in smaller pieces according to [stt : token_env] For example:
Code: "a => 3;" Lexer => ['a', '=>', '3', ';'] - + Here ';' is in stt which makes the '3;' pretoken to explode in two.
Functions: lex stt pretoken lex_string str - + * Sexp -> sexp_parse: Node Sexp - + Group Sexp into Nodes according to the specified grammar. -Create the program tree. +Create the program tree.
Code: "a => 3;" sexp_parse => Node('_=>_', ['a', '3']) - + Functions: sexp_parse sexp - node_parse_string str - + sexp_parse_str str + * Sexp -> Pexp: ~ Lexical Analysis - + Identify nodes and transform them into language primitives
Code: "a => 3;" @@ -55,8 +55,7 @@ Identify nodes and transform them into language primitives Functions: pexp_parse sexp % For evaluable expression pexp_p_decls % For top level declaration - pexp_p_toplevel % Parses using the appropriate parsing function - + * Pexp -> Lexp: ~ Semantic Analysis
Replace variable name by their (reverse) index in the environment. @@ -66,20 +65,19 @@ Lexps are very close to pexps Lexp: Arrow(kind='=>', a, 3)
Functions: - lexp_p_toplevel lexp_parse lexp_p_decls - lexp_parse_string - + lexp_expr_str + lexp_decl_str + * Lexp -> Value: ~ Evaluation
Functions: - eval % Evals expression do not modify runtime + eval_all % 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 + eval_decl_str + eval_expr_str + +
- - -
===================================== src/REPL.ml ===================================== --- a/src/REPL.ml +++ b/src/REPL.ml @@ -113,7 +113,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 ldecls, lctx = lexp_p_decls pdecls lctx in let lexprs = lexp_parse_all pexprs lctx in (ldecls, lexprs), lctx ;;
===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -136,10 +136,10 @@ let env_lookup_type ctx (v : vref) = t (* Shift (dbi - roft, t) *) else ( let (rof, (_, dname), _, t) = Myers.nth (dbi - sync_offset) info_env in - print_string (" DBI: " ^ dname); + print_string (" DBI: " ^ dname ^ " " ^ rname); print_int (dbi - sync_offset); print_string "\n"; internal_error ("DeBruijn index refers to wrong name. Expected: "" - ^ rname ^ "" got "" ^ dname ^ """) ) + ^ rname ^ "" got "" ^ dname ^ """))
with Not_found -> internal_error "DeBruijn index out of bounds!"
===================================== src/full_debug.ml → src/debug_util.ml ===================================== --- a/src/full_debug.ml +++ b/src/debug_util.ml @@ -150,7 +150,7 @@ let main () = let ctx = default_lctx () in
let lexps, nctx = - try lexp_decls pexps ctx + try lexp_p_decls pexps ctx with e -> ( print_lexp_ctx (!_global_lexp_ctx); print_lexp_trace ();
===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -80,14 +80,18 @@ let print_rte_ctx ctx =
let get_int lxp = match lxp with - | Imm(Integer(_, l)) -> l - | _ -> lexp_print lxp; -40 + | Imm(Integer(_, l)) -> Some l + | _ -> None ;;
+(* Offset is used when we eval declaration one by one *) +(* i.e not everything is present so we need to account for missing decls *) +type decls_offset = int + (* Runtime Environ *) -type runtime_env = ((string option * lexp) myers) * (int * int) +type runtime_env = ((string option * lexp) myers) * (int * int * decls_offset)
-let make_runtime_ctx = (nil, (0, 0));; +let make_runtime_ctx = (nil, (0, 0, 0));;
let add_rte_variable name x ctx = let (l, b) = ctx in @@ -95,7 +99,8 @@ let add_rte_variable name x ctx = (lst, b);;
let get_rte_variable (name: string option) (idx: int) (ctx: runtime_env): lexp = - let (l, _) = ctx in + let (l, (_, _, offset)) = ctx in + let idx = if idx >= offset then idx - offset else idx in let (tn, x) = (nth idx l) in match (tn, name) with | (Some n1, Some n2) -> ( @@ -109,19 +114,20 @@ let get_rte_variable (name: string option) (idx: int) (ctx: runtime_env): lexp = | _ -> x (* can't check variable's name (call args do not have names) *) ;;
-let get_rte_size (ctx: runtime_env): int = let (l, b) = ctx in length l;; +let get_rte_size (ctx: runtime_env): int = let (l, _) = ctx in length l;;
-(* This function is used when we enter a new scope *) +(* This function is used when we enter a new scope *) +(* it allow us to removed temporary variables when we enter temporary scope *) let local_ctx ctx = - let (l, _) = ctx in + let (l, (_, _, off)) = ctx in let osize = length l in - (l, (osize, 0)) + (l, (osize, 0, off)) ;;
let select_n ctx n = let (l, a) = ctx in let r = ref nil in - let s = (length l) - 1in + let s = (length l) - 1 in
for i = 0 to n - 1 do r := (cons (nth (s - i) l) (!r)); @@ -130,7 +136,7 @@ let select_n ctx n = ((!r), a)
let temp_ctx ctx = - let (l, (osize, _)) = ctx in + let (l, (osize, _, _)) = ctx in let tsize = length l in (* Check if temporary variables are present *) if tsize != osize then @@ -150,8 +156,9 @@ let nfirst_rte_var n ctx = ;;
let _global_eval_trace = ref [] -let _global_eval_ctx = ref (nil, (0, 0)) +let _global_eval_ctx = ref (nil, (0, 0, 0)) let _eval_max_recursion_depth = ref 255 +let reset_eval_trace () = _global_eval_trace := []
(* currently, we don't do much *) type value_type = lexp @@ -160,6 +167,7 @@ type value_type = lexp * 'i' is the recursion depth used to print the call trace *) let rec _eval lxp ctx i: (value_type) = let tloc = lexp_location lxp in + let str_idx idx = "[" ^ (string_of_int idx) ^ "]" in
(if i > (!_eval_max_recursion_depth) then raise (internal_error "Recursion Depth exceeded")); @@ -168,30 +176,37 @@ let rec _eval lxp ctx i: (value_type) = _global_eval_trace := (i, tloc, lxp)::!_global_eval_trace;
match lxp with - (* This is already a leaf *) + (* Leafs *) + (* ---------------- *) | Imm(v) -> lxp + | Inductive (_, _, _, _) as e -> e + | Cons (_, _) as e -> e + + (* Lambda's body is evaluated when called *) + | Lambda _ -> lxp
(* Return a value stored in the environ *) - | Var((loc, name), idx) as e -> begin + | Var((loc, name), idx) as e ->( (* find variable binding i.e we do not want a another variable *) + (* (-3) represent a variable which should not be replaced *) let rec var_crawling expr k = (if k > 255 then( lexp_print expr; print_string "\n"; flush stdout; - raise (internal_error "Variable lookup failed"))); + eval_error tloc "Variable lookup failed")); match expr with + | Var(_, j) when j = (-3)-> e | Var((_, name2), j) -> let p = (get_rte_variable (Some name2) j ctx) in var_crawling p (k + 1) | _ -> expr in
- try - (var_crawling e 0) - with - Not_found -> - print_string ("Variable: " ^ name ^ " was not found | "); - print_int idx; print_string "\n"; flush stdout; - raise Not_found end + try (var_crawling e 0) + with Not_found -> + eval_error tloc ("Variable: " ^ + name ^ (str_idx idx) ^ " was not found "))
+ (* Nodes *) + (* ---------------- *) (* this works for non recursive let *) | Let(_, decls, inst) -> (* First we _evaluate all declaration then we eval the instruction *) @@ -203,189 +218,210 @@ let rec _eval lxp ctx i: (value_type) = let nctx = build_arg_list args ctx i in *)
(* Function call *) - | Call (lname, args) -> ( - (* create a clean environment *) - let clean_ctx = temp_ctx ctx in - - let n = List.length args in - match lname with - (* Hardcoded functions *) - (* FIXME: These should not be hardcoded here, but should be - * stuffed into the "initial environment", i.e. the value of - * `ctx` used at top-level. *) - - (* + is read as a nested binary operator *) - | Var((_, name), _) when name = "_+_" -> - let nctx = build_arg_list args ctx i in - - let l = get_int (get_rte_variable (None) 0 nctx) in - let r = get_int (get_rte_variable (None) 1 nctx) in - Imm(Integer(dloc, l + r)) - - (* _*_ is read as a single function with x args *) - | Var((_, name), _) when name = "_*_" -> - 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)) - - (* This is a named function call *) - | Var((_, name), idx) -> ( - (* get function's body from current context *) - let body = get_rte_variable (Some name) idx ctx in - - (* _eval every args using current context *) - let arg_val = - List.map (fun (k, e) -> _eval e ctx (i + 1)) args in - - match body with - (* If 'cons', build it back with evaluated args *) - | Cons _ -> - Call(lname, (List.map (fun g -> - (Aexplicit, g)) arg_val)) - | _ -> - (* Add args inside our clean context *) - let clean_ctx = - List.fold_left (fun c v -> add_rte_variable None v c) - clean_ctx arg_val in - - _eval body clean_ctx (i + 1)) - - (* TODO Everything else *) - (* Which includes a call to a lambda *) - | _ -> Imm(String(dloc, "Funct Not Implemented"))) - - (* Lambdas have one single mandatory argument *) - (* Nested lambda are collapsed then executed *) - (* I am thinking about building a 'get_free_variable' to be able to *) - (* handle partial application i.e build a new lambda if Partial App *) - | Lambda(_, vr, _, body) -> begin - (* let (loc, name) = vr in *) - - (* This was redundant since we already pushed args - * when processing the call expression *) - (* Get first arg * ) - let value = (get_rte_variable (Some name) 0 ctx) in - let nctx = add_rte_variable (Some name) value ctx in - - (* Collapse nested lambdas. Returns body *) - let rec collapse bd idx nctx = - match bd with - | Lambda(_, vr, _, body) -> - let (loc, name) = vr in - (* Get Variable from call context *) - let value = (get_rte_variable (Some name) idx ctx) in - (* Build lambda context *) - let nctx = add_rte_variable (Some name) value nctx in - (collapse body (idx + 1) nctx) - | _ -> bd, nctx in - - let body, nctx = collapse body 1 nctx in*) - _eval body ctx (i + 1) end - - (* Inductive is a type declaration. We have nothing to eval *) - | Inductive (_, _, _, _) as e -> e - - (* inductive-cons build a type too? *) - | Cons (_, _) as e -> e + | Call (lname, args) -> eval_call ctx i lname args
(* Case *) - | Case (loc, target, _, pat, dflt) -> begin - - (* Eval target *) - let v = _eval target ctx (i + 1) in - - let (_, (osize, _)) = ctx in - let csize = get_rte_size ctx in - let offset = csize - osize in - - (* V must be a constructor Call *) - let ctor_name, args = match v with - | Call(lname, args) -> (match lname with - (* FIXME we should check that ctor_name is an existing - * constructor with the correct number of args *) - | Var((_, ctor_name), _) -> ctor_name, args - | _ -> eval_error loc "Target is not a Constructor" ) - - | Cons(((_, vname), idx), (_, cname)) -> begin - (* retrieve type definition *) - let info = get_rte_variable (Some vname) (idx + offset) ctx in - let ctor_def = match info with - | Inductive(_, _, _, c) -> c - | _ -> eval_error loc "Not an Inductive Type" in - - try match SMap.find cname ctor_def with - | [] -> cname, [] - | carg -> - let ctor_n = List.length carg in - eval_error loc ("Constructor not applied. " ^ - "Constructor name: "" ^ cname ^ - "": " ^ (string_of_int ctor_n) ^ - " argument(s) expected") - with - Not_found -> - 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 - - (* Check if a default is present *) - let run_default df = - match df with - | None -> Imm(String(loc, "Match Failure")) - | Some lxp -> _eval lxp ctx (i + 1) 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 - - (* if the argument is a reference to a variable its index need to be - * shifted *) - let arg_shift xp offset = - match xp with - | Var(a, idx) -> Var(a, idx + offset) - | _ -> xp in - - (* Search for the working pattern *) - let sol = SMap.filter is_true pat in - if SMap.is_empty sol then - run_default dflt - else - (* Get working pattern *) - let key, (_, pat_args, exp) = SMap.min_binding sol in - - (* count the number of declared variables *) - let case_offset = List.fold_left (fun i g -> - match g with None -> i | _ -> i + 1) - 0 pat_args in - - let toffset = case_offset + offset in - - (* build context *) - let nctx = List.fold_left2 (fun nctx pat arg -> - match pat with - | None -> nctx - | Some (_, (_, name)) -> - let (_, xp) = arg in - let xp = (arg_shift xp toffset) in - add_rte_variable (Some name) xp nctx) - - ctx pat_args args in - (* eval body *) - _eval exp nctx (i + 1) end + | Case (loc, target, _, pat, dflt) -> (eval_case ctx i loc target pat dflt)
| _ -> Imm(String(dloc, "eval Not Implemented"))
+and eval_call ctx i lname args = + (* create a clean environment *) + let tloc = lexp_location lname in + let clean_ctx = temp_ctx ctx in + let args_n = List.length args in + + (* To handle partial call we need to consume args and *) + (* lambdas together an return the remaining lambda *) + (* Call by name: replace variables then eval *) + let rec consume_args (ctx: runtime_env) (lxp: lexp) args (k: int): value_type = + match lxp, args with + (* Base Case*) + | Lambda(_, (_, name), _, body), arg::tl -> + let ctx = add_rte_variable (Some name) arg ctx in + consume_args ctx body tl (k + 1) + + (* Partial Application *) + (* In truth we don't really stop here. We push missing args *) + (* as such that missing args will be replaced by themselves *) + (* when the full eval will be called *) + | Lambda(kind, (loc, name), l, body), [] -> + let ctx = add_rte_variable (Some name) (Var((loc, name), -3)) ctx in + let b = consume_args ctx body [] (k + 1) in + Lambda(kind, (loc, name), l, b) + + (* Full Eval *) + | _, [] -> + _eval lxp ctx (k + i) + + (* Too many args *) + | _, _ -> + eval_error tloc ("Wrong Number of arguments. " ^ + " Got:" ^ (string_of_int args_n) ^ " arg(s) " ^ + " Expected: " ^ (string_of_int k) ^ " arg(s) ") in + + match lname with + (* Hardcoded functions *) + (* FIXME: These should not be hardcoded here, but should be + * stuffed into the "initial environment", i.e. the value of + * `ctx` used at top-level. *) + + (* + is read as a nested binary operator *) + | Var((_, name), _) when name = "_+_" -> + let nctx = build_arg_list args ctx i in + + let llxp = (get_rte_variable (None) 0 nctx) in + let rlxp = (get_rte_variable (None) 1 nctx) in + let l = get_int llxp in + let r = get_int rlxp in + + (* if l and r are not ints this is a partial eval *) + if l = None || r = None then + Call(lname, [(Aexplicit, llxp); (Aexplicit, rlxp)]) + else ( + let v, w = match l, r with + | Some v, Some w -> v, w + | _, _ -> (-40), (-40) in + Imm(Integer(dloc, v + w))) + + (* _*_ is read as a single function with x args *) + | Var((_, name), _) when name = "_*_" -> + let nctx = build_arg_list args ctx i in + + let vint = (nfirst_rte_var args_n nctx) in + let varg = List.map (fun g -> get_int g) vint in + + let (partial, prod) = List.fold_left (fun a g -> + let (partial, prod) = a in + match g with + | Some v -> (partial, v * prod) + | None -> (true, 0)) + (false, 1) varg in + + if partial then + let args = List.map (fun g -> (Aexplicit, g)) vint in + Call(lname, args) + else + Imm(Integer(dloc, prod)) + + (* This is a named function call *) + | Var((_, name), idx) -> ( + (* get function's body from current context *) + let body = get_rte_variable (Some name) idx ctx in + + (* _eval every args using current context *) + let arg_val = List.map (fun (k, e) -> _eval e ctx (i + 1)) args in + let arg_val2 = List.map (fun (k, e) -> e) args in + + match body with + (* If 'cons', build it back with evaluated args *) + | Cons _ -> + Call(lname, (List.map (fun g -> (Aexplicit, g)) arg_val)) + + | Lambda _ -> + (consume_args clean_ctx body arg_val 0) + + | _ -> + (* Add args inside our clean context *) + let nctx = List.fold_left (fun c v -> add_rte_variable None v c) + clean_ctx arg_val in + _eval body nctx (i + 1)) + + (* TODO Everything else *) + (* Which includes a call to a lambda *) + | _ -> Imm(String(dloc, "Funct Not Implemented")) + +and eval_case ctx i loc target pat dflt = + (* Eval target *) + let v = _eval target ctx (i + 1) in + + let (_, (osize, _, _)) = ctx in + let csize = get_rte_size ctx in + let offset = csize - osize in + + (* V must be a constructor Call *) + let ctor_name, args = match v with + | Call(lname, args) -> (match lname with + (* FIXME we should check that ctor_name is an existing + * constructor with the correct number of args *) + | Var((_, ctor_name), _) -> ctor_name, args + | _ -> eval_error loc "Target is not a Constructor" ) + + | Cons(((_, vname), idx), (_, cname)) -> begin + (* retrieve type definition *) + let info = get_rte_variable (Some vname) (idx + offset) ctx in + let ctor_def = match info with + | Inductive(_, _, _, c) -> c + | _ -> eval_error loc "Not an Inductive Type" in + + try match SMap.find cname ctor_def with + | [] -> cname, [] + | carg -> + let ctor_n = List.length carg in + eval_error loc ("Constructor not applied. " ^ + "Constructor name: "" ^ cname ^ + "": " ^ (string_of_int ctor_n) ^ + " argument(s) expected") + with + Not_found -> + 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 + + (* Check if a default is present *) + let run_default df = + match df with + | None -> Imm(String(loc, "Match Failure")) + | Some lxp -> _eval lxp ctx (i + 1) 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 + + (* if the argument is a reference to a variable its index need to be + * shifted *) + let arg_shift xp offset = + match xp with + | Var(a, idx) -> Var(a, idx + offset) + | _ -> xp in + + (* Search for the working pattern *) + let sol = SMap.filter is_true pat in + if SMap.is_empty sol then + run_default dflt + else + (* Get working pattern *) + let key, (_, pat_args, exp) = SMap.min_binding sol in + + (* count the number of declared variables *) + let case_offset = List.fold_left (fun i g -> + match g with None -> i | _ -> i + 1) + 0 pat_args in + + let toffset = case_offset + offset in + + (* build context *) + let nctx = List.fold_left2 (fun nctx pat arg -> + match pat with + | None -> nctx + | Some (_, (_, name)) -> + let (_, xp) = arg in + let xp = (arg_shift xp toffset) in + add_rte_variable (Some name) xp nctx) + + ctx pat_args args in + (* eval body *) + _eval exp nctx (i + 1) + and build_arg_list args ctx i = (* _eval every args *) let arg_val = List.map (fun (k, e) -> _eval e ctx (i + 1)) args in @@ -401,21 +437,35 @@ and build_ctx decls ctx i =
List.fold_left f ctx decls
-and eval_decl ((l, n), lxp, ltp) ctx = - add_rte_variable (Some n) lxp ctx - -and eval_decls (decls: ((vdef * lexp * ltype) list)) - (ctx: runtime_env): runtime_env = - let rec loop decls ctx = - match decls with - | [] -> ctx - | hd::tl -> - let ((_, n), lxp, ltp) = hd in - let nctx = add_rte_variable (Some n) lxp ctx in - loop tl nctx in - - let nctx = loop decls ctx in - (local_ctx nctx) +and eval_decls decls ctx = _eval_decls decls ctx 1 +and _eval_decls (decls: ((vdef * lexp * ltype) list)) + (ctx: runtime_env) i: runtime_env = + + let set_offset ctx off = + let (l, (a, b, c)) = ctx in + (l , (a, b, off)) in + + let n = (List.length decls) - 1 in + + try + + let dctx, _ = List.fold_left (fun (ctx, k) g -> + let ((_, name), lxp, _) = g in + let lxp = _eval lxp ctx (i + 1) in + let ctx = set_offset ctx (n - k) in + let ctx = add_rte_variable (Some name) lxp ctx in + (ctx, k + 1)) + (ctx, 0) decls in + + let dctx = set_offset dctx 0 in + (local_ctx dctx) + + with e ->( + print_rte_ctx (!_global_eval_ctx); + print_eval_trace (); + raise e + ) +
and print_eval_result i lxp = print_string " Out[";
===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -139,7 +139,7 @@ and _lexp_parse p ctx i: lexp =
(* Let, Variable declaration + local scope *) | Plet(loc, decls, body) -> - let decl, nctx = lexp_decls decls ctx in + let decl, nctx = _lexp_decls decls ctx i in let bdy = lexp_parse body nctx in Let(tloc, decl, bdy)
@@ -328,56 +328,91 @@ and lexp_parse_inductive ctors ctx i = SMap.empty ctors
(* Parse let declaration *) -and lexp_decls decls ctx: (((vdef * lexp * ltype) list) * lexp_context) = - (* The new implementation suppose that forward declarations are - * used when mutually recursive type are declared. - * old implementation was going through declaration 4 times - * now everything is done by going through them once *) - let lexp_parse p ctx = _lexp_parse p ctx 1 in - let m = (List.length decls) + (get_size ctx) in - - (* Make it look like we processed all declarations once already*) - let forge_ctx ctx n = - let ((m, map), a, b) = ctx in - ((n, map), a, b) in - - let iter_fun (idx, ctx, sset, acc) elem = - let ((loc, name), pxp, bl) = elem in ( - (* Process Type *) - if bl then ( - (* Temporary extend *) - (* type info must be present for recursive call *) - let tctx = env_extend ctx (loc, name) None dltype in - let ltp = lexp_parse pxp (forge_ctx tctx m) in - - let ctx = env_extend ctx (loc, name) None ltp in - let sset = StringMap.add name ltp sset in - (idx + 1, ctx, sset, acc) - ) - (* Process instruction *) - else( - (* Type annotations was provided *) - try - let ltp = StringMap.find name sset in - (* Type check *) - let lxp = lexp_p_check pxp ltp (forge_ctx ctx m) in - (idx + 1, ctx, sset, ((loc, name), lxp, ltp)::acc) - - (* No Type annotations *) - with Not_found -> - let tctx = env_extend ctx (loc, name) None dltype in - let lxp, ltp = lexp_p_infer pxp (forge_ctx tctx m) in - - let ctx = env_extend ctx (loc, name) (Some lxp) ltp in - (idx + 1, ctx, sset, ((loc, name), lxp, ltp)::acc)) - ) in - - let (n, nctx, _, decls) = List.fold_left iter_fun - (0, ctx, StringMap.empty, []) decls in - (* NB: if some var x was type annotated then it does not have - * a "value" in the env. A second pass through the declaration could - * solve this. Nevertheless, I not sure if it is truly useful *) - (List.rev decls), nctx +and lexp_p_decls decls ctx = _lexp_decls decls ctx 1 +and _lexp_decls decls ctx i: (((vdef * lexp * ltype) list) * lexp_context) = + let lexp_parse v c = _lexp_parse v c (i + 1) in + (* Merge Type info and declaration together *) + + (* merge with a map to guarantee uniqueness. *) + let rec merge_decls (decls: (pvar * pexp * bool) list) merged acc: + ((location * pexp option * pexp option) SMap.t * string list) = + + (* we cant evaluate here because variable are not in the environment *) + match decls with + | [] -> merged, (List.rev acc) + | hd::tl -> + match hd with + (* Type Info: Var:Type *) + | ((loc, name), type_info, true) -> begin + try + (* If found its means the instruction was declared + * before the type info. Should we allow this? *) + let (l, inst, _) = SMap.find name merged in + let new_decl = (l, inst, Some type_info) in + let nmerged = SMap.add name new_decl merged in + (merge_decls tl nmerged acc) + with Not_found -> + let new_decl = (loc, None, Some type_info) in + let nmerged = SMap.add name new_decl merged in + (merge_decls tl nmerged (name::acc)) end + + (* Instruction: Var = expr *) + | ((loc, name), inst, false) -> begin + try + let (l, _, tp) = SMap.find name merged in + let new_decl = (l, Some inst, tp) in + let nmerged = SMap.add name new_decl merged in + (merge_decls tl nmerged acc) + + with Not_found -> + let new_decl = (loc, Some inst, None) in + let nmerged = SMap.add name new_decl merged in + (merge_decls tl nmerged (name::acc)) end in + + let mdecls, ord = merge_decls decls SMap.empty [] in + + (* cast map to list to preserve declaration order *) + let decls = List.map (fun name -> + let (l, inst, tp) = SMap.find name mdecls in + ((l, name), inst, tp) ) ord + in + + (* Add Each Variable to the environment *) + let nctx = List.fold_left (fun ctx hd -> + match hd with + | (_, None, _) -> ctx (* Unused variable: No Instruction *) + | (var, _, _) -> senv_add_var var ctx) + ctx decls in + + let n = (List.length decls) - 1 in + + (* Add Variable info *) + let rec process_var_info dcl_lst ctx acc m = + 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 ctx = env_add_var_info (0, (loc, name), + Some lxp, ltp) ctx in + process_var_info tl ctx nacc (m - 1)) + + | ((loc, name), Some pinst, Some ptype) ->( + let linst = lexp_parse pinst ctx in + let ltyp = lexp_parse ptype ctx in + let nacc = ((loc, name), linst, ltyp)::acc in + let ctx = env_add_var_info (0, (loc, name), + Some linst, ltyp) ctx in + process_var_info tl ctx nacc (m - 1)) + + (* Skip the variable *) + | ((loc, name), None, _) -> (lexp_warning loc "Unused Variable"; + process_var_info tl ctx acc m) in + + let acc, ctx = process_var_info decls nctx [] n in + acc, ctx
and _lexp_parse_all (p: pexp list) (ctx: lexp_context) i : lexp list =
@@ -504,12 +539,14 @@ and lexp_p_infer (p : pexp) (env : lexp_context): lexp * ltype = (* Leafs *) (* ------------ *)
- (* Why don't we always return tp ? We want to be able to use *) - (* type aliases Nat = inductive_ *) - (* We want the type to be inferred as Nat not _inductive... *) - (* But sometimes we need tp to be return *) - | Var vrf -> let tp = env_lookup_type ctx vrf in - if (is_type tp) then lxp else tp + (* Why don't we always return tp ? We want to be able to use *) + (* type aliases Nat = inductive_ *) + (* We want the type to be inferred as 'Nat' not 'inductive_'... *) + (* But sometimes we need tp to be returned *) + | Var vrf -> (try let tp = env_lookup_type ctx vrf in + (if (is_type tp) then lxp else tp) + with e -> + UnknownType(dloc))
(* I am not sure we should consider a constructor as a function *) (* Another way to do what is done here is to handle cons in Call *) @@ -823,7 +860,7 @@ let _lexp_decl_str (str: string) tenv grm limit ctx = let toks = lex tenv pretoks in let sxps = sexp_parse_all_to_list grm toks limit in let pxps = pexp_decls_all sxps in - lexp_decls pxps ctx + lexp_p_decls pxps ctx ;;
(* specialized version *)
===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -4,6 +4,14 @@ open Eval (* make_rte_ctx *) open Utest_lib open Util open Lexp +open Sexp + + +let get_int lxp = + match lxp with + | Imm(Integer(_, l)) -> l + | _ -> (-40); +;;
(* default environment *) @@ -13,6 +21,7 @@ let rctx = add_rte_variable (Some "_+_") iop_binary rctx let rctx = add_rte_variable (Some "_*_") iop_binary rctx
let _ = (add_test "EVAL" "Variable Cascade" (fun () -> + reset_eval_trace ();
let dcode = " a = 10; @@ -36,6 +45,8 @@ let _ = (add_test "EVAL" "Variable Cascade" (fun () -> * ------------------------ *)
let _ = (add_test "EVAL" "Let" (fun () -> + reset_eval_trace (); + (* Noise. Makes sure the correct variables are selected *) let dcode = " c = 3; e = 1; f = 2; d = 4;" in @@ -56,6 +67,7 @@ let _ = (add_test "EVAL" "Let" (fun () -> (* Lambda * ------------------------ *) let _ = (add_test "EVAL" "Lambda" (fun () -> + reset_eval_trace ();
(* Declare lambda *) let rctx, lctx = eval_decl_str "sqr = lambda x -> x * x;" lctx rctx in @@ -70,6 +82,8 @@ let _ = (add_test "EVAL" "Lambda" (fun () -> ;;
let _ = (add_test "EVAL" "Nested Lambda" (fun () -> + reset_eval_trace (); + let code = " sqr = lambda x -> x * x; cube = lambda x -> x * (sqr x);" in @@ -89,7 +103,10 @@ let _ = (add_test "EVAL" "Nested Lambda" (fun () -> (* This makes sure contexts are reinitialized between calls * i.e the context should not grow *) let _ = (add_test "EVAL" "Infinite Recursion failure" (fun () -> + reset_eval_trace (); + let code = " + infinity : Int -> Int; infinity = lambda (beyond : Int) -> (infinity beyond);" in
let rctx, lctx = eval_decl_str code lctx rctx in @@ -99,17 +116,19 @@ let _ = (add_test "EVAL" "Infinite Recursion failure" (fun () -> let _ = _eval_expr_str "(infinity 0);" lctx rctx true in failure () with - Internal_error m -> + Internal_error m -> ( if m = "Recursion Depth exceeded" then success () else - failure () + failure ()) ));;
(* Cases + Inductive types * ------------------------ *)
let _ = (add_test "EVAL" "Inductive::Case" (fun () -> + reset_eval_trace (); + (* Inductive type declaration + Noisy declarations *) let code = " i = 90;\n @@ -167,13 +186,13 @@ let bool_decl = " true = inductive-cons Bool true;" ;;
- let _ = (add_test "EVAL" "Inductive::Recursive Call" (fun () -> + reset_eval_trace ();
let code = nat_decl ^ " one = (succ zero); two = (succ one); - three = (succ three);" in + three = (succ two);" in
let rctx, lctx = eval_decl_str code lctx rctx in
@@ -196,17 +215,16 @@ let _ = (add_test "EVAL" "Inductive::Recursive Call" (fun () -> ;;
let _ = (add_test "EVAL" "Inductive::Nat Plus" (fun () -> - - _eval_max_recursion_depth := 80000; + reset_eval_trace ();
let code = nat_decl ^ " one = (succ zero); two = (succ one); - three = (succ three); + three = (succ two);
- plus = lambda x y -> case x - | zero => y - | succ z => succ (plus z y); + plus = lambda (x : Nat) -> lambda (y : Nat) -> case x + | zero => y + | succ z => succ (plus z y); " in
let rctx, lctx = eval_decl_str code lctx rctx in @@ -231,21 +249,21 @@ let _ = (add_test "EVAL" "Inductive::Nat Plus" (fun () -> | _ -> failure () ));;
-(* TODO *) let _ = (add_test "EVAL" "Mutually Recursive Definition" (fun () -> + reset_eval_trace ();
let dcode = nat_decl ^ " one = (succ zero); two = (succ one); - three = (succ three); + three = (succ two);
- odd : Int -> Int; - even : Int -> Int; - odd = lambda n -> case n + odd : Nat -> Int; + even : Nat -> Int; + odd = lambda (n : Nat) -> case n | zero => 0 | succ y => (even y);
- even = lambda n -> case n + even = lambda (n : Nat) -> case n | zero => 1 | succ y => (odd y);" in
@@ -260,8 +278,8 @@ let _ = (add_test "EVAL" "Mutually Recursive Definition" (fun () -> | [a; b; c; d] -> let t1 = expect_equal_int (get_int a) 1 in let t2 = expect_equal_int (get_int b) 0 in - let t3 = expect_equal_int (get_int c) 1 in - let t4 = expect_equal_int (get_int d) 0 in + let t3 = expect_equal_int (get_int c) 0 in + let t4 = expect_equal_int (get_int d) 1 in if t1 = 0 && t2 = 0 && t3 = 0 && t4 = 0 then success () else @@ -270,14 +288,19 @@ let _ = (add_test "EVAL" "Mutually Recursive Definition" (fun () -> ));;
let _ = (add_test "EVAL" "Partial Application" (fun () -> + reset_eval_trace (); +
let dcode = " - mult = lambda x y -> (x * y); - twice = (mult 2);" in + add : Int -> Int -> Int; + add = lambda x y -> (x + y); + + inc : Int -> Int; + inc = (add 1);" in
let rctx, lctx = eval_decl_str dcode lctx rctx in
- let rcode = "(twice 1); (twice 2); (twice 3);" in + let rcode = "(inc 1); (inc 2); (inc 3);" in
(* Eval defined lambda *) let ret = eval_expr_str rcode lctx rctx in
View it on GitLab: https://gitlab.com/monnier/typer/commit/7cfabe06d633d03e2b32d22dd0057f10f307...