ftuong
/
citadelle-devel
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity
2,216 Commits 1 Branch 0 Tags 28 MiB
Commit Graph

2216 Commits

Author SHA1 Message Date
Frédéric Tuong bb48a55b88 bind the parsing to generated tokens 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13555 3260e6d1-4efc-4170-b0a7-36055960796d
 2019-01-28 15:46:34 +00:00
Frédéric Tuong 8f6e9fe878 remove some unused code 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13554 3260e6d1-4efc-4170-b0a7-36055960796d
 2019-01-28 15:31:01 +00:00
Frédéric Tuong eef11fc185 deactivate nesting mode 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13553 3260e6d1-4efc-4170-b0a7-36055960796d
 2019-01-28 15:26:19 +00:00
Frédéric Tuong f65aca61dc implement the library binding 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13552 3260e6d1-4efc-4170-b0a7-36055960796d
 2019-01-28 15:14:15 +00:00
Frédéric Tuong 8c7b95f179 permute some paragraphs 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13551 3260e6d1-4efc-4170-b0a7-36055960796d
 2019-01-28 14:08:00 +00:00
Frédéric Tuong c119229fa1 update the generated files 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13550 3260e6d1-4efc-4170-b0a7-36055960796d
 2019-01-28 13:52:01 +00:00
Frédéric Tuong 38b0fc282e update the generated 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13549 3260e6d1-4efc-4170-b0a7-36055960796d
 2019-01-28 13:10:23 +00:00
Frédéric Tuong 586d0925cf copy 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13548 3260e6d1-4efc-4170-b0a7-36055960796d
 2019-01-28 13:08:05 +00:00
Frédéric Tuong 2e85ecd4a2 permute some paragraphs 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13547 3260e6d1-4efc-4170-b0a7-36055960796d
 2019-01-28 13:03:20 +00:00
Frédéric Tuong f97b3553b8 generate monadic code 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13546 3260e6d1-4efc-4170-b0a7-36055960796d
 2019-01-24 15:24:12 +00:00
Frédéric Tuong cbaffaf4c5 implement C_lex 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13545 3260e6d1-4efc-4170-b0a7-36055960796d
 2019-01-18 15:44:10 +00:00
Frédéric Tuong 0a7ff80061 copy 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13544 3260e6d1-4efc-4170-b0a7-36055960796d
 2019-01-16 16:58:18 +00:00
Frédéric Tuong ea7d171853 implement C_lex 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13543 3260e6d1-4efc-4170-b0a7-36055960796d
 2019-01-16 16:53:05 +00:00
Frédéric Tuong 18d823a514 copy ML_Lex 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13542 3260e6d1-4efc-4170-b0a7-36055960796d
 2019-01-16 16:42:27 +00:00
Frédéric Tuong d5479b9ff8 use the repository of mlton 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13541 3260e6d1-4efc-4170-b0a7-36055960796d
 2019-01-15 16:36:06 +00:00
Frédéric Tuong f195d8c4b0 continue 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13540 3260e6d1-4efc-4170-b0a7-36055960796d
 2019-01-14 13:55:28 +00:00
Frédéric Tuong 42e9f208d0 add the SML definition of language-c library 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13539 3260e6d1-4efc-4170-b0a7-36055960796d
 2019-01-11 14:47:04 +00:00
Frédéric Tuong cdd834d49d switch to a mode where termination theorems are generated for functions 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13538 3260e6d1-4efc-4170-b0a7-36055960796d
 2019-01-11 12:30:32 +00:00
Frédéric Tuong ba038925ec continue r13534 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13537 3260e6d1-4efc-4170-b0a7-36055960796d
 2019-01-11 12:24:40 +00:00
Frédéric Tuong b2db24200a store all encountered constructors in the environment 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13536 3260e6d1-4efc-4170-b0a7-36055960796d
 2019-01-10 18:37:56 +00:00
Frédéric Tuong 369279e7d1 continue r13531 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13535 3260e6d1-4efc-4170-b0a7-36055960796d
 2019-01-10 18:30:36 +00:00
Frédéric Tuong 7d2f98d899 generate extra functions for them to be extracted "uncurried" at SML side 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13534 3260e6d1-4efc-4170-b0a7-36055960796d
 2019-01-10 18:02:55 +00:00
Frédéric Tuong 3e3612e2f5 implement meta_command', similar as meta_command but providing the current computed state of the manipulated environment 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13533 3260e6d1-4efc-4170-b0a7-36055960796d
 2019-01-10 15:52:45 +00:00
Frédéric Tuong 3514d453d0 display the immediate-level commands to be executed whenever meta_command receives native Isabelle commands in deep-mode 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13532 3260e6d1-4efc-4170-b0a7-36055960796d
 2019-01-10 14:51:45 +00:00
