По-видимому, вы предполагаете, что существует такая вещь, как функция div
. В голом Coq, без загруженной библиотеки, такой функции не существует.
Чтобы иметь функцию, которая выглядит как деление натуральных чисел, я предлагаю вам загрузить библиотеку Arith
. Тогда вам будет разрешено использовать обозначение a / b
для деления.
Вот пример:
Require Import Arith.
Check (fun x y => x / y).
(* this returns : fun x y : nat => x / y : nat -> nat -> nat *)
Compute (12 / 5).
(* this returns : = 2 : nat *)
Locate "_ / _".
(* this returns : "x / y" := Nat.div x y : nat_scope *)
Я до сих пор не понимаю, что вы подразумеваете под минимумом и максимумом группы, но, по крайней мере, вы сможете написать некоторый код Coq, который будет принят по системе.
Вот regex, который обработает все данные, которые я могу бросить в него:
(\d++(?! */))? *-? *(?:(\d+) */ *(\d+))?.*$
Это поместит цифры в следующие группы:
Кроме того, вот объяснение RegexBuddy элементов (который помог мне очень при построении его):
Match the regular expression below and capture its match into backreference number 1 «(\d++(?! */))?»
Between zero and one times, as many times as possible, giving back as needed (greedy) «?»
Match a single digit 0..9 «\d++»
Between one and unlimited times, as many times as possible, without giving back (possessive) «++»
Assert that it is impossible to match the regex below starting at this position (negative lookahead) «(?! */)»
Match the character “ ” literally « *»
Between zero and unlimited times, as many times as possible, giving back as needed (greedy) «*»
Match the character “/” literally «/»
Match the character “ ” literally « *»
Between zero and unlimited times, as many times as possible, giving back as needed (greedy) «*»
Match the character “-” literally «-?»
Between zero and one times, as many times as possible, giving back as needed (greedy) «?»
Match the character “ ” literally « *»
Between zero and unlimited times, as many times as possible, giving back as needed (greedy) «*»
Match the regular expression below «(?:(\d+) */ *(\d+))?»
Between zero and one times, as many times as possible, giving back as needed (greedy) «?»
Match the regular expression below and capture its match into backreference number 2 «(\d+)»
Match a single digit 0..9 «\d+»
Between one and unlimited times, as many times as possible, giving back as needed (greedy) «+»
Match the character “ ” literally « *»
Between zero and unlimited times, as many times as possible, giving back as needed (greedy) «*»
Match the character “/” literally «/»
Match the character “ ” literally « *»
Between zero and unlimited times, as many times as possible, giving back as needed (greedy) «*»
Match the regular expression below and capture its match into backreference number 3 «(\d+)»
Match a single digit 0..9 «\d+»
Between one and unlimited times, as many times as possible, giving back as needed (greedy) «+»
Match any single character that is not a line break character «.*»
Between zero and unlimited times, as many times as possible, giving back as needed (greedy) «*»
Assert position at the end of the string (or before the line break at the end of the string, if any) «$»
Я думаю, что может быть легче заняться различными случаями (полный смешанный, фракционироваться только, только число) отдельно друг от друга. Например:
sub parse_mixed {
my($mixed) = @_;
if($mixed =~ /^ *(\d+)[- ]+(\d+) *\/ *(\d)+(\D.*)?$/) {
return $1+$2/$3;
} elsif($mixed =~ /^ *(\d+) *\/ *(\d+)(\D.*)?$/) {
return $1/$2;
} elsif($mixed =~ /^ *(\d+)(\D.*)?$/) {
return $1;
}
}
print parse_mixed("10"), "\n";
print parse_mixed("1/3"), "\n";
print parse_mixed("1 / 3"), "\n";
print parse_mixed("10 1/3"), "\n";
print parse_mixed("10-1/3"), "\n";
print parse_mixed("10 - 1/3"), "\n";
Если Вы используете Perl 5.10
, это - то, как я записал бы это.
m{ ^ \s* # skip leading spaces (?'whole' \d++ (?! \s*[\/] ) # there should not be a slash immediately following a whole number ) \s* (?: # the rest should fail or succeed as a group -? # ignore possible neg sign \s* (?'numerator' \d+ ) \s* [\/] \s* (?'denominator' \d+ ) )? }x
Затем можно получить доступ к значениям от %+
переменная как это:
$+{whole};
$+{numerator};
$+{denominator};