Stefan pushed to branch master at Stefan / Typer

Commits: 1e29f31a by Stefan Monnier at 2017-12-01T12:47:12-05:00 Provide type of Built-in via context, it's more flexible

* src/elab.ml (sform_built_in): Change to take the type from `ot` rather than from an argument.

* btl/builtins.typer: Adjust and simplify accordingly.

* src/builtin.ml (predef_names): Rename from `predef_name`.

- - - - -

5 changed files:

- btl/builtins.typer - src/builtin.ml - src/elab.ml - src/opslexp.ml - tests/eval_test.ml

Changes:

===================================== btl/builtins.typer ===================================== --- a/btl/builtins.typer +++ b/btl/builtins.typer @@ -41,15 +41,16 @@ Void = typecons 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_refl : ((x : ?t) ≡> Eq x x); % FIXME: `Eq ?x ?x` causes an error! +Eq_refl = Built-in "Eq.refl";

-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); +Eq_cast : (x : ?) ≡> (y : ?) + ≡> (p : Eq x y) + ≡> (l : TypeLevel) ≡> (f : ? -> Type_ l) + ≡> f x -> f y; +%% FIXME: I'd like to just say: +%% Eq_cast : (p : Eq ?x ?y) ≡> ?f ?x -> ?f ?y; +Eq_cast = Built-in "Eq.cast";

%% Commutativity of equality! %% FIXME: I'd like to just say: @@ -64,20 +65,20 @@ Eq_comm p = Eq_cast (f := lambda xy -> Eq (t := t) xy x) %% Whether this breaks consistency or not is a good question. %% The basic idea is the following: %% -%% The `witness` argument presumably makes sure that "Y f" can only +%% The `witness` argument presumably makes sure that `Y f` can only %% create new recursive values for types which were already inhabited. %% So there's no `f` such that `Y f : False`. %% %% But this is not sufficient, because you could use `Y` to create %% new recursive *types* which then let you construct new arbitrary %% recursive values of previously uninhabited types. -%% E.g. you could create Y <something> = ((... → t) -> t) -> t -%% and then give the term "λx. x x" inhabiting that type, and from that +%% E.g. you could create `Y <something> = ((... → t) -> t) -> t` +%% and then give the term `λx. x x` inhabiting that type, and from that %% get a proof of False. %% %% So we have a secondary restriction: This `Y` is a builtin primitive/axiom -%% with no reduction rule, so that Y <something> is never convertible -%% to something like ((... → t) -> t) -> t +%% with no reduction rule, so that `Y <something>` is never convertible +%% to something like `((... → t) -> t) -> t` %% %% Of course, we do have a "natural" evaluation rule for it, so after type %% checking we can run our recursive functions just fine, but those @@ -85,45 +86,45 @@ Eq_comm p = Eq_cast (f := lambda xy -> Eq (t := t) xy x) %% %% FIXME: Really, this Y should be used internally/transparently for any %% function which has not been termination-checked successfully (or at all). -Y = Built-in "Y" ((a : Type) ≡> (b : Type) ≡> (witness : a -> b) ≡> - ((a -> b) -> (a -> b)) -> (a -> b)); +Y : (witness : ?a -> ?b) ≡> ((?a -> ?b) -> (?a -> ?b)) -> (?a -> ?b); +Y = Built-in "Y";

Bool = typecons (Bool) (true) (false); true = datacons Bool true; false = datacons Bool false;

