source: extracted/option.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.0 KB
Line 
1open Preamble
2
3open Jmeq
4
5open Russell
6
7open Bool
8
9open Nat
10
11open List
12
13open Setoids
14
15open Relations
16
17open Hints_declaration
18
19open Core_notation
20
21open Pts
22
23open Logic
24
25open Types
26
27open Monad
28
29(** val option0 : Monad.monadProps **)
30let option0 =
31  Monad.makeMonadProps (fun _ x -> Types.Some x) (fun _ _ m f ->
32    match m with
33    | Types.None -> Types.None
34    | Types.Some x -> f x)
35
36(** val opt_safe : 'a1 Types.option -> 'a1 **)
37let opt_safe m =
38  (match m with
39   | Types.None -> (fun _ -> Logic.false_rect_Type0 __)
40   | Types.Some t -> (fun _ -> t)) __
41
42(** val opt_try_catch : 'a1 Types.option -> (Types.unit0 -> 'a1) -> 'a1 **)
43let opt_try_catch m f =
44  match m with
45  | Types.None -> f Types.It
46  | Types.Some x -> x
47
48(** val optPred : Monad.injMonadPred **)
49let optPred =
50  { Monad.im_pred = Monad.Mk_MonadPred; Monad.mp_inject = (fun _ _ m_sig ->
51    let m = m_sig in
52    (match Obj.magic m with
53     | Types.None -> (fun _ -> Obj.magic Types.None)
54     | Types.Some x -> (fun _ -> Obj.magic (Types.Some x))) __) }
55
Note: See TracBrowser for help on using the repository browser.