Mars 2017 - Typer - mailman.iro.umontreal.ca

Datatypes and tuples
by Stefan Monnier 03 Oct '18

03 Oct '18

Hi guys, Wondering if you might have an idea: In Typer, the basic datastructure is the "algebraic datatype" (which combines a sum, product, and recursion), and the basic eliminator is the "pattern matching case". It works OK, but is unsatisfactory: 1- both of those are fairly large/complex. 2- it means that extracting a record field is a "case" operation that discards all but the required field, so it's an O(n) operation (where n is the size of the record), if not in the final code, at least in intermediate code. 3- it means the choice of representation of datatype tags is hardcoded in the blackbox compiler. While point n°2 might seem irrelevant, it is a pain with large records, such as those you might get when records are used to represent modules: the encoding of the simple "String.concat" reference ends up taking space proportional to the number of primitives exported from the "String" module, which can be rather large. I'd like to find another option and was thinking of something along the following lines: - provide a separate product primitive. - provide a "union" type, i.e. an *untagged* sum. - provide primitive discrimination operations, such as "dispatch on an Int". then the Either type could look like Either a b = union (Singleton(1), a) (Singleton(2), b) and case e | Left x => ... | Right y => ... would turn into switch (e.0 <withmagicproof>) | 1 => let e' = cast (Singleton(1), a) e; x = e'.1 in ... | 2 => let e' = cast (Singleton(2), b) e; y = e'.1 in ... Obviously, we'd still want to have "case", but written as a macro. The `magicproof` is needed to convince Typer that all union members have a field 0. And of course, each `cast` would also need to provide a proof (constructed from a proof provided by `switch`) that indeed we know that `e` is this specific member of the union. The way I presented it is fairly general, but pretty heavyweight to define and to use: every "case" will be compiled to that big switch-with-proofs and the definition of a "record selection out of a union" (such as the "e.0 <withmagicproof>") seems fairly complex as well. Does anyone here have another approach to suggest? Stefan

5 7

[Git][monnier/typer][master] * doc/primer.md: First cut at some user doc
by Stefan 16 Mar '17

16 Mar '17

Stefan pushed to branch master at Stefan / Typer Commits: 0851032e by Stefan Monnier at 2017-03-16T11:34:54-04:00 * doc/primer.md: First cut at some user doc - - - - - 1 changed file: - + doc/primer.md Changes: ===================================== doc/primer.md ===================================== --- /dev/null +++ b/doc/primer.md @@ -0,0 +1,208 @@ +# Typer Primer + +## Basic functional programming + +Typer at its core is a fairly standard statically typed functional +programming language, and shares a lot with languages like Haskell, OCaml, +SML, ... + +### Simple definitions + +A file is composed of a sequence of declarations, which are mostly made of +definitions. For example, you can define a new variable with `<var> = <exp>`: + + x = 4; + +Note that the `;` does not *terminate* declarations but *separates* them so +it's not needed at the very end of a sequence of declarations. + +You can also declare the type of a variable type before giving its definition: + + y : Int; + y = 5; + +### Function definitions + +You can define functions with the syntax `f <args> = <exp>`: + + sub x y = x - y; + +A function call like `sub 47 5` will then return `42`. + +You can also use anonymous functions with the expression +`lambda <args> -> <exp>`, so the above definition is syntactic sugar for: + + sub = lambda x y -> x - y; + +There is hence a single namespace for functions and other variables. +Functions are curried, so you can use `sub 0` as a function of one +argument which returns its negative. + +The type of `sub` above could be written as: + + sub : Int -> Int -> Int; + +but you can also give names to the arguments in the type signature: + + sub : (x : Int) -> (y : Int) -> Int + +### Type definitions + +You can define a new algebraic datatype with +`type <name> | <cons1> <args1> | ...`. For example the types of pairs and +booleans can be defined as: + + type Bool + | true + | false; + type Pair a b + | pair a b; + +after which you can construct a pair for example with `pair 5 6`: +constructors are invoked like functions, and are curried. To extract +information from an algebraic datatype, you have to use `case` whose syntax +is `case <exp> | <cons1> <args1> => <exp1> | ...`. For example: + + not b = case b + | true => false + | false => true; + left x = case x | pair l _ => l; + right x = case x | pair _ r => r; + +Types share also the same namespace as other variables. + +You can name your fields in type constructors: + + type Pair a b | pair (left : a) (right : b); + +This can be used to pass arguments by name rather than by position. +For example, you can then construct a pair with either of: + + x = pair 5 6; + y = pair (right := 6) (left := 5); + left x = case x | pair (left := l) _ => l; + right x = case x | pair (right := r) _ => r; + +You can also use such named arguments for normal functions. +E.g. `sub (y := 5) 47` would also return 42. + +### Recursion + +Type annotations play a double role: they also play the role of forward +declarations. They are needed in recursive declarations. For example, when +defining the (recursive) type of simply-linked lists, you'd need: + + List : Type -> Type; + type List a + | nil + | cons a (List a) + +This is also needed for mutual recursion: + + odd : Int -> Int; + even : Int -> Int; + odd x = case Int_eq x 0 + | true => false + | false => even (x - 1); + even x = case Int_eq x 0 + | true => true + | false => odd (x - 1); + +### Polymorphism + +In the above `Pair` example, the type is polymorphic in that each field can +have any type. The real type of the `pair` constructor is: + + pair : (a : Type) ≡> (b : Type) ≡> a -> b -> Pair a b + +Where `(x : t) ≡> e` is used to specify arguments that are implicit and only +exist for type-checking purposes, so you can just call `pair 5 6` and let +Typer infer the types `a` and `b`. This said, if you want, you can provide +those type arguments explicitly using the named arguments syntax: + + p = pair (a := Int) (b := Int -> Int) 5 (lambda x -> x); + +## Macros + +Typer macros are modeled after Lisp macros, so they mostly manipulate the +program represented as an S-expression. + +### S-expressions + +S-expressions are represented using the `Sexp` type. This type is internal, +but is conceptually equivalent to the following datatype: + + type Sexp + | symbol String + | string String + | integer Int + | float Float + | node Sexp (List Sexp) + +Because it is not defined as an datatype, you currently cannot match it with +`case` and construct elements in the usual way. Instead, you need to use +the following constructors: + + Sexp_symbol : String -> Sexp; + Sexp_string : String -> Sexp; + Sexp_integer : Int -> Sexp; + Sexp_float : Float -> Sexp; + Sexp_node : Sexp -> List Sexp -> Sexp; + +and the following dispatch function: + + Sexp_dispatch : (a : Type) ≡> + Sexp + -> (node : Sexp -> List Sexp -> a) + -> (symbol : String -> a) + -> (string : String -> a) + -> (int : Int -> a) + -> (float : Float -> a) + -> (block : List Sexp -> a) + -> a; + +### Parsing code as S-expressions + +Contrary to Lisp, Typer uses an infix (or rather mixfix) syntax, so its +notion of S-expressions is a bit more complex than that of Lisp. When Typer +code is parsed its first turned into an S-expression where mixfix syntax is +replaced with "standard" prefix syntax. The source code does not actually +need to use the mixfix syntax and can always use the prefix syntax instead. + +The conversion between the two basically adds the `_` character to the +combination of keywords that make up a given mixfix construction. +For example, the term `a + b` gets converted to `_+_ a b` and the `lambda +x -> e` term turns into `lambda_->_ x e`. + +Here's a more complex example: + + type List a + | nil + | cons (hd : a) (tl : List a) + +turns into + + type_ (_|_ (List a) + nil + (cons (_:_ hd a) (_:_ tl (List a)))) + +Those above two forms are completely indistinguishable to Typer. +Note that contrary to Lisp, parentheses are not significant (other than to +clarify structure), so you can add parentheses anywhere you want as long as +they don't affect the structure. + +### Macro definitions + +A macro is little more than a function of S-expressions, which is invoked at +compile time. To turn such a function into a macro, just wrap it in the +`macro` constructor: + + fun = macro (lambda args -> Sexp_node (Sexp_symbol "lambda_->_") args); + +after which you can use it with the normal "function call" syntax: + + inc1 = fun x (x + 1); + +which will macroexpand to: + + inc1 = lambda_->_ x (x + 1); View it on GitLab: https://gitlab.com/monnier/typer/commit/0851032ef42817fa8c0e8fce5026d2737d6…

