diff options
-rw-r--r-- | frontend/generics1.icl | 92 | ||||
-rw-r--r-- | frontend/syntax.dcl | 2 | ||||
-rw-r--r-- | frontend/syntax.icl | 2 |
3 files changed, 53 insertions, 43 deletions
diff --git a/frontend/generics1.icl b/frontend/generics1.icl index 399a7e9..8e82e47 100644 --- a/frontend/generics1.icl +++ b/frontend/generics1.icl @@ -978,7 +978,7 @@ where = build_exprs_for_conses is_record 0 (length cons_def_syms) type_def_mod cons_def_syms heaps error # case_patterns = AlgebraicPatterns {glob_module = type_def_mod, glob_object = type_def_index} case_alts # (case_expr, heaps) = buildCaseExpr arg_expr case_patterns heaps - = (case_expr, heaps, error) + = (case_expr, heaps, error) // build conversions for constructors build_exprs_for_conses :: !Bool !Int !Int !Int ![DefinedSymbol] !*Heaps !*ErrorAdmin @@ -989,7 +989,7 @@ where #! (alt, heaps, error) = build_expr_for_cons is_record i n type_def_mod cons_def_sym heaps error #! (alts, heaps, error) = build_exprs_for_conses is_record (i+1) n type_def_mod cons_def_syms heaps error = ([alt:alts], heaps, error) - + // build conversion for a constructor build_expr_for_cons :: !Bool !Int !Int !Int !DefinedSymbol !*Heaps !*ErrorAdmin -> (AlgebraicPattern, !*Heaps, !*ErrorAdmin) @@ -2055,7 +2055,7 @@ where // generic function specialized to the generic representation of the type build_specialized_expr gc_pos gc_ident gcf_generic gtr_type td_args generated_arg_exprs gen_info_ptr funs_and_groups td_infos heaps error - #! spec_env = [(atv_variable, TVI_Expr expr) \\ {atv_variable} <- td_args & expr <- generated_arg_exprs] + #! spec_env = [(atv_variable, TVI_Expr False expr) \\ {atv_variable} <- td_args & expr <- generated_arg_exprs] # generic_bimap = predefs.[PD_GenericBimap] | gcf_generic.gi_module==generic_bimap.pds_module && gcf_generic.gi_index==generic_bimap.pds_def @@ -2128,11 +2128,11 @@ where build_bimap_expr non_gen_var KindConst funs_and_groups heaps # (expr, funs_and_groups, heaps) = bimap_id_expression main_module_index predefs funs_and_groups heaps - = ((non_gen_var, TVI_Expr expr), funs_and_groups, heaps) + = ((non_gen_var, TVI_Expr True expr), funs_and_groups, heaps) build_bimap_expr non_gen_var kind funs_and_groups heaps #! (expr, heaps) = buildGenericApp bimap_module bimap_index bimap_ident kind [] heaps - = ((non_gen_var, TVI_Expr expr), funs_and_groups, heaps) + = ((non_gen_var, TVI_Expr False expr), funs_and_groups, heaps) buildGenericCaseBody main_module_index {gc_ident,gc_pos} has_generic_info st predefs funs_and_groups td_infos modules heaps error # error = reportError gc_ident gc_pos "cannot specialize to this type" error @@ -2378,7 +2378,7 @@ where # (expr, th_vars) = readPtr tv_info_ptr th_vars # heaps = {heaps & hp_type_heaps = {th & th_vars = th_vars}} = case expr of - TVI_Expr expr + TVI_Expr is_bimap_id expr -> (expr, (td_infos, heaps, error)) TVI_Iso iso_ds to_ds from_ds # (expr,heaps) = buildFunApp main_module_index iso_ds [] heaps @@ -2420,14 +2420,14 @@ where = (expr @ arg_exprs, st) specialize (GTSVar tv) st = specialize_type_var tv st - specialize (GTSArrow x y) st - | is_bimap_id x + specialize (GTSArrow x y) st=:(_,heaps,_) + | is_bimap_id x heaps #! (y, st) = specialize y st # (funs_and_groups, heaps, error) = st (expr, funs_and_groups, heaps) = bimap_arrow_arg_id_expression [y] main_module_index predefs funs_and_groups heaps = (expr, (funs_and_groups, heaps, error)) - | is_bimap_id y + | is_bimap_id y heaps #! (x, st) = specialize x st # (funs_and_groups, heaps, error) = st (expr, funs_and_groups, heaps) @@ -2480,7 +2480,7 @@ where # (expr, th_vars) = readPtr tv_info_ptr th_vars # heaps = {heaps & hp_type_heaps = {th & th_vars = th_vars}} = case expr of - TVI_Expr expr + TVI_Expr is_bimap_id expr -> (expr, (funs_and_groups, heaps, error)) TVI_Iso iso_ds to_ds from_ds # (expr,heaps) = buildFunApp main_module_index iso_ds [] heaps @@ -2491,10 +2491,6 @@ where = buildGenericApp gen_index.gi_module gen_index.gi_index gen_ident kind arg_exprs heaps = (expr, (funs_and_groups, heaps, error)) -is_bimap_id (GTSAppCons KindConst []) = True -is_bimap_id GTSAppConsBimapKindConst = True -is_bimap_id _ = False - adapt_with_specialized_generic_bimap :: !GlobalIndex // generic index !GenTypeStruct // type to specialize to @@ -2527,13 +2523,13 @@ where adapt_args arg_exprs args_type st = ([],arg_exprs,args_type,st) - adapt_arg arg_type arg_expr st - | is_bimap_id arg_type + adapt_arg arg_type arg_expr st=:(_,_,heaps,_) + | is_bimap_id arg_type heaps = (arg_expr,st) = specialize_to_with_arg arg_type arg_expr st - adapt_result arg_exprs type specialized_expr adapted_arg_exprs st - | is_bimap_id type + adapt_result arg_exprs type specialized_expr adapted_arg_exprs st=:(_,_,heaps,_) + | is_bimap_id type heaps = (build_body_expr specialized_expr adapted_arg_exprs arg_exprs,st) with build_body_expr specialized_expr [] [] @@ -2561,7 +2557,7 @@ where # (expr, th_vars) = readPtr tv_info_ptr th_vars # heaps = {heaps & hp_type_heaps = {th & th_vars = th_vars}} = case expr of - TVI_Expr expr + TVI_Expr is_bimap_id expr # expr = build_map_to_expr expr predefs @ [arg] -> (expr, (funs_and_groups, modules, heaps, error)) TVI_Iso iso_ds to_ds from_ds @@ -2578,7 +2574,7 @@ where # (expr, th_vars) = readPtr tv_info_ptr th_vars # heaps = {heaps & hp_type_heaps = {th & th_vars = th_vars}} = case expr of - TVI_Expr expr + TVI_Expr is_bimap_id expr # expr = build_map_from_expr expr predefs @ [arg] -> (expr, (funs_and_groups, modules, heaps, error)) TVI_Iso iso_ds to_ds from_ds @@ -2603,12 +2599,12 @@ where # (x_expr, th_vars) = readPtr xp th_vars (y_expr, th_vars) = readPtr yp th_vars heaps = {heaps & hp_type_heaps = {th & th_vars = th_vars}} - | is_bimap_id_expression x_expr main_module_index funs_and_groups + | is_bimap_id_expression x_expr # (y,heaps) = build_map_from_tvi_expr y_expr main_module_index predefs heaps (expr, funs_and_groups, heaps) = bimap_from_arrow_arg_id_expression [y] main_module_index predefs funs_and_groups heaps = (expr, (funs_and_groups, modules, heaps, error)) - | is_bimap_id_expression y_expr main_module_index funs_and_groups + | is_bimap_id_expression y_expr # (x,heaps) = build_map_to_tvi_expr x_expr main_module_index predefs heaps (expr, funs_and_groups, heaps) = bimap_from_arrow_res_id_expression [x] main_module_index predefs funs_and_groups heaps @@ -2621,7 +2617,7 @@ where specialize_from (GTSArrow (GTSVar {tv_info_ptr}) y) (funs_and_groups, modules, heaps=:{hp_type_heaps=th=:{th_vars}}, error) #! (expr, th_vars) = readPtr tv_info_ptr th_vars # heaps = {heaps & hp_type_heaps = {th & th_vars = th_vars}} - | is_bimap_id_expression expr main_module_index funs_and_groups + | is_bimap_id_expression expr # st = (funs_and_groups, modules, heaps, error) = specialize_from_arrow_arg_id y st # (x,heaps) = build_map_to_tvi_expr expr main_module_index predefs heaps @@ -2633,7 +2629,7 @@ where specialize_from (GTSArrow x (GTSVar {tv_info_ptr})) (funs_and_groups, modules, heaps=:{hp_type_heaps=th=:{th_vars}}, error) #! (expr, th_vars) = readPtr tv_info_ptr th_vars # heaps = {heaps & hp_type_heaps = {th & th_vars = th_vars}} - | is_bimap_id_expression expr main_module_index funs_and_groups + | is_bimap_id_expression expr # st = (funs_and_groups, modules, heaps, error) = specialize_from_arrow_res_id x st # (y,heaps) = build_map_from_tvi_expr expr main_module_index predefs heaps @@ -2653,7 +2649,7 @@ where # (expr, th_vars) = readPtr tv_info_ptr th_vars # heaps = {heaps & hp_type_heaps = {th & th_vars = th_vars}} = case expr of - TVI_Expr expr + TVI_Expr is_bimap_id expr # from_expr = build_map_from_expr expr predefs -> (from_expr, (funs_and_groups, modules, heaps, error)) TVI_Iso iso_ds to_ds from_ds @@ -2667,7 +2663,7 @@ where = bimap_from_Bimap_expression [arg1,arg2] main_module_index predefs funs_and_groups heaps = (expr, (funs_and_groups, modules, heaps, error)) specialize_from type (funs_and_groups, modules, heaps, error) - #! (bimap_expr, st) + #! (bimap_expr, st) = specialize type (funs_and_groups, modules, heaps, error) # adaptor_expr = build_map_from_expr bimap_expr predefs = (adaptor_expr, st) @@ -2690,7 +2686,7 @@ where # (expr, th_vars) = readPtr tv_info_ptr th_vars # heaps = {heaps & hp_type_heaps = {th & th_vars = th_vars}} = case expr of - TVI_Expr expr + TVI_Expr is_bimap_id expr # from_expr = build_map_to_expr expr predefs -> (from_expr, (funs_and_groups, modules, heaps, error)) TVI_Iso iso_ds to_ds from_ds @@ -2730,14 +2726,14 @@ where = (expr @ arg_exprs, st) specialize (GTSVar tv) st = specialize_type_var tv st - specialize (GTSArrow x y) st - | is_bimap_id x + specialize (GTSArrow x y) st=:(_,_,heaps,_) + | is_bimap_id x heaps #! (y, st) = specialize y st # (funs_and_groups, modules, heaps, error) = st (expr, funs_and_groups, heaps) = bimap_arrow_arg_id_expression [y] main_module_index predefs funs_and_groups heaps = (expr, (funs_and_groups, modules, heaps, error)) - | is_bimap_id y + | is_bimap_id y heaps #! (x, st) = specialize x st # (funs_and_groups, modules, heaps, error) = st (expr, funs_and_groups, heaps) @@ -2761,7 +2757,7 @@ where # (expr, th_vars) = readPtr tv_info_ptr th_vars # heaps = {heaps & hp_type_heaps = {th & th_vars = th_vars}} = case expr of - TVI_Expr expr + TVI_Expr is_bimap_id expr -> (expr, (funs_and_groups, modules, heaps, error)) TVI_Iso iso_ds to_ds from_ds # (expr,heaps) = buildFunApp main_module_index iso_ds [] heaps @@ -2792,8 +2788,8 @@ where build_to_alg_patterns [] [] type_module_n funs_and_groups modules heaps error = ([],funs_and_groups,modules,heaps,error) - specialize_to_with_args [type:types] [arg:args] st - | is_bimap_id type + specialize_to_with_args [type:types] [arg:args] st=:(_,_,heaps,_) + | is_bimap_id type heaps # (args,st) = specialize_to_with_args types args st = ([arg:args],st) @@ -2826,9 +2822,9 @@ where = ([alg_pattern:alg_patterns],funs_and_groups,modules,heaps,error) build_from_alg_patterns [] [] type_module_n funs_and_groups modules heaps error = ([],funs_and_groups,modules,heaps,error) - - specialize_from_with_args [type:types] [arg:args] st - | is_bimap_id type + + specialize_from_with_args [type:types] [arg:args] st=:(_,_,heaps,_) + | is_bimap_id type heaps # (args,st) = specialize_from_with_args types args st = ([arg:args],st) @@ -2899,9 +2895,23 @@ where # heaps = {heaps & hp_expression_heap = hp_expression_heap} = (alg_pattern,heaps) -is_bimap_id_expression (TVI_Expr (App {app_symb={symb_kind=SK_Function fun_glob},app_args=[]})) main_module_index {fg_bimap_functions={bimap_id_function={fii_index}}} - = fii_index>=0 && fun_glob.glob_module==main_module_index && fun_glob.glob_object==fii_index -is_bimap_id_expression _ main_module_index _ +is_bimap_id :: !GenTypeStruct !Heaps -> Bool +is_bimap_id (GTSAppCons KindConst []) heaps + = True +is_bimap_id GTSAppConsBimapKindConst heaps + = True +is_bimap_id (GTSVar {tv_info_ptr}) heaps + = case sreadPtr tv_info_ptr heaps.hp_type_heaps.th_vars of + TVI_Expr is_bimap_id expr + -> is_bimap_id + _ + -> False +is_bimap_id _ heaps + = False + +is_bimap_id_expression (TVI_Expr is_bimap_id _) + = is_bimap_id +is_bimap_id_expression _ = False set_tvs spec_env heaps=:{hp_type_heaps=hp_type_heaps=:{th_vars}} @@ -4292,7 +4302,7 @@ buildCaseExpr case_arg case_alts heaps=:{hp_expression_heap} # heaps = { heaps & hp_expression_heap = hp_expression_heap} = (expr, heaps) -build_map_from_tvi_expr (TVI_Expr bimap_expr) main_module_index predefs heaps +build_map_from_tvi_expr (TVI_Expr is_bimap_id bimap_expr) main_module_index predefs heaps = (buildRecordSelectionExpr bimap_expr PD_map_from 1 predefs, heaps) build_map_from_tvi_expr (TVI_Iso iso_ds to_ds from_ds) main_module_index predefs heaps = buildFunApp main_module_index from_ds [] heaps @@ -4300,7 +4310,7 @@ build_map_from_tvi_expr (TVI_Iso iso_ds to_ds from_ds) main_module_index predefs build_map_from_expr bimap_expr predefs = buildRecordSelectionExpr bimap_expr PD_map_from 1 predefs -build_map_to_tvi_expr (TVI_Expr bimap_expr) main_module_index predefs heaps +build_map_to_tvi_expr (TVI_Expr is_bimap_id bimap_expr) main_module_index predefs heaps = (buildRecordSelectionExpr bimap_expr PD_map_to 0 predefs, heaps) build_map_to_tvi_expr (TVI_Iso iso_ds to_ds from_ds) main_module_index predefs heaps = buildFunApp main_module_index to_ds [] heaps diff --git a/frontend/syntax.dcl b/frontend/syntax.dcl index 851125e..11b13b2 100644 --- a/frontend/syntax.dcl +++ b/frontend/syntax.dcl @@ -1028,7 +1028,7 @@ cNonRecursiveAppl :== False | TVI_Kind !TypeKind | TVI_ConsInstance !DefinedSymbol //AA: generic cons instance function | TVI_Normalized !Int /* MV - position of type variable in its definition */ - | TVI_Expr !Expression /* AA: Expression corresponding to the type var during generic specialization */ + | TVI_Expr !Bool !Expression /* AA: Expression corresponding to the type var during generic specialization */ | TVI_Iso !DefinedSymbol !DefinedSymbol !DefinedSymbol | TVI_GenTypeVarNumber !Int | TVI_CPSTypeVar !CheatCompiler /* MdM: a pointer to a variable in CleanProverSystem is stored here, using a cast */ diff --git a/frontend/syntax.icl b/frontend/syntax.icl index c98e112..ffc46fb 100644 --- a/frontend/syntax.icl +++ b/frontend/syntax.icl @@ -803,7 +803,7 @@ where (<<<) file (TVI_PropClass _ _ _) = file <<< "TVI_PropClass" (<<<) file (TVI_TypeKind kind_info_ptr) = file <<< "TVI_TypeKind " <<< (ptrToInt kind_info_ptr) (<<<) file (TVI_Kind kind) = file <<< "TVI_Kind" <<< kind - (<<<) file (TVI_Expr expr) = file <<< "TVI_Expr " <<< expr + (<<<) file (TVI_Expr is_bimap_id expr) = file <<< "TVI_Expr " <<< is_bimap_id <<< ' ' <<< expr instance <<< AttrVarInfo where |