Frédéric Tuong 8e2edbd84b provide the binding of hide_const, abbreviation, code_reflect' 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13531 3260e6d1-4efc-4170-b0a7-36055960796d
 2019-01-10 14:12:26 +00:00
Frédéric Tuong 8f387bdf78 augment the new year 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13530 3260e6d1-4efc-4170-b0a7-36055960796d
 2019-01-04 10:31:35 +00:00
Frédéric Tuong 6739ac8159 Merge branch 2017 into devel 2018-10-10 13:21:27 -04:00
Frédéric Tuong ccbe8a3bd5 Merge branch 2017 into devel 2018-10-10 12:20:23 -04:00
Frédéric Tuong 38ae96b09e simplify 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13513 3260e6d1-4efc-4170-b0a7-36055960796d
 2018-10-10 16:03:12 +00:00
Frédéric Tuong 62b271ee4b add an option to specify if the code generated by 'language' should be understood as being a generator of meta-commands, and then automatically executed in the latter case 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13502 3260e6d1-4efc-4170-b0a7-36055960796d
 2018-09-24 20:13:56 +00:00
Frédéric Tuong 11ba388b50 implement the generic 'meta_command' 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13501 3260e6d1-4efc-4170-b0a7-36055960796d
 2018-09-24 19:50:24 +00:00
Frédéric Tuong c821215ec0 simplify 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13500 3260e6d1-4efc-4170-b0a7-36055960796d
 2018-09-24 13:37:04 +00:00
Frédéric Tuong 9a194bbc03 generalize the folding from Core.thy to later theories, so that for instance all_meta_trs can be called in all_meta_tr whenever it would be needed for a command to recursively generate several meta-commands 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13499 3260e6d1-4efc-4170-b0a7-36055960796d
 2018-09-24 13:20:44 +00:00
Frédéric Tuong 1acc157774 add an option to specify which function to immediately apply on a parsed value 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13498 3260e6d1-4efc-4170-b0a7-36055960796d
 2018-09-19 20:33:00 +00:00
Frédéric Tuong 94f04b8081 simplify 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13497 3260e6d1-4efc-4170-b0a7-36055960796d
 2018-09-19 20:22:23 +00:00
Frédéric Tuong 4d462a304f Merge branch 2017 into devel 2018-09-12 18:01:29 -04:00
Frédéric Tuong fcaea38a64 fix r13207 for each hook to receive the final state 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13479 3260e6d1-4efc-4170-b0a7-36055960796d
 2018-09-11 00:30:35 +00:00
Frédéric Tuong fd4d57977d upgrade to Isabelle devel/91162dd89571 (i.e., Isabelle2018) and afp-devel 2018-08-22 16:56:55 -04:00
Frédéric Tuong b24c51e830 Merge branch 2017 into devel 2018-08-22 16:10:51 -04:00
Frédéric Tuong 22d654219c fix r13210 : choosing a command_keyword classified as 'diag' would let the evaluating engine not propagate 'theory' results sequentially (which is necessary as Toplevel.read_write can be seen as acting on 'theory'). Then a solution is to use instead a 'thy_decl' tag. 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13451 3260e6d1-4efc-4170-b0a7-36055960796d
 2018-07-31 16:04:51 +00:00
Frédéric Tuong ec7ee9c97e fix r13210 : choosing a command_keyword classified as 'diag' would let the evaluating engine not propagate 'theory' results sequentially (which is necessary as Toplevel.read_write can be seen as acting on 'theory'). Then a solution is to use instead a 'thy_decl' tag. 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13450 3260e6d1-4efc-4170-b0a7-36055960796d
 2018-07-31 15:36:38 +00:00
Frédéric Tuong ca29d0390a alpha-rename 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13449 3260e6d1-4efc-4170-b0a7-36055960796d
 2018-07-25 14:33:57 +00:00
Frédéric Tuong d2c60c580b continue a03cc6ccde 2018-07-23 19:30:22 -04:00
Frédéric Tuong 0c7f27b743 Merge branch 2017 into devel 2018-07-23 15:11:11 -04:00
Frédéric Tuong 2dddcf8d0c fix a03cc6ccde 2018-07-23 09:37:47 -04:00
Frédéric Tuong f849a48a22 update headers 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13447 3260e6d1-4efc-4170-b0a7-36055960796d
 2018-07-23 07:47:56 +00:00
Frédéric Tuong 29b9af3ec4 simplify 
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13446 3260e6d1-4efc-4170-b0a7-36055960796d
 2018-07-23 07:47:15 +00:00
Frédéric Tuong 22cd2e4ffc synchronize with afp-devel 2018-07-19 17:11:28 -04:00
Frédéric Tuong 2b403a9f39 synchronize with afp-devel 2018-07-19 15:27:13 -04:00
Frédéric Tuong 0ab18b558e synchronize with afp-devel 2018-07-18 17:04:05 -04:00