diff options
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 38 |
1 files changed, 16 insertions, 22 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 939eeef5d5..1105550113 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -54,8 +54,7 @@ let compare_stack_shape stk1 stk2 = | (_, Zapp l2::s2) -> compare_rec (bal-Array.length l2) stk1 s2 | (Zproj (n1,m1,p1)::s1, Zproj (n2,m2,p2)::s2) -> Int.equal bal 0 && compare_rec 0 s1 s2 - | ((Zcase(c1,_,_)|ZcaseT(c1,_,_,_))::s1, - (Zcase(c2,_,_)|ZcaseT(c2,_,_,_))::s2) -> + | (ZcaseT(c1,_,_,_)::s1, ZcaseT(c2,_,_,_)::s2) -> Int.equal bal 0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 s2 | (Zfix(_,a1)::s1, Zfix(_,a2)::s2) -> Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2 @@ -89,9 +88,8 @@ let pure_stack lfts stk = let (lfx,pa) = pure_rec l a in (l, Zlfix((lfx,fx),pa)::pstk) | (ZcaseT(ci,p,br,e),(l,pstk)) -> - (l,Zlcase(ci,l,mk_clos e p,Array.map (mk_clos e) br)::pstk) - | (Zcase(ci,p,br),(l,pstk)) -> - (l,Zlcase(ci,l,p,br)::pstk)) in + (l,Zlcase(ci,l,mk_clos e p,Array.map (mk_clos e) br)::pstk)) + in snd (pure_rec lfts stk) (****************************************************************************) @@ -147,7 +145,7 @@ let betazeta_appvect n c v = (* Conversion utility functions *) type 'a conversion_function = env -> 'a -> 'a -> unit type 'a trans_conversion_function = Names.transparent_state -> 'a conversion_function -type 'a universe_conversion_function = env -> Univ.universes -> 'a -> 'a -> unit +type 'a universe_conversion_function = env -> UGraph.t -> 'a -> 'a -> unit type 'a trans_universe_conversion_function = Names.transparent_state -> 'a universe_conversion_function @@ -180,7 +178,7 @@ type 'a universe_state = 'a * 'a universe_compare type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a -> 'b -type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.constraints +type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.constraints let sort_cmp_universes env pb s0 s1 (u, check) = (check.compare env pb s0 s1 u, check) @@ -235,7 +233,6 @@ let rec no_arg_available = function | Zshift _ :: stk -> no_arg_available stk | Zapp v :: stk -> Int.equal (Array.length v) 0 && no_arg_available stk | Zproj _ :: _ -> true - | Zcase _ :: _ -> true | ZcaseT _ :: _ -> true | Zfix _ :: _ -> true @@ -248,7 +245,6 @@ let rec no_nth_arg_available n = function if n >= k then no_nth_arg_available (n-k) stk else false | Zproj _ :: _ -> true - | Zcase _ :: _ -> true | ZcaseT _ :: _ -> true | Zfix _ :: _ -> true @@ -258,13 +254,12 @@ let rec no_case_available = function | Zshift _ :: stk -> no_case_available stk | Zapp _ :: stk -> no_case_available stk | Zproj (_,_,p) :: _ -> false - | Zcase _ :: _ -> false | ZcaseT _ :: _ -> false | Zfix _ :: _ -> true let in_whnf (t,stk) = match fterm_of t with - | (FLetIn _ | FCase _ | FCaseT _ | FApp _ + | (FLetIn _ | FCaseT _ | FApp _ | FCLOS _ | FLIFT _ | FCast _) -> false | FLambda _ -> no_arg_available stk | FConstruct _ -> no_case_available stk @@ -530,8 +525,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = else raise NotConvertible (* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *) - | ( (FLetIn _, _) | (FCase _,_) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_) - | (_, FLetIn _) | (_,FCase _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _) + | ( (FLetIn _, _) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_) + | (_, FLetIn _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _) | (FLOCKED,_) | (_,FLOCKED) ) -> assert false (* In all other cases, terms are not convertible *) @@ -563,10 +558,10 @@ let clos_fconv trans cv_pb l2r evars env univs t1 t2 = let check_eq univs u u' = - if not (check_eq univs u u') then raise NotConvertible + if not (UGraph.check_eq univs u u') then raise NotConvertible let check_leq univs u u' = - if not (check_leq univs u u') then raise NotConvertible + if not (UGraph.check_leq univs u u') then raise NotConvertible let check_sort_cmp_universes env pb s0 s1 univs = match (s0,s1) with @@ -593,7 +588,7 @@ let checked_sort_cmp_universes env pb s0 s1 univs = check_sort_cmp_universes env pb s0 s1 univs; univs let check_convert_instances ~flex u u' univs = - if Univ.Instance.check_eq univs u u' then univs + if UGraph.check_eq_instances univs u u' then univs else raise NotConvertible let checked_universes = @@ -601,12 +596,12 @@ let checked_universes = compare_instances = check_convert_instances } let infer_eq (univs, cstrs as cuniv) u u' = - if Univ.check_eq univs u u' then cuniv + if UGraph.check_eq univs u u' then cuniv else univs, (Univ.enforce_eq u u' cstrs) let infer_leq (univs, cstrs as cuniv) u u' = - if Univ.check_leq univs u u' then cuniv + if UGraph.check_leq univs u u' then cuniv else let cstrs' = Univ.enforce_leq u u' cstrs in univs, cstrs' @@ -635,7 +630,7 @@ let infer_cmp_universes env pb s0 s1 univs = let infer_convert_instances ~flex u u' (univs,cstrs) = (univs, Univ.enforce_eq_instances u u' cstrs) -let inferred_universes : (Univ.universes * Univ.Constraint.t) universe_compare = +let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare = { compare = infer_cmp_universes; compare_instances = infer_convert_instances } @@ -721,9 +716,8 @@ let vm_conv cv_pb env t1 t2 = try !vm_conv cv_pb env t1 t2 with Not_found | Invalid_argument _ -> - (Pp.msg_warning - (Pp.str "Bytecode compilation failed, falling back to default conversion"); - fconv cv_pb false (fun _->None) env t1 t2) + Pp.msg_warning (Pp.str "Bytecode compilation failed, falling back to standard conversion"); + fconv cv_pb false (fun _->None) env t1 t2 let default_conv cv_pb ?(l2r=false) env t1 t2 = fconv cv_pb false (fun _ -> None) env t1 t2 |