From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- engine/eConstr.ml | 259 ++++++++++++++++-------------------------------------- 1 file changed, 77 insertions(+), 182 deletions(-) (limited to 'engine/eConstr.ml') diff --git a/engine/eConstr.ml b/engine/eConstr.ml index bd47a04f..e109cbd0 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -13,132 +13,8 @@ open Util open Names open Constr open Context -open Evd - -module API : -sig -module ESorts : -sig -type t -val make : Sorts.t -> t -val kind : Evd.evar_map -> t -> Sorts.t -val unsafe_to_sorts : t -> Sorts.t -end -module EInstance : -sig -type t -val make : Univ.Instance.t -> t -val kind : Evd.evar_map -> t -> Univ.Instance.t -val empty : t -val is_empty : t -> bool -val unsafe_to_instance : t -> Univ.Instance.t -end -type t -val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_term -val kind_upto : Evd.evar_map -> constr -> (constr, types, Sorts.t, Univ.Instance.t) Constr.kind_of_term -val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type -val whd_evar : Evd.evar_map -> t -> t -val of_kind : (t, t, ESorts.t, EInstance.t) Constr.kind_of_term -> t -val of_constr : Constr.t -> t -val to_constr : evar_map -> t -> Constr.t -val unsafe_to_constr : t -> Constr.t -val unsafe_eq : (t, Constr.t) eq -val of_named_decl : (Constr.t, Constr.types) Context.Named.Declaration.pt -> (t, t) Context.Named.Declaration.pt -val unsafe_to_named_decl : (t, t) Context.Named.Declaration.pt -> (Constr.t, Constr.types) Context.Named.Declaration.pt -val unsafe_to_rel_decl : (t, t) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt -val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, t) Context.Rel.Declaration.pt -val to_rel_decl : Evd.evar_map -> (t, t) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt -end = -struct - -module ESorts = -struct - type t = Sorts.t - let make s = s - let kind sigma = function - | Sorts.Type u -> Sorts.sort_of_univ (Evd.normalize_universe sigma u) - | s -> s - let unsafe_to_sorts s = s -end - -module EInstance = -struct - type t = Univ.Instance.t - let make i = i - let kind sigma i = - if Univ.Instance.is_empty i then i - else Evd.normalize_universe_instance sigma i - let empty = Univ.Instance.empty - let is_empty = Univ.Instance.is_empty - let unsafe_to_instance t = t -end -type t = Constr.t - -let safe_evar_value sigma ev = - try Some (Evd.existential_value sigma ev) - with NotInstantiatedEvar | Not_found -> None - -let rec whd_evar sigma c = - match Constr.kind c with - | Evar ev -> - begin match safe_evar_value sigma ev with - | Some c -> whd_evar sigma c - | None -> c - end - | App (f, args) when isEvar f -> - (** Enforce smart constructor invariant on applications *) - let ev = destEvar f in - begin match safe_evar_value sigma ev with - | None -> c - | Some f -> whd_evar sigma (mkApp (f, args)) - end - | Cast (c0, k, t) when isEvar c0 -> - (** Enforce smart constructor invariant on casts. *) - let ev = destEvar c0 in - begin match safe_evar_value sigma ev with - | None -> c - | Some c -> whd_evar sigma (mkCast (c, k, t)) - end - | _ -> c - -let kind sigma c = Constr.kind (whd_evar sigma c) -let kind_upto = kind -let kind_of_type sigma c = Term.kind_of_type (whd_evar sigma c) -let of_kind = Constr.of_kind -let of_constr c = c -let unsafe_to_constr c = c -let unsafe_eq = Refl - -let rec to_constr sigma c = match Constr.kind c with -| Evar ev -> - begin match safe_evar_value sigma ev with - | Some c -> to_constr sigma c - | None -> Constr.map (fun c -> to_constr sigma c) c - end -| Sort (Sorts.Type u) -> - let u' = Evd.normalize_universe sigma u in - if u' == u then c else mkSort (Sorts.sort_of_univ u') -| Const (c', u) when not (Univ.Instance.is_empty u) -> - let u' = Evd.normalize_universe_instance sigma u in - if u' == u then c else mkConstU (c', u') -| Ind (i, u) when not (Univ.Instance.is_empty u) -> - let u' = Evd.normalize_universe_instance sigma u in - if u' == u then c else mkIndU (i, u') -| Construct (co, u) when not (Univ.Instance.is_empty u) -> - let u' = Evd.normalize_universe_instance sigma u in - if u' == u then c else mkConstructU (co, u') -| _ -> Constr.map (fun c -> to_constr sigma c) c - -let of_named_decl d = d -let unsafe_to_named_decl d = d -let of_rel_decl d = d -let unsafe_to_rel_decl d = d -let to_rel_decl sigma d = Context.Rel.Declaration.map_constr (to_constr sigma) d - -end - -include API +include Evd.MiniEConstr type types = t type constr = t @@ -201,6 +77,14 @@ let isFix sigma c = match kind sigma c with Fix _ -> true | _ -> false let isCoFix sigma c = match kind sigma c with CoFix _ -> true | _ -> false let isCase sigma c = match kind sigma c with Case _ -> true | _ -> false let isProj sigma c = match kind sigma c with Proj _ -> true | _ -> false + +let rec isType sigma c = match kind sigma c with + | Sort s -> (match ESorts.kind sigma s with + | Sorts.Type _ -> true + | _ -> false ) + | Cast (c,_,_) -> isType sigma c + | _ -> false + let isVarId sigma id c = match kind sigma c with Var id' -> Id.equal id id' | _ -> false let isRelN sigma n c = @@ -381,8 +265,7 @@ let decompose_prod_n_assum sigma n c = in prodec_rec Context.Rel.empty n c -let existential_type sigma (evk, args) = - of_constr (existential_type sigma (evk, Array.map unsafe_to_constr args)) +let existential_type = Evd.existential_type let map sigma f c = match kind sigma c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ @@ -410,7 +293,7 @@ let map sigma f c = match kind sigma c with else mkLetIn (na, b', t', k') | App (b,l) -> let b' = f b in - let l' = Array.smartmap f l in + let l' = Array.Smart.map f l in if b'==b && l'==l then c else mkApp (b', l') | Proj (p,t) -> @@ -418,23 +301,23 @@ let map sigma f c = match kind sigma c with if t' == t then c else mkProj (p, t') | Evar (e,l) -> - let l' = Array.smartmap f l in + let l' = Array.Smart.map f l in if l'==l then c else mkEvar (e, l') | Case (ci,p,b,bl) -> let b' = f b in let p' = f p in - let bl' = Array.smartmap f bl in + let bl' = Array.Smart.map f bl in if b'==b && p'==p && bl'==bl then c else mkCase (ci, p', b', bl') | Fix (ln,(lna,tl,bl)) -> - let tl' = Array.smartmap f tl in - let bl' = Array.smartmap f bl in + let tl' = Array.Smart.map f tl in + let bl' = Array.Smart.map f bl in if tl'==tl && bl'==bl then c else mkFix (ln,(lna,tl',bl')) | CoFix(ln,(lna,tl,bl)) -> - let tl' = Array.smartmap f tl in - let bl' = Array.smartmap f bl in + let tl' = Array.Smart.map f tl in + let bl' = Array.Smart.map f bl in if tl'==tl && bl'==bl then c else mkCoFix (ln,(lna,tl',bl')) @@ -464,7 +347,7 @@ let map_with_binders sigma g f l c0 = match kind sigma c0 with else mkLetIn (na, b', t', c') | App (c, al) -> let c' = f l c in - let al' = CArray.Fun1.smartmap f l al in + let al' = Array.Fun1.Smart.map f l al in if c' == c && al' == al then c0 else mkApp (c', al') | Proj (p, t) -> @@ -472,25 +355,25 @@ let map_with_binders sigma g f l c0 = match kind sigma c0 with if t' == t then c0 else mkProj (p, t') | Evar (e, al) -> - let al' = CArray.Fun1.smartmap f l al in + let al' = Array.Fun1.Smart.map f l al in if al' == al then c0 else mkEvar (e, al') | Case (ci, p, c, bl) -> let p' = f l p in let c' = f l c in - let bl' = CArray.Fun1.smartmap f l bl in + let bl' = Array.Fun1.Smart.map f l bl in if p' == p && c' == c && bl' == bl then c0 else mkCase (ci, p', c', bl') | Fix (ln, (lna, tl, bl)) -> - let tl' = CArray.Fun1.smartmap f l tl in + let tl' = Array.Fun1.Smart.map f l tl in let l' = iterate g (Array.length tl) l in - let bl' = CArray.Fun1.smartmap f l' bl in + let bl' = Array.Fun1.Smart.map f l' bl in if tl' == tl && bl' == bl then c0 else mkFix (ln,(lna,tl',bl')) | CoFix(ln,(lna,tl,bl)) -> - let tl' = CArray.Fun1.smartmap f l tl in + let tl' = Array.Fun1.Smart.map f l tl in let l' = iterate g (Array.length tl) l in - let bl' = CArray.Fun1.smartmap f l' bl in + let bl' = Array.Fun1.Smart.map f l' bl in mkCoFix (ln,(lna,tl',bl')) let iter sigma f c = match kind sigma c with @@ -516,9 +399,9 @@ let iter_with_full_binders sigma g f n c = | Prod (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c | Lambda (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c | LetIn (na,b,t,c) -> f n b; f n t; f (g (LocalDef (na, b, t)) n) c - | App (c,l) -> f n c; CArray.Fun1.iter f n l - | Evar (_,l) -> CArray.Fun1.iter f n l - | Case (_,p,c,bl) -> f n p; f n c; CArray.Fun1.iter f n bl + | App (c,l) -> f n c; Array.Fun1.iter f n l + | Evar (_,l) -> Array.Fun1.iter f n l + | Case (_,p,c,bl) -> f n p; f n c; Array.Fun1.iter f n bl | Proj (p,c) -> f n c | Fix (_,(lna,tl,bl)) -> Array.iter (f n) tl; @@ -551,10 +434,22 @@ let fold sigma f acc c = match kind sigma c with let compare_gen k eq_inst eq_sort eq_constr nargs c1 c2 = (c1 == c2) || Constr.compare_head_gen_with k k eq_inst eq_sort eq_constr nargs c1 c2 +let eq_einstance sigma i1 i2 = + let i1 = EInstance.kind sigma (EInstance.make i1) in + let i2 = EInstance.kind sigma (EInstance.make i2) in + Univ.Instance.equal i1 i2 + +let eq_esorts sigma s1 s2 = + let s1 = ESorts.kind sigma (ESorts.make s1) in + let s2 = ESorts.kind sigma (ESorts.make s2) in + Sorts.equal s1 s2 + let eq_constr sigma c1 c2 = let kind c = kind_upto sigma c in + let eq_inst _ _ i1 i2 = eq_einstance sigma i1 i2 in + let eq_sorts s1 s2 = eq_esorts sigma s1 s2 in let rec eq_constr nargs c1 c2 = - compare_gen kind (fun _ _ -> Univ.Instance.equal) Sorts.equal eq_constr nargs c1 c2 + compare_gen kind eq_inst eq_sorts eq_constr nargs c1 c2 in eq_constr 0 (unsafe_to_constr c1) (unsafe_to_constr c2) @@ -567,32 +462,34 @@ let eq_constr_nounivs sigma c1 c2 = let compare_constr sigma cmp c1 c2 = let kind c = kind_upto sigma c in + let eq_inst _ _ i1 i2 = eq_einstance sigma i1 i2 in + let eq_sorts s1 s2 = eq_esorts sigma s1 s2 in let cmp nargs c1 c2 = cmp (of_constr c1) (of_constr c2) in - compare_gen kind (fun _ _ -> Univ.Instance.equal) Sorts.equal cmp 0 (unsafe_to_constr c1) (unsafe_to_constr c2) + compare_gen kind eq_inst eq_sorts cmp 0 (unsafe_to_constr c1) (unsafe_to_constr c2) let compare_cumulative_instances cv_pb nargs_ok variances u u' cstrs = - let open Universes in + let open UnivProblem in if not nargs_ok then enforce_eq_instances_univs false u u' cstrs else CArray.fold_left3 (fun cstrs v u u' -> let open Univ.Variance in match v with - | Irrelevant -> Constraints.add (UWeak (u,u')) cstrs + | Irrelevant -> Set.add (UWeak (u,u')) cstrs | Covariant -> let u = Univ.Universe.make u in let u' = Univ.Universe.make u' in (match cv_pb with - | Reduction.CONV -> Constraints.add (UEq (u,u')) cstrs - | Reduction.CUMUL -> Constraints.add (ULe (u,u')) cstrs) + | Reduction.CONV -> Set.add (UEq (u,u')) cstrs + | Reduction.CUMUL -> Set.add (ULe (u,u')) cstrs) | Invariant -> let u = Univ.Universe.make u in let u' = Univ.Universe.make u' in - Constraints.add (UEq (u,u')) cstrs) + Set.add (UEq (u,u')) cstrs) cstrs variances (Univ.Instance.to_array u) (Univ.Instance.to_array u') let cmp_inductives cv_pb (mind,ind as spec) nargs u1 u2 cstrs = - let open Universes in + let open UnivProblem in match mind.Declarations.mind_universes with | Declarations.Monomorphic_ind _ -> assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0); @@ -605,7 +502,7 @@ let cmp_inductives cv_pb (mind,ind as spec) nargs u1 u2 cstrs = compare_cumulative_instances cv_pb (Int.equal num_param_arity nargs) variances u1 u2 cstrs let cmp_constructors (mind, ind, cns as spec) nargs u1 u2 cstrs = - let open Universes in + let open UnivProblem in match mind.Declarations.mind_universes with | Declarations.Monomorphic_ind _ -> cstrs @@ -616,7 +513,7 @@ let cmp_constructors (mind, ind, cns as spec) nargs u1 u2 cstrs = if not (Int.equal num_cnstr_args nargs) then enforce_eq_instances_univs false u1 u2 cstrs else - Array.fold_left2 (fun cstrs u1 u2 -> Universes.(Constraints.add (UWeak (u1,u2)) cstrs)) + Array.fold_left2 (fun cstrs u1 u2 -> UnivProblem.(Set.add (UWeak (u1,u2)) cstrs)) cstrs (Univ.Instance.to_array u1) (Univ.Instance.to_array u2) let eq_universes env sigma cstrs cv_pb ref nargs l l' = @@ -624,7 +521,8 @@ let eq_universes env sigma cstrs cv_pb ref nargs l l' = else let l = Evd.normalize_universe_instance sigma l and l' = Evd.normalize_universe_instance sigma l' in - let open Universes in + let open GlobRef in + let open UnivProblem in match ref with | VarRef _ -> assert false (* variables don't have instances *) | ConstRef _ -> @@ -639,11 +537,11 @@ let eq_universes env sigma cstrs cv_pb ref nargs l l' = true let test_constr_universes env sigma leq m n = - let open Universes in + let open UnivProblem in let kind c = kind_upto sigma c in - if m == n then Some Constraints.empty + if m == n then Some Set.empty else - let cstrs = ref Constraints.empty in + let cstrs = ref Set.empty in let cv_pb = if leq then Reduction.CUMUL else Reduction.CONV in let eq_universes ref nargs l l' = eq_universes env sigma cstrs Reduction.CONV ref nargs l l' and leq_universes ref nargs l l' = eq_universes env sigma cstrs cv_pb ref nargs l l' in @@ -651,7 +549,7 @@ let test_constr_universes env sigma leq m n = let s1 = ESorts.kind sigma (ESorts.make s1) in let s2 = ESorts.kind sigma (ESorts.make s2) in if Sorts.equal s1 s2 then true - else (cstrs := Constraints.add + else (cstrs := Set.add (UEq (Sorts.univ_of_sort s1,Sorts.univ_of_sort s2)) !cstrs; true) in @@ -660,7 +558,7 @@ let test_constr_universes env sigma leq m n = let s2 = ESorts.kind sigma (ESorts.make s2) in if Sorts.equal s1 s2 then true else - (cstrs := Constraints.add + (cstrs := Set.add (ULe (Sorts.univ_of_sort s1,Sorts.univ_of_sort s2)) !cstrs; true) in @@ -689,24 +587,23 @@ let compare_head_gen_proj env sigma equ eqs eqc' nargs m n = | App (f, args), Proj (p, c) -> (match kind_upto sigma f with | Const (p', u) when Constant.equal (Projection.constant p) p' -> - let pb = Environ.lookup_projection p env in - let npars = pb.Declarations.proj_npars in - if Array.length args == npars + 1 then + let npars = Projection.npars p in + if Array.length args == npars + 1 then eqc' 0 c args.(npars) else false | _ -> false) | _ -> Constr.compare_head_gen_with kind kind equ eqs eqc' nargs m n let eq_constr_universes_proj env sigma m n = - let open Universes in - if m == n then Some Constraints.empty + let open UnivProblem in + if m == n then Some Set.empty else - let cstrs = ref Constraints.empty in + let cstrs = ref Set.empty in let eq_universes ref l l' = eq_universes env sigma cstrs Reduction.CONV ref l l' in let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else - (cstrs := Constraints.add + (cstrs := Set.add (UEq (Sorts.univ_of_sort s1, Sorts.univ_of_sort s2)) !cstrs; true) in @@ -716,25 +613,14 @@ let eq_constr_universes_proj env sigma m n = let res = eq_constr' 0 (unsafe_to_constr m) (unsafe_to_constr n) in if res then Some !cstrs else None -let universes_of_constr env sigma c = +let universes_of_constr sigma c = let open Univ in - let open Declarations in let rec aux s c = match kind sigma c with | Const (c, u) -> - begin match (Environ.lookup_constant c env).const_universes with - | Polymorphic_const _ -> LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s - | Monomorphic_const (univs, _) -> - LSet.union s univs - end | Ind ((mind,_), u) | Construct (((mind,_),_), u) -> - begin match (Environ.lookup_mind mind env).mind_universes with - | Cumulative_ind _ | Polymorphic_ind _ -> LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s - | Monomorphic_ind (univs,_) -> - LSet.union s univs - end | Sort u -> let sort = ESorts.kind sigma u in if Sorts.is_small sort then s @@ -743,7 +629,7 @@ let universes_of_constr env sigma c = LSet.fold LSet.add (Universe.levels u) s | Evar (k, args) -> let concl = Evd.evar_concl (Evd.find sigma k) in - fold sigma aux (aux s (of_constr concl)) c + fold sigma aux (aux s concl) c | _ -> fold sigma aux s c in aux LSet.empty c @@ -901,9 +787,13 @@ let named_context e = cast_named_context (sym unsafe_eq) (named_context e) let val_of_named_context e = val_of_named_context (cast_named_context unsafe_eq e) let named_context_of_val e = cast_named_context (sym unsafe_eq) (named_context_of_val e) +let of_existential : Constr.existential -> existential = + let gen : type a b. (a,b) eq -> 'c * b array -> 'c * a array = fun Refl x -> x in + gen unsafe_eq + let lookup_rel i e = cast_rel_decl (sym unsafe_eq) (lookup_rel i e) let lookup_named n e = cast_named_decl (sym unsafe_eq) (lookup_named n e) -let lookup_named_val n e = cast_named_decl (sym unsafe_eq) (lookup_named_val n e) +let lookup_named_val n e = cast_named_decl (sym unsafe_eq) (lookup_named_ctxt n e) let map_rel_context_in_env f env sign = let rec aux env acc = function @@ -916,7 +806,7 @@ let map_rel_context_in_env f env sign = let fresh_global ?loc ?rigid ?names env sigma reference = let (evd,t) = Evd.fresh_global ?loc ?rigid ?names env sigma reference in - evd, of_constr t + evd, t let is_global sigma gr c = Globnames.is_global gr (to_constr sigma c) @@ -928,5 +818,10 @@ let to_instance = EInstance.unsafe_to_instance let to_constr = unsafe_to_constr let to_rel_decl = unsafe_to_rel_decl let to_named_decl = unsafe_to_named_decl +let to_named_context = + let gen : type a b. (a, b) eq -> (a,a) Context.Named.pt -> (b,b) Context.Named.pt + = fun Refl x -> x + in + gen unsafe_eq let eq = unsafe_eq end -- cgit v1.2.3