1 0

Properties and namespaces
by Stefan Monnier 15 Mar '17

15 Mar '17

There are a few things around "properties" I'd like to have in Typer which are similar yet different. If any of you has ideas about how to conflate/merge some of them, or how to clearly distinguish them or what to do about them, I'd like to hear it: Some properties I'm thinking of would be: - docstrings (as annotations on functions, types, and other variables): These could be properties of *values*, or properties of *bindings*. For types and functions, properties of values would probably work well (tho it prevents giving different docstrings to different names of the same function), but for variables holding things like integers, associating the docstring to the integer is not going to work well, so we probably need to support properties of bindings (we can probably limit them to actual declarations (i.e. let-bindings) since docstrings of function arguments are probably not needed). - decision procedures: These are the "macros" associated with a given type to automatically find/construct an expression of that type, as needed for implicit arguments. This is what we need to implement type classes. These can be associated to *values* or the *bindings*. In general I'd prefer using values than bindings since its natural/normal to manipulate values whereas it's unusual to manipulate bindings. Also, I'd like to have those properties be lexically scoped, so I can locally add a decision procedure for a type and elsewhere add another decision procedure for that same type. - declaration macros: normal macros (invoked using the function call syntax) are special values of type Macro, but there are other macros to use in other syntactic contexts, such as declaration macros (i.e. macros that can be invoked in the <decls> part of "let <decls> in <exp>"). Currently, declaration macros are shared with normal macros, i.e. it's one and the same namespace so if you define a `foo` macro it will apply to invocations of `foo` in <exp> as in <decls>. I'd like to separate those two cases. Especially because there will inevitably be more cases (e.g. lvalue macros, case-pattern macros, ...). These could be implemented as properties of bindings. But that means that if I rebind the `or` function, I end up also affecting the `or` pattern macro. So maybe another way to solve this would be to provided different namespaces. So I can independently define the `foo` var, the `foo` pattern-macro, the `foo` lvalue-macro, the `foo` declaration macro etc... without interference. A cheap way to do that is to use some name-prefixing scheme, so the `foo` pattern-macro is kept in the `patternmacro_foo` variable. I kind of like this name-prefixing solution, but I'm not sure what the convention should look like (which magic character to use). Also, better would be to have the "namespace prefix" be an object rather than a string. Hmm... so reading what I wrote, maybe what I need/want is to extend the `senv`, which is the part of the elaboration environment used to find the deBruijn index of a variable. IOW currently it's a Map from strings (variable identifiers) to (reverse) deBruijn indices, and the above suggests I should maybe extend this map such that it can be indexed by arbitrary objects (e.g. a pair of a namespace-object and a string). This said, currently those `senv` are environments specific to the elaboration phase, they tend to be transient, so we'd probably want to promote them somehow. Related to this: how should the above interact with modules (which are basically tuples with names fields)? How can a module indicate what is the docstring/decision-procedure/declaration-macro corresponding to a particular field? Stefan

1 0

[Git][monnier/typer][report/els-2017] Add ELS17 reviews
by Stefan 13 Mar '17

13 Mar '17

