Stefan pushed to branch master at Stefan / Typer

Commits: 2b74a79a by Stefan Monnier at 2017-02-23T17:34:23-05:00 * src/env.ml (value_type) <Vtype>: New, replaces Vdummy and Vinductive

(value_equal): Adjust accordingly. Emit a warning for Vundefined.

* src/eval.ml (make_symbol, make_string, make_integer): Simplify. (make_float): Implement. (make_block): Comment out. (read_impl, write_impl): Simplify. (eval_call): Adjust Vinductive case to the new Vtype and tweak it so that the result can itself be passed to eval_call, in case the inductive type is applied to more than one argument. (_eval_decls, y_operator): Use Vundefined instead of Vdummy. (register_built_functions): Comment out `block_`.

* src/lexp.ml (_lexp_str): Remove unreachable case. (lexp_str.septp): Remove, unused.

* btl/builtins.typer (block_): Comment out, not implemented.

* src/elexp.ml (elexp): Unify Type and Inductive. Keep lexp in `Type`.

* tests/env_test.ml (_.rctx): Use Vundefined instead of Vdummy.

- - - - -

7 changed files:

- btl/builtins.typer - src/elexp.ml - src/env.ml - src/eval.ml - src/lexp.ml - src/opslexp.ml - tests/env_test.ml

Changes:

===================================== btl/builtins.typer ===================================== --- a/btl/builtins.typer +++ b/btl/builtins.typer @@ -3,7 +3,7 @@ %* %* --------------------------------------------------------------------------- %* -%* Copyright (C) 2011-2016 Free Software Foundation, Inc. +%* Copyright (C) 2011-2017 Free Software Foundation, Inc. %* %* Author: Pierre Delaunay pierre.delaunay@hec.ca %* Keywords: languages, lisp, dependent types. @@ -118,7 +118,7 @@ cons = datacons List cons; % Macro % -----------------------------------------------------

-block_ = Built-in "block_" (List Sexp -> Sexp); +%% block_ = Built-in "block_" (List Pretoken -> Sexp); symbol_ = Built-in "symbol_" (String -> Sexp); string_ = Built-in "string_" (String -> Sexp); node_ = Built-in "node_" (Sexp -> List Sexp -> Sexp);

===================================== src/elexp.ml ===================================== --- a/src/elexp.ml +++ b/src/elexp.ml @@ -35,6 +35,7 @@ open Sexp (* Sexp type *) open Pexp (* Aexplicit *)

module U = Util +module L = Lexp

type vname = U.vname type vref = U.vref @@ -55,10 +56,7 @@ type elexp = | Case of U.location * elexp * (U.location * (vname option) list * elexp) SMap.t * (vname option * elexp) option - (* Type place-holder just in case *) - | Type - (* Inductive takes a slot in the env that is why it need to be here *) - | Inductive of U.location * label + | Type of L.lexp

let rec elexp_location e = match e with @@ -70,8 +68,7 @@ let rec elexp_location e = | Call (f,_) -> elexp_location f | Cons ((l,_)) -> l | Case (l,_,_,_) -> l - | Inductive(l, _) -> l - | Type -> U.dummy_location + | Type e -> L.lexp_location e

let elexp_name e = @@ -82,10 +79,9 @@ let elexp_name e = | Call _ -> "Call" | Cons _ -> "Cons" | Case _ -> "Case" - | Type -> "Type" + | Type _ -> "Type" | Lambda _ -> "Lambda" | Builtin _ -> "Builtin" - | Inductive _ -> "Inductive"

let rec elexp_print lxp = print_string (elexp_string lxp) and elexp_string lxp = @@ -132,7 +128,4 @@ and elexp_string lxp = | Case(_, t, cases, default) -> "case " ^ (elexp_string t) ^ (str_cases cases) ^ (maybe_str default)

- | Inductive(_, (_, s)) -> - "typecons " ^ s - - | Type -> "Type " + | Type e -> "Type(" ^ L.lexp_string e ^ ") "