%% 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); - -Int_< = Built-in "Int.<" (Int -> Int -> Bool); -Int_> = Built-in "Int.>" (Int -> Int -> Bool); -Int_eq = Built-in "Int.=" (Int -> Int -> Bool); -Int_<= = Built-in "Int.<=" (Int -> Int -> Bool); -Int_>= = Built-in "Int.>=" (Int -> Int -> Bool); -Int->Integer = Built-in "Int->Integer" (Int -> Integer); - -Integer_+ = Built-in "Integer.+" (Integer -> Integer -> Integer); -Integer_- = Built-in "Integer.-" (Integer -> Integer -> Integer); -Integer_* = Built-in "Integer.*" (Integer -> Integer -> Integer); -Integer_/ = Built-in "Integer./" (Integer -> Integer -> Integer); - -Integer_< = Built-in "Integer.<" (Integer -> Integer -> Bool); -Integer_> = Built-in "Integer.>" (Integer -> Integer -> Bool); -Integer_eq = Built-in "Integer.=" (Integer -> Integer -> Bool); -Integer_<= = Built-in "Integer.<=" (Integer -> Integer -> Bool); -Integer_>= = Built-in "Integer.>=" (Integer -> Integer -> Bool); - -Float_+ = Built-in "Float.+" (Float -> Float -> Float); -Float_- = Built-in "Float.-" (Float -> Float -> Float); -Float_* = Built-in "Float.*" (Float -> Float -> Float); -Float_/ = Built-in "Float./" (Float -> Float -> Float); -Float->String = Built-in "Float->String" (Float -> String); - -String_eq = Built-in "String.=" (String -> String -> Bool); -Sexp_eq = Built-in "Sexp.=" (Sexp -> Sexp -> Bool); +_+_ = Built-in "Int.+" : Int -> Int -> Int; +_-_ = Built-in "Int.-" : Int -> Int -> Int; +_*_ = Built-in "Int.*" : Int -> Int -> Int; +_/_ = Built-in "Int./" : Int -> Int -> Int; + +Int_< = Built-in "Int.<" : Int -> Int -> Bool; +Int_> = Built-in "Int.>" : Int -> Int -> Bool; +Int_eq = Built-in "Int.=" : Int -> Int -> Bool; +Int_<= = Built-in "Int.<=" : Int -> Int -> Bool; +Int_>= = Built-in "Int.>=" : Int -> Int -> Bool; +Int->Integer = Built-in "Int->Integer" : Int -> Integer; + +Integer_+ = Built-in "Integer.+" : Integer -> Integer -> Integer; +Integer_- = Built-in "Integer.-" : Integer -> Integer -> Integer; +Integer_* = Built-in "Integer.*" : Integer -> Integer -> Integer; +Integer_/ = Built-in "Integer./" : Integer -> Integer -> Integer; + +Integer_< = Built-in "Integer.<" : Integer -> Integer -> Bool; +Integer_> = Built-in "Integer.>" : Integer -> Integer -> Bool; +Integer_eq = Built-in "Integer.=" : Integer -> Integer -> Bool; +Integer_<= = Built-in "Integer.<=" : Integer -> Integer -> Bool; +Integer_>= = Built-in "Integer.>=" : Integer -> Integer -> Bool; + +Float_+ = Built-in "Float.+" : Float -> Float -> Float; +Float_- = Built-in "Float.-" : Float -> Float -> Float; +Float_* = Built-in "Float.*" : Float -> Float -> Float; +Float_/ = Built-in "Float./" : Float -> Float -> Float; +Float->String = Built-in "Float->String" : Float -> String; + +String_eq = Built-in "String.=" : String -> String -> Bool; +Sexp_eq = Built-in "Sexp.=" : Sexp -> Sexp -> Bool;

%% ----------------------------------------------------- %% List @@ -140,12 +141,12 @@ cons = datacons List cons;

%%%% Macro-related definitions

-%% Sexp_block= Built-in "Sexp.block" (List Pretoken -> Sexp); -Sexp_symbol = Built-in "Sexp.symbol" (String -> Sexp); -Sexp_string = Built-in "Sexp.string" (String -> Sexp); -Sexp_node = Built-in "Sexp.node" (Sexp -> List Sexp -> Sexp); -Sexp_integer = Built-in "Sexp.integer" (Integer -> Sexp); -Sexp_float = Built-in "Sexp.float" (Float -> Sexp); +%% Sexp_block= Built-in "Sexp.block" : List Pretoken -> Sexp; +Sexp_symbol = Built-in "Sexp.symbol" : String -> Sexp; +Sexp_string = Built-in "Sexp.string" : String -> Sexp; +Sexp_node = Built-in "Sexp.node" : Sexp -> List Sexp -> Sexp; +Sexp_integer = Built-in "Sexp.integer" : Integer -> Sexp; +Sexp_float = Built-in "Sexp.float" : Float -> Sexp;

Macro = typecons (Macro) (macro (List Sexp -> Sexp)); @@ -155,27 +156,26 @@ Macro_expand : Macro -> List Sexp -> Sexp; Macro_expand = lambda m -> lambda args -> case m | macro f => f args;

-Sexp_dispatch = Built-in "Sexp.dispatch" ( - (a : Type) ≡> - Sexp - -> (node : Sexp -> List Sexp -> a) - -> (symbol : String -> a) - -> (string : String -> a) - -> (int : Integer -> a) - -> (float : Float -> a) - -> (block : List Sexp -> a) - -> a - ); +Sexp_dispatch = Built-in "Sexp.dispatch" + : (a : Type) ≡> + Sexp + -> (node : Sexp -> List Sexp -> a) + -> (symbol : String -> a) + -> (string : String -> a) + -> (int : Integer -> a) + -> (float : Float -> a) + -> (block : List Sexp -> a) + -> a ;

%%%% Monads

%% Builtin bind -IO_bind = Built-in "IO.bind" ( - (a : Type) ≡> - (b : Type) ≡> - IO a -> (a -> IO b) -> (IO b)); +IO_bind = Built-in "IO.bind" + : (a : Type) ≡> + (b : Type) ≡> + IO a -> (a -> IO b) -> (IO b);

-IO_return = Built-in "IO.return" ((a : Type) ≡> a -> IO a); +IO_return = Built-in "IO.return" : (a : Type) ≡> a -> IO a;

%% `runIO` should have type IO Unit -> b -> b %% or IO a -> b -> b, which means "run the IO, throw away the result, @@ -183,17 +183,17 @@ IO_return = Built-in "IO.return" ((a : Type) ≡> a -> IO a); %% is actually crucial to make sure the result of runIO is used, otherwise %% the whole call would look like a dead function call and could be %% optimized away! -IO_run = Built-in "IO.run" ((a : Type) ≡> IO Unit -> a -> a); +IO_run = Built-in "IO.run" : (a : Type) ≡> IO Unit -> a -> a;

