diff options
Diffstat (limited to 'pretyping/evardefine.ml')
| -rw-r--r-- | pretyping/evardefine.ml | 207 |
1 files changed, 207 insertions, 0 deletions
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml new file mode 100644 index 00000000..f9ab75ce --- /dev/null +++ b/pretyping/evardefine.ml @@ -0,0 +1,207 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Util +open Pp +open Names +open Term +open Vars +open Termops +open Namegen +open Environ +open Evd +open Evarutil +open Pretype_errors +open Sigma.Notations + +let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal typ = + let evd = Sigma.Unsafe.of_evar_map evd in + let Sigma (evk, evd, _) = new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ in + (Sigma.to_evar_map evd, evk) + +let env_nf_evar sigma env = + let open Context.Rel.Declaration in + process_rel_context + (fun d e -> push_rel (map_constr (nf_evar sigma) d) e) env + +let env_nf_betaiotaevar sigma env = + let open Context.Rel.Declaration in + process_rel_context + (fun d e -> + push_rel (map_constr (Reductionops.nf_betaiota sigma) d) e) env + +(****************************************) +(* Operations on value/type constraints *) +(****************************************) + +type type_constraint = types option + +type val_constraint = constr option + +(* Old comment... + * Basically, we have the following kind of constraints (in increasing + * strength order): + * (false,(None,None)) -> no constraint at all + * (true,(None,None)) -> we must build a judgement which _TYPE is a kind + * (_,(None,Some ty)) -> we must build a judgement which _TYPE is ty + * (_,(Some v,_)) -> we must build a judgement which _VAL is v + * Maybe a concrete datatype would be easier to understand. + * We differentiate (true,(None,None)) from (_,(None,Some Type)) + * because otherwise Case(s) would be misled, as in + * (n:nat) Case n of bool [_]nat end would infer the predicate Type instead + * of Set. + *) + +(* The empty type constraint *) +let empty_tycon = None + +(* Builds a type constraint *) +let mk_tycon ty = Some ty + +(* Constrains the value of a type *) +let empty_valcon = None + +(* Builds a value constraint *) +let mk_valcon c = Some c + +let idx = Namegen.default_dependent_ident + +(* Refining an evar to a product *) + +let define_pure_evar_as_product evd evk = + let open Context.Named.Declaration in + 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 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 + (Sigma.to_evar_map evd1, e) + in + let evd2,rng = + 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 + (* Impredicative product, conclusion must fall in [Prop]. *) + new_evar_unsafe newenv evd1 concl ~src ~filter + else + let status = univ_flexible_alg in + let evd3, (rng, srng) = + let evd1 = Sigma.Unsafe.of_evar_map evd1 in + let Sigma (e, evd3, _) = new_type_evar newenv evd1 status ~src ~filter in + (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 + evd3, rng + in + let prod = mkProd (Name id, dom, subst_var id rng) in + let evd3 = Evd.define evk prod evd2 in + evd3,prod + +(* Refine an applied evar to a product and returns its instantiation *) + +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 evrngargs = Array.cons (mkRel 1) (Array.map (lift 1) args) in + let evrng = mkEvar (fst (destEvar rng), evrngargs) in + evd,mkProd (na, evdom, evrng) + +(* Refine an evar with an abstraction + + I.e., solve x1..xq |- ?e:T(x1..xq) with e:=λy:A.?e'[x1..xq,y] where: + - either T(x1..xq) = πy:A(x1..xq).B(x1..xq,y) + or T(x1..xq) = ?d[x1..xq] and we define ?d := πy:?A.?B + with x1..xq |- ?A:Type and x1..xq,y |- ?B:Type + - x1..xq,y:A |- ?e':B +*) + +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 + | Prod (na,dom,rng) -> (evd,(na,dom,rng)) + | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd typ + | _ -> error_not_product_loc Loc.ghost env evd typ in + let avoid = ids_of_named_context (evar_context evi) in + let id = + next_name_away_with_default_using_types "x" na avoid (Reductionops.whd_evar evd dom) in + let newenv = push_named (LocalAssum (id, dom)) evenv in + let filter = Filter.extend 1 (evar_filter evi) in + 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 + +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 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 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 + evar_absorb_arguments env evd (evk, Array.cons a args) l + +(* Refining an evar to a sort *) + +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 + +(* Propagation of constraints through application and abstraction: + Given a type constraint on a functional term, returns the type + constraint on its domain and codomain. If the input constraint is + an evar instantiate it with the product of 2 new evars. *) + +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 + | 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 + evd',(Anonymous, dom, rng) + | App (c,args) when isEvar c -> + let (evd',lam) = define_evar_as_lambda env evd (destEvar c) in + real_split evd' (mkApp (lam,args)) + | _ -> error_not_product_loc loc env evd c + in + match tycon with + | None -> evd,(Anonymous,None,None) + | Some c -> + let evd', (n, dom, rng) = real_split evd c in + evd', (n, mk_tycon dom, mk_tycon rng) + +let valcon_of_tycon x = x +let lift_tycon n = Option.map (lift n) + +let pr_tycon env = function + None -> str "None" + | Some t -> Termops.print_constr_env env t |