extracted/graphs.ml

   1 open Preamble
   2
   3 open Hints_declaration
   4
   5 open Core_notation
   6
   7 open Pts
   8
   9 open Logic
  10
  11 open Types
  12
  13 open Deqsets
  14
  15 open Setoids
  16
  17 open Monad
  18
  19 open Option
  20
  21 open Extranat
  22
  23 open Vector
  24
  25 open Div_and_mod
  26
  27 open Jmeq
  28
  29 open Russell
  30
  31 open List
  32
  33 open Util
  34
  35 open FoldStuff
  36
  37 open Bool
  38
  39 open Relations
  40
  41 open Nat
  42
  43 open BitVector
  44
  45 open BitVectorTrie
  46
  47 open Proper
  48
  49 open PositiveMap
  50
  51 open ErrorMessages
  52
  53 open PreIdentifiers
  54
  55 open Errors
  56
  57 open Extralib
  58
  59 open Lists
  60
  61 open Positive
  62
  63 open Identifiers
  64
  65 open Exp
  66
  67 open Arithmetic
  68
  69 open Integers
  70
  71 open AST
  72
  73 type label = PreIdentifiers.identifier
  74
  75 (** val label_to_ident : label -> AST.ident **)
  76 let label_to_ident l =
  77   let l0 = l in l0
  78
  79 (** val label_eq : label -> label -> (__, __) Types.sum **)
  80 let label_eq =
  81   Identifiers.identifier_eq PreIdentifiers.LabelTag
  82
  83 type 'x graph = 'x Identifiers.identifier_map
  84
  85 (** val graph_fold :
  86     (Positive.pos -> 'a1 -> 'a2 -> 'a2) -> 'a1 graph -> 'a2 -> 'a2 **)
  87 let graph_fold f graph0 seed =
  88   let map = graph0 in PositiveMap.fold f map seed
  89
  90 (** val graph_num_nodes : 'a1 graph -> Nat.nat **)
  91 let graph_num_nodes g =
  92   Identifiers.id_map_size PreIdentifiers.LabelTag g
  93