forked from HIPERFIT/contracts
-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathExtraction.v
138 lines (112 loc) · 4.37 KB
/
Extraction.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
Require Import Denotational.
Require Import Reduction.
Require Import Horizon.
Require Import Templates.
Require Import Specialise.
Require Import TimedTyping.
Require Import ILTranslation.
Require Import ILSemantics.
Require Import CutPayoff.
Require Import Simplify.
Require Import Nat.
Require Import Days.
Require Import Misc.
Extraction Language Haskell.
Extract Inductive unit => "()" [ "()" ].
Extract Inductive bool => "Bool" [ "True" "False" ].
Extract Inductive sumbool => "Bool" [ "True" "False" ].
Extract Inlined Constant orb => "(||)".
Extract Inlined Constant andb => "(&&)".
Extract Inlined Constant compose => "(.)".
Extract Inductive list => "List" [ "[]" "(:)" ].
Extract Inlined Constant map => "P.map".
Extract Inlined Constant fold_right => "foldr".
Extract Inlined Constant concat => "concat".
Extract Inlined Constant concatMap => "concatMap".
Extract Inlined Constant flat_map => "concatMap".
Extract Inlined Constant app => "(++)".
Extract Inductive nat => "Int" ["0" "succ"] "(\fO fS n -> if n==0 then fO () else fS (n-1))".
Extract Inductive Z => "Int" ["0" "id" "negate"].
Extract Inductive positive => "Int" ["unused" "unused" "1"].
Extract Inlined Constant Z.leb => "(<=)".
Extract Inlined Constant Z.ltb => "(<)".
Extract Inlined Constant Z.add => "(+)".
Extract Inlined Constant Z.sub => "(-)".
Extract Inlined Constant Z.mul => "(*)".
Extract Inlined Constant Z.opp => "negate".
Extract Inlined Constant Z.max => "max".
Extract Inlined Constant Z.min => "min".
Extract Inlined Constant R => "Double".
Extract Inlined Constant Rleb => "(<=)".
Extract Inlined Constant Reqb => "(==)".
Extract Inlined Constant Req_dec => "(==)".
Extract Inlined Constant Rltb => "(<)".
Extract Inlined Constant Rplus => "(+)".
Extract Inlined Constant Rminus => "(-)".
Extract Inlined Constant Rmult => "(*)".
Extract Inlined Constant Rdiv => "(/)".
Extract Inlined Constant Ropp => "negate".
Extract Inlined Constant R1 => "1".
Extract Inlined Constant R0 => "0".
Extract Inlined Constant negb => "not".
Extract Inlined Constant Z.eqb => "(==)".
Extract Inlined Constant Nat.leb => "(<=)".
Extract Inlined Constant Nat.ltb => "(<)".
Extract Inductive prod => "(,)" [ "(,)" ].
Extract Inlined Constant fst => "fst".
Extract Inlined Constant snd => "snd".
Extract Inlined Constant plus => "(+)".
Extract Inlined Constant minus => "(-)".
Extract Inlined Constant max => "max".
Extract Inlined Constant Z.of_nat => "id".
Extract Inlined Constant Z.to_nat => "id".
Extract Inlined Constant Nat.eqb => "(==)".
Extract Inductive option => "Maybe" [ "Just" "Nothing" ].
Extract Constant option_rect => "flip maybe".
Extraction Inline option_rect option_rec.
Extract Inlined Constant bind => "(>>=)".
Extract Inlined Constant liftM => "liftM".
Extract Inlined Constant liftM2 => "liftM2".
Extract Inlined Constant liftM3 => "liftM3".
Extract Inlined Constant pure => "return".
Extract Inlined Constant sequence => "sequence".
Extract Inlined Constant mapM => "mapM".
Extract Inlined Constant default => "fromMaybe".
Extract Inductive sum => "Either" ["Left" "Right"].
Extract Inlined Constant Asset => "Asset".
Extract Inlined Constant Party => "Party".
Extract Inlined Constant BoolObs => "BoolObs".
Extract Inlined Constant RealObs => "RealObs".
Extract Inlined Constant Asset.eqb => "(==)".
Extract Inlined Constant Party.eqb => "(==)".
Extract Inlined Constant FMap.FMap => "FMap".
Extract Inlined Constant FMap.empty => "Map.empty".
Extract Inlined Constant FMap.add => "Map.insert".
Extract Inlined Constant FMap.find => "Map.lookup".
Extract Inlined Constant FMap.is_empty => "Map.null".
Extract Inlined Constant FMap.map => "Map.map".
Extract Inlined Constant FMap.union_with => "unionWith".
(* Coq extracts [SMap_rec] and [SMap.SMap_rect], even though they are
not used. The inlining commands below prevent that. *)
Extract Inlined Constant SMap.SMap_rec => "unused".
Extract Inlined Constant SMap.SMap_rect => "unused".
Extract Inlined Constant compare => "compare".
Extract Inductive comparison => "Ordering" [ "EQ" "LT" "GT"].
Extraction "Extraction/contracts-haskell/src/Contracts/ContractExtracted.hs"
transfDays
obsDays
lookupEnv
Contr
horizon
redfun
specialise
has_type
inst_contr
flat_map.
Extraction "Extraction/contracts-haskell/src/Contracts/ContractTranslationExtracted.hs"
fromExp
fromContr
fromExtEnv
cutPayoff
ILsem
simp_loopif.