aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile1
-rw-r--r--contrib/subtac/Utils.v28
-rw-r--r--contrib/subtac/subtac_coercion.ml11
-rw-r--r--contrib/subtac/subtac_command.ml6
-rw-r--r--contrib/subtac/subtac_interp_fixpoint.ml68
-rw-r--r--contrib/subtac/subtac_interp_fixpoint.mli7
-rw-r--r--contrib/subtac/subtac_pretyping.ml3
-rw-r--r--contrib/subtac/subtac_pretyping_F.ml639
-rw-r--r--contrib/subtac/subtac_utils.ml78
-rw-r--r--contrib/subtac/subtac_utils.mli2
-rw-r--r--contrib/subtac/test/ListsTest.v44
-rw-r--r--interp/topconstr.ml6
-rw-r--r--interp/topconstr.mli6
-rw-r--r--parsing/g_constr.ml48
-rw-r--r--parsing/g_proofs.ml42
-rw-r--r--parsing/g_xml.ml42
-rw-r--r--pretyping/cases.ml7
-rw-r--r--pretyping/coercion.ml8
-rw-r--r--pretyping/coercion.mli8
-rw-r--r--pretyping/detyping.ml2
-rw-r--r--pretyping/pretyping.ml51
-rw-r--r--pretyping/rawterm.ml6
-rw-r--r--pretyping/rawterm.mli6
-rw-r--r--toplevel/command.ml2
-rw-r--r--toplevel/record.ml2
25 files changed, 829 insertions, 174 deletions
diff --git a/Makefile b/Makefile
index 70e20ac72e..fe8d729084 100644
--- a/Makefile
+++ b/Makefile
@@ -301,6 +301,7 @@ SUBTACCMO=\
contrib/subtac/context.cmo \
contrib/subtac/subtac_errors.cmo \
contrib/subtac/subtac_coercion.cmo \
+ contrib/subtac/subtac_pretyping_F.cmo \
contrib/subtac/subtac_pretyping.cmo \
contrib/subtac/subtac_interp_fixpoint.cmo \
contrib/subtac/subtac_command.cmo \
diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v
index 9acb10aeff..db10cb2a1b 100644
--- a/contrib/subtac/Utils.v
+++ b/contrib/subtac/Utils.v
@@ -1,20 +1,17 @@
Set Implicit Arguments.
+Notation "'fun' { x : A | P } => Q" :=
+ (fun x:{x:A|P} => Q)
+ (at level 200, x ident, right associativity).
+
+Notation "( x & y )" := (@existS _ _ x y) : core_scope.
+
Definition ex_pi1 (A : Prop) (P : A -> Prop) (t : ex P) : A.
intros.
induction t.
exact x.
Defined.
-Check proj1_sig.
-Lemma subset_simpl : forall (A : Set) (P : A -> Prop)
- (t : sig P), P (proj1_sig t).
-Proof.
-intros.
-induction t.
- simpl ; auto.
-Qed.
-
Lemma ex_pi2 : forall (A : Prop) (P : A -> Prop) (t : ex P),
P (ex_pi1 t).
intros A P.
@@ -23,12 +20,17 @@ simpl.
exact p.
Defined.
+
+Notation "` t" := (proj1_sig t) (at level 100) : core_scope.
Notation "'forall' { x : A | P } , Q" :=
(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).
+Lemma subset_simpl : forall (A : Set) (P : A -> Prop)
+ (t : sig P), P (` t).
+Proof.
+intros.
+induction t.
+ simpl ; auto.
+Qed.
-Notation "( x & y )" := (@existS _ _ x y) : core_scope.
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index 4a9cf8eb47..cdad003721 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -97,7 +97,7 @@ module Coercion = struct
app_opt f (mkApp ((Lazy.force sig_).proj1,
[| u; p; x |]))),
ct)
- | None -> (None, t)
+ | None -> (None, v)
in aux t
and coerce loc env isevars (x : Term.constr) (y : Term.constr)
@@ -153,7 +153,7 @@ module Coercion = struct
if i = Term.destInd existS.typ
then
begin
- debug 1 (str "In coerce sigma types");
+ trace (str "In coerce sigma types");
let (a, pb), (a', pb') =
pair_of_array l, pair_of_array l'
in
@@ -339,6 +339,13 @@ module Coercion = struct
| _ ->
inh_tosort_force loc env isevars j
+ let inh_coerce_to_base loc env isevars j =
+ let typ = whd_betadeltaiota env (evars_of isevars) j.uj_type in
+ let ct, typ' = mu env isevars typ in
+ isevars, { uj_val = app_opt ct j.uj_val;
+ uj_type = typ' }
+
+
let inh_coerce_to_fail env isevars c1 v t =
let v', t' =
try
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 24edeba699..552acf137d 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -55,8 +55,8 @@ 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
- msgnl (str "Pretyping " ++ my_print_constr_expr c);
+ let c' = Subtac_utils.rewrite_cases env c' in
+ trace (str "Pretyping " ++ my_print_constr_expr c);
let c' = SPretyping.pretype_gen isevars env ([],[]) kind c' in
evar_nf isevars c'
@@ -339,13 +339,13 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
let evm = Evd.evars_of isevars in
let _, _, typ = arrec.(i) in
let id = namerec.(i) in
- let evars_def, evars_typ, evars = Eterm.eterm_term evm def (Some typ) 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 =
diff --git a/contrib/subtac/subtac_interp_fixpoint.ml b/contrib/subtac/subtac_interp_fixpoint.ml
index 599dbe39e2..858fad1a8b 100644
--- a/contrib/subtac/subtac_interp_fixpoint.ml
+++ b/contrib/subtac/subtac_interp_fixpoint.ml
@@ -110,7 +110,7 @@ let rewrite_fixpoint env l (f, decl) =
let body =
(* cast or we will loose some info at pretyping time as body
is a function *)
- CCast (dummy_loc, body, DEFAULTcast, typ)
+ CCast (dummy_loc, body, CastConv DEFAULTcast, typ)
in
let body' = (* body abstracted by rec call *)
mkLambdaC ([(dummy_loc, Name id)], internal_type, body)
@@ -151,69 +151,3 @@ let rewrite_fixpoint env l (f, decl) =
Ppconstr.pr_constr_expr body')
in (id, (succ n, ro), bl', typ, body'), decl
-let list_mapi f =
- let rec aux i = function
- hd :: tl -> f i hd :: aux (succ i) tl
- | [] -> []
- in aux 0
-
-let rewrite_cases_aux (loc, po, tml, eqns) =
- let tml = list_mapi (fun i (c, (n, opt)) -> c,
- ((match n with
- Name id -> (match c with
- | RVar (_, id') when id = id' ->
- Name (id_of_string (string_of_id id ^ "'"))
- | _ -> n)
- | Anonymous -> Name (id_of_string ("x" ^ string_of_int i))),
- opt)) tml
- in
- let mkHole = RHole (dummy_loc, InternalHole) in
- let mkeq c n = RApp (dummy_loc, RRef (dummy_loc, (Lazy.force eqind_ref)),
- [mkHole; c; n])
- in
- let eqs_types =
- List.map
- (fun (c, (n, _)) ->
- let id = match n with Name id -> id | _ -> assert false in
- let heqid = id_of_string ("Heq" ^ string_of_id id) in
- Name heqid, mkeq c (RVar (dummy_loc, id)))
- tml
- in
- let po =
- List.fold_right
- (fun (n,t) acc ->
- RProd (dummy_loc, Anonymous, t, acc))
- eqs_types (match po with
- Some e -> e
- | None -> mkHole)
- in
- let eqns =
- List.map (fun (loc, idl, cpl, c) ->
- let c' =
- List.fold_left
- (fun acc (n, t) ->
- RLambda (dummy_loc, n, mkHole, acc))
- c eqs_types
- in (loc, idl, cpl, c'))
- eqns
- in
- let mk_refl_equal c = RApp (dummy_loc, RRef (dummy_loc, Lazy.force refl_equal_ref),
- [mkHole; c])
- in
- let refls = List.map (fun (c, _) -> mk_refl_equal c) tml in
- let case = RCases (loc,Some po,tml,eqns) in
- let app = RApp (dummy_loc, case, refls) in
- app
-
-let rec rewrite_cases c =
- match c with
- RCases _ -> let c' = map_rawconstr rewrite_cases c in
- (match c' with
- | RCases (x, y, z, w) -> rewrite_cases_aux (x,y,z,w)
- | _ -> assert(false))
- | _ -> map_rawconstr rewrite_cases c
-
-let rewrite_cases env c =
- let c' = rewrite_cases c in
- let _ = trace (str "Rewrote cases: " ++ spc () ++ my_print_rawconstr env c') in
- c'
diff --git a/contrib/subtac/subtac_interp_fixpoint.mli b/contrib/subtac/subtac_interp_fixpoint.mli
index 128511c137..fafbb2da53 100644
--- a/contrib/subtac/subtac_interp_fixpoint.mli
+++ b/contrib/subtac/subtac_interp_fixpoint.mli
@@ -26,10 +26,3 @@ val rewrite_fixpoint :
Topconstr.local_binder list * Topconstr.constr_expr *
Topconstr.constr_expr) *
'c
-val list_mapi : (int -> 'a -> 'b) -> 'a list -> 'b list
-val rewrite_cases_aux :
- Util.loc * Rawterm.rawconstr option *
- Rawterm.tomatch_tuple * Rawterm.cases_clauses
- -> Rawterm.rawconstr
-
-val rewrite_cases : Environ.env -> Rawterm.rawconstr -> Rawterm.rawconstr
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index f73a6e393d..1d37900f16 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -39,7 +39,7 @@ open Subtac_errors
open Context
open Eterm
-module Pretyping = Pretyping.Pretyping_F(Subtac_coercion.Coercion)
+module Pretyping = Subtac_pretyping_F.SubtacPretyping_F(Subtac_coercion.Coercion)
open Pretyping
@@ -128,6 +128,7 @@ let subtac_process env isevars id l c tycon =
mk_tycon coqt
in
let c = coqintern !isevars env_binders c in
+ let c = Subtac_utils.rewrite_cases env c in
let _ = trace (str "Internalized term: " ++ my_print_rawconstr env c) in
let coqc, ctyp = interp env_binders isevars c tycon in
let _ = trace (str "Interpreted term: " ++ my_print_constr env_binders coqc ++ spc () ++
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
new file mode 100644
index 0000000000..823ff41af6
--- /dev/null
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -0,0 +1,639 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Names
+open Sign
+open Evd
+open Term
+open Termops
+open Reductionops
+open Environ
+open Type_errors
+open Typeops
+open Libnames
+open Nameops
+open Classops
+open List
+open Recordops
+open Evarutil
+open Pretype_errors
+open Rawterm
+open Evarconv
+open Pattern
+open Dyn
+open Pretyping
+
+(************************************************************************)
+(* This concerns Cases *)
+open Declarations
+open Inductive
+open Inductiveops
+
+module SubtacPretyping_F (Coercion : Coercion.S) = struct
+
+ module Cases = Cases.Cases_F(Coercion)
+
+ (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
+ let allow_anonymous_refs = ref false
+
+ let evd_comb0 f isevars =
+ let (evd',x) = f !isevars in
+ isevars := evd';
+ x
+
+ let evd_comb1 f isevars x =
+ let (evd',y) = f !isevars x in
+ isevars := evd';
+ y
+
+ let evd_comb2 f isevars x y =
+ let (evd',z) = f !isevars x y in
+ isevars := evd';
+ z
+
+ let evd_comb3 f isevars x y z =
+ let (evd',t) = f !isevars x y z in
+ isevars := evd';
+ t
+
+ let mt_evd = Evd.empty
+
+ let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t)
+
+ (* Utilisé pour inférer le prédicat des Cases *)
+ (* Semble exagérement fort *)
+ (* Faudra préférer une unification entre les types de toutes les clauses *)
+ (* et autoriser des ? à rester dans le résultat de l'unification *)
+
+ let evar_type_fixpoint loc env isevars lna lar vdefj =
+ let lt = Array.length vdefj in
+ if Array.length lar = lt then
+ for i = 0 to lt-1 do
+ if not (e_cumul env isevars (vdefj.(i)).uj_type
+ (lift lt lar.(i))) then
+ error_ill_typed_rec_body_loc loc env (evars_of !isevars)
+ i lna vdefj lar
+ done
+
+ let check_branches_message loc env isevars c (explft,lft) =
+ for i = 0 to Array.length explft - 1 do
+ if not (e_cumul env isevars lft.(i) explft.(i)) then
+ let sigma = evars_of !isevars in
+ error_ill_formed_branch_loc loc env sigma c i lft.(i) explft.(i)
+ done
+
+ (* coerce to tycon if any *)
+ let inh_conv_coerce_to_tycon loc env isevars j = function
+ | None -> j
+ | 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
+
+ (*
+ let evar_type_case isevars env ct pt lft p c =
+ let (mind,bty,rslty) = type_case_branches env (evars_of isevars) ct pt p c
+ in check_branches_message isevars env (c,ct) (bty,lft); (mind,rslty)
+ *)
+
+ let strip_meta id = (* For Grammar v7 compatibility *)
+ let s = string_of_id id in
+ if s.[0]='$' then id_of_string (String.sub s 1 (String.length s - 1))
+ else id
+
+ let pretype_id loc env (lvar,unbndltacvars) id =
+ let id = strip_meta id in (* May happen in tactics defined by Grammar *)
+ try
+ let (n,typ) = lookup_rel_id id (rel_context env) in
+ { uj_val = mkRel n; uj_type = type_app (lift n) typ }
+ with Not_found ->
+ try
+ List.assoc id lvar
+ with Not_found ->
+ try
+ let (_,_,typ) = lookup_named id env in
+ { uj_val = mkVar id; uj_type = typ }
+ with Not_found ->
+ try (* To build a nicer ltac error message *)
+ match List.assoc id unbndltacvars with
+ | None -> user_err_loc (loc,"",
+ str "variable " ++ pr_id id ++ str " should be bound to a term")
+ | Some id0 -> Pretype_errors.error_var_not_found_loc loc id0
+ with Not_found ->
+ error_var_not_found_loc loc id
+
+ (* make a dependent predicate from an undependent one *)
+
+ let make_dep_of_undep env (IndType (indf,realargs)) pj =
+ let n = List.length realargs in
+ let rec decomp n p =
+ if n=0 then p else
+ match kind_of_term p with
+ | Lambda (_,_,c) -> decomp (n-1) c
+ | _ -> decomp (n-1) (applist (lift 1 p, [mkRel 1]))
+ in
+ let sign,s = decompose_prod_n n pj.uj_type in
+ let ind = build_dependent_inductive env indf in
+ let s' = mkProd (Anonymous, ind, s) in
+ let ccl = lift 1 (decomp n pj.uj_val) in
+ let ccl' = mkLambda (Anonymous, ind, ccl) in
+ {uj_val=lam_it ccl' sign; uj_type=prod_it s' sign}
+
+ (*************************************************************************)
+ (* Main pretyping function *)
+
+ let pretype_ref isevars env ref =
+ let c = constr_of_global ref in
+ make_judge c (Retyping.get_type_of env Evd.empty c)
+
+ let pretype_sort = function
+ | RProp c -> judge_of_prop_contents c
+ | RType _ -> judge_of_new_Type ()
+
+ (* [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 : type_constraint) env isevars lvar = function
+ | RRef (loc,ref) ->
+ inh_conv_coerce_to_tycon loc env isevars
+ (pretype_ref isevars env ref)
+ tycon
+
+ | RVar (loc, id) ->
+ inh_conv_coerce_to_tycon loc env isevars
+ (pretype_id loc env lvar id)
+ tycon
+
+ | REvar (loc, ev, instopt) ->
+ (* Ne faudrait-il pas s'assurer que hyps est bien un
+ sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *)
+ let hyps = evar_context (Evd.find (evars_of !isevars) ev) in
+ let args = match instopt with
+ | None -> instance_from_named_context hyps
+ | Some inst -> failwith "Evar subtitutions not implemented" in
+ let c = mkEvar (ev, args) in
+ let j = (Retyping.get_judgment_of env (evars_of !isevars) c) in
+ inh_conv_coerce_to_tycon loc env isevars j tycon
+
+ | RPatVar (loc,(someta,n)) ->
+ anomaly "Found a pattern variable in a rawterm to type"
+
+ | RHole (loc,k) ->
+ let ty =
+ match tycon with
+ | Some (None, ty) -> 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 }
+
+ | RRec (loc,fixkind,names,bl,lar,vdef) ->
+ let rec type_bl env ctxt = function
+ [] -> ctxt
+ | (na,None,ty)::bl ->
+ let ty' = pretype_type empty_valcon env isevars lvar ty in
+ let dcl = (na,None,ty'.utj_val) in
+ type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl
+ | (na,Some bd,ty)::bl ->
+ let ty' = pretype_type empty_valcon env isevars lvar ty in
+ let bd' = pretype (mk_tycon ty'.utj_val) env isevars lvar ty in
+ let dcl = (na,Some bd'.uj_val,ty'.utj_val) in
+ type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl in
+ let ctxtv = Array.map (type_bl env empty_rel_context) bl in
+ let larj =
+ array_map2
+ (fun e ar ->
+ pretype_type empty_valcon (push_rel_context e env) isevars lvar ar)
+ ctxtv lar in
+ let lara = Array.map (fun a -> a.utj_val) larj in
+ let ftys = array_map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in
+ let nbfix = Array.length lar in
+ let names = Array.map (fun id -> Name id) names in
+ (* Note: bodies are not used by push_rec_types, so [||] is safe *)
+ let newenv = push_rec_types (names,ftys,[||]) env in
+ let vdefj =
+ array_map2_i
+ (fun i ctxt def ->
+ (* we lift nbfix times the type in tycon, because of
+ * the nbfix variables pushed to newenv *)
+ let (ctxt,ty) =
+ decompose_prod_n_assum (rel_context_length ctxt)
+ (lift nbfix ftys.(i)) in
+ let nenv = push_rel_context ctxt newenv in
+ let j = pretype (mk_tycon ty) nenv isevars lvar def in
+ { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt;
+ uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
+ ctxtv vdef in
+ evar_type_fixpoint loc env isevars names ftys vdefj;
+ let fixj = match fixkind with
+ | RFix (vn,i) ->
+ let guard_indexes = Array.mapi
+ (fun i (n,_) -> match n with
+ | Some n -> n
+ | None ->
+ (* Recursive argument was not given by the user : We
+ check that there is only one inductive argument *)
+ let ctx = ctxtv.(i) in
+ let isIndApp t =
+ isInd (fst (decompose_app (strip_head_cast t))) in
+ (* This could be more precise (e.g. do some delta) *)
+ let lb = List.rev_map (fun (_,_,t) -> isIndApp t) ctx in
+ try (list_unique_index true lb) - 1
+ with Not_found ->
+ Util.user_err_loc
+ (loc,"pretype",
+ Pp.str "cannot guess decreasing argument of fix"))
+ vn
+ in
+ let fix = ((guard_indexes, i),(names,ftys,Array.map j_val vdefj)) in
+ (try check_fix env fix with e -> Stdpp.raise_with_loc loc e);
+ make_judge (mkFix fix) ftys.(i)
+ | RCoFix i ->
+ let cofix = (i,(names,ftys,Array.map j_val vdefj)) in
+ (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e);
+ make_judge (mkCoFix cofix) ftys.(i) in
+ inh_conv_coerce_to_tycon loc env isevars fixj tycon
+
+ | RSort (loc,s) ->
+ inh_conv_coerce_to_tycon loc env isevars (pretype_sort s) tycon
+
+ | RApp (loc,f,args) ->
+ let length = List.length args in
+ let ftycon =
+ match tycon with
+ None -> None
+ | Some (None, ty) -> mk_abstr_tycon length ty
+ | Some (Some (init, cur), ty) ->
+ Some (Some (length + init, length + cur), 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
+ match kind_of_term resty with
+ | Prod (na,c1,c2) ->
+ let hj = pretype (mk_tycon c1) env isevars lvar c in
+ 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 =
+ option_map
+ (fun (abs, ty) ->
+ match abs with
+ None ->
+ isevars := Coercion.inh_conv_coerces_to loc env !isevars typ'
+ (abs, ty);
+ (abs, ty)
+ | Some (init, cur) ->
+ isevars := Coercion.inh_conv_coerces_to loc env !isevars typ'
+ (abs, ty);
+ (Some (init, pred cur), ty))
+ tycon
+ in
+ apply_rec env (n+1)
+ { uj_val = nf_isevar !isevars value;
+ uj_type = nf_isevar !isevars typ' }
+ (option_map (fun (abs, c) -> abs, nf_isevar !isevars c) 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 ftycon = option_map (lift_abstr_tycon_type (-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 ->
+ let sigma = evars_of !isevars in
+ let t = Retyping.type_of_inductive_knowing_parameters env sigma (destInd f) args in
+ let s = snd (splay_arity env sigma t) in
+ on_judgment_type (set_inductive_level env s) resj
+ (* Rem: no need to send sigma: no head evar, it's an arity *)
+ | _ -> resj in
+ inh_conv_coerce_to_tycon loc env isevars resj tycon
+
+ | RLambda(loc,name,c1,c2) ->
+ let (name',dom,rng) = evd_comb1 (split_tycon loc env) isevars tycon in
+ let dom_valcon = valcon_of_tycon dom in
+ let j = pretype_type dom_valcon env isevars lvar c1 in
+ let var = (name,None,j.utj_val) in
+ let j' = pretype rng (push_rel var env) isevars lvar c2 in
+ judge_of_abstraction env name j j'
+
+ | RProd(loc,name,c1,c2) ->
+ let j = pretype_type empty_valcon env isevars lvar c1 in
+ let var = (name,j.utj_val) in
+ let env' = push_rel_assum var env in
+ let j' = pretype_type empty_valcon env' isevars lvar c2 in
+ let resj =
+ try judge_of_product env name j j'
+ with TypeError _ as e -> Stdpp.raise_with_loc loc e in
+ inh_conv_coerce_to_tycon loc env isevars resj tycon
+
+ | RLetIn(loc,name,c1,c2) ->
+ 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 = 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 }
+
+ | RLetTuple (loc,nal,(na,po),c,d) ->
+ let cj = pretype empty_tycon env isevars lvar c in
+ let (IndType (indf,realargs)) =
+ try find_rectype env (evars_of !isevars) cj.uj_type
+ with Not_found ->
+ let cloc = loc_of_rawconstr c in
+ error_case_not_inductive_loc cloc env (evars_of !isevars) cj
+ in
+ let cstrs = get_constructors env indf in
+ if Array.length cstrs <> 1 then
+ user_err_loc (loc,"",str "Destructing let is only for inductive types with one constructor");
+ let cs = cstrs.(0) in
+ if List.length nal <> cs.cs_nargs then
+ user_err_loc (loc,"", str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables");
+ let fsign = List.map2 (fun na (_,c,t) -> (na,c,t))
+ (List.rev nal) cs.cs_args in
+ let env_f = push_rels fsign env in
+ (* Make dependencies from arity signature impossible *)
+ let arsgn =
+ let arsgn,_ = get_arity env indf in
+ if not !allow_anonymous_refs then
+ List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn
+ else arsgn
+ in
+ let psign = (na,None,build_dependent_inductive env indf)::arsgn in
+ let nar = List.length arsgn in
+ (match po with
+ | Some p ->
+ let env_p = push_rels psign env in
+ let pj = pretype_type empty_valcon env_p isevars lvar p in
+ let ccl = nf_evar (evars_of !isevars) pj.utj_val in
+ let psign = make_arity_signature env true indf in (* with names *)
+ let p = it_mkLambda_or_LetIn ccl psign in
+ let inst =
+ (Array.to_list cs.cs_concl_realargs)
+ @[build_dependent_constructor cs] in
+ let lp = lift cs.cs_nargs p in
+ let fty = hnf_lam_applist env (evars_of !isevars) lp inst in
+ let fj = pretype (mk_tycon fty) env_f isevars lvar d in
+ let f = it_mkLambda_or_LetIn fj.uj_val fsign in
+ let v =
+ let mis,_ = dest_ind_family indf in
+ let ci = make_default_case_info env LetStyle mis in
+ mkCase (ci, p, cj.uj_val,[|f|]) in
+ { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl }
+
+ | None ->
+ 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
+ let ccl =
+ if noccur_between 1 cs.cs_nargs ccl then
+ lift (- cs.cs_nargs) ccl
+ else
+ error_cant_find_case_type_loc loc env (evars_of !isevars)
+ cj.uj_val in
+ let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
+ let v =
+ let mis,_ = dest_ind_family indf in
+ let ci = make_default_case_info env LetStyle mis in
+ mkCase (ci, p, cj.uj_val,[|f|] )
+ in
+ { uj_val = v; uj_type = ccl })
+
+ | RIf (loc,c,(na,po),b1,b2) ->
+ let cj = pretype empty_tycon env isevars lvar c in
+ let (IndType (indf,realargs)) =
+ try find_rectype env (evars_of !isevars) cj.uj_type
+ with Not_found ->
+ let cloc = loc_of_rawconstr c in
+ error_case_not_inductive_loc cloc env (evars_of !isevars) cj in
+ let cstrs = get_constructors env indf in
+ if Array.length cstrs <> 2 then
+ user_err_loc (loc,"",
+ str "If is only for inductive types with two constructors");
+
+ let arsgn =
+ let arsgn,_ = get_arity env indf in
+ if not !allow_anonymous_refs then
+ (* Make dependencies from arity signature impossible *)
+ List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn
+ else arsgn
+ in
+ let nar = List.length arsgn in
+ let psign = (na,None,build_dependent_inductive env indf)::arsgn in
+ let pred,p = match po with
+ | Some p ->
+ let env_p = push_rels psign env in
+ 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
+ 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 (None, ty) -> 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 = 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
+ List.map (fun (_,b,t) -> (Anonymous,b,t)) cs.cs_args
+ else
+ List.map
+ (fun (n, b, t) ->
+ match n with
+ Name _ -> (n, b, t)
+ | Anonymous -> (Name (id_of_string "H"), b, t))
+ cs.cs_args
+ in
+ let env_c = push_rels csgn env 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 v =
+ let mis,_ = dest_ind_family indf in
+ let ci = make_default_case_info env IfStyle mis in
+ mkCase (ci, pred, cj.uj_val, [|b1;b2|])
+ in
+ { uj_val = v; uj_type = p }
+
+ | RCases (loc,po,tml,eqns) ->
+ Cases.compile_cases loc
+ ((fun vtyc env -> pretype vtyc env isevars lvar),isevars)
+ tycon env (* loc *) (po,tml,eqns)
+
+ | RCast(loc,c,k,t) ->
+ let cj =
+ match k with
+ CastCoerce ->
+ let cj = pretype empty_tycon env isevars lvar c in
+ evd_comb1 (Coercion.inh_coerce_to_base loc env) isevars cj
+ | CastConv k ->
+ 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 *)
+ let v = mkCast (cj.uj_val, k, tj.utj_val) in
+ { uj_val = v; uj_type = tj.utj_val }
+ in
+ inh_conv_coerce_to_tycon loc env isevars cj tycon
+
+ | RDynamic (loc,d) ->
+ if (tag d) = "constr" then
+ let c = constr_out d in
+ let j = (Retyping.get_judgment_of env (evars_of !isevars) c) in
+ j
+ (*inh_conv_coerce_to_tycon loc env isevars j tycon*)
+ else
+ user_err_loc (loc,"pretype",(str "Not a constr tagged Dynamic"))
+
+ (* [pretype_type valcon env isevars lvar c] coerces [c] into a type *)
+ and pretype_type valcon env isevars lvar = function
+ | RHole loc ->
+ (match valcon with
+ | Some v ->
+ let s =
+ let sigma = evars_of !isevars in
+ let t = Retyping.get_type_of env sigma v in
+ match kind_of_term (whd_betadeltaiota env sigma t) with
+ | Sort s -> s
+ | Evar v when is_Type (existential_type sigma v) ->
+ evd_comb1 (define_evar_as_sort) isevars v
+ | _ -> anomaly "Found a type constraint which is not a type"
+ in
+ { utj_val = v;
+ utj_type = s }
+ | None ->
+ let s = new_Type_sort () in
+ { utj_val = e_new_evar isevars env ~src:loc (mkSort s);
+ utj_type = s})
+ | c ->
+ let j = pretype empty_tycon env isevars lvar c in
+ let loc = loc_of_rawconstr c in
+ let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) isevars j in
+ match valcon with
+ | None -> tj
+ | Some v ->
+ if e_cumul env isevars v tj.utj_val then tj
+ else
+ error_unexpected_type_loc
+ (loc_of_rawconstr c) env (evars_of !isevars) tj.utj_val v
+
+ let pretype_gen isevars env lvar kind c =
+ let c' = match kind with
+ | OfType exptyp ->
+ let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
+ (pretype tycon env isevars lvar c).uj_val
+ | IsType ->
+ (pretype_type empty_valcon env isevars lvar c).utj_val in
+ nf_evar (evars_of !isevars) c'
+
+ (* [check_evars] fails if some unresolved evar remains *)
+ (* it assumes that the defined existentials have already been substituted
+ (should be done in unsafe_infer and unsafe_infer_type) *)
+
+ let check_evars env initial_sigma isevars c =
+ let sigma = evars_of !isevars in
+ let rec proc_rec c =
+ match kind_of_term c with
+ | Evar (ev,args) ->
+ assert (Evd.mem sigma ev);
+ if not (Evd.mem initial_sigma ev) then
+ let (loc,k) = evar_source ev !isevars in
+ error_unsolvable_implicit loc env sigma k
+ | _ -> iter_constr proc_rec c
+ in
+ proc_rec c(*;
+ let (_,pbs) = get_conv_pbs !isevars (fun _ -> true) in
+ if pbs <> [] then begin
+ pperrnl
+ (str"TYPING OF "++Termops.print_constr_env env c++fnl()++
+ prlist_with_sep fnl
+ (fun (pb,c1,c2) ->
+ Termops.print_constr c1 ++
+ (if pb=Reduction.CUMUL then str " <="++ spc()
+ else str" =="++spc()) ++
+ Termops.print_constr c2)
+ pbs ++ fnl())
+ end*)
+
+ (* TODO: comment faire remonter l'information si le typage a resolu des
+ variables du sigma original. il faudrait que la fonction de typage
+ retourne aussi le nouveau sigma...
+ *)
+
+ let understand_judgment sigma env c =
+ let isevars = ref (create_evar_defs sigma) in
+ let j = pretype empty_tycon env isevars ([],[]) c in
+ let j = j_nf_evar (evars_of !isevars) j in
+ check_evars env sigma isevars (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
+ j
+
+ 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
+ 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 (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
+
+ (** Entry points of the high-level type synthesis algorithm *)
+
+ let understand_gen kind sigma env c =
+ snd (ise_pretype_gen true sigma env ([],[]) kind c)
+
+ let understand sigma env ?expected_type:exptyp c =
+ snd (ise_pretype_gen true sigma env ([],[]) (OfType exptyp) c)
+
+ let understand_type sigma env c =
+ snd (ise_pretype_gen true sigma env ([],[]) IsType c)
+
+ 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 ev, t = ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c in
+ Evd.evars_of ev, t
+end
+
+module Default : S = SubtacPretyping_F(Coercion.Default)
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 6c165dada1..966aa80a9e 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -57,7 +57,7 @@ let natind = lazy (init_constant ["Init"; "Datatypes"] "nat")
let intind = lazy (init_constant ["ZArith"; "binint"] "Z")
let existSind = lazy (init_constant ["Init"; "Specif"] "sigS")
-let existS = lazy (build_sigma_set ())
+let existS = lazy (build_sigma_type ())
let prod = lazy (build_prod ())
@@ -244,3 +244,79 @@ let destruct_ex ext ex =
in aux ex ext
+let list_mapi f =
+ let rec aux i = function
+ hd :: tl -> f i hd :: aux (succ i) tl
+ | [] -> []
+ in aux 0
+
+open Rawterm
+
+let rewrite_cases_aux (loc, po, tml, eqns) =
+ let tml' = list_mapi (fun i (c, (n, opt)) -> c,
+ ((match n with
+ Name id -> (match c with
+ | RVar (_, id') when id = id' ->
+ id, (id_of_string (string_of_id id ^ "Heq_id"))
+ | RVar (_, id') ->
+ id', id
+ | _ -> id_of_string (string_of_id id ^ "Heq_id"), id)
+ | Anonymous ->
+ let str = "Heq_id" ^ string_of_int i in
+ id_of_string str, id_of_string (str ^ "'")),
+ opt)) tml
+ in
+ let mkHole = RHole (dummy_loc, InternalHole) in
+ let mkCoerceCast c = RCast (dummy_loc, c, CastCoerce, mkHole) in
+ let mkeq c n = RApp (dummy_loc, RRef (dummy_loc, (Lazy.force eqind_ref)),
+ [mkHole; c; n])
+ in
+ let eqs_types =
+ List.map
+ (fun (c, ((id, id'), _)) ->
+ let heqid = id_of_string ("Heq" ^ string_of_id id) in
+ Name heqid, mkeq (RVar (dummy_loc, id')) c)
+ tml'
+ in
+ let po =
+ List.fold_right
+ (fun (n,t) acc ->
+ RProd (dummy_loc, Anonymous, t, acc))
+ eqs_types (match po with
+ Some e -> e
+ | None -> mkHole)
+ in
+ let eqns =
+ List.map (fun (loc, idl, cpl, c) ->
+ let c' =
+ List.fold_left
+ (fun acc (n, t) ->
+ RLambda (dummy_loc, n, mkHole, acc))
+ c eqs_types
+ in (loc, idl, cpl, c'))
+ eqns
+ in
+ let mk_refl_equal c = RApp (dummy_loc, RRef (dummy_loc, Lazy.force refl_equal_ref),
+ [mkHole; c])
+ in
+ let refls = List.map (fun (c, ((id, _), _)) -> mk_refl_equal (mkCoerceCast c)) tml' in
+ let tml'' = List.map (fun (c, ((id, id'), opt)) -> c, (Name id', opt)) tml' in
+ let case = RCases (loc,Some po,tml'',eqns) in
+ let app = RApp (dummy_loc, case, refls) in
+(* let letapp = List.fold_left (fun acc (c, ((id, id'), opt)) -> RLetIn (dummy_loc, Name id, c, acc)) *)
+(* app tml' *)
+(* in *)
+ app
+
+let rec rewrite_cases c =
+ match c with
+ RCases _ -> let c' = map_rawconstr rewrite_cases c in
+ (match c' with
+ | RCases (x, y, z, w) -> rewrite_cases_aux (x,y,z,w)
+ | _ -> assert(false))
+ | _ -> map_rawconstr rewrite_cases c
+
+let rewrite_cases env c =
+ let c' = rewrite_cases c in
+ let _ = trace (str "Rewrote cases: " ++ spc () ++ my_print_rawconstr env c') in
+ c'
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index 92a995c891..5ef3af18e6 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -83,3 +83,5 @@ 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
+
+val rewrite_cases : Environ.env -> Rawterm.rawconstr -> Rawterm.rawconstr
diff --git a/contrib/subtac/test/ListsTest.v b/contrib/subtac/test/ListsTest.v
index e5f42defb9..a29cd03964 100644
--- a/contrib/subtac/test/ListsTest.v
+++ b/contrib/subtac/test/ListsTest.v
@@ -1,38 +1,28 @@
Require Import Coq.subtac.Utils.
Require Import List.
-Require Import Arith.
+
Variable A : Set.
-Notation "` t" := (proj1_sig t) (at level 100) : core_scope.
-Extraction Inline proj1_sig.
-Notation "'forall' { x : A | P } , Q" :=
- (forall x:{x:A|P}, Q)
- (at level 200, x ident, right associativity).
-Require Import Omega.
-Program Definition myhd :
- forall { l : list A | length l <> 0 }, A :=
-
+Program Definition myhd : forall { l : list A | length l <> 0 }, A :=
fun l =>
match l with
| nil => _
| hd :: tl => hd
end.
-
Proof.
destruct l ; simpl ; intro H ; rewrite <- H in n ; intuition.
Defined.
-Extraction myhd.
-Program Definition mytail :
- forall { l : list A | length l <> 0 }, list A :=
+Extraction myhd.
+Extraction Inline proj1_sig.
+Program Definition mytail : forall { l : list A | length l <> 0 }, list A :=
fun l =>
- match `l with
+ match l with
| nil => _
| hd :: tl => tl
end.
-
Proof.
destruct l ; simpl ; intro H ; rewrite <- H in n ; intuition.
Defined.
@@ -48,35 +38,39 @@ Defined.
Extraction test_hd.
-Program Definition test_tail : list A := mytail nil.
+(*Program Definition test_tail : list A := mytail nil.*)
+
+
+
+
Program Fixpoint append (l : list A) (l' : list A) { struct l } :
{ r : list A | length r = length l + length l' } :=
match l with
- nil => l'
+ | nil => l'
| hd :: tl => hd :: (append tl l')
end.
-rewrite Heql ; auto.
simpl.
-rewrite (subset_simpl (append tl0 l')).
-unfold tl0 ; unfold hd0.
-rewrite Heql.
+subst ; auto.
+simpl ; rewrite (subset_simpl (append tl0 l')).
+simpl ; subst.
simpl ; auto.
Defined.
Extraction append.
-Lemma append_app' : forall l : list A, (`append nil l) = l.
+
+Program Lemma append_app' : forall l : list A, l = append nil l.
Proof.
simpl ; auto.
Qed.
-Lemma append_app : forall l : list A, (`append l nil) = l.
+Program Lemma append_app : forall l : list A, l = append l nil.
Proof.
intros.
induction l ; simpl ; auto.
simpl in IHl.
-rewrite IHl.
+rewrite <- IHl.
reflexivity.
Qed.
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 7a634a71a4..5b9b404425 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -45,7 +45,7 @@ type aconstr =
| ASort of rawsort
| AHole of Evd.hole_kind
| APatVar of patvar
- | ACast of aconstr * cast_kind * aconstr
+ | ACast of aconstr * cast_type * aconstr
let name_app f e = function
| Name id -> let (id, e) = f id e in (e, Name id)
@@ -94,7 +94,7 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
| AIf (c,(na,po),b1,b2) ->
let e,na = name_app g e na in
RIf (loc,f e c,(na,option_map (f e) po),f e b1,f e b2)
- | ACast (c,k,t) -> RCast (loc,f e c,k,f e t)
+ | ACast (c,k,t) -> RCast (loc,f e c, k,f e t)
| ASort x -> RSort (loc,x)
| AHole x -> RHole (loc,x)
| APatVar n -> RPatVar (loc,(false,n))
@@ -524,7 +524,7 @@ type constr_expr =
| CPatVar of loc * (bool * patvar)
| CEvar of loc * existential_key
| CSort of loc * rawsort
- | CCast of loc * constr_expr * cast_kind * constr_expr
+ | CCast of loc * constr_expr * cast_type * constr_expr
| CNotation of loc * notation * constr_expr list
| CPrim of loc * prim_token
| CDelimiters of loc * string * constr_expr
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index d5b718d343..9173d3116e 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -41,7 +41,7 @@ type aconstr =
| ASort of rawsort
| AHole of Evd.hole_kind
| APatVar of patvar
- | ACast of aconstr * cast_kind * aconstr
+ | ACast of aconstr * cast_type * aconstr
val rawconstr_of_aconstr_with_binders : loc ->
(identifier -> 'a -> identifier * 'a) ->
@@ -107,7 +107,7 @@ type constr_expr =
| CPatVar of loc * (bool * patvar)
| CEvar of loc * existential_key
| CSort of loc * rawsort
- | CCast of loc * constr_expr * cast_kind * constr_expr
+ | CCast of loc * constr_expr * cast_type * constr_expr
| CNotation of loc * notation * constr_expr list
| CPrim of loc * prim_token
| CDelimiters of loc * string * constr_expr
@@ -143,7 +143,7 @@ val names_of_cases_indtype : constr_expr -> identifier list
val mkIdentC : identifier -> constr_expr
val mkRefC : reference -> constr_expr
val mkAppC : constr_expr * constr_expr list -> constr_expr
-val mkCastC : constr_expr * cast_kind * constr_expr -> constr_expr
+val mkCastC : constr_expr * cast_type * constr_expr -> constr_expr
val mkLambdaC : name located list * constr_expr * constr_expr -> constr_expr
val mkLetInC : name located * constr_expr * constr_expr -> constr_expr
val mkProdC : name located list * constr_expr * constr_expr -> constr_expr
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 64d96ae4b6..82e1114256 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -28,7 +28,7 @@ let _ = List.iter (fun s -> Lexer.add_token("",s)) constr_kw
let mk_cast = function
(c,(_,None)) -> c
- | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, DEFAULTcast,ty)
+ | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, CastConv DEFAULTcast, ty)
let mk_lam = function
([],c) -> c
@@ -155,8 +155,8 @@ GEXTEND Gram
[ "200" RIGHTA
[ c = binder_constr -> c ]
| "100" RIGHTA
- [ c1 = operconstr; ":"; c2 = binder_constr -> CCast(loc,c1,DEFAULTcast,c2)
- | c1 = operconstr; ":"; c2 = SELF -> CCast(loc,c1,DEFAULTcast,c2) ]
+ [ c1 = operconstr; ":"; c2 = binder_constr -> CCast(loc,c1, CastConv DEFAULTcast,c2)
+ | c1 = operconstr; ":"; c2 = SELF -> CCast(loc,c1,CastConv DEFAULTcast,c2) ]
| "99" RIGHTA [ ]
| "90" RIGHTA
[ c1 = operconstr; "->"; c2 = binder_constr -> CArrow(loc,c1,c2)
@@ -320,7 +320,7 @@ GEXTEND Gram
| "("; id=name; ":="; c=lconstr; ")" ->
LocalRawDef (id,c)
| "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" ->
- LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c,DEFAULTcast,t))
+ LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv DEFAULTcast,t))
] ]
;
binder:
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 5d392846de..a1a7030990 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -117,6 +117,6 @@ GEXTEND Gram
;
constr_body:
[ [ ":="; c = lconstr -> c
- | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c,Term.DEFAULTcast,t) ] ]
+ | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c, Rawterm.CastConv Term.DEFAULTcast,t) ] ]
;
END
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 56be1ff5a8..bdedaf1764 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -181,7 +181,7 @@ let rec interp_xml_constr = function
let ln,lc,lt = list_split3 (List.map interp_xml_CoFixFunction xl) in
RRec (loc, RCoFix (get_xml_noFun al), Array.of_list ln, [||], Array.of_list lc, Array.of_list lt)
| XmlTag (loc,"CAST",al,[x1;x2]) ->
- RCast (loc, interp_xml_term x1, DEFAULTcast, interp_xml_type x2)
+ RCast (loc, interp_xml_term x1, CastConv DEFAULTcast, interp_xml_type x2)
| XmlTag (loc,"SORT",al,[]) ->
RSort (loc, get_xml_sort al)
| XmlTag (loc,s,_,_) -> user_err_loc (loc,"", str "Unexpected tag " ++ str s)
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 7a77d6eabb..b3cff232b9 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1482,7 +1482,7 @@ let set_arity_signature dep n arsign tomatchl pred x =
in
decomp_block [] pred (tomatchl,arsign)
-let prepare_predicate_from_tycon loc dep env isevars tomatchs c =
+let prepare_predicate_from_tycon loc dep env isevars tomatchs sign c =
let cook (n, l, env, signs) = function
| c,IsInd (_,IndType(indf,realargs)) ->
let indf' = lift_inductive_family n indf in
@@ -1594,7 +1594,7 @@ let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function
(match tycon with
| Some (None, t) ->
let names,pred =
- prepare_predicate_from_tycon loc false env isevars tomatchs t
+ prepare_predicate_from_tycon loc false env isevars tomatchs sign t
in Some (build_initial_predicate false names pred)
| _ -> None)
@@ -1607,7 +1607,8 @@ let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function
let predcclj = typing_fun (mk_tycon (new_Type ())) env rtntyp in
let _ =
option_map (fun tycon ->
- isevars := Coercion.inh_conv_coerces_to loc env !isevars predcclj.uj_val tycon)
+ isevars := Coercion.inh_conv_coerces_to loc env !isevars predcclj.uj_val
+ (lift_tycon_type (List.length arsign) tycon))
tycon
in
let predccl = (j_nf_isevar !isevars predcclj).uj_val in
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 1b128e43a7..8a55a46d2e 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -35,6 +35,12 @@ module type S = sig
type a sort; it fails if no coercion is applicable *)
val inh_coerce_to_sort : loc ->
env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_type_judgment
+
+ (* [inh_coerce_to_base env isevars j] coerces [j] to its base type; i.e. it
+ inserts a coercion into [j], if needed, in such a way it gets as
+ type its base type (the notion depends on the coercion system) *)
+ val inh_coerce_to_base : loc ->
+ env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment
(* [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type
[t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and
@@ -143,6 +149,8 @@ module Default = struct
| _ ->
inh_tosort_force loc env isevars j
+ let inh_coerce_to_base loc env isevars j = (isevars, j)
+
let inh_coerce_to_fail env isevars c1 v t =
let v', t' =
try
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index 667f207307..5476a4820c 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -33,13 +33,19 @@ module type S = sig
type a sort; it fails if no coercion is applicable *)
val inh_coerce_to_sort : loc ->
env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_type_judgment
+
+ (* [inh_coerce_to_base env isevars j] coerces [j] to its base type; i.e. it
+ inserts a coercion into [j], if needed, in such a way it gets as
+ type its base type (the notion depends on the coercion system) *)
+ val inh_coerce_to_base : loc ->
+ env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment
(* [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type
[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 -> 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 *)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index ec6edcbdfd..1fcc6d8b7c 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -374,7 +374,7 @@ let rec detype isgoal avoid env t =
RVar (dl, id))
| Sort s -> RSort (dl,detype_sort s)
| Cast (c1,k,c2) ->
- RCast(dl,detype isgoal avoid env c1, k,
+ RCast(dl,detype isgoal avoid env c1, CastConv k,
detype isgoal avoid env c2)
| Prod (na,ty,c) -> detype_binder isgoal BProd avoid env na ty c
| Lambda (na,ty,c) -> detype_binder isgoal BLambda avoid env na ty c
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index d1d30980b8..be24d22b59 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -363,17 +363,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct
inh_conv_coerce_to_tycon loc env isevars (pretype_sort s) tycon
| RApp (loc,f,args) ->
- let length = List.length args in
- let ftycon =
- match tycon with
- None -> None
- | Some (None, ty) -> mk_abstr_tycon length ty
- | Some (Some (init, cur), ty) ->
- Some (Some (length + init, length + cur), ty)
- in
let fj = pretype empty_tycon env isevars lvar f in
let floc = loc_of_rawconstr f in
- let rec apply_rec env n resj tycon = function
+ let rec apply_rec env n resj = function
| [] -> resj
| c::rest ->
let argloc = loc_of_rawconstr c in
@@ -384,33 +376,17 @@ module Pretyping_F (Coercion : Coercion.S) = struct
let hj = pretype (mk_tycon c1) env isevars lvar c in
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 =
- option_map
- (fun (abs, ty) ->
- match abs with
- None ->
- isevars := Coercion.inh_conv_coerces_to loc env !isevars typ'
- (abs, ty);
- (abs, ty)
- | Some (init, cur) ->
- isevars := Coercion.inh_conv_coerces_to loc env !isevars typ'
- (abs, ty);
- (Some (init, pred cur), ty))
- tycon
- in
apply_rec env (n+1)
{ uj_val = nf_isevar !isevars value;
- uj_type = nf_isevar !isevars typ' }
- (option_map (fun (abs, c) -> abs, nf_isevar !isevars c) tycon) rest
-
+ uj_type = typ' }
+ 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 ftycon = option_map (lift_abstr_tycon_type (-1)) ftycon in
- let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj ftycon args) in
+ let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj args) in
let resj =
match kind_of_term resj.uj_val with
| App (f,args) when isInd f ->
@@ -590,12 +566,19 @@ module Pretyping_F (Coercion : Coercion.S) = struct
tycon env (* loc *) (po,tml,eqns)
| RCast(loc,c,k,t) ->
- 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 *)
- let v = mkCast (cj.uj_val, k, tj.utj_val) in
- let cj = { uj_val = v; uj_type = tj.utj_val } in
+ let cj =
+ match k with
+ CastCoerce ->
+ let cj = pretype empty_tycon env isevars lvar c in
+ evd_comb1 (Coercion.inh_coerce_to_base loc env) isevars cj
+ | CastConv k ->
+ 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 *)
+ let v = mkCast (cj.uj_val, k, tj.utj_val) in
+ { uj_val = v; uj_type = tj.utj_val }
+ in
inh_conv_coerce_to_tycon loc env isevars cj tycon
| RDynamic (loc,d) ->
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index d536adcb0e..480ee13b2b 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -47,6 +47,10 @@ type 'a bindings =
type 'a with_bindings = 'a * 'a bindings
+type cast_type =
+ | CastConv of cast_kind
+ | CastCoerce (* Cast to a base type (eg, an underlying inductive type) *)
+
type rawconstr =
| RRef of (loc * global_reference)
| RVar of (loc * identifier)
@@ -64,7 +68,7 @@ type rawconstr =
rawconstr array * rawconstr array
| RSort of loc * rawsort
| RHole of (loc * hole_kind)
- | RCast of loc * rawconstr * cast_kind * rawconstr
+ | RCast of loc * rawconstr * cast_type * rawconstr
| RDynamic of loc * Dyn.t
and rawdecl = name * rawconstr option * rawconstr
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index d85ca0158a..d64ba03a79 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -44,6 +44,10 @@ type 'a bindings =
type 'a with_bindings = 'a * 'a bindings
+type cast_type =
+ | CastConv of cast_kind
+ | CastCoerce (* Cast to a base type (eg, an underlying inductive type) *)
+
type rawconstr =
| RRef of (loc * global_reference)
| RVar of (loc * identifier)
@@ -61,7 +65,7 @@ type rawconstr =
rawconstr array * rawconstr array
| RSort of loc * rawsort
| RHole of (loc * Evd.hole_kind)
- | RCast of loc * rawconstr * cast_kind * rawconstr
+ | RCast of loc * rawconstr * cast_type * rawconstr
| RDynamic of loc * Dyn.t
and rawdecl = name * rawconstr option * rawconstr
diff --git a/toplevel/command.ml b/toplevel/command.ml
index bfead59aaf..0f7f449cee 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -112,7 +112,7 @@ let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) =
| Some comtyp ->
(* We use a cast to avoid troubles with evars in comtyp *)
(* that can only be resolved knowing com *)
- let b = abstract_constr_expr (mkCastC (com,DEFAULTcast,comtyp)) bl in
+ let b = abstract_constr_expr (mkCastC (com, Rawterm.CastConv DEFAULTcast,comtyp)) bl in
let (body,typ) = destSubCast (interp_constr sigma env b) in
{ const_entry_body = body;
const_entry_type = Some typ;
diff --git a/toplevel/record.ml b/toplevel/record.ml
index f4f0c9150c..9c2d9732a3 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -36,7 +36,7 @@ let interp_decl sigma env = function
| Vernacexpr.DefExpr((_,id),c,t) ->
let c = match t with
| None -> c
- | Some t -> mkCastC (c,DEFAULTcast,t)
+ | Some t -> mkCastC (c, Rawterm.CastConv DEFAULTcast,t)
in
let j = interp_constr_judgment Evd.empty env c in
(id,Some j.uj_val, j.uj_type)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 16:00:15 +0000