definition module syntax import StdEnv import scanner, general, typeproperties, Heap PA_BUG on off :== on switch_import_syntax one_point_three two_point_zero :== one_point_three /* when finally removing this switch also remove the argument of STE_Instance and ID_OldSyntax */ SwitchFusion fuse dont_fuse :== dont_fuse :: Ident = { id_name :: !String , id_info :: !SymbolPtr } instance toString Ident /* Each Identifier is equipped with a pointer to a SymbolTableEntry that is used for binding the identifier with its definition. */ :: SymbolTable :== Heap SymbolTableEntry :: SymbolPtr :== Ptr SymbolTableEntry :: SymbolTableEntry = { ste_kind :: !STE_Kind , ste_index :: !Index , ste_def_level :: !Level , ste_previous :: SymbolTableEntry } :: STE_BoundTypeVariable = { stv_count :: !Int, stv_attribute :: !TypeAttribute, stv_info_ptr :: !TypeVarInfoPtr /* TD */, stv_position :: Int } :: STE_Kind = STE_FunctionOrMacro ![Index] | STE_Type | STE_Constructor | STE_Selector ![Global Index] | STE_Field !Ident | STE_Class | STE_Member | STE_Generic // AA: For generic declarations | STE_Instance !Ident // argument: the class (used in explicitimports (1.3 syntax only)) | STE_Variable !VarInfoPtr | STE_TypeVariable !TypeVarInfoPtr | STE_TypeAttribute !AttrVarInfoPtr | STE_BoundTypeVariable !STE_BoundTypeVariable | STE_Imported !STE_Kind !Index | STE_DclFunction | STE_Module !(Module (CollectedDefinitions ClassInstance IndexRange)) | STE_ClosedModule | STE_Empty /* for creating class dictionaries */ | STE_DictType !CheckedTypeDef | STE_DictCons !ConsDef | STE_DictField !SelectorDef | STE_Called ![Index] /* used during macro expansion to indicate that this function is called */ | STE_ExplImpSymbol !Int | STE_ExplImpComponentNrs ![ComponentNrAndIndex] ![Declaration] /* stores the numbers of all module components that import the symbol from the "actual" dcl module. Further for each class all encountered instances are accumulated. */ | STE_BelongingSymbol !Int :: Declaration = Declaration !DeclarationRecord :: DeclarationRecord = { decl_ident :: !Ident , decl_pos :: !Position , decl_kind :: !STE_Kind , decl_index :: !Index } :: ComponentNrAndIndex = { cai_component_nr :: !Int , cai_index :: !Int // points into ExplImpInfos } :: Global object = { glob_object :: !object , glob_module :: !Index } :: Module defs = { mod_name :: !Ident , mod_type :: !ModuleKind , mod_imports :: ![ParsedImport] , mod_imported_objects :: ![ImportedObject] , mod_defs :: !defs } :: ParsedModule :== Module [ParsedDefinition] :: ScannedModule :== Module (CollectedDefinitions (ParsedInstance FunDef) IndexRange) :: ModuleKind = MK_Main | MK_Module | MK_System | MK_None :: RhsDefsOfType = ConsList ![ParsedConstructor] | SelectorList !Ident ![ATypeVar] ![ParsedSelector] | TypeSpec !AType | EmptyRhs !BITVECT :: CollectedDefinitions instance_kind macro_defs = { def_types :: ![TypeDef TypeRhs] , def_constructors :: ![ConsDef] , def_selectors :: ![SelectorDef] , def_macros :: !macro_defs , def_classes :: ![ClassDef] , def_members :: ![MemberDef] , def_generics :: ![GenericDef] // AA , def_funtypes :: ![FunType] , def_instances :: ![instance_kind] } :: LocalDefs = LocalParsedDefs [ParsedDefinition] | CollectedLocalDefs CollectedLocalDefs :: IndexRange = { ir_from :: !Index, ir_to :: !Index } :: Index :== Int NoIndex :== -1 :: Level :== Int NotALevel :== -1 :: CollectedLocalDefs = { loc_functions :: !IndexRange , loc_nodes :: ![(Optional SymbolType, NodeDef ParsedExpr)] } :: NodeDef dst = { nd_dst ::!dst, nd_alts ::!OptGuardedAlts, nd_locals ::!LocalDefs, nd_position ::!Position } :: Rhs = { rhs_alts :: !OptGuardedAlts , rhs_locals :: !LocalDefs } cIsAFunction :== True cIsNotAFunction :== False :: ParsedDefinition = PD_Function Position Ident Bool [ParsedExpr] Rhs FunKind | PD_NodeDef Position ParsedExpr Rhs | PD_Type ParsedTypeDef | PD_TypeSpec Position Ident Priority (Optional SymbolType) Specials | PD_Class ClassDef [ParsedDefinition] | PD_Generic GenericDef // AA | PD_Instance (ParsedInstance ParsedDefinition) | PD_Instances [ParsedInstance ParsedDefinition] | PD_Import [ParsedImport] | PD_ImportedObjects [ImportedObject] | PD_Erroneous :: FunKind = FK_Function !Bool | FK_Macro | FK_Caf | FK_Unknown :: DefOrImpFunKind = FK_DefFunction !Bool| FK_ImpFunction !Bool | FK_DefMacro | FK_ImpMacro | FK_ImpCaf | FK_DefOrImpUnknown cNameNotLocationDependent :== False cNameLocationDependent :== True :: ParsedSelector = { ps_field_name :: !Ident , ps_selector_name :: !Ident , ps_field_type :: !AType , ps_field_var :: !Ident , ps_field_pos :: !Position } :: ParsedConstructor = { pc_cons_name :: !Ident , pc_cons_arity :: !Int , pc_exi_vars :: ![ATypeVar] , pc_arg_types :: ![AType] , pc_cons_prio :: !Priority , pc_cons_pos :: !Position } :: ParsedInstance member = { pi_class :: !Ident , pi_ident :: !Ident , pi_types :: ![Type] , pi_context :: ![TypeContext] , pi_pos :: !Position , pi_members :: ![member] , pi_specials :: !Specials , pi_generate :: !Bool // AA: instance is to be generated } /* Objects of type Specials are used to specify specialized instances of overloaded functions. These can only occur in definition modules. After parsing the SP_ParsedSubstitutions alternative is used to indicate the specific instantiation. The SP_Substitutions alternative is used to deduce the type of the specialized version. Finally the SP_ContextTypes alternative is set and used during the typing to check whether this instance has been used. The auxiliary SP_FunIndex alternative is used to store the index of the function that has been specialized. */ :: Specials = SP_ParsedSubstitutions ![Env Type TypeVar] | SP_Substitutions ![SpecialSubstitution] | SP_ContextTypes ![Special] | SP_FunIndex !Index | SP_TypeOffset !Int | SP_None :: SpecialSubstitution = { ss_environ :: !Env Type TypeVar , ss_context :: ![TypeContext] , ss_vars :: ![TypeVar] , ss_attrs :: ![AttributeVar] } :: Special = { spec_index :: !Global Index , spec_types :: ![[Type]] , spec_vars :: ![TypeVar] , spec_attrs :: ![AttributeVar] } :: AttrInequality = { ai_demanded :: !AttributeVar , ai_offered :: !AttributeVar } :: DefinedSymbol = { ds_ident :: !Ident , ds_arity :: !Int , ds_index :: !Index } :: ClassDef = { class_name :: !Ident , class_arity :: !Int , class_args :: ![TypeVar] , class_context :: ![TypeContext] , class_members :: !{# DefinedSymbol} , class_dictionary :: !DefinedSymbol , class_pos :: !Position , class_cons_vars :: !BITVECT } :: MemberDef = { me_symb :: !Ident , me_class :: !Global Index , me_offset :: !Index , me_type :: !SymbolType , me_type_ptr :: !VarInfoPtr , me_class_vars :: ![TypeVar] , me_pos :: !Position , me_priority :: !Priority } // AA ... :: GenericDef = { gen_name :: !Ident // the generics name in the IC_Class , gen_member_name :: !Ident // the generics name in the IC_Member , gen_type :: !GenericType , gen_pos :: !Position , gen_classes :: !GenericClassInfos // generated classes , gen_isomap :: !DefinedSymbol // isomap function } :: GenericType = { gt_type :: !SymbolType , gt_vars :: ![TypeVar] // generic arguments , gt_arity :: !Int // number of generic arguments } :: GenericClassInfo = { gci_kind :: !TypeKind , gci_class :: !DefinedSymbol } :: GenericClassInfos :== [GenericClassInfo] getGenericClassForKind :: !GenericDef !TypeKind -> (!Bool, DefinedSymbol) addGenericKind :: !GenericDef !TypeKind -> !GenericDef // ... AA :: InstanceType = { it_vars :: [TypeVar] , it_types :: ![Type] , it_attr_vars :: [AttributeVar] , it_context :: ![TypeContext] } :: ClassInstance = { ins_class :: !Global DefinedSymbol , ins_ident :: !Ident , ins_type :: !InstanceType , ins_members :: !{# DefinedSymbol} , ins_specials :: !Specials , ins_pos :: !Position , ins_is_generic :: !Bool //AA , ins_generate :: !Bool //AA , ins_generic :: !Global Index //AA } /* :: Export = { export_class :: Ident , export_types :: [Type] } */ :: Import from_symbol = { import_module :: !Ident , import_symbols :: ![from_symbol] , import_file_position:: !Position // for error messages } instance toString (Import from_symbol), AttributeVar, TypeAttribute, Annotation :: ParsedImport :== Import ImportDeclaration :: ImportedIdent = { ii_ident :: !Ident , ii_extended :: !Bool } :: ImportDeclaration = ID_Function !ImportedIdent | ID_Class !ImportedIdent !(Optional [ImportedIdent]) | ID_Type !ImportedIdent !(Optional [ImportedIdent]) | ID_Record !ImportedIdent !(Optional [ImportedIdent]) | ID_Instance !ImportedIdent !Ident !(![Type],![TypeContext]) | ID_OldSyntax ![Ident] cIsImportedLibrary :== True cIsImportedObject :== False :: ImportedObject = { io_is_library :: !Bool , io_name :: !{#Char} } :: RecordType = { rt_constructor :: !DefinedSymbol , rt_fields :: !{# FieldSymbol} } :: FieldSymbol = { fs_name :: !Ident , fs_var :: !Ident , fs_index :: !Index } :: TypeRhs = AlgType ![DefinedSymbol] | SynType !AType | RecordType !RecordType | AbstractType !BITVECT | UnknownType :: ParsedTypeDef :== TypeDef RhsDefsOfType :: CheckedTypeDef :== TypeDef TypeRhs /* cIsHyperStrict :== True cIsNotHyperStrict :== False */ cAllBitsClear :== 0 cIsHyperStrict :== 1 cIsNonCoercible :== 2 // cMayBeNonCoercible :== 4 :: TypeDef type_rhs = { td_name :: !Ident , td_index :: !Int , td_arity :: !Int , td_args :: ![ATypeVar] , td_attrs :: ![AttributeVar] , td_context :: ![TypeContext] , td_rhs :: !type_rhs , td_attribute :: !TypeAttribute , td_pos :: !Position } :: TypeDefInfo = { tdi_kinds :: ![TypeKind] , tdi_properties :: !BITVECT , tdi_group :: ![Global Index] , tdi_group_nr :: !Int , tdi_group_vars :: ![Int] , tdi_cons_vars :: ![Int] , tdi_tmp_index :: !Int , tdi_classification :: !TypeClassification } :: TypeDefInfos :== {# .{# TypeDefInfo}} :: FunType = { ft_symb :: !Ident , ft_arity :: !Int , ft_priority :: !Priority , ft_type :: !SymbolType , ft_pos :: !Position , ft_specials :: !Specials , ft_type_ptr :: !VarInfoPtr } :: FreeVar = { fv_def_level :: !Level , fv_name :: !Ident , fv_info_ptr :: !VarInfoPtr // , fv_expr_ptr :: !ExprInfoPtr , fv_count :: !Int } :: FunCall = { fc_level :: !Level , fc_index :: !Index } /* Sjaak 19-3-2001 ... */ FI_IsMacroFun :== 1 // whether the function is a local function of a macro FI_HasTypeSpec :== 2 // whether the function has u user defined type :: FunInfo = { fi_calls :: ![FunCall] , fi_group_index :: !Index , fi_def_level :: !Level , fi_free_vars :: ![FreeVar] , fi_local_vars :: ![FreeVar] , fi_dynamics :: ![ExprInfoPtr] , fi_properties :: !BITVECT } /* ... Sjaak 19-3-2001 */ :: ParsedBody = { pb_args :: ![ParsedExpr] , pb_rhs :: !Rhs , pb_position :: !Position } :: CheckedBody = { cb_args :: ![FreeVar] , cb_rhs :: ![CheckedAlternative] } :: CheckedAlternative = { ca_rhs :: !Expression , ca_position :: !Position // the position is NoPos iff the position information for this } // alternative is already stored in a case alternative // (in ap_position, bp_position or dp_position) :: TransformedBody = { tb_args :: ![FreeVar] , tb_rhs :: !Expression } :: FunctionBody = ParsedBody ![ParsedBody] | CheckedBody !CheckedBody /* The next three constructors are used during macro expansion (module transform) */ | PartioningMacro | PartioningFunction !CheckedBody !Int | RhsMacroBody !CheckedBody /* macro expansion transforms a CheckedBody into a TransformedBody */ | TransformedBody !TransformedBody | Expanding ![FreeVar] // the parameters of the newly generated function | BackendBody ![BackendBody] | NoBody :: BackendBody = { bb_args :: ![FunctionPattern] , bb_rhs :: !Expression } :: FunDef = { fun_symb :: !Ident , fun_arity :: !Int , fun_priority :: !Priority , fun_body :: !FunctionBody , fun_type :: !Optional SymbolType , fun_pos :: !Position , fun_index :: !Int , fun_kind :: !DefOrImpFunKind , fun_lifted :: !Int , fun_info :: !FunInfo } cIsAGlobalVar :== True cIsALocalVar :== False :: ConsClasses = { cc_size ::!Int , cc_args ::![ConsClass] , cc_linear_bits ::![Bool] } :: ConsClass :== Int :: OptionalVariable :== Optional (Bind Ident VarInfoPtr) :: AuxiliaryPattern = AP_Algebraic !(Global DefinedSymbol) !Index [AuxiliaryPattern] OptionalVariable | AP_Variable !Ident !VarInfoPtr OptionalVariable | AP_Basic !BasicValue OptionalVariable | AP_Dynamic !AuxiliaryPattern !DynamicType !OptionalVariable | AP_Constant !AP_Kind !(Global DefinedSymbol) !Priority | AP_WildCard !OptionalVariable | AP_Empty !Ident :: AP_Kind = APK_Constructor !Index | APK_Macro :: VarInfo = VI_Empty | VI_Type !AType !(Optional CoercionPosition) | VI_Occurrence !Occurrence | VI_UsedVar !Ident | VI_Expression !Expression | VI_Variable !Ident !VarInfoPtr | VI_LiftedVariable !VarInfoPtr | VI_Count !Int /* the reference count of a variable */ !Bool /* true if the variable is global, false otherwise */ | VI_AccVar !ConsClass !ArgumentPosition /* used during fusion to determine accumulating parameters of functions */ | VI_Alias !BoundVar /* used for resolving aliases just before type checking (in transform) */ | /* used during elimination and lifting of cases */ VI_FreeVar !Ident !VarInfoPtr !Int !AType | VI_BoundVar !AType | VI_LocalVar | VI_ClassVar !Ident !VarInfoPtr !Int | /* to hold dictionary variables during overloading */ VI_ForwardClassVar !VarInfoPtr | /* to hold the dictionary variable generated during overloading */ VI_Forward !BoundVar | VI_LetVar !LetVarInfo | VI_LetExpression !LetExpressionInfo | VI_CaseVar !VarInfoPtr | VI_CorrespondenceNumber !Int | /* it is assumed that this alternative is _only_ used in module comparedefimp */ VI_SequenceNumber !Int | VI_Used | /* for indicating that an imported function has been used */ VI_PropagationType !SymbolType | /* for storing the type with propagation environment of an imported function */ VI_ExpandedType !SymbolType | /* for storing the (expanded) type of an imported function */ VI_Record ![AuxiliaryPattern] | VI_Pattern !AuxiliaryPattern | VI_Default !Int | VI_Indirection !Int | /* used during conversion of dynamics; the Int indiacted the refenrence count */ VI_Body !SymbIdent !TransformedBody ![FreeVar] | /* used during fusion */ VI_Dictionary !SymbIdent ![Expression] !Type | /* used during fusion */ 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 */ // ... MdM :: ExtendedVarInfo = EVI_VarType !AType :: ArgumentPosition :== Int :: VarInfoPtr :== Ptr VarInfo :: LetVarInfo = { lvi_count :: !Int , lvi_depth :: !Int , lvi_new :: !Bool , lvi_var :: !Ident , lvi_expression :: !Expression , lvi_previous :: ![PreviousLetVarInfo] } :: PreviousLetVarInfo = { plvi_count :: !Int , plvi_depth :: !Int , plvi_new :: !Bool } :: LetExpressionStatus = LES_Untouched | LES_Moved | LES_Updated !Expression :: LetExpressionInfo = { lei_count :: !Int , lei_depth :: !Int , lei_var :: !FreeVar , lei_expression :: !Expression , lei_status :: !LetExpressionStatus , lei_type :: !AType } cNotVarNumber :== -1 :: BoundVar = { var_name :: !Ident , var_info_ptr :: !VarInfoPtr , var_expr_ptr :: !ExprInfoPtr } /* cRecursiveAppl :== True cNonRecursiveAppl :== False :: ApplicationKind :== Bool */ :: TypeSymbIdent = { type_name :: !Ident , type_arity :: !Int , type_index :: !Global Index , type_prop :: !TypeSymbProperties } :: TypeSymbProperties = { tsp_sign :: !SignClassification , tsp_propagation :: !PropClassification , tsp_coercible :: !Bool } :: SymbKind = SK_Unknown | SK_Function !(Global Index) | SK_LocalMacroFunction !Index | SK_OverloadedFunction !(Global Index) | SK_Generic !(Global Index) !TypeKind // AA | SK_Constructor !(Global Index) | SK_Macro !(Global Index) // | SK_RecordSelector !(Global Index) | SK_GeneratedFunction !FunctionInfoPtr !Index | SK_TypeCode /* Some auxiliary type definitions used during fusion. Actually, these definitions should have been given in seperate module. Unfortunately, Clean's module system forbids cyclic dependencies between def modules. */ :: FunctionHeap :== Heap FunctionInfo :: FunctionInfoPtr :== Ptr FunctionInfo :: FunctionInfo = FI_Empty | FI_Function !GeneratedFunction :: Producer = PR_Empty | PR_Function !SymbIdent !Index | PR_Class !App ![(BoundVar, Type)] !Type // | PR_Constructor !SymbIdent ![Expression] | PR_GeneratedFunction !SymbIdent !Index | PR_Curried !SymbIdent :: InstanceInfo = II_Empty | II_Node !{! Producer} !FunctionInfoPtr !InstanceInfo !InstanceInfo :: GeneratedFunction = { gf_fun_def :: !FunDef , gf_instance_info :: !InstanceInfo , gf_cons_args :: !ConsClasses , gf_fun_index :: !Index } /* ... main type definitions continued .... */ :: ExpressionHeap :== Heap ExprInfo :: ExprInfoPtr :== Ptr ExprInfo :: TempLocalVar :== Int :: DynamicPtr :== ExprInfoPtr :: ExprInfo = EI_Empty /* For handling overloading */ | EI_Overloaded !OverloadedCall /* initial, set by the type checker */ | EI_Instance !(Global DefinedSymbol) ![Expression] /* intermedediate, used during resolving of overloading */ // | EI_Selection ![Selection] !BoundVar ![Expression] /* intermedediate, used during resolving of overloading */ | EI_Selection ![Selection] !VarInfoPtr ![Expression] /* intermedediate, used during resolving of overloading */ | EI_Context ![Expression] /* intermedediate, used during resolving of overloading */ /* For handling dynamics */ | EI_Dynamic !(Optional DynamicType) | EI_DynamicType !DynamicType ![DynamicPtr] // | EI_DynamicType !DynamicType !(Optional ExprInfoPtr) /* Auxiliary, was EI_DynamicType before checking */ | EI_DynamicTypeWithVars ![TypeVar] !DynamicType ![DynamicPtr] // | EI_DynamicTypeWithVars ![TypeVar] !DynamicType !(Optional ExprInfoPtr) /* Auxiliary, used during type checking */ | EI_TempDynamicType !(Optional DynamicType) !AType ![TypeContext] !ExprInfoPtr !SymbIdent // | EI_TempDynamicPattern ![TypeVar] !DynamicType !(Optional ExprInfoPtr) ![TempLocalVar] !AType ![TypeContext] !ExprInfoPtr !SymbIdent | EI_TempDynamicPattern ![TypeVar] !DynamicType ![DynamicPtr] ![TempLocalVar] !AType ![TypeContext] !ExprInfoPtr !SymbIdent | EI_TypeOfDynamic ![VarInfoPtr] !TypeCodeExpression /* Final */ | EI_TypeOfDynamicPattern ![VarInfoPtr] !TypeCodeExpression /* Final */ | EI_TypeCode !TypeCodeExpression | EI_TypeCodes ![TypeCodeExpression] | EI_Attribute !Int /* EI_DictionaryType is used to store the instance type of a class. This type are used during fusion to generate proper types for the fusion result (i.e. the resulting function after elimination of dictionaries) */ | EI_DictionaryType !Type | EI_CaseType !CaseType | EI_LetType ![AType] | EI_CaseTypeAndRefCounts !CaseType !RefCountsInCase | EI_LetTypeAndRefCounts ![AType] ![Int] /* for converting case into function patterns the following auxiliary constuctors are used */ | EI_Default !Expression !AType !ExprInfoPtr | EI_DefaultFunction !SymbIdent ![Expression] | EI_Extended !ExtendedExprInfo !ExprInfo :: ExtendedExprInfo = EEI_ActiveCase !ActiveCaseInfo :: ActiveCaseInfo = { aci_params :: ![FreeVar] , aci_opt_unfolder :: !(Optional SymbIdent) , aci_free_vars :: !Optional [BoundVar] , aci_linearity_of_patterns :: ![[Bool]] } :: RefCountsInCase = { rcc_all_variables :: ![CountedVariable] , rcc_default_variables :: ![CountedVariable] , rcc_pattern_variables :: ![[CountedVariable]] } :: CountedVariable = { cv_variable :: !VarInfoPtr , cv_count :: !Int } /* :: UnboundVariable = { free_name :: !Ident , free_info_ptr :: !VarInfoPtr , free_selections :: ![Int] } */ /* OverloadedCall contains (type) information about functions that are overloaded. This structure is built during type checking and used after (standard) unification to insert the proper instances of the corresponding functions. */ :: OverloadedCall = { oc_symbol :: !SymbIdent , oc_context :: ![TypeContext] , oc_specials :: ![Special] } /* CaseType contains the type information needed to type the corresponding case construct: ct_pattern_type : the type of the pattern ct_result_type : the type of the result (of each pattern) ct_cons_types : the types of the arguments of each pattern constructor */ :: CaseType = { ct_pattern_type :: !AType , ct_result_type :: !AType , ct_cons_types :: ![[AType]] } :: SymbIdent = { symb_name :: !Ident , symb_kind :: !SymbKind , symb_arity :: !Int } :: ConsDef = { cons_symb :: !Ident , cons_type :: !SymbolType , cons_arg_vars :: ![[ATypeVar]] , cons_priority :: !Priority , cons_index :: !Index , cons_type_index :: !Index , cons_exi_vars :: ![ATypeVar] // , cons_exi_attrs :: ![AttributeVar] , cons_type_ptr :: !VarInfoPtr , cons_pos :: !Position } :: SelectorDef = { sd_symb :: !Ident , sd_field :: !Ident , sd_type :: !SymbolType , sd_exi_vars :: ![ATypeVar] // , sd_exi_attrs :: ![AttributeVar] , sd_field_nr :: !Int , sd_type_index :: !Int , sd_type_ptr :: !VarInfoPtr , sd_pos :: !Position } :: SymbolType = { st_vars :: ![TypeVar] , st_args :: ![AType] , st_arity :: !Int , st_result :: !AType , st_context :: ![TypeContext] , st_attr_vars :: ![AttributeVar] , st_attr_env :: ![AttrInequality] } :: TypeContext = { tc_class :: !Global DefinedSymbol , tc_types :: ![Type] , tc_var :: !VarInfoPtr } :: AType = { at_attribute :: !TypeAttribute , at_annotation :: !Annotation , at_type :: !Type } :: TempAttrId :== Int :: TempVarId :== Int :: Type = TA !TypeSymbIdent ![AType] | (-->) infixr 9 !AType !AType | (:@:) infixl 9 !ConsVariable ![AType] | TB !BasicType // | TFA [ATypeVar] Type | GTV !TypeVar | TV !TypeVar | TempV !TempVarId /* Auxiliary, used during type checking */ | TQV TypeVar | TempQV !TempVarId /* Auxiliary, used during type checking */ | TLifted !TypeVar /* Auxiliary, used during type checking of lifted arguments */ | TE :: ConsVariable = CV !TypeVar | TempCV !TempVarId | TempQCV !TempVarId :: DynamicType = { dt_uni_vars :: ![ATypeVar] , dt_global_vars :: ![TypeVar] , dt_type :: !AType } :: KindHeap :== Heap KindInfo :: KindInfoPtr :== Ptr KindInfo :: KindInfo = KI_Var !KindInfoPtr | KI_Indirection !KindInfo | KI_Arrow ![KindInfo] | KI_Const | KI_ConsVar | KI_VarBind !KindInfoPtr | KI_NormVar !Int :: TypeVarInfo = TVI_Empty | TVI_Type !Type | TVI_Forward !TempVarId | TVI_TypeKind !KindInfoPtr | TVI_SignClass !Index !SignClassification !TypeVarInfo | TVI_PropClass !Index !PropClassification !TypeVarInfo | TVI_Attribute TypeAttribute | TVI_CorrespondenceNumber !Int /* auxiliary used in module comparedefimp */ | TVI_AType !AType /* auxiliary used in module comparedefimp */ | TVI_Used /* to administer that this variable is encountered (in checkOpenTypes) */ | TVI_TypeCode !TypeCodeExpression | TVI_CPSLocalTypeVar !Int /* MdM - the index of the variable as generated by the theorem prover */ | TVI_Normalized !Int /* MV - position of type variable in its definition */ :: TypeVarInfoPtr :== Ptr TypeVarInfo :: TypeVarHeap :== Heap TypeVarInfo :: AttrVarInfo = AVI_Empty | AVI_Attr !TypeAttribute | AVI_Forward !TempAttrId | AVI_CorrespondenceNumber !Int /* auxiliary used in module comparedefimp */ | AVI_Used | AVI_Count !Int /* auxiliary used in module typesupport */ :: AttrVarInfoPtr :== Ptr AttrVarInfo :: AttrVarHeap :== Heap AttrVarInfo :: TypeHeaps = { th_vars :: ! .TypeVarHeap , th_attrs :: ! .AttrVarHeap } :: TypeVar = { tv_name :: !Ident , tv_info_ptr :: !TypeVarInfoPtr } :: ATypeVar = { atv_attribute :: !TypeAttribute , atv_annotation :: !Annotation , atv_variable :: !TypeVar } :: TypeAttribute = TA_Unique | TA_Multi | TA_Var !AttributeVar | TA_RootVar AttributeVar | TA_TempVar !Int | TA_TempExVar | TA_Anonymous | TA_None | TA_List !Int !TypeAttribute | TA_Locked !TypeAttribute | TA_MultiOfPropagatingConsVar // only filled in after type checking, semantically equal to TA_Multi :: AttributeVar = { av_name :: !Ident , av_info_ptr :: !AttrVarInfoPtr } :: Annotation = AN_Strict | AN_None :: BasicType = BT_Int | BT_Char | BT_Real | BT_Bool | BT_Dynamic | BT_File | BT_World | BT_String !Type /* the internal string type synonym only used to type string denotations */ :: BasicValue = BVI !String | BVC !String | BVB !Bool | BVR !String | BVS !String :: TypeKind = KindVar !KindInfoPtr | KindConst | KindArrow ![TypeKind] instance toString TypeKind instance <<< TypeKind instance == TypeKind instance toString KindInfo /* A few obscure type definitions */ :: Occurrence = { occ_ref_count :: !ReferenceCount // , occ_aliases :: ![[(FreeVar,Int)]] // , occ_expression :: !Expression , occ_bind :: !OccurrenceBinding , occ_observing :: !Bool // , occ_attribute :: !ExprInfoPtr , occ_previous :: ![ReferenceCount] } :: ReferenceCount = RC_Used !RC_Used | RC_Unused :: SelectiveUse = { su_field :: !Int, su_multiply :: ![ExprInfoPtr], su_uniquely :: ![ExprInfoPtr] } :: RC_Used = { rcu_multiply :: ![ExprInfoPtr], rcu_selectively :: ![SelectiveUse], rcu_uniquely :: ![ExprInfoPtr] } :: OccurrenceBinding = OB_Empty | OB_OpenLet !Expression | OB_LockedLet !Expression | OB_Pattern ![(FreeVar, Int)] !OccurrenceBinding // | OB_Closed !LetOccurrences | OB_Marked !LetOccurrences /* :: LetOccurrences = { lo_used_lets :: ![FreeVar] , lo_free_variables :: ![(FreeVar, ReferenceCount)] } */ :: OptGuardedAlts = GuardedAlts ![GuardedExpr] !(Optional ExprWithLocalDefs) | UnGuardedExpr !ExprWithLocalDefs :: GuardedExpr = { alt_nodes :: ![NodeDefWithLocals] , alt_guard :: !ParsedExpr , alt_expr :: !OptGuardedAlts , alt_ident :: !Ident , alt_position:: !Position } :: ExprWithLocalDefs = { ewl_nodes :: ![NodeDefWithLocals] , ewl_expr :: !ParsedExpr , ewl_locals :: !LocalDefs , ewl_position:: !Position } :: NodeDefWithLocals = { ndwl_strict :: !Bool , ndwl_def :: !Bind ParsedExpr ParsedExpr , ndwl_locals :: !LocalDefs , ndwl_position :: !Position } :: CaseAlt = { calt_pattern :: !ParsedExpr , calt_rhs :: !Rhs } :: LocalDef :== ParsedDefinition cUniqueSelection :== True cNonUniqueSelection :== False :: ParsedExpr = PE_List ![ParsedExpr] | PE_Ident !Ident | PE_Basic !BasicValue | PE_Bound !BoundExpr | PE_Lambda !Ident ![ParsedExpr] !ParsedExpr !Position | PE_Tuple ![ParsedExpr] | PE_Record !ParsedExpr !(Optional Ident) ![FieldAssignment] | PE_ArrayPattern ![ElemAssignment] | PE_UpdateComprehension !ParsedExpr !ParsedExpr !ParsedExpr ![Qualifier] | PE_ArrayDenot ![ParsedExpr] | PE_Selection !Bool !ParsedExpr ![ParsedSelection] | PE_Update !ParsedExpr [ParsedSelection] ParsedExpr | PE_Case !Ident !ParsedExpr [CaseAlt] | PE_If !Ident !ParsedExpr !ParsedExpr !ParsedExpr | PE_Let !Bool !LocalDefs !ParsedExpr | PE_Compr !GeneratorKind !ParsedExpr ![Qualifier] | PE_Sequ Sequence | PE_WildCard | PE_Field !ParsedExpr !(Global FieldSymbol) /* Auxiliary, used during checking */ | PE_ABC_Code ![String] !Bool | PE_Any_Code !(CodeBinding Ident) !(CodeBinding Ident) ![String] | PE_DynamicPattern !ParsedExpr !DynamicType | PE_Dynamic !ParsedExpr !(Optional DynamicType) | PE_Generic !Ident !TypeKind /* AA: For generics, kind indexed identifier */ | PE_Empty :: ParsedSelection = PS_Record !Ident !(Optional Ident) | PS_Array !ParsedExpr | PS_Erroneous :: GeneratorKind :== Bool cIsListGenerator :== True cIsArrayGenerator :== False :: LineAndColumn = {lc_line :: !Int, lc_column :: !Int} :: Generator = { gen_kind :: !GeneratorKind , gen_pattern :: !ParsedExpr , gen_expr :: !ParsedExpr , gen_position :: !LineAndColumn } :: Qualifier = { qual_generators :: ![Generator] , qual_filter :: !Optional ParsedExpr , qual_position :: !LineAndColumn , qual_filename :: !FileName } :: Sequence = SQ_FromThen ParsedExpr ParsedExpr | SQ_FromThenTo ParsedExpr ParsedExpr ParsedExpr | SQ_From ParsedExpr | SQ_FromTo ParsedExpr ParsedExpr :: BoundExpr :== Bind ParsedExpr Ident :: FieldAssignment :== Bind ParsedExpr Ident :: ElemAssignment :== Bind ParsedExpr [ParsedExpr] cIsStrict :== True cIsNotStrict :== False /* :: SelectorKind = SEK_Normal | SEK_First | SEK_Next | SEK_Last :: ArraySelector = DictionarySelection !(Global DefinedSymbol) !Int !Expression | SelectorInstance !(Global DefinedSymbol) */ :: Expression = Var !BoundVar | App !App | (@) infixl 9 !Expression ![Expression] | Let !Let | Case !Case | Selection !(Optional (Global DefinedSymbol)) !Expression ![Selection] // Yes: a "!" selection | Update !Expression ![Selection] Expression | RecordUpdate !(Global DefinedSymbol) !Expression ![Bind Expression (Global FieldSymbol)] | TupleSelect !DefinedSymbol !Int !Expression // | Lambda .[FreeVar] !Expression | BasicExpr !BasicValue !BasicType | WildCard | Conditional !Conditional | AnyCodeExpr !(CodeBinding BoundVar) !(CodeBinding FreeVar) ![String] | ABCCodeExpr ![String] !Bool | MatchExpr !(Optional (Global DefinedSymbol)) !(Global DefinedSymbol) !Expression | FreeVar FreeVar | Constant !SymbIdent !Int !Priority !Bool /* auxiliary clause used during checking */ | ClassVariable !VarInfoPtr /* auxiliary clause used during overloading */ | DynamicExpr !DynamicExpr // | TypeCase !TypeCase | TypeCodeExpression !TypeCodeExpression | EE | NoBind ExprInfoPtr /* auxiliary, to store fields that are not specified in a record expression */ :: CodeBinding variable :== Env String variable :: App = { app_symb :: !SymbIdent , app_args :: ![Expression] , app_info_ptr :: !ExprInfoPtr } :: Case = { case_expr :: !Expression // , case_guards :: ![PatternExpression] , case_guards :: !CasePatterns , case_default :: !Optional Expression , case_ident :: !Optional Ident , case_info_ptr :: !ExprInfoPtr , case_default_pos:: !Position } :: Let = { let_strict_binds :: ![LetBind] , let_lazy_binds :: ![LetBind] , let_expr :: !Expression , let_info_ptr :: !ExprInfoPtr , let_expr_position :: !Position } :: LetBind = { lb_dst :: !FreeVar , lb_src :: !Expression , lb_position :: !Position } :: Conditional = { if_cond :: !Expression , if_then :: !Expression , if_else :: !Optional Expression } /* :: Conditional = { if_cond :: !Condition , if_then :: !Expression , if_else :: !Optional Expression } :: Condition = { con_positive :: !Bool , con_expression :: !Expression } */ :: DynamicExpr = { dyn_expr :: !Expression , dyn_opt_type :: !Optional DynamicType , dyn_info_ptr :: !ExprInfoPtr , dyn_uni_vars :: ![VarInfoPtr] /* filled after type checking */ , dyn_type_code :: !TypeCodeExpression /* filled after type checking */ } :: CasePatterns = AlgebraicPatterns !(Global Index) ![AlgebraicPattern] | BasicPatterns !BasicType [BasicPattern] | DynamicPatterns [DynamicPattern] /* auxiliary */ | NoPattern /* auxiliary */ :: Selection = RecordSelection !(Global DefinedSymbol) !Int | ArraySelection !(Global DefinedSymbol) !ExprInfoPtr !Expression | DictionarySelection !BoundVar ![Selection] !ExprInfoPtr !Expression //:: TypeCodeExpression = TCE_Empty | TCE_Var !VarInfoPtr | TCE_Constructor !Index ![TypeCodeExpression] | TCE_Selector ![Selection] !VarInfoPtr :: TypeCodeExpression = TCE_Empty | TCE_Var !VarInfoPtr /* MV */ | TCE_TypeTerm !VarInfoPtr | TCE_Constructor !Index ![TypeCodeExpression] | TCE_Selector ![Selection] !VarInfoPtr :: GlobalTCType = GTT_Basic !BasicType | GTT_Constructor !TypeSymbIdent !String | GTT_Function /* :: PatternExpression = { guard_pattern :: !GuardPattern , guard_expr :: !Expression } :: GuardPattern = BasicPattern !BasicValue | AlgebraicPattern !(Global DefinedSymbol) ![FreeVar] | VariablePattern !FreeVar */ :: FunctionPattern = FP_Basic !BasicValue !(Optional FreeVar) | FP_Algebraic !(Global DefinedSymbol) ![FunctionPattern] !(Optional FreeVar) | FP_Variable !FreeVar | FP_Dynamic ![VarInfoPtr] !FreeVar !TypeCodeExpression !(Optional FreeVar) | FP_Empty :: AlgebraicPattern = { ap_symbol :: !(Global DefinedSymbol) , ap_vars :: ![FreeVar] , ap_expr :: !Expression , ap_position :: !Position } :: BasicPattern = { bp_value :: !BasicValue , bp_expr :: !Expression , bp_position :: !Position } :: TypeCase = { type_case_dynamic :: !Expression , type_case_patterns :: ![DynamicPattern] , type_case_default :: !Optional Expression , type_case_info_ptr :: !ExprInfoPtr } :: DynamicPattern = { dp_var :: !FreeVar , dp_type :: !ExprInfoPtr , dp_type_patterns_vars :: ![VarInfoPtr] /* filled after type checking */ , dp_type_code :: !TypeCodeExpression /* filled after type checking */ , dp_rhs :: !Expression , dp_position :: !Position } /* error handling */ :: Position = FunPos FileName LineNr FunctName | LinePos FileName LineNr | PreDefPos Ident | NoPos :: CoercionPosition = CP_Expression !Expression | CP_FunArg !Ident !Int // Function symbol, argument position (>=1) :: IdentPos = { ip_ident :: !Ident , ip_line :: !Int , ip_file :: !FileName } :: FileName :== String :: FunctName :== String :: LineNr :== Int cNotALineNumber :== -1 /* Used for hashing identifiers */ instance == ModuleKind, Ident instance <<< (Module a) | <<< a, ParsedDefinition, InstanceType, AttributeVar, TypeVar, SymbolType, Expression, Type, Ident, (Global object) | <<< object, Position, CaseAlt, AType, FunDef, ParsedExpr, TypeAttribute, (Bind a b) | <<< a & <<< b, ParsedConstructor, (TypeDef a) | <<< a, TypeVarInfo, BasicValue, ATypeVar, TypeRhs, FunctionPattern, (Import from_symbol) | <<< from_symbol, ImportDeclaration, ImportedIdent, CasePatterns, (Optional a) | <<< a, ConsVariable, BasicType, Annotation, Selection, SelectorDef, ConsDef, LocalDefs, FreeVar, ClassInstance, SignClassification, TypeCodeExpression, CoercionPosition, AttrInequality, LetBind, Declaration, STE_Kind, BoundVar instance <<< FunctionBody instance == TypeAttribute instance == Annotation /* ErrorToString :: Error -> String */ EmptySymbolTableEntry :== EmptySymbolTableEntryCAF.boxed_symbol_table_entry ::BoxedSymbolTableEntry = {boxed_symbol_table_entry::!SymbolTableEntry} EmptySymbolTableEntryCAF :: BoxedSymbolTableEntry cNotAGroupNumber :== -1 EmptyTypeDefInfo :== { tdi_kinds = [], tdi_properties = cAllBitsClear, tdi_group = [], tdi_group_vars = [], tdi_cons_vars = [], tdi_classification = EmptyTypeClassification, tdi_group_nr = cNotAGroupNumber, tdi_tmp_index = NoIndex } MakeTypeVar name :== { tv_name = name, tv_info_ptr = nilPtr } MakeVar name :== { var_name = name, var_info_ptr = nilPtr, var_expr_ptr = nilPtr } MakeAttributedType type :== { at_attribute = TA_None, at_annotation = AN_None, at_type = type } MakeAttributedTypeVar type_var :== { atv_attribute = TA_None, atv_annotation = AN_None, atv_variable = type_var } EmptyFunInfo :== { fi_calls = [], fi_group_index = NoIndex, fi_def_level = NotALevel, fi_free_vars = [], fi_local_vars = [], fi_dynamics = [], fi_properties=0 } BottomSignClass :== { sc_pos_vect = 0, sc_neg_vect = 0 } PostiveSignClass :== { sc_pos_vect = bitnot 0, sc_neg_vect = 0 } NoPropClass :== 0 PropClass :== bitnot 0 newTypeSymbIdentCAF :: TypeSymbIdent; MakeNewTypeSymbIdent name arity :== {newTypeSymbIdentCAF & type_name=name, type_arity=arity } MakeTypeSymbIdent type_index name arity :== { newTypeSymbIdentCAF & type_name = name, type_arity = arity, type_index = type_index } MakeSymbIdent name arity :== { symb_name = name, symb_kind = SK_Unknown, symb_arity = arity } MakeConstant name :== MakeSymbIdent name 0 ParsedSelectorToSelectorDef sd_type_index ps :== { sd_symb = ps.ps_selector_name, sd_field_nr = NoIndex, sd_pos = ps.ps_field_pos, sd_type_index = sd_type_index, sd_exi_vars = [], sd_type_ptr = nilPtr, sd_field = ps.ps_field_name, sd_type = { st_vars = [], st_args = [], st_result = ps.ps_field_type, st_arity = 0, st_context = [], st_attr_env = [], st_attr_vars = [] }} ParsedConstructorToConsDef pc :== { cons_symb = pc.pc_cons_name, cons_pos = pc.pc_cons_pos, cons_priority = pc.pc_cons_prio, cons_index = NoIndex, cons_type_index = NoIndex, cons_type = { st_vars = [], st_args = pc.pc_arg_types, st_result = MakeAttributedType TE, st_arity = pc.pc_cons_arity, st_context = [], st_attr_env = [], st_attr_vars = []}, cons_exi_vars = pc.pc_exi_vars, cons_type_ptr = nilPtr, cons_arg_vars = [] } ParsedInstanceToClassInstance pi members :== { ins_class = {glob_object = MakeDefinedSymbol pi.pi_class NoIndex (length pi.pi_types), glob_module = NoIndex}, ins_ident = pi.pi_ident, ins_type = { it_vars = [], it_types = pi.pi_types, it_attr_vars = [], it_context = pi.pi_context }, ins_members = members, ins_specials = pi.pi_specials, ins_pos = pi.pi_pos, /*AA*/ ins_is_generic = False, ins_generate = pi.pi_generate, ins_generic = {glob_module = NoIndex, glob_object = NoIndex}} MakeTypeDef name lhs rhs attr contexts pos :== { td_name = name, td_index = -1, td_arity = length lhs, td_args = lhs, td_attrs = [], td_attribute = attr, td_context = contexts, td_pos = pos, td_rhs = rhs } MakeDefinedSymbol ident index arity :== { ds_ident = ident, ds_arity = arity, ds_index = index } MakeNewFunctionType name arity prio type pos specials var_ptr :== { ft_symb = name, ft_arity = arity, ft_priority = prio, ft_type = type, ft_pos = pos, ft_specials = specials, ft_type_ptr = var_ptr } backslash :== '\\'