diff options
| -rw-r--r-- | frontend/IndexType.dcl | 6 | ||||
| -rw-r--r-- | frontend/IndexType.icl | 6 | ||||
| -rw-r--r-- | frontend/syntax.dcl | 9 |
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 |