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

[Git][monnier/typer][master] Fix Macro handling. Removed some dead code
by Setepenre 29 Avr '16

29 Avr '16

Setepenre pushed to branch master at Stefan / Typer Commits: 3be5ffe6 by Pierre Delaunay at 2016-04-29T12:21:49-04:00 Fix Macro handling. Removed some dead code Changes to be committed: * src/lparse.ml - - - - - 10 changed files: - btl/list.typer - samples/macro.typer - samples/nat.typer - src/builtin.ml - src/debug.ml - src/env.ml - src/eval.ml - src/lexp.ml - src/lparse.ml - tests/eval_test.ml Changes: ===================================== btl/list.typer ===================================== --- a/btl/list.typer +++ b/btl/list.typer @@ -25,4 +25,6 @@ tail = lambda a => lambda xs -> case xs | nil => nil - | cons hd tl => tl; \ No newline at end of file + | cons hd tl => tl; + + ===================================== samples/macro.typer ===================================== --- a/samples/macro.typer +++ b/samples/macro.typer @@ -11,4 +11,4 @@ give_type = lambda expr -> sqr = Macro_ (give_type sqr_fun sqr_type); -main = (sqr 2); \ No newline at end of file +main = (sqr 2); ===================================== samples/nat.typer ===================================== --- a/samples/nat.typer +++ b/samples/nat.typer @@ -25,8 +25,6 @@ n1 = (to-num zero); n2 = (to-num one); n3 = (to-num two); - - -m1 = (to-num (plus zero two)); % 2 +m1 = (to-num (plus zero two)); % 2 m2 = (to-num (plus two zero)); % 2 m3 = (to-num (plus two one)); % 3 \ No newline at end of file ===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -85,17 +85,14 @@ let builtin_fmult = Builtin (FMult, "_*_", fop_binary) *) (* Builtin of builtin * string * ltype *) let _generic_binary_iop name f loc (args_val: value_type list) (ctx: runtime_env) = - (* We don't have to access context because: *) - (* x + y is parsed as Call(_+_ x y) *) - (* Partial application handling aggregates arguments in a ctx *) - (* once all arguments are present Call(_+_ x y) is called *) - (* First, its arguments are evaluated which is where x, y are replaced *) - (* by their value in the context then _generic_binary_iop handle the function *) - (* i.e we don't need to push x and y in the context. *) - (* We don't even need the context *) - let l, r = match args_val with - | [a; b] -> a, b - | _ -> builtin_error loc (name ^ " expects 2 arguments") in + + (* + let l, r = get_rte_variable None 0 ctx, + get_rte_variable None 1 ctx in *) + + let l, r = match args_val with + | [l; r] -> l, r + | _ -> builtin_error loc (name ^ " expects 2 Integers arguments") in match l, r with | Vint(v), Vint(w) -> Vint(f v w) @@ -169,13 +166,12 @@ let builtin_float = Builtin (SexpType, "float_", type_mfloat) let builtin_node = Builtin (SexpType, "node_", type_mnode) (* let builtin_expand = Builtin (SexpType, "expand_", type_mexpand) *) -let type_macro = - let ctors = SMap.empty in - let ctors = SMap.add "Macro_" [(Aexplicit, None, type_sexp)] ctors in - Inductive (dloc, (dloc, "built-in"), [], ctors) let builtin_macro = Cons (((dloc, "Macro"), (-4)), (dloc, "Macro_")) -let macro_cons = Arrow (Aexplicit, None, type_sexp , dloc, type_macro) +let type_macro = Builtin (MacroType, "Macro", type0) +let macro_cons = Arrow (Aexplicit, None, type_sexp, dloc, type_macro) + + (* * Should we have a function that * -> returns a new context inside typer ? (So we need to add a ctx type too) @@ -222,7 +218,7 @@ let _builtin_lookup = SMap.empty typer_builtins -let get_builtin_impl btype str ltp loc = +let get_builtin_impl btype str loc = try SMap.find str _builtin_lookup with Not_found -> builtin_error loc "Requested Built-in does not exist" ===================================== src/debug.ml ===================================== --- a/src/debug.ml +++ b/src/debug.ml @@ -189,25 +189,35 @@ let str_split str sep = List.rev (!ret));; let debug_lexp_decls decls = - + let sep = " : " in List.iter (fun e -> let ((loc, name), lxp, ltp) = e in print_string " "; lalign_print_string (lexp_to_string lxp) 15; - print_string "["; print_loc loc; print_string "] "; + print_string "["; print_loc loc; print_string "]"; let str = _lexp_str_decls (!debug_ppctx) [e] in + (* First col size = 15 + 1 + 2 + 3 + 5 + 6 + * = 32 *) + let str = match str with - | hd::tl -> print_string hd; print_string "\n"; tl + | fst::tl -> print_string (sep ^ fst); print_string "\n"; tl | _ -> [] in (* inefficient but makes things pretty iff -fmt-pretty=on *) let str = List.flatten (List.map (fun g -> str_split g '\n') str) in + let str = match str with + | scd::tl -> + print_string " FILE: "; + lalign_print_string loc.file 25; + print_string (sep ^ scd); print_string "\n"; tl + | _ -> [] in + List.iter (fun g -> - print_string (make_line ' ' 34); + print_string ((make_line ' ' 32) ^ sep); print_string g; print_string "\n") str; ===================================== src/env.ml ===================================== --- a/src/env.ml +++ b/src/env.ml @@ -54,7 +54,7 @@ type value_type = | Vint of int | Vstring of string | Vcons of symbol * value_type list - | Vbuiltin + | Vbuiltin of builtin * string | Closure of lexp * (((string option * value_type) ref myers) * (int * int)) (* Macro type *) | Vsexp of sexp @@ -74,11 +74,8 @@ let rec value_print (vtp: value_type) = List.iter (fun arg -> print_string " "; value_print arg) args; print_string ")"; - + | Vbuiltin(_, str) -> print_string str | Vdummy -> print_string "value_print_dummy" - | Vbuiltin -> print_string "value_print_builtin" - | _ -> print_string "value_print_bug" - let value_location (vtp: value_type) = match vtp with @@ -178,9 +175,10 @@ let temp_ctx (ctx: runtime_env): runtime_env = let (l, (osize, _)) = ctx in let tsize = length l in (* Check if temporary variables are present *) - if tsize != osize then - (* remove them *) - (select_n ctx osize) + if tsize != osize then( + (* remove them + print_string "temp ctx was useful\n"; *) + (select_n ctx osize)) else ctx ;; ===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -74,14 +74,14 @@ let rec _eval lxp ctx i: (value_type) = match lxp with (* Leafs *) (* ---------------- *) - | Imm(Integer (_, i)) -> Vint(i) - | Imm(String (_, s)) -> Vstring(s) - | Inductive (_, _, _, _) -> Vdummy - | Cons (_, label) -> Vcons (label, []) - | Lambda (_, _, _, lxp) -> Closure(lxp, ctx) - | Builtin _ -> Vbuiltin - - (* Return a value stored in the env *) + | Imm(Integer (_, i)) -> Vint(i) + | Imm(String (_, s)) -> Vstring(s) + | Inductive (_, _, _, _) -> Vdummy + | Cons (_, label) -> Vcons (label, []) + | Lambda (_, _, _, lxp) -> Closure(lxp, ctx) + | Builtin (btype, str, _) -> Vbuiltin(btype, str) + + (* Return a value stored in env *) | Var((loc, name), idx) as e -> eval_var ctx e ((loc, name), idx) (* Nodes *) @@ -90,22 +90,12 @@ let rec _eval lxp ctx i: (value_type) = let nctx = _eval_decls decls ctx i in _eval inst nctx (i + 1) - (* Built-in Function *) - | Call(Builtin(btype, str, ltp), args)-> - (* built-in does not have location info. So we extract it from args *) - let tloc = match args with - | (_, hd)::tl -> lexp_location hd - | _ -> dloc in - let args_val = List.map (fun (k, e) -> _eval e ctx (i + 1)) args in - (get_builtin_impl btype str ltp tloc) tloc args_val ctx - (* Function call *) - | Call (lname, args) as call -> eval_call ctx i lname args call + | Call (lname, args) -> eval_call ctx i lname args (* Case *) | Case (loc, target, _, pat, dflt) -> (eval_case ctx i loc target pat dflt) - | _ -> print_string "debug catch-all eval: "; lexp_print lxp; Vstring("eval Not Implemented") @@ -115,16 +105,30 @@ and eval_var ctx lxp v = with e -> eval_error loc ("Variable: " ^ name ^ (str_idx idx) ^ " was not found ") -and eval_call ctx i lname args call = - (* create a clean environment *) - let args_val = List.map (fun (k, e) -> _eval e ctx (i + 1)) args in - let clean_ctx = temp_ctx ctx in +and eval_call ctx i lname args = + let loc = lexp_location lname in + let args = List.map (fun (k, e) -> _eval e ctx (i + 1)) args in + let f = _eval lname ctx (i + 1) in + + (* + let eval_call' f arg = + match f with + | Vcons(label, fields) -> + Vcons (label, arg::fields) + + | Closure (lxp, ctx) -> + _eval lxp (add_rte_variable None arg ctx) (i + 1) + + | Vbuiltin (btype, str) -> + (get_builtin_impl btype str loc) loc [] (add_rte_variable None arg ctx) - (* get function body *) - let body = _eval lname ctx (i + 1) in + | _ -> value_print f; + eval_error loc "Cannot eval function" in - let rec eval_call body args ctx = - match body, args with + List.fold_left eval_call' f args *) + + let rec eval_call f args ctx = + match f, args with | Vcons (n, []), _ -> Vcons(n, args) (* we add an argument to the closure *) @@ -133,16 +137,18 @@ and eval_call ctx i lname args call = let ret = _eval lxp nctx (i + 1) in eval_call ret tl nctx - (* No more arguments *) - | Closure (_, _), [] -> body + | Vbuiltin (btype, str), args -> + (* lookup the built-in implementation and call it *) + (get_builtin_impl btype str loc) loc args ctx (* return result of eval *) - | _, [] -> body + | Closure (_, _), [] -> f + | _, [] -> f - | _ -> value_print body; - eval_error dloc "Cannot eval function" in + | _ -> value_print f; + eval_error loc "Cannot eval function" in - eval_call body args_val clean_ctx + eval_call f args ctx and eval_case ctx i loc target pat dflt = (* Eval target *) @@ -160,7 +166,7 @@ and eval_case ctx i loc target pat dflt = (* -- Crash -- *) eval_error loc "Target is not a Constructor" in - let ctor_n = List.length args in + (* let ctor_n = List.length args in *) (* Check if a default is present *) let run_default df = @@ -186,7 +192,8 @@ and eval_case ctx i loc target pat dflt = (* Get working pattern *) let key, (_, pat_args, exp) = SMap.min_binding sol in - (* build context (List.fold2 has problem with some cases) *) + (* build context (List.fold2 has problem with some cases) *) + (* This is more robust *) let rec fold2 nctx pats args = match pats, args with | (Some (_, (_, name)))::pats, arg::args -> @@ -267,9 +274,9 @@ let eval_all lxps rctx silent = (* build a rctx from a lctx *) let from_lctx (ctx: lexp_context): runtime_env = let ((_, _), env, _) = ctx in - let rctx = ref (default_rctx ()) in + let rctx = ref make_runtime_ctx in - (* Skip builtins *) + (* Skip builtins: They are already in default_rctx() *) let bsize = List.length typer_builtins in let csize = get_size ctx in @@ -295,7 +302,3 @@ let from_lctx (ctx: lexp_context): runtime_env = rctx := set_rte_variable j (Some name) vxp (!rctx) done; !rctx - - - - ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -622,14 +622,19 @@ and _lexp_to_str ctx exp = | Call(fname, args) -> ( (* get function name *) - let str, idx = match fname with - | Var((_, name), idx) -> name, idx - | Builtin (_, name, _) -> name, 0 - | _ -> (error "unkwn"), -1 in + let str, idx, inner_parens, outer_parens = match fname with + | Var((_, name), idx) -> name, idx, false, true + | Builtin (_, name, _) -> name, 0, false, true + | Lambda _ -> "__", 0, true, false + | Cons _ -> "__", 0, false, false + | _ -> "__", -1, true, true in let binop_str op (_, lhs) (_, rhs) = (lexp_to_str lhs) ^ op ^ (lexp_to_str rhs) in + let add_parens bl str = + if bl then "(" ^ str ^ ")" else str in + match (str, args) with (* Special Operators *) | ("_=_", [lhs; rhs]) -> binop_str " = " lhs rhs @@ -643,7 +648,10 @@ and _lexp_to_str ctx exp = (fun str (_, lxp) -> str ^ " " ^ (lexp_to_str lxp)) "" args in - "(" ^ (fun_call (lexp_to_str fname)) ^ args ^ ")") + let str = fun_call (lexp_to_str fname) in + let str = add_parens inner_parens str in + let str = str ^ args in + add_parens outer_parens str) | Inductive (_, (_, name), [], ctors) -> (keyword "inductive_") ^ " (" ^ name ^") " ^ ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -339,12 +339,12 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = let new_args = List.map (fun g -> (Aexplicit, g)) largs in (* consume Arrows and args together *) - let rec get_return_type i ltp args = + let rec get_return_type name i ltp args = match ltp, args with | _, [] -> ltp - | Arrow(_, _, _, _, ltp), hd::tl -> (get_return_type (i + 1) ltp tl) + | Arrow(_, _, _, _, ltp), hd::tl -> (get_return_type name (i + 1) ltp tl) | _, _ -> lexp_warning loc - ("Function was provided with too many args. Expected: " ^ + (name ^ " was provided with too many args. Expected: " ^ (string_of_int i)); ltp in (* Vanilla : sqr is inferred and (lambda x -> x * x) is returned @@ -354,13 +354,13 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = (* retrieve function's body *) let body, ltp = _lexp_p_infer fun_name ctx (i + 1) in - let ret_type = get_return_type 0 ltp new_args in + (* let ret_type = get_return_type 0 ltp new_args in *) - (* handle named functions*) - let named_call (loc, name) = + let handle_named_call (loc, name) = try (* Check if the function was defined *) let idx = senv_lookup name ctx in let vf = (make_var name idx loc) in + let ret_type = get_return_type name 0 ltp new_args in (* Replace a built-in name by builtin so they can be recognized * during eval *) @@ -378,131 +378,53 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = let vf = (make_var name (-1) loc) in Call(vf, new_args), ltp in - (* determine function type *) - match fun_name, ltp with - (* Anonymous *) - | ((Plambda _), _) -> Call(body, new_args), ltp - - (* Call to a macro *) - | (Pvar (loc, name), Inductive _) -> - (* look up for definition *) - let idx = senv_lookup name ctx in - let vf = (make_var name idx loc) in + let handle_macro_call (loc, name) = + (* look up for definition *) + let idx = try senv_lookup name ctx + with Not_found -> + lexp_fatal loc ("Could not find Variable: " ^ name) in - (* Get the macro *) - let lxp = match env_lookup_expr ctx ((loc, name), idx) with - | None -> lexp_fatal loc "The macro cannot be expanded"; - | Some e -> e in + (* Get the macro *) + let lxp = try match env_lookup_expr ctx ((loc, name), idx) with + | None -> lexp_fatal loc "The macro cannot be expanded"; + | Some e -> e + with Not_found -> + lexp_fatal loc (name ^ " was found but " ^ (string_of_int idx) ^ + " is not a correct index.") in - print_string "HERE"; + let rctx = try (from_lctx ctx) + with e -> + lexp_fatal loc "Could not convert lexp context into rte context" in - let rctx = (from_lctx ctx) in + let sxp = match eval lxp rctx with + (* (Macro_ sexp) is returned *) + | Vcons(_, [Vsexp(sxp)]) -> sxp + | v -> value_print v; print_string "\n"; + lexp_fatal loc "Macro_ expects sexp" in - print_string "HERE"; + let pxp = pexp_parse sxp in + (* Generated Code *) + let lxp, ltp = _lexp_p_infer pxp ctx (i + 1) in + Call(lxp, new_args), ltp in - let sxp = match eval lxp rctx with - | Vsexp(sxp) -> sxp - | v -> value_print v; - lexp_fatal loc "Macro_ expects sexp" in + (* determine function type *) + match fun_name, ltp with + (* Anonymous *) + | ((Plambda _), _) -> Call(body, new_args), ltp - let pxp = pexp_parse sxp in - (* Generated Code *) - let lxp, ltp = _lexp_p_infer pxp ctx (i + 1) in - Call(lxp, new_args), ltp + (* Call to a macro *) + | (Pvar (l, n), Builtin(tp, "Macro", _)) when tp = MacroType -> + handle_macro_call (l, n) (* Call to Vanilla or constructor *) - | (Pvar v, _) -> named_call v + | (Pvar v, _) -> handle_named_call v (* Constructor. This case is rarely used *) - | (Pcons(_, v), _) -> named_call v + | (Pcons(_, v), _) -> handle_named_call v | e, _ -> lexp_fatal (pexp_location e) "This expression cannot be called" - (* - (* Process Arguments *) - let pargs = List.map pexp_parse _args in - let largs = _lexp_parse_all pargs ctx i in - let new_args = List.map (fun g -> (Aexplicit, g)) largs in - - (* check if anonymous *) - match fname with - (* arg_kind * pvar * pexp option * pexp *) - | Plambda _ -> let lbd, ltype = _lexp_p_infer fname ctx (i + 1) in - Call(lbd, new_args), ltype - - | _ -> begin - - (* get function name *) - let name, loc = match fname with - | Pvar(loc, nm) -> nm, loc - | Pcons (_, (loc, nm)) -> nm, loc - | _-> - lexp_fatal (pexp_location fname) "This expression cannot be called" in - - (* retrieve function body *) - let body, ltp = _lexp_p_infer fname ctx (i + 1) in - - (* Check if macro *) - let _ = match ltp with - | Inductive (_, (_, "built-in"), [], _) -> lexp_print body; print_string "\n"; - | _ -> () in - - try - - (* Check if the function was defined *) - let idx = senv_lookup name ctx in - let vf = (make_var name idx loc) in - - (* consume Arrows and args together *) - let rec get_return_type i ltp args = - match ltp, args with - | _, [] -> ltp - | Arrow(_, _, _, _, ltp), hd::tl -> (get_return_type (i + 1) ltp tl) - | _, _ -> lexp_warning loc ("\""^ name ^ - "\" was provided with too many args. Expected: " ^ - (string_of_int i)); ltp in - - let ret_type = get_return_type 0 ltp new_args in - - (* Is the function built-in ? *) - (* built-in cannot be partially applied that is why we can get_return_type *) - (* they can only if you redefine the operation *) - if (is_lbuiltin idx ctx) then ( - match env_lookup_expr ctx ((loc, name), idx) with - | None -> lexp_error loc "Unknown builtin"; - Call(vf, new_args), ret_type - - (* Is it a macro ? *) - | Some Cons (((_, "Macro"), _), (_, "Macro_")) -> - Call(vf, new_args), type_macro - (* - let lxp = match largs with - | [lxp] -> lxp - | hd::tl -> lexp_error loc "Macro_ expects one lexp"; hd - | _ -> lexp_fatal loc "Macro_ expects one lexp" in - - let rctx = (from_lctx ctx) in - - (* eval argument *) - let sxp = match eval lxp rctx with - | Vsexp(sxp) -> sxp - | v -> lexp_fatal loc "Macro_ expects sexp" in - - let pxp = pexp_parse sxp in - _lexp_p_infer pxp ctx (i + 1) *) - - (* a builtin functions *) - | Some e -> Call(e, new_args), ret_type - ) - else Call(vf, new_args), ret_type - - 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), ltp end *) - (* Read a pattern and create the equivalent representation *) and lexp_read_pattern pattern exp target ctx: ((string * location * (arg_kind * vdef) option list) * lexp_context) = ===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -362,7 +362,7 @@ length = lambda a => lambda xs -> case xs | nil => 0 - | cons hd tl => (1 + length a tl); + | cons hd tl => (1 + (length a tl)); head : (a : Type) => List a -> a; head = lambda a => View it on GitLab: https://gitlab.com/monnier/typer/commit/3be5ffe62c3419a0b566b449bc9c3f6128e…

