Stefan pushed to branch master at Stefan / Typer
Commits: 65acc4ec by Stefan Monnier at 2016-12-02T10:21:43-05:00 Keep uppercase for types
* btl/builtins.typer (Void, False, True, Not, Decidable): New types. (true, false, some, none): Lowercase the name.
* samples/test.typer: Remove.
* src/builtin.ml (predef_name): Remove Unit and Bool. Adjust to new bool names. (o2l_bool): New function. (o2l_list): Rename from olist2tlist_lexp. Switch arg order. (o2v_list): Rename from olist2tlist_rte. (v2o_list): Rename from tlist2olist. Drop first arg.
* src/eval.ml (o2v_bool): Rename from btyper.
* src/lparse.ml (sform_has_attribute): Use `mem` and o2l_bool.
- - - - -
9 changed files:
- btl/builtins.typer - samples/pervasive.typer - samples/quote.typer - − samples/test.typer - src/builtin.ml - src/eval.ml - src/lparse.ml - tests/eval_test.ml - tests/unify_test.ml
Changes:
===================================== btl/builtins.typer ===================================== --- a/btl/builtins.typer +++ b/btl/builtins.typer @@ -35,23 +35,26 @@ % Base Types % -----------------------------------------------------
+% The trivial type which carries no information. Unit = inductive_ Unit unit; unit = datacons Unit unit;
+% The empty type, with no constructors: nothing can have this type. +Void = inductive_ Void; + % Basic operators _+_ = Built-in "Int.+" (Int -> Int -> Int); _-_ = Built-in "Int.-" (Int -> Int -> Int); _*_ = Built-in "Int.*" (Int -> Int -> Int); _/_ = Built-in "Int./" (Int -> Int -> Int);
-Bool = inductive_ (Boolean) (True) (False); -True = datacons Bool True; -False = datacons Bool False; +Bool = inductive_ (Boolean) (true) (false); +true = datacons Bool true; +false = datacons Bool false;
-%Option : Type -> Type; -Option = inductive_ (Option (a : Type)) (None) (Some a); -Some = datacons Option Some; -None = datacons Option None; +Option = inductive_ (Option (a : Type)) (none) (some a); +some = datacons Option some; +none = datacons Option none;
string_eq = Built-in "string_eq" (String -> String -> Bool); int_eq = Built-in "int_eq" (Int -> Int -> Bool); @@ -83,8 +86,8 @@ head : (a : Type) ≡> List a -> Option a; head = lambda a ≡> lambda xs -> case xs - | nil => None - | cons hd tl => Some hd; + | nil => none + | cons hd tl => some hd;
tail : (a : Type) ≡> List a -> List a; tail = lambda a ≡> @@ -164,3 +167,20 @@ run-io = Built-in "run-io" ((a : Type) ≡> IO Unit -> a -> a); open = Built-in "open" (String -> String -> IO FileHandle); write = Built-in "write" (FileHandle -> String -> IO Unit); read = Built-in "read" (FileHandle -> Int -> IO String); + + +% ----------------------------------------------------- +% Logic +% ----------------------------------------------------- + +% False should be one of the many empty types. +% Other common choices are False = ∀a.a and True = ∃a.a. +False = Void; +True = Unit; + +Not : Type -> Type; +Not prop = prop -> False; + +% Like Bool, except that it additionally carries the meaning of its value. +Decidable = inductive_ (Decidable (prop : Type)) + (true (p ::: prop)) (false (p ::: Not prop));
===================================== samples/pervasive.typer ===================================== --- a/samples/pervasive.typer +++ b/samples/pervasive.typer @@ -2,8 +2,6 @@
Nat = inductive_ Type (zero : Nat) (succ : Nat -> Nat);
-False = inductive_ Type; - Macro = inductive_ Type (MacroExp : Nat -> Macro);
%% Use for `cast'. @@ -13,6 +11,4 @@ or = inductive_ (t -> t -> Type) (left: t1 -> or t1 t2) (right: t2 -> or t1 t2);
-not = lambda x -> (x -> False); - -classical-or = lambda x -> lambda y -> not (not (or x y)); +classical-or = lambda x -> lambda y -> Not (Not (or x y));
===================================== samples/quote.typer ===================================== --- a/samples/quote.typer +++ b/samples/quote.typer @@ -35,8 +35,8 @@ node : Sexp -> List Sexp -> Sexp; node = lambda (op : Sexp) -> lambda (y : List Sexp) -> case (sexp_eq op (symbol_ "uquote")) - | True => has-uquote y - | False => hasnot-uquote op y; + | true => has-uquote y + | false => hasnot-uquote op y;
% tree traversal
===================================== samples/test.typer deleted ===================================== --- a/samples/test.typer +++ /dev/null @@ -1,76 +0,0 @@ -%% Issues: -%% - syntax of "telescopes", especially the implicit and erasable args. -%% -%% test {t} [dict : t -> t -> Bool] (x : t) (y : t) : Int = ...def... -%% -%% - syntax of Inductives. -%% -%% type List t -%% | nil -%% | cons [dict : Ord t] (head : t) (tail : List t) -%% -%% - syntax of funcalls -%% -%% test {t = Int} [dict = int_eq] 3 4 -%% -%% Notes: -%% - by analogy to the ->/=>/≡> distinctions, we could potentially use -%% "a :/::/:::/ b", but that wouldn't work for the case where we don't -%% want to specify the type explicitly. -%% - in telescopes (i.e. definitions), we could use the same syntax for -%% implicit and erasable, and distinguish based on the use of the variable -%% (e.g. in function definitions, see if it can be erasable), tho it's not -%% clear how to do it for Inductive definitions. -%% - in funcalls, we could use the same syntax for implicit and erasable, -%% and distinguish based on the type of the function being called. - -a = 3; - -Nat : Type -Nat = inductive_ (dummy_Nat) (zero) (succ Nat); -zero = datacons Nat zero; -succ = datacons Nat succ; -toZero = lambda z -> - case z - | zero => zero - | succ x => toZero x; -x = 1; - -id = lambda (α : Type) ≡> lambda x : α -> x; - -%% This requires HM inference, not yet implemented. -%% identity = lambda x -> x; - -%% This requires HM inference, not yet implemented. -%% x : a -> a; -%% x = lambda y ≡> lambda z -> z; - -plus = lambda x y -> - case x - | zero => y - | succ x => succ (plus x y); - -List = inductive (dummy_List (α : Type)) - (nil) - (cons α (List α)); -nil = datacons List nil; -cons = datacons List cons; -length : (α : Type) ≡> List α -> Nat; -length = lambda α ≡> lambda (xs : List α) -> - case xs - | nil => zero - | cons x xs => succ (length xs); - -%% This requires HM inference, not yet implemented. -%% length2 : List α -> Nat; -%% length2 = lambda xs -> -%% case_ xs -%% (nil => zero) -%% (cons x xs => succ (length2 xs)); - -False = inductive (dummy_False); -Unit = inductive (dummy_Unit) (unit); -unit = datacons Unit unit; -Bool = inductive (dummy_Bool) (true) (false); -false = datacons Bool false; -true = datacons Bool true;
===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -62,7 +62,7 @@ module OL = Opslexp open Lexp
module DB = Debruijn -open Env (* get_rte_variable *) +module E = Env
let error loc msg = msg_error "BUILT-IN" loc msg; raise (internal_error msg) let warning loc msg = msg_warning "BUILT-IN" loc msg @@ -70,10 +70,8 @@ let warning loc msg = msg_warning "BUILT-IN" loc msg let predef_name = [ "cons"; "nil"; - "Unit"; - "True"; - "False"; - "Bool"; + "true"; + "false"; "Macro"; "expand_macro_"; "expand_dmacro_"; @@ -113,33 +111,38 @@ let type_eq = let lv = (dloc, "l") in DB.type0))))
+let o2l_bool ctx b = get_predef (if b then "true" else "false") ctx + (* lexp Imm list *) -let olist2tlist_lexp lst ctx = +let o2l_list ctx lst = let tcons = get_predef "cons" ctx in let tnil = get_predef "nil" ctx in
let rlst = List.rev lst in List.fold_left (fun tail elem -> - mkCall(tcons, [(Aexplicit, (Imm(elem))); + mkCall(tcons, [(Aexplicit, (Imm (elem))); (Aexplicit, tail)])) tnil rlst
(* typer list as seen during runtime *) -let olist2tlist_rte lst = - let tnil = Vcons((dloc, "nil"), []) in - let rlst = List.rev lst in - List.fold_left (fun tail elem -> - Vcons((dloc, "cons"), [Vsexp(elem); tail])) tnil rlst +let o2v_list lst = + (* FIXME: We're not using predef here. This will break if we change + * the definition of `List` in builtins.typer. *) + List.fold_left (fun tail elem + -> E.Vcons ((dloc, "cons"), [E.Vsexp (elem); tail])) + (E.Vcons ((dloc, "nil"), [])) + (List.rev lst)
(* Typer list to Ocaml list *) -let rec tlist2olist acc expr = - match expr with - | Vcons((_, "cons"), [hd; tl]) -> tlist2olist (hd::acc) tl - | Vcons((_, "nil"), []) -> List.rev acc - | _ -> - print_string (value_name expr); print_string "\n"; - value_print expr; - error dloc "List conversion failure'" +let v2o_list v = + let rec v2o_list acc v = + match v with + | E.Vcons ((_, "cons"), [hd; tl]) -> v2o_list (hd::acc) tl + | E.Vcons ((_, "nil"), []) -> List.rev acc + | _ -> print_string (E.value_name v); print_string "\n"; + E.value_print v; + error dloc "List conversion failure'" in + v2o_list [] v
(* Map of lexp builtin elements accessible via (## <name>). *) let lmap = ref (SMap.empty : (lexp * ltype) SMap.t)
===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -157,7 +157,7 @@ let make_node loc depth args_val =
(* value_print tlist; print_string "\n"; *)
- let args = tlist2olist [] tlist in + let args = v2o_list tlist in
let s = List.map (fun g -> match g with | Vsexp(sxp) -> sxp @@ -191,23 +191,25 @@ let make_integer loc depth args_val = let make_float loc depth args_val = Vdummy let make_block loc depth args_val = Vdummy
-let ttrue = Vcons((dloc, "True"), []) -let tfalse = Vcons((dloc, "False"), []) -let btyper b = if b then ttrue else tfalse +(* FIXME: We're not using predef here. This will break if we change + * the definition of `Bool` in builtins.typer. *) +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)] -> btyper (s1 = s2) + | [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)] -> btyper (s1 = s2) + | [Vint(s1); Vint(s2)] -> o2v_bool (s1 = s2) | _ -> error loc "int_eq expects 2 integer"
let sexp_eq loc depth args_val = match args_val with - | [Vsexp (s1); Vsexp (s2)] -> btyper (sexp_equal s1 s2) + | [Vsexp (s1); Vsexp (s2)] -> o2v_bool (sexp_equal s1 s2) | _ -> error loc "sexp_eq expects 2 sexp"
let open_impl loc depth args_val = @@ -466,7 +468,7 @@ and sexp_dispatch loc depth args = match sxp with | Node (op, s) ->( let rctx = add_rte_variable None (Vsexp(op)) rctx in - let rctx = add_rte_variable None (olist2tlist_rte s) rctx in + let rctx = add_rte_variable None (o2v_list s) rctx in match eval nd rctx with | Closure(_, nd, _) -> eval nd rctx | _ -> error loc "Node has 2 arguments") @@ -480,7 +482,7 @@ and sexp_dispatch loc depth args = | Float (_ , f) -> eval flt (add_rte_variable None (Vfloat(f)) rctx) (* | Block (_ , s, _) -> - eval blk (add_rte_variable None (olist2tlist_rte s)) *) + eval blk (add_rte_variable None (o2v_list s)) *) | _ -> error loc "sexp_dispatch error"
(* -------------------------------------------------------------------------- *)
===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -821,7 +821,7 @@ and lexp_expand_macro_ macro_funct sargs ctx expand_fun : value_type = (* Build the function to be called *) let macro_expand = BI.get_predef expand_fun ctx in let args = [(Aexplicit, macro_funct); - (Aexplicit, (BI.olist2tlist_lexp sargs ctx))] in + (Aexplicit, (BI.o2l_list ctx sargs))] in
(* FIXME: Don't `mkCall + eval` but use eval_call instead! *) let macro = mkCall (macro_expand, args) in @@ -842,7 +842,7 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * elab_context) = let ret = lexp_expand_dmacro lxp sargs ctx in
(* convert typer list to ocaml *) - let decls = BI.tlist2olist [] ret in + let decls = BI.v2o_list ret in
(* extract sexp from result *) let decls = List.map (fun g -> @@ -1014,12 +1014,10 @@ and sform_has_attribute ctx loc (sargs : sexp list) = let meta_ctx, _ = !global_substitution in let map, attr_type = match OL.lexp_whnf table (ectx_to_lctx ctx) meta_ctx with | Builtin (_, attr_type, Some map) -> map, attr_type - | lxp -> lexp_fatal loc lxp "get-attribute expects a table as first argument" in + | lxp -> lexp_fatal loc lxp + "get-attribute expects a table as first argument" in
- try let _ = AttributeMap.find var map in - BI.get_predef "True" ctx - with Not_found -> - BI.get_predef "False" ctx + BI.o2l_bool ctx (AttributeMap.mem var map)
and sform_declexpr ctx loc sargs = match List.map (lexp_parse_sexp ctx) sargs with
===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -258,7 +258,7 @@ let _ = test_eval_eqv_named head my_list; head (tail my_list)"
- "4; Some 1; Some 2" + "4; some 1; some 2"
(* * Special forms @@ -279,7 +279,7 @@ let _ = test_eval_eqv_named "has-attribute greater-than w; (get-attribute greater-than w) 3;"
- "True; 3" + "true; 3"
let _ = (add_test "EVAL" "Monads" (fun () ->
===================================== tests/unify_test.ml ===================================== --- a/tests/unify_test.ml +++ b/tests/unify_test.ml @@ -81,9 +81,9 @@ let fmt (lst: (lexp * lexp * result * result) list): string list = let str_induct = "Nat : Type; Nat = inductive_ (dNat) (zero) (succ Nat)" let str_int_3 = "i = 3" let str_int_4 = "i = 4" -let str_case = "i = case True -| True => 2 -| False => 42" +let str_case = "i = case true +| true => 2 +| false => 42" let str_case2 = "i = case nil(a := Int) | nil => 12 | _ => 24"
View it on GitLab: https://gitlab.com/monnier/typer/commit/65acc4ece8ebc41dac9d808263b87a52169c...