blob: a642a10064abc54ce0577edadc72b13c3c6b60b7 (
plain)
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
|
Require Export Coq.extraction.Extraction.
Require Export Coq.extraction.ExtrOcamlBasic.
Require Export Coq.extraction.ExtrOcamlString.
Require Import Coq.Lists.List.
Require Import Coq.Strings.Ascii.
Require Import Coq.Strings.String.
Require Crypto.Util.Strings.String.
Require Import Crypto.Util.Strings.Decimal.
Require Import Crypto.Util.Strings.HexString.
Require Import Crypto.Experiments.NewPipeline.PushButtonSynthesis.
Require Import Crypto.Experiments.NewPipeline.CLI.
Require Import Crypto.Util.Notations.
Import ListNotations. Local Open Scope string_scope.
Global Set Warnings Append "-extraction-opaque-accessed".
Extraction Language Ocaml.
Global Unset Extraction Optimize.
Inductive int : Set := int_O | int_S (x : int).
Axiom printf_char : Ascii.ascii -> unit.
Axiom flush : unit -> unit.
Axiom string : Set.
Axiom string_length : string -> int.
Axiom string_get : string -> int -> Ascii.ascii.
Axiom sys_argv : list string.
Axiom string_init : int -> (int -> Ascii.ascii) -> string.
Axiom raise_Failure : forall A, string -> A.
Extract Inductive int
=> int [ "0" "Pervasives.succ" ]
"(fun fO fS n -> if n=0 then fO () else fS (n-1))".
Extract Constant printf_char =>
"fun c -> Printf.printf ""%c%!"" c".
Extract Constant flush =>
"fun () -> Printf.printf ""%!""".
Extract Inlined Constant string => "string".
Extract Inlined Constant string_length => "String.length".
Extract Inlined Constant string_get => "String.get".
Extract Constant sys_argv => "Array.to_list Sys.argv".
Extract Inlined Constant string_init => "String.init".
Extract Constant raise_Failure => "fun x -> raise (Failure x)".
Fixpoint nat_of_int (x : int) : nat
:= match x with
| int_O => O
| int_S x' => S (nat_of_int x')
end.
Fixpoint int_of_nat (x : nat) : int
:= match x with
| O => int_O
| S x' => int_S (int_of_nat x')
end.
Coercion nat_of_int : int >-> nat.
Coercion int_of_nat : nat >-> int.
Definition string_of_Coq_string (s : String.string) : string
:= let s := String.to_list s in
string_init
(List.length s)
(fun n => List.nth n s "?"%char).
Definition string_to_Coq_string (s : string) : String.string
:= String.of_list
(List.map (fun n:nat => string_get s n) (List.seq 0 (string_length s))).
Definition seq {A B} (x : unit -> A) (f : A -> B) : B := let y := x tt in f y.
Extraction NoInline seq.
(*
Axiom seq : forall A B, (unit -> A) -> (A -> B) -> B.
Extract Inlined Constant seq => "(fun x f => let y = x () in f y)".
*)
Fixpoint list_iter {A} (f : A -> unit) (ls : list A) : unit
:= match ls with
| cons x xs => seq (fun _ => f x) (fun _ => @list_iter A f xs)
| nil => tt
end.
Definition printf_list_string (strs : list String.string) : unit
:= list_iter
(fun ls
=> list_iter printf_char (String.to_list ls))
strs.
Definition printf_list_string_with_newlines (strs : list String.string) : unit
:= match strs with
| nil => printf_list_string nil
| str :: strs => printf_list_string (str :: List.map (String.String Ascii.NewLine) strs
++ [String.NewLine; String.NewLine])%list
end.
Definition raise_failure {A} (msg : list String.string) : A
:= seq (fun _ => printf_list_string_with_newlines msg)
(fun _ => raise_Failure _ (string_of_Coq_string "Synthesis failed")).
Module UnsaturatedSolinas.
Definition main : unit
:= let argv := List.map string_to_Coq_string sys_argv in
ForExtraction.UnsaturatedSolinas.PipelineMain
argv
printf_list_string
raise_failure.
End UnsaturatedSolinas.
Module WordByWordMontgomery.
Definition main : unit
:= let argv := List.map string_to_Coq_string sys_argv in
ForExtraction.WordByWordMontgomery.PipelineMain
argv
printf_list_string
raise_failure.
End WordByWordMontgomery.
Module SaturatedSolinas.
Definition main : unit
:= let argv := List.map string_to_Coq_string sys_argv in
ForExtraction.SaturatedSolinas.PipelineMain
argv
printf_list_string
raise_failure.
End SaturatedSolinas.
|