Mars 2016 - Typer - mailman.iro.umontreal.ca

[Git][monnier/typer][master] Fix mutually recursive definition lexp parsing
by Setepenre 31 Mar '16

31 Mar '16

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/7cfabe06d633d03e2b32d22dd0057f10f30…

1 0

[Git][monnier/typer][master] Allow restricted type aliasing during type inference
by Setepenre 30 Mar '16

30 Mar '16

Setepenre pushed to branch master at Stefan / Typer Commits: 33279ef6 by Pierre Delaunay at 2016-03-30T09:53:57-04:00 Allow restricted type aliasing during type inference In 'Nat = inductive_' We want to use the alias 'Nat' instead of the full declaration during type inference. It is restricted aliasing because only inductive type can be aliased that way. Changes to be committed: * GNUmakefile: tests don't run when using make all * src/eval.ml: Call eval check for constructor before evaluating (Test - Nat Plus Work) * src/lparse.ml: - Type inference: Allow restricted type aliasing - Type inference: Call now allow partial application - Type inference: Cons are typed as function * src/lexer.ml: added (lex_str) and (sexp_parse_str) * src/pexp.ml: removed useless declaration/include * tests/eval_test.ml: - Mutually rec decl tests - Partial Application test new file: * tests/sexp_test.ml: test _*_ and _+_ precedence which both seems to be buggy - - - - - 13 changed files: - GNUmakefile - src/REPL.ml - src/debug.ml - src/eval.ml - src/lexer.ml - src/lexp.ml - src/lparse.ml - src/pexp.ml - src/sexp.ml - tests/eval_test.ml - tests/lexp_test.ml - + tests/sexp_test.ml - tests/utest_main.ml Changes: ===================================== GNUmakefile ===================================== --- a/GNUmakefile +++ b/GNUmakefile @@ -6,7 +6,7 @@ TEST_FILES := $(wildcard ./tests/*_test.ml) CFLAG = -cflag -rectypes -build-dir _build -all: ityper typer debug tests +all: ityper typer debug tests-build typer: # ============================ @@ -40,10 +40,7 @@ tests-build: @mv _build/tests/utest_main.native _build/tests/utests tests-run: - # ============================ - # Run tests - # ============================ - @./_build/tests/utests --verbose= 3 + @./_build/tests/utests --verbose= 2 tests: tests-build tests-run ===================================== src/REPL.ml ===================================== --- a/src/REPL.ml +++ b/src/REPL.ml @@ -36,6 +36,7 @@ this program. If not, see <http://www.gnu.org/licenses/>. *) * * -------------------------------------------------------------------------- *) +(* FIXME: Prevent ityper from crashing when an error is thrown *) open Debug open Prelexer ===================================== src/debug.ml ===================================== --- a/src/debug.ml +++ b/src/debug.ml @@ -134,7 +134,7 @@ let debug_pexp_print 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_info "Not Impl " l ptop *) ;; let debug_pexp_decls decls = ===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -31,6 +31,7 @@ * --------------------------------------------------------------------------- *) open Util +open Pexp (* Arg_kind *) open Lexp open Lparse open Myers @@ -197,6 +198,10 @@ let rec _eval lxp ctx i: (value_type) = let nctx = build_ctx decls ctx i in _eval inst (local_ctx nctx) (i + 1) + (* Built-in Function * ) + | Call(Builtin(v, name, ltp), args) -> + let nctx = build_arg_list args ctx i in *) + (* Function call *) | Call (lname, args) -> ( (* create a clean environment *) @@ -227,7 +232,7 @@ let rec _eval lxp ctx i: (value_type) = Imm(Integer(dloc, v)) (* This is a named function call *) - | Var((_, name), idx) -> + | Var((_, name), idx) -> ( (* get function's body from current context *) let body = get_rte_variable (Some name) idx ctx in @@ -235,12 +240,18 @@ let rec _eval lxp ctx i: (value_type) = let arg_val = List.map (fun (k, e) -> _eval e ctx (i + 1)) args in - (* 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) + 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 *) ===================================== src/lexer.ml ===================================== --- a/src/lexer.ml +++ b/src/lexer.ml @@ -23,6 +23,7 @@ this program. If not, see <http://www.gnu.org/licenses/>. *) open Util open Prelexer open Sexp +open Grammar (*************** The Lexer phase *********************) @@ -42,7 +43,7 @@ let digit_p char = in Char.code '0' <= code && code <= Char.code '9' type num_part = | NPint | NPfrac | NPexp - + let nexttoken (stt : token_env) (pts : pretoken list) bpos cpos (* The returned Sexp may not be a Node. *) : sexp * pretoken list * bytepos * charpos = @@ -118,15 +119,19 @@ let lex tenv (pts : pretoken list) : sexp list = in gettokens pts bpos cpos (tok :: acc) in gettokens pts 0 0 [] ;; - -let lex_string (str: string) tenv = + +let _lex_str (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 +let lex_str str = _lex_str str default_stt + +let _sexp_parse_str (str: string) tenv grm limit = + let toks = _lex_str str tenv in sexp_parse_all_to_list grm toks limit ;; - + +let sexp_parse_str str = + _sexp_parse_str str default_stt default_grammar (Some ";") + ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -21,7 +21,6 @@ You should have received a copy of the GNU General Public License along with this program. If not, see <http://www.gnu.org/licenses/>. *) open Util -open Lexer open Sexp open Pexp open Myers @@ -274,6 +273,8 @@ let rec lexp_location e = | Inductive (l,_,_,_) -> l | Cons (_,(l,_)) -> l | Case (l,_,_,_,_) -> l + | UnknownType l -> l + | Shift (_, l) -> lexp_location l (* | Susp (_, e) -> lexp_location e * | Metavar ((l,_),_,_) -> l *) ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -87,9 +87,7 @@ let default_lctx () = (* populate ctx *) List.fold_left (fun ctx (name, lxp) -> - let var = (dloc, name) in - let ctx = senv_add_var var ctx in - env_add_var_info (0, var, None, lxp) ctx) + env_extend ctx (dloc, name) None lxp) lctx lexp_builtins ;; @@ -477,21 +475,70 @@ and lexp_p_infer (p : pexp) (env : lexp_context): lexp * ltype = let tloc = pexp_location p in let lxp = lexp_parse p env in - let rec get_return_type lxp = + let consume_args args lxp ctx = + let arg_n = List.length args in + let rec _implt args lxp i = match args, lxp with + (* No args left, return the remaining type *) + | [], _ -> lxp + | _, UnknownType _ -> lxp + + (* Basic case consume an arg and an arrow *) + | hd::tl, Arrow(_, _, ltp, _, ret_type) -> + (* FIXME: Check hd and ltp are of the same type *) + _implt tl ret_type (i + 1) + + (* We still have args to consume but type is not an arrow *) + | (_, hd)::tl, tp -> + lexp_error tloc ("Number of Arg mismatch. Expected: " ^ + (string_of_int i) ^ " arg(s). Got " ^ (string_of_int arg_n)); + tp in + _implt args lxp 0 in + + let is_type lxp = match lxp with - | Arrow(_, _, _, _, ret_type) -> (get_return_type ret_type) - | _ -> lxp in + | Inductive _ -> true + | _ -> false in let rec get_type lxp ctx = match lxp with (* Leafs *) (* ------------ *) - | Var vrf -> env_lookup_type ctx vrf - | Cons (vrf, _) -> env_lookup_type ctx vrf + + (* 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 + + (* 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 *) + | Cons (vrf, (_, n)) ->( + let rec build_arrow_type args acc = + match args with + | [] -> acc + | (kind, var, ltp)::tl -> + build_arrow_type tl (Arrow(kind, var, ltp, dloc, acc)) + in + + match env_lookup_type ctx vrf with + | Inductive(_, _, _, ctor_map) -> ( + try match SMap.find n ctor_map with + (* No Args *) + | [] -> Var(vrf) (* return its inductive type *) + (* Return a Constructor function *) + | args -> build_arrow_type (List.rev args) (Var(vrf)) + + with Not_found -> + (lexp_error tloc ("Constructor " ^ n ^ + " does not exist"); dltype)) + | _ -> (lexp_error tloc "Inductive type was expected"; dltype)) + | Imm sxp -> (match sxp with - (* FIXME use the ones that are already in the ctx *) - | Integer _ -> type_int - | Float _ -> type_float + | Integer _ -> let idx = senv_lookup "Int" ctx in + env_lookup_type ctx ((dloc, "Int"), idx) + | Float _ -> let idx = senv_lookup "Float" ctx in + env_lookup_type ctx ((dloc, "Float"), idx) | _ -> lexp_error tloc "Could not infer type"; dltype) (* Types by definition *) @@ -503,17 +550,29 @@ and lexp_p_infer (p : pexp) (env : lexp_context): lexp * ltype = (* Nodes *) (* ------------ *) | Let (_, _, body) -> (get_type body ctx) - | Call(f, _) -> - (* FIXME: check arg and f type are compatible *) - (* FIXME: call cannot be partial *) - (get_return_type (get_type f ctx)) - - (* we need to check that all branches return the same type *) - | Case (_, _, _, branches, dflt) ->( - (* FIXME *) - match dflt with - | None -> lexp_error tloc "Could not infer type"; dltype - | Some expr -> (get_type expr ctx)) + | Call(f, args) -> + (consume_args args (get_type f ctx) ctx) + + + | Case (_, _, _, branches, dflt) -> + (* we need to check that all branches return the same type *) + let lst = SMap.bindings branches in + let types = List.map + (fun (_, (_, args, body)) -> + (* FIXME: We need to lookup arg type *) + let nctx = List.fold_left (fun c v -> + match v with + | None -> c + | Some (_, arg) -> env_extend ctx arg None dltype) + ctx args in + get_type body nctx) lst in + + let types = match dflt with + | None -> types + | Some expr -> (get_type expr ctx)::types in + let tp = List.hd types in + (* FIXME: do type checking *) + tp | Lambda (kind, vdef, ltp, lxp) -> let nctx = env_extend ctx vdef (Some ltp) lxp in @@ -534,6 +593,7 @@ and lexp_p_check (p : pexp) (t : ltype) (env : lexp_context): lexp = -> let (e, inferred_t) = lexp_p_infer p env in (* FIXME: check that inferred_t = t! *) e + (* * Printing * --------------------- *) @@ -643,7 +703,6 @@ and lexp_print_ctors opt ctors = ctors and lexp_print_type opt ltp = - let (_, _, prtp) = opt in match ltp with | Inductive(_, (_, l), _, _) -> print_string l; | _ -> lexp_print_adv opt ltp @@ -712,7 +771,6 @@ and print_lexp_trace () = and lexp_print_var_info ctx = let ((m, _), env, _) = ctx in let n = Myers.length env in - let sync_offset = m - n in for i = 0 to n - 1 do ( let (_, (_, name), exp, tp) = Myers.nth i env in ===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -21,9 +21,8 @@ You should have received a copy of the GNU General Public License along with this program. If not, see <http://www.gnu.org/licenses/>. *) open Util -open Sexp +open Sexp (* Symbol *) open Lexer -open Prelexer open Grammar let pexp_error = msg_error "PEXP" @@ -358,13 +357,6 @@ 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 -;; - let pexp_decls_all (nodes: sexp list): ((pvar * pexp * bool) list) = let rec loop nodes acc = match nodes with @@ -382,9 +374,7 @@ let pexp_decls_all (nodes: sexp list): ((pvar * pexp * bool) list) = (* Lexp helper *) let _pexp_expr_str (str: string) (tenv: bool array) (grm: grammar) (limit: string option) = - let pretoks = prelex_string str in - let toks = lex tenv pretoks in - let sxps = sexp_parse_all_to_list grm toks limit in + let sxps = _sexp_parse_str str tenv grm limit in pexp_parse_all sxps ;; @@ -393,11 +383,8 @@ let pexp_expr_str str = _pexp_expr_str str default_stt default_grammar (Some ";") ;; - let _pexp_decl_str (str: string) tenv grm limit = - let pretoks = prelex_string str in - let toks = lex tenv pretoks in - let sxps = sexp_parse_all_to_list grm toks limit in + let sxps = _sexp_parse_str str tenv grm limit in pexp_decls_all sxps ;; ===================================== src/sexp.ml ===================================== --- a/src/sexp.ml +++ b/src/sexp.ml @@ -231,3 +231,7 @@ let sexp_parse_all_to_list grm tokens limit = sexp_parse_impl grm rest limit (sxp :: acc) in sexp_parse_impl grm tokens limit [] ;; + + + + ===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -90,7 +90,7 @@ let _ = (add_test "EVAL" "Nested Lambda" (fun () -> * i.e the context should not grow *) let _ = (add_test "EVAL" "Infinite Recursion failure" (fun () -> let code = " - infinity = lambda beyond -> (infinity beyond);" in + infinity = lambda (beyond : Int) -> (infinity beyond);" in let rctx, lctx = eval_decl_str code lctx rctx in @@ -109,7 +109,7 @@ let _ = (add_test "EVAL" "Infinite Recursion failure" (fun () -> (* Cases + Inductive types * ------------------------ *) -let _ = (add_test "EVAL" "Case" (fun () -> +let _ = (add_test "EVAL" "Inductive::Case" (fun () -> (* Inductive type declaration + Noisy declarations *) let code = " i = 90;\n @@ -146,9 +146,8 @@ let _ = (add_test "EVAL" "Case" (fun () -> success () else failure () - | _ -> failure ()) -) -;; + | _ -> failure () +));; (* Those wil be used multiple times *) let nat_decl = " @@ -169,7 +168,7 @@ let bool_decl = " ;; -let _ = (add_test "EVAL" "Recursive Call" (fun () -> +let _ = (add_test "EVAL" "Inductive::Recursive Call" (fun () -> let code = nat_decl ^ " one = (succ zero); @@ -196,7 +195,9 @@ let _ = (add_test "EVAL" "Recursive Call" (fun () -> ) ;; -let _ = (add_test "EVAL" "Nat Plus" (fun () -> +let _ = (add_test "EVAL" "Inductive::Nat Plus" (fun () -> + + _eval_max_recursion_depth := 80000; let code = nat_decl ^ " one = (succ zero); @@ -213,7 +214,7 @@ let _ = (add_test "EVAL" "Nat Plus" (fun () -> let rcode = " (tonum (plus zero two)); (tonum (plus two zero)); - 5;"in + (tonum (plus two one));"in (* Eval defined lambda *) let ret = eval_expr_str rcode lctx rctx in @@ -222,14 +223,76 @@ let _ = (add_test "EVAL" "Nat Plus" (fun () -> | [a; b; c] -> let t1 = expect_equal_int (get_int a) 2 in let t2 = expect_equal_int (get_int b) 2 in - let t3 = expect_equal_int (get_int c) 5 in + let t3 = expect_equal_int (get_int c) 3 in if t1 = 0 && t2 = 0 && t3 = 0 then success () else failure () - | _ -> failure ()) -) -;; + | _ -> failure () +));; + +(* TODO *) +let _ = (add_test "EVAL" "Mutually Recursive Definition" (fun () -> + + let dcode = nat_decl ^ " + one = (succ zero); + two = (succ one); + three = (succ three); + + odd : Int -> Int; + even : Int -> Int; + odd = lambda n -> case n + | zero => 0 + | succ y => (even y); + + even = lambda n -> case n + | zero => 1 + | succ y => (odd y);" in + + let rctx, lctx = eval_decl_str dcode lctx rctx in + + let rcode = "(odd one); (even one); (odd two); (even two);" in + + (* Eval defined lambda *) + let ret = eval_expr_str rcode lctx rctx in + (* Expect a 3 results *) + match ret with + | [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 + if t1 = 0 && t2 = 0 && t3 = 0 && t4 = 0 then + success () + else + failure () + | _ -> failure () +));; + +let _ = (add_test "EVAL" "Partial Application" (fun () -> + + let dcode = " + mult = lambda x y -> (x * y); + twice = (mult 2);" in + + let rctx, lctx = eval_decl_str dcode lctx rctx in + + let rcode = "(twice 1); (twice 2); (twice 3);" in + + (* Eval defined lambda *) + let ret = eval_expr_str rcode lctx rctx in + (* Expect a 3 results *) + match ret with + | [a; b; c] -> + let t1 = expect_equal_int (get_int a) 2 in + let t2 = expect_equal_int (get_int b) 4 in + let t3 = expect_equal_int (get_int c) 6 in + if t1 = 0 && t2 = 0 && t3 = 0 then + success () + else + failure () + | _ -> failure () +));; (* List = inductive (dList (a : Type)) (nil) (cons a (List a)); ===================================== tests/lexp_test.ml ===================================== --- a/tests/lexp_test.ml +++ b/tests/lexp_test.ml @@ -5,10 +5,7 @@ open Pexp open Utest_lib (* default environment *) -let lctx = make_lexp_context -let lctx = add_def "_+_" lctx -let lctx = add_def "_*_" lctx - +let lctx = default_lctx () let _ = (add_test "LEXP" "Built-in type Inference" (fun () -> ===================================== tests/sexp_test.ml ===================================== --- /dev/null +++ b/tests/sexp_test.ml @@ -0,0 +1,57 @@ +open Sexp +open Lexer +open Utest_lib + + +(* _+_ precedence is too low ? + * + * a = lambda x -> x + x + x + * is parsed to + * a = (_+_ (_+_ (lambda_->_ x x) x) x) <=> a = (lambda x -> x) + x + x + * instead of + * a = (lambda_->_ x (_+_ (_+_ x x) x)) *) +let _ = (add_test "SEXP" "lambda x -> x + x" (fun () -> + + let dcode = "lambda x -> x + x;" in + + let ret = sexp_parse_str dcode in + match ret with + | [n] ->(match n with + | Node(Symbol(_, "lambda"), [arg; body]) -> success () + (* arg = Symbol(_, "x") *) + (* body = Node(Symbol(_, "_+_"), [Symbol(_, "x"); Symbol(_, "x")]) *) + | _ -> failure ()) + | _ -> failure () +));; + + +(* _*_ is not a binary operator + * + * b = lambda x -> (x * x * x); + * is parsed to + * b = (lambda_->_ x (_*_ x x x)) + * instead of + * b = (lambda_->_ x (_*_ (_*_ x x) x)) *) +let _ = (add_test "SEXP" "x * x * x" (fun () -> + + let dcode = "x * x * x;" in + + let ret = sexp_parse_str dcode in + match ret with + | [n] ->(match n with + | Node(Symbol(_, "_*_"), + [Node(Symbol(_, "_*_"), [Symbol(_, "x"); Symbol(_, "x")]); Symbol(_, "x")]) + -> success () + + | Node(Symbol(_, "_*_"), + [Symbol(_, "x"); Node(Symbol(_, "_*_"), [Symbol(_, "x")]); Symbol(_, "x")]) + -> success () + + | _ -> failure ()) + | _ -> failure () + +));; + +(* run all tests *) +run_all () +;; ===================================== tests/utest_main.ml ===================================== --- a/tests/utest_main.ml +++ b/tests/utest_main.ml @@ -119,7 +119,9 @@ let main () = failed_test := !failed_test + 1) else (if verbose 1 then print_file_name (!tests_n) files_n file true); - ) + ); + + (if verbose 2 then print_newline ()); ) files; @@ -127,7 +129,7 @@ let main () = print_string " Test Ran : "; print_int !tests_n; print_string "\n Test Failed : "; print_int !failed_test; print_string "\n Test Passed : "; print_int (!tests_n - !failed_test); - print_endline ""; + print_endline "\n"; ;; main (); View it on GitLab: https://gitlab.com/monnier/typer/commit/33279ef68725a368296431c6a3701901f37…

