From 7dad05c8192311f0d646b8f25311bd0c167d7628 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 12 Nov 2018 15:46:52 -0500 Subject: Add support for parsing Q and bool Factors a bit of code out of PRs that are not yet merged --- src/Experiments/NewPipeline/CLI.v | 13 +++++++++++++ 1 file changed, 13 insertions(+) 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. -- cgit v1.2.3