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?

Tobias

René Thiemann schrieb:
> 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
> begin
> 
> types
>   ('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
> 
> abbreviation
>   return :: "'a => ('t, 'a)parser"
> where
>   "return x = (%ts. Inr (x, ts))"
> 
> definition
>   bind :: "('t, 'a) parser => ('a => ('t, 'b) parser) => ('t, 'b) parser"
> where
>   "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
> termination
> proof
> (*  impossible, since there is no link between input ts and the list
>     of tokens that is used for recursive foo-calls *)
> oops
> 
> 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,
> René
> 
> PS: The small theory file is attached.
> 
> 






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