diff options
| -rw-r--r-- | frontend/convertDynamics.icl | 12 | ||||
| -rw-r--r-- | frontend/syntax.dcl | 7 | ||||
| -rw-r--r-- | frontend/syntax.icl | 7 | ||||
| -rw-r--r-- | frontend/trans.dcl | 4 | ||||
| -rw-r--r-- | frontend/trans.icl | 26 |
5 files changed, 46 insertions, 10 deletions
diff --git a/frontend/convertDynamics.icl b/frontend/convertDynamics.icl index d4f4d52..3627c7a 100644 --- a/frontend/convertDynamics.icl +++ b/frontend/convertDynamics.icl @@ -56,15 +56,19 @@ where # (fun_body, ci) = convert_dynamics_in_body {cinp_st_args = [], cinp_glob_type_inst = global_type_instances, cinp_group_index = group_nr} fun_body fun_type ci = ({fun_defs & [fun] = { fun_def & fun_body = fun_body, fun_info = { fun_info & fi_local_vars = ci.ci_new_variables ++ fun_info.fi_local_vars }}}, { ci & ci_new_variables = [] }) - - convert_dynamics_in_body global_type_instances (TransformedBody {tb_args,tb_rhs}) (Yes {st_args}) ci - # vars_with_types = bindVarsToTypes tb_args st_args [] +// MV .. + convert_dynamics_in_body global_type_instances (TransformedBody {tb_args,tb_rhs}) (Yes {st_context, st_args}) ci + # vars_with_types = bindVarsToTypes2 st_context tb_args st_args [] common_defs +// .. MV (tb_rhs, ci) = convertDynamics {global_type_instances & cinp_st_args = tb_args} vars_with_types No tb_rhs ci = (TransformedBody {tb_args = tb_args,tb_rhs = tb_rhs}, ci) convert_dynamics_in_body global_type_instances other fun_type ci = abort "unexpected value in 'convert dynamics.convert_dynamics_in_body'" - +// MV .. +bindVarsToTypes2 st_context vars types typed_vars common_defs + :== bindVarsToTypes vars (addTypesOfDictionaries common_defs st_context types) typed_vars +// .. MV bindVarsToTypes vars types typed_vars = fold2St bind_var_to_type vars types typed_vars where diff --git a/frontend/syntax.dcl b/frontend/syntax.dcl index 9605315..32927ce 100644 --- a/frontend/syntax.dcl +++ b/frontend/syntax.dcl @@ -472,7 +472,9 @@ cIsALocalVar :== False VI_Dictionary !SymbIdent ![Expression] !Type | /* used during fusion */ VI_Extended !ExtendedVarInfo !VarInfo | VI_Defined /* for marking type code variables during overloading */ | VI_LocallyDefined | - VI_TheoremProverVariable !Int !Int /* MdM - first int is kind (0:parameter;1:case;2:let), second its index */ +// MdM + VI_CPSLocalExprVar !Int /* MdM - the index of the variable as generated by the theorem prover */ +// ... MdM :: ExtendedVarInfo = EVI_VarType !AType @@ -796,6 +798,9 @@ cNonRecursiveAppl :== False | TVI_Used /* to administer that this variable is encountered (in checkOpenTypes) */ // | TVI_Clean !Int /* to keep the unique number that has been assigned to this variable during 'clean_up' */ | TVI_TypeCode !TypeCodeExpression +// MdM + | TVI_CPSLocalTypeVar !Int /* MdM - the index of the variable as generated by the theorem prover */ +// ... MdM :: TypeVarInfoPtr :== Ptr TypeVarInfo :: TypeVarHeap :== Heap TypeVarInfo diff --git a/frontend/syntax.icl b/frontend/syntax.icl index 84729c9..cc3e3b5 100644 --- a/frontend/syntax.icl +++ b/frontend/syntax.icl @@ -447,7 +447,9 @@ cIsALocalVar :== False VI_Dictionary !SymbIdent ![Expression] !Type | /* used during fusion */ VI_Extended !ExtendedVarInfo !VarInfo | VI_Defined /* for marking type code variables during overloading */ | VI_LocallyDefined | - VI_TheoremProverVariable !Int !Int /* MdM - first int is kind (0:parameter;1:case;2:let), second its index */ +// MdM + VI_CPSLocalExprVar !Int /* MdM - the index of the variable as generated by the theorem prover */ +// ... MdM :: ExtendedVarInfo = EVI_VarType !AType @@ -756,6 +758,9 @@ cNotVarNumber :== -1 | TVI_AType !AType /* auxiliary used in module comparedefimp */ | TVI_Used /* to adminster that this variable is encountered (in checkOpenTypes) */ | TVI_TypeCode !TypeCodeExpression +// MdM + | TVI_CPSLocalTypeVar !Int /* MdM - the index of the variable as generated by the theorem prover */ +// ... MdM :: TypeVarInfoPtr :== Ptr TypeVarInfo :: TypeVarHeap :== Heap TypeVarInfo diff --git a/frontend/trans.dcl b/frontend/trans.dcl index b9d252d..67fe32c 100644 --- a/frontend/trans.dcl +++ b/frontend/trans.dcl @@ -23,3 +23,7 @@ partitionateFunctions :: !*{# FunDef} ![IndexRange] -> (!*{! Group}, !*{# FunDef convertSymbolType :: !{# CommonDefs} !SymbolType !*{#{# CheckedTypeDef}} !ImportedConstructors !*TypeHeaps !*VarHeap -> (!SymbolType, !*{#{# CheckedTypeDef}}, !ImportedConstructors, !*TypeHeaps, !*VarHeap) + +// MV .. +addTypesOfDictionaries :: w:(a x:CommonDefs) .[TypeContext] u:[AType] -> v:[AType] | Array .a, [u <= v, w <= x]; +// .. MV
\ No newline at end of file diff --git a/frontend/trans.icl b/frontend/trans.icl index b8456f6..c139943 100644 --- a/frontend/trans.icl +++ b/frontend/trans.icl @@ -704,8 +704,8 @@ setExtendedVarInfo var_info_ptr extension var_heap = case old_var_info of VI_Extended _ original_var_info -> writePtr var_info_ptr (VI_Extended extension original_var_info) var_heap _ -> writePtr var_info_ptr (VI_Extended extension old_var_info) var_heap -neverMatchingCase = { case_expr = EE, case_guards = NoPattern, case_default = No, case_ident = No, - case_info_ptr = nilPtr, case_default_pos = NoPos } +neverMatchingCase = { case_expr = EE, case_guards = NoPattern, case_default = No, case_ident = No, case_info_ptr = nilPtr, + case_default_pos = NoPos } instance transform DynamicExpr where transform dyn=:{dyn_expr} ro ti @@ -1416,7 +1416,10 @@ where # ({fun_type=Yes symbol_type}, fun_defs) = fun_defs![glob_object] = (symbol_type, fun_defs, fun_heap) # {ft_type} = ro.ro_imported_funs.[glob_module].[glob_object] - st_args = mapAppend (add_types_of_dictionary ro.ro_common_defs) ft_type.st_context ft_type.st_args +// MV .. + st_args = addTypesOfDictionaries ro.ro_common_defs ft_type.st_context ft_type.st_args +// was: st_args = mapAppend (add_types_of_dictionary ro.ro_common_defs) ft_type.st_context ft_type.st_args +// .. MV = ({ft_type & st_args = st_args, st_arity = length st_args, st_context = [] }, fun_defs, fun_heap) get_producer_type {symb_kind=SK_GeneratedFunction fun_ptr _} ro fun_defs fun_heap @@ -2025,6 +2028,18 @@ convertSymbolType common_defs st imported_types collected_imports type_heaps va , ets_type_heaps :: !.TypeHeaps , ets_var_heap :: !.VarHeap } + +// MV .. +addTypesOfDictionaries :: w:(a x:CommonDefs) .[TypeContext] u:[AType] -> v:[AType] | Array .a, [u <= v, w <= x]; +addTypesOfDictionaries common_defs type_contexts type_args + = mapAppend (add_types_of_dictionary common_defs) type_contexts type_args +where + add_types_of_dictionary common_defs {tc_class = {glob_module, glob_object={ds_index}}, tc_types} + # {class_arity, class_dictionary={ds_ident,ds_index}} = common_defs.[glob_module].com_class_defs.[ds_index] + dict_type_symb = MakeTypeSymbIdent { glob_object = ds_index, glob_module = glob_module } ds_ident class_arity + = { at_attribute = TA_Multi, at_annotation = AN_Strict, at_type = TA dict_type_symb ( + map (\type -> { at_attribute = TA_Multi, at_annotation = AN_None, at_type = type }) tc_types) } +// .. MV class expandSynTypes a :: !{# CommonDefs} !a !*ExpandTypeState -> (!a, !*ExpandTypeState) @@ -2036,8 +2051,11 @@ instance expandSynTypes SymbolType where expandSynTypes common_defs st=:{st_args,st_result,st_context} ets # ((st_args,st_result), ets) = expandSynTypes common_defs (st_args,st_result) ets - # st_args = mapAppend (add_types_of_dictionary common_defs) st_context st_args +// MV .. + # st_args = addTypesOfDictionaries common_defs st_context st_args +// was: # st_args = mapAppend (add_types_of_dictionary common_defs) st_context st_args = ({st & st_args = st_args, st_result = st_result, st_arity = length st_args, st_context = [] }, ets) +// .. MV add_types_of_dictionary common_defs {tc_class = {glob_module, glob_object={ds_index}}, tc_types} # {class_arity, class_dictionary={ds_ident,ds_index}} = common_defs.[glob_module].com_class_defs.[ds_index] |