source: extracted/foldStuff.ml @ 2746

Last change on this file since 2746 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.6 KB
Line 
1open Preamble
2
3open Div_and_mod
4
5open Jmeq
6
7open Russell
8
9open Bool
10
11open Relations
12
13open Nat
14
15open Hints_declaration
16
17open Core_notation
18
19open Pts
20
21open Logic
22
23open Types
24
25open List
26
27open Util
28
29(** val foldl_strong_internal :
30    'a1 List.list -> ('a1 List.list -> 'a1 -> 'a1 List.list -> __ -> 'a2 ->
31    'a2) -> 'a1 List.list -> 'a1 List.list -> 'a2 -> 'a2 **)
32let rec foldl_strong_internal l h prefix0 suffix acc =
33  (match suffix with
34   | List.Nil ->
35     (fun _ ->
36       Util.eq_rect_Type0_r0 prefix0 acc (List.append prefix0 List.Nil))
37   | List.Cons (hd0, tl) ->
38     (fun _ ->
39       Logic.eq_coerc
40         (foldl_strong_internal l h
41           (List.append prefix0 (List.Cons (hd0, List.Nil))) tl
42           (h prefix0 hd0 tl __ acc)))) __
43
44(** val foldl_strong :
45    'a1 List.list -> ('a1 List.list -> 'a1 -> 'a1 List.list -> __ -> 'a2 ->
46    'a2) -> 'a2 -> 'a2 **)
47let foldl_strong l h acc =
48  foldl_strong_internal l h List.Nil l acc
49
50(** val foldr_strong_internal :
51    'a1 List.list -> ('a1 List.list -> 'a1 -> 'a1 List.list -> __ -> 'a2 ->
52    'a2) -> 'a1 List.list -> 'a1 List.list -> 'a2 -> 'a2 **)
53let rec foldr_strong_internal l h prefix0 suffix acc =
54  (match suffix with
55   | List.Nil -> (fun _ -> acc)
56   | List.Cons (hd0, tl) ->
57     (fun _ ->
58       h prefix0 hd0 tl __
59         (foldr_strong_internal l h
60           (List.append prefix0 (List.Cons (hd0, List.Nil))) tl acc))) __
61
62(** val foldr_strong :
63    'a1 List.list -> ('a1 List.list -> 'a1 -> 'a1 List.list -> __ -> 'a2 ->
64    'a2) -> 'a2 -> 'a2 **)
65let foldr_strong l h acc =
66  foldr_strong_internal l h List.Nil l acc
67
Note: See TracBrowser for help on using the repository browser.