Skip to Content.
Sympa Menu

ssreflect - Re: [ssreflect] Running computations inside Coq

Subject: Ssreflect Users Discussion List

List archive

Re: [ssreflect] Running computations inside Coq


Chronological Thread 
  • From: Felipe Cerqueira <>
  • To: "" <>
  • Subject: Re: [ssreflect] Running computations inside Coq
  • Date: Sat, 6 Feb 2016 11:54:32 +0100
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None ; spf=Pass ; spf=None
  • Ironport-phdr: 9a23:HGowVBReqQeA9/M8MXBpMSqW8tpsv+yvbD5Q0YIujvd0So/mwa64bBeN2/xhgRfzUJnB7Loc0qyN4/+mAzBLuMbJmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbvipNuJP04R1HKUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGfayQ6NtB6dDFjkoN20++OXurgOGTA2V53JaU2MMkxMODRKPpEXhRY38vC/3vfZV3TKAeMzwV7E9HzWk9aZiDhHy3nQpLTk8pU/ajs1ogepwrQi4uhF+2YecNI+YMPtmc6j1eMsbAHFeRYBWTSMXUdD0VJcGE+dUZbUQlIL6vVZb9RY=
Hi Emilio,

thanks for your help.

On 2/6/16 1:17 AM, Emilio Jesús Gallego Arias wrote:
Indeed it should be possible, but some times it can get a bit painful
depending on what abstractions you use.

For instance, I use the following hack to run `finset` specified
programs using a MSetAVL version:

