PreviousUpNext

15.4.674  src/lib/compiler/front/typer/types/eq-types.pkg

## eq-types.pkg 

# Compiled by:
#     src/lib/compiler/front/typer/typer.sublib

# This file does not belong here.
# It relies on the module semantics and
# it should be moved to modules/ directory. (ZHONG)    XXX BUGGO FIXME


stipulate
    package mld =  module_level_declarations;                                   # module_level_declarations     is from   src/lib/compiler/front/typer-stuff/modules/module-level-declarations.pkg
herein

    api Eq_Types {
        #
        eq_analyze:  (mld::Package,
                      (stamp::Stamp -> Bool),
                      error_message::Plaint_Sink)
                    -> Void;

        define_eq_props:  (List( types::Typ ),
                           expand_typ::Api_Context,
                           typerstore::Typerstore)
                        -> Void;

        check_eq_ty_sig:  (types::Type,
                           types::Type_Scheme_Arg_Eq_Properties) 
                       -> Bool;

           # check whether type type is an equality type, given a Type_Scheme_Arg_Eq_Properties
           # indicating which TYPE_SCHEME_ARG_I elements are equality types.  
           # This isn't accurate on (relatized) types containing PATHtyps,
           # which are effectively treated as ty::CHUNK


        is_equality_typ:  types::Typ -> Bool;
        is_equality_type:  types::Type -> Bool;
        debugging:  Ref(  Bool );

    };
end;


stipulate
    package err =  error_message;                               # error_message                 is from   src/lib/compiler/front/basics/errormsg/error-message.pkg
    package ip  =  inverse_path;                                # inverse_path                  is from   src/lib/compiler/front/typer-stuff/basics/symbol-path.pkg
    package lms =  list_mergesort;                              # list_mergesort                is from   src/lib/src/list-mergesort.pkg
    package mj  =  module_junk;                                 # module_junk                   is from   src/lib/compiler/front/typer-stuff/modules/module-junk.pkg
    package mld =  module_level_declarations;                   # module_level_declarations     is from   src/lib/compiler/front/typer-stuff/modules/module-level-declarations.pkg
    package sta =  stamp;                                       # stamp                         is from   src/lib/compiler/front/typer-stuff/basics/stamp.pkg
    package ts  =  type_junk;                                   # type_junk                     is from   src/lib/compiler/front/typer-stuff/types/type-junk.pkg
    package ty  =  types;                                       # types                         is from   src/lib/compiler/front/typer-stuff/types/types.pkg
    package tyj =  type_junk;                                   # type_junk                     is from   src/lib/compiler/front/typer-stuff/types/type-junk.pkg
    #
