aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--frontend/IndexType.dcl6
-rw-r--r--frontend/IndexType.icl6
-rw-r--r--frontend/syntax.dcl9
3 files changed, 18 insertions, 3 deletions
diff --git a/frontend/IndexType.dcl b/frontend/IndexType.dcl
new file mode 100644
index 0000000..39eecc8
--- /dev/null
+++ b/frontend/IndexType.dcl
@@ -0,0 +1,6 @@
+definition module
+ IndexType
+
+:: Index :== Int
+
+:: CheatCompiler = CheatCompiler \ No newline at end of file
diff --git a/frontend/IndexType.icl b/frontend/IndexType.icl
new file mode 100644
index 0000000..20f3cef
--- /dev/null
+++ b/frontend/IndexType.icl
@@ -0,0 +1,6 @@
+implementation module
+ IndexType
+
+:: Index :== Int
+
+:: CheatCompiler = CheatCompiler \ No newline at end of file
diff --git a/frontend/syntax.dcl b/frontend/syntax.dcl
index 0cb99d9..68f7380 100644
--- a/frontend/syntax.dcl
+++ b/frontend/syntax.dcl
@@ -3,6 +3,7 @@ definition module syntax
import StdEnv
import scanner, general, typeproperties, Heap
+import IndexType
:: Ident =
{ id_name :: !String
@@ -135,7 +136,6 @@ instance == FunctionOrMacroIndex
ali_instances_range :: !IndexRange
}
-:: Index :== Int
NoIndex :== -1
@@ -632,7 +632,7 @@ from convertDynamics import :: TypeCodeVariableInfo, :: DynamicValueAliasInfo
VI_Extended !ExtendedVarInfo !VarInfo |
VI_Defined /* for marking type code variables during overloading */ | VI_LocallyDefined |
// MdM
- VI_CPSLocalExprVar !Int /* MdM - the index of the variable as generated by the theorem prover */
+ VI_CPSExprVar !CheatCompiler /* a pointer to a variable in CleanProverSystem is stored here, using a cast */
// ... MdM
| VI_Labelled_Empty {#Char} // RWS debugging
| VI_LocalLetVar // RWS, mark Let vars during case transformation
@@ -948,7 +948,10 @@ cNonRecursiveAppl :== False
| TVI_ConsInstance !DefinedSymbol //AA: generic cons instance function
| TVI_Normalized !Int /* MV - position of type variable in its definition */
| TVI_Expr !Expression /* AA: Expression corresponding to the type var during generic specialization */
-
+// MdM
+ | TVI_CPSTypeVar !CheatCompiler /* a pointer to a variable in CleanProverSystem is stored here, using a cast */
+// ... MdM
+
:: TypeVarInfoPtr :== Ptr TypeVarInfo
:: TypeVarHeap :== Heap TypeVarInfo