Stefan pushed to branch report/els-2017 at Stefan / Typer Commits: d118f4c6 by Stefan Monnier at 2017-03-12T23:38:55-04:00 Add ELS17 reviews - - - - - 1 changed file: - + REVIEWS Changes: ===================================== REVIEWS ===================================== --- /dev/null +++ b/REVIEWS @@ -0,0 +1,215 @@ +-*- org -*- +* ELS'17 +** ----------------------- REVIEW 1 --------------------- +PAPER: 14 +TITLE: Typer: An infix statically typed Lisp +AUTHORS: Pierre Delaunay, Vincent Archambault-Bouffard and Stefan Monnier + +Overall evaluation: 1 (weak accept) + +----------- Overall evaluation ----------- +The paper has merit in exploring the combination of mixfix syntax and lisp +style macros, and interleaved type inference and +macro-expansion. I recommend it for acceptance with some modifications. + +The text wastes two pages out of eight on explaining why macros are a good +idea, and how lisp parsing works: the first can be assumed as a given +in a Lisp-conference, and the second is relatively irrelevant and can also +mostly be assumed as a given. + +In contrast the text is quite light on details of the syntax and typing: it +assumes readers to be familiar with ML-family languages. In general this is +probably a fair assumption for any paper dealing with statically typed pure +functional languages, but possibly somewhat out of place +for a Lisp-conference. + +A paper obviously has a shelf-life far longer than the conference it appears +in, but some adjustment to expectations placed on the reader would be +beneficial. A small section exploring the costs and benefits of mixfix +syntax would be desirable as well. + +One of the most interesting parts of the presented language is the +interleaved type inference and macro-expansion, which the paper skims over +rather lightly. This would deserve elaboration, since it seems to be one of +the major features here. Syntaxes and parsers are a dime a dozen, though the +one presented is noteworthy for elegant integration of macros outside +S-expressions, but getting a proof-system out of macro-system by +interleaving it with type inference? That’s interesting. + +Detailed notes: + +Section 2.1 on S-expression parsing is not only largely needless, but +somewhat problematic as well. It seems to conflate structural parsing and +semantic analysis. + +Section 2.2 states that Lisp gets rid of difference between declarations and +expressions, which is manifestly not true for Common Lisp -- but that +difference is semantic, not structural: consider DECLARE and PROCLAIM, which +cannot appear in arbitrary places. Conflation of structure and semantics +again. From parsing point Lisp has only expressions, from execution point +this is not true. From the point of view of the paper this expressing this +distinction is meaningless, but having the language changed so that it +doesn’t actually state things that are untrue would be good. + +Section 2.2 also states that there are syntactic categories for symbols and +lvalues, but this is stretching those definitions and possibly +misunderstanding workings of SYMBOL-MACROLET and SETF-functions and macros: +they cannot be considered syntactic categories in any real +sense. Possibly a reflection of how assumptions built into mainstream CS +discourse don’t properly map 1:1 to fringe languages like Common +Lisp. However, as above, the distinction here doesn’t really matter for +the paper. + +Section 2.5 explores different macro implementation strategies, and is just +noise. The second bullet is overly vague and hard to understand. The third +bullet makes a weak and incorrect claim about particular implementation +strategy “typically implying that macros cannot be used in the file where +they are defined”. (That implementation strategy makes it more work, but not +terribly much so.) + +Recommend condensing entirety to 2.* sections: instead of trying to sort out +the problematic comparisons to Lisp just remove them. + +Section 3. Flippancy about hiding the scary Greek letter is out of place and +reads as somewhat condescending, which is probably not intentional. This is +the section that needs most clarification if audience is not assumed to be +fluent in ML-family languages. Given an audience of lispers use of +parenthesis should be clarified early on, instead of saved for section +4.2… :) + +Section 4 starts with a bizarre claim that Lisp’s parsing is in +3 steps. Some implementation might, but it’s an awfully strange way to look +at things. Again, the way Lisp may or may not do things doesn’t really +matter for this paper: keep the focus on Typer. + +Section 4.1’s contra-OCaml example near the end is tad confusing, possibly +due to overly tautological example. The note about altered precedence of ‘;’ +in OCaml is a good one, and deserves an example, but if possible some +clarification might be in order. + +Section 4.2 neglects to mention what [] actually do. Presumably they are +tuple of list constructors. + +Section 4.3 mentions a small set of default single-char tokens. If this set +can be user-extended, that’s worth a mention. + +Figure 3. Papers can be serious without using excessively terse +names. “arw”, “con”, “adt”. Not critical, but using readable names would +be nice. + +Section 5.1. Should at least mention which cases require special handling, +even if only function call elaboration is sketched out. + +Section 5.3. Why is “one big elaboration phase” a “significant downside”? It +seems to be one of the major strong points of the design. Would like to see +some elaboration, maybe a small example, on how the interleaved type +inference and macro expansion allow for macros to work as proof +tactics. This seems both novel and interesting. + +Section 6.3. Comparison to typed Racket mentions that this is a non-hygienic +system. It is not obvious to me that this is a deep property of the +presented macro-system: either this needs to be clarified, or the +intentional design choice should be mentioned up-front. + +Section 7. Does not actually discuss future work, so might just call +it Conclusions. + + +** ----------------------- REVIEW 2 --------------------- +PAPER: 14 +TITLE: Typer: An infix statically typed Lisp +AUTHORS: Pierre Delaunay, Vincent Archambault-Bouffard and Stefan Monnier + +Overall evaluation: -3 (strong reject) + +----------- Overall evaluation ----------- +This paper discusses some details about the language, Typer, which +seeks to integrate a variety of ideas of syntax with some ideas about +type systems. The paper has as an introduction to macros, a discussion +of the Typer reader, and a bit about its type system. The paper +includes no evaluation of any of its components. Each component is not +explained in enough detail to represent a contribution of +knowledge. Related work is treated carelessly. The intriguing parts of +the system are only hinted at with most of the paper time being +focused on minutiae and broad comments. + +--- Detailed Comments + +Sec 1 - Unprofessional writing + +1.47 - Many other static Lisps + +3 goals are poorly explained. (Why does "language is functional" mean +there should be infix?) + +Sec 2 - Prose is better than a list in a paper. + +2.19 - This assumes the reader already knows what you're talking about +and doesn't actually explain. + +2.23 - What is an "S-exp"? + +2.42 - This is trite. + +Sec 2.1 - I think you want to read the Honu paper. + +Sec 2.2 - Because Typed Racket does something doesn't make it good. + +Sec 2 - This whole section has no flow and is just a list of stuff. + +Sec 2.4 - Why does this actually matter though for your system or for +programmers? + +Sec 2.5 - What is the beginning of this section referring to? + +Sec 2 - This entire section was a waste of space. It doesn't really +add anything to your contribution and is not a novel explanation. + +3.11 - This is trite. + +Sec 3 - The repeated use of "Notice" and "Note" is bad style and +exposes that your explanation is not thorough or thought out. + +3.40 - What is this? + +Sec 3 - It would be interesting for you to elaborate what is +problematic about declarations being expressions. We don't know enough +about your language at this point to understand what the problems +could be. + +Sec 3 - The most important part of this section is not the run through +of your Haskell-like syntax; it is the discussion of the +macros. Unfortunately, you don't explain why a monad is necessary or +how we are supposed to understand the definition of `mylet`. In +particular, there appears to be no effect, so why the monad? + +4.21 - "You can think of" ... is very unprofessional + +Sec 4 - The choice of OPG is actually interesting, but the most +interesting part of the design choice is pushed to small bullets +rather than a true explanation of the trade-offs and analysis that led +to the choice. + +Sec 4.2 - I like these examples, but I would like to know exactly what +the numbers and the pairings are because you've explained OPGs that +way. At this point in the paper, its purpose is very unclear: is this +a paper about a type system? That's what the introduction made me +assume, but then I thought it was a paper about macros, but now I +think it is a paper about reading and parsing. The introduction does +not serve the paper by providing a guide to how the rest should be +read. + +5.56 - I don't understand this paragraph. How can you do that and why +do you want to? + +Sec 5.1 - This is bewildering because it seems like the type checker +is the most important part, but you say that it is outside of the +paper's scope! + +6.53 - I don't see any connection between closedness and phases. Phase +separation is about separate compilation and modularity. + +Sec 5 - The last paragraph is very bizarre because it throws in a +totally new topic that has never been hinted at before that seems +fascinating. Unfortunately, we have no explanation! + View it on GitLab: https://gitlab.com/monnier/typer/commit/d118f4c6d975d600949b106547d99698538…

1 0

[Git][monnier/typer][master] * btl/pervasive.typer: Redefine lambda as a macro
by Stefan 11 Mar '17

11 Mar '17

