Commit 49e0b226 authored by Sjaak Smetsers's avatar Sjaak Smetsers
Browse files

Sjaak: Improved dynamics, not yet finished.

parent f5fe2b44
......@@ -390,12 +390,20 @@ where
convertDynamics cinp bound_vars default_expr (MatchExpr opt_symb symb expression) ci
# (expression,ci) = convertDynamics cinp bound_vars default_expr expression ci
= (MatchExpr opt_symb symb expression, ci)
/* Sjaak ... */
convertDynamics cinp bound_vars default_expr (DynamicExpr {dyn_expr, dyn_info_ptr, dyn_type_code}) ci=:{ci_symb_ident}
# (dyn_expr, ci) = convertDynamics cinp bound_vars default_expr dyn_expr ci
(_,dyn_type_code, _, _, ci) = convertTypecode2 cinp dyn_type_code False [] [] ci
= (App { app_symb = ci_symb_ident,
app_args = [dyn_expr, dyn_type_code],
app_info_ptr = nilPtr }, ci)
/* ... Sjaak */
/* WAS ...
convertDynamics cinp bound_vars default_expr (DynamicExpr {dyn_expr, dyn_info_ptr, dyn_uni_vars, dyn_type_code}) ci=:{ci_symb_ident}
// # (twoTuple_symb, ci) = getSymbol (GetTupleConsIndex 2) SK_Constructor 2 ci
# (let_binds, ci) = createVariables dyn_uni_vars [] ci
(dyn_expr, ci) = convertDynamics cinp bound_vars default_expr dyn_expr ci
(_,dyn_type_code,_,_,ci) = convertTypecode2 cinp dyn_type_code False [] [] ci
// (_,dyn_type_code, ci) = convertTypecode cinp dyn_type_code ci
= case let_binds of
[] -> (App { app_symb = ci_symb_ident, //USE_TUPLES twoTuple_symb ci_symb_ident, //twoTuple_symb,
app_args = [dyn_expr, dyn_type_code],
......@@ -406,9 +414,9 @@ where
let_expr = App { app_symb = ci_symb_ident, //USE_TUPLES twoTuple_symb ci_symb_ident,
app_args = [dyn_expr, dyn_type_code],
app_info_ptr = nilPtr },
// MW0 let_info_ptr = let_info_ptr,}, ci)
let_info_ptr = let_info_ptr,
let_expr_position = NoPos}, ci)
*/
convertDynamics cinp bound_vars default_expr (TypeCodeExpression type_code) ci
= abort "convertDynamics cinp bound_vars default_expr (TypeCodeExpression" //convertTypecode cinp type_code ci
convertDynamics cinp bound_vars default_expr EE ci
......@@ -426,6 +434,19 @@ where
*/
/* Sjaak ... */
convertTypecode2 cinp (TCE_UniType uni_vars type_code) replace_tc_args binds placeholders_and_tc_args ci
# (let_binds, ci) = createVariables uni_vars [] ci
(let_info_ptr, ci) = let_ptr ci
(e, type_code_expr, binds, placeholders_and_tc_args, ci) = convertTypecode2 cinp type_code False [] [] ci
= (e, Let { let_strict_binds = [],
let_lazy_binds = let_binds,
let_expr = type_code_expr,
let_info_ptr = let_info_ptr,
let_expr_position = NoPos}, binds, placeholders_and_tc_args, ci)
/* ... Sjaak */
// ci_placeholders_and_tc_args
convertTypecode2 cinp=:{cinp_st_args} t=:(TCE_Var var_info_ptr) replace_tc_args binds placeholders_and_tc_args ci
#! cinp_st_args
......
......@@ -43,9 +43,7 @@ tryToSolveOverloading :: ![(Optional [TypeContext], [ExprInfoPtr], IdentPos, Ind
{ tci_next_index :: !Index
, tci_instances :: ![GlobalTCInstance]
, tci_type_var_heap :: !.TypeVarHeap
// MV ...
, tci_dcl_modules :: !{# DclModule}
// ... MV
}
removeOverloadedFunctions :: ![Index] ![LocalTypePatternVariable] !Int !*{#FunDef} !*{! FunctionType} !*ExpressionHeap
......
This diff is collapsed.
......@@ -506,22 +506,17 @@ where
where
initial_occurrence {fv_name,fv_info_ptr} (subst, type_def_infos, var_heap, expr_heap)
# (var_info, var_heap) = readPtr fv_info_ptr var_heap
= case var_info of
VI_Type {at_type,at_attribute} _
-> case at_type of
TempV tv_number
#! is_oberving = has_observing_type type_def_infos subst.[tv_number]
-> (subst, type_def_infos, var_heap <:= (fv_info_ptr,
VI_Occurrence { occ_ref_count = RC_Unused, occ_previous = [],
occ_observing = is_oberving, occ_bind = OB_Empty }), expr_heap)
// ---> ("initial_occurrence",fv_name, fv_info_ptr, is_oberving)
_
-> (subst, type_def_infos, var_heap <:= (fv_info_ptr,
VI_Occurrence { occ_ref_count = RC_Unused, occ_previous = [],
occ_observing = False, occ_bind = OB_Empty }), expr_heap)
_
-> abort ("initial_occurrence (refmark.icl)" ---> ((fv_name,fv_info_ptr) ))//<<- var_info))
#! occ_observing = has_observing_base_type var_info type_def_infos subst
= (subst, type_def_infos,
var_heap <:= (fv_info_ptr, VI_Occurrence { occ_ref_count = RC_Unused, occ_previous = [],
occ_observing = occ_observing, occ_bind = OB_Empty }), expr_heap)
has_observing_base_type (VI_Type {at_type} _) type_def_infos subst
= has_observing_type at_type type_def_infos subst
has_observing_base_type (VI_FAType _ {at_type}) type_def_infos subst
= has_observing_type at_type type_def_infos subst
has_observing_base_type _ type_def_infos subst
= abort "has_observing_base_type (refmark.icl)"
make_shared_vars_non_unique vars coercion_env var_heap expr_heap error
= foldl make_shared_var_non_unique (coercion_env, var_heap, expr_heap, error) vars
......@@ -555,16 +550,22 @@ where
make_selection_non_unique fv {su_multiply} cee
= make_shared_occurrences_non_unique fv su_multiply cee
/*
has_observing_type type_def_infos TE
= True
has_observing_type type_def_infos (TB basic_type)
= True
has_observing_type type_def_infos (TempV var_number)
*/
has_observing_type (TB basic_type) type_def_infos subst
= True
has_observing_type type_def_infos (TA {type_index = {glob_object,glob_module}} type_args)
has_observing_type (TempV var_number) type_def_infos subst
= case subst.[var_number] of
TE
-> True
subst_type
-> has_observing_type subst_type type_def_infos subst
has_observing_type (TA {type_index = {glob_object,glob_module}} type_args) type_def_infos subst
# {tdi_properties} = type_def_infos.[glob_module].[glob_object]
= foldSt (\ {at_type} ok -> ok && has_observing_type type_def_infos at_type) type_args (tdi_properties bitand cIsHyperStrict <> 0)
has_observing_type type_def_infos type
= foldSt (\ {at_type} ok -> ok && has_observing_type at_type type_def_infos subst) type_args (tdi_properties bitand cIsHyperStrict <> 0)
has_observing_type type type_def_infos subst
= False
......
......@@ -860,6 +860,7 @@ cNonRecursiveAppl :== False
:: TypeVarInfo = TVI_Empty
| TVI_Type !Type
| TVI_TypeVar !TypeVarInfoPtr // Sjaak: to collect universally quantified type variables
| TVI_Forward !TempVarId | TVI_TypeKind !KindInfoPtr
| TVI_SignClass !Index !SignClassification !TypeVarInfo | TVI_PropClass !Index !PropClassification !TypeVarInfo
| TVI_Attribute TypeAttribute
......@@ -876,7 +877,10 @@ cNonRecursiveAppl :== False
:: TypeVarInfoPtr :== Ptr TypeVarInfo
:: TypeVarHeap :== Heap TypeVarInfo
:: AttrVarInfo = AVI_Empty | AVI_Attr !TypeAttribute | AVI_Forward !TempAttrId
:: AttrVarInfo = AVI_Empty
| AVI_Attr !TypeAttribute
| AVI_AttrVar !AttrVarInfoPtr // Sjaak: to collect universally quantified attribute variables
| AVI_Forward !TempAttrId
| AVI_CorrespondenceNumber !Int /* auxiliary used in module comparedefimp */
| AVI_Used
| AVI_Count !Int /* auxiliary used in module typesupport */
......@@ -1154,7 +1158,7 @@ cIsNotStrict :== False
{ dyn_expr :: !Expression
, dyn_opt_type :: !Optional DynamicType
, dyn_info_ptr :: !ExprInfoPtr
, dyn_uni_vars :: ![VarInfoPtr] /* filled after type checking */
// , dyn_uni_vars :: ![VarInfoPtr] /* filled after type checking */
, dyn_type_code :: !TypeCodeExpression /* filled after type checking */
}
......@@ -1167,19 +1171,15 @@ cIsNotStrict :== False
| 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
:: TypeCodeExpression = TCE_Empty
| TCE_Var !VarInfoPtr
| TCE_TypeTerm !VarInfoPtr
| TCE_Constructor !Index ![TypeCodeExpression]
| TCE_Selector ![Selection] !VarInfoPtr
| TCE_UniType ![VarInfoPtr] !TypeCodeExpression
:: 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)
......
......@@ -831,12 +831,15 @@ cNotVarNumber :== -1
| KI_NormVar !Int
:: TypeVarInfo = TVI_Empty | TVI_Type !Type | TVI_Forward !TempVarId | TVI_TypeKind !KindInfoPtr
:: TypeVarInfo = TVI_Empty
| TVI_Type !Type
| TVI_TypeVar !TypeVarInfoPtr // Sjaak: to collect universally quantified type variables
| 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 adminster that this variable is encountered (in checkOpenTypes) */
| 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_Kinds ![TypeKind] // AA: used to collect kinds during checking
......@@ -847,10 +850,14 @@ cNotVarNumber :== -1
:: TypeVarInfoPtr :== Ptr TypeVarInfo
:: TypeVarHeap :== Heap TypeVarInfo
:: AttrVarInfo = AVI_Empty | AVI_Attr !TypeAttribute | AVI_Forward !TempAttrId
:: AttrVarInfo = AVI_Empty
| AVI_Attr !TypeAttribute
| AVI_AttrVar !AttrVarInfoPtr // Sjaak: to collect universally quantified attribute variables
| 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
......@@ -1101,7 +1108,7 @@ cIsNotStrict :== False
{ dyn_expr :: !Expression
, dyn_opt_type :: !Optional DynamicType
, dyn_info_ptr :: !ExprInfoPtr
, dyn_uni_vars :: ![VarInfoPtr] /* filled after type checking */
// , dyn_uni_vars :: ![VarInfoPtr] /* filled after type checking */
, dyn_type_code :: !TypeCodeExpression /* filled after type checking */
}
......@@ -1114,7 +1121,12 @@ cIsNotStrict :== False
| ArraySelection !(Global DefinedSymbol) !ExprInfoPtr !Expression
| DictionarySelection !BoundVar ![Selection] !ExprInfoPtr !Expression
:: TypeCodeExpression = TCE_Empty | TCE_Var !VarInfoPtr /* MV */ | TCE_TypeTerm !VarInfoPtr | TCE_Constructor !Index ![TypeCodeExpression] | TCE_Selector ![Selection] !VarInfoPtr
:: TypeCodeExpression = TCE_Empty
| TCE_Var !VarInfoPtr
| TCE_TypeTerm !VarInfoPtr
| TCE_Constructor !Index ![TypeCodeExpression]
| TCE_Selector ![Selection] !VarInfoPtr
| TCE_UniType ![VarInfoPtr] !TypeCodeExpression
:: GlobalTCType = GTT_Basic !BasicType | GTT_Constructor !TypeSymbIdent !String | GTT_Function
......@@ -1254,11 +1266,11 @@ where
instance <<< TypeVar
where
(<<<) file varid = file <<< varid.tv_name
// (<<<) file varid = file <<< varid.tv_name <<< "<" <<< ptrToInt (varid.tv_info_ptr) <<< ">"
// (<<<) file varid = file <<< varid.tv_name <<< "<" <<< varid.tv_info_ptr <<< ">"
instance <<< AttributeVar
where
// (<<<) file {av_name,av_info_ptr} = file <<< av_name <<< "[" <<< ptrToInt av_info_ptr <<< "]"
// (<<<) file {av_name,av_info_ptr} = file <<< av_name <<< "[" <<< av_info_ptr <<< "]"
(<<<) file {av_name,av_info_ptr} = file <<< av_name
instance toString AttributeVar
......@@ -1336,9 +1348,9 @@ where
= file <<< type <<< " @" <<< types
(<<<) file (TB tb)
= file <<< tb
/* (<<<) file (TFA vars types)
(<<<) file (TFA vars types)
= file <<< "A." <<< vars <<< ':' <<< types
*/ (<<<) file (TQV varid)
(<<<) file (TQV varid)
= file <<< "E." <<< varid
(<<<) file (TempQV tv_number)
= file <<< "E." <<< tv_number <<< ' '
......@@ -1388,7 +1400,7 @@ where
instance <<< TypeContext
where
(<<<) file co = file <<< co.tc_class <<< " " <<< co.tc_types <<< " <" <<< ptrToInt co.tc_var <<< '>'
(<<<) file co = file <<< co.tc_class <<< " " <<< co.tc_types <<< " <" <<< co.tc_var <<< '>'
instance <<< SymbIdent
where
......@@ -1414,7 +1426,7 @@ where
instance <<< BoundVar
where
(<<<) file {var_name,var_info_ptr,var_expr_ptr}
= file <<< var_name <<< "<I" <<< ptrToInt var_info_ptr <<< ", E" <<< ptrToInt var_expr_ptr <<< '>'
= file <<< var_name <<< "<I" <<< var_info_ptr <<< ", E" <<< var_expr_ptr <<< '>'
instance <<< (Bind a b) | <<< a & <<< b
where
......@@ -1507,7 +1519,8 @@ where
(<<<) file (MatchExpr _ cons expr) = file <<< cons <<< " =: " <<< expr
(<<<) file EE = file <<< "** E **"
(<<<) file (NoBind _) = file <<< "** NB **"
(<<<) file (DynamicExpr {dyn_expr,dyn_uni_vars,dyn_type_code}) = writeVarPtrs (file <<< "dynamic " <<< dyn_expr <<< " :: dyn_uni_vars") dyn_uni_vars <<< "dyn_type_code=" <<< dyn_type_code
(<<<) file (DynamicExpr {dyn_expr,dyn_type_code}) = file <<< "dynamic " <<< dyn_expr <<< " :: " <<< dyn_type_code
// (<<<) file (DynamicExpr {dyn_expr,dyn_uni_vars,dyn_type_code}) = writeVarPtrs (file <<< "dynamic " <<< dyn_expr <<< " :: dyn_uni_vars") dyn_uni_vars <<< "dyn_type_code=" <<< dyn_type_code
// (<<<) file (TypeCase type_case) = file <<< type_case
(<<<) file (TypeCodeExpression type_code) = file <<< type_code
(<<<) file (Constant symb _ _ _) = file <<< "** Constant **" <<< symb
......@@ -1516,7 +1529,7 @@ where
(<<<) file (AnyCodeExpr input output code_sequence) = file <<< "code\n" <<< input <<< "\n" <<< output <<< "\n" <<< code_sequence
(<<<) file (FreeVar {fv_name}) = file <<< fv_name
(<<<) file (ClassVariable info_ptr) = file <<< "ClassVariable " <<< ptrToInt info_ptr
(<<<) file (ClassVariable info_ptr) = file <<< "ClassVariable " <<< info_ptr
(<<<) file expr = abort ("<<< (Expression) [line 1290]" )//<<- expr)
......@@ -1542,9 +1555,9 @@ writeVarPtrs file vars
= write_var_ptrs (file <<< '<') vars <<< '>'
where
write_var_ptrs file [var]
= file <<< ptrToInt var
= file <<< var
write_var_ptrs file [var : vars]
= write_var_ptrs (file <<< ptrToInt var <<< '.') vars
= write_var_ptrs (file <<< var <<< '.') vars
instance <<< TypeCodeExpression
......@@ -1552,15 +1565,20 @@ where
(<<<) file TCE_Empty
= file
(<<<) file (TCE_Var info_ptr)
= file <<< "TCE_Var " <<< ptrToInt info_ptr
// MV ..
= file <<< "TCE_Var " <<< info_ptr
(<<<) file (TCE_TypeTerm info_ptr)
= file <<< "TCE_TypeTerm " <<< ptrToInt info_ptr
// .. MV
= file <<< "TCE_TypeTerm " <<< info_ptr
(<<<) file (TCE_Constructor index exprs)
= file <<< "TCE_Constructor " <<< index <<< ' ' <<< exprs
(<<<) file (TCE_Selector selectors info_ptr)
= file <<< "TCE_Selector " <<< selectors <<< "VAR " <<< ptrToInt info_ptr
= file <<< "TCE_Selector " <<< selectors <<< "VAR " <<< info_ptr
(<<<) file (TCE_UniType vars type_code)
= file <<< "TCE_UniType " <<< vars <<< " " <<< type_code
instance <<< (Ptr a)
where
(<<<) file ptr
= file <<< ptrToInt ptr
instance <<< Selection
where
......@@ -1688,7 +1706,7 @@ where
instance <<< FreeVar
where
(<<<) file {fv_name,fv_info_ptr,fv_count} = file <<< fv_name <<< '.' <<< fv_count <<< '<' <<< ptrToInt fv_info_ptr <<< '>'
(<<<) file {fv_name,fv_info_ptr,fv_count} = file <<< fv_name <<< '.' <<< fv_count <<< '<' <<< fv_info_ptr <<< '>'
instance <<< DynamicType
where
......@@ -1951,7 +1969,7 @@ where
instance <<< Declaration
where
(<<<) file (Declaration { decl_ident, decl_kind })
= file <<< decl_ident <<< '<' <<< ptrToInt decl_ident.id_info <<< '>' <<< '(' <<< decl_kind <<< ')'
= file <<< decl_ident <<< '<' <<< decl_ident.id_info <<< '>' <<< '(' <<< decl_kind <<< ')'
instance <<< STE_Kind
where
......
......@@ -5,8 +5,7 @@ import syntax, check
typeProgram ::!{! Group} !Int !*{# FunDef} !IndexRange !(Optional Bool) !CommonDefs ![Declaration] !{# DclModule} !NumberSet !*TypeDefInfos !*Heaps !*PredefinedSymbols !*File !*File !{# DclModule}
-> (!Bool, !*{# FunDef}, !IndexRange, {! GlobalTCType}, !{# CommonDefs}, !{# {# FunType} }, !*TypeDefInfos, !*Heaps, !*PredefinedSymbols, !*File, !*File)
//typeProgram ::!{! Group} !Int !*{# FunDef} !IndexRange !(Optional Bool) !CommonDefs ![Declaration] !{# DclModule} !NumberSet !*Heaps !*PredefinedSymbols !*File !*File !{# DclModule}
// -> (!Bool, !*{# FunDef}, !IndexRange, {! GlobalTCType}, !{# CommonDefs}, !{# {# FunType} }, !.TypeDefInfos, !*Heaps, !*PredefinedSymbols, !*File, !*File)
addPropagationAttributesToAType :: {#CommonDefs} !AType !*PropState -> *(!AType,Int,!*PropState);
......
......@@ -96,6 +96,11 @@ where
| ok
-> (True, simplified_type, subst)
-> (False, tcv, subst)
arraySubst tfa_type=:(TFA vars type) subst
# (changed, type, subst) = arraySubst type subst
| changed
= (changed, TFA vars type, subst)
= (False, tfa_type, subst)
arraySubst type subst
= (False, type, subst)
......@@ -470,7 +475,7 @@ where
# (fresh_attribute, th_attrs) = freshCopyOfTypeAttribute at_attribute th_attrs
(fresh_type, type_heaps) = freshCopy at_type { type_heaps & th_attrs = th_attrs }
= ({ type & at_type = fresh_type, at_attribute = fresh_attribute }, type_heaps)
instance freshCopy Type
where
freshCopy (TV tv) type_heaps
......@@ -485,6 +490,7 @@ where
freshCopy (TFA vars type) type_heaps
# type_heaps = foldSt bind_var_and_attr vars type_heaps
(type, type_heaps) = freshCopy type type_heaps
# type_heaps = clearBindings vars type_heaps
= (TFA vars type, type_heaps)
where
bind_var_and_attr {atv_attribute, atv_variable = tv=:{tv_info_ptr}} type_heaps=:{th_vars,th_attrs}
......@@ -617,7 +623,6 @@ freshSymbolType fresh_context_vars st=:{st_vars,st_args,st_result,st_context,st_
= vars
= [var_id : add_variable new_var_id var_ids]
// JVG: added type:
freshInequality :: AttrInequality *(Heap AttrVarInfo) -> (!AttrCoercion,!.Heap AttrVarInfo);
freshInequality {ai_demanded,ai_offered} attr_heap
# (av_dem_info, attr_heap) = readPtr ai_demanded.av_info_ptr attr_heap
......@@ -958,8 +963,8 @@ where
where
bind_var_and_attr {atv_attribute, atv_variable = {tv_info_ptr}} ts=:{ts_var_store, ts_type_heaps}
= { ts & ts_var_store = inc ts_var_store, ts_type_heaps =
{ ts_type_heaps & th_vars = ts_type_heaps.th_vars <:= (tv_info_ptr, TVI_Type (TempQV ts_var_store)),
th_attrs = bind_attr atv_attribute ts_type_heaps.th_attrs }}
{ ts_type_heaps & th_vars = ts_type_heaps.th_vars <:= (tv_info_ptr, TVI_Type (TempV ts_var_store)),
th_attrs = bind_attr atv_attribute ts_type_heaps.th_attrs }}
where
bind_attr (TA_Var {av_info_ptr}) attr_heap
= attr_heap <:= (av_info_ptr, AVI_Attr TA_TempExVar)
......@@ -1069,7 +1074,7 @@ where
requirements_of_dynamic_pattern dyn_type dyn_context dyn_expr_ptr type_code_symbol
ti goal_type {dp_var={fv_info_ptr},dp_rhs} (reqs, ts=:{ts_expr_heap, ts_var_heap})
# ts_var_heap = ts_var_heap <:= (fv_info_ptr, VI_Type dyn_type No)
# ts_var_heap = addToBase fv_info_ptr dyn_type No ts_var_heap
(dp_rhs_type, opt_expr_ptr, (reqs, ts)) = requirements ti dp_rhs (reqs, { ts & ts_expr_heap = ts_expr_heap, ts_var_heap = ts_var_heap })
ts_expr_heap = storeAttribute opt_expr_ptr dp_rhs_type.at_attribute ts.ts_expr_heap
type_coercion = { tc_demanded = goal_type, tc_offered = dp_rhs_type, tc_position = CP_Expression dp_rhs, tc_coercible = True }
......@@ -1395,13 +1400,13 @@ makeBase _ _ [] [] ts_var_heap
= ts_var_heap
makeBase fun_or_cons_ident arg_nr [{fv_name, fv_info_ptr} : vars] [type : types] ts_var_heap
| is_rare_name fv_name
= makeBase fun_or_cons_ident (arg_nr+1) vars types (bind_type fv_info_ptr type (Yes (CP_FunArg fun_or_cons_ident arg_nr)) ts_var_heap)
= makeBase fun_or_cons_ident (arg_nr+1) vars types (bind_type fv_info_ptr type No ts_var_heap)
where
bind_type info_ptr atype=:{at_type = TFA atvs type} _ ts_var_heap
= ts_var_heap <:= (info_ptr, VI_FAType atvs { atype & at_type = type})
bind_type info_ptr type optional_position ts_var_heap
= ts_var_heap <:= (info_ptr, VI_Type type optional_position)
= makeBase fun_or_cons_ident (arg_nr+1) vars types (addToBase fv_info_ptr type (Yes (CP_FunArg fun_or_cons_ident arg_nr)) ts_var_heap)
= makeBase fun_or_cons_ident (arg_nr+1) vars types (addToBase fv_info_ptr type No ts_var_heap)
addToBase info_ptr atype=:{at_type = TFA atvs type} _ ts_var_heap
= ts_var_heap <:= (info_ptr, VI_FAType atvs { atype & at_type = type})
addToBase info_ptr type optional_position ts_var_heap
= ts_var_heap <:= (info_ptr, VI_Type type optional_position)
attributedBasicType (BT_String string_type) ts=:{ts_attr_store}
= ({ at_annotation = AN_None, at_attribute = TA_TempVar ts_attr_store, at_type = string_type}, {ts & ts_attr_store = inc ts_attr_store})
......@@ -1515,10 +1520,11 @@ where
(expr_ptr, expr_heap) = newPtr EI_Empty expr_heap //---> ("^EI_Dynamic No=" +++ toString var_store)
-> (inc var_store, type_heaps, var_heap,
expr_heap <:= (dyn_ptr, EI_TempDynamicType No tdt_type [context] expr_ptr tc_member_symb), predef_symbols)
EI_DynamicTypeWithVars loc_type_vars dt=:{dt_type,dt_global_vars} loc_dynamics
EI_DynamicTypeWithVars loc_type_vars dt=:{dt_uni_vars,dt_type,dt_global_vars} loc_dynamics
# (fresh_vars, (th_vars, var_store)) = fresh_existential_variables loc_type_vars (type_heaps.th_vars, var_store)
// ---> ("fresh_dynamic (EI_DynamicTypeWithVars)", dt_uni_vars)
(th_vars, var_store) = fresh_type_variables dt_global_vars (th_vars, var_store)
(tdt_type, type_heaps) = freshCopy dt_type { type_heaps & th_vars = th_vars }
(tdt_type, type_heaps) = freshCopy (add_universal_vars_to_type dt_uni_vars dt_type) { type_heaps & th_vars = th_vars }
(contexts, expr_ptr, type_code_symbol, (var_heap, expr_heap, type_var_heap, predef_symbols))
= determine_context_and_expr_ptr dt_global_vars (var_heap, expr_heap, type_heaps.th_vars, predef_symbols)
-> fresh_local_dynamics loc_dynamics (var_store, { type_heaps & th_vars = type_var_heap }, var_heap,
......@@ -1577,6 +1583,10 @@ where
(new_var_ptr, var_heap) = newPtr VI_Empty var_heap
= ({tc_class = tc_class_symb, tc_types = [fresh_var], tc_var = new_var_ptr}, (var_heap, type_var_heap))
add_universal_vars_to_type [] at
= at
add_universal_vars_to_type uni_vars at=:{at_type}
= { at & at_type = TFA uni_vars at_type }
specification_error type type1 err
# err = errorHeading "Type error" err
......@@ -1760,10 +1770,7 @@ where
update_instances_of_class common_defs mod_index ins_index (dummy, error, class_instances, type_var_heap, td_infos)
#!{ins_class={glob_object={ds_ident={id_name}, ds_index},glob_module},ins_type={it_types},ins_pos} = common_defs.[mod_index].com_instance_defs.[ins_index]
id_name = id_name ---> ("update_instances_of_class" +++ id_name +++ " " +++ (toString glob_module) +++
" " +++ toString (size class_instances))
(mod_instances, class_instances) = replace class_instances glob_module dummy
id_name = id_name ---> "done"
(instances, mod_instances) = replace mod_instances ds_index IT_Empty
(error, instances) = insert it_types ins_index mod_index common_defs error instances
(_, mod_instances) = replace mod_instances ds_index instances
......
......@@ -75,6 +75,8 @@ instance substitute AType, Type, TypeContext, AttrInequality, CaseType, [a] | su
instance <<< TempSymbolType
clearBindings :: ![ATypeVar] !*TypeHeaps -> !*TypeHeaps
removeInequality :: !Int !Int !*Coercions -> .Coercions
flattenCoercionTree :: !u:CoercionTree -> (![Int], !u:CoercionTree)
// retrieve all numbers from a coercion tree
......
......@@ -62,6 +62,7 @@ where
(at_type, cus) = clean_up cui at_type cus
= ({atype & at_attribute = at_attribute, at_type = at_type, at_annotation = AN_None}, cus)
attrIsUndefined TA_None = True
attrIsUndefined _ = False
......@@ -105,6 +106,9 @@ where
= (attr, { cus & cus_appears_in_lifted_part = cus_appears_in_lifted_part,
cus_error = cus_error })
= (TA_Multi, cus)
clean_up cui (TA_Var av=:{av_info_ptr}) cus=:{cus_heaps}
# (AVI_AttrVar new_info_ptr, th_attrs) = readPtr av_info_ptr cus_heaps.th_attrs
= (TA_Var { av & av_info_ptr = new_info_ptr }, { cus & cus_heaps = { cus_heaps & th_attrs = th_attrs }})
clean_up cui TA_TempExVar cus
= PA_BUG (TA_Multi, cus) (abort "clean_up cui (TA_TempExVar)")
......@@ -137,6 +141,26 @@ where
| cui.cui_top_level
= cleanUpVariable True type qv_number {cus & cus_error = existentialError cus_error}
= cleanUpVariable False type qv_number cus
clean_up cui (TV tv=:{tv_info_ptr}) cus=:{cus_heaps}
# (TVI_TypeVar new_info_ptr, th_vars) = readPtr tv_info_ptr cus_heaps.th_vars
= (TV { tv & tv_info_ptr = new_info_ptr }, { cus & cus_heaps = { cus_heaps & th_vars = th_vars }})
clean_up cui (TFA vars type) cus=:{cus_heaps}
# (new_vars, cus_heaps) = mapSt refresh_var_and_attr vars cus_heaps
(type, cus) = clean_up cui type { cus & cus_heaps = cus_heaps }
cus_heaps = clearBindings vars cus.cus_heaps
= (TFA vars type, { cus & cus_heaps = cus_heaps })
where
refresh_var_and_attr atv=:{atv_attribute, atv_variable = tv=:{tv_info_ptr}} type_heaps=:{th_vars,th_attrs}
# (new_info_ptr, th_vars) = newPtr TVI_Empty th_vars
(atv_attribute, th_attrs) = refresh_attr atv_attribute th_attrs
= ( { atv & atv_attribute = atv_attribute, atv_variable = { tv & tv_info_ptr = new_info_ptr }},
{ type_heaps & th_vars = th_vars <:= (tv_info_ptr, TVI_TypeVar new_info_ptr), th_attrs = th_attrs })
where
refresh_attr (TA_Var av=:{av_info_ptr}) attr_heap
# (new_info_ptr, attr_heap) = newPtr AVI_Empty attr_heap
= (TA_Var {av & av_info_ptr = new_info_ptr}, attr_heap <:= (av_info_ptr, AVI_AttrVar new_info_ptr))
refresh_attr attr attr_heap
= (attr, attr_heap)
clean_up cui TE cus
= abort "unknown pattern in function clean_up"
......@@ -156,6 +180,17 @@ cleanUpVariable top_level (TLifted var) tv_number cus=:{cus_error}
cleanUpVariable _ type tv_number cus
= (type, cus)
clearBindings :: ![ATypeVar] !*TypeHeaps -> !*TypeHeaps
clearBindings atvs type_heaps
= foldSt clear_binding_of_var_and_attr atvs type_heaps
where
clear_binding_of_var_and_attr {atv_attribute, atv_variable = tv=:{tv_info_ptr}} type_heaps=:{th_vars,th_attrs}
= { type_heaps & th_vars = th_vars <:= (tv_info_ptr, TVI_Empty), th_attrs = clear_attr atv_attribute th_attrs }
clear_attr var=:(TA_Var {av_info_ptr}) attr_heap
= attr_heap <:= (av_info_ptr, AVI_Empty)
clear_attr attr attr_heap
= attr_heap
:: CleanUpResult :== BITVECT
......
......@@ -347,6 +347,8 @@ where
| changed
= (True, [t0:ts], subst, ls)
= (False, ts0, subst, ls)
lift modules cons_vars (TFA vars type) subst ls
= abort "lift (TFA) (unitype.icl)"
lift modules cons_vars type subst ls
= (False, type, subst, ls)
......
Supports Markdown
0% or .
<