coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Cuihtlauac ALVARADO <cuihtlauac.alvarado AT francetelecom.com>
- To: coq-club AT pauillac.inria.fr
- Cc: nadeem AT acm.org
- Subject: [Fwd: [Coq-Club] OCaml tactics]
- Date: Fri, 10 Oct 2003 18:14:48 +0200
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
- Organization: France Télécom R&D
Hi Nadeem,
Writing ML tactics seems a bit old fashioned today :-( Fortunately, I like vintage stuff :-)
Basically, the following code will do what you expect. Writing Makefile and .ml4 file is simple but somehow counter-intuitive. You'll find them in the nadeem.tgz archive.
let (>>) = Tacticals.tclTHEN
let tac_in_concl =
Tactics.intro
>> (Tacticals.tclLAST_HYP Tactics.simplest_elim)
>> (Tacticals.tclLAST_HYP (fun x -> Tactics.clear [Term.destVar x]))
The nice point is tclLAST_HYP which permits writing the tactic without introducing any fresh name.
I've also included another simple example in the convert.tgz archive. The Convert tactics make something in between Change and Unfold, but in a Rewrite style.
Hope it helps
--
Cuihtlauac ALVARADO - France Telecom R&D - DTL/TAL
2, avenue Pierre Marzin - 22307 Lannion - France
Tel: +33 2 96 05 32 73 - Mob: +33 6 08 10 80 41
Attachment:
convert-0.2.tgz
Description: GNU Zip compressed data
Attachment:
nadeem.tgz
Description: GNU Zip compressed data
--- Begin Message ---Hi,
- From: Nadeem Abdul Hamid <nadeem AT acm.org>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] OCaml tactics
- Date: Thu, 09 Oct 2003 16:36:51 -0400
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
- Organization: Yale University
How does one go about writing tactics for Coq at the OCaml level? I've looked through the /tactics directory in the source distribution but don't know really where to get started.
Maybe a complete example would be helpful. For example, take the simple tactic below:
< Tactic Definition ElimEx hyp var := Elim hyp; Clear hyp; Intros var hyp.
which applies to a hypothesis of form:
H: (EX m:nat | P(m))
< ElimEx H m.
would result in:
m: nat
H: P(m)
Now, instead of doing this in the toplevel tactic language of Coq, how could you write the same tactic in OCaml and what tools do you use to load it into the toplevel.
Thanks for your help,
--- nadeem
--------------------------------------------------------
Bug reports: http://coq.inria.fr/bin/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
--- End Message ---
- [Fwd: [Coq-Club] OCaml tactics], Cuihtlauac ALVARADO
Archive powered by MhonArc 2.6.16.