Commit ed0bbd09 authored by Martijn Vervoort's avatar Martijn Vervoort
Browse files

dynamic type bug fixed; changes to support theorem prover

parent 2d1eb791
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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
......@@ -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]
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment