Commit d24979c9 authored by Ronny Wichers Schreur's avatar Ronny Wichers Schreur 🏘
Browse files

reification of type definitions

parent dc49712a
......@@ -2,7 +2,7 @@ definition module check
import syntax, transform, checksupport, typesupport, predef
checkModule :: !ScannedModule !IndexRange ![FunDef] !Int !Int !(Optional ScannedModule) ![ScannedModule] !{#DclModule} !*{#*{#FunDef}} !*PredefinedSymbols !*SymbolTable !*File !*Heaps
checkModule :: !Bool !ScannedModule !IndexRange ![FunDef] !Int !Int !(Optional ScannedModule) ![ScannedModule] !{#DclModule} !*{#*{#FunDef}} !*PredefinedSymbols !*SymbolTable !*File !*Heaps
-> (!Bool, *IclModule, *{# DclModule}, *{! Group}, !*{#*{#FunDef}},!Int, !*Heaps, !*PredefinedSymbols, !*SymbolTable, *File, [String])
checkFunctions :: !Index !Level !Index !Index !Int !*{#FunDef} !*ExpressionInfo !*Heaps !*CheckState
......
This diff is collapsed.
......@@ -96,6 +96,7 @@ cConversionTableSize :== 10
, icl_instances :: ![IndexRange]
, icl_specials :: !IndexRange
, icl_gencases :: ![IndexRange]
, icl_type_funs :: ![IndexRange]
, icl_common :: !.CommonDefs
, icl_import :: !{!Declaration}
, icl_imported_objects :: ![ImportedObject]
......@@ -112,6 +113,7 @@ cConversionTableSize :== 10
, dcl_macros :: !IndexRange
, dcl_specials :: !IndexRange
, dcl_gencases :: !IndexRange
, dcl_type_funs :: !IndexRange
, dcl_common :: !CommonDefs
, dcl_sizes :: !{# Int}
, dcl_dictionary_info :: !DictionaryInfo
......
......@@ -1446,6 +1446,7 @@ where
, td_attribute = TA_None
, td_pos = NoPos
, td_used_types = []
, td_fun_index = NoIndex
}
cons_def =
......
......@@ -646,8 +646,14 @@ where
# predef_type_index
= type_index + FirstTypePredefinedSymbolIndex
= constructorExp (predefinedTypeConstructor predef_type_index) SK_Function 0 ci
typeConstructor (GTT_Constructor cons_ident) ci
= (App {app_symb = cons_ident, app_args = [], app_info_ptr = nilPtr}, ci)
typeConstructor (GTT_Constructor cons_ident fun_ident) ci
# type_cons
= App {app_symb = cons_ident, app_args = [], app_info_ptr = nilPtr}
# type_fun
= App {app_symb = fun_ident, app_args = [], app_info_ptr = nilPtr}
# (to_tc_symb, ci)
= getSymbol PD_Dyn__to_TypeCodeConstructor SK_Function 2 ci
= (App {app_symb = to_tc_symb, app_args = [type_cons, type_fun], app_info_ptr = nilPtr}, ci)
typeConstructor (GTT_Basic basic_type) ci
= constructorExp (basicTypeConstructor basic_type) SK_Function 0 ci
typeConstructor GTT_Function ci
......
......@@ -4,8 +4,8 @@
implementation module frontend
import scanner, parse, postparse, check, type, trans, convertcases, overloading, utilities, convertDynamics,
convertimportedtypes, compilerSwitches, analtypes, generics1
convertimportedtypes, compilerSwitches, analtypes, generics1,
typereify
//import coredump
//import print
......@@ -51,7 +51,8 @@ frontEndInterface options mod_ident search_paths cached_dcl_modules functions_an
# symbol_table = hash_table.hte_symbol_heap
#! n_cached_dcl_modules=size cached_dcl_modules
# (ok, icl_mod, dcl_mods, components, cached_dcl_macros,main_dcl_module_n,heaps, predef_symbols, symbol_table, error, directly_imported_dcl_modules)
= checkModule mod global_fun_range mod_functions n_functions_and_macros_in_dcl_modules dcl_module_n_in_cache optional_dcl_mod modules cached_dcl_modules functions_and_macros predef_symbols (symbol_table -*-> "Checking") error heaps
= checkModule support_dynamics mod global_fun_range mod_functions n_functions_and_macros_in_dcl_modules dcl_module_n_in_cache optional_dcl_mod modules cached_dcl_modules functions_and_macros predef_symbols (symbol_table -*-> "Checking") error heaps
hash_table = { hash_table & hte_symbol_heap = symbol_table}
| not ok
......@@ -62,7 +63,8 @@ frontEndInterface options mod_ident search_paths cached_dcl_modules functions_an
select_and_remove_icl_functions_from_record :: !*IclModule -> (!.{#FunDef},!.IclModule)
select_and_remove_icl_functions_from_record icl_mod=:{icl_functions} = (icl_functions,{icl_mod & icl_functions={}})
# {icl_global_functions,icl_instances,icl_gencases, icl_specials, icl_common,icl_name,icl_import,icl_imported_objects,icl_foreign_exports,icl_used_module_numbers,icl_copied_from_dcl} = icl_mod
# {icl_global_functions,icl_instances,icl_gencases, icl_specials, icl_common,icl_name,icl_import,icl_imported_objects,
icl_type_funs, icl_foreign_exports,icl_used_module_numbers,icl_copied_from_dcl} = icl_mod
/*
(_,f,files) = fopen "components" FWriteText files
(components, icl_functions, f) = showComponents components 0 True icl_functions f
......@@ -101,6 +103,16 @@ frontEndInterface options mod_ident search_paths cached_dcl_modules functions_an
// ti_common_defs = { ti_common_defs & [main_dcl_module_n] = icl_common }
// # (td_infos, th_vars, error_admin) = analyseTypeDefs ti_common_defs type_groups td_infos type_heaps.th_vars error_admin
({com_type_defs}, ti_common_defs) = replace ti_common_defs main_dcl_module_n icl_common
| support_dynamics && not (sanityCheckTypeFunctions main_dcl_module_n icl_common dcl_mods fun_defs)
= abort "frontend: sanityCheckTypeFunctions failed"
# hp_var_heap = heaps.hp_var_heap
# (fun_defs, predef_symbols, hp_var_heap, type_heaps)
= if support_dynamics
(buildTypeFunctions main_dcl_module_n fun_defs ti_common_defs
predef_symbols hp_var_heap type_heaps)
(fun_defs, predef_symbols, hp_var_heap, type_heaps)
# (td_infos, th_vars, error_admin) = analyseTypeDefs ti_common_defs type_groups com_type_defs main_dcl_module_n td_infos type_heaps.th_vars error_admin
# (class_infos, td_infos, th_vars, error_admin)
= determineKindsOfClasses icl_used_module_numbers ti_common_defs td_infos th_vars error_admin
......@@ -110,7 +122,7 @@ frontEndInterface options mod_ident search_paths cached_dcl_modules functions_an
type_heaps = { type_heaps & th_vars = th_vars }
# heaps = { heaps & hp_type_heaps = type_heaps, hp_expression_heap = hp_expression_heap, hp_generic_heap = gen_heap }
# heaps = { heaps & hp_type_heaps = type_heaps, hp_expression_heap = hp_expression_heap, hp_generic_heap = gen_heap, hp_var_heap=hp_var_heap }
# (saved_main_dcl_common, ti_common_defs) = replace (dcl_common_defs dcl_mods) main_dcl_module_n icl_common
with
dcl_common_defs :: .{#DclModule} -> .{#CommonDefs} // needed for Clean 2.0 to disambiguate overloading
......@@ -159,7 +171,7 @@ frontEndInterface options mod_ident search_paths cached_dcl_modules functions_an
# (fun_def_size, fun_defs) = usize fun_defs
# (components, fun_defs) = partitionateFunctions (fun_defs -*-> "partitionateFunctions")
(icl_global_functions++icl_instances ++ [icl_specials] ++ icl_gencases ++ generic_ranges)
(icl_global_functions++icl_instances ++ [icl_specials] ++ icl_gencases ++ generic_ranges ++ icl_type_funs)
| options.feo_up_to_phase == FrontEndPhaseTypeCheck
= frontSyntaxTree cached_dcl_macros cached_dcl_mods n_functions_and_macros_in_dcl_modules main_dcl_module_n
......@@ -191,7 +203,7 @@ frontEndInterface options mod_ident search_paths cached_dcl_modules functions_an
= transformGroups cleanup_info main_dcl_module_n stdStrictLists_module_n def_min def_max (components -*-> "Transform") fun_defs acc_args common_defs imported_funs dcl_types used_conses_in_dynamics type_def_infos var_heap type_heaps expression_heap options.feo_fusion error predef_symbols
# error_admin = {ea_file = error, ea_loc = [], ea_ok = True }
# {dcl_instances,dcl_specials,dcl_gencases} = dcl_mods.[main_dcl_module_n]
# {dcl_instances,dcl_specials,dcl_gencases,dcl_type_funs} = dcl_mods.[main_dcl_module_n]
# (start_rule_index,predef_symbols) = get_index_of_start_rule predef_symbols
with
get_index_of_start_rule predef_symbols
......@@ -206,7 +218,7 @@ frontEndInterface options mod_ident search_paths cached_dcl_modules functions_an
# exported_global_functions = case start_rule_index of
NoIndex -> [icl_exported_global_functions]
sri -> [{ir_from=sri,ir_to=inc sri},icl_exported_global_functions]
# exported_functions = exported_global_functions ++ [dcl_instances,dcl_specials,dcl_gencases]
# exported_functions = exported_global_functions ++ [dcl_instances,dcl_specials,dcl_gencases,dcl_type_funs]
# (components, fun_defs, predef_symbols, var_heap, expression_heap, error_admin)
= case options.feo_strip_unused of
True -> partitionateFunctions` (fun_defs -*-> "partitionateFunctions`")
......@@ -272,7 +284,8 @@ frontEndInterface options mod_ident search_paths cached_dcl_modules functions_an
icl_common=icl_common, icl_gencases = icl_gencases ++ generic_ranges,
icl_import=icl_import, icl_imported_objects=icl_imported_objects, icl_foreign_exports=icl_foreign_exports,
icl_name=icl_name,icl_used_module_numbers=icl_used_module_numbers,
icl_copied_from_dcl=icl_copied_from_dcl,icl_modification_time=icl_mod.icl_modification_time}
icl_copied_from_dcl=icl_copied_from_dcl,icl_modification_time=icl_mod.icl_modification_time,
icl_type_funs = icl_type_funs}
, fe_dcls = dcl_mods
, fe_components = components
......
......@@ -1300,6 +1300,8 @@ toTypeCodeConstructor type=:{glob_object=type_index, glob_module=module_index} c
// sanity check ...
# type_ident
= types.[type_index].td_ident.id_name
# td_fun_index
= types.[type_index].td_fun_index
# tc_type_name
= types.[tc_type_index].td_ident.id_name
| "TC;" +++ type_ident <> tc_type_name
......@@ -1311,7 +1313,15 @@ toTypeCodeConstructor type=:{glob_object=type_index, glob_module=module_index} c
= { symb_ident = ds_ident
, symb_kind = SK_Constructor {glob_module = module_index, glob_object = ds_index}
}
= GTT_Constructor type_constructor
// sanity check ...
| td_fun_index == NoIndex
= fatal "toTypeCodeConstructor" ("no function (" +++ type_ident +++ ")")
// ... sanity check
# type_fun
= { symb_ident = {ds_ident & id_info = nilPtr} // this is wrong but let's give it a try
, symb_kind = SK_Function {glob_module = module_index, glob_object = td_fun_index}
}
= GTT_Constructor type_constructor type_fun
fatal :: {#Char} {#Char} -> .a
fatal function_name message
......
......@@ -1062,13 +1062,13 @@ parseAndScanDclModule dcl_module import_file_position parsed_modules cached_modu
# (parse_ok, mod, ca_hash_table, err_file, files) = wantModule cWantDclFile dcl_module import_file_position support_generics ca_hash_table ca_error.pea_file searchPaths modtimefunction files
# ca = {ca & ca_hash_table=ca_hash_table, ca_error={pea_file=err_file,pea_ok=True} }
| parse_ok
= scan_dcl_module mod parsed_modules searchPaths modtimefunction files ca
= scan_dcl_module dcl_module mod parsed_modules searchPaths modtimefunction files ca
= (False, [MakeEmptyModule mod.mod_ident MK_None: parsed_modules],files, ca)
where
scan_dcl_module :: ParsedModule [ScannedModule] !SearchPaths (ModTimeFunction *Files) *Files *CollectAdmin -> (Bool, [ScannedModule],*Files, *CollectAdmin)
scan_dcl_module mod=:{mod_defs = pdefs} parsed_modules searchPaths modtimefunction files ca
scan_dcl_module :: Ident ParsedModule [ScannedModule] !SearchPaths (ModTimeFunction *Files) *Files *CollectAdmin -> (Bool, [ScannedModule],*Files, *CollectAdmin)
scan_dcl_module dcl_module mod=:{mod_defs = pdefs} parsed_modules searchPaths modtimefunction files ca
# (_, defs, imports, imported_objects,foreign_exports,ca)
= reorganiseDefinitionsAndAddTypes support_dynamics False pdefs ca
= reorganiseDefinitionsAndAddTypes dcl_module support_dynamics False pdefs ca
(def_macros, ca) = collectFunctions defs.def_macros False {ca & ca_fun_count=0,ca_rev_fun_defs=[]}
(range, ca) = addFunctionsRange def_macros ca
(rev_fun_defs,ca) = ca!ca_rev_fun_defs
......@@ -1089,7 +1089,7 @@ scanModule mod=:{mod_ident,mod_type,mod_defs = pdefs} cached_modules support_gen
, ca_rev_fun_defs = []
, ca_hash_table = hash_table
}
(fun_defs, defs, imports, imported_objects,foreign_exports,ca) = reorganiseDefinitionsAndAddTypes support_dynamics True pdefs ca
(fun_defs, defs, imports, imported_objects,foreign_exports,ca) = reorganiseDefinitionsAndAddTypes mod_ident support_dynamics True pdefs ca
(reorganise_icl_ok, ca) = ca!ca_error.pea_ok
......@@ -1156,7 +1156,7 @@ where
| not parse_ok
= (False, No,NoIndex, [],cached_modules, files, ca)
# pdefs = mod.mod_defs
# (_, defs, imports, imported_objects,foreign_exports,ca) = reorganiseDefinitionsAndAddTypes support_dynamics False pdefs ca
# (_, defs, imports, imported_objects,foreign_exports,ca) = reorganiseDefinitionsAndAddTypes mod_ident support_dynamics False pdefs ca
# mod = { mod & mod_imports = imports, mod_imported_objects = imported_objects, mod_defs = defs}
# cached_modules = [mod.mod_ident:cached_modules]
# (import_ok, parsed_modules,files, ca) = scanModules imports [] cached_modules searchPaths support_generics support_dynamics modtimefunction files ca
......@@ -1467,10 +1467,18 @@ reorganiseDefinitions icl_module [] _ _ _ _ ca
def_instances = [], def_funtypes = [],
def_generics = [], def_generic_cases = []}, [], [], [], ca)
reorganiseDefinitionsAndAddTypes support_dynamics icl_module defs ca
reorganiseDefinitionsAndAddTypes mod_ident support_dynamics icl_module defs ca
| support_dynamics
# clean_types_module_ident
= predefined_idents.[PD_CleanTypes]
# clean_types_module =
{ import_module = clean_types_module_ident
, import_symbols = []
, import_file_position = NoPos
}
# imports = if (mod_ident == clean_types_module_ident) [] [clean_types_module]
# (rev_defs, ca)
= addTypeConstructors defs [] ca
= addTypeConstructors defs [PD_Import imports] ca
= reorganiseDefinitions icl_module (reverse rev_defs) 0 0 0 0 ca
= reorganiseDefinitions icl_module defs 0 0 0 0 ca
where
......@@ -1501,6 +1509,7 @@ addTypeConstructor def=:{td_ident, td_attribute, td_attrs, td_args, td_arity, td
, td_attribute = attr
, td_pos = position
, td_used_types = []
, td_fun_index = NoIndex
}
type_tc_cons cons_ident type_ident args arity position
= { pc_cons_ident = cons_ident
......
......@@ -248,7 +248,20 @@ PD_FromThenToU :== 259
PD_FromThenToUTS :== 260
PD_FromThenToO :== 261
PD_NrOfPredefSymbols :== 262
/* Clean Type introspection */
PD_CleanTypes :== 262
PD_CTTypeDef :== 263
PD_CTAlgType :== 264
PD_CTRecordType :== 265
PD_CTSynType :== 266
PD_CTPredefined :== 267
PD_CTConsDef :== 268
PD__CTToCons :== 269
PD_CTFieldDef :== 270
PD_Dyn__to_TypeCodeConstructor :== 271
PD_NrOfPredefSymbols :== 272
GetTupleConsIndex tup_arity :== PD_Arity2TupleSymbol + tup_arity - 2
GetTupleTypeIndex tup_arity :== PD_Arity2TupleType + tup_arity - 2
......
......@@ -132,6 +132,8 @@ predefined_idents
[PD_Dyn_TypeCodeConstructor_StrictArray] = i "TypeCodeConstructor_StrictArray",
[PD_Dyn_TypeCodeConstructor_UnboxedArray] = i "TypeCodeConstructor_UnboxedArray",
[PD_Dyn__to_TypeCodeConstructor] = i "_to_TypeCodeConstructor",
[PD_StdGeneric] = i "StdGeneric",
[PD_TypeBimap] = i "Bimap",
[PD_ConsBimap] = i "_Bimap",
......@@ -213,7 +215,17 @@ predefined_idents
[PD_FromThenToSTS]= i "_from_then_to_sts",
[PD_FromThenToU]= i "_from_then_to_u",
[PD_FromThenToUTS]= i "_from_then_to_uts",
[PD_FromThenToO]= i "_from_then_to_o"
[PD_FromThenToO]= i "_from_then_to_o",
[PD_CleanTypes] = i "StdCleanTypes",
[PD_CTTypeDef] = i "CTTypeDef",
[PD_CTAlgType] = i "CTAlgType",
[PD_CTRecordType] = i "CTRecordType",
[PD_CTSynType] = i "CTSynType",
[PD_CTPredefined] = i "CTPredefined",
[PD_CTConsDef] = i "CTConsDef",
[PD__CTToCons] = i "CTToCons",
[PD_CTFieldDef] = i "CTFieldDef"
}
=: idents
......@@ -364,6 +376,8 @@ where
<<- (local_predefined_idents, IC_Expression, PD_Dyn_TypeCodeConstructor_StrictArray)
<<- (local_predefined_idents, IC_Expression, PD_Dyn_TypeCodeConstructor_UnboxedArray)
<<- (local_predefined_idents, IC_Expression, PD_Dyn__to_TypeCodeConstructor)
<<- (local_predefined_idents, IC_Module, PD_StdGeneric)
<<- (local_predefined_idents, IC_Type, PD_TypeBimap)
<<- (local_predefined_idents, IC_Expression, PD_ConsBimap)
......@@ -412,6 +426,16 @@ where
<<- (local_predefined_idents, IC_Expression, PD_abort)
<<- (local_predefined_idents, IC_Expression, PD_undef)
<<- (local_predefined_idents, IC_Module, PD_CleanTypes)
<<- (local_predefined_idents, IC_Type, PD_CTTypeDef)
<<- (local_predefined_idents, IC_Expression, PD_CTAlgType)
<<- (local_predefined_idents, IC_Expression, PD_CTRecordType)
<<- (local_predefined_idents, IC_Expression, PD_CTSynType)
<<- (local_predefined_idents, IC_Expression, PD_CTPredefined)
<<- (local_predefined_idents, IC_Type, PD_CTConsDef)
<<- (local_predefined_idents, IC_Expression, PD__CTToCons)
<<- (local_predefined_idents, IC_Type, PD_CTFieldDef)
<<- (local_predefined_idents, IC_Expression, PD_Start)
<<- (local_predefined_idents, IC_Expression, PD_FromS)
......
......@@ -444,6 +444,7 @@ NoGlobalIndex :== {gi_module=NoIndex,gi_index=NoIndex}
, td_attribute :: !TypeAttribute
, td_pos :: !Position
, td_used_types :: ![GlobalIndex]
, td_fun_index :: !Index
}
:: TypeDefInfo =
......@@ -936,6 +937,7 @@ cNonRecursiveAppl :== False
| TVI_AttrAndRefCount !TypeAttribute !Int
| TVI_CorrespondenceNumber !Int /* auxiliary used in module comparedefimp */
| TVI_AType !AType /* auxiliary used in module comparedefimp */
| TVI_Reify !Int
| 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 */
......@@ -1278,7 +1280,11 @@ instance == OverloadedListType
| TCE_UniType ![VarInfoPtr] !TypeCodeExpression
| TCE_UnqType !TypeCodeExpression
:: GlobalTCType = GTT_Basic !BasicType | GTT_Constructor !SymbIdent | GTT_PredefTypeConstructor !(Global Index) | GTT_Function
:: GlobalTCType
= GTT_Basic !BasicType
| GTT_Constructor !SymbIdent !SymbIdent // type_cons type_fun
| GTT_PredefTypeConstructor !(Global Index)
| GTT_Function
:: AlgebraicPattern =
{ ap_symbol :: !(Global DefinedSymbol)
......@@ -1417,7 +1423,8 @@ ParsedInstanceToClassInstance pi members :==
MakeTypeDef name lhs rhs attr contexts pos :==
{ td_ident = 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, td_used_types = [] }
td_pos = pos, td_rhs = rhs, td_used_types = [], td_fun_index = NoIndex
}
MakeDefinedSymbol ident index arity :== { ds_ident = ident, ds_arity = arity, ds_index = index }
......
Markdown is supported
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