Ignore:
Timestamp:
Feb 23, 2013, 1:16:55 AM (7 years ago)
Author:
sacerdot
Message:

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/errorMessages.ml

    r2649 r2717  
    6969| EmptyStack
    7070| OutOfBounds
     71| UnexpectedIO
     72| TerminatedEarly
    7173
    7274(** val errorMessage_rect_Type4 :
     
    7779    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    7880    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
    79     errorMessage -> 'a1 **)
    80 let rec errorMessage_rect_Type4 h_MISSING h_EXTERNAL h_Jump_expansion_failed h_ValueIsNotABoolean h_BadCast h_BadlyTypedTerm h_UnknownIdentifier h_BadLvalueTerm h_FailedLoad h_FailedOp h_WrongNumberOfParameters h_FailedStore h_NonsenseState h_ReturnMismatch h_UnknownLabel h_BadFunctionValue h_MainMissing h_UnknownField h_UndeclaredIdentifier h_BadlyTypedAccess h_BadLvalue h_MissingField h_FIXME h_MissingLabel h_ParamGlobalMixup h_DuplicateLabel h_TypeMismatch h_UnknownLocal h_FailedConstant h_BadState h_StoppedMidIO h_UnsupportedOp h_CorruptedPointer h_NotATwoBytesPointer h_ValueNotABoolean h_NotAnInt32Val h_WrongLength h_InitDataStoreFailed h_DuplicateVariable h_MissingId h_IllTypedEvent h_InternalStackFull h_InternalStackEmpty h_BadProgramCounter h_ProgramCounterOutOfCode h_PointNotFound h_LabelNotFound h_MissingSymbol h_BadFunction h_SuccessorNotProvided h_BadPointer h_NoSuccessor h_MissingStackSize h_ExternalMain h_BadRegister h_BadMain h_MissingRegister h_MissingStatement h_BadJumpTable h_BadJumpValue h_FinalState h_EmptyStack h_OutOfBounds = function
     81    'a1 -> 'a1 -> errorMessage -> 'a1 **)
     82let rec errorMessage_rect_Type4 h_MISSING h_EXTERNAL h_Jump_expansion_failed h_ValueIsNotABoolean h_BadCast h_BadlyTypedTerm h_UnknownIdentifier h_BadLvalueTerm h_FailedLoad h_FailedOp h_WrongNumberOfParameters h_FailedStore h_NonsenseState h_ReturnMismatch h_UnknownLabel h_BadFunctionValue h_MainMissing h_UnknownField h_UndeclaredIdentifier h_BadlyTypedAccess h_BadLvalue h_MissingField h_FIXME h_MissingLabel h_ParamGlobalMixup h_DuplicateLabel h_TypeMismatch h_UnknownLocal h_FailedConstant h_BadState h_StoppedMidIO h_UnsupportedOp h_CorruptedPointer h_NotATwoBytesPointer h_ValueNotABoolean h_NotAnInt32Val h_WrongLength h_InitDataStoreFailed h_DuplicateVariable h_MissingId h_IllTypedEvent h_InternalStackFull h_InternalStackEmpty h_BadProgramCounter h_ProgramCounterOutOfCode h_PointNotFound h_LabelNotFound h_MissingSymbol h_BadFunction h_SuccessorNotProvided h_BadPointer h_NoSuccessor h_MissingStackSize h_ExternalMain h_BadRegister h_BadMain h_MissingRegister h_MissingStatement h_BadJumpTable h_BadJumpValue h_FinalState h_EmptyStack h_OutOfBounds h_UnexpectedIO h_TerminatedEarly = function
    8183| MISSING -> h_MISSING
    8284| EXTERNAL -> h_EXTERNAL
     
    142144| EmptyStack -> h_EmptyStack
    143145| OutOfBounds -> h_OutOfBounds
     146| UnexpectedIO -> h_UnexpectedIO
     147| TerminatedEarly -> h_TerminatedEarly
    144148
    145149(** val errorMessage_rect_Type5 :
     
    150154    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    151155    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
    152     errorMessage -> 'a1 **)
    153 let rec errorMessage_rect_Type5 h_MISSING h_EXTERNAL h_Jump_expansion_failed h_ValueIsNotABoolean h_BadCast h_BadlyTypedTerm h_UnknownIdentifier h_BadLvalueTerm h_FailedLoad h_FailedOp h_WrongNumberOfParameters h_FailedStore h_NonsenseState h_ReturnMismatch h_UnknownLabel h_BadFunctionValue h_MainMissing h_UnknownField h_UndeclaredIdentifier h_BadlyTypedAccess h_BadLvalue h_MissingField h_FIXME h_MissingLabel h_ParamGlobalMixup h_DuplicateLabel h_TypeMismatch h_UnknownLocal h_FailedConstant h_BadState h_StoppedMidIO h_UnsupportedOp h_CorruptedPointer h_NotATwoBytesPointer h_ValueNotABoolean h_NotAnInt32Val h_WrongLength h_InitDataStoreFailed h_DuplicateVariable h_MissingId h_IllTypedEvent h_InternalStackFull h_InternalStackEmpty h_BadProgramCounter h_ProgramCounterOutOfCode h_PointNotFound h_LabelNotFound h_MissingSymbol h_BadFunction h_SuccessorNotProvided h_BadPointer h_NoSuccessor h_MissingStackSize h_ExternalMain h_BadRegister h_BadMain h_MissingRegister h_MissingStatement h_BadJumpTable h_BadJumpValue h_FinalState h_EmptyStack h_OutOfBounds = function
     156    'a1 -> 'a1 -> errorMessage -> 'a1 **)
     157let rec errorMessage_rect_Type5 h_MISSING h_EXTERNAL h_Jump_expansion_failed h_ValueIsNotABoolean h_BadCast h_BadlyTypedTerm h_UnknownIdentifier h_BadLvalueTerm h_FailedLoad h_FailedOp h_WrongNumberOfParameters h_FailedStore h_NonsenseState h_ReturnMismatch h_UnknownLabel h_BadFunctionValue h_MainMissing h_UnknownField h_UndeclaredIdentifier h_BadlyTypedAccess h_BadLvalue h_MissingField h_FIXME h_MissingLabel h_ParamGlobalMixup h_DuplicateLabel h_TypeMismatch h_UnknownLocal h_FailedConstant h_BadState h_StoppedMidIO h_UnsupportedOp h_CorruptedPointer h_NotATwoBytesPointer h_ValueNotABoolean h_NotAnInt32Val h_WrongLength h_InitDataStoreFailed h_DuplicateVariable h_MissingId h_IllTypedEvent h_InternalStackFull h_InternalStackEmpty h_BadProgramCounter h_ProgramCounterOutOfCode h_PointNotFound h_LabelNotFound h_MissingSymbol h_BadFunction h_SuccessorNotProvided h_BadPointer h_NoSuccessor h_MissingStackSize h_ExternalMain h_BadRegister h_BadMain h_MissingRegister h_MissingStatement h_BadJumpTable h_BadJumpValue h_FinalState h_EmptyStack h_OutOfBounds h_UnexpectedIO h_TerminatedEarly = function
    154158| MISSING -> h_MISSING
    155159| EXTERNAL -> h_EXTERNAL
     
    215219| EmptyStack -> h_EmptyStack
    216220| OutOfBounds -> h_OutOfBounds
     221| UnexpectedIO -> h_UnexpectedIO
     222| TerminatedEarly -> h_TerminatedEarly
    217223
    218224(** val errorMessage_rect_Type3 :
     
    223229    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    224230    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
    225     errorMessage -> 'a1 **)
    226 let rec errorMessage_rect_Type3 h_MISSING h_EXTERNAL h_Jump_expansion_failed h_ValueIsNotABoolean h_BadCast h_BadlyTypedTerm h_UnknownIdentifier h_BadLvalueTerm h_FailedLoad h_FailedOp h_WrongNumberOfParameters h_FailedStore h_NonsenseState h_ReturnMismatch h_UnknownLabel h_BadFunctionValue h_MainMissing h_UnknownField h_UndeclaredIdentifier h_BadlyTypedAccess h_BadLvalue h_MissingField h_FIXME h_MissingLabel h_ParamGlobalMixup h_DuplicateLabel h_TypeMismatch h_UnknownLocal h_FailedConstant h_BadState h_StoppedMidIO h_UnsupportedOp h_CorruptedPointer h_NotATwoBytesPointer h_ValueNotABoolean h_NotAnInt32Val h_WrongLength h_InitDataStoreFailed h_DuplicateVariable h_MissingId h_IllTypedEvent h_InternalStackFull h_InternalStackEmpty h_BadProgramCounter h_ProgramCounterOutOfCode h_PointNotFound h_LabelNotFound h_MissingSymbol h_BadFunction h_SuccessorNotProvided h_BadPointer h_NoSuccessor h_MissingStackSize h_ExternalMain h_BadRegister h_BadMain h_MissingRegister h_MissingStatement h_BadJumpTable h_BadJumpValue h_FinalState h_EmptyStack h_OutOfBounds = function
     231    'a1 -> 'a1 -> errorMessage -> 'a1 **)
     232let rec errorMessage_rect_Type3 h_MISSING h_EXTERNAL h_Jump_expansion_failed h_ValueIsNotABoolean h_BadCast h_BadlyTypedTerm h_UnknownIdentifier h_BadLvalueTerm h_FailedLoad h_FailedOp h_WrongNumberOfParameters h_FailedStore h_NonsenseState h_ReturnMismatch h_UnknownLabel h_BadFunctionValue h_MainMissing h_UnknownField h_UndeclaredIdentifier h_BadlyTypedAccess h_BadLvalue h_MissingField h_FIXME h_MissingLabel h_ParamGlobalMixup h_DuplicateLabel h_TypeMismatch h_UnknownLocal h_FailedConstant h_BadState h_StoppedMidIO h_UnsupportedOp h_CorruptedPointer h_NotATwoBytesPointer h_ValueNotABoolean h_NotAnInt32Val h_WrongLength h_InitDataStoreFailed h_DuplicateVariable h_MissingId h_IllTypedEvent h_InternalStackFull h_InternalStackEmpty h_BadProgramCounter h_ProgramCounterOutOfCode h_PointNotFound h_LabelNotFound h_MissingSymbol h_BadFunction h_SuccessorNotProvided h_BadPointer h_NoSuccessor h_MissingStackSize h_ExternalMain h_BadRegister h_BadMain h_MissingRegister h_MissingStatement h_BadJumpTable h_BadJumpValue h_FinalState h_EmptyStack h_OutOfBounds h_UnexpectedIO h_TerminatedEarly = function
    227233| MISSING -> h_MISSING
    228234| EXTERNAL -> h_EXTERNAL
     
    288294| EmptyStack -> h_EmptyStack
    289295| OutOfBounds -> h_OutOfBounds
     296| UnexpectedIO -> h_UnexpectedIO
     297| TerminatedEarly -> h_TerminatedEarly
    290298
    291299(** val errorMessage_rect_Type2 :
     
    296304    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    297305    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
    298     errorMessage -> 'a1 **)
    299 let rec errorMessage_rect_Type2 h_MISSING h_EXTERNAL h_Jump_expansion_failed h_ValueIsNotABoolean h_BadCast h_BadlyTypedTerm h_UnknownIdentifier h_BadLvalueTerm h_FailedLoad h_FailedOp h_WrongNumberOfParameters h_FailedStore h_NonsenseState h_ReturnMismatch h_UnknownLabel h_BadFunctionValue h_MainMissing h_UnknownField h_UndeclaredIdentifier h_BadlyTypedAccess h_BadLvalue h_MissingField h_FIXME h_MissingLabel h_ParamGlobalMixup h_DuplicateLabel h_TypeMismatch h_UnknownLocal h_FailedConstant h_BadState h_StoppedMidIO h_UnsupportedOp h_CorruptedPointer h_NotATwoBytesPointer h_ValueNotABoolean h_NotAnInt32Val h_WrongLength h_InitDataStoreFailed h_DuplicateVariable h_MissingId h_IllTypedEvent h_InternalStackFull h_InternalStackEmpty h_BadProgramCounter h_ProgramCounterOutOfCode h_PointNotFound h_LabelNotFound h_MissingSymbol h_BadFunction h_SuccessorNotProvided h_BadPointer h_NoSuccessor h_MissingStackSize h_ExternalMain h_BadRegister h_BadMain h_MissingRegister h_MissingStatement h_BadJumpTable h_BadJumpValue h_FinalState h_EmptyStack h_OutOfBounds = function
     306    'a1 -> 'a1 -> errorMessage -> 'a1 **)
     307let rec errorMessage_rect_Type2 h_MISSING h_EXTERNAL h_Jump_expansion_failed h_ValueIsNotABoolean h_BadCast h_BadlyTypedTerm h_UnknownIdentifier h_BadLvalueTerm h_FailedLoad h_FailedOp h_WrongNumberOfParameters h_FailedStore h_NonsenseState h_ReturnMismatch h_UnknownLabel h_BadFunctionValue h_MainMissing h_UnknownField h_UndeclaredIdentifier h_BadlyTypedAccess h_BadLvalue h_MissingField h_FIXME h_MissingLabel h_ParamGlobalMixup h_DuplicateLabel h_TypeMismatch h_UnknownLocal h_FailedConstant h_BadState h_StoppedMidIO h_UnsupportedOp h_CorruptedPointer h_NotATwoBytesPointer h_ValueNotABoolean h_NotAnInt32Val h_WrongLength h_InitDataStoreFailed h_DuplicateVariable h_MissingId h_IllTypedEvent h_InternalStackFull h_InternalStackEmpty h_BadProgramCounter h_ProgramCounterOutOfCode h_PointNotFound h_LabelNotFound h_MissingSymbol h_BadFunction h_SuccessorNotProvided h_BadPointer h_NoSuccessor h_MissingStackSize h_ExternalMain h_BadRegister h_BadMain h_MissingRegister h_MissingStatement h_BadJumpTable h_BadJumpValue h_FinalState h_EmptyStack h_OutOfBounds h_UnexpectedIO h_TerminatedEarly = function
    300308| MISSING -> h_MISSING
    301309| EXTERNAL -> h_EXTERNAL
     
    361369| EmptyStack -> h_EmptyStack
    362370| OutOfBounds -> h_OutOfBounds
     371| UnexpectedIO -> h_UnexpectedIO
     372| TerminatedEarly -> h_TerminatedEarly
    363373
    364374(** val errorMessage_rect_Type1 :
     
    369379    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    370380    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
    371     errorMessage -> 'a1 **)
    372 let rec errorMessage_rect_Type1 h_MISSING h_EXTERNAL h_Jump_expansion_failed h_ValueIsNotABoolean h_BadCast h_BadlyTypedTerm h_UnknownIdentifier h_BadLvalueTerm h_FailedLoad h_FailedOp h_WrongNumberOfParameters h_FailedStore h_NonsenseState h_ReturnMismatch h_UnknownLabel h_BadFunctionValue h_MainMissing h_UnknownField h_UndeclaredIdentifier h_BadlyTypedAccess h_BadLvalue h_MissingField h_FIXME h_MissingLabel h_ParamGlobalMixup h_DuplicateLabel h_TypeMismatch h_UnknownLocal h_FailedConstant h_BadState h_StoppedMidIO h_UnsupportedOp h_CorruptedPointer h_NotATwoBytesPointer h_ValueNotABoolean h_NotAnInt32Val h_WrongLength h_InitDataStoreFailed h_DuplicateVariable h_MissingId h_IllTypedEvent h_InternalStackFull h_InternalStackEmpty h_BadProgramCounter h_ProgramCounterOutOfCode h_PointNotFound h_LabelNotFound h_MissingSymbol h_BadFunction h_SuccessorNotProvided h_BadPointer h_NoSuccessor h_MissingStackSize h_ExternalMain h_BadRegister h_BadMain h_MissingRegister h_MissingStatement h_BadJumpTable h_BadJumpValue h_FinalState h_EmptyStack h_OutOfBounds = function
     381    'a1 -> 'a1 -> errorMessage -> 'a1 **)
     382let rec errorMessage_rect_Type1 h_MISSING h_EXTERNAL h_Jump_expansion_failed h_ValueIsNotABoolean h_BadCast h_BadlyTypedTerm h_UnknownIdentifier h_BadLvalueTerm h_FailedLoad h_FailedOp h_WrongNumberOfParameters h_FailedStore h_NonsenseState h_ReturnMismatch h_UnknownLabel h_BadFunctionValue h_MainMissing h_UnknownField h_UndeclaredIdentifier h_BadlyTypedAccess h_BadLvalue h_MissingField h_FIXME h_MissingLabel h_ParamGlobalMixup h_DuplicateLabel h_TypeMismatch h_UnknownLocal h_FailedConstant h_BadState h_StoppedMidIO h_UnsupportedOp h_CorruptedPointer h_NotATwoBytesPointer h_ValueNotABoolean h_NotAnInt32Val h_WrongLength h_InitDataStoreFailed h_DuplicateVariable h_MissingId h_IllTypedEvent h_InternalStackFull h_InternalStackEmpty h_BadProgramCounter h_ProgramCounterOutOfCode h_PointNotFound h_LabelNotFound h_MissingSymbol h_BadFunction h_SuccessorNotProvided h_BadPointer h_NoSuccessor h_MissingStackSize h_ExternalMain h_BadRegister h_BadMain h_MissingRegister h_MissingStatement h_BadJumpTable h_BadJumpValue h_FinalState h_EmptyStack h_OutOfBounds h_UnexpectedIO h_TerminatedEarly = function
    373383| MISSING -> h_MISSING
    374384| EXTERNAL -> h_EXTERNAL
     
    434444| EmptyStack -> h_EmptyStack
    435445| OutOfBounds -> h_OutOfBounds
     446| UnexpectedIO -> h_UnexpectedIO
     447| TerminatedEarly -> h_TerminatedEarly
    436448
    437449(** val errorMessage_rect_Type0 :
     
    442454    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    443455    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
    444     errorMessage -> 'a1 **)
    445 let rec errorMessage_rect_Type0 h_MISSING h_EXTERNAL h_Jump_expansion_failed h_ValueIsNotABoolean h_BadCast h_BadlyTypedTerm h_UnknownIdentifier h_BadLvalueTerm h_FailedLoad h_FailedOp h_WrongNumberOfParameters h_FailedStore h_NonsenseState h_ReturnMismatch h_UnknownLabel h_BadFunctionValue h_MainMissing h_UnknownField h_UndeclaredIdentifier h_BadlyTypedAccess h_BadLvalue h_MissingField h_FIXME h_MissingLabel h_ParamGlobalMixup h_DuplicateLabel h_TypeMismatch h_UnknownLocal h_FailedConstant h_BadState h_StoppedMidIO h_UnsupportedOp h_CorruptedPointer h_NotATwoBytesPointer h_ValueNotABoolean h_NotAnInt32Val h_WrongLength h_InitDataStoreFailed h_DuplicateVariable h_MissingId h_IllTypedEvent h_InternalStackFull h_InternalStackEmpty h_BadProgramCounter h_ProgramCounterOutOfCode h_PointNotFound h_LabelNotFound h_MissingSymbol h_BadFunction h_SuccessorNotProvided h_BadPointer h_NoSuccessor h_MissingStackSize h_ExternalMain h_BadRegister h_BadMain h_MissingRegister h_MissingStatement h_BadJumpTable h_BadJumpValue h_FinalState h_EmptyStack h_OutOfBounds = function
     456    'a1 -> 'a1 -> errorMessage -> 'a1 **)
     457let rec errorMessage_rect_Type0 h_MISSING h_EXTERNAL h_Jump_expansion_failed h_ValueIsNotABoolean h_BadCast h_BadlyTypedTerm h_UnknownIdentifier h_BadLvalueTerm h_FailedLoad h_FailedOp h_WrongNumberOfParameters h_FailedStore h_NonsenseState h_ReturnMismatch h_UnknownLabel h_BadFunctionValue h_MainMissing h_UnknownField h_UndeclaredIdentifier h_BadlyTypedAccess h_BadLvalue h_MissingField h_FIXME h_MissingLabel h_ParamGlobalMixup h_DuplicateLabel h_TypeMismatch h_UnknownLocal h_FailedConstant h_BadState h_StoppedMidIO h_UnsupportedOp h_CorruptedPointer h_NotATwoBytesPointer h_ValueNotABoolean h_NotAnInt32Val h_WrongLength h_InitDataStoreFailed h_DuplicateVariable h_MissingId h_IllTypedEvent h_InternalStackFull h_InternalStackEmpty h_BadProgramCounter h_ProgramCounterOutOfCode h_PointNotFound h_LabelNotFound h_MissingSymbol h_BadFunction h_SuccessorNotProvided h_BadPointer h_NoSuccessor h_MissingStackSize h_ExternalMain h_BadRegister h_BadMain h_MissingRegister h_MissingStatement h_BadJumpTable h_BadJumpValue h_FinalState h_EmptyStack h_OutOfBounds h_UnexpectedIO h_TerminatedEarly = function
    446458| MISSING -> h_MISSING
    447459| EXTERNAL -> h_EXTERNAL
     
    507519| EmptyStack -> h_EmptyStack
    508520| OutOfBounds -> h_OutOfBounds
    509 
     521| UnexpectedIO -> h_UnexpectedIO
     522| TerminatedEarly -> h_TerminatedEarly
     523
Note: See TracChangeset for help on using the changeset viewer.