Stefan pushed to branch master at Stefan / Typer Commits: ae543b55 by Stefan Monnier at 2018-11-23T21:43:09Z * samples/hurkens.typer: New file. - - - - - 4 changed files: - btl/builtins.typer - + samples/hurkens.typer - src/builtin.ml - src/eval.ml Changes: ===================================== btl/builtins.typer ===================================== @@ -31,6 +31,9 @@ %%%% Base Types used in builtin functions +%% TypeLevel_succ = Built-in "TypeLevel.succ" : TypeLevel -> TypeLevel; +%% TypeLevel_⊔ = Built-in "TypeLevel.⊔" : TypeLevel -> TypeLevel -> TypeLevel; + %% The trivial type which carries no information. Unit = typecons Unit unit; unit = datacons Unit unit; @@ -423,10 +426,10 @@ Test_info = Built-in "Test.info" : String -> String -> IO Unit; %% Test_location = Built-in "Test.location" : Unit -> String; -%%% -%%% Do some test which print a message: "[ OK]" or "[FAIL]" -%%% followed by a message passed as argument -%%% +%% +%% Do some test which print a message: "[ OK]" or "[FAIL]" +%% followed by a message passed as argument +%% %% %% Takes a message and a boolean which should be true ===================================== samples/hurkens.typer ===================================== @@ -0,0 +1,71 @@ +%%% hurkens.typer --- Hurken's paradox + +%%% Commentary: + +%% @InProceedings{Hurkens95, +%% author = {Antonius Hurkens}, +%% title = {A simplification of {G}irard's paradox}, +%% crossref = {TLCA95}, +%% url = {http://www.cs.cmu.edu/~kw/scans/hurkens95tlca.pdf}, +%% pages = {266-278} +%% } + +%%% Code: + +⊥ : Type; +⊥ = (p : Type) ≡> p; + +¬ : Type -> Type; +¬ t = t -> ⊥; + +* = Type; +\square = Type1; + +%% p (S) = (S -> *); FIXME: internal error! +𝓅 : \square -> \square; +𝓅 (S : \square) = (S -> Type); +𝓅𝓅 S = 𝓅 (𝓅 S); + +U : \square; +U = (X : \square) ≡> (𝓅𝓅 X -> X) -> 𝓅𝓅 X; + +τ : 𝓅𝓅 U -> U; +τ t = lambda (X : \square) + ≡> lambda (f : (𝓅𝓅 X) -> X) + -> lambda (p : 𝓅 X) + -> t (lambda (y : U) -> p (f ((y (X := X) f)))); + +σ : U -> 𝓅𝓅 U; +σ (s : U) = (s (X := U) (lambda (t : 𝓅𝓅 U) -> τ t)); + +Δ : 𝓅 U; +Δ = lambda (y : U) -> ¬((p : 𝓅 U) ≡> σ y p -> p (τ (σ y))); + +Ω : U; +Ω = τ (lambda (p : 𝓅 U) -> ((y : U) ≡> σ y p -> p y)); + +boom1 : ((p : 𝓅 U) ≡> ((y : U) ≡> σ y p -> p y) -> p Ω) -> ⊥; +boom1 = lambda (v0 : (p : 𝓅 U) ≡> ((y : U) ≡> σ y p -> p y) -> p Ω) + -> v0 (p := Δ) + (lambda (y : U) ≡> + lambda (v2 : σ y Δ) -> + lambda (v3 : (p : 𝓅 U) ≡> σ y p -> p (τ (σ y))) + -> v3 (p := Δ) + v2 + (lambda (p : 𝓅 U) + ≡> v3 (p := lambda (y : U) -> p (τ (σ y))))) + (lambda (p : 𝓅 U) ≡> v0 (p := lambda (y : U) -> p (τ (σ y)))); + +boom2 : (p : 𝓅 U) ≡> ((y : U) ≡> σ y p -> p y) -> p Ω; +boom2 = lambda (p : 𝓅 U) + ≡> lambda (v1 : (y : U) ≡> σ y p -> p y) + -> v1 (y := Ω) + (lambda (y : U) ≡> v1 (y := τ (σ y))); + +%% FIXME: Defining `boom` as below inf-loops, which I believe is a bug +%% (call it an accidental feature)! +%%boom : ⊥; +%%boom = boom1 boom2; + + +%%% hurkens.typer ends here. ===================================== src/builtin.ml ===================================== @@ -152,7 +152,7 @@ let new_builtin_type name kind = let register_builtin_csts () = add_builtin_cst "TypeLevel" DB.type_level; - add_builtin_cst "TypeLevel.z" DB.level0; + add_builtin_cst "TypeLevel_z" DB.level0; add_builtin_cst "Type" DB.type0; add_builtin_cst "Type1" DB.type1; add_builtin_cst "Int" DB.type_int; ===================================== src/eval.ml ===================================== @@ -973,16 +973,27 @@ let test_neq loc depth args_val = match args_val with ttrue) | _ -> error loc "Test.neq takes a String and two values as argument" +let typelevel_succ loc (depth : eval_debug_info) (args_val: value_type list) = + match args_val with + | [Vint v] -> Vint(v + 1) + | _ -> error loc ("`Typlevel.succ` expects 1 TypeLevel argument") +let typelevel_lub loc (depth : eval_debug_info) (args_val: value_type list) = + match args_val with + | [Vint v1; Vint v2] -> Vint(max v1 v2) + | _ -> error loc ("`Typlevel.⊔` expects 2 TypeLevel argument2") + let register_builtin_functions () = List.iter (fun (name, f, arity) -> add_builtin_function name f arity) [ - ("Sexp.block" , make_block, 1); + ("Sexp.block" , make_block, 1); ("Sexp.symbol" , make_symbol, 1); ("Sexp.string" , make_string, 1); ("Sexp.integer" , make_integer, 1); ("Sexp.float" , make_float, 1); ("Sexp.node" , make_node, 2); ("Sexp.dispatch" , sexp_dispatch, 7); + ("TypeLevel.succ" , typelevel_succ, 1); + ("TypeLevel.⊔" , typelevel_lub, 2); ("Parser.default", parser_default,1); ("Parser.custom" , parser_custom,2); ("Parser.newest" , parser_newest,1); View it on GitLab: https://gitlab.com/monnier/typer/commit/ae543b55a78b4cf86c6b90d344eeb6ab268c... -- View it on GitLab: https://gitlab.com/monnier/typer/commit/ae543b55a78b4cf86c6b90d344eeb6ab268c... You're receiving this email because of your account on gitlab.com.