Stefan pushed to branch master at Stefan / Typer Commits: b2c05da9 by Stefan Monnier at 2017-03-10T21:33:38-05:00 * btl/pervasive.typer: Redefine lambda as a macro * btl/pervasive.typer (List_foldr, List_find): New functions. (Sexp_error): Move. (Sexp_to_list, multiarg_lambda): New functions. (lambda_->_, lambda_=>_, lambda_≡>_): Redefine to add multiarg support via macros. (List_head, List_map, List_foldl): * btl/builtins.typer (Eq_comm, Macro_expand): Don't use multi-arg lambdas (yet). - - - - - 2 changed files: - btl/builtins.typer - btl/pervasive.typer Changes: ===================================== btl/builtins.typer ===================================== --- a/btl/builtins.typer +++ b/btl/builtins.typer @@ -54,7 +54,7 @@ Eq_cast = Built-in "Eq.cast" %% 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_comm = lambda l ≡> lambda t ≡> lambda x ≡> lambda y ≡> lambda p -> Eq_cast (f := lambda xy -> Eq (t := t) xy x) (p := p) Eq_refl; @@ -133,12 +133,12 @@ Sexp_node = Built-in "Sexp.node" (Sexp -> List Sexp -> Sexp); Sexp_integer = Built-in "Sexp.integer" (Int -> Sexp); Sexp_float = Built-in "Sexp.float" (Float -> Sexp); -Macro = typecons (Macro) - (macro (List Sexp -> Sexp)); +Macro = typecons (Macro) + (macro (List Sexp -> Sexp)); macro = datacons Macro macro; Macro_expand : Macro -> List Sexp -> Sexp; -Macro_expand m args = case m +Macro_expand = lambda m -> lambda args -> case m | macro f => f args; Sexp_dispatch = Built-in "Sexp.dispatch" ( ===================================== btl/pervasive.typer ===================================== --- a/btl/pervasive.typer +++ b/btl/pervasive.typer @@ -72,7 +72,7 @@ List_head1 = lambda a ≡> lambda xs -> case xs | cons hd tl => some hd; List_head : (a : Type) ≡> a -> List a -> a; -List_head = lambda a ≡> lambda x xs -> case xs +List_head = lambda a ≡> lambda x -> lambda xs -> case xs | cons x _ => x | nil => x; @@ -82,15 +82,96 @@ List_tail = lambda a ≡> lambda xs -> case xs | cons hd tl => tl; List_map : (a : Type) ≡> (b : Type) ≡> (a -> b) -> List a -> List b; -List_map = lambda a b ≡> lambda f xs -> case xs +List_map = lambda a ≡> lambda b ≡> lambda f -> lambda xs -> case xs | nil => nil | cons x xs => cons (f x) (List_map f xs); List_foldl : (a : Type) ≡> (b : Type) ≡> (a -> b -> a) -> a -> List b -> a; -List_foldl = lambda a b ≡> lambda f i xs -> case xs +List_foldl = lambda a ≡> lambda b ≡> lambda f -> lambda i -> lambda xs -> case xs | nil => i | cons x xs => List_foldl f (f i x) xs; +List_foldr : (a : Type) ≡> (b : Type) ≡> (b -> a -> a) -> List b -> a -> a; +List_foldr = lambda a ≡> lambda b ≡> lambda f -> lambda xs -> lambda i -> case xs + | nil => i + | cons x xs => f x (List_foldr f xs i); + +List_find : (a : Type) ≡> (a -> Bool) -> List a -> Option a; +List_find = lambda a ≡> lambda f -> lambda xs -> case xs + | nil => none + | cons x xs => case f x | true => some x | false => List_find f xs; + +%%%% A more flexible `lambda`. + +%% An Sexp which we use to represents an error. +Sexp_error = Sexp_symbol "<error>"; + +Sexp_to_list : Sexp -> List Sexp -> List Sexp; +Sexp_to_list = lambda s -> lambda exceptions + -> let singleton = lambda (a : Type) ≡> lambda (_ : a) -> cons s nil in + Sexp_dispatch + s + (node := lambda head -> lambda tail + -> case List_find (Sexp_eq head) exceptions + | some _ => singleton () + | none => cons head tail) + (symbol := lambda s + -> case String_eq "" s + | true => nil + | false => singleton ()) + singleton singleton singleton singleton; + +multiarg_lambda = + %% let bodytail = cons body nil; + %% mklam = lambda (a : Type) ≡> lambda (_ : a) + %% -> Sexp_node (Sexp_symbol "##lambda_->_") + %% (cons arg bodytail) in + %% Sexp_dispatch + %% arg + %% (node := (lambda head -> lambda tail -> + %% Sexp_dispatch + %% head + %% (symbol := (lambda s -> case String_eq s "_:_" + %% | true -> mklam () + %% | false -> case String_eq s "_::_" + %% | true + %% -> Sexp_node (Sexp_symbol "##lambda_=>_") + %% (cons (Sexp_node + %% (Sexp_symbol "_:_") + %% tail) + %% bodytail) + %% | false -> case String_eq s "_:::_" + %% | true + %% -> Sexp_node (Sexp_symbol "##lambda_≡>_") + %% (cons (Sexp_node + %% (Sexp_symbol "_:_") + %% tail) + %% bodytail) + %% | false -> mklam ())) + %% mklam mklam mklam mklam mklam)) + %% mklam mklam mklam mklam mklam + let exceptions = List_map Sexp_symbol + (cons "_:_" (cons "_::_" (cons "_:::_" nil))) in + lambda name -> + let sym = (Sexp_symbol name); + mklambda = lambda arg -> lambda body -> + Sexp_node sym (cons arg (cons body nil)) in + lambda (margs : List Sexp) -> case margs + | nil => Sexp_error + | cons fargs margstail + => case margstail + | nil => Sexp_error + | cons body bodytail + => case bodytail + | cons _ _ => Sexp_error + | nil => List_foldr mklambda + (Sexp_to_list fargs exceptions) + body; + +lambda_->_ = macro (multiarg_lambda "##lambda_->_"); +lambda_=>_ = macro (multiarg_lambda "##lambda_=>_"); +lambda_≡>_ = macro (multiarg_lambda "##lambda_≡>_"); + %%%% Quasi-Quote macro %% f = (quote (uquote x) * x) (node _*_ [(Sexp_node unquote "x") "x"]) @@ -99,9 +180,6 @@ List_foldl = lambda a b ≡> lambda f i xs -> case xs %% %% => x -%% An Sexp which we use to represents an error. -Sexp_error = Sexp_symbol "<error>"; - quote1 : Sexp -> Sexp; quote1 x = let k = K x; node op y = case (Sexp_eq op (Sexp_symbol "uquote")) View it on GitLab: https://gitlab.com/monnier/typer/commit/b2c05da97266b422ee07c8f4a1fdd473dcd…

1 0

[Git][monnier/typer][master] Improve type inference and add `.` macro.
by Stefan 09 Mar '17

09 Mar '17

