aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authormsozeau2006-04-07 15:08:12 +0000
committermsozeau2006-04-07 15:08:12 +0000
commit26ca22424b286f5ff22a1fa97c38d15e224b3dc2 (patch)
tree190e12acf505e47d3a81ef0fd625a405ff782c04
parent5f9b04da0f3c72f4b582cd094edae721b1bc9a9e (diff)
- Documentation of the Program tactics.
- Fixes to the subtac implementation, utility tactic to apply existentials to a function and build a dependent sum out of name, constr lists. Also defined a Utils coq module for tactics related to subsets and the projections for ex in Prop. - Enhancements to inference algorithm added but not used in the default version as there are some remaining bugs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8688 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat
-rw-r--r--Makefile2
-rw-r--r--contrib/subtac/FixSub.v10
-rw-r--r--contrib/subtac/Utils.v22
-rw-r--r--contrib/subtac/eterm.ml64
-rw-r--r--contrib/subtac/eterm.mli9
-rw-r--r--contrib/subtac/g_subtac.ml419
-rw-r--r--contrib/subtac/subtac.ml1
-rw-r--r--contrib/subtac/subtac_coercion.ml312
-rw-r--r--contrib/subtac/subtac_command.ml330
-rw-r--r--contrib/subtac/subtac_command.mli10
-rw-r--r--contrib/subtac/subtac_interp_fixpoint.ml49
-rw-r--r--contrib/subtac/subtac_interp_fixpoint.mli4
-rw-r--r--contrib/subtac/subtac_pretyping.ml3
-rw-r--r--contrib/subtac/subtac_utils.ml119
-rw-r--r--contrib/subtac/subtac_utils.mli23
-rw-r--r--contrib/xml/xmlcommand.ml1
-rw-r--r--doc/Makefile2
-rw-r--r--doc/refman/Program.tex491
-rw-r--r--doc/refman/Reference-Manual.tex2
-rw-r--r--interp/coqlib.ml7
-rw-r--r--interp/coqlib.mli2
-rw-r--r--pretyping/cases.ml114
-rw-r--r--pretyping/clenv.ml2
-rw-r--r--pretyping/coercion.ml175
-rw-r--r--pretyping/coercion.mli10
-rw-r--r--pretyping/evarutil.ml82
-rw-r--r--pretyping/evarutil.mli30
-rw-r--r--pretyping/evd.ml7
-rw-r--r--pretyping/evd.mli1
-rw-r--r--pretyping/pretype_errors.ml3
-rw-r--r--pretyping/pretype_errors.mli2
-rw-r--r--pretyping/pretyping.ml104
-rw-r--r--pretyping/pretyping.mli5
33 files changed, 1575 insertions, 442 deletions
diff --git a/Makefile b/Makefile
index 1cd605a35b..2a70f129f5 100644
--- a/Makefile
+++ b/Makefile
@@ -1014,7 +1014,7 @@ JPROVERVO=
CCVO=
-SUBTACVO=contrib/subtac/FixSub.vo
+SUBTACVO=contrib/subtac/FixSub.vo contrib/subtac/Utils.vo
RTAUTOVO = \
contrib/rtauto/Bintree.vo contrib/rtauto/Rtauto.vo
diff --git a/contrib/subtac/FixSub.v b/contrib/subtac/FixSub.v
index 6face72d11..a9a22ca76e 100644
--- a/contrib/subtac/FixSub.v
+++ b/contrib/subtac/FixSub.v
@@ -21,8 +21,10 @@ End FixPoint.
End Well_founded.
-(*Check Fix_sub.*)
-
Notation "'forall' { x : A | P } , Q" :=
- (forall x:{x:A|P}, (fun x => Q) (proj1_sig x))
- (at level 200, x ident, right associativity). \ No newline at end of file
+ (forall x:{x:A|P}, Q)
+ (at level 200, x ident, right associativity).
+
+Notation "'fun' { x : A | P } => Q" :=
+ (fun x:{x:A|P} => Q)
+ (at level 200, x ident, right associativity).
diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v
new file mode 100644
index 0000000000..ceb8279fc2
--- /dev/null
+++ b/contrib/subtac/Utils.v
@@ -0,0 +1,22 @@
+Set Implicit Arguments.
+Lemma subset_simpl : forall (A : Set) (P : A -> Prop)
+ (t : sig P), P (proj1_sig t).
+Proof.
+intros.
+induction t.
+ simpl ; auto.
+Qed.
+
+Definition ex_pi1 (A : Prop) (P : A -> Prop) (t : ex P) : A.
+intros.
+induction t.
+exact x.
+Defined.
+
+Lemma ex_pi2 : forall (A : Prop) (P : A -> Prop) (t : ex P),
+ P (ex_pi1 t).
+intros A P.
+dependent inversion t.
+simpl.
+exact p.
+Defined.
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index ced1756f13..5703c0efc1 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -10,10 +10,14 @@ open Names
open Evd
open List
open Pp
+open Util
let reverse_array arr =
Array.of_list (List.rev (Array.to_list arr))
+let trace s =
+ if !Options.debug then msgnl s
+ else ()
(** Utilities to find indices in lists *)
let list_index x l =
@@ -37,14 +41,14 @@ let subst_evars evs n t =
| [] -> raise Not_found
in
let (idx, hyps, v) = aux 0 evs in
- idx + 1, hyps
+ n + idx + 1, hyps
in
let rec substrec depth c = match kind_of_term c with
| Evar (k, args) ->
(try
let index, hyps = evar_info k in
- msgnl (str "Evar " ++ int k ++ str " found, applied to " ++ int (Array.length args) ++ str "arguments," ++
- int (List.length hyps) ++ str " hypotheses");
+ trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (Array.length args) ++ str "arguments," ++
+ int (List.length hyps) ++ str " hypotheses");
let ex = mkRel (index + depth) in
(* Evar arguments are created in inverse order,
@@ -63,8 +67,7 @@ let subst_evars evs n t =
in
mkApp (ex, Array.of_list args)
with Not_found ->
- msgnl (str "Evar " ++ int k ++ str " not found!!!");
- c)
+ anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found"))
| _ -> map_constr_with_binders succ substrec depth c
in
substrec 0 t
@@ -100,29 +103,33 @@ let etype_of_evar evs ev hyps =
open Tacticals
-let eterm evm t =
+let eterm_term evm t tycon =
(* 'Serialize' the evars, we assume that the types of the existentials
refer to previous existentials in the list only *)
let evl = to_list evm in
let evts =
(* Remove existential variables in types and build the corresponding products *)
- fold_left
- (fun l (id, ev) ->
+ fold_right
+ (fun (id, ev) l ->
let hyps = Environ.named_context_of_val ev.evar_hyps in
let y' = (id, hyps, etype_of_evar l ev hyps) in
y' :: l)
- [] evl
+ evl []
in
let t' = (* Substitute evar refs in the term by De Bruijn indices *)
subst_evars evts 0 t
in
- let t'' =
- (* Make the lambdas 'generalizing' the existential variables *)
- fold_left
- (fun acc (id, _, c) ->
- mkLambda (Name (id_of_string ("Evar" ^ string_of_int id)),
- c, acc))
- t' evts
+ let evar_names =
+ List.map (fun (id, _, c) -> (id_of_string ("Evar" ^ string_of_int id)), c) evts
+ in
+ let evar_bl =
+ List.map (fun (id, c) -> Name id, None, c) evar_names
+ in
+ let anon_evar_bl = List.map (fun (_, x, y) -> (Anonymous, x, y)) evar_bl in
+ (* Generalize over the existential variables *)
+ let t'' = Termops.it_mkLambda_or_LetIn t' evar_bl
+ and tycon = option_app
+ (fun typ -> Termops.it_mkProd_wo_LetIn typ anon_evar_bl) tycon
in
let _declare_evar (id, c) =
let id = id_of_string ("Evar" ^ string_of_int id) in
@@ -133,12 +140,29 @@ let eterm evm t =
let id = id_of_string ("Evar" ^ string_of_int id) in
tclTHEN acc (Tactics.assert_tac false (Name id) c)
in
- msgnl (str "Term given to eterm" ++ spc () ++
+ trace (str "Term given to eterm" ++ spc () ++
Termops.print_constr_env (Global.env ()) t);
- msgnl (str "Term constructed in eterm" ++ spc () ++
+ trace (str "Term constructed in eterm" ++ spc () ++
Termops.print_constr_env (Global.env ()) t'');
- Tactics.apply_term t'' (List.map (fun _ -> Evarutil.mk_new_meta ()) evts)
+ ignore(option_app
+ (fun typ ->
+ trace (str "Type :" ++ spc () ++
+ Termops.print_constr_env (Global.env ()) typ))
+ tycon);
+ t'', tycon, evar_names
+
+let mkMetas n =
+ let rec aux i acc =
+ if i > 0 then aux (pred i) (Evarutil.mk_new_meta () :: acc)
+ else acc
+ in aux n []
+
+let eterm evm t (tycon : types option) =
+ let t, tycon, evs = eterm_term evm t tycon in
+ match tycon with
+ Some typ -> Tactics.apply_term (mkCast (t, DEFAULTcast, typ)) []
+ | None -> Tactics.apply_term t (mkMetas (List.length evs))
open Tacmach
-let etermtac (evm, t) = eterm evm t
+let etermtac (evm, t) = eterm evm t None
diff --git a/contrib/subtac/eterm.mli b/contrib/subtac/eterm.mli
index bcb9b4c56d..d6f058ebda 100644
--- a/contrib/subtac/eterm.mli
+++ b/contrib/subtac/eterm.mli
@@ -9,5 +9,12 @@
(*i $Id$ i*)
open Tacmach
+open Term
+open Evd
+open Names
-val etermtac : Evd.open_constr -> tactic
+val mkMetas : int -> constr list
+
+val eterm_term : evar_map -> constr -> types option -> constr * types option * (identifier * types) list
+
+val etermtac : open_constr -> tactic
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index d9c7a8c023..2f47608c10 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -49,13 +49,6 @@ GEXTEND Gram
;
END
-(* type wf_proof_type_argtype = (Subtac_utils.wf_proof_type, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type *)
-
-(* let (wit_subtac_wf_proof_type : wf_proof_type_argtype), *)
-(* (globwit_subtac_wf_proof_type : wf_proof_type_argtype), *)
-(* (rawwit_subtac_wf_proof_type : wf_proof_type_argtype) = *)
-(* Genarg.create_arg "subtac_wf_proof_type" *)
-
type gallina_loc_argtype = (Vernacexpr.vernac_expr located, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type
let (wit_subtac_gallina_loc : gallina_loc_argtype),
@@ -63,18 +56,6 @@ let (wit_subtac_gallina_loc : gallina_loc_argtype),
(rawwit_subtac_gallina_loc : gallina_loc_argtype) =
Genarg.create_arg "subtac_gallina_loc"
-(* type subtac_recdef_argtype = (Subtac_utils.recursion_order option, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type *)
-
-(* let (wit_subtac_recdef : subtac_recdef_argtype), *)
-(* (globwit_subtac_recdef : subtac_recdef_argtype), *)
-(* (rawwit_subtac_recdef : subtac_recdef_argtype) = *)
-(* Genarg.create_arg "subtac_recdef" *)
-
-(* VERNAC COMMAND EXTEND SubtacRec *)
-(* [ "Recursive" "program" ident(id) subtac_binders(l) subtac_recdef(f) ] -> *)
-(* [ Interp.subtac id l Environ.empty_env f ] *)
-(* END *)
-
VERNAC COMMAND EXTEND Subtac
[ "Program" subtac_gallina_loc(g) ] ->
[ Subtac.subtac g ]
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index 01c959a47d..8b59b7eff5 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -119,6 +119,7 @@ let subtac (loc, command) =
check_required_library ["Coq";"Init";"Datatypes"];
check_required_library ["Coq";"Init";"Specif"];
require_library "Coq.subtac.FixSub";
+ require_library "Coq.subtac.Utils";
try
match command with
VernacDefinition (defkind, (locid, id), expr, hook) ->
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index c605314018..4b4a25e718 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -35,7 +35,7 @@ let make_name s = Name (id_of_string s)
module Coercion = struct
- exception NoCoercion
+ exception NoSubtacCoercion
let rec disc_subset x =
match kind_of_term x with
@@ -86,6 +86,8 @@ module Coercion = struct
| Type _, Prop Null -> Prop Null
| _, Type _ -> s2
+ let hnf env isevars c = whd_betadeltaiota env (evars_of !isevars) c
+
let rec mu env isevars t =
let rec aux v =
match disc_subset v with
@@ -101,17 +103,22 @@ module Coercion = struct
and coerce loc env isevars (x : Term.constr) (y : Term.constr)
: (Term.constr -> Term.constr) option
=
- trace (str "Coerce called for " ++ (my_print_constr env x) ++
- str " and "++ my_print_constr env y);
-
+ let x = nf_evar (evars_of !isevars) x and y = nf_evar (evars_of !isevars) y in
+ trace (str "Coerce called for " ++ (my_print_constr env x) ++
+ str " and "++ my_print_constr env y ++
+ str " with evars: " ++ spc () ++
+ my_print_evardefs !isevars);
let rec coerce_unify env x y =
- if e_cumul env isevars x y then (
+ trace (str "coerce_unify from " ++ (my_print_constr env x) ++
+ str " to "++ my_print_constr env y);
+ try
+ isevars := the_conv_x_leq env x y !isevars;
trace (str "Unified " ++ (my_print_constr env x) ++
- str " and "++ my_print_constr env y);
+ str " and "++ my_print_constr env y);
None
- ) else coerce' env x y (* head recutions needed *)
+ with Reduction.NotConvertible -> coerce' env (hnf env isevars x) (hnf env isevars y)
and coerce' env x y : (Term.constr -> Term.constr) option =
- let subco () = subset_coerce env x y in
+ let subco () = subset_coerce env isevars x y in
trace (str "coerce' from " ++ (my_print_constr env x) ++
str " to "++ my_print_constr env y);
match (kind_of_term x, kind_of_term y) with
@@ -137,43 +144,78 @@ module Coercion = struct
| App (c, l), App (c', l') ->
(match kind_of_term c, kind_of_term c' with
- Ind i, Ind i' ->
+ Ind i, Ind i' -> (* Sigma types *)
let len = Array.length l in
let existS = Lazy.force existS in
- if len = Array.length l' && len = 2
- && i = i' && i = Term.destInd existS.typ
- then
- begin (* Sigma types *)
- debug 1 (str "In coerce sigma types");
- let (a, pb), (a', pb') =
- pair_of_array l, pair_of_array l'
- in
- let c1 = coerce_unify env a a' in
- let remove_head c =
- let (_, _, x) = Term.destProd c in
- x
- in
- let b, b' = remove_head pb, remove_head pb' in
- let env' = push_rel (make_name "x", None, a) env in
- let c2 = coerce_unify env' b b' in
- match c1, c2 with
- None, None -> None
- | _, _ ->
- Some
- (fun x ->
- let x, y =
- app_opt c1 (mkApp (existS.proj1,
- [| a; pb; x |])),
- app_opt c2 (mkApp (existS.proj2,
- [| a; pb'; x |]))
- in
- mkApp (existS.intro, [| x ; y |]))
- end
+ let prod = Lazy.force prod in
+ if len = Array.length l' && len = 2 && i = i'
+ then
+ if i = Term.destInd existS.typ
+ then
+ begin
+ debug 1 (str "In coerce sigma types");
+ let (a, pb), (a', pb') =
+ pair_of_array l, pair_of_array l'
+ in
+ let c1 = coerce_unify env a a' in
+ let rec remove_head a c =
+ match kind_of_term c with
+ | Lambda (n, t, t') -> c, t'
+ (*| Prod (n, t, t') -> t'*)
+ | Evar (k, args) ->
+ let (evs, t) = Evarutil.define_evar_as_lambda !isevars (k,args) in
+ isevars := evs;
+ let (n, dom, rng) = destLambda t in
+ let (domk, args) = destEvar dom in
+ isevars := evar_define domk a !isevars;
+ t, rng
+ | _ -> raise NoSubtacCoercion
+ in
+ let (pb, b), (pb', b') = remove_head a pb, remove_head a' pb' in
+ let env' = push_rel (make_name "x", None, a) env in
+ let c2 = coerce_unify env' b b' in
+ match c1, c2 with
+ None, None ->
+ trace (str "No coercion needed");
+ None
+ | _, _ ->
+ Some
+ (fun x ->
+ let x, y =
+ app_opt c1 (mkApp (existS.proj1,
+ [| a; pb; x |])),
+ app_opt c2 (mkApp (existS.proj2,
+ [| a; pb; x |]))
+ in
+ mkApp (existS.intro, [| a'; pb'; x ; y |]))
+ end
+ else if i = Term.destInd prod.typ then
+ begin
+ debug 1 (str "In coerce prod types");
+ let (a, b), (a', b') =
+ pair_of_array l, pair_of_array l'
+ in
+ let c1 = coerce_unify env a a' in
+ let c2 = coerce_unify env b b' in
+ match c1, c2 with
+ None, None -> None
+ | _, _ ->
+ Some
+ (fun x ->
+ let x, y =
+ app_opt c1 (mkApp (prod.proj1,
+ [| a; b; x |])),
+ app_opt c2 (mkApp (prod.proj2,
+ [| a; b; x |]))
+ in
+ mkApp (prod.intro, [| a'; b'; x ; y |]))
+ end
+ else subco ()
else subco ()
| _ -> subco ())
| _, _ -> subco ()
- and subset_coerce env x y =
+ and subset_coerce env isevars x y =
match disc_subset x with
Some (u, p) ->
let c = coerce_unify env u y in
@@ -193,15 +235,16 @@ module Coercion = struct
(mkApp
((Lazy.force sig_).intro,
[| u; p; cx; evar |])))
- | None -> raise NoCoercion
+ | None ->
+ raise NoSubtacCoercion
+ (*isevars := Evd.add_conv_pb (Reduction.CONV, x, y) !isevars;
+ None*)
in coerce_unify env x y
- let coerce_itf loc env isevars hj c1 =
- let {uj_val = v; uj_type = t} = hj in
+ let coerce_itf loc env isevars v t c1 =
let evars = ref isevars in
let coercion = coerce loc env evars t c1 in
- !evars, {uj_val = app_opt coercion v;
- uj_type = t}
+ !evars, option_app (app_opt coercion) v, t
(* Taken from pretyping/coercion.ml *)
@@ -224,9 +267,8 @@ module Coercion = struct
in
apply_rec [] funj.uj_type argl
- exception NoCoercion
-
(* appliquer le chemin de coercions de patterns p *)
+ exception NoCoercion
let apply_pattern_coercion loc pat p =
List.fold_left
@@ -275,7 +317,7 @@ module Coercion = struct
try
let coercef, t = mu env isevars t in
(isevars, { uj_val = app_opt coercef j.uj_val; uj_type = t })
- with NoCoercion ->
+ with NoSubtacCoercion | NoCoercion ->
(isevars,j))
let inh_tosort_force loc env isevars j =
@@ -297,79 +339,141 @@ module Coercion = struct
| _ ->
inh_tosort_force loc env isevars j
- let inh_coerce_to_fail env isevars c1 hj =
- let hj' =
+ let inh_coerce_to_fail env isevars c1 v t =
+ let v', t' =
try
let t1,i1 = class_of1 env (evars_of isevars) c1 in
- let t2,i2 = class_of1 env (evars_of isevars) hj.uj_type in
+ let t2,i2 = class_of1 env (evars_of isevars) t in
let p = lookup_path_between (i2,i1) in
- apply_coercion env p hj t2
+ match v with
+ Some v ->
+ let j = apply_coercion env p {uj_val = v; uj_type = t} t2 in
+ Some j.uj_val, j.uj_type
+ | None -> None, t
with Not_found -> raise NoCoercion
in
- try (the_conv_x_leq env hj'.uj_type c1 isevars, hj')
+ try (the_conv_x_leq env t' c1 isevars, v', t')
with Reduction.NotConvertible -> raise NoCoercion
- let rec inh_conv_coerce_to_fail env isevars hj c1 =
- let {uj_val = v; uj_type = t} = hj in
- try (the_conv_x_leq env t c1 isevars, hj)
- with Reduction.NotConvertible ->
- (try
- inh_coerce_to_fail env isevars c1 hj
+ let rec inh_conv_coerce_to_fail loc env isevars v t c1 =
+ (try
+ trace (str "inh_conv_coerce_to_fail called for " ++
+ Termops.print_constr_env env t ++ str " and "++ spc () ++
+ Termops.print_constr_env env c1 ++ str " with evars: " ++ spc () ++
+ Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
+ Termops.print_env env);
+ with _ -> ());
+ try (the_conv_x_leq env t c1 isevars, v, t)
+ with Reduction.NotConvertible ->
+ (try
+ inh_coerce_to_fail env isevars c1 v t
with NoCoercion ->
(match kind_of_term (whd_betadeltaiota env (evars_of isevars) t),
kind_of_term (whd_betadeltaiota env (evars_of isevars) c1) with
| Prod (_,t1,t2), Prod (name,u1,u2) ->
- let v' = whd_betadeltaiota env (evars_of isevars) v in
+ let v' = option_app (whd_betadeltaiota env (evars_of isevars)) v in
let (evd',b) =
- match kind_of_term v' with
- | Lambda (_,v1,v2) ->
- (try the_conv_x env v1 u1 isevars, true (* leq v1 u1? *)
- with Reduction.NotConvertible -> (isevars, false))
- | _ -> (isevars,false) in
- if b
- then
- let (x,v1,v2) = destLambda v' in
- let env1 = push_rel (x,None,v1) env in
- let (evd'',h2) = inh_conv_coerce_to_fail env1 evd'
- {uj_val = v2; uj_type = t2 } u2 in
- (evd'',{ uj_val = mkLambda (x, v1, h2.uj_val);
- uj_type = mkProd (x, v1, h2.uj_type) })
- else
- (* Mismatch on t1 and u1 or not a lambda: we eta-expand *)
- (* we look for a coercion c:u1->t1 s.t. [name:u1](v' (c x)) *)
- (* has type (name:u1)u2 (with v' recursively obtained) *)
- let name = (match name with
- | Anonymous -> Name (id_of_string "x")
- | _ -> name) in
- let env1 = push_rel (name,None,u1) env in
- let (evd',h1) =
- inh_conv_coerce_to_fail env1 isevars
- {uj_val = mkRel 1; uj_type = (lift 1 u1) }
- (lift 1 t1) in
- let (evd'',h2) = inh_conv_coerce_to_fail env1 evd'
- { uj_val = mkApp (lift 1 v, [|h1.uj_val|]);
- uj_type = subst1 h1.uj_val t2 }
- u2
- in
- (evd'',
- { uj_val = mkLambda (name, u1, h2.uj_val);
- uj_type = mkProd (name, u1, h2.uj_type) })
+ match v' with
+ Some v' ->
+ (match kind_of_term v' with
+ | Lambda (x,v1,v2) ->
+ (try the_conv_x env v1 u1 isevars, Some (x, v1, v2) (* leq v1 u1? *)
+ with Reduction.NotConvertible -> (isevars, None))
+ | _ -> (isevars, None))
+ | None -> (isevars, None)
+ in
+ (match b with
+ Some (x, v1, v2) ->
+ let env1 = push_rel (x,None,v1) env in
+ let (evd'', v2', t2') = inh_conv_coerce_to_fail loc env1 evd'
+ (Some v2) t2 u2 in
+ (evd'', option_app (fun v2' -> mkLambda (x, v1, v2')) v2',
+ mkProd (x, v1, t2'))
+ | None ->
+ (* Mismatch on t1 and u1 or not a lambda: we eta-expand *)
+ (* we look for a coercion c:u1->t1 s.t. [name:u1](v' (c x)) *)
+ (* has type (name:u1)u2 (with v' recursively obtained) *)
+ let name = (match name with
+ | Anonymous -> Name (id_of_string "x")
+ | _ -> name) in
+ let env1 = push_rel (name,None,u1) env in
+ let (evd', v1', t1') =
+ inh_conv_coerce_to_fail loc env1 isevars
+ (Some (mkRel 1)) (lift 1 u1) (lift 1 t1)
+ in
+ let (evd'', v2', t2') =
+ let v2 =
+ match v with
+ Some v -> option_app (fun v1' -> mkApp (lift 1 v, [|v1'|])) v1'
+ | None -> None
+ and evd', t2 =
+ match v1' with
+ Some v1' -> evd', subst1 v1' t2
+ | None ->
+ let evd', ev = new_evar evd' env ~src:(loc, InternalHole) t1' in
+ evd', subst1 ev t2
+ in
+ inh_conv_coerce_to_fail loc env1 evd' v2 t2 u2
+ in
+ (evd'', option_app (fun v2' -> mkLambda (name, u1, v2')) v2',
+ mkProd (name, u1, t2')))
| _ -> raise NoCoercion))
+
(* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
- let inh_conv_coerce_to loc env isevars cj t =
- trace (str "inh_conv_coerce_to called for " ++ (my_print_constr env cj.uj_type) ++
- str " and "++ my_print_constr env t);
- let (evd',cj') =
- try
- inh_conv_coerce_to_fail env isevars cj t
- with NoCoercion ->
- try
- coerce_itf loc env isevars cj t
+ let inh_conv_coerce_to loc env isevars cj ((n, t) as tycon) =
+ (try
+ trace (str "inh_conv_coerce_to called for " ++
+ Termops.print_constr_env env cj.uj_type ++ str " and "++ spc () ++
+ Evarutil.pr_tycon_type env tycon ++ str " with evars: " ++ spc () ++
+ Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
+ Termops.print_env env);
+ with _ -> ());
+ if n = 0 then
+ let (evd', val', type') =
+ try
+ inh_conv_coerce_to_fail loc env isevars (Some cj.uj_val) cj.uj_type t
with NoCoercion ->
let sigma = evars_of isevars in
- debug 2 (str "No coercion found");
- error_actual_type_loc loc env sigma cj t
+ try
+ coerce_itf loc env isevars (Some cj.uj_val) cj.uj_type t
+ with NoSubtacCoercion ->
+ error_actual_type_loc loc env sigma cj t
+ in
+ let val' = match val' with Some v -> v | None -> assert(false) in
+ (evd',{ uj_val = val'; uj_type = t })
+ else
+ (isevars, cj)
+
+ let inh_conv_coerces_to loc env isevars t ((abs, t') as tycon) =
+ (try
+ trace (str "inh_conv_coerces_to called for " ++
+ Termops.print_constr_env env t ++ str " and "++ spc () ++
+ Evarutil.pr_tycon_type env tycon ++ str " with evars: " ++ spc () ++
+ Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
+ Termops.print_env env);
+ with _ -> ());
+ let (rels, rng) =
+ (* a little more effort to get products is needed *)
+ try decompose_prod_n abs t
+ with _ ->
+ trace (str "decompose_prod_n failed");
+ raise (Invalid_argument "Subtac_coercion.inh_conv_coerces_to")
in
- (evd',{ uj_val = cj'.uj_val; uj_type = t })
+ (* The final range free variables must have been replaced by evars, we accept only that evars
+ in rng are applied to free vars. *)
+ if noccur_with_meta 0 (succ abs) rng then (
+ trace (str "No occur between 0 and " ++ int (succ abs));
+ let env', t, t' =
+ let env' = List.fold_right (fun (n, t) env -> push_rel (n, None, t) env) rels env in
+ env', rng, lift abs t'
+ in
+ try
+ pi1 (try inh_conv_coerce_to_fail loc env' isevars None t t'
+ with NoCoercion ->
+ coerce_itf loc env' isevars None t t')
+ with NoSubtacCoercion ->
+ let sigma = evars_of isevars in
+ error_cannot_coerce env' sigma (t, t'))
+ else isevars
end
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 5659950bc9..94f2d70ac4 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -1,4 +1,3 @@
-
open Closure
open RedFlags
open Declarations
@@ -34,7 +33,9 @@ open Mod_subst
open Printer
open Inductiveops
open Syntax_def
-
+open Environ
+open Tactics
+open Tacticals
open Tacinterp
open Vernacexpr
open Notation
@@ -46,13 +47,17 @@ open Pretyping
(*********************************************************************)
(* Functions to parse and interpret constructions *)
+let evar_nf isevars c =
+ isevars := Evarutil.nf_evar_defs !isevars;
+ Evarutil.nf_isevar !isevars c
+
let interp_gen kind isevars env
?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[]))
c =
let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_soapp ~ltacvars (Evd.evars_of !isevars) env c in
let c' = Subtac_interp_fixpoint.rewrite_cases env c' in
let c' = SPretyping.pretype_gen isevars env ([],[]) kind c' in
- non_instanciated_map env isevars, c'
+ evar_nf isevars c'
let interp_constr isevars env c =
interp_gen (OfType None) isevars env c
@@ -64,14 +69,47 @@ let interp_casted_constr isevars env ?(impls=([],[])) c typ =
interp_gen (OfType (Some typ)) isevars env ~impls c
let interp_open_constr isevars env c =
- SPretyping.pretype_gen isevars env ([], []) (OfType None)
- (Constrintern.intern_constr (Evd.evars_of !isevars) env c)
+ let c = SPretyping.pretype_gen isevars env ([], []) (OfType None)
+ (Constrintern.intern_constr (Evd.evars_of !isevars) env c) in
+ evar_nf isevars c
let interp_constr_judgment isevars env c =
- let s, j = SPretyping.understand_judgment_tcc (Evd.evars_of !isevars) env
- (Constrintern.intern_constr (Evd.evars_of !isevars) env c)
- in
- Evd.create_evar_defs s, j
+ let j =
+ SPretyping.understand_judgment_tcc isevars env
+ (Constrintern.intern_constr (Evd.evars_of !isevars) env c)
+ in
+ { uj_val = evar_nf isevars j.uj_val; uj_type = evar_nf isevars j.uj_type }
+
+let locate_if_isevar loc na = function
+ | RHole _ ->
+ (try match na with
+ | Name id -> Reserve.find_reserved_type id
+ | Anonymous -> raise Not_found
+ with Not_found -> RHole (loc, Evd.BinderType na))
+ | x -> x
+
+let interp_binder sigma env na t =
+ let t = Constrintern.intern_gen true (Evd.evars_of !sigma) env t in
+ SPretyping.understand_type (Evd.evars_of !sigma) env (locate_if_isevar (loc_of_rawconstr t) na t)
+
+
+let interp_context sigma env params =
+ List.fold_left
+ (fun (env,params) d -> match d with
+ | LocalRawAssum ([_,na],(CHole _ as t)) ->
+ let t = interp_binder sigma env na t in
+ let d = (na,None,t) in
+ (push_rel d env, d::params)
+ | LocalRawAssum (nal,t) ->
+ let t = interp_type sigma env t in
+ let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in
+ let ctx = List.rev ctx in
+ (push_rel_context ctx env, ctx@params)
+ | LocalRawDef ((_,na),c) ->
+ let c = interp_constr_judgment sigma env c in
+ let d = (na, Some c.uj_val, c.uj_type) in
+ (push_rel d env,d::params))
+ (env,[]) params
(* try to find non recursive definitions *)
@@ -85,7 +123,7 @@ let collect_non_rec env =
let i =
list_try_find_i
(fun i f ->
- if List.for_all (fun (_, def) -> not (occur_var env f def)) ldefrec
+ if List.for_all (fun (_, _, def) -> not (occur_var env f def)) ldefrec
then i else failwith "try_find_i")
0 lnamerec
in
@@ -108,6 +146,9 @@ let collect_non_rec env =
in
searchrec []
+let definition_message id =
+ Options.if_verbose message ((string_of_id id) ^ " is defined")
+
let recursive_message v =
match Array.length v with
| 0 -> error "no recursive definition"
@@ -115,13 +156,27 @@ let recursive_message v =
| _ -> hov 0 (prvect_with_sep pr_coma Printer.pr_global v ++
spc () ++ str "are recursively defined")
+let filter_map f l =
+ let rec aux acc = function
+ hd :: tl -> (match f hd with Some t -> aux (t :: acc) tl
+ | None -> aux acc tl)
+ | [] -> List.rev acc
+ in aux [] l
+
+let list_of_local_binders l =
+ let rec aux acc = function
+ Topconstr.LocalRawDef (n, c) :: tl -> aux ((n, Some c, None) :: acc) tl
+ | Topconstr.LocalRawAssum (nl, c) :: tl ->
+ aux (List.fold_left (fun acc n -> (n, None, Some c) :: acc) acc nl) tl
+ | [] -> List.rev acc
+ in aux [] l
+
let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed =
let sigma = Evd.empty
and env0 = Global.env()
- and protos = List.map (fun ((f, n, _, _, _),_) -> f,n) lnameargsardef
in
- let lnameargsardef =
- List.map (fun (f, d) -> Subtac_interp_fixpoint.rewrite_fixpoint env0 protos (f, d))
+ let lnameargsardef =
+ (*List.map (fun (f, d) -> Subtac_interp_fixpoint.rewrite_fixpoint env0 protos (f, d))*)
lnameargsardef
in
let lrecnames = List.map (fun ((f,_,_,_,_),_) -> f) lnameargsardef
@@ -130,16 +185,56 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
(* Build the recursive context and notations for the recursive types *)
let (rec_sign,rec_impls,arityl) =
List.fold_left
- (fun (env,impls,arl) ((recname,_,bl,arityc,_),_) ->
- let arityc = Command.generalize_constr_expr arityc bl in
- let isevars = ref (Evd.create_evar_defs sigma) in
- let isevars, arity = interp_type isevars env0 arityc in
- let impl =
- if Impargs.is_implicit_args()
- then Impargs.compute_implicits env0 arity
- else [] in
- let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in
- (Environ.push_named (recname,None,arity) env, impls', (isevars, arity)::arl))
+ (fun (env,impls,arl) ((recname,(n, ro),bl,arityc,body),_) ->
+ let isevars = ref (Evd.create_evar_defs sigma) in
+ match ro with
+ CStructRec ->
+ let arityc = Command.generalize_constr_expr arityc bl in
+ let arity = interp_type isevars env0 arityc in
+ let impl =
+ if Impargs.is_implicit_args()
+ then Impargs.compute_implicits env0 arity
+ else [] in
+ let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in
+ (Environ.push_named (recname,None,arity) env, impls', (isevars, None, arity)::arl)
+ | CWfRec r ->
+ let _ = trace (str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++
+ Ppconstr.pr_binders bl ++ str " : " ++
+ Ppconstr.pr_constr_expr arityc ++ str " := " ++ spc () ++
+ Ppconstr.pr_constr_expr body)
+ in
+ let env', binders_rel = interp_context isevars env0 bl in
+ let before, ((argname, _, argtyp) as arg), after = list_chop_hd n binders_rel in
+ let argid = match argname with Name n -> n | _ -> assert(false) in
+ let after' = List.map (fun (n, c, t) -> (n, option_app (lift 1) c, lift 1 t)) after in
+ let envwf = push_rel_context before env0 in
+ let wf_rel = interp_constr isevars envwf r in
+ let accarg_id = id_of_string ("Acc_" ^ string_of_id argid) in
+ let accarg = (Name accarg_id, None, mkApp (Lazy.force acc_inv, [| wf_rel; mkRel 1 |])) in
+ let argid' = id_of_string (string_of_id argid ^ "'") in
+ let before_length, after_length = List.length before, List.length after in
+ let full_length = before_length + 1 + after_length in
+ let wfarg = (Name argid, None,
+ mkSubset (Name argid') argtyp
+ (mkApp (wf_rel, [|mkRel 1; mkRel (full_length + 1)|])))
+ in
+ let new_bl = before @ (arg :: accarg :: after')
+ and intern_bl = before @ (wfarg :: after)
+ in
+ let intern_env = push_rel_context intern_bl env0 in
+ let env' = push_rel_context new_bl env0 in
+ let arity = interp_type isevars intern_env arityc in
+ let intern_arity = it_mkProd_or_LetIn arity intern_bl in
+ let arity' = interp_type isevars env' arityc in
+ let arity' = it_mkProd_or_LetIn arity' new_bl in
+ let fun_bl = before @ (arg :: (Name recname, None, arity) :: after') in
+ let impl =
+ if Impargs.is_implicit_args()
+ then Impargs.compute_implicits intern_env arity'
+ else [] in
+ let impls' = (recname,([],impl,compute_arguments_scope arity'))::impls in
+ (Environ.push_named (recname,None,arity') env, impls',
+ (isevars, Some (full_length - n, argtyp, wf_rel, fun_bl, intern_bl, intern_arity), arity')::arl))
(env0,[],[]) lnameargsardef in
let arityl = List.rev arityl in
let notations =
@@ -155,10 +250,17 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
List.iter (fun (df,c,scope) -> (* No scope for tmp notation *)
Metasyntax.add_notation_interpretation df rec_impls c None) notations;
List.map2
- (fun ((_,_,bl,_,def),_) (evm, arity) ->
- let def = abstract_constr_expr def bl in
- interp_casted_constr (ref (Evd.create_evar_defs evm)) rec_sign ~impls:([],rec_impls)
- def arity)
+ (fun ((_,_,bl,_,def),_) (isevars, info, arity) ->
+ match info with
+ None ->
+ let def = abstract_constr_expr def bl in
+ isevars, info, interp_casted_constr isevars rec_sign ~impls:([],rec_impls)
+ def arity
+ | Some (n, artyp, wfrel, bl, intern_bl, intern_arity) ->
+ let rec_sign = push_rel_context bl rec_sign in
+ let cstr = interp_casted_constr isevars rec_sign ~impls:([],rec_impls)
+ def intern_arity
+ in isevars, info, cstr)
lnameargsardef arityl
with e ->
States.unfreeze fs; raise e in
@@ -173,7 +275,8 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in
let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in
let rec declare i fi =
- trace (str "Declaring: " ++ pr_id fi);
+ trace (str "Declaring: " ++ pr_id fi ++ spc () ++
+ my_print_constr env0 (recvec.(i)));
let ce =
{ const_entry_body = mkFix ((nvrec',i),recdecls);
const_entry_type = Some arrec.(i);
@@ -185,76 +288,131 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
(* declare the recursive definitions *)
let lrefrec = Array.mapi declare namerec in
Options.if_verbose ppnl (recursive_message lrefrec);
- (* (* The others are declared as normal definitions *)
- let var_subst id = (id, Constrintern.global_reference id) in
- let _ =
- List.fold_left
+
+
+ (*(* The others are declared as normal definitions *)
+ let var_subst id = (id, Constrintern.global_reference id) in
+ let _ =
+ List.fold_left
(fun subst (f,def,t) ->
- let ce = { const_entry_body = replace_vars subst def;
- const_entry_type = Some t;
- const_entry_opaque = false;
- const_entry_boxed = boxed } in
- let _ =
- Declare.declare_constant f (DefinitionEntry ce,IsDefinition Definition)
- in
- warning ((string_of_id f)^" is non-recursively defined");
- (var_subst f) :: subst)
+ let ce = { const_entry_body = replace_vars subst def;
+ const_entry_type = Some t;
+ const_entry_opaque = false;
+ const_entry_boxed = boxed } in
+ let _ =
+ Declare.declare_constant f (DefinitionEntry ce,IsDefinition Definition)
+ in
+ warning ((string_of_id f)^" is non-recursively defined");
+ (var_subst f) :: subst)
(List.map var_subst (Array.to_list namerec))
lnonrec
- in*)
+ in*)
List.iter (fun (df,c,scope) ->
Metasyntax.add_notation_interpretation df [] c scope) notations
in
let declare l =
let recvec = Array.of_list l
- and arrec = Array.map snd arrec
+ and arrec = Array.map pi3 arrec
in declare arrec recvec
in
let recdefs = Array.length defrec in
trace (int recdefs ++ str " recursive definitions");
(* Solve remaining evars *)
- let rec solve_evars i acc =
+ let rec collect_evars i acc =
if i < recdefs then
- let (evm, def) = defrec.(i) in
- if Evd.dom evm = [] then
- solve_evars (succ i) (def :: acc)
- else
- let _,typ = arrec.(i) in
- let id = namerec.(i) in
- (* Generalize by the recursive prototypes *)
- let def =
- Termops.it_mkNamedLambda_or_LetIn def (Environ.named_context rec_sign)
- and typ =
- Termops.it_mkNamedProd_or_LetIn typ (Environ.named_context rec_sign) in
- let tac = Eterm.etermtac (evm, def) in
- let _ =
- trace (str "Starting proof of a fixpoint def:" ++ spc () ++ my_print_constr env0 def ++
- spc () ++ str " with goal: " ++ my_print_constr env0 typ ++
- spc () ++ str " with evar map = " ++ Evd.pr_evar_map evm)
- in
- begin
- Command.start_proof (id_of_string (string_of_id id ^ "_evars")) goal_kind typ
- (fun _ gr ->
- let _ = trace (str "Got a proof of: " ++ pr_global gr) in
- let constant = match gr with Libnames.ConstRef c -> c
- | _ -> assert(false)
- in
- try
- let def = Environ.constant_value (Global.env ()) constant in
- let _ = trace (str "Got constant value") in
- let _, c = decompose_lam_n recdefs def in
- let _ = trace (str "Fixpoint body is: " ++ spc () ++ my_print_constr (Global.env ()) c) in
- solve_evars (succ i) (c :: acc)
- with Environ.NotEvaluableConst cer ->
- match cer with
- Environ.NoBody -> trace (str "Constant has no body")
- | Environ.Opaque -> trace (str "Constant is opaque")
- );
- trace (str "Started proof");
- Pfedit.by tac;
- trace (str "Applied eterm tac");
- end
- else declare (List.rev acc)
- in solve_evars 0 []
+ let (isevars, info, def) = defrec.(i) in
+ let _ = trace (str "In solve evars, isevars is: " ++ Evd.pr_evar_defs !isevars) in
+ let def = evar_nf isevars def in
+ let isevars = Evd.undefined_evars !isevars in
+ let _ = trace (str "In solve evars, undefined is: " ++ Evd.pr_evar_defs isevars) in
+ let evm = Evd.evars_of isevars in
+ let _, _, typ = arrec.(i) in
+ let id = namerec.(i) in
+ let def =
+ match info with
+ Some (n, artyp, wfrel, funbl, bl, arity) ->
+ def (* mkApp (def, *)
-
+ | None -> def
+ in
+ (* Generalize by the recursive prototypes *)
+ let def =
+ Termops.it_mkNamedLambda_or_LetIn def (Environ.named_context rec_sign)
+ and typ =
+ Termops.it_mkNamedProd_or_LetIn typ (Environ.named_context rec_sign) in
+ let evars_def, evars_typ, evars = Eterm.eterm_term evm def (Some typ) in
+ (*let evars_typ = match evars_typ with Some t -> t | None -> assert(false) in*)
+ (*let fi = id_of_string (string_of_id id ^ "_evars") in*)
+ (*let ce =
+ { const_entry_body = evars_def;
+ const_entry_type = Some evars_typ;
+ const_entry_opaque = false;
+ const_entry_boxed = boxed} in
+ let kn = Declare.declare_constant fi (DefinitionEntry ce,IsDefinition Definition) in
+ definition_message fi;
+ trace (str (string_of_id fi) ++ str " is defined");*)
+ let evar_sum =
+ if evars = [] then None
+ else
+ let sum = Subtac_utils.build_dependent_sum evars in
+ trace (str "Evars sum: " ++ my_print_constr env0 (pi1 sum));
+ Some sum
+ in
+ collect_evars (succ i) ((id, evars_def, evar_sum) :: acc)
+ else acc
+ in
+ let defs = collect_evars 0 [] in
+
+ (* Solve evars then create the definitions *)
+ let real_evars =
+ filter_map (fun (id, kn, sum) ->
+ match sum with Some (sumg, sumtac, _) -> Some (id, kn, sumg, sumtac) | None -> None)
+ defs
+ in
+ Subtac_utils.and_tac real_evars
+ (fun f _ gr ->
+ let _ = trace (str "Got a proof of: " ++ pr_global gr) in
+ let constant = match gr with Libnames.ConstRef c -> c
+ | _ -> assert(false)
+ in
+ try
+ (*let value = Environ.constant_value (Global.env ()) constant in*)
+ let pis = f (mkConst constant) in
+ trace (str "Accessors: " ++
+ List.fold_right (fun (_, _, _, c) acc -> my_print_constr env0 c ++ spc () ++ acc)
+ pis (mt()));
+ trace (str "Applied existentials: " ++
+ (List.fold_right
+ (fun (id, kn, sumg, pi) acc ->
+ let args = Subtac_utils.destruct_ex pi sumg in
+ my_print_constr env0 (mkApp (kn, Array.of_list args)))
+ pis (mt ())));
+ let rec aux pis acc = function
+ (id, kn, sum) :: tl ->
+ (match sum with
+ None -> aux pis (kn :: acc) tl
+ | Some (sumg, _, _) ->
+ let (id, kn, sumg, pi), pis = List.hd pis, List.tl pis in
+ let args = Subtac_utils.destruct_ex pi sumg in
+ let args =
+ List.map (fun c ->
+ try Reductionops.whd_betadeltaiota (Global.env ()) Evd.empty c
+ with Not_found ->
+ trace (str "Not_found while reducing " ++
+ my_print_constr (Global.env ()) c);
+ c
+ ) args
+ in
+ let _, newdef = decompose_lam_n (recdefs + List.length args) kn in
+ let constr = Term.substl (mkRel 1 :: List.rev args) newdef in
+ aux pis (constr :: acc) tl)
+ | [] -> List.rev acc
+ in
+ declare (aux pis [] defs)
+ with Environ.NotEvaluableConst cer ->
+ match cer with
+ Environ.NoBody -> trace (str "Constant has no body")
+ | Environ.Opaque -> trace (str "Constant is opaque")
+ )
+
+
diff --git a/contrib/subtac/subtac_command.mli b/contrib/subtac/subtac_command.mli
index 6c1b0103ff..e1bbbbb5b0 100644
--- a/contrib/subtac/subtac_command.mli
+++ b/contrib/subtac/subtac_command.mli
@@ -16,26 +16,26 @@ val interp_gen :
?impls:full_implicits_env ->
?allow_soapp:bool ->
?ltacvars:ltac_sign ->
- constr_expr -> evar_map * constr
+ constr_expr -> constr
val interp_constr :
evar_defs ref ->
- env -> constr_expr -> evar_map * constr
+ env -> constr_expr -> constr
val interp_type :
evar_defs ref ->
env ->
?impls:full_implicits_env ->
- constr_expr -> evar_map * constr
+ constr_expr -> constr
val interp_casted_constr :
evar_defs ref ->
env ->
?impls:full_implicits_env ->
- constr_expr -> types -> evar_map * constr
+ constr_expr -> types -> constr
val interp_open_constr :
evar_defs ref -> env -> constr_expr -> constr
val interp_constr_judgment :
evar_defs ref ->
env ->
- constr_expr -> evar_defs * unsafe_judgment
+ constr_expr -> unsafe_judgment
val list_chop_hd : int -> 'a list -> 'a list * 'a * 'a list
val recursive_message : global_reference array -> std_ppcmds
val build_recursive :
diff --git a/contrib/subtac/subtac_interp_fixpoint.ml b/contrib/subtac/subtac_interp_fixpoint.ml
index 3ed5790e33..599dbe39e2 100644
--- a/contrib/subtac/subtac_interp_fixpoint.ml
+++ b/contrib/subtac/subtac_interp_fixpoint.ml
@@ -51,8 +51,8 @@ let list_of_local_binders l =
| [] -> List.rev acc
in aux [] l
-let abstract_constr_expr_bl c bl =
- List.fold_right (fun (n, t) c -> mkLambdaC ([n], t, c)) bl c
+let abstract_constr_expr_bl abs c bl =
+ List.fold_right (fun (n, t) c -> abs ([n], t, c)) bl c
let pr_binder_list b =
List.fold_right (fun ((loc, name), t) acc -> Nameops.pr_name name ++ str " : " ++
@@ -73,14 +73,14 @@ let rewrite_fixpoint env l (f, decl) =
Ppconstr.pr_constr_expr typ ++ str " := " ++ spc () ++
Ppconstr.pr_constr_expr body)
in
- let after, before = list_chop n bls in
+ let before, after = list_chop n bls in
let _ = trace (str "Binders before the recursion arg: " ++ spc () ++
pr_binder_list before ++ str "; after the recursion arg: " ++
pr_binder_list after)
in
- let ((locn, name), ntyp), before = match before with
+ let ((locn, name) as lnid, ntyp), after = match after with
hd :: tl -> hd, tl
- | _ -> assert(false) (* Rec arg must be in before *)
+ | _ -> assert(false) (* Rec arg must be in after *)
in
let nid = match name with
Name id -> id
@@ -96,27 +96,36 @@ let rewrite_fixpoint env l (f, decl) =
id_of_string (nid ^ "'"), id_of_string ("Acc_" ^ nid)
in
let lnid', laccproofid = (dummy_loc, Name nid'), (dummy_loc, Name accproofid) in
- let coqP = abstract_constr_expr_bl typ after in
+ let wf_prop = (mkAppC (wfrel, [ mkIdentC nid'; mkIdentC nid ])) in
+ let lam_wf_prop = mkLambdaC ([lnid'], ntyp, wf_prop) in
+ let typnid' = mkSubset lnid' ntyp wf_prop in
+ let internal_type =
+ abstract_constr_expr_bl mkProdC
+ (mkProdC ([lnid'], typnid',
+ mkLetInC (lnid, mkProj1 ntyp lam_wf_prop (mkIdentC nid'),
+ abstract_constr_expr_bl mkProdC typ after)))
+ before
+ in
let body' =
- let prop = (mkAppC (wfrel, [ mkIdentC nid'; mkIdentC nid ])) in
- let lamprop = mkLambdaC ([lnid'], ntyp, prop) in
- let typnid' = mkSubset lnid' ntyp prop in
+ let body =
+ (* cast or we will loose some info at pretyping time as body
+ is a function *)
+ CCast (dummy_loc, body, DEFAULTcast, typ)
+ in
let body' = (* body abstracted by rec call *)
- mkLambdaC ([(dummy_loc, Name id)],
- mkProdC ([lnid'], typnid', coqP),
- body)
+ mkLambdaC ([(dummy_loc, Name id)], internal_type, body)
in
mkAppC (body',
[mkLambdaC
([lnid'], typnid',
mkAppC (mkIdentC id,
- [mkProj1 ntyp lamprop (mkIdentC nid');
+ [mkProj1 ntyp lam_wf_prop (mkIdentC nid');
(mkAppExplC (acc_inv_ref,
[ ntyp; wfrel;
mkIdentC nid;
mkIdentC accproofid;
- mkProj1 ntyp lamprop (mkIdentC nid');
- mkProj2 ntyp lamprop (mkIdentC nid') ])) ]))])
+ mkProj1 ntyp lam_wf_prop (mkIdentC nid');
+ mkProj2 ntyp lam_wf_prop (mkIdentC nid') ])) ]))])
in
let acctyp = mkAppExplC (acc_ref, [ ntyp; wfrel; mkIdentC nid ]) in
let bl' =
@@ -127,12 +136,12 @@ let rewrite_fixpoint env l (f, decl) =
let rec aux' bl' = function
((loc, name') as x) :: tl ->
if name' = name then
- LocalRawAssum (List.rev (x :: bl'), typ) ::
- LocalRawAssum ([(dummy_loc, Name accproofid)], acctyp) ::
- if tl = [] then [] else [LocalRawAssum (tl, typ)]
+ (if tl = [] then [] else [LocalRawAssum (tl, typ)]) @
+ LocalRawAssum ([(dummy_loc, Name accproofid)], acctyp) ::
+ [LocalRawAssum (List.rev (x :: bl'), typ)]
else aux' (x :: bl') tl
| [] -> [assum]
- in aux (acc @ List.rev (aux' [] bl)) tl
+ in aux (aux' [] bl @ acc) tl
| [] -> List.rev acc
in aux [] bl
in
@@ -173,7 +182,7 @@ let rewrite_cases_aux (loc, po, tml, eqns) =
let po =
List.fold_right
(fun (n,t) acc ->
- RProd (dummy_loc, n, t, acc))
+ RProd (dummy_loc, Anonymous, t, acc))
eqs_types (match po with
Some e -> e
| None -> mkHole)
diff --git a/contrib/subtac/subtac_interp_fixpoint.mli b/contrib/subtac/subtac_interp_fixpoint.mli
index ef551aa8d2..b0de064167 100644
--- a/contrib/subtac/subtac_interp_fixpoint.mli
+++ b/contrib/subtac/subtac_interp_fixpoint.mli
@@ -12,10 +12,6 @@ val mkProj2 :
val list_of_local_binders :
Topconstr.local_binder list ->
(Names.name Util.located * Topconstr.constr_expr) list
-val abstract_constr_expr_bl :
- Topconstr.constr_expr ->
- (Names.name Util.located * Topconstr.constr_expr) list ->
- Topconstr.constr_expr
val pr_binder_list :
(('a * Names.name) * Topconstr.constr_expr) list -> Pp.std_ppcmds
val rewrite_rec_calls : 'a -> 'b -> 'b
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index 5cc7351855..f73a6e393d 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -71,7 +71,8 @@ let merge_evms x y =
let interp env isevars c tycon =
let j = pretype tycon env isevars ([],[]) c in
- j.uj_val, j.uj_type
+ let evm = evars_of !isevars in
+ nf_evar evm j.uj_val, nf_evar evm j.uj_type
let find_with_index x l =
let rec aux i = function
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index eb9888c161..d620c8e9fa 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -12,11 +12,15 @@ let contrib_name = "subtac"
let subtac_dir = [contrib_name]
let fix_sub_module = "FixSub"
+let utils_module = "Utils"
let fixsub_module = subtac_dir @ [fix_sub_module]
+let utils_module = subtac_dir @ [utils_module]
let init_constant dir s = gen_constant contrib_name dir s
let init_reference dir s = gen_reference contrib_name dir s
let fixsub = lazy (init_constant fixsub_module "Fix_sub")
+let ex_pi1 = lazy (init_constant utils_module "ex_pi1")
+let ex_pi2 = lazy (init_constant utils_module "ex_pi2")
let make_ref s = Qualid (dummy_loc, (qualid_of_string s))
let well_founded_ref = make_ref "Init.Wf.Well_founded"
@@ -41,6 +45,12 @@ let eqind = lazy (init_constant ["Init"; "Logic"] "eq")
let eqind_ref = lazy (init_reference ["Init"; "Logic"] "eq")
let refl_equal_ref = lazy (init_reference ["Init"; "Logic"] "refl_equal")
+let ex_ind = lazy (init_constant ["Init"; "Logic"] "ex")
+let ex_intro = lazy (init_reference ["Init"; "Logic"] "ex_intro")
+
+let proj1 = lazy (init_constant ["Init"; "Logic"] "proj1")
+let proj2 = lazy (init_constant ["Init"; "Logic"] "proj2")
+
let boolind = lazy (init_constant ["Init"; "Datatypes"] "bool")
let sumboolind = lazy (init_constant ["Init"; "Specif"] "sumbool")
let natind = lazy (init_constant ["Init"; "Datatypes"] "nat")
@@ -49,9 +59,14 @@ let existSind = lazy (init_constant ["Init"; "Specif"] "sigS")
let existS = lazy (build_sigma_set ())
+let prod = lazy (build_prod ())
+
+
(* orders *)
let well_founded = lazy (init_constant ["Init"; "Wf"] "well_founded")
let fix = lazy (init_constant ["Init"; "Wf"] "Fix")
+let acc = lazy (init_constant ["Init"; "Wf"] "Acc")
+let acc_inv = lazy (init_constant ["Init"; "Wf"] "Acc_inv")
let extconstr = Constrextern.extern_constr true (Global.env ())
let extsort s = Constrextern.extern_constr true (Global.env ()) (mkSort s)
@@ -62,21 +77,22 @@ let my_print_constr = Termops.print_constr_env
let my_print_context = Termops.print_rel_context
let my_print_env = Termops.print_env
let my_print_rawconstr = Printer.pr_rawconstr_env
+let my_print_evardefs = Evd.pr_evar_defs
+
+let my_print_tycon_type = Evarutil.pr_tycon_type
-let debug_level = ref 0
let debug n s =
- if n >= !debug_level then (
- msgnl s;
- msg_warning s;
- ) else ()
+ if !Options.debug then
+ msgnl s
+ else ()
let debug_msg n s =
- if n >= !debug_level then s
+ if !Options.debug then s
else mt ()
let trace s =
- if !debug_level < 2 then (msgnl s)
+ if !Options.debug then msgnl s
else ()
let wf_relations = Hashtbl.create 10
@@ -138,3 +154,92 @@ let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definiti
let global_fix_kind = Decl_kinds.IsDefinition Decl_kinds.Fixpoint
let goal_fix_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Fixpoint
+
+open Tactics
+open Tacticals
+
+let build_dependent_sum l =
+ let rec aux (acc, tac, typ) = function
+ (n, t) :: tl ->
+ let t' = mkLambda (Name n, t, typ) in
+ trace (str ("treating " ^ string_of_id n) ++
+ str "assert: " ++ my_print_constr (Global.env ()) t);
+ let tac' =
+ tclTHEN (assert_tac true (Name n) t)
+ (tclTHENLIST
+ [intros;
+ (tclTHENSEQ
+ [tclTRY (constructor_tac (Some 1) 1
+ (Rawterm.ImplicitBindings [mkVar n]));
+ tac]);
+ ])
+ in
+ aux (mkApp (Lazy.force ex_ind, [| t; t'; |]), tac', t') tl
+ | [] -> acc, tac, typ
+ in
+ match l with
+ (_, hd) :: tl -> aux (hd, intros, hd) tl
+ | [] -> raise (Invalid_argument "build_dependent_sum")
+
+open Proof_type
+open Tacexpr
+
+let mkProj1 a b c =
+ mkApp (Lazy.force proj1, [| a; b; c |])
+
+let mkProj2 a b c =
+ mkApp (Lazy.force proj2, [| a; b; c |])
+
+let mk_ex_pi1 a b c =
+ mkApp (Lazy.force ex_pi1, [| a; b; c |])
+
+let mk_ex_pi2 a b c =
+ mkApp (Lazy.force ex_pi2, [| a; b; c |])
+
+
+let mkSubset name typ prop =
+ mkApp ((Lazy.force sig_).typ,
+ [| typ; mkLambda (name, typ, prop) |])
+
+let and_tac l hook =
+ let andc = Coqlib.build_coq_and () in
+ let rec aux ((accid, goal, tac, extract) as acc) = function
+ | [] -> (* Singleton *) acc
+
+ | (id, x, elgoal, eltac) :: tl ->
+ let tac' = tclTHEN simplest_split (tclTHENLIST [tac; eltac]) in
+ let proj = fun c -> mkProj2 goal elgoal c in
+ let extract = List.map (fun (id, x, y, f) -> (id, x, y, (fun c -> f (mkProj1 goal elgoal c)))) extract in
+ aux ((string_of_id id) ^ "_" ^ accid, mkApp (andc, [| goal; elgoal |]), tac',
+ (id, x, elgoal, proj) :: extract) tl
+
+ in
+ let and_proof_id, and_goal, and_tac, and_extract =
+ match l with
+ | [] -> raise (Invalid_argument "and_tac: empty list of goals")
+ | (hdid, x, hdg, hdt) :: tl -> aux (string_of_id hdid, hdg, hdt, [hdid, x, hdg, (fun c -> c)]) tl
+ in
+ let and_proofid = id_of_string (and_proof_id ^ "_and_proof") in
+ Command.start_proof and_proofid goal_kind and_goal
+ (hook (fun c -> List.map (fun (id, x, t, f) -> (id, x, t, f c)) and_extract));
+ trace (str "Started and proof");
+ Pfedit.by and_tac;
+ trace (str "Applied and tac")
+
+
+let destruct_ex ext ex =
+ let rec aux c acc =
+ match kind_of_term c with
+ App (f, args) ->
+ (match kind_of_term f with
+ Ind i when i = Term.destInd (Lazy.force ex_ind) && Array.length args = 2 ->
+ let (dom, rng) =
+ try (args.(0), args.(1))
+ with _ -> assert(false)
+ in
+ (mk_ex_pi1 dom rng acc) :: aux rng (mk_ex_pi2 dom rng acc)
+ | _ -> [acc])
+ | _ -> [acc]
+ in aux ex ext
+
+
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index 84001c3740..a53016484b 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -8,6 +8,8 @@ open Decl_kinds
open Topconstr
open Rawterm
open Util
+open Evarutil
+open Names
val contrib_name : string
val subtac_dir : string list
@@ -36,15 +38,22 @@ val natind : constr lazy_t
val intind : constr lazy_t
val existSind : constr lazy_t
val existS : coq_sigma_data lazy_t
+val prod : coq_sigma_data lazy_t
+
val well_founded : constr lazy_t
val fix : constr lazy_t
+val acc : constr lazy_t
+val acc_inv : constr lazy_t
val extconstr : constr -> constr_expr
val extsort : sorts -> constr_expr
val my_print_constr : env -> constr -> std_ppcmds
+val my_print_evardefs : evar_defs -> std_ppcmds
val my_print_context : env -> std_ppcmds
val my_print_env : env -> std_ppcmds
val my_print_rawconstr : env -> rawconstr -> std_ppcmds
-val debug_level : int ref
+val my_print_tycon_type : env -> type_constraint_type -> std_ppcmds
+
+
val debug : int -> std_ppcmds -> unit
val debug_msg : int -> std_ppcmds -> std_ppcmds
val trace : std_ppcmds -> unit
@@ -61,3 +70,15 @@ val global_kind : logical_kind
val goal_kind : locality_flag * goal_object_kind
val global_fix_kind : logical_kind
val goal_fix_kind : locality_flag * goal_object_kind
+
+val mkSubset : name -> constr -> constr -> constr
+val mkProj1 : constr -> constr -> constr -> constr
+val mkProj1 : constr -> constr -> constr -> constr
+val mk_ex_pi1 : constr -> constr -> constr -> constr
+val mk_ex_pi1 : constr -> constr -> constr -> constr
+
+val build_dependent_sum : (identifier * types) list -> constr * Proof_type.tactic * types
+val and_tac : (identifier * 'a * constr * Proof_type.tactic) list ->
+ ((constr -> (identifier * 'a * constr * constr) list) -> Tacexpr.declaration_hook) -> unit
+
+val destruct_ex : constr -> constr -> constr list
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 39a12a7ea7..871a7f15cb 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -214,7 +214,6 @@ let theory_filename xml_library_root =
None -> None (* stdout *)
| Some xml_library_root' ->
let toks = List.map N.string_of_id (N.repr_dirpath (Lib.library_dp ())) in
- let hd = List.hd toks in
(* theory from A/B/C/F.v goes into A/B/C/F.theory *)
let alltoks = List.rev toks in
Some (join_dirs xml_library_root' alltoks ^ ".theory")
diff --git a/doc/Makefile b/doc/Makefile
index e0fd8ac7bf..07b130394c 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -112,7 +112,7 @@ REFMANCOQTEXFILES=\
refman/RefMan-tacex.v.tex refman/RefMan-syn.v.tex \
refman/RefMan-oth.v.tex \
refman/Cases.v.tex refman/Coercion.v.tex refman/Extraction.v.tex \
- refman/Omega.v.tex refman/Polynom.v.tex \
+ refman/Program.v.tex refman/Omega.v.tex refman/Polynom.v.tex \
refman/Setoid.v.tex refman/Helm.tex # refman/Natural.v.tex
REFMANTEXFILES=\
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
new file mode 100644
index 0000000000..4f3fadcbd5
--- /dev/null
+++ b/doc/refman/Program.tex
@@ -0,0 +1,491 @@
+\def\Program{\textsc{Program}}
+\def\Russel{\textsc{Russel}}
+
+\achapter{The \Program{} tactic}
+\label{Program}
+\aauthor{Matthieu Sozeau}
+\index{Program}
+
+\begin{flushleft}
+ \em The status of \Program is experimental.
+\end{flushleft}
+
+We present here the \Coq\ \Program tactic commands, used to build certified
+\Coq programs, elaborating them from their algorithmic skeleton and a
+rich specification. It can be sought of as a dual of extraction \ref{Extraction}.
+The languages available as input are currently restricted to \Coq's term
+language, but may be extended to \ocaml{}, \textsc{Haskell} and others
+in the future. Input terms and types are typed in an extended system (\Russel) and
+interpreted into \Coq\ terms. The interpretation process may produce
+some proof obligations which need to be resolved to create the final term.
+
+\asection{Elaborating programs}
+\comindex{Program Fixpoint}
+
+The next two commands are similar to they standard counterparts
+\ref{Simpl-definitions} and \ref{Fixpoint} in that
+they define constants. However, they may require the user to prove some
+goals to construct the final definitions.
+
+\section{\tt Program Definition {\ident} := {\term}.
+ \comindex{Program Definition}\label{ProgramDefinition}}
+
+This command types the value {\term} in \Russel and generate subgoals
+corresponding to proof obligations. Once solved, it binds the final
+\Coq\ term to the name {\ident} in the environment.
+
+\begin{ErrMsgs}
+\item \errindex{{\ident} already exists}
+\end{ErrMsgs}
+
+\begin{Variants}
+\item {\tt Program Definition {\ident} {\tt :}{\term$_1$} :=
+ {\term$_2$}.}\\
+ It interprets the type {\term$_1$}, potentially generating proof
+ obligations to be resolved. Once done with them, we have a \Coq\ type
+ {\term$_1'$}. It then checks that the type of the interpretation of
+ {\term$_2$} is coercible to {\term$_1'$}, and registers {\ident} as
+ being of type {\term$_1'$} once the set of obligations generated
+ during the interpretation of {\term$_2$} and the aforementioned
+ coercion derivation are solved.
+\item {\tt Program Definition {\ident} {\binder$_1$}\ldots{\binder$_n$}
+ {\tt :}\term$_1$ {\tt :=} {\term$_2$}.}\\
+ This is equivalent to \\
+ {\tt Program Definition\,{\ident}\,{\tt :\,forall}\,%
+ {\binder$_1$}\ldots{\binder$_n$}{\tt ,}\,\term$_1$\,{\tt :=}}\,%
+ {\tt fun}\,{\binder$_1$}\ldots{\binder$_n$}\,{\tt =>}\,{\term$_2$}\,%
+ {\tt .}
+\end{Variants}
+
+\begin{ErrMsgs}
+\item \errindex{In environment {\dots} the term: {\term$_2$} does not have type
+ {\term$_1$}}.\\
+ \texttt{Actually, it has type {\term$_3$}}.
+\end{ErrMsgs}
+
+\SeeAlso Sections \ref{Opaque}, \ref{Transparent}, \ref{unfold}
+
+\section{\tt Program Fixpoint {\ident} {\params} {\tt \{order\}} : type$_0$ := \term$_0$
+ \comindex{Program Fixpoint}
+ \label{ProgramFixpoint}}
+
+This command allows to define objects using a fixed point
+construction. The meaning of this declaration is to define {\it ident}
+a recursive function with arguments specified by
+{\binder$_1$}\ldots{\binder$_n$} such that {\it ident} applied to
+arguments corresponding to these binders has type \type$_0$, and is
+equivalent to the expression \term$_0$. The type of the {\ident} is
+consequently {\tt forall {\params} {\tt,} \type$_0$}
+and the value is equivalent to {\tt fun {\params} {\tt =>} \term$_0$}.
+
+There are two ways to define fixpoints with \Program{}, structural and
+well-founded recursion.
+
+\subsection{\tt Program Fixpoint {\ident} {\params} {\tt \{struct}
+ \ident$_0$ {\tt \}} : type$_0$ := \term$_0$
+ \comindex{Program Fixpoint Struct}
+ \label{ProgramFixpointStruct}}
+
+To be accepted, a structural {\tt Fixpoint} definition has to satisfy some
+syntactical constraints on a special argument called the decreasing
+argument. They are needed to ensure that the {\tt Fixpoint} definition
+always terminates. The point of the {\tt \{struct \ident {\tt \}}}
+annotation is to let the user tell the system which argument decreases
+along the recursive calls. This annotation may be left implicit for
+fixpoints with one argument. For instance, one can define the identity
+function on naturals as :
+
+\begin{coq_example}
+Program Fixpoint id (n : nat) : { x : nat | x = n } :=
+ match n with
+ | O => O
+ | S p => S (id p)
+ end.
+\end{coq_example}
+
+The {\tt match} operator matches a value (here \verb:n:) with the
+various constructors of its (inductive) type. The remaining arguments
+give the respective values to be returned, as functions of the
+parameters of the corresponding constructor. Thus here when \verb:n:
+equals \verb:O: we return \verb:0:, and when \verb:n: equals
+\verb:(S p): we return \verb:(S (id p)):.
+
+The {\tt match} operator is formally described
+in detail in Section~\ref{Caseexpr}. The system recognizes that in
+the inductive call {\tt (id p)} the argument actually
+decreases because it is a {\em pattern variable} coming from {\tt match
+ n with}.
+
+Here again, proof obligations may be generated. In our example, we would
+have one for each branch:
+\begin{coq_example}
+Show.
+\end{coq_example}
+
+% \subsection{\tt Program Fixpoint {\ident} {(\ident_$_0$ : \type_$_0$)
+% \cdots (\ident_$_n$ : \type_$_n$)} {\tt \{wf}
+% \ident$_i$ \term_{wf} {\tt \}} : type$_t$ := \term$_0$
+% \comindex{Program Fixpoint Wf}
+% \label{ProgramFixpointWf}}
+
+% To be accepted, a well-founded {\tt Fixpoint} definition has to satisfy some
+% logical constraints on the decreasing argument.
+% They are needed to ensure that the {\tt Fixpoint} definition
+% always terminates. The point of the {\tt \{wf \ident \term {\tt \}}}
+% annotation is to let the user tell the system which argument decreases
+% in which well-founded relation along the recursive calls.
+% The term \term$_0$ will be typed in a different context than usual,
+% The typing problem will in fact be reduced to:
+
+% % \begin{center}
+% % {\tt forall} {\params} {\ident : (\ident$_0$ : type$_0$) \cdots
+% % \{ \ident$_i'$ : \type$_i$ | \term_{wf} \ident$_i'$ \ident$_i$ \}
+% % \cdots (\ident$_n$ : type$_n$), type$_t$} : type$_t$ := \term$_0$
+% % \end{center}
+
+% \begin{coq_example}
+% Program Fixpoint id (n : nat) : { x : nat | x = n } :=
+% match n with
+% | O => O
+% | S p => S (id p)
+% end
+% \end{coq_example}
+
+% The {\tt match} operator matches a value (here \verb:n:) with the
+% various constructors of its (inductive) type. The remaining arguments
+% give the respective values to be returned, as functions of the
+% parameters of the corresponding constructor. Thus here when \verb:n:
+% equals \verb:O: we return \verb:0:, and when \verb:n: equals
+% \verb:(S p): we return \verb:(S (id p)):.
+
+% The {\tt match} operator is formally described
+% in detail in Section~\ref{Caseexpr}. The system recognizes that in
+% the inductive call {\tt (id p)} the argument actually
+% decreases because it is a {\em pattern variable} coming from {\tt match
+% n with}.
+
+% Here again, proof obligations may be generated. In our example, we would
+% have one for each branch:
+% \begin{coq_example}
+% Show.
+% \end{coq_example}
+% \begin{coq_eval}
+% Abort.
+% \end{coq_eval}
+
+
+
+
+% \asubsection{A detailed example: Euclidean division}
+
+% The file {\tt Euclid} contains the proof of Euclidean division
+% (theorem {\tt eucl\_dev}). The natural numbers defined in the example
+% files are unary integers defined by two constructors $O$ and $S$:
+% \begin{coq_example*}
+% Inductive nat : Set :=
+% | O : nat
+% | S : nat -> nat.
+% \end{coq_example*}
+
+% This module contains a theorem {\tt eucl\_dev}, and its extracted term
+% is of type
+% \begin{verbatim}
+% forall b:nat, b > 0 -> forall a:nat, diveucl a b
+% \end{verbatim}
+% where {\tt diveucl} is a type for the pair of the quotient and the modulo.
+% We can now extract this program to \ocaml:
+
+% \begin{coq_eval}
+% Reset Initial.
+% \end{coq_eval}
+% \begin{coq_example}
+% Require Import Euclid.
+% Extraction Inline Wf_nat.gt_wf_rec Wf_nat.lt_wf_rec.
+% Recursive Extraction eucl_dev.
+% \end{coq_example}
+
+% The inlining of {\tt gt\_wf\_rec} and {\tt lt\_wf\_rec} is not
+% mandatory. It only enhances readability of extracted code.
+% You can then copy-paste the output to a file {\tt euclid.ml} or let
+% \Coq\ do it for you with the following command:
+
+% \begin{coq_example}
+% Extraction "euclid" eucl_dev.
+% \end{coq_example}
+
+% Let us play the resulting program:
+
+% \begin{verbatim}
+% # #use "euclid.ml";;
+% type sumbool = Left | Right
+% type nat = O | S of nat
+% type diveucl = Divex of nat * nat
+% val minus : nat -> nat -> nat = <fun>
+% val le_lt_dec : nat -> nat -> sumbool = <fun>
+% val le_gt_dec : nat -> nat -> sumbool = <fun>
+% val eucl_dev : nat -> nat -> diveucl = <fun>
+% # eucl_dev (S (S O)) (S (S (S (S (S O)))));;
+% - : diveucl = Divex (S (S O), S O)
+% \end{verbatim}
+% It is easier to test on \ocaml\ integers:
+% \begin{verbatim}
+% # let rec i2n = function 0 -> O | n -> S (i2n (n-1));;
+% val i2n : int -> nat = <fun>
+% # let rec n2i = function O -> 0 | S p -> 1+(n2i p);;
+% val n2i : nat -> int = <fun>
+% # let div a b =
+% let Divex (q,r) = eucl_dev (i2n b) (i2n a) in (n2i q, n2i r);;
+% div : int -> int -> int * int = <fun>
+% # div 173 15;;
+% - : int * int = 11, 8
+% \end{verbatim}
+
+% \asubsection{Another detailed example: Heapsort}
+
+% The file {\tt Heap.v}
+% contains the proof of an efficient list sorting algorithm described by
+% Bjerner. Is is an adaptation of the well-known {\em heapsort}
+% algorithm to functional languages. The main function is {\tt
+% treesort}, whose type is shown below:
+
+
+% \begin{coq_eval}
+% Reset Initial.
+% Require Import Relation_Definitions.
+% Require Import List.
+% Require Import Sorting.
+% Require Import Permutation.
+% \end{coq_eval}
+% \begin{coq_example}
+% Require Import Heap.
+% Check treesort.
+% \end{coq_example}
+
+% Let's now extract this function:
+
+% \begin{coq_example}
+% Extraction Inline sort_rec is_heap_rec.
+% Extraction NoInline list_to_heap.
+% Extraction "heapsort" treesort.
+% \end{coq_example}
+
+% One more time, the {\tt Extraction Inline} and {\tt NoInline}
+% directives are cosmetic. Without it, everything goes right,
+% but the output is less readable.
+% Here is the produced file {\tt heapsort.ml}:
+
+% \begin{verbatim}
+% type nat =
+% | O
+% | S of nat
+
+% type 'a sig2 =
+% 'a
+% (* singleton inductive, whose constructor was exist2 *)
+
+% type sumbool =
+% | Left
+% | Right
+
+% type 'a list =
+% | Nil
+% | Cons of 'a * 'a list
+
+% type 'a multiset =
+% 'a -> nat
+% (* singleton inductive, whose constructor was Bag *)
+
+% type 'a merge_lem =
+% 'a list
+% (* singleton inductive, whose constructor was merge_exist *)
+
+% (** val merge : ('a1 -> 'a1 -> sumbool) -> ('a1 -> 'a1 -> sumbool) ->
+% 'a1 list -> 'a1 list -> 'a1 merge_lem **)
+
+% let rec merge leA_dec eqA_dec l1 l2 =
+% match l1 with
+% | Nil -> l2
+% | Cons (a, l) ->
+% let rec f = function
+% | Nil -> Cons (a, l)
+% | Cons (a0, l3) ->
+% (match leA_dec a a0 with
+% | Left -> Cons (a,
+% (merge leA_dec eqA_dec l (Cons (a0, l3))))
+% | Right -> Cons (a0, (f l3)))
+% in f l2
+
+% type 'a tree =
+% | Tree_Leaf
+% | Tree_Node of 'a * 'a tree * 'a tree
+
+% type 'a insert_spec =
+% 'a tree
+% (* singleton inductive, whose constructor was insert_exist *)
+
+% (** val insert : ('a1 -> 'a1 -> sumbool) -> ('a1 -> 'a1 -> sumbool) ->
+% 'a1 tree -> 'a1 -> 'a1 insert_spec **)
+
+% let rec insert leA_dec eqA_dec t a =
+% match t with
+% | Tree_Leaf -> Tree_Node (a, Tree_Leaf, Tree_Leaf)
+% | Tree_Node (a0, t0, t1) ->
+% let h3 = fun x -> insert leA_dec eqA_dec t0 x in
+% (match leA_dec a0 a with
+% | Left -> Tree_Node (a0, t1, (h3 a))
+% | Right -> Tree_Node (a, t1, (h3 a0)))
+
+% type 'a build_heap =
+% 'a tree
+% (* singleton inductive, whose constructor was heap_exist *)
+
+% (** val list_to_heap : ('a1 -> 'a1 -> sumbool) -> ('a1 -> 'a1 ->
+% sumbool) -> 'a1 list -> 'a1 build_heap **)
+
+% let rec list_to_heap leA_dec eqA_dec = function
+% | Nil -> Tree_Leaf
+% | Cons (a, l0) ->
+% insert leA_dec eqA_dec (list_to_heap leA_dec eqA_dec l0) a
+
+% type 'a flat_spec =
+% 'a list
+% (* singleton inductive, whose constructor was flat_exist *)
+
+% (** val heap_to_list : ('a1 -> 'a1 -> sumbool) -> ('a1 -> 'a1 ->
+% sumbool) -> 'a1 tree -> 'a1 flat_spec **)
+
+% let rec heap_to_list leA_dec eqA_dec = function
+% | Tree_Leaf -> Nil
+% | Tree_Node (a, t0, t1) -> Cons (a,
+% (merge leA_dec eqA_dec (heap_to_list leA_dec eqA_dec t0)
+% (heap_to_list leA_dec eqA_dec t1)))
+
+% (** val treesort : ('a1 -> 'a1 -> sumbool) -> ('a1 -> 'a1 -> sumbool)
+% -> 'a1 list -> 'a1 list sig2 **)
+
+% let treesort leA_dec eqA_dec l =
+% heap_to_list leA_dec eqA_dec (list_to_heap leA_dec eqA_dec l)
+
+% \end{verbatim}
+
+% Let's test it:
+% % Format.set_margin 72;;
+% \begin{verbatim}
+% # #use "heapsort.ml";;
+% type sumbool = Left | Right
+% type nat = O | S of nat
+% type 'a tree = Tree_Leaf | Tree_Node of 'a * 'a tree * 'a tree
+% type 'a list = Nil | Cons of 'a * 'a list
+% val merge :
+% ('a -> 'a -> sumbool) -> 'b -> 'a list -> 'a list -> 'a list = <fun>
+% val heap_to_list :
+% ('a -> 'a -> sumbool) -> 'b -> 'a tree -> 'a list = <fun>
+% val insert :
+% ('a -> 'a -> sumbool) -> 'b -> 'a tree -> 'a -> 'a tree = <fun>
+% val list_to_heap :
+% ('a -> 'a -> sumbool) -> 'b -> 'a list -> 'a tree = <fun>
+% val treesort :
+% ('a -> 'a -> sumbool) -> 'b -> 'a list -> 'a list = <fun>
+% \end{verbatim}
+
+% One can remark that the argument of {\tt treesort} corresponding to
+% {\tt eqAdec} is never used in the informative part of the terms,
+% only in the logical parts. So the extracted {\tt treesort} never use
+% it, hence this {\tt 'b} argument. We will use {\tt ()} for this
+% argument. Only remains the {\tt leAdec}
+% argument (of type {\tt 'a -> 'a -> sumbool}) to really provide.
+
+% \begin{verbatim}
+% # let leAdec x y = if x <= y then Left else Right;;
+% val leAdec : 'a -> 'a -> sumbool = <fun>
+% # let rec listn = function 0 -> Nil
+% | n -> Cons(Random.int 10000,listn (n-1));;
+% val listn : int -> int list = <fun>
+% # treesort leAdec () (listn 9);;
+% - : int list = Cons (160, Cons (883, Cons (1874, Cons (3275, Cons
+% (5392, Cons (7320, Cons (8512, Cons (9632, Cons (9876, Nil)))))))))
+% \end{verbatim}
+
+% Some tests on longer lists (10000 elements) show that the program is
+% quite efficient for Caml code.
+
+
+% \asubsection{The Standard Library}
+
+% As a test, we propose an automatic extraction of the
+% Standard Library of \Coq. In particular, we will find back the
+% two previous examples, {\tt Euclid} and {\tt Heapsort}.
+% Go to directory {\tt contrib/extraction/test} of the sources of \Coq,
+% and run commands:
+% \begin{verbatim}
+% make tree; make
+% \end{verbatim}
+% This will extract all Standard Library files and compile them.
+% It is done via many {\tt Extraction Module}, with some customization
+% (see subdirectory {\tt custom}).
+
+% %The result of this extraction of the Standard Library can be browsed
+% %at URL
+% %\begin{flushleft}
+% %\url{http://www.lri.fr/~letouzey/extraction}.
+% %\end{flushleft}
+
+% %Reals theory is normally not extracted, since it is an axiomatic
+% %development. We propose nonetheless a dummy realization of those
+% %axioms, to test, run: \\
+% %
+% %\mbox{\tt make reals}\\
+
+% This test works also with Haskell. In the same directory, run:
+% \begin{verbatim}
+% make tree; make -f Makefile.haskell
+% \end{verbatim}
+% The haskell compiler currently used is {\tt hbc}. Any other should
+% also work, just adapt the {\tt Makefile.haskell}. In particular {\tt
+% ghc} is known to work.
+
+% \asubsection{Extraction's horror museum}
+
+% Some pathological examples of extraction are grouped in the file
+% \begin{verbatim}
+% contrib/extraction/test_extraction.v
+% \end{verbatim}
+% of the sources of \Coq.
+
+% \asubsection{Users' Contributions}
+
+% Several of the \Coq\ Users' Contributions use extraction to produce
+% certified programs. In particular the following ones have an automatic
+% extraction test (just run {\tt make} in those directories):
+
+% \begin{itemize}
+% \item Bordeaux/Additions
+% \item Bordeaux/EXCEPTIONS
+% \item Bordeaux/SearchTrees
+% \item Dyade/BDDS
+% \item Lannion
+% \item Lyon/CIRCUITS
+% \item Lyon/FIRING-SQUAD
+% \item Marseille/CIRCUITS
+% \item Muenchen/Higman
+% \item Nancy/FOUnify
+% \item Rocq/ARITH/Chinese
+% \item Rocq/COC
+% \item Rocq/GRAPHS
+% \item Rocq/HIGMAN
+% \item Sophia-Antipolis/Stalmarck
+% \item Suresnes/BDD
+% \end{itemize}
+
+% Lannion, Rocq/HIGMAN and Lyon/CIRCUITS are a bit particular. They are
+% the only examples of developments where {\tt Obj.magic} are needed.
+% This is probably due to an heavy use of impredicativity.
+% After compilation those two examples run nonetheless,
+% thanks to the correction of the extraction~\cite{Let02}.
+
+% $Id$
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "Reference-Manual"
+%%% End:
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index b125720d34..8cebfa4d9b 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -89,9 +89,9 @@
\include{Coercion.v}%
%%SUPPRIME \include{Natural.v}%
\include{Omega.v}%
-%%SUPPRIME \include{Program.v}%
%%SUPPRIME \include{Correctness.v}% = preuve de pgms imperatifs
\include{Extraction.v}%
+\include{Program.v}%
\include{Polynom.v}% = Ring
\include{Setoid.v}% Tactique pour les setoides
%BEGIN LATEX
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 8a55bfc2c8..f9a1c6466f 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -166,6 +166,13 @@ let build_sigma_type () =
intro = init_constant ["Specif"] "existT";
typ = init_constant ["Specif"] "sigT" }
+let build_prod () =
+ { proj1 = init_constant ["Datatypes"] "fst";
+ proj2 = init_constant ["Datatypes"] "snd";
+ elim = init_constant ["Datatypes"] "prod_rec";
+ intro = init_constant ["Datatypes"] "pair";
+ typ = init_constant ["Datatypes"] "prod" }
+
(* Equalities *)
type coq_leibniz_eq_data = {
eq : constr;
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index ed5e46c1a0..098dad1d5f 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -94,6 +94,8 @@ type coq_sigma_data = {
val build_sigma_set : coq_sigma_data delayed
val build_sigma_type : coq_sigma_data delayed
+(* Non-dependent pairs in Set from Datatypes *)
+val build_prod : coq_sigma_data delayed
type coq_leibniz_eq_data = {
eq : constr;
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index b2ef8060d6..ec1246b745 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -352,7 +352,7 @@ let find_tomatch_tycon isevars env loc = function
| Some (_,ind,_),_
(* Otherwise try to get constraints from (the 1st) constructor in clauses *)
| None, Some (_,(ind,_)) ->
- Some (inductive_template isevars env loc ind)
+ Some (0, inductive_template isevars env loc ind)
| None, None ->
empty_tycon
@@ -412,7 +412,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps) =
current
else
(evd_comb2 (Coercion.inh_conv_coerce_to dummy_loc pb.env)
- pb.isevars (make_judge current typ) indt).uj_val in
+ pb.isevars (make_judge current typ) (0, indt)).uj_val in
let sigma = Evd.evars_of !(pb.isevars) in
let typ = IsInd (indt,find_rectype pb.env sigma indt) in
((current,typ),deps))
@@ -1571,8 +1571,9 @@ let prepare_predicate_from_tycon loc dep env isevars tomatchs c =
e_new_evar isevars env ~src:(loc, Evd.CasesType)
(Retyping.get_type_of env (Evd.evars_of !isevars) c)
else
- map_constr_with_full_binders push_rel build_skeleton env c in
- names, build_skeleton env (lift n c)
+ map_constr_with_full_binders push_rel build_skeleton env c
+ in
+ names, build_skeleton env (lift n c)
(* Here, [pred] is assumed to be in the context built from all *)
(* realargs and terms to match *)
@@ -1639,6 +1640,15 @@ let extract_arity_signature env0 tomatchl tmsign =
| _ -> assert false
in List.rev (buildrec 0 (tomatchl,tmsign))
+let inh_conv_coerce_to_tycon loc env isevars j tycon =
+ match tycon with
+ | Some p ->
+ let (evd',j) = Coercion.inh_conv_coerce_to loc env !isevars j p in
+ isevars := evd';
+ j
+ | None -> j
+
+
(* Builds the predicate. If the predicate is dependent, its context is
* made of 1+nrealargs assumptions for each matched term in an inductive
* type and 1 assumption for each term not _syntactically_ in an
@@ -1653,11 +1663,11 @@ let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function
(* No type annotation *)
| None ->
(match tycon with
- | None -> None
- | Some t ->
- let names,pred =
- prepare_predicate_from_tycon loc false env isevars tomatchs t in
- Some (build_initial_predicate false names pred))
+ | Some (0, t) ->
+ let names,pred =
+ prepare_predicate_from_tycon loc false env isevars tomatchs t
+ in Some (build_initial_predicate false names pred)
+ | _ -> None)
(* Some type annotation *)
| Some rtntyp ->
@@ -1665,52 +1675,52 @@ let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function
let arsign = extract_arity_signature env tomatchs sign in
let env = List.fold_right push_rels arsign env in
let allnames = List.rev (List.map (List.map pi1) arsign) in
- let predccl = (typing_fun (mk_tycon (new_Type ())) env rtntyp).uj_val in
- Some (build_initial_predicate true allnames predccl)
+ let predcclj = typing_fun (mk_tycon (new_Type ())) env rtntyp in
+ let _ =
+ option_app (fun tycon ->
+ isevars := Coercion.inh_conv_coerces_to loc env !isevars predcclj.uj_val tycon)
+ tycon
+ in
+ let predccl = (j_nf_isevar !isevars predcclj).uj_val in
+ Some (build_initial_predicate true allnames predccl)
(**************************************************************************)
(* Main entry of the matching compilation *)
- let compile_cases loc (typing_fun, isevars) tycon env (predopt, tomatchl, eqns)=
+let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns)=
+
+ (* We build the matrix of patterns and right-hand-side *)
+ let matx = matx_of_eqns env tomatchl eqns in
+
+ (* We build the vector of terms to match consistently with the *)
+ (* constructors found in patterns *)
+ let tomatchs = coerce_to_indtype typing_fun isevars env matx tomatchl in
+
+ (* We build the elimination predicate if any and check its consistency *)
+ (* with the type of arguments to match *)
+ let tmsign = List.map snd tomatchl in
+ let pred = prepare_predicate loc typing_fun isevars env tomatchs tmsign tycon predopt in
- (* We build the matrix of patterns and right-hand-side *)
- let matx = matx_of_eqns env tomatchl eqns in
-
- (* We build the vector of terms to match consistently with the *)
- (* constructors found in patterns *)
- let tomatchs = coerce_to_indtype typing_fun isevars env matx tomatchl in
-
- (* We build the elimination predicate if any and check its consistency *)
- (* with the type of arguments to match *)
- let tmsign = List.map snd tomatchl in
- let pred = prepare_predicate loc typing_fun isevars env tomatchs tmsign tycon predopt in
-
- (* We deal with initial aliases *)
- let matx = prepare_initial_aliases (known_dependent pred) tomatchs matx in
-
- (* We push the initial terms to match and push their alias to rhs' envs *)
- (* names of aliases will be recovered from patterns (hence Anonymous here) *)
- let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in
-
- let pb =
- { env = env;
- isevars = isevars;
- pred = pred;
- tomatch = initial_pushed;
- history = start_history (List.length initial_pushed);
- mat = matx;
- caseloc = loc;
- typing_function = typing_fun } in
-
- let _, j = compile pb in
-
- (* We check for unused patterns *)
- List.iter (check_unused_pattern env) matx;
-
- match tycon with
- | Some p ->
- let (evd',j) = Coercion.inh_conv_coerce_to loc env !isevars j p in
- isevars := evd';
- j
- | None -> j
+ (* We deal with initial aliases *)
+ let matx = prepare_initial_aliases (known_dependent pred) tomatchs matx in
+
+ (* We push the initial terms to match and push their alias to rhs' envs *)
+ (* names of aliases will be recovered from patterns (hence Anonymous here) *)
+ let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in
+
+ let pb =
+ { env = env;
+ isevars = isevars;
+ pred = pred;
+ tomatch = initial_pushed;
+ history = start_history (List.length initial_pushed);
+ mat = matx;
+ caseloc = loc;
+ typing_function = typing_fun } in
+
+ let _, j = compile pb in
+ (* We check for unused patterns *)
+ List.iter (check_unused_pattern env) matx;
+ inh_conv_coerce_to_tycon loc env isevars j tycon
end
+
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index cb8c2cf2b5..d7c8a6dd0c 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -31,7 +31,7 @@ open Mod_subst
(* *)
let w_coerce env c ctyp target evd =
let j = make_judge c ctyp in
- let (evd',j') = Coercion.Default.inh_conv_coerce_to dummy_loc env evd j target in
+ let (evd',j') = Coercion.Default.inh_conv_coerce_to dummy_loc env evd j (mk_tycon_type target) in
(evd',j'.uj_val)
let pf_env gls = Global.env_of_context gls.it.evar_hyps
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 3b2d85b1ff..841e6b0347 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -40,8 +40,15 @@ module type S = sig
[t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and
[j.uj_type] are convertible; it fails if no coercion is applicable *)
val inh_conv_coerce_to : loc ->
- env -> evar_defs -> unsafe_judgment -> types -> evar_defs * unsafe_judgment
+ env -> evar_defs -> unsafe_judgment -> type_constraint_type -> evar_defs * unsafe_judgment
+
+ (* [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t]
+ is coercible to an object of type [t'] adding evar constraints if needed;
+ it fails if no coercion exists *)
+ val inh_conv_coerces_to : loc ->
+ env -> evar_defs -> types -> type_constraint_type -> evar_defs
+
(* [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases
pattern [pat] typed in [ind1] into a pattern typed in [ind2];
raises [Not_found] if no coercion found *)
@@ -136,73 +143,129 @@ module Default = struct
| _ ->
inh_tosort_force loc env isevars j
- let inh_coerce_to_fail env isevars c1 hj =
- let hj' =
+ let inh_coerce_to_fail env isevars c1 v t =
+ let v', t' =
try
let t1,i1 = class_of1 env (evars_of isevars) c1 in
- let t2,i2 = class_of1 env (evars_of isevars) hj.uj_type in
+ let t2,i2 = class_of1 env (evars_of isevars) t in
let p = lookup_path_between (i2,i1) in
- apply_coercion env p hj t2
+ match v with
+ Some v ->
+ let j = apply_coercion env p {uj_val = v; uj_type = t} t2 in
+ Some j.uj_val, j.uj_type
+ | None -> None, t
with Not_found -> raise NoCoercion
in
- try (the_conv_x_leq env hj'.uj_type c1 isevars, hj')
+ try (the_conv_x_leq env t' c1 isevars, v', t')
with Reduction.NotConvertible -> raise NoCoercion
-
- let rec inh_conv_coerce_to_fail env isevars hj c1 =
- let {uj_val = v; uj_type = t} = hj in
- try (the_conv_x_leq env t c1 isevars, hj)
- with Reduction.NotConvertible ->
- (try
- inh_coerce_to_fail env isevars c1 hj
+ open Pp
+ let rec inh_conv_coerce_to_fail loc env isevars v t c1 =
+(* (try *)
+(* msgnl (str "inh_conv_coerces_to_fail called for " ++ *)
+(* Termops.print_constr_env env t ++ str " and "++ spc () ++ *)
+(* Termops.print_constr_env env c1 ++ str " with evars: " ++ spc () ++ *)
+(* Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++ *)
+(* Termops.print_env env); *)
+(* with _ -> ()); *)
+ try (the_conv_x_leq env t c1 isevars, v, t)
+ with Reduction.NotConvertible ->
+ (try
+ inh_coerce_to_fail env isevars c1 v t
with NoCoercion ->
(match kind_of_term (whd_betadeltaiota env (evars_of isevars) t),
kind_of_term (whd_betadeltaiota env (evars_of isevars) c1) with
| Prod (_,t1,t2), Prod (name,u1,u2) ->
- let v' = whd_betadeltaiota env (evars_of isevars) v in
+ let v' = option_app (whd_betadeltaiota env (evars_of isevars)) v in
let (evd',b) =
- match kind_of_term v' with
- | Lambda (_,v1,v2) ->
- (try the_conv_x env v1 u1 isevars, true (* leq v1 u1? *)
- with Reduction.NotConvertible -> (isevars, false))
- | _ -> (isevars,false) in
- if b
- then
- let (x,v1,v2) = destLambda v' in
- let env1 = push_rel (x,None,v1) env in
- let (evd'',h2) = inh_conv_coerce_to_fail env1 evd'
- {uj_val = v2; uj_type = t2 } u2 in
- (evd'',{ uj_val = mkLambda (x, v1, h2.uj_val);
- uj_type = mkProd (x, v1, h2.uj_type) })
- else
- (* Mismatch on t1 and u1 or not a lambda: we eta-expand *)
- (* we look for a coercion c:u1->t1 s.t. [name:u1](v' (c x)) *)
- (* has type (name:u1)u2 (with v' recursively obtained) *)
- let name = (match name with
- | Anonymous -> Name (id_of_string "x")
- | _ -> name) in
- let env1 = push_rel (name,None,u1) env in
- let (evd',h1) =
- inh_conv_coerce_to_fail env1 isevars
- {uj_val = mkRel 1; uj_type = (lift 1 u1) }
- (lift 1 t1) in
- let (evd'',h2) = inh_conv_coerce_to_fail env1 evd'
- { uj_val = mkApp (lift 1 v, [|h1.uj_val|]);
- uj_type = subst1 h1.uj_val t2 }
- u2
- in
- (evd'',
- { uj_val = mkLambda (name, u1, h2.uj_val);
- uj_type = mkProd (name, u1, h2.uj_type) })
+ match v' with
+ Some v' ->
+ (match kind_of_term v' with
+ | Lambda (x,v1,v2) ->
+ (try the_conv_x env v1 u1 isevars, Some (x, v1, v2) (* leq v1 u1? *)
+ with Reduction.NotConvertible -> (isevars, None))
+ | _ -> (isevars, None))
+ | None -> (isevars, None)
+ in
+ (match b with
+ Some (x, v1, v2) ->
+ let env1 = push_rel (x,None,v1) env in
+ let (evd'', v2', t2') = inh_conv_coerce_to_fail loc env1 evd'
+ (Some v2) t2 u2 in
+ (evd'', option_app (fun v2' -> mkLambda (x, v1, v2')) v2',
+ mkProd (x, v1, t2'))
+ | None ->
+ (* Mismatch on t1 and u1 or not a lambda: we eta-expand *)
+ (* we look for a coercion c:u1->t1 s.t. [name:u1](v' (c x)) *)
+ (* has type (name:u1)u2 (with v' recursively obtained) *)
+ let name = (match name with
+ | Anonymous -> Name (id_of_string "x")
+ | _ -> name) in
+ let env1 = push_rel (name,None,u1) env in
+ let (evd', v1', t1') =
+ inh_conv_coerce_to_fail loc env1 isevars
+ (Some (mkRel 1)) (lift 1 u1) (lift 1 t1)
+ in
+ let (evd'', v2', t2') =
+ let v2 =
+ match v with
+ Some v -> option_app (fun v1' -> mkApp (lift 1 v, [|v1'|])) v1'
+ | None -> None
+ and evd', t2 =
+ match v1' with
+ Some v1' -> evd', subst1 v1' t2
+ | None ->
+ let evd', ev = new_evar evd' env ~src:(loc, InternalHole) t1' in
+ evd', subst1 ev t2
+ in
+ inh_conv_coerce_to_fail loc env1 evd' v2 t2 u2
+ in
+ (evd'', option_app (fun v2' -> mkLambda (name, u1, v2')) v2',
+ mkProd (name, u1, t2')))
| _ -> raise NoCoercion))
-
+
(* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
- let inh_conv_coerce_to loc env isevars cj t =
- let (evd',cj') =
- try
- inh_conv_coerce_to_fail env isevars cj t
- with NoCoercion ->
- let sigma = evars_of isevars in
- error_actual_type_loc loc env sigma cj t
+ let inh_conv_coerce_to loc env isevars cj (n, t) =
+ if n = 0 then
+ let (evd', val', type') =
+ try
+ inh_conv_coerce_to_fail loc env isevars (Some cj.uj_val) cj.uj_type t
+ with NoCoercion ->
+ let sigma = evars_of isevars in
+ error_actual_type_loc loc env sigma cj t
+ in
+ let val' = match val' with Some v -> v | None -> assert(false) in
+ (evd',{ uj_val = val'; uj_type = t })
+ else
+ (isevars, cj)
+
+ open Pp
+ let inh_conv_coerces_to loc env isevars t (abs, t') = isevars
+ (* Still bugguy
+(* (try *)
+(* msgnl (str "inh_conv_coerces_to called for " ++ *)
+(* Termops.print_constr_env env t ++ str " and "++ spc () ++ *)
+(* Evarutil.pr_tycon_type env tycon ++ str " with evars: " ++ spc () ++ *)
+(* Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++ *)
+(* Termops.print_env env); *)
+(* with _ -> ()); *)
+ try let (rels, rng) =
+ (* a little more effort to get products is needed *)
+ try decompose_prod_n abs t
+ with _ ->
+ raise (Invalid_argument "Coercion.inh_conv_coerces_to")
in
- (evd',{ uj_val = cj'.uj_val; uj_type = t })
+ if noccur_between 0 (succ abs) rng then (
+ (* msgnl (str "No occur between 0 and " ++ int (succ abs)); *)
+ let env', t, t' =
+ let env' = List.fold_right (fun (n, t) env -> push_rel (n, None, t) env) rels env in
+ env', rng, lift abs t'
+ in
+ try
+ pi1 (inh_conv_coerce_to_fail loc env' isevars None t t')
+ with NoCoercion ->
+ isevars) (* Maybe not enough information to unify *)
+ (*let sigma = evars_of isevars in
+ error_cannot_coerce env' sigma (t, t'))*)
+ else isevars
+ with Invalid_argument _ -> isevars *)
end
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index cc2211f5f8..667f207307 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -38,8 +38,14 @@ module type S = sig
[t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and
[j.uj_type] are convertible; it fails if no coercion is applicable *)
val inh_conv_coerce_to : loc ->
- env -> evar_defs -> unsafe_judgment -> types -> evar_defs * unsafe_judgment
-
+ env -> evar_defs -> unsafe_judgment -> type_constraint_type -> evar_defs * unsafe_judgment
+
+ (* [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t]
+ is coercible to an object of type [t'] adding evar constraints if needed;
+ it fails if no coercion exists *)
+ val inh_conv_coerces_to : loc ->
+ env -> evar_defs -> types -> type_constraint_type -> evar_defs
+
(* [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases
pattern [pat] typed in [ind1] into a pattern typed in [ind2];
raises [Not_found] if no coercion found *)
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index ec8fcd2a8c..e9f605ecb5 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -67,6 +67,17 @@ let nf_evar_info evc info =
evar_hyps = map_named_val (Reductionops.nf_evar evc) info.evar_hyps;
evar_body = info.evar_body}
+let nf_evars evm = Evd.fold (fun ev evi evm' -> Evd.add evm' ev (nf_evar_info evm evi))
+ evm Evd.empty
+
+let nf_evar_defs isevars = Evd.evars_reset_evd (nf_evars (Evd.evars_of isevars)) isevars
+
+let nf_isevar isevars = nf_evar (Evd.evars_of isevars)
+let j_nf_isevar isevars = j_nf_evar (Evd.evars_of isevars)
+let jl_nf_isevar isevars = jl_nf_evar (Evd.evars_of isevars)
+let jv_nf_isevar isevars = jv_nf_evar (Evd.evars_of isevars)
+let tj_nf_isevar isevars = tj_nf_evar (Evd.evars_of isevars)
+
(**********************)
(* Creating new metas *)
(**********************)
@@ -545,7 +556,9 @@ let solve_simple_eqn conv_algo env isevars (pbty,(n1,args1 as ev1),t2) =
(* Operations on value/type constraints *)
-type type_constraint = constr option
+type type_constraint_type = int * constr
+type type_constraint = type_constraint_type option
+
type val_constraint = constr option
(* Old comment...
@@ -565,8 +578,13 @@ type val_constraint = constr option
(* The empty type constraint *)
let empty_tycon = None
+let mk_tycon_type c = (0, c)
+let mk_abstr_tycon_type n c = (n, c)
+
(* Builds a type constraint *)
-let mk_tycon ty = Some ty
+let mk_tycon ty = Some (mk_tycon_type ty)
+
+let mk_abstr_tycon n ty = Some (mk_abstr_tycon_type n ty)
(* Constrains the value of a type *)
let empty_valcon = None
@@ -579,7 +597,7 @@ let mk_valcon c = Some c
(* Declaring any type to be in the sort Type shouldn't be harmful since
cumulativity now includes Prop and Set in Type...
It is, but that's not too bad *)
-let define_evar_as_arrow evd (ev,args) =
+let define_evar_as_abstraction abs evd (ev,args) =
let evi = Evd.map (evars_of evd) ev in
let evenv = evar_env evi in
let (evd1,dom) = new_evar evd evenv (new_Type()) in
@@ -589,14 +607,20 @@ let define_evar_as_arrow evd (ev,args) =
let newenv = push_named (nvar, None, dom) evenv in
let (evd2,rng) =
new_evar evd1 newenv ~src:(evar_source ev evd1) (new_Type()) in
- let prod = mkProd (Name nvar, dom, subst_var nvar rng) in
+ let prod = abs (Name nvar, dom, subst_var nvar rng) in
let evd3 = Evd.evar_define ev prod evd2 in
let evdom = fst (destEvar dom), args in
let evrng =
fst (destEvar rng), array_cons (mkRel 1) (Array.map (lift 1) args) in
- let prod' = mkProd (Name nvar, mkEvar evdom, mkEvar evrng) in
+ let prod' = abs (Name nvar, mkEvar evdom, mkEvar evrng) in
(evd3,prod')
+let define_evar_as_arrow evd (ev,args) =
+ define_evar_as_abstraction (fun t -> mkProd t) evd (ev,args)
+
+let define_evar_as_lambda evd (ev,args) =
+ define_evar_as_abstraction (fun t -> mkLambda t) evd (ev,args)
+
let define_evar_as_sort isevars (ev,args) =
let s = new_Type () in
Evd.evar_define ev s isevars, destSort s
@@ -612,20 +636,44 @@ let judge_of_new_Type () = Typeops.judge_of_type (new_univ ())
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 isevars = function
- | None -> isevars,(Anonymous,None,None)
- | Some c ->
- let sigma = evars_of isevars in
- let t = whd_betadeltaiota env sigma c in
+let split_tycon loc env isevars tycon =
+ let rec real_split c =
+ let sigma = evars_of isevars in
+ let t = whd_betadeltaiota env sigma c in
match kind_of_term t with
- | Prod (na,dom,rng) -> isevars, (na, Some dom, Some rng)
+ | Prod (na,dom,rng) -> isevars, (na, mk_tycon dom, mk_tycon rng)
| Evar ev when not (Evd.is_defined_evar isevars ev) ->
let (isevars',prod) = define_evar_as_arrow isevars ev in
- let (_,dom,rng) = destProd prod in
- isevars',(Anonymous, Some dom, Some rng)
+ let (_,dom,rng) = destProd prod in
+ isevars',(Anonymous, mk_tycon dom, mk_tycon rng)
| _ -> error_not_product_loc loc env sigma c
-
-let valcon_of_tycon x = x
-
-let lift_tycon = option_app (lift 1)
+ in
+ match tycon with
+ | None -> isevars,(Anonymous,None,None)
+ | Some (abs, c) ->
+ if abs = 0 then real_split c
+ else if abs = 1 then
+ isevars, (Anonymous, None, mk_tycon c)
+ else
+ isevars, (Anonymous, None, Some (pred abs, c))
+
+let valcon_of_tycon x =
+ match x with
+ | Some (0, t) -> Some t
+ | _ -> None
+
+let lift_tycon_type n (abs, c) =
+ let abs' = abs + n in
+ if abs' < 0 then raise (Invalid_argument "lift_tycon_type")
+ else (abs', c)
+
+let lift_tycon n = option_app (lift_tycon_type n)
+
+let pr_tycon_type env (abs, t) =
+ if abs = 0 then Termops.print_constr_env env t
+ else str "Abstract " ++ int abs ++ str " " ++ Termops.print_constr_env env t
+
+let pr_tycon env = function
+ None -> str "None"
+ | Some t -> pr_tycon_type env t
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 8550258c45..7260b5ad35 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -79,6 +79,7 @@ val solve_simple_eqn :
evar_defs * bool
val define_evar_as_arrow : evar_defs -> existential -> evar_defs * types
+val define_evar_as_lambda : evar_defs -> existential -> evar_defs * types
val define_evar_as_sort : evar_defs -> existential -> evar_defs * sorts
(***********************************************************)
@@ -86,11 +87,16 @@ val define_evar_as_sort : evar_defs -> existential -> evar_defs * sorts
val judge_of_new_Type : unit -> unsafe_judgment
-type type_constraint = constr option
+type type_constraint_type = int * constr
+type type_constraint = type_constraint_type option
+
type val_constraint = constr option
val empty_tycon : type_constraint
+val mk_tycon_type : constr -> type_constraint_type
+val mk_abstr_tycon_type : int -> constr -> type_constraint_type
val mk_tycon : constr -> type_constraint
+val mk_abstr_tycon : int -> constr -> type_constraint
val empty_valcon : val_constraint
val mk_valcon : constr -> val_constraint
@@ -100,7 +106,8 @@ val split_tycon :
val valcon_of_tycon : type_constraint -> val_constraint
-val lift_tycon : type_constraint -> type_constraint
+val lift_tycon_type : int -> type_constraint_type -> type_constraint_type
+val lift_tycon : int -> type_constraint -> type_constraint
(***********************************************************)
@@ -117,8 +124,27 @@ val tj_nf_evar :
evar_map -> unsafe_type_judgment -> unsafe_type_judgment
val nf_evar_info : evar_map -> evar_info -> evar_info
+val nf_evars : evar_map -> evar_map
+
+(* Same for evar defs *)
+val nf_isevar : evar_defs -> constr -> constr
+val j_nf_isevar : evar_defs -> unsafe_judgment -> unsafe_judgment
+val jl_nf_isevar :
+ evar_defs -> unsafe_judgment list -> unsafe_judgment list
+val jv_nf_isevar :
+ evar_defs -> unsafe_judgment array -> unsafe_judgment array
+val tj_nf_isevar :
+ evar_defs -> unsafe_type_judgment -> unsafe_type_judgment
+
+val nf_evar_defs : evar_defs -> evar_defs
(* Replacing all evars *)
exception Uninstantiated_evar of existential_key
val whd_ise : evar_map -> constr -> constr
val whd_castappevar : evar_map -> constr -> constr
+
+(*********************************************************************)
+(* debug pretty-printer: *)
+
+val pr_tycon_type : env -> type_constraint_type -> Pp.std_ppcmds
+val pr_tycon : env -> type_constraint -> Pp.std_ppcmds
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 26df8f7938..5da0a1a999 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -408,6 +408,13 @@ let is_undefined_evar isevars c = match kind_of_term c with
| Evar ev -> not (is_defined_evar isevars ev)
| _ -> false
+let undefined_evars isevars =
+ let evd =
+ fold (fun ev evi sigma -> if evi.evar_body = Evar_empty then
+ add sigma ev evi else sigma)
+ isevars.evars empty
+ in
+ { isevars with evars = evd }
(* extracts conversion problems that satisfy predicate p *)
(* Note: conv_pbs not satisying p are stored back in reverse order *)
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 2f51ebf2d3..35bcb67c70 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -126,6 +126,7 @@ type hole_kind =
| TomatchTypeParameter of inductive * int
val is_defined_evar : evar_defs -> existential -> bool
val is_undefined_evar : evar_defs -> constr -> bool
+val undefined_evars : evar_defs -> evar_defs
val evar_declare :
Environ.named_context_val -> evar -> types -> ?src:loc * hole_kind ->
evar_defs -> evar_defs
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index d87a26c223..a0f69e701b 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -157,6 +157,9 @@ let error_unsolvable_implicit loc env sigma e =
let error_cannot_unify env sigma (m,n) =
raise (PretypeError (env_ise sigma env,CannotUnify (m,n)))
+let error_cannot_coerce env sigma (m,n) =
+ raise (PretypeError (env_ise sigma env,CannotUnify (m,n)))
+
(*s Ml Case errors *)
let error_cant_find_case_type_loc loc env sigma expr =
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index dc8fdd03d9..ad8293a3c7 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -82,6 +82,8 @@ val error_ill_typed_rec_body_loc :
val error_not_a_type_loc :
loc -> env -> Evd.evar_map -> unsafe_judgment -> 'b
+val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b
+
(*s Implicit arguments synthesis errors *)
val error_occur_check : env -> Evd.evar_map -> existential_key -> constr -> 'b
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index b99ada7693..217a9714be 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -72,6 +72,9 @@ sig
val understand_tcc :
evar_map -> env -> ?expected_type:types -> rawconstr -> open_constr
+
+ val understand_tcc_evars :
+ evar_defs ref -> env -> typing_constraint -> rawconstr -> constr
(* More general entry point with evars from ltac *)
@@ -109,7 +112,7 @@ sig
(* Idem but do not fail on unresolved evars *)
- val understand_judgment_tcc : evar_map -> env -> rawconstr -> evar_map * unsafe_judgment
+ val understand_judgment_tcc : evar_defs ref -> env -> rawconstr -> unsafe_judgment
(*i*)
(* Internal of Pretyping...
@@ -189,7 +192,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
(* coerce to tycon if any *)
let inh_conv_coerce_to_tycon loc env isevars j = function
| None -> j
- | Some typ -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) isevars j typ
+ | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) isevars j t
let push_rels vars env = List.fold_right push_rel vars env
@@ -256,8 +259,14 @@ module Pretyping_F (Coercion : Coercion.S) = struct
(* [pretype tycon env isevars lvar lmeta cstr] attempts to type [cstr] *)
(* in environment [env], with existential variables [(evars_of isevars)] and *)
(* the type constraint tycon *)
- let rec pretype tycon env isevars lvar = function
-
+ let rec pretype (tycon : type_constraint) env isevars lvar c =
+(* (try
+ msgnl (str "pretype with tycon: " ++
+ Evarutil.pr_tycon env tycon ++ str " with evars: " ++ spc () ++
+ Evd.pr_evar_defs !isevars ++ str " in env: " ++ spc () ++
+ Termops.print_env env);
+ with _ -> ());*)
+ match c with
| RRef (loc,ref) ->
inh_conv_coerce_to_tycon loc env isevars
(pretype_ref isevars env ref)
@@ -285,8 +294,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct
| RHole (loc,k) ->
let ty =
match tycon with
- | Some ty -> ty
- | None ->
+ | Some (n, ty) when n = 0 -> ty
+ | None | Some _ ->
e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ()) in
{ uj_val = e_new_evar isevars env ~src:(loc,k) ty; uj_type = ty }
@@ -344,31 +353,48 @@ module Pretyping_F (Coercion : Coercion.S) = struct
inh_conv_coerce_to_tycon loc env isevars (pretype_sort s) tycon
| RApp (loc,f,args) ->
- let fj = pretype empty_tycon env isevars lvar f in
- let floc = loc_of_rawconstr f in
- let rec apply_rec env n resj = function
+ let length = List.length args in
+ let ftycon =
+ match tycon with
+ None -> None
+ | Some (n, ty) ->
+ if n = 0 then mk_abstr_tycon length ty
+ else Some (n + length, ty)
+ in
+ let fj = pretype ftycon env isevars lvar f in
+ let floc = loc_of_rawconstr f in
+ let rec apply_rec env n resj tycon = function
| [] -> resj
| c::rest ->
let argloc = loc_of_rawconstr c in
let resj = evd_comb1 (Coercion.inh_app_fun env) isevars resj in
- let resty =
- whd_betadeltaiota env (evars_of !isevars) resj.uj_type in
+ let resty = whd_betadeltaiota env (evars_of !isevars) resj.uj_type in
match kind_of_term resty with
| Prod (na,c1,c2) ->
let hj = pretype (mk_tycon c1) env isevars lvar c in
- let newresj =
- { uj_val = applist (j_val resj, [j_val hj]);
- uj_type = subst1 hj.uj_val c2 } in
- apply_rec env (n+1) newresj rest
+ let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in
+ let typ' = nf_isevar !isevars typ in
+ let tycon =
+ match tycon with
+ Some (abs, ty) ->
+ isevars := Coercion.inh_conv_coerces_to loc env !isevars typ'
+ (abs, ty);
+ Some (pred abs, nf_isevar !isevars ty)
+ | None -> None
+ in
+ apply_rec env (n+1)
+ { uj_val = nf_isevar !isevars value;
+ uj_type = nf_isevar !isevars typ' }
+ tycon rest
| _ ->
let hj = pretype empty_tycon env isevars lvar c in
error_cant_apply_not_functional_loc
(join_loc floc argloc) env (evars_of !isevars)
resj [hj]
-
- in
- let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj args) in
+ in
+ let ftycon = lift_tycon (-1) ftycon in
+ let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj ftycon args) in
let resj =
match kind_of_term resj.uj_val with
| App (f,args) when isInd f ->
@@ -402,7 +428,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
let j = pretype empty_tycon env isevars lvar c1 in
let t = refresh_universes j.uj_type in
let var = (name,Some j.uj_val,t) in
- let tycon = option_app (lift 1) tycon in
+ let tycon = lift_tycon 1 tycon in
let j' = pretype tycon (push_rel var env) isevars lvar c2 in
{ uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ;
uj_type = subst1 j.uj_val j'.uj_type }
@@ -454,7 +480,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
{ uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl }
| None ->
- let tycon = option_app (lift cs.cs_nargs) tycon in
+ let tycon = lift_tycon cs.cs_nargs tycon in
let fj = pretype tycon env_f isevars lvar d in
let f = it_mkLambda_or_LetIn fj.uj_val fsign in
let ccl = nf_evar (evars_of !isevars) fj.uj_type in
@@ -499,17 +525,24 @@ module Pretyping_F (Coercion : Coercion.S) = struct
let pj = pretype_type empty_valcon env_p isevars lvar p in
let ccl = nf_evar (evars_of !isevars) pj.utj_val in
let pred = it_mkLambda_or_LetIn ccl psign in
- pred, lift (- nar) (beta_applist (pred,[cj.uj_val]))
+ let typ = lift (- nar) (beta_applist (pred,[cj.uj_val])) in
+ let jtyp = inh_conv_coerce_to_tycon loc env isevars {uj_val = pred;
+ uj_type = typ} tycon
+ in
+ jtyp.uj_val, jtyp.uj_type
| None ->
let p = match tycon with
- | Some ty -> ty
- | None ->
+ | Some (n, ty) when n = 0 -> ty
+ | None | Some _ ->
e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ())
in
it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
+ let pred = nf_evar (evars_of !isevars) pred in
+ let p = nf_evar (evars_of !isevars) p in
+ (* msgnl (str "Pred is: " ++ Termops.print_constr_env env pred);*)
let f cs b =
let n = rel_context_length cs.cs_args in
- let pi = liftn n 2 pred in
+ let pi = lift n pred in (* liftn n 2 pred ? *)
let pi = beta_applist (pi, [build_dependent_constructor cs]) in
let csgn =
if not !allow_anonymous_refs then
@@ -523,12 +556,11 @@ module Pretyping_F (Coercion : Coercion.S) = struct
cs.cs_args
in
let env_c = push_rels csgn env in
- let bj = pretype (Some pi) env_c isevars lvar b in
+(* msgnl (str "Pi is: " ++ Termops.print_constr_env env_c pi); *)
+ let bj = pretype (mk_tycon pi) env_c isevars lvar b in
it_mkLambda_or_LetIn bj.uj_val cs.cs_args in
let b1 = f cstrs.(0) b1 in
let b2 = f cstrs.(1) b2 in
- let pred = nf_evar (evars_of !isevars) pred in
- let p = nf_evar (evars_of !isevars) p in
let v =
let mis,_ = dest_ind_family indf in
let ci = make_default_case_info env IfStyle mis in
@@ -542,7 +574,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
tycon env (* loc *) (po,tml,eqns)
| RCast(loc,c,k,t) ->
- let tj = pretype_type empty_tycon env isevars lvar t in
+ let tj = pretype_type empty_valcon env isevars lvar t in
let cj = pretype (mk_tycon tj.utj_val) env isevars lvar c in
(* User Casts are for helping pretyping, experimentally not to be kept*)
(* ... except for Correctness *)
@@ -641,22 +673,21 @@ module Pretyping_F (Coercion : Coercion.S) = struct
check_evars env sigma isevars (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
j
- let understand_judgment_tcc sigma env c =
- let isevars = ref (create_evar_defs sigma) in
+ let understand_judgment_tcc isevars env c =
let j = pretype empty_tycon env isevars ([],[]) c in
let sigma = evars_of !isevars in
let j = j_nf_evar sigma j in
- sigma, j
+ j
(* Raw calls to the unsafe inference machine: boolean says if we must
fail on unresolved evars; the unsafe_judgment list allows us to
extend env with some bindings *)
let ise_pretype_gen fail_evar sigma env lvar kind c =
- let isevars = ref (create_evar_defs sigma) in
+ let isevars = ref (Evd.create_evar_defs sigma) in
let c = pretype_gen isevars env lvar kind c in
if fail_evar then check_evars env sigma isevars c;
- (!isevars, c)
+ !isevars, c
(** Entry points of the high-level type synthesis algorithm *)
@@ -671,10 +702,13 @@ module Pretyping_F (Coercion : Coercion.S) = struct
let understand_ltac sigma env lvar kind c =
ise_pretype_gen false sigma env lvar kind c
+
+ let understand_tcc_evars isevars env kind c =
+ pretype_gen isevars env ([],[]) kind c
let understand_tcc sigma env ?expected_type:exptyp c =
- let evars,c = ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c in
- evars_of evars,c
+ let ev, t = ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c in
+ Evd.evars_of ev, t
end
module Default : S = Pretyping_F(Coercion.Default)
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index ac8e6fec78..ca1a1ded4c 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -38,6 +38,9 @@ sig
val understand_tcc :
evar_map -> env -> ?expected_type:types -> rawconstr -> open_constr
+ val understand_tcc_evars :
+ evar_defs ref -> env -> typing_constraint -> rawconstr -> constr
+
(* More general entry point with evars from ltac *)
(* Generic call to the interpreter from rawconstr to constr, failing
@@ -73,7 +76,7 @@ sig
val understand_judgment : evar_map -> env -> rawconstr -> unsafe_judgment
(* Idem but do not fail on unresolved evars *)
- val understand_judgment_tcc : evar_map -> env -> rawconstr -> evar_map * unsafe_judgment
+ val understand_judgment_tcc : evar_defs ref -> env -> rawconstr -> unsafe_judgment
(*i*)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:05:37 +0000