Re: [isabelle] code-generation Efficient_Nat



Hi Christian,

> I thought Efficient_Nat would take care of transforming an equation as
> the one causing the error into a form using 'if/then/else' instead of
> the pattern? Am I doing anything wrong, or does Efficient_Nat not work
> as expected?

In general, this procedure is not complete, c.f. »Eliminating pattern
matching on natural numbers.« on p77 in
http://www4.in.tum.de/~haftmann/pdf/codegen_hol_haftmann_phd.pdf

Concerning your problem in particular,

> *** "Nat.Suc" is not a constructor, on left hand side of equation:
> *** fit_length ?a (Suc ?v) [] == replicate (Suc ?v) ?a

you should inspect the code equations for fit_length using
print_codesetup and see whether they bear a problem.  In case, you can
always replace the offending code equations manually.

Hope this helps,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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