Re: [isabelle] Problems with cong-rules for parser

Not an answer but a thought: maybe result checking can simplify your
life? Maybe you can write your parser directly in ML and verify each run
of the parser by unparsing and comparison with the input?

Yes and no: We do unparsing and comparison in any way, however, we cannot write our parser in ML as we want to have the parser also in the target- language from the code-generator (as the generated verifier has to parse), or can the code-generator
generate (Haskell)-code from ML (in the new release)?

Hence, we need a parser in HOL which does not have to satisfy any properties since comparison against the input is performed. However, for the code- generator we need termination of all functions we would like to export (including the parser). And since termination of the parser is currently the only axiom we use, we would
like to get rid of this axiom by actually proving termination.


Dear all,

we currently have problems setting up the right cong-rules for our
parser such termination is provable.

Here, the major problems are parsers which call themselves twice in a row.

Consider the following theory:

theory Test imports Main

 ('t, 'a) parser = "'t list => string + ('a x 't list)"

take a token list and produce a string error-message or a pair of result
and remaining token list

(state-monad with errors)

now we can define the standard return and bind operations

 return :: "'a => ('t, 'a)parser"
 "return x = (%ts. Inr (x, ts))"

bind :: "('t, 'a) parser => ('a => ('t, 'b) parser) => ('t, 'b) parser"
 "bind m f ts = (case m ts of
     Inl e => Inl e
   | Inr (x,ts') => f x ts')"

consuming one character

fun consume :: "('t,'t)parser"
where "consume [] = Inl ''error''"
  |  "consume (t # ts) = Inr (t, ts)"

now, here is the difficult function:

function foo :: "('t, 't list)parser"
where "foo ts = (bind consume
                  (% t. bind foo
                  (% us. bind foo
                  (% vs. return (t # us @ vs))))) ts"
by pat_completeness auto
(*  impossible, since there is no link between input ts and the list
   of tokens that is used for recursive foo-calls *)

so, let us add some congruence rule:

lemma bind_cong[fundef_cong]:
 fixes m1 :: "('t,'a)parser"
 assumes "m1 ts1 = m2 ts1" and "!! y ts. m1 ts1 = Inr (y,ts) ==> f1 y
ts = f2 y ts" and "ts1 = ts2"
 shows "((bind m1 f1) ts1) = ((bind m2 f2) ts2)"
using assms unfolding bind_def by (cases "m1 ts1", auto)

now, indeed a simplied version of foo can be proven to be terminating
(if there is only one recursive call)

function foo' :: "('t, 't list)parser"
where "foo' ts = (bind consume
                  (% t. bind foo'
                  (% vs. return (t # vs)))) ts"
by pat_completeness auto
termination by ... tedious reasoning

but, if we want to have the full version which two recursive calls, then
not even the function
definition is accepted:

function foo'' :: "('t, 't list)parser"
where "foo'' ts = (bind consume
                  (% t. bind foo''
                  (% us. bind foo''
                  (% vs. return (t # us @ vs))))) ts"
exception THM 0 raised (line 709 of "thm.ML"): implies_elim: major premise

Does someone have an idea, what went wrong in this case?

Best regards,

PS: The small theory file is attached.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.