===================================== src/env.ml ===================================== --- a/src/env.ml +++ b/src/env.ml @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2016 Free Software Foundation, Inc. + * Copyright (C) 2011-2017 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -56,8 +56,7 @@ type value_type = | Vsexp of sexp (* Values passed to macros. *) (* Unable to eval during macro expansion, only throw if the value is used *) | Vundefined - | Vdummy - | Vinductive + | Vtype of L.lexp (* The lexp value can't be trusted. *) | Vin of in_channel | Vout of out_channel | Vcommand of (unit -> value_type) @@ -68,33 +67,33 @@ type value_type =

let rec value_equal a b = match a, b with - | Vint(i1), Vint(i2) -> i1 = i2 - | Vstring(s1), Vstring(s2) -> s1 = s2 - | Vbuiltin(s1), Vbuiltin(s2) -> s1 = s2 - | Vfloat(f1), Vfloat(f2) -> f1 = f2 - | Vsexp(a), Vsexp(b) -> sexp_equal a b - | Vin (c1), Vin(c2) -> c1 = c2 - | Vout (c1), Vout(c2) -> c2 = c2 - | Vcommand (f1), Vcommand(f2)-> f1 = f2 - | Vdummy, Vdummy -> warning dloc "Vdummy"; true - | Vinductive, Vinductive -> warning dloc "Vinductive"; true - - | Closure(s1, b1, ctx1), Closure(s2, b2, ctx2) -> - warning dloc "Closure"; - if (s1 != s2) then false else true - - | Vcons((_, ct1), a1), Vcons((_, ct2), a2) -> - if (ct1 != ct2) then false else - not (List.exists2 - (fun a b -> not (value_equal a b)) a1 a2) + | Vint (i1), Vint (i2) -> i1 = i2 + | Vstring (s1), Vstring (s2) -> s1 = s2 + | Vbuiltin (s1), Vbuiltin (s2) -> s1 = s2 + | Vfloat (f1), Vfloat (f2) -> f1 = f2 + | Vsexp (a), Vsexp (b) -> sexp_equal a b + | Vin (c1), Vin (c2) -> c1 = c2 + | Vout (c1), Vout (c2) -> c2 = c2 + | Vcommand (f1), Vcommand (f2) -> f1 = f2 + | Vundefined, _ | _, Vundefined -> warning dloc "Vundefined"; false + | Vtype e1, Vtype e2 -> warning dloc "Vtype"; false + + | Closure (s1, b1, ctx1), Closure (s2, b2, ctx2) + -> warning dloc "Closure"; + if (s1 != s2) then false else true + + | Vcons ((_, ct1), a1), Vcons ((_, ct2), a2) + -> if (ct1 != ct2) then false else + not (List.exists2 + (fun a b -> not (value_equal a b)) + a1 a2)

| _ -> false

let rec value_eq_list a b = match a, b with | [], [] -> true - | v1::vv1, v2::vv2 -> - value_equal v1 v2 && value_eq_list vv1 vv2 + | v1::vv1, v2::vv2 -> value_equal v1 v2 && value_eq_list vv1 vv2 | _ -> false

let value_location (vtp: value_type) = @@ -110,22 +109,19 @@ let value_name v = | Vout _ -> "Vout" | Vint _ -> "Vint" | Vsexp _ -> "Vsexp" + | Vtype _ -> "Vtype" | Vcons _ -> "Vcons" | Vfloat _ -> "Vfloat" | Vundefined -> "Vundefined" - | Vdummy -> "Vdummy" | Vstring _ -> "Vstring" | Closure _ -> "Closure" | Vbuiltin _ -> "Vbuiltin" | Vcommand _ -> "Vcommand" - | Vinductive -> "Vinductive"

let rec value_string v = match v with | Vin _ -> "in_channel" | Vout _ -> "out_channe;" - | Vdummy -> "dummy" - | Vinductive -> "inductive" | Vundefined -> "<undefined!>" | Vcommand _ -> "command" | Vstring s -> """ ^ s ^ """ @@ -133,11 +129,13 @@ let rec value_string v = | Vint i -> string_of_int i | Vfloat f -> string_of_float f | Vsexp s -> sexp_string s + | Vtype e -> L.lexp_string e | Closure (s, elexp, _) -> "(lambda " ^ s ^ " -> " ^ (elexp_string elexp) ^ ")" - | Vcons ((_, s), lst) -> - let args = List.fold_left (fun str v -> - (str ^ " " ^ (value_string v))) "" lst in - "(" ^ s ^ args ^ ")" + | Vcons ((_, s), lst) + -> let args = List.fold_left + (fun str v -> str ^ " " ^ value_string v) + "" lst in + "(" ^ s ^ args ^ ")"

let value_print (vtp: value_type) = print_string (value_string vtp)

@@ -174,9 +172,9 @@ let set_rte_variable idx name (v: value_type) (ctx : runtime_env) = let (n, ref_cell) = (M.nth idx ctx) in

(match (n, name) with - | Some n1, Some n2 -> - if (n1 != n2) then - error dloc ("Variable's Name must Match: " ^ n1 ^ " vs " ^ n2) + | Some n1, Some n2 + -> if (n1 != n2) then + error dloc ("Variable's Name must Match: " ^ n1 ^ " vs " ^ n2) | _ -> ());

ref_cell := v

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -138,15 +138,9 @@ let _ = add_binary_iop "+" (+); add_binary_iop "*" ( * ); add_binary_iop "/" (/)

-let make_symbol loc depth args_val = - (* symbol is a simple string *) - let lxp = match args_val with - | [r] -> r - | _ -> error loc ("symbol_ expects 1 argument") in - - match lxp with - | Vstring(str) -> Vsexp(Symbol(loc, str)) - | _ -> value_error loc lxp "symbol_ expects one string as argument" +let make_symbol loc depth args_val = match args_val with + | [Vstring str] -> Vsexp (Symbol (loc, str)) + | _ -> error loc "symbol_ expects one string as argument"

let make_node loc depth args_val =

@@ -170,26 +164,22 @@ let make_node loc depth args_val =

Vsexp(Node(op, s))

-let make_string loc depth args_val = - let lxp = match args_val with - | [r] -> r - | _ -> error loc "string_ expects 1 argument" in +let make_string loc depth args_val = match args_val with + | [Vstring str] -> Vsexp (String (loc, str)) + | _ -> error loc "string_ expects one string as argument"

- match lxp with - | Vstring(str) -> Vsexp(String(loc, str)) - | _ -> value_error loc lxp "string_ expects one string as argument" +let make_integer loc depth args_val = match args_val with + | [Vint (str)] -> Vsexp (Integer (loc, str)) + | _ -> error loc "integer_ expects one integer as argument"

-let make_integer loc depth args_val = - let lxp = match args_val with - | [r] -> r - | _ -> error loc "integer_ expects 1 argument" in

- match lxp with - | Vint(str) -> Vsexp(Integer(loc, str)) - | _ -> value_error loc lxp "integer_ expects one string as argument" +let make_float loc depth args_val = match args_val with + | [Vfloat x] -> Vsexp (Float (loc, x)) + | _ -> error loc "float_ expects one float as argument"

-let make_float loc depth args_val = Vdummy -let make_block loc depth args_val = Vdummy +(* let make_block loc depth args_val = match args_val with + * | [Vblock b] -> Vsexp (Block (loc, b)) + * | _ -> error loc "float_ expects one block as argument" *)

(* FIXME: We're not using predef here. This will break if we change * the definition of `Bool` in builtins.typer. *) @@ -197,20 +187,17 @@ let ttrue = Vcons ((dloc, "true"), []) let tfalse = Vcons ((dloc, "false"), []) let o2v_bool b = if b then ttrue else tfalse

-let string_eq loc depth args_val = - match args_val with - | [Vstring(s1); Vstring(s2)] -> o2v_bool (s1 = s2) - | _ -> error loc "string_eq expects 2 strings" +let string_eq loc depth args_val = match args_val with + | [Vstring s1; Vstring s2] -> o2v_bool (s1 = s2) + | _ -> error loc "string_eq expects 2 strings"

-let int_eq loc depth args_val = - match args_val with - | [Vint(s1); Vint(s2)] -> o2v_bool (s1 = s2) - | _ -> error loc "int_eq expects 2 integer" +let int_eq loc depth args_val = match args_val with + | [Vint i1; Vint i2] -> o2v_bool (i1 = i2) + | _ -> error loc "int_eq expects 2 integers"

-let sexp_eq loc depth args_val = - match args_val with - | [Vsexp (s1); Vsexp (s2)] -> o2v_bool (sexp_equal s1 s2) - | _ -> error loc "sexp_eq expects 2 sexp" +let sexp_eq loc depth args_val = match args_val with + | [Vsexp (s1); Vsexp (s2)] -> o2v_bool (sexp_equal s1 s2) + | _ -> error loc "sexp_eq expects 2 sexps"

let open_impl loc depth args_val =

@@ -225,27 +212,21 @@ let open_impl loc depth args_val = | "w" -> Vout(open_out file) | _ -> error loc "wrong open mode")

-let read_impl loc depth args_val = - - let channel = match args_val with - | [Vin(c); _] -> c - | _ -> - List.iter (fun v -> value_print v; print_string "\n") args_val; - error loc "read expects an in_channel" in - - let line = input_line channel in - Vstring(line) +let read_impl loc depth args_val = match args_val with + (* FIXME: Either rename it to "readline" and drop the second arg, + * or actually pay attention to the second arg. *) + | [Vin channel; Vint n] -> Vstring (input_line channel) + | _ -> List.iter (fun v -> value_print v; print_string "\n") args_val; + error loc "read expects an in_channel"

-let write_impl loc depth args_val =

- let channel, msg = match args_val with - | [Vout(c); Vstring(msg)] -> c, msg - | _ -> - List.iter (fun v -> value_print v) args_val; - error loc "read expects an out_channel" in +let write_impl loc depth args_val = match args_val with + | [Vout channel; Vstring msg] -> fprintf channel "%s" msg; + (* FIXME: This should be the unit value! *) + Vundefined + | _ -> List.iter (fun v -> value_print v) args_val; + error loc "write expects an out_channel and a string"

- fprintf channel "%s" msg; - Vdummy

let rec _eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type) =

