types.spad

)abbrev domain MTYPE MType
++ Author: Martin Baker
++ Date Created: April 2014
++ Date Last Updated: April 2014
++ Description:
++   MType stands for 'matchable type'. The intention is to be
++   able to represent types in a way that is more powerful than
++   the existing FriCAS types.
++   So this is 'lifted', that is, values in this domain represent
++   types.
++   I want to be able to have type variables and to use
++   type constructors in a more flexible way.
++   The original reason for writing this is that I needed to
++   represent types in a SPAD version of the interpreter that I
++   am working on. In this interpreter it is used by TypeMatcher
++   to hold type information.
++
++   I have put information about representing types and the
++   design of this code here:
++ http://www.euclideanspace.com/prog/scratchpad/mycode/discrete/type/
++   I have put specific information about type matcher here:
++ http://www.euclideanspace.com/prog/scratchpad/mycode/system/interpreter/typematch/

MType : Exports == Implementation where
  NNI==> NonNegativeInteger
  TOKENTYPE ==> Symbol
    ++ valid token types are:
    ++id: Symbol
    ++key: Symbol
    ++integer: Symbol
    ++rinteger: Symbol
    ++float: Symbol
    ++string: Symbol
    ++comment: Symbol
    ++negcomment: Symbol
    ++error: Symbol
    ++spaces: Symbol
  TOKEN ==> Record(tt:TOKENTYPE,tokVal:String)
  TYPEDVALUE ==> Record(tt:TOKENTYPE,tokVal:String)

  Exports == Join(Ring,ConvertibleTo(Pattern(MType)),_
      PatternMatchable(MType),Comparable) with

    typeConstruct:(bas:Symbol) -> %
      ++ constructor to construct integer,float,symbol,string,etc.

    typeConstruct:(bas:Symbol,parameters:List %) -> %
      ++ constructor for compound type
      
    zero?:(n:%) -> Boolean
    one?:(n:%) -> Boolean
    getBase:(n:%) -> Symbol

  Implementation ==> add

    import Pattern(MType)
    import PatternMatchable(MType)
    import PatternMatchResult(MType,PatternMatchable(MType))

    Rep := Record(sym:Symbol,par:List(%))
      ++ type is one of:
      ++ Symbol
      ++ Integer
      ++ Float
      ++ String
      ++ Boolean
      ++ other domain name
      ++ Record[%]
      ++ Union[%]
      ++ Function[%]

    -- constructor to construct integer,float,symbol,string,etc.
    typeConstruct(bas:Symbol):% ==
      [bas,empty()$List(%)]

    -- constructor for compound type
    typeConstruct(bas:Symbol,parameters:List %):% ==
      [bas,parameters]
      
    getBase(n:%) == n.sym

    zero?(n:%):Boolean ==
     n.sym = "NONE"::Symbol

    one?(n:%):Boolean ==
     n.sym = "ANY"::Symbol
    
    -- returns true if they have the same values
    x = y ==
      if x.sym ~= y.sym then return false
      if x.par ~= y.par then return false
      true

    0 == typeConstruct("NONE"::Symbol)
    1 == typeConstruct("ANY"::Symbol)
    x + y == typeConstruct("UNION"::Symbol,[x,y])
    x - y == typeConstruct("ERROR"::Symbol,[x,y])
    _*(x:Integer,y:%):% == typeConstruct("ERROR"::Symbol,[y])
    _*(x:PositiveInteger,y:%):% == typeConstruct("ERROR"::Symbol,[y])
    x * y == typeConstruct("RECORD"::Symbol,[x,y])
    _-(x:%):% == typeConstruct("ERROR"::Symbol)

    -- Required to implement Comparable which is needed
    -- to implement Expression(MType)
    -- This implies that MType has a total order
    -- but inheritance only gives a partial order.
    smaller?(x:%,y:%):Boolean ==
      false

    -- Required to implement category PatternMatchable(MType)
    -- A set R is PatternMatchable over MType if elements
    -- of R can be matched to patterns over MType.
    --
    -- patternMatch(expr, pat, res) matches the pattern pat to the
    -- expression expr. res contains the variables of pat which
    -- are already matched and their matches (necessary for recursion).
    -- Initially, res is just the result of new
    -- which is an empty list of matches.
    patternMatch(expr:%,pat:Pattern(MType),_
                      res:PatternMatchResult(MType,%)):_
                      PatternMatchResult(MType,%) ==
      mathprint("MType patternMatch")$Lisp
      res

    -- required to implement category ConvertibleTo(Pattern(MType))
    convert(x : %): Pattern(MType)==
      ty := "Type"::Symbol
      ty::Pattern(MType)

    hash(n: %):SingleInteger ==
      0::SingleInteger

    coerce(n: %):OutputForm ==
      if empty?(n.par) then return n.sym::OutputForm
      params:List OutputForm := [x::OutputForm for x in n.par]
      commaparams:OutputForm := commaSeparate(params)$OutputForm
      hconcat([n.sym::OutputForm,"("::OutputForm,_
                 commaparams,")"::OutputForm])$OutputForm
