legacy/oldfan/ch_fan/fan_definition.hl

   1 hypermap_tybij;;
   2 type_of `tuple_hypermap`;;
   3 type_of `hypermap`;;
   4 restrict;;
   5
   6 (* restriction of a function to a domain, identity outside domain *)
   7
   8 let restrict = define `restrict (f:A->A) X = (\x. if (X x) then (f x) else x)`;;
   9
  10 (* essentailly the same as fan.ml set_of_edges
  11
  12 let edge_at =  define `edge_at (V,E) v = { w | E {v,w} }`;;  (* set_of_edges v E *)
  13 *)
  14
  15 let dart_set =
  16   define `dart_set (V,E) = ({(v,v) | set_of_edges v E = EMPTY} UNION {(v,w) | E {v,w} })`;;
  17
  18 (* check order of args in sigma_fan fan.ml *)
  19
  20 let face_map_of_fan =
  21     define `face_map_of_fan' (V,E) (v,w) =
  22     if (E {v,w}) then (w,inverse_sigma_fan (vec 0) V E w v) else (v,w)`;;
  23
  24 let edge_map_of_fan =
  25    define `edge_map_of_fan (V,E) (v,w) = (w,v)`;;
  26
  27 let node_map_of_fan =
  28      define `node_map_of_fan (V,E) (v,w) = (v,sigma_fan (vec 0) V E v w)`;;
  29
  30 (* text:hyp(V,E) *)
  31
  32 let hyp_of_fano  = define `hyp_of_fano (V,E) =
  33   (let D = dart_set (V,E) in
  34    hypermap( D   ,(restrict (edge_map_of_fan (V,E)) D  )  ,
  35    (restrict (node_map_of_fan (V,E)) D)  ,
  36   (restrict (face_map_of_fan (V,E)) D) ))`;;
  37