login  home  contents  what's new  discussion  bug reports     help  links  subscribe  changes  refresh  edit
SandBox
AWAIC  ← ↑ →  DependentTypeTest2

DependentTypeTest1
  
last edited 2 years ago by pagani

Edit detail for DependentTypeTest1 revision 1 of 1
1
Editor: pagani
Time: 2022/09/01 14:53:45 GMT+0
Note: 
changed:
-
\begin{spad}
)abbrev category ACAT A_Categeroy
A_Categeroy() : Category == SetCategory with
  degree : % -> Polynomial Integer 
        
)abbrev domain BDOM B
B(p) : Exports == Implementation where 
  p : Polynomial Integer
  BOP ==> BasicOperator 
  ACAT ==> A_Categeroy
  Exports == A_Categeroy with
    coerce : Symbol -> %  
  Implementation == BOP add 
    Rep := BOP  
    coerce(s:Symbol):% == operator s
    degree x == p
  

)abbrev domain CDOM C
C(a,b) : Exports == Implementation where 
  ACAT ==> A_Categeroy
  OF ==> OutputForm
  a:ACAT
  b:ACAT 
  PINT ==> Polynomial Integer
  Exports == ACAT with
    _* : (a,b) -> %   
  Implementation == add 
    Rep := Record(left:a,right:b)   
    x * y == [x,y]@Rep
    degree x == degree(x.left)$a + degree(x.right)$b
    coerce(x:%):OutputForm == tensor(x.left::OF,x.right::OF)
  

)abbrev domain DDOM D
D(a) : Exports == Implementation where 
  ACAT ==> A_Categeroy
  OF ==> OutputForm
  a:ACAT
  PINT ==> Polynomial Integer
  Exports == ACAT with
    d : % -> B(r)
    d : a -> %   
  Implementation == add 
    Rep := Record(arg:a) 
    r:PINT
    NullForm:B(r):="NULL"::Symbol::B(r)
    d(x:%): B(r) == NullForm 
    d(x:a):% == [x]@Rep
    degree x == 1 + degree(x.arg)$a 
    coerce(x:%):OutputForm == 
      hconcat(outputForm("d"::Symbol)$OF,bracket(x.arg::OF))
\end{spad}

\begin{axiom}
a:=a::B(p)
b:=b::B(q)
c:=c::B(99)
o:=o::B(0)

test(degree a = p)
test(degree o = 0)

r := a*b
s := c*o

degree r
degree s
degree (r*s)

d r
d (r*c)
a* d (b*a*b)
degree % 
d r*d a
d %
degree %

-- r=0 -> :(

d d r
\end{axiom}

fricas
(1) -> <spad>
fricas
)abbrev category ACAT A_Categeroy
A_Categeroy() : Category == SetCategory with
  degree : % -> Polynomial Integer
fricas
)abbrev domain BDOM B
B(p) : Exports == Implementation where 
  p : Polynomial Integer
  BOP ==> BasicOperator 
  ACAT ==> A_Categeroy
  Exports == A_Categeroy with
    coerce : Symbol -> %  
  Implementation == BOP add 
    Rep := BOP  
    coerce(s:Symbol):% == operator s
    degree x == p
fricas
)abbrev domain CDOM C
C(a,b) : Exports == Implementation where 
  ACAT ==> A_Categeroy
  OF ==> OutputForm
  a:ACAT
  b:ACAT 
  PINT ==> Polynomial Integer
  Exports == ACAT with
    _* : (a,b) -> %   
  Implementation == add 
    Rep := Record(left:a,right:b)   
    x * y == [x,y]@Rep
    degree x == degree(x.left)$a + degree(x.right)$b
    coerce(x:%):OutputForm == tensor(x.left::OF,x.right::OF)
