diff options
40 files changed, 227 insertions, 161 deletions
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml index 3fb6641879..dc1dc2cfb2 100644 --- a/contrib/funind/indfun.ml +++ b/contrib/funind/indfun.ml @@ -209,7 +209,7 @@ let rec is_rec names = let rec lookup names = function | RVar(_,id) -> check_id id names | RRef _ | REvar _ | RPatVar _ | RSort _ | RHole _ | RDynamic _ -> false - | RCast(_,b,_,_) -> lookup names b + | RCast(_,b,_) -> lookup names b | RRec _ -> error "RRec not handled" | RIf(_,b,_,lhs,rhs) -> (lookup names b) || (lookup names lhs) || (lookup names rhs) @@ -611,8 +611,10 @@ let rec add_args id new_args b = | CPatVar _ -> b | CEvar _ -> b | CSort _ -> b - | CCast(loc,b1,ck,b2) -> - CCast(loc,add_args id new_args b1,ck,add_args id new_args b2) + | CCast(loc,b1,CastConv(ck,b2)) -> + CCast(loc,add_args id new_args b1,CastConv(ck,add_args id new_args b2)) + | CCast(loc,b1,CastCoerce) -> + CCast(loc,add_args id new_args b1,CastCoerce) | CNotation _ -> anomaly "add_args : CNotation" | CPrim _ -> b | CDelimiters _ -> anomaly "add_args : CDelimiters" diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml index aca84f0627..b34a1097a3 100644 --- a/contrib/funind/rawterm_to_relation.ml +++ b/contrib/funind/rawterm_to_relation.ml @@ -351,7 +351,7 @@ let rec find_type_of nb b = then raise (Invalid_argument "find_type_of : not a valid inductive"); ind_type end - | RCast(_,b,_,_) -> find_type_of nb b + | RCast(_,b,_) -> find_type_of nb b | RApp _ -> assert false (* we have decomposed any application via raw_decompose_app *) | _ -> raise (Invalid_argument "not a ref") @@ -575,7 +575,7 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return = let f_res = build_entry_lc env funnames args_res.to_avoid f in combine_results combine_app f_res args_res | RDynamic _ ->error "Not handled RDynamic" - | RCast(_,b,_,_) -> + | RCast(_,b,_) -> (* for an applied cast we just trash the cast part and restart the work. @@ -685,7 +685,7 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return = end | RRec _ -> error "Not handled RRec" - | RCast(_,b,_,_) -> + | RCast(_,b,_) -> build_entry_lc env funnames avoid b | RDynamic _ -> error "Not handled RDynamic" and build_entry_lc_from_case env funname make_discr diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml index 6af8d2c36c..f9e188dacf 100644 --- a/contrib/funind/rawtermops.ml +++ b/contrib/funind/rawtermops.ml @@ -18,7 +18,7 @@ let mkRLetIn(n,t,b) = RLetIn(dummy_loc,n,t,b) let mkRCases(rto,l,brl) = RCases(dummy_loc,rto,l,brl) let mkRSort s = RSort(dummy_loc,s) let mkRHole () = RHole(dummy_loc,Evd.BinderType Anonymous) -let mkRCast(b,t) = RCast(dummy_loc,b,CastCoerce,t) +let mkRCast(b,t) = RCast(dummy_loc,b,CastConv (Term.DEFAULTcast,t)) (* Some basic functions to decompose rawconstrs @@ -177,8 +177,10 @@ let change_vars = | RRec _ -> error "Local (co)fixes are not supported" | RSort _ -> rt | RHole _ -> rt - | RCast(loc,b,k,t) -> - RCast(loc,change_vars mapping b,k,change_vars mapping t) + | RCast(loc,b,CastConv (k,t)) -> + RCast(loc,change_vars mapping b, CastConv (k,change_vars mapping t)) + | RCast(loc,b,CastCoerce) -> + RCast(loc,change_vars mapping b,CastCoerce) | RDynamic _ -> error "Not handled RDynamic" and change_vars_br mapping ((loc,idl,patl,res) as br) = let new_mapping = List.fold_right Idmap.remove idl mapping in @@ -356,8 +358,10 @@ let rec alpha_rt excluded rt = | RRec _ -> error "Not handled RRec" | RSort _ -> rt | RHole _ -> rt - | RCast (loc,b,k,t) -> - RCast(loc,alpha_rt excluded b,k,alpha_rt excluded t) + | RCast (loc,b,CastConv (k,t)) -> + RCast(loc,alpha_rt excluded b,CastConv(k,alpha_rt excluded t)) + | RCast (loc,b,CastCoerce) -> + RCast(loc,alpha_rt excluded b,CastCoerce) | RDynamic _ -> error "Not handled RDynamic" | RApp(loc,f,args) -> RApp(loc, @@ -407,7 +411,8 @@ let is_free_in id = | RRec _ -> raise (UserError("",str "Not handled RRec")) | RSort _ -> false | RHole _ -> false - | RCast (_,b,_,t) -> is_free_in b || is_free_in t + | RCast (_,b,CastConv (_,t)) -> is_free_in b || is_free_in t + | RCast (_,b,CastCoerce) -> is_free_in b | RDynamic _ -> raise (UserError("",str "Not handled RDynamic")) and is_free_in_br (_,ids,_,rt) = (not (List.mem id ids)) && is_free_in rt @@ -501,8 +506,10 @@ let replace_var_by_term x_id term = | RRec _ -> raise (UserError("",str "Not handled RRec")) | RSort _ -> rt | RHole _ -> rt - | RCast(loc,b,k,t) -> - RCast(loc,replace_var_by_pattern b,k,replace_var_by_pattern t) + | RCast(loc,b,CastConv(k,t)) -> + RCast(loc,replace_var_by_pattern b,CastConv(k,replace_var_by_pattern t)) + | RCast(loc,b,CastCoerce) -> + RCast(loc,replace_var_by_pattern b,CastCoerce) | RDynamic _ -> raise (UserError("",str "Not handled RDynamic")) and replace_var_by_pattern_br ((loc,idl,patl,res) as br) = if List.exists (fun id -> id_ord id x_id == 0) idl @@ -586,7 +593,8 @@ let ids_of_rawterm c = | RLambda (loc,na,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc | RProd (loc,na,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc | RLetIn (loc,na,b,c) -> idof na :: ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc - | RCast (loc,c,k,t) -> ids_of_rawterm [] c @ ids_of_rawterm [] t @ acc + | RCast (loc,c,CastConv(k,t)) -> ids_of_rawterm [] c @ ids_of_rawterm [] t @ acc + | RCast (loc,c,CastCoerce) -> ids_of_rawterm [] c @ acc | RIf (loc,c,(na,po),b1,b2) -> ids_of_rawterm [] c @ ids_of_rawterm [] b1 @ ids_of_rawterm [] b2 @ acc | RLetTuple (_,nal,(na,po),b,c) -> List.map idof nal @ ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc @@ -651,8 +659,10 @@ let zeta_normalize = | RRec _ -> raise (UserError("",str "Not handled RRec")) | RSort _ -> rt | RHole _ -> rt - | RCast(loc,b,k,t) -> - RCast(loc,zeta_normalize_term b,k,zeta_normalize_term t) + | RCast(loc,b,CastConv(k,t)) -> + RCast(loc,zeta_normalize_term b,CastConv(k,zeta_normalize_term t)) + | RCast(loc,b,CastCoerce) -> + RCast(loc,zeta_normalize_term b,CastCoerce) | RDynamic _ -> raise (UserError("",str "Not handled RDynamic")) and zeta_normalize_br (loc,idl,patl,res) = (loc,idl,patl,zeta_normalize_term res) @@ -692,7 +702,8 @@ let expand_as = expand_as map br1, expand_as map br2) | RRec _ -> error "Not handled RRec" | RDynamic _ -> error "Not handled RDynamic" - | RCast(loc,b,kind,t) -> RCast(loc,expand_as map b,kind,expand_as map t) + | RCast(loc,b,CastConv(kind,t)) -> RCast(loc,expand_as map b,CastConv(kind,expand_as map t)) + | RCast(loc,b,CastCoerce) -> RCast(loc,expand_as map b,CastCoerce) | RCases(loc,po,el,brl) -> RCases(loc, option_map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el, List.map (expand_as_br map) brl) diff --git a/contrib/subtac/FunctionalExtensionality.v b/contrib/subtac/FunctionalExtensionality.v index 07a19ab376..4610f3467a 100644 --- a/contrib/subtac/FunctionalExtensionality.v +++ b/contrib/subtac/FunctionalExtensionality.v @@ -1,3 +1,11 @@ +Lemma equal_f : forall A B : Type, forall (f g : A -> B), + f = g -> forall x, f x = g x. +Proof. + intros. + rewrite H. + auto. +Qed. + Axiom fun_extensionality : forall A B (f g : A -> B), (forall x, f x = g x) -> f = g. diff --git a/contrib/subtac/SubtacTactics.v b/contrib/subtac/SubtacTactics.v index e678cf5d93..e1c48769c4 100644 --- a/contrib/subtac/SubtacTactics.v +++ b/contrib/subtac/SubtacTactics.v @@ -24,14 +24,19 @@ Ltac induction_with_subterms c c' H := Ltac destruct_one_pair := match goal with - | [H : (ex _) |- _] => destruct H - | [H : (ex2 _) |- _] => destruct H - | [H : (sig _) |- _] => destruct H - | [H : (_ /\ _) |- _] => destruct H - | [H : prod _ _ |- _] => destruct H -end. + | [H : (ex2 _) |- _] => destruct H + | [H : (_ /\ _) |- _] => destruct H + | [H : prod _ _ |- _] => destruct H + end. -Ltac destruct_exists := repeat (destruct_one_pair) . +Ltac destruct_one_ex := + let tac H := let ph := fresh "H" in destruct H as [H ph] in + match goal with + | [H : (ex _) |- _] => tac H + | [H : (sig ?P) |- _ ] => tac H + end. + +Ltac destruct_exists := repeat (destruct_one_pair || destruct_one_ex). Ltac on_call f tac := match goal with diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v index 6250794526..bf4876a03c 100644 --- a/contrib/subtac/Utils.v +++ b/contrib/subtac/Utils.v @@ -2,58 +2,37 @@ Require Export Coq.subtac.SubtacTactics. Set Implicit Arguments. -Notation "'fun' { x : A | P } => Q" := - (fun x:{x:A|P} => Q) - (at level 200, x ident, right associativity). - Notation " {{ x }} " := (tt : { y : unit | x }). -Notation "( x & ? )" := (@exist _ _ x _) : core_scope. +Notation "{ ( x , y ) : A | P }" := + (sig (fun t:A => let (x,y) := t in P)) + (x ident, y ident) : type_scope. Notation " ! " := (False_rect _ _). -Require Import Coq.Bool.Sumbool. -Notation "'dec'" := (sumbool_of_bool) (at level 0). - -Definition ex_pi1 (A : Prop) (P : A -> Prop) (t : ex P) : A. -intros. -induction t. -exact x. -Defined. +Notation "` t" := (proj1_sig t) (at level 100) : core_scope. +Notation "( x & ? )" := (@exist _ _ x _) : core_scope. -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. +(** Coerces objects before comparing them *) +Notation " x '`=' y " := ((x :>) = (y :>)) (at level 70). +(** Quantifying over subsets *) +Notation "'fun' { x : A | P } => Q" := + (fun x:{x:A|P} => Q) + (at level 200, x ident, right associativity). -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). -Lemma subset_simpl : forall (A : Set) (P : A -> Prop) - (t : sig P), P (` t). -Proof. -intros. -induction t. - simpl ; auto. -Qed. - -Lemma equal_f : forall A B : Type, forall (f g : A -> B), - f = g -> forall x, f x = g x. -Proof. - intros. - rewrite H. - auto. -Qed. +Require Import Coq.Bool.Sumbool. +Notation "'dec'" := (sumbool_of_bool) (at level 0). +(** Default simplification tactic. *) Ltac subtac_simpl := simpl ; intros ; destruct_exists ; simpl in * ; try subst ; - try (solve [ red ; intros ; discriminate ]) ; auto with arith. + try (solve [ red ; intros ; discriminate ]) ; auto with *. +(** Extraction directives *) Extraction Inline proj1_sig. Extract Inductive unit => "unit" [ "()" ]. Extract Inductive bool => "bool" [ "true" "false" ]. diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml index e0711cade9..1989e7dcf0 100644 --- a/contrib/subtac/eterm.ml +++ b/contrib/subtac/eterm.ml @@ -65,7 +65,8 @@ let subst_evar_constr evs n t = and we must not apply to defined ones (i.e. LetIn's) *) let args = - let (l, r) = list_split_at chop (List.rev (Array.to_list args)) in + let n = match chop with None -> 0 | Some c -> c in + let (l, r) = list_split_at n (List.rev (Array.to_list args)) in List.rev r in let args = @@ -144,14 +145,16 @@ let rec chop_product n t = | Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None | _ -> None -let eterm_obligations name nclen evm fs t tycon = +let eterm_obligations name nclen isevars evm fs t tycon = (* 'Serialize' the evars, we assume that the types of the existentials refer to previous existentials in the list only *) let evl = List.rev (to_list evm) in let evn = let i = ref (-1) in List.rev_map (fun (id, ev) -> incr i; - (id, (!i, id_of_string (string_of_id name ^ "_obligation_" ^ string_of_int (succ !i))), ev)) evl + (id, (!i, id_of_string + (string_of_id name ^ "_obligation_" ^ string_of_int (succ !i))), + ev)) evl in let evts = (* Remove existential variables in types and build the corresponding products *) @@ -171,7 +174,10 @@ let eterm_obligations name nclen evm fs t tycon = t, trunc_named_context fs hyps, fs | None -> evtyp, hyps, 0 in - let y' = (id, ((n, nstr), hyps, chop, evtyp, deps)) in + let loc, k = evar_source id isevars in + let opacity = match k with QuestionMark o -> o | _ -> true in + let opaque = if not opacity || chop <> fs then None else Some chop in + let y' = (id, ((n, nstr), hyps, opaque, evtyp, deps)) in y' :: l) evn [] in @@ -179,7 +185,7 @@ let eterm_obligations name nclen evm fs t tycon = subst_evar_constr evts 0 t in let evars = - List.map (fun (_, ((_, name), _, chop, typ, deps)) -> name, typ, chop = fs, deps) evts + List.map (fun (_, ((_, name), _, opaque, typ, deps)) -> name, typ, not (opaque = None), deps) evts in (try trace (str "Term given to eterm" ++ spc () ++ diff --git a/contrib/subtac/eterm.mli b/contrib/subtac/eterm.mli index a67020c52d..71fd766e35 100644 --- a/contrib/subtac/eterm.mli +++ b/contrib/subtac/eterm.mli @@ -18,9 +18,10 @@ val mkMetas : int -> constr list (* val eterm_term : evar_map -> constr -> types option -> constr * types option * (identifier * types) list *) -val eterm_obligations : identifier -> int -> evar_map -> int -> constr -> types option -> (* id, named context length, evars, number of - function prototypes to try to clear from evars contexts *) +(* id, named context length, evars, number of + function prototypes to try to clear from evars contexts, object and optional type *) +val eterm_obligations : identifier -> int -> evar_defs -> evar_map -> int -> constr -> types option -> (identifier * types * bool * Intset.t) array * constr - (* Obl. name, type as product, chopping of products flag, and dependencies as indexes into the array *) + (* Obl. name, type as product, opacity (true = opaque) and dependencies as indexes into the array *) val etermtac : open_constr -> tactic diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml index b697e93320..fc2da8f587 100644 --- a/contrib/subtac/subtac.ml +++ b/contrib/subtac/subtac.ml @@ -145,10 +145,28 @@ let print_subgoals () = Options.if_verbose (fun () -> msg (Printer.pr_open_subgo let start_proof_and_print env isevars idopt k t hook = start_proof_com env isevars idopt k t hook; print_subgoals () - (*if !pcoq <> None then (out_some !pcoq).start_proof ()*) +(* if !pcoq <> None then (out_some !pcoq).start_proof () *) let _ = Detyping.set_detype_anonymous (fun loc n -> RVar (loc, id_of_string ("Anonymous_REL_" ^ string_of_int n))) + +let assumption_message id = + Options.if_verbose message ((string_of_id id) ^ " is assumed") + +let declare_assumption env isevars idl is_coe k bl c = + if not (Pfedit.refining ()) then + let evm, c, typ = + Subtac_pretyping.subtac_process env isevars (snd (List.hd idl)) [] (Command.generalize_constr_expr c bl) None + in + List.iter (Command.declare_one_assumption is_coe k c) idl + else + errorlabstrm "Command.Assumption" + (str "Cannot declare an assumption while in proof editing mode.") + +let vernac_assumption env isevars kind l = + List.iter (fun (is_coe,(idl,c)) -> declare_assumption env isevars idl is_coe kind [] c) l + + let subtac (loc, command) = check_required_library ["Coq";"Init";"Datatypes"]; check_required_library ["Coq";"Init";"Specif"]; @@ -159,7 +177,7 @@ let subtac (loc, command) = let env = Global.env () in let isevars = ref (create_evar_defs Evd.empty) in try - match command with + match command with VernacDefinition (defkind, (locid, id), expr, hook) -> (match expr with ProveBody (bl, c) -> Subtac_pretyping.subtac_proof env isevars id bl c None @@ -190,6 +208,8 @@ let subtac (loc, command) = start_proof_and_print env isevars (Some id) (Global, Proof thkind) (bl,t) hook + | VernacAssumption (stre,l) -> + vernac_assumption env isevars stre l (*| VernacEndProof e -> subtac_end_proof e*) diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml index b7243374b2..72fd421893 100644 --- a/contrib/subtac/subtac_cases.ml +++ b/contrib/subtac/subtac_cases.ml @@ -1762,7 +1762,7 @@ let constrs_of_pats typing_fun tycon env isevars eqns tomatchs sign neqs arity = | l -> RApp (dummy_loc, bref, l) in let branch = match ineqs with - Some _ -> RApp (dummy_loc, branch, [ RHole (dummy_loc, Evd.QuestionMark) ]) + Some _ -> RApp (dummy_loc, branch, [ RHole (dummy_loc, Evd.QuestionMark true) ]) | None -> branch in (* let branch = *) diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index 94f1bdec0a..09ed69fb4d 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -286,7 +286,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = mkApp (constr_of_reference (Lazy.force fix_sub_ref), [| argtyp ; wf_rel ; - make_existential dummy_loc intern_before_env isevars wf_proof ; + make_existential dummy_loc ~opaque:false intern_before_env isevars wf_proof ; prop ; intern_body_lam |]) | Some f -> @@ -309,7 +309,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = (* in *) let evm = non_instanciated_map env isevars in (* let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) with _ -> () in *) - let evars, evars_def = Eterm.eterm_obligations recname nc_len evm 0 fullcoqc (Some fullctyp) in + let evars, evars_def = Eterm.eterm_obligations recname nc_len !isevars evm 0 fullcoqc (Some fullctyp) in (* (try trace (str "Generated obligations : "); *) (* Array.iter *) (* (fun (n, t, _) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env t)) *) @@ -392,7 +392,7 @@ let build_mutrec l boxed = and typ = Termops.it_mkNamedProd_or_LetIn typ rec_sign in - let evars, def = Eterm.eterm_obligations id nc_len evm recdefs def (Some typ) in + let evars, def = Eterm.eterm_obligations id nc_len isevars evm recdefs def (Some typ) in collect_evars (succ i) ((id, def, typ, evars) :: acc) else acc in diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml index 647c47b6ad..e83ee66585 100644 --- a/contrib/subtac/subtac_pretyping.ml +++ b/contrib/subtac/subtac_pretyping.ml @@ -151,5 +151,5 @@ let subtac_proof env isevars id l c tycon = let nc = named_context env in let nc_len = named_context_length nc in let evm, coqc, coqt = subtac_process env isevars id l c tycon in - let evars, def = Eterm.eterm_obligations id nc_len evm 0 coqc (Some coqt) in + let evars, def = Eterm.eterm_obligations id nc_len !isevars evm 0 coqc (Some coqt) in add_definition id def coqt evars diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml index 990ee115f6..c2132f61b5 100644 --- a/contrib/subtac/subtac_pretyping_F.ml +++ b/contrib/subtac/subtac_pretyping_F.ml @@ -495,13 +495,13 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct ((fun vtyc env -> pretype vtyc env isevars lvar),isevars) tycon env (* loc *) (po,tml,eqns) - | RCast(loc,c,k,t) -> + | RCast(loc,c,k) -> 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 -> + | CastConv (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*) diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml index 4dc157397a..2e362a2107 100644 --- a/contrib/subtac/subtac_utils.ml +++ b/contrib/subtac/subtac_utils.ml @@ -152,8 +152,8 @@ let app_opt c e = let print_args env args = Array.fold_right (fun a acc -> my_print_constr env a ++ spc () ++ acc) args (str "") -let make_existential loc env isevars c = - let evar = Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark) c in +let make_existential loc ?(opaque = true) env isevars c = + let evar = Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark opaque) c in let (key, args) = destEvar evar in (try trace (str "Constructed evar " ++ int key ++ str " applied to args: " ++ print_args env args ++ str " for type: "++ @@ -169,7 +169,7 @@ let make_existential_expr loc env c = let string_of_hole_kind = function | ImplicitArg _ -> "ImplicitArg" | BinderType _ -> "BinderType" - | QuestionMark -> "QuestionMark" + | QuestionMark _ -> "QuestionMark" | CasesType -> "CasesType" | InternalHole -> "InternalHole" | TomatchTypeParameter _ -> "TomatchTypeParameter" @@ -182,7 +182,7 @@ let non_instanciated_map env evd = debug 2 (str "evar " ++ int key ++ str " has kind " ++ str (string_of_hole_kind k)); match k with - QuestionMark -> Evd.add evm key evi + QuestionMark _ -> Evd.add evm key evi | _ -> debug 2 (str " and is an implicit"); Pretype_errors.error_unsolvable_implicit loc env evm k) diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli index 00f01d6e1c..37ee1ac23a 100644 --- a/contrib/subtac/subtac_utils.mli +++ b/contrib/subtac/subtac_utils.mli @@ -82,7 +82,7 @@ val wf_relations : (constr, constr lazy_t) Hashtbl.t type binders = local_binder list val app_opt : ('a -> 'a) option -> 'a -> 'a val print_args : env -> constr array -> std_ppcmds -val make_existential : loc -> env -> evar_defs ref -> types -> constr +val make_existential : loc -> ?opaque:bool -> env -> evar_defs ref -> types -> constr val make_existential_expr : loc -> 'a -> 'b -> constr_expr val string_of_hole_kind : hole_kind -> string val non_instanciated_map : env -> evar_defs ref -> evar_map diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 96548df711..4fbf57e07a 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -204,9 +204,11 @@ let rec check_same_type ty1 ty2 = | CHole _, CHole _ -> () | CPatVar(_,i1), CPatVar(_,i2) when i1=i2 -> () | CSort(_,s1), CSort(_,s2) when s1=s2 -> () - | CCast(_,a1,_,b1), CCast(_,a2,_,b2) -> + | CCast(_,a1,CastConv (_,b1)), CCast(_,a2, CastConv(_,b2)) -> check_same_type a1 a2; check_same_type b1 b2 + | CCast(_,a1,CastCoerce), CCast(_,a2, CastCoerce) -> + check_same_type a1 a2 | CNotation(_,n1,e1), CNotation(_,n2,e2) when n1=n2 -> List.iter2 check_same_type e1 e2 | CPrim(_,i1), CPrim(_,i2) when i1=i2 -> () @@ -296,8 +298,8 @@ let rec same_raw c d = | RSort(_,s1), RSort(_,s2) -> if s1<>s2 then failwith "RSort" | RHole _, _ -> () | _, RHole _ -> () - | RCast(_,c1,_,_),r2 -> same_raw c1 r2 - | r1, RCast(_,c2,_,_) -> same_raw r1 c2 + | RCast(_,c1,_),r2 -> same_raw c1 r2 + | r1, RCast(_,c2,_) -> same_raw r1 c2 | RDynamic(_,d1), RDynamic(_,d2) -> if d1<>d2 then failwith"RDynamic" | _ -> failwith "same_raw" @@ -757,8 +759,10 @@ let rec extern inctx scopes vars r = | RHole (loc,e) -> CHole loc - | RCast (loc,c,k,t) -> - CCast (loc,sub_extern true scopes vars c,k,extern_typ scopes vars t) + | RCast (loc,c, CastConv (k,t)) -> + CCast (loc,sub_extern true scopes vars c, CastConv (k,extern_typ scopes vars t)) + | RCast (loc,c, CastCoerce) -> + CCast (loc,sub_extern true scopes vars c, CastCoerce) | RDynamic (loc,d) -> CDynamic (loc,d) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 244f8228a9..5a41f35086 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -915,7 +915,7 @@ let internalise sigma globalenv env allow_patvar lvar c = let p' = option_map (intern_type env'') po in RIf (loc, c', (na', p'), intern env b1, intern env b2) | CHole loc -> - RHole (loc, Evd.QuestionMark) + RHole (loc, Evd.QuestionMark true) | CPatVar (loc, n) when allow_patvar -> RPatVar (loc, n) | CPatVar (loc, _) -> @@ -924,8 +924,10 @@ let internalise sigma globalenv env allow_patvar lvar c = REvar (loc, n, None) | CSort (loc, s) -> RSort(loc,s) - | CCast (loc, c1, k, c2) -> - RCast (loc,intern env c1,k,intern_type env c2) + | CCast (loc, c1, CastConv (k, c2)) -> + RCast (loc,intern env c1, CastConv (k, intern_type env c2)) + | CCast (loc, c1, CastCoerce) -> + RCast (loc,intern env c1, CastCoerce) | CDynamic (loc,d) -> RDynamic (loc,d) diff --git a/interp/reserve.ml b/interp/reserve.ml index 39ba6d6fd5..5a8eafff7b 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -73,7 +73,8 @@ let rec unloc = function bl, Array.map unloc tyl, Array.map unloc bv) - | RCast (_,c,k,t) -> RCast (dummy_loc,unloc c,k,unloc t) + | RCast (_,c, CastConv (k,t)) -> RCast (dummy_loc,unloc c, CastConv (k,unloc t)) + | RCast (_,c, CastCoerce) -> RCast (dummy_loc,unloc c, CastCoerce) | RSort (_,x) -> RSort (dummy_loc,x) | RHole (_,x) -> RHole (dummy_loc,x) | RRef (_,x) -> RRef (dummy_loc,x) diff --git a/interp/topconstr.ml b/interp/topconstr.ml index da3f73149f..514c0811c7 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_type * aconstr + | ACast of aconstr * aconstr cast_type (**********************************************************************) (* Re-interpret a notation as a rawconstr, taking care of binders *) @@ -102,7 +102,10 @@ let rawconstr_of_aconstr_with_binders loc g f e = function | AIf (c,(na,po),b1,b2) -> let e,na = name_fold_map 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) -> RCast (loc,f e c, + match k with + | CastConv (k,t) -> CastConv (k,f e t) + | CastCoerce -> CastCoerce) | ASort x -> RSort (loc,x) | AHole x -> RHole (loc,x) | APatVar n -> RPatVar (loc,(false,n)) @@ -196,7 +199,9 @@ let aconstr_and_vars_of_rawconstr a = | RIf (loc,c,(na,po),b1,b2) -> add_name found na; AIf (aux c,(na,option_map aux po),aux b1,aux b2) - | RCast (_,c,k,t) -> ACast (aux c,k,aux t) + | RCast (_,c,k) -> ACast (aux c, + match k with CastConv (k,t) -> CastConv (k,aux t) + | CastCoerce -> CastCoerce) | RSort (_,s) -> ASort s | RHole (_,w) -> AHole w | RRef (_,r) -> ARef r @@ -342,15 +347,21 @@ let rec subst_aconstr subst bound raw = let ref',t = subst_global subst ref in if ref' == ref then raw else AHole (Evd.InternalHole) - | AHole (Evd.BinderType _ | Evd.QuestionMark | Evd.CasesType | - Evd.InternalHole | Evd.TomatchTypeParameter _) -> raw - - | ACast (r1,k,r2) -> - let r1' = subst_aconstr subst bound r1 - and r2' = subst_aconstr subst bound r2 in - if r1' == r1 && r2' == r2 then raw else - ACast (r1',k,r2') - + | AHole (Evd.BinderType _ | Evd.QuestionMark _ | Evd.CasesType + | Evd.InternalHole | Evd.TomatchTypeParameter _) -> raw + + | ACast (r1,k) -> + match k with + CastConv (k, r2) -> + let r1' = subst_aconstr subst bound r1 + and r2' = subst_aconstr subst bound r2 in + if r1' == r1 && r2' == r2 then raw else + ACast (r1',CastConv (k,r2')) + | CastCoerce -> + let r1' = subst_aconstr subst bound r1 in + if r1' == r1 then raw else + ACast (r1',CastCoerce) + let encode_list_value l = RApp (dummy_loc,RVar (dummy_loc,ldots_var),l) @@ -454,8 +465,10 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with let (alp,sigma) = List.fold_left2 (match_names metas) (alp,sigma) nal1 nal2 in match_ alp metas sigma c1 c2 - | RCast(_,c1,_,t1), ACast(c2,_,t2) -> + | RCast(_,c1, CastConv(_,t1)), ACast(c2, CastConv (_,t2)) -> match_ alp metas (match_ alp metas sigma c1 c2) t1 t2 + | RCast(_,c1, CastCoerce), ACast(c2, CastCoerce) -> + match_ alp metas sigma c1 c2 | RSort (_,s1), ASort s2 when s1 = s2 -> sigma | RPatVar _, AHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match | a, AHole _ -> sigma @@ -554,7 +567,7 @@ type constr_expr = | CPatVar of loc * (bool * patvar) | CEvar of loc * existential_key | CSort of loc * rawsort - | CCast of loc * constr_expr * cast_type * constr_expr + | CCast of loc * constr_expr * constr_expr cast_type | CNotation of loc * notation * constr_expr list | CPrim of loc * prim_token | CDelimiters of loc * string * constr_expr @@ -616,7 +629,7 @@ let constr_loc = function | CPatVar (loc,_) -> loc | CEvar (loc,_) -> loc | CSort (loc,_) -> loc - | CCast (loc,_,_,_) -> loc + | CCast (loc,_,_) -> loc | CNotation (loc,_,_) -> loc | CPrim (loc,_) -> loc | CDelimiters (loc,_,_) -> loc @@ -694,7 +707,8 @@ let fold_constr_expr_with_binders g f n acc = function | CApp (loc,(_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l) | CProdN (_,l,b) | CLambdaN (_,l,b) -> fold_constr_expr_binders g f n acc b l | CLetIn (_,na,a,b) -> fold_constr_expr_binders g f n acc b [[na],a] - | CCast (loc,a,_,b) -> f n (f n acc a) b + | CCast (loc,a,CastConv(_,b)) -> f n (f n acc a) b + | CCast (loc,a,CastCoerce) -> f n acc a | CNotation (_,_,l) -> List.fold_left (f n) acc l | CDelimiters (loc,_,a) -> f n acc a | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CDynamic _ | CRef _ -> @@ -731,7 +745,7 @@ let occur_var_constr_expr id c = Idset.mem id (free_vars_of_constr_expr c) let mkIdentC id = CRef (Ident (dummy_loc, id)) let mkRefC r = CRef r let mkAppC (f,l) = CApp (dummy_loc, (None,f), List.map (fun x -> (x,None)) l) -let mkCastC (a,k,b) = CCast (dummy_loc,a,k,b) +let mkCastC (a,k) = CCast (dummy_loc,a,k) let mkLambdaC (idl,a,b) = CLambdaN (dummy_loc,[idl,a],b) let mkLetInC (id,a,b) = CLetIn (dummy_loc,id,a,b) let mkProdC (idl,a,b) = CProdN (dummy_loc,[idl,a],b) @@ -804,7 +818,8 @@ let map_constr_expr_with_binders g f e = function | CLambdaN (loc,bl,b) -> let (e,bl) = map_binders f g e bl in CLambdaN (loc,bl,f e b) | CLetIn (loc,na,a,b) -> CLetIn (loc,na,f e a,f (name_fold g (snd na) e) b) - | CCast (loc,a,k,b) -> CCast (loc,f e a,k,f e b) + | CCast (loc,a,CastConv (k,b)) -> CCast (loc,f e a,CastConv(k, f e b)) + | CCast (loc,a,CastCoerce) -> CCast (loc,f e a,CastCoerce) | CNotation (loc,n,l) -> CNotation (loc,n,List.map (f e) l) | CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a) | CHole _ | CEvar _ | CPatVar _ | CSort _ diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 7d1a7a8096..75dbb7cf2b 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_type * aconstr + | ACast of aconstr * aconstr cast_type (**********************************************************************) (* Translate a rawconstr into a notation given the list of variables *) @@ -127,7 +127,7 @@ type constr_expr = | CPatVar of loc * (bool * patvar) | CEvar of loc * existential_key | CSort of loc * rawsort - | CCast of loc * constr_expr * cast_type * constr_expr + | CCast of loc * constr_expr * constr_expr cast_type | CNotation of loc * notation * constr_expr list | CPrim of loc * prim_token | CDelimiters of loc * string * constr_expr @@ -167,7 +167,7 @@ val ids_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_type * constr_expr -> constr_expr +val mkCastC : constr_expr * constr_expr cast_type -> 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 e05fe036d2..fb3c7940ba 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, CastConv DEFAULTcast, ty) + | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, CastConv (DEFAULTcast, ty)) let mk_lam = function ([],c) -> c @@ -138,13 +138,15 @@ GEXTEND Gram [ c = binder_constr -> c ] | "100" RIGHTA [ c1 = operconstr; "<:"; c2 = binder_constr -> - CCast(loc,c1, CastConv VMcast,c2) + CCast(loc,c1, CastConv (VMcast,c2)) | c1 = operconstr; "<:"; c2 = SELF -> - CCast(loc,c1, CastConv VMcast,c2) + CCast(loc,c1, CastConv (VMcast,c2)) | c1 = operconstr; ":";c2 = binder_constr -> - CCast(loc,c1, CastConv DEFAULTcast,c2) + CCast(loc,c1, CastConv (DEFAULTcast,c2)) | c1 = operconstr; ":"; c2 = SELF -> - CCast(loc,c1, CastConv DEFAULTcast,c2) ] + CCast(loc,c1, CastConv (DEFAULTcast,c2)) + | c1 = operconstr; ":>" -> + CCast(loc,c1, CastCoerce) ] | "99" RIGHTA [ ] | "90" RIGHTA [ c1 = operconstr; "->"; c2 = binder_constr -> CArrow(loc,c1,c2) @@ -317,7 +319,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, CastConv 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 afa5160116..e13962ce88 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -118,6 +118,6 @@ GEXTEND Gram ; constr_body: [ [ ":="; c = lconstr -> c - | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c, Rawterm.CastConv Term.DEFAULTcast,t) ] ] + | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c, Rawterm.CastConv (Term.DEFAULTcast,t)) ] ] ; END diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 4c9056f09b..34d7997456 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -204,7 +204,7 @@ GEXTEND Gram def_body: [ [ bl = LIST0 binder_let; ":="; red = reduce; c = lconstr -> (match c with - CCast(_,c,k,t) -> DefineBody (bl, red, c, Some t) + CCast(_,c, Rawterm.CastConv (k,t)) -> DefineBody (bl, red, c, Some t) | _ -> DefineBody (bl, red, c, None)) | bl = LIST0 binder_let; ":"; t = lconstr; ":="; red = reduce; c = lconstr -> DefineBody (bl, red, c, Some t) @@ -306,7 +306,7 @@ GEXTEND Gram t = lconstr; ":="; b = lconstr -> (oc,DefExpr (id,b,Some t)) | id = name; ":="; b = lconstr -> match b with - CCast(_,b,_,t) -> (false,DefExpr(id,b,Some t)) + CCast(_,b, Rawterm.CastConv (_, t)) -> (false,DefExpr(id,b,Some t)) | _ -> (false,DefExpr(id,b,None)) ] ] ; assum_list: diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index a1181939f7..dea45ac11c 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -183,7 +183,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, CastConv 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/parsing/ppconstr.ml b/parsing/ppconstr.ml index 901866523f..f0a44311bc 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -215,7 +215,7 @@ let pr_binder_among_many pr_c = function pr_binder true pr_c (nal,t) | LocalRawDef (na,c) -> let c,topt = match c with - | CCast(_,c,_,t) -> c, t + | CCast(_,c, CastConv (_,t)) -> c, t | _ -> c, CHole dummy_loc in hov 1 (surround (pr_lname na ++ pr_opt_type pr_c topt ++ @@ -566,10 +566,13 @@ let rec pr sep inherited a = | CEvar (_,n) -> str (Evd.string_of_existential n), latom | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom | CSort (_,s) -> pr_rawsort s, latom - | CCast (_,a,k,b) -> - let s = match k with CastConv VMcast -> "<:" | _ -> ":" in + | CCast (_,a,CastConv (k,b)) -> + let s = match k with VMcast -> "<:" | DEFAULTcast -> ":" in hv 0 (pr mt (lcast,L) a ++ cut () ++ str s ++ pr mt (-lcast,E) b), lcast + | CCast (_,a,CastCoerce) -> + hv 0 (pr mt (lcast,L) a ++ cut () ++ str ":>"), + lcast | CNotation (_,"( _ )",[t]) -> pr (fun()->str"(") (max_int,L) t ++ str")", latom | CNotation (_,s,env) -> pr_notation (pr mt) s env @@ -590,7 +593,7 @@ let pr = pr mt let rec strip_context n iscast t = if n = 0 then - [], if iscast then match t with CCast (_,c,_,_) -> c | _ -> t else t + [], if iscast then match t with CCast (_,c,_) -> c | _ -> t else t else match t with | CLambdaN (loc,(nal,t)::bll,c) -> let n' = List.length nal in @@ -613,7 +616,7 @@ let rec strip_context n iscast t = | CArrow (loc,t,c) -> let bl', c = strip_context (n-1) iscast c in LocalRawAssum ([loc,Anonymous],t) :: bl', c - | CCast (_,c,_,_) -> strip_context n false c + | CCast (_,c,_) -> strip_context n false c | CLetIn (_,na,b,c) -> let bl', c = strip_context (n-1) iscast c in LocalRawDef (na,b) :: bl', c diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4 index 768bc45c14..21c851dfbe 100644 --- a/parsing/q_constr.ml4 +++ b/parsing/q_constr.ml4 @@ -73,7 +73,7 @@ EXTEND | "0" [ s = sort -> <:expr< Rawterm.RSort ($dloc$,s) >> | id = ident -> <:expr< Rawterm.RVar ($dloc$,$id$) >> - | "_" -> <:expr< Rawterm.RHole ($dloc$,QuestionMark) >> + | "_" -> <:expr< Rawterm.RHole ($dloc$, QuestionMark False) >> | "?"; id = ident -> <:expr< Rawterm.RPatVar($dloc$,(False,$id$)) >> | "{"; c1 = constr; "}"; "+"; "{"; c2 = constr; "}" -> apply_ref <:expr< coq_sumbool_ref >> [c1;c2] diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index a0071d5b6d..412275c108 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -380,8 +380,7 @@ let rec detype (isgoal:bool) avoid env t = RVar (dl, id)) | Sort s -> RSort (dl,detype_sort s) | Cast (c1,k,c2) -> - RCast(dl,detype isgoal avoid env c1, CastConv k, - detype isgoal avoid env c2) + 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 | LetIn (na,b,_,c) -> detype_binder isgoal BLetIn avoid env na b c @@ -633,14 +632,18 @@ let rec subst_rawconstr subst raw = let ref',_ = subst_global subst ref in if ref' == ref then raw else RHole (loc,InternalHole) - | RHole (loc, (BinderType _ | QuestionMark | CasesType | + | RHole (loc, (BinderType _ | QuestionMark _ | CasesType | InternalHole | TomatchTypeParameter _)) -> raw - | RCast (loc,r1,k,r2) -> - let r1' = subst_rawconstr subst r1 and r2' = subst_rawconstr subst r2 in - if r1' == r1 && r2' == r2 then raw else - RCast (loc,r1',k,r2') - + | RCast (loc,r1,k) -> + (match k with + CastConv (k,r2) -> + let r1' = subst_rawconstr subst r1 and r2' = subst_rawconstr subst r2 in + if r1' == r1 && r2' == r2 then raw else + RCast (loc,r1', CastConv (k,r2')) + | CastCoerce -> + let r1' = subst_rawconstr subst r1 in + if r1' == r1 then raw else RCast (loc,r1',k)) | RDynamic _ -> raw (* Utilities to transform kernel cases to simple pattern-matching problem *) diff --git a/pretyping/evd.ml b/pretyping/evd.ml index a247b5b1ef..b9a443317f 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -366,7 +366,7 @@ let metamap_to_list m = type hole_kind = | ImplicitArg of global_reference * (int * identifier option) | BinderType of name - | QuestionMark + | QuestionMark of bool | CasesType | InternalHole | TomatchTypeParameter of inductive * int diff --git a/pretyping/evd.mli b/pretyping/evd.mli index ac1ed145af..8a1f6a53f3 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -132,7 +132,7 @@ val evars_reset_evd : evar_map -> evar_defs -> evar_defs type hole_kind = | ImplicitArg of global_reference * (int * identifier option) | BinderType of name - | QuestionMark + | QuestionMark of bool (* Can it be turned into an obligation ? *) | CasesType | InternalHole | TomatchTypeParameter of inductive * int diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index b0fd76cb76..c3b49b9749 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -233,7 +233,7 @@ let rec pat_of_raw metas vars = function PSort s | RHole _ -> PMeta None - | RCast (_,c,_,t) -> + | RCast (_,c,_) -> Options.if_verbose Pp.warning "Cast not taken into account in constr pattern"; pat_of_raw metas vars c diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index dc3ea869c1..3aefeeb077 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -578,13 +578,13 @@ module Pretyping_F (Coercion : Coercion.S) = struct ((fun vtyc env -> pretype vtyc env isevars lvar),isevars) tycon env (* loc *) (po,tml,eqns) - | RCast(loc,c,k,t) -> + | RCast (loc,c,k) -> 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 -> + | CastConv (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*) diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index 683182bc1f..63e40a0521 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -47,8 +47,8 @@ type 'a bindings = type 'a with_bindings = 'a * 'a bindings -type cast_type = - | CastConv of cast_kind +type 'a cast_type = + | CastConv of cast_kind * 'a | CastCoerce (* Cast to a base type (eg, an underlying inductive type) *) type rawconstr = @@ -68,7 +68,7 @@ type rawconstr = rawconstr array * rawconstr array | RSort of loc * rawsort | RHole of (loc * hole_kind) - | RCast of loc * rawconstr * cast_type * rawconstr + | RCast of loc * rawconstr * rawconstr cast_type | RDynamic of loc * Dyn.t and rawdecl = name * rawconstr option * rawconstr @@ -120,7 +120,7 @@ let map_rawconstr f = function | RRec (loc,fk,idl,bl,tyl,bv) -> RRec (loc,fk,idl,Array.map (List.map (map_rawdecl f)) bl, Array.map f tyl,Array.map f bv) - | RCast (loc,c,k,t) -> RCast (loc,f c,k,f t) + | RCast (loc,c,k) -> RCast (loc,f c, match k with CastConv (k,t) -> CastConv (k, f t) | x -> x) | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) as x -> x @@ -190,7 +190,7 @@ let occur_rawconstr id = (na=Name id or not(occur_fix bl)) in occur_fix bl) idl bl tyl bv) - | RCast (loc,c,_,t) -> (occur c) or (occur t) + | RCast (loc,c,k) -> (occur c) or (match k with CastConv (_, t) -> occur t | CastCoerce -> false) | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> false and occur_pattern (loc,idl,p,c) = not (List.mem id idl) & (occur c) @@ -247,7 +247,8 @@ let free_rawvars = vars bounded1 vs2 bv.(i) in array_fold_left_i vars_fix vs idl - | RCast (loc,c,_,t) -> vars bounded (vars bounded vs c) t + | RCast (loc,c,k) -> let v = vars bounded vs c in + (match k with CastConv (_,t) -> vars bounded v t | _ -> v) | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> vs and vars_pattern bounded vs (loc,idl,p,c) = @@ -280,7 +281,7 @@ let loc_of_rawconstr = function | RRec (loc,_,_,_,_,_) -> loc | RSort (loc,_) -> loc | RHole (loc,_) -> loc - | RCast (loc,_,_,_) -> loc + | RCast (loc,_,_) -> loc | RDynamic (loc,_) -> loc (**********************************************************************) diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 2a1fef22cd..c43c290e86 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -51,8 +51,8 @@ type 'a bindings = type 'a with_bindings = 'a * 'a bindings -type cast_type = - | CastConv of cast_kind +type 'a cast_type = + | CastConv of cast_kind * 'a | CastCoerce (* Cast to a base type (eg, an underlying inductive type) *) type rawconstr = @@ -72,7 +72,7 @@ type rawconstr = rawconstr array * rawconstr array | RSort of loc * rawsort | RHole of (loc * Evd.hole_kind) - | RCast of loc * rawconstr * cast_type * rawconstr + | RCast of loc * rawconstr * rawconstr cast_type | RDynamic of loc * Dyn.t and rawdecl = name * rawconstr option * rawconstr diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml index f341580eb1..87a472003f 100644 --- a/tactics/decl_interp.ml +++ b/tactics/decl_interp.ml @@ -346,7 +346,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = (fun (loc,(id,_)) -> RVar (loc,id)) params in let dum_args= - list_tabulate (fun _ -> RHole (dummy_loc,Evd.QuestionMark)) + list_tabulate (fun _ -> RHole (dummy_loc,Evd.QuestionMark false)) oib.Declarations.mind_nrealargs in raw_app(dummy_loc,rind,rparams@rparams_rec@dum_args) in let pat_vars,aliases,patt = interp_pattern env pat in @@ -369,7 +369,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = let term2 = RLetIn(dummy_loc,Anonymous, RCast(dummy_loc,raw_of_pat npatt, - CastConv DEFAULTcast,app_ind),term1) in + CastConv (DEFAULTcast,app_ind)),term1) in let term3=List.fold_right let_in_one_alias aliases term2 in let term4=List.fold_right prod_one_id loc_ids term3 in let term5=List.fold_right prod_one_hyp params term4 in diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 971e0986ae..75f517023f 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1246,7 +1246,7 @@ open Evd let solvable_by_tactic env evi (ev,args) src = match (!implicit_tactic, src) with - | Some tac, (ImplicitArg _ | QuestionMark) + | Some tac, (ImplicitArg _ | QuestionMark _) when Environ.named_context_of_val evi.evar_hyps = Environ.named_context env -> diff --git a/toplevel/command.ml b/toplevel/command.ml index 739a7b47f7..ecd0a6d7e3 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -111,7 +111,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, Rawterm.CastConv 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/command.mli b/toplevel/command.mli index c4ef924474..9540888dd3 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -36,6 +36,9 @@ val declare_definition : identifier -> definition_kind -> val syntax_definition : identifier -> constr_expr -> bool -> bool -> unit +val declare_one_assumption : coercion_flag -> assumption_kind -> Term.types -> + Names.variable located -> unit + val declare_assumption : identifier located list -> coercion_flag -> assumption_kind -> local_binder list -> constr_expr -> unit diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 305685cc7b..49a1d07f7d 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -329,7 +329,7 @@ let explain_occur_check env ev rhs = str" with term" ++ brk(1,1) ++ pt let explain_hole_kind env = function - | QuestionMark -> str "a term for this placeholder" + | QuestionMark _ -> str "a term for this placeholder" | CasesType -> str "the type of this pattern-matching problem" | BinderType (Name id) -> diff --git a/toplevel/record.ml b/toplevel/record.ml index f3ec4732d7..b339d493b3 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, Rawterm.CastConv 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) diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index eb9fdae30e..b41bcec8b0 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -139,11 +139,11 @@ let rec uri_of_constr c = | RLetIn (_,na,b,c) -> url_string "let "; url_of_name na; url_string "\\def "; uri_of_constr b; url_string " in "; uri_of_constr c - | RCast (_,c,_,t) -> + | RCast (_,c, CastConv (_,t)) -> uri_of_constr c; url_string ":"; uri_of_constr t | RRec _ | RIf _ | RLetTuple _ | RCases _ -> error "Whelp does not support pattern-matching and (co-)fixpoint" - | RVar _ | RRef _ | RHole _ | REvar _ | RSort _ -> + | RVar _ | RRef _ | RHole _ | REvar _ | RSort _ | RCast (_,_, CastCoerce) -> anomaly "Written w/o parenthesis" | RPatVar _ | RDynamic _ -> anomaly "Found constructors not supported in constr") () |