diff options
Diffstat (limited to 'pretyping/patternops.ml')
| -rw-r--r-- | pretyping/patternops.ml | 72 |
1 files changed, 36 insertions, 36 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 4e3c77cb1a..c788efda48 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -280,66 +280,64 @@ let rec liftn_pattern k n = function let lift_pattern k = liftn_pattern k 1 -let rec subst_pattern subst pat = +let rec subst_pattern env sigma subst pat = match pat with | PRef ref -> let ref',t = subst_global subst ref in if ref' == ref then pat else (match t with | None -> PRef ref' | Some t -> - let env = Global.env () in - let evd = Evd.from_env env in - pattern_of_constr env evd t.Univ.univ_abstracted_value) + pattern_of_constr env sigma t.Univ.univ_abstracted_value) | PVar _ | PEvar _ | PRel _ | PInt _ -> pat | PProj (p,c) -> let p' = Projection.map (subst_mind subst) p in - let c' = subst_pattern subst c in + let c' = subst_pattern env sigma subst c in if p' == p && c' == c then pat else PProj(p',c') | PApp (f,args) -> - let f' = subst_pattern subst f in - let args' = Array.Smart.map (subst_pattern subst) args in + let f' = subst_pattern env sigma subst f in + let args' = Array.Smart.map (subst_pattern env sigma subst) args in if f' == f && args' == args then pat else PApp (f',args') | PSoApp (i,args) -> - let args' = List.Smart.map (subst_pattern subst) args in + let args' = List.Smart.map (subst_pattern env sigma subst) args in if args' == args then pat else PSoApp (i,args') | PLambda (name,c1,c2) -> - let c1' = subst_pattern subst c1 in - let c2' = subst_pattern subst c2 in + let c1' = subst_pattern env sigma subst c1 in + let c2' = subst_pattern env sigma subst c2 in if c1' == c1 && c2' == c2 then pat else PLambda (name,c1',c2') | PProd (name,c1,c2) -> - let c1' = subst_pattern subst c1 in - let c2' = subst_pattern subst c2 in + let c1' = subst_pattern env sigma subst c1 in + let c2' = subst_pattern env sigma subst c2 in if c1' == c1 && c2' == c2 then pat else PProd (name,c1',c2') | PLetIn (name,c1,t,c2) -> - let c1' = subst_pattern subst c1 in - let t' = Option.Smart.map (subst_pattern subst) t in - let c2' = subst_pattern subst c2 in + let c1' = subst_pattern env sigma subst c1 in + let t' = Option.Smart.map (subst_pattern env sigma subst) t in + let c2' = subst_pattern env sigma subst c2 in if c1' == c1 && t' == t && c2' == c2 then pat else PLetIn (name,c1',t',c2') | PSort _ | PMeta _ -> pat | PIf (c,c1,c2) -> - let c' = subst_pattern subst c in - let c1' = subst_pattern subst c1 in - let c2' = subst_pattern subst c2 in + let c' = subst_pattern env sigma subst c in + let c1' = subst_pattern env sigma subst c1 in + let c2' = subst_pattern env sigma subst c2 in if c' == c && c1' == c1 && c2' == c2 then pat else PIf (c',c1',c2') | PCase (cip,typ,c,branches) -> let ind = cip.cip_ind in let ind' = Option.Smart.map (subst_ind subst) ind in let cip' = if ind' == ind then cip else { cip with cip_ind = ind' } in - let typ' = subst_pattern subst typ in - let c' = subst_pattern subst c in + let typ' = subst_pattern env sigma subst typ in + let c' = subst_pattern env sigma subst c in let subst_branch ((i,n,c) as br) = - let c' = subst_pattern subst c in + let c' = subst_pattern env sigma subst c in if c' == c then br else (i,n,c') in let branches' = List.Smart.map subst_branch branches in @@ -347,13 +345,13 @@ let rec subst_pattern subst pat = then pat else PCase(cip', typ', c', branches') | PFix (lni,(lna,tl,bl)) -> - let tl' = Array.Smart.map (subst_pattern subst) tl in - let bl' = Array.Smart.map (subst_pattern subst) bl in + let tl' = Array.Smart.map (subst_pattern env sigma subst) tl in + let bl' = Array.Smart.map (subst_pattern env sigma subst) bl in if bl' == bl && tl' == tl then pat else PFix (lni,(lna,tl',bl')) | PCoFix (ln,(lna,tl,bl)) -> - let tl' = Array.Smart.map (subst_pattern subst) tl in - let bl' = Array.Smart.map (subst_pattern subst) bl in + let tl' = Array.Smart.map (subst_pattern env sigma subst) tl in + let bl' = Array.Smart.map (subst_pattern env sigma subst) bl in if bl' == bl && tl' == tl then pat else PCoFix (ln,(lna,tl',bl')) @@ -472,17 +470,19 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function PCase (info, pred, pat_of_raw metas vars c, brs) | GRec (GFix (ln,n), ids, decls, tl, cl) -> - if Array.exists (function (Some n, GStructRec) -> false | _ -> true) ln then - err ?loc (Pp.str "\"struct\" annotation is expected.") - else - let ln = Array.map (fst %> Option.get) ln in - let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls tl in - let tl = Array.map (fun (ctx,tl) -> it_mkPProd_or_LetIn tl ctx) ctxtl in - let vars = Array.fold_left (fun vars na -> Name na::vars) vars ids in - let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls cl in - let cl = Array.map (fun (ctx,cl) -> it_mkPLambda_or_LetIn cl ctx) ctxtl in - let names = Array.map (fun id -> Name id) ids in - PFix ((ln,n), (names, tl, cl)) + let get_struct_arg = function + | Some n -> n + | None -> err ?loc (Pp.str "\"struct\" annotation is expected.") + (* TODO why can't the annotation be omitted? *) + in + let ln = Array.map get_struct_arg ln in + let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls tl in + let tl = Array.map (fun (ctx,tl) -> it_mkPProd_or_LetIn tl ctx) ctxtl in + let vars = Array.fold_left (fun vars na -> Name na::vars) vars ids in + let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls cl in + let cl = Array.map (fun (ctx,cl) -> it_mkPLambda_or_LetIn cl ctx) ctxtl in + let names = Array.map (fun id -> Name id) ids in + PFix ((ln,n), (names, tl, cl)) | GRec (GCoFix n, ids, decls, tl, cl) -> let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls tl in |