@

)abbrev domain MEXPR MTypeExpression
++ Type expressions
++   I have put information about representing types and the
++   design of this code here:
++ http://www.euclideanspace.com/prog/scratchpad/mycode/discrete/type/
++   I have put specific information about type matcher here:
++ http://www.euclideanspace.com/prog/scratchpad/mycode/system/interpreter/typematch/
MTypeExpression(R:Comparable) : Exports == Implementation where
  K   ==> Kernel %
  MP  ==> SparseMultivariatePolynomial(MType, K)

  Exports ==> Join(FunctionSpace(R),ConvertibleTo(Pattern(MType)),_
      PatternMatchable(MType)) with

    --coerce:(n: MType) -> %
    coerce:(n: R) -> %
      ++ or should this be coerce:(n:R) -> %
    coerce:(sy:Symbol) -> %
      ++ sy represents variable
    coerce:(spmp:SparseMultivariatePolynomial(R, K)) -> %
      ++ R is usually MType

  --Implementation ==> Expression(R) add
  Implementation ==> add

    import MType
    import Pattern(MType)
    import PatternMatchable(MType)
    import PatternMatchResult(MType,PatternMatchable(MType))
    -- KernelFunctions2 required for constantKernel
    import KernelFunctions2(R, %)
    
    Rep := MP
    0 == 0$Rep
    1 == 1$Rep
    - x : % == -$Rep x
    n:Integer *x:% == n*$Rep x
    x:% * y:% == x *$Rep y
    x:% + y:% == x +$Rep y
    x:% = y:% == x =$Rep y

    if R is MType then
      numer(x:%):SparseMultivariatePolynomial(R, K) ==
        x pretend SparseMultivariatePolynomial(R, K)
 
    -- Required to implement category PatternMatchable(MType)
    -- A set R is PatternMatchable over MType if elements
    -- of R can be matched to patterns over MType.
    --
    -- patternMatch(expr, pat, res) matches the pattern pat to the
    -- expression expr. res contains the variables of pat which
    -- are already matched and their matches (necessary for recursion).
    -- Initially, res is just the result of new
    -- which is an empty list of matches.
    patternMatch(expr:%,pat:Pattern(MType),_
                      res:PatternMatchResult(MType,%)):_
                      PatternMatchResult(MType,%) ==
      mathprint("MTypeExpression patternMatch pat=")$Lisp
      print(pat::OutputForm)
      mathprint("MTypeExpression patternMatch res=")$Lisp
      print(res::OutputForm)
      res

    -- required to implement category ConvertibleTo(Pattern(MType))
    convert(x : %): Pattern(MType)==
      mathprint("MTypeExpression convert to pattern")$Lisp
      ty := "Type"::Symbol
      ty::Pattern(MType)

    -- coerce SparseMultivariatePolynomial(R, K)
    -- to % which is SparseMultivariatePolynomial(MType, K)
    -- R is usually MType so just pretend
    coerce(spmp:SparseMultivariatePolynomial(R, K)):% ==
      spmp pretend %

    -- coerce symbol, representing a variable, to
    -- MTypeExpression(MType)
    coerce(sy:Symbol):% ==
      kernel(sy)@K :: %

    -- coerce MType to MTypeExpression(MType)
    -- rep is of Expression in ring is SparseMultivariatePolynomial(R,K)
    -- which is Union of MType or variable
    if R is MType then
      coerce(constant: R):% ==
        zero?(constant) => 0$Rep
        one?(constant) => 1$Rep
        -- constantKernel defined in KernelFunctions2
        -- as kernel(constantOperator r, nil(), 1)
        -- this produces continous random output
        -- even when coerce to output form turned off
        --constantKernel(constant)::%
        --
        -- If the following is enabled then everthing is
        -- MType and coerce to OutputForm is not even called
        -- for this MTypeExpression
        --coerce(constant)$MP
        coerce(getBase(constant))$Expression(MType) pretend %
    else
      coerce(constant: R):% ==
        0

    -- output
    if R is MType then
      coerce(x : %):OutputForm ==
        x1:MP := x pretend MP
        D := SparseUnivariatePolynomial(%)
        VPoly := Record(v : R, ts : D)
        --VarSet is an instance of OrderedSet
        MPREP := Union(single:R,mult:VPoly)
        x2:MPREP := x1 pretend MPREP
        --return x1::OutputForm
        x2 case single => (x2.single)::OutputForm
        vp:VPoly := x2.mult
        v1:R := vp.v
        ts1:D := vp.ts
        s:String := (mathObject2String$Lisp v1)@String
        mathprint("MTypeExpression output "s)$Lisp
        -- the following fails - although v1 is MType
        -- it really sometimes seems to be an expression?
        --opf:OutputForm := v1::OutputForm
        --outputForm(ts1,opf)$D
        coerce(x1)$MP
        --"x"::OutputForm
    else
      coerce(x : %):OutputForm ==
        mathprint("MTypeExpression not MType output")$Lisp
        coerce(x pretend Expression(R))$Expression(R)
