From 465eb43ae41bae4c4ee9d5a6e7b5fe95768fb92e Mon Sep 17 00:00:00 2001 From: msozeau Date: Tue, 2 Sep 2008 20:27:45 +0000 Subject: Initial implementation of a new command to define (dependent) functions by equations. It is essentially an implementation of the "Eliminating Dependent Pattern-Matching" paper by Goguen, McBride and McKinna, relying on the new dependent eliminations tactics. The bulk is in contrib/subtac/equations.ml4. It implements a tree splitting on a set of clauses and the generation of a corresponding proof term along with some obligations at each splitting node. The obligations are solved by driving the dependent elimination tactic and you get a complete proof term at the end with the code given by the equations at the right spots, the rest of the cases being pruned automatically. Does not support recursion yet, a file with examples is in the test-suite. With recursion, it would be similar to Agda 2's pattern matching, except it won't reduce in Coq due to JMeq's/K. Incidentally, the simplification tactics after dependent elimination have been improved, resulting in a clearer and more space efficient implementation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11352 85f007b7-540e-0410-9357-904b9bb8a0f7 --- Makefile.common | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Makefile.common') diff --git a/Makefile.common b/Makefile.common index e323e2d9b..08ae6f835 100644 --- a/Makefile.common +++ b/Makefile.common @@ -309,8 +309,8 @@ SUBTACCMO:=contrib/subtac/subtac_utils.cmo contrib/subtac/eterm.cmo \ contrib/subtac/subtac_obligations.cmo contrib/subtac/subtac_cases.cmo \ contrib/subtac/subtac_pretyping_F.cmo contrib/subtac/subtac_pretyping.cmo \ contrib/subtac/subtac_command.cmo contrib/subtac/subtac_classes.cmo \ - contrib/subtac/subtac.cmo \ - contrib/subtac/g_subtac.cmo + contrib/subtac/subtac.cmo contrib/subtac/g_subtac.cmo \ + contrib/subtac/equations.cmo RTAUTOCMO:=contrib/rtauto/proof_search.cmo contrib/rtauto/refl_tauto.cmo \ contrib/rtauto/g_rtauto.cmo -- cgit v1.2.3