Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Codegenerator_Test/Code_Test_PolyML.thy
author haftmann
Mon, 04 Nov 2019 20:38:15 +0000
changeset 71042 400e9512f1d3
parent 68155 8b50f29a1992
permissions -rw-r--r--
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
59720
f893472fff31 proper headers;
wenzelm
parents: 58626
diff changeset 
     1
 
(*  Title:      HOL/Codegenerator_Test/Code_Test_PolyML.thy
58039
469a375212c1 add testing framework for generated code
Andreas Lochbihler
parents:
diff changeset 
     2
 
    Author:     Andreas Lochbihler, ETH Zurich
469a375212c1 add testing framework for generated code
Andreas Lochbihler
parents:
diff changeset 
     3
 












469a375212c1
add testing framework for generated code



Andreas Lochbihler


parents: 

diff
changeset




     4


Test case for test_code on PolyML













469a375212c1
add testing framework for generated code



Andreas Lochbihler


parents: 

diff
changeset




     5


*)













469a375212c1
add testing framework for generated code



Andreas Lochbihler


parents: 

diff
changeset




     6









68155






8b50f29a1992
new tool Code_Lazy



Andreas Lochbihler


parents: 
66453

diff
changeset




     7


theory Code_Test_PolyML imports  "HOL-Library.Code_Test" Code_Lazy_Test begin








58039






469a375212c1
add testing framework for generated code



Andreas Lochbihler


parents: 

diff
changeset




     8














469a375212c1
add testing framework for generated code



Andreas Lochbihler


parents: 

diff
changeset




     9


test_code "14 + 7 * -12 = (140 div -2 :: integer)" in PolyML













469a375212c1
add testing framework for generated code



Andreas Lochbihler


parents: 

diff
changeset




    10









58348






2d47c7d10b62
add target language evaluators for the value command;



Andreas Lochbihler


parents: 
58039

diff
changeset




    11


value [PolyML] "14 + 7 * -12 :: integer"








58039






469a375212c1
add testing framework for generated code



Andreas Lochbihler


parents: 

diff
changeset




    12









68155






8b50f29a1992
new tool Code_Lazy



Andreas Lochbihler


parents: 
66453

diff
changeset




    13


test_code "stake 10 (cycle ''ab'') = ''ababababab''" in PolyML













8b50f29a1992
new tool Code_Lazy



Andreas Lochbihler


parents: 
66453

diff
changeset




    14









58039






469a375212c1
add testing framework for generated code



Andreas Lochbihler


parents: 

diff
changeset




    15


end















isabelle