,----
| Definition eqS e i := forall x, reflect (In x e) (x \in i).
|
| Lemma unionE e1 e2 i1 i2 (h1 : eqS e1 i1) (h2 : eqS e2 i2) :
|   eqS (union e1 e2) (i1 :|: i2).
|
| etc...
`----

It works but is a (worthwhile) pain.

When you provide these reflection lemmas, does it help with the Eval of the computation?
Is it somehow automatic? I didn't understand the general idea.



Currently I get a very long output like this:

Could you post the Coq producing that output?

I'm afraid it may be hard to understand where the  computation is
getting stuck just from that output snippet.

Best regards,
Emilio

The code depends on many definitions across different files,
but to simplify it's just an iter applying map to a list.
The functions that I apply are mostly based on \sum , +, -, div.

  Let initial_state := fun ts => [seq (tsk, task_cost tsk) | tsk <- ts].  

  Let max_steps :=  fun ts => \sum_(tsk <- ts) (task_deadline tsk - task_cost tsk) + 1.

  Let function_that_hangs (ts: taskset) :=
    iter (max_steps ts)
      (edf_rta_iteration task_cost task_period task_deadline num_cpus)
      (initial_state ts).

I was not able to pinpoint where the computation stops, but after looking at the end of the file
it really seems to be the big sum operator (\big plus): http://pastebin.com/73V4t6Vh

In fact, it I run this code,

    Require Import ssreflect ssrbool ssrnat eqtype seq bigop.

    Let l := [:: 1; 2; 3].
    Eval compute in (\sum_(x <- l) x).

I get the following output:

 = \big[(fix plus (n m : nat) {struct n} : nat :=
               match n with
               | 0 => m
               | p.+1 => (plus p m).+1
               end)/0]_(x <- [:: 1; 2; 3]) x
     : nat

I don't know if the canonical structures affect the computation somehow.
Is there any easy way to make these big operators output-friendly?

Thanks,
Felipe
= if (fix all (s : seq (concrete_task * nat)) : bool :=
match s with
| [::] => true
| x :: s' =>
if let (tsk, R) := x in
(fix eqn (m n : nat) {struct m} : bool :=
match m with
| 0 => match n with
| 0 => true
| _.+1 => false
end
| m'.+1 =>
match n with
| 0 => false
| n'.+1 => eqn m' n'
end
end)
((fix minus (n m : nat) {struct n} : nat :=
match n with
| 0 => n
| k.+1 =>
match m with
| 0 => n
| l.+1 => minus k l
end
end) R
(let (_, _, task_deadline) := tsk in task_deadline))
0
then all s'
else false
end)
((fix loop (m : nat) : seq (concrete_task * nat) :=
match m with
| 0 =>
[:: ({|
task_cost := 1;
task_period := 10;
task_deadline := 10 |}, 1);
({|
task_cost := 2;
task_period := 10;
task_deadline := 10 |}, 2);
({|
task_cost := 3;
task_period := 10;
task_deadline := 10 |}, 3)]
| i.+1 =>
(fix map (s : seq (concrete_task * nat)) :
seq (concrete_task * nat) :=
match s with
| [::] => [::]
| x :: s' =>
(let (tsk, R) := x in
(tsk,
(fix plus (n m0 : nat) {struct n} : nat :=
match n with
| 0 => m0
| p.+1 => (plus p m0).+1
end)
(let (task_cost, _, _) := tsk in task_cost)
(let (x0, _) :=
(fix loop0 (m0 q : nat) {struct m0} :
nat * nat :=
match
(fix minus
(n m1 : nat) {struct n} : nat :=
match n with
| 0 => n
| k.+1 =>
match m1 with
| 0 => n
| l.+1 => minus k l
end
end) m0 1
with
| 0 => (q, m0)
| m'.+1 => loop0 m' q.+1
end)
(\big[(fix plus
(n m0 : nat) {struct n} : nat :=
match n with
| 0 => m0
| p.+1 => (plus p m0).+1
end)/0]_(i0 <-
loop i | let '
(tsk_other, _) := i0 in
if if
if
(fix eqn
(m0 n : nat) {struct m0} :
bool :=
match m0 with
| 0 =>
match n with
| 0 => true
| _.+1 => false
end
| m'.+1 =>
match n with
| 0 => false
| n'.+1 => eqn m' n'
end
end)
(let
(task_cost, _, _) :=
tsk_other in
task_cost)
(let
(task_cost, _, _) := tsk in
task_cost)
then
(fix eqn
(m0 n : nat) {struct m0} :
bool :=
match m0 with
| 0 =>
match n with
| 0 => true
| _.+1 => false
end
| m'.+1 =>
match n with
| 0 => false
| n'.+1 => eqn m' n'
end
end)
(let
(_, task_period, _) :=
tsk_other in
task_period)
(let
(_, task_period, _) :=
tsk in
task_period)
else false
then
(fix eqn
(m0 n : nat) {struct m0} :
bool :=
match m0 with
| 0 =>
match n with
| 0 => true
| _.+1 => false
end
| m'.+1 =>
match n with
| 0 => false
| n'.+1 => eqn m' n'
end
end)
(let
(_, _, task_deadline) :=
tsk_other in
task_deadline)
(let
(_, _, task_deadline) :=
tsk in
task_deadline)
else false
then false
else true)
(let '(tsk_other, R_other) := i0 in
if (fix eqn
(m0 n : nat) {struct m0} :
bool :=
match m0 with
| 0 =>
match n with
| 0 => true
| _.+1 => false
end
| m'.+1 =>
match n with
| 0 => false
| n'.+1 => eqn m' n'
end
end)
match
(fix plus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => m0
| p.+1 => (plus p m0).+1
end)
((fix mult
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => 0
| p.+1 =>
(fix plus
(n0 m1 : nat) {struct n0} :
nat :=
match .. with
| 0 => m1
| p0.+1 => (..).+1
end) m0
(mult p m0)
end)
(let
(x0, _) :=
if
(fix eqn
(m0 n : nat) {struct m0} :
bool :=
match .. with
| .. ..
| .. ..
end)
match .. with
| 0 => 1
| _.+1 => 0
end 0
then
(fix loop0
(m0 q : nat) {struct m0} :
nat * nat :=
match .. with
| .. ..
| .. ..
end)
(let
(_, _, task_deadline) :=
tsk in
task_deadline) 0
else
(0,
let
(_, _, task_deadline) :=
tsk in
task_deadline) in
x0)
(let
(task_cost, _, _) :=
tsk_other in
task_cost))
(if
(fix eqn
(m0 n : nat) {struct m0} :
bool :=
match m0 with
| 0 =>
match n with
| 0 => true
| _.+1 => false
end
| m'.+1 =>
match n with
| 0 => false
| n'.+1 => eqn m' n'
end
end)
match
(fix minus
.. {struct n} : nat :=
..
..
..
end)
(if .. then .. else ..)
((..) (..) R_other)
with
| 0 =>
(let
(task_cost, _, _) :=
tsk_other in
task_cost).+1
| l.+1 =>
(fix minus
(n m0 : nat) {struct n} :
nat :=
match .. with
| 0 => n
| k.+1 => ..
..
..
end
end)
(let
(task_cost, _, _) :=
tsk_other in
task_cost) l
end 0
then
let
(task_cost, _, _) :=
tsk_other in
task_cost
else
(fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match m0 with
| 0 => n
| l.+1 => minus k l
end
end)
(if
(fix eqn
(m0 n : nat) {struct m0} :
bool :=
match .. with
| .. ..
| .. ..
end)
match .. with
| 0 => 1
| _.+1 => 0
end 0
then
(fix loop0
(m0 : nat) : nat :=
match .. with
| .. m0
| .. ..
end)
(let
(_, _, task_deadline) :=
tsk in
task_deadline)
else
let
(_, _, task_deadline) :=
tsk in
task_deadline)
((fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match .. with
| .. n
| .. ..
end
end)
(let
(_, _, task_deadline) :=
tsk_other in
task_deadline) R_other))
with
| 0 =>
(if
(fix eqn
(m0 n : nat) {struct m0} :
bool :=
match m0 with
| 0 =>
match n with
| 0 => true
| _.+1 => false
end
| m'.+1 =>
match n with
| 0 => false
| n'.+1 => eqn m' n'
end
end)
match
(fix plus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => m0
| p.+1 => (plus p m0).+1
end)
((fix minus
(n m0 : nat) {struct n} :
nat :=
match .. with
| .. n
| .. ..
end) R
(let
(task_cost, _, _) := tsk in
task_cost)) 1
with
| 0 =>
((fix plus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => m0
| p.+1 => (plus p m0).+1
end)
(if
(fix eqn
.. {struct m0} : bool :=
..
..
..
end)
match .. with
| 0 => (..).+1
| l.+1 => .. .. l
end 0
then
let
(task_cost, _, _) :=
tsk_other in
task_cost
else
(fix minus
.. {struct n} : nat :=
..
..
..
end)
((..) (..) (..))
((..) (..) (..)))
((fix mult
(n m0 : nat) {struct n} :
nat :=
match .. with
| 0 => 0
| p.+1 => .. m0 ..
end)
(let
(x0, _) :=
if .. then .. else .. in
x0)
(let
(task_cost, _, _) :=
tsk_other in
task_cost))).+1
| l.+1 =>
(fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match m0 with
| 0 => n
| l0.+1 => minus k l0
end
end)
((fix plus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => m0
| p.+1 => (plus p m0).+1
end)
(if
(fix eqn .. : bool := ..)
match .. with
| .. ...+1
| .. ..
end 0
then
let
(task_cost, _, _) :=
tsk_other in
task_cost
else
(fix minus .. : nat := ..)
(.. .. ..)
(.. .. ..))
((fix mult
(n m0 : nat) {struct n} :
nat :=
match .. with
| .. 0
| .. ..
end)
(let
(x0, _) := .. .. .. in
x0)
(let
(task_cost, _, _) :=
tsk_other in
task_cost))) l
end 0
then
(fix plus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => m0
| p.+1 => (plus p m0).+1
end)
(if
(fix eqn
(m0 n : nat) {struct m0} :
bool :=
match m0 with
| 0 =>
match .. with
| 0 => true
| _.+1 => false
end
| m'.+1 =>
match .. with
| 0 => false
| n'.+1 => eqn m' n'
end
end)
match
(fix minus .. : nat := ..)
(.. .. ..)
(.. .. ..)
with
| 0 =>
(let
(task_cost, _, _) :=
tsk_other in
task_cost).+1
| l.+1 =>
(fix minus
(n m0 : nat) {struct n} :
nat :=
match .. with
| .. n
| .. ..
end)
(let
(task_cost, _, _) :=
tsk_other in
task_cost) l
end 0
then
let
(task_cost, _, _) :=
tsk_other in
task_cost
else
(fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match .. with
| 0 => n
| l.+1 => minus k l
end
end)
((fix minus
(n m0 : nat) {struct n} :
nat :=
match .. with
| 0 => n
| k.+1 => ..
..
..
end
end)
((fix plus
.. {struct n} : nat :=
..
..
..
end) R R_other)
(let
(task_cost, _, _) :=
tsk_other in
task_cost))
((fix mult
(n m0 : nat) {struct n} :
nat :=
match .. with
| 0 => 0
| p.+1 => .. m0 ..
end)
(let
(x0, _) :=
if .. then .. else .. in
x0)
(let
(_, task_period, _) :=
tsk_other in
task_period)))
((fix mult
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => 0
| p.+1 =>
(fix plus
(n0 m1 : nat) {struct n0} :
nat :=
match .. with
| .. m1
| .. ...+1
end) m0
(mult p m0)
end)
(let
(x0, _) :=
if
(fix eqn
.. {struct m0} : bool :=
..
..
..
end)
match .. with
| 0 => 1
| _.+1 => 0
end 0
then
(fix loop0
.. {struct m0} :
nat * nat :=
..
..
..
end)
((..) (..) (..)) 0
else
(0,
(fix minus .. : nat := ..)
(.. R R_other)
(let .. task_cost)) in
x0)
(let
(task_cost, _, _) :=
tsk_other in
task_cost))
else
(fix plus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => m0
| p.+1 => (plus p m0).+1
end)
((fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match m0 with
| 0 => n
| l.+1 => minus k l
end
end) R
(let
(task_cost, _, _) := tsk in
task_cost)) 1).+1
| l.+1 =>
(fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match m0 with
| 0 => n
| l0.+1 => minus k l0
end
end)
(if
(fix eqn
(m0 n : nat) {struct m0} :
bool :=
match m0 with
| 0 =>
match n with
| 0 => true
| _.+1 => false
end
| m'.+1 =>
match n with
| 0 => false
| n'.+1 => eqn m' n'
end
end)
match
(fix plus
(n m0 : nat) {struct n} :
nat :=
match .. with
| 0 => m0
| p.+1 => (..).+1
end)
((fix minus
.. {struct n} : nat :=
..
..
..
end) R
(let
(task_cost, _, _) := tsk in
task_cost)) 1
with
| 0 =>
((fix plus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => m0
| p.+1 => (plus p m0).+1
end)
(if
(fix eqn .. : bool := ..)
match .. with
| .. ...+1
| .. ..
end 0
then
let
(task_cost, _, _) :=
tsk_other in
task_cost
else
(fix minus .. : nat := ..)
(.. .. ..)
(.. .. ..))
((fix mult
(n m0 : nat) {struct n} :
nat :=
match .. with
| .. 0
| .. ..
end)
(let
(x0, _) := .. .. .. in
x0)
(let
(task_cost, _, _) :=
tsk_other in
task_cost))).+1
| l0.+1 =>
(fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match .. with
| 0 => n
| l1.+1 => minus k l1
end
end)
((fix plus
(n m0 : nat) {struct n} :
nat :=
match .. with
| 0 => m0
| p.+1 => (..).+1
end)
(if (..) ..
..
..
end 0
then
let
(task_cost, _, _) :=
tsk_other in
task_cost
else (..) (..) (..))
((fix mult
.. {struct n} : nat :=
..
..
..
end)
(let (x0, _) := .. in x0)
(let
(task_cost, _, _) :=
tsk_other in
task_cost))) l0
end 0
then
(fix plus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => m0
| p.+1 => (plus p m0).+1
end)
(if
(fix eqn
(m0 n : nat) {struct m0} :
bool :=
match m0 with
| 0 =>
match .. with
| .. true
| .. false
end
| m'.+1 =>
match .. with
| .. false
| .. ..
end
end)
match (..) (..) (..) with
| 0 =>
(let
(task_cost, _, _) :=
tsk_other in
task_cost).+1
| l0.+1 =>
(fix minus
.. {struct n} : nat :=
..
..
..
end)
(let
(task_cost, _, _) :=
tsk_other in
task_cost) l0
end 0
then
let
(task_cost, _, _) :=
tsk_other in
task_cost
else
(fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match .. with
| .. n
| .. ..
end
end)
((fix minus
(n m0 : nat) {struct n} :
nat :=
match .. with
| .. n
| .. ..
end)
((fix plus .. : nat := ..)
R R_other)
(let
(task_cost, _, _) :=
tsk_other in
task_cost))
((fix mult
(n m0 : nat) {struct n} :
nat :=
match .. with
| .. 0
| .. ..
end)
(let
(x0, _) := .. .. .. in
x0)
(let
(_, task_period, _) :=
tsk_other in
task_period)))
((fix mult
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => 0
| p.+1 =>
(fix plus
.. {struct n0} : nat :=
..
..
..
end) m0
(mult p m0)
end)
(let
(x0, _) :=
if
(fix eqn .. : bool := ..)
match .. with
| .. 1
| .. 0
end 0
then
(fix loop0 .. : .. := ..)
(.. .. ..) 0
else (0, (..) (..) (..)) in
x0)
(let
(task_cost, _, _) :=
tsk_other in
task_cost))
else
(fix plus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => m0
| p.+1 => (plus p m0).+1
end)
((fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match m0 with
| 0 => n
| l0.+1 => minus k l0
end
end) R
(let
(task_cost, _, _) := tsk in
task_cost)) 1) l
end 0
then
if
(fix eqn
(m0 n : nat) {struct m0} :
bool :=
match m0 with
| 0 =>
match n with
| 0 => true
| _.+1 => false
end
| m'.+1 =>
match n with
| 0 => false
| n'.+1 => eqn m' n'
end
end)
match
(fix plus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => m0
| p.+1 => (plus p m0).+1
end)
((fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match m0 with
| 0 => n
| l.+1 => minus k l
end
end) R
(let
(task_cost, _, _) := tsk in
task_cost)) 1
with
| 0 =>
((fix plus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => m0
| p.+1 => (plus p m0).+1
end)
(if
(fix eqn
(m0 n : nat) {struct m0} :
bool :=
match m0 with
| 0 =>
match .. with
| 0 => true
| _.+1 => false
end
| m'.+1 =>
match .. with
| 0 => false
| n'.+1 => eqn m' n'
end
end)
match
(fix minus .. : nat := ..)
(.. .. ..)
(.. .. ..)
with
| 0 =>
(let
(task_cost, _, _) :=
tsk_other in
task_cost).+1
| l.+1 =>
(fix minus
(n m0 : nat) {struct n} :
nat :=
match .. with
| .. n
| .. ..
end)
(let
(task_cost, _, _) :=
tsk_other in
task_cost) l
end 0
then
let
(task_cost, _, _) :=
tsk_other in
task_cost
else
(fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match .. with
| 0 => n
| l.+1 => minus k l
end
end)
((fix minus
(n m0 : nat) {struct n} :
nat :=
match .. with
| 0 => n
| k.+1 => ..
..
..
end
end)
((fix plus
.. {struct n} : nat :=
..
..
..
end) R R_other)
(let
(task_cost, _, _) :=
tsk_other in
task_cost))
((fix mult
(n m0 : nat) {struct n} :
nat :=
match .. with
| 0 => 0
| p.+1 => .. m0 ..
end)
(let
(x0, _) :=
if .. then .. else .. in
x0)
(let
(_, task_period, _) :=
tsk_other in
task_period)))
((fix mult
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => 0
| p.+1 =>
(fix plus
(n0 m1 : nat) {struct n0} :
nat :=
match .. with
| .. m1
| .. ...+1
end) m0
(mult p m0)
end)
(let
(x0, _) :=
if
(fix eqn
.. {struct m0} : bool :=
..
..
..
end)
match .. with
| 0 => 1
| _.+1 => 0
end 0
then
(fix loop0
.. {struct m0} :
nat * nat :=
..
..
..
end)
((..) (..) (..)) 0
else
(0,
(fix minus .. : nat := ..)
(.. R R_other)
(let .. task_cost)) in
x0)
(let
(task_cost, _, _) :=
tsk_other in
task_cost))).+1
| l.+1 =>
(fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match m0 with
| 0 => n
| l0.+1 => minus k l0
end
end)
((fix plus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => m0
| p.+1 => (plus p m0).+1
end)
(if
(fix eqn
(m0 n : nat) {struct m0} :
bool :=
match m0 with
| 0 =>
match .. with
| .. true
| .. false
end
| m'.+1 =>
match .. with
| .. false
| .. ..
end
end)
match (..) (..) (..) with
| 0 =>
(let
(task_cost, _, _) :=
tsk_other in
task_cost).+1
| l0.+1 =>
(fix minus
.. {struct n} : nat :=
..
..
..
end)
(let
(task_cost, _, _) :=
tsk_other in
task_cost) l0
end 0
then
let
(task_cost, _, _) :=
tsk_other in
task_cost
else
(fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match .. with
| .. n
| .. ..
end
end)
((fix minus
(n m0 : nat) {struct n} :
nat :=
match .. with
| .. n
| .. ..
end)
((fix plus .. : nat := ..)
R R_other)
(let
(task_cost, _, _) :=
tsk_other in
task_cost))
((fix mult
(n m0 : nat) {struct n} :
nat :=
match .. with
| .. 0
| .. ..
end)
(let
(x0, _) := .. .. .. in
x0)
(let
(_, task_period, _) :=
tsk_other in
task_period)))
((fix mult
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => 0
| p.+1 =>
(fix plus
.. {struct n0} : nat :=
..
..
..
end) m0
(mult p m0)
end)
(let
(x0, _) :=
if
(fix eqn .. : bool := ..)
match .. with
| .. 1
| .. 0
end 0
then
(fix loop0 .. : .. := ..)
(.. .. ..) 0
else (0, (..) (..) (..)) in
x0)
(let
(task_cost, _, _) :=
tsk_other in
task_cost))) l
end 0
then
(fix plus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => m0
| p.+1 => (plus p m0).+1
end)
(if
(fix eqn
(m0 n : nat) {struct m0} :
bool :=
match m0 with
| 0 =>
match n with
| 0 => true
| _.+1 => false
end
| m'.+1 =>
match n with
| 0 => false
| n'.+1 => eqn m' n'
end
end)
match
(fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match .. with
| .. n
| .. ..
end
end)
((fix minus
(n m0 : nat) {struct n} :
nat :=
match .. with
| .. n
| .. ..
end)
((fix plus .. : nat := ..)
R R_other)
(let
(task_cost, _, _) :=
tsk_other in
task_cost))
((fix mult
(n m0 : nat) {struct n} :
nat :=
match .. with
| .. 0
| .. ..
end)
(let
(x0, _) := .. .. .. in
x0)
(let
(_, task_period, _) :=
tsk_other in
task_period))
with
| 0 =>
(let
(task_cost, _, _) :=
tsk_other in
task_cost).+1
| l.+1 =>
(fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match m0 with
| 0 => n
| l0.+1 => minus k l0
end
end)
(let
(task_cost, _, _) :=
tsk_other in
task_cost) l
end 0
then
let
(task_cost, _, _) :=
tsk_other in
task_cost
else
(fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match m0 with
| 0 => n
| l.+1 => minus k l
end
end)
((fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match m0 with
| 0 => n
| l.+1 => minus k l
end
end)
((fix plus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => m0
| p.+1 => (plus p m0).+1
end) R R_other)
(let
(task_cost, _, _) :=
tsk_other in
task_cost))
((fix mult
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => 0
| p.+1 =>
(fix plus
(n0 m1 : nat) {struct n0} :
nat :=
match .. with
| .. m1
| .. ...+1
end) m0
(mult p m0)
end)
(let
(x0, _) :=
if
(fix eqn
.. {struct m0} : bool :=
..
..
..
end)
match .. with
| 0 => 1
| _.+1 => 0
end 0
then
(fix loop0
.. {struct m0} :
nat * nat :=
..
..
..
end)
((..) (..) (..)) 0
else
(0,
(fix minus .. : nat := ..)
(.. R R_other)
(let .. task_cost)) in
x0)
(let
(_, task_period, _) :=
tsk_other in
task_period)))
((fix mult
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => 0
| p.+1 =>
(fix plus
(n0 m1 : nat) {struct n0} :
nat :=
match n0 with
| 0 => m1
| p0.+1 => (plus p0 m1).+1
end) m0
(mult p m0)
end)
(let
(x0, _) :=
if
(fix eqn
(m0 n : nat) {struct m0} :
bool :=
match m0 with
| 0 =>
match .. with
| 0 => true
| _.+1 => false
end
| m'.+1 =>
match .. with
| 0 => false
| n'.+1 => eqn m' n'
end
end)
match
(let
(_, task_period, _) :=
tsk_other in
task_period)
with
| 0 => 1
| _.+1 => 0
end 0
then
(fix loop0
(m0 q : nat) {struct m0} :
nat * nat :=
match .. m0 .. with
| 0 => (q, m0)
| m'.+1 => loop0 m' q.+1
end)
((fix minus
(n m0 : nat) {struct n} :
nat :=
match .. with
| 0 => n
| k.+1 => ..
..
..
end
end)
((fix plus
.. {struct n} : nat :=
..
..
..
end) R R_other)
(let
(task_cost, _, _) :=
tsk_other in
task_cost)) 0
else
(0,
(fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match .. with
| .. n
| .. ..
end
end)
((fix plus
(n m0 : nat) {struct n} :
nat :=
match .. with
| .. m0
| .. ...+1
end) R R_other)
(let
(task_cost, _, _) :=
tsk_other in
task_cost)) in
x0)
(let
(task_cost, _, _) :=
tsk_other in
task_cost))
else
(fix plus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => m0
| p.+1 => (plus p m0).+1
end)
((fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match m0 with
| 0 => n
| l.+1 => minus k l
end
end) R
(let
(task_cost, _, _) := tsk in
task_cost)) 1
else
(fix plus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => m0
| p.+1 => (plus p m0).+1
end)
((fix mult
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => 0
| p.+1 =>
(fix plus
(n0 m1 : nat) {struct n0} :
nat :=
match n0 with
| 0 => m1
| p0.+1 => (plus p0 m1).+1
end) m0
(mult p m0)
end)
(let
(x0, _) :=
if
(fix eqn
(m0 n : nat) {struct m0} :
bool :=
match m0 with
| 0 =>
match n with
| 0 => true
| _.+1 => false
end
| m'.+1 =>
match n with
| 0 => false
| n'.+1 => eqn m' n'
end
end)
match
(let
(_, task_period, _) :=
tsk_other in
task_period)
with
| 0 => 1
| _.+1 => 0
end 0
then
(fix loop0
(m0 q : nat) {struct m0} :
nat * nat :=
match
(fix minus .. : nat := ..)
m0
match .. with
| .. ..
| .. u
end
with
| 0 => (q, m0)
| m'.+1 => loop0 m' q.+1
end)
(let
(_, _, task_deadline) :=
tsk in
task_deadline) 0
else
(0,
let
(_, _, task_deadline) :=
tsk in
task_deadline) in
x0)
(let
(task_cost, _, _) :=
tsk_other in
task_cost))
(if
(fix eqn
(m0 n : nat) {struct m0} :
bool :=
match m0 with
| 0 =>
match n with
| 0 => true
| _.+1 => false
end
| m'.+1 =>
match n with
| 0 => false
| n'.+1 => eqn m' n'
end
end)
match
(fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match m0 with
| 0 => n
| l.+1 => minus k l
end
end)
(if
(fix eqn
(m0 n : nat) {struct m0} :
bool :=
match .. with
| .. ..
| .. ..
end)
match .. with
| 0 => 1
| _.+1 => 0
end 0
then
(fix loop0
(m0 : nat) : nat :=
match .. with
| .. m0
| .. ..
end)
(let
(_, _, task_deadline) :=
tsk in
task_deadline)
else
let
(_, _, task_deadline) :=
tsk in
task_deadline)
((fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match .. with
| .. n
| .. ..
end
end)
(let
(_, _, task_deadline) :=
tsk_other in
task_deadline) R_other)
with
| 0 =>
(let
(task_cost, _, _) :=
tsk_other in
task_cost).+1
| l.+1 =>
(fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match m0 with
| 0 => n
| l0.+1 => minus k l0
end
end)
(let
(task_cost, _, _) :=
tsk_other in
task_cost) l
end 0
then
let
(task_cost, _, _) :=
tsk_other in
task_cost
else
(fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match m0 with
| 0 => n
| l.+1 => minus k l
end
end)
(if
(fix eqn
(m0 n : nat) {struct m0} :
bool :=
match m0 with
| 0 =>
match n with
| 0 => true
| _.+1 => false
end
| m'.+1 =>
match n with
| 0 => false
| n'.+1 => eqn m' n'
end
end)
match
(let
(_, task_period, _) :=
tsk_other in
task_period)
with
| 0 => 1
| _.+1 => 0
end 0
then
(fix loop0
(m0 : nat) : nat :=
match
(fix minus .. : nat := ..)
m0
match .. with
| .. ..
| .. u
end
with
| 0 => m0
| m'.+1 => loop0 m'
end)
(let
(_, _, task_deadline) :=
tsk in
task_deadline)
else
let
(_, _, task_deadline) :=
tsk in
task_deadline)
((fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match m0 with
| 0 => n
| l.+1 => minus k l
end
end)
(let
(_, _, task_deadline) :=
tsk_other in
task_deadline) R_other))))
0 in
x0))) :: map s'
end) (loop i)
end)
((fix plus (n m : nat) {struct n} : nat :=
match n with
| 0 => m
| p.+1 => (plus p m).+1
end)
(\big[(fix plus (n m : nat) {struct n} : nat :=
match n with
| 0 => m
| p.+1 => (plus p m).+1
end)/0]_(tsk <- [:: {|
task_cost := 1;
task_period := 10;
task_deadline := 10 |};
{|
task_cost := 2;
task_period := 10;
task_deadline := 10 |};
{|
task_cost := 3;
task_period := 10;
task_deadline := 10 |}])
(fix minus (n m : nat) {struct n} : nat :=
match n with
| 0 => n
| k.+1 =>
match m with
| 0 => n
| l.+1 => minus k l
end
end)
(let (_, _, task_deadline) := tsk in task_deadline)
(let (task_cost, _, _) := tsk in task_cost)) 1))
then
Some
((fix loop (m : nat) : seq (concrete_task * nat) :=
match m with
| 0 =>
[:: ({|
task_cost := 1;
task_period := 10;
task_deadline := 10 |}, 1);
({|
task_cost := 2;
task_period := 10;
task_deadline := 10 |}, 2);
({|
task_cost := 3;
task_period := 10;
task_deadline := 10 |}, 3)]
| i.+1 =>
(fix map (s : seq (concrete_task * nat)) :
seq (concrete_task * nat) :=
match s with
| [::] => [::]
| x :: s' =>
(let (tsk, R) := x in
(tsk,
(fix plus (n m0 : nat) {struct n} : nat :=
match n with
| 0 => m0
| p.+1 => (plus p m0).+1
end) (let (task_cost, _, _) := tsk in task_cost)
(let (x0, _) :=
(fix loop0 (m0 q : nat) {struct m0} :
nat * nat :=
match
(fix minus (n m1 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match m1 with
| 0 => n
| l.+1 => minus k l
end
end) m0 1
with
| 0 => (q, m0)
| m'.+1 => loop0 m' q.+1
end)
(\big[(fix plus
(n m0 : nat) {struct n} : nat :=
match n with
| 0 => m0
| p.+1 => (plus p m0).+1
end)/0]_(i0 <-
loop i | let '(tsk_other, _) := i0 in
if
if
if
(fix eqn
(m0 n : nat) {struct m0} :
bool :=
match m0 with
| 0 =>
match n with
| 0 => true
| _.+1 => false
end
| m'.+1 =>
match n with
| 0 => false
| n'.+1 => eqn m' n'
end
end)
(let
(task_cost, _, _) :=
tsk_other in
task_cost)
(let
(task_cost, _, _) := tsk in
task_cost)
then
(fix eqn
(m0 n : nat) {struct m0} :
bool :=
match m0 with
| 0 =>
match n with
| 0 => true
| _.+1 => false
end
| m'.+1 =>
match n with
| 0 => false
| n'.+1 => eqn m' n'
end
end)
(let
(_, task_period, _) :=
tsk_other in
task_period)
(let
(_, task_period, _) :=
tsk in
task_period)
else false
then
(fix eqn
(m0 n : nat) {struct m0} :
bool :=
match m0 with
| 0 =>
match n with
| 0 => true
| _.+1 => false
end
| m'.+1 =>
match n with
| 0 => false
| n'.+1 => eqn m' n'
end
end)
(let
(_, _, task_deadline) :=
tsk_other in
task_deadline)
(let
(_, _, task_deadline) :=
tsk in
task_deadline)
else false
then false
else true)
(let '(tsk_other, R_other) := i0 in
if (fix eqn
(m0 n : nat) {struct m0} :
bool :=
match m0 with
| 0 =>
match n with
| 0 => true
| _.+1 => false
end
| m'.+1 =>
match n with
| 0 => false
| n'.+1 => eqn m' n'
end
end)
match
(fix plus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => m0
| p.+1 => (plus p m0).+1
end)
((fix mult
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => 0
| p.+1 =>
(fix plus
(n0 m1 : nat) {struct n0} :
nat :=
match .. with
| 0 => m1
| p0.+1 => (..).+1
end) m0
(mult p m0)
end)
(let
(x0, _) :=
if
(fix eqn
(m0 n : nat) {struct m0} :
bool :=
match .. with
| .. ..
| .. ..
end)
match .. with
| 0 => 1
| _.+1 => 0
end 0
then
(fix loop0
(m0 q : nat) {struct m0} :
nat * nat :=
match .. with
| .. ..
| .. ..
end)
(let
(_, _, task_deadline) :=
tsk in
task_deadline) 0
else
(0,
let
(_, _, task_deadline) :=
tsk in
task_deadline) in
x0)
(let
(task_cost, _, _) :=
tsk_other in
task_cost))
(if
(fix eqn
(m0 n : nat) {struct m0} :
bool :=
match m0 with
| 0 =>
match n with
| 0 => true
| _.+1 => false
end
| m'.+1 =>
match n with
| 0 => false
| n'.+1 => eqn m' n'
end
end)
match
(fix minus
.. {struct n} : nat :=
..
..
..
end)
(if .. then .. else ..)
((..) (..) R_other)
with
| 0 =>
(let
(task_cost, _, _) :=
tsk_other in
task_cost).+1
| l.+1 =>
(fix minus
(n m0 : nat) {struct n} :
nat :=
match .. with
| 0 => n
| k.+1 => ..
..
..
end
end)
(let
(task_cost, _, _) :=
tsk_other in
task_cost) l
end 0
then
let
(task_cost, _, _) :=
tsk_other in
task_cost
else
(fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match m0 with
| 0 => n
| l.+1 => minus k l
end
end)
(if
(fix eqn
(m0 n : nat) {struct m0} :
bool :=
match .. with
| .. ..
| .. ..
end)
match .. with
| 0 => 1
| _.+1 => 0
end 0
then
(fix loop0
(m0 : nat) : nat :=
match .. with
| .. m0
| .. ..
end)
(let
(_, _, task_deadline) :=
tsk in
task_deadline)
else
let
(_, _, task_deadline) :=
tsk in
task_deadline)
((fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match .. with
| .. n
| .. ..
end
end)
(let
(_, _, task_deadline) :=
tsk_other in
task_deadline) R_other))
with
| 0 =>
(if
(fix eqn
(m0 n : nat) {struct m0} :
bool :=
match m0 with
| 0 =>
match n with
| 0 => true
| _.+1 => false
end
| m'.+1 =>
match n with
| 0 => false
| n'.+1 => eqn m' n'
end
end)
match
(fix plus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => m0
| p.+1 => (plus p m0).+1
end)
((fix minus
(n m0 : nat) {struct n} :
nat :=
match .. with
| .. n
| .. ..
end) R
(let
(task_cost, _, _) := tsk in
task_cost)) 1
with
| 0 =>
((fix plus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => m0
| p.+1 => (plus p m0).+1
end)
(if
(fix eqn
.. {struct m0} : bool :=
..
..
..
end)
match .. with
| 0 => (..).+1
| l.+1 => .. .. l
end 0
then
let
(task_cost, _, _) :=
tsk_other in
task_cost
else
(fix minus
.. {struct n} : nat :=
..
..
..
end)
((..) (..) (..))
((..) (..) (..)))
((fix mult
(n m0 : nat) {struct n} :
nat :=
match .. with
| 0 => 0
| p.+1 => .. m0 ..
end)
(let
(x0, _) :=
if .. then .. else .. in
x0)
(let
(task_cost, _, _) :=
tsk_other in
task_cost))).+1
| l.+1 =>
(fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match m0 with
| 0 => n
| l0.+1 => minus k l0
end
end)
((fix plus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => m0
| p.+1 => (plus p m0).+1
end)
(if
(fix eqn .. : bool := ..)
match .. with
| .. ...+1
| .. ..
end 0
then
let
(task_cost, _, _) :=
tsk_other in
task_cost
else
(fix minus .. : nat := ..)
(.. .. ..)
(.. .. ..))
((fix mult
(n m0 : nat) {struct n} :
nat :=
match .. with
| .. 0
| .. ..
end)
(let
(x0, _) := .. .. .. in
x0)
(let
(task_cost, _, _) :=
tsk_other in
task_cost))) l
end 0
then
(fix plus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => m0
| p.+1 => (plus p m0).+1
end)
(if
(fix eqn
(m0 n : nat) {struct m0} :
bool :=
match m0 with
| 0 =>
match .. with
| 0 => true
| _.+1 => false
end
| m'.+1 =>
match .. with
| 0 => false
| n'.+1 => eqn m' n'
end
end)
match
(fix minus .. : nat := ..)
(.. .. ..)
(.. .. ..)
with
| 0 =>
(let
(task_cost, _, _) :=
tsk_other in
task_cost).+1
| l.+1 =>
(fix minus
(n m0 : nat) {struct n} :
nat :=
match .. with
| .. n
| .. ..
end)
(let
(task_cost, _, _) :=
tsk_other in
task_cost) l
end 0
then
let
(task_cost, _, _) :=
tsk_other in
task_cost
else
(fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match .. with
| 0 => n
| l.+1 => minus k l
end
end)
((fix minus
(n m0 : nat) {struct n} :
nat :=
match .. with
| 0 => n
| k.+1 => ..
..
..
end
end)
((fix plus
.. {struct n} : nat :=
..
..
..
end) R R_other)
(let
(task_cost, _, _) :=
tsk_other in
task_cost))
((fix mult
(n m0 : nat) {struct n} :
nat :=
match .. with
| 0 => 0
| p.+1 => .. m0 ..
end)
(let
(x0, _) :=
if .. then .. else .. in
x0)
(let
(_, task_period, _) :=
tsk_other in
task_period)))
((fix mult
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => 0
| p.+1 =>
(fix plus
(n0 m1 : nat) {struct n0} :
nat :=
match .. with
| .. m1
| .. ...+1
end) m0
(mult p m0)
end)
(let
(x0, _) :=
if
(fix eqn
.. {struct m0} : bool :=
..
..
..
end)
match .. with
| 0 => 1
| _.+1 => 0
end 0
then
(fix loop0
.. {struct m0} :
nat * nat :=
..
..
..
end)
((..) (..) (..)) 0
else
(0,
(fix minus .. : nat := ..)
(.. R R_other)
(let .. task_cost)) in
x0)
(let
(task_cost, _, _) :=
tsk_other in
task_cost))
else
(fix plus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => m0
| p.+1 => (plus p m0).+1
end)
((fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match m0 with
| 0 => n
| l.+1 => minus k l
end
end) R
(let
(task_cost, _, _) := tsk in
task_cost)) 1).+1
| l.+1 =>
(fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match m0 with
| 0 => n
| l0.+1 => minus k l0
end
end)
(if
(fix eqn
(m0 n : nat) {struct m0} :
bool :=
match m0 with
| 0 =>
match n with
| 0 => true
| _.+1 => false
end
| m'.+1 =>
match n with
| 0 => false
| n'.+1 => eqn m' n'
end
end)
match
(fix plus
(n m0 : nat) {struct n} :
nat :=
match .. with
| 0 => m0
| p.+1 => (..).+1
end)
((fix minus
.. {struct n} : nat :=
..
..
..
end) R
(let
(task_cost, _, _) := tsk in
task_cost)) 1
with
| 0 =>
((fix plus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => m0
| p.+1 => (plus p m0).+1
end)
(if
(fix eqn .. : bool := ..)
match .. with
| .. ...+1
| .. ..
end 0
then
let
(task_cost, _, _) :=
tsk_other in
task_cost
else
(fix minus .. : nat := ..)
(.. .. ..)
(.. .. ..))
((fix mult
(n m0 : nat) {struct n} :
nat :=
match .. with
| .. 0
| .. ..
end)
(let
(x0, _) := .. .. .. in
x0)
(let
(task_cost, _, _) :=
tsk_other in
task_cost))).+1
| l0.+1 =>
(fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match .. with
| 0 => n
| l1.+1 => minus k l1
end
end)
((fix plus
(n m0 : nat) {struct n} :
nat :=
match .. with
| 0 => m0
| p.+1 => (..).+1
end)
(if (..) ..
..
..
end 0
then
let
(task_cost, _, _) :=
tsk_other in
task_cost
else (..) (..) (..))
((fix mult
.. {struct n} : nat :=
..
..
..
end)
(let (x0, _) := .. in x0)
(let
(task_cost, _, _) :=
tsk_other in
task_cost))) l0
end 0
then
(fix plus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => m0
| p.+1 => (plus p m0).+1
end)
(if
(fix eqn
(m0 n : nat) {struct m0} :
bool :=
match m0 with
| 0 =>
match .. with
| .. true
| .. false
end
| m'.+1 =>
match .. with
| .. false
| .. ..
end
end)
match (..) (..) (..) with
| 0 =>
(let
(task_cost, _, _) :=
tsk_other in
task_cost).+1
| l0.+1 =>
(fix minus
.. {struct n} : nat :=
..
..
..
end)
(let
(task_cost, _, _) :=
tsk_other in
task_cost) l0
end 0
then
let
(task_cost, _, _) :=
tsk_other in
task_cost
else
(fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match .. with
| .. n
| .. ..
end
end)
((fix minus
(n m0 : nat) {struct n} :
nat :=
match .. with
| .. n
| .. ..
end)
((fix plus .. : nat := ..)
R R_other)
(let
(task_cost, _, _) :=
tsk_other in
task_cost))
((fix mult
(n m0 : nat) {struct n} :
nat :=
match .. with
| .. 0
| .. ..
end)
(let
(x0, _) := .. .. .. in
x0)
(let
(_, task_period, _) :=
tsk_other in
task_period)))
((fix mult
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => 0
| p.+1 =>
(fix plus
.. {struct n0} : nat :=
..
..
..
end) m0
(mult p m0)
end)
(let
(x0, _) :=
if
(fix eqn .. : bool := ..)
match .. with
| .. 1
| .. 0
end 0
then
(fix loop0 .. : .. := ..)
(.. .. ..) 0
else (0, (..) (..) (..)) in
x0)
(let
(task_cost, _, _) :=
tsk_other in
task_cost))
else
(fix plus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => m0
| p.+1 => (plus p m0).+1
end)
((fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match m0 with
| 0 => n
| l0.+1 => minus k l0
end
end) R
(let
(task_cost, _, _) := tsk in
task_cost)) 1) l
end 0
then
if (fix eqn
(m0 n : nat) {struct m0} :
bool :=
match m0 with
| 0 =>
match n with
| 0 => true
| _.+1 => false
end
| m'.+1 =>
match n with
| 0 => false
| n'.+1 => eqn m' n'
end
end)
match
(fix plus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => m0
| p.+1 => (plus p m0).+1
end)
((fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match m0 with
| 0 => n
| l.+1 => minus k l
end
end) R
(let
(task_cost, _, _) := tsk in
task_cost)) 1
with
| 0 =>
((fix plus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => m0
| p.+1 => (plus p m0).+1
end)
(if
(fix eqn
(m0 n : nat) {struct m0} :
bool :=
match m0 with
| 0 =>
match .. with
| 0 => true
| _.+1 => false
end
| m'.+1 =>
match .. with
| 0 => false
| n'.+1 => eqn m' n'
end
end)
match
(fix minus .. : nat := ..)
(.. .. ..)
(.. .. ..)
with
| 0 =>
(let
(task_cost, _, _) :=
tsk_other in
task_cost).+1
| l.+1 =>
(fix minus
(n m0 : nat) {struct n} :
nat :=
match .. with
| .. n
| .. ..
end)
(let
(task_cost, _, _) :=
tsk_other in
task_cost) l
end 0
then
let
(task_cost, _, _) :=
tsk_other in
task_cost
else
(fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match .. with
| 0 => n
| l.+1 => minus k l
end
end)
((fix minus
(n m0 : nat) {struct n} :
nat :=
match .. with
| 0 => n
| k.+1 => ..
..
..
end
end)
((fix plus
.. {struct n} : nat :=
..
..
..
end) R R_other)
(let
(task_cost, _, _) :=
tsk_other in
task_cost))
((fix mult
(n m0 : nat) {struct n} :
nat :=
match .. with
| 0 => 0
| p.+1 => .. m0 ..
end)
(let
(x0, _) :=
if .. then .. else .. in
x0)
(let
(_, task_period, _) :=
tsk_other in
task_period)))
((fix mult
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => 0
| p.+1 =>
(fix plus
(n0 m1 : nat) {struct n0} :
nat :=
match .. with
| .. m1
| .. ...+1
end) m0
(mult p m0)
end)
(let
(x0, _) :=
if
(fix eqn
.. {struct m0} : bool :=
..
..
..
end)
match .. with
| 0 => 1
| _.+1 => 0
end 0
then
(fix loop0
.. {struct m0} :
nat * nat :=
..
..
..
end)
((..) (..) (..)) 0
else
(0,
(fix minus .. : nat := ..)
(.. R R_other)
(let .. task_cost)) in
x0)
(let
(task_cost, _, _) :=
tsk_other in
task_cost))).+1
| l.+1 =>
(fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match m0 with
| 0 => n
| l0.+1 => minus k l0
end
end)
((fix plus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => m0
| p.+1 => (plus p m0).+1
end)
(if
(fix eqn
(m0 n : nat) {struct m0} :
bool :=
match m0 with
| 0 =>
match .. with
| .. true
| .. false
end
| m'.+1 =>
match .. with
| .. false
| .. ..
end
end)
match (..) (..) (..) with
| 0 =>
(let
(task_cost, _, _) :=
tsk_other in
task_cost).+1
| l0.+1 =>
(fix minus
.. {struct n} : nat :=
..
..
..
end)
(let
(task_cost, _, _) :=
tsk_other in
task_cost) l0
end 0
then
let
(task_cost, _, _) :=
tsk_other in
task_cost
else
(fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match .. with
| .. n
| .. ..
end
end)
((fix minus
(n m0 : nat) {struct n} :
nat :=
match .. with
| .. n
| .. ..
end)
((fix plus .. : nat := ..)
R R_other)
(let
(task_cost, _, _) :=
tsk_other in
task_cost))
((fix mult
(n m0 : nat) {struct n} :
nat :=
match .. with
| .. 0
| .. ..
end)
(let
(x0, _) := .. .. .. in
x0)
(let
(_, task_period, _) :=
tsk_other in
task_period)))
((fix mult
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => 0
| p.+1 =>
(fix plus
.. {struct n0} : nat :=
..
..
..
end) m0
(mult p m0)
end)
(let
(x0, _) :=
if
(fix eqn .. : bool := ..)
match .. with
| .. 1
| .. 0
end 0
then
(fix loop0 .. : .. := ..)
(.. .. ..) 0
else (0, (..) (..) (..)) in
x0)
(let
(task_cost, _, _) :=
tsk_other in
task_cost))) l
end 0
then
(fix plus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => m0
| p.+1 => (plus p m0).+1
end)
(if
(fix eqn
(m0 n : nat) {struct m0} :
bool :=
match m0 with
| 0 =>
match n with
| 0 => true
| _.+1 => false
end
| m'.+1 =>
match n with
| 0 => false
| n'.+1 => eqn m' n'
end
end)
match
(fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match .. with
| .. n
| .. ..
end
end)
((fix minus
(n m0 : nat) {struct n} :
nat :=
match .. with
| .. n
| .. ..
end)
((fix plus .. : nat := ..)
R R_other)
(let
(task_cost, _, _) :=
tsk_other in
task_cost))
((fix mult
(n m0 : nat) {struct n} :
nat :=
match .. with
| .. 0
| .. ..
end)
(let
(x0, _) := .. .. .. in
x0)
(let
(_, task_period, _) :=
tsk_other in
task_period))
with
| 0 =>
(let
(task_cost, _, _) :=
tsk_other in
task_cost).+1
| l.+1 =>
(fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match m0 with
| 0 => n
| l0.+1 => minus k l0
end
end)
(let
(task_cost, _, _) :=
tsk_other in
task_cost) l
end 0
then
let
(task_cost, _, _) :=
tsk_other in
task_cost
else
(fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match m0 with
| 0 => n
| l.+1 => minus k l
end
end)
((fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match m0 with
| 0 => n
| l.+1 => minus k l
end
end)
((fix plus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => m0
| p.+1 => (plus p m0).+1
end) R R_other)
(let
(task_cost, _, _) :=
tsk_other in
task_cost))
((fix mult
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => 0
| p.+1 =>
(fix plus
(n0 m1 : nat) {struct n0} :
nat :=
match .. with
| .. m1
| .. ...+1
end) m0
(mult p m0)
end)
(let
(x0, _) :=
if
(fix eqn
.. {struct m0} : bool :=
..
..
..
end)
match .. with
| 0 => 1
| _.+1 => 0
end 0
then
(fix loop0
.. {struct m0} :
nat * nat :=
..
..
..
end)
((..) (..) (..)) 0
else
(0,
(fix minus .. : nat := ..)
(.. R R_other)
(let .. task_cost)) in
x0)
(let
(_, task_period, _) :=
tsk_other in
task_period)))
((fix mult
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => 0
| p.+1 =>
(fix plus
(n0 m1 : nat) {struct n0} :
nat :=
match n0 with
| 0 => m1
| p0.+1 => (plus p0 m1).+1
end) m0
(mult p m0)
end)
(let
(x0, _) :=
if
(fix eqn
(m0 n : nat) {struct m0} :
bool :=
match m0 with
| 0 =>
match .. with
| 0 => true
| _.+1 => false
end
| m'.+1 =>
match .. with
| 0 => false
| n'.+1 => eqn m' n'
end
end)
match
(let
(_, task_period, _) :=
tsk_other in
task_period)
with
| 0 => 1
| _.+1 => 0
end 0
then
(fix loop0
(m0 q : nat) {struct m0} :
nat * nat :=
match .. m0 .. with
| 0 => (q, m0)
| m'.+1 => loop0 m' q.+1
end)
((fix minus
(n m0 : nat) {struct n} :
nat :=
match .. with
| 0 => n
| k.+1 => ..
..
..
end
end)
((fix plus
.. {struct n} : nat :=
..
..
..
end) R R_other)
(let
(task_cost, _, _) :=
tsk_other in
task_cost)) 0
else
(0,
(fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match .. with
| .. n
| .. ..
end
end)
((fix plus
(n m0 : nat) {struct n} :
nat :=
match .. with
| .. m0
| .. ...+1
end) R R_other)
(let
(task_cost, _, _) :=
tsk_other in
task_cost)) in
x0)
(let
(task_cost, _, _) :=
tsk_other in
task_cost))
else
(fix plus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => m0
| p.+1 => (plus p m0).+1
end)
((fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match m0 with
| 0 => n
| l.+1 => minus k l
end
end) R
(let
(task_cost, _, _) := tsk in
task_cost)) 1
else
(fix plus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => m0
| p.+1 => (plus p m0).+1
end)
((fix mult
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => 0
| p.+1 =>
(fix plus
(n0 m1 : nat) {struct n0} :
nat :=
match n0 with
| 0 => m1
| p0.+1 => (plus p0 m1).+1
end) m0
(mult p m0)
end)
(let
(x0, _) :=
if
(fix eqn
(m0 n : nat) {struct m0} :
bool :=
match m0 with
| 0 =>
match n with
| 0 => true
| _.+1 => false
end
| m'.+1 =>
match n with
| 0 => false
| n'.+1 => eqn m' n'
end
end)
match
(let
(_, task_period, _) :=
tsk_other in
task_period)
with
| 0 => 1
| _.+1 => 0
end 0
then
(fix loop0
(m0 q : nat) {struct m0} :
nat * nat :=
match
(fix minus .. : nat := ..)
m0
match .. with
| .. ..
| .. u
end
with
| 0 => (q, m0)
| m'.+1 => loop0 m' q.+1
end)
(let
(_, _, task_deadline) :=
tsk in
task_deadline) 0
else
(0,
let
(_, _, task_deadline) :=
tsk in
task_deadline) in
x0)
(let
(task_cost, _, _) :=
tsk_other in
task_cost))
(if
(fix eqn
(m0 n : nat) {struct m0} :
bool :=
match m0 with
| 0 =>
match n with
| 0 => true
| _.+1 => false
end
| m'.+1 =>
match n with
| 0 => false
| n'.+1 => eqn m' n'
end
end)
match
(fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match m0 with
| 0 => n
| l.+1 => minus k l
end
end)
(if
(fix eqn
(m0 n : nat) {struct m0} :
bool :=
match .. with
| .. ..
| .. ..
end)
match .. with
| 0 => 1
| _.+1 => 0
end 0
then
(fix loop0
(m0 : nat) : nat :=
match .. with
| .. m0
| .. ..
end)
(let
(_, _, task_deadline) :=
tsk in
task_deadline)
else
let
(_, _, task_deadline) :=
tsk in
task_deadline)
((fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match .. with
| .. n
| .. ..
end
end)
(let
(_, _, task_deadline) :=
tsk_other in
task_deadline) R_other)
with
| 0 =>
(let
(task_cost, _, _) :=
tsk_other in
task_cost).+1
| l.+1 =>
(fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match m0 with
| 0 => n
| l0.+1 => minus k l0
end
end)
(let
(task_cost, _, _) :=
tsk_other in
task_cost) l
end 0
then
let
(task_cost, _, _) :=
tsk_other in
task_cost
else
(fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match m0 with
| 0 => n
| l.+1 => minus k l
end
end)
(if
(fix eqn
(m0 n : nat) {struct m0} :
bool :=
match m0 with
| 0 =>
match n with
| 0 => true
| _.+1 => false
end
| m'.+1 =>
match n with
| 0 => false
| n'.+1 => eqn m' n'
end
end)
match
(let
(_, task_period, _) :=
tsk_other in
task_period)
with
| 0 => 1
| _.+1 => 0
end 0
then
(fix loop0
(m0 : nat) : nat :=
match
(fix minus .. : nat := ..)
m0
match .. with
| .. ..
| .. u
end
with
| 0 => m0
| m'.+1 => loop0 m'
end)
(let
(_, _, task_deadline) :=
tsk in
task_deadline)
else
let
(_, _, task_deadline) :=
tsk in
task_deadline)
((fix minus
(n m0 : nat) {struct n} :
nat :=
match n with
| 0 => n
| k.+1 =>
match m0 with
| 0 => n
| l.+1 => minus k l
end
end)
(let
(_, _, task_deadline) :=
tsk_other in
task_deadline) R_other))))
0 in
x0))) :: map s'
end) (loop i)
end)
((fix plus (n m : nat) {struct n} : nat :=
match n with
| 0 => m
| p.+1 => (plus p m).+1
end)
(\big[(fix plus (n m : nat) {struct n} : nat :=
match n with
| 0 => m
| p.+1 => (plus p m).+1
end)/0]_(tsk <- [:: {|
task_cost := 1;
task_period := 10;
task_deadline := 10 |};
{|
task_cost := 2;
task_period := 10;
task_deadline := 10 |};
{|
task_cost := 3;
task_period := 10;
task_deadline := 10 |}])
(fix minus (n m : nat) {struct n} : nat :=
match n with
| 0 => n
| k.+1 =>
match m with
| 0 => n
| l.+1 => minus k l
end
end)
(let (_, _, task_deadline) := tsk in task_deadline)
(let (task_cost, _, _) := tsk in task_cost)) 1))
else None
: option (seq (task_eqType * nat))

Archive powered by MHonArc 2.6.18.

Top of Page