fricas
)abbrev domain DDOM D
D(a) : Exports == Implementation where 
  ACAT ==> A_Categeroy
  OF ==> OutputForm
  a:ACAT
  PINT ==> Polynomial Integer
  Exports == ACAT with
    d : % -> B(r)
    d : a -> %   
  Implementation == add 
    Rep := Record(arg:a) 
    r:PINT
    NullForm:B(r):="NULL"::Symbol::B(r)
    d(x:%): B(r) == NullForm 
    d(x:a):% == [x]@Rep
    degree x == 1 + degree(x.arg)$a 
    coerce(x:%):OutputForm == 
      hconcat(outputForm("d"::Symbol)$OF,bracket(x.arg::OF))</spad>
fricas
Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/46105402477848525-25px001.spad
      using old system compiler.
   ACAT abbreviates category A_Categeroy 
------------------------------------------------------------------------
   initializing NRLIB ACAT for A_Categeroy 
   compiling into NRLIB ACAT 

;;;     ***       |A_Categeroy| REDEFINED
Time: 0 SEC.

   finalizing NRLIB ACAT 
   Processing A_Categeroy for Browser database:
--->-->A_Categeroy(constructor): Not documented!!!!
--->-->A_Categeroy((degree ((Polynomial (Integer)) %))): Not documented!!!!
--->-->A_Categeroy(): Missing Description
; compiling file "/var/aw/var/LatexWiki/ACAT.NRLIB/ACAT.lsp" (written 01 SEP 2022 02:53:46 PM):

; /var/aw/var/LatexWiki/ACAT.NRLIB/ACAT.fasl written
; compilation finished in 0:00:00.004
------------------------------------------------------------------------
   A_Categeroy is now explicitly exposed in frame initial 
   A_Categeroy will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/ACAT.NRLIB/ACAT

   BDOM abbreviates domain B 
------------------------------------------------------------------------
   initializing NRLIB BDOM for B 
   compiling into NRLIB BDOM 
   compiling exported coerce : Symbol -> $
Time: 0.01 SEC.

   compiling exported degree : $ -> Polynomial Integer
Time: 0.03 SEC.

(time taken in buildFunctor:  0)

;;;     ***       B REDEFINED

;;;     ***       B REDEFINED
Time: 0 SEC.

   Cumulative Statistics for Constructor B
      Time: 0.04 seconds

