sync with flavor

.gitignore

@@ -8,3 +8,7 @@
 Makefile.coq
 Makefile.coq.conf
 .Makefile.coq.d
+www/*.cmo
+www/*.cmi
+www/*.bytes
+www/*.js

theories/generic_trajectories.v

@@ -664,6 +664,22 @@ end.
 Definition path_reverse (s : seq (annotated_point * annotated_point)) :=
   List.map (fun p => (snd p, fst p)) (List.rev_append s nil).
 
+Definition strict_inside_closed p c :=
+  negb (point_under_edge p (low c)) &&
+  point_strictly_under_edge p (high c) &&
+ (R_ltb (left_limit c) (p_x p) &&
+ (R_ltb (p_x p) (right_limit c))).
+
+Definition safe_intermediate_point_in_cell (p1 p2 : pt) (c : cell)
+   (ci : nat) :=
+  let new_x := p_x (cell_center c) in
+  let new_y := R_div (R_add (p_y p1) (p_y p2)) R2 in
+  let new_pt := {|p_x := new_x; p_y := new_y|} in
+    if strict_inside_closed new_pt c then
+      Apt new_pt (ci :: nil)
+    else
+      Apt (cell_center c) (ci :: nil).
+
 (* This function creates a safe path from the door between
   c1 and c2 and the door between c2 and c3.  When op1 and op2
   are not provided, midpoints are used as path anchors,
@@ -691,8 +707,7 @@ let p2 := match op2 with
             end
           end in
 if R_eqb (p_x p1) (p_x p2) then
-  let intermediate_point :=
-    Apt (cell_center c2) (c2i :: nil) in
+  let intermediate_point :=  safe_intermediate_point_in_cell p1 p2 c2 c2i in
   (Apt p1 (c1i :: c2i :: nil), intermediate_point) ::
   (intermediate_point, Apt p2 (c2i :: c3i :: nil)) :: nil
 else
@@ -739,12 +754,6 @@ Definition path_adjacent_cells (cells : seq cell) (source target : pt)
   | None => None
   end.
 
-Definition strict_inside_closed p c :=
-  negb (point_under_edge p (low c)) &&
-  point_strictly_under_edge p (high c) &&
- (R_ltb (left_limit c) (p_x p) &&
- (R_ltb (p_x p) (right_limit c))).
-
 (* find_origin_cells returns a list of cell indices. *)
 (* If the list is empty, it should mean that the point is not in the
   safe part of the work space (it is either outside the box or on

theories/shortest_path.v

@@ -0,0 +1,67 @@
+From mathcomp Require Import all_ssreflect all_algebra.
+Require Import ZArith List String OrderedType OrderedTypeEx FMapAVL.
+
+Notation head := seq.head.
+Notation seq := seq.seq.
+Notation sort := path.sort.
+
+Section shortest_path.
+
+Variable R : numFieldType.
+Variable cell : Type.
+Variable cells : seq cell.
+Variable node : eqType.
+Variable neighbors_of_node : node -> seq (node * R).
+Variable source target : node.
+
+Definition path := seq node.
+Variable priority_queue : Type.
+Variable empty : priority_queue.
+Variable find : priority_queue -> node -> option (path * option R).
+Variable update : priority_queue -> node -> path -> option R -> priority_queue.
+Variable pop :  priority_queue -> option (node * path * option R * priority_queue).
+
+Definition cmp_option (v v' : option R) :=
+  if v is Some x then
+    if v' is Some y then
+       (x < y)%O
+    else
+      true
+   else
+     false.
+
+Definition Dijkstra_step (d : node) (p : seq node) (dist : R)
+  (q : priority_queue) : priority_queue :=
+  let neighbors := neighbors_of_node d in
+  foldr (fun '(d', dist') q => 
+           match find q d' with
+           | None => q
+           | Some (p', o_dist) =>
+             let new_dist_to_d' := Some (dist + dist')%R in
+             if cmp_option new_dist_to_d' o_dist then
+                update q d' (d :: p) new_dist_to_d'
+             else q
+           end) q neighbors.
+
+Fixpoint Dijkstra (fuel : nat) (q : priority_queue) :=
+  match fuel with
+  | 0 => None
+  |S fuel' =>
+    match pop q with
+    | Some (d, p, Some dist, q') =>
+      if d == target then Some p else 
+        Dijkstra fuel' (Dijkstra_step d p dist q')
+    | _ => None
+    end
+  end.
+
+Definition shortest_path (s : seq node) :=
+  Dijkstra (size s)
+    (foldr [fun n q => update q n [::] None] empty s).
+
+Definition neighbors_of_node (d : node) :  seq (node * R) :=
+  let (c1, c2) := node_to_cells d in
+  let ds1 := cell_to_nodes c1 in
+  let ds2 := cell_to_nodes c2 in
+  let ds := undup [seq x | x <- ds1 ++ ds2 & x != d] in
+  [seq (x, node_distance d x) | x <- ds].

www/Add.html

@@ -0,0 +1,30 @@
+
+
+<HTML>
+
+    <HEAD>
+
+        <TITLE>Add</TITLE>
+
+    </HEAD><BODY>
+
+        <H1> Add </H1>
+
+        <p>
+	        <script src="Add.js"></script>
+	        <script src="AddScript.js"></script>
+  </div>
+  <div>
+    <textarea id="text" name="text"
+          rows="1" cols="33">
+1 2 1 2 
+</textarea>
+<p>
+  <button onclick="myadd()" class="Clear"> Test </button>
+ </div>
+</div>
+        </p>
+
+    </BODY>
+
+</HTML>