Stefan pushed to branch master at Stefan / Typer Commits: b10e7943 by Stefan Monnier at 2017-03-08T23:43:02-05:00 Improve type inference and add `.` macro. For tuples and `.` macro to work, type inference needed to be improved. This improvement is to annotate metavars so they can't accidentally refer to local vars. IOW rather than "grafted", they're now "logical". This also refined slightly the inversion of substitutions, tho I'm not sure it makes an actual difference in the end. * btl/pervasive.typer (BoolMod): Prototype of a Bool module. (Pair): New type. (__.__): New macro. * emacs/typer-mode.el (typer-smie-rules): Add dangling `in` rule, as used in OCaml. Don't move up to the parent when indenting a `case` or `lambda` with a `case`'s branch. * src/debruijn.ml (scope_level, lctx_length): New types. (elab_context): Add scope data. (make_elab_context): Rename to empty_elab_context. (ectx_new_scope, ectx_get_scope): New functions. * src/debug_util.ml (main.ctx_to_cctx): Remove, use ectx_to_lctx instead. * src/inverse_subst.ml (dummy_var): Remove. (substIR): Add destination count. (transfo.transfo): Refine the transformation so it is reversible. (inverse): Check success. * src/lexp.ml (lexp_name): Move so we can use lexp_string for "trivial" cases. (subst_string): Use it to avoid pathological cases. * src/lparse.ml (_global_lexp_ctx): Remove. (check): Shift metavars so they can't refer to vars from within the scope. (infer_call.handle_fun_args): Unify two branches. (lexp_decls_1, sform_letin): Introduce new scope for metavars. * src/pexp.ml (pexp_p_actual_arg): Remove, unused. (pexp_p_decls): Use sexp_u_list. * tests/eval_test.ml: Add test of the `.` notation. - - - - - 11 changed files: - btl/builtins.typer - btl/pervasive.typer - emacs/typer-mode.el - src/debruijn.ml - src/debug_util.ml - src/eval.ml - src/inverse_subst.ml - src/lexp.ml - src/lparse.ml - src/pexp.ml - tests/eval_test.ml Changes: ===================================== btl/builtins.typer ===================================== --- a/btl/builtins.typer +++ b/btl/builtins.typer @@ -126,7 +126,7 @@ cons = datacons List cons; %%%% Macro-related definitions -%% block_ = Built-in "block_" (List Pretoken -> 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); @@ -139,7 +139,7 @@ macro = datacons Macro macro; Macro_expand : Macro -> List Sexp -> Sexp; Macro_expand m args = case m - | macro f => (f args); + | macro f => f args; Sexp_dispatch = Built-in "Sexp.dispatch" ( (a : Type) ≡> ===================================== btl/pervasive.typer ===================================== --- a/btl/pervasive.typer +++ b/btl/pervasive.typer @@ -218,6 +218,40 @@ length = List_length; head = List_head1; tail = List_tail; +%%%% Tuples + +%% Sample tuple: a module holding Bool and its constructors. +BoolMod = (##datacons (typecons _ (cons (t :: ?) (true :: ?) (false :: ?))) + cons) + (_ := Bool) (_ := true) (_ := false); + +Pair = typecons (Pair (a : Type) (b : Type)) (cons (x :: a) (y :: b)); + +__\.__ = + let mksel o f = + let constructor = Sexp_node (Sexp_symbol "##datacons") + (cons (Sexp_symbol "?") + (cons (Sexp_symbol "cons") + nil)); + pattern = Sexp_node constructor + (cons (Sexp_node (Sexp_symbol "_:=_") + (cons f (cons (Sexp_symbol "v") + nil))) + nil); + branch = Sexp_node (Sexp_symbol "_=>_") + (cons pattern (cons (Sexp_symbol "v") nil)); + in Sexp_node (Sexp_symbol "case_") + (cons (Sexp_node (Sexp_symbol "_|_") + (cons o (cons branch nil))) + nil) + in macro (lambda args + -> case args + | cons o tail + => (case tail + | cons f _ => mksel o f + | nil => Sexp_error) + | nil => Sexp_error); + %%%% Logic %% False should be one of the many empty types. ===================================== emacs/typer-mode.el ===================================== --- a/emacs/typer-mode.el +++ b/emacs/typer-mode.el @@ -172,10 +172,12 @@ ;; along the lines of what's done in Tuareg. (pcase (cons kind token) (`(:before . "|") (smie-rule-parent (if (smie-rule-parent-p "type") 2))) + (`(:after . "in") (if (smie-rule-hanging-p) (smie-rule-parent))) (`(:before . "(") (if (smie-rule-hanging-p) (smie-rule-parent))) (`(:before . ,(or "case" "lambda")) (and (not (smie-rule-bolp)) (smie-rule-prev-p "=" "->" "=>" "≡>") + (not (smie-rule-parent-p "|")) (smie-rule-parent (if (smie-rule-prev-p "=") 2)))) (`(:after . "=") 2) (`(:after . ,(or "->" "=>" "≡>")) ===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -104,13 +104,20 @@ type scope = db_ridx SMap.t (* Map<String, db_ridx>*) type senv_length = int (* it is not the map true length *) type senv_type = senv_length * scope +(* Scope level is used to detect "out of scope" metavars. + * See http://okmij.org/ftp/ML/generalization.html + * The lctx_length keeps track of the lctx's length when that scope level was + * entered in order to know by how much to shift metavars. *) +type scope_level = int +type lctx_length = db_ridx + (* This is the *elaboration context* (i.e. a context that holds * a lexp context plus some side info. *) -type elab_context = senv_type * lexp_context +type elab_context = senv_type * lexp_context * (scope_level * lctx_length) (* Extract the lexp context from the context used during elaboration. *) let ectx_to_lctx (ectx : elab_context) : lexp_context = - let (_, lctx) = ectx in lctx + let (_, lctx, _) = ectx in lctx (* internal definitions * ---------------------------------- *) @@ -122,16 +129,14 @@ let _make_myers = M.nil (* Public methods: DO USE * ---------------------------------- *) -let make_elab_context = (_make_senv_type, _make_myers) - -let get_roffset ctx = let (_, _, (_, rof)) = ctx in rof +let empty_elab_context : elab_context = (_make_senv_type, _make_myers, (0, 0)) -let get_size ctx = let ((n, _), _) = ctx in n +let get_size ctx = let ((n, _), _, _) = ctx in n (* return its current DeBruijn index *) let rec senv_lookup (name: string) (ctx: elab_context): int = - let ((n, map), _) = ctx in - n - (SMap.find name map) - 1 + let ((n, map), _, _) = ctx in + n - (SMap.find name map) - 1 let lexp_ctx_cons (ctx : lexp_context) offset d v t = assert (offset >= 0 @@ -150,18 +155,19 @@ let lctx_extend (ctx : lexp_context) (def: vname option) (v: varbind) (t: lexp) let env_extend_rec r (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = let (loc, name) = def in - let ((n, map), env) = ctx in + let ((n, map), env, sl) = ctx in let nmap = SMap.add name n map in ((n + 1, nmap), - lexp_ctx_cons env r (Some def) v t) + lexp_ctx_cons env r (Some def) v t, + sl) let env_extend (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = env_extend_rec 0 ctx def v t let ectx_extend (ectx: elab_context) (def: vname option) (v: varbind) (t: lexp) : elab_context = match def with - | None -> let ((n, map), lctx) = ectx in - ((n + 1, map), lexp_ctx_cons lctx 0 None v t) + | None -> let ((n, map), lctx, sl) = ectx in + ((n + 1, map), lexp_ctx_cons lctx 0 None v t, sl) | Some def -> env_extend ectx def v t let lctx_extend_rec (ctx : lexp_context) (defs: (vname * lexp * ltype) list) = @@ -174,12 +180,19 @@ let lctx_extend_rec (ctx : lexp_context) (defs: (vname * lexp * ltype) list) = ctx let ectx_extend_rec (ctx: elab_context) (defs: (vname * lexp * ltype) list) = - let ((n, senv), lctx) = ctx in + let ((n, senv), lctx, sl) = ctx in let senv', _ = List.fold_left (fun (senv, i) ((_, vname), _, _) -> SMap.add vname i senv, i + 1) (senv, n) defs in - ((n + List.length defs, senv'), lctx_extend_rec lctx defs) + ((n + List.length defs, senv'), lctx_extend_rec lctx defs, sl) + +let ectx_new_scope ectx : elab_context = + let (senv, lctx, (scope, _)) = ectx in + (senv, lctx, (scope + 1, Myers.length lctx)) + +let ectx_get_scope (ectx : elab_context) : (scope_level * lctx_length) = + let (_, _, sl) = ectx in sl let env_lookup_by_index index (ctx: lexp_context): env_elem = Myers.nth index ctx ===================================== src/debug_util.ml ===================================== --- a/src/debug_util.ml +++ b/src/debug_util.ml @@ -410,13 +410,10 @@ let main () = ) flexps)); (* get typecheck context *) - let lctx_to_cctx (lctx: elab_context) = - let (_, env) = ctx in env in - (if (get_p_option "typecheck") then( print_string (make_title " TYPECHECK "); - let cctx = lctx_to_cctx ctx in + let cctx = ectx_to_lctx ctx in (* run type check *) List.iter (fun (_, lxp, _) -> let _ = OL.check VMap.empty cctx lxp in ()) ===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -208,7 +208,7 @@ let make_float loc depth args_val = match args_val with let string_eq loc depth args_val = match args_val with | [Vstring s1; Vstring s2] -> o2v_bool (s1 = s2) - | _ -> error loc "string_eq expects 2 strings" + | _ -> error loc "String.= expects 2 strings" let sexp_eq loc depth args_val = match args_val with | [Vsexp (s1); Vsexp (s2)] -> o2v_bool (sexp_equal s1 s2) @@ -266,8 +266,8 @@ let rec _eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type | Builtin ((_, str)) -> Vbuiltin (str) (* Return a value stored in env *) - | Var((loc, name), idx) as e -> - eval_var ctx e ((loc, name), idx) + | Var((loc, name), idx) as e + -> eval_var ctx e ((loc, name), idx) (* Nodes *) (* ---------------- *) ===================================== src/inverse_subst.ml ===================================== --- a/src/inverse_subst.ml +++ b/src/inverse_subst.ml @@ -51,15 +51,14 @@ module S = Subst type inter_subst = lexp list (* Intermediate between "tree"-like substitution and fully flattened subsitution *) -let dummy_var = Var((dummy_location, "DummyVar"), -1) - -type substIR = ((int * int) list * int) +type substIR = ((int * int) list * int * int) (** Transform a substitution to a more linear substitution * makes the inversion easier * Example of result : ((new_idx, old_position)::..., shift)*) let transfo (s: lexp S.subst) : substIR option = - let rec transfo (s: lexp S.subst) (off_acc: int) (idx: int): substIR option = + let rec transfo (s: lexp S.subst) (off_acc: int) (idx: int) (imp_cnt : int) + : substIR option = let indexOf (v: lexp): int = (* Helper : return the index of a variabble *) match v with | Var (_, v) -> v @@ -70,15 +69,17 @@ let transfo (s: lexp S.subst) : substIR option = in match s with | S.Cons (Var _ as v, s) -> - (match transfo s off_acc (idx + 1) with - | Some (tail, off) -> let newVar = shiftVar v off_acc + (match transfo s off_acc (idx + 1) imp_cnt with + | Some (tail, off, imp) -> let newVar = shiftVar v off_acc in if newVar >= off then None (* Error *) - else Some (((shiftVar v off_acc), idx)::tail, off) - | None -> None) - | S.Shift (s, offset) -> transfo s (offset + off_acc) idx - | S.Identity -> Some ([], off_acc) (* End of recursion *) + else Some (((shiftVar v off_acc), idx)::tail, off, imp) + | None -> None) + | S.Cons (Imm (Sexp.Symbol (_, "")), s) + -> transfo s off_acc (idx + 1) (imp_cnt + 1) + | S.Shift (s, offset) -> transfo s (offset + off_acc) idx imp_cnt + | S.Identity -> Some ([], off_acc, imp_cnt) (* End of recursion *) | _ -> None (* Error *) - in transfo s 0 0 + in transfo s 0 0 0 (* Inverse *) @@ -110,7 +111,7 @@ let fill (l: (int * int) list) (nbVar: int) (shift: int): lexp S.subst option = in let fill_before (l: (int * int) list) (s: lexp S.subst) (nbVar: int): lexp S.subst option = (* Fill if the first var is not 0 *) match l with - | [] -> Some (genDummyVar 0 nbVar S.identity) + | [] -> Some (genDummyVar 0 nbVar s) | (i1, v1)::_ when i1 > 0 -> Some (genDummyVar 0 i1 s) | _ -> Some s in let rec fill_after (l: (int * int) list) (nbVar: int) (shift: int): lexp S.subst option = (* Fill gaps *) @@ -122,23 +123,32 @@ let fill (l: (int * int) list) (nbVar: int) (shift: int): lexp S.subst option = | None -> None | Some s -> Some (S.cons (mkVar val1) (genDummyVar (idx1 + 1) idx2 s))) - | (idx1, val1)::(idx2, val2)::tail -> - (match fill_after ((idx2, val2)::tail) nbVar shift with - | None -> None - | Some s -> Some (S.cons (mkVar val1) s)) + | (idx1, val1)::(idx2, val2)::tail + -> (match fill_after ((idx2, val2)::tail) nbVar shift with + | None -> None + | Some s -> Some (S.cons (mkVar val1) s)) - | (idx1, val1)::[] when (idx1 + 1) < nbVar -> - Some (S.cons (mkVar val1) (genDummyVar (idx1 + 1) nbVar (S.shift shift))) + | (idx1, val1)::[] when (idx1 + 1) < nbVar + -> Some (S.cons (mkVar val1) + (genDummyVar (idx1 + 1) nbVar (S.shift shift))) - | (idx1, val1)::[] -> - Some (S.cons (mkVar val1) (S.shift shift)) + | (idx1, val1)::[] + -> Some (S.cons (mkVar val1) (S.shift shift)) - | [] -> - Some (S.shift shift) + | [] + -> Some (S.shift shift) in match fill_after l nbVar shift with | None -> None | Some s -> fill_before l s nbVar +let is_identity s = + let rec is_identity s acc = + match s with + | S.Cons(Var(_, idx), s1) when idx = acc -> is_identity s1 (acc + 1) + | S.Shift(S.Identity, shift) -> acc = shift + | _ -> S.identity_p s + in is_identity s 0 + (** Compute the inverse, if there is one, of the substitution. <code>s:S.subst, l:lexp, s':S.subst</code> where <code>l[s][s'] = l</code> and <code> inverse s = s' </code> @@ -147,6 +157,21 @@ let inverse (s: lexp S.subst) : lexp S.subst option = let sort = List.sort (fun (ei1, _) (ei2, _) -> compare ei1 ei2) in match transfo s with | None -> None - | Some (cons_lst, shift_val) -> - let size = sizeOf cons_lst - in fill (sort cons_lst) shift_val size + | Some (cons_lst, shift_val, imp_cnt) + -> let size = imp_cnt + sizeOf cons_lst in + (* print_string ("imp_cnt = " ^ string_of_int imp_cnt + * ^ "; shift_val = " ^ string_of_int shift_val + * ^ "; size = " ^ string_of_int size + * ^ "\n"); *) + let res = fill (sort cons_lst) shift_val size in + (match res with + | Some s1 + -> if is_identity (Lexp.scompose s s1) + || is_identity (Lexp.scompose s1 s) then () + else (print_string ("Subst-inversion-bug: " + ^ subst_string s ^ " ∘ " + ^ subst_string s1 ^ " == " + ^ subst_string (Lexp.scompose s1 s) + ^ " !!\n")) + | _ -> ()); + res ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -346,24 +346,6 @@ let clean meta_ctx e = with Not_found -> mkMetavar (idx, s, l, t) in clean S.identity e -let lexp_name e = - match e with - | Imm _ -> "Imm" - | Var _ -> "Var" - | Let _ -> "let" - | Arrow _ -> "Arrow" - | Lambda _ -> "lambda" - | Call _ -> "Call" - | Cons _ -> "datacons" - | Case _ -> "case" - | Inductive _ -> "typecons" - | Susp _ -> "Susp" - | Builtin (_, _, None) -> "Builtin" - | Builtin _ -> "AttributeTable" - | Metavar _ -> "Metavar" - | Sort _ -> "Sort" - | SortLevel _ -> "SortLevel" - let sdatacons = Symbol (U.dummy_location, "##datacons") let stypecons = Symbol (U.dummy_location, "##typecons") @@ -491,7 +473,25 @@ and lexp_string lxp = sexp_string (lexp_unparse lxp) and subst_string s = match s with | S.Identity -> "Id" | S.Shift (s, n) -> "(↑"^ string_of_int n ^ " " ^ subst_string s ^ ")" - | S.Cons (l, s) -> lexp_string l ^ " · " ^ subst_string s + | S.Cons (l, s) -> lexp_name l ^ " · " ^ subst_string s + +and lexp_name e = + match e with + | Imm _ -> lexp_string e + | Var _ -> lexp_string e + | Let _ -> "let" + | Arrow _ -> "Arrow" + | Lambda _ -> "lambda" + | Call _ -> "Call" + | Cons _ -> "datacons" + | Case _ -> "case" + | Inductive _ -> "typecons" + | Susp _ -> "Susp" + | Builtin (_, _, None) -> "Builtin" + | Builtin _ -> "AttributeTable" + | Metavar _ -> "Metavar" + | Sort _ -> "Sort" + | SortLevel _ -> "SortLevel" (* ------------------------------------------------------------------------- *) (* Printing *) ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -60,7 +60,6 @@ let make_var name index loc = (* dummies *) let dloc = dummy_location -let _global_lexp_ctx = ref make_elab_context let _parsing_internals = ref false let btl_folder = ref "./btl/" @@ -248,10 +247,6 @@ let rec infer (p : sexp) (ctx : elab_context): lexp * ltype = let tloc = sexp_location p in - (* Save current trace in a global variable. If an error occur, - we will be able to retrieve the most recent trace and context. *) - _global_lexp_ctx := ctx; - match p with | Symbol (l,name) when String.length name >= 1 && String.get name 0 == '#' @@ -446,11 +441,18 @@ and check (p : sexp) (t : ltype) (ctx : elab_context): lexp = let (e, inferred_t) = infer_call ctx (f, ft) args in check_inferred ctx e inferred_t t - | Symbol (l,"?") -> newMetavar l "v" t - | Symbol (l, name) when String.length name > 1 + | Symbol (l, name) when String.length name >= 1 && String.get name 0 = '?' - -> sexp_error l "Named metavars not supported (yet)"; - newMetavar l name t + -> let name = if name = "?" then "v" else + (sexp_error l "Named metavars not supported (yet)"; + String.sub name 1 (String.length name)) in + let (_, slen) = ectx_get_scope ctx in + (* Shift the var so it can't refer to the local vars. + * This is used so that in cases like "lambda t (y : ?) ... " + * type inference can guess ? without having to wonder whether it + * can refer `t` or not. If the user wants ? to be able to refer to + * `t`, then she should explicitly write (y : ? t). *) + mkSusp (newMetavar l name t) (S.shift ((get_size ctx) - slen)) | _ -> infer_and_check p ctx t @@ -458,7 +460,7 @@ and infer_and_check pexp ctx t = let (e, inferred_t) = infer pexp ctx in check_inferred ctx e inferred_t t -(* This is a crucial function: take an expression `e` of type `inferred_t +(* This is a crucial function: take an expression `e` of type `inferred_t` * and convert it into something of type `t`. Currently the only conversion * we use is to instantiate implicit arguments when needed, but we could/should * do lots of other things. *) @@ -715,16 +717,15 @@ and infer_call ctx (func, ltp) (sargs: sexp list) = ^ "` have no matching formal args")); largs, ltp - | sarg :: sargs, Arrow (Aexplicit, _, arg_type, _, ret_type) - -> let larg = check sarg arg_type ctx in + | sarg :: sargs, _ + -> let (arg_type, ret_type) = match ltp' with + | Arrow (ak, _, arg_type, _, ret_type) + -> assert (ak = Aexplicit); (arg_type, ret_type) + | _ -> unify_with_arrow ctx (sexp_location sarg) + ltp' Aexplicit (dloc, "<anon>") None in + let larg = check sarg arg_type ctx in handle_fun_args ((Aexplicit, larg) :: largs) sargs pending - (L.mkSusp ret_type (S.substitute larg)) - - | sarg :: sargs, t - -> print_lexp_ctx (ectx_to_lctx ctx); - lexp_fatal (sexp_location sarg) t - ("Explicit arg `" ^ sexp_string sarg - ^ "` to non-function (type = " ^ lexp_string ltp ^ ")") in + (L.mkSusp ret_type (S.substitute larg)) in let largs, ret_type = handle_fun_args [] sargs SMap.empty ltp in mkCall (func, List.rev largs), ret_type @@ -850,9 +851,9 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) -> let adjusted_ltp = push_susp ltp (S.shift (i + 1)) in assert (t == ltp); let e = check pexp adjusted_ltp nctx in - let (ec, lc) = nctx in + let (ec, lc, sl) = nctx in (IntMap.add i (v, e, ltp) map, - (ec, Myers.set_nth i (o, v', LetDef e, t) lc)) + (ec, Myers.set_nth i (o, v', LetDef e, t) lc, sl)) | _ -> U.internal_error "Defining same slot!") defs (IntMap.empty, nctx) in let decls = List.rev (List.map (fun (_, d) -> d) (IntMap.bindings declmap)) in @@ -876,7 +877,7 @@ and lexp_decls_1 [], [], nctx | Ptype ((l, vname) as v, ptp) :: pdecls - -> let ltp = infer_type ptp nctx (Some v) in + -> let ltp = infer_type ptp (ectx_new_scope nctx) (Some v) in if SMap.mem vname pending_decls then (error l ("Variable `" ^ vname ^ "` declared twice!"); lexp_decls_1 pdecls ectx nctx pending_decls pending_defs) @@ -893,7 +894,7 @@ and lexp_decls_1 when SMap.is_empty pending_decls -> assert (pending_defs == []); assert (ectx == nctx); - let (lexp, ltp) = infer pexp nctx in + let (lexp, ltp) = infer pexp (ectx_new_scope nctx) in (* Lexp decls are always recursive, so we have to shift by 1 to account * for the extra var (ourselves). *) [(v, mkSusp lexp (S.shift 1), ltp)], pdecls, @@ -904,6 +905,7 @@ and lexp_decls_1 let pending_decls = SMap.remove vname pending_decls in let pending_defs = ((v, pexp, ltp) :: pending_defs) in if SMap.is_empty pending_decls then + let nctx = ectx_new_scope nctx in let decls, nctx = lexp_check_decls ectx nctx pending_defs in decls, pdecls, nctx else @@ -1216,7 +1218,7 @@ let sform_letin ctx loc sargs ot = match sargs with -> let pdecls = pexp_p_decls sdecls in let declss, nctx = lexp_p_decls pdecls ctx in (* FIXME: Use `elaborate`. *) - let bdy, ltp = infer sbody nctx in + let bdy, ltp = infer sbody (ectx_new_scope nctx) in let s = List.fold_left (OL.lexp_defs_subst loc) S.identity declss in (lexp_let_decls declss bdy nctx, Inferred (mkSusp ltp s)) @@ -1316,7 +1318,7 @@ let default_ectx warning dloc "Predef not found"; in (* Empty context *) - let lctx = make_elab_context in + let lctx = empty_elab_context in let lctx = SMap.fold (fun key (e, t) ctx -> if String.get key 0 = '-' then ctx else ctx_define ctx (dloc, key) e t) ===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -54,16 +54,6 @@ let rec pexp_pat_location e = match e with | Ppatsym (l,_) -> l | Ppatcons (e, _) -> sexp_location e -and pexp_p_actual_arg arg : (arg_kind * pvar option * sexp) = - match arg with - | Node (Symbol (_, ":≡"), [Symbol s; e]) - -> (Aerasable, Some s, e) - | Node (Symbol (_, ":="), [Symbol s; e]) - -> (Aimplicit, Some s, e) - | Node (Symbol (_, ":-"), [Symbol s; e]) - -> (Aexplicit, Some s, e) - | e -> (Aexplicit, None, e) - and pexp_p_formal_arg arg : (arg_kind * pvar * sexp option) = match arg with | Node (Symbol (_, "_:::_"), [Symbol s; e]) @@ -149,18 +139,16 @@ and pexp_p_decls e: pdecl list = | Symbol (_, "") -> [] | Node (Symbol (_, ("_;_" | "_;" | ";_")), decls) -> List.concat (List.map pexp_p_decls decls) - | Node (Symbol (_, "_:_"), [Symbol s; t]) -> [Ptype(s, t)] - | Node (Symbol (_, "_=_"), [Symbol s; t]) -> [Pexpr(s, t)] + | Node (Symbol (_, "_:_"), [Symbol s; t]) -> [Ptype (s, t)] + | Node (Symbol (_, "_=_"), [Symbol s; t]) -> [Pexpr (s, t)] | Node (Symbol (l, "_=_"), [Node (Symbol s, args) as d; t]) -> + (* FIXME: Hardcode "lambda_->_"! *) [Pexpr (s, Node (Symbol (sexp_location d, "lambda_->_"), - [(match args with - | [] -> Sexp.dummy_epsilon - | arg::args -> Node (arg, args)); - t]))] + [sexp_u_list args; t]))] (* everything else is considered a macro * An error will be produced during lexp_parsing if the macro does not exist * once expanded the Pmcall macro will produce a list of pdecl *) - | Node (Symbol (l, op), args) -> [Pmcall((l, op), args)] + | Node (Symbol (l, op), args) -> [Pmcall ((l, op), args)] | _ -> print_string ((sexp_name e) ^ ": \""); sexp_print e; print_string "\"\n"; pexp_error (sexp_location e) ("Unknown declaration"); [] ===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -372,12 +372,19 @@ let _ = test_eval_eqv_named p : P; p = lambda a ≡> lambda x notx -> notx x; tP : Decidable P; - tP = (datacons Decidable true) (prop := P) (p := p);" + tP = (datacons Decidable true) (prop := P) (p := p); + + ptest : Pair Int String; + ptest = (##datacons Pair cons) (x := 4) (y := \"hello\"); + + px = case ptest | (##datacons ? cons) (x := v) => v; + + py = ptest.y;" "case tP | (datacons ? true) (p := _) => 3 - | (datacons ? false) (p := _) => 4;" - "3;" + | (datacons ? false) (p := _) => 4; px; py" + "3; 4; \"hello\";" let _ = test_eval_eqv_named "Y" View it on GitLab: https://gitlab.com/monnier/typer/commit/b10e7943e9ec2caf4e559b098d24c74e978…

1 0