Stefan pushed to branch master at Stefan / Typer

Commits: e5fa8b6d by Stefan Monnier at 2016-08-27T10:35:44-04:00 Fix syntax of explicit-implicit args

* typer-mode.el (typer-smie-grammar): Fix grammar for `:=`. Add if/then/else to the grammar. Remove `:-` and `:≡`. * tests/sexp_test.ml: Add test for `:=` and if/then/else. * tests/eval_test.ml, tests/macro_test.ml: Use explicit implicit args. * src/grammar.ml (default_grammar): Update from type-mode.el. * doc/manual.texi (Core Syntax): Only keep `:=` for explicit args. * src/builtin.ml (get_attribute_impl, declexpr_impl) (is_builtin_macro): Silence compiler-warning. * btl/types.typer (length): Pass explicitly implicit parameter.

- - - - -

9 changed files:

- DESIGN - btl/types.typer - doc/manual.texi - src/builtin.ml - src/grammar.ml - tests/eval_test.ml - tests/macro_test.ml - tests/sexp_test.ml - typer-mode.el

Changes:

===================================== DESIGN ===================================== --- a/DESIGN +++ b/DESIGN @@ -99,7 +99,6 @@ or "implicit". This has 2 downsides: * Syntax

arw ::= '≡>' | '=>' | '->' -assign::= ':≡' | ':=' | ':-' colon ::= ':::' | '::' | ':' exp ::= '(' id ':' exp ')' arw exp | exp arw exp #Function Types | 'let' decls 'in' exp @@ -115,8 +114,8 @@ decl ::= id ':' exp simple_arg ::= id | '('id ':' exp')' formal_arg ::= id | '(' id colon exp ')' ind_arg ::= exp | '(' id colon exp ')' -pat_arg ::= id | '(' id assign pattern ')' -actual_arg ::= exp | '(' id assign exp ')' +pat_arg ::= id | '(' id ':=' pattern ')' +actual_arg ::= exp | '(' id ':=' exp ')'

An identifier which starts with a question mark is one meant to be generalized as an implicit/erasable argument. E.g. @@ -1434,7 +1433,13 @@ need to do anyway. Does it come with a cost? That depends on the universe-level of the equality type.

-*** E.g. if (=) is in Type 0: +We can encode equality in CoC: + + eq x y = ∀f. f x -> f y + eq_refl : ∀x. eq x x + eq_refl x f P = P + +*** E.g. if (x = y) is in Type 0:

type (=) (t:Type l) (a:t) : t -> Type 0 refl: a = a @@ -1461,7 +1466,7 @@ this should not affect typing very much since

so the level of T is not affected.

-*** E.g. if (=) is in Type l: +*** E.g. if (x = y) is in Type l:

type (=) (t:Type l) (a:t) : t -> Type l refl: a = a @@ -1506,6 +1511,21 @@ make sense for "erasable" terms. Also, by marking "large" elements of inductive definitions as erasable, we'd get something similar to preventing strong elimination for them.

+E.g. in cast-ultimate.v I had to use axioms like + + EQ_ex : Exists K1 TF1 = Exists K2 TF2 -> (∀F. F K1 TF1 = F K2 TF2) + +whose soundness is actually not known. +With impredicative erasable args we do not need an axiom de define: + + EQ_ex : Exists(K:≡K1) TF1 = Exists(K:≡K2) TF2 + -> (∀F. F(K:≡K1) TF1 = F(K:≡K2) TF2) + +Notice how F only takes an erasable version of K1 and K2, thus +imposing a constraint on the axiom which might indeed be sufficient to make +it sound. Hopefully it's also still sufficient for the cast-ultimate.v proof +to go through! + ** Universe level of equality

In current Coq, homogenous equality is: @@ -1553,6 +1573,31 @@ Which I guess is comparable to: type (~=) (t1:Type l) (a1:t1) (t2:Type l) (Q:t1 = t2) : t2 -> Type l refl: a1 ~= (coerce Q a1)

