Commit 3ca8c743 authored by Léon Gondelman's avatar Léon Gondelman
Browse files

change the order of return type in exhaling functions

parent 3b9627d9
......@@ -52,7 +52,7 @@ Section denv.
end
end.
Fixpoint denv_inhale_frac (i : nat) (m : denv) : option (frac * dval * denv) :=
Fixpoint denv_inhale_frac (i : nat) (m : denv) : option (denv * frac * dval) :=
match m with
| [] => None
| dio :: m' =>
......@@ -60,12 +60,12 @@ Section denv.
| O =>
''(DenvItem lv q dv) dio;
guard (lv = ULvl);
Some ((q / 2)%Qp, dv, Some (DenvItem lv (q / 2) dv) :: m')
| S i => ''(q, dv, m') denv_inhale_frac i m; Some (q, dv, dio :: m')
Some (Some (DenvItem lv (q / 2) dv) :: m', (q / 2)%Qp, dv)
| S i => ''(m', q, dv) denv_inhale_frac i m; Some (dio :: m', q, dv)
end
end.
Fixpoint denv_inhale_full_aux (i : nat) (m : denv) : option (frac * dval * denv) :=
Fixpoint denv_inhale_full_aux (i : nat) (m : denv) : option (denv * frac * dval) :=
match m with
| [] => None
| dio :: m' =>
......@@ -73,33 +73,34 @@ Section denv.
| O =>
''(DenvItem lv q dv) dio;
guard (lv = ULvl);
Some (q, dv, None :: m')
| S i => ''(q, dv, mf) denv_inhale_full_aux i m'; Some (q, dv, dio :: mf)
Some (None :: m', q, dv)
| S i => ''(mf, q, dv) denv_inhale_full_aux i m'; Some (dio :: mf, q, dv)
end
end.
Definition denv_inhale_full (i : nat) (m : denv) : option (dval * denv) :=
''(q,dv,m') denv_inhale_full_aux i m;
Definition denv_inhale_full (i : nat) (m : denv) : option (denv * dval) :=
''(m', q, dv) denv_inhale_full_aux i m;
guard (q = 1)%Qp;
Some (dv,m').
Some (m', dv).
Definition denv_unlock (m: denv) : denv :=
map (λ dio, ''(DenvItem _ q dv) dio; Some (DenvItem ULvl q dv)) m.
Definition denv_inhale_frac_2 (i : nat) (m1 m2 : denv) : option (denv * denv * frac * dval) :=
match denv_inhale_frac i m1 with
| Some (q, dv, m1') => Some (m1', m2, q, dv)
| Some (m1', q, dv) => Some (m1', m2, q, dv)
| None =>
match denv_inhale_frac i m2 with
| Some (q, dv, m2') => Some (m1, m2', q, dv)
| Some (m2', q, dv) => Some (m1, m2', q, dv)
| None => None
end
end.
Definition denv_inhale_full_2 (i : nat) (m1 m2: denv) : option (denv * denv * dval) :=
match denv_inhale_full_aux i m1, denv_inhale_full_aux i m2 with
| None, Some (q, dv, m2') => guard (q = 1)%Qp; Some (m1, m2', dv)
| Some (q, dv, m1'), None => guard (q = 1)%Qp; Some (m1', m2, dv)
| Some (q1, dv, m1'), Some (q2, _, m2') => guard (q1 + q2 = 1)%Qp; Some (m1', m2', dv)
| None, Some (m2', q, dv) => guard (q = 1)%Qp; Some (m1, m2', dv)
| Some (m1', q, dv), None => guard (q = 1)%Qp; Some (m1', m2, dv)
| Some (m1', q1, dv), Some (m2', q2, _) => guard (q1 + q2 = 1)%Qp; Some (m1', m2', dv)
| _, _ => None
end.
End denv.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment