diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-06 11:44:53 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-06 11:46:04 +0200 |
| commit | 7a01de25661456406cc2d4a0edcef81af643889c (patch) | |
| tree | 31edb58e9936d488e7a502d2e63ae1e515e6f978 /checker/reduction.ml | |
| parent | 5d888e0f4943877df04114a0513d70687d9b2c11 (diff) | |
Cleanup code for looking up projection bodies.
Diffstat (limited to 'checker/reduction.ml')
| -rw-r--r-- | checker/reduction.ml | 44 |
1 files changed, 9 insertions, 35 deletions
diff --git a/checker/reduction.ml b/checker/reduction.ml index b8677f5aa..0886ab748 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -216,13 +216,9 @@ let oracle_order fl1 fl2 = | _ -> false let unfold_projection infos p c = - (* if RedFlags.red_set infos.i_flags (RedFlags.fCONST p) then *) - (match try Some (lookup_projection p (infos_env infos)) with Not_found -> None with - | Some pb -> - let s = Zproj (pb.proj_npars, pb.proj_arg, p) in - Some (c, s) - | None -> None) - (* else None *) + let pb = lookup_projection p (infos_env infos) in + let s = Zproj (pb.proj_npars, pb.proj_arg, p) in + (c, s) (* Conversion between [lft1]term1 and [lft2]term2 *) let rec ccnv univ cv_pb infos lft1 lft2 term1 term2 = @@ -297,35 +293,13 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = | None -> raise NotConvertible) in eqappr univ cv_pb infos app1 app2) - | (FProj (p1,c1), FProj (p2, c2)) -> - (* Projections: prefer unfolding to first-order unification, - which will happen naturally if the terms c1, c2 are not in constructor - form *) - (match unfold_projection infos p1 c1 with - | Some (def1,s1) -> - eqappr univ cv_pb infos (lft1, whd_stack infos def1 (s1 :: v1)) appr2 - | None -> - match unfold_projection infos p2 c2 with - | Some (def2,s2) -> - eqappr univ cv_pb infos appr1 (lft2, whd_stack infos def2 (s2 :: v2)) - | None -> - if Names.eq_con_chk p1 p2 && compare_stack_shape v1 v2 then - let () = ccnv univ CONV infos el1 el2 c1 c2 in - convert_stacks univ infos lft1 lft2 v1 v2 - else (* Two projections in WHNF: unfold *) - raise NotConvertible) - - | (FProj (p1,c1), t2) -> - (match unfold_projection infos p1 c1 with - | Some (def1,s1) -> - eqappr univ cv_pb infos (lft1, whd_stack infos def1 (s1 :: v1)) appr2 - | None -> raise NotConvertible) - + | (FProj (p1,c1), _) -> + let (def1, s1) = unfold_projection infos p1 c1 in + eqappr univ cv_pb infos (lft1, whd_stack infos def1 (s1 :: v1)) appr2 + | (_, FProj (p2,c2)) -> - (match unfold_projection infos p2 c2 with - | Some (def2,s2) -> - eqappr univ cv_pb infos appr1 (lft2, whd_stack infos def2 (s2 :: v2)) - | None -> raise NotConvertible) + let (def2, s2) = unfold_projection infos p2 c2 in + eqappr univ cv_pb infos appr1 (lft2, whd_stack infos def2 (s2 :: v2)) (* other constructors *) | (FLambda _, FLambda _) -> |