Email Gateway (Aug 18 2022 at 17:29): Email Gateway (Aug 18 2022 at 17:29):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
Hi there,
I ran into the following Problem when using Efficient_Nat
Now generating code...
*** "Nat.Suc" is not a constructor, on left hand side of equation:
*** fit_length ?a (Suc ?v) [] == replicate (Suc ?v) ?a
I am generating code by the command
$(ISABELLE_TOOL) codegen $(ISAFOR) Ceta \
'certifyProof in Haskell module_name Ceta file
"../generated/Haskell/"';
where $(ISAFOR) is a Heap-Image whose last theory is Ceta.thy and the
last import of Ceta.thy is Efficient_Nat.
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?
cheers
chris
Email Gateway (Aug 18 2022 at 17:30):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC