#
# ChangeLog for src/RTL
#
# Generated by Trac 1.2
# Jan 16, 2021, 10:46:22 AM

Wed, 21 Sep 2011 13:58:32 GMT sacerdot [1237]
	* src/RTL/RTLinterpret.ma (deleted)

	Wrong commit repaired.


Wed, 21 Sep 2011 09:57:20 GMT sacerdot [1233]
	* src/LIN/LIN.ma (modified)
	* src/LTL/LTL.ma (modified)
	* src/LTL/LTLToLIN.ma (modified)
	* src/RTL/semantics.ma (modified)
	* src/common/SmallstepExec.ma (modified)
	* src/joint/Joint.ma (modified)
	* src/joint/semantics.ma (modified)

	1) Ported to Brian's new dependent type for fullexec
	2) Universe ...


Tue, 30 Aug 2011 14:22:54 GMT mulligan [1149]
	* src/LIN/LINToASM.ma (modified)
	* src/LTL/LTLToLIN.ma (modified)
	* src/RTL/RTLtoERTL.ma (modified)
	* src/RTLabs/RTLAbstoRTL.ma (modified)

	changes to get everything type checking again after changing names of ...


Tue, 30 Aug 2011 13:33:30 GMT sacerdot [1141]
	* src/RTL/semantics.ma (modified)

	Comment (about a bug) added.


Tue, 30 Aug 2011 10:08:25 GMT mulligan [1138]
	* src/ERTL/ERTL.ma (modified)
	* src/ERTL/ERTLToLTLI.ma (modified)
	* src/RTL/RTLtoERTL.ma (modified)
	* src/RTLabs/RTLAbstoRTL.ma (modified)

	merged ertl_st_opaccs_a and ertl_st_opaccs_b into each other


Mon, 29 Aug 2011 15:19:31 GMT mulligan [1131]
	* src/ERTL/ERTL.ma (modified)
	* src/ERTL/ERTLToLTLI.ma (modified)
	* src/RTL/RTLtoERTL.ma (modified)

	changes to syntax of ertl: removed ertl_st_addr_l and ertl_st_addr_h ...


Mon, 29 Aug 2011 13:07:53 GMT sacerdot [1126]
	* src/RTL/semantics.ma (modified)

	Semantics completed up to initial state creation.


Fri, 26 Aug 2011 18:06:01 GMT sacerdot [1122]
	* src/RTL/semantics.ma (modified)

	Internal function call implemented too.


Fri, 26 Aug 2011 18:00:06 GMT sacerdot [1121]
	* src/RTL/semantics.ma (modified)

	External function calls implemented (but look at the new comment on ...


Fri, 26 Aug 2011 17:41:46 GMT sacerdot [1120]
	* src/RTL/semantics.ma (modified)

	All operations implemented.


Fri, 26 Aug 2011 17:08:07 GMT sacerdot [1118]
	* src/RTL/semantics.ma (modified)

	All derivatives of St_const implemented (up to axioms to match the ...


Fri, 26 Aug 2011 16:47:52 GMT sacerdot [1117]
	* src/RTL/semantics.ma (modified)

	More operations implemented.


Fri, 26 Aug 2011 16:47:05 GMT sacerdot [1115]
	* src/RTL/RTL.ma (modified)

	Some comments.


Fri, 26 Aug 2011 11:01:04 GMT sacerdot [1114]
	* src/RTL/semantics.ma (modified)

	some more operations implemented


Fri, 26 Aug 2011 10:40:00 GMT sacerdot [1113]
	* src/RTL/semantics.ma (added)

	Semantics (interpreter) of RTL.
	The file does not compile yet. I am ...


Wed, 24 Aug 2011 12:43:58 GMT mulligan [1107]
	* src/ERTL/ERTL.ma (modified)
	* src/ERTL/liveness.ma (modified)
	* src/RTL/RTLtoERTL.ma (modified)

	got rtl-ertl pass working again


Wed, 24 Aug 2011 12:23:48 GMT mulligan [1106]
	* src/RTL/RTL.ma (modified)

	changes necessary to get RTLabs->RTL to compile


Wed, 27 Jul 2011 15:50:25 GMT mulligan [1089]
	* src/ASM/I8051.ma (modified)
	* src/LIN/JointLTLLIN.ma (modified)
	* src/LTL/LTL.ma (modified)
	* src/RTL/RTL.ma (modified)
	* src/RTL/RTLinterpret.ma (added)

	more changes from earlier in the week


Wed, 20 Jul 2011 09:26:21 GMT mulligan [1081]
	* src/RTL/RTLTailcall.ma (modified)
	* src/RTL/RTLtoERTL.ma (modified)

	completed rtl-ertl pass


Tue, 19 Jul 2011 15:28:38 GMT mulligan [1080]
	* src/RTL/RTLTailcall.ma (modified)
	* src/common/Graphs.ma (modified)

	more added


Tue, 19 Jul 2011 14:30:04 GMT mulligan [1079]
	* src/RTL/RTLtoERTL.ma (modified)

	finished rtl to ertl pass modulo conversion of tailcall ...


Tue, 19 Jul 2011 10:23:32 GMT mulligan [1077]
	* src/ERTL/ERTL.ma (modified)
	* src/RTL/RTLtoERTL.ma (modified)
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/common/Graphs.ma (modified)
	* src/common/Identifiers.ma (modified)

	ack, dependent types are scary


Mon, 18 Jul 2011 15:40:33 GMT mulligan [1076]
	* src/RTL/RTLtoERTL.ma (modified)

	small changes


Mon, 18 Jul 2011 15:21:14 GMT mulligan [1075]
	* src/ASM/I8051.ma (modified)
	* src/ASM/Util.ma (modified)
	* src/RTL/RTLtoERTL.ma (modified)
	* src/utilities/RegisterSet.ma (modified)

	nearly completed rtl -> ertl pass removing all option types with dep. ...


Fri, 15 Jul 2011 12:40:40 GMT mulligan [1071]
	* src/ASM/I8051.ma (modified)
	* src/ASM/Util.ma (modified)
	* src/ERTL/ERTL.ma (modified)
	* src/RTL/RTL.ma (modified)
	* src/RTL/RTLtoERTL.ma (modified)
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/RTLabs/syntax.ma (modified)

	changes the specific form that the added proofs take to use None, not ...


Thu, 14 Jul 2011 12:27:41 GMT mulligan [1068]
	* src/RTL/RTL.ma (modified)
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/common/Identifiers.ma (modified)

	rtlabs translation complete subject to axioms


Wed, 13 Jul 2011 15:12:10 GMT mulligan [1066]
	* src/ASM/I8051.ma (modified)
	* src/RTL/RTL.ma (modified)
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/utilities/Compare.ma (modified)

	changes from today


Tue, 12 Jul 2011 15:52:07 GMT mulligan [1064]
	* src/ASM/Util.ma (modified)
	* src/RTL/RTL.ma (modified)
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/common/AST.ma (modified)

	changes from today, nearly complete rtlabs translation pass


Fri, 08 Jul 2011 15:49:22 GMT mulligan [1061]
	* src/ASM/Util.ma (modified)
	* src/RTL/RTL.ma (modified)
	* src/RTLabs/RTLAbstoRTL.ma (modified)

	more work, bug found, ridiculous map3 function with dep. types added


Fri, 08 Jul 2011 10:17:14 GMT mulligan [1060]
	* src/ASM/I8051.ma (modified)
	* src/ASM/Util.ma (modified)
	* src/RTL/RTL.ma (modified)
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/common/AST.ma (modified)

	work from this morning and yesterday


Fri, 03 Jun 2011 15:35:27 GMT campbell [878]
	* src/Cminor/syntax.ma (modified)
	* src/ERTL/ERTL.ma (modified)
	* src/LIN/LIN.ma (modified)
	* src/RTL/RTL.ma (modified)
	* src/RTLabs/import.ma (modified)
	* src/RTLabs/syntax.ma (modified)

	Removal of manually inserted record projections.


Fri, 29 Apr 2011 11:59:07 GMT mulligan [784]
	* src/RTL/RTLTailcall.ma (added)

	Added missing tailcall simplification file.


Fri, 29 Apr 2011 11:36:35 GMT mulligan [783]
	* src/ERTL/ERTL.ma (modified)
	* src/RTL/RTL.ma (modified)
	* src/RTL/RTLtoERTL.ma (modified)

	rtl to ertl pass complete (modulo some straightforward axioms that ...


Thu, 28 Apr 2011 15:36:33 GMT mulligan [782]
	* src/ASM/BitVectorTrie.ma (modified)
	* src/ASM/Util.ma (modified)
	* src/ERTL/ERTL.ma (modified)
	* src/RTL/RTL.ma (modified)
	* src/RTL/RTLtoERTL.ma (modified)
	* src/common/Identifiers.ma (modified)
	* src/utilities/RegisterSet.ma (modified)

	More work on rtl-ertl pass from today, plus resolved conflict.


Wed, 27 Apr 2011 15:25:26 GMT mulligan [777]
	* src/ASM/I8051.ma (modified)
	* src/ASM/RegisterSet.ma (added)
	* src/ASM/Util.ma (modified)
	* src/ERTL/ERTL.ma (modified)
	* src/ERTL/Uses.ma (modified)
	* src/RTL/RTLtoERTL.ma (modified)
	* src/common/Registers.ma (modified)

	Lots of work on RTL to ERTL pass from today.


Wed, 20 Apr 2011 09:33:35 GMT mulligan [763]
	* src/RTL/RTLtoERTL.ma (modified)

	Changes to RTL-ERTL pass.


Mon, 18 Apr 2011 15:32:46 GMT mulligan [759]
	* src/ERTL/ERTL.ma (modified)
	* src/ERTL/ERTLToLTL.ma (modified)
	* src/LTL/LTLToLIN.ma (modified)
	* src/RTL/RTLtoERTL.ma (modified)

	More work on the RTL to ERTL pass.


Fri, 15 Apr 2011 15:47:32 GMT mulligan [756]
	* src/ERTL/Build.ma (modified)
	* src/ERTL/ERTL.ma (modified)
	* src/ERTL/Liveness.ma (modified)
	* src/ERTL/Uses.ma (modified)
	* src/RTL/RTL.ma (modified)
	* src/RTL/RTLtoERTL.ma (added)

	Made a start on RTL.  Renaming in ERTL and below to move closer to ...


Fri, 15 Apr 2011 11:29:16 GMT mulligan [754]
	* src/RTL (added)
	* src/RTL/RTL.ma (added)

	Syntax of RTL.