1 0

[Git][monnier/typer][master] Continued Stefan `value_type` changes
by Setepenre 28 Avr '16

28 Avr '16

Setepenre pushed to branch master at Stefan / Typer Commits: 4af18f1c by Pierre Delaunay at 2016-04-28T16:45:35-04:00 Continued Stefan `value_type` changes (Broke Macro Handling) Changes to be committed: * src/env.ml : value_type definition - no more `Value of lexp` - Adapted Files * src/eval.ml * src/builtin.ml * tests/* - - - - - 8 changed files: - + samples/nat.typer - src/builtin.ml - src/env.ml - src/eval.ml - src/lparse.ml - tests/env_test.ml - tests/eval_test.ml - tests/macro_test.ml Changes: ===================================== samples/nat.typer ===================================== --- /dev/null +++ b/samples/nat.typer @@ -0,0 +1,32 @@ +Nat = inductive_ (dNat) (zero) (succ Nat); + +zero = inductive-cons Nat zero; +succ = inductive-cons Nat succ; + +to-num : Nat -> Int; +to-num = lambda (x : Nat) -> + case x + | (succ y) => (1 + (to-num y)) + | zero => 0; + +one = (succ zero); +two = (succ one); +three = (succ two); + +plus : Nat -> Nat -> Nat; +plus = lambda (x : Nat) -> + lambda (y : Nat) -> + case x + | zero => y + | succ z => succ (plus z y); + + +n1 = (to-num zero); +n2 = (to-num one); +n3 = (to-num two); + + + +m1 = (to-num (plus zero two)); % 2 +m2 = (to-num (plus two zero)); % 2 +m3 = (to-num (plus two one)); % 3 \ No newline at end of file ===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -82,26 +82,6 @@ let builtin_eq = Builtin (EqType, "_=_", type_eq) let builtin_fadd = Builtin (FAdd, "_+_", fop_binary) let builtin_fmult = Builtin (FMult, "_*_", fop_binary) *) -(* Math Functions *) -let get_int (lxp: value_type): (int option) = - let lxp = get_value_lexp lxp in - match lxp with - | Imm(Integer(_, l)) -> Some l - | _ -> None -;; - -let get_string (lxp: value_type): (string option) = - let lxp = get_value_lexp lxp in - match lxp with - | Imm(String(_, l)) -> Some l - | _ -> None -;; - -let get_sexp (lxp: value_type): (sexp option) = - match lxp with - | Vsexp l -> Some l - | _ -> None -;; (* Builtin of builtin * string * ltype *) let _generic_binary_iop name f loc (args_val: value_type list) (ctx: runtime_env) = @@ -117,8 +97,8 @@ let _generic_binary_iop name f loc (args_val: value_type list) (ctx: runtime_env | [a; b] -> a, b | _ -> builtin_error loc (name ^ " expects 2 arguments") in - match (get_int l), (get_int r) with - | Some v, Some w -> Value(Imm(Integer (loc, (f v w)))) + match l, r with + | Vint(v), Vint(w) -> Vint(f v w) | _ -> value_print l; print_string " "; value_print r; builtin_error loc (name ^ " expects Integers as arguments") @@ -147,33 +127,29 @@ let make_symbol loc args_val ctx = | [r] -> r | _ -> builtin_error loc ("symbol_ expects 1 argument") in - let s = get_string lxp in - match s with - | Some str -> Vsexp(Symbol(loc, str)) + match lxp with + | Vstring(str) -> Vsexp(Symbol(loc, str)) | _ -> builtin_error loc ("symbol_ expects one string as argument") let make_node loc args_val ctx = - let head, args = match args_val with - | hd::tl -> (get_sexp hd), tl + let op, args = match args_val with + | Vsexp(s)::tl -> s, tl + | _::tl -> builtin_error loc ("node_ expects sexp as operator") | _ -> builtin_error loc ("node_ expects at least 2 arguments") in - let op = match head with - | Some sxp -> sxp - | None -> builtin_error loc ("node_ expects sexp as operator") in - - let s = List.map (fun g -> match get_sexp g with - | Some sxp -> sxp - | None -> builtin_error loc ("node_ expects sexp as arguments")) args in + let s = List.map (fun g -> match g with + | Vsexp(sxp) -> sxp + | _ -> builtin_error loc ("node_ expects sexp as arguments")) args in Vsexp(Node(op, s)) -let make_block loc args_val ctx = Value(type0) -let make_string loc args_val ctx = Value(type0) -let make_integer loc args_val ctx = Value(type0) -let make_float loc args_val ctx = Value(type0) +let make_block loc args_val ctx = Vdummy +let make_string loc args_val ctx = Vdummy +let make_integer loc args_val ctx = Vdummy +let make_float loc args_val ctx = Vdummy let type_string = type0 let type_mblock = type0 @@ -272,7 +248,7 @@ let default_rctx () = (* populate ctx *) List.fold_left (fun ctx (name, lxp, ltp, f) -> - add_rte_variable (Some name) (Value(lxp)) ctx) + add_rte_variable (Some name) (Vdummy) ctx) rctx typer_builtins ;; ===================================== src/env.ml ===================================== --- a/src/env.ml +++ b/src/env.ml @@ -51,31 +51,42 @@ let str_idx idx = "[" ^ (string_of_int idx) ^ "]" (* currently, we don't do much *) type value_type = - | Value of lexp + | Vint of int + | Vstring of string + | Vcons of symbol * value_type list + | Vbuiltin | Closure of lexp * (((string option * value_type) ref myers) * (int * int)) (* Macro type *) | Vsexp of sexp (* Unable to eval during macro expansion, only throw if the value is used *) | Vdummy -let get_value_lexp (vtp: value_type) = - match vtp with - | Value s -> s - | Closure (s, _) -> s - | _ -> env_error dloc "Does not hold a lexp" - -let value_print (vtp: value_type) = +let rec value_print (vtp: value_type) = match vtp with | Closure (lxp, _) -> print_string ("Closure(" ^ (_lexp_to_str (!debug_ppctx) lxp) ^ ")") - | Value s -> lexp_print s | Vsexp sxp -> sexp_print sxp - | _ -> print_string "value_print_dummy" + | Vint(i) -> print_int i; + | Vstring(s) -> print_string ("\"" ^ s ^ "\"") + | Vcons ((_, n), []) -> print_string n + | Vcons ((_, n), args) -> + print_string ("(" ^ n); + List.iter (fun arg -> print_string " "; value_print arg) args; + print_string ")"; -let value_location (vtp: value_type) = lexp_location (get_value_lexp vtp) + | Vdummy -> print_string "value_print_dummy" + | Vbuiltin -> print_string "value_print_builtin" + | _ -> print_string "value_print_bug" +let value_location (vtp: value_type) = + match vtp with + | Vcons ((loc, _), _) -> loc + | Closure (lxp, _) -> lexp_location lxp + (* location info was lost or never existed *) + | _ -> dloc + (* Runtime Environ *) type env_cell = (string option * value_type) ref type runtime_env = (env_cell myers) * (int * int) @@ -161,6 +172,8 @@ let select_n (ctx: runtime_env) n: runtime_env = ((!r), a) +(* This removes temporary variables from the environment *) +(* and create a clean context free of function arguments *) let temp_ctx (ctx: runtime_env): runtime_env = let (l, (osize, _)) = ctx in let tsize = length l in ===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -74,12 +74,12 @@ let rec _eval lxp ctx i: (value_type) = match lxp with (* Leafs *) (* ---------------- *) - | Imm(v) -> Value(lxp) - | Inductive (_, _, _, _) as e -> Value(e) - | Cons (_, _) as e -> Value(e) - - (* Lambda's body is evaluated when called *) - | Lambda (_, _, _, lxp) -> Closure(lxp, ctx) + | Imm(Integer (_, i)) -> Vint(i) + | Imm(String (_, s)) -> Vstring(s) + | Inductive (_, _, _, _) -> Vdummy + | Cons (_, label) -> Vcons (label, []) + | Lambda (_, _, _, lxp) -> Closure(lxp, ctx) + | Builtin _ -> Vbuiltin (* Return a value stored in the env *) | Var((loc, name), idx) as e -> eval_var ctx e ((loc, name), idx) @@ -90,9 +90,6 @@ let rec _eval lxp ctx i: (value_type) = let nctx = _eval_decls decls ctx i in _eval inst nctx (i + 1) - (* I don't really know why Built-in is ever evaluated... but it is sometimes *) - | Builtin _ -> Vdummy - (* Built-in Function *) | Call(Builtin(btype, str, ltp), args)-> (* built-in does not have location info. So we extract it from args *) @@ -110,7 +107,7 @@ let rec _eval lxp ctx i: (value_type) = | _ -> print_string "debug catch-all eval: "; - lexp_print lxp; Value(Imm(String(dloc, "eval Not Implemented"))) + lexp_print lxp; Vstring("eval Not Implemented") and eval_var ctx lxp v = let ((loc, name), idx) = v in @@ -128,19 +125,7 @@ and eval_call ctx i lname args call = let rec eval_call body args ctx = match body, args with - (* first lambda *) - | Value (lxp), hd::tl -> (match lxp with - | Cons _ -> - let cons_args = List.map (fun g -> - (Aexplicit, (get_value_lexp g))) args_val in - Value(Call(lname, (cons_args))) - | _ -> - (* Push first arg *) - let nctx = add_rte_variable None hd ctx in - (* eval first lambda *) - let ret = _eval lxp nctx (i + 1) in - - eval_call ret tl nctx) + | Vcons (n, []), _ -> Vcons(n, args) (* we add an argument to the closure *) | Closure (lxp, ctx), hd::tl -> @@ -150,7 +135,10 @@ and eval_call ctx i lname args call = (* No more arguments *) | Closure (_, _), [] -> body + + (* return result of eval *) | _, [] -> body + | _ -> value_print body; eval_error dloc "Cannot eval function" in @@ -158,114 +146,61 @@ and eval_call ctx i lname args call = and eval_case ctx i loc target pat dflt = (* Eval target *) - let v = (get_value_lexp (_eval target ctx (i + 1))) in - - let (_, (osize, _)) = ctx in (* number of variable declared outside *) - let csize = get_rte_size ctx in (* current size *) - let offset = csize - osize in - - (* Get inductive type from a constructor *) - let get_inductive_ref lxp = - match lxp with - | Cons(((_, vname), idx), (_, cname)) ->( - let info = (get_value_lexp - (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 - info, ctor_def) - | _ -> eval_error loc "Target is not a Constructor" in - - (* I think checks should be in lexp not done during eval *) - (* check if a constructor 'cname' exist *) - let check_ctor cname cargs ctor_def = - try let targs = (SMap.find cname ctor_def) in - let n_targs = List.length targs in - let n_cargs = List.length cargs in - - match (n_targs - n_cargs) with - | 0 -> cname, cargs - | _ -> eval_error loc ("Constructor not applied. " ^ - cname ^ " expected " ^ (string_of_int n_targs) ^ " arg(s)." ^ - " Given " ^ (string_of_int n_cargs) ^ " arg(s).") - - with Not_found -> - eval_error loc ("Constructor \"" ^ cname ^ "\" does not exist") in - - (* extract constructor name and check its validity *) - let ctor_name, args = match v with - | Call(Var((_, cname), tp), args) ->( - (* Don't check the constructor this job will be done in lexping *) - cname, args) - - (* get constructor * ) - try let ctor = get_rte_variable None (tp + offset) ctx in - let idt, ctor_def = get_inductive_ref ctor in - check_ctor cname args ctor_def - - (* currently we have a little bug with ctor checking *) - with e -> cname, args) *) - - | Cons(((_, vname), idx), (_, cname)) as ctor -> - let idt, ctor_def = get_inductive_ref ctor in - check_ctor cname [] ctor_def + let v = _eval target ctx (i + 1) in - | _ -> lexp_print target; print_string "\n"; - lexp_print v; print_string "\n"; + (* extract constructor name and arguments *) + let ctor_name, args = match v with + (* | Call(Var((_, cname), tp), args) -> cname, args *) + | Vcons((_, cname), args) -> cname, args + + | _ -> + (* -- Debug print -- *) + lexp_print target; print_string "\n"; + value_print v; print_string "\n"; + (* -- Crash -- *) eval_error loc "Target is not a Constructor" in + let ctor_n = List.length args in + (* Check if a default is present *) let run_default df = match df with - | None -> eval_error loc "Match Failure" - | Some lxp -> _eval lxp ctx (i + 1) in - - let ctor_n = List.length args in + | Some lxp -> _eval lxp ctx (i + 1) + | None -> + (* -- Debug print -- *) + lexp_print target; print_string "\n"; + value_print v; print_string "\n"; + (* -- Crash -- *) + eval_error loc "Match Failure" in (* Build a filter option *) - let is_true key value = - let (_, pat_args, _) = value in - let pat_n = List.length pat_args in - (* FIXME: Shouldn't pat_n != ctor_n cause an error ? *) - 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 + let is_true key (_, pat_args, _) = + (*let pat_n = List.length pat_args in (pat_n = ctor_n) && *) + (ctor_name = key) 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) (Value(xp)) nctx) - - ctx pat_args args in - (* eval body *) - _eval exp nctx (i + 1) + if SMap.is_empty sol then + run_default dflt + else( + (* Get working pattern *) + let key, (_, pat_args, exp) = SMap.min_binding sol in + + (* build context (List.fold2 has problem with some cases) *) + let rec fold2 nctx pats args = + match pats, args with + | (Some (_, (_, name)))::pats, arg::args -> + let nctx = add_rte_variable (Some name) arg nctx in + fold2 nctx pats args + | None::pats, arg::args -> fold2 nctx pats args + (* Errors *) + | _::_, [] -> eval_warning loc "a) Eval::Case Pattern Error"; nctx + | [], _::_ -> eval_warning loc "b) Eval::Case Pattern Error"; nctx + (* Normal case *) + | [], [] -> nctx in + + let nctx = fold2 ctx pat_args args in + _eval exp nctx (i + 1)) and build_arg_list args ctx i = (* _eval every args *) @@ -274,13 +209,13 @@ and build_arg_list args ctx i = (* Add args inside context *) List.fold_left (fun c v -> add_rte_variable None v c) ctx arg_val -and eval_decls decls ctx = _eval_decls decls ctx 1 +and eval_decls decls ctx = _eval_decls decls ctx 0 and _eval_decls (decls: ((vdef * lexp * ltype) list)) (ctx: runtime_env) i: runtime_env = (* Read declarations once and push them *) let ctx = List.fold_left (fun ctx ((_, name), lxp, ltp) -> - add_rte_variable (Some name) (Value(lxp)) ctx) + add_rte_variable (Some name) Vdummy ctx) ctx decls in (* local ctx saves the number of declared variable inside ctx *) @@ -290,7 +225,7 @@ and _eval_decls (decls: ((vdef * lexp * ltype) list)) (* Read declarations once and push them *) let _, ctx = List.fold_left (fun (idx, ctx) ((_, name), lxp, ltp) -> - + _global_eval_trace := []; let lxp = _eval lxp ctx (i + 1) in let ctx = set_rte_variable idx (Some name) lxp ctx in (idx - 1, ctx)) @@ -310,10 +245,12 @@ and print_eval_trace () = ;; let eval lxp ctx = + _global_eval_trace := []; _eval lxp ctx 1 let debug_eval lxp ctx = try + _global_eval_trace := []; eval lxp ctx with e -> ( print_rte_ctx (!_global_eval_ctx); @@ -350,7 +287,9 @@ let from_lctx (ctx: lexp_context): runtime_env = let (_, (_, name), exp, _) = !(Myers.nth j env) in let vxp = match exp with - | Some lxp -> (eval lxp !rctx) + | Some lxp -> (try (eval lxp !rctx) + with e -> lexp_print lxp; raise e) + | None -> Vdummy in rctx := set_rte_variable j (Some name) vxp (!rctx) ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -167,17 +167,17 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = ) formal_args in (* (arg_kind * vdef * ltype) list *) - (* -- Should I do that ?? --*) + (* -- Should I do that ?? --* ) let rec make_type args tp = match args with | (kind, (loc, n), ltp)::tl -> make_type tl (Arrow(kind, Some (loc, n), ltp, loc, tp)) - | [] -> tp in + | [] -> tp in *) let ctx = !ctx in let map_ctor = lexp_parse_inductive ctors ctx i in let v = Inductive(tloc, label, formal, map_ctor) in - v, (make_type formal type0) + v, type0 (* This case can be inferred *) | Plambda (kind, var, optype, body) -> @@ -330,7 +330,96 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = e (* Identify Call Type and return processed call *) -and lexp_call (fname: pexp) (_args: sexp list) ctx i = +and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = + let loc = pexp_location fun_name in + + (* Process Arguments *) + let pargs = List.map pexp_parse sargs in + let largs = _lexp_parse_all pargs ctx i in + let new_args = List.map (fun g -> (Aexplicit, g)) largs in + + (* consume Arrows and args together *) + let rec get_return_type i ltp args = + match ltp, args with + | _, [] -> ltp + | Arrow(_, _, _, _, ltp), hd::tl -> (get_return_type (i + 1) ltp tl) + | _, _ -> lexp_warning loc + ("Function was provided with too many args. Expected: " ^ + (string_of_int i)); ltp in + + (* Vanilla : sqr is inferred and (lambda x -> x * x) is returned + * Macro : sqr is returned + * Constructor : a constructor is returned + * Anonymous : lambda *) + + (* retrieve function's body *) + let body, ltp = _lexp_p_infer fun_name ctx (i + 1) in + let ret_type = get_return_type 0 ltp new_args in + + (* handle named functions*) + let named_call (loc, name) = + try (* Check if the function was defined *) + let idx = senv_lookup name ctx in + let vf = (make_var name idx loc) in + + (* Replace a built-in name by builtin so they can be recognized + * during eval *) + if (is_lbuiltin idx ctx) then ( + match env_lookup_expr ctx ((loc, name), idx) with + | None -> lexp_error loc "Unknown builtin"; + Call(vf, new_args), ret_type + + (* a builtin functions *) + | Some e -> Call(e, new_args), ret_type + ) + else Call(vf, new_args), ret_type + with Not_found -> + lexp_error loc ("The function \"" ^ name ^ "\" was not defined"); + let vf = (make_var name (-1) loc) in + Call(vf, new_args), ltp in + + (* determine function type *) + match fun_name, ltp with + (* Anonymous *) + | ((Plambda _), _) -> Call(body, new_args), ltp + + (* Call to a macro *) + | (Pvar (loc, name), Inductive _) -> + (* look up for definition *) + let idx = senv_lookup name ctx in + let vf = (make_var name idx loc) in + + (* Get the macro *) + let lxp = match env_lookup_expr ctx ((loc, name), idx) with + | None -> lexp_fatal loc "The macro cannot be expanded"; + | Some e -> e in + + print_string "HERE"; + + let rctx = (from_lctx ctx) in + + print_string "HERE"; + + let sxp = match eval lxp rctx with + | Vsexp(sxp) -> sxp + | v -> value_print v; + lexp_fatal loc "Macro_ expects sexp" in + + let pxp = pexp_parse sxp in + (* Generated Code *) + let lxp, ltp = _lexp_p_infer pxp ctx (i + 1) in + Call(lxp, new_args), ltp + + (* Call to Vanilla or constructor *) + | (Pvar v, _) -> named_call v + + (* Constructor. This case is rarely used *) + | (Pcons(_, v), _) -> named_call v + + | e, _ -> lexp_fatal (pexp_location e) "This expression cannot be called" + + + (* (* Process Arguments *) let pargs = List.map pexp_parse _args in let largs = _lexp_parse_all pargs ctx i in @@ -354,6 +443,11 @@ and lexp_call (fname: pexp) (_args: sexp list) ctx i = (* retrieve function body *) let body, ltp = _lexp_p_infer fname ctx (i + 1) in + (* Check if macro *) + let _ = match ltp with + | Inductive (_, (_, "built-in"), [], _) -> lexp_print body; print_string "\n"; + | _ -> () in + try (* Check if the function was defined *) @@ -381,7 +475,8 @@ and lexp_call (fname: pexp) (_args: sexp list) ctx i = (* Is it a macro ? *) | Some Cons (((_, "Macro"), _), (_, "Macro_")) -> - + Call(vf, new_args), type_macro + (* let lxp = match largs with | [lxp] -> lxp | hd::tl -> lexp_error loc "Macro_ expects one lexp"; hd @@ -395,7 +490,7 @@ and lexp_call (fname: pexp) (_args: sexp list) ctx i = | v -> lexp_fatal loc "Macro_ expects sexp" in let pxp = pexp_parse sxp in - _lexp_p_infer pxp ctx (i + 1) + _lexp_p_infer pxp ctx (i + 1) *) (* a builtin functions *) | Some e -> Call(e, new_args), ret_type @@ -406,7 +501,7 @@ and lexp_call (fname: pexp) (_args: sexp list) ctx i = (* 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), ltp end + Call(vf, new_args), ltp end *) (* Read a pattern and create the equivalent representation *) and lexp_read_pattern pattern exp target ctx: ===================================== tests/env_test.ml ===================================== --- a/tests/env_test.ml +++ b/tests/env_test.ml @@ -37,7 +37,7 @@ open Env let rctx = default_rctx () -let make_val value = Imm(String(dloc, value)) +let make_val value = Vstring(value) let _ = (add_test "ENV" "Set Variables" (fun () -> @@ -55,13 +55,13 @@ let _ = (add_test "ENV" "Set Variables" (fun () -> let n = (List.length var) - 1 in let rctx = List.fold_left (fun ctx (n, t, _) -> - add_rte_variable n (Value(t)) ctx) + add_rte_variable n (Vdummy) ctx) rctx var in print_rte_ctx rctx; let rctx, _ = List.fold_left (fun (ctx, idx) (n, _, v) -> - ((set_rte_variable idx n (Value(v)) ctx), idx - 1)) + ((set_rte_variable idx n (Vdummy) ctx), idx - 1)) (rctx, n) var in print_rte_ctx rctx; ===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -37,13 +37,6 @@ open Eval (* reset_eval_trace *) open Builtin open Env -let get_int lxp = - let lxp = get_value_lexp lxp in - match lxp with - | Imm(Integer(_, l)) -> l - | _ -> (-40); -;; - (* default environment *) let lctx = default_lctx () let rctx = default_rctx () @@ -64,7 +57,7 @@ let _ = (add_test "EVAL" "Variable Cascade" (fun () -> let ret = eval_expr_str ecode lctx rctx in match ret with - | [r] -> expect_equal_int (get_int r) 10 + | [Vint(r)] -> expect_equal_int r 10 | _ -> failure ()) );; @@ -86,7 +79,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 (get_int r) 30 + | [Vint(r)] -> expect_equal_int r 30 | _ -> failure ()) ) ;; @@ -109,7 +102,7 @@ let _ = (add_test "EVAL" "Lambda" (fun () -> let ret = eval_expr_str "(sqr 4);" lctx rctx in (* Expect a single result *) match ret with - | [r] -> expect_equal_int (get_int r) (4 * 4) + | [Vint(r)] -> expect_equal_int r (4 * 4) | _ -> failure ()) ) ;; @@ -131,7 +124,7 @@ let _ = (add_test "EVAL" "Nested Lambda" (fun () -> let ret = eval_expr_str "(cube 4);" lctx rctx in (* Expect a single result *) match ret with - | [r] -> expect_equal_int (get_int r) (4 * 4 * 4) + | [Vint(r)] -> expect_equal_int r (4 * 4 * 4) | _ -> failure ()) ) ;; @@ -175,7 +168,7 @@ let _ = (add_test "EVAL" "Inductive::Case" (fun () -> ctr0 = inductive-cons idt ctr0; e = 20; ctr1 = inductive-cons idt ctr1; f = 30; ctr2 = inductive-cons idt ctr2; g = 40; - ctr3 = inductive-cons idt ctr2; h = 50; + ctr3 = inductive-cons idt ctr3; h = 50; a = (ctr1 (ctr2 ctr0)); y = 2; b = (ctr2 (ctr2 ctr0)); z = 3; @@ -194,10 +187,10 @@ let _ = (add_test "EVAL" "Inductive::Case" (fun () -> 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 - let t2 = expect_equal_int (get_int b) 2 in - let t3 = expect_equal_int (get_int c) 3 in + | [Vint(a); Vint(b); Vint(c)] -> + let t1 = expect_equal_int a 1 in + let t2 = expect_equal_int b 2 in + let t3 = expect_equal_int c 3 in if t1 = 0 && t2 = 0 && t3 = 0 then success () else @@ -240,10 +233,10 @@ let _ = (add_test "EVAL" "Inductive::Recursive Call" (fun () -> 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 - let t2 = expect_equal_int (get_int b) 1 in - let t3 = expect_equal_int (get_int c) 2 in + | [Vint(a); Vint(b); Vint(c)] -> + let t1 = expect_equal_int a 0 in + let t2 = expect_equal_int b 1 in + let t3 = expect_equal_int c 2 in if t1 = 0 && t2 = 0 && t3 = 0 then success () else @@ -277,10 +270,10 @@ let _ = (add_test "EVAL" "Inductive::Nat Plus" (fun () -> 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) 2 in - let t3 = expect_equal_int (get_int c) 3 in + | [Vint(a); Vint(b); Vint(c)] -> + let t1 = expect_equal_int a 2 in + let t2 = expect_equal_int b 2 in + let t3 = expect_equal_int c 3 in if t1 = 0 && t2 = 0 && t3 = 0 then success () else @@ -314,11 +307,11 @@ let _ = (add_test "EVAL" "Mutually Recursive Definition" (fun () -> 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) 0 in - let t4 = expect_equal_int (get_int d) 1 in + | [Vint(a); Vint(b); Vint(c); Vint(d)] -> + let t1 = expect_equal_int a 1 in + let t2 = expect_equal_int b 0 in + let t3 = expect_equal_int c 0 in + let t4 = expect_equal_int d 1 in if t1 = 0 && t2 = 0 && t3 = 0 && t4 = 0 then success () else @@ -345,10 +338,10 @@ let _ = (add_test "EVAL" "Partial Application" (fun () -> 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) 3 in - let t3 = expect_equal_int (get_int c) 4 in + | [Vint(a); Vint(b); Vint(c)] -> + let t1 = expect_equal_int a 2 in + let t2 = expect_equal_int b 3 in + let t3 = expect_equal_int c 4 in if t1 = 0 && t2 = 0 && t3 = 0 then success () else @@ -364,29 +357,26 @@ List = inductive_ (dList (a : Type)) (nil) (cons a (List a)); nil = inductive-cons List nil; cons = inductive-cons List cons; -% length : (a : Type) => List a -> Int; -% length = lambda a => -length : List a -> Int; -length = lambda (xs : List a) -> +length : (a : Type) => List a -> Int; +length = lambda a => + lambda xs -> case xs - | nil => 0 - | cons hd tl => (1 + length tl); + | nil => 0 + | cons hd tl => (1 + length a tl); -% head : (a : Type) => List a -> a; -% head = lambda a => -head : List a -> a; -head = lambda (xs : List a) -> +head : (a : Type) => List a -> a; +head = lambda a => + lambda xs -> case xs - | nil => nil - | cons hd tl => hd; + | nil => nil + | cons hd tl => hd; -% tail : (a : Type) => List a -> List a; -% tail = lambda a => -tail : List a -> List a; -tail = lambda (xs : List a) -> +tail : (a : Type) => List a -> List a; +tail = lambda a => + lambda xs -> case xs - | nil => nil - | cons hd tl => tl; + | nil => nil + | cons hd tl => tl; ";; let _ = (add_test "EVAL" "List" (fun () -> @@ -398,18 +388,18 @@ let _ = (add_test "EVAL" "List" (fun () -> let rctx, lctx = eval_decl_str dcode lctx rctx in - let rcode = "(length my_list); - (head my_list); - (head (tail my_list));" in + let rcode = "(length Int my_list); + (head Int my_list); + (head Int (tail Int my_list));" 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) 4 in - let t2 = expect_equal_int (get_int b) 1 in - let t3 = expect_equal_int (get_int c) 2 in + | [Vint(a); Vint(b); Vint(c)] -> + let t1 = expect_equal_int a 4 in + let t2 = expect_equal_int b 1 in + let t3 = expect_equal_int c 2 in if t1 = 0 && t2 = 0 && t3 = 0 then success () else ===================================== tests/macro_test.ml ===================================== --- a/tests/macro_test.ml +++ b/tests/macro_test.ml @@ -37,12 +37,6 @@ open Eval (* reset_eval_trace *) open Builtin open Env -let get_int lxp = - let lxp = get_value_lexp lxp in - match lxp with - | Imm(Integer(_, l)) -> l - | _ -> (-40); -;; (* default environment *) let lctx = default_lctx () @@ -72,7 +66,7 @@ let _ = (add_test "MACROS" "macros base" (fun () -> let ret = eval_expr_str ecode lctx rctx in match ret with - | [r] -> expect_equal_int (get_int r) (3 * 3) + | [Vint(r)] -> expect_equal_int r (3 * 3) | _ -> failure ()) );; View it on GitLab: https://gitlab.com/monnier/typer/commit/4af18f1cbb92d24a892b50fc7649f3346b1…

1 0

Macros
by Pierre Delaunay 28 Avr '16

28 Avr '16

Bonjour, je viens de modifier comment les macros sont gérés. J'ai une question sur le comportement attendu des macros. Voici l'exemple que j'utilise: sqr_fun = node_ (symbol_ "lambda_->_") (symbol_ "x") (node_ (symbol_ "_*_") (symbol_ "x") (symbol_ "x")); sqr_type = node_ (symbol_ "_->_") (symbol_ "Int") (symbol_ "Int"); give_type : Sexp -> Sexp -> Sexp; give_type = lambda expr -> lambda tp -> node_ (symbol_ "_:_") expr tp; sqr = Macro_ (give_type sqr_fun sqr_type); main = (sqr 2); Est-ce que l'on s’attend à sqr = (lambda x -> x * x) : Int -> Int ou sqr = Macro_ (give_type sqr_fun sqr_type); main = (((lambda x -> x * x) : Int -> Int) 2) Pour l'instant (commit 6967d92) fait le premier cas. Mais je pense que le second est le comportement attendu. Pour lexp_decls, j'ai un problème parce que pour certain cas nous avons besoin d'avoir le Type et l'expression ensemble (pour lexp_p_check) mais nous avons aussi besoin d'avoir le Type tout seul (pour les définitions récursives). -- Pierre Delaunay

2 1

[Git][monnier/typer][master] 2 commits: fix little things
by Setepenre 28 Avr '16

28 Avr '16

Setepenre pushed to branch master at Stefan / Typer Commits: 5521e11a by Pierre Delaunay at 2016-04-27T11:02:03-04:00 fix little things Changes to be committed: * GNUmakefile: compile to bytecote to avoid recompilation * src/pexp.ml: fix formal arg parsing * tests/sexp_test.ml: fix sexp_test - - - - - 6967d92c by Pierre Delaunay at 2016-04-28T09:51:02-04:00 fix lexp_decls and Macro Changes to be committed: * README.md: minor updates * src/lparse.ml: - add an error message when lambda does not habe type info - fix lexp.Arrow, its variable was not added to the environement * src/builtin.ml * btl/macro.typer: - added some ideas on how to define type built-in * src/lexp.ml: - fix lexp_print Inductive's formal args - - - - - 15 changed files: - GNUmakefile - README.md - samples/BTL.typer → btl/list.typer - + btl/macro.typer - + samples/macro.typer - src/builtin.ml - src/debruijn.ml - src/env.ml - src/eval.ml - src/lexp.ml - src/lparse.ml - src/pexp.ml - src/subst.ml - tests/macro_test.ml - tests/sexp_test.ml Changes: ===================================== GNUmakefile ===================================== --- a/GNUmakefile +++ b/GNUmakefile @@ -5,18 +5,19 @@ CPL_FILES := $(wildcard ./_build/src/*.cmo) TEST_FILES := $(wildcard ./tests/*_test.ml) OBFLAGS = -build-dir _build -COMPILE_MODE = native +# COMPILE_MODE = native all: ityper typer debug tests-build ifeq ($(OS), Windows_NT) # Windows need '-r' and building to native can be problematic (linking error) # So we build to byte instead - OBFLAGS = $(OBFLAGS) -r +endif + COMPILE_MODE = byte -endif + typer: ===================================== README.md ===================================== --- a/README.md +++ b/README.md @@ -12,19 +12,19 @@ Typer By default ocamlbuild creates a '_build' folder which holds all the compiled files. -* make typer: build typer interpreter 'typer' -* make debug: build typer with debug info 'debug' -* make tests: run interpreter's tests '/.tests/utest_main.byte' +* `make typer`: build typer interpreter './typer' +* `make debug`: build typer with debug info './debug_util' +* `make tests`: run interpreter's tests './tests/utests' # Directory layout -* src/ interpreter's source -* doc/ interpreter's doc files -* sample/ typer code sample for testing purposes -* tests/ ocaml test files - +* `src/` interpreter's source +* `doc/` interpreter's doc files +* `sample/` typer code sample for testing purposes +* `tests/` ocaml test files +* `btl/` builtin typer library + # Emacs files /typer-mode.el - - \ No newline at end of file + ===================================== samples/BTL.typer → btl/list.typer ===================================== --- a/samples/BTL.typer +++ b/btl/list.typer @@ -6,26 +6,23 @@ List = inductive_ (dList (a : Type)) (nil) (cons a (List a)); nil = inductive-cons List nil; cons = inductive-cons List cons; -% length : (a : Type) => List a -> Int; -% length = lambda a => -length : List a -> Int; -length = lambda (xs : List a) -> +length : (a : Type) => List a -> Int; +length = lambda a => + lambda xs -> case xs - | nil => 0 - | cons hd tl => (1 + length tl); + | nil => 0 + | cons hd tl => (1 + length tl); -% head : (a : Type) => List a -> a; -% head = lambda a => -head : List a -> a; -head = lambda (xs : List a) -> +head : (a : Type) => List a -> a; +head = lambda a => + lambda xs -> case xs - | nil => nil - | cons hd tl => hd; + | nil => nil + | cons hd tl => hd; -% tail : (a : Type) => List a -> List a; -% tail = lambda a => -tail : List a -> List a; -tail = lambda (xs : List a) -> +tail : (a : Type) => List a -> List a; +tail = lambda a => + lambda xs -> case xs - | nil => nil - | cons hd tl => tl; \ No newline at end of file + | nil => nil + | cons hd tl => tl; \ No newline at end of file ===================================== btl/macro.typer ===================================== --- /dev/null +++ b/btl/macro.typer @@ -0,0 +1,24 @@ + +% define Sexp constructor +Sexp : Type; +Sexp = inductive_ (built-in) (block_ Sexp) + (symbol_ string) (string_ string) (integer_ Int) (float_ Float) + (node_ Sexp List Sexp); + +Macro : Type; +Macro = inductive_ (built-in) (Macro_ sexp); + +%% Basic usage +% +% sqr = (Macro_ +% (node_ (symbol_ "lambda_->_") (symbol "x") +% (node_ "_*_" (symbol "x") (symbol "x")))); +% +% (sqr 4); % <=> 4 * 4 +% +% +%% Using Quasi Quote ` +% +% sqr = (Macro_ (qq (lambda x -> ,x * ,x))); +% +% (sqr 4); % <=> 4 * 4 ===================================== samples/macro.typer ===================================== --- /dev/null +++ b/samples/macro.typer @@ -0,0 +1,14 @@ + +sqr_fun = node_ (symbol_ "lambda_->_") (symbol_ "x") + (node_ (symbol_ "_*_") (symbol_ "x") (symbol_ "x")); + +sqr_type = node_ (symbol_ "_->_") (symbol_ "Int") (symbol_ "Int"); + +give_type : Sexp -> Sexp -> Sexp; +give_type = lambda expr -> + lambda tp -> + node_ (symbol_ "_:_") expr tp; + +sqr = Macro_ (give_type sqr_fun sqr_type); + +main = (sqr 2); \ No newline at end of file ===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -56,9 +56,9 @@ let type_omega = Sort (dloc, StypeOmega) let type_level = Sort (dloc, StypeLevel) let type_level = Builtin (LevelType, "TypeLevel", type_level) - -let type_int = Builtin (IntType, "Int", type0) +let type_int = Builtin (IntType, "Int", type0) let type_float = Builtin (FloatType, "Float", type0) +let type_sexp = Builtin (SexpType, "sexp", type0) let op_binary t = Arrow (Aexplicit, None, t, dloc, Arrow (Aexplicit, None, t, dloc, t)) @@ -77,7 +77,7 @@ let type_eq = let lv = (dloc, "l") in let builtin_iadd = Builtin (IAdd, "_+_", iop_binary) let builtin_imult = Builtin (IMult, "_*_", iop_binary) let builtin_eq = Builtin (EqType, "_=_", type_eq) -let builtin_sexp = Builtin (SexpType, "sexp", type0) + (* let builtin_fadd = Builtin (FAdd, "_+_", fop_binary) let builtin_fmult = Builtin (FMult, "_*_", fop_binary) *) @@ -178,12 +178,12 @@ let make_float loc args_val ctx = Value(type0) let type_string = type0 let type_mblock = type0 -let type_msymbol = Arrow (Aexplicit, None, type_string, dloc, builtin_sexp) -let type_mstring = Arrow (Aexplicit, None, type_string, dloc, builtin_sexp) -let type_minteger = Arrow (Aexplicit, None, type_int, dloc, builtin_sexp) -let type_mfloat = Arrow (Aexplicit, None, type_float, dloc, builtin_sexp) -let type_mnode = Arrow (Aexplicit, None, builtin_sexp,dloc, builtin_sexp) -let type_mexpand = Arrow (Aexplicit, None, builtin_sexp,dloc, type0) +let type_msymbol = Arrow (Aexplicit, None, type_string, dloc, type_sexp) +let type_mstring = Arrow (Aexplicit, None, type_string, dloc, type_sexp) +let type_minteger = Arrow (Aexplicit, None, type_int , dloc, type_sexp) +let type_mfloat = Arrow (Aexplicit, None, type_float , dloc, type_sexp) +let type_mnode = Arrow (Aexplicit, None, type_sexp , dloc, type_sexp) +let type_mexpand = Arrow (Aexplicit, None, type_sexp , dloc, type0) let builtin_block = Builtin (SexpType, "block_", type_mblock) let builtin_symbol = Builtin (SexpType, "symbol_", type_msymbol) @@ -191,8 +191,15 @@ let builtin_string = Builtin (SexpType, "string_", type_mstring) let builtin_integer = Builtin (SexpType, "integer_", type_minteger) let builtin_float = Builtin (SexpType, "float_", type_mfloat) let builtin_node = Builtin (SexpType, "node_", type_mnode) -let builtin_expand = Builtin (SexpType, "expand_", type_mexpand) +(* let builtin_expand = Builtin (SexpType, "expand_", type_mexpand) *) +let type_macro = + let ctors = SMap.empty in + let ctors = SMap.add "Macro_" [(Aexplicit, None, type_sexp)] ctors in + Inductive (dloc, (dloc, "built-in"), [], ctors) + +let builtin_macro = Cons (((dloc, "Macro"), (-4)), (dloc, "Macro_")) +let macro_cons = Arrow (Aexplicit, None, type_sexp , dloc, type_macro) (* * Should we have a function that * -> returns a new context inside typer ? (So we need to add a ctx type too) @@ -210,12 +217,14 @@ let typer_builtins = [ ("Int" , type_int , type0, none_fun); ("Float" , type_float , type0, none_fun); ("String", type_string, type0, none_fun); + ("Sexp" , type_sexp , type0, none_fun); + ("Macro" , type_macro , type0, none_fun); (* Built-in Functions *) - ("_=_" , builtin_eq, type_eq, none_fun); (* t -> t -> bool *) - ("_+_" , builtin_iadd, iop_binary, iadd_impl); (* int -> int -> int *) - ("_*_" , builtin_imult, iop_binary, imult_impl); (* int -> int -> int *) - + ("_=_" , builtin_eq, type_eq, none_fun); (* t -> t -> bool *) + ("_+_" , builtin_iadd, iop_binary, iadd_impl); (* int -> int -> int *) + ("_*_" , builtin_imult, iop_binary, imult_impl); (* int -> int -> int *) + ("Macro_", builtin_macro, macro_cons, none_fun); (* Macro primitives *) ("block_" , builtin_block , type_mblock , make_block); ("symbol_" , builtin_symbol , type_msymbol , make_symbol); @@ -223,7 +232,7 @@ let typer_builtins = [ ("integer_", builtin_integer, type_minteger, make_integer); ("float_" , builtin_float , type_mfloat , make_float); ("node_" , builtin_node , type_mnode , make_node); - ("expand_" , builtin_expand , type_mexpand , none_fun); + (* ("expand_" , builtin_expand , type_mexpand , none_fun); *) (* Macros primitives type ? *) ===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -119,7 +119,7 @@ let senv_add_var (loc, name) ctx = let env_add_var_info var (ctx: lexp_context) = let (a, env, f) = ctx in - (a, cons (ref var) env, f) + (a, cons (ref var) env, f) let env_extend (ctx: lexp_context) (def: vdef) (v: lexp option) (t: lexp) = let ((n, map), e, f) = ctx in ===================================== src/env.ml ===================================== --- a/src/env.ml +++ b/src/env.ml @@ -134,7 +134,7 @@ let set_rte_variable idx name (lxp: value_type) ctx = match (n, name) with | Some n1, Some n2 -> if (n1 != n2) then - env_error dloc ("Variable Name must Match:" ^ n1 ^ " " ^ n2) + env_error dloc ("Variable's Name must Match: " ^ n1 ^ " vs " ^ n2) else( ref_cell := (name, lxp); ctx) ===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -90,6 +90,9 @@ let rec _eval lxp ctx i: (value_type) = let nctx = _eval_decls decls ctx i in _eval inst nctx (i + 1) + (* I don't really know why Built-in is ever evaluated... but it is sometimes *) + | Builtin _ -> Vdummy + (* Built-in Function *) | Call(Builtin(btype, str, ltp), args)-> (* built-in does not have location info. So we extract it from args *) @@ -105,13 +108,14 @@ let rec _eval lxp ctx i: (value_type) = (* Case *) | Case (loc, target, _, pat, dflt) -> (eval_case ctx i loc target pat dflt) + | _ -> print_string "debug catch-all eval: "; lexp_print lxp; Value(Imm(String(dloc, "eval Not Implemented"))) and eval_var ctx lxp v = let ((loc, name), idx) = v in try get_rte_variable (Some name) (idx) ctx - with Not_found -> + with e -> eval_error loc ("Variable: " ^ name ^ (str_idx idx) ^ " was not found ") and eval_call ctx i lname args call = @@ -146,8 +150,9 @@ and eval_call ctx i lname args call = (* No more arguments *) | Closure (_, _), [] -> body - | Value (lxp), [] -> body - | _ -> eval_error dloc "Cannot eval function" in + | _, [] -> body + | _ -> value_print body; + eval_error dloc "Cannot eval function" in eval_call body args_val clean_ctx @@ -331,16 +336,25 @@ let from_lctx (ctx: lexp_context): runtime_env = let bsize = List.length typer_builtins in let csize = get_size ctx in + (* add all variables *) for i = bsize to csize do - let (_, (_, name), exp, _) = !(Myers.nth (csize - i) env) in + let (_, (_, name), _, _) = !(Myers.nth (csize - i) env) in + rctx := add_rte_variable (Some name) Vdummy (!rctx) + done; + + let diff = csize - bsize in + + (* process all of them *) + for i = 0 to diff do + let j = diff - i (* - 1 *) in + let (_, (_, name), exp, _) = !(Myers.nth j env) in let vxp = match exp with | Some lxp -> (eval lxp !rctx) | None -> Vdummy in - rctx := add_rte_variable (Some name) vxp (!rctx) + rctx := set_rte_variable j (Some name) vxp (!rctx) done; - !rctx ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -54,6 +54,7 @@ type builtin = | IMult | EqType | LevelType + | MacroType (* Pour la propagation des types bidirectionnelle, tout va dans `infer`, * sauf Lambda et Case qui vont dans `check`. Je crois. *) @@ -583,6 +584,10 @@ and _lexp_to_str ctx exp = match k with | Aexplicit -> "->" | Aimplicit -> "=>" | Aerasable -> "≡>" in + let kindp_str k = + match k with + | Aexplicit -> ":" | Aimplicit -> "::" | Aerasable -> ":::" in + match exp with | Imm(value) -> (match value with | String (_, s) -> tval ("\"" ^ s ^ "\"") @@ -640,8 +645,17 @@ and _lexp_to_str ctx exp = "(" ^ (fun_call (lexp_to_str fname)) ^ args ^ ")") - | Inductive (_, (_, name), _, ctors) -> - (keyword "inductive_") ^ " (" ^ name ^ ") " ^ (lexp_str_ctor ctx ctors) + | Inductive (_, (_, name), [], ctors) -> + (keyword "inductive_") ^ " (" ^ name ^") " ^ + (lexp_str_ctor ctx ctors) + + | Inductive (_, (_, name), args, ctors) -> + let args_str = List.fold_left (fun str (arg_kind, (_, name), ltype) -> + str ^ " (" ^ name ^ " " ^ (kindp_str arg_kind) ^ " " ^ (lexp_to_str ltype) ^ ")") + "" args in + + (keyword "inductive_") ^ " (" ^ name ^ args_str ^") " ^ + (lexp_str_ctor ctx ctors) | Case (_, target, tpe, map, dflt) ->( let str = (keyword "case ") ^ (lexp_to_str target) ^ @@ -665,8 +679,10 @@ and _lexp_to_str ctx exp = | Builtin (_, name, _) -> name - | Sort (_, _) -> "Sort" - | SortLevel _ -> "SortLevel" + | Sort (_, Stype lvl) -> (match lvl with + | SortLevel (SLn 0) -> "Type" + | SortLevel (SLn v) -> "Type" ^ (string_of_int v) + | _ -> "Type") | _ -> print_string "Printing Not Implemented"; "" ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -143,16 +143,14 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = Let(tloc, decl, bdy), ltp (* ------------------------------------------------------------------ *) - | Parrow (kind, Some var, tp, loc, expr) -> - let ltyp, _ = lexp_infer tp ctx in - let lxp, _ = lexp_infer expr ctx in - let v = Arrow(kind, Some var, ltyp, tloc, lxp) in - v, type0 + | Parrow (kind, ovar, tp, loc, expr) -> + let ltp, _ = lexp_infer tp ctx in + let ctx = match ovar with + | None -> ctx + | Some var -> env_extend ctx var None ltp in - | Parrow (kind, None, tp, loc, expr) -> - let ltyp, _ = lexp_infer tp ctx in let lxp, _ = lexp_infer expr ctx in - let v = Arrow(kind, None, ltyp, tloc, lxp) in + let v = Arrow(kind, ovar, ltp, tloc, lxp) in v, type0 (* Pinductive *) @@ -169,14 +167,25 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = ) formal_args in (* (arg_kind * vdef * ltype) list *) + (* -- Should I do that ?? --*) + let rec make_type args tp = + match args with + | (kind, (loc, n), ltp)::tl -> + make_type tl (Arrow(kind, Some (loc, n), ltp, loc, tp)) + | [] -> tp in + let ctx = !ctx in let map_ctor = lexp_parse_inductive ctors ctx i in let v = Inductive(tloc, label, formal, map_ctor) in - v, type0 + v, (make_type formal type0) (* This case can be inferred *) - | Plambda (kind, var, Some ptype, body) -> - let ltp, _ = lexp_infer ptype ctx in + | Plambda (kind, var, optype, body) -> + let ltp, _ = match optype with + | Some ptype -> lexp_infer ptype ctx + (* This case must have been lexp_p_check *) + | None -> lexp_error tloc "Lambda require type annotation"; + dltype, dltype in let nctx = env_extend ctx var None ltp in let lbody, lbtp = lexp_infer body nctx in @@ -267,6 +276,7 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = | hd::tl, Some _ -> hd | hd::tl, None -> hd | _, Some v -> v + (* This will change *) | _, None -> lexp_error loc "case with no branch ?"; dltype in Case(loc, tlxp, tltp, lpattern, dflt), (return_type) @@ -289,7 +299,7 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = | Plambda (kind, var, None, body) -> (* Read var type from the provided type *) let ltp, lbtp = match t with - | Arrow(kind, None, ltp, _, lbtp) -> ltp, lbtp + | Arrow(kind, _, ltp, _, lbtp) -> ltp, lbtp | _ -> lexp_error tloc "Type does not match"; dltype, dltype in let nctx = env_extend ctx var None ltp in @@ -297,6 +307,7 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = Lambda(kind, var, ltp, lbody) + (* | Pcall (Pvar(_, "expand_"), _args) ->( let pargs = List.map pexp_parse _args in let largs = _lexp_parse_all pargs ctx i in @@ -312,7 +323,7 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = | _ -> lexp_fatal tloc "expand_ expects sexp" in let pxp = pexp_parse sxp in - _lexp_p_check pxp t ctx (i + 1)) + _lexp_p_check pxp t ctx (i + 1)) *) | _ -> let (e, inferred_t) = _lexp_p_infer p ctx (i + 1) in (* FIXME: check that inferred_t = t! *) @@ -350,16 +361,18 @@ and lexp_call (fname: pexp) (_args: sexp list) ctx i = let vf = (make_var name idx loc) in (* consume Arrows and args together *) - let rec get_return_type ltp args = + let rec get_return_type i ltp args = match ltp, args with | _, [] -> ltp - | Arrow(_, _, _, _, ltp), hd::tl -> (get_return_type ltp tl) - | _, _ -> lexp_warning loc "Too many args"; ltp in + | Arrow(_, _, _, _, ltp), hd::tl -> (get_return_type (i + 1) ltp tl) + | _, _ -> lexp_warning loc ("\""^ name ^ + "\" was provided with too many args. Expected: " ^ + (string_of_int i)); ltp in - let ret_type = get_return_type ltp new_args in + let ret_type = get_return_type 0 ltp new_args in (* Is the function built-in ? *) - (* built-in cannot be partially applied that us why we can get_return_type *) + (* built-in cannot be partially applied that is why we can get_return_type *) (* they can only if you redefine the operation *) if (is_lbuiltin idx ctx) then ( match env_lookup_expr ctx ((loc, name), idx) with @@ -367,9 +380,22 @@ and lexp_call (fname: pexp) (_args: sexp list) ctx i = Call(vf, new_args), ret_type (* Is it a macro ? *) - | Some Builtin (_, "expand_", _) -> - lexp_error loc "expand_ require type annotation"; - dltype, dltype + | Some Cons (((_, "Macro"), _), (_, "Macro_")) -> + + let lxp = match largs with + | [lxp] -> lxp + | hd::tl -> lexp_error loc "Macro_ expects one lexp"; hd + | _ -> lexp_fatal loc "Macro_ expects one lexp" in + + let rctx = (from_lctx ctx) in + + (* eval argument *) + let sxp = match eval lxp rctx with + | Vsexp(sxp) -> sxp + | v -> lexp_fatal loc "Macro_ expects sexp" in + + let pxp = pexp_parse sxp in + _lexp_p_infer pxp ctx (i + 1) (* a builtin functions *) | Some e -> Call(e, new_args), ret_type @@ -466,64 +492,9 @@ and lexp_parse_inductive ctors ctx i = SMap.empty ctors (* Parse let declaration *) -and lexp_p_decls decls ctx = _lexp_decls decls ctx 1 +and lexp_p_decls decls ctx = _lexp_decls decls ctx 0 and _lexp_decls decls ctx i: (((vdef * lexp * ltype) list) * lexp_context) = - (* (pvar * pexp * bool) list * ) - - let ctx = ref ctx in - let mdecls = ref SMap.empty in - let order = ref [] in - let found = ref false in - - List.iter (fun ((loc, name), pxp, bl) -> - (* Check if variable was already defined *) - let (l, olxp, oltp, _) = try found := true; SMap.find name !mdecls - with Not_found -> - (* keep track of declaration order *) - order := (name::!order); - found := false; - (* create an empty element *) - (loc, None, None, 0) in - - (* create a dummy env for lexp_parse *) - let denv = env_extend (!ctx) (loc, name) None dltype in - - (* Do we already have a type ? *) - let lxp, ltp = match oltp with - (* We infer *) - | None -> _lexp_p_infer pxp denv (i + 1) - - (* We check *) - | Some ltp -> (_lexp_p_check pxp ltp denv (i + 1)), ltp in - - (* update declaration *) - (* FIXME: modify env when lxp is found *) - let new_decl = match bl with - | true -> (if !found then () else ctx := env_extend (!ctx) (loc, name) None lxp); - (l, olxp, Some lxp, i) - | false -> (if !found then () else ctx := env_extend (!ctx) (loc, name) (Some lxp) ltp); - (l, Some lxp, oltp, i) in - - (* Add Variable to the map *) - mdecls := SMap.add name new_decl !mdecls) - - decls; - - let ctx = !ctx in - let mdecls = !mdecls in - let order = !order in - (* Cast Map to list *) - let ndecls = List.map (fun name -> - let (l, inst, tp, _) = SMap.find name mdecls in - match inst, tp with - | Some lxp, Some ltp -> ((l, name), lxp, ltp) - | Some lxp, None -> ((l, name), lxp, dltype) - | None, Some ltp -> lexp_warning l "Type with no expression"; - ((l, name), dltype, ltp) - | None, None -> lexp_warning l "No expression, No Type"; - ((l, name), dltype, dltype)) order in - - (List.rev ndecls), ctx *) + (* (pvar * pexp * bool) list *) let ctx = ref ctx in let idx = ref 0 in ===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -187,21 +187,13 @@ and pexp_p_actual_arg arg : (arg_kind * pvar option * pexp) = | e -> (Aexplicit, None, pexp_parse e) and pexp_p_formal_arg arg : (arg_kind * pvar * pexp option) = - (* FYI: None of the formal arg type work *) - (* (a ::: Type) -> (a ::: Type) instead of (::: a Type) - * (a :: Type) -> (a :: Type) instead of (:: a Type) - * (a : Type) -> (_:_ a Type) instead of (_:_ a Type) *) match arg with - | Node (Symbol (_, ":::"), [Symbol s; e]) + | Node (Symbol (_, "_:::_"), [Symbol s; e]) -> (Aerasable, s, Some (pexp_parse e)) - | Node (Symbol (_, "::"), [Symbol s; e]) + | Node (Symbol (_, "_::_"), [Symbol s; e]) -> (Aimplicit, s, Some (pexp_parse e)) - | Node (Symbol (_, ":"), [Symbol s; e]) - -> (Aexplicit, s, Some (pexp_parse e)) - (* ------ FIXME: temp FIX ------ *) | Node (Symbol (_, "_:_"), [Symbol s; e]) -> (Aexplicit, s, Some (pexp_parse e)) - (* ------ --------------- ------ *) | Symbol s -> (Aexplicit, s, None) | _ -> sexp_print arg; (pexp_error (sexp_location arg) "Unrecognized formal arg"); ===================================== src/subst.ml ===================================== --- a/src/subst.ml +++ b/src/subst.ml @@ -206,6 +206,7 @@ type 'a subst = (* lexp subst *) * context Δₛ₁ΔₜΔₛ₂ where Δₛ₂ has size N and Δₜ has size M. *) | Identity | Cons of 'a * 'a subst + (* we enter a let/lambda/case/inductive (with formal args) *) | Shift of 'a subst * db_offset (* | Lift of db_index * db_offset *) ===================================== tests/macro_test.ml ===================================== --- a/tests/macro_test.ml +++ b/tests/macro_test.ml @@ -54,11 +54,16 @@ let _ = (add_test "MACROS" "macros base" (fun () -> (* define 'lambda x -> x * x' using macros *) let dcode = " - sqr_sexp = (node_ (symbol_ \"lambda_->_\") (symbol_ \"x\") - (node_ (symbol_ \"_*_\") (symbol_ \"x\") (symbol_ \"x\"))); + sqr_fun = node_ (symbol_ \"lambda_->_\") (symbol_ \"x\") + (node_ (symbol_ \"_*_\") (symbol_ \"x\") (symbol_ \"x\")); - sqr : Int -> Int; - sqr = (expand_ sqr_sexp);" in + sqr_type = node_ (symbol_ \"_->_\") (symbol_ \"Int\") (symbol_ \"Int\"); + + has_type = lambda (expr : Sexp) -> + lambda (tp : Sexp) -> + node_ (symbol_ \"_:_\") expr tp; + + sqr = Macro_ (has_type sqr_fun sqr_type);" in let rctx, lctx = eval_decl_str dcode lctx rctx in ===================================== tests/sexp_test.ml ===================================== --- a/tests/sexp_test.ml +++ b/tests/sexp_test.ml @@ -2,36 +2,19 @@ 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 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 () + let ret = sexp_parse_str dcode in + match ret with + | [Node(lbd, [x; add])] -> (match lbd, x, add with + | (Symbol(_, "lambda_->_"), Symbol(_, "x"), + Node(Symbol(_, "_+_"), [Symbol(_, "x"); Symbol(_, "x")])) -> success () + | _ -> 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 View it on GitLab: https://gitlab.com/monnier/typer/compare/731e1482be1e361602378f998525042566…

1 0

[Git][monnier/typer][master] * src/grammar.ml (default_grammar): Sync with typer-mode.el
by Stefan 26 Avr '16

26 Avr '16

Stefan pushed to branch master at Stefan / Typer Commits: 731e1482 by Stefan Monnier at 2016-04-26T21:58:46-04:00 * src/grammar.ml (default_grammar): Sync with typer-mode.el - - - - - 1 changed file: - src/grammar.ml Changes: ===================================== src/grammar.ml ===================================== --- a/src/grammar.ml +++ b/src/grammar.ml @@ -58,37 +58,37 @@ let default_stt = let default_grammar : grammar = List.fold_left (fun g (n, ll, rl) -> SMap.add n (ll, rl) g) SMap.empty - [("^", Some 171, Some 159); - ("/", Some 148, Some 160); - ("-", Some 92, Some 110); - ("+", Some 93, Some 111); - ("!=", Some 94, Some 75); - (">=", Some 95, Some 76); - ("<=", Some 96, Some 77); - (">", Some 97, Some 78); - ("<", Some 98, Some 79); - ("&&", Some 64, Some 81); - ("||", Some 39, Some 51); - (",", Some 26, Some 26); - ("then", Some 1, Some 0); - ("=", Some 99, Some 80); - ("type", None, Some 27); - (";", Some 15, Some 15); - ("*", Some 137, Some 137); - (":", Some 173, Some 115); - ("]", Some 3, None); - ("->", Some 126, Some 114); - ("=>", Some 126, Some 113); - ("=>", Some 126, Some 112); - ("in", Some 2, Some 53); - ("else", Some 0, Some 52); - ("|", Some 40, Some 40); - (")", Some 4, None); - ("[", None, Some 3); - ("case", None, Some 28); - ("lambda", None, Some 126); - ("letrec", None, Some 2); - ("let", None, Some 2); - ("if", None, Some 1); - ("(", None, Some 4); + [("^", Some 165, Some 152); + ("/", Some 140, Some 153); + ("*", Some 141, Some 154); + ("-", Some 109, Some 128); + ("+", Some 110, Some 129); + ("!=", Some 111, Some 89); + (">=", Some 112, Some 90); + ("<=", Some 113, Some 91); + (">", Some 114, Some 92); + ("<", Some 115, Some 93); + ("==", Some 116, Some 94); + ("&&", Some 77, Some 95); + ("||", Some 53, Some 65); + (",", Some 41, Some 41); + (":≡", Some 166, Some 0); + (":-", Some 167, Some 1); + (":=", Some 168, Some 2); + ("::", Some 169, Some 17); + (":::", Some 170, Some 16); + (";", Some 15, Some 15); + ("type", None, Some 30); + ("=", Some 28, Some 29); + ("in", Some 4, Some 66); + ("|", Some 54, Some 54); + (")", Some 3, None); + ("->", Some 117, Some 98); + ("=>", Some 117, Some 97); + ("≡>", Some 117, Some 96); + ("let", None, Some 4); + (":", Some 78, Some 78); + ("lambda", None, Some 117); + ("case", None, Some 42); + ("(", None, Some 3) ] View it on GitLab: https://gitlab.com/monnier/typer/commit/731e1482be1e361602378f9985250425663…

1 0

[Git][monnier/typer][master] -
by Setepenre 21 Avr '16

21 Avr '16

Setepenre pushed to branch master at Stefan / Typer Commits: 29bde6e0 by Pierre Delaunay at 2016-04-21T17:36:03-04:00 - Changes to be committed: * new file: samples/BTL.typer (list implementation) * new file: samples/autodiff.typer simple symbolic diff example * src/lparse.ml: - improved lexp_decls (lexp_decls now lexp_p_check when it can) - handle Phas_type - lexp_p_check: handle Plambda - moved macro handling to lexp_p_check * tests/eval_test.ml: - added list test - added necessary type annotations - - - - - 9 changed files: - + samples/BTL.typer - + samples/autodiff.typer - src/builtin.ml - src/eval.ml - src/lparse.ml - src/pexp.ml - src/typecheck.ml - tests/eval_test.ml - tests/macro_test.ml Changes: ===================================== samples/BTL.typer ===================================== --- /dev/null +++ b/samples/BTL.typer @@ -0,0 +1,31 @@ + + +List : Type; +List = inductive_ (dList (a : Type)) (nil) (cons a (List a)); + +nil = inductive-cons List nil; +cons = inductive-cons List cons; + +% length : (a : Type) => List a -> Int; +% length = lambda a => +length : List a -> Int; +length = lambda (xs : List a) -> + case xs + | nil => 0 + | cons hd tl => (1 + length tl); + +% head : (a : Type) => List a -> a; +% head = lambda a => +head : List a -> a; +head = lambda (xs : List a) -> + case xs + | nil => nil + | cons hd tl => hd; + +% tail : (a : Type) => List a -> List a; +% tail = lambda a => +tail : List a -> List a; +tail = lambda (xs : List a) -> + case xs + | nil => nil + | cons hd tl => tl; \ No newline at end of file ===================================== samples/autodiff.typer ===================================== --- /dev/null +++ b/samples/autodiff.typer @@ -0,0 +1,123 @@ +%* +%* Typer Compiler +%* +%* --------------------------------------------------------------------------- +%* +%(* Copyright (C) 2011-2016 Free Software Foundation, Inc. +%* +%* Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> +%* Keywords: languages, lisp, dependent types. +%* +%* 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: +%* Build a very basic symbolic differentiation library +%* +%* Limitations: +%* - Only (add) and (mult) +%* - Only a single unknown +%* - Only Integer operations +%* +%* ---------------------------------------------------------------------------*) + +Sym : Type; +Sym = inductive_ (dSym) + % leafs + (constant Int) + (placeholder String) + + % Nodes + (add Sym Sym) + (mult Sym Sym) + (inv Sym) + (neg Sym); + +constant = inductive-cons Sym constant; +placeholder = inductive-cons Sym placeholder; +add = inductive-cons Sym add; +mult = inductive-cons Sym mult; +inv = inductive-cons Sym inv; +neg = inductive-cons Sym neg; + +div : Sym -> Sym -> Sym; +div = lambda (up : Sym) -> + lambda (down : Sym) -> + (mult up (inv down)); + +sub : Sym -> Sym -> Sym; +sub = lambda (x : Sym) -> + lambda (y : Sym) -> + (add x (neg y)); + +sqr : Sym -> Sym; +sqr = lambda (x : Sym) -> + mult x x; + +zero = constant 0; +one = constant 1; +two = constant 2; + +% p should be even +%pow : Sym -> Int -> Sym; +%pow = lambda *x : Sym) -> lambda (p : Int) -> +% case p +% | 0 -> one +% | 1 -> x +% | _ -> mult (pow x (p / 2)) (pow x (p / 2)); + +eval : Int -> Sym -> Int; +eval = lambda (value : Int) -> + lambda (s : Sym) -> case s + | constant v => v + | placeholder _ => value + | add s1 s2 => ((eval value s1) + (eval value s2)) + | mult s1 s2 => (eval value s1) * (eval value s2); +% | inv s => (1 / (eval value s)) +% | neg s => (- (eval value s)) + +%print : Sym -> Type; +%print = lambda (s : Sym) -> +% case s +% | constant v => to-string v +% | placeholder n => to-string n +% | add s1 s2 => to-string s1 "+" s2 +% | mult s1 s2 => to-string s1 "*" s2; +% | inv s => to-string "1/" s +% | neg s => to-string "-" s; + +deriv : Sym -> Sym; +deriv = lambda (s : Sym) -> + case s + | constant v => zero + | placeholder _ => one + | add s1 s2 => (add (deriv s1) (deriv s2)) + | mult s1 s2 => let ds1 = (deriv s1); ds2 = (deriv s2); in + (add (mult ds1 s2) (mult ds2 s1)); +% | inv s => let up = (deriv s); down = (mult s s); in +% (neg (div up (sqr down))) +% | neg s => (- (deriv s)); + +y = placeholder "y"; +expr = mult y y; % y ^ 2 + +v1 = eval 4 expr; % 16 +main = eval 4 (deriv expr); % 8 + + + + ===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -40,7 +40,6 @@ open Debruijn open Env (* get_rte_variable *) - let builtin_error loc msg = msg_error "BUILT-IN" loc msg; raise (internal_error msg) @@ -115,12 +114,14 @@ let _generic_binary_iop name f loc (args_val: value_type list) (ctx: runtime_env (* i.e we don't need to push x and y in the context. *) (* We don't even need the context *) let l, r = match args_val with - | [a; b] -> (get_int a), (get_int b) + | [a; b] -> a, b | _ -> builtin_error loc (name ^ " expects 2 arguments") in - match l, r with + match (get_int l), (get_int r) with | Some v, Some w -> Value(Imm(Integer (loc, (f v w)))) - | _ -> builtin_error loc (name ^ " expects Integers as arguments") + | _ -> + value_print l; print_string " "; value_print r; + builtin_error loc (name ^ " expects Integers as arguments") ;; let iadd_impl = _generic_binary_iop "Integer::add" (fun a b -> a + b) @@ -128,6 +129,13 @@ let isub_impl = _generic_binary_iop "Integer::sub" (fun a b -> a - b) let imult_impl = _generic_binary_iop "Integer::mult" (fun a b -> a * b) let idiv_impl = _generic_binary_iop "Integer::div" (fun a b -> a / b) +(* +let eq_impl loc args_val ctx = + let l, r = match args_val with + | [a; b] -> a, b + | _ -> builtin_error loc "_=_ expects 2 arguments") in + + conv_p l r *) (* loc is given by the compiler *) let none_fun = (fun loc args_val ctx -> @@ -197,10 +205,11 @@ let builtin_expand = Builtin (SexpType, "expand_", type_mexpand) (* Built-in list of types/functions *) (* Some of the information is redundant but it suppress a lot of warnings *) let typer_builtins = [ -(* NAME | LXP | Type | impl *) - ("Type" , type0 , type0, none_fun); - ("Int" , type_int , type0, none_fun); - ("Float", type_float, type0, none_fun); +(* NAME | LXP | Type | impl *) + ("Type" , type0 , type0, none_fun); + ("Int" , type_int , type0, none_fun); + ("Float" , type_float , type0, none_fun); + ("String", type_string, type0, none_fun); (* Built-in Functions *) ("_=_" , builtin_eq, type_eq, none_fun); (* t -> t -> bool *) ===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -127,8 +127,9 @@ and eval_call ctx i lname args call = (* first lambda *) | Value (lxp), hd::tl -> (match lxp with | Cons _ -> - let cons_args = List.map (fun g -> (Aexplicit, (get_value_lexp g))) args_val in - Value(Call(lname, (cons_args))) + let cons_args = List.map (fun g -> + (Aexplicit, (get_value_lexp g))) args_val in + Value(Call(lname, (cons_args))) | _ -> (* Push first arg *) let nctx = add_rte_variable None hd ctx in ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -117,8 +117,8 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = | Pimm value -> (Imm(value), match value with | Integer _ -> type_int - | Float _ -> type_float - | String _ -> lexp_error tloc "Could not find String"; dltype; + | Float _ -> type_float + | String _ -> type_string; | _ -> lexp_error tloc "Could not find type"; pexp_print p; print_string "\n"; dltype) @@ -156,17 +156,27 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = v, type0 (* Pinductive *) - | Pinductive (label, [], ctors) -> + | Pinductive (label, formal_args, ctors) -> + let ctx = ref ctx in + (* (arg_kind * pvar * pexp option) list *) + let formal = List.map (fun (kind, var, opxp) -> + let ltp, _ = match opxp with + | Some pxp -> _lexp_p_infer pxp !ctx (i + 1) + | None -> dltype, dltype in + + ctx := env_extend !ctx var None dltype; + (kind, var, ltp) + ) formal_args in + (* (arg_kind * vdef * ltype) list *) + + let ctx = !ctx in let map_ctor = lexp_parse_inductive ctors ctx i in - let v = Inductive(tloc, label, [], map_ctor) in + let v = Inductive(tloc, label, formal, map_ctor) in v, type0 - (* *) - - | Plambda (kind, var, ptype, body) -> - let ltp, _ = match ptype with - | None -> dltype, dltype - | Some pt -> lexp_infer pt ctx in + (* This case can be inferred *) + | Plambda (kind, var, Some ptype, body) -> + let ltp, _ = lexp_infer ptype ctx in let nctx = env_extend ctx var None ltp in let lbody, lbtp = lexp_infer body nctx in @@ -261,7 +271,12 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = Case(loc, tlxp, tltp, lpattern, dflt), (return_type) - | _ -> lexp_fatal tloc "Unhandled Pexp" + | Phastype (_, pxp, ptp) -> + let ltp, _ = lexp_infer ptp ctx in + (_lexp_p_check pxp ltp ctx (i + 1)), ltp + + | _ -> pexp_print p; print_string "\n"; + lexp_fatal tloc "Unhandled Pexp" and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = let tloc = pexp_location p in @@ -270,6 +285,35 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = _global_lexp_trace := (i, tloc, p)::!_global_lexp_trace; match p with + (* This case cannot be inferred *) + | Plambda (kind, var, None, body) -> + (* Read var type from the provided type *) + let ltp, lbtp = match t with + | Arrow(kind, None, ltp, _, lbtp) -> ltp, lbtp + | _ -> lexp_error tloc "Type does not match"; dltype, dltype in + + let nctx = env_extend ctx var None ltp in + let lbody = _lexp_p_check body lbtp nctx (i + 1) in + + Lambda(kind, var, ltp, lbody) + + | Pcall (Pvar(_, "expand_"), _args) ->( + let pargs = List.map pexp_parse _args in + let largs = _lexp_parse_all pargs ctx i in + + let lxp = match largs with + | [lxp] -> lxp + | hd::tl -> lexp_error tloc "expand_ expects one lexp"; hd + | _ -> lexp_fatal tloc "expand_ expects one lexp" in + + (* eval argument *) + let sxp = match eval lxp (from_lctx ctx) with + | Vsexp(sxp) -> sxp + | _ -> lexp_fatal tloc "expand_ expects sexp" in + + let pxp = pexp_parse sxp in + _lexp_p_check pxp t ctx (i + 1)) + | _ -> let (e, inferred_t) = _lexp_p_infer p ctx (i + 1) in (* FIXME: check that inferred_t = t! *) e @@ -323,19 +367,9 @@ and lexp_call (fname: pexp) (_args: sexp list) ctx i = Call(vf, new_args), ret_type (* Is it a macro ? *) - | Some Builtin (_, "expand_", _) ->( - let lxp = match largs with - | [lxp] -> lxp - | hd::tl -> lexp_error loc "expand_ one lexp"; hd - | _ -> lexp_fatal loc "expand_ one lexp" in - - (* eval argument *) - let sxp = match eval lxp (from_lctx ctx) with - | Vsexp(sxp) -> sxp - | _ -> lexp_fatal loc "expand_ expects sexp" in - - let pxp = pexp_parse sxp in - lexp_p_infer pxp ctx) + | Some Builtin (_, "expand_", _) -> + lexp_error loc "expand_ require type annotation"; + dltype, dltype (* a builtin functions *) | Some e -> Call(e, new_args), ret_type @@ -499,40 +533,22 @@ and _lexp_decls decls ctx i: (((vdef * lexp * ltype) list) * lexp_context) = let rec merge_decls (decls: (pvar * pexp * bool) list) merged acc: ((location * pexp option * pexp option * int) SMap.t * string list) = - (* we cant evaluate here because variable are not in the environment *) + (* we cant evaluate here because variables 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 let (l, inst, _, i) = SMap.find name merged in - let new_decl = (l, inst, Some type_info, i) in - let nmerged = SMap.add name new_decl merged in - (merge_decls tl nmerged acc) - + | ((loc, name), pxp, bl)::tl -> + let (l, opxp, optp, i), acc = try (SMap.find name merged), acc with Not_found -> - (* add variable to ctx *) - let new_decl = (loc, None, Some type_info, !idx) in - let nmerged = SMap.add name new_decl merged in - idx := !idx + 1; - ctx := env_extend (!ctx) (loc, name) None dltype; - (merge_decls tl nmerged (name::acc)) end - - (* Instruction: Var = expr *) - | ((loc, name), inst, false) -> begin - try let (l, _, tp, i) = SMap.find name merged in - let new_decl = (l, Some inst, tp, i) in - let nmerged = SMap.add name new_decl merged in - (merge_decls tl nmerged acc) + idx := !idx + 1; + ctx := env_extend (!ctx) (loc, name) None dltype; + (loc, None, None, !idx - 1), (name::acc) in - with Not_found -> - (* add variable to ctx *) - let new_decl = (loc, Some inst, None, !idx) in - let nmerged = SMap.add name new_decl merged in - idx := !idx + 1; - ctx := env_extend (!ctx) (loc, name) None dltype; - (merge_decls tl nmerged (name::acc)) end in + let new_decl = match bl with + | true -> (l, opxp, Some pxp, i) + | false -> (l, Some pxp, optp, i) in + + let nmerged = SMap.add name new_decl merged in + (merge_decls tl nmerged acc) in let mdecls, ord = merge_decls decls SMap.empty [] in @@ -572,9 +588,9 @@ and _lexp_decls decls ctx i: (((vdef * lexp * ltype) list) * lexp_context) = n := !n - 1; match opxp, otpxp with - | Some pxp, Some _ -> + | Some pxp, Some ptp -> let ltp = env_lookup_type ctx vref in - let lxp, _ = _lexp_p_infer pxp ctx (i + 1) in + let lxp = _lexp_p_check pxp ltp ctx (i + 1) in (env_set_var_info ctx vref (Some lxp) ltp); lst := (vdef, lxp, ltp)::!lst ===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -187,6 +187,10 @@ and pexp_p_actual_arg arg : (arg_kind * pvar option * pexp) = | e -> (Aexplicit, None, pexp_parse e) and pexp_p_formal_arg arg : (arg_kind * pvar * pexp option) = + (* FYI: None of the formal arg type work *) + (* (a ::: Type) -> (a ::: Type) instead of (::: a Type) + * (a :: Type) -> (a :: Type) instead of (:: a Type) + * (a : Type) -> (_:_ a Type) instead of (_:_ a Type) *) match arg with | Node (Symbol (_, ":::"), [Symbol s; e]) -> (Aerasable, s, Some (pexp_parse e)) @@ -194,8 +198,13 @@ and pexp_p_formal_arg arg : (arg_kind * pvar * pexp option) = -> (Aimplicit, s, Some (pexp_parse e)) | Node (Symbol (_, ":"), [Symbol s; e]) -> (Aexplicit, s, Some (pexp_parse e)) + (* ------ FIXME: temp FIX ------ *) + | Node (Symbol (_, "_:_"), [Symbol s; e]) + -> (Aexplicit, s, Some (pexp_parse e)) + (* ------ --------------- ------ *) | Symbol s -> (Aexplicit, s, None) - | _ -> (pexp_error (sexp_location arg) "Unrecognized formal arg"); + | _ -> sexp_print arg; + (pexp_error (sexp_location arg) "Unrecognized formal arg"); (Aexplicit, (sexp_location arg, "{arg}"), None) and pexp_u_formal_arg (arg : arg_kind * pvar * pexp option) = ===================================== src/typecheck.ml ===================================== --- a/src/typecheck.ml +++ b/src/typecheck.ml @@ -28,7 +28,7 @@ open Sexp (* open Myers *) (* open Grammar *) open Lexp -open Builtin (* type_float *) + (* open Unify *) module S = Subst module L = List @@ -174,7 +174,7 @@ let rec unsusp e s = (* Push a suspension one level down. *) | Some e -> Some (mkSusp e s)) (********* Testing if a lexp is properly typed *********) - + type varbind = | Variable | ForwardRef @@ -288,4 +288,4 @@ let rec check ctx e = (* FIXME: If there are no branches nor default, then we have no * way to infer the type! *) (* FIXME: Check branches and default! *) - + ===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -97,8 +97,13 @@ let _ = (add_test "EVAL" "Let" (fun () -> let _ = (add_test "EVAL" "Lambda" (fun () -> reset_eval_trace (); + let dcode = " + sqr : Int -> Int; + sqr = lambda x -> x * x; + " in + (* Declare lambda *) - let rctx, lctx = eval_decl_str "sqr = lambda x -> x * x;" lctx rctx in + let rctx, lctx = eval_decl_str dcode lctx rctx in (* Eval defined lambda *) let ret = eval_expr_str "(sqr 4);" lctx rctx in @@ -113,7 +118,10 @@ let _ = (add_test "EVAL" "Nested Lambda" (fun () -> reset_eval_trace (); let code = " + sqr : Int -> Int; sqr = lambda x -> x * x; + + cube : Int -> Int; cube = lambda x -> x * (sqr x);" in (* Declare lambda *) @@ -204,9 +212,9 @@ let nat_decl = " zero = inductive-cons Nat zero; succ = inductive-cons Nat succ; - tonum : Nat -> Int; - tonum = lambda (x : Nat) -> case x - | (succ y) => (1 + (tonum y)) + to-num : Nat -> Int; + to-num = lambda (x : Nat) -> case x + | (succ y) => (1 + (to-num y)) | zero => 0;" ;; @@ -226,7 +234,7 @@ let _ = (add_test "EVAL" "Inductive::Recursive Call" (fun () -> let rctx, lctx = eval_decl_str code lctx rctx in - let rcode = "(tonum zero); (tonum one); (tonum two);"in + let rcode = "(to-num zero); (to-num one); (to-num two);"in (* Eval defined lambda *) let ret = eval_expr_str rcode lctx rctx in @@ -261,9 +269,9 @@ let _ = (add_test "EVAL" "Inductive::Nat Plus" (fun () -> let rctx, lctx = eval_decl_str code lctx rctx in let rcode = " - (tonum (plus zero two)); - (tonum (plus two zero)); - (tonum (plus two one));"in + (to-num (plus zero two)); + (to-num (plus two zero)); + (to-num (plus two one));"in (* Eval defined lambda *) let ret = eval_expr_str rcode lctx rctx in @@ -348,19 +356,66 @@ let _ = (add_test "EVAL" "Partial Application" (fun () -> | _ -> failure () ));; -(* + +let list_decl = " +List : Type; List = inductive_ (dList (a : Type)) (nil) (cons a (List a)); nil = inductive-cons List nil; cons = inductive-cons List cons; -length : (a : Type) => List a -> Nat; -length = lambda a => lambda (xs : List a) -> +% length : (a : Type) => List a -> Int; +% length = lambda a => +length : List a -> Int; +length = lambda (xs : List a) -> case xs - | nil => zero - | cons x xs => succ (length xs); -*) + | nil => 0 + | cons hd tl => (1 + length tl); + +% head : (a : Type) => List a -> a; +% head = lambda a => +head : List a -> a; +head = lambda (xs : List a) -> + case xs + | nil => nil + | cons hd tl => hd; + +% tail : (a : Type) => List a -> List a; +% tail = lambda a => +tail : List a -> List a; +tail = lambda (xs : List a) -> + case xs + | nil => nil + | cons hd tl => tl; +";; + +let _ = (add_test "EVAL" "List" (fun () -> + reset_eval_trace (); + + let dcode = list_decl ^ " + my_list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + " in + + let rctx, lctx = eval_decl_str dcode lctx rctx in + + let rcode = "(length my_list); + (head my_list); + (head (tail my_list));" 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) 4 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 () +));; (* run all tests *) ===================================== tests/macro_test.ml ===================================== --- a/tests/macro_test.ml +++ b/tests/macro_test.ml @@ -57,6 +57,7 @@ let _ = (add_test "MACROS" "macros base" (fun () -> sqr_sexp = (node_ (symbol_ \"lambda_->_\") (symbol_ \"x\") (node_ (symbol_ \"_*_\") (symbol_ \"x\") (symbol_ \"x\"))); + sqr : Int -> Int; sqr = (expand_ sqr_sexp);" in let rctx, lctx = eval_decl_str dcode lctx rctx in View it on GitLab: https://gitlab.com/monnier/typer/commit/29bde6e0d32025100113463a0516a45e48c…

1 0

[Git][monnier/typer][master] * src/subst.ml (compose): Simplify
by Stefan 20 Avr '16

20 Avr '16

Stefan pushed to branch master at Stefan / Typer Commits: 70f86081 by Stefan Monnier at 2016-04-20T15:42:17-04:00 * src/subst.ml (compose): Simplify (Shift): Switch argument order to better match the notation. (lookup): Rename from `apply`. - - - - - 2 changed files: - src/subst.ml - src/typecheck.ml Changes: ===================================== src/subst.ml ===================================== --- a/src/subst.ml +++ b/src/subst.ml @@ -139,31 +139,27 @@ module U = Util * * I guess I'm leaning towards a kind of λσ, but with * - * σ = nil | σ ↑n | a·σ + * σ = id | σ ↑n | a·σ * - * where lift σ == #0·(σ ∘ nil ↑) == #0·(σ ↑) - * and σ ↑n == (σ ∘ ↑n) + * where σ ↑n == (σ ∘ ↑n) + * and lift σ == #0·(σ ↑) * and #n == [#0, ↑n] * * (λt₁)t₂ ==> [t₁, t₂·nil] * [λt, σ] ==> λ[t, lift σ] - * [t, nil] ==> t + * [t, id] ==> t * [#0, t·σ] ==> t * [#i+1, t·σ] ==> [#i, σ] (because => [[#i, ↑] t·σ] => [#i, ↑ ∘ t·σ]) * [#i, σ ↑n] ==> [[#i, σ], ↑n] * * Merging rules: * - * nil ∘ σ ==> σ - * σ ∘ nil ==> σ - * (σ ↑n₂) ↑n₁ ==> σ ↑(n₁+n₂) - * σ ↑n₁ ∘ nil ↑n₂ ==> σ ↑(n₁+n₂) - * σ₁ ↑n₁ ∘ (a·σ₂) ↑n₂ ==> σ₁ ↑(n₁-1) ∘ σ₂ ↑n₂ - * σ₁ ↑n ∘ a·σ₂ ==> σ₁ ↑(n-1) ∘ σ₂ - * a·σ₁ ∘ σ₂ ↑n ==> (a·σ₁ ∘ σ₂) ↑n - * a·σ₁ ∘ σ₂ ==> [a, σ₂]·(σ₁ ∘ σ₂) - * - * σ ∘ nil ↑n ==> σ ↑n + * (σ ↑n₂) ↑n₁ ==> σ ↑(n₁+n₂) {part of m1} + * σ₁ ∘ id ==> σ₁ {m2} + * σ₁ ∘ σ₂ ↑n ==> (σ₁ ∘ σ₂) ↑n {part of m1} + * id ∘ σ ==> σ {m3} + * σ₁ ↑n ∘ a·σ₂ ==> σ₁ ↑(n-1) ∘ σ₂ {m4 & m5} + * a·σ₁ ∘ σ₂ ==> [a, σ₂]·(σ₁ ∘ σ₂) {m6} * * The optimisations used in FLINT would translate to: * @@ -172,7 +168,7 @@ module U = Util * ==> [t₁, #0·(σ ↑) ∘ t₂·nil] * ==> [t₁, [#0, t₂·nil]·(σ ↑ ∘ t₂·nil)] * ==> [t₁, t₂·σ] - * [[t, σ], nil ↑n] ==> [t, σ ∘ nil ↑n] + * [[t, σ], id ↑n] ==> [t, σ ∘ id ↑n] * ==> [t, σ ↑n] * * Confluence: @@ -180,11 +176,13 @@ module U = Util * a·σ₁ ∘ σ₂ ↑n ==> (a·σ₁ ∘ σ₂) ↑n * a·σ₁ ∘ σ₂ ↑n ==> [a, σ₂ ↑n]·(σ₁ ∘ σ₂ ↑n) * - * so we also need a rule + * so we might also need to make sure that * * (a·σ₁ ∘ σ₂) ↑n <==> [a, σ₂ ↑n]·(σ₁ ∘ σ₂ ↑n) * - * for confluence + * for confluence. Which might boild down to adding a rule like + * + * (a·σ₁) ↑n <==> [a, id ↑n]·(σ₁ ↑n) *) (* We define here substitutions which take a variable within a source context @@ -208,29 +206,31 @@ type 'a subst = (* lexp subst *) * context Δₛ₁ΔₜΔₛ₂ where Δₛ₂ has size N and Δₜ has size M. *) | Identity | Cons of 'a * 'a subst - | Shift of db_offset * 'a subst + | Shift of 'a subst * db_offset (* | Lift of db_index * db_offset *) -(* Apply a substitution. Also called `lookup`. *) -let apply (mkVar : 'b -> db_index -> 'a) - (mkShift: db_offset -> 'a -> 'a) +(* Apply a substitution to a single variable. *) +let lookup (mkVar : 'b -> db_index -> 'a) + (mkShift: 'a -> db_offset -> 'a) (s: 'a subst) (l : 'b) (v:db_index) : 'a = - let rec apply' (o:db_offset) (s: 'a subst) (v:db_index) : 'a = + let rec lookup' (o:db_offset) (s: 'a subst) (v:db_index) : 'a = match s with | Identity -> mkVar l (v+o) - | Shift (o', s) -> apply' (o+o') s v - | Cons (e, s) -> if v>0 then apply' o s (v-1) - else mkShift o e - in apply' 0 s v + | Shift (s, o') -> lookup' (o+o') s v + | Cons (e, s) -> if v>0 then lookup' o s (v-1) + else mkShift e o + in lookup' 0 s v -let mkShift (m:db_offset) s = - match s with Shift (n, s') -> Shift (n+m, s') - | _ -> if m>0 then Shift (m, s) else s +let mkShift s (m:db_offset) = + if m>0 then + match s with Shift (s', n) -> Shift (s', n+m) + | _ -> Shift (s, m) + else s (* A substitution which adds M to every deBruijn index. * I.e. one that takes variables from a context Δₛ to an extended * context ΔₛΔₜ where Δₜ has size M. *) -let shift (m:db_offset) = mkShift m Identity +let shift (m:db_offset) = mkShift Identity m (* The trivial substitution which doesn't do anything. *) let identity = Identity @@ -245,14 +245,9 @@ let compose (mkSusp : 'a -> 'a subst -> 'a) match s1, s2 with | (Identity, s2) -> s2 | (s1, Identity) -> s1 - | (Shift (o1, s1), Shift (o2, Identity)) -> Shift (o1+o2, s1) - | (s1, Shift (o, Identity)) -> Shift (o, s1) - | (Shift (o1, s1), Shift (o2, Cons (e, s2))) - -> compose' (mkShift (o1-1) s1) (mkShift o2 s2) - | (Shift (o1, s1), Cons (e, s2)) -> compose' (mkShift (o1-1) s1) s2 - | (Cons (e, s1), Shift (o2, s2)) -> Shift (o2, compose' (Cons (e, s1)) s2) + | (s1, Shift (s2, o2)) -> mkShift (compose' s1 s2) o2 + | (Shift (s1, o1), Cons (e, s2)) -> compose' (mkShift s1 (o1-1)) s2 | (Cons (e, s1), s2) -> Cons (mkSusp e s2, compose' s1 s2) - | (_, Shift (_, Shift (_, _))) -> U.internal_error "Nested Shift!" in compose' s1 s2 (* Adjust a substitution for use under one more binder. @@ -260,7 +255,7 @@ let compose (mkSusp : 'a -> 'a subst -> 'a) * from Δs,x to Δₜ,x. * Also known as `lift`. *) let sink (mkVar : 'b -> db_index -> 'a) (l:'b) (s:'a subst) = - Cons (mkVar l 0, mkShift 1 s) + Cons (mkVar l 0, mkShift s 1) (* Return a substitution which replaces #0 with `e`. *) let substitute e = Cons (e, Identity) ===================================== src/typecheck.ml ===================================== --- a/src/typecheck.ml +++ b/src/typecheck.ml @@ -45,12 +45,12 @@ let rec mkSusp e s = if S.identity_p s then e else match e with | Susp (e, s') -> mkSusp e (scompose s' s) - | Var (l,v) -> sapply s l v (* Apply the substitution eagerly. *) + | Var (l,v) -> slookup s l v (* Apply the substitution eagerly. *) | _ -> Susp (e, s) and scompose s1 s2 = S.compose mkSusp s1 s2 -and sapply s l v = S.apply (fun l i -> Var (l, i)) - (fun o e -> mkSusp e (S.shift o)) - s l v +and slookup s l v = S.lookup (fun l i -> Var (l, i)) + (fun e o -> mkSusp e (S.shift o)) + s l v let ssink = S.sink (fun l i -> Var (l, i)) @@ -76,9 +76,9 @@ and conv_p' (s1:lexp S.subst) (s2:lexp S.subst) e1 e2 : bool = (* BEWARE: When we'll make expand let-defined vars here, we'll have to * be careful not to introduce infinite-recursion. *) | (Var (l1, v1), e2) when not (S.identity_p s1) -> - conv_p' S.identity s2 (sapply s1 l1 v1) e2 + conv_p' S.identity s2 (slookup s1 l1 v1) e2 | (e1, Var (l2, v2)) when not (S.identity_p s2) -> - conv_p' s1 S.identity e1 (sapply s2 l2 v2) + conv_p' s1 S.identity e1 (slookup s2 l2 v2) | (Var (_, v1), Var (_, v2)) -> v1 == v2 | (Susp (e1, s1'), e2) -> conv_p' (scompose s1' s1) s2 e1 e2 | (e1, Susp (e2, s2')) -> conv_p' s1 (scompose s2' s2) e1 e2 @@ -129,7 +129,7 @@ let rec unsusp e s = (* Push a suspension one level down. *) | Sort (l, Stype e) -> Sort (l, Stype (mkSusp e s)) | Sort (l, _) -> e | Builtin _ -> e - | Var ((l,_) as lv,v) -> U.msg_error "SUSP" l "¡Susp(Var)!"; sapply s lv v + | Var ((l,_) as lv,v) -> U.msg_error "SUSP" l "¡Susp(Var)!"; slookup s lv v | Susp (e,s') -> U.msg_error "SUSP" (lexp_location e) "¡Susp(Susp)!"; mkSusp e (scompose s' s) | Let (l, defs, e) View it on GitLab: https://gitlab.com/monnier/typer/commit/70f8608101d7088a9079bba090d6c078a85…

1 0

[Git][monnier/typer][master] 5 commits: minor changes
by Setepenre 20 Avr '16

20 Avr '16

Setepenre pushed to branch master at Stefan / Typer Commits: acbe9589 by Pierre Delaunay at 2016-04-17T20:09:54-04:00 minor changes - - - - - 66678b3b by Pierre Delaunay at 2016-04-18T10:42:21-04:00 Merge branch 'master' of https://gitlab.com/monnier/typer - - - - - f1ee2eb8 by Pierre Delaunay at 2016-04-19T12:40:55-04:00 new implementations lexp_p_decls Changes to be committed: * src/lparse.ml: - added type of types - added a new implementation of lexp_p_decls but commented it out as it requires handling shifting - - - - - 6a2ba53d by Pierre Delaunay at 2016-04-19T15:12:23-04:00 Merge branch 'master' of https://gitlab.com/monnier/typer - - - - - de90e983 by Pierre Delaunay at 2016-04-20T02:46:34-04:00 Added macro handling in lparse.ml Changes to be committed: * src/builtin.ml: added (expand_) * src/eval.ml: new function (from_lctx) * src/lparse.ml: handle the macro case in lexp_call - - - - - 8 changed files: - GNUmakefile - src/builtin.ml - src/debruijn.ml - src/env.ml - src/eval.ml - src/lparse.ml - src/subst.ml - tests/macro_test.ml Changes: ===================================== GNUmakefile ===================================== --- a/GNUmakefile +++ b/GNUmakefile @@ -78,3 +78,6 @@ run/ityper: run/tests: @./_build/tests/utests --verbose= 1 + +run/ityper-file: + @./_build/ityper ./samples/test__.typer ===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -75,9 +75,11 @@ let type_eq = let lv = (dloc, "l") in Arrow (Aexplicit, None, Var (tv, 1), dloc, type0)))) -let builtin_iadd = Builtin (IAdd, "_+_", iop_binary) +let builtin_iadd = Builtin (IAdd, "_+_", iop_binary) let builtin_imult = Builtin (IMult, "_*_", iop_binary) -let builtin_eq = Builtin (EqType, "_=_", type_eq) (* +let builtin_eq = Builtin (EqType, "_=_", type_eq) +let builtin_sexp = Builtin (SexpType, "sexp", type0) +(* let builtin_fadd = Builtin (FAdd, "_+_", fop_binary) let builtin_fmult = Builtin (FMult, "_*_", fop_binary) *) @@ -135,12 +137,12 @@ let make_symbol loc args_val ctx = (* symbol is a simple string *) let lxp = match args_val with | [r] -> r - | _ -> builtin_error loc ("symbol_ expects 1 arguments") in + | _ -> builtin_error loc ("symbol_ expects 1 argument") in let s = get_string lxp in match s with | Some str -> Vsexp(Symbol(loc, str)) - | _ -> builtin_error loc ("symbol_ expects sexp as arguments") + | _ -> builtin_error loc ("symbol_ expects one string as argument") let make_node loc args_val ctx = @@ -159,17 +161,29 @@ let make_node loc args_val ctx = Vsexp(Node(op, s)) + let make_block loc args_val ctx = Value(type0) let make_string loc args_val ctx = Value(type0) let make_integer loc args_val ctx = Value(type0) let make_float loc args_val ctx = Value(type0) -let builtin_block = Builtin (SexpType, "block_", type0) -let builtin_symbol = Builtin (SexpType, "symbol_", type0) -let builtin_string = Builtin (SexpType, "string_", type0) -let builtin_integer = Builtin (SexpType, "integer_", type0) -let builtin_float = Builtin (SexpType, "float_", type0) -let builtin_node = Builtin (SexpType, "node_", type0) +let type_string = type0 +let type_mblock = type0 + +let type_msymbol = Arrow (Aexplicit, None, type_string, dloc, builtin_sexp) +let type_mstring = Arrow (Aexplicit, None, type_string, dloc, builtin_sexp) +let type_minteger = Arrow (Aexplicit, None, type_int, dloc, builtin_sexp) +let type_mfloat = Arrow (Aexplicit, None, type_float, dloc, builtin_sexp) +let type_mnode = Arrow (Aexplicit, None, builtin_sexp,dloc, builtin_sexp) +let type_mexpand = Arrow (Aexplicit, None, builtin_sexp,dloc, type0) + +let builtin_block = Builtin (SexpType, "block_", type_mblock) +let builtin_symbol = Builtin (SexpType, "symbol_", type_msymbol) +let builtin_string = Builtin (SexpType, "string_", type_mstring) +let builtin_integer = Builtin (SexpType, "integer_", type_minteger) +let builtin_float = Builtin (SexpType, "float_", type_mfloat) +let builtin_node = Builtin (SexpType, "node_", type_mnode) +let builtin_expand = Builtin (SexpType, "expand_", type_mexpand) (* * Should we have a function that @@ -194,12 +208,13 @@ let typer_builtins = [ ("_*_" , builtin_imult, iop_binary, imult_impl); (* int -> int -> int *) (* Macro primitives *) - ("block_" , builtin_block , type0, make_block); - ("symbol_" , builtin_symbol , type0, make_symbol); - ("string_" , builtin_string , type0, make_string); - ("integer_", builtin_integer, type0, make_integer); - ("float_" , builtin_float , type0, make_float); - ("node_" , builtin_node , type0, make_node); + ("block_" , builtin_block , type_mblock , make_block); + ("symbol_" , builtin_symbol , type_msymbol , make_symbol); + ("string_" , builtin_string , type_mstring , make_string); + ("integer_", builtin_integer, type_minteger, make_integer); + ("float_" , builtin_float , type_mfloat , make_float); + ("node_" , builtin_node , type_mnode , make_node); + ("expand_" , builtin_expand , type_mexpand , none_fun); (* Macros primitives type ? *) ===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -122,7 +122,8 @@ let env_add_var_info var (ctx: lexp_context) = (a, cons (ref 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 ((n, map), e, f) = ctx in + env_add_var_info (n, def, v, t) (senv_add_var def ctx) let _name_error loc estr str = ===================================== src/env.ml ===================================== --- a/src/env.ml +++ b/src/env.ml @@ -37,7 +37,7 @@ open Sexp open Lexp (* lexp_print *) open Myers - +open Debruijn let dloc = dummy_location @@ -55,6 +55,8 @@ type value_type = | Closure of lexp * (((string option * value_type) ref myers) * (int * int)) (* Macro type *) | Vsexp of sexp + (* Unable to eval during macro expansion, only throw if the value is used *) + | Vdummy let get_value_lexp (vtp: value_type) = match vtp with @@ -65,9 +67,10 @@ let get_value_lexp (vtp: value_type) = let value_print (vtp: value_type) = match vtp with | Closure (lxp, _) -> - print_string ("Closure(" ^ (_lexp_to_str (!debug_ppctx) lxp)) + print_string ("Closure(" ^ (_lexp_to_str (!debug_ppctx) lxp) ^ ")") | Value s -> lexp_print s | Vsexp sxp -> sexp_print sxp + | _ -> print_string "value_print_dummy" let value_location (vtp: value_type) = lexp_location (get_value_lexp vtp) @@ -108,6 +111,16 @@ let get_rte_variable (name: string option) (idx: int) (ctx: runtime_env): value_ n ^ "\" idx: " ^ (str_idx idx)) ;; +let rte_shift vref ctx = + let (_, (osize, _)) = ctx in (* number of variable declared outside *) + let csize = get_rte_size ctx in (* current size *) + let offset = csize - osize in + let ((loc, name), idx) = vref in + (* check if variable is free *) + let offset = if idx > offset then offset else 0 in + (* shift idx *) + idx + offset + let add_rte_variable name (x: value_type) (ctx: runtime_env): runtime_env = let (l, b) = ctx in let lst = (cons (ref (name, x)) l) in @@ -198,3 +211,4 @@ let print_rte_ctx (ctx: runtime_env) = value_print g; print_string "\n") ;; + ===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -105,11 +105,12 @@ let rec _eval lxp ctx i: (value_type) = (* Case *) | Case (loc, target, _, pat, dflt) -> (eval_case ctx i loc target pat dflt) - | _ -> lexp_print lxp; Value(Imm(String(dloc, "eval Not Implemented"))) + | _ -> print_string "debug catch-all eval: "; + lexp_print lxp; Value(Imm(String(dloc, "eval Not Implemented"))) and eval_var ctx lxp v = let ((loc, name), idx) = v in - try get_rte_variable (Some name) idx ctx + try get_rte_variable (Some name) (idx) ctx with Not_found -> eval_error loc ("Variable: " ^ name ^ (str_idx idx) ^ " was not found ") @@ -283,7 +284,7 @@ and _eval_decls (decls: ((vdef * lexp * ltype) list)) (* Read declarations once and push them *) let _, ctx = List.fold_left (fun (idx, ctx) ((_, name), lxp, ltp) -> - _global_eval_trace := []; + let lxp = _eval lxp ctx (i + 1) in let ctx = set_rte_variable idx (Some name) lxp ctx in (idx - 1, ctx)) @@ -303,7 +304,6 @@ and print_eval_trace () = ;; let eval lxp ctx = - _global_eval_trace := []; _eval lxp ctx 1 let debug_eval lxp ctx = @@ -321,3 +321,27 @@ let eval_all lxps rctx silent = List.map (fun g -> evalfun g rctx) lxps;; +(* build a rctx from a lctx *) +let from_lctx (ctx: lexp_context): runtime_env = + let ((_, _), env, _) = ctx in + let rctx = ref (default_rctx ()) in + + (* Skip builtins *) + let bsize = List.length typer_builtins in + let csize = get_size ctx in + + for i = bsize to csize do + let (_, (_, name), exp, _) = !(Myers.nth (csize - i) env) in + + let vxp = match exp with + | Some lxp -> (eval lxp !rctx) + | None -> Vdummy in + + rctx := add_rte_variable (Some name) vxp (!rctx) + done; + + !rctx + + + + ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -38,6 +38,7 @@ open Sexp open Pexp open Lexp +open Env open Debruijn open Eval @@ -141,19 +142,26 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = let bdy, ltp = lexp_infer body nctx in Let(tloc, decl, bdy), ltp - (* ->/=> *) + (* ------------------------------------------------------------------ *) | Parrow (kind, Some var, tp, loc, expr) -> - let nvar = var in (* /!\ HERE *) let ltyp, _ = lexp_infer tp ctx in let lxp, _ = lexp_infer expr ctx in - let v = Arrow(kind, Some nvar, ltyp, tloc, lxp) in - v, v + let v = Arrow(kind, Some var, ltyp, tloc, lxp) in + v, type0 | Parrow (kind, None, tp, loc, expr) -> let ltyp, _ = lexp_infer tp ctx in let lxp, _ = lexp_infer expr ctx in let v = Arrow(kind, None, ltyp, tloc, lxp) in - v, v + v, type0 + + (* Pinductive *) + | Pinductive (label, [], ctors) -> + let map_ctor = lexp_parse_inductive ctors ctx i in + let v = Inductive(tloc, label, [], map_ctor) in + v, type0 + + (* *) | Plambda (kind, var, ptype, body) -> let ltp, _ = match ptype with @@ -169,12 +177,6 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = | Pcall (fname, _args) -> lexp_call fname _args ctx i - (* Pinductive *) - | Pinductive (label, [], ctors) -> - let map_ctor = lexp_parse_inductive ctors ctx i in - let v = Inductive(tloc, label, [], map_ctor) in - v, v - (* Pcons *) | Pcons(vr, sym) -> ( let (loc, type_name) = vr in @@ -183,14 +185,14 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = (* 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 *) - let idt = env_lookup_type ctx (vr, idx) in + let idt = env_lookup_expr ctx (vr, idx) in (* make Base type *) let inductive_type = Var((loc, type_name), idx) in (* Get constructor args *) let args = match idt with - | Inductive(_, _, _, ctor_def) -> ( + | Some Inductive(_, _, _, ctor_def) -> ( try (SMap.find cname ctor_def) with Not_found -> lexp_error loc @@ -261,7 +263,7 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = | _ -> lexp_fatal tloc "Unhandled Pexp" -and lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = +and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = let tloc = pexp_location p in _global_lexp_ctx := ctx; @@ -319,6 +321,23 @@ and lexp_call (fname: pexp) (_args: sexp list) ctx i = match env_lookup_expr ctx ((loc, name), idx) with | None -> lexp_error loc "Unknown builtin"; Call(vf, new_args), ret_type + + (* Is it a macro ? *) + | Some Builtin (_, "expand_", _) ->( + let lxp = match largs with + | [lxp] -> lxp + | hd::tl -> lexp_error loc "expand_ one lexp"; hd + | _ -> lexp_fatal loc "expand_ one lexp" in + + (* eval argument *) + let sxp = match eval lxp (from_lctx ctx) with + | Vsexp(sxp) -> sxp + | _ -> lexp_fatal loc "expand_ expects sexp" in + + let pxp = pexp_parse sxp in + lexp_p_infer pxp ctx) + + (* a builtin functions *) | Some e -> Call(e, new_args), ret_type ) else Call(vf, new_args), ret_type @@ -415,6 +434,62 @@ and lexp_parse_inductive ctors ctx i = (* Parse let declaration *) and lexp_p_decls decls ctx = _lexp_decls decls ctx 1 and _lexp_decls decls ctx i: (((vdef * lexp * ltype) list) * lexp_context) = + (* (pvar * pexp * bool) list * ) + + let ctx = ref ctx in + let mdecls = ref SMap.empty in + let order = ref [] in + let found = ref false in + + List.iter (fun ((loc, name), pxp, bl) -> + (* Check if variable was already defined *) + let (l, olxp, oltp, _) = try found := true; SMap.find name !mdecls + with Not_found -> + (* keep track of declaration order *) + order := (name::!order); + found := false; + (* create an empty element *) + (loc, None, None, 0) in + + (* create a dummy env for lexp_parse *) + let denv = env_extend (!ctx) (loc, name) None dltype in + + (* Do we already have a type ? *) + let lxp, ltp = match oltp with + (* We infer *) + | None -> _lexp_p_infer pxp denv (i + 1) + + (* We check *) + | Some ltp -> (_lexp_p_check pxp ltp denv (i + 1)), ltp in + + (* update declaration *) + (* FIXME: modify env when lxp is found *) + let new_decl = match bl with + | true -> (if !found then () else ctx := env_extend (!ctx) (loc, name) None lxp); + (l, olxp, Some lxp, i) + | false -> (if !found then () else ctx := env_extend (!ctx) (loc, name) (Some lxp) ltp); + (l, Some lxp, oltp, i) in + + (* Add Variable to the map *) + mdecls := SMap.add name new_decl !mdecls) + + decls; + + let ctx = !ctx in + let mdecls = !mdecls in + let order = !order in + (* Cast Map to list *) + let ndecls = List.map (fun name -> + let (l, inst, tp, _) = SMap.find name mdecls in + match inst, tp with + | Some lxp, Some ltp -> ((l, name), lxp, ltp) + | Some lxp, None -> ((l, name), lxp, dltype) + | None, Some ltp -> lexp_warning l "Type with no expression"; + ((l, name), dltype, ltp) + | None, None -> lexp_warning l "No expression, No Type"; + ((l, name), dltype, dltype)) order in + + (List.rev ndecls), ctx *) let ctx = ref ctx in let idx = ref 0 in @@ -469,35 +544,52 @@ and _lexp_decls decls ctx i: (((vdef * lexp * ltype) list) * lexp_context) = (* This is required for later *) let ctx = !ctx in let lst = ref [] in - let n = ref ((List.length ndecls) - 1) in - (* for each declaration lexp their rhs *) - List.iter (fun ((loc, name), opxp, otpxp) -> - let vdef = (loc, name) in - let vref = (vdef, !n) in - n := !n - 1; - - match opxp, otpxp with - | Some pxp, Some tpxp -> - (* Add type first (for recursive definition) *) - let ltp, _ = _lexp_p_infer tpxp ctx (i + 1) in - (env_set_var_info ctx vref None ltp); - let lxp, _ = _lexp_p_infer pxp ctx (i + 1) in - (env_set_var_info ctx vref (Some lxp) ltp); + (* Doing types and expressions separately allow us to use *) + (* all typing information when lexp_parsing recursive definition *) + (* The price of this is iterating twice over declarations *) + (* + now we need to lookup type info *) - lst := (vdef, lxp, ltp)::!lst - - | Some pxp, None -> - let lxp, ltp = _lexp_p_infer pxp ctx (i + 1) in - (env_set_var_info ctx vref (Some lxp) ltp); - lst := (vdef, lxp, ltp)::!lst + (* Process types once *) + let n = ref ((List.length ndecls) - 1) in + (* for each declaration lexp their types *) + List.iter (fun ((loc, name), opxp, otpxp) -> + let vdef = (loc, name) in + let vref = (vdef, !n) in + n := !n - 1; + + match opxp, otpxp with + | _, Some tpxp -> let ltp, _ = _lexp_p_infer tpxp ctx (i + 1) in + (env_set_var_info ctx vref None ltp); + | _ -> ()) + ndecls; - | None, _ -> lexp_warning loc "Unused Variable" + (* Process declaration in itself*) + let n = ref ((List.length ndecls) - 1) in + List.iter (fun ((loc, name), opxp, otpxp) -> + let vdef = (loc, name) in + let vref = (vdef, !n) in + n := !n - 1; + + match opxp, otpxp with + | Some pxp, Some _ -> + let ltp = env_lookup_type ctx vref in + let lxp, _ = _lexp_p_infer pxp ctx (i + 1) in + (env_set_var_info ctx vref (Some lxp) ltp); + lst := (vdef, lxp, ltp)::!lst + + | Some pxp, None -> + let lxp, ltp = _lexp_p_infer pxp ctx (i + 1) in + (env_set_var_info ctx vref (Some lxp) ltp); + lst := (vdef, lxp, ltp)::!lst + + | None, _ -> lexp_warning loc "Unused Variable" ) ndecls; List.rev (!lst), ctx + and _lexp_parse_all (p: pexp list) (ctx: lexp_context) i : lexp list = let rec loop (plst: pexp list) ctx (acc: lexp list) = @@ -640,4 +732,4 @@ 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 -;; \ No newline at end of file +;; ===================================== src/subst.ml ===================================== --- a/src/subst.ml +++ b/src/subst.ml @@ -21,6 +21,40 @@ this program. If not, see <http://www.gnu.org/licenses/>. *) module U = Util + +(* Suspensions definitions. + * + * ol: old embedding level ('associate' level, length with environement) + * nl: new .... + * + * n: A Natural Number + * i: A positive integer + * + * t ::= c : + * #i : Debruijn Index variable bound by the ith abstraction + * (t, t) : Applications + * (λ t) : Abstractions + * [t, n, n, e] : Suspensions + * + * length level + * e ::= nil : 0 : 0 + * (t, n)::e : n + len(e) : n + * {e1, nl, ol, e2} : len(e1) + len(e2) - nl : lev(e1) + nl - ol + * + * level is the dbi index ? + * + * Substitutions Compositions definitions. + * + * a ::= 1 + * a b + * (λ a) : + * a[s] : + * + * s ::= id : identity + * a . s : cons replace dbi_idx = 0 by a use s for the rest + * s o t : Composition + * shift : dbi_index + 1 + *) (* Substitutions. * * There are many different ways to implement a calculus with explicit @@ -40,7 +74,7 @@ module U = Util * The normal beta rule is: * * (λ t₁) t₂ ==> [t₁, 1, 0, (t₂,0) :: nil] - * + * * which would be instantiated to * * (λ [t₁, ol, nl, e]) t₂ ==> [[t₁, ol, nl, e], 1, 0, (t₂,0) :: nil] @@ -168,7 +202,7 @@ type db_offset = int (* DeBruijn index offset. *) * In practice, 'a is always lexp, but we keep it as a paramter: * - for better modularity of the code. * - to break a mutual dependency between the Lexp and the Subst modules. *) -type 'a subst = +type 'a subst = (* lexp subst *) (* Lift (n,m) increases indices≥N by M. * IOW, it takes variables from a source context Δₛ₁Δₛ₂ to a destination * context Δₛ₁ΔₜΔₛ₂ where Δₛ₂ has size N and Δₜ has size M. *) ===================================== tests/macro_test.ml ===================================== --- a/tests/macro_test.ml +++ b/tests/macro_test.ml @@ -54,17 +54,19 @@ let _ = (add_test "MACROS" "macros base" (fun () -> (* define 'lambda x -> x * x' using macros *) let dcode = " - sqrt_sexp = (node_ (symbol_ \"lambda_->_\") (symbol_ \"x\") - (node_ (symbol_ \"_*_\") (symbol_ \"x\") (symbol_ \"x\"))); " in + sqr_sexp = (node_ (symbol_ \"lambda_->_\") (symbol_ \"x\") + (node_ (symbol_ \"_*_\") (symbol_ \"x\") (symbol_ \"x\"))); + + sqr = (expand_ sqr_sexp);" in let rctx, lctx = eval_decl_str dcode lctx rctx in - let ecode = "(sqrt_sexp);" in + let ecode = "(sqr 3);" in let ret = eval_expr_str ecode lctx rctx in match ret with - | [r] -> value_print r; print_string "\n"; success (); + | [r] -> expect_equal_int (get_int r) (3 * 3) | _ -> failure ()) );; View it on GitLab: https://gitlab.com/monnier/typer/compare/ccb4d1aa4a79f15f6fa26f92885f1b79db…

1 0

[Git][monnier/typer][master] * src/typecheck.ml (check): Handle Susp and Call
by Stefan 18 Avr '16

18 Avr '16

Stefan pushed to branch master at Stefan / Typer Commits: ccb4d1aa by Stefan Monnier at 2016-04-18T21:13:23-04:00 * src/typecheck.ml (check): Handle Susp and Call * src/subst.ml (substitute): New function. * src/typecheck.ml: Don't open Util any more. (unsusp, sort_compose): New functions. (check): Improve: add Call case, and half of Inductive. - - - - - 3 changed files: - src/lexp.ml - src/subst.ml - src/typecheck.ml Changes: ===================================== src/lexp.ml ===================================== #<Gitlab::Git::Diff:0x007fd224679938> ===================================== src/subst.ml ===================================== #<Gitlab::Git::Diff:0x007fd224679398> ===================================== src/typecheck.ml ===================================== #<Gitlab::Git::Diff:0x007fd224678da8> View it on GitLab: https://gitlab.com/monnier/typer/commit/ccb4d1aa4a79f15f6fa26f92885f1b79db7…

1 0

[Git][monnier/typer][master] * src/subst.ml: Rewrite completely, mostly following the λσ approach
by Stefan 18 Avr '16

18 Avr '16

Stefan pushed to branch master at Stefan / Typer Commits: b978cb6b by Stefan Monnier at 2016-04-18T08:21:44-04:00 * src/subst.ml: Rewrite completely, mostly following the λσ approach * .gitignore: Add missing final newline. Fix #*# pattern. * src/lexp.ml (lexp): Swap Susp's arguments, to match the order usually used in papers. Adjust all users accordingly. * src/typecheck.ml (mkSusp, scompose, sapply, ssink): New helpers to use the new substitutions. (conv_p'): Adjust to new substitutions's type. (check): Check that Let's types are indeed types. Fix compilation. - - - - - 5 changed files: - .gitignore - DESIGN - src/lexp.ml - src/subst.ml - src/typecheck.ml Changes: ===================================== .gitignore ===================================== #<Gitlab::Git::Diff:0x000000058ce830> ===================================== DESIGN ===================================== #<Gitlab::Git::Diff:0x000000058ce0d8> ===================================== src/lexp.ml ===================================== #<Gitlab::Git::Diff:0x000000058cd840> ===================================== src/subst.ml ===================================== #<Gitlab::Git::Diff:0x000000058cd340> ===================================== src/typecheck.ml ===================================== #<Gitlab::Git::Diff:0x000000058ccc88> View it on GitLab: https://gitlab.com/monnier/typer/commit/b978cb6bc84bf6316d6e60e3793139d8bfb…

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Avril 2016