Stefan pushed to branch master at Stefan / Typer
Commits: 411ba805 by Stefan Monnier at 2016-12-02T11:23:22-05:00 Add Eq type
* btl/builtins.typer (Eq_refl, Eq_cast, Eq_comm): New definitions.
* src/builtin.ml (type_eq): Fix level of return value. (register_builtin_types): Add "Eq".
* src/eval.ml (arity0_fun, nop_fun): New functions. (register_built_functions): Use them for Eq.refl, Eq.cast.
* tests/eval_test.ml ("Equalities"): New test.
- - - - -
4 changed files:
- btl/builtins.typer - src/builtin.ml - src/eval.ml - tests/eval_test.ml
Changes:
===================================== btl/builtins.typer ===================================== --- a/btl/builtins.typer +++ b/btl/builtins.typer @@ -42,6 +42,27 @@ unit = datacons Unit unit; % The empty type, with no constructors: nothing can have this type. Void = inductive_ Void;
+% Eq : (l : TypeLevel) ≡> (t : Type_ l) ≡> t -> t -> Type_ l +% Eq' : (l : TypeLevel) ≡> Type_ l -> Type_ l -> Type_ l +Eq_refl = Built-in "Eq.refl" + ((l : TypeLevel) ≡> (t : Type_ l) ≡> (x : t) + ≡> Eq (t := t) x x); + +Eq_cast = Built-in "Eq.cast" + ((l1 : TypeLevel) ≡> (t : Type_ l1) ≡> (x : t) ≡> (y : t) + ≡> (p : Eq (t := t) x y) + ≡> (l2 : TypeLevel) ≡> (f : t -> Type_ l2) + ≡> f x -> f y); + +%% Commutativity of equality! +Eq_comm : (l : TypeLevel) ≡> (t : Type_ l) ≡> (x : t) ≡> (y : t) + ≡> (p : Eq (t := t) x y) -> Eq (t := t) y x; +Eq_comm = lambda l t x y ≡> lambda p -> + Eq_cast (f := lambda xy -> Eq (t := t) xy x) + (p := p) + %% FIXME: Removing (l := l) gives bogus error! + (Eq_refl (l := l) (t := t) (x := x)); + % Basic operators _+_ = Built-in "Int.+" (Int -> Int -> Int); _-_ = Built-in "Int.-" (Int -> Int -> Int);
===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -99,17 +99,18 @@ let dloc = DB.dloc let op_binary t = mkArrow (Aexplicit, None, t, dloc, mkArrow (Aexplicit, None, t, dloc, t))
-let type_eq = let lv = (dloc, "l") in - let tv = (dloc, "t") in - mkArrow (Aerasable, Some lv, - DB.type_level, dloc, - mkArrow (Aerasable, Some tv, - mkSort (dloc, Stype (Var (lv, 0))), dloc, - mkArrow (Aexplicit, None, Var (tv, 0), dloc, - mkArrow (Aexplicit, None, - mkVar (tv, 1), dloc, - DB.type0)))) - +let type_eq = + let lv = (dloc, "l") in + let tv = (dloc, "t") in + mkArrow (Aerasable, Some lv, + DB.type_level, dloc, + mkArrow (Aerasable, Some tv, + mkSort (dloc, Stype (Var (lv, 0))), dloc, + mkArrow (Aexplicit, None, + Var (tv, 0), dloc, + mkArrow (Aexplicit, None, + mkVar (tv, 1), dloc, + mkSort (dloc, Stype (Var (lv, 3)))))))
let o2l_bool ctx b = get_predef (if b then "true" else "false") ctx
@@ -158,7 +159,7 @@ let new_builtin_type name kind = add_builtin_cst name t; t
-let builtins = +let register_builtin_csts () = add_builtin_cst "TypeLevel" DB.type_level; add_builtin_cst "TypeLevel.z" DB.level0; add_builtin_cst "Type" DB.type0; @@ -167,7 +168,13 @@ let builtins = add_builtin_cst "Float" DB.type_float; add_builtin_cst "String" DB.type_string
-let _ = new_builtin_type "Sexp" DB.type0 -let _ = new_builtin_type - "IO" (mkArrow (Aexplicit, None, DB.type0, dloc, DB.type0)) -let _ = new_builtin_type "FileHandle" DB.type0 +let register_builtin_types () = + let _ = new_builtin_type "Sexp" DB.type0 in + let _ = new_builtin_type + "IO" (mkArrow (Aexplicit, None, DB.type0, dloc, DB.type0)) in + let _ = new_builtin_type "FileHandle" DB.type0 in + let _ = new_builtin_type "Eq" type_eq in + () + +let _ = register_builtin_csts (); + register_builtin_types ()
===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -545,24 +545,33 @@ and print_eval_trace trace = let (a, b) = !_global_eval_trace in print_trace " EVAL TRACE " trace a
-let _ = List.iter (fun (name, f, arity) -> add_builtin_function name f arity) - [ - ("block_" , make_block, 1); - ("symbol_" , make_symbol, 1); - ("string_" , make_string, 1); - ("integer_" , make_integer, 1); - ("float_" , make_float, 1); - ("node_" , make_node, 2); - ("sexp_dispatch_", sexp_dispatch, 7); - ("string_eq" , string_eq, 2); - ("int_eq" , int_eq, 2); - ("sexp_eq" , sexp_eq, 2); - ("open" , open_impl, 2); - ("bind" , bind_impl, 2); - ("run-io" , run_io, 2); - ("read" , read_impl, 2); - ("write" , write_impl, 2); - ] +let arity0_fun loc _ _ = error loc "Called a 0-arity function!?" +let nop_fun loc _ vs = match vs with + | [v] -> v + | _ -> error loc "Wrong number of argument to nop" + +let register_built_functions () = + List.iter (fun (name, f, arity) -> add_builtin_function name f arity) + [ + ("block_" , make_block, 1); + ("symbol_" , make_symbol, 1); + ("string_" , make_string, 1); + ("integer_" , make_integer, 1); + ("float_" , make_float, 1); + ("node_" , make_node, 2); + ("sexp_dispatch_", sexp_dispatch, 7); + ("string_eq" , string_eq, 2); + ("int_eq" , int_eq, 2); + ("sexp_eq" , sexp_eq, 2); + ("open" , open_impl, 2); + ("bind" , bind_impl, 2); + ("run-io" , run_io, 2); + ("read" , read_impl, 2); + ("write" , write_impl, 2); + ("Eq.refl" , arity0_fun, 0); + ("Eq.cast" , nop_fun, 1); + ] +let _ = register_built_functions ()
let eval lxp ctx = _eval lxp ctx ([], [])
===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -355,6 +355,17 @@ let _ = test_eval_eqv_named
"3; 3"
+let _ = test_eval_eqv_named + "Equalities" + + "f : (α : Type) ≡> (p : Eq (t := Type) Int α) -> Int -> α; + f = lambda α ≡> lambda p x -> + Eq_cast (t := Type) (x := Int) (y := α) (f := (lambda v -> v)) (p := p) x" + + (* FIXME: If I remove the (l := ?) I get + * Explicit actual args `t, x` have no matching formal args *) + "f (Eq_refl (l := ?) (t := Type) (x := Int)) 3" + "3"
(* run all tests *) let _ = run_all ()
View it on GitLab: https://gitlab.com/monnier/typer/commit/411ba805c142bbc2407df977c4e5ea57468b...