%hide
automatic_names(True)
from xml.etree import ElementTree as ET
myxml_modified = (myxml.replace('\n','')).replace('\t','')
ggb = ET.XML(myxml_modified)
"""Since the construction XML element lies on different parts in GeoGebra 3.2 and GeoGebra 4.0, we read it as appropriate and set its value in cons"""
if ggb.items()[1][1]=='3.2':
cons=ggb[3]
else:
cons=ggb[5]
#################Caso Locus####################
if myxml.find("ocus") > -1:
######
#print "Locus!"
#########
#next we process the GeoGebra locus construction
BoVar=[eval ('x%s'%p) for p in range(1,100)];BoVar.reverse()
Todo={}
def FreePoint(pnt,absc,orde):
"""Adds the point $pnt$ with coordinates $(absc,orde)$ to the geometric construction."""
Todo.update({pnt:{'coords':(absc,orde),'parents':Set([]),'type':'FreePoint','hist':['FreePoint',pnt,absc,orde],'eq':Set([])}})
def BoundedPoint(pnt, absc, orde):
Todo.update({pnt:{'coords':(absc,orde),'type':'BoundedPoint'}})
def is_point(p):
return ((p in Todo.keys()) and (Todo[p]['type']=='FreePoint' or Todo[p]['type']=='BoundedPoint'))
def x(obj):
if is_point(obj):
return Todo[obj]['coords'][0]
def y(obj):
if is_point(obj):
return Todo[obj]['coords'][1]
""" anc is a global variable used in the function ancestors. It must be set to nil before evaluating the function"""
anc=[]
def ancestors(n):
"""Returns a set consisting of $n$ and all its ancestors, if $n$ is a construction object. It returns the empty set in other case."""
global anc
res=anc
if n in Todo.keys():
res.append(n)
t=list(Todo[n]['parents'])
res.extend(t)
for i in t:
ancestors(i)
return Set(res)
def Line(n,p,q):
"""Constructs the line $n$ that goes through the points $p$ and $q$."""
vdir=(x(q) - x(p), y(q) - y(p))
eq=Set([(absc - x(p))*(y(q) - y(p)) - (orde - y(p))*(x(q) - x(p))])
pare=Set([p,q])
Todo.update({n:{'vdir':vdir,'eq':eq, 'parents':pare,'type':'Line','hist':['Line',n,p,q]}})
def Segment(n,p,q):
"""Constructs the line $n$ that goes through the points $p$ and $q$. Defined for GeoGebra compatibility."""
vdir=(x(q) - x(p), y(q) - y(p))
eq=Set([(absc - x(p))*(y(q) - y(p)) - (orde - y(p))*(x(q) - x(p))])
pare=Set([p,q])
Todo.update({n:{'vdir':vdir,'eq':eq, 'parents':pare,'type':'Line','hist':['Segment',n,p,q]}})
def Circle(n,c,p,*q):
"""Constructs the circle $n$ with center the point $c$ and radius (squared!) $p^2$ if $p$ is a number. If $p$ is a point, $n$is the circle
with center $c$ and passing through the point $p$. If there is a fourth argument, the point $q$, then so must be $p$ and the circle has center
$c$ and radius (squared) the distance between $p$ and $q$"""
pare=[c]
if is_point(p):
pare.append(p)
if len(q)==1:
radius2=(x(p)-x(q[0]))^2+(y(p)-y(q[0]))^2
pare.append(q[0])
else:
radius2=(x(p)-x(c))^2+(y(p)-y(c))^2
else:
radius2=p^2
eq=Set([(absc - x(c))^2 + (orde - y(c))^2 - radius2])
Todo.update({n:{'center':c,'radius2':radius2,'eq':eq, 'parents':Set(pare),'type':'Line','hist':['Circle',n,c,p,q]}})
def MidPoint(n,p,q):
"""Constructs the midpoint $n$ of points $p$ and $q$."""
if n in Todo.keys():
eq=Todo[n]['eq']
parents=Todo[n]['parents']
temp=Todo[n]['coords']
else:
eq=Set([])
parents=Set([])
temp=(BoVar.pop(),BoVar.pop())
eq=eq.union(Set([temp[0]-1/2*(x(p)+x(q)),temp[1]-1/2*(y(p)+y(q))]))
parents=parents.union(Set([p,q]))
Todo.update({n:{'coords':temp,'type':'BoundedPoint','eq':eq,'parents':parents,'hist':['MidPoint',n,p,q]}})
def PointOnObject(n,o):
"""Constructs a point $n$ lying on object $o$."""
if n in Todo.keys():
eq=Todo[n]['eq']
temp=Todo[n]['coords']
parents=Todo[n]['parents']
else:
eq=Set([])
parents=Set([])
temp=(BoVar.pop(),BoVar.pop())
flag_subs=False
for i in list(Todo[o]['eq']):
if (absc in list(i.variables()) or orde in list(i.variables())):
flag_subs=True
eq=eq.union(Set([i.subs(absc=temp[0],orde=temp[1])]))
parents=parents.union(Set([o]))
if flag_subs:
Todo.update({n:{'coords':temp,'parents':parents,'eq':eq,'type':'BoundedPoint','hist':['PointOnObject',n,o]}})
def ParallelLine(n,p,l):
"""Constructs the line $n$ parallel to the line $l$ passing through $p$."""
vdir=Todo[l]['vdir']
eq=Set([(absc - x(p))*vdir[1] - (orde - y(p))*vdir[0]])
pare=Set([p,l])
Todo.update({n:{'vdir':vdir,'eq':eq, 'parents':pare,'type':'Line','hist':['ParallelLine',n,p,l]}})
def PerpendicularLine(n,p,l):
"""Constructs the line $n$ perpendicular to the line $l$ passing through $p$."""
vdir=Todo[l]['vdir']
eq=Set([(absc - x(p))*vdir[0] + (orde - y(p))*vdir[1]])
vdir=(-vdir[1],vdir[0])
pare=Set([p,l])
Todo.update({n:{'vdir':vdir,'eq':eq, 'parents':pare,'type':'Line','hist':['PerpendicularLine',n,p,l]}})
def IntersectionObjectObject(n,o1,o2):
"""Constructs a point $n$ as intersection of objects $o1$ and $o2$."""
PointOnObject(n,o1)
PointOnObject(n,o2)
def Locus(n,t,*m):
"""Constructs the locus $n$ with tracer $t$. The third argument, if it exists, $m$, is the mover. If it does not exist, the locus is an
implicit one."""
#######
#locus_name = n
#print "locus name:" + locus_name
#######
if len(m)==1:
mover=str(m[0])
implicit=False
else:
implicit=True
mover=''
if implicit:
parents=Set([t])
else:
parents=Set([t,mover])
vbl='';vblist=[]
anc=[];anc_de_t=ancestors(t)
anc=[];anc_de_m=ancestors_de_m=ancestors(mover)
anc_set=anc_de_t.union(anc_de_m)
for i in anc_set:
if Todo[i]['type']=='BoundedPoint':
vbl=vbl+','+str(x(i))
vblist.append(x(i))
vbl=vbl+','+str(y(i))
vblist.append(y(i))
vbl=vbl.replace(',','',1)
vblist.remove(x(t));vblist.remove(y(t))
Eqs=[]
for i in anc_set:
if Todo[i]['type']=='BoundedPoint':
for j in list(Todo[i]['eq']):
Eqs.append(j)
S = PolynomialRing(QQ, vbl)
S.inject_variables()
I=Eqs*S
H=I.elimination_ideal(eval(str(vblist)))
res=H.gens()
"""res=map(factor,H.gens())"""
eq=[]
a,b=str(x(t)),str(y(t))
for i in res:
i=str(i)
i=i.replace('^','**')
i=i.replace(a,'absc')
i=i.replace(b,'orde')
i=eval(i)
eq.append(i)
T=PolynomialRing(QQ,[absc,orde])
T.inject_variables()
J=eq*T
di=J.dimension()
print 'dimension=',di
if di==1:
type='Line'
eq=Set(eq)
elif di==0:
type='BoundedPoint'
temp=(BoVar.pop(),BoVar.pop())
eqq=[]
for i in eq:
eqq.append(i.subs({absc:temp[0],orde:temp[1]}))
eq=Set(eqq)
elif di==2:
type='Plane'
eq=Set([0])
else:
type='Nil'
eq=Set([1])
##########
equation = """ """
equation = str(eq)
equation = equation.replace('absc','x')
equation = equation.replace('orde','y')
equation = equation.replace('{','')
equation = equation.replace('L','')
equation = equation.replace('}','') + " = 0"
html('<script type="text/javascript">document.applets[0].evalCommand("%s")</script>'%(equation))
html('<script type="text/javascript">var numberOfElements = document.applets[0].getObjectNumber(); var nameLastElement = document.applets[0].getObjectName(numberOfElements-1); document.applets[0].setColor(nameLastElement, 0, 0, 250); document.applets[0].setLineThickness(nameLastElement, 5); document.applets[0].setLineStyle(nameLastElement, 3);</script>')
print "The locus equation is \n" + equation + "\n\nIts graph has been added to the construction in the applet (dotted blue)."
##########
hist=['Locus',n,t]
if not implicit:
hist.append(mover)
diccio=[('implicit',implicit),('tracer',t),('mover',mover),('parents',parents),('eq',eq),('type',type),('hist',hist)]
if type=='BoundedPoint':
diccio.append(('coords',temp))
Todo.update({n:dict(diccio)})
def eval_cons(cons):
for i in cons:
b=i.items()
if i.tag=='element' and b[0][1]=='point' and not (b[1][1] in Todo.keys()):
dic=dict(i.find('coords').items())
coord_x=sage_eval(dic['x']);coord_y=sage_eval(dic['y'])
coord_x=coord_x.simplest_rational();coord_y=coord_y.simplest_rational()
FreePoint(str(b[1][1]),coord_x,coord_y)
elif i.tag=='command':
if b[0][1]=='Circle':
dic_in=dict(i.find('input').items())
dic_out=dict(i.find('output').items())
"""Circle cases: center-radius, center-point,center-radius_as_segment"""
if dic_in['a1'].find('Segment[') <> -1:
seg=dic_in['a1']
p=seg.split(',')[0];p=p.replace('Segment[','')
q=seg.split(',')[1];q=q.replace(']','');q=q.replace(' ','')
Circle(dic_out['a0'],dic_in['a0'],p,q)
elif dic_in['a1'][0].isalpha():
Circle(dic_out['a0'],dic_in['a0'],dic_in['a1'])
else:
rad=sage_eval(dic_in['a1']);rad=rad.simplest_rational()
Circle(dic_out['a0'],dic_in['a0'],rad)
elif b[0][1]=='Segment':
"""The second ggb Segment definition is not implemented here"""
dic_in=dict(i.find('input').items())
dic_out=dict(i.find('output').items())
Segment(dic_out['a0'],dic_in['a0'],dic_in['a1'])
elif b[0][1]=='Line':
"""2 cases: line(point,point) and line(point,line), meaning a parallel ..."""
dic_in=dict(i.find('input').items())
dic_out=dict(i.find('output').items())
if is_point(dic_in['a1']):
Line(dic_out['a0'],dic_in['a0'],dic_in['a1'])
else:
ParallelLine(dic_out['a0'],dic_in['a0'],dic_in['a1'])
elif b[0][1]=='Midpoint':
"""midpoint of two given points"""
dic_in=dict(i.find('input').items())
dic_out=dict(i.find('output').items())
MidPoint(dic_out['a0'],dic_in['a0'],dic_in['a1'])
elif b[0][1]=='OrthogonalLine':
"""perpendicular line through a given point to a given line"""
dic_in=dict(i.find('input').items())
dic_out=dict(i.find('output').items())
PerpendicularLine(dic_out['a0'],dic_in['a0'],dic_in['a1'])
elif b[0][1]=='Point':
"""Point on Circle"""
dic_in=dict(i.find('input').items())
dic_out=dict(i.find('output').items())
PointOnObject(dic_out['a0'],dic_in['a0'])
elif b[0][1]=='Intersect':
"""computes the intersection of any pair of linear objects"""
dic_in=dict(i.find('input').items())
dic_out=dict(i.find('output').items())
IntersectionObjectObject(dic_out['a0'],dic_in['a0'],dic_in['a1'])
elif b[0][1]=='Locus':
"""computes an explicit locus"""
dic_in=dict(i.find('input').items())
dic_out=dict(i.find('output').items())
Locus(dic_out['a0'],dic_in['a0'],dic_in['a1'])
def get_eq_internal(n):
e=list(Todo[n]['eq'])
for i in e:
if Set(map(str,i.variables())).union(Set(['absc','orde']))!=Set(['absc','orde']):
return 'The object is parametrically defined'
if len(e)==1:
res=[]
for i in e[0].factor_list():
res.append(i[0])
return res
elif len(e)==0:
return 'The object has no equations'
else:
res=[]
for j in e:
restemp=[]
for i in j.factor_list():
restemp.append(i[0])
res.append(restemp)
return res
def get_eq(n):
e=list(Todo[n]['eq'])
for i in e:
if Set(map(str,i.variables())).union(Set(['absc','orde']))!=Set(['absc','orde']):
return 'The object is parametrically defined'
if len(e)==1:
res=[]
for i in e[0].factor_list():
res.append(i[0].subs({absc:X,orde:Y}))
return res
elif len(e)==0:
return 'The object has no equations'
else:
res=[]
for j in e:
restemp=[]
for i in j.factor_list():
restemp.append(i[0].subs({absc:X,orde:Y}))
res.append(restemp)
return res
def box_dim2d(e):
"""Returns adequate box dimensions for plotting the 2d-geometric object described by $e$, if $e$ is compact. Usa .roots(ring=RR) sobre los polinomios univariables para calcular las raices"""
e1,e2=diff(e,absc),diff(e,orde)
S = PolynomialRing(QQ, [absc,orde])
S.inject_variables()
I=[e,e2]*S
H=I.elimination_ideal([orde])
if H.is_principal() and not H.is_one() and not H.is_zero():
eq=gens(H)[0].subs({absc:X,orde:Y})
if eq==0:
m0,M1,px=0,0,0
else:
raices=eq.roots(ring=RR,multiplicities=False)
if raices==[]:
return False
M1,m0=max(raices),min(raices)
px=(M1-m0)/10
if px==0:
px=.5
else:
return False
I=[e,e1]*S
H=I.elimination_ideal([absc])
if H.is_principal() and not H.is_one() and not H.is_zero():
eq=gens(H)[0].subs({absc:X,orde:Y})
if eq==0:
m2,M3,py=0,0,0
else:
raices=eq.roots(ring=RR,multiplicities=False)
if raices==[]:
return False
M3,m2=max(raices),min(raices)
py=(M3-m2)/10
if py==0:
py=.5
else:
return False
"""px and py extend the drawing box"""
return [m0-px,M1+px,m2-py,M3+py]
def get_plot(l):
l=get_eq_internal(l)
if l==[]:
return 'There is nothing to plot'
else:
a=Graphics()
for i in l:
i=expand(i)
dim=box_dim2d(i)
if not (dim==False):
a=a+implicit_plot(i,(absc,dim[0],dim[1]),(orde,dim[2],dim[3]),aspect_ratio=1)
else:
a=a+implicit_plot(i,(absc,dims[0],dims[1]),(orde,dims[2],dims[3]),aspect_ratio=1)
return a
def get_plot_window(l):
l=get_eq_internal(l)
if l==[]:
return 'There is nothing to plot'
else:
a=Graphics()
for i in l:
i=expand(i)
dim=box_dim2d(i)
a=a+implicit_plot(i,(absc,dims[0],dims[1]),(orde,dims[2],dims[3]),aspect_ratio=1)
return a
eval_cons(cons)
#print "name of locus:" + locus_name
#ec = get_eq(locus_name)
#print ec
#############################
if myxml.find("boolean") > -1:
#####
#print "proof"
#####
#next we process the GeoGebra locus construction
#extend the number of variables as needed (currently 100)
BoVar=[eval ('x%s'%p) for p in range(1,100)];BoVar.reverse()
FrVar=[eval ('u%s'%p) for p in range(1,100)];FrVar.reverse()
Todo={}
def FreePoint(pnt,absc,orde):
"""Adds the point $pnt$ with coordinates $(absc,orde)$ to the geometric construction."""
Todo.update({pnt:{'coords':(absc,orde),'parents':Set([]),'type':'FreePoint','hist':['FreePoint',pnt,absc,orde],'eq':Set([])}})
def BoundedPoint(pnt, absc, orde):
Todo.update({pnt:{'coords':(absc,orde),'type':'BoundedPoint'}})
def is_point(p):
return ((p in Todo.keys()) and (Todo[p]['type']=='FreePoint' or Todo[p]['type']=='BoundedPoint'))
def x(obj):
if is_point(obj):
return Todo[obj]['coords'][0]
def y(obj):
if is_point(obj):
return Todo[obj]['coords'][1]
""" anc is a global variable used in the function ancestors. It must be set to nil before evaluating the function"""
anc=[]
def ancestors(n):
"""Returns a set consisting of $n$ and all its ancestors, if $n$ is a construction object. It returns the empty set in other case."""
global anc
res=anc
if n in Todo.keys():
res.append(n)
t=list(Todo[n]['parents'])
res.extend(t)
for i in t:
ancestors(i)
return Set(res)
def Line(n,p,q):
"""Constructs the line $n$ that goes through the points $p$ and $q$."""
vdir=(x(q) - x(p), y(q) - y(p))
eq=Set([(absc - x(p))*(y(q) - y(p)) - (orde - y(p))*(x(q) - x(p))])
pare=Set([p,q])
Todo.update({n:{'vdir':vdir,'eq':eq, 'parents':pare,'type':'Line','hist':['Line',n,p,q]}})
def Circle(n,c,p,*q):
"""Constructs the circle $n$ with center the point $c$ and radius (squared!) $p^2$ if $p$ is a number. If $p$ is a point, $n$is the circle
with center $c$ and passing through the point $p$. If there is a fourth argument, the point $q$, then so must be $p$ and the circle has center
$c$ and radius (squared) the distance between $p$ and $q$"""
pare=[c]
if is_point(p):
pare.append(p)
if len(q)==1:
radius2=(x(p)-x(q[0]))^2+(y(p)-y(q[0]))^2
pare.append(q[0])
else:
radius2=(x(p)-x(c))^2+(y(p)-y(c))^2
else:
radius2=p^2
eq=Set([(absc - x(c))^2 + (orde - y(c))^2 - radius2])
Todo.update({n:{'center':c,'radius2':radius2,'eq':eq, 'parents':Set(pare),'type':'Line','hist':['Circle',n,p,q]}})
def MidPoint(n,p,q):
"""Constructs the midpoint $n$ of points $p$ and $q$."""
if n in Todo.keys():
eq=Todo[n]['eq']
parents=Todo[n]['parents']
temp=Todo[n]['coords']
else:
eq=Set([])
parents=Set([])
temp=(BoVar.pop(),BoVar.pop())
eq=eq.union(Set([temp[0]-1/2*(x(p)+x(q)),temp[1]-1/2*(y(p)+y(q))]))
parents=parents.union(Set([p,q]))
Todo.update({n:{'coords':temp,'type':'BoundedPoint','eq':eq,'parents':parents,'hist':['MidPoint',n,p,q]}})
def PointOnObject(n,o):
"""Constructs a point $n$ lying on object $o$."""
if n in Todo.keys():
eq=Todo[n]['eq']
temp=Todo[n]['coords']
parents=Todo[n]['parents']
else:
eq=Set([])
parents=Set([])
temp=(BoVar.pop(),BoVar.pop())
flag_subs=False
for i in list(Todo[o]['eq']):
if (absc in list(i.variables()) or orde in list(i.variables())):
flag_subs=True
eq=eq.union(Set([i.subs(absc=temp[0],orde=temp[1])]))
parents=parents.union(Set([o]))
if flag_subs:
Todo.update({n:{'coords':temp,'parents':parents,'eq':eq,'type':'BoundedPoint','hist':['PointOnObject',n,o]}})
def ParallelLine(n,p,l):
"""Constructs the line $n$ parallel to the line $l$ passing through $p$."""
vdir=Todo[l]['vdir']
eq=Set([(absc - x(p))*vdir[1] - (orde - y(p))*vdir[0]])
pare=Set([p,l])
Todo.update({n:{'vdir':vdir,'eq':eq, 'parents':pare,'type':'Line','hist':['ParallelLine',n,p,l]}})
def PerpendicularLine(n,p,l):
"""Constructs the line $n$ perpendicular to the line $l$ passing through $p$."""
vdir=Todo[l]['vdir']
eq=Set([(absc - x(p))*vdir[0] + (orde - y(p))*vdir[1]])
vdir=(-vdir[1],vdir[0])
pare=Set([p,l])
Todo.update({n:{'vdir':vdir,'eq':eq, 'parents':pare,'type':'Line','hist':['PerpendicularLine',n,p,l]}})
def IntersectionObjectObject(n,o1,o2):
"""Constructs a point $n$ as intersection of objects $o1$ and $o2$."""
PointOnObject(n,o1)
PointOnObject(n,o2)
def Locus(n,t,*m):
"""Constructs the locus $n$ with tracer $t$. The third argument, if it exists, $m$, is the mover. If it does not exist, the locus is an
implicit one."""
if len(m)==1:
mover=str(m[0])
implicit=False
else:
implicit=True
mover=''
if implicit:
parents=Set([t])
else:
parents=Set([t,mover])
vbl='';vblist=[]
anc=[];anc_de_t=ancestors(t)
anc=[];anc_de_m=ancestors_de_m=ancestors(mover)
anc_set=anc_de_t.union(anc_de_m)
for i in anc_set:
if Todo[i]['type']=='BoundedPoint':
vbl=vbl+','+str(x(i))
vblist.append(x(i))
vbl=vbl+','+str(y(i))
vblist.append(y(i))
vbl=vbl.replace(',','',1)
vblist.remove(x(t));vblist.remove(y(t))
Eqs=[]
for i in anc_set:
if Todo[i]['type']=='BoundedPoint':
for j in list(Todo[i]['eq']):
Eqs.append(j)
S = PolynomialRing(QQ, vbl)
S.inject_variables()
I=Eqs*S
H=I.elimination_ideal(eval(str(vblist)))
res=H.gens()
"""res=map(factor,H.gens())"""
eq=[]
a,b=str(x(t)),str(y(t))
for i in res:
i=str(i)
i=i.replace('^','**')
i=i.replace(a,'absc')
i=i.replace(b,'orde')
i=eval(i)
eq.append(i)
T=PolynomialRing(QQ,[absc,orde])
T.inject_variables()
J=eq*T
di=J.dimension()
print 'dimension=',di
if di==1:
type='Line'
eq=Set(eq)
elif di==0:
type='BoundedPoint'
temp=(BoVar.pop(),BoVar.pop())
eqq=[]
for i in eq:
eqq.append(i.subs({absc:temp[0],orde:temp[1]}))
eq=Set(eqq)
elif di==2:
type='Plane'
eq=Set([0])
else:
type='Nil'
eq=Set([1])
hist=['Locus',n,t]
if not implicit:
hist.append(mover)
diccio=[('implicit',implicit),('tracer',t),('mover',mover),('parents',parents),('eq',eq),('type',type),('hist',hist)]
if type=='BoundedPoint':
diccio.append(('coords',temp))
Todo.update({n:dict(diccio)})
def are_aligned(p,q,r):
"""Returns a list with a polynomial stating the alignment of points $p$, $q$ and $r$ and the function arguments."""
return [(x(r)-x(p))*(y(q)-y(p))-(y(r)-y(p))*(x(q)-x(p)),[p,q,r]]
def perpendicular(l,m):
"""Returns a list with a polynomial stating the perpendicularity of lines $l$ and $m$ and the function arguments."""
return [Todo[l]['vdir'][1]*Todo[m]['vdir'][1]+Todo[l]['vdir'][0]*Todo[m]['vdir'][0],[l,m]]
def parallel(l,m):
"""Returns a list with a polynomial stating the parallelism of lines $l$ and $m$ and the function arguments."""
return [Todo[l]['vdir'][0]*Todo[m]['vdir'][1]-Todo[l]['vdir'][1]*Todo[m]['vdir'][0],[l,m]]
def same(p,q):
"""Returns a list with a polynomial stating that points $p$ and $q$ are the same point and the function arguments."""
return [(x(p)-x(q))^2+(y(p)-y(q))^2,[p,q]]
def get_hyp(lista):
"""devuelve una tupla formada por (lista) las variables de los polinomios hipotesis y una lista con los polinomios hipotesis. Estos ultimos on los campos eq de los BoundedPoint's de los ancestors de los elementos de lista."""
pol=Set([])
vbles=Set([])
for i in lista:
anc=[]
for j in ancestors(i):
if Todo[j]['type']=='FreePoint':
vbles=vbles.union(Set(Todo[j]['coords']))
if Todo[j]['type']=='BoundedPoint':
pol=pol.union(Todo[j]['eq'])
for k in Todo[j]['eq']:
vbles=vbles.union(Set(k.variables()))
v=list(vbles)
v.sort(key=lambda alph: str(alph))
return (v,list(pol))
def prove_sat(l):
deg=[]
tes=l[0]
args=l[1]
get_h=get_hyp(l[1])
vbles=get_h[0]
hyp_pol=get_h[1]
S = PolynomialRing(QQ, vbles)
S.inject_variables()
H=hyp_pol*S
T=[tes]*S
sat0=singular.sat(H,T)
id_sat0=list(sat0[1])*S
d_sat=singular.sat(H,id_sat0)
id_d_sat=list(d_sat[1])*S
return not(id_d_sat.is_one())
def eval_symb_cons(cons):
for i in cons:
b=i.items()
if i.tag=='element' and b[0][1]=='point' and not (b[1][1] in Todo.keys()):
dic=dict(i.find('coords').items())
coord_x=sage_eval(dic['x']);coord_y=sage_eval(dic['y'])
coord_x=coord_x.simplest_rational();coord_y=coord_y.simplest_rational()
FreePoint(str(b[1][1]),FrVar.pop(),FrVar.pop())
elif i.tag=='expression':
"""currently only parallelism and perpendicularity. Works only with symbolic coordinates for free points!"""
lab=b[1][1]
expr=b[0][1]
args=expr.split()
if args[1]==u'\u22a5':
return prove_sat(perpendicular(args[0],args[2]))
elif args[1]==u'\u2225':
return prove_sat(parallel(args[0],args[2]))
elif i.tag=='command':
if b[0][1]=='Circle':
dic_in=dict(i.find('input').items())
dic_out=dict(i.find('output').items())
"""Circle cases: center-radius, center-point,center-radius_as_segment"""
if dic_in['a1'].find('Segment[') <> -1:
seg=dic_in['a1']
p=seg.split(',')[0];p=p.replace('Segment[','')
q=seg.split(',')[1];q=q.replace(']','');q=q.replace(' ','')
Circle(dic_out['a0'],dic_in['a0'],p,q)
elif dic_in['a1'][0].isalpha():
Circle(dic_out['a0'],dic_in['a0'],dic_in['a1'])
else:
rad=sage_eval(dic_in['a1']);rad=rad.simplest_rational()
Circle(dic_out['a0'],dic_in['a0'],rad)
elif b[0][1]=='Segment':
"""The second ggb Segment definition is not implemented here"""
dic_in=dict(i.find('input').items())
dic_out=dict(i.find('output').items())
Segment(dic_out['a0'],dic_in['a0'],dic_in['a1'])
elif b[0][1]=='Line':
"""2 cases: line(point,point) and line(point,line), meaning a parallel ..."""
dic_in=dict(i.find('input').items())
dic_out=dict(i.find('output').items())
if is_point(dic_in['a1']):
Line(dic_out['a0'],dic_in['a0'],dic_in['a1'])
else:
ParallelLine(dic_out['a0'],dic_in['a0'],dic_in['a1'])
elif b[0][1]=='Midpoint':
"""midpoint of two given points"""
dic_in=dict(i.find('input').items())
dic_out=dict(i.find('output').items())
MidPoint(dic_out['a0'],dic_in['a0'],dic_in['a1'])
elif b[0][1]=='OrthogonalLine':
"""perpendicular line through a given point to a given line"""
dic_in=dict(i.find('input').items())
dic_out=dict(i.find('output').items())
PerpendicularLine(dic_out['a0'],dic_in['a0'],dic_in['a1'])
elif b[0][1]=='Point':
"""Point on Circle"""
dic_in=dict(i.find('input').items())
dic_out=dict(i.find('output').items())
PointOnObject(dic_out['a0'],dic_in['a0'])
elif b[0][1]=='Intersect':
"""computes the intersection of any pair of linear objects"""
dic_in=dict(i.find('input').items())
dic_out=dict(i.find('output').items())
IntersectionObjectObject(dic_out['a0'],dic_in['a0'],dic_in['a1'])
elif b[0][1]=='Locus':
"""computes an explicit locus"""
dic_in=dict(i.find('input').items())
dic_out=dict(i.find('output').items())
Locus(dic_out['a0'],dic_in['a0'],dic_in['a1'])
a=eval_symb_cons(cons)
print '\nThe GeoGebra statement is generally',a
|
|
Defining u1, u2, u3, u4, u5, u6, x1, x2
The GeoGebra statement is generally True
Defining u1, u2, u3, u4, u5, u6, x1, x2
The GeoGebra statement is generally True
|