diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 39 |
1 files changed, 21 insertions, 18 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 8ab040b3b1..18a0637efa 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -179,7 +179,7 @@ sig type 'a member = | App of 'a app_node - | Case of case_info * 'a * 'a array + | Case of case_info * 'a * ('a, EInstance.t) case_invert * 'a array | Proj of Projection.t | Fix of ('a, 'a) pfixpoint * 'a t | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red @@ -231,7 +231,7 @@ struct type 'a member = | App of 'a app_node - | Case of case_info * 'a * 'a array + | Case of case_info * 'a * ('a, EInstance.t) case_invert * 'a array | Proj of Projection.t | Fix of ('a, 'a) pfixpoint * 'a t | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red @@ -244,7 +244,7 @@ struct let pr_c x = hov 1 (pr_c x) in match member with | App app -> str "ZApp" ++ pr_app_node pr_c app - | Case (_,_,br) -> + | Case (_,_,_,br) -> str "ZCase(" ++ prvect_with_sep (pr_bar) pr_c br ++ str ")" @@ -285,7 +285,7 @@ struct ([],[]) -> Int.equal bal 0 | (App (i,_,j)::s1, _) -> compare_rec (bal + j + 1 - i) s1 stk2 | (_, App (i,_,j)::s2) -> compare_rec (bal - j - 1 + i) stk1 s2 - | (Case(c1,_,_)::s1, Case(c2,_,_)::s2) -> + | (Case(c1,_,_,_)::s1, Case(c2,_,_,_)::s2) -> Int.equal bal 0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 s2 | (Proj (p)::s1, Proj(p2)::s2) -> Int.equal bal 0 && compare_rec 0 s1 s2 @@ -305,7 +305,7 @@ struct let t1,l1 = decomp_node_last n1 q1 in let t2,l2 = decomp_node_last n2 q2 in aux (f o t1 t2) l1 l2 - | Case (_,t1,a1) :: q1, Case (_,t2,a2) :: q2 -> + | Case (_,t1,_,a1) :: q1, Case (_,t2,_,a2) :: q2 -> aux (Array.fold_left2 f (f o t1 t2) a1 a2) q1 q2 | Proj (p1) :: q1, Proj (p2) :: q2 -> aux o q1 q2 @@ -321,7 +321,8 @@ struct | App (i,a,j) -> let le = j - i + 1 in App (0,Array.map f (Array.sub a i le), le-1) - | Case (info,ty,br) -> Case (info, f ty, Array.map f br) + | Case (info,ty,iv,br) -> + Case (info, f ty, map_invert f iv, Array.map f br) | Fix ((r,(na,ty,bo)),arg) -> Fix ((r,(na,Array.map f ty, Array.map f bo)),map f arg) | Primitive (p,c,args,kargs) -> @@ -403,7 +404,7 @@ struct then a else Array.sub a i (j - i + 1) in zip (mkApp (f, a'), s) - | f, (Case (ci,rt,br)::s) -> zip (mkCase (ci,rt,f,br), s) + | f, (Case (ci,rt,iv,br)::s) -> zip (mkCase (ci,rt,iv,f,br), s) | f, (Fix (fix,st)::s) -> zip (mkFix fix, st @ (append_app [|f|] s)) | f, (Proj (p)::s) -> zip (mkProj (p,f),s) @@ -536,12 +537,13 @@ let reduce_and_refold_cofix recfun env sigma cofix sk = let reduce_mind_case sigma mia = match EConstr.kind sigma mia.mconstr with | Construct ((ind_sp,i),u) -> -(* let ncargs = (fst mia.mci).(i-1) in*) +(* let ncargs = (fst mia.mci).(i-1) in*) let real_cargs = List.skipn mia.mci.ci_npar mia.mcargs in applist (mia.mlf.(i-1),real_cargs) | CoFix cofix -> let cofix_def = contract_cofix sigma cofix in - mkCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf) + (* XXX Is NoInvert OK here? *) + mkCase (mia.mci, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf) | _ -> assert false (* contracts fix==FIX[nl;i](A1...Ak;[F1...Fk]{B1....Bk}) to produce @@ -805,8 +807,8 @@ let rec whd_state_gen flags env sigma = | _ -> fold ()) | _ -> fold ()) - | Case (ci,p,d,lf) -> - whrec (d, Stack.Case (ci,p,lf) :: stack) + | Case (ci,p,iv,d,lf) -> + whrec (d, Stack.Case (ci,p,iv,lf) :: stack) | Fix ((ri,n),_ as f) -> (match Stack.strip_n_app ri.(n) stack with @@ -819,7 +821,7 @@ let rec whd_state_gen flags env sigma = let use_fix = CClosure.RedFlags.red_set flags CClosure.RedFlags.fFIX in if use_match || use_fix then match Stack.strip_app stack with - |args, (Stack.Case(ci, _, lf)::s') when use_match -> + |args, (Stack.Case(ci, _, _, lf)::s') when use_match -> whrec (lf.(c-1), (Stack.tail ci.ci_npar args) @ s') |args, (Stack.Proj (p)::s') when use_match -> whrec (Stack.nth args (Projection.npars p + Projection.arg p), s') @@ -901,8 +903,8 @@ let local_whd_state_gen flags _env sigma = | Proj (p,c) when CClosure.RedFlags.red_projection flags p -> (whrec (c, Stack.Proj (p) :: stack)) - | Case (ci,p,d,lf) -> - whrec (d, Stack.Case (ci,p,lf) :: stack) + | Case (ci,p,iv,d,lf) -> + whrec (d, Stack.Case (ci,p,iv,lf) :: stack) | Fix ((ri,n),_ as f) -> (match Stack.strip_n_app ri.(n) stack with @@ -920,7 +922,7 @@ let local_whd_state_gen flags _env sigma = let use_fix = CClosure.RedFlags.red_set flags CClosure.RedFlags.fFIX in if use_match || use_fix then match Stack.strip_app stack with - |args, (Stack.Case(ci, _, lf)::s') when use_match -> + |args, (Stack.Case(ci, _, _, lf)::s') when use_match -> whrec (lf.(c-1), (Stack.tail ci.ci_npar args) @ s') |args, (Stack.Proj (p) :: s') when use_match -> whrec (Stack.nth args (Projection.npars p + Projection.arg p), s') @@ -1035,7 +1037,7 @@ let clos_norm_flags flgs env sigma t = try let evars ev = safe_evar_value sigma ev in EConstr.of_constr (CClosure.norm_val - (CClosure.create_clos_infos ~evars flgs env) + (CClosure.create_clos_infos ~univs:(Evd.universes sigma) ~evars flgs env) (CClosure.create_tab ()) (CClosure.inject (EConstr.Unsafe.to_constr t))) with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term") @@ -1044,7 +1046,7 @@ let clos_whd_flags flgs env sigma t = try let evars ev = safe_evar_value sigma ev in EConstr.of_constr (CClosure.whd_val - (CClosure.create_clos_infos ~evars flgs env) + (CClosure.create_clos_infos ~univs:(Evd.universes sigma) ~evars flgs env) (CClosure.create_tab ()) (CClosure.inject (EConstr.Unsafe.to_constr t))) with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term") @@ -1148,7 +1150,8 @@ let sigma_check_inductive_instances cv_pb variance u1 u2 sigma = let sigma_univ_state = let open Reduction in - { compare_sorts = sigma_compare_sorts; + { compare_graph = Evd.universes; + compare_sorts = sigma_compare_sorts; compare_instances = sigma_compare_instances; compare_cumul_instances = sigma_check_inductive_instances; } |