You can't detect matching braces with regular expressions.
(See e.g.
http://stackoverflow.com/questions/546433/regular-expression-to-match-outer-brackets
.)
What you probably need is to define your tactic language with a grammar and
write a parser for it.
You're going down a route that I think many people do by accident and end
up in a dead end or with a broken solution.
I recommend looking a little more into the background theory of formal
languages (e.g. read https://en.wikipedia.org/wiki/Formal_grammar).
On Tue, May 7, 2013 at 8:29 AM, Bill Richter
<rich...@math.northwestern.edu>wrote:
> Thanks, Ramana! I created my thmlist_tactics list in the same way that
> HOL Light creates the theorems database in hol_light/database.ml:
>
> needs "help.ml";;
> theorems :=
> [
> "ABSORPTION",ABSORPTION;
> "ABS_SIMP",ABS_SIMP;
> "ADD",ADD;
> [...]
> "vector",vector
> ];;
>
> That doesn't strike me as a painful solution, but I am curious that the
> only place that the association list theorems is referred to is help.mland
> update_database.ml.
>
> But the [theorems database] doesn't solve the problem of being able to
> represent and evaluate an OCaml expression within OCaml. [...]
> [The Scheme-style quote] would not at all be an easy extension to HOL4
> or HOL Light.
>
> Thanks! I'm having a problem with regular expressions. The Str library
> was quite helpful, and e.g. I implemented a consider function using
> (Str.regexp
> "[ \t\n]*consider[ \t\n]+\([^][]+[ \t\n]+such[ \t\n]+that[
> \t\n]+[^][]+[ \t\n]+\)\[\([^][]*\)\][ \t\n]+\[\([^!]*\)\][ \t\n]*")
>
> But Str doesn't seem to do everything I want. Take a HOL Light proof that
> has only THENs and no THENLs. Suppose we represent the proof as a string s
> where THENs are written as semicolons (;). Then
> Str.split (Str.regexp "[ \t\n]*;[ \t\n]*") s
> returns a list of the substrings delimited by ; and the surrounding
> whitespace. In very simple cases, these substrings will represent tactics
> which should be joined by THEN. But in more general cases, this won't
> work, as my tactics often themselves contain THENs, always contained in a
> square brace pair []. So I really want to break the string s up into
> substrings delimited by semicolons which are not captured by a square brace
> pair []. That doesn't sound too clear, so let me give an example of such a
> string s representing a proof:
>
> INTRO_TAC ∀A B C A' B', H1, H2 ;
> consider X such that
> move (A,B,C) (A,B,X) ∧ move (A,B,X) (A',B,X) [ABX]
> [HYP fol H1 H2 [Basic2move_THM]];
> ¬collinear {A,B,X} ∧ ¬collinear {A',B,X} []
> [so (HYP fol H1 [moveInvariant, ORIENTED_AREA_COLLINEAR_CONG])];
> ¬collinear {B,A',X} []
> [so (fol [collinearSymmetry])];
> consider Y such that move (B,A',X) (B,A',Y) ∧ move (B,A',Y) (B',A',Y)
> [BA'Y]
> [so (HYP fol H2 [Basic2move_THM])];
> move (A',B,X) (A',B,Y) ∧ move (A',B,Y) (A',B',Y) []
> [HYP fol BA'Y [moveSymmetry]] ;
> so (HYP fol ABX [] );
>
> That's actually too simple, because no proof inside a square brace pair
> contains a semicolon. Here's an example of such a substring in another
> proof:
>
> ∀n. (∃ q. reachableN p q n ∧ move q p') ⇒ reachableN p p' (SUC n)
> [Imp2]
> [INTRO_TAC ∀n; REWRITE_TAC[IMP_CONJ, LEFT_IMP_EXISTS_THM];
>
> So I want to delimit my proof string s only using only the semicolons like
> the last one, and not the semicolons like the one in the square brace proof
> [INTRO_TAC ... THM]
> I'm sure I could write a recursive function to do this, but it makes sense
> for ocaml to already have functions of this sort. I figure that I want to
> break up the string s as
> s1 ; s2 ; ... ; sn
> where each substring si has the same number of [s as ]s. Do such regexp
> issues arise in HOL4 and SML?
>
> --
> Best,
> Bill
>
>
> ------------------------------------------------------------------------------
> Learn Graph Databases - Download FREE O'Reilly Book
> "Graph Databases" is the definitive new guide to graph databases and
> their applications. This 200-page book is written by three acclaimed
> leaders in the field. The early access version is available now.
> Download your free book today! http://p.sf.net/sfu/neotech_d2d_may
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------------------------------------------------------
Learn Graph Databases - Download FREE O'Reilly Book
"Graph Databases" is the definitive new guide to graph databases and
their applications. This 200-page book is written by three acclaimed
leaders in the field. The early access version is available now.
Download your free book today! http://p.sf.net/sfu/neotech_d2d_may
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
