forked from mit-plv/koika
-
Notifications
You must be signed in to change notification settings - Fork 0
/
ExtractionSetup.v
56 lines (51 loc) · 3.29 KB
/
ExtractionSetup.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
(*! Interop | Custom extraction settings (also used by external Kôika programs !*)
Require Export Coq.extraction.Extraction.
From Coq.extraction Require Export ExtrOcamlBasic ExtrOcamlString ExtrOcamlNatInt ExtrOcamlZInt.
Require Koika.Types
Koika.TypedSyntaxFunctions
Koika.CircuitGeneration
Koika.CircuitOptimization.
(* The following commands work around problems due to incorrect extraction: *)
Extraction Inline Koika.CircuitGeneration.retVal.
Extraction Inline Types.argSigs.
Extract Constant Vect.index => int.
Extract Inductive Vect.index' => int [ "0" "Pervasives.succ" ]
"(fun fthisone fanotherone n -> if n = 0 then fthisone () else fanotherone (n - 1))".
Extract Constant Vect.index_of_nat => "fun sz x -> if x < sz then Some x else None".
Extract Constant Vect.index_to_nat => "fun _ x -> x".
Extract Constant Vect.largest_index => "fun x -> x".
(* This command makes extraction a bit more predictable *)
Global Set Extraction KeepSingleton.
(* The following commands make these functions much easier to use from the OCaml
side by removing unnecessary arguments. *)
Extraction Implicit CircuitOptimization.unannot [CR CSigma rwdata].
Extraction Implicit CircuitOptimization.lco_iter [csigma].
Extraction Implicit CircuitOptimization.lco_compose [csigma].
Extraction Implicit CircuitOptimization.lco_constprop [csigma].
Extraction Implicit CircuitOptimization.lco_identical [csigma].
Extraction Implicit CircuitOptimization.lco_muxelim [csigma].
Extraction Implicit CircuitOptimization.lco_simplify [csigma].
Extraction Implicit CircuitOptimization.lco_partialeval [csigma].
Extraction Implicit CircuitOptimization.lco_all [csigma].
Extraction Implicit CircuitOptimization.lco_all_iterated [csigma].
Extraction Implicit CircuitOptimization.unannot [CR CSigma rwdata].
Extraction Implicit TypedSyntaxFunctions.unannot [R Sigma sig tau].
Extraction Implicit TypedSyntaxFunctions.AnyAction [sig tau].
Extraction Implicit TypedSyntaxFunctions.action_footprint [R Sigma sig tau].
Extraction Implicit TypedSyntaxFunctions.action_footprint' [R Sigma sig tau].
Extraction Implicit TypedSyntaxFunctions.action_mentions_var [R Sigma sig tau].
Extraction Implicit TypedSyntaxFunctions.annotate_action_register_histories [Sigma sig tau].
Extraction Implicit TypedSyntaxFunctions.annotate_rule_register_histories [Sigma].
Extraction Implicit TypedSyntaxFunctions.compute_register_histories [Sigma].
Extraction Implicit TypedSyntaxFunctions.rule_max_log_size [R Sigma sig tau].
Extraction Implicit TypedSyntaxFunctions.action_mentions_shadowed_var [R Sigma sig tau].
Extraction Implicit TypedSyntaxFunctions.existsb_subterm [R Sigma sig tau].
Extraction Implicit TypedSyntaxFunctions.returns_zero [R Sigma sig tau].
Extraction Implicit TypedSyntaxFunctions.is_pure [R Sigma sig tau].
Extraction Implicit TypedSyntaxFunctions.is_tt [R Sigma sig tau].
Extraction Implicit TypedSyntaxFunctions.action_type [R Sigma sig tau].
Extraction Implicit TypedSyntaxFunctions.interp_arithmetic [R Sigma sig tau].
Extraction Implicit LoweredSyntaxFunctions.action_footprint [R Sigma sig tau].
Extraction Implicit LoweredSyntaxFunctions.action_footprint' [R Sigma sig tau].
Extraction Implicit TypedSyntaxFunctions.find_read1s_after_write1s' [R Sigma sig tau].
Extraction Implicit TypedSyntaxFunctions.find_read1s_after_write1s [R Sigma sig tau].