summaryrefslogtreecommitdiff
path: root/checker/reduction.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/reduction.ml')
-rw-r--r--checker/reduction.ml196
1 files changed, 139 insertions, 57 deletions
diff --git a/checker/reduction.ml b/checker/reduction.ml
index ec16aa26..4e508dc7 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -1,11 +1,14 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+open Names
open CErrors
open Util
open Cic
@@ -42,8 +45,8 @@ 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) ->
bal=0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 s2
| (Zfix(_,a1)::s1, Zfix(_,a2)::s2) ->
bal=0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2
@@ -52,7 +55,7 @@ let compare_stack_shape stk1 stk2 =
type lft_constr_stack_elt =
Zlapp of (lift * fconstr) array
- | Zlproj of Names.projection * lift
+ | Zlproj of Names.Projection.t * lift
| Zlfix of (lift * fconstr) * lft_constr_stack
| Zlcase of case_info * lift * fconstr * fconstr array
and lft_constr_stack = lft_constr_stack_elt list
@@ -78,8 +81,7 @@ let pure_stack lfts stk =
(l, Zlfix((lfx,fx),pa)::pstk)
| (ZcaseT(ci,p,br,env),(l,pstk)) ->
(l,Zlcase(ci,l,mk_clos env p,mk_clos_vect env br)::pstk)
- | (Zcase(ci,p,br),(l,pstk)) ->
- (l,Zlcase(ci,l,p,br)::pstk)) in
+ ) in
snd (pure_rec lfts stk)
(****************************************************************************)
@@ -117,6 +119,10 @@ let beta_appvect c v =
(* Conversion *)
(********************************************************************)
+type conv_pb =
+ | CONV
+ | CUMUL
+
(* Conversion utility functions *)
type 'a conversion_function = env -> 'a -> 'a -> unit
@@ -137,7 +143,7 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 =
| (Zlfix(fx1,a1),Zlfix(fx2,a2)) ->
f fx1 fx2; cmp_rec a1 a2
| (Zlproj (c1,l1),Zlproj (c2,l2)) ->
- if not (Names.eq_con_chk
+ if not (Names.Constant.UserOrd.equal
(Names.Projection.constant c1)
(Names.Projection.constant c2)) then
raise NotConvertible
@@ -152,11 +158,55 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 =
cmp_rec (pure_stack lft1 stk1) (pure_stack lft2 stk2)
else raise NotConvertible
-(* Convertibility of sorts *)
+let convert_inductive_instances cv_pb cumi u u' univs =
+ let len_instance =
+ Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) in
+ if not ((len_instance = Univ.Instance.length u) &&
+ (len_instance = Univ.Instance.length u')) then
+ anomaly (Pp.str "Invalid inductive subtyping encountered!")
+ else
+ let variance = Univ.ACumulativityInfo.variance cumi in
+ let comp_cst =
+ match cv_pb with
+ | CONV ->
+ Univ.Variance.eq_constraints variance u u' Univ.Constraint.empty
+ | CUMUL ->
+ Univ.Variance.leq_constraints variance u u' Univ.Constraint.empty
+ in
+ if (Univ.check_constraints comp_cst univs) then () else raise NotConvertible
+
+let convert_inductives
+ cv_pb (mind, ind) u1 sv1 u2 sv2 univs =
+ match mind.mind_universes with
+ | Monomorphic_ind _ | Polymorphic_ind _ -> convert_universes univs u1 u2
+ | Cumulative_ind cumi ->
+ let num_param_arity =
+ mind.mind_nparams + mind.mind_packets.(ind).mind_nrealargs
+ in
+ if not (num_param_arity = sv1 && num_param_arity = sv2) then
+ convert_universes univs u1 u2
+ else
+ convert_inductive_instances cv_pb cumi u1 u2 univs
+
+let convert_constructors
+ (mind, ind, cns) u1 sv1 u2 sv2 univs =
+ match mind.mind_universes with
+ | Monomorphic_ind _ | Polymorphic_ind _ -> convert_universes univs u1 u2
+ | Cumulative_ind cumi ->
+ let num_cnstr_args =
+ let nparamsctxt =
+ mind.mind_nparams + mind.mind_packets.(ind).mind_nrealargs
+ in
+ nparamsctxt + mind.mind_packets.(ind).mind_consnrealargs.(cns - 1)
+ in
+ if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then
+ convert_universes univs u1 u2
+ else
+ (** By invariant, both constructors have a common supertype,
+ so they are convertible _at that type_. *)
+ ()
-type conv_pb =
- | CONV
- | CUMUL
+(* Convertibility of sorts *)
let sort_cmp env univ pb s0 s1 =
match (s0,s1) with
@@ -176,9 +226,9 @@ let sort_cmp env univ pb s0 s1 =
then begin
if !Flags.debug then begin
let op = match pb with CONV -> "=" | CUMUL -> "<=" in
- Printf.eprintf "sort_cmp: %s\n%!" Pp.(string_of_ppcmds
- (str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut()
- ++ Univ.pr_universes univ))
+ Format.eprintf "sort_cmp: @[%a@]\n%!" Pp.pp_with Pp.(
+ str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut()
+ ++ Univ.pr_universes univ)
end;
raise NotConvertible
end
@@ -190,7 +240,6 @@ let rec no_arg_available = function
| Zshift _ :: stk -> no_arg_available stk
| Zapp v :: stk -> Array.length v = 0 && no_arg_available stk
| Zproj _ :: _ -> true
- | Zcase _ :: _ -> true
| ZcaseT _ :: _ -> true
| Zfix _ :: _ -> true
@@ -203,7 +252,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
@@ -213,13 +261,12 @@ let rec no_case_available = function
| Zshift _ :: stk -> no_case_available stk
| Zapp _ :: stk -> no_case_available stk
| Zproj (_,_,_) :: _ -> false
- | Zcase _ :: _ -> false
| ZcaseT _ :: _ -> false
| Zfix _ :: _ -> true
let in_whnf (t,stk) =
match fterm_of t with
- | (FLetIn _ | FCase _ | FCaseT _ | FApp _ | FCLOS _ | FLIFT _ | FCast _) -> false
+ | (FLetIn _ | FCaseT _ | FApp _ | FCLOS _ | FLIFT _ | FCast _) -> false
| FLambda _ -> no_arg_available stk
| FConstruct _ -> no_case_available stk
| FCoFix _ -> no_case_available stk
@@ -227,16 +274,34 @@ let in_whnf (t,stk) =
| (FFlex _ | FProd _ | FEvar _ | FInd _ | FAtom _ | FRel _ | FProj _) -> true
| FLOCKED -> assert false
-let oracle_order fl1 fl2 =
- match fl1,fl2 with
- ConstKey c1, ConstKey c2 -> (*height c1 > height c2*)false
- | _, ConstKey _ -> true
- | _ -> false
-
-let unfold_projection infos p c =
- let pb = lookup_projection p (infos_env infos) in
- let s = Zproj (pb.proj_npars, pb.proj_arg, p) in
- (c, s)
+let default_level = Level 0
+
+let get_strategy { var_opacity; cst_opacity } = function
+ | VarKey id ->
+ (try Names.Id.Map.find id var_opacity
+ with Not_found -> default_level)
+ | ConstKey (c, _) ->
+ (try Names.Cmap.find c cst_opacity
+ with Not_found -> default_level)
+ | RelKey _ -> Expand
+
+let oracle_order infos l2r k1 k2 =
+ let o = Closure.oracle_of_infos infos in
+ match get_strategy o k1, get_strategy o k2 with
+ | Expand, Expand -> l2r
+ | Expand, (Opaque | Level _) -> true
+ | (Opaque | Level _), Expand -> false
+ | Opaque, Opaque -> l2r
+ | Level _, Opaque -> true
+ | Opaque, Level _ -> false
+ | Level n1, Level n2 ->
+ if Int.equal n1 n2 then l2r
+ else n1 < n2
+
+let eq_table_key univ =
+ Names.eq_table_key (fun (c1,u1) (c2,u2) ->
+ Constant.UserOrd.equal c1 c2 &&
+ Univ.Instance.check_eq univ u1 u2)
(* Conversion between [lft1]term1 and [lft2]term2 *)
let rec ccnv univ cv_pb infos lft1 lft2 term1 term2 =
@@ -284,13 +349,13 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
(* 2 constants, 2 local defined vars or 2 defined rels *)
| (FFlex fl1, FFlex fl2) ->
(try (* try first intensional equality *)
- if eq_table_key fl1 fl2
+ if eq_table_key univ fl1 fl2
then convert_stacks univ infos lft1 lft2 v1 v2
else raise NotConvertible
with NotConvertible ->
(* else the oracle tells which constant is to be expanded *)
let (app1,app2) =
- if oracle_order fl1 fl2 then
+ if oracle_order infos false fl1 fl2 then
match unfold_reference infos fl1 with
| Some def1 -> ((lft1, whd_stack infos def1 v1), appr2)
| None ->
@@ -307,12 +372,12 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
eqappr univ cv_pb infos app1 app2)
| (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
+ let s1 = unfold_projection (infos_env infos) p1 in
+ eqappr univ cv_pb infos (lft1, whd_stack infos c1 (s1 :: v1)) appr2
| (_, FProj (p2,c2)) ->
- let (def2, s2) = unfold_projection infos p2 c2 in
- eqappr univ cv_pb infos appr1 (lft2, whd_stack infos def2 (s2 :: v2))
+ let s2 = unfold_projection (infos_env infos) p2 in
+ eqappr univ cv_pb infos appr1 (lft2, whd_stack infos c2 (s2 :: v2))
(* other constructors *)
| (FLambda _, FLambda _) ->
@@ -333,13 +398,13 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
(* Eta-expansion on the fly *)
| (FLambda _, _) ->
if v1 <> [] then
- anomaly (Pp.str "conversion was given unreduced term (FLambda)");
+ anomaly (Pp.str "conversion was given unreduced term (FLambda).");
let (_,_ty1,bd1) = destFLambda mk_clos hd1 in
eqappr univ CONV infos
(el_lift lft1,(bd1,[])) (el_lift lft2,(hd2,eta_expand_stack v2))
| (_, FLambda _) ->
if v2 <> [] then
- anomaly (Pp.str "conversion was given unreduced term (FLambda)");
+ anomaly (Pp.str "conversion was given unreduced term (FLambda).");
let (_,_ty2,bd2) = destFLambda mk_clos hd2 in
eqappr univ CONV infos
(el_lift lft1,(hd1,eta_expand_stack v1)) (el_lift lft2,(bd2,[]))
@@ -375,18 +440,37 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
(* Inductive types: MutInd MutConstruct Fix Cofix *)
| (FInd (ind1,u1), FInd (ind2,u2)) ->
- if mind_equiv_infos infos ind1 ind2
- then
- (let () = convert_universes univ u1 u2 in
- convert_stacks univ infos lft1 lft2 v1 v2)
- else raise NotConvertible
-
- | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) ->
- if Int.equal j1 j2 && mind_equiv_infos infos ind1 ind2
- then
- (let () = convert_universes univ u1 u2 in
- convert_stacks univ infos lft1 lft2 v1 v2)
- else raise NotConvertible
+ if mind_equiv_infos infos ind1 ind2 then
+ if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then
+ begin
+ convert_universes univ u1 u2;
+ convert_stacks univ infos lft1 lft2 v1 v2
+ end
+ else
+ let mind = Environ.lookup_mind (fst ind1) (infos_env infos) in
+ let () =
+ convert_inductives cv_pb (mind, snd ind1) u1 (stack_args_size v1)
+ u2 (stack_args_size v2) univ
+ in
+ convert_stacks univ infos lft1 lft2 v1 v2
+ else raise NotConvertible
+
+ | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) ->
+ if Int.equal j1 j2 && mind_equiv_infos infos ind1 ind2 then
+ if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then
+ begin
+ convert_universes univ u1 u2;
+ convert_stacks univ infos lft1 lft2 v1 v2
+ end
+ else
+ let mind = Environ.lookup_mind (fst ind1) (infos_env infos) in
+ let () =
+ convert_constructors
+ (mind, snd ind1, j1) u1 (stack_args_size v1)
+ u2 (stack_args_size v2) univ
+ in
+ convert_stacks univ infos lft1 lft2 v1 v2
+ else raise NotConvertible
(* Eta expansion of records *)
| (FConstruct ((ind1,j1),u1), _) ->
@@ -432,8 +516,8 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
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 *)
@@ -479,7 +563,7 @@ let vm_conv cv_pb = fconv cv_pb true
let hnf_prod_app env t n =
match whd_all env t with
| Prod (_,_,b) -> subst1 n b
- | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product")
+ | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product.")
let hnf_prod_applist env t nl =
List.fold_left (hnf_prod_app env) t nl
@@ -508,7 +592,6 @@ let dest_prod_assum env =
| LetIn (x,b,t,c) ->
let d = LocalDef (x,b,t) in
prodec_rec (push_rel d env) (d::l) c
- | Cast (c,_,_) -> prodec_rec env l c
| _ ->
let rty' = whd_all env rty in
if Term.eq_constr rty' rty then l, rty
@@ -526,7 +609,6 @@ let dest_lam_assum env =
| LetIn (x,b,t,c) ->
let d = LocalDef (x,b,t) in
lamec_rec (push_rel d env) (d::l) c
- | Cast (c,_,_) -> lamec_rec env l c
| _ -> l,rty
in
lamec_rec env empty_rel_context
@@ -536,5 +618,5 @@ let dest_arity env c =
let l, c = dest_prod_assum env c in
match c with
| Sort s -> l,s
- | _ -> error "not an arity"
+ | _ -> user_err Pp.(str "not an arity")
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-08 03:04:33 +0000