Re: [open-axiom-devel] add 'is' operator to conditional categories declarations

[Gabriel D. R. <gd...@in...>]

On Thu, Jul 17, 2008 at 9:49 PM, Yixin Cao
<ch...@us...> wrote:
> With this patch, categories can be declared conditionally with 'is'
> operator, e.g.
>
> Fake(T:Type, a:T): Public == Private where
>   Public == CoercibleTo OutputForm with
>     if T is Integer and a is 10 then CommutativeRing
>     if T is Matrix(Integer) then leftUnitary
>
>
>
> Index: functor.boot
> ===================================================================
> --- functor.boot        (revision 289)
> +++ functor.boot        (working copy)
> @@ -887,6 +887,7 @@
>
>  ICformat u ==
>        atom u => u
> +      u is ['is,a,b] => compIsFormat u
>        u is ['has,:.] => compHasFormat u
>        u is ['AND,:l] or u is ['and,:l] =>
>          l:= REMDUP [ICformat v for [v,:l'] in tails l | not member(v,l')]
> Index: nrunopt.boot
> ===================================================================
> --- nrunopt.boot        (revision 289)
> +++ nrunopt.boot        (working copy)
> @@ -299,6 +299,7 @@
>    op := QCAR x
>    MEMQ(op,'(HasCategory HasAttribute)) => x
>    EQ(op,'has) => compHasFormat x
> +  x is ['is,a,b] => compIsFormat x
>    [transHasCode y for y in x]
>
>  mungeAddGensyms(u,gal) ==
> Index: info.boot
> ===================================================================
> --- info.boot   (revision 289)
> +++ info.boot   (working copy)
> @@ -117,6 +117,7 @@
>      b is ["ATTRIBUTE",.] => u
>      b is ["SIGNATURE",:.] => u
>      ["has",a,["ATTRIBUTE",b]]
> +  u is ["is",a,b] => u
>    atom u => u
>    u is ["and",:v] => ["and",:[formatPred w for w in v]]
>    systemError '"formatPred"
> @@ -196,6 +197,10 @@
>  -- this is wrong TPD feb, 19, 2003
>      -- or/[AncestorP(cat,LIST CAR u) and knownInfo CADR u for u in CADR
> catlist] => true
>      false
> +  pred is ["is",name,value] =>
> +    name = value => true
> +    compForMode(name,$EmptyMode,$e)
> +    false
>    pred is ["SIGNATURE",name,op,sig,:.] =>
>      v:= get(op,"modemap",$e)
>      for w in v repeat
> @@ -272,6 +277,7 @@
>        $e:= put(name,"value",[vval,mkJoin(cat,vmode),venv],$e)
>      SAY("extension of ",vval," to ",cat," ignored")
>      $e
> +  u is ["is",name,value] => $e
>    systemError '"knownInfo"
>
>  mkJoin(cat,mode) ==
> Index: br-op1.boot
> ===================================================================
> --- br-op1.boot (revision 289)
> +++ br-op1.boot (working copy)
> @@ -977,6 +977,7 @@
>          [arg,p] := argl
>          p is ['ATTRIBUTE,a] => ['HasAttribute,arg,MKQ a]
>          ['HasCategory,arg,convertCatArg p]
> +      op = 'is => ['EQUAL, :argl]
>        systemError '"unknown predicate form"
>      pred = 'T => true
>      systemError nil
> Index: compiler.boot
> ===================================================================
> --- compiler.boot    (revision 289)
> +++ compiler.boot    (working copy)
> @@ -1028,6 +1059,14 @@
>    isDomainForm(b,$EmptyEnvironment) => ["EQUAL",a,b]
>    ["HasCategory",a,mkDomainConstructor b]
>
> +compIsFormat (pred is ["is",olda,b]) ==
> +  argl := rest $form
> +  formals := TAKE(#argl,$FormalMapVariableList)
> +  a := SUBLISLIS(argl,formals,olda)
> +  [a,:.] := comp(a,$EmptyMode,$e) or return nil
> +  a := SUBLISLIS(formals,argl,a)
> +  ["EQUAL",a,b]
> +
>  ++ Check whether the modemaps have specific properties.
>  compHasAlgebra (pred is ["has",a,b],m,e) ==
>    e:=addDomain(['Operation1, ['Integer], a], e)
>

I do not understand why this is correct.  And I believe I already
asked the same very question.

-- Gaby