+*** "Natural" level via encoding + +Let's check the "natural" level of the "eq" encoding: + + eq = λ(l:Level) ≡> λ(T:Type l) ≡> λ(x:T) (y:T) -> + (l':Level) ≡> (T':Type l') ≡> (f:T -> T') -> f x -> f y + eq x y : Typeω + +Ouch! But if we consider that the level of inductive definitions is +normally unaffected by the level at which they're eliminated (contrary to +what happens for the kind of impredicative encoding used here) we could +treat it more like + + eq = λ(l:Level) ≡> λ(T:Type l) ≡> λ(x:T) (y:T) -> + (T':Type 0) ≡> (f:T -> T') -> f x -> f y + eq x y : Type l + +Which gives us the dreaded "Type (l+1)" if T is "Type l". +But if x and y are types, we should be able to cut the middle man: + + eq' = λ(l : Level) ≡> λ(x : Type l) (y : Type l) -> + (T':Type 0) ≡> (f : Type l -> T') -> f x -> f y + eq' x y : Type l + +but that doesn't seem to help.

** Inference

@@ -1698,23 +1743,11 @@ sacrificing normalization. ** http://albatross-lang.sourceforge.net ** Idris's Effects http://eb.host.cs.st-andrews.ac.uk/drafts/dep-eff.pdf ** Read +*** (Co)Iteration for higher-order nested datatypes, Andreas Abel and Ralph Matthes, [Abel03] *** Inductive Families Need Not Store Their Indices, Edwin Brady, Conor McBride and James McKinna. http://www.cs.st-andrews.ac.uk/~eb/writings/types2003.pdf *** A Simplified Suspension Calculus and its Relationship to Other Explicit Substitution Calculi, Andrew Gacek and Gopalan Nadathur *** How OCaml type checker works, http://okmij.org/ftp/ML/generalization.html -* Skip lists - -SkipList a - | Empty - | Cons (val : a) (next : SkipList a) (skip : Nat) (dest : SkipList a) - -At position 2^n, we want skip=2^(n-1) -At position 2^n+2^(n-1) we want two contradictory things: -- skip=2^(n-1) to get to the pivotal 2^n (for when we start before - 2^n+2^(n-1) and need to go past 2^n). -- skip=2^(n-2) to do the binary search between 2^n+2^(n-1) and 2^n (for when - we don't want to go past 2^n, e.g. because we started from before - 2^(n+1)). * Related languages ** Idris ** F-star (https://www.fstar-lang.org)

===================================== btl/types.typer ===================================== --- a/btl/types.typer +++ b/btl/types.typer @@ -138,6 +138,12 @@ FileHandle = Built-in "FileHandle";

% define operation on file handle run-io = Built-in "run-io" ( + %% FIXME: runIO should have type IO Unit -> b -> b + %% or IO a -> b -> b, which means "run the IO, throw away the result, + %% and then return the second argument unchanged". The "dummy" b argument + %% 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! (a : Type) ≡> (b : Type) ≡> IO a -> (a -> IO b) -> (IO b) -> Unit); @@ -163,6 +169,7 @@ has-attribute = Built-in "has-attribute" (Macro); % Context Accessors % -----------------------------------------------------

+%% FIXME: These should be functions! decltype = Built-in "decltype" Macro; declexpr = Built-in "declexpr" Macro;

===================================== doc/manual.texi ===================================== --- a/doc/manual.texi +++ b/doc/manual.texi @@ -119,7 +119,6 @@ The core syntax of the language is as follows:

@example arw ::= '≡>' | '=>' | '->' -assign::= ':≡' | ':=' | ':-' colon ::= ':::' | '::' | ':' exp ::= id | '(' id ':' exp ')' arw exp @@ -137,12 +136,12 @@ decl ::= id ':' exp simple_arg ::= id | '(' id ':' exp ')' formal_arg ::= id | '(' id colon exp ')' ind_arg ::= exp | '(' id colon exp ')' -pat_arg ::= id | '(' id assign id ' )' -actual_arg ::= exp | '(' id assign exp ')' +pat_arg ::= id | '(' id ':=' id ' )' +actual_arg ::= exp | '(' id ':=' exp ')' label ::= id @end example

-The three different kinds of arrows, assign symbols and colons are +The three different kinds of arrows and colons are used respectively for @emph{erasable} arguments, @emph{implicit} arguments, and @emph{explicit} arguments. @emph{explicit} arguments are the normal kind of arguments we're all familiar with.

===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -347,8 +347,11 @@ let decltype_impl loc largs ctx ftype = ltype, type0

let builtin_macro = [ + (* FIXME: These should be functions! *) ("decltype", decltype_impl); ("declexpr", declexpr_impl); + (* FIXME: These are not macros but `special-forms`. + * We should add here `let_in_`, `case_`, etc... *) ("get-attribute", get_attribute_impl); ("new-attribute", new_attribute_impl); ("has-attribute", has_attribute_impl); @@ -366,7 +369,7 @@ let get_macro_impl loc name = with Not_found -> builtin_error loc ("Builtin macro" ^ name ^ " not found")

let is_builtin_macro name = - try SMap.find name macro_impl_map; true + try let _ = SMap.find name macro_impl_map in true with Not_found -> false

===================================== src/grammar.ml ===================================== --- a/src/grammar.ml +++ b/src/grammar.ml @@ -66,37 +66,38 @@ let default_stt : token_env = let default_grammar : grammar = List.fold_left (fun g (n, ll, rl) -> SMap.add n (ll, rl) g) SMap.empty - [("^", Some 165, Some 152); - ("/", Some 140, Some 153); - ("*", Some 141, Some 154); - ("-", Some 109, Some 128); - ("+", Some 110, Some 129); - ("!=", Some 111, Some 89); - (">=", Some 112, Some 90); - ("<=", Some 113, Some 91); - (">", Some 114, Some 92); - ("<", Some 115, Some 93); - ("==", Some 116, Some 94); - ("&&", Some 77, Some 95); + [("^", Some 166, Some 153); + ("/", Some 141, Some 154); + ("*", Some 142, Some 155); + ("-", Some 110, Some 129); + ("+", Some 111, Some 130); + ("!=", Some 112, Some 90); + (">=", Some 113, Some 91); + ("<=", Some 114, Some 92); + (">", Some 115, Some 93); + ("<", Some 116, Some 94); + ("==", Some 117, Some 95); + ("&&", Some 78, Some 96); ("||", Some 53, Some 65); (",", Some 41, Some 41); - (":≡", Some 166, Some 0); - (":-", Some 167, Some 1); - (":=", Some 168, Some 2); - ("::", Some 169, Some 17); - (":::", Some 170, Some 16); - (";", Some 15, Some 15); + ("::", Some 167, Some 17); + (":::", Some 168, Some 16); + ("then", Some 2, Some 1); + (";", Some 14, Some 14); ("type", None, Some 30); ("=", Some 28, Some 29); - ("in", Some 4, Some 66); + (":=", Some 170, Some 15); + ("in", Some 3, Some 67); + ("else", Some 1, Some 66); ("|", Some 54, Some 54); - (")", Some 3, None); - ("->", Some 117, Some 98); - ("=>", Some 117, Some 97); - ("≡>", Some 117, Some 96); - ("let", None, Some 4); - (":", Some 78, Some 78); - ("lambda", None, Some 117); + (")", Some 0, None); + ("->", Some 118, Some 99); + ("=>", Some 118, Some 98); + ("≡>", Some 118, Some 97); + ("let", None, Some 3); + (":", Some 79, Some 79); + ("lambda", None, Some 118); ("case", None, Some 42); - ("(", None, Some 3) + ("if", None, Some 2); + ("(", None, Some 0) ]

===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -350,14 +350,14 @@ let _ = (add_test "EVAL" "List" (fun () -> reset_eval_trace ();

let dcode = " - my_list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + my_list = (cons(a := Int) 1 (cons(a := Int) 2 (cons(a := Int) 3 (cons(a := Int) 4 (nil(a := Int)))))); " in

let rctx, lctx = eval_decl_str dcode lctx rctx in

- let rcode = "(length Int my_list); - (head Int my_list); - (head Int (tail Int my_list));" in + let rcode = "(length(a := Int) my_list); + (head(a := Int) my_list); + (head(a := Int) (tail(a := Int) my_list));" in

(* Eval defined lambda *) let ret = eval_expr_str rcode lctx rctx in

===================================== tests/macro_test.ml ===================================== --- a/tests/macro_test.ml +++ b/tests/macro_test.ml @@ -48,8 +48,8 @@ let _ = (add_test "MACROS" "macros base" (fun () -> (* define 'lambda x -> x * x' using macros *) let dcode = " my_fun = lambda (x : List Sexp) -> - let hd = head Sexp x in - (node_ (symbol_ "_*_") (cons hd (cons hd nil))); + let hd = head(a := Sexp) x in + (node_ (symbol_ "_*_") (cons(a := Sexp) hd (cons(a := Sexp) hd (nil(a := Sexp)))));

sqr = Macro_ my_fun; " in @@ -71,10 +71,10 @@ let _ = (add_test "MACROS" "macros decls" (fun () ->

let dcode = " decls-impl = lambda (x : List Sexp) -> - cons (node_ (symbol_ "_=_") - (cons (symbol_ "a") (cons (integer_ 1) nil))) - (cons (node_ (symbol_ "_=_") - (cons (symbol_ "b") (cons (integer_ 2) nil))) nil); + cons(a := Sexp) (node_ (symbol_ "_=_") + (cons(a := Sexp) (symbol_ "a") (cons(a := Sexp) (integer_ 1) (nil(a := Sexp))))) + (cons(a := Sexp) (node_ (symbol_ "_=_") + (cons(a := Sexp) (symbol_ "b") (cons(a := Sexp) (integer_ 2) (nil(a := Sexp))))) (nil(a := Sexp)));

my-decls = Macro_ decls-impl;

===================================== tests/sexp_test.ml ===================================== --- a/tests/sexp_test.ml +++ b/tests/sexp_test.ml @@ -36,6 +36,9 @@ let test_sexp_eqv dcode1 dcode2 =

let _ = test_sexp_eqv "((a) ((1.00)))" "a 1.0" let _ = test_sexp_eqv "(x + y)" "_+_ x y" +let _ = test_sexp_eqv "(x := y)" "_:=_ x y" +let _ = test_sexp_eqv "if A then B else C -> D" "if A then B else (C -> D)" +let _ = test_sexp_eqv "A : B -> C" "A : (B -> C)" let _ = test_sexp_eqv "f __; y" "(f ( __; ) y)" let _ = test_sexp_eqv "case e | p1 => e1 | p2 => e2" "case_ ( _|_ e ( _=>_ p1 e1) ( _=>_ p2 e2))"

===================================== typer-mode.el ===================================== --- a/typer-mode.el +++ b/typer-mode.el @@ -86,7 +86,7 @@ (smie-merge-prec2s (smie-bnf->prec2 '((id) - (exp ("(" exp ")") + (exp ("(" exp ")") ("(" explicit-arg ")") (exp "->" exp) (exp "=>" exp) (exp "≡>" exp) ("let" decls "in" exp) (exp ":" exp) @@ -96,7 +96,7 @@ ("lambda" simple_arg "≡>" exp) ("case" exp-branches) ;; ("letrec" decl "in" exp) - ;; ("if" exp "then" exp "else" exp) + ("if" exp "then" exp "else" exp) ) (simple_arg (id) ("(" typed_arg ")")) (typed_arg (id ":" exp)) @@ -106,7 +106,8 @@ (decls (decls ";" decls) (decl)) (decl (id ":" exp) (exp "=" exp) ("type" inductive_branches)) (inductive_branches (exp) (inductive_branches "|" inductive_branches)) - (explicit-arg (id ":=" exp) (id ":-" exp) (id ":≡" exp)) + (explicit-arg (id ":=" exp) ;; (id ":-" exp) (id ":≡" exp) + ) (exp-branches (exp "|" branches)) (branches (branches "|" branches) (pattern "=>" exp))) '((assoc ";") @@ -127,6 +128,11 @@ (assoc ":") ;Should this be left or right? (right "->" "=>" "≡>") ) + ;; There's also ambiguity with "else": should "...A else B => C" + ;; mean "(...A else B) => C" or "...A else (B => C)". + ;; I think it should be "...A else (B => C)". + '((nonassoc "else") + (nonassoc ":" "=>" "->" "≡>")) ) ;; Precedence of "=" is tricky as well. Cases to consider: ;; - "x : e1 = e2"

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