1 0

[Git][monnier/typer][master] Fix lexp's Induction to name fields. Fix lexp_context for real vars.
by Stefan 25 Mar '16

25 Mar '16

Stefan pushed to branch master at Stefan / Typer Commits: bc4698bc by Stefan Monnier at 2016-03-24T22:22:01-04:00 Fix lexp's Induction to name fields. Fix lexp_context for real vars. * src/debruijn.ml (db_idx, db_ridx): Re-introduce those type aliases. (senv_add_var): Remove redundancy. Change calling convention. (lexp_context): Make var's "value" optional. (env_extend): New function. * src/eval.ml (nfirst_rte_var._eval.ctor_name): Fix confusion in constructor args. * src/lexp.ml (lexp): Add optional name to constructor fields. * src/lparse.ml (default_lctx): Adjust to new senv_add_var. (lexp_parse): Consolidate the two Plambda cases. Don't mess with local_scope here. (lexp_parse_inductive): Rename from lexp_parse_constructors. Adapt to lexp changes. Use List.fold_left. (lexp_decls): Adjust to new senv_add_var. (lexp_context_print): Handle vars without value. - - - - - 5 changed files: - src/debruijn.ml - src/eval.ml - src/lexp.ml - src/lparse.ml - tests/debug.ml Changes: ===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -44,45 +44,49 @@ let debruijn_warning = msg_warning "DEBRUIJN" * ---------------------------------- *) (* Index -> Variable Info *) -type env_elem = (int * (location * string) * lexp * ltype) +type env_elem = (int * (location * string) * lexp option * ltype) type env_type = env_elem myers (* This exist because I don't want that file to depend on anything *) module StringMap = Map.Make (struct type t = string let compare = String.compare end) -;; + +type db_idx = int (* DeBruijn index. *) +type db_ridx = int (* DeBruijn reverse index (i.e. counting from the root). *) (* Map matching variable name and its distance in the current scope *) -type scope = (int) StringMap.t (* Map<String, int>*) +type scope = db_ridx StringMap.t (* Map<String, db_ridx>*) type senv_length = int (* it is not the map true length *) type senv_type = senv_length * scope - (* name -> index * index -> info * (outer_size, r_offset) *) +(* FIXME: What is this "outer_size" and "r_offset"? *) +(* name -> index * index -> info * (outer_size, r_offset) *) type lexp_context = senv_type * env_type * (int * int) (* internal definitions * ---------------------------------- *) -let _make_scope = StringMap.empty;; -let _make_senv_type = (0, _make_scope);; +let _make_scope = StringMap.empty +let _make_senv_type = (0, _make_scope) let _make_myers = nil -let _get_env(ctx: lexp_context): env_type = let (_, ev, _) = ctx in ev ;; +let _get_env(ctx: lexp_context): env_type = let (_, ev, _) = ctx in ev (* Public methods: DO USE * ---------------------------------- *) -let make_lexp_context = (_make_senv_type, _make_myers, (0, 0));; +let make_lexp_context = (_make_senv_type, _make_myers, (0, 0)) + +let get_roffset ctx = let (_, _, (_, rof)) = ctx in rof -let get_roffset ctx = let (_, _, (_, rof)) = ctx in rof;; +(* FIXME: I have no idea what is a "scope" here! *) (* Enter a local scope such as let *) let local_scope ctx pos = let ((l, map), b, c) = ctx in (* Check size *) - let n = (length b) in - ((l, map), b, (l, pos)) -;; + (* let n = (length b) in *) + ((l, map), b, (l, pos)) (* Enter a temporary scope such as Calls *) let temp_scope ctx bound = let (a, b, c) = ctx in (a, b, bound) @@ -95,29 +99,24 @@ let rec senv_lookup (name: string) (ctx: lexp_context): int = raw_idx - rof (* Shift if the variable is not bound *) else *) raw_idx -;; (* We first add variable into our map. Later on, we will add them into * the environment. The reason for this is that the type info is * known after lexp parsing which need the index fist *) -let senv_add_var name loc ctx = +let senv_add_var (loc, name) ctx = let ((n, map), e, f) = ctx in - try - let _ = senv_lookup name ctx in - debruijn_warning loc ("Variable Shadowing " ^ name); - let nmap = StringMap.add name n map in - ((n + 1, nmap), e, f) - with - Not_found -> - let nmap = StringMap.add name n map in - ((n + 1, nmap), e, f) -;; + (try let _ = senv_lookup name ctx in + debruijn_warning loc ("Variable Shadowing " ^ name) + with Not_found -> ()); + let nmap = StringMap.add name n map in + ((n + 1, nmap), e, f) -(* *) let env_add_var_info var (ctx: lexp_context) = let (a, env, f) = ctx in (a, cons var env, f) -;; + +let env_extend (ctx:lexp_context) (def:vdef) (v: lexp option) (t:lexp) = + env_add_var_info (0, def, v, t) (senv_add_var def ctx) let env_lookup_type_by_index index ctx = try @@ -125,7 +124,6 @@ let env_lookup_type_by_index index ctx = Shift (index - roffset, t) with Not_found -> internal_error "DeBruijn index out of bounds!" -;; let env_lookup_type ctx (v : vref) = let ((_, rname), dbi) = v in @@ -138,5 +136,3 @@ let env_lookup_type ctx (v : vref) = let env_lookup_by_index index (ctx: lexp_context): env_elem = Myers.nth index (_get_env ctx) -;; - ===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -252,7 +252,7 @@ let rec _eval lxp ctx i: (value_type) = (* 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 + (* let (loc, name) = vr in *) (* This was redundant since we already pushed args * when processing the call expression *) @@ -304,8 +304,9 @@ let rec _eval lxp ctx i: (value_type) = | Inductive(_, _, _, c) -> c | _ -> eval_error loc "Not an Inductive Type" in - try let args = SMap.find cname ctor_def in - cname, args + try match SMap.find cname ctor_def with + | [] -> cname, [] + | _ -> eval_error loc "Constructor not applied" with Not_found -> eval_error loc "Constructor does not exist" end ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -71,7 +71,7 @@ type ltype = lexp | Lambda of arg_kind * vdef * ltype * lexp | Call of lexp * (arg_kind * lexp) list (* Curried call. *) | Inductive of location * label * ((arg_kind * vdef * ltype) list) - * ((arg_kind * ltype) list) SMap.t + * ((arg_kind * vdef option * ltype) list) SMap.t | Cons of vref * symbol (* = Type info * ctor_name*) | Case of location * lexp * ltype (* The base inductive type over which we switch. *) ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -84,11 +84,13 @@ let default_lctx = let lctx = make_lexp_context in (* populate ctx *) - List.fold_left (fun ctx (name, lxp) -> - let ctx = senv_add_var name dloc ctx in - env_add_var_info (0, (dloc, name), lxp, lxp) ctx) - lctx - lexp_builtins + List.fold_left + (fun ctx (name, lxp) -> + let var = (dloc, name) in + let ctx = senv_add_var var ctx in + env_add_var_info (0, var, None, lxp) ctx) + lctx + lexp_builtins ;; @@ -144,43 +146,26 @@ let rec lexp_parse (p: pexp) (ctx: lexp_context): lexp = let lxp = lexp_parse expr ctx in Arrow(kind, None, ltyp, tloc, lxp) - (* *) - | Plambda (kind, var, Some ptype, body) -> - (* Add argument to context *) - let (loc, vname) = var in - let ltp = lexp_parse ptype ctx in (* Get Type *) - - let nctx = senv_add_var vname loc ctx in - let nctx = env_add_var_info (0, (loc, vname), dlxp, ltp) nctx in - - let ltyp = lexp_parse ptype nctx in - - let nctx = (local_scope nctx (get_roffset nctx)) in - let lbody = lexp_parse body nctx in - Lambda(kind, var, ltyp, lbody) - - | Plambda (kind, var, None, body) -> - 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 nctx = (local_scope nctx (get_roffset nctx)) in - let lbody = lexp_parse body nctx in - Lambda(kind, var, UnknownType(tloc), lbody) + | Plambda (kind, var, pt, body) -> + let nctx = senv_add_var var ctx in + let ltp = match pt with + | None -> dltype + | Some pt -> lexp_parse pt ctx in + let nctx = env_add_var_info (0, var, None, ltp) nctx in + let lbody = lexp_parse body nctx in + Lambda(kind, var, ltp, lbody) | Pcall (fname, _args) -> lexp_call fname _args ctx (* Pinductive *) | Pinductive (label, [], ctors) -> - let map_ctor, nctx = lexp_parse_constructors ctors ctx in - Inductive(tloc, label, [], map_ctor) + let map_ctor = lexp_parse_inductive ctors ctx in + Inductive(tloc, label, [], map_ctor) (* Pcons *) | 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 *) @@ -269,18 +254,18 @@ and lexp_read_pattern pattern exp target ctx: | Ppatany (loc) -> (* Catch all expression nothing to do *) ("_", loc, []), ctx - | Ppatvar (loc, name) ->( + | Ppatvar ((loc, name) as var) ->( (* FIXME better check *) try - let idx = senv_lookup name ctx in + let _ = senv_lookup name ctx in (* constructor with no args *) (name, loc, []), ctx (* would it not make a default match too? *) with Not_found -> (* Create a variable containing target *) - let nctx = senv_add_var name loc ctx in - let nctx = env_add_var_info (0, (loc, name), target, dltype) nctx in + let nctx = senv_add_var var ctx in + let nctx = env_add_var_info (0, var, Some target, dltype) nctx in (name, loc, []), nctx) | Ppatcons (ctor_name, args) -> @@ -302,46 +287,41 @@ and lexp_read_pattern_args args ctx: match pat with (* Nothing to do *) | Ppatany (loc) -> loop tl (None::acc) ctx - | Ppatvar (loc, name) -> + | Ppatvar ((loc, name) as var) -> (* 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 + let nctx = senv_add_var var ctx in + let nctx = env_add_var_info (0, var, None, dltype) nctx in + let nacc = (Some (Aexplicit, var))::acc in loop tl nacc nctx | _ -> lexp_error dloc "Constructor inside a Constructor"; loop tl (None::acc) ctx) in loop args [] ctx -(* Parse inductive constructor *) -and lexp_parse_constructors ctors ctx = +(* Parse inductive type definition. *) +and lexp_parse_inductive ctors ctx = - let make_args (args:(arg_kind * pvar option * pexp) list): - (arg_kind * ltype) list * lexp_context = + let make_args (args:(arg_kind * pvar option * pexp) list) ctx + : (arg_kind * vdef option * ltype) list = let rec loop args acc ctx = match args with - | [] -> (List.rev acc), ctx + | [] -> (List.rev acc) | hd::tl -> begin match hd with - (* What does the optional Pvar do ? - that expression does not exist in LEXP*) - | (kind, _, exp) -> - let lxp = lexp_parse exp ctx in - loop tl ((kind, lxp)::acc) ctx end in + | (kind, var, exp) -> + let lxp = lexp_parse exp ctx in + match var with + | None -> loop tl ((kind, None, lxp)::acc) ctx + | Some (var) -> + let nctx = env_extend ctx var None dltype in + loop tl ((kind, Some var, lxp)::acc) nctx + end in loop args [] ctx in - let rec loop ctors merged ctx = - match ctors with - | [] -> merged, ctx - | hd::tl -> begin - match hd with - | ((loc, name), args) -> - let largs, nctx = make_args args in - let nmerged = SMap.add name largs merged in - loop tl nmerged ctx - end in - - loop ctors SMap.empty ctx + List.fold_left + (fun lctors ((_, name), args) -> + SMap.add name (make_args args ctx) lctors) + SMap.empty ctors (* Parse let declaration *) and lexp_decls decls ctx: (((vdef * lexp * ltype) list) * lexp_context) = @@ -396,7 +376,7 @@ and lexp_decls decls ctx: (((vdef * lexp * ltype) list) * lexp_context) = let nctx = List.fold_left (fun ctx hd -> match hd with | (_, None, _) -> ctx (* Unused variable: No Instruction *) - | ((loc, name), _, _) -> senv_add_var name loc ctx) + | (var, _, _) -> senv_add_var var ctx) ctx decls in let n = (List.length decls) - 1 in @@ -411,7 +391,8 @@ and lexp_decls decls ctx: (((vdef * lexp * ltype) list) * lexp_context) = let nctx = local_scope _ctx m in let lxp, ltp = lexp_p_infer pinst nctx in let nacc = ((loc, name), lxp, ltp)::acc in - let ctx2 = env_add_var_info (0, (loc, name), lxp, ltp) nctx in + let ctx2 = env_add_var_info (0, (loc, name), + Some lxp, ltp) nctx in process_var_info tl ctx2 nacc (m - 1)) | ((loc, name), Some pinst, Some ptype) ->( @@ -419,7 +400,8 @@ and lexp_decls decls ctx: (((vdef * lexp * ltype) list) * lexp_context) = let linst = lexp_parse pinst nctx in let ltyp = lexp_parse ptype nctx in let nacc = ((loc, name), linst, ltyp)::acc in - let ctx3 = env_add_var_info (0, (loc, name), linst, ltyp) nctx in + let ctx3 = env_add_var_info (0, (loc, name), + Some linst, ltyp) nctx in process_var_info tl ctx3 nacc (m - 1)) (* Skip the variable *) @@ -660,7 +642,7 @@ and lexp_print_adv opt exp = and lexp_print_ctors opt ctors = SMap.iter (fun key value -> print_string ("(" ^ key ^ ": "); - List.iter (fun (kind, arg) -> + List.iter (fun (kind, _, arg) -> lexp_print_adv opt arg; print_string " ") value; print_string ")") ctors @@ -706,7 +688,9 @@ and lexp_context_print ctx = 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; + (match exp with + | None -> print_string "<var>" + | Some exp -> lexp_print_adv (false, 0, true) exp); print_string ": "; lexp_print_adv (false, 0, true) tp; print_string "\n" @@ -738,8 +722,9 @@ let lexp_print e = lexp_print_adv (false, 0, true) e;; (* add dummy definition helper *) let add_def name ctx = - let ctx = senv_add_var name dloc ctx in - env_add_var_info (0, (dloc, name), dlxp, dlxp) ctx + let var = (dloc, name) in + let ctx = senv_add_var var ctx in + env_add_var_info (0, var, None, dlxp) ctx ;; ===================================== tests/debug.ml ===================================== --- a/tests/debug.ml +++ b/tests/debug.ml @@ -159,7 +159,6 @@ let debug_pexp_print_all pexps = (* Print lexp with debug info *) let debug_lexp_print tlxp = print_string " "; - let dloc = dummy_location in let print_info msg loc lex = print_string msg; print_string "["; print_loc loc; View it on GitLab: https://gitlab.com/monnier/typer/commit/bc4698bc8d534e53471380285d41375c96d…

1 0

"tests" subdir
by Stefan Monnier 25 Mar '16

25 Mar '16

Je pense qu'une partie du code dans "tests" devrait être déplacé dans "src". On ne devrait garder dans "tests" que le code qui est spécifique aux tests (voire même, seulement le code des tests eux-mêmes). Par exemple tout ce qui est de "ityper" devrait être dans "src" vu que "ityper" est utile indépendemment des tests. Stefan

1 0

[Git][monnier/typer][master] Fix compilation yet again; Fix the "executable bit" in various files
by Stefan 25 Mar '16

25 Mar '16

Stefan pushed to branch master at Stefan / Typer Commits: 6fa07a98 by Stefan Monnier at 2016-03-24T17:15:11-04:00 Fix compilation yet again; Fix the "executable bit" in various files * tests/REPL.ml (ieval): Fix type error. * src/eval.ml (eval_all): Reduce redundancy. - - - - - 13 changed files: - DESIGN - GNUmakefile - − _tags - − side-effects - src/debruijn.ml - src/eval.ml - src/fmt.ml - src/grammar.ml - src/lexp.ml - src/prelexer.ml - tests/REPL.ml - tests/debug.ml - tests/full_debug.ml Changes: ===================================== DESIGN ===================================== --- a/DESIGN +++ b/DESIGN @@ -1616,6 +1616,7 @@ Or almost: with these classical definitions we cannot prove the classical axiom of choice as a theorem, so if you need it, you have to add it as an axiom. * Papers +** BigBang: Designing a statically typed scripting language ** Dependently typed Racket ** Dependently typed Haskell "My dissertation (github.com/goldfirere/thesis) is about adding dependent ===================================== GNUmakefile ===================================== --- a/GNUmakefile +++ b/GNUmakefile ===================================== _tags deleted ===================================== --- a/_tags +++ /dev/null ===================================== side-effects deleted ===================================== --- a/side-effects +++ /dev/null @@ -1 +0,0 @@ -../papers/side-effects \ No newline at end of file ===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml ===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -439,10 +439,8 @@ let debug_eval lxp ctx = (* Eval a list of lexp *) let eval_all lxps rctx silent = - if silent then - List.map (fun g -> eval g rctx) lxps - else - List.map (fun g -> debug_eval g rctx) lxps;; + let evalfun = if silent then eval else debug_eval in + List.map (fun g -> evalfun g rctx) lxps;; (* Eval String * ---------------------- *) ===================================== src/fmt.ml ===================================== --- a/src/fmt.ml +++ b/src/fmt.ml ===================================== src/grammar.ml ===================================== --- a/src/grammar.ml +++ b/src/grammar.ml ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml ===================================== src/prelexer.ml ===================================== --- a/src/prelexer.ml +++ b/src/prelexer.ml @@ -1,6 +1,6 @@ (* prelexer.ml --- First half of lexical analysis of Typer. -Copyright (C) 2011-2012 Free Software Foundation, Inc. +Copyright (C) 2011-2012, 2016 Free Software Foundation, Inc. Author: Stefan Monnier <monnier(a)iro.umontreal.ca> Keywords: languages, lisp, dependent types. @@ -134,17 +134,18 @@ let rec prelex (file : string) (fin : in_channel) ln ctx acc | ((ln, cpos, _, _) :: ctx) -> (prelexer_error {file=file; line=ln; column=cpos} "Unmatched opening brace"; List.rev acc) - - + + 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 = + * really matters. Plus it will make testing easier. *) +let prelex_string str = + (* FIXME: we should use a proper temp file (e.g. with mktemp). *) let fin = open_out "_temp_hack" in output_string fin str; (flush_all); @@ -162,8 +163,3 @@ let rec pretokens_print pretokens = | Prestring(_, str) -> print_string "\""; print_string str; print_string "\"") pretokens - - - - - \ No newline at end of file ===================================== tests/REPL.ml ===================================== --- a/tests/REPL.ml +++ b/tests/REPL.ml @@ -1,3 +1,24 @@ +(* REPL.ml --- Read Eval Print Loop (REPL) + +Copyright (C) 2016 Pierre Delaunay + +Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> + +This file is part of Typer. + +Typer is free software; you can redistribute it and/or modify it under the +terms of the GNU General Public License as published by the Free Software +Foundation, either version 3 of the License, or (at your option) any +later version. + +Typer is distributed in the hope that it will be useful, but WITHOUT ANY +WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS +FOR A PARTICULAR PURPOSE. See the GNU General Public License for +more details. + +You should have received a copy of the GNU General Public License along with +this program. If not, see <http://www.gnu.org/licenses/>. *) + (* * Description: * Read Eval Print Loop (REPL). It allows you to eval typer code @@ -13,7 +34,7 @@ * . a + b; * Out[ 3] >> 6 * - * --------------------------------------------------------------------------- *) + * -------------------------------------------------------------------------- *) open Debug @@ -99,7 +120,7 @@ let ilexp_parse pexps lctx = let ieval lexps rctx = let (ldecls, lexprs) = lexps in let rctx = eval_decls ldecls rctx in - let vals = eval_all lexprs rctx in + let vals = eval_all lexprs rctx false in vals, rctx ;; ===================================== tests/debug.ml ===================================== --- a/tests/debug.ml +++ b/tests/debug.ml ===================================== tests/full_debug.ml ===================================== --- a/tests/full_debug.ml +++ b/tests/full_debug.ml View it on GitLab: https://gitlab.com/monnier/typer/commit/6fa07a985f46b2881ed04a3c603b1c31672…

1 0

[Git][monnier/typer][master] 2 commits: eval removes old temporary variables from ctx between function calls
by Setepenre 24 Mar '16

24 Mar '16

Setepenre pushed to branch master at Stefan / Typer Commits: cdec9d9a by Pierre Delaunay at 2016-03-23T23:37:17-04:00 eval removes old temporary variables from ctx between function calls Changes to be committed: * src/debruijn.ml : rollback, old dbi were correct * src/eval.ml : - ctx is reinitialized between calls - new function debug_eval (equiv to old eval) - eval does not print call_trace and context if an error is raised * tests/eval_test.ml : test ctx reinit * tests/full_debug.ml: use debug_eval instead of eval - - - - - bd7fd362 by Pierre Delaunay at 2016-03-23T23:47:47-04:00 All tests are passed - Recursion with case are working Changes to be committed: * minor modifications - - - - - 5 changed files: - − samples/test__.typer - src/debruijn.ml - src/eval.ml - tests/eval_test.ml - tests/full_debug.ml Changes: ===================================== samples/test__.typer deleted ===================================== --- a/samples/test__.typer +++ /dev/null @@ -1,61 +0,0 @@ - - - -%a = lambda x -> -% let a1 : Nat; a1 = 2; b1 : Nat; b1 = 3; in -% a1 + b1 + x -%; - -% main = (a 2) - - -a = 2; - -Nat = inductive_ (dNat) (zero) (succ Nat); - -zero = inductive-cons Nat zero; -succ = inductive-cons Nat succ; - -one = (succ zero); -two = (succ one); -three = (succ two); - -tonum = lambda x -> case x - | (succ y) => (1 + (tonum y)) - | _ => 0 -; - -x = zero; -% main = zero; => zero(Nat[1]) -% main = x; => succ(Nat[2]) - -main = (tonum one); - - - -%================================ CALL TRACE ================================ -% size = 6 -%---------------------------------------------------------------------------- -%|+- Call: (tonum[1] zero[6]) -%|:+- Var: zero[6] -%|:+- Lambda: lambda (x: unkwn) -> case x[0]: unkwn| succ y -> 1 + (tonum[4] y[0]); | zero -> 0; -%|:|+- Case: case x[0]: unkwn| succ y -> 1 + (tonum[4] y[0]); | zero -> 0; -%|:|:+- Var: x[0] -%|:|:+- Imm: 0 -%============================================================================ - -%================================ CALL TRACE ================================ -% size = 11 -%---------------------------------------------------------------------------- -%|+- Call: (tonum[2] x[1]) -%|:+- Var: x[1] -%|:+- Lambda: lambda (x: unkwn) -> case x[0]: unkwn| succ y -> 1 + (tonum[2] y[0]); | _ -> 0; -%|:|+- Case: case x[0]: unkwn| succ y -> 1 + (tonum[2] y[0]); | _ -> 0; -%|:|:+- Var: x[0] -%|:|:+- Var: zero[6] -%|:|:+- Call: 1 + (tonum[2] y[0]) -%|:|:|+- Imm: 1 -%|:|:|+- Call: (tonum[2] y[0]) -%|:|:|:+- Var: y[0] -%|:|:|:+- Var: zero[6] -%============================================================================ ===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -90,11 +90,11 @@ let temp_scope ctx bound = let (a, b, c) = ctx in (a, b, bound) (* return its current DeBruijn index *) let rec senv_lookup (name: string) (ctx: lexp_context): int = let ((n, map), _, (csize, rof)) = ctx in - let raw_idx = n - (StringMap.find name map) - 1 in + let raw_idx = n - (StringMap.find name map) - 1 in (* if raw_idx > (n - csize) then raw_idx - rof (* Shift if the variable is not bound *) - else - raw_idx + else *) + raw_idx ;; (* We first add variable into our map. Later on, we will add them into ===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -48,12 +48,6 @@ let eval_error loc msg = let dloc = dummy_location 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 print_myers_list l print_fun = let n = (length l) - 1 in @@ -70,6 +64,18 @@ let print_myers_list l print_fun = print_string (make_sep '='); ;; +let print_rte_ctx ctx = + let (l, b) = ctx in + print_myers_list l + (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") +;; + + let get_int lxp = match lxp with | Imm(Integer(_, l)) -> l @@ -77,43 +83,77 @@ let get_int lxp = ;; (* Runtime Environ *) -type runtime_env = (string option * lexp) myers -let make_runtime_ctx = nil;; -let add_rte_variable name x l = (cons (name, x) l);; +type runtime_env = ((string option * lexp) myers) * (int * int) + +let make_runtime_ctx = (nil, (0, 0));; -let get_rte_variable (*name: string option*) (idx: int) (l: runtime_env): lexp = - (* FIXME: Check that the variable's name is right! *) - let (tn, x) = (nth idx l) in x +let add_rte_variable name x ctx = + let (l, b) = ctx in + let lst = (cons (name, x) l) in + (lst, b);; - (* +let get_rte_variable (name: string option) (idx: int) (ctx: runtime_env): lexp = + let (l, _) = ctx in + let (tn, x) = (nth idx l) in match (tn, name) with - | (Some n1, Some n2) -> - if n1 = n2 then x else (eval_error dloc - ("Variable lookup failure. Expected: " ^ n2 ^ " got " ^ n1); x) - | _ -> x (* can't check variable's name *) *) + | (Some n1, Some n2) -> ( + if n1 = n2 then + x + else ( + eval_error dloc + ("Variable lookup failure. Expected: \"" ^ n2 ^ "\" got \"" ^ n1 ^ "\""))) + + | _ -> x (* can't check variable's name (call args do not have names) *) ;; -let get_rte_size (l: runtime_env): int = length l;; +let get_rte_size (ctx: runtime_env): int = let (l, b) = ctx in length l;; -let print_rte_ctx l = print_myers_list l - (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") +(* This function is used when we enter a new scope *) +let local_ctx ctx = + let (l, _) = ctx in + let osize = length l in + (l, (osize, 0)) ;; +let select_n ctx n = + let (l, a) = ctx in + let r = ref nil in + let s = (length l) - 1in + + for i = 0 to n - 1 do + r := (cons (nth (s - i) l) (!r)); + done; + + ((!r), a) + +let temp_ctx ctx = + let (l, (osize, _)) = ctx in + let tsize = length l in + (* Check if temporary variables are present *) + if tsize != osize then + (* remove temp var *) + (select_n ctx osize) + else + ctx +;; let nfirst_rte_var n ctx = let rec loop i acc = if i < n then - loop (i + 1) ((get_rte_variable i ctx)::acc) + loop (i + 1) ((get_rte_variable None i ctx)::acc) else List.rev acc in loop 0 [] ;; +type call_trace_type = (int * lexp) list + +let global_trace = ref [] +let global_env = ref (nil, (0, 0)) +let _eval_max_recursion_depth = ref 255 + +let add_call cll i = global_trace := (i, cll)::!global_trace + (* currently, we don't do much *) type value_type = lexp @@ -121,10 +161,12 @@ type value_type = lexp * 'i' is the recursion depth used to print the call trace *) let rec _eval lxp ctx i: (value_type) = - (if i > 255 then + (if i > (!_eval_max_recursion_depth) then raise (internal_error "Recursion Depth exceeded")); add_call lxp i; + global_env := ctx; (* Allow us to print the latest used environment *) + match lxp with (* This is already a leaf *) | Imm(v) -> lxp @@ -132,18 +174,18 @@ let rec _eval lxp ctx i: (value_type) = (* Return a value stored in the environ *) | Var((loc, name), idx) as e -> begin (* find variable binding i.e we do not want a another variable *) - let rec var_crawling expr i k = + let rec var_crawling expr k = (if k > 255 then( lexp_print expr; print_string "\n"; flush stdout; raise (internal_error "Variable lookup failed"))); match expr with - | Var(_, j) -> - let p = (get_rte_variable (i + j) ctx) in - var_crawling p (i + j) (k + 1) + | 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 0) + (var_crawling e 0) with Not_found -> print_string ("Variable: " ^ name ^ " was not found | "); @@ -154,11 +196,13 @@ let rec _eval lxp ctx i: (value_type) = | Let(_, decls, inst) -> (* First we _evaluate all declaration then we eval the instruction *) let nctx = build_ctx decls ctx i in - _eval inst nctx (i + 1) + _eval inst (local_ctx nctx) (i + 1) (* Function call *) | Call (lname, args) -> ( - (* Try to extract name *) + (* create a clean environment *) + let clean_ctx = temp_ctx ctx in + let n = List.length args in match lname with (* Hardcoded functions *) @@ -170,9 +214,9 @@ let rec _eval lxp ctx i: (value_type) = | Var((_, name), _) when name = "_+_" -> 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 - Imm(Integer(dloc, l + r)) + 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 = "_*_" -> @@ -181,17 +225,23 @@ let rec _eval lxp ctx i: (value_type) = 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)) + Imm(Integer(dloc, v)) (* This is a named function call *) | Var((_, name), idx) -> - (* get function body *) - let body = get_rte_variable idx ctx in + (* get function body from current context *) + let body = get_rte_variable (Some name) idx ctx in - (* Add args in the scope *) - let nctx = build_arg_list args ctx i in - _eval body nctx (i + 1) + (* _eval every args using current context *) + let arg_val = + List.map (fun (k, e) -> _eval e ctx (i + 1)) args in + + (* 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 *) @@ -203,8 +253,11 @@ let rec _eval lxp ctx i: (value_type) = (* handle partial application i.e build a new lambda if Partial App *) | Lambda(_, vr, _, body) -> begin let (loc, name) = vr in - (* Get first arg *) - let value = (get_rte_variable 0 ctx) in + + (* 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 *) @@ -213,14 +266,14 @@ let rec _eval lxp ctx i: (value_type) = | Lambda(_, vr, _, body) -> let (loc, name) = vr in (* Get Variable from call context *) - let value = (get_rte_variable idx ctx) in + 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 nctx (i + 1) end + 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 @@ -234,16 +287,19 @@ let rec _eval lxp ctx i: (value_type) = (* 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 | Var((_, ctor_name), _) -> ctor_name, args | _ -> eval_error loc "Target is not a Constructor" ) - | Cons((_, idx), (_, cname)) -> begin + | Cons(((_, vname), idx), (_, cname)) -> begin (* retrieve type definition *) - - let info = get_rte_variable idx ctx in + 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 @@ -275,6 +331,13 @@ let rec _eval lxp ctx i: (value_type) = 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 @@ -283,12 +346,21 @@ let rec _eval lxp ctx i: (value_type) = (* 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 cl -> + let nctx = List.fold_left2 (fun nctx pat arg -> match pat with | None -> nctx - | Some (_, (_, name)) -> let (_, xp) = cl in - add_rte_variable (Some name) xp 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 *) @@ -324,7 +396,8 @@ and eval_decls (decls: ((vdef * lexp * ltype) list)) let nctx = add_rte_variable (Some n) lxp ctx in loop tl nctx in - loop decls ctx + let nctx = loop decls ctx in + (local_ctx nctx) and print_eval_result i lxp = print_string " Out["; @@ -352,26 +425,34 @@ and print_call_trace () = ;; let eval lxp ctx = + global_trace := []; + _eval lxp ctx 1 + +let debug_eval lxp ctx = try - _eval lxp ctx 1 + eval lxp ctx with e -> ( - print_rte_ctx ctx; + print_rte_ctx (!global_env); print_call_trace (); raise e) ;; (* Eval a list of lexp *) -let eval_all lxps rctx = - global_trace := []; - List.map (fun g -> eval g rctx) lxps;; +let eval_all lxps rctx silent = + if silent then + List.map (fun g -> eval g rctx) lxps + else + List.map (fun g -> debug_eval g rctx) lxps;; (* Eval String * ---------------------- *) -let eval_expr_str str lctx rctx = +let _eval_expr_str str lctx rctx silent = let lxps = lexp_expr_str str lctx in - (eval_all lxps rctx) + (eval_all lxps rctx silent) ;; +let eval_expr_str str lctx rctx = _eval_expr_str str lctx rctx false + let eval_decl_str str lctx rctx = let lxps, lctx = lexp_decl_str str lctx in (eval_decls lxps rctx), lctx ===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -1,50 +1,51 @@ open Lparse (* add_def *) open Debruijn (* make_lexp_context *) open Eval (* make_rte_ctx *) -open Utest_lib +open Utest_lib +open Util +open Lexp (* default environment *) let lctx = make_lexp_context let lctx = add_def "_+_" lctx let lctx = add_def "_*_" lctx -let rctx = make_runtime_ctx -let rctx = add_rte_variable (Some "_+_") dlxp rctx -let rctx = add_rte_variable (Some "_-_") dlxp rctx - - +let rctx = make_runtime_ctx +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 () -> - + let dcode = " - a = 10; - b = a; - c = b; + a = 10; + b = a; + c = b; d = c;" in - + let rctx, lctx = eval_decl_str dcode lctx rctx in - + let ecode = "d;" in - + let ret = eval_expr_str ecode lctx rctx in - + match ret with | [r] -> expect_equal_int (get_int r) 10 | _ -> failure ()) );; - - + + (* Let * ------------------------ *) - + let _ = (add_test "EVAL" "Let" (fun () -> (* Noise. Makes sure the correct variables are selected *) let dcode = " c = 3; e = 1; f = 2; d = 4;" in let rctx, lctx = eval_decl_str dcode lctx rctx in - + let ecode = " let a = 10; x = 50; y = 60; b = 20; in a + b;" in - + let ret = eval_expr_str ecode lctx rctx in (* Expect a single result *) match ret with @@ -59,7 +60,7 @@ let _ = (add_test "EVAL" "Let" (fun () -> let _ = (add_test "EVAL" "Lambda" (fun () -> (* Declare lambda *) let rctx, lctx = eval_decl_str "sqr = lambda x -> x * x;" lctx rctx in - + (* Eval defined lambda *) let ret = eval_expr_str "(sqr 4);" lctx rctx in (* Expect a single result *) @@ -72,11 +73,11 @@ let _ = (add_test "EVAL" "Lambda" (fun () -> let _ = (add_test "EVAL" "Nested Lambda" (fun () -> let code = " sqr = lambda x -> x * x; - cube = lambda x -> x * (sqr x); " in - + cube = lambda x -> x * (sqr x);" in + (* Declare lambda *) let rctx, lctx = eval_decl_str code lctx rctx in - + (* Eval defined lambda *) let ret = eval_expr_str "(cube 4);" lctx rctx in (* Expect a single result *) @@ -86,22 +87,42 @@ 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 () -> + let code = " + infinity = lambda beyond -> (infinity beyond);" in + + let rctx, lctx = eval_decl_str code lctx rctx in + + (* Expect throwing *) + try (* use the silent version as an error will be thrown *) + let _ = _eval_expr_str "(infinity 0);" lctx rctx true in + failure () + with + Internal_error m -> + if m = "Recursion Depth exceeded" then + success () + else + failure () +));; + (* Cases + Inductive types * ------------------------ *) - + let _ = (add_test "EVAL" "Case" (fun () -> (* Inductive type declaration + Noisy declarations *) let code = " i = 90;\n idt = inductive_ (idtd) (ctr0) (ctr1 idt) (ctr2 idt) (ctr3 idt);\n j = 100;\n - + d = 10;\n ctr0 = inductive-cons idt ctr0;\n e = 20;\n ctr1 = inductive-cons idt ctr1;\n f = 30;\n ctr2 = inductive-cons idt ctr2;\n g = 40;\n ctr3 = inductive-cons idt ctr2;\n h = 50;\n - + x = 1;\n a = (ctr1 (ctr2 ctr0));\n y = 2;\n b = (ctr2 (ctr2 ctr0));\n z = 3;\n @@ -111,17 +132,17 @@ let _ = (add_test "EVAL" "Case" (fun () -> | ctr1 l => 1\n | ctr2 l => 2\n | _ => 3;\n" in - + let rctx, lctx = eval_decl_str code lctx rctx in - + let rcode = "(test_fun a); (test_fun b); (test_fun c)"in - + (* Eval defined lambda *) let ret = eval_expr_str rcode lctx rctx in (* Expect 3 results *) match ret with - | [a; b; c] -> - let t1 = expect_equal_int (get_int a) 1 in + | [a; b; c] -> + let t1 = expect_equal_int (get_int a) 1 in let t2 = expect_equal_int (get_int b) 2 in let t3 = expect_equal_int (get_int c) 3 in if t1 = 0 && t2 = 0 && t3 = 0 then @@ -138,28 +159,28 @@ let _ = (add_test "EVAL" "Recursive Call" (fun () -> let code = " a = 1;\n Nat = inductive_ (dNat) (zero) (succ Nat); b = 2;\n - + zero = inductive-cons Nat zero; c = 3;\n succ = inductive-cons Nat succ; d = 4;\n - + one = (succ zero); e = 5;\n two = (succ one); f = 6;\n three = (succ three); g = 7;\n - tonum = lambda x -> case x + tonum = lambda x -> case x | (succ y) => (1 + (tonum y)) - | _ => 0;" in - + | zero => 0;" in + let rctx, lctx = eval_decl_str code lctx rctx in - - let rcode = "(tonum zero); (tonum zero); (tonum zero);"in - + + let rcode = "(tonum zero); (tonum one); (tonum two);"in + (* Eval defined lambda *) let ret = eval_expr_str rcode lctx rctx in (* Expect a 3 results *) match ret with - | [a; b; c] -> - let t1 = expect_equal_int (get_int a) 0 in + | [a; b; c] -> + let t1 = expect_equal_int (get_int a) 0 in let t2 = expect_equal_int (get_int b) 1 in let t3 = expect_equal_int (get_int c) 2 in if t1 = 0 && t2 = 0 && t3 = 0 then ===================================== tests/full_debug.ml ===================================== --- a/tests/full_debug.ml +++ b/tests/full_debug.ml @@ -81,7 +81,7 @@ let arg_defs = [ add_p_option "sexp" (); add_p_option "pexp" (); add_p_option "lexp" ()), - " Print all compilation step with debug info"); + " Print all debug info"); ];; let parse_args () = @@ -172,9 +172,9 @@ let main () = (* Push main args here if any *) (* get main body *) - let body = (get_rte_variable main rctx) in + let body = (get_rte_variable (Some "main") main rctx) in (* eval main *) - let r = (eval body rctx) in + let r = (debug_eval body rctx) in print_eval_result 0 r with View it on GitLab: https://gitlab.com/monnier/typer/compare/aa416638d2073a688f3c9cb00e27bcbe9d…

1 0

[Git][monnier/typer][master] 3 commits: bound is inside lexp_ctx
by Setepenre 23 Mar '16

23 Mar '16

Setepenre pushed to branch master at Stefan / Typer Commits: 2e53f40d by Pierre Delaunay at 2016-03-22T18:41:03-04:00 bound is inside lexp_ctx - - - - - db4f6c1e by Pierre Delaunay at 2016-03-22T19:51:41-04:00 ityper can interpret files before REPL - - - - - aa416638 by Pierre Delaunay at 2016-03-23T11:41:25-04:00 add arg parsing for ityper and full_debug Changes to be committed: * GNUmakefile : new option "make tests", build tests and run them * tests/REPL.ml : files can be interpreted to populate environments * tests/full_debug.ml : we can choose how much info we want to print - - - - - 10 changed files: - GNUmakefile - src/debruijn.ml - src/eval.ml - src/lparse.ml - tests/REPL.ml - tests/debug.ml - tests/full_debug.ml - tests/lexp_test.ml - tests/pexp_test.ml - tests/utest_lib.ml Changes: ===================================== GNUmakefile ===================================== --- a/GNUmakefile +++ b/GNUmakefile @@ -6,17 +6,14 @@ TEST_FILES := $(wildcard ./tests/*_test.ml) CFLAG = -cflag -rectypes -build-dir _build -# This is for windows: windows version is old - - all: ityper typer debug tests -typer: +typer: ocamlbuild src/main.native $(CFLAG) @mv _build/src/main.native _build/typer # debug file eval -debug: +debug: ocamlbuild tests/full_debug.native -I src $(CFLAG) @mv _build/tests/full_debug.native _build/full_debug @@ -25,7 +22,7 @@ ityper: ocamlbuild tests/REPL.native -I src $(CFLAG) @mv _build/tests/REPL.native _build/ityper -tests-build: +tests-build: # ============================ # Build tests # ============================ @@ -39,7 +36,9 @@ tests-run: # ============================ @./_build/tests/utests -# Make language doc +tests: tests-build tests-run + +# Make language doc doc-tex: texi2pdf ./doc/manual.texi --pdf --build=clean @@ -49,6 +48,6 @@ doc-ocaml: # everything is expected to be compiled in the "./_build/" folder clean: - -rm -rf _build + -rm -rf _build .PHONY: ityper typer debug tests ===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -52,70 +52,71 @@ module StringMap = Map.Make (struct type t = string let compare = String.compare end) ;; - (* Map matching variable name and its distance in the current scope *) type scope = (int) StringMap.t (* Map<String, int>*) type senv_length = int (* it is not the map true length *) type senv_type = senv_length * scope - (* name -> index * index -> info *) -type lexp_context = senv_type * env_type + (* name -> index * index -> info * (outer_size, r_offset) *) +type lexp_context = senv_type * env_type * (int * int) -(* internal definitions: DO NOT USE +(* internal definitions * ---------------------------------- *) let _make_scope = StringMap.empty;; let _make_senv_type = (0, _make_scope);; let _make_myers = nil +let _get_env(ctx: lexp_context): env_type = let (_, ev, _) = ctx in ev ;; -let _get_senv (ctx: lexp_context) = - let (ct, _) = ctx in ct -;; +(* Public methods: DO USE + * ---------------------------------- *) -let _get_scope(ctx: lexp_context): scope = - let ((_, ev), _) = ctx in ev -;; +let make_lexp_context = (_make_senv_type, _make_myers, (0, 0));; -let _get_env(ctx: lexp_context): env_type = - let (_, ev) = ctx in ev -;; +let get_roffset ctx = let (_, _, (_, rof)) = ctx in rof;; -let _add_var_env variable ctx = - let (a, env) = ctx in cons variable env +(* Enter a local scope such as let *) +let local_scope ctx pos = + let ((l, map), b, c) = ctx in + (* Check size *) + let n = (length b) in + ((l, map), b, (l, pos)) ;; -(* Public methods: DO USE - * ---------------------------------- *) - -let make_lexp_context = (_make_senv_type, _make_myers);; +(* Enter a temporary scope such as Calls *) +let temp_scope ctx bound = let (a, b, c) = ctx in (a, b, bound) (* return its current DeBruijn index *) let rec senv_lookup (name: string) (ctx: lexp_context): int = - let ((n, map), _) = ctx in - n - (StringMap.find name map) - 1 + let ((n, map), _, (csize, rof)) = ctx in + let raw_idx = n - (StringMap.find name map) - 1 in + if raw_idx > (n - csize) then + raw_idx - rof (* Shift if the variable is not bound *) + else + raw_idx ;; (* We first add variable into our map. Later on, we will add them into * the environment. The reason for this is that the type info is * known after lexp parsing which need the index fist *) let senv_add_var name loc ctx = - let ((n, map), e) = ctx in + let ((n, map), e, f) = ctx in try - let idx = senv_lookup name ctx in + let _ = senv_lookup name ctx in debruijn_warning loc ("Variable Shadowing " ^ name); let nmap = StringMap.add name n map in - ((n + 1, nmap), e) + ((n + 1, nmap), e, f) with Not_found -> let nmap = StringMap.add name n map in - ((n + 1, nmap), e) + ((n + 1, nmap), e, f) ;; (* *) let env_add_var_info var (ctx: lexp_context) = - let (a, env) = ctx in - (a, cons var env) + let (a, env, f) = ctx in + (a, cons var env, f) ;; let env_lookup_type_by_index index ctx = @@ -135,5 +136,7 @@ let env_lookup_type ctx (v : vref) = internal_error "DeBruijn index refers to wrong name!" with Not_found -> internal_error "DeBruijn index out of bounds!" -let env_lookup_by_index index ctx = Myers.nth index (_get_env ctx);; +let env_lookup_by_index index (ctx: lexp_context): env_elem = + Myers.nth index (_get_env ctx) +;; ===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -40,20 +40,19 @@ open Debruijn open Grammar -let _eval_error loc msg = - msg_error "eval" loc msg; +let eval_error loc msg = + msg_error "EVAL" loc msg; raise (internal_error msg) ;; let dloc = dummy_location -let _eval_warning = msg_warning "eval" +let eval_warning = msg_warning "EVAL" type call_trace_type = (int * lexp) list let global_trace = ref [] let add_call cll i = global_trace := (i, cll)::!global_trace -let reinit_call_trace () = global_trace := [] let print_myers_list l print_fun = let n = (length l) - 1 in @@ -71,12 +70,6 @@ let print_myers_list l print_fun = print_string (make_sep '='); ;; -let get_function_name fname = - match fname with - | Var(v) -> let ((loc, name), idx) = v in name - | _ -> "Name Lookup failure" -;; - let get_int lxp = match lxp with | Imm(Integer(_, l)) -> l @@ -88,9 +81,16 @@ type runtime_env = (string option * lexp) myers let make_runtime_ctx = nil;; let add_rte_variable name x l = (cons (name, x) l);; -let get_rte_variable (idx: int) (l: runtime_env): lexp = +let get_rte_variable (*name: string option*) (idx: int) (l: runtime_env): lexp = (* FIXME: Check that the variable's name is right! *) - let (_, x) = (nth idx l) in x + let (tn, x) = (nth idx l) in x + + (* + match (tn, name) with + | (Some n1, Some n2) -> + if n1 = n2 then x else (eval_error dloc + ("Variable lookup failure. Expected: " ^ n2 ^ " got " ^ n1); x) + | _ -> x (* can't check variable's name *) *) ;; let get_rte_size (l: runtime_env): int = length l;; @@ -207,8 +207,8 @@ let rec _eval lxp ctx i: (value_type) = let value = (get_rte_variable 0 ctx) in let nctx = add_rte_variable (Some name) value ctx in - (* Collapse nested lambdas *) - let rec build_body bd idx nctx = + (* Collapse nested lambdas. Returns body *) + let rec collapse bd idx nctx = match bd with | Lambda(_, vr, _, body) -> let (loc, name) = vr in @@ -216,10 +216,10 @@ let rec _eval lxp ctx i: (value_type) = let value = (get_rte_variable idx ctx) in (* Build lambda context *) let nctx = add_rte_variable (Some name) value nctx in - (build_body body (idx + 1) nctx) + (collapse body (idx + 1) nctx) | _ -> bd, nctx in - let body, nctx = build_body body 1 nctx in + let body, nctx = collapse body 1 nctx in _eval body nctx (i + 1) end (* Inductive is a type declaration. We have nothing to eval *) @@ -233,28 +233,30 @@ let rec _eval lxp ctx i: (value_type) = (* Eval target *) let v = _eval target ctx (i + 1) in - let nctx = ctx in (* V must be a constructor Call *) let ctor_name, args = match v with | Call(lname, args) -> (match lname with | Var((_, ctor_name), _) -> ctor_name, args - | _ -> _eval_error loc "Target is not a Constructor" ) + | _ -> eval_error loc "Target is not a Constructor" ) | Cons((_, idx), (_, cname)) -> begin (* retrieve type definition *) - print_int idx; + let info = get_rte_variable idx ctx in - let Inductive(_, _, _, ctor_def) = info in + let ctor_def = match info with + | Inductive(_, _, _, c) -> c + | _ -> eval_error loc "Not an Inductive Type" in + try let args = SMap.find cname ctor_def in cname, args with Not_found -> - _eval_error loc "Constructor does not exist" end + eval_error loc "Constructor does not exist" end | _ -> lexp_print target; print_string "\n"; lexp_print v; print_string "\n"; - _eval_error loc "Can't match expression" in + eval_error loc "Can't match expression" in (* Check if a default is present *) let run_default df = @@ -336,7 +338,8 @@ and print_call_trace () = print_string (make_title " CALL TRACE "); let n = List.length !global_trace in - print_string " size = "; print_int n; print_string "\n"; + print_string " size = "; print_int n; + print_string (" max_printed = 50" ^ "\n"); print_string (make_sep '-'); let racc = List.rev !global_trace in @@ -358,12 +361,13 @@ let eval lxp ctx = ;; (* Eval a list of lexp *) -let eval_all lxps rctx = List.map (fun g -> eval g rctx) lxps;; +let eval_all lxps rctx = + global_trace := []; + List.map (fun g -> eval g rctx) lxps;; (* Eval String * ---------------------- *) let eval_expr_str str lctx rctx = - global_trace := []; let lxps = lexp_expr_str str lctx in (eval_all lxps rctx) ;; ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -105,18 +105,9 @@ let default_lctx = * possible for env to hold more variables than senv since senv is a map * which does not allow multiple definition while env does. * - * a = 1; - * let a = 3; b = 5 in a + b; - * *) -let rec lexp_parse p ctx: lexp = - _lexp_parse p ctx (0, 0) - -(* bound is used to determine if the variable require shifting - * bound = (inner_size, r_offset) - *) -and _lexp_parse (p: pexp) (ctx: lexp_context) bound: lexp = +let rec lexp_parse (p: pexp) (ctx: lexp_context): lexp = (* So I don't have to extract it *) let tloc = pexp_location p in match p with @@ -127,12 +118,8 @@ and _lexp_parse (p: pexp) (ctx: lexp_context) bound: lexp = | Pvar (loc, name) -> begin try (* Send Variable loc *) - let (isize, rof) = bound in - let idx = senv_lookup name ctx in( - if idx > isize then - (make_var name (idx - rof) loc) - else - (make_var name idx loc)) + let idx = senv_lookup name ctx in + (make_var name idx loc) with Not_found -> (lexp_error loc ("The Variable: " ^ name ^ " was not declared"); @@ -142,22 +129,19 @@ and _lexp_parse (p: pexp) (ctx: lexp_context) bound: lexp = (* Let, Variable declaration + local scope *) | Plet(loc, decls, body) -> let decl, nctx = lexp_decls decls ctx in - (* Body cannot modify context *) - let (_, rof) = bound in - let bound = ((List.length decl), rof) in - let bdy = _lexp_parse body nctx bound in + let bdy = lexp_parse body (local_scope nctx (get_roffset nctx)) in Let(tloc, decl, bdy) (* ->/=> *) | Parrow (kind, Some var, tp, loc, expr) -> let nvar = var in (* /!\ HERE *) - let ltyp = _lexp_parse tp ctx bound in - let lxp = _lexp_parse expr ctx bound in + let ltyp = lexp_parse tp ctx in + let lxp = lexp_parse expr ctx in Arrow(kind, Some nvar, ltyp, tloc, lxp) | Parrow (kind, None, tp, loc, expr) -> - let ltyp = _lexp_parse tp ctx bound in - let lxp = _lexp_parse expr ctx bound in + let ltyp = lexp_parse tp ctx in + let lxp = lexp_parse expr ctx in Arrow(kind, None, ltyp, tloc, lxp) (* *) @@ -169,10 +153,10 @@ and _lexp_parse (p: pexp) (ctx: lexp_context) bound: lexp = let nctx = senv_add_var vname loc ctx in let nctx = env_add_var_info (0, (loc, vname), dlxp, ltp) nctx in - let ltyp = _lexp_parse ptype nctx bound in - let (_, rof) = bound in - let bound = (1, rof) in - let lbody = _lexp_parse body nctx bound in + let ltyp = lexp_parse ptype nctx in + + let nctx = (local_scope nctx (get_roffset nctx)) in + let lbody = lexp_parse body nctx in Lambda(kind, var, ltyp, lbody) | Plambda (kind, var, None, body) -> @@ -181,29 +165,27 @@ and _lexp_parse (p: pexp) (ctx: lexp_context) bound: lexp = let nctx = senv_add_var vname loc ctx in let nctx = env_add_var_info (0, (loc, vname), dlxp, dltype) nctx in - let (_, rof) = bound in - let bound = (1, rof) in - let lbody = _lexp_parse body nctx bound in + let nctx = (local_scope nctx (get_roffset nctx)) in + let lbody = lexp_parse body nctx in Lambda(kind, var, UnknownType(tloc), lbody) | Pcall (fname, _args) -> - lexp_call fname _args ctx bound + lexp_call fname _args ctx (* Pinductive *) | Pinductive (label, [], ctors) -> - let map_ctor, nctx = lexp_parse_constructors ctors ctx bound in - Inductive(tloc, label, [], map_ctor) + let map_ctor, nctx = lexp_parse_constructors ctors ctx in + Inductive(tloc, label, [], map_ctor) (* Pcons *) | Pcons(vr, sym) -> ( let (loc, type_name) = vr in let (_, ctor_name) = sym in - let (isize, rof) = bound in (* An inductive type named type_name must be in the environment *) try let idx = senv_lookup type_name ctx in (* Check if the constructor exists *) (* TODO *) - Cons((vr, idx - rof), sym) + Cons((vr, idx), sym) with Not_found -> lexp_error loc ("The inductive type: " ^ type_name ^ " was not declared"); @@ -213,7 +195,7 @@ and _lexp_parse (p: pexp) (ctx: lexp_context) bound: lexp = | Pcase (loc, target, patterns) -> (* I need type info HERE *) - let lxp = _lexp_parse target ctx bound in + let lxp = lexp_parse target ctx in let ltp = UnknownType(loc) in (* Read patterns one by one *) @@ -225,7 +207,7 @@ and _lexp_parse (p: pexp) (ctx: lexp_context) bound: lexp = (* Create pattern context *) let (name, iloc, arg), nctx = lexp_read_pattern pat exp lxp ctx in (* parse using pattern context *) - let exp = _lexp_parse exp nctx bound in + let exp = lexp_parse exp nctx in if name = "_" then loop tl merged (Some exp) @@ -241,7 +223,7 @@ and _lexp_parse (p: pexp) (ctx: lexp_context) bound: lexp = -> UnknownType(tloc) (* Identify Call Type and return processed call *) -and lexp_call (fname: pexp) (_args: sexp list) ctx bound = +and lexp_call (fname: pexp) (_args: sexp list) ctx = (* Process Arguments *) let pargs = List.map pexp_parse _args in @@ -254,30 +236,29 @@ and lexp_call (fname: pexp) (_args: sexp list) ctx bound = | Pcons (_, (loc, nm)) -> nm, loc | _ -> raise Not_found in - let largs = lexp_parse_all pargs ctx bound in + let largs = lexp_parse_all pargs ctx in let new_args = List.map (fun g -> (Aexplicit, g)) largs in try (* Check if the function was defined *) let idx = senv_lookup name ctx in let vf = (make_var name idx loc) in - - Call(vf, new_args) + Call(vf, new_args) with Not_found -> (* Don't stop even if an error was found *) lexp_error loc ("The function \"" ^ name ^ "\" was not defined"); let vf = (make_var name (-1) loc) in - Call(vf, new_args) end + Call(vf, new_args) end (* Call to a nameless function *) with Not_found -> - let largs = lexp_parse_all pargs ctx bound in + let largs = lexp_parse_all pargs ctx in let new_args = List.map (fun g -> (Aexplicit, g)) largs in (* I think this should not modify context. * if so, funny things might happen when evaluating *) - let fname = _lexp_parse fname ctx bound in + let fname = lexp_parse fname ctx in Call(fname, new_args) end (* Read a pattern and create the equivalent representation *) @@ -333,7 +314,7 @@ and lexp_read_pattern_args args ctx: in loop args [] ctx (* Parse inductive constructor *) -and lexp_parse_constructors ctors ctx bound = +and lexp_parse_constructors ctors ctx = let make_args (args:(arg_kind * pvar option * pexp) list): (arg_kind * ltype) list * lexp_context = @@ -345,7 +326,7 @@ and lexp_parse_constructors ctors ctx bound = (* What does the optional Pvar do ? that expression does not exist in LEXP*) | (kind, _, exp) -> - let lxp = _lexp_parse exp ctx bound in + let lxp = lexp_parse exp ctx in loop tl ((kind, lxp)::acc) ctx end in loop args [] ctx in @@ -427,18 +408,18 @@ and lexp_decls decls ctx: (((vdef * lexp * ltype) list) * lexp_context) = | hd::tl -> match hd with | ((loc, name), Some pinst, None) ->( - let bound = (0, m) in - let lxp, ltp = lexp_p_infer pinst _ctx bound in + let nctx = local_scope _ctx m in + let lxp, ltp = lexp_p_infer pinst nctx in let nacc = ((loc, name), lxp, ltp)::acc in - let ctx2 = env_add_var_info (0, (loc, name), lxp, ltp) _ctx in + let ctx2 = env_add_var_info (0, (loc, name), lxp, ltp) nctx in process_var_info tl ctx2 nacc (m - 1)) | ((loc, name), Some pinst, Some ptype) ->( - let bound = (0, m) in - let linst = _lexp_parse pinst _ctx bound in - let ltyp = _lexp_parse ptype _ctx bound in + let nctx = local_scope _ctx m in + let linst = lexp_parse pinst nctx in + let ltyp = lexp_parse ptype nctx in let nacc = ((loc, name), linst, ltyp)::acc in - let ctx3 = env_add_var_info (0, (loc, name), linst, ltyp) _ctx in + let ctx3 = env_add_var_info (0, (loc, name), linst, ltyp) nctx in process_var_info tl ctx3 nacc (m - 1)) (* Skip the variable *) @@ -448,12 +429,12 @@ and lexp_decls decls ctx: (((vdef * lexp * ltype) list) * lexp_context) = let acc, ctx = process_var_info decls nctx [] n in acc, ctx -and lexp_parse_all (p: pexp list) (ctx: lexp_context) bound: lexp list = +and lexp_parse_all (p: pexp list) (ctx: lexp_context): lexp list = let rec loop (plst: pexp list) ctx (acc: lexp list) = match plst with | [] -> (List.rev acc) - | _ -> let lxp = _lexp_parse (List.hd plst) ctx bound in + | _ -> let lxp = lexp_parse (List.hd plst) ctx in (loop (List.tl plst) ctx (lxp::acc)) in (loop p ctx []) @@ -538,11 +519,11 @@ and free_variable pxp = * - use lexp_p_check whenever you can. *) -and lexp_p_infer (p : pexp) (env : lexp_context) bound: lexp * ltype = +and lexp_p_infer (p : pexp) (env : lexp_context): lexp * ltype = (* Parse expr *) let tloc = pexp_location p in - let lxp = _lexp_parse p env bound in + let lxp = lexp_parse p env in (* determine type *) match lxp with @@ -555,7 +536,7 @@ and lexp_p_infer (p : pexp) (env : lexp_context) bound: lexp * ltype = (lxp, UnknownType(tloc))) - (* Pcall lookup fname *) + (* Pcall lookup fname type *) (* Pinductive *) (* PCons return its Pinductive type *) @@ -574,14 +555,13 @@ and lexp_p_infer (p : pexp) (env : lexp_context) bound: lexp * ltype = and lexp_p_check (p : pexp) (t : ltype) (env : lexp_context): lexp = match p with | _ - -> let (e, inferred_t) = lexp_p_infer p env (0, 0) in + -> let (e, inferred_t) = lexp_p_infer p env in (* FIXME: check that inferred_t = t! *) e (* * Printing * --------------------- *) - -(* Print back in CET (Close Enough Typer) easier to read *) +(* FIXME: transform to lexp_to_buffer *) and lexp_print_adv opt exp = let slexp_print = lexp_print_adv opt in (* short_lexp_print *) let (pty, indent, prtp) = opt in @@ -702,7 +682,7 @@ and lexp_print_decls opt decls = (* Print context *) and lexp_context_print ctx = - let ((n, map), env) = ctx in + let ((n, map), env, f) = ctx in print_string (make_title " LEXP CONTEXT "); @@ -773,7 +753,7 @@ let _lexp_expr_str (str: string) (tenv: bool array) let toks = lex tenv pretoks in let sxps = sexp_parse_all_to_list grm toks limit in let pxps = pexp_parse_all sxps in - lexp_parse_all pxps ctx (0, 0) + lexp_parse_all pxps ctx ;; (* specialized version *) ===================================== tests/REPL.ml ===================================== --- a/tests/REPL.ml +++ b/tests/REPL.ml @@ -5,7 +5,7 @@ * * Example: * - * $./_build/ityper + * $./_build/ityper [files] * In[ 1] >> sqr = lambda x -> x * x; * In[ 2] >> (sqr 4); * Out[ 2] >> 16 @@ -49,7 +49,7 @@ let rec read_input i = let line = input_line stdin in let s = String.length str in let n = String.length line in - if s = 0 && n = 0 then read_input (i + 1) else + if s = 0 && n = 0 then read_input i else (if n = 0 then ( print_string " . "; print_string (make_line ' ' (i * 4)); @@ -63,7 +63,7 @@ let rec read_input i = print_string (make_line ' ' (i * 4)); loop str (i + 1))) in - loop "" 1 + loop "" i ;; (* Interactive mode is not usual typer @@ -75,7 +75,7 @@ type ldecl = vdef * lexp * ltype type lexpr = lexp (* Grouping declaration together will enable us to support mutually recursive - * declarations *) + * declarations while bringing us closer to normal typer *) let ipexp_parse (sxps: sexp list): (pdecl list * pexpr list) = let rec _pxp_parse sxps dacc pacc = match sxps with @@ -92,7 +92,7 @@ let ipexp_parse (sxps: sexp list): (pdecl list * pexpr list) = let ilexp_parse pexps lctx = let pdecls, pexprs = pexps in let ldecls, lctx = lexp_decls pdecls lctx in - let lexprs = lexp_parse_all pexprs lctx (0, 0) in + let lexprs = lexp_parse_all pexprs lctx in (ldecls, lexprs), lctx ;; @@ -103,8 +103,8 @@ let ieval lexps rctx = vals, rctx ;; -let ieval_string str lctx rctx = - let pres = prelex_string str in +let _ieval f str lctx rctx = + let pres = (f str) in let sxps = lex default_stt pres in let nods = sexp_parse_all_to_list default_grammar sxps (Some ";") in @@ -115,33 +115,47 @@ let ieval_string str lctx rctx = v, lctx, rctx ;; -(* Specials commands %[command-name] *) -let rec repl () = - let lxp_ctx = make_lexp_context in - let rctx = make_runtime_ctx in +let ieval_string = _ieval prelex_string +let ieval_file = _ieval prelex_file - (* Those are hardcoded operation *) - let lxp_ctx = add_def "_+_" lxp_ctx in - let lxp_ctx = add_def "_*_" lxp_ctx in - - let rec loop i clxp rctx = - let ipt = read_input i in - match ipt with - (* Check special keywords *) - | "%quit" -> () - | "%who" -> (print_rte_ctx rctx; loop (i + 1) clxp rctx) - | "%info" -> (lexp_context_print clxp; loop (i + 1) clxp rctx) - | "%calltrace" -> (print_call_trace (); loop (i + 1) clxp rctx) - (* eval input *) - | _ -> let (ret, clxp, rctx) = (ieval_string ipt clxp rctx) in - - List.iter (print_eval_result i) ret; - loop (i + 1) clxp rctx in - - loop 1 lxp_ctx rctx +(* Specials commands %[command-name] *) +let rec repl i clxp rctx = + let ipt = read_input i in + match ipt with + (* Check special keywords *) + | "%quit" -> () + | "%who" -> (print_rte_ctx rctx; repl (i + 1) clxp rctx) + | "%info" -> (lexp_context_print clxp; repl (i + 1) clxp rctx) + | "%calltrace" -> (print_call_trace (); repl (i + 1) clxp rctx) + (* eval input *) + | _ -> let (ret, clxp, rctx) = (ieval_string ipt clxp rctx) in + List.iter (print_eval_result i) ret; + repl (i + 1) clxp rctx ;; +let arg_files = ref [] + + +(* ./ityper [options] files *) +let arg_defs = [ + (*"-I", + Arg.String (fun f -> searchpath := f::!searchpath), + "Append a directory to the search path"*) +];; + +let parse_args () = + Arg.parse arg_defs (fun s -> arg_files:= s::!arg_files) "" + let main () = + parse_args (); + + let lctx = ref make_lexp_context in + let rctx = ref make_runtime_ctx in + + (* Those are hardcoded operation *) + lctx := add_def "_+_" !lctx; + lctx := add_def "_*_" !lctx; + print_string (make_title " TYPER REPL "); print_string " %quit : leave REPL\n"; print_string " %who : print runtime environment\n"; @@ -150,7 +164,25 @@ let main () = print_string (make_sep '-'); flush stdout; - repl () + let nfiles = List.length !arg_files in + + (* Read specified files *) + List.iteri (fun i file -> + print_string " In["; ralign_print_int (i + 1) 2; print_string "] >> "; + print_string ("%readfile " ^ file); print_string "\n"; + + let (ret, lctx1, rctx1) = ieval_file file (!lctx) (!rctx) in + lctx := lctx1; + rctx := rctx1; + List.iter (print_eval_result i) ret; + ) + + !arg_files; + + flush stdout; + + (* Initiate REPL. This will allow us to inspect interpreted code *) + repl (nfiles + 1) (!lctx) (!rctx) ;; ===================================== tests/debug.ml ===================================== --- a/tests/debug.ml +++ b/tests/debug.ml @@ -26,9 +26,8 @@ * --------------------------------------------------------------------------- * * Description: - * Provide helper functions to print out - * extracted Pretoken - * extracted Sexp + * Provide helper functions to print out extracted + * Pretoken, Sexp, pexp and lexp * * --------------------------------------------------------------------------- *) ===================================== tests/full_debug.ml ===================================== --- a/tests/full_debug.ml +++ b/tests/full_debug.ml @@ -20,11 +20,11 @@ * FOR A PARTICULAR PURPOSE. See the GNU General Public License for * more details. * - * You should have received a copy of the GNU General Public License along - * with this program. If not, see <http://www.gnu.org/licenses/>. + * You should have received a copy of the GNU General Public License along + * with this program. If not, see <http://www.gnu.org/licenses/>. * * --------------------------------------------------------------------------- - * + * * Description: * print out each compilation' steps * @@ -38,136 +38,152 @@ open Grammar open Pexp open Util open Fmt - -let dloc = dummy_location;; - open Debruijn open Myers open Lparse open Eval open Lexp - +let dloc = dummy_location;; let dummy_decl = Imm(String(dloc, "Dummy"));; -(* -let pexp_lexp_all nodes ctx = - - let rec loop nodes ctx acc = - match nodes with - | [] -> ((List.rev acc), ctx) - | hd::tl -> - let lxp, new_ctx = pexp_lexp_one hd ctx in - (loop tl new_ctx (lxp::acc)) in - (loop nodes ctx []) -;; +let discard v = ();; +(* Argument parsing *) +let arg_print_options = ref SMap.empty;; +let arg_files = ref [] +let add_p_option name () = + arg_print_options := SMap.add name true (!arg_print_options);; -let add_rte_def name ctx = - (add_rte_variable (Some name) dummy_decl ctx);; - +let get_p_option name = + try let _ = SMap.find name (!arg_print_options) in + true + with + Not_found -> false +;; -let eval_until_nth xpr n rctx = +let arg_defs = [ + ("-pretok", + Arg.Unit (add_p_option "pretok"), " Print pretok debug info"); + ("-tok", + Arg.Unit (add_p_option "tok"), " Print tok debug info"); + ("-sexp", + Arg.Unit (add_p_option "sexp"), " Print sexp debug info"); + ("-pexp", + Arg.Unit (add_p_option "pexp"), " Print pexp debug info"); + ("-lexp", + Arg.Unit (add_p_option "lexp"), " Print lexp debug info"); + ("-all", + Arg.Unit (fun () -> + add_p_option "pretok" (); + add_p_option "tok" (); + add_p_option "sexp" (); + add_p_option "pexp" (); + add_p_option "lexp" ()), + " Print all compilation step with debug info"); +];; + +let parse_args () = + Arg.parse arg_defs (fun s -> arg_files:= s::!arg_files) "" + +let make_default () = + arg_print_options := SMap.empty; + add_p_option "sexp" (); + add_p_option "pexp" (); + add_p_option "lexp" () +;; - let rec loop xpr nb rctx = - match xpr, nb with - | [], _ -> rctx - | _, nb when nb = n -> rctx - | hd::tl, _ -> - let c, rctx = eval_toplevel hd rctx in - print_eval_result nb c; - loop tl (nb + 1) rctx in - loop xpr 0 rctx -;; *) - -let discard v = ();; - -let main () = +let main () = + parse_args (); let arg_n = Array.length Sys.argv in - let usage = - " Usage: \n " ^ Sys.argv.(0) ^ " <file_name> [options] \n\n" in - + + let usage = + "\n Usage: " ^ Sys.argv.(0) ^ " <file_name> [options]\n" in + (* Print Usage *) if arg_n == 1 then - begin - print_string usage; - print_string " Options:\n"; - end + (Arg.usage (Arg.align arg_defs) usage) else begin - let filename = Sys.argv.(1) in - (* Read additional Args if any *) + (if arg_n = 2 then make_default ()); + + let filename = List.hd (!arg_files) in print_string (make_title " ERRORS "); (* get pretokens*) let pretoks = prelex_file filename in - + (* get sexp/tokens *) let toks = lex default_stt pretoks in - + (* get node sexp *) let nodes = sexp_parse_all_to_list default_grammar toks (Some ";") in - + (* Parse All Declaration *) let pexps = pexp_decls_all nodes in - (* let pexps = pexp_parse_all nodes in *) (* get lexp *) let ctx = make_lexp_context in (* Those are hardcoded operation *) let ctx = add_def "_+_" ctx in let ctx = add_def "_*_" ctx in - - (* let lexps, new_ctx = lexp_parse_all pexps ctx in *) + let lexps, nctx = lexp_decls pexps ctx in - + print_string "\n\n"; - (* Printing *)(* - print_title "PreTokens"; debug_pretokens_print_all pretoks; - print_title "Base Sexp"; debug_sexp_print_all toks; *) - print_string (make_title " Node Sexp "); debug_sexp_print_all nodes; - print_string "\n"; - print_string (make_title " Pexp "); debug_pexp_decls pexps; - (*debug_pexp_print_all pexps;*) - print_string "\n"; - print_string (make_title " Lexp "); debug_lexp_decls lexps; - (* debug_lexp_print_all lexps; *) - print_string "\n"; + (* Printing *) + (if (get_p_option "pretok") then( + print_string (make_title " PreTokens"); + debug_pretokens_print_all pretoks; print_string "\n")); + + (if (get_p_option "tok") then( + print_string (make_title " Base Sexp"); + debug_sexp_print_all toks; print_string "\n")); + + (if (get_p_option "sexp") then( + print_string (make_title " Node Sexp "); + debug_sexp_print_all nodes; print_string "\n")); + + (if (get_p_option "pexp") then( + print_string (make_title " Pexp "); + debug_pexp_decls pexps; print_string "\n")); + + (if (get_p_option "lexp") then( + print_string (make_title " Lexp "); + debug_lexp_decls lexps; print_string "\n")); print_string "\n"; lexp_context_print nctx; print_string "\n"; - + (* Eval Each Expression *) print_string (make_title " Eval Print "); - - + (* Eval declaration *) - let rctx = make_runtime_ctx in + let rctx = make_runtime_ctx in let rctx = eval_decls lexps rctx in - - let _ = + + let _ = try (* Check if main is present *) let main = (senv_lookup "main" nctx) in (* Push main args here if any *) - + (* get main body *) let body = (get_rte_variable main rctx) in (* eval main *) let r = (eval body rctx) in print_eval_result 0 r - - with + + with Not_found -> () in - + (* Print info *) print_string "\n\n"; - print_rte_ctx rctx; - - + print_rte_ctx rctx; + print_call_trace (); end ;; ===================================== tests/lexp_test.ml ===================================== --- a/tests/lexp_test.ml +++ b/tests/lexp_test.ml @@ -1,6 +1,7 @@ open Lparse (* add_def *) open Debruijn (* make_lexp_context *) open Lexp +open Pexp open Utest_lib (* default environment *) @@ -9,42 +10,42 @@ let lctx = add_def "_+_" lctx let lctx = add_def "_*_" lctx -let _ = (add_test "LEXP" "Built-in Inference" (fun () -> +let _ = (add_test "LEXP" "Built-in type Inference" (fun () -> let dcode = "a = 10; b = 1.12;" in let ret, _ = lexp_decl_str dcode lctx in - + match ret with (* (vdef * lexp * ltype) *) - | [(_, _, Builtin(_, "Int", _)); - (_, _, Builtin(_, "Float", _))] -> + | [(_, _, Builtin(_, "Int", _)); + (_, _, Builtin(_, "Float", _))] -> success() | _ -> failure ()) );; -open Pexp - let set_to_list s = StringSet.fold (fun g a -> g::a) s [] ;; let _ = (add_test "LEXP" "Free Variable" (fun () -> - + let dcode = " a = 2; b = 3; f = lambda n -> (a + n); % a is a fv - g = lambda x -> ((f b) + a + x); % f,a,b is fv + g = lambda x -> ((f b) + a + x); % f,a,b are fv " in let ret = pexp_decl_str dcode in - let (_, g, _)::_ = List.rev ret in + let g = match List.rev ret with + | (_, g, _)::_ -> g + | _ -> raise (Unexpected_result "Unexpected empty list") in let (bound, free) = free_variable g in - + let bound = set_to_list bound in let (free, _) = free in @@ -56,9 +57,7 @@ let _ = (add_test "LEXP" "Free Variable" (fun () -> | _ -> failure () ));; - - (* run all tests *) run_all () -;; \ No newline at end of file +;; ===================================== tests/pexp_test.ml ===================================== --- a/tests/pexp_test.ml +++ b/tests/pexp_test.ml @@ -1,25 +1,22 @@ -open Pexp -open Utest_lib +open Pexp +open Utest_lib + - let _ = (add_test "PEXP" "Type Parsing" (fun () -> let dcode = " let a : Nat; a = 1; b : Nat; b = 3; in a + b;" in - + let ret = pexp_expr_str dcode in match ret with | [expr] ->( match expr with - | Plet(_, arg, _) -> match arg with + | Plet(_, arg, _) -> (match arg with | [] -> failure () | (_, tp, bl)::_ ->( - if bl = true then - success () - else - failure ()) + if bl = true then success () else failure ())) | _ -> failure ()) - | [] -> failure ()) + | _ -> failure ()) ) ;; ===================================== tests/utest_lib.ml ===================================== --- a/tests/utest_lib.ml +++ b/tests/utest_lib.ml @@ -56,12 +56,15 @@ let _global_sections = ref StringMap.empty let _insertion_order = ref [] let _ret_code = ref 0 +(* Exception *) +exception Unexpected_result of string + (* Value Checking *) (* USAGE: expect_something_type value expected_value *) (* return success() if match else failure () *) let unexpected_throw sk tk e = print_string ("[ FAIL] " ^ sk ^ " - " ^ tk ^ "\n"); - print_string "[ ] UNEXPECTED THROW: \n"; + print_string "[ ] UNEXPECTED THROW:\n"; print_string "[ ] "; print_string ((Printexc.to_string e) ^ "\n"); ;; @@ -101,7 +104,7 @@ let add_section sname = *) let add_test sname tname tfun = - (* Does Section Exists ? *) + (* Does Section Exist ? *) let (tmap, lst) = add_section sname in try let _ = StringMap.find tname tmap in @@ -124,8 +127,8 @@ let for_all_tests sk tmap tk = flush stdout; try let r = tv () in - if r = 0 then - (print_string ("[ OK] " ^ sk ^ " - " ^ tk ^ "\n")) + if r = 0 then( + print_string ("[ OK] " ^ sk ^ " - " ^ tk ^ "\n")) else( print_string ("[ FAIL] " ^ sk ^ " - " ^ tk ^ "\n"); _ret_code := failure ()) @@ -151,8 +154,3 @@ let run_all () = (* return success or failure *) exit !_ret_code ;; - - - - - View it on GitLab: https://gitlab.com/monnier/typer/compare/74750a6624e99e6a45b0f766201b32ba4a…

1 0

[Git][monnier/typer][master] ityper fix + remove trailling space for consistency
by Setepenre 23 Mar '16

23 Mar '16

Setepenre pushed to branch master at Stefan / Typer Commits: 74750a66 by Pierre Delaunay at 2016-03-21T23:22:08-04:00 ityper fix + remove trailling space for consistency - - - - - 11 changed files: - src/debruijn.ml - src/eval.ml - src/grammar.ml - src/lexp.ml - src/lparse.ml - src/pexp.ml - src/sexp.ml - tests/REPL.ml - tests/debug.ml - tests/utest_lib.ml - tests/utest_main.ml Changes: ===================================== src/debruijn.ml ===================================== #<Gitlab::Git::Diff:0x007f5008674df0> ===================================== src/eval.ml ===================================== #<Gitlab::Git::Diff:0x007f5008672398> ===================================== src/grammar.ml ===================================== #<Gitlab::Git::Diff:0x007f5008671d80> ===================================== src/lexp.ml ===================================== #<Gitlab::Git::Diff:0x007f5008671830> ===================================== src/lparse.ml ===================================== #<Gitlab::Git::Diff:0x007f5008671268> ===================================== src/pexp.ml ===================================== #<Gitlab::Git::Diff:0x007f5008670bd8> ===================================== src/sexp.ml ===================================== #<Gitlab::Git::Diff:0x007f5008670570> ===================================== tests/REPL.ml ===================================== #<Gitlab::Git::Diff:0x007f5008670020> ===================================== tests/debug.ml ===================================== #<Gitlab::Git::Diff:0x007f500866f5d0> ===================================== tests/utest_lib.ml ===================================== #<Gitlab::Git::Diff:0x007f500866ee78> ===================================== tests/utest_main.ml ===================================== #<Gitlab::Git::Diff:0x007f500866e8d8> View it on GitLab: https://gitlab.com/monnier/typer/commit/74750a6624e99e6a45b0f766201b32ba4a8…

3 2

[Git][monnier/typer][master] 18 commits: add new eval/lexp/pexp string
by Setepenre 22 Mar '16

22 Mar '16

Setepenre pushed to branch master at Stefan / Typer Commits: 1a13cb32 by Pierre Delaunay at 2016-03-16T20:02:23-04:00 add new eval/lexp/pexp string - - - - - 94117ebf by Pierre Delaunay at 2016-03-16T20:04:24-04:00 variable cascade - - - - - d27dd338 by Pierre Delaunay at 2016-03-16T20:11:37-04:00 eval does not return ctx anymore - - - - - 9bbc1472 by Pierre Delaunay at 2016-03-16T20:40:54-04:00 removed useless definitions - - - - - 408e47b6 by Pierre Delaunay at 2016-03-16T20:44:38-04:00 fix double declarations - - - - - bcc59cc4 by Pierre Delaunay at 2016-03-16T21:00:23-04:00 dbi info - - - - - 86861d63 by Pierre Delaunay at 2016-03-16T21:11:55-04:00 lexp does not return ctx anymore - - - - - eceb5ece by Pierre Delaunay at 2016-03-17T09:49:49-04:00 check - - - - - 49bf1cb1 by Pierre Delaunay at 2016-03-19T17:56:51-04:00 utest check return code - - - - - 48362db8 by Pierre Delaunay at 2016-03-19T18:07:41-04:00 Debruijn partial fix - - - - - e502bfc8 by Pierre Delaunay at 2016-03-20T12:35:44-04:00 builtin type inference - - - - - df91a4f1 by Pierre Delaunay at 2016-03-20T17:14:15-04:00 free var - - - - - 96867ec2 by U-SDM-9528\Etudiants at 2016-03-21T13:31:48-04:00 merging - - - - - 7a0bb44f by U-SDM-9528\Etudiants at 2016-03-21T13:59:33-04:00 merging (compile) - - - - - d14e36a4 by Pierre Delaunay at 2016-03-21T14:05:35-04:00 rollback - - - - - 015c8a70 by Pierre Delaunay at 2016-03-21T14:26:42-04:00 merged - - - - - a3eb218d by Pierre Delaunay at 2016-03-21T14:32:59-04:00 merge with experimental branch - - - - - 932370de by Pierre Delaunay at 2016-03-21T14:46:09-04:00 merge again - - - - - 17 changed files: - .gitignore - GNUmakefile - + samples/test__.typer - src/debruijn.ml - src/eval.ml - src/fmt.ml - src/grammar.ml - src/lexp.ml - src/lparse.ml - src/pexp.ml - tests/REPL.ml - tests/debug.ml - tests/eval_test.ml - tests/full_debug.ml - tests/lexp_test.ml - tests/utest_lib.ml - tests/utest_main.ml Changes: ===================================== .gitignore ===================================== --- a/.gitignore +++ b/.gitignore @@ -18,3 +18,4 @@ manual.?? test__.ml _temp_hack test__.typer +*.orig \ No newline at end of file ===================================== GNUmakefile ===================================== --- a/GNUmakefile +++ b/GNUmakefile @@ -4,39 +4,40 @@ SRC_FILES := $(wildcard ./src/*.ml) CPL_FILES := $(wildcard ./_build/src/*.cmo) TEST_FILES := $(wildcard ./tests/*_test.ml) +CFLAG = -cflag -rectypes -build-dir _build + # This is for windows: windows version is old -ifeq ($(OS),Windows_NT) -SHELL=C:/Windows/System32/cmd.exe -endif + all: ityper typer debug tests typer: - ocamlbuild src/main.byte -cflag -rectypes - mv _build/src/main.byte _build/typer # move and rename executable + ocamlbuild src/main.native $(CFLAG) + @mv _build/src/main.native _build/typer # debug file eval debug: - ocamlbuild tests/full_debug.native -I src -cflag -rectypes - mv _build/tests/full_debug.native _build/full_debug + ocamlbuild tests/full_debug.native -I src $(CFLAG) + @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 + ocamlbuild tests/REPL.native -I src $(CFLAG) + @mv _build/tests/REPL.native _build/ityper tests-build: -# ============================ -# Build tests -# ============================ - $(foreach test, $(TEST_FILES), ocamlbuild $(subst ./,,$(subst .ml,.native,$(test))) -I src -cflag -rectypes;) + # ============================ + # Build tests + # ============================ + @$(foreach test, $(TEST_FILES), ocamlbuild $(subst ./,,$(subst .ml,.native,$(test))) -I src $(CFLAG);) + @ocamlbuild tests/utest_main.native $(CFLAG) + @mv _build/tests/utest_main.native _build/tests/utests tests-run: -# ============================ -# Run tests -# ============================ - ocamlbuild tests/utest_main.native - ./_build/tests/utest_main.native + # ============================ + # Run tests + # ============================ + @./_build/tests/utests # Make language doc doc-tex: @@ -44,9 +45,10 @@ doc-tex: # Make implementation doc doc-ocaml: - ocamldoc -html -d _build $(SRC_FILES) + ocamldoc -html -d _build/doc $(SRC_FILES) + +# everything is expected to be compiled in the "./_build/" folder +clean: + -rm -rf _build -.PHONY: ityper -.PHONY: typer -.PHONY: debug -.PHONY: tests +.PHONY: ityper typer debug tests ===================================== samples/test__.typer ===================================== --- /dev/null +++ b/samples/test__.typer @@ -0,0 +1,61 @@ + + + +%a = lambda x -> +% let a1 : Nat; a1 = 2; b1 : Nat; b1 = 3; in +% a1 + b1 + x +%; + +% main = (a 2) + + +a = 2; + +Nat = inductive_ (dNat) (zero) (succ Nat); + +zero = inductive-cons Nat zero; +succ = inductive-cons Nat succ; + +one = (succ zero); +two = (succ one); +three = (succ two); + +tonum = lambda x -> case x + | (succ y) => (1 + (tonum y)) + | _ => 0 +; + +x = zero; +% main = zero; => zero(Nat[1]) +% main = x; => succ(Nat[2]) + +main = (tonum one); + + + +%================================ CALL TRACE ================================ +% size = 6 +%---------------------------------------------------------------------------- +%|+- Call: (tonum[1] zero[6]) +%|:+- Var: zero[6] +%|:+- Lambda: lambda (x: unkwn) -> case x[0]: unkwn| succ y -> 1 + (tonum[4] y[0]); | zero -> 0; +%|:|+- Case: case x[0]: unkwn| succ y -> 1 + (tonum[4] y[0]); | zero -> 0; +%|:|:+- Var: x[0] +%|:|:+- Imm: 0 +%============================================================================ + +%================================ CALL TRACE ================================ +% size = 11 +%---------------------------------------------------------------------------- +%|+- Call: (tonum[2] x[1]) +%|:+- Var: x[1] +%|:+- Lambda: lambda (x: unkwn) -> case x[0]: unkwn| succ y -> 1 + (tonum[2] y[0]); | _ -> 0; +%|:|+- Case: case x[0]: unkwn| succ y -> 1 + (tonum[2] y[0]); | _ -> 0; +%|:|:+- Var: x[0] +%|:|:+- Var: zero[6] +%|:|:+- Call: 1 + (tonum[2] y[0]) +%|:|:|+- Imm: 1 +%|:|:|+- Call: (tonum[2] y[0]) +%|:|:|:+- Var: y[0] +%|:|:|:+- Var: zero[6] +%============================================================================ ===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -52,6 +52,7 @@ module StringMap = Map.Make (struct type t = string let compare = String.compare end) ;; + (* Map matching variable name and its distance in the current scope *) type scope = (int) StringMap.t (* Map<String, int>*) @@ -136,10 +137,3 @@ let env_lookup_type ctx (v : vref) = let env_lookup_by_index index ctx = Myers.nth index (_get_env ctx);; - - - - - - - \ No newline at end of file ===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -20,18 +20,18 @@ * FOR A PARTICULAR PURPOSE. See the GNU General Public License for * more details. * - * You should have received a copy of the GNU General Public License along - * with this program. If not, see <http://www.gnu.org/licenses/>. + * You should have received a copy of the GNU General Public License along + * with this program. If not, see <http://www.gnu.org/licenses/>. * * --------------------------------------------------------------------------- - * + * * Description: * Simple interpreter * * --------------------------------------------------------------------------- *) - + open Util -open Lexp +open Lexp open Lparse open Myers open Sexp @@ -40,7 +40,7 @@ open Debruijn open Grammar -let _eval_error loc msg = +let _eval_error loc msg = msg_error "eval" loc msg; raise (internal_error msg) ;; @@ -55,13 +55,13 @@ 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 print_myers_list l print_fun = let n = (length l) - 1 in - + print_string (make_title " ENVIRONMENT "); make_rheader [(None, "INDEX"); (None, "VARIABLE NAME"); (None, "VALUE")]; print_string (make_sep '-'); - + for i = 0 to n do print_string " | "; ralign_print_int (n - i) 5; @@ -79,7 +79,7 @@ let get_function_name fname = let get_int lxp = match lxp with - | Imm(Integer(_, l)) -> l + | Imm(Integer(_, l)) -> l | _ -> lexp_print lxp; -40 ;; @@ -95,9 +95,9 @@ let get_rte_variable (idx: int) (l: runtime_env): lexp = let get_rte_size (l: runtime_env): int = length l;; -let print_rte_ctx l = print_myers_list l - (fun (n, g) -> - let _ = +let print_rte_ctx l = print_myers_list l + (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 @@ -106,7 +106,7 @@ let print_rte_ctx l = print_myers_list l let nfirst_rte_var n ctx = - let rec loop i acc = + let rec loop i acc = if i < n then loop (i + 1) ((get_rte_variable i ctx)::acc) else @@ -119,33 +119,43 @@ type value_type = lexp (* This is an internal definition * 'i' is the recursion depth used to print the call trace *) -let rec _eval lxp ctx i: (value_type) = - - (if i > 255 then +let rec _eval lxp ctx i: (value_type) = + + (if i > 255 then raise (internal_error "Recursion Depth exceeded")); add_call lxp i; match lxp with (* This is already a leaf *) | Imm(v) -> lxp - + (* Return a value stored in the environ *) - | Var((loc, name), idx) -> begin + | Var((loc, name), idx) as e -> begin + (* find variable binding i.e we do not want a another variable *) + let rec var_crawling expr i k = + (if k > 255 then( + lexp_print expr; print_string "\n"; flush stdout; + raise (internal_error "Variable lookup failed"))); + match expr with + | Var(_, j) -> + let p = (get_rte_variable (i + j) ctx) in + var_crawling p (i + j) (k + 1) + | _ -> expr in + try - (get_rte_variable idx ctx) - with + (var_crawling e 0 0) + with Not_found -> - print_string ("Variable: " ^ name ^ " was not found | "); + print_string ("Variable: " ^ name ^ " was not found | "); 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 *) + | Let(_, decls, inst) -> + (* First we _evaluate all declaration then we eval the instruction *) let nctx = build_ctx decls ctx i in - (* Then we eval the body *) - _eval inst nctx (i + 1) end - + _eval inst nctx (i + 1) + (* Function call *) | Call (lname, args) -> ( (* Try to extract name *) @@ -159,49 +169,48 @@ let rec _eval lxp ctx i: (value_type) = (* + 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 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)) - + (* _*_ is reas 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) -> (* Check if the call is a constructor call *) - + (* get function body *) let body = get_rte_variable idx ctx in - + (* Add args in the scope *) let nctx = build_arg_list args ctx i in - (* eval body *) _eval body nctx (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 + | Lambda(_, vr, _, body) -> begin let (loc, name) = vr in (* Get first arg *) let value = (get_rte_variable 0 ctx) in let nctx = add_rte_variable (Some name) value ctx in - + (* Collapse nested lambdas *) - let rec build_body bd idx nctx = + let rec build_body bd idx nctx = match bd with | Lambda(_, vr, _, body) -> let (loc, name) = vr in @@ -211,76 +220,61 @@ let rec _eval lxp ctx i: (value_type) = let nctx = add_rte_variable (Some name) value nctx in (build_body body (idx + 1) nctx) | _ -> bd, nctx in - + let body, nctx = build_body body 1 nctx in - (* eval lambda body *) - _eval body nctx (i + 1) end - + _eval body nctx (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 - - (* Case *) + + (* Case *) | Case (loc, target, _, pat, dflt) -> begin - + (* Eval target *) let v = _eval target ctx (i + 1) in - - let check_ctor ctor_name type_idx = - let info = get_rte_variable type_idx ctx in - match info with - | Inductive(_, _, _, ctor_def) -> SMap.find ctor_name ctor_def - | _ -> _eval_error loc "Target is not a Constructor" in - - (* 'v' must be a constructor *) - let ctor_name, args, idx = match v with - - (* multi arg constructor are parsed as Call *) + let nctx = ctx in + + (* V must be a constructor Call *) + let ctor_name, args = match v with | Call(lname, args) -> (match lname with - | Var((_, ctor_name), idx) -> - let offset = (get_rte_size ctx) - idx - 1 in - let tidx = idx + offset in - ctor_name, args, tidx - - | _ -> _eval_error loc "Target is not a Constructor" ) - - | Cons((_, idx), (_, cname)) -> - let offset = (get_rte_size ctx) - idx - 1 in - let tidx = idx + offset in - cname, [], tidx - - | _ -> lexp_print v; + | Var((_, ctor_name), _) -> ctor_name, args + | _ -> _eval_error loc "Target is not a Constructor" ) + + | Cons((_, idx), (_, cname)) -> begin + (* retrieve type definition *) + print_int idx; + let info = get_rte_variable idx ctx in + let Inductive(_, _, _, ctor_def) = info in + 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; print_string "\n"; + lexp_print v; print_string "\n"; _eval_error loc "Can't match expression" in - - (* Check if the constructor was defined *) - let targs = try check_ctor ctor_name idx - with Not_found -> _eval_error loc "Constructor does not exist" in - - (* Check number of args *) - let n_targs = List.length targs in - let n_args = List.length args in - (if n_targs != n_args then - _eval_error loc "Wrong number of arguments"); - + (* Check if a default is present *) - let run_default df = + 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 + if pat_n = ctor_n && ctor_name = key then true - else + else false in - + (* Search for the working pattern *) let sol = SMap.filter is_true pat in if SMap.is_empty sol then @@ -288,54 +282,51 @@ let rec _eval lxp ctx i: (value_type) = else (* 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 + | None -> nctx | Some (_, (_, name)) -> let (_, xp) = cl in - add_rte_variable (Some name) xp nctx) - + add_rte_variable (Some name) xp nctx) + ctx pat_args args in (* eval body *) _eval exp nctx (i + 1) end | _ -> Imm(String(dloc, "eval Not Implemented")) - + 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 - + let arg_val = List.map (fun (k, e) -> _eval e ctx (i + 1)) 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 i = - match decls with - | [] -> ctx - | hd::tl -> - let (v, exp, tp) = hd in - let value = _eval exp ctx (i + 1) in - let nctx = add_rte_variable None value ctx in - build_ctx tl nctx i - + let f nctx e = + let (v, exp, tp) = e in + let value = _eval exp ctx (i + 1) in + add_rte_variable None value nctx in + + List.fold_left f ctx decls + and eval_decl ((l, n), lxp, ltp) ctx = add_rte_variable (Some n) lxp ctx - + (* Eval a declaration if a main is found it is returned *) -and eval_decls (decls: ((vdef * lexp * ltype) list)) +and eval_decls (decls: ((vdef * lexp * ltype) list)) (ctx: runtime_env): runtime_env = let rec loop decls ctx = - match decls with + match decls with | [] -> ctx - | hd::tl -> + | hd::tl -> let ((_, n), lxp, ltp) = hd in let nctx = add_rte_variable (Some n) lxp ctx in loop tl nctx in loop decls ctx - + and print_eval_result i lxp = print_string " Out["; ralign_print_int i 2; @@ -343,27 +334,25 @@ and print_eval_result i lxp = match lxp with | Imm(v) -> sexp_print v; print_string "\n" | e -> lexp_print e; print_string "\n" - and print_call_trace () = print_string (make_title " CALL TRACE "); - + let n = List.length !global_trace in print_string " size = "; print_int n; print_string "\n"; print_string (make_sep '-'); - + let racc = List.rev !global_trace in - print_first 50 racc (fun j (i, g) -> + print_first 50 racc (fun j (i, g) -> _print_ct_tree i; print_string "+- "; print_string (lexp_to_string g); print_string ": "; lexp_print g; print_string "\n"); - + print_string (make_sep '='); ;; -(* eval_expr *) -let eval lxp ctx = +let eval lxp ctx = try - (_eval lxp ctx 1) + _eval lxp ctx 1 with e -> ( print_rte_ctx ctx; print_call_trace (); ===================================== src/fmt.ml ===================================== --- a/src/fmt.ml +++ b/src/fmt.ml ===================================== src/grammar.ml ===================================== --- a/src/grammar.ml +++ b/src/grammar.ml ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -72,7 +72,7 @@ type ltype = lexp | Call of lexp * (arg_kind * lexp) list (* Curried call. *) | Inductive of location * label * ((arg_kind * vdef * ltype) list) * ((arg_kind * ltype) list) SMap.t - | Cons of vref * symbol + | Cons of vref * symbol (* = Type info * ctor_name*) | Case of location * lexp * ltype (* The base inductive type over which we switch. *) * (location * (arg_kind * vdef) option list * lexp) SMap.t ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -62,16 +62,37 @@ let lexp_fatal loc msg = ;; +module StringSet + = Set.Make (struct type t = string let compare = String.compare end) +;; + (* 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;; +(* Built-in list of types/functions *) +let lexp_builtins = [ +(* NAME | LXP *) + ("Int" , type_int); + ("Float", type_float); + ("_=_" , type_eq); (* t -> t -> bool *) + ("_+_" , iop_binary); (* int -> int -> int *) +] + +(* Make lxp context with built-in types *) +let default_lctx = + (* Empty context *) + let lctx = make_lexp_context in + + (* populate ctx *) + List.fold_left (fun ctx (name, lxp) -> + let ctx = senv_add_var name dloc ctx in + env_add_var_info (0, (dloc, name), lxp, lxp) ctx) + lctx + lexp_builtins +;; -(* 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) +(* 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. @@ -89,8 +110,13 @@ let pvar_to_vdef p = p;; * *) +let rec lexp_parse p ctx: lexp = + _lexp_parse p ctx (0, 0) -let rec lexp_parse (p: pexp) (ctx: lexp_context): lexp = +(* bound is used to determine if the variable require shifting + * bound = (inner_size, r_offset) + *) +and _lexp_parse (p: pexp) (ctx: lexp_context) bound: lexp = (* So I don't have to extract it *) let tloc = pexp_location p in match p with @@ -98,37 +124,42 @@ let rec lexp_parse (p: pexp) (ctx: lexp_context): lexp = | Pimm value -> Imm(value) (* Symbol i.e identifier *) - | Pvar (loc, name) -> - (try + | Pvar (loc, name) -> begin + try (* Send Variable loc *) - let idx = senv_lookup name ctx in - make_var name idx loc; + let (isize, rof) = bound in + let idx = senv_lookup name ctx in( + if idx > isize then + (make_var name (idx - rof) loc) + else + (make_var name idx loc)) with Not_found -> (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)) + (make_var name (-1) loc)) end (* Let, Variable declaration + local scope *) | Plet(loc, decls, body) -> let decl, nctx = lexp_decls decls ctx in (* Body cannot modify context *) - let bdy = lexp_parse body nctx in - (* Send back old context as we exit the inner scope *) + let (_, rof) = bound in + let bound = ((List.length decl), rof) in + let bdy = _lexp_parse body nctx bound in Let(tloc, decl, bdy) (* ->/=> *) | Parrow (kind, Some var, tp, loc, expr) -> - let nvar = pvar_to_vdef var in (* /!\ HERE *) - let ltyp = lexp_parse tp ctx in - let lxp = lexp_parse expr ctx in (* FIXME: add nvar to ctx! *) + let nvar = var in (* /!\ HERE *) + let ltyp = _lexp_parse tp ctx bound in + let lxp = _lexp_parse expr ctx bound in Arrow(kind, Some nvar, ltyp, tloc, lxp) | Parrow (kind, None, tp, loc, expr) -> - let ltyp = lexp_parse tp ctx in - let lxp = lexp_parse expr ctx in - Arrow(kind, None, ltyp, tloc, lxp) - + let ltyp = _lexp_parse tp ctx bound in + let lxp = _lexp_parse expr ctx bound in + Arrow(kind, None, ltyp, tloc, lxp) + (* *) | Plambda (kind, var, Some ptype, body) -> (* Add argument to context *) @@ -138,10 +169,11 @@ let rec lexp_parse (p: pexp) (ctx: lexp_context): lexp = let nctx = senv_add_var vname loc ctx in let nctx = env_add_var_info (0, (loc, vname), dlxp, ltp) nctx in - let lbody = lexp_parse body nctx in - - (* Return old context as we exit lambda scope*) - Lambda(kind, var, ltp, lbody) + let ltyp = _lexp_parse ptype nctx bound in + let (_, rof) = bound in + let bound = (1, rof) in + let lbody = _lexp_parse body nctx bound in + Lambda(kind, var, ltyp, lbody) | Plambda (kind, var, None, body) -> let (loc, vname) = var in @@ -149,28 +181,31 @@ let rec lexp_parse (p: pexp) (ctx: lexp_context): lexp = let nctx = senv_add_var vname loc ctx in let nctx = env_add_var_info (0, (loc, vname), dlxp, dltype) nctx in - let lbody = lexp_parse body nctx in + let (_, rof) = bound in + let bound = (1, rof) in + let lbody = _lexp_parse body nctx bound in Lambda(kind, var, UnknownType(tloc), lbody) - | Pcall (fname, args) -> lexp_call fname args ctx + | Pcall (fname, _args) -> + lexp_call fname _args ctx bound (* Pinductive *) | Pinductive (label, [], ctors) -> - let map_ctor = lexp_parse_constructors ctors ctx in + let map_ctor, nctx = lexp_parse_constructors ctors ctx bound in Inductive(tloc, label, [], map_ctor) (* Pcons *) | Pcons(vr, sym) -> ( let (loc, type_name) = vr in let (_, ctor_name) = sym in - + let (isize, rof) = bound in (* An inductive type named type_name must be in the environment *) try let idx = senv_lookup type_name ctx in (* Check if the constructor exists *) (* TODO *) - Cons((vr, idx), sym) + Cons((vr, idx - rof), sym) with Not_found -> - lexp_error loc + lexp_error loc ("The inductive type: " ^ type_name ^ " was not declared"); Cons((vr, -1), sym)) @@ -178,7 +213,7 @@ let rec lexp_parse (p: pexp) (ctx: lexp_context): lexp = | Pcase (loc, target, patterns) -> (* I need type info HERE *) - let lxp = lexp_parse target ctx in + let lxp = _lexp_parse target ctx bound in let ltp = UnknownType(loc) in (* Read patterns one by one *) @@ -188,10 +223,9 @@ let rec lexp_parse (p: pexp) (ctx: lexp_context): lexp = | hd::tl -> let (pat, exp) = hd in (* Create pattern context *) - let (name, iloc, arg), nctx2 = - lexp_read_pattern pat exp lxp ctx in + let (name, iloc, arg), nctx = lexp_read_pattern pat exp lxp ctx in (* parse using pattern context *) - let exp = lexp_parse exp nctx2 in + let exp = _lexp_parse exp nctx bound in if name = "_" then loop tl merged (Some exp) @@ -207,7 +241,7 @@ let rec lexp_parse (p: pexp) (ctx: lexp_context): lexp = -> UnknownType(tloc) (* Identify Call Type and return processed call *) -and lexp_call (fname: pexp) (_args: sexp list) ctx = +and lexp_call (fname: pexp) (_args: sexp list) ctx bound = (* Process Arguments *) let pargs = List.map pexp_parse _args in @@ -220,7 +254,7 @@ and lexp_call (fname: pexp) (_args: sexp list) ctx = | Pcons (_, (loc, nm)) -> nm, loc | _ -> raise Not_found in - let largs, fctx = lexp_parse_all pargs ctx in + let largs, fctx = lexp_parse_all pargs ctx bound in let new_args = List.map (fun g -> (Aexplicit, g)) largs in try @@ -239,11 +273,11 @@ and lexp_call (fname: pexp) (_args: sexp list) ctx = (* Call to a nameless function *) with Not_found -> - let largs, fctx = lexp_parse_all pargs ctx in + let largs, fctx = lexp_parse_all pargs ctx bound in let new_args = List.map (fun g -> (Aexplicit, g)) largs in (* I think this should not modify context. * if so, funny things might happen when evaluating *) - let fname = lexp_parse fname ctx in + let fname = _lexp_parse fname ctx bound in Call(fname, new_args) end (* Read a pattern and create the equivalent representation *) @@ -266,7 +300,7 @@ and lexp_read_pattern pattern exp target ctx: (* Create a variable containing target *) let nctx = senv_add_var name loc ctx in let nctx = env_add_var_info (0, (loc, name), target, dltype) nctx in - ("_", loc, []), nctx) + (name, loc, []), nctx) | Ppatcons (ctor_name, args) -> let (loc, name) = ctor_name in @@ -299,7 +333,7 @@ and lexp_read_pattern_args args ctx: in loop args [] ctx (* Parse inductive constructor *) -and lexp_parse_constructors ctors ctx = +and lexp_parse_constructors ctors ctx bound = let make_args (args:(arg_kind * pvar option * pexp) list): (arg_kind * ltype) list * lexp_context = @@ -311,13 +345,13 @@ and lexp_parse_constructors ctors ctx = (* What does the optional Pvar do ? that expression does not exist in LEXP*) | (kind, _, exp) -> - let lxp = lexp_parse exp ctx in + let lxp = _lexp_parse exp ctx bound in loop tl ((kind, lxp)::acc) ctx end in loop args [] ctx in let rec loop ctors merged ctx = match ctors with - | [] -> merged + | [] -> merged, ctx | hd::tl -> begin match hd with | ((loc, name), args) -> @@ -332,11 +366,6 @@ and lexp_parse_constructors ctors ctx = and lexp_decls decls ctx: (((vdef * lexp * ltype) list) * lexp_context) = (* Merge Type info and declaration together *) - (* We use a list because order matters and Maps reorder elements *) - (* - let rec is_equal target (p:(vdef * pexp option * pexp option)): bool = - let ((_, name), _, _) = p in - if name == target then true else false in *) (* merge with a map to guarantee uniqueness. *) let rec merge_decls (decls: (pvar * pexp * bool) list) merged acc: @@ -376,7 +405,7 @@ and lexp_decls decls ctx: (((vdef * lexp * ltype) list) * lexp_context) = let mdecls, ord = merge_decls decls SMap.empty [] in - (* cast map to list*) + (* 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 @@ -389,44 +418,106 @@ and lexp_decls decls ctx: (((vdef * lexp * ltype) list) * lexp_context) = | ((loc, name), _, _) -> senv_add_var name loc ctx) ctx decls in - let n_decls = List.length decls in + let n = (List.length decls) - 1 in (* Add Variable info *) - let rec process_var_info dcl_lst _ctx acc i = + 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 bound = (0, m) in + let lxp, ltp = lexp_p_infer pinst _ctx bound in let nacc = ((loc, name), lxp, ltp)::acc in - let ctx2 = env_add_var_info (n_decls - i, (loc, name), lxp, ltp) _ctx in - process_var_info tl ctx2 nacc (i + 1)) + let ctx2 = env_add_var_info (0, (loc, name), lxp, ltp) _ctx in + process_var_info tl ctx2 nacc (m - 1)) | ((loc, name), Some pinst, Some ptype) ->( - let linst = lexp_parse pinst _ctx in - let ltyp = lexp_parse ptype _ctx in + let bound = (0, m) in + let linst = _lexp_parse pinst _ctx bound in + let ltyp = _lexp_parse ptype _ctx bound in let nacc = ((loc, name), linst, ltyp)::acc in - let ctx3 = env_add_var_info (n_decls - i, (loc, name), linst, ltyp) _ctx in - process_var_info tl ctx3 nacc (i + 1)) + let ctx3 = env_add_var_info (0, (loc, name), linst, ltyp) _ctx in + process_var_info tl ctx3 nacc (m - 1)) (* Skip the variable *) - | ((loc, name), None, _) -> (lexp_warning loc ("Unused Variable: " ^ name); - process_var_info tl _ctx acc i) in + | ((loc, name), None, _) -> (lexp_warning loc "Unused Variable"; + process_var_info tl _ctx acc m) in - let acc, ctx = process_var_info decls nctx [] 0 in + let acc, ctx = process_var_info decls nctx [] n in acc, ctx -and lexp_parse_all (p: pexp list) (ctx: lexp_context): +and lexp_parse_all (p: pexp list) (ctx: lexp_context) bound: (lexp list * lexp_context) = let rec loop (plst: pexp list) ctx (acc: lexp list) = match plst with | [] -> ((List.rev acc), ctx) - | _ -> let lxp = lexp_parse (List.hd plst) ctx in + | _ -> let lxp = _lexp_parse (List.hd plst) ctx bound in (loop (List.tl plst) ctx (lxp::acc)) in (loop p ctx []) (* + * Free Variables + * --------------------- *) +(** Return a list of all free variables contained in an expression lxp *) + +(* Tree Nodes that make reference to declarations are: + * Call/Var/Cons + *) + +(* free_var should use a lexp since we are going to need free_v during eval *) +and free_variable pxp = +(* Expression that can have free variables: + * - Lambda + * - Let + * - Call + * Expression that can be free variables: + * - Var/ Function (Call) *) + + let bound = StringSet.empty in (* bound variables *) + let free = ([], StringSet.empty) in (* decl order * map *) + + let rec _fv pxp (bound, free) = + match pxp with + | Plambda (_, (_, name), _, body) -> + let bound = StringSet.add name bound in + _fv body (bound, free) + + (* + | Plet (_, args, body) -> + + let bound = List.fold_left + (fun s ((_, name), _, _) -> StringSet.add name s) bound args in + _fv body bound free *) + + | Pcall (xp, lst) -> + (* check if function is declared outside *) + let (bound, free) = _fv xp (bound, free) in + let pargs = List.map pexp_parse lst in + (* check for fv inside call args *) + List.fold_left (fun a g -> _fv g a) (bound, free) pargs + + | Pvar (_, name) ->( + try let _ = StringSet.find name bound in + (bound, free) + with + Not_found ->( + let (arr, set) = free in + try let _ = StringSet.find name set in + (bound, free) + with + Not_found ->( + let set = StringSet.add name set in + let arr = name :: arr in + (bound, (arr, set))))) + | _ -> (bound, free) in + + let (bound, (afree, sfree)) = _fv pxp (bound, free) in + (bound, (List.rev afree, sfree)) + + +(* * Type Inference * --------------------- *) (* Parsing a Pexp into an Lexp is really "elaboration", i.e. it needs to @@ -446,14 +537,43 @@ and lexp_parse_all (p: pexp list) (ctx: lexp_context): * - use lexp_p_check whenever you can. *) -and lexp_p_infer (p : pexp) (env : lexp_context) : lexp * ltype = - let lxp = lexp_parse p env in - lxp, UnknownType(dummy_location) +and lexp_p_infer (p : pexp) (env : lexp_context) bound: lexp * ltype = + + (* Parse expr *) + let tloc = pexp_location p in + let lxp = _lexp_parse p env bound in + + (* determine type *) + match lxp with + (* Trivial *) + | Imm (sxp) -> ( + match sxp with + | Integer _ -> (lxp, type_int) + | Float _ -> (lxp, type_float) + | _ -> lexp_error tloc "Could not infer type"; + (lxp, UnknownType(tloc))) + + + (* Pcall lookup fname *) + (* Pinductive *) + (* PCons return its Pinductive type *) + + (* Plambda *) + (* we need to build (t0 -> ... -> tn) *) + + (* PCase *) + (* return target type *) + + (**) + + (* dev catch all *) + | _ -> (lxp, UnknownType(dloc)) + 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 + -> let (e, inferred_t) = lexp_p_infer p env (0, 0) in (* FIXME: check that inferred_t = t! *) e (* @@ -461,7 +581,6 @@ and lexp_p_check (p : pexp) (t : ltype) (env : lexp_context): lexp = * --------------------- *) (* 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 *) let (pty, indent, prtp) = opt in @@ -549,9 +668,12 @@ and lexp_print_adv opt exp = print_string "| _ -> "; slexp_print df; print_string ";"; if pty then print_string "\n"; end + | Builtin (tp, name, lxp) -> + print_string name; + (* debug catch all *) | UnknownType (loc) -> print_string "unkwn"; - | _ -> print_string "Printint Not Implemented" + | _ -> print_string "Printing Not Implemented" and lexp_print_ctors opt ctors = @@ -650,7 +772,7 @@ let _lexp_expr_str (str: string) (tenv: bool array) let toks = lex tenv pretoks in let sxps = sexp_parse_all_to_list grm toks limit in let pxps = pexp_parse_all sxps in - lexp_parse_all pxps ctx + lexp_parse_all pxps ctx (0, 0) ;; (* specialized version *) ===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -353,6 +353,18 @@ and pexp_u_decls ds = let pexp_print e = sexp_print (pexp_unparse e) +(* Parse All Pexp as a list *) +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 +;; + let pexp_decls_all (nodes: sexp list): ((pvar * pexp * bool) list) = let rec loop nodes acc = match nodes with @@ -364,20 +376,19 @@ let pexp_decls_all (nodes: sexp list): ((pvar * pexp * bool) list) = loop nodes [] ;; -(* Parse All Pexp as a list *) -let pexp_parse_all (nodes: sexp list) = - List.map pexp_parse nodes -;; +(* String Parsing + * ------------------------ *) -(* Pexp String - * ------------------- *) -let _pexp_expr_str (str: string) tenv grm limit = +(* Lexp helper *) +let _pexp_expr_str (str: string) (tenv: bool array) + (grm: grammar) (limit: string option) = 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 ;; +(* specialized version *) let pexp_expr_str str = _pexp_expr_str str default_stt default_grammar (Some ";") ;; @@ -390,6 +401,7 @@ let _pexp_decl_str (str: string) tenv grm limit = pexp_decls_all sxps ;; +(* specialized version *) let pexp_decl_str str = _pexp_decl_str str default_stt default_grammar (Some ";") ;; ===================================== tests/REPL.ml ===================================== --- a/tests/REPL.ml +++ b/tests/REPL.ml @@ -116,7 +116,7 @@ let ieval_string str lctx rctx = let v, rctx = ieval_all lxps rctx in v, lctx, rctx ;; - + (* Specials commands %[command-name] *) let rec repl () = let tenv = default_stt in ===================================== tests/debug.ml ===================================== --- a/tests/debug.ml +++ b/tests/debug.ml @@ -43,7 +43,6 @@ open Lparse open Debruijn open Fmt open Grammar -open Eval (* Print aPretokens *) let rec debug_pretokens_print pretoken = ===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -9,6 +9,28 @@ let lctx = make_lexp_context let lctx = add_def "_+_" lctx let lctx = add_def "_*_" lctx let rctx = make_runtime_ctx +let rctx = add_rte_variable (Some "_+_") dlxp rctx +let rctx = add_rte_variable (Some "_-_") dlxp rctx + + +let _ = (add_test "EVAL" "Variable Cascade" (fun () -> + + let dcode = " + a = 10; + b = a; + c = b; + d = c;" in + + let rctx, lctx = eval_decl_str dcode lctx rctx in + + let ecode = "d;" in + + let ret = eval_expr_str ecode lctx rctx in + + match ret with + | [r] -> expect_equal_int (get_int r) 10 + | _ -> failure ()) +);; (* Let @@ -17,7 +39,7 @@ let rctx = make_runtime_ctx let _ = (add_test "EVAL" "Let" (fun () -> (* Noise. Makes sure the correct variables are selected *) let dcode = " - c = 3; a = 1; b = 2; d = 4;" in + c = 3; e = 1; f = 2; d = 4;" in let rctx, lctx = eval_decl_str dcode lctx rctx in let ecode = " @@ -26,7 +48,7 @@ let _ = (add_test "EVAL" "Let" (fun () -> let ret = eval_expr_str ecode lctx rctx in (* Expect a single result *) match ret with - | [r] -> expect_equal_int 30 (get_int r) + | [r] -> expect_equal_int (get_int r) 30 | _ -> failure ()) ) ;; @@ -65,25 +87,29 @@ let _ = (add_test "EVAL" "Nested Lambda" (fun () -> ;; (* Cases + Inductive types - * ------------------------ *) (* + * ------------------------ *) let _ = (add_test "EVAL" "Case" (fun () -> - (* Inductive type declaration *) + (* Inductive type declaration + Noisy declarations *) let code = " + i = 90;\n idt = inductive_ (idtd) (ctr0) (ctr1 idt) (ctr2 idt) (ctr3 idt);\n + j = 100;\n - ctr0 = inductive-cons idt ctr0;\n - ctr1 = inductive-cons idt ctr1;\n - ctr2 = inductive-cons idt ctr2;\n - ctr3 = inductive-cons idt ctr2;\n + d = 10;\n + ctr0 = inductive-cons idt ctr0;\n e = 20;\n + ctr1 = inductive-cons idt ctr1;\n f = 30;\n + ctr2 = inductive-cons idt ctr2;\n g = 40;\n + ctr3 = inductive-cons idt ctr2;\n h = 50;\n - a = (ctr1 (ctr2 ctr0));\n - b = (ctr2 (ctr2 ctr0));\n - c = (ctr3 (ctr2 ctr0));\n + x = 1;\n + a = (ctr1 (ctr2 ctr0));\n y = 2;\n + b = (ctr2 (ctr2 ctr0));\n z = 3;\n + c = (ctr3 (ctr2 ctr0));\n w = 4;\n - test_fun = lambda x -> case x\n - | ctr1 y => 1\n - | ctr2 y => 2\n + test_fun = lambda k -> case k\n + | ctr1 l => 1\n + | ctr2 l => 2\n | _ => 3;\n" in let rctx, lctx = eval_decl_str code lctx rctx in @@ -92,7 +118,7 @@ let _ = (add_test "EVAL" "Case" (fun () -> (* Eval defined lambda *) let ret = eval_expr_str rcode lctx rctx in - (* Expect a 3 results *) + (* Expect 3 results *) match ret with | [a; b; c] -> let t1 = expect_equal_int (get_int a) 1 in @@ -104,19 +130,21 @@ let _ = (add_test "EVAL" "Case" (fun () -> failure () | _ -> failure ()) ) -;; *) +;; + let _ = (add_test "EVAL" "Recursive Call" (fun () -> (* Inductive type declaration *) let code = " - Nat = inductive_ (dNat) (zero) (succ Nat); + a = 1;\n + Nat = inductive_ (dNat) (zero) (succ Nat); b = 2;\n - zero = inductive-cons Nat zero; - succ = inductive-cons Nat succ; + zero = inductive-cons Nat zero; c = 3;\n + succ = inductive-cons Nat succ; d = 4;\n - one = (succ zero); - two = (succ one); - three = (succ three); + one = (succ zero); e = 5;\n + two = (succ one); f = 6;\n + three = (succ three); g = 7;\n tonum = lambda x -> case x | (succ y) => (1 + (tonum y)) @@ -124,22 +152,20 @@ let _ = (add_test "EVAL" "Recursive Call" (fun () -> let rctx, lctx = eval_decl_str code lctx rctx in - let rcode = "(tonum one);"in + let rcode = "(tonum zero); (tonum zero); (tonum zero);"in (* Eval defined lambda *) let ret = eval_expr_str rcode lctx rctx in (* Expect a 3 results *) match ret with - | [a] -> expect_equal_int (get_int a) 1 - - (*| [a; b; c] -> - let t1 = expect_equal_int (get_int a) 1 in - let t2 = expect_equal_int (get_int b) 2 in - let t3 = expect_equal_int (get_int c) 3 in + | [a; b; c] -> + let t1 = expect_equal_int (get_int a) 0 in + let t2 = expect_equal_int (get_int b) 1 in + let t3 = expect_equal_int (get_int c) 2 in if t1 = 0 && t2 = 0 && t3 = 0 then success () else - failure () *) + failure () | _ -> failure ()) ) ;; ===================================== tests/full_debug.ml ===================================== --- a/tests/full_debug.ml +++ b/tests/full_debug.ml ===================================== tests/lexp_test.ml ===================================== --- a/tests/lexp_test.ml +++ b/tests/lexp_test.ml @@ -1,47 +1,64 @@ -open Lparse +open Lparse (* add_def *) open Debruijn (* make_lexp_context *) -open Lexp -open Utest_lib +open Lexp +open Utest_lib (* default environment *) let lctx = make_lexp_context let lctx = add_def "_+_" lctx let lctx = add_def "_*_" lctx + + +let _ = (add_test "LEXP" "Built-in Inference" (fun () -> + + let dcode = "a = 10; b = 1.12;" in + + let ret, _ = lexp_decl_str dcode lctx in -(* Check if annotation are parsed and kept *) -(* Let and top level declarations are using the same code *) -(* We only have to check if let's type parsing is correct *) -let _ = (add_test "LEXP" "Type Parsing" (fun () -> + match ret with + (* (vdef * lexp * ltype) *) + | [(_, _, Builtin(_, "Int", _)); + (_, _, Builtin(_, "Float", _))] -> + success() + + | _ -> failure ()) +);; + +open Pexp + + +let set_to_list s = + StringSet.fold (fun g a -> g::a) s [] +;; + +let _ = (add_test "LEXP" "Free Variable" (fun () -> - (* This is garbage. I just want Nat to be defined *) let dcode = " - Nat = inductive_ (dNat) (zero) (succ Nat);\n" in - - let _, lctx = lexp_decl_str dcode lctx in + a = 2; + b = 3; + f = lambda n -> (a + n); % a is a fv + g = lambda x -> ((f b) + a + x); % f,a,b is fv + " in + + let ret = pexp_decl_str dcode in + let (_, g, _)::_ = List.rev ret in + + let (bound, free) = free_variable g in - let ecode = " - let a : Nat; a = 1; b : Nat; b = 3; - in - a + b;" in - - let ret, _ = lexp_expr_str ecode lctx in - match ret with - | [expr] ->( - match expr with - | Let(_, arg, _) -> match arg with - | [] -> failure () - | (_, xp, tp)::_ ->( - (* tp must match Nat *) - match tp with - | Var((_, name), _) -> expect_equal_str name "Nat" - | _ -> failure () - ) + let bound = set_to_list bound in + let (free, _) = free in + + match bound with + | ["x"] ->( + match free with + | ["_+_"; "f"; "b"; "a"] -> success () | _ -> failure ()) - | [] -> failure ()) -) -;; + | _ -> failure () +));; + +(* run all tests *) run_all () ;; \ No newline at end of file ===================================== tests/utest_lib.ml ===================================== --- a/tests/utest_lib.ml +++ b/tests/utest_lib.ml @@ -30,6 +30,7 @@ * * --------------------------------------------------------------------------- *) +open Util module StringMap = @@ -39,7 +40,7 @@ module StringMap = type test_fun = (unit -> int) type tests = (test_fun) StringMap.t -type sections = (tests) StringMap.t +type sections = ((tests) StringMap.t) * string list let success () = 0;; let failure () = (-1);; @@ -52,6 +53,8 @@ let failure () = (-1);; * "Lambda" - "Nested" *) let _global_sections = ref StringMap.empty +let _insertion_order = ref [] +let _ret_code = ref 0 (* USAGE *) @@ -70,35 +73,76 @@ let _global_sections = ref StringMap.empty let add_test sname tname tfun = (* Does Section Exists ? *) - let tmap = - try + let (tmap, lst) = + try StringMap.find sname (!_global_sections) with - Not_found -> StringMap.empty in + Not_found -> + _insertion_order := sname::(!_insertion_order); + StringMap.empty, ref [] in + + try let _ = StringMap.find tname tmap in + print_string "TEST ALREADY EXISTS" + with + Not_found -> + + lst := tname::(!lst); (* add test *) let ntmap = StringMap.add tname tfun tmap in - _global_sections := StringMap.add sname ntmap (!_global_sections); + _global_sections := StringMap.add sname (ntmap, lst) (!_global_sections); + +;; + +let unexpected_throw sk tk e = + print_string ("[ FAIL] " ^ sk ^ " - " ^ tk ^ "\n"); + match e with + | Internal_error msg -> + print_string ("[ ] UNEXPECTED THROW: " ^ msg ^ "\n") + | _ ->( + print_string "[ ] UNEXPECTED THROW: \n"; + print_string "[ ] "; + print_string (Printexc.to_string e); print_string "\n") ;; (* Run all *) let run_all () = + _insertion_order := List.rev (!_insertion_order); + (* iter over all sections *) - StringMap.iter (fun sk sv -> + List.iter (fun sk -> + + let tmap, tst = StringMap.find sk (!_global_sections) in + tst := List.rev (!tst); + print_string ("[RUN ] " ^ sk ^ " \n"); + (* iter over all tests in the current sections *) - StringMap.iter (fun tk tv -> - (* RUN TEST*) - let r = tv () in - if r = 0 then - (print_string ("[ OK] " ^ sk ^ " - " ^ tk ^ "\n")) - else - (print_string ("[ FAIL] " ^ sk ^ " - " ^ tk ^ "\n")) + List.iter (fun tk -> + let tv = StringMap.find tk tmap in + + (* RUN TEST *) + flush stdout; + try + let r = tv () in + if r = 0 then + (print_string ("[ OK] " ^ sk ^ " - " ^ tk ^ "\n")) + else( + (print_string ("[ FAIL] " ^ sk ^ " - " ^ tk ^ "\n"); + _ret_code := failure () + )) + with e + -> _ret_code := failure (); + unexpected_throw sk tk e ) - sv; - flush stdout; + (!tst); + ) - (!_global_sections) + (!_insertion_order); + + (* return success or failure *) + exit !_ret_code +;; let expect_equal_int value expect = ===================================== tests/utest_main.ml ===================================== --- a/tests/utest_main.ml +++ b/tests/utest_main.ml @@ -66,8 +66,10 @@ let main () = begin tests_n := !tests_n + 1; - exit_code := Sys.command (folder ^ files.(i) ^ " " ^ root_folder); + + (if !exit_code != 0 then + failed_test := !failed_test + 1) end) done; View it on GitLab: https://gitlab.com/monnier/typer/compare/6cd883591bc13c03681fd31b642bc04fa5…

1 0

Recursion et Indices de Debruijn
by Pierre Delaunay 21 Mar '16

21 Mar '16

Bonjour, J'aimerais juste faire une rapide "sanity check" sur les indices de De Bruijn * * r_index * / * [4] Nat = [..] * [3] a = [..] r_index r_offset * [2] b = [..] \ / * [1] zero = Nat [..] || Nat DBI = 4 - 1 = 3 (zero, a, b) * [0] one = Nat [..] || Nat DBI = 4 - 0 = 4 * || Zero DBI = 1 Dans le cas d'une récursion j'ai besoin de repérer les variables libres pour les push dans le contexte de la lambda. Cette étape va être faite deux fois, une fois pendant le lexp parsing pour déterminer l'index et une fois pendant l'évaluation pour créer le contexte de la lambda. -- Pierre Delaunay

3 3