Mercurial > cpdt > repo
comparison src/Match.v @ 137:c0bda476b44b
Functional programming in Ltac
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sun, 26 Oct 2008 15:18:13 -0400 |
| parents | d6b1e9de7fc1 |
| children | 59a2110acf64 |
comparison
equal
deleted
inserted
replaced
| 136:d6b1e9de7fc1 | 137:c0bda476b44b |
|---|---|
| 438 (** The problem is that unification variables may not contain locally-bound variables. In this case, [?P] would need to be bound to [x = x], which contains the local quantified variable [x]. By using a wildcard in the earlier version, we avoided this restriction. | 438 (** The problem is that unification variables may not contain locally-bound variables. In this case, [?P] would need to be bound to [x = x], which contains the local quantified variable [x]. By using a wildcard in the earlier version, we avoided this restriction. |
| 439 | 439 |
| 440 The Coq 8.2 release includes a special pattern form for a unification variable with an explicit set of free variables. That unification variable is then bound to a function from the free variables to the "real" value. In Coq 8.1 and earlier, there is no such workaround. | 440 The Coq 8.2 release includes a special pattern form for a unification variable with an explicit set of free variables. That unification variable is then bound to a function from the free variables to the "real" value. In Coq 8.1 and earlier, there is no such workaround. |
| 441 | 441 |
| 442 No matter which version you use, it is important to be aware of this restriction. As we have alluded to, the restriction is the culprit behind the infinite-looping behavior of [completer']. We unintentionally match quantified facts with the modus ponens rule, circumventing the "already present" check and leading to different behavior. *) | 442 No matter which version you use, it is important to be aware of this restriction. As we have alluded to, the restriction is the culprit behind the infinite-looping behavior of [completer']. We unintentionally match quantified facts with the modus ponens rule, circumventing the "already present" check and leading to different behavior. *) |
| 443 | |
| 444 | |
| 445 (** * Functional Programming in Ltac *) | |
| 446 | |
| 447 (** Ltac supports quite convenient functional programming, with a Lisp-with-syntax kind of flavor. However, there are a few syntactic conventions involved in getting programs to be accepted. The Ltac syntax is optimized for tactic-writing, so one has to deal with some inconveniences in writing more standard functional programs. | |
| 448 | |
| 449 To illustrate, let us try to write a simple list length function. We start out writing it just like in Gallina, simply replacing [Fixpoint] (and its annotations) with [Ltac]. | |
| 450 | |
| 451 [[ | |
| 452 Ltac length ls := | |
| 453 match ls with | |
| 454 | nil => O | |
| 455 | _ :: ls' => S (length ls') | |
| 456 end. | |
| 457 | |
| 458 [[ | |
| 459 Error: The reference ls' was not found in the current environment | |
| 460 ]] | |
| 461 | |
| 462 At this point, we hopefully remember that pattern variable names must be prefixed by question marks in Ltac. | |
| 463 | |
| 464 [[ | |
| 465 Ltac length ls := | |
| 466 match ls with | |
| 467 | nil => O | |
| 468 | _ :: ?ls' => S (length ls') | |
| 469 end. | |
| 470 | |
| 471 [[ | |
| 472 Error: The reference S was not found in the current environment | |
| 473 ]] | |
| 474 | |
| 475 The problem is that Ltac treats the expression [S (length ls')] as an invocation of a tactic [S] with argument [length ls']. We need to use a special annotation to "escape into" the Gallina parsing nonterminal. *) | |
| 476 | |
| 477 Ltac length ls := | |
| 478 match ls with | |
| 479 | nil => O | |
| 480 | _ :: ?ls' => constr:(S (length ls')) | |
| 481 end. | |
| 482 | |
| 483 (** This definition is accepted. It can be a little awkward to test Ltac definitions like this. Here is one method. *) | |
| 484 | |
| 485 Goal False. | |
| 486 let n := length (1 :: 2 :: 3 :: nil) in | |
| 487 pose n. | |
| 488 (** [[ | |
| 489 | |
| 490 n := S (length (2 :: 3 :: nil)) : nat | |
| 491 ============================ | |
| 492 False | |
| 493 ]] | |
| 494 | |
| 495 [n] only has the length calculation unrolled one step. What has happened here is that, by escaping into the [constr] nonterminal, we referred to the [length] function of Gallina, rather than the [length] Ltac function that we are defining. *)Abort. | |
| 496 | |
| 497 Reset length. | |
| 498 | |
| 499 (** The thing to remember is that Gallina terms built by tactics must be bound explicitly via [let] or a similar technique, rather than inserting Ltac calls directly in other Gallina terms. *) | |
| 500 | |
| 501 Ltac length ls := | |
| 502 match ls with | |
| 503 | nil => O | |
| 504 | _ :: ?ls' => | |
| 505 let ls'' := length ls' in | |
| 506 constr:(S ls'') | |
| 507 end. | |
| 508 | |
| 509 Goal False. | |
| 510 let n := length (1 :: 2 :: 3 :: nil) in | |
| 511 pose n. | |
| 512 (** [[ | |
| 513 | |
| 514 n := 3 : nat | |
| 515 ============================ | |
| 516 False | |
| 517 ]] *) | |
| 518 Abort. | |
| 519 | |
| 520 (** We can also use anonymous function expressions and local function definitions in Ltac, as this example of a standard list [map] function shows. *) | |
| 521 | |
| 522 Ltac map T f := | |
| 523 let rec map' ls := | |
| 524 match ls with | |
| 525 | nil => constr:(@nil T) | |
| 526 | ?x :: ?ls' => | |
| 527 let x' := f x in | |
| 528 let ls'' := map' ls' in | |
| 529 constr:(x' :: ls'') | |
| 530 end in | |
| 531 map'. | |
| 532 | |
| 533 (** Ltac functions can have no implicit arguments. It may seem surprising that we need to pass [T], the carried type of the output list, explicitly. We cannot just use [type of f], because [f] is an Ltac term, not a Gallina term, and Ltac programs are dynamically typed. [f] could use very syntactic methods to decide to return differently typed terms for different inputs. We also could not replace [constr:(@nil T)] with [constr:nil], because we have no strongly-typed context to use to infer the parameter to [nil]. Luckily, we do have sufficient context within [constr:(x' :: ls'')]. | |
| 534 | |
| 535 Sometimes we need to employ the opposite direction of "nonterminal escape," when we want to pass a complicated tactic expression as an argument to another tactic, as we might want to do in invoking [map]. *) | |
| 536 | |
| 537 Goal False. | |
| 538 let ls := map (nat * nat)%type ltac:(fun x => constr:(x, x)) (1 :: 2 :: 3 :: nil) in | |
| 539 pose ls. | |
| 540 (** [[ | |
| 541 | |
| 542 l := (1, 1) :: (2, 2) :: (3, 3) :: nil : list (nat * nat) | |
| 543 ============================ | |
| 544 False | |
| 545 ]] *) | |
| 546 Abort. | |
| 547 |