%% File monad

%% Define operations on file handle. -File_open = Built-in "File.open" (String -> String -> IO FileHandle); -File_stdout = Built-in "File.stdout" (Unit -> FileHandle); -File_write = Built-in "File.write" (FileHandle -> String -> IO Unit); -File_read = Built-in "File.read" (FileHandle -> Int -> IO String); +File_open = Built-in "File.open" : String -> String -> IO FileHandle; +File_stdout = Built-in "File.stdout" : Unit -> FileHandle; +File_write = Built-in "File.write" : FileHandle -> String -> IO Unit; +File_read = Built-in "File.read" : FileHandle -> Int -> IO String;

-Sys_cpu_time = Built-in "Sys.cpu_time" (Unit -> IO Float); -Sys_exit = Built-in "Sys.exit" (Int -> IO Unit); +Sys_cpu_time = Built-in "Sys.cpu_time" : Unit -> IO Float; +Sys_exit = Built-in "Sys.exit" : Int -> IO Unit;

%%% builtins.typer ends here.

===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -67,9 +67,9 @@ 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

-let predef_name = [ - "cons"; - "nil"; +let predef_names = [ + "cons"; (* FIXME: Should be used but isn't! *) + "nil"; (* FIXME: Should be used but isn't! *) "true"; "false"; "Macro"; @@ -83,7 +83,7 @@ let predef_map : lexp SMap.t ref * the builtins.typer file. *) = ref (SMap.add "Macro" impossible SMap.empty)

-let get_predef (name: string) (ctx: DB.elab_context) = +let get_predef (name: string) (ctx: DB.elab_context) : lexp = try let r = (DB.get_size ctx) - !builtin_size - 0 in let p = SMap.find name (!predef_map) in mkSusp p (S.shift r) @@ -125,6 +125,8 @@ let o2v_list lst =

(* Typer list to Ocaml list *) let v2o_list v = + (* FIXME: We're not using predef here. This will break if we change + * the definition of `List` in builtins.typer. *) let rec v2o_list acc v = match v with | E.Vcons ((_, "cons"), [hd; tl]) -> v2o_list (hd::acc) tl

===================================== src/elab.ml ===================================== --- a/src/elab.ml +++ b/src/elab.ml @@ -1187,14 +1187,17 @@ let builtin_value_types : ltype option SMap.t ref = ref SMap.empty

let sform_built_in ctx loc sargs ot = match !_parsing_internals, sargs with - | true, [String (_, name); stp] - -> let ltp = infer_type stp ctx None in - let ltp' = OL.lexp_close (ectx_to_lctx ctx) ltp in - let bi = mkBuiltin ((loc, name), ltp', None) in - if not (SMap.mem name (!EV.builtin_functions)) then - sexp_error loc ("Unknown built-in `" ^ name ^ "`"); - BI.add_builtin_cst name bi; - (bi, Inferred ltp') + | true, [String (_, name)] + -> (match ot with + | Some ltp + -> let ltp' = OL.lexp_close (ectx_to_lctx ctx) ltp in + let bi = mkBuiltin ((loc, name), ltp', None) in + if not (SMap.mem name (!EV.builtin_functions)) then + sexp_error loc ("Unknown built-in `" ^ name ^ "`"); + BI.add_builtin_cst name bi; + (bi, Checked) + | None -> error loc "Built-in's type not provided by context!"; + sform_dummy_ret ctx loc)

| true, _ -> error loc "Wrong Usage of `Built-in`"; sform_dummy_ret ctx loc @@ -1549,7 +1552,7 @@ let default_ectx try List.iter (fun name -> let idx = senv_lookup name elctx in let v = Var((dloc, name), idx) in - BI.set_predef name v) BI.predef_name; + BI.set_predef name v) BI.predef_names; with e -> warning dloc "Predef not found"; in

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -915,3 +915,5 @@ and clean_map cases = SMap.map (fun (l, args, expr) -> (l, (clean_arg_list args), (erase_type expr))) cases + +(* opslexp.ml ends here. *)

===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -357,9 +357,9 @@ let _ = test_eval_eqv_named let _ = test_eval_eqv_named "Equalities"

- "f : (α : Type) ≡> (p : Eq (t := Type) Int α) -> Int -> α; + "f : (α : Type) ≡> (p : Eq Int α) -> Int -> α; f = lambda α ≡> lambda p x -> - Eq_cast (t := Type) (x := Int) (y := α) (f := (lambda v -> v)) (p := p) x" + Eq_cast (f := lambda v -> v) (p := p) x"

"f Eq_refl 3" "3"

View it on GitLab: https://gitlab.com/monnier/typer/commit/1e29f31a392bce22568c929a38c4a41b6244...

--- View it on GitLab: https://gitlab.com/monnier/typer/commit/1e29f31a392bce22568c929a38c4a41b6244... You're receiving this email because of your account on gitlab.com.