source: extracted/graphs.ml @ 2601

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

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

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