herein 

    package   eq_types
    : (weak)  Eq_Types                                          # Eq_Types      is from   src/lib/compiler/front/typer/types/eq-types.pkg
    {
        # Functions to determine and check equality types 
        #

        #  Debugging 
        fun bug msg = err::impossible("EqTypes: " + msg);
        say = control_print::say;
        debugging = REF FALSE;

        fun if_debugging_say (msg: String)
            =
            if   *debugging 
                say msg;
                say "\n";
            fi;

        fun all (f: X -> Bool) [] =>   TRUE;
            all f (x ! r)         =>   f x  and  all f r;
        end;

        #  join of eqprops 

        exception INCONSISTENT;

        fun join (ty::eq_type::UNDEF,         ty::eq_type::YES          ) => ty::eq_type::YES;
            join (ty::eq_type::YES,           ty::eq_type::UNDEF        ) => ty::eq_type::YES;
            join (ty::eq_type::UNDEF,         ty::eq_type::NO           ) => ty::eq_type::NO;
            join (ty::eq_type::NO,            ty::eq_type::UNDEF        ) => ty::eq_type::NO;
            join (ty::eq_type::UNDEF,         ty::eq_type::INDETERMINATE) => ty::eq_type::INDETERMINATE;
            join (ty::eq_type::INDETERMINATE, ty::eq_type::UNDEF        ) => ty::eq_type::INDETERMINATE;
            join (ty::eq_type::UNDEF,         ty::eq_type::DATA         ) => ty::eq_type::DATA;
            join (ty::eq_type::DATA,          ty::eq_type::UNDEF        ) => ty::eq_type::DATA;
            join (ty::eq_type::UNDEF,         ty::eq_type::UNDEF        ) => ty::eq_type::UNDEF;
            join (ty::eq_type::DATA,          ty::eq_type::YES          ) => ty::eq_type::YES;
            join (ty::eq_type::YES,           ty::eq_type::DATA         ) => ty::eq_type::YES;
            join (ty::eq_type::DATA,          ty::eq_type::NO           ) => ty::eq_type::NO;
            join (ty::eq_type::NO,            ty::eq_type::DATA         ) => ty::eq_type::NO;
            join (ty::eq_type::DATA,          ty::eq_type::INDETERMINATE) => ty::eq_type::INDETERMINATE;
            join (ty::eq_type::INDETERMINATE, ty::eq_type::DATA         ) => ty::eq_type::INDETERMINATE;
            join (ty::eq_type::DATA,          ty::eq_type::DATA         ) => ty::eq_type::DATA;
            join (ty::eq_type::INDETERMINATE, ty::eq_type::YES          ) => ty::eq_type::YES; #  ? 
            join (ty::eq_type::YES,           ty::eq_type::INDETERMINATE) => ty::eq_type::YES; #  ? 
            join (ty::eq_type::INDETERMINATE, ty::eq_type::NO           ) => ty::eq_type::NO;
            join (ty::eq_type::NO,            ty::eq_type::INDETERMINATE) => ty::eq_type::NO;
            join (ty::eq_type::INDETERMINATE, ty::eq_type::INDETERMINATE) => ty::eq_type::INDETERMINATE;
            join (ty::eq_type::YES,           ty::eq_type::YES          ) => ty::eq_type::YES;
            join (ty::eq_type::NO,            ty::eq_type::NO           ) => ty::eq_type::NO;
            join (ty::eq_type::CHUNK,         ty::eq_type::CHUNK        ) => ty::eq_type::CHUNK;
            #
            join (ty::eq_type::EQ_ABSTRACT, e) => join (ty::eq_type::NO, e);
            join (e, ty::eq_type::EQ_ABSTRACT) => join (e, ty::eq_type::NO);
            #
            join (e1, e2)
                => 
                {   say (string::cat [tyj::equality_property_to_string e1, ", ", tyj::equality_property_to_string e2, "\n"]);
                    raise exception INCONSISTENT;
                };
        end;

        fun chunk_typ (ty::PLAIN_TYP { eqtype_info => REF ty::eq_type::CHUNK, ... } ) => TRUE;
            chunk_typ _ => FALSE;
        end;

        #  Calculating eqtypes in toplevel apis 

        exception NOT_EQ;
        exception UNBOUND_STAMP;

        # eqAnalyze is called in just one place,
        # in MacroExpand, to compute the actual
        # eqprops of types in a macro expanded api.
        #
        # It has to propagate equality properties to respect type equivalences
        # induced by sharing  constraints. 
        #
        fun eq_analyze (str, local_stamp:  sta::Stamp -> Bool, err:  err::Plaint_Sink)
            =
            {   typs  =  REF stamp_map::empty;
                depend  =  REF stamp_map::empty;
                dependr =  REF stamp_map::empty;

                equality_property     =  REF stamp_map::empty;
                depends_indeterminate =  REF FALSE;

                my tyc_stamps_ref:  Ref( List( sta::Stamp ) )
                    =
                    REF NIL;

                fun dfl_apply dfl (mr, k)
                    =
                    case (stamp_map::get (*mr, k))
                        #
                        NULL => dfl;
                        THE x => x;
                    esac;

                fun apply_map'  x   =   dfl_apply [] x;
                fun apply_map'' x   =   dfl_apply ty::eq_type::UNDEF x;

                fun update_map mr (k, v)
                    =
                    mr := stamp_map::set (*mr, k, v);

                err   =   fn s =  err err::ERROR s err::null_error_body;

                fun checkdcons ( datatyc_stamp: sta::Stamp,
                                 evalty:        ty::Type -> ty::Type,
                                 dcons:         List( ty::Constructor_Description ),
                                 stamps,
                                 members,
                                 free_typs
                               )
                               : (ty::eq_type::Data, List(sta::Stamp))
                    =
                    {   depend                =  REF ([]: List( sta::Stamp ));
                        depends_indeterminate =  REF FALSE;

                        fun member (stamp,[]) => FALSE;
                            member (st, st' ! rest) => sta::same_stamp (st, st') or member (st, rest);
                        end;

                        fun eqtyc (typ as ty::PLAIN_TYP { stamp, eqtype_info, ... } )
                                =>
                                case *eqtype_info
                                    #
                                    ty::eq_type::YES               =>  ();
                                    ty::eq_type::CHUNK             =>  ();

                                   (ty::eq_type::NO | ty::eq_type::EQ_ABSTRACT) =>  raise exception NOT_EQ;
                                   ty::eq_type::INDETERMINATE      =>  depends_indeterminate := TRUE;

                                   (ty::eq_type::DATA | ty::eq_type::UNDEF)
                                        =>
                                        if (not ( (member (stamp,*depend)) 
                                                  or
                                                  sta::same_stamp (stamp, datatyc_stamp)
                                           )    )

                                            depend :=  stamp ! *depend;
                                        fi;
                                esac;

                            eqtyc (ty::RECORD_TYP _) => ();
                            eqtyc _ => bug "eqAnalyze::eqtyc";
                        end 

                        also
                        fun eqty (ty::TYPE_VARIABLE_REF { id, ref_typevar => REF (ty::RESOLVED_TYPE_VARIABLE type) } ) 
                                =>
                                eqty type;                      # Shouldn't happen.

                            eqty (type as ty::TYPCON_TYPE (typ, args))
                                =>
                                {   ntyc = case typ
                                               #
                                               ty::FREE_TYPE i
                                                 =>
                                                 (list::nth (free_typs, i) except _ =
                                                    bug "unexpected free_typs in eqty");

                                               _ => typ;
                                           esac;

                                    case ntyc
                                        #
                                        ty::PLAIN_TYP _
                                            =>
                                            if (not (chunk_typ ntyc)) 
                                                 eqtyc ntyc;
                                                 apply eqty args;
                                            fi;

                                        ty::DEFINED_TYP { type_scheme, ... }
                                            =>
                                            eqty (tyj::head_reduce_type type);

                                        ty::RECURSIVE_TYPE i
                                            =>
                                            {  stamp = vector::get (stamps, i);

                                                my { typ_name, constructor_list, ... }
                                                    :
                                                    ty::Datatype_Member
                                                    =  
                                                    vector::get (members, i);


                                                if (   not (member (stamp,*depend))
                                                   and not (sta::same_stamp (stamp, datatyc_stamp))
                                                   )

                                                     depend := stamp ! *depend;
                                                fi;
                                            };

                                       _ => apply eqty args;
                                  esac;
                                };

                            eqty _ => ();
                        end;

                    
                        apply eqdcon dcons
                        where
                            fun eqdcon { domain => THE type',  name,  form } => eqty type';
                                eqdcon _ => ();
                            end;
                        end;

                        case (*depend, *depends_indeterminate)
                            #
                            ([], FALSE) => (ty::eq_type::YES,[]);
                            (d,  FALSE) => (ty::eq_type::DATA, d);
                            (_,  TRUE ) => (ty::eq_type::INDETERMINATE,[]);
                        esac;
                    }
                    except
                        NOT_EQ =  (ty::eq_type::NO, []);

                fun addstr (str as mld::A_PACKAGE { an_api, typechecked_package => { typerstore, ... }, ... } )
                        =>
                        {   fun addtyc (typ as (ty::PLAIN_TYP { stamp, eqtype_info, kind, path, ... } ))
                                    =>
                                    if (local_stamp stamp)        #  local spec 
                                        #
                                        {   update_map typs
                                                    (stamp, typ ! apply_map'(typs, stamp));
                                                    tyc_stamps_ref := stamp ! *tyc_stamps_ref;

                                            case kind
                                                #
                                                ty::DATATYPE { index, stamps, family=> { members, ... }, root, free_typs }
                                                    =>
                                                    {   dcons =  .constructor_list (vector::get (members, index));
                                                        #
                                                        eq_orig = *eqtype_info;

                                                        my (eqp_calc, deps)
                                                            =
                                                            case eq_orig
                                                                #
                                                                ty::eq_type::DATA
                                                                    => 
                                                                    checkdcons (stamp,
                                                                               mj::translate_type  typerstore,
                                                                               dcons, stamps, members,
                                                                               free_typs);

                                                                e => (e,[]);
                                                            esac;

                                                        #  ASSERT: e = ty::YES or ty::NO 
                                                        eq' =
                                                            join (join (eq_orig,
                                                                      apply_map''(equality_property, stamp)),
                                                                 eqp_calc);

                                                        eqtype_info :=  eq';

                                                        update_map equality_property (stamp, eq');

                                                        apply (fn s = update_map dependr (s, stamp ! apply_map'(dependr, s)))
                                                              deps;

                                                        update_map depend
                                                              (stamp, deps @ apply_map'(depend, stamp));
                                                    };

                                                (ty::FLEXIBLE_TYP _ | ty::ABSTRACT _ | ty::BASE _)
                                                    =>
                                                    {   eq' = join (apply_map''(equality_property, stamp), *eqtype_info);
                                                        #
                                                        eqtype_info :=  eq';
                                                        #
                                                        update_map equality_property (stamp, eq');
                                                    };

                                                  _ => bug "eqAnalyze::scan::tscan";
                                            esac;
                                        }
                                        except
                                            INCONSISTENT
                                                = 
                                                err "inconsistent equality properties";

                                    fi; #  external -- assume equality_property already defined 

                                addtyc _ => ();
                            end;

                            if (local_stamp (mj::get_package_stamp str))
                                list::apply (fn s => addstr s; end ) (mj::get_packages str);
                                list::apply (fn t => addtyc t; end ) (mj::get_typs str);
                                #  BUG? - why can we get away with ignoring generic elements??? XXX BUGGO FIXME 
                            fi;
                        };

                    addstr _ => ();   #  must be external or error package 
                end;

                fun propagate (eqp, depset, earlier)
                    =
                    prop
                    where
                        fun prop stamp'
                            =
                            apply (fn s
                                     =
                                     {   eqpold = apply_map''(equality_property, s);
                                         eqpnew = join (eqp, eqpold);

                                         if (eqpold != eqpnew)
                                               update_map equality_property (s, eqp);
                                               if (earlier s) prop s; fi;
                                         fi;
                                      }
                                      except
                                          INCONSISTENT
                                              =
                                              err "inconsistent equality properties B"
                                  )
                                  (depset (stamp')); 
                    end;

                #  Propagate the ty::eq_type::NO equality_property forward and the ty::YES equality_property backward 

                fun propagate_yes_no (stamp)
                    =
                    {   fun earlier s
                            =
                            sta::compare (s, stamp) == LESS;
                    
                        case (apply_map''(equality_property, stamp))
                            #                     
                            ty::eq_type::YES => propagate (ty::eq_type::YES, (fn s =  apply_map'(depend,  s)), earlier) stamp;
                            ty::eq_type::NO  => propagate (ty::eq_type::NO,  (fn s =  apply_map'(dependr, s)), earlier) stamp;
                            _   => ();
                        esac;
                    };


                #  Propagate the IND equality_property 

                fun propagate_ind (stamp)
                    =
                    {   fun depset s
                            =
                            apply_map'(dependr, s);

                        fun earlier s
                            =
                            sta::compare (s, stamp) == LESS;
                    
                        case (apply_map''(equality_property, stamp))
                            #                     
                            ty::eq_type::UNDEF
                                =>
                                {   update_map equality_property (stamp, ty::eq_type::INDETERMINATE);
                                      propagate (ty::eq_type::INDETERMINATE, depset, earlier) stamp;
                                };

                            ty::eq_type::INDETERMINATE =>
                                propagate (ty::eq_type::INDETERMINATE, depset, earlier) stamp;

                            _ => ();
                        esac;
                    };

                # Phase 0: scan api strenv, joining
                # eqprops of shared typs 
                #
                addstr str;

                tyc_stamps
                    =
                    lms::sort_list
                        (fn xy =  sta::compare xy == GREATER)
                        *tyc_stamps_ref;
             
                #  Phase 1: propagate ty::YES backwards and ty::eq_type::NO forward 
                #
                apply propagate_yes_no tyc_stamps;

                #  Phase 2: convert ty::eq_type::UNDEF to ty::eq_type::INDETERMINATE and propagate ty::eq_type::INDETERMINATEs 
                #
                apply propagate_ind tyc_stamps;

                #  Phase 3: convert ty::DATA to ty::YES; reset stored eqprops from equality_property map 
                #
                apply
                    (fn s = {   eqp = case (apply_map''(equality_property, s))
                                          ty::eq_type::DATA => ty::eq_type::YES;
                                          e => e;
                                      esac;

                                fun set (ty::PLAIN_TYP { eqtype_info, ... } )
                                        =>
                                        eqtype_info :=  eqp;

                                    set _ => ();
                                end;

                                apply set (apply_map'(typs, s)); 
                            }
                    )
                    tyc_stamps;
            };

        exception CHECKEQ;


        # WARNING - defineEqTyp uses eq field REF as a typ identifier.  
        # Since defineEqTyp is called only within type_datatype_declaration, this
        # should be ok.

        void_type = type_types::void_type;

        fun member (_,[])
                =>
                FALSE;

            member (i: Int, j ! rest)
                =>
                i == j   or
                member (i, rest);
        end;

        fun names_to_string ([]: List( symbol::Symbol ))
                =>
                "[]";

            names_to_string (x ! xs)
                =>
                string::cat ("["
                              ! (symbol::name x)
                              ! fold_forward (fn (y, l) = ", " ! (symbol::name y) ! l)    ["]"]    xs
                            );
        end;

        fun define_eq_props (datatyps, api_context, api_typerstore)
            = 
            {   names =   map tyj::typ_name datatyps;

                if_debugging_say (">>defineEqProps: "  +  names_to_string  names);

                n = list::length datatyps;

                my { family => { members, ... },   free_typs, ... }
                    =
                    case (list::head  datatyps)
                        #
                        ty::PLAIN_TYP { kind => ty::DATATYPE x, ... }
                            =>
                            x;

                        _ => bug "defineEqProps (list::head datatyps)";
                    esac;

                eqs = map  get  datatyps
                      where
                          fun get (ty::PLAIN_TYP { eqtype_info, ... } ) => eqtype_info;
                              get _ => bug "eqs: get";
                          end;
                      end;

                fun get_eq i
                    = 
                    *(list::nth (eqs, i))
                    except
                        (SUBSCRIPT | INDEX_OUT_OF_BOUNDS)
                            =
                            {   say "@@@getEq ";
                                say (int::to_string i);
                                say " from ";
                                say (int::to_string (length eqs));
                                say "\n";
                                raise exception SUBSCRIPT;
                            };


                fun set_eq (i, eqp)
                    =
                    {   if_debugging_say (string::cat ["setEq: ", int::to_string i, " ",
                                         tyj::equality_property_to_string eqp]);

                        (list::nth (eqs, i) := eqp)
                        except
                            (SUBSCRIPT | INDEX_OUT_OF_BOUNDS)
                                =
                                {   say (string::cat ["@@@setEq ", (int::to_string i), " from ",
                                        (int::to_string (length eqs)), "\n"]);

                                    raise exception SUBSCRIPT;
                                };
                    };

                visited = REF ([]: List( Int ));

                fun check_typ (typ0 as ty::PLAIN_TYP { eqtype_info, kind, path, ... } )
                     =>
                     case (*eqtype_info, kind)
                        #
                        (ty::eq_type::DATA, ty::DATATYPE { index, ... } )
                            =>
                            {   if_debugging_say (">>check_typ: " +
                                                  symbol::name (ip::last path) + " " +
                                                  int::to_string index);

                                fun eqtyc (ty::PLAIN_TYP { eqtype_info => e', kind => k', path, ... } )
                                        =>
                                        case (*e', k')
                                            #
                                            (ty::eq_type::DATA, ty::DATATYPE { index, ... } )
                                                =>
                                                {   if_debugging_say ("eqtyc[ty::PLAIN_TYP (ty::DATA)]: " +
                                                           symbol::name (ip::last path) +
                                                           " " + int::to_string index);

                                                    #  ASSERT: argument typ is a member of datatyps 

                                                    check_domains index;
                                                };

                                            (ty::eq_type::UNDEF, _)
                                                =>
                                                {   if_debugging_say ("eqtyc[ty::PLAIN_TYP (ty::eq_type::UNDEF)]: " +
                                                           symbol::name (ip::last path));

                                                    ty::eq_type::INDETERMINATE;
                                                };

                                            (eqp, _)
                                                =>
                                                {   if_debugging_say ("eqtyc[ty::PLAIN_TYP(_)]: " +
                                                           symbol::name (ip::last path) +
                                                           " " + tyj::equality_property_to_string eqp);

                                                    eqp;
                                                };
                                        esac;

                                    eqtyc (ty::RECURSIVE_TYPE i)
                                        => 
                                        {   if_debugging_say ("eqtyc[ty::RECURSIVE_TYPE]: " + int::to_string i);
                                            #
                                            check_domains i;
                                        };

                                    eqtyc (ty::RECORD_TYP _)  => ty::eq_type::YES;
                                    eqtyc (ty::ERRONEOUS_TYP) => ty::eq_type::INDETERMINATE;
                                    eqtyc (ty::FREE_TYPE i) => bug "eqtyc - ty::FREE_TYPE";
                                    eqtyc (ty::TYP_BY_STAMPPATH _) => bug "eqtyc - ty::TYP_BY_STAMPPATH";
                                    eqtyc (ty::DEFINED_TYP _) => bug "eqtyc - ty::DEFINED_TYP";
                                end 

                                also
                                fun check_domains i
                                    =
                                    if (member (i, *visited))

                                        get_eq i;
                                    else
                                        visited := i ! *visited;

                                        my { typ_name, constructor_list, ... }:   ty::Datatype_Member
                                            =
                                            vector::get (members, i)
                                            except
                                                (SUBSCRIPT | INDEX_OUT_OF_BOUNDS)
                                                =
                                                {   say (string::cat
                                                          ["@@@getting member ",
                                                           int::to_string i,
                                                           " from ",
                                                           int::to_string (vector::length members), "\n"]);

                                                    raise exception SUBSCRIPT;
                                                };

                                        if_debugging_say (
                                                    "checkDomains: visiting "
                                                  + symbol::name typ_name
                                                  + " "
                                                  + int::to_string i
                                                );

                                        domains
                                            = 
                                            map fn { domain=>THE type, name, form } =>        type;
                                                   { domain=>NULL,     name, form } =>   void_type;
                                                end
                                                constructor_list;

                                        eqp = eqtylist (domains);

                                        set_eq (i, eqp);

                                        if_debugging_say
                                          (
                                              "checkDomains: setting "
                                            + int::to_string i
                                            + " to "
                                            + tyj::equality_property_to_string eqp
                                          );

                                        eqp;
                                    fi

                                also
                                fun eqty (ty::TYPE_VARIABLE_REF { id, ref_typevar => REF (ty::RESOLVED_TYPE_VARIABLE type) } )
                                        =>
                                        #  shouldn't happen 
                                        eqty type;

                                    eqty (ty::TYPCON_TYPE (typ, args))
                                        =>
                                        case (expand_typ::expand_typ ( typ, api_context, api_typerstore))
                                            #
                                            ty::FREE_TYPE i
                                                =>
                                                {   if_debugging_say ("eqtyc[ty::FREE_TYPE]: " + int::to_string i);

                                                    tc = (list::nth (free_typs, i)
                                                              except _ =
                                                                     bug "unexpected free_typs 343");

                                                    eqty (ty::TYPCON_TYPE (tc, args));
                                                };

                                            ty::DEFINED_TYP { type_scheme, ... }
                                                =>
                                                # shouldn't happen - type abbrevs in domains
                                                # should have been expanded
                                                eqty (tyj::apply_type_scheme (type_scheme, args));

                                            typ
                                                => 
                                                case (eqtyc typ)

                                                    ( ty::eq_type::NO
                                                    | ty::eq_type::EQ_ABSTRACT
                                                    )          =>  ty::eq_type::NO;

                                                    ty::eq_type::CHUNK     =>  ty::eq_type::YES;
                                                    ty::eq_type::YES       =>  eqtylist args;

                                                    ty::eq_type::DATA => case (eqtylist args)
                                                                    #
                                                                    ty::eq_type::YES =>  ty::eq_type::DATA;
                                                                    e          =>  e;
                                                                esac;

                                                    ty::eq_type::INDETERMINATE => ty::eq_type::INDETERMINATE;

                                                    ty::eq_type::UNDEF
                                                        => 
                                                        bug ("defineEqTyp::eqty: ty::eq_type::UNDEF - " + symbol::name (tyj::typ_name typ));
                                                esac;
                                        esac;

                                    eqty _ => ty::eq_type::YES;
                                end 

                                also
                                fun eqtylist tys
                                    =
                                    loop (tys, ty::eq_type::YES)
                                    where
                                        fun loop ([], eqp)
                                                =>
                                                eqp;

                                            loop (type ! rest, eqp)
                                                =>
                                                case (eqty type)
                                                    #
                                                    ( ty::eq_type::NO
                                                    | ty::eq_type::EQ_ABSTRACT
                                                    )    => ty::eq_type::NO;                    # Return ty::NO immediately; no further checking.

                                                    ty::eq_type::YES           => loop (rest, eqp);
                                                    ty::eq_type::INDETERMINATE => loop (rest, ty::eq_type::INDETERMINATE);

                                                    ty::eq_type::DATA => case eqp
                                                                    ty::eq_type::INDETERMINATE => loop (rest, ty::eq_type::INDETERMINATE);
                                                                    _             => loop (rest, ty::eq_type::DATA         );
                                                                esac;

                                                    _ => bug "defineEqTyp::eqtylist";
                                                esac;
                                        end;
                                    end;


                                case (eqtyc typ0)
                                    #
                                    ty::eq_type::YES => apply (fn i = case (get_eq i)
                                                                 ty::eq_type::DATA => set_eq (i, ty::eq_type::YES);
                                                                 _    => ();
                                                             esac
                                                     )

                                                 *visited;

                                    ty::eq_type::DATA => apply (fn i = case (get_eq i)
                                                                  ty::eq_type::DATA => set_eq (i, ty::eq_type::YES);
                                                                  _ => ();
                                                              esac
                                                  )

                                                  *visited;

                                    ty::eq_type::NO => apply (fn i = if (i > index)
                                                             case (get_eq i)
                                                                 ty::eq_type::INDETERMINATE => set_eq (i, ty::eq_type::DATA);
                                                                _ => ();
                                                             esac;
                                                        fi
                                                )

                                               *visited;

                                    # Have to be reanalyzed, throwing away information ???  XXX BUGGO FIXME
                                    #
                                    ty::eq_type::INDETERMINATE =>  ();
                                    _             =>  bug "defineEqTyp";

                                esac;

                                #  ASSERT: equality_property of typeconstructor0 is ty::eq_type::YES, ty::eq_type::NO, or ty::eq_type::INDETERMINATE 
                                #       
                                case *eqtype_info
                                    #
                                    (ty::eq_type::YES | ty::eq_type::NO | ty::eq_type::INDETERMINATE) =>   ();
                                    #
                                    ty::eq_type::DATA =>   bug ("checkTypeConstructor[=>ty::eq_type::DATA]: " + symbol::name (ip::last path));
                                    _           =>   bug ("checkTypeConstructor[=>other]: " + symbol::name (ip::last path));
                                esac;
                            };
                        #
                        _ => ();
                    esac;

                    check_typ _ => ();
                end;
            
                list::apply check_typ datatyps;
            };

        fun is_equality_type type
            =
            {   fun eqty (ty::TYPE_VARIABLE_REF { id, ref_typevar => REF (ty::RESOLVED_TYPE_VARIABLE type) } )
                        =>
                        eqty type;

                    eqty (ty::TYPE_VARIABLE_REF { id, ref_typevar => REF (ty::META_TYPE_VARIABLE { eq, ... } ) } )
                        =>
                        if eq  ();
                        else   raise exception CHECKEQ;
                        fi;

                    eqty (ty::TYPE_VARIABLE_REF { id, ref_typevar => REF (ty::INCOMPLETE_RECORD_TYPE_VARIABLE { eq, ... } ) } )
                        =>
                        if eq  ();
                        else   raise exception CHECKEQ;
                        fi;

                    eqty (ty::TYPCON_TYPE (ty::DEFINED_TYP { type_scheme, ... }, args))
                        =>
                        eqty (tyj::apply_type_scheme (type_scheme, args));

                    eqty (ty::TYPCON_TYPE (ty::PLAIN_TYP { eqtype_info, ... }, args))
                        =>
                        case *eqtype_info
                            #
                            ty::eq_type::CHUNK => ();
                            ty::eq_type::YES   => apply eqty args;
                            (ty::eq_type::NO | ty::eq_type::EQ_ABSTRACT | ty::eq_type::INDETERMINATE) => raise exception CHECKEQ;
                            _ => bug "isEqType";
                        esac;

                    eqty (ty::TYPCON_TYPE (ty::RECORD_TYP _, args))
                        =>
                        apply eqty args;

                    eqty _ => ();
                end;
            
                eqty type;
                TRUE;
            }
            except
                CHECKEQ = FALSE;

        fun check_eq_ty_sig
              ( type,
                an_api:   ty::Type_Scheme_Arg_Eq_Properties
              )
            =
            {   fun eqty (ty::TYPE_VARIABLE_REF { id, ref_typevar => REF (ty::RESOLVED_TYPE_VARIABLE type) } )
                        =>
                        eqty type;

                    eqty (ty::TYPCON_TYPE (ty::DEFINED_TYP { type_scheme, ... }, args))
                        =>
                        eqty (tyj::apply_type_scheme (type_scheme, args));

                    eqty (ty::TYPCON_TYPE (ty::PLAIN_TYP { eqtype_info, ... }, args))
                        =>
                        case *eqtype_info
                            #
                            ty::eq_type::CHUNK => ();
                            ty::eq_type::YES => apply eqty args;
                            (ty::eq_type::NO | ty::eq_type::EQ_ABSTRACT | ty::eq_type::INDETERMINATE) => raise exception CHECKEQ;
                            _ => bug "checkEqTySig";
                        esac;

                    eqty (ty::TYPE_SCHEME_ARG_I n)
                        => 
                        {   eq = list::nth (an_api, n);
                            #   
                            if (not eq)   raise exception CHECKEQ;   fi;
                        };

                    eqty _ => ();
                end;
            
                eqty type;
                TRUE;
            }
            except
                CHECKEQ = FALSE;

        fun replicate (0, x)  =>  NIL;
            replicate (i, x)  =>  x ! replicate (i - 1, x);
        end;

        fun is_equality_typ (ty::PLAIN_TYP { eqtype_info, ... } )
                =>
                case *eqtype_info
                    #
                    ty::eq_type::YES   => TRUE;
                    ty::eq_type::CHUNK => TRUE;
                    _             => FALSE;
                esac;

            is_equality_typ (ty::DEFINED_TYP { type_scheme as ty::TYPE_SCHEME { arity, ... }, ... } )
                =>
                is_equality_type (tyj::apply_type_scheme (type_scheme, replicate (arity, type_types::int_type)));

            is_equality_typ _
                =>
                bug "is_equality_typ";
        end;
    };                                                                                          # package eq_types 
end;                                                                                            # stipulate




Comments and suggestions to: bugs@mythryl.org

PreviousUpNext