basic.gl

line A:P B:P -> a:L
  <- not_eq A B
  THEN
  a <- prim__line A B
  <- lies_on A a
  <- lies_on B a

direction_of l:L -> dir:A
  THEN
  dir <- prim__direction_of l
direction_of A:P B:P -> dir:A
  <- not_eq A B
  l <- line A B
  dir <- direction_of l
perp_direction l:L -> dir_p:A
  dir <- direction_of l
  dir_p <- angle_compute 1/2 dir 1
perp_direction A:P B:P -> dir_p:A
  dir <- direction_of A B
  dir_p <- angle_compute 1/2 dir 1

line_with_direction A:P d:A -> p:L
  THEN
  p <- prim__line_with_direction A d
  <- lies_on A p
  d' <- direction_of p
  <- == d' d

dist A:P B:P -> d:D
  <- not_eq A B
  THEN
  d <- prim__dist A B

eq_dist A0:P B0:P d1:D -> 
  d0 <- dist A0 B0
  <- == d0 d1
eq_dist d1:D A0:P B0:P -> 
  d0 <- dist A0 B0
  <- == d0 d1
eq_dist A0:P B0:P A1:P B1:P -> 
  d0 <- dist A0 B0
  d1 <- dist A1 B1
  <- == d0 d1

dist_ratio A0:P B0:P A1:P B1:P -> r:D
  <- not_eq A0 B0
  <- not_eq A1 B1
  d0 <- dist A0 B0
  d1 <- dist A1 B1
  r <- ratio_compute 1 d0 1 d1 -1

circumcircle A:P B:P C:P -> c:C
  <- not_collinear A B C
  THEN
  c <- prim__circumcircle A B C
  <- lies_on A c
  <- lies_on B c
  <- lies_on C c

radius_of c:C -> r:D
  THEN
  r <- prim__radius_of c
center_of c:C -> C:P
  THEN
  C <- prim__center_of c
circle C:P r:D -> c:C
  THEN
  c <- prim__circle C r
  r' <- radius_of c
  C' <- center_of c
  <- == r r'
  <- == C C'

point_on_circle X:P c:C -> 
  <- lies_on X c
  THEN
  C <- center_of c
  d <- dist X C
  r <- radius_of c
  <- == r d
point_to_circle X:P c:C -> 
  C <- center_of c
  r <- radius_of c
  <- eq_dist X C r
  THEN
  <- lies_on X c

not_parallel l0:L l1:L -> 
  x <- direction_of l0
  y <- direction_of l1
  <- not_eq x y

intersection a:L b:L -> X:P
  <- not_parallel a b
  THEN
  X <- prim__intersection a b
  <- lies_on X a
  <- lies_on X b

angle l0:L l1:L -> alpha:A
  d0 <- direction_of l0
  d1 <- direction_of l1
  alpha <- angle_compute 0 d0 -1 d1 1
#angle l0:L A1:P B1:P -> alpha:A
#  l1 <- line A1 B1
#  alpha <- angle l0 l1
angle l0:L A1:P B1:P -> alpha:A
  d0 <- direction_of l0
  d1 <- direction_of A1 B1
  alpha <- angle_compute 0 d0 -1 d1 1
angle A0:P B0:P l1:L -> alpha:A
  d0 <- direction_of A0 B0
  d1 <- direction_of l1
  alpha <- angle_compute 0 d0 -1 d1 1
#angle A0:P B0:P A1:P B1:P -> alpha:A
#  l1 <- line A1 B1
#  alpha <- angle A0 B0 l1
angle A0:P B0:P A1:P B1:P -> alpha:A
  d0 <- direction_of A0 B0
  d1 <- direction_of A1 B1
  alpha <- angle_compute 0 d0 -1 d1 1
#angle A:P B:P C:P -> alpha:A
#  l1 <- line B C
#  alpha <- angle B A l1
angle A:P B:P C:P -> alpha:A
  alpha <- angle B A B C

eq_angle a0:L b0:L a1:L b1:L -> 
  alpha0 <- angle a0 b0
  alpha1 <- angle a1 b1
  <- == alpha0 alpha1
eq_angle A0:P B0:P C0:P a1:L b1:L -> 
  alpha0 <- angle A0 B0 C0
  alpha1 <- angle a1 b1
  <- == alpha0 alpha1
eq_angle a0:L b0:L A1:P B1:P C1:P -> 
  alpha0 <- angle a0 b0
  alpha1 <- angle A1 B1 C1
  <- == alpha0 alpha1
eq_angle A0:P B0:P C0:P A1:P B1:P C1:P -> 
  alpha0 <- angle A0 B0 C0
  alpha1 <- angle A1 B1 C1
  <- == alpha0 alpha1
eq_angle A0:P B0:P C0:P alpha1:A ->
  alpha0 <- angle A0 B0 C0
  <- == alpha0 alpha1

sim_aa A0:P B0:P C0:P A1:P B1:P C1:P -> 
  <- not_collinear A0 B0 C0
  <- eq_angle C0 A0 B0 C1 A1 B1
  <- eq_angle A0 B0 C0 A1 B1 C1
  ra <- dist_ratio B0 C0 B1 C1
  rb <- dist_ratio C0 A0 C1 A1
  rc <- dist_ratio A0 B0 A1 B1
  THEN
  <- == ra rb
  <- == ra rc
sim_aa_r A0:P B0:P C0:P A1:P B1:P C1:P -> 
  <- not_collinear A0 B0 C0
  ra <- dist_ratio B0 C0 B1 C1
  rb <- dist_ratio C0 A0 C1 A1
  rc <- dist_ratio A0 B0 A1 B1
  <- eq_angle C0 A0 B0 B1 A1 C1
  <- eq_angle A0 B0 C0 C1 B1 A1
  THEN
  <- == ra rb
  <- == ra rc

isosceles_ss A:P B:P C:P -> 
  <- not_eq B C
  <- eq_dist A B A C
  THEN
  <- eq_angle A B C B C A

midpoint A:P B:P -> M:P
  l <- line A B
  THEN
  M <- prim__midpoint A B
  <- lies_on M l
  <- eq_dist A M M B
  r <- dist_ratio A B A M
  <- ratio_pred 1/2 r 1

perpline l:L A:P -> p:L
  dir <- perp_direction l
  p <- line_with_direction A dir
perpline X0:P X1:P A:P -> p:L
  l <- line X0 X1
  p <- perpline l A
perp_bisector A:P B:P -> p:L
  M <- midpoint A B
  ab <- line A B
  p <- perpline ab M
point_on_perp_bisector X:P A:P B:P -> 
  p <- perp_bisector A B
  <- lies_on X p
  THEN
  <- eq_dist X A X B
  a <- line A X
  b <- line B X
  <- eq_angle a p p b
point_to_perp_bisector X:P A:P B:P -> 
  <- eq_dist X A X B
  p <- perp_bisector A B
  THEN
  <- lies_on X p

half_direction A:P B:P -> dir:A
  <- not_eq A B
  THEN
  dir <- prim__half_direction A B
  dir2 <- direction_of A B
  <- angle_pred 0 dir 2 dir2 -1

double_direction A:P dir:A d:D -> B:P
  THEN
  B <- prim__double_direction A dir d
  dir2 <- direction_of A B
  <- angle_pred 0 dir 2 dir2 -1
  d2 <- dist A B
  <- == d d2

angle_2_to_3 ang2:A -> ang3:A
  a90 <- angle_compute 1/2
  <- not_eq ang2 a90
  THEN
  ang3 <- prim__angle_2_to_3 ang2
  <- angle_pred 0 ang3 3 ang2 -2