@@ -267,7 +248,6 @@ let rec _eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type | Imm(Integer (_, i)) -> Vint(i) | Imm(String (_, s)) -> Vstring(s) | Imm(sxp) -> Vsexp(sxp) - | Inductive (_, _) -> Vinductive | Cons (label) -> Vcons (label, []) | Lambda ((_, n), lxp) -> Closure(n, lxp, ctx) | Builtin ((_, str)) -> Vbuiltin(str) @@ -292,7 +272,17 @@ let rec _eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type | Case (loc, target, pat, dflt) -> (eval_case ctx trace loc target pat dflt)

- | Type -> Vcons((tloc, "Unit"), []) + (* FIXME: Here, we'd want to apply `ctx` to `e`, but we can't + * apply a runtime-ctx to a lexp! + * E.g. say we have `λt ≡> Ind (arg : t)`: by the time we get here, + * Our `Type` carries `Ind (arg : t)` but `t` is not in `ctx`! + * So we should either use an elexp instead of a lexp, + * or somehow recover a lexp-ctx from the runtime-ctx (maybe + * with extra info that `Type` could carry), + * or find another trick. + * Hence, the `e` carried by `Vtype` is just indicative and not + * something we can use. *) + | Type e -> Vtype e

and eval_var ctx lxp v = @@ -350,12 +340,15 @@ and eval_call loc unef i f args = buildbody (arity - nargs - 1), buildctx args Myers.nil)

