separates computations to make functions available in the polynomial ring

triangulation_algorithm.v

@@ -8,11 +8,46 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+Section num_computations.
+
+Variable P : Type.
+
+Variable R : unitRingType.
+
+Variables coords : P -> R * R.
+
+Definition mkf3 (T : Type) (a b c : T) :=
+  [ffun i : 'I_3 => if val i == 0 then a else if val i == 1 then b else c].
+
+Notation "<< a ; b ; c >>" := (mkf3 a b c).
+
+Definition project_p (p : R * R) : R ^ 3 :=
+  [ffun i => if val i == 0 then 1%R else if val i == 1 then p.1 else p.2].
+
+Definition surface_mx (t : (R * R)%type ^ 3) :=
+  (\matrix_(i < 3, j < 3) project_p (t i) j)%R.
+
+End num_computations.
+
+Section num_computations_comparison.
+
+Variable P : Type.
+
+Variable R : realDomainType.
+
+Variable coords : P -> R * R.
+
+Definition ccw0 (a b c : R * R) := (0 < \det (surface_mx (mkf3 a b c)))%R.
+
+Definition ccw (a b c : P) := ccw0 (coords a) (coords b) (coords c).
+
+End num_computations_comparison.
+
 Section abstract_over_types.
 
 Variable P : finType.
 
-Variable R : numDomainType.
+Variable R : realDomainType.
 
 Variable coords : P -> R * R.
 
@@ -22,20 +57,9 @@ Variable pick_set : {set P} -> option P.
 
 Variable pick_triangle : {set {set P}} -> P -> option {set P}.
 
-Definition mkf3 (T : Type) (a b c : T) :=
-  [ffun i : 'I_3 => if val i == 0 then a else if val i == 1 then b else c].
-
 Notation "<< a ; b ; c >>" := (mkf3 a b c).
 
-Definition project_p (p : P) : R ^ 3 :=
-  [ffun i =>
-     if val i == 0 then 1%R
-     else if val i == 1 then (coords p).1 else (coords p).2].
-
-Definition surface_mx (t : P ^ 3) :=
-  (\matrix_(i < 3, j < 3) project_p (t i) j)%R.
-
-Definition ccw (a b c : P) := (0 < \det (surface_mx << a; b; c>>))%R.
+Notation ccw := (ccw coords).
 
 Definition separated (t : {set P}) (q p : P) :=
   (q \in t) &&
@@ -280,15 +304,15 @@ Definition naive_triangulate' (s : {set P}) := naive_triangulate #|s| s.
 Definition flip_edge (t1 t2 : {set P}) :=
   [set x |: (t1 :\: t2) :|: (t2 :\: t1) | x in t1 :&: t2].
 
-Definition in_circle_l (p : P) : R ^ 4 :=
+Definition in_circle_l (p : R * R) : R ^ 4 :=
   [ffun i : 'I_4 =>
    if val i < 3 then
      project_p p (inord i)
    else
-    ((coords p).1 ^+ 2 + (coords p).2 ^+ 2)%R].
+    (p.1 ^+ 2 + p.2 ^+ 2)%R].
 
 Definition in_circle_mx (t : P ^ 4) :=
-  (\matrix_(i < 4, j < 4) in_circle_l (t i) j)%R.
+  (\matrix_(i < 4, j < 4) in_circle_l (coords (t i)) j)%R.