Typer
Threads by month
- ----- 2026 -----
- August
- July
- June
- May
- April
- March
- February
- January
- ----- 2025 -----
- December
- November
- October
- September
- August
- July
- June
- May
- April
- March
- February
- January
- ----- 2024 -----
- December
- November
- October
- September
- August
- July
- June
- May
- April
- March
- February
- January
- ----- 2023 -----
- December
- November
- October
- September
- August
- July
- June
- May
- April
- March
- February
- January
- ----- 2022 -----
- December
- November
- October
- September
- August
- July
- June
- May
- April
- March
- February
- January
- ----- 2021 -----
- December
- November
- October
- September
- August
- July
- June
- May
- April
- March
- February
- January
- ----- 2020 -----
- December
- November
- October
- September
- August
- July
- June
- May
- April
- March
- February
- January
- ----- 2019 -----
- December
- November
- October
- September
- August
- July
- June
- May
- April
- March
- February
- January
- ----- 2018 -----
- December
- November
- October
- September
- August
- July
- June
- May
- April
- March
- February
- January
- ----- 2017 -----
- December
- November
- October
- September
- August
- July
- June
- May
- April
- March
- February
- January
- ----- 2016 -----
- December
- November
- October
- September
- August
- July
- June
- May
- April
- March
- February
April 2016
- 4 participants
- 22 discussions
29 Apr '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
28 Apr '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
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
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 Apr '16
by Stefan 26 Apr '16
26 Apr '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
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
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
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
18 Apr '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 Apr '16
by Stefan 18 Apr '16
18 Apr '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