source: extracted/listb.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.1 KB
Line 
1open Preamble
2
3open Bool
4
5open Relations
6
7open Nat
8
9open Hints_declaration
10
11open Core_notation
12
13open Pts
14
15open Logic
16
17open Types
18
19open List
20
21open Sets
22
23open Deqsets
24
25(** val isnilb : 'a1 List.list -> Bool.bool **)
26let rec isnilb = function
27| List.Nil -> Bool.True
28| List.Cons (hd0, tl) -> Bool.False
29
30(** val memb : Deqsets.deqSet -> __ -> __ List.list -> Bool.bool **)
31let rec memb s x = function
32| List.Nil -> Bool.False
33| List.Cons (a, tl) -> Bool.orb (Deqsets.eqb s x a) (memb s x tl)
34
35(** val uniqueb : Deqsets.deqSet -> __ List.list -> Bool.bool **)
36let rec uniqueb s = function
37| List.Nil -> Bool.True
38| List.Cons (a, tl) -> Bool.andb (Bool.notb (memb s a tl)) (uniqueb s tl)
39
40(** val unique_append :
41    Deqsets.deqSet -> __ List.list -> __ List.list -> __ List.list **)
42let rec unique_append s l1 l2 =
43  match l1 with
44  | List.Nil -> l2
45  | List.Cons (a, tl) ->
46    let r = unique_append s tl l2 in
47    (match memb s a r with
48     | Bool.True -> r
49     | Bool.False -> List.Cons (a, r))
50
51(** val exists0 : ('a1 -> Bool.bool) -> 'a1 List.list -> Bool.bool **)
52let rec exists0 p = function
53| List.Nil -> Bool.False
54| List.Cons (h, t) -> Bool.orb (p h) (exists0 p t)
55
Note: See TracBrowser for help on using the repository browser.