- with Not_found -> - error loc ("Requested Built-in `" ^ name ^ "` does not exist") - | e -> error loc ("Exception thrown from primitive `" ^ name ^"`")) + with Not_found + -> error loc ("Requested Built-in `" ^ name ^ "` does not exist") + | e -> error loc ("Exception thrown from primitive `" ^ name ^"`"))

- (* Type Alias is not a fun call, we just ignore it*) - | Vinductive, _ -> Vundefined + | Vtype e, _ + (* We may call a Vlexp e.g. for "x = Map Int String". + * FIXME: The arg will sometimes be a Vlexp but not always, so this is + * really just broken! *) + -> Vtype (L.mkCall (e, [(Aexplicit, Var ((dummy_location, "?"), -1))])) | _ -> value_fatal loc f "Trying to call a non-function!"

and eval_case ctx i loc target pat dflt = @@ -409,7 +402,7 @@ and _eval_decls (decls: (vname * elexp) list)

(* Read declarations once and push them *) let nctx = List.fold_left (fun ctx ((_, name), _) -> - add_rte_variable (Some name) Vdummy ctx) ctx decls in + add_rte_variable (Some name) Vundefined ctx) ctx decls in

List.iteri (fun idx ((_, name), lxp) -> let v = _eval lxp nctx i in @@ -559,7 +552,7 @@ and print_eval_trace trace = let y_operator loc depth args = match args with | [f] -> let aname = "<anon>" in - let yf_ref = ref Vdummy in + let yf_ref = ref Vundefined in let yf = Closure(aname, Call (Var ((dloc, "f"), 1), [Var ((dloc, "yf"), 2); @@ -579,7 +572,7 @@ let nop_fun loc _ vs = match vs with let register_built_functions () = List.iter (fun (name, f, arity) -> add_builtin_function name f arity) [ - ("block_" , make_block, 1); + (* ("block_" , make_block, 1); *) ("symbol_" , make_symbol, 1); ("string_" , make_string, 1); ("integer_" , make_integer, 1);

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -657,7 +657,6 @@ and _lexp_str ctx (exp : lexp) : string = let h1, decls, idt_lvl = match _lexp_str_decls inter_ctx decls with | h1::decls -> h1, decls, 2 - | h1::[] -> h1, [], 1 | _ -> "", [], 1 in

let decls = List.fold_left (fun str elem -> @@ -773,9 +772,6 @@ and _lexp_str_decls ctx decls =

let lexp_str = _lexp_str ctx in let sepdecl = (if pp_decl ctx then "\n" else "") in - let septp = match pp_parent ctx with - | Some _ -> "" - | None -> "\n" in

let type_str name lxp = (if pp_type ctx then ( name ^ " : " ^ (lexp_str lxp) ^ ";") else "") in

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -839,11 +839,11 @@ let rec erase_type (lxp: L.lexp): E.elexp = | L.Susp(l, s) -> erase_type (L.push_susp l s)

(* To be thrown out *) - | L.Arrow _ -> E.Type - | L.SortLevel _ -> E.Type - | L.Sort _ -> E.Type + | L.Arrow _ -> E.Type lxp + | L.SortLevel _ -> E.Type lxp + | L.Sort _ -> E.Type lxp (* Still useful to some extent. *) - | L.Inductive(l, label, _, _) -> E.Inductive(l, label) + | L.Inductive(l, label, _, _) -> E.Type lxp | L.Metavar _ -> U.internal_error "Metavar in erase_type"

and filter_arg_list lst =

===================================== tests/env_test.ml ===================================== --- a/tests/env_test.ml +++ b/tests/env_test.ml @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2016 Free Software Foundation, Inc. + * Copyright (C) 2011-2017 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -56,14 +56,14 @@ 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 (Vdummy) ctx) + add_rte_variable n Vundefined ctx) rctx var in

print_rte_ctx rctx;

let rctx, _ = List.fold_left (fun (ctx, idx) (n, _, v) -> - (set_rte_variable idx n (Vdummy) ctx); + (set_rte_variable idx n Vundefined ctx); (ctx, idx - 1)) (rctx, n) var in

View it on GitLab: https://gitlab.com/monnier/typer/commit/2b74a79aa66909fa373baeb8bdcbcf47faef...