diff options
Diffstat (limited to 'engine/eConstr.ml')
| -rw-r--r-- | engine/eConstr.ml | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index d303038c5d..9ac16b5b48 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -150,6 +150,8 @@ type rel_declaration = (constr, types) Context.Rel.Declaration.pt type named_context = (constr, types) Context.Named.pt type rel_context = (constr, types) Context.Rel.pt +type 'a puniverses = 'a * EInstance.t + let in_punivs a = (a, EInstance.empty) let mkProp = of_kind (Sort (ESorts.make Sorts.prop)) @@ -693,6 +695,10 @@ let cast_rel_context : type a b. (a,b) eq -> (a, a) Rel.pt -> (b, b) Rel.pt = fun Refl x -> x +let cast_rec_decl : + type a b. (a,b) eq -> (a, a) Constr.prec_declaration -> (b, b) Constr.prec_declaration = + fun Refl x -> x + let cast_named_decl : type a b. (a,b) eq -> (a, a) Named.Declaration.pt -> (b, b) Named.Declaration.pt = fun Refl x -> x @@ -768,6 +774,20 @@ let rec isArity sigma c = | Sort _ -> true | _ -> false +type arity = rel_context * ESorts.t + +let destArity sigma = + let open Context.Rel.Declaration in + let rec prodec_rec l c = + match kind sigma c with + | Prod (x,t,c) -> prodec_rec (LocalAssum (x,t) :: l) c + | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t) :: l) c + | Cast (c,_,_) -> prodec_rec l c + | Sort s -> l,s + | _ -> anomaly ~label:"destArity" (Pp.str "not an arity.") + in + prodec_rec [] + let mkProd_or_LetIn decl c = let open Context.Rel.Declaration in match decl with @@ -801,6 +821,7 @@ let it_mkLambda_or_LetIn t ctx = List.fold_left (fun c d -> mkLambda_or_LetIn d let push_rel d e = push_rel (cast_rel_decl unsafe_eq d) e let push_rel_context d e = push_rel_context (cast_rel_context unsafe_eq d) e +let push_rec_types d e = push_rec_types (cast_rec_decl unsafe_eq d) e let push_named d e = push_named (cast_named_decl unsafe_eq d) e let push_named_context d e = push_named_context (cast_named_context unsafe_eq d) e let push_named_context_val d e = push_named_context_val (cast_named_decl unsafe_eq d) e @@ -815,6 +836,15 @@ 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 map_rel_context_in_env f env sign = + let rec aux env acc = function + | d::sign -> + aux (push_rel d env) (Context.Rel.Declaration.map_constr (f env) d :: acc) sign + | [] -> + acc + in + aux env [] (List.rev 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 |