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