diff options
Diffstat (limited to 'src/Experiments')
-rw-r--r-- | src/Experiments/NewPipeline/CLI.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/Experiments/NewPipeline/CLI.v b/src/Experiments/NewPipeline/CLI.v index 524def965..2b9dbdf23 100644 --- a/src/Experiments/NewPipeline/CLI.v +++ b/src/Experiments/NewPipeline/CLI.v @@ -1,3 +1,4 @@ +Require Import Coq.QArith.QArith. Require Import Coq.ZArith.ZArith. Require Import Coq.Strings.Ascii. Require Import Coq.Lists.List. @@ -31,6 +32,18 @@ Module ForExtraction. sgn * Z.of_N (parse_N s). Definition parse_nat (s : string) : nat := N.to_nat (parse_N s). + Definition parse_Q (s : string) : option Q + := match List.map parse_Z (String.split "/" s) with + | [num;Zpos den] => Some (Qmake num den) + | [num] => Some (Qmake num 1) + | _ => None + end. + Definition parse_bool (s : string) : option bool + := if string_dec s "true" + then Some true + else if string_dec s "false" + then Some false + else None. Definition parse_n (n : string) : nat := parse_nat n. |