source: extracted/graphs.ml @ 2746

Last change on this file since 2746 was 2717, checked in by sacerdot, 7 years ago

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

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