Case c of c1 | c2 .. | cn end *) -let mkCase (ci, p, iv, c, ac) = Case (ci, p, iv, c, ac) +let mkCase (ci, u, params, p, iv, c, ac) = Case (ci, u, params, p, iv, c, ac) (* If recindxs = [|i1,...in|] funnames = [|f1,...fn|] @@ -425,7 +435,7 @@ let destConstruct c = match kind c with (* Destructs a term
Case c of lc1 | lc2 .. | lcn end *) let destCase c = match kind c with - | Case (ci,p,iv,c,v) -> (ci,p,iv,c,v) + | Case (ci,u,params,p,iv,c,v) -> (ci,u,params,p,iv,c,v) | _ -> raise DestKO let destProj c = match kind c with @@ -484,7 +494,8 @@ let fold f acc c = match kind c with | App (c,l) -> Array.fold_left f (f acc c) l | Proj (_p,c) -> f acc c | Evar (_,l) -> List.fold_left f acc l - | Case (_,p,iv,c,bl) -> Array.fold_left f (f (fold_invert f (f acc p) iv) c) bl + | Case (_,_,pms,(_,p),iv,c,bl) -> + Array.fold_left (fun acc (_, b) -> f acc b) (f (fold_invert f (f (Array.fold_left f acc pms) p) iv) c) bl | Fix (_,(_lna,tl,bl)) -> Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl | CoFix (_,(_lna,tl,bl)) -> @@ -511,7 +522,8 @@ let iter f c = match kind c with | App (c,l) -> f c; Array.iter f l | Proj (_p,c) -> f c | Evar (_,l) -> List.iter f l - | Case (_,p,iv,c,bl) -> f p; iter_invert f iv; f c; Array.iter f bl + | Case (_,_,pms,p,iv,c,bl) -> + Array.iter f pms; f (snd p); iter_invert f iv; f c; Array.iter (fun (_, b) -> f b) bl | Fix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl | CoFix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl | Array(_u,t,def,ty) -> Array.iter f t; f def; f ty @@ -531,7 +543,12 @@ let iter_with_binders g f n c = match kind c with | LetIn (_,b,t,c) -> f n b; f n t; f (g n) c | App (c,l) -> f n c; Array.Fun1.iter f n l | Evar (_,l) -> List.iter (fun c -> f n c) l - | Case (_,p,iv,c,bl) -> f n p; iter_invert (f n) iv; f n c; Array.Fun1.iter f n bl + | Case (_,_,pms,p,iv,c,bl) -> + Array.Fun1.iter f n pms; + f (iterate g (Array.length (fst p)) n) (snd p); + iter_invert (f n) iv; + f n c; + Array.Fun1.iter (fun n (ctx, b) -> f (iterate g (Array.length ctx) n) b) n bl | Proj (_p,c) -> f n c | Fix (_,(_,tl,bl)) -> Array.Fun1.iter f n tl; @@ -560,7 +577,11 @@ let fold_constr_with_binders g f n acc c = | App (c,l) -> Array.fold_left (f n) (f n acc c) l | Proj (_p,c) -> f n acc c | Evar (_,l) -> List.fold_left (f n) acc l - | Case (_,p,iv,c,bl) -> Array.fold_left (f n) (f n (fold_invert (f n) (f n acc p) iv) c) bl + | Case (_,_,pms,p,iv,c,bl) -> + let fold_ctx n accu (nas, c) = + f (iterate g (Array.length nas) n) accu c + in + Array.fold_left (fold_ctx n) (f n (fold_invert (f n) (fold_ctx n (Array.fold_left (f n) acc pms) p) iv) c) bl | Fix (_,(_,tl,bl)) -> let n' = iterate g (Array.length tl) n in let fd = Array.map2 (fun t b -> (t,b)) tl bl in @@ -576,53 +597,30 @@ let fold_constr_with_binders g f n acc c = not recursive and the order with which subterms are processed is not specified *) -let rec map_under_context f n d = - if n = 0 then f d else - match kind d with - | LetIn (na,b,t,c) -> - let b' = f b in - let t' = f t in - let c' = map_under_context f (n-1) c in - if b' == b && t' == t && c' == c then d - else mkLetIn (na,b',t',c') - | Lambda (na,t,b) -> - let t' = f t in - let b' = map_under_context f (n-1) b in - if t' == t && b' == b then d - else mkLambda (na,t',b') - | _ -> CErrors.anomaly (Pp.str "Ill-formed context") - -let map_branches f ci bl = - let nl = Array.map List.length ci.ci_pp_info.cstr_tags in - let bl' = Array.map2 (map_under_context f) nl bl in +let map_under_context f d = + let (nas, p) = d in + let p' = f p in + if p' == p then d else (nas, p') + +let map_branches f bl = + let bl' = Array.map (map_under_context f) bl in if Array.for_all2 (==) bl' bl then bl else bl' -let map_return_predicate f ci p = - map_under_context f (List.length ci.ci_pp_info.ind_tags) p - -let rec map_under_context_with_binders g f l n d = - if n = 0 then f l d else - match kind d with - | LetIn (na,b,t,c) -> - let b' = f l b in - let t' = f l t in - let c' = map_under_context_with_binders g f (g l) (n-1) c in - if b' == b && t' == t && c' == c then d - else mkLetIn (na,b',t',c') - | Lambda (na,t,b) -> - let t' = f l t in - let b' = map_under_context_with_binders g f (g l) (n-1) b in - if t' == t && b' == b then d - else mkLambda (na,t',b') - | _ -> CErrors.anomaly (Pp.str "Ill-formed context") - -let map_branches_with_binders g f l ci bl = - let tags = Array.map List.length ci.ci_pp_info.cstr_tags in - let bl' = Array.map2 (map_under_context_with_binders g f l) tags bl in +let map_return_predicate f p = + map_under_context f p + +let map_under_context_with_binders g f l d = + let (nas, p) = d in + let l = iterate g (Array.length nas) l in + let p' = f l p in + if p' == p then d else (nas, p') + +let map_branches_with_binders g f l bl = + let bl' = Array.map (map_under_context_with_binders g f l) bl in if Array.for_all2 (==) bl' bl then bl else bl' -let map_return_predicate_with_binders g f l ci p = - map_under_context_with_binders g f l (List.length ci.ci_pp_info.ind_tags) p +let map_return_predicate_with_binders g f l p = + map_under_context_with_binders g f l p let map_invert f = function | NoInvert -> NoInvert @@ -631,7 +629,7 @@ let map_invert f = function if args == args' then orig else CaseInvert {univs;args=args';} -let map_gen userview f c = match kind c with +let map f c = match kind c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ | Int _ | Float _) -> c | Cast (b,k,t) -> @@ -668,20 +666,14 @@ let map_gen userview f c = match kind c with let l' = List.Smart.map f l in if l'==l then c else mkEvar (e, l') - | Case (ci,p,iv,b,bl) when userview -> - let b' = f b in - let iv' = map_invert f iv in - let p' = map_return_predicate f ci p in - let bl' = map_branches f ci bl in - if b'==b && iv'==iv && p'==p && bl'==bl then c - else mkCase (ci, p', iv', b', bl') - | Case (ci,p,iv,b,bl) -> + | Case (ci,u,pms,p,iv,b,bl) -> + let pms' = Array.Smart.map f pms in let b' = f b in let iv' = map_invert f iv in - let p' = f p in - let bl' = Array.Smart.map f bl in - if b'==b && iv'==iv && p'==p && bl'==bl then c - else mkCase (ci, p', iv', b', bl') + let p' = map_return_predicate f p in + let bl' = map_branches f bl in + if b'==b && iv'==iv && p'==p && bl'==bl && pms'==pms then c + else mkCase (ci, u, pms', p', iv', b', bl') | Fix (ln,(lna,tl,bl)) -> let tl' = Array.Smart.map f tl in let bl' = Array.Smart.map f bl in @@ -699,9 +691,6 @@ let map_gen userview f c = match kind c with if def'==def && t==t' && ty==ty' then c else mkArray(u,t',def',ty') -let map_user_view = map_gen true -let map = map_gen false - (* Like {!map} but with an accumulator. *) let fold_map_invert f acc = function @@ -711,6 +700,18 @@ let fold_map_invert f acc = function if args==args' then acc, orig else acc, CaseInvert {univs;args=args';} +let fold_map_under_context f accu d = + let (nas, p) = d in + let accu, p' = f accu p in + if p' == p then accu, d else accu, (nas, p') + +let fold_map_branches f accu bl = + let accu, bl' = Array.Smart.fold_left_map (fold_map_under_context f) accu bl in + if Array.for_all2 (==) bl' bl then accu, bl else accu, bl' + +let fold_map_return_predicate f accu p = + fold_map_under_context f accu p + let fold_map f accu c = match kind c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ | Int _ | Float _) -> accu, c @@ -749,13 +750,14 @@ let fold_map f accu c = match kind c with let accu, l' = List.fold_left_map f accu l in if l'==l then accu, c else accu, mkEvar (e, l') - | Case (ci,p,iv,b,bl) -> - let accu, b' = f accu b in + | Case (ci,u,pms,p,iv,b,bl) -> + let accu, pms' = Array.Smart.fold_left_map f accu pms in + let accu, p' = fold_map_return_predicate f accu p in let accu, iv' = fold_map_invert f accu iv in - let accu, p' = f accu p in - let accu, bl' = Array.Smart.fold_left_map f accu bl in - if b'==b && iv'==iv && p'==p && bl'==bl then accu, c - else accu, mkCase (ci, p', iv', b', bl') + let accu, b' = f accu b in + let accu, bl' = fold_map_branches f accu bl in + if pms'==pms && p'==p && iv'==iv && b'==b && bl'==bl then accu, c + else accu, mkCase (ci, u, pms', p', iv', b', bl') | Fix (ln,(lna,tl,bl)) -> let accu, tl' = Array.Smart.fold_left_map f accu tl in let accu, bl' = Array.Smart.fold_left_map f accu bl in @@ -816,13 +818,14 @@ let map_with_binders g f l c0 = match kind c0 with let al' = List.Smart.map (fun c -> f l c) al in if al' == al then c0 else mkEvar (e, al') - | Case (ci, p, iv, c, bl) -> - let p' = f l p in + | Case (ci, u, pms, p, iv, c, bl) -> + let pms' = Array.Fun1.Smart.map f l pms in + let p' = map_return_predicate_with_binders g f l p in let iv' = map_invert (f l) iv in let c' = f l c in - let bl' = Array.Fun1.Smart.map f l bl in - if p' == p && iv' == iv && c' == c && bl' == bl then c0 - else mkCase (ci, p', iv', c', bl') + let bl' = map_branches_with_binders g f l bl in + if pms' == pms && p' == p && iv' == iv && c' == c && bl' == bl then c0 + else mkCase (ci, u, pms', p', iv', c', bl') | Fix (ln, (lna, tl, bl)) -> let tl' = Array.Fun1.Smart.map f l tl in let l' = iterate g (Array.length tl) l in @@ -886,6 +889,9 @@ let eq_invert eq leq_universes iv1 iv2 = leq_universes univs iv2.univs && Array.equal eq args iv2.args +let eq_under_context eq (_nas1, p1) (_nas2, p2) = + eq p1 p2 + let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t1 t2 = match kind_nocast_gen kind1 t1, kind_nocast_gen kind2 t2 with | Cast _, _ | _, Cast _ -> assert false (* kind_nocast *) @@ -911,8 +917,12 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t | Ind (c1,u1), Ind (c2,u2) -> Ind.CanOrd.equal c1 c2 && leq_universes (Some (GlobRef.IndRef c1, nargs)) u1 u2 | Construct (c1,u1), Construct (c2,u2) -> Construct.CanOrd.equal c1 c2 && leq_universes (Some (GlobRef.ConstructRef c1, nargs)) u1 u2 - | Case (_,p1,iv1,c1,bl1), Case (_,p2,iv2,c2,bl2) -> - eq 0 p1 p2 && eq_invert (eq 0) (leq_universes None) iv1 iv2 && eq 0 c1 c2 && Array.equal (eq 0) bl1 bl2 + | Case (ci1,u1,pms1,p1,iv1,c1,bl1), Case (ci2,u2,pms2,p2,iv2,c2,bl2) -> + (** FIXME: what are we doing with u1 = u2 ? *) + Ind.CanOrd.equal ci1.ci_ind ci2.ci_ind && leq_universes (Some (GlobRef.IndRef ci1.ci_ind, 0)) u1 u2 && + Array.equal (eq 0) pms1 pms2 && eq_under_context (eq 0) p1 p2 && + eq_invert (eq 0) (leq_universes None) iv1 iv2 && + eq 0 c1 c2 && Array.equal (eq_under_context (eq 0)) bl1 bl2 | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) -> Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 && Array.equal_norefl (eq 0) tl1 tl2 && Array.equal_norefl (eq 0) bl1 bl2 @@ -1063,6 +1073,9 @@ let constr_ord_int f t1 t2 = let fix_cmp (a1, i1) (a2, i2) = ((Array.compare Int.compare) =? Int.compare) a1 a2 i1 i2 in + let ctx_cmp f (_n1, p1) (_n2, p2) = + f p1 p2 + in match kind t1, kind t2 with | Cast (c1,_,_), _ -> f c1 t2 | _, Cast (c2,_,_) -> f t1 c2 @@ -1096,12 +1109,13 @@ let constr_ord_int f t1 t2 = | Ind _, _ -> -1 | _, Ind _ -> 1 | Construct (ct1,_u1), Construct (ct2,_u2) -> Construct.CanOrd.compare ct1 ct2 | Construct _, _ -> -1 | _, Construct _ -> 1 - | Case (_,p1,iv1,c1,bl1), Case (_,p2,iv2,c2,bl2) -> - let c = f p1 p2 in + | Case (_,_u1,pms1,p1,iv1,c1,bl1), Case (_,_u2,pms2,p2,iv2,c2,bl2) -> + let c = Array.compare f pms1 pms2 in + if Int.equal c 0 then let c = ctx_cmp f p1 p2 in if Int.equal c 0 then let c = compare_invert f iv1 iv2 in if Int.equal c 0 then let c = f c1 c2 in - if Int.equal c 0 then Array.compare f bl1 bl2 - else c else c else c + if Int.equal c 0 then Array.compare (ctx_cmp f) bl1 bl2 + else c else c else c else c | Case _, _ -> -1 | _, Case _ -> 1 | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) -> ((fix_cmp =? (Array.compare f)) ==? (Array.compare f)) @@ -1180,6 +1194,9 @@ let invert_eqeq iv1 iv2 = iv1.univs == iv2.univs && iv1.args == iv2.args +let hasheq_ctx (nas1, c1) (nas2, c2) = + array_eqeq nas1 nas2 && c1 == c2 + let hasheq t1 t2 = match t1, t2 with | Rel n1, Rel n2 -> n1 == n2 @@ -1197,8 +1214,11 @@ let hasheq t1 t2 = | Const (c1,u1), Const (c2,u2) -> c1 == c2 && u1 == u2 | Ind (ind1,u1), Ind (ind2,u2) -> ind1 == ind2 && u1 == u2 | Construct (cstr1,u1), Construct (cstr2,u2) -> cstr1 == cstr2 && u1 == u2 - | Case (ci1,p1,iv1,c1,bl1), Case (ci2,p2,iv2,c2,bl2) -> - ci1 == ci2 && p1 == p2 && invert_eqeq iv1 iv2 && c1 == c2 && array_eqeq bl1 bl2 + | Case (ci1,u1,pms1,p1,iv1,c1,bl1), Case (ci2,u2,pms2,p2,iv2,c2,bl2) -> + (** FIXME: use deeper equality for contexts *) + u1 == u2 && array_eqeq pms1 pms2 && + ci1 == ci2 && hasheq_ctx p1 p2 && + invert_eqeq iv1 iv2 && c1 == c2 && Array.equal hasheq_ctx bl1 bl2 | Fix ((ln1, i1),(lna1,tl1,bl1)), Fix ((ln2, i2),(lna2,tl2,bl2)) -> Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 @@ -1247,7 +1267,7 @@ let sh_instance = Univ.Instance.share representation for [constr] using [hash_consing_functions] on leaves. *) let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = - let rec hash_term t = + let rec hash_term (t : t) = match t with | Var i -> (Var (sh_id i), combinesmall 1 (Id.hash i)) @@ -1289,13 +1309,27 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = let u', hu = sh_instance u in (Construct (sh_construct c, u'), combinesmall 11 (combine (Construct.SyntacticOrd.hash c) hu)) - | Case (ci,p,iv,c,bl) -> - let p, hp = sh_rec p - and iv, hiv = sh_invert iv - and c, hc = sh_rec c in - let bl,hbl = hash_term_array bl in - let hbl = combine4 hc hp hiv hbl in - (Case (sh_ci ci, p, iv, c, bl), combinesmall 12 hbl) + | Case (ci,u,pms,p,iv,c,bl) -> + (** FIXME: use a dedicated hashconsing structure *) + let hcons_ctx (lna, c) = + let () = Array.iteri (fun i x -> Array.unsafe_set lna i (sh_na x)) lna in + let fold accu na = combine (hash_annot Name.hash na) accu in + let hna = Array.fold_left fold 0 lna in + let c, hc = sh_rec c in + (lna, c), combine hna hc + in + let u, hu = sh_instance u in + let pms,hpms = hash_term_array pms in + let p, hp = hcons_ctx p in + let iv, hiv = sh_invert iv in + let c, hc = sh_rec c in + let fold accu c = + let c, h = hcons_ctx c in + combine accu h, c + in + let hbl, bl = Array.fold_left_map fold 0 bl in + let hbl = combine (combine hc (combine hiv (combine hpms (combine hu hp)))) hbl in + (Case (sh_ci ci, u, pms, p, iv, c, bl), combinesmall 12 hbl) | Fix (ln,(lna,tl,bl)) -> let bl,hbl = hash_term_array bl in let tl,htl = hash_term_array tl in @@ -1400,8 +1434,8 @@ let rec hash t = combinesmall 10 (combine (Ind.CanOrd.hash ind) (Instance.hash u)) | Construct (c,u) -> combinesmall 11 (combine (Construct.CanOrd.hash c) (Instance.hash u)) - | Case (_ , p, iv, c, bl) -> - combinesmall 12 (combine4 (hash c) (hash p) (hash_invert iv) (hash_term_array bl)) + | Case (_ , u, pms, p, iv, c, bl) -> + combinesmall 12 (combine (combine (hash c) (combine (hash_invert iv) (combine (hash_term_array pms) (combine (Instance.hash u) (hash_under_context p))))) (hash_branches bl)) | Fix (_ln ,(_, tl, bl)) -> combinesmall 13 (combine (hash_term_array bl) (hash_term_array tl)) | CoFix(_ln, (_, tl, bl)) -> @@ -1426,6 +1460,11 @@ and hash_term_array t = and hash_term_list t = List.fold_left (fun acc t -> combine (hash t) acc) 0 t +and hash_under_context (_, t) = hash t + +and hash_branches bl = + Array.fold_left (fun acc t -> combine acc (hash_under_context t)) 0 bl + module CaseinfoHash = struct type t = case_info @@ -1551,10 +1590,15 @@ let rec debug_print c = | Construct (((sp,i),j),u) -> str"Constr(" ++ pr_puniverses (MutInd.print sp ++ str"," ++ int i ++ str"," ++ int j) u ++ str")" | Proj (p,c) -> str"Proj(" ++ Constant.debug_print (Projection.constant p) ++ str"," ++ bool (Projection.unfolded p) ++ debug_print c ++ str")" - | Case (_ci,p,iv,c,bl) -> v 0 - (hv 0 (str"<"++debug_print p++str">"++ cut() ++ str"Case " ++ - debug_print c ++ debug_invert iv ++ str"of") ++ cut() ++ - prlist_with_sep (fun _ -> brk(1,2)) debug_print (Array.to_list bl) ++ + | Case (_ci,_u,pms,p,iv,c,bl) -> + let pr_ctx (nas, c) = + prvect_with_sep spc (fun na -> Name.print na.binder_name) nas ++ spc () ++ str "|-" ++ spc () ++ + debug_print c + in + v 0 (hv 0 (str"Case " ++ + debug_print c ++ cut () ++ str "as" ++ cut () ++ prlist_with_sep cut debug_print (Array.to_list pms) ++ + cut () ++ str"return"++ cut () ++ pr_ctx p ++ debug_invert iv ++ cut () ++ str"with") ++ cut() ++ + prlist_with_sep (fun _ -> brk(1,2)) pr_ctx (Array.to_list bl) ++ cut() ++ str"end") | Fix f -> debug_print_fix debug_print f | CoFix(i,(lna,tl,bl)) -> diff --git a/kernel/constr.mli b/kernel/constr.mli index ed63ac507c..17c7da1cf6 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -49,7 +49,7 @@ type case_info = ci_pp_info : case_printing (* not interpreted by the kernel *) } -type ('constr, 'univs) case_invert = +type ('constr, 'univs) pcase_invert = | NoInvert (** Normal reduction: match when the scrutinee is a constructor. *) @@ -152,14 +152,30 @@ val mkRef : GlobRef.t Univ.puniverses -> constr (** Constructs a destructor of inductive type. - [mkCase ci p c ac] stand for match [c] as [x] in [I args] return [p] with [ac] + [mkCase ci params p c ac] stand for match [c] as [x] in [I args] return [p] with [ac] presented as describe in [ci]. - [p] structure is [fun args x -> "return clause"] + + [p] structure is [args x |- "return clause"] [ac]{^ ith} element is ith constructor case presented as - {e lambda construct_args (without params). case_term } *) -val mkCase : case_info * constr * (constr,Univ.Instance.t) case_invert * constr * constr array -> constr + {e construct_args |- case_term } *) + +type 'constr pcase_branch = Name.t Context.binder_annot array * 'constr +(** Names of the indices + name of self *) + +type 'types pcase_return = Name.t Context.binder_annot array * 'types +(** Names of the branches *) + +type ('constr, 'types, 'univs) pcase = + case_info * 'univs * 'constr array * 'types pcase_return * ('constr, 'univs) pcase_invert * 'constr * 'constr pcase_branch array + +type case_invert = (constr, Univ.Instance.t) pcase_invert +type case_return = types pcase_return +type case_branch = constr pcase_branch +type case = (constr, types, Univ.Instance.t) pcase + +val mkCase : case -> constr (** If [recindxs = [|i1,...in|]] [funnames = [|f1,.....fn|]] @@ -243,7 +259,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | Ind of (inductive * 'univs) (** A name of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *) | Construct of (constructor * 'univs) (** A constructor of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *) - | Case of case_info * 'constr * ('constr,'univs) case_invert * 'constr * 'constr array + | Case of case_info * 'univs * 'constr array * 'types pcase_return * ('constr,'univs) pcase_invert * 'constr * 'constr pcase_branch array | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint | Proj of Projection.t * 'constr @@ -351,7 +367,7 @@ Ci(...yij...) => ti | ... end] (or [let (..y1i..) := c as x in I args return P in t1], or [if c then t1 else t2]) @return [(info,c,fun args x => P,[|...|fun yij => ti| ...|])] where [info] is pretty-printing information *) -val destCase : constr -> case_info * constr * (constr,Univ.Instance.t) case_invert * constr * constr array +val destCase : constr -> case (** Destructs a projection *) val destProj : constr -> Projection.t * constr @@ -421,12 +437,6 @@ val lift : int -> constr -> constr (** {6 Functionals working on expressions canonically abstracted over a local context (possibly with let-ins)} *) -(** [map_under_context f l c] maps [f] on the immediate subterms of a - term abstracted over a context of length [n] (local definitions - are counted) *) - -val map_under_context : (constr -> constr) -> int -> constr -> constr - (** [map_branches f br] maps [f] on the immediate subterms of an array of "match" branches [br] in canonical eta-let-expanded form; it is not recursive and the order with which subterms are processed is @@ -434,7 +444,7 @@ val map_under_context : (constr -> constr) -> int -> constr -> constr types and possibly terms occurring in the context of each branch as well as the body of each branch *) -val map_branches : (constr -> constr) -> case_info -> constr array -> constr array +val map_branches : (constr -> constr) -> case_branch array -> case_branch array (** [map_return_predicate f p] maps [f] on the immediate subterms of a return predicate of a "match" in canonical eta-let-expanded form; @@ -443,16 +453,7 @@ val map_branches : (constr -> constr) -> case_info -> constr array -> constr arr the types and possibly terms occurring in the context of each branch as well as the body of the predicate *) -val map_return_predicate : (constr -> constr) -> case_info -> constr -> constr - -(** [map_under_context_with_binders g f n l c] maps [f] on the - immediate subterms of a term abstracted over a context of length - [n] (local definitions are counted); it preserves sharing; it - carries an extra data [n] (typically a lift index) which is - processed by [g] (which typically add 1 to [n]) at each binder - traversal *) - -val map_under_context_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> int -> constr -> constr +val map_return_predicate : (constr -> constr) -> case_return -> case_return (** [map_branches_with_binders f br] maps [f] on the immediate subterms of an array of "match" branches [br] in canonical @@ -464,7 +465,7 @@ val map_under_context_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> ' occurring in the context of the branch as well as the body of the branch *) -val map_branches_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_info -> constr array -> constr array +val map_branches_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_branch array -> case_branch array (** [map_return_predicate_with_binders f p] maps [f] on the immediate subterms of a return predicate of a "match" in canonical @@ -476,7 +477,7 @@ val map_branches_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> occurring in the context of each branch as well as the body of the predicate *) -val map_return_predicate_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_info -> constr -> constr +val map_return_predicate_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_return -> case_return (** {6 Functionals working on the immediate subterm of a construction } *) @@ -486,7 +487,7 @@ val map_return_predicate_with_binders : ('a -> 'a) -> ('a -> constr -> constr) - val fold : ('a -> constr -> 'a) -> 'a -> constr -> 'a -val fold_invert : ('a -> 'b -> 'a) -> 'a -> ('b, 'c) case_invert -> 'a +val fold_invert : ('a -> 'b -> 'a) -> 'a -> ('b, 'c) pcase_invert -> 'a (** [map f c] maps [f] on the immediate subterms of [c]; it is not recursive and the order with which subterms are processed is @@ -494,21 +495,14 @@ val fold_invert : ('a -> 'b -> 'a) -> 'a -> ('b, 'c) case_invert -> 'a val map : (constr -> constr) -> constr -> constr -val map_invert : ('a -> 'a) -> ('a, 'b) case_invert -> ('a, 'b) case_invert - -(** [map_user_view f c] maps [f] on the immediate subterms of [c]; it - differs from [map f c] in that the typing context and body of the - return predicate and of the branches of a [match] are considered as - immediate subterm of a [match] *) - -val map_user_view : (constr -> constr) -> constr -> constr +val map_invert : ('a -> 'a) -> ('a, 'b) pcase_invert -> ('a, 'b) pcase_invert (** Like {!map}, but also has an additional accumulator. *) val fold_map : ('a -> constr -> 'a * constr) -> 'a -> constr -> 'a * constr val fold_map_invert : ('a -> 'b -> 'a * 'b) -> - 'a -> ('b, 'c) case_invert -> 'a * ('b, 'c) case_invert + 'a -> ('b, 'c) pcase_invert -> 'a * ('b, 'c) pcase_invert (** [map_with_binders g f n c] maps [f n] on the immediate subterms of [c]; it carries an extra data [n] (typically a lift @@ -525,7 +519,7 @@ val map_with_binders : val iter : (constr -> unit) -> constr -> unit -val iter_invert : ('a -> unit) -> ('a, 'b) case_invert -> unit +val iter_invert : ('a -> unit) -> ('a, 'b) pcase_invert -> unit (** [iter_with_binders g f n c] iters [f n] on the immediate subterms of [c]; it carries an extra data [n] (typically a lift @@ -604,7 +598,7 @@ val compare_head_gen_leq : Univ.Instance.t instance_compare_fn -> constr constr_compare_fn val eq_invert : ('a -> 'a -> bool) -> ('b -> 'b -> bool) - -> ('a, 'b) case_invert -> ('a, 'b) case_invert -> bool + -> ('a, 'b) pcase_invert -> ('a, 'b) pcase_invert -> bool (** {6 Hashconsing} *) diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 3707a75157..930efa5d36 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -75,30 +75,30 @@ let share_univs cache r u l = let (u', args) = share cache r l in mkApp (instantiate_my_gr r (Instance.append u' u), args) -let update_case cache ci iv modlist = - match share cache (IndRef ci.ci_ind) modlist with - | exception Not_found -> ci, iv - | u, l -> - let iv = match iv with - | NoInvert -> NoInvert - | CaseInvert {univs; args;} -> - let univs = Instance.append u univs in - let args = Array.append l args in - CaseInvert {univs; args;} - in - { ci with ci_npar = ci.ci_npar + Array.length l }, iv - let is_empty_modlist (cm, mm) = Cmap.is_empty cm && Mindmap.is_empty mm let expmod_constr cache modlist c = let share_univs = share_univs cache in - let update_case = update_case cache in let rec substrec c = match kind c with - | Case (ci,p,iv,t,br) -> - let ci,iv = update_case ci iv modlist in - Constr.map substrec (mkCase (ci,p,iv,t,br)) + | Case (ci, u, pms, p, iv, t, br) -> + begin match share cache (IndRef ci.ci_ind) modlist with + | (u', prefix) -> + let u = Instance.append u' u in + let pms = Array.append prefix pms in + let ci = { ci with ci_npar = ci.ci_npar + Array.length prefix } in + let iv = match iv with + | NoInvert -> NoInvert + | CaseInvert {univs; args;} -> + let univs = Instance.append u' univs in + let args = Array.append prefix args in + CaseInvert {univs; args;} + in + Constr.map substrec (mkCase (ci,u,pms,p,iv,t,br)) + | exception Not_found -> + Constr.map substrec c + end | Ind (ind,u) -> (try diff --git a/kernel/inductive.ml b/kernel/inductive.ml index ce12d65614..eb18d4b90e 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -72,7 +72,7 @@ let constructor_instantiate mind u mib c = let s = ind_subst mind mib u in substl s (subst_instance_constr u c) -let instantiate_params full t u args sign = +let instantiate_params t u args sign = let fail () = anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch.") in let (rem_args, subs, ty) = @@ -81,8 +81,7 @@ let instantiate_params full t u args sign = match (decl, largs, kind ty) with | (LocalAssum _, a::args, Prod(_,_,t)) -> (args, a::subs, t) | (LocalDef (_,b,_), _, LetIn(_,_,_,t)) -> - (largs, (substl subs (subst_instance_constr u b))::subs, t) - | (_,[],_) -> if full then fail() else ([], subs, ty) + (largs, (substl subs (subst_instance_constr u b))::subs, t) | _ -> fail ()) sign ~init:(args,[],t) @@ -93,11 +92,11 @@ let instantiate_params full t u args sign = let full_inductive_instantiate mib u params sign = let dummy = Sorts.prop in let t = Term.mkArity (Vars.subst_instance_context u sign,dummy) in - fst (Term.destArity (instantiate_params true t u params mib.mind_params_ctxt)) + fst (Term.destArity (instantiate_params t u params mib.mind_params_ctxt)) let full_constructor_instantiate ((mind,_),u,(mib,_),params) t = let inst_ind = constructor_instantiate mind u mib t in - instantiate_params true inst_ind u params mib.mind_params_ctxt + instantiate_params inst_ind u params mib.mind_params_ctxt (************************************************************************) (************************************************************************) @@ -372,6 +371,91 @@ let check_correct_arity env c pj ind specif params = with LocalArity kinds -> error_elim_arity env ind c pj kinds +(** {6 Changes of representation of Case nodes} *) + +(** Provided: + - a universe instance [u] + - a term substitution [subst] + - name replacements [nas] + [instantiate_context u subst nas ctx] applies both [u] and [subst] to [ctx] + while replacing names using [nas] (order reversed) +*) +let instantiate_context u subst nas ctx = + let rec instantiate i ctx = match ctx with + | [] -> assert (Int.equal i (-1)); [] + | LocalAssum (_, ty) :: ctx -> + let ctx = instantiate (pred i) ctx in + let ty = substnl subst i (subst_instance_constr u ty) in + LocalAssum (nas.(i), ty) :: ctx + | LocalDef (_, ty, bdy) :: ctx -> + let ctx = instantiate (pred i) ctx in + let ty = substnl subst i (subst_instance_constr u ty) in + let bdy = substnl subst i (subst_instance_constr u bdy) in + LocalDef (nas.(i), ty, bdy) :: ctx + in + instantiate (Array.length nas - 1) ctx + +let expand_case_specif mib (ci, u, params, p, iv, c, br) = + (* Γ ⊢ c : I@{u} params args *) + (* Γ, indices, self : I@{u} params indices ⊢ p : Type *) + let mip = mib.mind_packets.(snd ci.ci_ind) in + let paramdecl = Vars.subst_instance_context u mib.mind_params_ctxt in + let paramsubst = Vars.subst_of_rel_context_instance paramdecl (Array.to_list params) in + (* Expand the return clause *) + let ep = + let (nas, p) = p in + let realdecls, _ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in + let self = + let args = Context.Rel.to_extended_vect mkRel 0 mip.mind_arity_ctxt in + let inst = Instance.of_array (Array.init (Instance.length u) Level.var) in + mkApp (mkIndU (ci.ci_ind, inst), args) + in + let realdecls = LocalAssum (Context.anonR, self) :: realdecls in + let realdecls = instantiate_context u paramsubst nas realdecls in + Term.it_mkLambda_or_LetIn p realdecls + in + (* Expand the branches *) + let subst = paramsubst @ ind_subst (fst ci.ci_ind) mib u in + let ebr = + let build_one_branch i (nas, br) (ctx, _) = + let ctx, _ = List.chop mip.mind_consnrealdecls.(i) ctx in + let ctx = instantiate_context u subst nas ctx in + Term.it_mkLambda_or_LetIn br ctx + in + Array.map2_i build_one_branch br mip.mind_nf_lc + in + (ci, ep, iv, c, ebr) + +let expand_case env (ci, _, _, _, _, _, _ as case) = + let specif = Environ.lookup_mind (fst ci.ci_ind) env in + expand_case_specif specif case + +let contract_case env (ci, p, iv, c, br) = + let (mib, mip) = lookup_mind_specif env ci.ci_ind in + let (arity, p) = Term.decompose_lam_n_decls (mip.mind_nrealdecls + 1) p in + let (u, pms) = match arity with + | LocalAssum (_, ty) :: _ -> + (** Last binder is the self binder for the term being eliminated *) + let (ind, args) = decompose_appvect ty in + let (ind, u) = destInd ind in + let () = assert (Ind.CanOrd.equal ind ci.ci_ind) in + let pms = Array.sub args 0 mib.mind_nparams in + (** Unlift the parameters from under the index binders *) + let dummy = List.make mip.mind_nrealdecls mkProp in + let pms = Array.map (fun c -> Vars.substl dummy c) pms in + (u, pms) + | _ -> assert false + in + let p = + let nas = Array.of_list (List.rev_map get_annot arity) in + (nas, p) + in + let map i br = + let (ctx, br) = Term.decompose_lam_n_decls mip.mind_consnrealdecls.(i) br in + let nas = Array.of_list (List.rev_map get_annot ctx) in + (nas, br) + in + (ci, u, pms, p, iv, c, Array.mapi map br) (************************************************************************) (* Type of case branches *) @@ -793,7 +877,8 @@ let rec subterm_specif renv stack t = let f,l = decompose_app (whd_all renv.env t) in match kind f with | Rel k -> subterm_var k renv - | Case (ci,p,_iv,c,lbr) -> (* iv ignored: it's just a cache *) + | Case (ci, u, pms, p, iv, c, lbr) -> (* iv ignored: it's just a cache *) + let (ci, p, _iv, c, lbr) = expand_case renv.env (ci, u, pms, p, iv, c, lbr) in let stack' = push_stack_closures renv l stack in let cases_spec = branches_specif renv (lazy_subterm_specif renv [] c) ci @@ -1018,7 +1103,8 @@ let check_one_fix renv recpos trees def = check_rec_call renv stack (Term.applist(lift p c,l)) end - | Case (ci,p,iv,c_0,lrest) -> (* iv ignored: it's just a cache *) + | Case (ci, u, pms, ret, iv, c_0, br) -> (* iv ignored: it's just a cache *) + let (ci, p, _iv, c_0, lrest) = expand_case renv.env (ci, u, pms, ret, iv, c_0, br) in begin try List.iter (check_rec_call renv []) (c_0::p::l); (* compute the recarg info for the arguments of each branch *) @@ -1040,7 +1126,7 @@ let check_one_fix renv recpos trees def = (* the call to whd_betaiotazeta will reduce the apparent iota redex away *) check_rec_call renv [] - (Term.applist (mkCase (ci,p,iv,c_0,lrest), l)) + (Term.applist (mkCase (ci, u, pms, ret, iv, c_0, br), l)) | _ -> Exninfo.iraise exn end @@ -1324,13 +1410,14 @@ let check_one_cofix env nbfix def deftype = else raise (CoFixGuardError (env,UnguardedRecursiveCall c)) - | Case (_,p,_,tm,vrest) -> (* iv ignored: just a cache *) - begin - let tree = match restrict_spec env (Subterm (Strict, tree)) p with - | Dead_code -> assert false - | Subterm (_, tree') -> tree' - | _ -> raise (CoFixGuardError (env, ReturnPredicateNotCoInductive c)) - in + | Case (ci, u, pms, p, iv, tm, br) -> (* iv ignored: just a cache *) + begin + let (_, p, _iv, tm, vrest) = expand_case env (ci, u, pms, p, iv, tm, br) in + let tree = match restrict_spec env (Subterm (Strict, tree)) p with + | Dead_code -> assert false + | Subterm (_, tree') -> tree' + | _ -> raise (CoFixGuardError (env, ReturnPredicateNotCoInductive c)) + in if (noccur_with_meta n nbfix p) then if (noccur_with_meta n nbfix tm) then if (List.for_all (noccur_with_meta n nbfix) args) then diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 78658dc4de..5808a3fa65 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -79,6 +79,23 @@ val arities_of_specif : MutInd.t puniverses -> mind_specif -> types array val inductive_params : mind_specif -> int +(** Given a pattern-matching represented compactly, expands it so as to produce + lambda and let abstractions in front of the return clause and the pattern + branches. *) +val expand_case : env -> case -> (case_info * constr * case_invert * constr * constr array) + +val expand_case_specif : mutual_inductive_body -> case -> (case_info * constr * case_invert * constr * constr array) + +(** Dual operation of the above. Fails if the return clause or branch has not + the expected form. *) +val contract_case : env -> (case_info * constr * case_invert * constr * constr array) -> case + +(** [instantiate_context u subst nas ctx] applies both [u] and [subst] + to [ctx] while replacing names using [nas] (order reversed). In particular, + assumes that [ctx] and [nas] have the same length. *) +val instantiate_context : Instance.t -> Vars.substl -> Name.t Context.binder_annot array -> + rel_context -> rel_context + (** [type_case_branches env (I,args) (p:A) c] computes useful types about the following Cases expression:
Cases (c :: (I args)) of b1..bn end diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml index d02f92ef26..50c3ba1cc6 100644 --- a/kernel/inferCumulativity.ml +++ b/kernel/inferCumulativity.ml @@ -198,7 +198,9 @@ let rec infer_fterm cv_pb infos variances hd stk = let variances = infer_vect infos variances elems in infer_stack infos variances stk - | FCaseInvert (_,p,_,_,br,e) -> + | FCaseInvert (ci, u, pms, p, _, _, br, e) -> + let mib = Environ.lookup_mind (fst ci.ci_ind) (info_env (fst infos)) in + let (_, p, _, _, br) = Inductive.expand_case_specif mib (ci, u, pms, p, NoInvert, mkProp, br) in let infer c variances = infer_fterm CONV infos variances (mk_clos e c) [] in let variances = infer p variances in Array.fold_right infer br variances @@ -217,7 +219,10 @@ and infer_stack infos variances (stk:CClosure.stack) = | Zfix (fx,a) -> let variances = infer_fterm CONV infos variances fx [] in infer_stack infos variances a - | ZcaseT (_, p, br, e) -> + | ZcaseT (ci,u,pms,p,br,e) -> + let dummy = mkProp in + let case = (ci, u, pms, p, NoInvert, dummy, br) in + let (_, p, _, _, br) = Inductive.expand_case (info_env (fst infos)) case in let variances = infer_fterm CONV infos variances (mk_clos e p) [] in infer_vect infos variances (Array.map (mk_clos e) br) | Zshift _ -> variances diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 4778bf1121..c5ac57a2cd 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -355,21 +355,26 @@ let rec map_kn f f' c = | Construct (((kn,i),j),u) -> let kn' = f kn in if kn'==kn then c else mkConstructU (((kn',i),j),u) - | Case (ci,p,iv,ct,l) -> + | Case (ci,u,pms,p,iv,ct,l) -> let ci_ind = let (kn,i) = ci.ci_ind in let kn' = f kn in if kn'==kn then ci.ci_ind else kn',i in - let p' = func p in + let f_ctx (nas, c as d) = + let c' = func c in + if c' == c then d else (nas, c') + in + let pms' = Array.Smart.map func pms in + let p' = f_ctx p in let iv' = map_invert func iv in let ct' = func ct in - let l' = Array.Smart.map func l in - if (ci.ci_ind==ci_ind && p'==p && iv'==iv + let l' = Array.Smart.map f_ctx l in + if (ci.ci_ind==ci_ind && pms'==pms && p'==p && iv'==iv && l'==l && ct'==ct)then c else - mkCase ({ci with ci_ind = ci_ind}, - p',iv',ct', l') + mkCase ({ci with ci_ind = ci_ind}, u, + pms',p',iv',ct', l') | Cast (ct,k,t) -> let ct' = func ct in let t'= func t in diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 09db29d222..c19b883e3d 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -2101,7 +2101,7 @@ let compile_deps env sigma prefix init t = | Proj (p,c) -> let init = compile_mind_deps env prefix init (Projection.mind p) in aux env lvl init c - | Case (ci, _p, _iv, _c, _ac) -> + | Case (ci, _u, _pms, _p, _iv, _c, _ac) -> let mind = fst ci.ci_ind in let init = compile_mind_deps env prefix init mind in fold_constr_with_binders succ (aux env) lvl init t diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index b27c53ef0f..f3b483467d 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -535,7 +535,8 @@ let rec lambda_of_constr cache env sigma c = let prefix = get_mind_prefix env (fst ind) in mkLapp (Lproj (prefix, ind, Projection.arg p)) [|lambda_of_constr cache env sigma c|] - | Case(ci,t,_iv,a,branches) -> (* XXX handle iv *) + | Case (ci, u, pms, t, iv, a, br) -> (* XXX handle iv *) + let (ci, t, _iv, a, branches) = Inductive.expand_case env (ci, u, pms, t, iv, a, br) in let (mind,i as ind) = ci.ci_ind in let mib = lookup_mind mind env in let oib = mib.mind_packets.(i) in diff --git a/kernel/reduction.ml b/kernel/reduction.ml index cf40263f61..1e39756d47 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -56,7 +56,7 @@ let compare_stack_shape stk1 stk2 = | (_, Zapp l2::s2) -> compare_rec (bal-Array.length l2) stk1 s2 | (Zproj _p1::s1, Zproj _p2::s2) -> Int.equal bal 0 && compare_rec 0 s1 s2 - | (ZcaseT(_c1,_,_,_)::s1, 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 @@ -74,7 +74,7 @@ type lft_constr_stack_elt = Zlapp of (lift * fconstr) array | Zlproj of Projection.Repr.t * lift | Zlfix of (lift * fconstr) * lft_constr_stack - | Zlcase of case_info * lift * constr * constr array * fconstr subs + | Zlcase of case_info * lift * Univ.Instance.t * constr array * case_return * case_branch array * fconstr subs | Zlprimitive of CPrimitives.t * pconstant * lft_fconstr list * lft_fconstr next_native_args and lft_constr_stack = lft_constr_stack_elt list @@ -109,8 +109,8 @@ let pure_stack lfts stk = | (Zfix(fx,a),(l,pstk)) -> 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,p,br,e)::pstk) + | (ZcaseT(ci,u,pms,p,br,e),(l,pstk)) -> + (l,Zlcase(ci,l,u,pms,p,br,e)::pstk) | (Zprimitive(op,c,rargs,kargs),(l,pstk)) -> (l,Zlprimitive(op,c,List.map (fun t -> (l,t)) rargs, List.map (fun (k,t) -> (k,(l,t))) kargs)::pstk)) @@ -233,6 +233,9 @@ let convert_instances ~flex u u' (s, check) = exception MustExpand +let convert_instances_cumul pb var u u' (s, check) = + (check.compare_cumul_instances pb var u u' s, check) + let get_cumulativity_constraints cv_pb variance u u' = match cv_pb with | CONV -> @@ -294,8 +297,6 @@ let conv_table_key infos ~nargs k1 k2 cuniv = | RelKey n, RelKey n' when Int.equal n n' -> cuniv | _ -> raise NotConvertible -exception IrregularPatternShape - let unfold_ref_with_args infos tab fl v = match unfold_reference infos tab fl with | Def def -> Some (def, v) @@ -327,17 +328,6 @@ let push_relevance infos r = let push_relevances infos nas = { infos with cnv_inf = CClosure.push_relevances infos.cnv_inf nas } -let rec skip_pattern infos relevances n c1 c2 = - if Int.equal n 0 then {infos with cnv_inf = CClosure.set_info_relevances infos.cnv_inf relevances}, c1, c2 - else match kind c1, kind c2 with - | Lambda (x, _, c1), Lambda (_, _, c2) -> - skip_pattern infos (Range.cons x.Context.binder_relevance relevances) (pred n) c1 c2 - | _ -> raise IrregularPatternShape - -let skip_pattern infos n c1 c2 = - if Int.equal n 0 then infos, c1, c2 - else skip_pattern infos (info_relevances infos.cnv_inf) n c1 c2 - let is_irrelevant infos lft c = let env = info_env infos.cnv_inf in try Relevanceops.relevance_of_fterm env (info_relevances infos.cnv_inf) lft c == Sorts.Irrelevant with _ -> false @@ -364,6 +354,39 @@ let eta_expand_constructor env ((ind,ctor),u as pctor) = let c = Term.it_mkLambda_or_LetIn c ctx in inject c +let inductive_subst (mind, _) mib u pms = + let open Context.Rel.Declaration in + let ntypes = mib.mind_ntypes in + let rec self i accu = + if Int.equal i ntypes then accu + else self (i + 1) (subs_cons (inject (mkIndU ((mind, i), u))) accu) + in + let accu = self 0 (subs_id 0) in + let rec mk_pms pms ctx = match ctx, pms with + | [], [] -> accu + | LocalAssum _ :: ctx, c :: pms -> + let subs = mk_pms pms ctx in + subs_cons c subs + | LocalDef (_, c, _) :: ctx, pms -> + let c = Vars.subst_instance_constr u c in + let subs = mk_pms pms ctx in + subs_cons (mk_clos subs c) subs + | LocalAssum _ :: _, [] | [], _ :: _ -> assert false + in + mk_pms (List.rev pms) mib.mind_params_ctxt + +let esubst_of_rel_context_instance ctx u args e = + let open Context.Rel.Declaration in + let rec aux lft e args ctx = match ctx with + | [] -> lft, e + | LocalAssum _ :: ctx -> aux (lft + 1) (subs_lift e) (subs_lift args) ctx + | LocalDef (_, c, _) :: ctx -> + let c = Vars.subst_instance_constr u c in + let c = mk_clos args c in + aux lft (subs_cons c e) (subs_cons c args) ctx + in + aux 0 e args (List.rev ctx) + (* Conversion between [lft1]term1 and [lft2]term2 *) let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv = try eqappr cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv @@ -672,13 +695,23 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = if Float64.equal f1 f2 then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible - | FCaseInvert (ci1,p1,_,_,br1,e1), FCaseInvert (ci2,p2,_,_,br2,e2) -> + | FCaseInvert (ci1,u1,pms1,p1,_,_,br1,e1), FCaseInvert (ci2,u2,pms2,p2,_,_,br2,e2) -> (if not (Ind.CanOrd.equal ci1.ci_ind ci2.ci_ind) then raise NotConvertible); let el1 = el_stack lft1 v1 and el2 = el_stack lft2 v2 in - let ccnv = ccnv CONV l2r infos el1 el2 in - let cuniv = ccnv (mk_clos e1 p1) (mk_clos e2 p2) cuniv in - Array.fold_right2 (fun b1 b2 cuniv -> ccnv (mk_clos e1 b1) (mk_clos e2 b2) cuniv) - br1 br2 cuniv + let fold c1 c2 cuniv = ccnv CONV l2r infos el1 el2 c1 c2 cuniv in + (** FIXME: cache the presence of let-bindings in the case_info *) + let mind = Environ.lookup_mind (fst ci1.ci_ind) (info_env infos.cnv_inf) in + let mip = mind.Declarations.mind_packets.(snd ci1.ci_ind) in + let cuniv = + let ind = (mind,snd ci1.ci_ind) in + let nargs = inductive_cumulativity_arguments ind in + convert_inductives CONV ind nargs u1 u2 cuniv + in + let pms1 = Array.map_to_list (fun c -> mk_clos e1 c) pms1 in + let pms2 = Array.map_to_list (fun c -> mk_clos e2 c) pms2 in + let cuniv = List.fold_right2 fold pms1 pms2 cuniv in + let cuniv = convert_return_clause ci1.ci_ind mind mip l2r infos e1 e2 el1 el2 u1 u2 pms1 pms2 p1 p2 cuniv in + convert_branches ci1.ci_ind mind mip l2r infos e1 e2 el1 el2 u1 u2 pms1 pms2 br1 br2 cuniv | FArray (u1,t1,ty1), FArray (u2,t2,ty2) -> let len = Parray.length_int t1 in @@ -714,11 +747,27 @@ and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv = | (Zlfix(fx1,a1),Zlfix(fx2,a2)) -> let cu2 = f fx1 fx2 cu1 in cmp_rec a1 a2 cu2 - | (Zlcase(ci1,l1,p1,br1,e1),Zlcase(ci2,l2,p2,br2,e2)) -> + | (Zlcase(ci1,l1,u1,pms1,p1,br1,e1),Zlcase(ci2,l2,u2,pms2,p2,br2,e2)) -> if not (Ind.CanOrd.equal ci1.ci_ind ci2.ci_ind) then raise NotConvertible; - let cu2 = f (l1, mk_clos e1 p1) (l2, mk_clos e2 p2) cu1 in - convert_branches l2r infos ci1 e1 e2 l1 l2 br1 br2 cu2 + let cu = cu1 in + (** FIXME: cache the presence of let-bindings in the case_info *) + let mind = Environ.lookup_mind (fst ci1.ci_ind) (info_env infos.cnv_inf) in + let mip = mind.Declarations.mind_packets.(snd ci1.ci_ind) in + let cu = + if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then + convert_instances ~flex:false u1 u2 cu + else + match mind.Declarations.mind_variance with + | None -> convert_instances ~flex:false u1 u2 cu + | Some variances -> convert_instances_cumul CONV variances u1 u2 cu + in + let pms1 = Array.map_to_list (fun c -> mk_clos e1 c) pms1 in + let pms2 = Array.map_to_list (fun c -> mk_clos e2 c) pms2 in + let fold_params c1 c2 accu = f (l1, c1) (l2, c2) accu in + let cu = List.fold_right2 fold_params pms1 pms2 cu in + let cu = convert_return_clause ci1.ci_ind mind mip l2r infos e1 e2 l1 l2 u1 u2 pms1 pms2 p1 p2 cu in + convert_branches ci1.ci_ind mind mip l2r infos e1 e2 l1 l2 u1 u2 pms1 pms2 br1 br2 cu | (Zlprimitive(op1,_,rargs1,kargs1),Zlprimitive(op2,_,rargs2,kargs2)) -> if not (CPrimitives.equal op1 op2) then raise NotConvertible else let cu2 = List.fold_right2 f rargs1 rargs2 cu1 in @@ -743,21 +792,55 @@ and convert_vect l2r infos lft1 lft2 v1 v2 cuniv = fold 0 cuniv else raise NotConvertible -and convert_branches l2r infos ci e1 e2 lft1 lft2 br1 br2 cuniv = - (** Skip comparison of the pattern types. We know that the two terms are - living in a common type, thus this check is useless. *) - let fold n c1 c2 cuniv = match skip_pattern infos n c1 c2 with - | (infos, c1, c2) -> - let lft1 = el_liftn n lft1 in - let lft2 = el_liftn n lft2 in +and convert_under_context l2r infos e1 e2 lft1 lft2 ctx (nas1, c1) (nas2, c2) cu = + let n = Array.length nas1 in + let () = assert (Int.equal n (Array.length nas2)) in + let n, e1, e2 = match ctx with + | None -> (* nolet *) let e1 = subs_liftn n e1 in let e2 = subs_liftn n e2 in - ccnv CONV l2r infos lft1 lft2 (mk_clos e1 c1) (mk_clos e2 c2) cuniv - | exception IrregularPatternShape -> - (** Might happen due to a shape invariant that is not enforced *) - ccnv CONV l2r infos lft1 lft2 (mk_clos e1 c1) (mk_clos e2 c2) cuniv + (n, e1, e2) + | Some (ctx, u1, u2, args1, args2) -> + let n1, e1 = esubst_of_rel_context_instance ctx u1 args1 e1 in + let n2, e2 = esubst_of_rel_context_instance ctx u2 args2 e2 in + let () = assert (Int.equal n1 n2) in + n1, e1, e2 + in + let lft1 = el_liftn n lft1 in + let lft2 = el_liftn n lft2 in + let infos = push_relevances infos nas1 in + ccnv CONV l2r infos lft1 lft2 (mk_clos e1 c1) (mk_clos e2 c2) cu + +and convert_return_clause ind mib mip l2r infos e1 e2 l1 l2 u1 u2 pms1 pms2 p1 p2 cu = + let ctx = + if Int.equal mip.mind_nrealargs mip.mind_nrealdecls then None + else + let ctx, _ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in + let pms1 = inductive_subst ind mib u1 pms1 in + let pms2 = inductive_subst ind mib u1 pms2 in + let open Context.Rel.Declaration in + (* Add the inductive binder *) + let dummy = mkProp in + let ctx = LocalAssum (Context.anonR, dummy) :: ctx in + Some (ctx, u1, u2, pms1, pms2) + in + convert_under_context l2r infos e1 e2 l1 l2 ctx p1 p2 cu + +and convert_branches ind mib mip l2r infos e1 e2 lft1 lft2 u1 u2 pms1 pms2 br1 br2 cuniv = + let fold i (ctx, _) cuniv = + let ctx = + if Int.equal mip.mind_consnrealdecls.(i) mip.mind_consnrealargs.(i) then None + else + let ctx, _ = List.chop mip.mind_consnrealdecls.(i) ctx in + let pms1 = inductive_subst ind mib u1 pms1 in + let pms2 = inductive_subst ind mib u2 pms2 in + Some (ctx, u1, u2, pms1, pms2) + in + let c1 = br1.(i) in + let c2 = br2.(i) in + convert_under_context l2r infos e1 e2 lft1 lft2 ctx c1 c2 cuniv in - Array.fold_right3 fold ci.ci_cstr_nargs br1 br2 cuniv + Array.fold_right_i fold mip.mind_nf_lc cuniv and convert_list l2r infos lft1 lft2 v1 v2 cuniv = match v1, v2 with | [], [] -> cuniv diff --git a/kernel/relevanceops.ml b/kernel/relevanceops.ml index f12b8cba37..986fc685d1 100644 --- a/kernel/relevanceops.ml +++ b/kernel/relevanceops.ml @@ -61,7 +61,7 @@ let rec relevance_of_fterm env extra lft f = | FProj (p, _) -> relevance_of_projection env p | FFix (((_,i),(lna,_,_)), _) -> (lna.(i)).binder_relevance | FCoFix ((i,(lna,_,_)), _) -> (lna.(i)).binder_relevance - | FCaseT (ci, _, _, _, _) | FCaseInvert (ci, _, _, _, _, _) -> ci.ci_relevance + | FCaseT (ci, _, _, _, _, _, _) | FCaseInvert (ci, _, _, _, _, _, _, _) -> ci.ci_relevance | FLambda (len, tys, bdy, e) -> let extra = List.fold_left (fun accu (x, _) -> Range.cons (binder_relevance x) accu) extra tys in let lft = Esubst.el_liftn len lft in @@ -97,7 +97,7 @@ and relevance_of_term_extra env extra lft subs c = | App (c, _) -> relevance_of_term_extra env extra lft subs c | Const (c,_) -> relevance_of_constant env c | Construct (c,_) -> relevance_of_constructor env c - | Case (ci, _, _, _, _) -> ci.ci_relevance + | Case (ci, _, _, _, _, _, _) -> ci.ci_relevance | Fix ((_,i),(lna,_,_)) -> (lna.(i)).binder_relevance | CoFix (i,(lna,_,_)) -> (lna.(i)).binder_relevance | Proj (p, _) -> relevance_of_projection env p diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 802a32b0e7..83e41a63ec 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -548,7 +548,9 @@ let rec execute env cstr = | Construct c -> cstr, type_of_constructor env c - | Case (ci,p,iv,c,lf) -> + | Case (ci, u, pms, p, iv, c, lf) -> + (** FIXME: change type_of_case to handle the compact form *) + let (ci, p, iv, c, lf) = expand_case env (ci, u, pms, p, iv, c, lf) in let c', ct = execute env c in let iv' = match iv with | NoInvert -> NoInvert @@ -563,7 +565,7 @@ let rec execute env cstr = let lf', lft = execute_array env lf in let ci', t = type_of_case env ci p' pt iv' c' ct lf' lft in let cstr = if ci == ci' && c == c' && p == p' && iv == iv' && lf == lf' then cstr - else mkCase(ci',p',iv',c',lf') + else mkCase (Inductive.contract_case env (ci',p',iv',c',lf')) in cstr, t @@ -720,11 +722,6 @@ let judge_of_inductive env indu = let judge_of_constructor env cu = make_judge (mkConstructU cu) (type_of_constructor env cu) -let judge_of_case env ci pj iv cj lfj = - let lf, lft = dest_judgev lfj in - let ci, t = type_of_case env ci pj.uj_val pj.uj_type iv cj.uj_val cj.uj_type lf lft in - make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, iv, cj.uj_val, lft)) t - (* Building type of primitive operators and type *) let type_of_prim_const env _u c = diff --git a/kernel/typeops.mli b/kernel/typeops.mli index d381e55dd6..5ea7163f72 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -92,12 +92,6 @@ val judge_of_cast : val judge_of_inductive : env -> inductive puniverses -> unsafe_judgment val judge_of_constructor : env -> constructor puniverses -> unsafe_judgment -(** {6 Type of Cases. } *) -val judge_of_case : env -> case_info - -> unsafe_judgment -> (constr,Instance.t) case_invert -> unsafe_judgment - -> unsafe_judgment array - -> unsafe_judgment - (** {6 Type of global references. } *) val type_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t diff --git a/kernel/vars.ml b/kernel/vars.ml index a446fa413c..0f71057787 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -253,12 +253,21 @@ let subst_univs_level_constr subst c = if u' == u then t else (changed := true; mkSort (Sorts.sort_of_univ u')) - | Case (ci,p,CaseInvert {univs;args},c,br) -> - if Univ.Instance.is_empty univs then Constr.map aux t + | Case (ci, u, pms, p, CaseInvert {univs;args}, c, br) -> + if Univ.Instance.is_empty u && Univ.Instance.is_empty univs then Constr.map aux t else + let u' = f u in let univs' = f univs in - if univs' == univs then Constr.map aux t - else (changed:=true; Constr.map aux (mkCase (ci,p,CaseInvert {univs=univs';args},c,br))) + if u' == u && univs' == univs then Constr.map aux t + else (changed:=true; Constr.map aux (mkCase (ci,u',pms,p,CaseInvert {univs=univs';args},c,br))) + + | Case (ci, u, pms, p, NoInvert, c, br) -> + if Univ.Instance.is_empty u then Constr.map aux t + else + let u' = f u in + if u' == u then Constr.map aux t + else + (changed := true; Constr.map aux (mkCase (ci, u', pms, p, NoInvert, c, br))) | Array (u,elems,def,ty) -> let u' = f u in @@ -305,10 +314,19 @@ let subst_instance_constr subst c = if u' == u then t else (mkSort (Sorts.sort_of_univ u')) - | Case (ci,p,CaseInvert {univs;args},c,br) -> + | Case (ci, u, pms, p, CaseInvert {univs;args}, c, br) -> + let u' = f u in let univs' = f univs in - if univs' == univs then Constr.map aux t - else Constr.map aux (mkCase (ci,p,CaseInvert {univs=univs';args},c,br)) + if u' == u && univs' == univs then Constr.map aux t + else Constr.map aux (mkCase (ci,u',pms,p,CaseInvert {univs=univs';args},c,br)) + + | Case (ci, u, pms, p, NoInvert, c, br) -> + if Univ.Instance.is_empty u then Constr.map aux t + else + let u' = f u in + if u' == u then Constr.map aux t + else + Constr.map aux (mkCase (ci, u', pms, p, NoInvert, c, br)) | Array (u,elems,def,ty) -> let u' = f u in @@ -348,8 +366,11 @@ let universes_of_constr c = | Array (u,_,_,_) -> let s = LSet.fold LSet.add (Instance.levels u) s in Constr.fold aux s c - | Case (_,_,CaseInvert {univs;args=_},_,_) -> + | Case (_, u, _, _, CaseInvert {univs;args=_},_ ,_) -> + let s = LSet.fold LSet.add (Instance.levels u) s in let s = LSet.fold LSet.add (Instance.levels univs) s in Constr.fold aux s c + | Case (_, u, _, _, NoInvert, _, _) -> + Constr.fold aux (LSet.fold LSet.add (Instance.levels u) s) c | _ -> Constr.fold aux s c in aux LSet.empty c diff --git a/kernel/vmlambda.ml b/kernel/vmlambda.ml index 390fa58883..91de58b0e6 100644 --- a/kernel/vmlambda.ml +++ b/kernel/vmlambda.ml @@ -674,7 +674,8 @@ let rec lambda_of_constr env c = | Construct _ -> lambda_of_app env c empty_args - | Case(ci,t,_iv,a,branches) -> (* XXX handle iv *) + | Case (ci, u, pms, t, iv, a, br) -> (* XXX handle iv *) + let (ci, t, _iv, a, branches) = Inductive.expand_case env.global_env (ci, u, pms, t, iv, a, br) in let ind = ci.ci_ind in let mib = lookup_mind (fst ind) env.global_env in let oib = mib.mind_packets.(snd ind) in -- cgit v1.2.3 From 868b948f8a7bd583d467c5d02dfb34d328d53d37 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 11 Dec 2020 13:20:54 +0100 Subject: Remove redundant univ and parameter info from CaseInvert --- kernel/cClosure.ml | 22 +++++++++--------- kernel/constr.ml | 68 +++++++++++++++++++++++++----------------------------- kernel/constr.mli | 22 +++++++++--------- kernel/cooking.ml | 7 ------ kernel/typeops.ml | 8 ++++--- kernel/vars.ml | 21 +++++++---------- 6 files changed, 67 insertions(+), 81 deletions(-) (limited to 'kernel') diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 5613bf645e..a32c8f1cd1 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -357,7 +357,7 @@ and fterm = | FCLOS of constr * fconstr subs | FLOCKED -and finvert = Univ.Instance.t * fconstr array +and finvert = fconstr array let fterm_of v = v.term let set_ntrl v = v.mark <- Mark.set_ntrl v.mark @@ -582,8 +582,8 @@ let rec to_constr lfts v = | FConstruct op -> mkConstructU op | FCaseT (ci, u, pms, p, c, ve, env) -> to_constr_case lfts ci u pms p NoInvert c ve env - | FCaseInvert (ci, u, pms, p, (univs, args), c, ve, env) -> - let iv = CaseInvert {univs;args=Array.map (to_constr lfts) args} in + | FCaseInvert (ci, u, pms, p, indices, c, ve, env) -> + let iv = CaseInvert {indices=Array.map (to_constr lfts) indices} in to_constr_case lfts ci u pms p iv c ve env | FFix ((op,(lna,tys,bds)) as fx, e) -> if is_subs_id e && is_lift_id lfts then @@ -1370,8 +1370,8 @@ and knht info e t stk = knht info e a (append_stack (mk_clos_vect e b) stk) | Case(ci,u,pms,p,NoInvert,t,br) -> knht info e t (ZcaseT(ci, u, pms, p, br, e)::stk) - | Case(ci,u,pms,p,CaseInvert{univs;args},t,br) -> - let term = FCaseInvert (ci, u, pms, p, (univs,Array.map (mk_clos e) args), mk_clos e t, br, e) in + | Case(ci,u,pms,p,CaseInvert{indices},t,br) -> + let term = FCaseInvert (ci, u, pms, p, (Array.map (mk_clos e) indices), mk_clos e t, br, e) in { mark = mark Red Unknown; term }, stk | Fix fx -> knh info { mark = mark Cstr Unknown; term = FFix (fx, e) } stk | Cast(a,_,_) -> knht info e a stk @@ -1478,8 +1478,9 @@ let rec knr info tab m stk = kni info tab a (Zprimitive(op,c,rargs,nargs)::s) end | (_, _, s) -> (m, s)) - | FCaseInvert (ci, _u, _pms, _p,iv,_c,v,env) when red_set info.i_flags fMATCH -> - begin match case_inversion info tab ci iv v with + | FCaseInvert (ci, u, pms, _p,iv,_c,v,env) when red_set info.i_flags fMATCH -> + let pms = mk_clos_vect env pms in + begin match case_inversion info tab ci u pms iv v with | Some c -> knit info tab env c stk | None -> (m, stk) end @@ -1496,18 +1497,17 @@ and knit info tab e t stk = let (ht,s) = knht info e t stk in knr info tab ht s -and case_inversion info tab ci (univs,args) v = +and case_inversion info tab ci u params indices v = let open Declarations in (* No binders / lets at all in the unique branch *) let v = match v with | [| [||], v |] -> v | _ -> assert false in - if Array.is_empty args then Some v + if Array.is_empty indices then Some v else let env = info_env info in let ind = ci.ci_ind in - let params, indices = Array.chop ci.ci_npar args in let psubst = subs_consn params 0 ci.ci_npar (subs_id 0) in let mib = Environ.lookup_mind (fst ind) env in let mip = mib.mind_packets.(snd ind) in @@ -1516,7 +1516,7 @@ and case_inversion info tab ci (univs,args) v = let _ind, expect_args = destApp expect in let check_index i index = let expected = expect_args.(ci.ci_npar + i) in - let expected = Vars.subst_instance_constr univs expected in + let expected = Vars.subst_instance_constr u expected in let expected = mk_clos psubst expected in !conv {info with i_flags=all} tab expected index in diff --git a/kernel/constr.ml b/kernel/constr.ml index 0dc72025af..30542597c5 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -83,15 +83,15 @@ type pconstant = Constant.t puniverses type pinductive = inductive puniverses type pconstructor = constructor puniverses -type ('constr, 'univs) pcase_invert = +type 'constr pcase_invert = | NoInvert - | CaseInvert of { univs : 'univs; args : 'constr array } + | CaseInvert of { indices : 'constr array } type 'constr pcase_branch = Name.t Context.binder_annot array * 'constr type 'types pcase_return = Name.t Context.binder_annot array * 'types type ('constr, 'types, 'univs) pcase = - case_info * 'univs * 'constr array * 'types pcase_return * ('constr, 'univs) pcase_invert * 'constr * 'constr pcase_branch array + case_info * 'univs * 'constr array * 'types pcase_return * 'constr pcase_invert * 'constr * 'constr pcase_branch array (* [Var] is used for named variables and [Rel] for variables as de Bruijn indices. *) @@ -109,7 +109,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | Const of (Constant.t * 'univs) | Ind of (inductive * 'univs) | Construct of (constructor * 'univs) - | Case of case_info * 'univs * 'constr array * 'types pcase_return * ('constr, 'univs) pcase_invert * 'constr * 'constr pcase_branch array + | Case of case_info * 'univs * 'constr array * 'types pcase_return * 'constr pcase_invert * 'constr * 'constr pcase_branch array | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint | Proj of Projection.t * 'constr @@ -125,7 +125,7 @@ type existential = existential_key * constr list type types = constr -type case_invert = (constr, Instance.t) pcase_invert +type case_invert = constr pcase_invert type case_return = types pcase_return type case_branch = constr pcase_branch type case = (constr, types, Instance.t) pcase @@ -481,8 +481,8 @@ let decompose_appvect c = let fold_invert f acc = function | NoInvert -> acc - | CaseInvert {univs=_;args} -> - Array.fold_left f acc args + | CaseInvert {indices} -> + Array.fold_left f acc indices let fold f acc c = match kind c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ @@ -509,8 +509,8 @@ let fold f acc c = match kind c with let iter_invert f = function | NoInvert -> () - | CaseInvert {univs=_; args;} -> - Array.iter f args + | CaseInvert {indices;} -> + Array.iter f indices let iter f c = match kind c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ @@ -624,10 +624,10 @@ let map_return_predicate_with_binders g f l p = let map_invert f = function | NoInvert -> NoInvert - | CaseInvert {univs;args;} as orig -> - let args' = Array.Smart.map f args in - if args == args' then orig - else CaseInvert {univs;args=args';} + | CaseInvert {indices;} as orig -> + let indices' = Array.Smart.map f indices in + if indices == indices' then orig + else CaseInvert {indices=indices';} let map f c = match kind c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ @@ -695,10 +695,10 @@ let map f c = match kind c with let fold_map_invert f acc = function | NoInvert -> acc, NoInvert - | CaseInvert {univs;args;} as orig -> - let acc, args' = Array.fold_left_map f acc args in - if args==args' then acc, orig - else acc, CaseInvert {univs;args=args';} + | CaseInvert {indices;} as orig -> + let acc, indices' = Array.fold_left_map f acc indices in + if indices==indices' then acc, orig + else acc, CaseInvert {indices=indices';} let fold_map_under_context f accu d = let (nas, p) = d in @@ -881,13 +881,12 @@ type 'constr constr_compare_fn = int -> 'constr -> 'constr -> bool optimisation that physically equal arrays are equals (hence the calls to {!Array.equal_norefl}). *) -let eq_invert eq leq_universes iv1 iv2 = +let eq_invert eq iv1 iv2 = match iv1, iv2 with | NoInvert, NoInvert -> true | NoInvert, CaseInvert _ | CaseInvert _, NoInvert -> false - | CaseInvert {univs;args}, CaseInvert iv2 -> - leq_universes univs iv2.univs - && Array.equal eq args iv2.args + | CaseInvert {indices}, CaseInvert iv2 -> + Array.equal eq indices iv2.indices let eq_under_context eq (_nas1, p1) (_nas2, p2) = eq p1 p2 @@ -921,7 +920,7 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t (** FIXME: what are we doing with u1 = u2 ? *) Ind.CanOrd.equal ci1.ci_ind ci2.ci_ind && leq_universes (Some (GlobRef.IndRef ci1.ci_ind, 0)) u1 u2 && Array.equal (eq 0) pms1 pms2 && eq_under_context (eq 0) p1 p2 && - eq_invert (eq 0) (leq_universes None) iv1 iv2 && + eq_invert (eq 0) iv1 iv2 && eq 0 c1 c2 && Array.equal (eq_under_context (eq 0)) bl1 bl2 | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) -> Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 @@ -1060,8 +1059,7 @@ let compare_invert f iv1 iv2 = | NoInvert, CaseInvert _ -> -1 | CaseInvert _, NoInvert -> 1 | CaseInvert iv1, CaseInvert iv2 -> - (* univs ignored deliberately *) - Array.compare f iv1.args iv2.args + Array.compare f iv1.indices iv2.indices let constr_ord_int f t1 t2 = let (=?) f g i1 i2 j1 j2= @@ -1190,9 +1188,8 @@ let invert_eqeq iv1 iv2 = match iv1, iv2 with | NoInvert, NoInvert -> true | NoInvert, CaseInvert _ | CaseInvert _, NoInvert -> false - | CaseInvert iv1, CaseInvert iv2 -> - iv1.univs == iv2.univs - && iv1.args == iv2.args + | CaseInvert {indices=i1}, CaseInvert {indices=i2} -> + i1 == i2 let hasheq_ctx (nas1, c1) (nas2, c2) = array_eqeq nas1 nas2 && c1 == c2 @@ -1368,10 +1365,9 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = and sh_invert = function | NoInvert -> NoInvert, 0 - | CaseInvert {univs;args;} -> - let univs, hu = sh_instance univs in - let args, ha = hash_term_array args in - CaseInvert {univs;args;}, combinesmall 1 (combine hu ha) + | CaseInvert {indices;} -> + let indices, ha = hash_term_array indices in + CaseInvert {indices;}, combinesmall 1 ha and sh_rec t = let (y, h) = hash_term t in @@ -1451,8 +1447,8 @@ let rec hash t = and hash_invert = function | NoInvert -> 0 - | CaseInvert {univs;args;} -> - combinesmall 1 (combine (Instance.hash univs) (hash_term_array args)) + | CaseInvert {indices;} -> + combinesmall 1 (hash_term_array indices) and hash_term_array t = Array.fold_left (fun acc t -> combine acc (hash t)) 0 t @@ -1617,6 +1613,6 @@ let rec debug_print c = and debug_invert = let open Pp in function | NoInvert -> mt() - | CaseInvert {univs;args;} -> - spc() ++ str"Invert {univs=" ++ Instance.pr Level.pr univs ++ - str "; args=" ++ prlist_with_sep spc debug_print (Array.to_list args) ++ str "} " + | CaseInvert {indices;} -> + spc() ++ str"Invert {indices=" ++ + prlist_with_sep spc debug_print (Array.to_list indices) ++ str "} " diff --git a/kernel/constr.mli b/kernel/constr.mli index 17c7da1cf6..57dd850ee7 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -49,11 +49,11 @@ type case_info = ci_pp_info : case_printing (* not interpreted by the kernel *) } -type ('constr, 'univs) pcase_invert = +type 'constr pcase_invert = | NoInvert (** Normal reduction: match when the scrutinee is a constructor. *) - | CaseInvert of { univs : 'univs; args : 'constr array; } + | CaseInvert of { indices : 'constr array; } (** Reduce when the indices match those of the unique constructor. (SProp to non SProp only) *) @@ -168,9 +168,9 @@ type 'types pcase_return = Name.t Context.binder_annot array * 'types (** Names of the branches *) type ('constr, 'types, 'univs) pcase = - case_info * 'univs * 'constr array * 'types pcase_return * ('constr, 'univs) pcase_invert * 'constr * 'constr pcase_branch array + case_info * 'univs * 'constr array * 'types pcase_return * 'constr pcase_invert * 'constr * 'constr pcase_branch array -type case_invert = (constr, Univ.Instance.t) pcase_invert +type case_invert = constr pcase_invert type case_return = types pcase_return type case_branch = constr pcase_branch type case = (constr, types, Univ.Instance.t) pcase @@ -259,7 +259,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | Ind of (inductive * 'univs) (** A name of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *) | Construct of (constructor * 'univs) (** A constructor of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *) - | Case of case_info * 'univs * 'constr array * 'types pcase_return * ('constr,'univs) pcase_invert * 'constr * 'constr pcase_branch array + | Case of case_info * 'univs * 'constr array * 'types pcase_return * 'constr pcase_invert * 'constr * 'constr pcase_branch array | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint | Proj of Projection.t * 'constr @@ -487,7 +487,7 @@ val map_return_predicate_with_binders : ('a -> 'a) -> ('a -> constr -> constr) - val fold : ('a -> constr -> 'a) -> 'a -> constr -> 'a -val fold_invert : ('a -> 'b -> 'a) -> 'a -> ('b, 'c) pcase_invert -> 'a +val fold_invert : ('a -> 'b -> 'a) -> 'a -> 'b pcase_invert -> 'a (** [map f c] maps [f] on the immediate subterms of [c]; it is not recursive and the order with which subterms are processed is @@ -495,14 +495,14 @@ val fold_invert : ('a -> 'b -> 'a) -> 'a -> ('b, 'c) pcase_invert -> 'a val map : (constr -> constr) -> constr -> constr -val map_invert : ('a -> 'a) -> ('a, 'b) pcase_invert -> ('a, 'b) pcase_invert +val map_invert : ('a -> 'a) -> 'a pcase_invert -> 'a pcase_invert (** Like {!map}, but also has an additional accumulator. *) val fold_map : ('a -> constr -> 'a * constr) -> 'a -> constr -> 'a * constr val fold_map_invert : ('a -> 'b -> 'a * 'b) -> - 'a -> ('b, 'c) pcase_invert -> 'a * ('b, 'c) pcase_invert + 'a -> 'b pcase_invert -> 'a * 'b pcase_invert (** [map_with_binders g f n c] maps [f n] on the immediate subterms of [c]; it carries an extra data [n] (typically a lift @@ -519,7 +519,7 @@ val map_with_binders : val iter : (constr -> unit) -> constr -> unit -val iter_invert : ('a -> unit) -> ('a, 'b) pcase_invert -> unit +val iter_invert : ('a -> unit) -> 'a pcase_invert -> unit (** [iter_with_binders g f n c] iters [f n] on the immediate subterms of [c]; it carries an extra data [n] (typically a lift @@ -597,8 +597,8 @@ val compare_head_gen_leq : Univ.Instance.t instance_compare_fn -> constr constr_compare_fn -> constr constr_compare_fn -val eq_invert : ('a -> 'a -> bool) -> ('b -> 'b -> bool) - -> ('a, 'b) pcase_invert -> ('a, 'b) pcase_invert -> bool +val eq_invert : ('a -> 'a -> bool) + -> 'a pcase_invert -> 'a pcase_invert -> bool (** {6 Hashconsing} *) diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 930efa5d36..f82b754c59 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -88,13 +88,6 @@ let expmod_constr cache modlist c = let u = Instance.append u' u in let pms = Array.append prefix pms in let ci = { ci with ci_npar = ci.ci_npar + Array.length prefix } in - let iv = match iv with - | NoInvert -> NoInvert - | CaseInvert {univs; args;} -> - let univs = Instance.append u' univs in - let args = Array.append prefix args in - CaseInvert {univs; args;} - in Constr.map substrec (mkCase (ci,u,pms,p,iv,t,br)) | exception Not_found -> Constr.map substrec c diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 83e41a63ec..741491c917 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -554,12 +554,14 @@ let rec execute env cstr = let c', ct = execute env c in let iv' = match iv with | NoInvert -> NoInvert - | CaseInvert {univs;args} -> - let ct' = mkApp (mkIndU (ci.ci_ind,univs), args) in + | CaseInvert {indices} -> + let args = Array.append pms indices in + let ct' = mkApp (mkIndU (ci.ci_ind,u), args) in let (ct', _) : constr * Sorts.t = execute_is_type env ct' in let () = conv_leq false env ct ct' in let _, args' = decompose_appvect ct' in - if args == args' then iv else CaseInvert {univs;args=args'} + if args == args' then iv + else CaseInvert {indices=Array.sub args' (Array.length pms) (Array.length indices)} in let p', pt = execute env p in let lf', lft = execute_array env lf in diff --git a/kernel/vars.ml b/kernel/vars.ml index 0f71057787..b09577d4db 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -253,13 +253,12 @@ let subst_univs_level_constr subst c = if u' == u then t else (changed := true; mkSort (Sorts.sort_of_univ u')) - | Case (ci, u, pms, p, CaseInvert {univs;args}, c, br) -> - if Univ.Instance.is_empty u && Univ.Instance.is_empty univs then Constr.map aux t + | Case (ci, u, pms, p, CaseInvert {indices}, c, br) -> + if Univ.Instance.is_empty u then Constr.map aux t else let u' = f u in - let univs' = f univs in - if u' == u && univs' == univs then Constr.map aux t - else (changed:=true; Constr.map aux (mkCase (ci,u',pms,p,CaseInvert {univs=univs';args},c,br))) + if u' == u then Constr.map aux t + else (changed:=true; Constr.map aux (mkCase (ci,u',pms,p,CaseInvert {indices},c,br))) | Case (ci, u, pms, p, NoInvert, c, br) -> if Univ.Instance.is_empty u then Constr.map aux t @@ -314,11 +313,10 @@ let subst_instance_constr subst c = if u' == u then t else (mkSort (Sorts.sort_of_univ u')) - | Case (ci, u, pms, p, CaseInvert {univs;args}, c, br) -> + | Case (ci, u, pms, p, CaseInvert {indices}, c, br) -> let u' = f u in - let univs' = f univs in - if u' == u && univs' == univs then Constr.map aux t - else Constr.map aux (mkCase (ci,u',pms,p,CaseInvert {univs=univs';args},c,br)) + if u' == u then Constr.map aux t + else Constr.map aux (mkCase (ci,u',pms,p,CaseInvert {indices},c,br)) | Case (ci, u, pms, p, NoInvert, c, br) -> if Univ.Instance.is_empty u then Constr.map aux t @@ -366,11 +364,8 @@ let universes_of_constr c = | Array (u,_,_,_) -> let s = LSet.fold LSet.add (Instance.levels u) s in Constr.fold aux s c - | Case (_, u, _, _, CaseInvert {univs;args=_},_ ,_) -> + | Case (_, u, _, _, _,_ ,_) -> let s = LSet.fold LSet.add (Instance.levels u) s in - let s = LSet.fold LSet.add (Instance.levels univs) s in Constr.fold aux s c - | Case (_, u, _, _, NoInvert, _, _) -> - Constr.fold aux (LSet.fold LSet.add (Instance.levels u) s) c | _ -> Constr.fold aux s c in aux LSet.empty c -- cgit v1.2.3