summaryrefslogtreecommitdiff
path: root/pretyping/evardefine.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2016-12-27 16:53:30 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2016-12-27 16:53:30 +0100
commita4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch)
tree26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /pretyping/evardefine.ml
parent164c6861860e6b52818c031f901ffeff91fca16a (diff)
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'pretyping/evardefine.ml')
-rw-r--r--pretyping/evardefine.ml207
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