--------------non extending category----------------------
.. B(#1) of cat 
(|Join| (|A_Categeroy|) (CATEGORY |domain| (SIGNATURE |coerce| ($ (|Symbol|)))))   has no 
(|OrderedSet|)    finalizing NRLIB BDOM 
   Processing B for Browser database:
--->-->B(constructor): Not documented!!!!
--->-->B((coerce (% (Symbol)))): Not documented!!!!
--->-->B(): Missing Description
; compiling file "/var/aw/var/LatexWiki/BDOM.NRLIB/BDOM.lsp" (written 01 SEP 2022 02:53:46 PM):

; /var/aw/var/LatexWiki/BDOM.NRLIB/BDOM.fasl written
; compilation finished in 0:00:00.028
------------------------------------------------------------------------
   B is now explicitly exposed in frame initial 
   B will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/BDOM.NRLIB/BDOM

   CDOM abbreviates domain C 
------------------------------------------------------------------------
   initializing NRLIB CDOM for C 
   compiling into NRLIB CDOM 
Local variable Rep type redefined: (Join (SetCategory) (CATEGORY domain (SIGNATURE construct ((Record (: left a) (: right b)) a b)) (SIGNATURE ~= ((Boolean) (Record (: left a) (: right b)) (Record (: left a) (: right b)))) (SIGNATURE coerce ((OutputForm) (Record (: left a) (: right b)))) (SIGNATURE elt (a (Record (: left a) (: right b)) left)) (SIGNATURE elt (b (Record (: left a) (: right b)) right)) (SIGNATURE setelt! (a (Record (: left a) (: right b)) left a)) (SIGNATURE setelt! (b (Record (: left a) (: right b)) right b)) (SIGNATURE copy ((Record (: left a) (: right b)) (Record (: left a) (: right b)))))) to (Join (OrderedSet) (CATEGORY domain (SIGNATURE name ((Symbol) $)) (SIGNATURE properties ((AssociationList (Symbol) (None)) $)) (SIGNATURE copy ($ $)) (SIGNATURE operator ($ (Symbol))) (SIGNATURE operator ($ (Symbol) (NonNegativeInteger))) (SIGNATURE arity ((Union (NonNegativeInteger) failed) $)) (SIGNATURE nullary? ((Boolean) $)) (SIGNATURE unary? ((Boolean) $)) (SIGNATURE nary? ((Boolean) $)) (SIGNATURE weight ((NonNegativeInteger) $)) (SIGNATURE weight ($ $ (NonNegativeInteger))) (SIGNATURE equality ($ $ (Mapping (Boolean) $ $))) (SIGNATURE comparison ($ $ (Mapping (Boolean) $ $))) (SIGNATURE display ((Union (Mapping (OutputForm) (List (OutputForm))) failed) $)) (SIGNATURE display ($ $ (Mapping (OutputForm) (List (OutputForm))))) (SIGNATURE display ($ $ (Mapping (OutputForm) (OutputForm)))) (SIGNATURE input ($ $ (Mapping (InputForm) (List (InputForm))))) (SIGNATURE input ((Union (Mapping (InputForm) (List (InputForm))) failed) $)) (SIGNATURE is? ((Boolean) $ (Symbol))) (SIGNATURE has? ((Boolean) $ (Symbol))) (SIGNATURE assert ($ $ (Symbol))) (SIGNATURE deleteProperty! ($ $ (Symbol))) (SIGNATURE property ((Union (None) failed) $ (Symbol))) (SIGNATURE setProperty ($ $ (Symbol) (None))) (SIGNATURE setProperties ($ $ (AssociationList (Symbol) (None))))))
   compiling exported * : (a,b) -> $
      CDOM;*;ab$;1 is replaced by CONS 
Time: 0 SEC.

   compiling exported degree : $ -> Polynomial Integer
Time: 0 SEC.

   compiling exported coerce : $ -> OutputForm
Time: 0 SEC.

(time taken in buildFunctor:  0)

;;;     ***       C REDEFINED

;;;     ***       C REDEFINED
Time: 0 SEC.

   Warnings: 
      [1] degree:  left has no value
      [2] degree:  right has no value

   Cumulative Statistics for Constructor C
      Time: 0 seconds

   finalizing NRLIB CDOM 
   Processing C for Browser database:
--->-->C(constructor): Not documented!!!!
--->-->C((* (% a b))): Not documented!!!!
--->-->C(): Missing Description
; compiling file "/var/aw/var/LatexWiki/CDOM.NRLIB/CDOM.lsp" (written 01 SEP 2022 02:53:46 PM):

; /var/aw/var/LatexWiki/CDOM.NRLIB/CDOM.fasl written
; compilation finished in 0:00:00.015
------------------------------------------------------------------------
   C is now explicitly exposed in frame initial 
   C will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/CDOM.NRLIB/CDOM

   DDOM abbreviates domain D 
------------------------------------------------------------------------
   initializing NRLIB DDOM for D 
   compiling into NRLIB DDOM 
Local variable Rep type redefined: (Join (SetCategory) (CATEGORY domain (SIGNATURE construct ((Record (: arg a)) a)) (SIGNATURE ~= ((Boolean) (Record (: arg a)) (Record (: arg a)))) (SIGNATURE coerce ((OutputForm) (Record (: arg a)))) (SIGNATURE elt (a (Record (: arg a)) arg)) (SIGNATURE setelt! (a (Record (: arg a)) arg a)) (SIGNATURE copy ((Record (: arg a)) (Record (: arg a)))))) to (Join (SetCategory) (CATEGORY domain (SIGNATURE construct ((Record (: left a) (: right b)) a b)) (SIGNATURE ~= ((Boolean) (Record (: left a) (: right b)) (Record (: left a) (: right b)))) (SIGNATURE coerce ((OutputForm) (Record (: left a) (: right b)))) (SIGNATURE elt (a (Record (: left a) (: right b)) left)) (SIGNATURE elt (b (Record (: left a) (: right b)) right)) (SIGNATURE setelt! (a (Record (: left a) (: right b)) left a)) (SIGNATURE setelt! (b (Record (: left a) (: right b)) right b)) (SIGNATURE copy ((Record (: left a) (: right b)) (Record (: left a) (: right b))))))
   compiling exported d : $ -> B r
Time: 0 SEC.

   compiling exported d : a -> $
      DDOM;d;a$;2 is replaced by LIST 
Time: 0 SEC.

   compiling exported degree : $ -> Polynomial Integer
Time: 0.04 SEC.

   compiling exported coerce : $ -> OutputForm
Time: 0 SEC.

(time taken in buildFunctor:  0)

;;;     ***       D REDEFINED

;;;     ***       D REDEFINED
Time: 0 SEC.

   Warnings: 
      [1]  r has no value
      [2] degree:  arg has no value
      [3] coerce:  arg has no value

   Cumulative Statistics for Constructor D
      Time: 0.04 seconds

   finalizing NRLIB DDOM 
   Processing D for Browser database:
--->-->D(constructor): Not documented!!!!
--->-->D((d ((B r) %))): Not documented!!!!
--->-->D((d (% a))): Not documented!!!!
--->-->D(): Missing Description
; compiling file "/var/aw/var/LatexWiki/DDOM.NRLIB/DDOM.lsp" (written 01 SEP 2022 02:53:46 PM):

; /var/aw/var/LatexWiki/DDOM.NRLIB/DDOM.fasl written
; compilation finished in 0:00:00.016
------------------------------------------------------------------------
   D is now explicitly exposed in frame initial 
   D will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/DDOM.NRLIB/DDOM

fricas
a:=a::B(p)
\label{eq1}a(1)
Type: B(p)
fricas
b:=b::B(q)
\label{eq2}b(2)
Type: B(q)
fricas
c:=c::B(99)
\label{eq3}c(3)
Type: B(99)
fricas
o:=o::B(0)
\label{eq4}o(4)
Type: B(0)
fricas
test(degree a = p)
\label{eq5} \mbox{\rm true} (5)
Type: Boolean
fricas
test(degree o = 0)
\label{eq6} \mbox{\rm true} (6)
Type: Boolean
fricas
r := a*b
\label{eq7}a \otimes b(7)
Type: C(B(p),B(q))
fricas
s := c*o
\label{eq8}c \otimes o(8)
Type: C(B(99),B(0))
fricas
degree r
\label{eq9}q + p(9)
Type: Polynomial(Integer)
fricas
degree s
\label{eq10}99(10)
Type: Polynomial(Integer)
fricas
degree (r*s)
\label{eq11}q + p +{99}(11)
Type: Polynomial(Integer)
fricas
d r
\label{eq12}d{\left[ a \otimes b \right]}(12)
Type: D(C(B(p),B(q)))
fricas
d (r*c)
\label{eq13}d{\left[{a \otimes b}\otimes c \right]}(13)
Type: D(C(C(B(p),B(q)),B(99)))
fricas
a* d (b*a*b)
\label{eq14}a \otimes{d{\left[{b \otimes a}\otimes b \right]}}(14)
Type: C(B(p),D(C(C(B(q),B(p)),B(q))))
fricas
degree %
\label{eq15}{2 \ q}+{2 \ p}+ 1(15)
Type: Polynomial(Integer)
fricas
d r*d a
\label{eq16}{d{\left[ a \otimes b \right]}}\otimes{d{\left[ a \right]}}(16)
Type: C(D(C(B(p),B(q))),D(B(p)))
fricas
d %
\label{eq17}d{\left[{d{\left[ a \otimes b \right]}}\otimes{d{\left[ a \right]}}\right]}(17)
Type: D(C(D(C(B(p),B(q))),D(B(p))))
fricas
degree %
\label{eq18}q +{2 \ p}+ 3(18)
Type: Polynomial(Integer)
fricas
-- r=0 -> :(

d d r
\label{eq19}\hbox{\axiomType{NULL}\ }(19)
Type: B(r)