diff options
Diffstat (limited to 'pretyping/evardefine.ml')
| -rw-r--r-- | pretyping/evardefine.ml | 70 |
1 files changed, 36 insertions, 34 deletions
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index 06f619410..c5ae684e3 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -10,10 +10,11 @@ open Util open Pp open Names open Term -open Vars open Termops -open Namegen open Environ +open EConstr +open Vars +open Namegen open Evd open Evarutil open Pretype_errors @@ -27,21 +28,22 @@ let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal t (Sigma.to_evar_map evd, evk) let env_nf_evar sigma env = + let nf_evar c = nf_evar sigma c in process_rel_context - (fun d e -> push_rel (RelDecl.map_constr (nf_evar sigma) d) e) env + (fun d e -> push_rel (RelDecl.map_constr nf_evar d) e) env let env_nf_betaiotaevar sigma env = process_rel_context (fun d e -> - push_rel (RelDecl.map_constr (Reductionops.nf_betaiota sigma) d) e) env + push_rel (RelDecl.map_constr (fun c -> Reductionops.nf_betaiota sigma c) d) e) env (****************************************) (* Operations on value/type constraints *) (****************************************) -type type_constraint = types option +type type_constraint = EConstr.types option -type val_constraint = constr option +type val_constraint = EConstr.constr option (* Old comment... * Basically, we have the following kind of constraints (in increasing @@ -78,8 +80,8 @@ let define_pure_evar_as_product evd evk = let evi = Evd.find_undefined evd evk in let evenv = evar_env evi in let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in - let concl = Reductionops.whd_all evenv evd evi.evar_concl in - let s = destSort concl in + let concl = Reductionops.whd_all evenv evd (EConstr.of_constr evi.evar_concl) in + let s = destSort evd concl in let evd1,(dom,u1) = let evd = Sigma.Unsafe.of_evar_map evd in let Sigma (e, evd1, _) = new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in @@ -89,7 +91,7 @@ let define_pure_evar_as_product evd evk = let newenv = push_named (LocalAssum (id, dom)) evenv in let src = evar_source evk evd1 in let filter = Filter.extend 1 (evar_filter evi) in - if is_prop_sort s then + if is_prop_sort (ESorts.kind evd1 s) then (* Impredicative product, conclusion must fall in [Prop]. *) new_evar_unsafe newenv evd1 concl ~src ~filter else @@ -100,11 +102,11 @@ let define_pure_evar_as_product evd evk = (Sigma.to_evar_map evd3, e) in let prods = Univ.sup (univ_of_sort u1) (univ_of_sort srng) in - let evd3 = Evd.set_leq_sort evenv evd3 (Type prods) s in + let evd3 = Evd.set_leq_sort evenv evd3 (Type prods) (ESorts.kind evd1 s) in evd3, rng in let prod = mkProd (Name id, dom, subst_var id rng) in - let evd3 = Evd.define evk prod evd2 in + let evd3 = Evd.define evk (EConstr.Unsafe.to_constr prod) evd2 in evd3,prod (* Refine an applied evar to a product and returns its instantiation *) @@ -112,11 +114,11 @@ let define_pure_evar_as_product evd evk = let define_evar_as_product evd (evk,args) = let evd,prod = define_pure_evar_as_product evd evk in (* Quick way to compute the instantiation of evk with args *) - let na,dom,rng = destProd prod in - let evdom = mkEvar (fst (destEvar dom), args) in + let na,dom,rng = destProd evd prod in + let evdom = mkEvar (fst (destEvar evd dom), args) in let evrngargs = Array.cons (mkRel 1) (Array.map (lift 1) args) in - let evrng = mkEvar (fst (destEvar rng), evrngargs) in - evd,mkProd (na, evdom, evrng) + let evrng = mkEvar (fst (destEvar evd rng), evrngargs) in + evd, mkProd (na, evdom, evrng) (* Refine an evar with an abstraction @@ -131,10 +133,10 @@ let define_pure_evar_as_lambda env evd evk = let open Context.Named.Declaration in let evi = Evd.find_undefined evd evk in let evenv = evar_env evi in - let typ = Reductionops.whd_all evenv evd (evar_concl evi) in - let evd1,(na,dom,rng) = match kind_of_term typ with + let typ = Reductionops.whd_all evenv evd (EConstr.of_constr (evar_concl evi)) in + let evd1,(na,dom,rng) = match EConstr.kind evd typ with | Prod (na,dom,rng) -> (evd,(na,dom,rng)) - | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd typ + | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd evd typ | _ -> error_not_product env evd typ in let avoid = ids_of_named_context (evar_context evi) in let id = @@ -144,23 +146,23 @@ let define_pure_evar_as_lambda env evd evk = let src = evar_source evk evd1 in let evd2,body = new_evar_unsafe newenv evd1 ~src (subst1 (mkVar id) rng) ~filter in let lam = mkLambda (Name id, dom, subst_var id body) in - Evd.define evk lam evd2, lam + Evd.define evk (EConstr.Unsafe.to_constr lam) evd2, lam let define_evar_as_lambda env evd (evk,args) = let evd,lam = define_pure_evar_as_lambda env evd evk in (* Quick way to compute the instantiation of evk with args *) - let na,dom,body = destLambda lam in + let na,dom,body = destLambda evd lam in let evbodyargs = Array.cons (mkRel 1) (Array.map (lift 1) args) in - let evbody = mkEvar (fst (destEvar body), evbodyargs) in - evd,mkLambda (na, dom, evbody) + let evbody = mkEvar (fst (destEvar evd body), evbodyargs) in + evd, mkLambda (na, dom, evbody) let rec evar_absorb_arguments env evd (evk,args as ev) = function | [] -> evd,ev | a::l -> (* TODO: optimize and avoid introducing intermediate evars *) let evd,lam = define_pure_evar_as_lambda env evd evk in - let _,_,body = destLambda lam in - let evk = fst (destEvar body) in + let _,_,body = destLambda evd lam in + let evk = fst (destEvar evd body) in evar_absorb_arguments env evd (evk, Array.cons a args) l (* Refining an evar to a sort *) @@ -169,10 +171,10 @@ let define_evar_as_sort env evd (ev,args) = let evd, u = new_univ_variable univ_rigid evd in let evi = Evd.find_undefined evd ev in let s = Type u in - let concl = Reductionops.whd_all (evar_env evi) evd evi.evar_concl in - let sort = destSort concl in - let evd' = Evd.define ev (mkSort s) evd in - Evd.set_leq_sort env evd' (Type (Univ.super u)) sort, s + let concl = Reductionops.whd_all (evar_env evi) evd (EConstr.of_constr evi.evar_concl) in + let sort = destSort evd concl in + let evd' = Evd.define ev (Constr.mkSort s) evd in + Evd.set_leq_sort env evd' (Type (Univ.super u)) (ESorts.kind evd' sort), s (* Propagation of constraints through application and abstraction: Given a type constraint on a functional term, returns the type @@ -182,14 +184,14 @@ let define_evar_as_sort env evd (ev,args) = let split_tycon loc env evd tycon = let rec real_split evd c = let t = Reductionops.whd_all env evd c in - match kind_of_term t with + match EConstr.kind evd t with | Prod (na,dom,rng) -> evd, (na, dom, rng) | Evar ev (* ev is undefined because of whd_all *) -> let (evd',prod) = define_evar_as_product evd ev in - let (_,dom,rng) = destProd prod in + let (_,dom,rng) = destProd evd prod in evd',(Anonymous, dom, rng) - | App (c,args) when isEvar c -> - let (evd',lam) = define_evar_as_lambda env evd (destEvar c) in + | App (c,args) when isEvar evd c -> + let (evd',lam) = define_evar_as_lambda env evd (destEvar evd c) in real_split evd' (mkApp (lam,args)) | _ -> error_not_product ~loc env evd c in @@ -202,6 +204,6 @@ let split_tycon loc env evd tycon = let valcon_of_tycon x = x let lift_tycon n = Option.map (lift n) -let pr_tycon env = function +let pr_tycon env sigma = function None -> str "None" - | Some t -> Termops.print_constr_env env t + | Some t -> Termops.print_constr_env env sigma t |