diff options
Diffstat (limited to 'contrib/subtac')
-rw-r--r-- | contrib/subtac/g_subtac.ml4 | 6 | ||||
-rw-r--r-- | contrib/subtac/subtac.ml | 5 | ||||
-rw-r--r-- | contrib/subtac/subtac_cases.ml | 8 | ||||
-rw-r--r-- | contrib/subtac/subtac_classes.ml | 43 | ||||
-rw-r--r-- | contrib/subtac/subtac_classes.mli | 10 | ||||
-rw-r--r-- | contrib/subtac/subtac_coercion.ml | 65 | ||||
-rw-r--r-- | contrib/subtac/subtac_command.ml | 27 | ||||
-rw-r--r-- | contrib/subtac/subtac_command.mli | 1 | ||||
-rw-r--r-- | contrib/subtac/subtac_obligations.ml | 3 | ||||
-rw-r--r-- | contrib/subtac/subtac_pretyping.ml | 11 | ||||
-rw-r--r-- | contrib/subtac/subtac_pretyping_F.ml | 51 | ||||
-rw-r--r-- | contrib/subtac/test/ListsTest.v | 20 | ||||
-rw-r--r-- | contrib/subtac/test/take.v | 18 |
13 files changed, 132 insertions, 136 deletions
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4 index 88243b60..4cf5336d 100644 --- a/contrib/subtac/g_subtac.ml4 +++ b/contrib/subtac/g_subtac.ml4 @@ -14,7 +14,7 @@ Syntax for the subtac terms and types. Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliātre *) -(* $Id: g_subtac.ml4 10919 2008-05-11 22:04:26Z msozeau $ *) +(* $Id: g_subtac.ml4 11282 2008-07-28 11:51:53Z msozeau $ *) open Flags @@ -139,10 +139,10 @@ VERNAC COMMAND EXTEND Subtac_Admit_Obligations END VERNAC COMMAND EXTEND Subtac_Set_Solver -| [ "Obligations" "Tactic" ":=" tactic(t) ] -> [ +| [ "Obligation" "Tactic" ":=" tactic(t) ] -> [ Coqlib.check_required_library ["Coq";"Program";"Tactics"]; Tacinterp.add_tacdef false - [(Qualid (dummy_loc, qualid_of_string "Coq.Program.Tactics.obligations_tactic"), true, t)] ] + [(Qualid (dummy_loc, qualid_of_string "Coq.Program.Tactics.obligation_tactic"), true, t)] ] END VERNAC COMMAND EXTEND Subtac_Show_Obligations diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml index a59ad6f5..7bfa107b 100644 --- a/contrib/subtac/subtac.ml +++ b/contrib/subtac/subtac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac.ml 11150 2008-06-19 11:38:27Z msozeau $ *) +(* $Id: subtac.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Global open Pp @@ -229,7 +229,8 @@ let subtac (loc, command) = debug 2 (Himsg.explain_pretype_error env exn); raise e - | (Stdpp.Exc_located (loc, e')) as e -> + | (Stdpp.Exc_located (loc, Proof_type.LtacLocated (_,e')) | + Stdpp.Exc_located (loc, e') as e) -> debug 2 (str "Parsing exception: "); (match e' with | Type_errors.TypeError (env, exn) -> diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml index c7182bd2..04bf54d3 100644 --- a/contrib/subtac/subtac_cases.ml +++ b/contrib/subtac/subtac_cases.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac_cases.ml 11154 2008-06-19 18:42:19Z msozeau $ *) +(* $Id: subtac_cases.ml 11282 2008-07-28 11:51:53Z msozeau $ *) open Cases open Util @@ -2056,8 +2056,10 @@ let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constra t, prepare_predicate_from_arsign_tycon loc env (Evd.evars_of !isevars) tomatchs sign (lift tomatchs_len t) in - let arity = - it_mkProd_or_LetIn (lift neqs arity) (context_of_arsign eqs) + let neqs, arity = + let ctx = context_of_arsign eqs in + let neqs = List.length ctx in + neqs, it_mkProd_or_LetIn (lift neqs arity) ctx in let lets, matx = (* Type the rhs under the assumption of equations *) diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml index 15addb44..9a5539e2 100644 --- a/contrib/subtac/subtac_classes.ml +++ b/contrib/subtac/subtac_classes.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: subtac_classes.ml 11047 2008-06-03 23:08:00Z msozeau $ i*) +(*i $Id: subtac_classes.ml 11282 2008-07-28 11:51:53Z msozeau $ i*) open Pretyping open Evd @@ -73,26 +73,18 @@ let interp_casted_constr_evars evdref env ?(impls=([],[])) c typ = let type_ctx_instance isevars env ctx inst subst = List.fold_left2 (fun (subst, instctx) (na, _, t) ce -> - let t' = replace_vars subst t in + let t' = substl subst t in let c = interp_casted_constr_evars isevars env ce t' in + isevars := resolve_typeclasses ~onlyargs:true ~fail:true env !isevars; let d = na, Some c, t' in - (na, c) :: subst, d :: instctx) + c :: subst, d :: instctx) (subst, []) (List.rev ctx) inst -(*let superclass_ce = CRef (Ident (dummy_loc, id_of_string ".superclass"))*) - let type_class_instance_params isevars env id n ctx inst subst = List.fold_left2 (fun (subst, instctx) (na, _, t) ce -> let t' = replace_vars subst t in - let c = -(* if ce = superclass_ce then *) - (* (\* Control over the evars which are direct superclasses to avoid partial instanciations *) - (* in instance search. *\) *) - (* Evarutil.e_new_evar isevars env ~src:(dummy_loc, ImplicitArg (VarRef id, (n, Some na))) t' *) - (* else *) - interp_casted_constr_evars isevars env ce t' - in + let c = interp_casted_constr_evars isevars env ce t' in let d = na, Some c, t' in (na, c) :: subst, d :: instctx) (subst, []) (List.rev ctx) inst @@ -140,9 +132,9 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class let k, ctx', imps, subst = let c = Command.generalize_constr_expr tclass ctx in let c', imps = interp_type_evars_impls ~evdref:isevars env c in - let ctx, c = Classes.decompose_named_assum c' in + let ctx, c = Sign.decompose_prod_assum c' in let cl, args = Typeclasses.dest_class_app c in - cl, ctx, imps, substitution_of_constrs (List.map snd cl.cl_context) (List.rev (Array.to_list args)) + cl, ctx, imps, (List.rev (Array.to_list args)) in let id = match snd instid with @@ -155,11 +147,11 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class let i = Nameops.add_suffix (Classes.id_of_class k) "_instance_0" in Termops.next_global_ident_away false i (Termops.ids_of_context env) in - let env' = Classes.push_named_context ctx' env in + let env' = push_rel_context ctx' env in isevars := Evarutil.nf_evar_defs !isevars; isevars := resolve_typeclasses ~onlyargs:false ~fail:true env' !isevars; let sigma = Evd.evars_of !isevars in - let substctx = Typeclasses.nf_substitution sigma subst in + let substctx = List.map (Evarutil.nf_evar sigma) subst in let subst, _propsctx = let props = List.map (fun (x, l, d) -> @@ -172,8 +164,8 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class List.fold_left (fun (props, rest) (id,_,_) -> try - let ((loc, mid), c) = List.find (fun ((_,id'), c) -> id' = id) rest in - let rest' = List.filter (fun ((_,id'), c) -> id' <> id) rest in + let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in + let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in Constrintern.add_glob loc (ConstRef (List.assoc mid k.cl_projs)); c :: props, rest' with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest) @@ -184,20 +176,13 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class else type_ctx_instance isevars env' k.cl_props props substctx in - let inst_constr, ty_constr = instance_constructor k (List.rev_map snd subst) in + let inst_constr, ty_constr = instance_constructor k (List.rev subst) in isevars := Evarutil.nf_evar_defs !isevars; - let term = Evarutil.nf_isevar !isevars (it_mkNamedLambda_or_LetIn inst_constr ctx') - and termtype = Evarutil.nf_isevar !isevars (it_mkNamedProd_or_LetIn ty_constr ctx') + let term = Evarutil.nf_isevar !isevars (it_mkLambda_or_LetIn inst_constr ctx') + and termtype = Evarutil.nf_isevar !isevars (it_mkProd_or_LetIn ty_constr ctx') in isevars := undefined_evars !isevars; Evarutil.check_evars env Evd.empty !isevars termtype; -(* let imps = *) -(* Util.list_map_i *) -(* (fun i binder -> *) -(* match binder with *) -(* ExplByPos (i, Some na), (true, true)) *) -(* 1 ctx *) -(* in *) let hook gr = let cst = match gr with ConstRef kn -> kn | _ -> assert false in let inst = Typeclasses.new_instance k pri global cst in diff --git a/contrib/subtac/subtac_classes.mli b/contrib/subtac/subtac_classes.mli index 43f00107..afb0d38d 100644 --- a/contrib/subtac/subtac_classes.mli +++ b/contrib/subtac/subtac_classes.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: subtac_classes.mli 10797 2008-04-15 13:19:33Z msozeau $ i*) +(*i $Id: subtac_classes.mli 11282 2008-07-28 11:51:53Z msozeau $ i*) (*i*) open Names @@ -26,11 +26,11 @@ open Classes val type_ctx_instance : Evd.evar_defs ref -> Environ.env -> - (Names.identifier * 'a * Term.constr) list -> + ('a * Term.constr option * Term.constr) list -> Topconstr.constr_expr list -> - (Names.identifier * Term.constr) list -> - (Names.identifier * Term.constr) list * - (Names.identifier * Term.constr option * Term.constr) list + Term.constr list -> + Term.constr list * + ('a * Term.constr option * Term.constr) list val new_instance : ?global:bool -> diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml index b45e23d0..b046f0b3 100644 --- a/contrib/subtac/subtac_coercion.ml +++ b/contrib/subtac/subtac_coercion.ml @@ -6,7 +6,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac_coercion.ml 11143 2008-06-18 15:52:42Z msozeau $ *) +(* $Id: subtac_coercion.ml 11282 2008-07-28 11:51:53Z msozeau $ *) open Util open Names @@ -111,41 +111,31 @@ module Coercion = struct : (Term.constr -> Term.constr) option = let x = nf_evar (evars_of !isevars) x and y = nf_evar (evars_of !isevars) y in -(* (try debug 1 (str "Coerce called for " ++ (my_print_constr env x) ++ *) -(* str " and "++ my_print_constr env y ++ *) -(* str " with evars: " ++ spc () ++ *) -(* my_print_evardefs !isevars); *) -(* with _ -> ()); *) let rec coerce_unify env x y = -(* (try debug 1 (str "coerce_unify from " ++ (my_print_constr env x) ++ *) -(* str " to "++ my_print_constr env y) *) -(* with _ -> ()); *) let x = hnf env isevars x and y = hnf env isevars y in try isevars := the_conv_x_leq env x y !isevars; - (* (try debug 1 (str "Unified " ++ (my_print_constr env x) ++ *) - (* str " and "++ my_print_constr env y); *) - (* with _ -> ()); *) None with Reduction.NotConvertible -> coerce' env x y and coerce' env x y : (Term.constr -> Term.constr) option = let subco () = subset_coerce env isevars x y in + let dest_prod c = + match Reductionops.decomp_n_prod env (evars_of !isevars) 1 c with + | [(na,b,t)], c -> (na,t), c + | _ -> raise NoSubtacCoercion + in let rec coerce_application typ typ' c c' l l' = let len = Array.length l in let rec aux tele typ typ' i co = -(* (try trace (str "coerce_application.aux from " ++ (my_print_constr env x) ++ *) -(* str " to "++ my_print_constr env y *) -(* ++ str "in env:" ++ my_print_env env); *) -(* with _ -> ()); *) if i < len then let hdx = l.(i) and hdy = l'.(i) in try isevars := the_conv_x_leq env hdx hdy !isevars; - let (n, eqT, restT) = destProd typ in - let (n', eqT', restT') = destProd typ' in + let (n, eqT), restT = dest_prod typ in + let (n', eqT'), restT' = dest_prod typ' in aux (hdx :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) co with Reduction.NotConvertible -> - let (n, eqT, restT) = destProd typ in - let (n', eqT', restT') = destProd typ' in + let (n, eqT), restT = dest_prod typ in + let (n', eqT'), restT' = dest_prod typ' in let _ = try isevars := the_conv_x_leq env eqT eqT' !isevars with Reduction.NotConvertible -> raise NoSubtacCoercion @@ -163,12 +153,12 @@ module Coercion = struct [| eqT; hdx; pred; x; hdy; evar|]) in aux (hdy :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) (fun x -> eq_app (co x)) else Some co - in aux [] typ typ' 0 (fun x -> x) + in + if isEvar c || isEvar c' then + (* Second-order unification needed. *) + raise NoSubtacCoercion; + aux [] typ typ' 0 (fun x -> x) in -(* (try trace (str "coerce' from " ++ (my_print_constr env x) ++ *) -(* str " to "++ my_print_constr env y *) -(* ++ str "in env:" ++ my_print_env env); *) -(* with _ -> ()); *) match (kind_of_term x, kind_of_term y) with | Sort s, Sort s' -> (match s, s' with @@ -179,13 +169,6 @@ module Coercion = struct | Prod (name, a, b), Prod (name', a', b') -> let name' = Name (Nameops.next_ident_away (id_of_string "x") (Termops.ids_of_context env)) in let env' = push_rel (name', None, a') env in - -(* let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in *) -(* let name'' = Name (Nameops.next_ident_away (id_of_string "x'") (Termops.ids_of_context env)) in *) -(* let env'' = push_rel (name'', Some (app_opt c1 (mkRel 1)), lift 1 a) env' in *) -(* let c2 = coerce_unify env'' (liftn 1 1 b) (lift 1 b') in *) -(* mkLetIn (name'', app_opt c1 (mkRel 1), (lift 1 a), *) - let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in (* env, x : a' |- c1 : lift 1 a' > lift 1 a *) let coec1 = app_opt c1 (mkRel 1) in @@ -295,7 +278,6 @@ module Coercion = struct and subset_coerce env isevars x y = match disc_subset x with Some (u, p) -> - (* trace (str "Inserting projection "); *) let c = coerce_unify env u y in let f x = app_opt c (mkApp ((Lazy.force sig_).proj1, @@ -423,7 +405,11 @@ module Coercion = struct isevars, { uj_val = app_opt ct j.uj_val; uj_type = typ' } - + let inh_coerce_to_prod loc env isevars t = + let typ = whd_betadeltaiota env (evars_of isevars) (snd t) in + let _, typ' = mu env isevars typ in + isevars, (fst t, typ') + let inh_coerce_to_fail env evd rigidonly v t c1 = if rigidonly & not (Heads.is_rigid env c1 && Heads.is_rigid env t) then @@ -504,14 +490,13 @@ module Coercion = struct None -> 0, 0 | Some (init, cur) -> init, cur in - (* a little more effort to get products is needed *) - try let rels, rng = decompose_prod_n nabs t in + try + let rels, rng = Reductionops.decomp_n_prod env (evars_of isevars) nabs t in (* The final range free variables must have been replaced by evars, we accept only that evars in rng are applied to free vars. *) - if noccur_with_meta 0 (succ nabsinit) rng then ( -(* trace (str "No occur between 0 and " ++ int (succ nabsinit)); *) + if noccur_with_meta 1 (succ nabs) rng then ( let env', t, t' = - let env' = List.fold_right (fun (n, t) env -> push_rel (n, None, t) env) rels env in + let env' = push_rel_context rels env in env', rng, lift nabs t' in try @@ -523,6 +508,4 @@ module Coercion = struct error_cannot_coerce env' sigma (t, t')) else isevars with _ -> isevars -(* trace (str "decompose_prod_n failed"); *) -(* raise (Invalid_argument "Subtac_coercion.inh_conv_coerces_to") *) end diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index 5bff6ad1..a2f54b02 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -350,9 +350,27 @@ let compute_possible_guardness_evidences (n,_) (_, fixctx) fixtype = let push_named_context = List.fold_right push_named +let check_evars env initial_sigma evd c = + let sigma = evars_of evd in + let c = nf_evar sigma c in + let rec proc_rec c = + match kind_of_term c with + | Evar (evk,args) -> + assert (Evd.mem sigma evk); + if not (Evd.mem initial_sigma evk) then + let (loc,k) = evar_source evk evd in + (match k with + | QuestionMark _ -> () + | _ -> + let evi = nf_evar_info sigma (Evd.find sigma evk) in + Pretype_errors.error_unsolvable_implicit loc env sigma evi k None) + | _ -> iter_constr proc_rec c + in proc_rec c + let interp_recursive fixkind l boxed = let env = Global.env() in let fixl, ntnl = List.split l in + let kind = if fixkind <> Command.IsCoFixpoint then Fixpoint else CoFixpoint in let fixnames = List.map (fun fix -> fix.Command.fix_name) fixl in (* Interp arities allowing for unresolved types *) @@ -384,20 +402,17 @@ let interp_recursive fixkind l boxed = let rec_sign = nf_named_context_evar (evars_of evd) rec_sign in let recdefs = List.length rec_sign in -(* List.iter (check_evars env_rec Evd.empty evd) fixdefs; *) -(* List.iter (check_evars env Evd.empty evd) fixtypes; *) -(* check_mutuality env kind (List.combine fixnames fixdefs); *) + List.iter (check_evars env_rec Evd.empty evd) fixdefs; + List.iter (check_evars env Evd.empty evd) fixtypes; + Command.check_mutuality env kind (List.combine fixnames fixdefs); (* Russell-specific code *) (* Get the interesting evars, those that were not instanciated *) let isevars = Evd.undefined_evars evd in - trace (str "got undefined evars" ++ Evd.pr_evar_defs isevars); let evm = Evd.evars_of isevars in - trace (str "got the evm, recdefs is " ++ int recdefs); (* Solve remaining evars *) let rec collect_evars id def typ imps = - let _ = try trace (str "In collect evars, isevars is: " ++ Evd.pr_evar_defs isevars) with _ -> () in (* Generalize by the recursive prototypes *) let def = Termops.it_mkNamedLambda_or_LetIn def rec_sign diff --git a/contrib/subtac/subtac_command.mli b/contrib/subtac/subtac_command.mli index 27520867..3a6a351b 100644 --- a/contrib/subtac/subtac_command.mli +++ b/contrib/subtac/subtac_command.mli @@ -42,6 +42,7 @@ val interp_binder : Evd.evar_defs ref -> Environ.env -> Names.name -> Topconstr.constr_expr -> Term.constr + val build_recursive : (fixpoint_expr * decl_notation) list -> bool -> unit diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml index 55cdc7c4..a393e2c9 100644 --- a/contrib/subtac/subtac_obligations.ml +++ b/contrib/subtac/subtac_obligations.ml @@ -119,7 +119,7 @@ let from_prg : program_info ProgMap.t ref = ref ProgMap.empty let freeze () = !from_prg, !default_tactic_expr let unfreeze (v, t) = from_prg := v; set_default_tactic t let init () = - from_prg := ProgMap.empty; set_default_tactic (Subtac_utils.tactics_call "obligations_tactic" []) + from_prg := ProgMap.empty; set_default_tactic (Subtac_utils.tactics_call "obligation_tactic" []) let _ = Summary.declare_summary "program-tcc-table" @@ -442,6 +442,7 @@ and solve_obligation_by_tac prg obls i tac = true else false with + | Stdpp.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s))) | Stdpp.Exc_located(_, Refiner.FailError (_, s)) | Refiner.FailError (_, s) -> user_err_loc (obl.obl_location, "solve_obligation", s) diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml index 0e987cf2..ad76bdeb 100644 --- a/contrib/subtac/subtac_pretyping.ml +++ b/contrib/subtac/subtac_pretyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac_pretyping.ml 11047 2008-06-03 23:08:00Z msozeau $ *) +(* $Id: subtac_pretyping.ml 11282 2008-07-28 11:51:53Z msozeau $ *) open Global open Pp @@ -117,7 +117,6 @@ let env_with_binders env isevars l = in aux (env, []) l let subtac_process env isevars id bl c tycon = -(* let bl = Implicit_quantifiers.ctx_of_class_binders (vars_of_env env) cbl @ l in *) let c = Command.abstract_constr_expr c bl in let tycon = match tycon with @@ -132,12 +131,14 @@ let subtac_process env isevars id bl c tycon = let imps = Implicit_quantifiers.implicits_of_rawterm c in let coqc, ctyp = interp env isevars c tycon in let evm = non_instanciated_map env isevars (evars_of !isevars) in - evm, coqc, (match tycon with Some (None, c) -> c | _ -> ctyp), imps + let ty = nf_isevar !isevars (match tycon with Some (None, c) -> c | _ -> ctyp) in + evm, coqc, ty, imps open Subtac_obligations let subtac_proof kind env isevars id bl c tycon = let evm, coqc, coqt, imps = subtac_process env isevars id bl c tycon in - let evm = Subtac_utils.evars_of_term evm Evd.empty coqc in - let evars, def, ty = Eterm.eterm_obligations env id !isevars evm 0 coqc coqt in + let evm' = Subtac_utils.evars_of_term evm Evd.empty coqc in + let evm' = Subtac_utils.evars_of_term evm evm' coqt in + let evars, def, ty = Eterm.eterm_obligations env id !isevars evm' 0 coqc coqt in add_definition id def ty ~implicits:imps ~kind:kind evars diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml index afa5817f..559b6ac1 100644 --- a/contrib/subtac/subtac_pretyping_F.ml +++ b/contrib/subtac/subtac_pretyping_F.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac_pretyping_F.ml 11143 2008-06-18 15:52:42Z msozeau $ *) +(* $Id: subtac_pretyping_F.ml 11282 2008-07-28 11:51:53Z msozeau $ *) open Pp open Util @@ -246,6 +246,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct uj_type = it_mkProd_or_LetIn j.uj_type ctxt }) ctxtv vdef in evar_type_fixpoint loc env isevars names ftys vdefj; + let ftys = Array.map (nf_evar (evars_of !isevars)) ftys in + let fdefs = Array.map (fun x -> nf_evar (evars_of !isevars) (j_val x)) vdefj in let fixj = match fixkind with | RFix (vn,i) -> (* First, let's find the guard indexes. *) @@ -260,11 +262,11 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct | None -> list_map_i (fun i _ -> i) 0 ctxtv.(i)) vn) in - let fixdecls = (names,ftys,Array.map j_val vdefj) in + let fixdecls = (names,ftys,fdefs) in let indexes = search_guard loc env possible_indexes fixdecls in make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) | RCoFix i -> - let cofix = (i,(names,ftys,Array.map j_val vdefj)) in + let cofix = (i,(names,ftys,fdefs)) 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 @@ -273,13 +275,15 @@ module SubtacPretyping_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 length = List.length args in let ftycon = - match tycon with - None -> None + if length > 0 then + 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) + else tycon in let fj = pretype ftycon env isevars lvar f in let floc = loc_of_rawconstr f in @@ -291,23 +295,13 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct 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 + Option.iter (fun ty -> isevars := + Coercion.inh_conv_coerces_to loc env !isevars resty ty) tycon; + let evd, (_, _, tycon) = split_tycon loc env !isevars tycon in + isevars := evd; + let hj = pretype (mk_tycon (nf_isevar !isevars 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' } @@ -319,7 +313,6 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct (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 @@ -332,12 +325,22 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct inh_conv_coerce_to_tycon loc env isevars resj tycon | RLambda(loc,name,k,c1,c2) -> - let (name',dom,rng) = evd_comb1 (split_tycon loc env) isevars tycon in + let tycon' = evd_comb1 + (fun evd tycon -> + match tycon with + | None -> evd, tycon + | Some ty -> + let evd, ty' = Coercion.inh_coerce_to_prod loc env evd ty in + evd, Some ty') + isevars tycon + in + 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' + let resj = judge_of_abstraction env name j j' in + inh_conv_coerce_to_tycon loc env isevars resj tycon | RProd(loc,name,k,c1,c2) -> let j = pretype_type empty_valcon env isevars lvar c1 in diff --git a/contrib/subtac/test/ListsTest.v b/contrib/subtac/test/ListsTest.v index 3ceea173..05fc0803 100644 --- a/contrib/subtac/test/ListsTest.v +++ b/contrib/subtac/test/ListsTest.v @@ -1,5 +1,5 @@ (* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *) -Require Import Coq.subtac.Utils. +Require Import Coq.Program.Program. Require Import List. Set Implicit Arguments. @@ -7,7 +7,7 @@ Set Implicit Arguments. Section Accessors. Variable A : Set. - 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 => ! @@ -39,7 +39,7 @@ Section app. Next Obligation. intros. - destruct_call app ; subtac_simpl. + destruct_call app ; program_simpl. Defined. Program Lemma app_id_l : forall l : list A, l = nil ++ l. @@ -49,7 +49,7 @@ Section app. Program Lemma app_id_r : forall l : list A, l = l ++ nil. Proof. - induction l ; simpl ; auto. + induction l ; simpl in * ; auto. rewrite <- IHl ; auto. Qed. @@ -70,16 +70,24 @@ Section Nth. Next Obligation. Proof. - intros. - inversion H. + simpl in *. auto with arith. Defined. + Next Obligation. + Proof. + inversion H. + Qed. + Program Fixpoint nth' (l : list A) (n : nat | n < length l) { struct l } : A := match l, n with | hd :: _, 0 => hd | _ :: tl, S n' => nth' tl n' | nil, _ => ! end. + Next Obligation. + Proof. + simpl in *. auto with arith. + Defined. Next Obligation. Proof. diff --git a/contrib/subtac/test/take.v b/contrib/subtac/test/take.v index 87ab47d6..2e17959c 100644 --- a/contrib/subtac/test/take.v +++ b/contrib/subtac/test/take.v @@ -1,9 +1,12 @@ (* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *) Require Import JMeq. Require Import List. -Require Import Coq.subtac.Utils. +Require Import Program. Set Implicit Arguments. +Obligations Tactic := idtac. + +Print cons. Program Fixpoint take (A : Set) (l : list A) (n : nat | n <= length l) { struct l } : { l' : list A | length l' = n } := match n with @@ -16,21 +19,14 @@ Program Fixpoint take (A : Set) (l : list A) (n : nat | n <= length l) { struct end. Require Import Omega. - +Solve All Obligations. Next Obligation. - intros. - simpl in l0. - apply le_S_n ; exact l0. -Defined. - -Next Obligation. - intros. - destruct_call take ; subtac_simpl. + destruct_call take ; program_simpl. Defined. Next Obligation. intros. - inversion l0. + inversion H. Defined. |