MathAction DependentTypeTest1



DependentTypeTest1
last edited 3 years ago by pagani

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 15 MAR 2025 07:03:21 AM):
; wrote /var/aw/var/LatexWiki/ACAT.NRLIB/ACAT.fasl ; compilation finished in 0:00:00.000 ------------------------------------------------------------------------ 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 SEC.
compiling exported degree : % -> Polynomial Integer Time: 0 SEC.
(time taken in buildFunctor: 0)
;;; *** B REDEFINED
;;; *** B REDEFINED Time: 0 SEC.
Cumulative Statistics for Constructor B Time: 0.01 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 15 MAR 2025 07:03:21 AM):
; wrote /var/aw/var/LatexWiki/BDOM.NRLIB/BDOM.fasl ; compilation finished in 0:00:00.004 ------------------------------------------------------------------------ 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 15 MAR 2025 07:03:21 AM):
; wrote /var/aw/var/LatexWiki/CDOM.NRLIB/CDOM.fasl ; compilation finished in 0:00:00.008 ------------------------------------------------------------------------ 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 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.01 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 15 MAR 2025 07:03:21 AM):
; wrote /var/aw/var/LatexWiki/DDOM.NRLIB/DDOM.fasl ; compilation finished in 0:00:00.004 ------------------------------------------------------------------------ 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)
Type: B(p)
fricas
b:=b::B(q)
Type: B(q)
fricas
c:=c::B(99)
Type: B(99)
fricas
o:=o::B(0)
Type: B(0)
fricas
test(degree a = p)
Type: Boolean
fricas
test(degree o = 0)
Type: Boolean
fricas
r := a*b
Type: C(B(p),B(q))
fricas
s := c*o
Type: C(B(99),B(0))
fricas
degree r
Type: Polynomial(Integer)
fricas
degree s
Type: Polynomial(Integer)
fricas
degree (r*s)
Type: Polynomial(Integer)
fricas
d r
Type: D(C(B(p),B(q)))
fricas
d (r*c)
Type: D(C(C(B(p),B(q)),B(99)))
fricas
a* d (b*a*b)
Type: C(B(p),D(C(C(B(q),B(p)),B(q))))
fricas
degree %
Type: Polynomial(Integer)
fricas
d r*d a
Type: C(D(C(B(p),B(q))),D(B(p)))
fricas
d %
Type: D(C(D(C(B(p),B(q))),D(B(p))))
fricas
degree %
Type: Polynomial(Integer)
fricas
-- r=0 -> :(
d d r
Type: B(r)




Subject: Be Bold !!
( 15 subscribers )
Please rate this page:

AltStyle によって変換されたページ (->オリジナル) /