From 6fdec59bbd3fc67ff3b0c48193201c1739aa7f70 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 1 Aug 2017 00:44:51 +0200 Subject: Adding documentation from the CEP. --- doc/ltac2.md | 642 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 642 insertions(+) create mode 100644 doc/ltac2.md (limited to 'doc') diff --git a/doc/ltac2.md b/doc/ltac2.md new file mode 100644 index 0000000000..38a56d3d6b --- /dev/null +++ b/doc/ltac2.md @@ -0,0 +1,642 @@ +# Summary + +The Ltac tactic language is probably one of the ingredients of the success of +Coq, yet it is at the same time its Achilles' heel. Indeed, Ltac: + +- has nothing like intended semantics +- is very non-uniform due to organic growth +- lacks expressivity and requires programming-by-hacking +- is slow +- is error-prone and fragile +- has an intricate implementation + +This has a lot of terrible consequences, most notably the fact that it is never +clear whether some observed behaviour is a bug or a proper one. + +Following the need of users that start developing huge projects relying +critically on Ltac, we believe that we should offer a proper modern language +that features at least the following: + +- at least informal, predictible semantics +- a typing system +- standard programming facilities (i.e. datatypes) + +This document describes the implementation of such a language. The +implementation of Ltac as of Coq 8.7 will be referred to as Ltac1. + +# General design + +There are various alternatives to Ltac1, such that Mtac or Rtac for instance. +While those alternatives can be quite distinct from Ltac1, we designed +Ltac2 to be closest as reasonably possible to Ltac1, while fixing the +aforementioned defects. + +In particular, Ltac2 is: +- a member of the ML family of languages, i.e. + * a call-by-value functional language + * with effects + * together with Hindley-Milner type system +- a language featuring meta-programming facilities for the manipulation of + Coq-side terms +- a language featuring notation facilities to help writing palatable scripts + +We describe more in details each point in the remainder of this document. + +# ML component + +The call-by-value functional language fragment is easy to implement. + +## Type Syntax + +At the level of terms, we simply elaborate on Ltac1 syntax, which is quite +close to e.g. the one of OCaml. Types follow the simply-typed syntax of OCaml. + +``` +TYPE := +| "(" TYPE₀ "," ... "," TYPEₙ ")" TYPECONST +| "(" TYPE₀ "*" ... "*" TYPEₙ ")" +| TYPE₁ "->" TYPE₂ +| TYPEVAR + +TYPECONST := ( MODPATH "." )* LIDENT + +TYPEVAR := "'" LIDENT + +TYPEPARAMS := "(" TYPEVAR₀ "," ... "," TYPEVARₙ ")" +``` + +The set of base types can be extended thanks to the usual ML type +declarations such as algebraic datatypes and records. + +Built-in types include: +- `int`, machine integers (size not specified, in practice inherited from OCaml) +- `string`, mutable strings +- `'a array`, mutable arrays +- `exn`, exceptions +- `constr`, kernel-side terms +- `pattern`, term patterns +- `ident`, well-formed identifiers + +## Type declarations + +One can define new types by the following commands. + +``` +VERNAC ::= +| "Ltac2" "Type" TYPEPARAMS LIDENT +| "Ltac2" "Type" RECFLAG TYPEPARAMS LIDENT ":=" TYPEDEF + +RECFLAG := ( "rec" ) +``` + +The first command defines an abstract type. It has no use for the end user and +is dedicated to types representing data coming from the OCaml world. + +The second command defines a type with a manifest. There are four possible +kinds of such definitions: alias, variant, record and open variant types. + +``` +TYPEDEF := +| TYPE +| "[" CONSTRUCTORDEF₀ "|" ... "|" CONSTRUCTORDEFₙ "]" +| "{" FIELDDEF₀ ";" ... ";" FIELDDEFₙ "}" +| "[" "..." "]" + +CONSTRUCTORDEF := +| IDENT ( "(" TYPE₀ "," ... "," TYPE₀ ")" ) + +FIELDDEF := +| MUTFLAG IDENT ":" TYPE + +MUTFLAG := ( "mutable" ) +``` + +Aliases are just a name for a given type expression and are transparently +unfoldable to it. They cannot be recursive. + +Variants are sum types defined by constructors and eliminated by +pattern-matching. They can be recursive, but the `RECFLAG` must be explicitly +set. Pattern-maching must be exhaustive. + +Records are product types with named fields and eliminated by projection. +Likewise they can be recursive if the `RECFLAG` is set. + +Open variants are a special kind of variant types whose constructors are not +statically defined, but can instead by extended dynamically. A typical example +is the standard `exn` type. Pattern-matching must always include a catch-all +clause. They can be extended by the following command. + +VERNAC ::= +| "Ltac2" "Type" TYPEPARAMS QUALID ":=" "[" CONSTRUCTORDEF "]" + +## Term Syntax + +The syntax of the functional fragment is very close to the one of Ltac1, except +that it adds a true pattern-matching feature. + +``` +VAR := LIDENT + +QUALID := ( MODPATH "." )* LIDENT + +CONSTRUCTOR := UIDENT + +TERM := +| QUALID +| CONSTRUCTOR TERM₀ ... TERMₙ +| TERM TERM₀ ... TERMₙ +| "fun" VAR "=>" TERM +| "let" VAR ":=" TERM "in" TERM +| "let" "rec" VAR ":=" TERM "in" TERM +| "match" TERM "with" BRANCH* "end" +| INT +| STRING +| "[|" TERM₀ ";" ... ";" TERMₙ "|]" +| "(" TERM₀ "," ... "," TERMₙ ")" +| "{" FIELD+ "}" +| TERM "." "(" QUALID ")" +| TERM₁ "." "(" QUALID ")" ":=" TERM₂ +| "["; TERM₀ ";" ... ";" TERMₙ "]" +| TERM₁ "::" TERM₂ +| ... + +BRANCH := +| PATTERN "=>" TERM + +PATTERN := +| VAR +| "_" +| "(" PATTERN₀ "," ... "," PATTERNₙ ")" +| CONSTRUCTOR PATTERN₀ ... PATTERNₙ +| "[" "]" +| PATTERN₁ "::" PATTERN₂ + +FIELD := +| QUALID ":=" TERM + +``` + +In practice, there is some additional syntactic sugar that allows e.g. to +bind a variable and match on it at the same time, in the usual ML style. + +There is a dedicated syntax for list and array litterals. + +Limitations: for now, deep pattern matching is not implemented yet. + +## Reduction + +We use the usual ML call-by-value reduction, with an otherwise unspecified +evaluation order. + +Note that this is already a departure from Ltac1 which uses heuristic to +decide when evaluating an expression, e.g. the following do not evaluate the +same way. + +``` +foo (idtac; let x := 0 in bar) + +foo (let x := 0 in bar) +``` + +Instead of relying on the `idtac` hack, we would now require an explicit thunk +not to compute the argument, and `foo` would have e.g. type +`(unit -> unit) -> unit`. + +``` +foo (fun () -> let x := 0 in bar) +``` + +## Typing + +Typing is strict and follows Hindley-Milner system. We will not implement the +current hackish subtyping semantics, and one will have to resort to conversion +functions. See notations though to make things more palatable. + +In this setting, all usual argument-free tactics have type `unit -> unit`, but +one can return as well a value of type `τ` thanks to terms of type `unit -> τ`, +or take additional arguments. + +## Effects + +Regarding effects, nothing involved here, except that instead of using the +standard IO monad as the ambient effectful world, Ltac2 is going to use the +tactic monad. + +Note that the order of evaluation of application is *not* specified and is +implementation-dependent, as in OCaml. + +We recall that the `Proofview.tactic` monad is essentially a IO monad together +with backtracking state representing the proof state. + +Intuitively a thunk of type `unit -> 'a` can do the following: +- It can perform non-backtracking IO like printing and setting mutable variables +- It can fail in a non-recoverable way +- It can use first-class backtrack. The proper way to figure that is that we + morally have the following isomorphism: + `(unit -> 'a) ~ unit -> ('a + (exn -> 'a))` i.e. thunks can produce a list + of results waiting for failure exceptions. +- It can access a backtracking proof state, made out amongst other things of + the current evar assignation and the list of goals under focus. + +### Standard IO + +The Ltac2 language features non-backtracking IO, notably mutable data and +printing operations. + +Mutable fields of records can be modified using the set syntax + +### Fatal errors + +The Ltac2 language provides non-backtracking exceptions through the +following primitive in module `Control`. + +``` +val throw : exn -> 'a +``` + +Contrarily to backtracking exceptions from the next section, this kind of error +is never caught by backtracking primitives, that is, throwing an exception +destroys the stack. This is materialized by the following equation, where `E` +is an evaluation context. + +``` +E[throw e] ≡ throw e +``` + +There is currently no way to catch such an exception and it is a design choice. +There might be at some future point a way to catch it in a brutal way, +destroying all backtrack and return values. + +### Backtrack + +In Ltac2, we have the following backtracking primitives, defined in the +`Control` module. + +``` +Ltac2 Type 'a result := [ Val ('a) | Err (exn) ]. + +val zero : exn -> 'a +val plus : (unit -> 'a) -> (exn -> 'a) -> 'a +val case : (unit -> 'a) -> ('a * (exn -> 'a)) result +``` + +If one sees thunks as lazy lists, then `zero` is the empty list and `plus` is +list concatenation, while `case` is pattern-matching. + +The backtracking is first-class, i.e. one can write +`plus "x" (fun () -> "y") : string` producing a backtracking string. + +These operations are expected to satisfy a few equations, most notably that they +form a monoid compatible with sequentialization. + +``` +plus t zero ≡ t () +plus (fun () -> zero e) f ≡ f e +plus (plus t f) g ≡ plus t (fun e -> plus (f e) g) + +case (fun () -> zero e) ≡ Err e +case (fun () -> plus (fun () -> t) f) ≡ Val t f + +let x := zero e in u ≡ fail e +let x := plus t f in u ≡ plus (fun () -> let x := t in u) (fun e -> let x := f e in u) + +(t, u, f, g, e values) +``` + +### Goals + +A goal is given by the data of its conclusion and hypotheses, i.e. it can be +represented as `[Γ ⊢ A]`. + +The tactic monad naturally operates over the whole proofview, which may +represent several goals, including none. Thus, there is no such thing as +*the current goal*. Goals are naturally ordered, though. + +It is natural to do the same in Ltac2, but we must provide a way to get access +to a given goal. This is the role of the `enter` primitive, that applies a +tactic to each currently focussed goal in turn. + +``` +val enter : (unit -> unit) -> unit +``` + +It is guaranteed that when evaluating `enter f`, `f` is called with exactly one +goal under focus. Note that `f` may be called several times, or never, depending +on the number of goals under focus before the call to `enter`. + +A more expressive primitive allows to retrieve the data returned by each tactic +and store it in a list. + +``` +val enter_val : (unit -> 'a) -> 'a list +``` + +Accessing the goal data is then implicit in the Ltac2 primitives, and may fail +if the invariants are not respected. The two essential functions for observing +goals are given below. + +``` +val hyp : ident -> constr +val goal : unit -> constr +``` + +The two above functions fail if there is not exactly one goal under focus. +In addition, `hyp` may also fail if there is no hypothesis with the +corresponding name. + +# Meta-programming + +## Overview + +One of the horrendous implementation issues of Ltac is the fact that it is +never clear whether an object refers to the object world or the meta-world. +This is an incredible source of slowness, as the interpretation must be +aware of bound variables and must use heuristics to decide whether a variable +is a proper one or referring to something in the Ltac context. + +Likewise, in Ltac1, constr parsing is implicit, so that `foo 0` is +not `foo` applied to the Ltac integer expression `0` (Ltac does have a +non-first-class notion of integers), but rather the Coq term `Datatypes.O`. + +We should stop doing that! We need to mark when quoting and unquoting, although +we need to do that in a short and elegant way so as not to be too cumbersome +to the user. + +## Syntax example + +Here is a suggestive example of a reasonable syntax. + +``` +let var := "H" in (* a string *) +let c := << fun $var$ => 0 >> (* the Coq term "fun H => 0" *) +let c' := << let x := $c$ in nat >> (* the Coq term "let x := fun H => 0 in nat" *) +... +``` + +## Term quotation + +### Syntax + +It is better to define primitively the quoting syntax to build terms, as this +is more robust to changes. + +``` +t, u ::= ... | << constr >> +``` + +The `constr` datatype have the same syntax as the usual Coq +terms, except that it also allows antiquotations of the form `$t$` whose type +is statically inferred from the position, e.g. + +``` +<< let $t$ := $u$ >> (** [t] is an ident, [u] is a constr *) +``` + +As the term syntax implicitly allows to inject other classes without marking, +antiquotations can refer explicitly to which class they belong to overcome this +limitation. + +``` +<< $ident:t$ >> (** [t] is an ident, and the corresponding constr is [GVar t] *) +<< $ref:t$ >> (** [t] is a reference, and the corresponding constr is [GRef t] *) +``` + +### Semantics + +Interpretation of a quoted constr is done in two phases, internalization and +evaluation. +- During internalization, variables are resolved and antiquotations are + type-checked as Ltac2 terms, effectively producing a `glob_constr` in Coq + implementation terminology, potentially ill-typed as a Coq term. +- During evaluation, a quoted term is fully evaluated to a kernel term, and is + in particular type-checked in the current environment. + +Internalization is part of the static semantics, i.e. it is done at typing +time, while evaluation is part of the dynamic semantics, i.e. it is done when +a term gets effectively computed. + +#### Static semantics + +The typing rule of a quoted constr is given below, where the `eᵢ` refer to +antiquoted terms. + +``` + Γ ⊢ e₁ : unit Γ ⊢ eₙ : unit +==================================== + Γ ⊢ << c{$e₁$, ..., $eₙ$} >> : constr +``` + +Note that the **static** environment of typing of antiquotations is **not** +expanded by the binders from the term. Namely, it means that the following +expression will **not** type-check. +``` +<< fun x : nat => $exact x$ >> +``` + +There is a simple reason for that, which is that the following expression would +not make sense in general. +``` +<< fun x : nat => $clear x; exact x$ >> +``` + +Rather, the tactic writer has to resort to the **dynamic** environment, and must +write instead something that amounts to the following. +``` +<< fun x : nat => $exact (hyp "x")$ >> +``` + +Obviously, we need to provide syntactic sugar to make this tractable. See the +corresponding section for more details. + +#### Dynamic semantics + +Evaluation of a quoted term is described below. +- The quoted term is evaluated by the pretyper. +- Antiquotations are evaluated in a context where there is exactly one goal +under focus, with the hypotheses coming from the current environment extended +with the bound variables of the term, and the resulting term is fed into the +quoted term. + +Relative orders of evaluation of antiquotations and quoted term is not +specified. + +## Patterns + +Terms can be used in pattern position just as any Ltac constructor. The accepted +syntax is a subset of the constr syntax in Ltac term position, where +antiquotations are variables binding in the right-hand side. + +Constructors and destructors can be derived from this. E.g. the previous +var-manipulating functions can be defined as follows. + +``` +let mkVar : ident -> constr = fun id -> << $ident:id$ >> + +let destVar : constr -> ident = function +| << $ident:x$ >> -> x +| _ -> fail () +``` + +One should be careful in patterns not to mix the syntax for evars with the one +for bound variables. + +The usual match construction from Ltac1 can be derived from those primitive +operations. We should provide syntactic sugar to do so. + +We need to decide how to handle bound variables in antiquotations, both in term +and pattern position. Should they bind? Should they not? What is the semantics +of the following snippet? + +``` +let foo = function << let x := t in $p$ >> -> p +let bar p = << let x := t in $p$ >> +``` + +What about the various kind of constrs? Untyped vs. typed, plus caring about +the context? + +### Lists and Gallina `match` + +It should be possible to manipulate Gallina `match` statements in a relatively +pain-free way. For this reason, there should be a way to match on lists: + +``` +let replace_args = function << $f$ $a1 .. an$ >> + << $g$ $b1 .. bn$ >> + -> << $f$ $b1 .. bn$ >> +let head = function << $f$ $a1 .. an$ >> -> << $f$ >> +let args : constr -> constr list = function << $f$ $a1 .. an$ >> -> [a1 ; .. ; an] +let apply (f : constr) : constr list -> constr = function +| $a1 .. an$ -> << $f$ $a1 .. an$ >> +let complicated_identity v = (let f = head v in let xs = args v in apply f xs) + +let open_term_under_binders = function << fun $a1 .. an$ => $body$ >> -> << $body$ >> +let binders : constr -> ident list = function << fun $a1 .. an$ => $body$ >> -> [a1 ; .. ; an] +let close_term (body : constr) : ident list -> constr = function $a1 .. an$ -> << fun $a1 .. an$ => $body$ >> +let complicated_function_identity v = + let b = open_term_under_binders v in + let xs = binders v in + close_term body xs +``` + +We could implement the `@?P` pattern as something like the desugaring rule: +``` +rule + (match term with + | (@?P a1 .. an)) + ~> + let P = type_check (<< fun $a1 .. an$ => $term$ >>) in ... +``` +The call to `type_check` ensures that there are no remaining holes in the term. +It is, perhaps, overkill. + +Then we could destructure a `match` via syntax like: +``` +let match_to_eta = function +| << match $t$ as $t'$ in $Ty$ return $P$ with + | $c1$ => $v1$ + .. + | $cm$ => $vm$ + end >> + -> << match $t$ in $Ty$ return $Ty$ with + | $c1$ => $c1$ + .. + | $cm$ => $cm$ + end >> +``` +which would take something like `match b with true => 0 | false => 1 end` and +return `match b with true => true | false => false end`. + +We should be able to construct the eliminators for inductive types +in Ltac 2.0, using this syntax to generate the bodies, together with some +primitives for acquiring the relevant types. + + +**Questions**: +- What exactly are the semantics of `..`? +- Should it be `$a1 .. an$` or `$a1$ .. $an$`? +- This syntax suggests that when open terms are used in binding positions, + unbound variables should become binding patterns. That is, if you have + `v` which has been constructed as `<< @cons _ $x$ $xs$ >>`, then + `<< fun ls : list nat => match ls with $v$ => $v$ | _ => nil end >>` should + be the eta-expansion of `ls`. Is this desired semantics? Are there issues + with it? + +# Notations + +Notations are the crux of the usability of Ltac. We should be able to recover +a feeling similar to the old implementation by using and abusing notations. +This would be done at at level totally different from the semantics, which +is not what is happening as of today. + +## Scopes + +We would like to attach some scopes to identifiers, so that it could be possible +to write e.g. + +``` +Ltac intro : string -> unit := ... + +Goal True -> True. +Proof. +intro "H". (** We require the quote here, as this is not a notation *) +Undo. +Top.intro "H". (** An alternative way, by fully qualifying the tactic *) +Abort. + +Tactic Notation "intro" ident(i) := intro i. + +Goal True -> True. +Proof. +intro H. +(** This sequence of tokens is elaborated at parsing time into [Top.intro "H"] + thanks to the above notation. *) +Undo. +Top.intro "H". +(** Here, the core tactic is still reachable using the fully qualified name *) +Abort. +``` + +A typical notation that would be useful is the Coq term one, so that the +following is possible. + +``` +Ltac destruct : constr -> unit := ... + +Tactic Notation "destruct" constr(x) := destruct x. + +Goal False -> True. +Proof. +intro H. (** assuming we have the previous notation in scope *) +destruct H. (** H is interpreted in the current goal? *) +Undo. +Top.destruct << H >> (** alternative without notation *) +``` + +Another one, probably useful for transition, would be a scope `legacy_constr` +that parses an identifier s.t. `legacy_constr(H)` elaborates to +`hyp H + mkVar H`. + +One should be able to define new scopes, by giving them a qualified name, +a old scope used for the parsing rule, and an expansion macro. We can maybe +unify such a scope creation process with the tactic notation one? + +## Syntactic sugar + +A few dedicated syntaxes should be built-in into Ltac2 for easy manipulation +of Coq-specific data. + +### Identifiers + +We need to write identifiers as easily as strings. What about `#foo` standing +for the identifier `foo`? + +### Hypotheses + +We need to be able to access easily a hypothesis from its name. What about +`` `foo `` being a shorthand for `hyp "foo"`? This needs to be accessible inside +terms as well. + +# Transition path + +TODO -- cgit v1.2.3 From 60e581f6fbcf033e134291016351492d9df7e319 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 1 Aug 2017 02:01:09 +0200 Subject: Fixup doc --- doc/ltac2.md | 2 ++ 1 file changed, 2 insertions(+) (limited to 'doc') diff --git a/doc/ltac2.md b/doc/ltac2.md index 38a56d3d6b..e2aa4cfb3b 100644 --- a/doc/ltac2.md +++ b/doc/ltac2.md @@ -126,8 +126,10 @@ statically defined, but can instead by extended dynamically. A typical example is the standard `exn` type. Pattern-matching must always include a catch-all clause. They can be extended by the following command. +``` VERNAC ::= | "Ltac2" "Type" TYPEPARAMS QUALID ":=" "[" CONSTRUCTORDEF "]" +``` ## Term Syntax -- cgit v1.2.3 From 21087463e0a14bd101e01683c6dd7850fcccb395 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 1 Aug 2017 02:03:30 +0200 Subject: Fixup doc --- doc/ltac2.md | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'doc') diff --git a/doc/ltac2.md b/doc/ltac2.md index e2aa4cfb3b..abd5493cec 100644 --- a/doc/ltac2.md +++ b/doc/ltac2.md @@ -263,6 +263,8 @@ is an evaluation context. ``` E[throw e] ≡ throw e + +(e value) ``` There is currently no way to catch such an exception and it is a design choice. @@ -286,7 +288,7 @@ If one sees thunks as lazy lists, then `zero` is the empty list and `plus` is list concatenation, while `case` is pattern-matching. The backtracking is first-class, i.e. one can write -`plus "x" (fun () -> "y") : string` producing a backtracking string. +`plus "x" (fun () => "y") : string` producing a backtracking string. These operations are expected to satisfy a few equations, most notably that they form a monoid compatible with sequentialization. @@ -299,7 +301,7 @@ plus (plus t f) g ≡ plus t (fun e -> plus (f e) g) case (fun () -> zero e) ≡ Err e case (fun () -> plus (fun () -> t) f) ≡ Val t f -let x := zero e in u ≡ fail e +let x := zero e in u ≡ zero e let x := plus t f in u ≡ plus (fun () -> let x := t in u) (fun e -> let x := f e in u) (t, u, f, g, e values) -- cgit v1.2.3 From 7cd31681eb5e3ccc7e7e920bb7eebe92827f6b16 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 1 Aug 2017 11:37:45 +0200 Subject: More in documentation. --- doc/ltac2.md | 385 ++++++++++++++++++++++++++--------------------------------- 1 file changed, 167 insertions(+), 218 deletions(-) (limited to 'doc') diff --git a/doc/ltac2.md b/doc/ltac2.md index abd5493cec..fee19e5df0 100644 --- a/doc/ltac2.md +++ b/doc/ltac2.md @@ -185,6 +185,20 @@ There is a dedicated syntax for list and array litterals. Limitations: for now, deep pattern matching is not implemented yet. +## Ltac Definitions + +One can define a new global Ltac2 value using the following syntax. +``` +VERNAC ::= +| "Ltac2" RECFLAG LIDENT ":=" TERM +``` + +For semantic reasons, the body of the Ltac2 definition must be a syntactical +value, i.e. a function, a constant or a pure constructor recursively applied to +values. + +If the `RECFLAG` is set, the tactic is expanded into a recursive binding. + ## Reduction We use the usual ML call-by-value reduction, with an otherwise unspecified @@ -235,8 +249,8 @@ Intuitively a thunk of type `unit -> 'a` can do the following: - It can fail in a non-recoverable way - It can use first-class backtrack. The proper way to figure that is that we morally have the following isomorphism: - `(unit -> 'a) ~ unit -> ('a + (exn -> 'a))` i.e. thunks can produce a list - of results waiting for failure exceptions. + `(unit -> 'a) ~ (unit -> exn + ('a * (exn -> 'a)))` i.e. thunks can produce a + lazy list of results where each tail is waiting for a continuation exception. - It can access a backtracking proof state, made out amongst other things of the current evar assignation and the list of goals under focus. @@ -245,7 +259,12 @@ Intuitively a thunk of type `unit -> 'a` can do the following: The Ltac2 language features non-backtracking IO, notably mutable data and printing operations. -Mutable fields of records can be modified using the set syntax +Mutable fields of records can be modified using the set syntax. Likewise, +built-in types like `string` and `array` feature imperative assignment. See +modules `String` and `Array` respectively. + +A few printing primitives are provided in the `Message` module, allowing to +display information to the user. ### Fatal errors @@ -328,14 +347,7 @@ It is guaranteed that when evaluating `enter f`, `f` is called with exactly one goal under focus. Note that `f` may be called several times, or never, depending on the number of goals under focus before the call to `enter`. -A more expressive primitive allows to retrieve the data returned by each tactic -and store it in a list. - -``` -val enter_val : (unit -> 'a) -> 'a list -``` - -Accessing the goal data is then implicit in the Ltac2 primitives, and may fail +Accessing the goal data is then implicit in the Ltac2 primitives, and may panic if the invariants are not respected. The two essential functions for observing goals are given below. @@ -344,7 +356,7 @@ val hyp : ident -> constr val goal : unit -> constr ``` -The two above functions fail if there is not exactly one goal under focus. +The two above functions panic if there is not exactly one goal under focus. In addition, `hyp` may also fail if there is no hypothesis with the corresponding name. @@ -366,94 +378,106 @@ We should stop doing that! We need to mark when quoting and unquoting, although we need to do that in a short and elegant way so as not to be too cumbersome to the user. -## Syntax example - -Here is a suggestive example of a reasonable syntax. +## Generic Syntax for Quotations +In general, quotations can be introduced in term by the following syntax, where +`QUOTENTRY` is some parsing entry. ``` -let var := "H" in (* a string *) -let c := << fun $var$ => 0 >> (* the Coq term "fun H => 0" *) -let c' := << let x := $c$ in nat >> (* the Coq term "let x := fun H => 0 in nat" *) -... +TERM ::= +| QUOTNAME ":" "(" QUOTENTRY ")" + +QUOTNAME := IDENT ``` -## Term quotation +The current implementation recognizes the following built-in quotations: +- "ident", which parses identifiers (type `Init.ident`). +- "constr", which parses Coq terms and produces an-evar free term at runtime + (type `Init.constr`). +- "open_constr", which parses Coq terms and produces a term potentially with + holes at runtime (type `Init.constr` as well). +- "pattern", which parses Coq patterns and produces a pattern used for term + matching (type `Init.pattern`). -### Syntax +The following syntactic sugar is provided for two common cases. +- `@id` is the same as ident:(id) +- `'t` is the same as open_constr:(t) -It is better to define primitively the quoting syntax to build terms, as this -is more robust to changes. +## Term Antiquotations -``` -t, u ::= ... | << constr >> -``` +### Syntax -The `constr` datatype have the same syntax as the usual Coq -terms, except that it also allows antiquotations of the form `$t$` whose type -is statically inferred from the position, e.g. +One can also insert Ltac2 code into Coq term, similarly to what was possible in +Ltac1. ``` -<< let $t$ := $u$ >> (** [t] is an ident, [u] is a constr *) +COQCONSTR ::= +| "ltac2" ":" "(" TERM ")" ``` -As the term syntax implicitly allows to inject other classes without marking, -antiquotations can refer explicitly to which class they belong to overcome this -limitation. - -``` -<< $ident:t$ >> (** [t] is an ident, and the corresponding constr is [GVar t] *) -<< $ref:t$ >> (** [t] is a reference, and the corresponding constr is [GRef t] *) -``` +Antiquoted terms are expected to have type `unit`, as they are only evaluated +for their side-effects. ### Semantics -Interpretation of a quoted constr is done in two phases, internalization and +Interpretation of a quoted Coq term is done in two phases, internalization and evaluation. -- During internalization, variables are resolved and antiquotations are - type-checked as Ltac2 terms, effectively producing a `glob_constr` in Coq - implementation terminology, potentially ill-typed as a Coq term. -- During evaluation, a quoted term is fully evaluated to a kernel term, and is - in particular type-checked in the current environment. -Internalization is part of the static semantics, i.e. it is done at typing -time, while evaluation is part of the dynamic semantics, i.e. it is done when -a term gets effectively computed. +- Internalization is part of the static semantics, i.e. it is done at Ltac2 + typing time. +- Evaluation is part of the dynamic semantics, i.e. it is done when + a term gets effectively computed by Ltac2. #### Static semantics -The typing rule of a quoted constr is given below, where the `eᵢ` refer to -antiquoted terms. +During internalization, Coq variables are resolved and antiquotations are +type-checked as Ltac2 terms, effectively producing a `glob_constr` in Coq +implementation terminology. Note that although it went through the +type-checking of *Ltac2*, the resulting term has not been fully computed and +is potentially ill-typed as a Coq term. ``` - Γ ⊢ e₁ : unit Γ ⊢ eₙ : unit -==================================== - Γ ⊢ << c{$e₁$, ..., $eₙ$} >> : constr +Ltac2 Definition myconstr () := constr:(nat -> 0). +// Valid with type `unit -> constr`, but will fail at runtime. ``` -Note that the **static** environment of typing of antiquotations is **not** -expanded by the binders from the term. Namely, it means that the following +Term antiquotations are type-checked in the enclosing Ltac2 typing context +of the corresponding term expression. For instance, the following with +type-check. + +``` +let x := '0 in constr:(1 + ltac2:(exact x)) +// type constr +``` + +Beware that the typing environment of typing of antiquotations is **not** +expanded by the Coq binders from the term. Namely, it means that the following expression will **not** type-check. ``` -<< fun x : nat => $exact x$ >> +constr:(fun x : nat => ltac2:(exact x)) +// Error: Unbound variable 'x' ``` There is a simple reason for that, which is that the following expression would not make sense in general. ``` -<< fun x : nat => $clear x; exact x$ >> +constr:(fun x : nat => ltac2:(clear @x; exact x)) ``` -Rather, the tactic writer has to resort to the **dynamic** environment, and must -write instead something that amounts to the following. +Rather, the tactic writer has to resort to the **dynamic** goal environment, +and must write instead explicitly that she is accessing a hypothesis, typically +as follows. ``` -<< fun x : nat => $exact (hyp "x")$ >> +constr:(fun x : nat => ltac2:(hyp @x)) ``` -Obviously, we need to provide syntactic sugar to make this tractable. See the -corresponding section for more details. +The `ltac2:(hyp @x)` pattern is so common that we provide a dedicated Coq +term notation for it. #### Dynamic semantics +During evaluation, a quoted term is fully evaluated to a kernel term, and is +in particular type-checked in the current environment. + Evaluation of a quoted term is described below. - The quoted term is evaluated by the pretyper. - Antiquotations are evaluated in a context where there is exactly one goal @@ -464,183 +488,108 @@ quoted term. Relative orders of evaluation of antiquotations and quoted term is not specified. -## Patterns - -Terms can be used in pattern position just as any Ltac constructor. The accepted -syntax is a subset of the constr syntax in Ltac term position, where -antiquotations are variables binding in the right-hand side. - -Constructors and destructors can be derived from this. E.g. the previous -var-manipulating functions can be defined as follows. - +For instance, in the following example, `tac` will be evaluated in a context +with exactly one goal under focus, whose last hypothesis is `H : nat`. The +whole expression will thus evaluate to the term `fun H : nat => nat`. ``` -let mkVar : ident -> constr = fun id -> << $ident:id$ >> - -let destVar : constr -> ident = function -| << $ident:x$ >> -> x -| _ -> fail () +let tac () := hyp @H in constr:(fun H : nat => ltac2:(tac ())) ``` -One should be careful in patterns not to mix the syntax for evars with the one -for bound variables. - -The usual match construction from Ltac1 can be derived from those primitive -operations. We should provide syntactic sugar to do so. - -We need to decide how to handle bound variables in antiquotations, both in term -and pattern position. Should they bind? Should they not? What is the semantics -of the following snippet? - -``` -let foo = function << let x := t in $p$ >> -> p -let bar p = << let x := t in $p$ >> -``` +Many standard tactics perform type-checking of their argument before going +further. It is your duty to ensure that terms are well-typed when calling +such tactics. Failure to do so will result in non-recoverable exceptions. -What about the various kind of constrs? Untyped vs. typed, plus caring about -the context? - -### Lists and Gallina `match` - -It should be possible to manipulate Gallina `match` statements in a relatively -pain-free way. For this reason, there should be a way to match on lists: - -``` -let replace_args = function << $f$ $a1 .. an$ >> - << $g$ $b1 .. bn$ >> - -> << $f$ $b1 .. bn$ >> -let head = function << $f$ $a1 .. an$ >> -> << $f$ >> -let args : constr -> constr list = function << $f$ $a1 .. an$ >> -> [a1 ; .. ; an] -let apply (f : constr) : constr list -> constr = function -| $a1 .. an$ -> << $f$ $a1 .. an$ >> -let complicated_identity v = (let f = head v in let xs = args v in apply f xs) - -let open_term_under_binders = function << fun $a1 .. an$ => $body$ >> -> << $body$ >> -let binders : constr -> ident list = function << fun $a1 .. an$ => $body$ >> -> [a1 ; .. ; an] -let close_term (body : constr) : ident list -> constr = function $a1 .. an$ -> << fun $a1 .. an$ => $body$ >> -let complicated_function_identity v = - let b = open_term_under_binders v in - let xs = binders v in - close_term body xs -``` - -We could implement the `@?P` pattern as something like the desugaring rule: -``` -rule - (match term with - | (@?P a1 .. an)) - ~> - let P = type_check (<< fun $a1 .. an$ => $term$ >>) in ... -``` -The call to `type_check` ensures that there are no remaining holes in the term. -It is, perhaps, overkill. - -Then we could destructure a `match` via syntax like: -``` -let match_to_eta = function -| << match $t$ as $t'$ in $Ty$ return $P$ with - | $c1$ => $v1$ - .. - | $cm$ => $vm$ - end >> - -> << match $t$ in $Ty$ return $Ty$ with - | $c1$ => $c1$ - .. - | $cm$ => $cm$ - end >> -``` -which would take something like `match b with true => 0 | false => 1 end` and -return `match b with true => true | false => false end`. - -We should be able to construct the eliminators for inductive types -in Ltac 2.0, using this syntax to generate the bodies, together with some -primitives for acquiring the relevant types. +## Patterns +Terms can be used in pattern position just as any Ltac constructor. The accepted +syntax is a subset of the constr syntax in Ltac term position. It does not +allow antiquotations. -**Questions**: -- What exactly are the semantics of `..`? -- Should it be `$a1 .. an$` or `$a1$ .. $an$`? -- This syntax suggests that when open terms are used in binding positions, - unbound variables should become binding patterns. That is, if you have - `v` which has been constructed as `<< @cons _ $x$ $xs$ >>`, then - `<< fun ls : list nat => match ls with $v$ => $v$ | _ => nil end >>` should - be the eta-expansion of `ls`. Is this desired semantics? Are there issues - with it? +Patterns quotations are typically used with the matching functions provided +in the `Pattern` module. # Notations -Notations are the crux of the usability of Ltac. We should be able to recover +Notations are the crux of the usability of Ltac1. We should be able to recover a feeling similar to the old implementation by using and abusing notations. -This would be done at at level totally different from the semantics, which -is not what is happening as of today. ## Scopes -We would like to attach some scopes to identifiers, so that it could be possible -to write e.g. +A scope is a name given to a grammar entry used to produce some Ltac2 expression +at parsing time. Scopes are described using a form of S-expression. ``` -Ltac intro : string -> unit := ... - -Goal True -> True. -Proof. -intro "H". (** We require the quote here, as this is not a notation *) -Undo. -Top.intro "H". (** An alternative way, by fully qualifying the tactic *) -Abort. - -Tactic Notation "intro" ident(i) := intro i. - -Goal True -> True. -Proof. -intro H. -(** This sequence of tokens is elaborated at parsing time into [Top.intro "H"] - thanks to the above notation. *) -Undo. -Top.intro "H". -(** Here, the core tactic is still reachable using the fully qualified name *) -Abort. +SCOPE := +| STRING +| INT +| LIDENT ( "(" SCOPE₀ "," ... "," SCOPEₙ ")" ) +``` + +A few scopes contain antiquotation features. For sake of uniformity, all +antiquotations are introduced by the syntax `"$" VAR`. + +The following scopes are built-in. +- constr: + + parses `c = COQCONSTR` and produces `constr:(c)` +- ident: + + parses `id = IDENT` and produces `ident:(id)` + + parses `"$" (x = IDENT)` and produces the variable `x` +- list0(*scope*): + + if *scope* parses `ENTRY`, parses ̀`(x₀, ..., xₙ = ENTRY*)` and produces + `[x₀; ...; xₙ]`. +- list0(*scope*, sep = STRING): + + if *scope* parses `ENTRY`, parses `(x₀ = ENTRY, "sep", ..., "sep", xₙ = ENTRY)` + and produces `[x₀; ...; xₙ]`. +- list1: same as list0 (with or without separator) but parses `ENTRY+` instead + of `ENTRY*`. +- opt(*scope*) + + if *scope* parses `ENTRY`, parses `ENTRY?` and produces either `None` or + `Some x` where `x` is the parsed expression. +- self: + + parses a Ltac2 expression at the current level and return it as is. +- next: + + parses a Ltac2 expression at the next level and return it as is. +- tactic(n = INT): + + parses a Ltac2 expression at the provided level *n* and return it as is. +- thunk(*scope*): + parses the same as *scope*, and if *e* is the parsed expression, returns + `fun () => e`. + +For now there is no way to declare new scopes from Ltac2 side, but this is +planned. + +## Notations + +The Ltac2 parser can be extended by syntactic notations. ``` +VERNAC ::= +| "Ltac2" "Notation" TOKEN+ LEVEL? ":=" TERM -A typical notation that would be useful is the Coq term one, so that the -following is possible. +LEVEL := ":" INT +TOKEN := +| VAR "(" SCOPE ")" +| STRING ``` -Ltac destruct : constr -> unit := ... -Tactic Notation "destruct" constr(x) := destruct x. +A Ltac2 notation adds a parsing rule to the Ltac2 grammar, which is expanded +to the provided body where every token from the notation is let-bound to the +corresponding generated expression. -Goal False -> True. -Proof. -intro H. (** assuming we have the previous notation in scope *) -destruct H. (** H is interpreted in the current goal? *) -Undo. -Top.destruct << H >> (** alternative without notation *) +For instance, assume we perform: +``` +Ltac2 Notation "foo" c(thunk(constr)) ids(list0(ident)) := Bar.f c ids. +``` +Then the following expression +``` +let y := @X in foo (nat -> nat) x ?y +``` +will expand at parsing time to +``` +let y := @X in +let c := fun () => constr:(nat -> nat) with ids := [@x; y] in Bar.f c ids ``` -Another one, probably useful for transition, would be a scope `legacy_constr` -that parses an identifier s.t. `legacy_constr(H)` elaborates to -`hyp H + mkVar H`. - -One should be able to define new scopes, by giving them a qualified name, -a old scope used for the parsing rule, and an expansion macro. We can maybe -unify such a scope creation process with the tactic notation one? - -## Syntactic sugar - -A few dedicated syntaxes should be built-in into Ltac2 for easy manipulation -of Coq-specific data. - -### Identifiers - -We need to write identifiers as easily as strings. What about `#foo` standing -for the identifier `foo`? - -### Hypotheses - -We need to be able to access easily a hypothesis from its name. What about -`` `foo `` being a shorthand for `hyp "foo"`? This needs to be accessible inside -terms as well. - -# Transition path - -TODO +Beware that the order of evaluation of multiple let-bindings is not specified, +so that you may have to resort to thunking to ensure that side-effects are +performed at the right time. -- cgit v1.2.3 From 30fc910b01f61ce3691ed63a0908c1c60cee76dd Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 1 Aug 2017 16:46:29 +0200 Subject: Fix documentation. --- doc/ltac2.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'doc') diff --git a/doc/ltac2.md b/doc/ltac2.md index fee19e5df0..7a3b2181f8 100644 --- a/doc/ltac2.md +++ b/doc/ltac2.md @@ -467,11 +467,11 @@ Rather, the tactic writer has to resort to the **dynamic** goal environment, and must write instead explicitly that she is accessing a hypothesis, typically as follows. ``` -constr:(fun x : nat => ltac2:(hyp @x)) +constr:(fun x : nat => ltac2:(exact (hyp @x))) ``` -The `ltac2:(hyp @x)` pattern is so common that we provide a dedicated Coq -term notation for it. +The `ltac2:(exact (hyp @x))` pattern is so common that we provide dedicated +Ltac2 and Coq term notations for it. #### Dynamic semantics -- cgit v1.2.3 From ea782d757d57dc31be9714edc607128c5c127205 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 2 Aug 2017 14:14:14 +0200 Subject: Extending the set of tactic scopes. We now allow mere tokens, keywords and sequencing amongst others. --- doc/ltac2.md | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/ltac2.md b/doc/ltac2.md index 7a3b2181f8..12687e9aff 100644 --- a/doc/ltac2.md +++ b/doc/ltac2.md @@ -552,8 +552,19 @@ The following scopes are built-in. - tactic(n = INT): + parses a Ltac2 expression at the provided level *n* and return it as is. - thunk(*scope*): - parses the same as *scope*, and if *e* is the parsed expression, returns + + parses the same as *scope*, and if *e* is the parsed expression, returns `fun () => e`. +- STRING: + + parses the corresponding string as a CAMLP5 IDENT and returns `()`. +- keyword(s = STRING): + + parses the string *s* as a keyword and returns `()`. +- terminal(s = STRING): + + parses the string *s* as a keyword, if it is already a + keyword, otherwise as an IDENT. Returns `()`. +- seq(*scope₁*, ..., *scopeₙ*): + + parses *scope₁*, ..., *scopeₙ* in this order, and produces a n-tuple made + out of the parsed values in the same order. It is forbidden for the various + subscopes to refer to the global entry using self of next. For now there is no way to declare new scopes from Ltac2 side, but this is planned. -- cgit v1.2.3 From d755c546a5c260232fd30971bd604b078d0afc18 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 2 Aug 2017 17:31:13 +0200 Subject: Properly implementing the notation to easily access hypotheses. --- doc/ltac2.md | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'doc') diff --git a/doc/ltac2.md b/doc/ltac2.md index 12687e9aff..bf6d9eb583 100644 --- a/doc/ltac2.md +++ b/doc/ltac2.md @@ -470,8 +470,12 @@ as follows. constr:(fun x : nat => ltac2:(exact (hyp @x))) ``` -The `ltac2:(exact (hyp @x))` pattern is so common that we provide dedicated -Ltac2 and Coq term notations for it. +This pattern is so common that we provide dedicated Ltac2 and Coq term notations +for it. + +- `&x` as an Ltac2 expression expands to `hyp @x`. +- `&x` as an Coq constr expression expands to + `ltac2:(refine (fun () => hyp @x))`. #### Dynamic semantics -- cgit v1.2.3 From 899476fa3dd2ae22f433a70fb860df0510a7ac88 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 2 Aug 2017 18:02:01 +0200 Subject: Expanding documentation. --- doc/ltac2.md | 78 ++++++++++++++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 65 insertions(+), 13 deletions(-) (limited to 'doc') diff --git a/doc/ltac2.md b/doc/ltac2.md index bf6d9eb583..20b043ea0b 100644 --- a/doc/ltac2.md +++ b/doc/ltac2.md @@ -44,7 +44,34 @@ We describe more in details each point in the remainder of this document. # ML component -The call-by-value functional language fragment is easy to implement. +## Overview + +Ltac2 is a member of the ML family of languages, in the sense that it is an +effectful call-by-value functional language, with static typing à la +Hindley-Milner. It is commonly accepted that ML constitutes a sweet spot in PL +design, as it is relatively expressive while not being either too lax +(contrarily to dynamic typing) nor too strict (contrarily to say, dependent +types). + +The main goal of Ltac2 is to serve as a meta-language for Coq. As such, it +naturally fits in the ML lineage, just as the historical ML was designed as +the tactic language for the LCF prover. It can also be seen as a general-purpose +language, by simply forgetting about the Coq-specific features. + +Sticking to a standard ML type system can be considered somewhat weak for a +meta-language designed to manipulate Coq terms. In particular, there is no +way to statically guarantee that a Coq term resulting from an Ltac2 +computation will be well-typed. This is actually a design choice, motivated +by retro-compatibility with Ltac1. Instead, well-typedness is deferred to +dynamic checks, allowing many primitive functions to fail whenever they are +provided with an ill-typed term. + +The language is naturally effectful as it manipulates the global state of the +proof engine. This allows to think of proof-modifying primitives as effects +in a straightforward way. Semantically, proof manipulation lives in a monad, +which allows to ensure that Ltac2 satisfies the same equations as a generic ML +with unspecified effects would do, e.g. function reduction is substitution +by a value. ## Type Syntax @@ -134,7 +161,8 @@ VERNAC ::= ## Term Syntax The syntax of the functional fragment is very close to the one of Ltac1, except -that it adds a true pattern-matching feature. +that it adds a true pattern-matching feature, as well as a few standard +constructions from ML. ``` VAR := LIDENT @@ -202,11 +230,21 @@ If the `RECFLAG` is set, the tactic is expanded into a recursive binding. ## Reduction We use the usual ML call-by-value reduction, with an otherwise unspecified -evaluation order. +evaluation order. This is a design choice making it compatible with OCaml, +if ever we implement native compilation. The expected equations are as follows. +``` +(fun x => t) V ≡ t{x := V} (βv) -Note that this is already a departure from Ltac1 which uses heuristic to -decide when evaluating an expression, e.g. the following do not evaluate the -same way. +let x := V in t ≡ t{x := V} (let) + +match C V₀ ... Vₙ with ... | C x₀ ... xₙ => t | ... end ≡ t {xᵢ := Vᵢ} (ι) + +(t any term, V values, C constructor) +``` + +Note that call-by-value reduction is already a departure from Ltac1 which uses +heuristics to decide when evaluating an expression. For instance, the following +expressions do not evaluate the same way in Ltac1. ``` foo (idtac; let x := 0 in bar) @@ -229,7 +267,7 @@ current hackish subtyping semantics, and one will have to resort to conversion functions. See notations though to make things more palatable. In this setting, all usual argument-free tactics have type `unit -> unit`, but -one can return as well a value of type `τ` thanks to terms of type `unit -> τ`, +one can return as well a value of type `t` thanks to terms of type `unit -> t`, or take additional arguments. ## Effects @@ -254,6 +292,8 @@ Intuitively a thunk of type `unit -> 'a` can do the following: - It can access a backtracking proof state, made out amongst other things of the current evar assignation and the list of goals under focus. +We describe more thoroughly the various effects existing in Ltac2 hereafter. + ### Standard IO The Ltac2 language features non-backtracking IO, notably mutable data and @@ -427,13 +467,16 @@ evaluation. - Evaluation is part of the dynamic semantics, i.e. it is done when a term gets effectively computed by Ltac2. +Remark that typing of Coq terms is a *dynamic* process occuring at Ltac2 +evaluation time, and not at Ltac2 typing time. + #### Static semantics During internalization, Coq variables are resolved and antiquotations are type-checked as Ltac2 terms, effectively producing a `glob_constr` in Coq implementation terminology. Note that although it went through the -type-checking of *Ltac2*, the resulting term has not been fully computed and -is potentially ill-typed as a Coq term. +type-checking of **Ltac2**, the resulting term has not been fully computed and +is potentially ill-typed as a runtime **Coq** term. ``` Ltac2 Definition myconstr () := constr:(nat -> 0). @@ -451,7 +494,7 @@ let x := '0 in constr:(1 + ltac2:(exact x)) Beware that the typing environment of typing of antiquotations is **not** expanded by the Coq binders from the term. Namely, it means that the following -expression will **not** type-check. +Ltac2 expression will **not** type-check. ``` constr:(fun x : nat => ltac2:(exact x)) // Error: Unbound variable 'x' @@ -462,6 +505,8 @@ not make sense in general. ``` constr:(fun x : nat => ltac2:(clear @x; exact x)) ``` +Indeed, a hypothesis can suddenly disappear from the runtime context if some +other tactic pulls the rug from under you. Rather, the tactic writer has to resort to the **dynamic** goal environment, and must write instead explicitly that she is accessing a hypothesis, typically @@ -482,9 +527,9 @@ for it. During evaluation, a quoted term is fully evaluated to a kernel term, and is in particular type-checked in the current environment. -Evaluation of a quoted term is described below. -- The quoted term is evaluated by the pretyper. -- Antiquotations are evaluated in a context where there is exactly one goal +Evaluation of a quoted term goes as follows. +- The quoted term is first evaluated by the pretyper. +- Antiquotations are then evaluated in a context where there is exactly one goal under focus, with the hypotheses coming from the current environment extended with the bound variables of the term, and the resulting term is fed into the quoted term. @@ -608,3 +653,10 @@ let c := fun () => constr:(nat -> nat) with ids := [@x; y] in Bar.f c ids Beware that the order of evaluation of multiple let-bindings is not specified, so that you may have to resort to thunking to ensure that side-effects are performed at the right time. + +# TODO + +- Implement deep pattern-matching. +- Implement compatibility layer with Ltac1 +- Craft an expressive set of primitive functions +- Implement native compilation to OCaml -- cgit v1.2.3 From 6e150eb19a55b16bbd4ea03964ee48f2d69084ed Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 2 Aug 2017 18:44:03 +0200 Subject: Typo in documentation. --- doc/ltac2.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/ltac2.md b/doc/ltac2.md index 20b043ea0b..c2d930c9b6 100644 --- a/doc/ltac2.md +++ b/doc/ltac2.md @@ -642,7 +642,7 @@ Ltac2 Notation "foo" c(thunk(constr)) ids(list0(ident)) := Bar.f c ids. ``` Then the following expression ``` -let y := @X in foo (nat -> nat) x ?y +let y := @X in foo (nat -> nat) x $y ``` will expand at parsing time to ``` -- cgit v1.2.3 From 77150cc524f5cbdc9bf340be03f31e7f7542c98d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 5 Aug 2017 17:14:21 +0200 Subject: Introducing grammar-free tactic notations. --- doc/ltac2.md | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) (limited to 'doc') diff --git a/doc/ltac2.md b/doc/ltac2.md index c2d930c9b6..b3596b2977 100644 --- a/doc/ltac2.md +++ b/doc/ltac2.md @@ -654,6 +654,38 @@ Beware that the order of evaluation of multiple let-bindings is not specified, so that you may have to resort to thunking to ensure that side-effects are performed at the right time. +## Abbreviations + +There exists a special kind of notations, called abbreviations, that is designed +so that it does not add any parsing rules. It is similar in spirit to Coq +abbreviations, insofar as its main purpose is to give an absolute name to a +piece of pure syntax, which can be transparently referred by this name as if it +were a proper definition. Abbreviations are introduced by the following +syntax. + +``` +VERNAC ::= +| "Ltac2" "Notation" IDENT ":=" TERM +``` + +The abbreviation can then be manipulated just as a normal Ltac2 definition, +except that it is expanded at internalization time into the given expression. +Furthermore, in order to make this kind of construction useful in practice in +an effectful language such as Ltac2, any syntactic argument to an abbreviation +is thunked on-the-fly during its expansion. + +For instance, suppose that we define the following. +``` +Ltac2 Notation foo := fun x => x (). +``` +Then we have the following expansion at internalization time. +``` +foo 0 ↦ (fun x => x ()) (fun _ => 0) +``` + +Note that abbreviations are not typechecked at all, and may result in typing +errors after expansion. + # TODO - Implement deep pattern-matching. -- cgit v1.2.3 From 7d496e618f35a17b8432ac3c7205138f03c95fd2 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 24 Aug 2017 14:58:46 +0200 Subject: Introducing a quotation for global references. --- doc/ltac2.md | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'doc') diff --git a/doc/ltac2.md b/doc/ltac2.md index b3596b2977..6c4912c8f3 100644 --- a/doc/ltac2.md +++ b/doc/ltac2.md @@ -437,6 +437,10 @@ The current implementation recognizes the following built-in quotations: holes at runtime (type `Init.constr` as well). - "pattern", which parses Coq patterns and produces a pattern used for term matching (type `Init.pattern`). +- "reference", which parses either a `QUALID` or `"&" IDENT`. Qualified names + are globalized at internalization into the corresponding global reference, + while `&id` is turned into `Std.VarRef id`. This produces at runtime a + `Std.reference`. The following syntactic sugar is provided for two common cases. - `@id` is the same as ident:(id) -- cgit v1.2.3 From 7cd041b42588e6d9ff0e5ea127960585666c4b07 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 24 Aug 2017 17:54:28 +0200 Subject: Documentation about the transition from Ltac1. --- doc/ltac2.md | 106 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 106 insertions(+) (limited to 'doc') diff --git a/doc/ltac2.md b/doc/ltac2.md index 6c4912c8f3..55780a7712 100644 --- a/doc/ltac2.md +++ b/doc/ltac2.md @@ -690,6 +690,112 @@ foo 0 ↦ (fun x => x ()) (fun _ => 0) Note that abbreviations are not typechecked at all, and may result in typing errors after expansion. +# Transition from Ltac1 + +Owing to the use of a bunch of notations, the transition shouldn't be +atrociously horrible and shockingly painful up to the point you want to retire +in the Ariège mountains, living off the land and insulting careless bypassers in +proto-georgian. + +That said, we do *not* guarantee you it is going to be a blissful walk either. +Hopefully, owing to the fact Ltac2 is typed, the interactive dialogue with Coq +will help you. + +We list the major changes and the transition strategies hereafter. + +## Syntax changes + +Due to conflicts, a few syntactic rules have changed. + +- The dispatch tactical `tac; [foo|bar]` is now written `tac > [foo|bar]`. +- Levels of a few operators have been revised. Some tacticals now parse as if + they were a normal function, i.e. one has to put parentheses around the + argument when it is complex, e.g an abstraction. List of affected tacticals: + `try`, `repeat`, `do`, `once`, `progress`, `time`, `abstract`. +- `idtac` is no more. Either use `()` if you expect nothing to happen, + `(fun () => ())` if you want a thunk (see next section), or use printing + primitives from the `Message` module if you wand to display something. + +## Tactic delay + +Tactics are not magically delayed anymore, neither as functions nor as +arguments. It is your responsibility to thunk them beforehand and apply them +at the call site. + +A typical example of a delayed function: +``` +Ltac foo := blah. +``` +becomes +``` +Ltac2 foo () := blah. +``` + +All subsequent calls to `foo` must be applied to perform the same effect as +before. + +Likewise, for arguments: +``` +Ltac bar tac := tac; tac; tac. +``` +becomes +``` +Ltac2 bar tac := tac (); tac (); tac (). +``` + +We recommend the use of syntactic notations to ease the transition. For +instance, the first example can alternatively written as: +``` +Ltac2 foo0 () := blah. +Ltac2 Notation foo := foo0 (). +``` + +This allows to keep the subsequent calls to the tactic as-is, as the +expression `foo` will be implicitly expanded everywhere into `foo0 ()`. Such +a trick also works for arguments, as arguments of syntactic notations are +implicitly thunked. The second example could thus be written as follows. + +``` +Ltac2 bar0 tac := tac (); tac (); tac (). +Ltac2 Notation bar := bar0. +``` + +## Variable binding + +Ltac1 relies on a crazy amount of dynamic trickery to be able to tell apart +bound variables from terms, hypotheses and whatnot. There is no such thing in +Ltac2, as variables are recognized statically and other constructions do not +live in the same syntactic world. Due to the abuse of quotations, it can +sometimes be complicated to know what a mere identifier represent in a tactic +expression. We recommend tracking the context and letting the compiler spit +typing errors to understand what is going on. + +We list below the typical changes one has to perform depending on the static +errors produced by the typechecker. + +### In Ltac expressions + +- `Unbound value X`, `Unbound constructor X`: + * if `X` is meant to be a term from the current stactic environment, replace + the problematic use by `'X`. + * if `X` is meant to be a hypothesis from the goal context, replace the + problematic use by `&X`. + +### In quotations + +- `The reference X was not found in the current environment`: + * if `X` is meant to be a tactic expression bound by a Ltac2 let or function, + replace the problematic use by `$X`. + * if `X` is meant to be a hypothesis from the goal context, replace the + problematic use by `&X`. + +## Exception catching + +Ltac2 features a proper exception-catching mechanism. For this reason, the +Ltac1 mechanism relying on `fail` taking integers and tacticals decreasing it +has been removed. Now exceptions are preserved by all tacticals, and it is +your duty to catch it and reraise it depending on your use. + # TODO - Implement deep pattern-matching. -- cgit v1.2.3 From 6875b016b0a502b03296e5f97f26cf0f6699a7aa Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 25 Aug 2017 17:16:01 +0200 Subject: Do not return STRING scopes in the tuple produced by "seq" scopes. --- doc/ltac2.md | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'doc') diff --git a/doc/ltac2.md b/doc/ltac2.md index 55780a7712..a645331e2d 100644 --- a/doc/ltac2.md +++ b/doc/ltac2.md @@ -615,8 +615,10 @@ The following scopes are built-in. + parses the string *s* as a keyword, if it is already a keyword, otherwise as an IDENT. Returns `()`. - seq(*scope₁*, ..., *scopeₙ*): - + parses *scope₁*, ..., *scopeₙ* in this order, and produces a n-tuple made - out of the parsed values in the same order. It is forbidden for the various + + parses *scope₁*, ..., *scopeₙ* in this order, and produces a tuple made + out of the parsed values in the same order. As an optimization, all + subscopes of the form STRING are left out of the returned tuple, instead + of returning a useless unit value. It is forbidden for the various subscopes to refer to the global entry using self of next. For now there is no way to declare new scopes from Ltac2 side, but this is -- cgit v1.2.3 From 126dc656963a7feb589b2a3574f0c55ad84d5f69 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Aug 2017 00:52:39 +0200 Subject: Allowing to insert calls to Ltac1 references in Ltac2. --- doc/ltac2.md | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'doc') diff --git a/doc/ltac2.md b/doc/ltac2.md index a645331e2d..51e3ab664d 100644 --- a/doc/ltac2.md +++ b/doc/ltac2.md @@ -692,6 +692,17 @@ foo 0 ↦ (fun x => x ()) (fun _ => 0) Note that abbreviations are not typechecked at all, and may result in typing errors after expansion. +# Compatibility layer with Ltac1 + +## Ltac1 from Ltac2 + +One can call Ltac1 code from Ltac2 by using the `ltac1` quotation. It parses +a Ltac1 expression, and semantics of this quotation is the evaluation of the +corresponding code for its side effects. + +Beware, Ltac1 **cannot** access variables from the Ltac2 scope. One is limited +to the use of standalone function calls. + # Transition from Ltac1 Owing to the use of a bunch of notations, the transition shouldn't be -- cgit v1.2.3 From bec2a0ad6eb60d33b5e3ab613d108f456df42a49 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 26 Aug 2017 09:40:31 +0200 Subject: Typos --- doc/ltac2.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'doc') diff --git a/doc/ltac2.md b/doc/ltac2.md index 51e3ab664d..5b1776b64f 100644 --- a/doc/ltac2.md +++ b/doc/ltac2.md @@ -488,7 +488,7 @@ Ltac2 Definition myconstr () := constr:(nat -> 0). ``` Term antiquotations are type-checked in the enclosing Ltac2 typing context -of the corresponding term expression. For instance, the following with +of the corresponding term expression. For instance, the following will type-check. ``` @@ -523,7 +523,7 @@ This pattern is so common that we provide dedicated Ltac2 and Coq term notations for it. - `&x` as an Ltac2 expression expands to `hyp @x`. -- `&x` as an Coq constr expression expands to +- `&x` as a Coq constr expression expands to `ltac2:(refine (fun () => hyp @x))`. #### Dynamic semantics @@ -538,7 +538,7 @@ under focus, with the hypotheses coming from the current environment extended with the bound variables of the term, and the resulting term is fed into the quoted term. -Relative orders of evaluation of antiquotations and quoted term is not +Relative orders of evaluation of antiquotations and quoted term are not specified. For instance, in the following example, `tac` will be evaluated in a context -- cgit v1.2.3 From 7f562a9539522e56004596a751758a08cee798b1 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Aug 2017 16:58:06 +0200 Subject: Allowing calls to Ltac2 inside Ltac1. --- doc/ltac2.md | 22 ++++++++++++++++++++-- 1 file changed, 20 insertions(+), 2 deletions(-) (limited to 'doc') diff --git a/doc/ltac2.md b/doc/ltac2.md index 5b1776b64f..d1c5c68494 100644 --- a/doc/ltac2.md +++ b/doc/ltac2.md @@ -698,11 +698,30 @@ errors after expansion. One can call Ltac1 code from Ltac2 by using the `ltac1` quotation. It parses a Ltac1 expression, and semantics of this quotation is the evaluation of the -corresponding code for its side effects. +corresponding code for its side effects. In particular, in cannot return values, +and the quotation has type `unit`. Beware, Ltac1 **cannot** access variables from the Ltac2 scope. One is limited to the use of standalone function calls. +## Ltac2 from Ltac1 + +Same as above by switching Ltac1 by Ltac2 and using the `ltac2` quotation +instead. + +Note that the tactic expression is evaluated eagerly, if one wants to use it as +an argument to a Ltac1 function, she has to resort to the good old +`idtac; ltac2:(foo)` trick. For instance, the code below will fail immediately +and won't print anything. + +``` +Ltac mytac tac := idtac "wow"; tac. + +Goal True. +Proof. +mytac ltac2:(fail). +``` + # Transition from Ltac1 Owing to the use of a bunch of notations, the transition shouldn't be @@ -812,6 +831,5 @@ your duty to catch it and reraise it depending on your use. # TODO - Implement deep pattern-matching. -- Implement compatibility layer with Ltac1 - Craft an expressive set of primitive functions - Implement native compilation to OCaml -- cgit v1.2.3 From 9bbdee3c09c92654bb8937b9939a9b9c69c23d1d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 27 Aug 2017 01:04:19 +0200 Subject: Introducing rebindable toplevel definitions. --- doc/ltac2.md | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/ltac2.md b/doc/ltac2.md index d1c5c68494..5c057b3ead 100644 --- a/doc/ltac2.md +++ b/doc/ltac2.md @@ -218,7 +218,7 @@ Limitations: for now, deep pattern matching is not implemented yet. One can define a new global Ltac2 value using the following syntax. ``` VERNAC ::= -| "Ltac2" RECFLAG LIDENT ":=" TERM +| "Ltac2" MUTFLAG RECFLAG LIDENT ":=" TERM ``` For semantic reasons, the body of the Ltac2 definition must be a syntactical @@ -227,6 +227,17 @@ values. If the `RECFLAG` is set, the tactic is expanded into a recursive binding. +If the `MUTFLAG` is set, the definition can be redefined at a later stage. This +can be performed through the following command. + +``` +VERNAC ::= +| "Ltac2" "Set" QUALID ":=" TERM +``` + +Mutable definitions act like dynamic binding, i.e. at runtime, the last defined +value for this entry is chosen. This is useful for global flags and the like. + ## Reduction We use the usual ML call-by-value reduction, with an otherwise unspecified -- cgit v1.2.3 From 99ec137899c2684da2a8c221f333e0e9adee2c48 Mon Sep 17 00:00:00 2001 From: gallais Date: Mon, 28 Aug 2017 14:33:17 +0200 Subject: typos --- doc/ltac2.md | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'doc') diff --git a/doc/ltac2.md b/doc/ltac2.md index 5c057b3ead..dd0dc391c6 100644 --- a/doc/ltac2.md +++ b/doc/ltac2.md @@ -149,7 +149,7 @@ Records are product types with named fields and eliminated by projection. Likewise they can be recursive if the `RECFLAG` is set. Open variants are a special kind of variant types whose constructors are not -statically defined, but can instead by extended dynamically. A typical example +statically defined, but can instead be extended dynamically. A typical example is the standard `exn` type. Pattern-matching must always include a catch-all clause. They can be extended by the following command. @@ -358,21 +358,21 @@ If one sees thunks as lazy lists, then `zero` is the empty list and `plus` is list concatenation, while `case` is pattern-matching. The backtracking is first-class, i.e. one can write -`plus "x" (fun () => "y") : string` producing a backtracking string. +`plus (fun () => "x") (fun _ => "y") : string` producing a backtracking string. These operations are expected to satisfy a few equations, most notably that they form a monoid compatible with sequentialization. ``` plus t zero ≡ t () -plus (fun () -> zero e) f ≡ f e -plus (plus t f) g ≡ plus t (fun e -> plus (f e) g) +plus (fun () => zero e) f ≡ f e +plus (plus t f) g ≡ plus t (fun e => plus (f e) g) -case (fun () -> zero e) ≡ Err e -case (fun () -> plus (fun () -> t) f) ≡ Val t f +case (fun () => zero e) ≡ Err e +case (fun () => plus (fun () => t) f) ≡ Val t f let x := zero e in u ≡ zero e -let x := plus t f in u ≡ plus (fun () -> let x := t in u) (fun e -> let x := f e in u) +let x := plus t f in u ≡ plus (fun () => let x := t in u) (fun e => let x := f e in u) (t, u, f, g, e values) ``` @@ -809,7 +809,7 @@ Ltac1 relies on a crazy amount of dynamic trickery to be able to tell apart bound variables from terms, hypotheses and whatnot. There is no such thing in Ltac2, as variables are recognized statically and other constructions do not live in the same syntactic world. Due to the abuse of quotations, it can -sometimes be complicated to know what a mere identifier represent in a tactic +sometimes be complicated to know what a mere identifier represents in a tactic expression. We recommend tracking the context and letting the compiler spit typing errors to understand what is going on. -- cgit v1.2.3 From d80e854d6827252676c2c504bb3108152a94d629 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 4 Sep 2017 15:24:33 +0200 Subject: Quick-and-dirty backtrace mechanism for the interpreter. --- doc/ltac2.md | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'doc') diff --git a/doc/ltac2.md b/doc/ltac2.md index dd0dc391c6..c1216d8f89 100644 --- a/doc/ltac2.md +++ b/doc/ltac2.md @@ -703,6 +703,11 @@ foo 0 ↦ (fun x => x ()) (fun _ => 0) Note that abbreviations are not typechecked at all, and may result in typing errors after expansion. +# Debug + +When the option `Ltac2 Backtrace` is set, toplevel failures will be printed with +a backtrace. + # Compatibility layer with Ltac1 ## Ltac1 from Ltac2 -- cgit v1.2.3 From dd5ad74b19530568159606828c8542ac298be29d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 4 Sep 2017 20:49:00 +0200 Subject: Implementing the non-strict mode. --- doc/ltac2.md | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) (limited to 'doc') diff --git a/doc/ltac2.md b/doc/ltac2.md index c1216d8f89..d7c8719a14 100644 --- a/doc/ltac2.md +++ b/doc/ltac2.md @@ -440,6 +440,8 @@ TERM ::= QUOTNAME := IDENT ``` +### Built-in quotations + The current implementation recognizes the following built-in quotations: - "ident", which parses identifiers (type `Init.ident`). - "constr", which parses Coq terms and produces an-evar free term at runtime @@ -457,6 +459,28 @@ The following syntactic sugar is provided for two common cases. - `@id` is the same as ident:(id) - `'t` is the same as open_constr:(t) +### Strict vs. non-strict mode + +Depending on the context, quotations producing terms (i.e. `constr` or +`open_constr`) are not internalized in the same way. There are two possible +modes, respectively called the *strict* and the *non-strict* mode. + +- In strict mode, all simple identifiers appearing in a term quotation are +required to be resolvable statically. That is, they must be the short name of +a declaration which is defined globally, excluding section variables and +hypotheses. If this doesn't hold, internalization will fail. To work around +this error, one has to specifically use the `&` notation. +- In non-strict mode, any simple identifier appearing in a term quotation which +is not bound in the global context is turned into a dynamic reference to a +hypothesis. That is to say, internalization will succeed, but the evaluation +of the term at runtime will fail if there is no such variable in the dynamic +context. + +Strict mode is enforced by default, e.g. for all Ltac2 definitions. Non-strict +mode is only set when evaluating Ltac2 snippets in interactive proof mode. The +rationale is that it is cumbersome to explicitly add `&` interactively, while it +is expected that global tactics enforce more invariants on their code. + ## Term Antiquotations ### Syntax -- cgit v1.2.3 From e0fd7c668bc284924c63a1f0a0e36fb4856c49e1 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 27 Oct 2017 16:04:00 +0200 Subject: Adding a command to evaluate Ltac2 expressions. --- doc/ltac2.md | 14 ++++++++++++++ 1 file changed, 14 insertions(+) (limited to 'doc') diff --git a/doc/ltac2.md b/doc/ltac2.md index d7c8719a14..6cbe0988d0 100644 --- a/doc/ltac2.md +++ b/doc/ltac2.md @@ -727,6 +727,20 @@ foo 0 ↦ (fun x => x ()) (fun _ => 0) Note that abbreviations are not typechecked at all, and may result in typing errors after expansion. +# Evaluation + +Ltac2 features a toplevel loop that can be used to evaluate expressions. + +``` +VERNAC ::= +| "Ltac2" "Eval" TERM +``` + +This command evaluates the term in the current proof if there is one, or in the +global environment otherwise, and displays the resulting value to the user +together with its type. This function is pure in the sense that it does not +modify the state of the proof, and in particular all side-effects are discarded. + # Debug When the option `Ltac2 Backtrace` is set, toplevel failures will be printed with -- cgit v1.2.3 From 71208e3eee6745ed8849bd03f66db638d9897516 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 27 Oct 2017 21:07:50 +0200 Subject: Adding documentation --- doc/ltac2.md | 91 ++++++++++++++++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 83 insertions(+), 8 deletions(-) (limited to 'doc') diff --git a/doc/ltac2.md b/doc/ltac2.md index 6cbe0988d0..cd0d8f4325 100644 --- a/doc/ltac2.md +++ b/doc/ltac2.md @@ -268,7 +268,7 @@ not to compute the argument, and `foo` would have e.g. type `(unit -> unit) -> unit`. ``` -foo (fun () -> let x := 0 in bar) +foo (fun () => let x := 0 in bar) ``` ## Typing @@ -559,7 +559,7 @@ for it. - `&x` as an Ltac2 expression expands to `hyp @x`. - `&x` as a Coq constr expression expands to - `ltac2:(refine (fun () => hyp @x))`. + `ltac2:(Control.refine (fun () => hyp @x))`. #### Dynamic semantics @@ -587,14 +587,86 @@ Many standard tactics perform type-checking of their argument before going further. It is your duty to ensure that terms are well-typed when calling such tactics. Failure to do so will result in non-recoverable exceptions. -## Patterns +## Trivial Term Antiquotations -Terms can be used in pattern position just as any Ltac constructor. The accepted -syntax is a subset of the constr syntax in Ltac term position. It does not -allow antiquotations. +It is possible to refer to a variable of type `constr` in the Ltac2 environment +through a specific syntax consistent with the antiquotations presented in +the notation section. -Patterns quotations are typically used with the matching functions provided -in the `Pattern` module. +``` +COQCONSTR ::= +| "$" LIDENT +``` + +In a Coq term, writing `$x` is semantically equivalent to +`ltac2:(Control.refine (fun () => x))`, up to re-typechecking. It allows to +insert in a concise way an Ltac2 variable of type `constr` into a Coq term. + +## Match over terms + +Ltac2 features a construction similar to Ltac1 `match` over terms, although +in a less hard-wired way. + +``` +TERM ::= +| "match!" TERM "with" CONSTR-MATCHING* "end" +| "lazy_match!" TERM "with" CONSTR-MATCHING* "end" +| "multi_match!" TERM "with" CONSTR-MATCHING*"end" + +CONSTR-MATCHING := +| "|" CONSTR-PATTERN "=>" TERM + +CONSTR-PATTERN := +| CONSTR +| "context" LIDENT? "[" CONSTR "]" +``` + +This construction is not primitive and is desugared at parsing time into +calls to term matching functions from the `Pattern` module. Internally, it is +implemented thanks to a specific scope accepting the `CONSTR-MATCHING` syntax. + +Variables from the `CONSTR-PATTERN` are statically bound in the body of the branch, to +values of type `constr` for the variables from the `CONSTR` pattern and to a +value of type `Pattern.context` for the variable `LIDENT`. + +Note that contrarily to Ltac, only lowercase identifiers are valid as Ltac2 +bindings, so that there will be a syntax error if one of the bound variables +starts with an uppercase character. + +The semantics of this construction is otherwise the same as the corresponding +one from Ltac1, except that it requires the goal to be focussed. + +## Match over goals + +Similarly, there is a way to match over goals in an elegant way, which is +just a notation desugared at parsing time. + +``` +TERM ::= +| "match!" MATCH-ORDER? "goal" "with" GOAL-MATCHING* "end" +| "lazy_match!" MATCH-ORDER? "goal" "with" GOAL-MATCHING* "end" +| "multi_match!" MATCH-ORDER? "goal" "with" GOAL-MATCHING*"end" + +GOAL-MATCHING := +| "|" "[" HYP-MATCHING* "|-" CONSTR-PATTERN "]" "=>" TERM + +HYP-MATCHING := +| LIDENT ":" CONSTR-PATTERN + +MATCH-ORDER := +| "reverse" +``` + +Variables from `HYP-MATCHING` and `CONSTR-PATTERN` are bound in the body of the +branch. Their types are: +- `constr` for pattern variables appearing in a `CONSTR` +- `Pattern.context` for variables binding a context +- `ident` for variables binding a hypothesis name. + +The same identifier caveat as in the case of matching over constr applies, and +this features has the same semantics as in Ltac1. In particular, a `reverse` +flag can be specified to match hypotheses from the more recently introduced to +the least recently introduced one. # Notations @@ -656,6 +728,9 @@ The following scopes are built-in. of returning a useless unit value. It is forbidden for the various subscopes to refer to the global entry using self of next. +A few other specific scopes exist to handle Ltac1-like syntax, but their use is +discouraged and they are thus not documented. + For now there is no way to declare new scopes from Ltac2 side, but this is planned. -- cgit v1.2.3 From 7dbf6dbd73f3a828bbb58458191912f895cf7779 Mon Sep 17 00:00:00 2001 From: Armael Date: Tue, 13 Mar 2018 16:13:18 +0100 Subject: Fix a typo --- doc/ltac2.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/ltac2.md b/doc/ltac2.md index cd0d8f4325..10a65fce44 100644 --- a/doc/ltac2.md +++ b/doc/ltac2.md @@ -875,7 +875,7 @@ Due to conflicts, a few syntactic rules have changed. `try`, `repeat`, `do`, `once`, `progress`, `time`, `abstract`. - `idtac` is no more. Either use `()` if you expect nothing to happen, `(fun () => ())` if you want a thunk (see next section), or use printing - primitives from the `Message` module if you wand to display something. + primitives from the `Message` module if you want to display something. ## Tactic delay -- cgit v1.2.3 From e31fa0ecb1f823cc5735fa63330f430e2c0d96e2 Mon Sep 17 00:00:00 2001 From: Armael Date: Tue, 13 Mar 2018 17:16:55 +0100 Subject: Fix another typo in the documentation's grammar for open variants --- doc/ltac2.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/ltac2.md b/doc/ltac2.md index 10a65fce44..9ba227c285 100644 --- a/doc/ltac2.md +++ b/doc/ltac2.md @@ -127,7 +127,7 @@ TYPEDEF := | TYPE | "[" CONSTRUCTORDEF₀ "|" ... "|" CONSTRUCTORDEFₙ "]" | "{" FIELDDEF₀ ";" ... ";" FIELDDEFₙ "}" -| "[" "..." "]" +| "[" ".." "]" CONSTRUCTORDEF := | IDENT ( "(" TYPE₀ "," ... "," TYPE₀ ")" ) -- cgit v1.2.3 From 6ff982c5d96cfa847f699bc25dc75553e7f718f0 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Tue, 7 Aug 2018 11:22:32 -0700 Subject: doc/ltac2.md: add table of contents --- doc/ltac2.md | 55 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 55 insertions(+) (limited to 'doc') diff --git a/doc/ltac2.md b/doc/ltac2.md index 9ba227c285..e8280a033a 100644 --- a/doc/ltac2.md +++ b/doc/ltac2.md @@ -24,6 +24,61 @@ that features at least the following: This document describes the implementation of such a language. The implementation of Ltac as of Coq 8.7 will be referred to as Ltac1. +# Contents + + +**Table of Contents** + +- [Summary](#summary) +- [Contents](#contents) +- [General design](#general-design) +- [ML component](#ml-component) + - [Overview](#overview) + - [Type Syntax](#type-syntax) + - [Type declarations](#type-declarations) + - [Term Syntax](#term-syntax) + - [Ltac Definitions](#ltac-definitions) + - [Reduction](#reduction) + - [Typing](#typing) + - [Effects](#effects) + - [Standard IO](#standard-io) + - [Fatal errors](#fatal-errors) + - [Backtrack](#backtrack) + - [Goals](#goals) +- [Meta-programming](#meta-programming) + - [Overview](#overview-1) + - [Generic Syntax for Quotations](#generic-syntax-for-quotations) + - [Built-in quotations](#built-in-quotations) + - [Strict vs. non-strict mode](#strict-vs-non-strict-mode) + - [Term Antiquotations](#term-antiquotations) + - [Syntax](#syntax) + - [Semantics](#semantics) + - [Static semantics](#static-semantics) + - [Dynamic semantics](#dynamic-semantics) + - [Trivial Term Antiquotations](#trivial-term-antiquotations) + - [Match over terms](#match-over-terms) + - [Match over goals](#match-over-goals) +- [Notations](#notations) + - [Scopes](#scopes) + - [Notations](#notations-1) + - [Abbreviations](#abbreviations) +- [Evaluation](#evaluation) +- [Debug](#debug) +- [Compatibility layer with Ltac1](#compatibility-layer-with-ltac1) + - [Ltac1 from Ltac2](#ltac1-from-ltac2) + - [Ltac2 from Ltac1](#ltac2-from-ltac1) +- [Transition from Ltac1](#transition-from-ltac1) + - [Syntax changes](#syntax-changes) + - [Tactic delay](#tactic-delay) + - [Variable binding](#variable-binding) + - [In Ltac expressions](#in-ltac-expressions) + - [In quotations](#in-quotations) + - [Exception catching](#exception-catching) +- [TODO](#todo) + + + + # General design There are various alternatives to Ltac1, such that Mtac or Rtac for instance. -- cgit v1.2.3 From 057345df3a6f5e46b76b9d8a395d75ba8b0965e9 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Tue, 7 Aug 2018 11:35:50 -0700 Subject: fix three small typos --- doc/ltac2.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'doc') diff --git a/doc/ltac2.md b/doc/ltac2.md index 9ba227c285..38cdef025e 100644 --- a/doc/ltac2.md +++ b/doc/ltac2.md @@ -17,7 +17,7 @@ Following the need of users that start developing huge projects relying critically on Ltac, we believe that we should offer a proper modern language that features at least the following: -- at least informal, predictible semantics +- at least informal, predictable semantics - a typing system - standard programming facilities (i.e. datatypes) @@ -388,7 +388,7 @@ represent several goals, including none. Thus, there is no such thing as It is natural to do the same in Ltac2, but we must provide a way to get access to a given goal. This is the role of the `enter` primitive, that applies a -tactic to each currently focussed goal in turn. +tactic to each currently focused goal in turn. ``` val enter : (unit -> unit) -> unit @@ -634,7 +634,7 @@ bindings, so that there will be a syntax error if one of the bound variables starts with an uppercase character. The semantics of this construction is otherwise the same as the corresponding -one from Ltac1, except that it requires the goal to be focussed. +one from Ltac1, except that it requires the goal to be focused. ## Match over goals -- cgit v1.2.3 From 387a56ced3a093af1e97ed08be02c93ceaf66aa8 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 19 Nov 2018 10:11:44 +0100 Subject: Adding a module to manipulate Ltac1 values. --- doc/ltac2.md | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) (limited to 'doc') diff --git a/doc/ltac2.md b/doc/ltac2.md index 3cee0ac494..b217cb08e6 100644 --- a/doc/ltac2.md +++ b/doc/ltac2.md @@ -880,6 +880,8 @@ a backtrace. ## Ltac1 from Ltac2 +### Simple API + One can call Ltac1 code from Ltac2 by using the `ltac1` quotation. It parses a Ltac1 expression, and semantics of this quotation is the evaluation of the corresponding code for its side effects. In particular, in cannot return values, @@ -888,6 +890,21 @@ and the quotation has type `unit`. Beware, Ltac1 **cannot** access variables from the Ltac2 scope. One is limited to the use of standalone function calls. +### Low-level API + +There exists a lower-level FFI into Ltac1 that is not recommended for daily use, +which is available in the `Ltac2.Ltac1` module. This API allows to directly +manipulate dynamically-typed Ltac1 values, either through the function calls, +or using the `ltac1val` quotation. The latter parses the same as `ltac1`, but +has type `Ltac2.Ltac1.t` instead of `unit`, and dynamically behaves as an Ltac1 +thunk, i.e. `ltac1val:(foo)` corresponds to the tactic closure that Ltac1 +would generate from `idtac; foo`. + +Due to intricate dynamic semantics, understanding when Ltac1 value quotations +focus is very hard. This is why some functions return a continuation-passing +style value, as it can dispatch dynamically between focused and unfocused +behaviour. + ## Ltac2 from Ltac1 Same as above by switching Ltac1 by Ltac2 and using the `ltac2` quotation -- cgit v1.2.3 From 66b6e83f4f4c32ad86333e13d65329be02c46048 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 25 Apr 2019 12:02:43 +0200 Subject: Prepare merge into Coq --- doc/ltac2.md | 1036 ---------------------------------------------------------- 1 file changed, 1036 deletions(-) delete mode 100644 doc/ltac2.md (limited to 'doc') diff --git a/doc/ltac2.md b/doc/ltac2.md deleted file mode 100644 index b217cb08e6..0000000000 --- a/doc/ltac2.md +++ /dev/null @@ -1,1036 +0,0 @@ -# Summary - -The Ltac tactic language is probably one of the ingredients of the success of -Coq, yet it is at the same time its Achilles' heel. Indeed, Ltac: - -- has nothing like intended semantics -- is very non-uniform due to organic growth -- lacks expressivity and requires programming-by-hacking -- is slow -- is error-prone and fragile -- has an intricate implementation - -This has a lot of terrible consequences, most notably the fact that it is never -clear whether some observed behaviour is a bug or a proper one. - -Following the need of users that start developing huge projects relying -critically on Ltac, we believe that we should offer a proper modern language -that features at least the following: - -- at least informal, predictable semantics -- a typing system -- standard programming facilities (i.e. datatypes) - -This document describes the implementation of such a language. The -implementation of Ltac as of Coq 8.7 will be referred to as Ltac1. - -# Contents - - -**Table of Contents** - -- [Summary](#summary) -- [Contents](#contents) -- [General design](#general-design) -- [ML component](#ml-component) - - [Overview](#overview) - - [Type Syntax](#type-syntax) - - [Type declarations](#type-declarations) - - [Term Syntax](#term-syntax) - - [Ltac Definitions](#ltac-definitions) - - [Reduction](#reduction) - - [Typing](#typing) - - [Effects](#effects) - - [Standard IO](#standard-io) - - [Fatal errors](#fatal-errors) - - [Backtrack](#backtrack) - - [Goals](#goals) -- [Meta-programming](#meta-programming) - - [Overview](#overview-1) - - [Generic Syntax for Quotations](#generic-syntax-for-quotations) - - [Built-in quotations](#built-in-quotations) - - [Strict vs. non-strict mode](#strict-vs-non-strict-mode) - - [Term Antiquotations](#term-antiquotations) - - [Syntax](#syntax) - - [Semantics](#semantics) - - [Static semantics](#static-semantics) - - [Dynamic semantics](#dynamic-semantics) - - [Trivial Term Antiquotations](#trivial-term-antiquotations) - - [Match over terms](#match-over-terms) - - [Match over goals](#match-over-goals) -- [Notations](#notations) - - [Scopes](#scopes) - - [Notations](#notations-1) - - [Abbreviations](#abbreviations) -- [Evaluation](#evaluation) -- [Debug](#debug) -- [Compatibility layer with Ltac1](#compatibility-layer-with-ltac1) - - [Ltac1 from Ltac2](#ltac1-from-ltac2) - - [Ltac2 from Ltac1](#ltac2-from-ltac1) -- [Transition from Ltac1](#transition-from-ltac1) - - [Syntax changes](#syntax-changes) - - [Tactic delay](#tactic-delay) - - [Variable binding](#variable-binding) - - [In Ltac expressions](#in-ltac-expressions) - - [In quotations](#in-quotations) - - [Exception catching](#exception-catching) -- [TODO](#todo) - - - - -# General design - -There are various alternatives to Ltac1, such that Mtac or Rtac for instance. -While those alternatives can be quite distinct from Ltac1, we designed -Ltac2 to be closest as reasonably possible to Ltac1, while fixing the -aforementioned defects. - -In particular, Ltac2 is: -- a member of the ML family of languages, i.e. - * a call-by-value functional language - * with effects - * together with Hindley-Milner type system -- a language featuring meta-programming facilities for the manipulation of - Coq-side terms -- a language featuring notation facilities to help writing palatable scripts - -We describe more in details each point in the remainder of this document. - -# ML component - -## Overview - -Ltac2 is a member of the ML family of languages, in the sense that it is an -effectful call-by-value functional language, with static typing à la -Hindley-Milner. It is commonly accepted that ML constitutes a sweet spot in PL -design, as it is relatively expressive while not being either too lax -(contrarily to dynamic typing) nor too strict (contrarily to say, dependent -types). - -The main goal of Ltac2 is to serve as a meta-language for Coq. As such, it -naturally fits in the ML lineage, just as the historical ML was designed as -the tactic language for the LCF prover. It can also be seen as a general-purpose -language, by simply forgetting about the Coq-specific features. - -Sticking to a standard ML type system can be considered somewhat weak for a -meta-language designed to manipulate Coq terms. In particular, there is no -way to statically guarantee that a Coq term resulting from an Ltac2 -computation will be well-typed. This is actually a design choice, motivated -by retro-compatibility with Ltac1. Instead, well-typedness is deferred to -dynamic checks, allowing many primitive functions to fail whenever they are -provided with an ill-typed term. - -The language is naturally effectful as it manipulates the global state of the -proof engine. This allows to think of proof-modifying primitives as effects -in a straightforward way. Semantically, proof manipulation lives in a monad, -which allows to ensure that Ltac2 satisfies the same equations as a generic ML -with unspecified effects would do, e.g. function reduction is substitution -by a value. - -## Type Syntax - -At the level of terms, we simply elaborate on Ltac1 syntax, which is quite -close to e.g. the one of OCaml. Types follow the simply-typed syntax of OCaml. - -``` -TYPE := -| "(" TYPE₀ "," ... "," TYPEₙ ")" TYPECONST -| "(" TYPE₀ "*" ... "*" TYPEₙ ")" -| TYPE₁ "->" TYPE₂ -| TYPEVAR - -TYPECONST := ( MODPATH "." )* LIDENT - -TYPEVAR := "'" LIDENT - -TYPEPARAMS := "(" TYPEVAR₀ "," ... "," TYPEVARₙ ")" -``` - -The set of base types can be extended thanks to the usual ML type -declarations such as algebraic datatypes and records. - -Built-in types include: -- `int`, machine integers (size not specified, in practice inherited from OCaml) -- `string`, mutable strings -- `'a array`, mutable arrays -- `exn`, exceptions -- `constr`, kernel-side terms -- `pattern`, term patterns -- `ident`, well-formed identifiers - -## Type declarations - -One can define new types by the following commands. - -``` -VERNAC ::= -| "Ltac2" "Type" TYPEPARAMS LIDENT -| "Ltac2" "Type" RECFLAG TYPEPARAMS LIDENT ":=" TYPEDEF - -RECFLAG := ( "rec" ) -``` - -The first command defines an abstract type. It has no use for the end user and -is dedicated to types representing data coming from the OCaml world. - -The second command defines a type with a manifest. There are four possible -kinds of such definitions: alias, variant, record and open variant types. - -``` -TYPEDEF := -| TYPE -| "[" CONSTRUCTORDEF₀ "|" ... "|" CONSTRUCTORDEFₙ "]" -| "{" FIELDDEF₀ ";" ... ";" FIELDDEFₙ "}" -| "[" ".." "]" - -CONSTRUCTORDEF := -| IDENT ( "(" TYPE₀ "," ... "," TYPE₀ ")" ) - -FIELDDEF := -| MUTFLAG IDENT ":" TYPE - -MUTFLAG := ( "mutable" ) -``` - -Aliases are just a name for a given type expression and are transparently -unfoldable to it. They cannot be recursive. - -Variants are sum types defined by constructors and eliminated by -pattern-matching. They can be recursive, but the `RECFLAG` must be explicitly -set. Pattern-maching must be exhaustive. - -Records are product types with named fields and eliminated by projection. -Likewise they can be recursive if the `RECFLAG` is set. - -Open variants are a special kind of variant types whose constructors are not -statically defined, but can instead be extended dynamically. A typical example -is the standard `exn` type. Pattern-matching must always include a catch-all -clause. They can be extended by the following command. - -``` -VERNAC ::= -| "Ltac2" "Type" TYPEPARAMS QUALID ":=" "[" CONSTRUCTORDEF "]" -``` - -## Term Syntax - -The syntax of the functional fragment is very close to the one of Ltac1, except -that it adds a true pattern-matching feature, as well as a few standard -constructions from ML. - -``` -VAR := LIDENT - -QUALID := ( MODPATH "." )* LIDENT - -CONSTRUCTOR := UIDENT - -TERM := -| QUALID -| CONSTRUCTOR TERM₀ ... TERMₙ -| TERM TERM₀ ... TERMₙ -| "fun" VAR "=>" TERM -| "let" VAR ":=" TERM "in" TERM -| "let" "rec" VAR ":=" TERM "in" TERM -| "match" TERM "with" BRANCH* "end" -| INT -| STRING -| "[|" TERM₀ ";" ... ";" TERMₙ "|]" -| "(" TERM₀ "," ... "," TERMₙ ")" -| "{" FIELD+ "}" -| TERM "." "(" QUALID ")" -| TERM₁ "." "(" QUALID ")" ":=" TERM₂ -| "["; TERM₀ ";" ... ";" TERMₙ "]" -| TERM₁ "::" TERM₂ -| ... - -BRANCH := -| PATTERN "=>" TERM - -PATTERN := -| VAR -| "_" -| "(" PATTERN₀ "," ... "," PATTERNₙ ")" -| CONSTRUCTOR PATTERN₀ ... PATTERNₙ -| "[" "]" -| PATTERN₁ "::" PATTERN₂ - -FIELD := -| QUALID ":=" TERM - -``` - -In practice, there is some additional syntactic sugar that allows e.g. to -bind a variable and match on it at the same time, in the usual ML style. - -There is a dedicated syntax for list and array litterals. - -Limitations: for now, deep pattern matching is not implemented yet. - -## Ltac Definitions - -One can define a new global Ltac2 value using the following syntax. -``` -VERNAC ::= -| "Ltac2" MUTFLAG RECFLAG LIDENT ":=" TERM -``` - -For semantic reasons, the body of the Ltac2 definition must be a syntactical -value, i.e. a function, a constant or a pure constructor recursively applied to -values. - -If the `RECFLAG` is set, the tactic is expanded into a recursive binding. - -If the `MUTFLAG` is set, the definition can be redefined at a later stage. This -can be performed through the following command. - -``` -VERNAC ::= -| "Ltac2" "Set" QUALID ":=" TERM -``` - -Mutable definitions act like dynamic binding, i.e. at runtime, the last defined -value for this entry is chosen. This is useful for global flags and the like. - -## Reduction - -We use the usual ML call-by-value reduction, with an otherwise unspecified -evaluation order. This is a design choice making it compatible with OCaml, -if ever we implement native compilation. The expected equations are as follows. -``` -(fun x => t) V ≡ t{x := V} (βv) - -let x := V in t ≡ t{x := V} (let) - -match C V₀ ... Vₙ with ... | C x₀ ... xₙ => t | ... end ≡ t {xᵢ := Vᵢ} (ι) - -(t any term, V values, C constructor) -``` - -Note that call-by-value reduction is already a departure from Ltac1 which uses -heuristics to decide when evaluating an expression. For instance, the following -expressions do not evaluate the same way in Ltac1. - -``` -foo (idtac; let x := 0 in bar) - -foo (let x := 0 in bar) -``` - -Instead of relying on the `idtac` hack, we would now require an explicit thunk -not to compute the argument, and `foo` would have e.g. type -`(unit -> unit) -> unit`. - -``` -foo (fun () => let x := 0 in bar) -``` - -## Typing - -Typing is strict and follows Hindley-Milner system. We will not implement the -current hackish subtyping semantics, and one will have to resort to conversion -functions. See notations though to make things more palatable. - -In this setting, all usual argument-free tactics have type `unit -> unit`, but -one can return as well a value of type `t` thanks to terms of type `unit -> t`, -or take additional arguments. - -## Effects - -Regarding effects, nothing involved here, except that instead of using the -standard IO monad as the ambient effectful world, Ltac2 is going to use the -tactic monad. - -Note that the order of evaluation of application is *not* specified and is -implementation-dependent, as in OCaml. - -We recall that the `Proofview.tactic` monad is essentially a IO monad together -with backtracking state representing the proof state. - -Intuitively a thunk of type `unit -> 'a` can do the following: -- It can perform non-backtracking IO like printing and setting mutable variables -- It can fail in a non-recoverable way -- It can use first-class backtrack. The proper way to figure that is that we - morally have the following isomorphism: - `(unit -> 'a) ~ (unit -> exn + ('a * (exn -> 'a)))` i.e. thunks can produce a - lazy list of results where each tail is waiting for a continuation exception. -- It can access a backtracking proof state, made out amongst other things of - the current evar assignation and the list of goals under focus. - -We describe more thoroughly the various effects existing in Ltac2 hereafter. - -### Standard IO - -The Ltac2 language features non-backtracking IO, notably mutable data and -printing operations. - -Mutable fields of records can be modified using the set syntax. Likewise, -built-in types like `string` and `array` feature imperative assignment. See -modules `String` and `Array` respectively. - -A few printing primitives are provided in the `Message` module, allowing to -display information to the user. - -### Fatal errors - -The Ltac2 language provides non-backtracking exceptions through the -following primitive in module `Control`. - -``` -val throw : exn -> 'a -``` - -Contrarily to backtracking exceptions from the next section, this kind of error -is never caught by backtracking primitives, that is, throwing an exception -destroys the stack. This is materialized by the following equation, where `E` -is an evaluation context. - -``` -E[throw e] ≡ throw e - -(e value) -``` - -There is currently no way to catch such an exception and it is a design choice. -There might be at some future point a way to catch it in a brutal way, -destroying all backtrack and return values. - -### Backtrack - -In Ltac2, we have the following backtracking primitives, defined in the -`Control` module. - -``` -Ltac2 Type 'a result := [ Val ('a) | Err (exn) ]. - -val zero : exn -> 'a -val plus : (unit -> 'a) -> (exn -> 'a) -> 'a -val case : (unit -> 'a) -> ('a * (exn -> 'a)) result -``` - -If one sees thunks as lazy lists, then `zero` is the empty list and `plus` is -list concatenation, while `case` is pattern-matching. - -The backtracking is first-class, i.e. one can write -`plus (fun () => "x") (fun _ => "y") : string` producing a backtracking string. - -These operations are expected to satisfy a few equations, most notably that they -form a monoid compatible with sequentialization. - -``` -plus t zero ≡ t () -plus (fun () => zero e) f ≡ f e -plus (plus t f) g ≡ plus t (fun e => plus (f e) g) - -case (fun () => zero e) ≡ Err e -case (fun () => plus (fun () => t) f) ≡ Val t f - -let x := zero e in u ≡ zero e -let x := plus t f in u ≡ plus (fun () => let x := t in u) (fun e => let x := f e in u) - -(t, u, f, g, e values) -``` - -### Goals - -A goal is given by the data of its conclusion and hypotheses, i.e. it can be -represented as `[Γ ⊢ A]`. - -The tactic monad naturally operates over the whole proofview, which may -represent several goals, including none. Thus, there is no such thing as -*the current goal*. Goals are naturally ordered, though. - -It is natural to do the same in Ltac2, but we must provide a way to get access -to a given goal. This is the role of the `enter` primitive, that applies a -tactic to each currently focused goal in turn. - -``` -val enter : (unit -> unit) -> unit -``` - -It is guaranteed that when evaluating `enter f`, `f` is called with exactly one -goal under focus. Note that `f` may be called several times, or never, depending -on the number of goals under focus before the call to `enter`. - -Accessing the goal data is then implicit in the Ltac2 primitives, and may panic -if the invariants are not respected. The two essential functions for observing -goals are given below. - -``` -val hyp : ident -> constr -val goal : unit -> constr -``` - -The two above functions panic if there is not exactly one goal under focus. -In addition, `hyp` may also fail if there is no hypothesis with the -corresponding name. - -# Meta-programming - -## Overview - -One of the horrendous implementation issues of Ltac is the fact that it is -never clear whether an object refers to the object world or the meta-world. -This is an incredible source of slowness, as the interpretation must be -aware of bound variables and must use heuristics to decide whether a variable -is a proper one or referring to something in the Ltac context. - -Likewise, in Ltac1, constr parsing is implicit, so that `foo 0` is -not `foo` applied to the Ltac integer expression `0` (Ltac does have a -non-first-class notion of integers), but rather the Coq term `Datatypes.O`. - -We should stop doing that! We need to mark when quoting and unquoting, although -we need to do that in a short and elegant way so as not to be too cumbersome -to the user. - -## Generic Syntax for Quotations - -In general, quotations can be introduced in term by the following syntax, where -`QUOTENTRY` is some parsing entry. -``` -TERM ::= -| QUOTNAME ":" "(" QUOTENTRY ")" - -QUOTNAME := IDENT -``` - -### Built-in quotations - -The current implementation recognizes the following built-in quotations: -- "ident", which parses identifiers (type `Init.ident`). -- "constr", which parses Coq terms and produces an-evar free term at runtime - (type `Init.constr`). -- "open_constr", which parses Coq terms and produces a term potentially with - holes at runtime (type `Init.constr` as well). -- "pattern", which parses Coq patterns and produces a pattern used for term - matching (type `Init.pattern`). -- "reference", which parses either a `QUALID` or `"&" IDENT`. Qualified names - are globalized at internalization into the corresponding global reference, - while `&id` is turned into `Std.VarRef id`. This produces at runtime a - `Std.reference`. - -The following syntactic sugar is provided for two common cases. -- `@id` is the same as ident:(id) -- `'t` is the same as open_constr:(t) - -### Strict vs. non-strict mode - -Depending on the context, quotations producing terms (i.e. `constr` or -`open_constr`) are not internalized in the same way. There are two possible -modes, respectively called the *strict* and the *non-strict* mode. - -- In strict mode, all simple identifiers appearing in a term quotation are -required to be resolvable statically. That is, they must be the short name of -a declaration which is defined globally, excluding section variables and -hypotheses. If this doesn't hold, internalization will fail. To work around -this error, one has to specifically use the `&` notation. -- In non-strict mode, any simple identifier appearing in a term quotation which -is not bound in the global context is turned into a dynamic reference to a -hypothesis. That is to say, internalization will succeed, but the evaluation -of the term at runtime will fail if there is no such variable in the dynamic -context. - -Strict mode is enforced by default, e.g. for all Ltac2 definitions. Non-strict -mode is only set when evaluating Ltac2 snippets in interactive proof mode. The -rationale is that it is cumbersome to explicitly add `&` interactively, while it -is expected that global tactics enforce more invariants on their code. - -## Term Antiquotations - -### Syntax - -One can also insert Ltac2 code into Coq term, similarly to what was possible in -Ltac1. - -``` -COQCONSTR ::= -| "ltac2" ":" "(" TERM ")" -``` - -Antiquoted terms are expected to have type `unit`, as they are only evaluated -for their side-effects. - -### Semantics - -Interpretation of a quoted Coq term is done in two phases, internalization and -evaluation. - -- Internalization is part of the static semantics, i.e. it is done at Ltac2 - typing time. -- Evaluation is part of the dynamic semantics, i.e. it is done when - a term gets effectively computed by Ltac2. - -Remark that typing of Coq terms is a *dynamic* process occuring at Ltac2 -evaluation time, and not at Ltac2 typing time. - -#### Static semantics - -During internalization, Coq variables are resolved and antiquotations are -type-checked as Ltac2 terms, effectively producing a `glob_constr` in Coq -implementation terminology. Note that although it went through the -type-checking of **Ltac2**, the resulting term has not been fully computed and -is potentially ill-typed as a runtime **Coq** term. - -``` -Ltac2 Definition myconstr () := constr:(nat -> 0). -// Valid with type `unit -> constr`, but will fail at runtime. -``` - -Term antiquotations are type-checked in the enclosing Ltac2 typing context -of the corresponding term expression. For instance, the following will -type-check. - -``` -let x := '0 in constr:(1 + ltac2:(exact x)) -// type constr -``` - -Beware that the typing environment of typing of antiquotations is **not** -expanded by the Coq binders from the term. Namely, it means that the following -Ltac2 expression will **not** type-check. -``` -constr:(fun x : nat => ltac2:(exact x)) -// Error: Unbound variable 'x' -``` - -There is a simple reason for that, which is that the following expression would -not make sense in general. -``` -constr:(fun x : nat => ltac2:(clear @x; exact x)) -``` -Indeed, a hypothesis can suddenly disappear from the runtime context if some -other tactic pulls the rug from under you. - -Rather, the tactic writer has to resort to the **dynamic** goal environment, -and must write instead explicitly that she is accessing a hypothesis, typically -as follows. -``` -constr:(fun x : nat => ltac2:(exact (hyp @x))) -``` - -This pattern is so common that we provide dedicated Ltac2 and Coq term notations -for it. - -- `&x` as an Ltac2 expression expands to `hyp @x`. -- `&x` as a Coq constr expression expands to - `ltac2:(Control.refine (fun () => hyp @x))`. - -#### Dynamic semantics - -During evaluation, a quoted term is fully evaluated to a kernel term, and is -in particular type-checked in the current environment. - -Evaluation of a quoted term goes as follows. -- The quoted term is first evaluated by the pretyper. -- Antiquotations are then evaluated in a context where there is exactly one goal -under focus, with the hypotheses coming from the current environment extended -with the bound variables of the term, and the resulting term is fed into the -quoted term. - -Relative orders of evaluation of antiquotations and quoted term are not -specified. - -For instance, in the following example, `tac` will be evaluated in a context -with exactly one goal under focus, whose last hypothesis is `H : nat`. The -whole expression will thus evaluate to the term `fun H : nat => nat`. -``` -let tac () := hyp @H in constr:(fun H : nat => ltac2:(tac ())) -``` - -Many standard tactics perform type-checking of their argument before going -further. It is your duty to ensure that terms are well-typed when calling -such tactics. Failure to do so will result in non-recoverable exceptions. - -## Trivial Term Antiquotations - -It is possible to refer to a variable of type `constr` in the Ltac2 environment -through a specific syntax consistent with the antiquotations presented in -the notation section. - -``` -COQCONSTR ::= -| "$" LIDENT -``` - -In a Coq term, writing `$x` is semantically equivalent to -`ltac2:(Control.refine (fun () => x))`, up to re-typechecking. It allows to -insert in a concise way an Ltac2 variable of type `constr` into a Coq term. - -## Match over terms - -Ltac2 features a construction similar to Ltac1 `match` over terms, although -in a less hard-wired way. - -``` -TERM ::= -| "match!" TERM "with" CONSTR-MATCHING* "end" -| "lazy_match!" TERM "with" CONSTR-MATCHING* "end" -| "multi_match!" TERM "with" CONSTR-MATCHING*"end" - -CONSTR-MATCHING := -| "|" CONSTR-PATTERN "=>" TERM - -CONSTR-PATTERN := -| CONSTR -| "context" LIDENT? "[" CONSTR "]" -``` - -This construction is not primitive and is desugared at parsing time into -calls to term matching functions from the `Pattern` module. Internally, it is -implemented thanks to a specific scope accepting the `CONSTR-MATCHING` syntax. - -Variables from the `CONSTR-PATTERN` are statically bound in the body of the branch, to -values of type `constr` for the variables from the `CONSTR` pattern and to a -value of type `Pattern.context` for the variable `LIDENT`. - -Note that contrarily to Ltac, only lowercase identifiers are valid as Ltac2 -bindings, so that there will be a syntax error if one of the bound variables -starts with an uppercase character. - -The semantics of this construction is otherwise the same as the corresponding -one from Ltac1, except that it requires the goal to be focused. - -## Match over goals - -Similarly, there is a way to match over goals in an elegant way, which is -just a notation desugared at parsing time. - -``` -TERM ::= -| "match!" MATCH-ORDER? "goal" "with" GOAL-MATCHING* "end" -| "lazy_match!" MATCH-ORDER? "goal" "with" GOAL-MATCHING* "end" -| "multi_match!" MATCH-ORDER? "goal" "with" GOAL-MATCHING*"end" - -GOAL-MATCHING := -| "|" "[" HYP-MATCHING* "|-" CONSTR-PATTERN "]" "=>" TERM - -HYP-MATCHING := -| LIDENT ":" CONSTR-PATTERN - -MATCH-ORDER := -| "reverse" -``` - -Variables from `HYP-MATCHING` and `CONSTR-PATTERN` are bound in the body of the -branch. Their types are: -- `constr` for pattern variables appearing in a `CONSTR` -- `Pattern.context` for variables binding a context -- `ident` for variables binding a hypothesis name. - -The same identifier caveat as in the case of matching over constr applies, and -this features has the same semantics as in Ltac1. In particular, a `reverse` -flag can be specified to match hypotheses from the more recently introduced to -the least recently introduced one. - -# Notations - -Notations are the crux of the usability of Ltac1. We should be able to recover -a feeling similar to the old implementation by using and abusing notations. - -## Scopes - -A scope is a name given to a grammar entry used to produce some Ltac2 expression -at parsing time. Scopes are described using a form of S-expression. - -``` -SCOPE := -| STRING -| INT -| LIDENT ( "(" SCOPE₀ "," ... "," SCOPEₙ ")" ) -``` - -A few scopes contain antiquotation features. For sake of uniformity, all -antiquotations are introduced by the syntax `"$" VAR`. - -The following scopes are built-in. -- constr: - + parses `c = COQCONSTR` and produces `constr:(c)` -- ident: - + parses `id = IDENT` and produces `ident:(id)` - + parses `"$" (x = IDENT)` and produces the variable `x` -- list0(*scope*): - + if *scope* parses `ENTRY`, parses ̀`(x₀, ..., xₙ = ENTRY*)` and produces - `[x₀; ...; xₙ]`. -- list0(*scope*, sep = STRING): - + if *scope* parses `ENTRY`, parses `(x₀ = ENTRY, "sep", ..., "sep", xₙ = ENTRY)` - and produces `[x₀; ...; xₙ]`. -- list1: same as list0 (with or without separator) but parses `ENTRY+` instead - of `ENTRY*`. -- opt(*scope*) - + if *scope* parses `ENTRY`, parses `ENTRY?` and produces either `None` or - `Some x` where `x` is the parsed expression. -- self: - + parses a Ltac2 expression at the current level and return it as is. -- next: - + parses a Ltac2 expression at the next level and return it as is. -- tactic(n = INT): - + parses a Ltac2 expression at the provided level *n* and return it as is. -- thunk(*scope*): - + parses the same as *scope*, and if *e* is the parsed expression, returns - `fun () => e`. -- STRING: - + parses the corresponding string as a CAMLP5 IDENT and returns `()`. -- keyword(s = STRING): - + parses the string *s* as a keyword and returns `()`. -- terminal(s = STRING): - + parses the string *s* as a keyword, if it is already a - keyword, otherwise as an IDENT. Returns `()`. -- seq(*scope₁*, ..., *scopeₙ*): - + parses *scope₁*, ..., *scopeₙ* in this order, and produces a tuple made - out of the parsed values in the same order. As an optimization, all - subscopes of the form STRING are left out of the returned tuple, instead - of returning a useless unit value. It is forbidden for the various - subscopes to refer to the global entry using self of next. - -A few other specific scopes exist to handle Ltac1-like syntax, but their use is -discouraged and they are thus not documented. - -For now there is no way to declare new scopes from Ltac2 side, but this is -planned. - -## Notations - -The Ltac2 parser can be extended by syntactic notations. -``` -VERNAC ::= -| "Ltac2" "Notation" TOKEN+ LEVEL? ":=" TERM - -LEVEL := ":" INT - -TOKEN := -| VAR "(" SCOPE ")" -| STRING -``` - -A Ltac2 notation adds a parsing rule to the Ltac2 grammar, which is expanded -to the provided body where every token from the notation is let-bound to the -corresponding generated expression. - -For instance, assume we perform: -``` -Ltac2 Notation "foo" c(thunk(constr)) ids(list0(ident)) := Bar.f c ids. -``` -Then the following expression -``` -let y := @X in foo (nat -> nat) x $y -``` -will expand at parsing time to -``` -let y := @X in -let c := fun () => constr:(nat -> nat) with ids := [@x; y] in Bar.f c ids -``` - -Beware that the order of evaluation of multiple let-bindings is not specified, -so that you may have to resort to thunking to ensure that side-effects are -performed at the right time. - -## Abbreviations - -There exists a special kind of notations, called abbreviations, that is designed -so that it does not add any parsing rules. It is similar in spirit to Coq -abbreviations, insofar as its main purpose is to give an absolute name to a -piece of pure syntax, which can be transparently referred by this name as if it -were a proper definition. Abbreviations are introduced by the following -syntax. - -``` -VERNAC ::= -| "Ltac2" "Notation" IDENT ":=" TERM -``` - -The abbreviation can then be manipulated just as a normal Ltac2 definition, -except that it is expanded at internalization time into the given expression. -Furthermore, in order to make this kind of construction useful in practice in -an effectful language such as Ltac2, any syntactic argument to an abbreviation -is thunked on-the-fly during its expansion. - -For instance, suppose that we define the following. -``` -Ltac2 Notation foo := fun x => x (). -``` -Then we have the following expansion at internalization time. -``` -foo 0 ↦ (fun x => x ()) (fun _ => 0) -``` - -Note that abbreviations are not typechecked at all, and may result in typing -errors after expansion. - -# Evaluation - -Ltac2 features a toplevel loop that can be used to evaluate expressions. - -``` -VERNAC ::= -| "Ltac2" "Eval" TERM -``` - -This command evaluates the term in the current proof if there is one, or in the -global environment otherwise, and displays the resulting value to the user -together with its type. This function is pure in the sense that it does not -modify the state of the proof, and in particular all side-effects are discarded. - -# Debug - -When the option `Ltac2 Backtrace` is set, toplevel failures will be printed with -a backtrace. - -# Compatibility layer with Ltac1 - -## Ltac1 from Ltac2 - -### Simple API - -One can call Ltac1 code from Ltac2 by using the `ltac1` quotation. It parses -a Ltac1 expression, and semantics of this quotation is the evaluation of the -corresponding code for its side effects. In particular, in cannot return values, -and the quotation has type `unit`. - -Beware, Ltac1 **cannot** access variables from the Ltac2 scope. One is limited -to the use of standalone function calls. - -### Low-level API - -There exists a lower-level FFI into Ltac1 that is not recommended for daily use, -which is available in the `Ltac2.Ltac1` module. This API allows to directly -manipulate dynamically-typed Ltac1 values, either through the function calls, -or using the `ltac1val` quotation. The latter parses the same as `ltac1`, but -has type `Ltac2.Ltac1.t` instead of `unit`, and dynamically behaves as an Ltac1 -thunk, i.e. `ltac1val:(foo)` corresponds to the tactic closure that Ltac1 -would generate from `idtac; foo`. - -Due to intricate dynamic semantics, understanding when Ltac1 value quotations -focus is very hard. This is why some functions return a continuation-passing -style value, as it can dispatch dynamically between focused and unfocused -behaviour. - -## Ltac2 from Ltac1 - -Same as above by switching Ltac1 by Ltac2 and using the `ltac2` quotation -instead. - -Note that the tactic expression is evaluated eagerly, if one wants to use it as -an argument to a Ltac1 function, she has to resort to the good old -`idtac; ltac2:(foo)` trick. For instance, the code below will fail immediately -and won't print anything. - -``` -Ltac mytac tac := idtac "wow"; tac. - -Goal True. -Proof. -mytac ltac2:(fail). -``` - -# Transition from Ltac1 - -Owing to the use of a bunch of notations, the transition shouldn't be -atrociously horrible and shockingly painful up to the point you want to retire -in the Ariège mountains, living off the land and insulting careless bypassers in -proto-georgian. - -That said, we do *not* guarantee you it is going to be a blissful walk either. -Hopefully, owing to the fact Ltac2 is typed, the interactive dialogue with Coq -will help you. - -We list the major changes and the transition strategies hereafter. - -## Syntax changes - -Due to conflicts, a few syntactic rules have changed. - -- The dispatch tactical `tac; [foo|bar]` is now written `tac > [foo|bar]`. -- Levels of a few operators have been revised. Some tacticals now parse as if - they were a normal function, i.e. one has to put parentheses around the - argument when it is complex, e.g an abstraction. List of affected tacticals: - `try`, `repeat`, `do`, `once`, `progress`, `time`, `abstract`. -- `idtac` is no more. Either use `()` if you expect nothing to happen, - `(fun () => ())` if you want a thunk (see next section), or use printing - primitives from the `Message` module if you want to display something. - -## Tactic delay - -Tactics are not magically delayed anymore, neither as functions nor as -arguments. It is your responsibility to thunk them beforehand and apply them -at the call site. - -A typical example of a delayed function: -``` -Ltac foo := blah. -``` -becomes -``` -Ltac2 foo () := blah. -``` - -All subsequent calls to `foo` must be applied to perform the same effect as -before. - -Likewise, for arguments: -``` -Ltac bar tac := tac; tac; tac. -``` -becomes -``` -Ltac2 bar tac := tac (); tac (); tac (). -``` - -We recommend the use of syntactic notations to ease the transition. For -instance, the first example can alternatively written as: -``` -Ltac2 foo0 () := blah. -Ltac2 Notation foo := foo0 (). -``` - -This allows to keep the subsequent calls to the tactic as-is, as the -expression `foo` will be implicitly expanded everywhere into `foo0 ()`. Such -a trick also works for arguments, as arguments of syntactic notations are -implicitly thunked. The second example could thus be written as follows. - -``` -Ltac2 bar0 tac := tac (); tac (); tac (). -Ltac2 Notation bar := bar0. -``` - -## Variable binding - -Ltac1 relies on a crazy amount of dynamic trickery to be able to tell apart -bound variables from terms, hypotheses and whatnot. There is no such thing in -Ltac2, as variables are recognized statically and other constructions do not -live in the same syntactic world. Due to the abuse of quotations, it can -sometimes be complicated to know what a mere identifier represents in a tactic -expression. We recommend tracking the context and letting the compiler spit -typing errors to understand what is going on. - -We list below the typical changes one has to perform depending on the static -errors produced by the typechecker. - -### In Ltac expressions - -- `Unbound value X`, `Unbound constructor X`: - * if `X` is meant to be a term from the current stactic environment, replace - the problematic use by `'X`. - * if `X` is meant to be a hypothesis from the goal context, replace the - problematic use by `&X`. - -### In quotations - -- `The reference X was not found in the current environment`: - * if `X` is meant to be a tactic expression bound by a Ltac2 let or function, - replace the problematic use by `$X`. - * if `X` is meant to be a hypothesis from the goal context, replace the - problematic use by `&X`. - -## Exception catching - -Ltac2 features a proper exception-catching mechanism. For this reason, the -Ltac1 mechanism relying on `fail` taking integers and tacticals decreasing it -has been removed. Now exceptions are preserved by all tacticals, and it is -your duty to catch it and reraise it depending on your use. - -# TODO - -- Implement deep pattern-matching. -- Craft an expressive set of primitive functions -- Implement native compilation to OCaml -- cgit v1.2.3 From 9779c0bf4945693bfd37b141e2c9f0fea200ba4d Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 25 Apr 2019 14:09:42 +0200 Subject: Integrate build and documentation of Ltac2 Since Ltac2 cannot be put under the stdlib logical root (some file names would clash), we move it to the `user-contrib` directory, to avoid adding another hardcoded path in `coqinit.ml`, following a suggestion by @ejgallego. Thanks to @Zimmi48 for the thorough documentation review and the numerous suggestions. --- doc/sphinx/biblio.bib | 17 + doc/sphinx/index.html.rst | 1 + doc/sphinx/index.latex.rst | 1 + doc/sphinx/proof-engine/ltac.rst | 4 +- doc/sphinx/proof-engine/ltac2.rst | 992 ++++++++++++++++++++++++++++++++++++++ 5 files changed, 1013 insertions(+), 2 deletions(-) create mode 100644 doc/sphinx/proof-engine/ltac2.rst (limited to 'doc') diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib index 0467852b19..85b02013d8 100644 --- a/doc/sphinx/biblio.bib +++ b/doc/sphinx/biblio.bib @@ -551,3 +551,20 @@ the Calculus of Inductive Constructions}}, biburl = {http://dblp.uni-trier.de/rec/bib/conf/cpp/BoespflugDG11}, bibsource = {dblp computer science bibliography, http://dblp.org} } + +@inproceedings{MilnerPrincipalTypeSchemes, + author = {Damas, Luis and Milner, Robin}, + title = {Principal Type-schemes for Functional Programs}, + booktitle = {Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, + series = {POPL '82}, + year = {1982}, + isbn = {0-89791-065-6}, + location = {Albuquerque, New Mexico}, + pages = {207--212}, + numpages = {6}, + url = {http://doi.acm.org/10.1145/582153.582176}, + doi = {10.1145/582153.582176}, + acmid = {582176}, + publisher = {ACM}, + address = {New York, NY, USA}, +} diff --git a/doc/sphinx/index.html.rst b/doc/sphinx/index.html.rst index a91c6a9c5f..0a20d1c47b 100644 --- a/doc/sphinx/index.html.rst +++ b/doc/sphinx/index.html.rst @@ -42,6 +42,7 @@ Contents proof-engine/proof-handling proof-engine/tactics proof-engine/ltac + proof-engine/ltac2 proof-engine/detailed-tactic-examples proof-engine/ssreflect-proof-language diff --git a/doc/sphinx/index.latex.rst b/doc/sphinx/index.latex.rst index 708820fff7..5562736997 100644 --- a/doc/sphinx/index.latex.rst +++ b/doc/sphinx/index.latex.rst @@ -41,6 +41,7 @@ The proof engine proof-engine/proof-handling proof-engine/tactics proof-engine/ltac + proof-engine/ltac2 proof-engine/detailed-tactic-examples proof-engine/ssreflect-proof-language diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 0322b43694..d3562b52c5 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -1,7 +1,7 @@ .. _ltac: -The tactic language -=================== +Ltac +==== This chapter gives a compact documentation of |Ltac|, the tactic language available in |Coq|. We start by giving the syntax, and next, we present the diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst new file mode 100644 index 0000000000..6e33862b39 --- /dev/null +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -0,0 +1,992 @@ +.. _ltac2: + +.. coqtop:: none + + From Ltac2 Require Import Ltac2. + +Ltac2 +===== + +The Ltac tactic language is probably one of the ingredients of the success of +Coq, yet it is at the same time its Achilles' heel. Indeed, Ltac: + +- has often unclear semantics +- is very non-uniform due to organic growth +- lacks expressivity (data structures, combinators, types, ...) +- is slow +- is error-prone and fragile +- has an intricate implementation + +Following the need of users that start developing huge projects relying +critically on Ltac, we believe that we should offer a proper modern language +that features at least the following: + +- at least informal, predictable semantics +- a typing system +- standard programming facilities (i.e. datatypes) + +This new language, called Ltac2, is described in this chapter. It is still +experimental but we encourage nonetheless users to start testing it, +especially wherever an advanced tactic language is needed. The previous +implementation of Ltac, described in the previous chapter, will be referred to +as Ltac1. + +.. _ltac2_design: + +General design +-------------- + +There are various alternatives to Ltac1, such that Mtac or Rtac for instance. +While those alternatives can be quite distinct from Ltac1, we designed +Ltac2 to be closest as reasonably possible to Ltac1, while fixing the +aforementioned defects. + +In particular, Ltac2 is: + +- a member of the ML family of languages, i.e. + + * a call-by-value functional language + * with effects + * together with Hindley-Milner type system + +- a language featuring meta-programming facilities for the manipulation of + Coq-side terms +- a language featuring notation facilities to help writing palatable scripts + +We describe more in details each point in the remainder of this document. + +ML component +------------ + +Overview +~~~~~~~~ + +Ltac2 is a member of the ML family of languages, in the sense that it is an +effectful call-by-value functional language, with static typing à la +Hindley-Milner (see :cite:`MilnerPrincipalTypeSchemes`). It is commonly accepted +that ML constitutes a sweet spot in PL design, as it is relatively expressive +while not being either too lax (unlike dynamic typing) nor too strict +(unlike, say, dependent types). + +The main goal of Ltac2 is to serve as a meta-language for Coq. As such, it +naturally fits in the ML lineage, just as the historical ML was designed as +the tactic language for the LCF prover. It can also be seen as a general-purpose +language, by simply forgetting about the Coq-specific features. + +Sticking to a standard ML type system can be considered somewhat weak for a +meta-language designed to manipulate Coq terms. In particular, there is no +way to statically guarantee that a Coq term resulting from an Ltac2 +computation will be well-typed. This is actually a design choice, motivated +by retro-compatibility with Ltac1. Instead, well-typedness is deferred to +dynamic checks, allowing many primitive functions to fail whenever they are +provided with an ill-typed term. + +The language is naturally effectful as it manipulates the global state of the +proof engine. This allows to think of proof-modifying primitives as effects +in a straightforward way. Semantically, proof manipulation lives in a monad, +which allows to ensure that Ltac2 satisfies the same equations as a generic ML +with unspecified effects would do, e.g. function reduction is substitution +by a value. + +Type Syntax +~~~~~~~~~~~ + +At the level of terms, we simply elaborate on Ltac1 syntax, which is quite +close to e.g. the one of OCaml. Types follow the simply-typed syntax of OCaml. + +The non-terminal :production:`lident` designates identifiers starting with a +lowercase. + +.. productionlist:: coq + ltac2_type : ( `ltac2_type`, ... , `ltac2_type` ) `ltac2_typeconst` + : ( `ltac2_type` * ... * `ltac2_type` ) + : `ltac2_type` -> `ltac2_type` + : `ltac2_typevar` + ltac2_typeconst : ( `modpath` . )* `lident` + ltac2_typevar : '`lident` + ltac2_typeparams : ( `ltac2_typevar`, ... , `ltac2_typevar` ) + +The set of base types can be extended thanks to the usual ML type +declarations such as algebraic datatypes and records. + +Built-in types include: + +- ``int``, machine integers (size not specified, in practice inherited from OCaml) +- ``string``, mutable strings +- ``'a array``, mutable arrays +- ``exn``, exceptions +- ``constr``, kernel-side terms +- ``pattern``, term patterns +- ``ident``, well-formed identifiers + +Type declarations +~~~~~~~~~~~~~~~~~ + +One can define new types by the following commands. + +.. cmd:: Ltac2 Type @ltac2_typeparams @lident + :name: Ltac2 Type + + This command defines an abstract type. It has no use for the end user and + is dedicated to types representing data coming from the OCaml world. + +.. cmdv:: Ltac2 Type {? rec} @ltac2_typeparams @lident := @ltac2_typedef + + This command defines a type with a manifest. There are four possible + kinds of such definitions: alias, variant, record and open variant types. + + .. productionlist:: coq + ltac2_typedef : `ltac2_type` + : [ `ltac2_constructordef` | ... | `ltac2_constructordef` ] + : { `ltac2_fielddef` ; ... ; `ltac2_fielddef` } + : [ .. ] + ltac2_constructordef : `uident` [ ( `ltac2_type` , ... , `ltac2_type` ) ] + ltac2_fielddef : [ mutable ] `ident` : `ltac2_type` + + Aliases are just a name for a given type expression and are transparently + unfoldable to it. They cannot be recursive. The non-terminal + :production:`uident` designates identifiers starting with an uppercase. + + Variants are sum types defined by constructors and eliminated by + pattern-matching. They can be recursive, but the `rec` flag must be + explicitly set. Pattern-maching must be exhaustive. + + Records are product types with named fields and eliminated by projection. + Likewise they can be recursive if the `rec` flag is set. + + .. cmdv:: Ltac2 Type @ltac2_typeparams @ltac2_qualid := [ @ltac2_constructordef ] + + Open variants are a special kind of variant types whose constructors are not + statically defined, but can instead be extended dynamically. A typical example + is the standard `exn` type. Pattern-matching must always include a catch-all + clause. They can be extended by this command. + +Term Syntax +~~~~~~~~~~~ + +The syntax of the functional fragment is very close to the one of Ltac1, except +that it adds a true pattern-matching feature, as well as a few standard +constructions from ML. + +.. productionlist:: coq + ltac2_var : `lident` + ltac2_qualid : ( `modpath` . )* `lident` + ltac2_constructor: `uident` + ltac2_term : `ltac2_qualid` + : `ltac2_constructor` + : `ltac2_term` `ltac2_term` ... `ltac2_term` + : fun `ltac2_var` => `ltac2_term` + : let `ltac2_var` := `ltac2_term` in `ltac2_term` + : let rec `ltac2_var` := `ltac2_term` in `ltac2_term` + : match `ltac2_term` with `ltac2_branch` ... `ltac2_branch` end + : `int` + : `string` + : `ltac2_term` ; `ltac2_term` + : [| `ltac2_term` ; ... ; `ltac2_term` |] + : ( `ltac2_term` , ... , `ltac2_term` ) + : { `ltac2_field` `ltac2_field` ... `ltac2_field` } + : `ltac2_term` . ( `ltac2_qualid` ) + : `ltac2_term` . ( `ltac2_qualid` ) := `ltac2_term` + : [; `ltac2_term` ; ... ; `ltac2_term` ] + : `ltac2_term` :: `ltac2_term` + : ... + ltac2_branch : `ltac2_pattern` => `ltac2_term` + ltac2_pattern : `ltac2_var` + : _ + : ( `ltac2_pattern` , ... , `ltac2_pattern` ) + : `ltac2_constructor` `ltac2_pattern` ... `ltac2_pattern` + : [ ] + : `ltac2_pattern` :: `ltac2_pattern` + ltac2_field : `ltac2_qualid` := `ltac2_term` + +In practice, there is some additional syntactic sugar that allows e.g. to +bind a variable and match on it at the same time, in the usual ML style. + +There is a dedicated syntax for list and array literals. + +.. note:: + + For now, deep pattern matching is not implemented. + +Ltac Definitions +~~~~~~~~~~~~~~~~ + +.. cmd:: Ltac2 {? mutable} {? rec} @lident := @ltac2_term + :name: Ltac2 + + This command defines a new global Ltac2 value. + + For semantic reasons, the body of the Ltac2 definition must be a syntactical + value, i.e. a function, a constant or a pure constructor recursively applied to + values. + + If ``rec`` is set, the tactic is expanded into a recursive binding. + + If ``mutable`` is set, the definition can be redefined at a later stage (see below). + +.. cmd:: Ltac2 Set @qualid := @ltac2_term + :name: Ltac2 Set + + This command redefines a previous ``mutable`` definition. + Mutable definitions act like dynamic binding, i.e. at runtime, the last defined + value for this entry is chosen. This is useful for global flags and the like. + +Reduction +~~~~~~~~~ + +We use the usual ML call-by-value reduction, with an otherwise unspecified +evaluation order. This is a design choice making it compatible with OCaml, +if ever we implement native compilation. The expected equations are as follows:: + + (fun x => t) V ≡ t{x := V} (βv) + + let x := V in t ≡ t{x := V} (let) + + match C V₀ ... Vₙ with ... | C x₀ ... xₙ => t | ... end ≡ t {xᵢ := Vᵢ} (ι) + + (t any term, V values, C constructor) + +Note that call-by-value reduction is already a departure from Ltac1 which uses +heuristics to decide when evaluating an expression. For instance, the following +expressions do not evaluate the same way in Ltac1. + +:n:`foo (idtac; let x := 0 in bar)` + +:n:`foo (let x := 0 in bar)` + +Instead of relying on the :n:`idtac` idiom, we would now require an explicit thunk +not to compute the argument, and :n:`foo` would have e.g. type +:n:`(unit -> unit) -> unit`. + +:n:`foo (fun () => let x := 0 in bar)` + +Typing +~~~~~~ + +Typing is strict and follows Hindley-Milner system. Unlike Ltac1, there +are no type casts at runtime, and one has to resort to conversion +functions. See notations though to make things more palatable. + +In this setting, all usual argument-free tactics have type :n:`unit -> unit`, but +one can return as well a value of type :n:`t` thanks to terms of type :n:`unit -> t`, +or take additional arguments. + +Effects +~~~~~~~ + +Effects in Ltac2 are straightforward, except that instead of using the +standard IO monad as the ambient effectful world, Ltac2 is going to use the +tactic monad. + +Note that the order of evaluation of application is *not* specified and is +implementation-dependent, as in OCaml. + +We recall that the `Proofview.tactic` monad is essentially a IO monad together +with backtracking state representing the proof state. + +Intuitively a thunk of type :n:`unit -> 'a` can do the following: + +- It can perform non-backtracking IO like printing and setting mutable variables +- It can fail in a non-recoverable way +- It can use first-class backtrack. The proper way to figure that is that we + morally have the following isomorphism: + :n:`(unit -> 'a) ~ (unit -> exn + ('a * (exn -> 'a)))` + i.e. thunks can produce a lazy list of results where each + tail is waiting for a continuation exception. +- It can access a backtracking proof state, made out amongst other things of + the current evar assignation and the list of goals under focus. + +We describe more thoroughly the various effects existing in Ltac2 hereafter. + +Standard IO ++++++++++++ + +The Ltac2 language features non-backtracking IO, notably mutable data and +printing operations. + +Mutable fields of records can be modified using the set syntax. Likewise, +built-in types like `string` and `array` feature imperative assignment. See +modules `String` and `Array` respectively. + +A few printing primitives are provided in the `Message` module, allowing to +display information to the user. + +Fatal errors +++++++++++++ + +The Ltac2 language provides non-backtracking exceptions, also known as *panics*, +through the following primitive in module `Control`.:: + + val throw : exn -> 'a + +Unlike backtracking exceptions from the next section, this kind of error +is never caught by backtracking primitives, that is, throwing an exception +destroys the stack. This is materialized by the following equation, where `E` +is an evaluation context.:: + + E[throw e] ≡ throw e + + (e value) + +There is currently no way to catch such an exception and it is a design choice. +There might be at some future point a way to catch it in a brutal way, +destroying all backtrack and return values. + +Backtrack ++++++++++ + +In Ltac2, we have the following backtracking primitives, defined in the +`Control` module.:: + + Ltac2 Type 'a result := [ Val ('a) | Err (exn) ]. + + val zero : exn -> 'a + val plus : (unit -> 'a) -> (exn -> 'a) -> 'a + val case : (unit -> 'a) -> ('a * (exn -> 'a)) result + +If one sees thunks as lazy lists, then `zero` is the empty list and `plus` is +list concatenation, while `case` is pattern-matching. + +The backtracking is first-class, i.e. one can write +:n:`plus (fun () => "x") (fun _ => "y") : string` producing a backtracking string. + +These operations are expected to satisfy a few equations, most notably that they +form a monoid compatible with sequentialization.:: + + plus t zero ≡ t () + plus (fun () => zero e) f ≡ f e + plus (plus t f) g ≡ plus t (fun e => plus (f e) g) + + case (fun () => zero e) ≡ Err e + case (fun () => plus (fun () => t) f) ≡ Val (t,f) + + let x := zero e in u ≡ zero e + let x := plus t f in u ≡ plus (fun () => let x := t in u) (fun e => let x := f e in u) + + (t, u, f, g, e values) + +Goals ++++++ + +A goal is given by the data of its conclusion and hypotheses, i.e. it can be +represented as `[Γ ⊢ A]`. + +The tactic monad naturally operates over the whole proofview, which may +represent several goals, including none. Thus, there is no such thing as +*the current goal*. Goals are naturally ordered, though. + +It is natural to do the same in Ltac2, but we must provide a way to get access +to a given goal. This is the role of the `enter` primitive, that applies a +tactic to each currently focused goal in turn.:: + + val enter : (unit -> unit) -> unit + +It is guaranteed that when evaluating `enter f`, `f` is called with exactly one +goal under focus. Note that `f` may be called several times, or never, depending +on the number of goals under focus before the call to `enter`. + +Accessing the goal data is then implicit in the Ltac2 primitives, and may panic +if the invariants are not respected. The two essential functions for observing +goals are given below.:: + + val hyp : ident -> constr + val goal : unit -> constr + +The two above functions panic if there is not exactly one goal under focus. +In addition, `hyp` may also fail if there is no hypothesis with the +corresponding name. + +Meta-programming +---------------- + +Overview +~~~~~~~~ + +One of the major implementation issues of Ltac1 is the fact that it is +never clear whether an object refers to the object world or the meta-world. +This is an incredible source of slowness, as the interpretation must be +aware of bound variables and must use heuristics to decide whether a variable +is a proper one or referring to something in the Ltac context. + +Likewise, in Ltac1, constr parsing is implicit, so that ``foo 0`` is +not ``foo`` applied to the Ltac integer expression ``0`` (Ltac does have a +notion of integers, though it is not first-class), but rather the Coq term +:g:`Datatypes.O`. + +The implicit parsing is confusing to users and often gives unexpected results. +Ltac2 makes these explicit using quoting and unquoting notation, although there +are notations to do it in a short and elegant way so as not to be too cumbersome +to the user. + +Generic Syntax for Quotations +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +In general, quotations can be introduced in terms using the following syntax, where +:production:`quotentry` is some parsing entry. + +.. prodn:: + ltac2_term += @ident : ( @quotentry ) + +Built-in quotations ++++++++++++++++++++ + +The current implementation recognizes the following built-in quotations: + +- ``ident``, which parses identifiers (type ``Init.ident``). +- ``constr``, which parses Coq terms and produces an-evar free term at runtime + (type ``Init.constr``). +- ``open_constr``, which parses Coq terms and produces a term potentially with + holes at runtime (type ``Init.constr`` as well). +- ``pattern``, which parses Coq patterns and produces a pattern used for term + matching (type ``Init.pattern``). +- ``reference``, which parses either a :n:`@qualid` or :n:`& @ident`. Qualified names + are globalized at internalization into the corresponding global reference, + while ``&id`` is turned into ``Std.VarRef id``. This produces at runtime a + ``Std.reference``. + +The following syntactic sugar is provided for two common cases. + +- ``@id`` is the same as ``ident:(id)`` +- ``'t`` is the same as ``open_constr:(t)`` + +Strict vs. non-strict mode +++++++++++++++++++++++++++ + +Depending on the context, quotations producing terms (i.e. ``constr`` or +``open_constr``) are not internalized in the same way. There are two possible +modes, respectively called the *strict* and the *non-strict* mode. + +- In strict mode, all simple identifiers appearing in a term quotation are + required to be resolvable statically. That is, they must be the short name of + a declaration which is defined globally, excluding section variables and + hypotheses. If this doesn't hold, internalization will fail. To work around + this error, one has to specifically use the ``&`` notation. +- In non-strict mode, any simple identifier appearing in a term quotation which + is not bound in the global context is turned into a dynamic reference to a + hypothesis. That is to say, internalization will succeed, but the evaluation + of the term at runtime will fail if there is no such variable in the dynamic + context. + +Strict mode is enforced by default, e.g. for all Ltac2 definitions. Non-strict +mode is only set when evaluating Ltac2 snippets in interactive proof mode. The +rationale is that it is cumbersome to explicitly add ``&`` interactively, while it +is expected that global tactics enforce more invariants on their code. + +Term Antiquotations +~~~~~~~~~~~~~~~~~~~ + +Syntax +++++++ + +One can also insert Ltac2 code into Coq terms, similarly to what is possible in +Ltac1. + +.. prodn:: + term += ltac2:( @ltac2_term ) + +Antiquoted terms are expected to have type ``unit``, as they are only evaluated +for their side-effects. + +Semantics ++++++++++ + +Interpretation of a quoted Coq term is done in two phases, internalization and +evaluation. + +- Internalization is part of the static semantics, i.e. it is done at Ltac2 + typing time. +- Evaluation is part of the dynamic semantics, i.e. it is done when + a term gets effectively computed by Ltac2. + +Note that typing of Coq terms is a *dynamic* process occurring at Ltac2 +evaluation time, and not at Ltac2 typing time. + +Static semantics +**************** + +During internalization, Coq variables are resolved and antiquotations are +type-checked as Ltac2 terms, effectively producing a ``glob_constr`` in Coq +implementation terminology. Note that although it went through the +type-checking of **Ltac2**, the resulting term has not been fully computed and +is potentially ill-typed as a runtime **Coq** term. + +.. example:: + + The following term is valid (with type `unit -> constr`), but will fail at runtime: + + .. coqtop:: in + + Ltac2 myconstr () := constr:(nat -> 0). + +Term antiquotations are type-checked in the enclosing Ltac2 typing context +of the corresponding term expression. + +.. example:: + + The following will type-check, with type `constr`. + + .. coqdoc:: + + let x := '0 in constr:(1 + ltac2:(exact x)) + +Beware that the typing environment of antiquotations is **not** +expanded by the Coq binders from the term. + + .. example:: + + The following Ltac2 expression will **not** type-check:: + + `constr:(fun x : nat => ltac2:(exact x))` + `(* Error: Unbound variable 'x' *)` + +There is a simple reason for that, which is that the following expression would +not make sense in general. + +`constr:(fun x : nat => ltac2:(clear @x; exact x))` + +Indeed, a hypothesis can suddenly disappear from the runtime context if some +other tactic pulls the rug from under you. + +Rather, the tactic writer has to resort to the **dynamic** goal environment, +and must write instead explicitly that she is accessing a hypothesis, typically +as follows. + +`constr:(fun x : nat => ltac2:(exact (hyp @x)))` + +This pattern is so common that we provide dedicated Ltac2 and Coq term notations +for it. + +- `&x` as an Ltac2 expression expands to `hyp @x`. +- `&x` as a Coq constr expression expands to + `ltac2:(Control.refine (fun () => hyp @x))`. + +Dynamic semantics +***************** + +During evaluation, a quoted term is fully evaluated to a kernel term, and is +in particular type-checked in the current environment. + +Evaluation of a quoted term goes as follows. + +- The quoted term is first evaluated by the pretyper. +- Antiquotations are then evaluated in a context where there is exactly one goal + under focus, with the hypotheses coming from the current environment extended + with the bound variables of the term, and the resulting term is fed into the + quoted term. + +Relative orders of evaluation of antiquotations and quoted term are not +specified. + +For instance, in the following example, `tac` will be evaluated in a context +with exactly one goal under focus, whose last hypothesis is `H : nat`. The +whole expression will thus evaluate to the term :g:`fun H : nat => H`. + +`let tac () := hyp @H in constr:(fun H : nat => ltac2:(tac ()))` + +Many standard tactics perform type-checking of their argument before going +further. It is your duty to ensure that terms are well-typed when calling +such tactics. Failure to do so will result in non-recoverable exceptions. + +**Trivial Term Antiquotations** + +It is possible to refer to a variable of type `constr` in the Ltac2 environment +through a specific syntax consistent with the antiquotations presented in +the notation section. + +.. prodn:: term += $@lident + +In a Coq term, writing :g:`$x` is semantically equivalent to +:g:`ltac2:(Control.refine (fun () => x))`, up to re-typechecking. It allows to +insert in a concise way an Ltac2 variable of type :n:`constr` into a Coq term. + +Match over terms +~~~~~~~~~~~~~~~~ + +Ltac2 features a construction similar to Ltac1 :n:`match` over terms, although +in a less hard-wired way. + +.. productionlist:: coq + ltac2_term : match! `ltac2_term` with `constrmatching` .. `constrmatching` end + : lazy_match! `ltac2_term` with `constrmatching` .. `constrmatching` end + : multi_match! `ltac2_term` with `constrmatching` .. `constrmatching` end + constrmatching : | `constrpattern` => `ltac2_term` + constrpattern : `term` + : context [ `term` ] + : context `lident` [ `term` ] + +This construction is not primitive and is desugared at parsing time into +calls to term matching functions from the `Pattern` module. Internally, it is +implemented thanks to a specific scope accepting the :n:`@constrmatching` syntax. + +Variables from the :n:`@constrpattern` are statically bound in the body of the branch, to +values of type `constr` for the variables from the :n:`@constr` pattern and to a +value of type `Pattern.context` for the variable :n:`@lident`. + +Note that unlike Ltac, only lowercase identifiers are valid as Ltac2 +bindings, so that there will be a syntax error if one of the bound variables +starts with an uppercase character. + +The semantics of this construction is otherwise the same as the corresponding +one from Ltac1, except that it requires the goal to be focused. + +Match over goals +~~~~~~~~~~~~~~~~ + +Similarly, there is a way to match over goals in an elegant way, which is +just a notation desugared at parsing time. + +.. productionlist:: coq + ltac2_term : match! [ reverse ] goal with `goalmatching` ... `goalmatching` end + : lazy_match! [ reverse ] goal with `goalmatching` ... `goalmatching` end + : multi_match! [ reverse ] goal with `goalmatching` ... `goalmatching` end + goalmatching : | [ `hypmatching` ... `hypmatching` |- `constrpattern` ] => `ltac2_term` + hypmatching : `lident` : `constrpattern` + : _ : `constrpattern` + +Variables from :n:`@hypmatching` and :n:`@constrpattern` are bound in the body of the +branch. Their types are: + +- ``constr`` for pattern variables appearing in a :n:`@term` +- ``Pattern.context`` for variables binding a context +- ``ident`` for variables binding a hypothesis name. + +The same identifier caveat as in the case of matching over constr applies, and +this features has the same semantics as in Ltac1. In particular, a ``reverse`` +flag can be specified to match hypotheses from the more recently introduced to +the least recently introduced one. + +Notations +--------- + +Notations are the crux of the usability of Ltac1. We should be able to recover +a feeling similar to the old implementation by using and abusing notations. + +Scopes +~~~~~~ + +A scope is a name given to a grammar entry used to produce some Ltac2 expression +at parsing time. Scopes are described using a form of S-expression. + +.. prodn:: + ltac2_scope ::= @string %| @integer %| @lident ({+, @ltac2_scope}) + +A few scopes contain antiquotation features. For sake of uniformity, all +antiquotations are introduced by the syntax :n:`$@lident`. + +The following scopes are built-in. + +- :n:`constr`: + + + parses :n:`c = @term` and produces :n:`constr:(c)` + +- :n:`ident`: + + + parses :n:`id = @ident` and produces :n:`ident:(id)` + + parses :n:`$(x = @ident)` and produces the variable :n:`x` + +- :n:`list0(@ltac2_scope)`: + + + if :n:`@ltac2_scope` parses :production:`entry`, parses :n:`(@entry__0, ..., @entry__n)` and produces + :n:`[@entry__0; ...; @entry__n]`. + +- :n:`list0(@ltac2_scope, sep = @string__sep)`: + + + if :n:`@ltac2_scope` parses :n:`@entry`, parses :n:`(@entry__0 @string__sep ... @string__sep @entry__n)` + and produces :n:`[@entry__0; ...; @entry__n]`. + +- :n:`list1`: same as :n:`list0` (with or without separator) but parses :n:`{+ @entry}` instead + of :n:`{* @entry}`. + +- :n:`opt(@ltac2_scope)` + + + if :n:`@ltac2_scope` parses :n:`@entry`, parses :n:`{? @entry}` and produces either :n:`None` or + :n:`Some x` where :n:`x` is the parsed expression. + +- :n:`self`: + + + parses a Ltac2 expression at the current level and return it as is. + +- :n:`next`: + + + parses a Ltac2 expression at the next level and return it as is. + +- :n:`tactic(n = @integer)`: + + + parses a Ltac2 expression at the provided level :n:`n` and return it as is. + +- :n:`thunk(@ltac2_scope)`: + + + parses the same as :n:`scope`, and if :n:`e` is the parsed expression, returns + :n:`fun () => e`. + +- :n:`STRING`: + + + parses the corresponding string as an identifier and returns :n:`()`. + +- :n:`keyword(s = @string)`: + + + parses the string :n:`s` as a keyword and returns `()`. + +- :n:`terminal(s = @string)`: + + + parses the string :n:`s` as a keyword, if it is already a + keyword, otherwise as an :n:`@ident`. Returns `()`. + +- :n:`seq(@ltac2_scope__1, ..., @ltac2_scope__2)`: + + + parses :n:`scope__1`, ..., :n:`scope__n` in this order, and produces a tuple made + out of the parsed values in the same order. As an optimization, all + subscopes of the form :n:`STRING` are left out of the returned tuple, instead + of returning a useless unit value. It is forbidden for the various + subscopes to refer to the global entry using self or next. + +A few other specific scopes exist to handle Ltac1-like syntax, but their use is +discouraged and they are thus not documented. + +For now there is no way to declare new scopes from Ltac2 side, but this is +planned. + +Notations +~~~~~~~~~ + +The Ltac2 parser can be extended by syntactic notations. + +.. cmd:: Ltac2 Notation {+ @lident (@ltac2_scope) %| @string } {? : @integer} := @ltac2_term + :name: Ltac2 Notation + + A Ltac2 notation adds a parsing rule to the Ltac2 grammar, which is expanded + to the provided body where every token from the notation is let-bound to the + corresponding generated expression. + + .. example:: + + Assume we perform: + + .. coqdoc:: + + Ltac2 Notation "foo" c(thunk(constr)) ids(list0(ident)) := Bar.f c ids. + + Then the following expression + + `let y := @X in foo (nat -> nat) x $y` + + will expand at parsing time to + + `let y := @X in` + `let c := fun () => constr:(nat -> nat) with ids := [@x; y] in Bar.f c ids` + + Beware that the order of evaluation of multiple let-bindings is not specified, + so that you may have to resort to thunking to ensure that side-effects are + performed at the right time. + +Abbreviations +~~~~~~~~~~~~~ + +.. cmdv:: Ltac2 Notation @lident := @ltac2_term + + This command introduces a special kind of notations, called abbreviations, + that is designed so that it does not add any parsing rules. It is similar in + spirit to Coq abbreviations, insofar as its main purpose is to give an + absolute name to a piece of pure syntax, which can be transparently referred + by this name as if it were a proper definition. + + The abbreviation can then be manipulated just as a normal Ltac2 definition, + except that it is expanded at internalization time into the given expression. + Furthermore, in order to make this kind of construction useful in practice in + an effectful language such as Ltac2, any syntactic argument to an abbreviation + is thunked on-the-fly during its expansion. + +For instance, suppose that we define the following. + +:n:`Ltac2 Notation foo := fun x => x ().` + +Then we have the following expansion at internalization time. + +:n:`foo 0 ↦ (fun x => x ()) (fun _ => 0)` + +Note that abbreviations are not typechecked at all, and may result in typing +errors after expansion. + +Evaluation +---------- + +Ltac2 features a toplevel loop that can be used to evaluate expressions. + +.. cmd:: Ltac2 Eval @ltac2_term + :name: Ltac2 Eval + + This command evaluates the term in the current proof if there is one, or in the + global environment otherwise, and displays the resulting value to the user + together with its type. This command is pure in the sense that it does not + modify the state of the proof, and in particular all side-effects are discarded. + +Debug +----- + +.. opt:: Ltac2 Backtrace + + When this option is set, toplevel failures will be printed with a backtrace. + +Compatibility layer with Ltac1 +------------------------------ + +Ltac1 from Ltac2 +~~~~~~~~~~~~~~~~ + +Simple API +++++++++++ + +One can call Ltac1 code from Ltac2 by using the :n:`ltac1` quotation. It parses +a Ltac1 expression, and semantics of this quotation is the evaluation of the +corresponding code for its side effects. In particular, it cannot return values, +and the quotation has type :n:`unit`. + +Beware, Ltac1 **cannot** access variables from the Ltac2 scope. One is limited +to the use of standalone function calls. + +Low-level API ++++++++++++++ + +There exists a lower-level FFI into Ltac1 that is not recommended for daily use, +which is available in the `Ltac2.Ltac1` module. This API allows to directly +manipulate dynamically-typed Ltac1 values, either through the function calls, +or using the `ltac1val` quotation. The latter parses the same as `ltac1`, but +has type `Ltac2.Ltac1.t` instead of `unit`, and dynamically behaves as an Ltac1 +thunk, i.e. `ltac1val:(foo)` corresponds to the tactic closure that Ltac1 +would generate from `idtac; foo`. + +Due to intricate dynamic semantics, understanding when Ltac1 value quotations +focus is very hard. This is why some functions return a continuation-passing +style value, as it can dispatch dynamically between focused and unfocused +behaviour. + +Ltac2 from Ltac1 +~~~~~~~~~~~~~~~~ + +Same as above by switching Ltac1 by Ltac2 and using the `ltac2` quotation +instead. + +Note that the tactic expression is evaluated eagerly, if one wants to use it as +an argument to a Ltac1 function, she has to resort to the good old +:n:`idtac; ltac2:(foo)` trick. For instance, the code below will fail immediately +and won't print anything. + +.. coqtop:: in + + From Ltac2 Require Import Ltac2. + Set Default Proof Mode "Classic". + +.. coqtop:: all + + Ltac mytac tac := idtac "wow"; tac. + + Goal True. + Proof. + Fail mytac ltac2:(fail). + +Transition from Ltac1 +--------------------- + +Owing to the use of a lot of notations, the transition should not be too +difficult. In particular, it should be possible to do it incrementally. That +said, we do *not* guarantee you it is going to be a blissful walk either. +Hopefully, owing to the fact Ltac2 is typed, the interactive dialogue with Coq +will help you. + +We list the major changes and the transition strategies hereafter. + +Syntax changes +~~~~~~~~~~~~~~ + +Due to conflicts, a few syntactic rules have changed. + +- The dispatch tactical :n:`tac; [foo|bar]` is now written :n:`tac > [foo|bar]`. +- Levels of a few operators have been revised. Some tacticals now parse as if + they were a normal function, i.e. one has to put parentheses around the + argument when it is complex, e.g an abstraction. List of affected tacticals: + :n:`try`, :n:`repeat`, :n:`do`, :n:`once`, :n:`progress`, :n:`time`, :n:`abstract`. +- :n:`idtac` is no more. Either use :n:`()` if you expect nothing to happen, + :n:`(fun () => ())` if you want a thunk (see next section), or use printing + primitives from the :n:`Message` module if you want to display something. + +Tactic delay +~~~~~~~~~~~~ + +Tactics are not magically delayed anymore, neither as functions nor as +arguments. It is your responsibility to thunk them beforehand and apply them +at the call site. + +A typical example of a delayed function: + +:n:`Ltac foo := blah.` + +becomes + +:n:`Ltac2 foo () := blah.` + +All subsequent calls to `foo` must be applied to perform the same effect as +before. + +Likewise, for arguments: + +:n:`Ltac bar tac := tac; tac; tac.` + +becomes + +:n:`Ltac2 bar tac := tac (); tac (); tac ().` + +We recommend the use of syntactic notations to ease the transition. For +instance, the first example can alternatively be written as: + +:n:`Ltac2 foo0 () := blah.` +:n:`Ltac2 Notation foo := foo0 ().` + +This allows to keep the subsequent calls to the tactic as-is, as the +expression `foo` will be implicitly expanded everywhere into `foo0 ()`. Such +a trick also works for arguments, as arguments of syntactic notations are +implicitly thunked. The second example could thus be written as follows. + +:n:`Ltac2 bar0 tac := tac (); tac (); tac ().` +:n:`Ltac2 Notation bar := bar0.` + +Variable binding +~~~~~~~~~~~~~~~~ + +Ltac1 relies on complex dynamic trickery to be able to tell apart bound +variables from terms, hypotheses, etc. There is no such thing in Ltac2, +as variables are recognized statically and other constructions do not live in +the same syntactic world. Due to the abuse of quotations, it can sometimes be +complicated to know what a mere identifier represents in a tactic expression. We +recommend tracking the context and letting the compiler print typing errors to +understand what is going on. + +We list below the typical changes one has to perform depending on the static +errors produced by the typechecker. + +In Ltac expressions ++++++++++++++++++++ + +.. exn:: Unbound ( value | constructor ) X + + * if `X` is meant to be a term from the current stactic environment, replace + the problematic use by `'X`. + * if `X` is meant to be a hypothesis from the goal context, replace the + problematic use by `&X`. + +In quotations ++++++++++++++ + +.. exn:: The reference X was not found in the current environment + + * if `X` is meant to be a tactic expression bound by a Ltac2 let or function, + replace the problematic use by `$X`. + * if `X` is meant to be a hypothesis from the goal context, replace the + problematic use by `&X`. + +Exception catching +~~~~~~~~~~~~~~~~~~ + +Ltac2 features a proper exception-catching mechanism. For this reason, the +Ltac1 mechanism relying on `fail` taking integers, and tacticals decreasing it, +has been removed. Now exceptions are preserved by all tacticals, and it is +your duty to catch them and reraise them depending on your use. -- cgit v1.2.3