source: extracted/costLabel.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: 785 bytes
Line 
1open Preamble
2
3open Proper
4
5open PositiveMap
6
7open Deqsets
8
9open PreIdentifiers
10
11open Errors
12
13open Extralib
14
15open Setoids
16
17open Monad
18
19open Option
20
21open Lists
22
23open Positive
24
25open Identifiers
26
27open Coqlib
28
29open Floats
30
31open Arithmetic
32
33open Char
34
35open String
36
37open Vector
38
39open Div_and_mod
40
41open Jmeq
42
43open Russell
44
45open List
46
47open Util
48
49open FoldStuff
50
51open BitVector
52
53open Extranat
54
55open Bool
56
57open Relations
58
59open Nat
60
61open Integers
62
63open Hints_declaration
64
65open Core_notation
66
67open Pts
68
69open Logic
70
71open Types
72
73open AST
74
75(** val costTag : String.string **)
76let costTag = "cost tag"
77  (*failwith "AXIOM TO BE REALIZED"*)
78
79type costlabel = PreIdentifiers.identifier
80
81(** val costlabel_of_nat : Nat.nat -> costlabel **)
82let costlabel_of_nat =
83  Identifiers.identifier_of_nat costTag
84
Note: See TracBrowser for help on using the repository browser.