hypermap_tybij;;
type_of `tuple_hypermap`;;
type_of `hypermap`;;
restrict;;

(* restriction of a function to a domain, identity outside domain *)

let restrict = define `restrict (f:A->A) X = (\x. if (X x) then (f x) else x)`;;

(* essentailly the same as fan.ml set_of_edges 

let edge_at =  define `edge_at (V,E) v = { w | E {v,w} }`;;  (* set_of_edges v E *)
*)

let dart_set = 
  define `dart_set (V,E) = ({(v,v) | set_of_edges v E = EMPTY} UNION {(v,w) | E {v,w} })`;;

(* check order of args in sigma_fan fan.ml *)

let face_map_of_fan = 
    define `face_map_of_fan' (V,E) (v,w) =
    if (E {v,w}) then (w,inverse_sigma_fan (vec 0) V E w v) else (v,w)`;; 

let edge_map_of_fan = 
   define `edge_map_of_fan (V,E) (v,w) = (w,v)`;;

let node_map_of_fan = 
     define `node_map_of_fan (V,E) (v,w) = (v,sigma_fan (vec 0) V E v w)`;;

(* text:hyp(V,E) *)

let hyp_of_fano  = define `hyp_of_fano (V,E) = 
  (let D = dart_set (V,E) in 
   hypermap( D   ,(restrict (edge_map_of_fan (V,E)) D  )  , 
   (restrict (node_map_of_fan (V,E)) D)  , 
  (restrict (face_map_of_fan (V,E)) D) ))`;;