@

)abbrev package TESTR TestRule
++ Author: Martin Baker
++ Date Created: April 2014
++ Date Last Updated: April 2014
++ Description:
++   I can't work out how to do this from the interprester
++   so I have compiled the test here.
++   I have put information about representing types and the
++   design of this code here:
++ http://www.euclideanspace.com/prog/scratchpad/mycode/discrete/type/
++   I have put specific information about type matcher here:
++ http://www.euclideanspace.com/prog/scratchpad/mycode/system/interpreter/typematch/
TestRule() : Target == Implementation where
  Target ==> with
    testRule:() -> RewriteRule(MType,MType,MTypeExpression(MType))
    testExpression:() -> MTypeExpression(MType)
    testApply:(RewriteRule(MType,MType,MTypeExpression(MType)),_
         MTypeExpression(MType)) -> MTypeExpression(MType)

  Implementation ==> add
    import MType
    import Pattern(MType)
    import PatternMatchable(MType)
    import PatternMatchResult(MType,PatternMatchable(MType))
    import MTypeExpression(MType)

    -- test
    testRule(): RewriteRule(MType,MType,MTypeExpression(MType))==
      a1:MType := typeConstruct("Integer"::Symbol)
      a:=a1::MTypeExpression(MType)
      b1:MType := typeConstruct("Float"::Symbol)
      b:=b1::MTypeExpression(MType)
      rule(a,b)$RewriteRule(MType,MType,MTypeExpression(MType))

    testExpression():MTypeExpression(MType)==
      a1:MType := typeConstruct("Integer"::Symbol)
      a1::MTypeExpression(MType)

    testApply(rr:RewriteRule(MType,MType,MTypeExpression(MType)),_
              ex:MTypeExpression(MType)): MTypeExpression(MType)==
      applyRules([rr],ex)$ApplyRules(MType,MType,MTypeExpression(MType))
@