diff options
Diffstat (limited to 'tactics/eqschemes.ml')
| -rw-r--r-- | tactics/eqschemes.ml | 104 |
1 files changed, 53 insertions, 51 deletions
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index c9764af1..1a45217a 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -44,12 +44,11 @@ natural expectation of the user. *) -open Errors +open CErrors open Util open Names open Term open Vars -open Context open Declarations open Environ open Inductive @@ -58,6 +57,8 @@ open Namegen open Inductiveops open Ind_tables open Indrec +open Sigma.Notations +open Context.Rel.Declaration let hid = Id.of_string "H" let xid = Id.of_string "X" @@ -70,8 +71,8 @@ let build_dependent_inductive ind (mib,mip) = let realargs,_ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in applist (mkIndU ind, - extended_rel_list mip.mind_nrealdecls mib.mind_params_ctxt - @ extended_rel_list 0 realargs) + Context.Rel.to_extended_list mip.mind_nrealdecls mib.mind_params_ctxt + @ Context.Rel.to_extended_list 0 realargs) let my_it_mkLambda_or_LetIn s c = it_mkLambda_or_LetIn c s let my_it_mkProd_or_LetIn s c = it_mkProd_or_LetIn c s @@ -104,11 +105,11 @@ let get_sym_eq_data env (ind,u) = error "Not an inductive type with a single constructor."; let arityctxt = Vars.subst_instance_context u mip.mind_arity_ctxt in let realsign,_ = List.chop mip.mind_nrealdecls arityctxt in - if List.exists (fun (_,b,_) -> not (Option.is_empty b)) realsign then + if List.exists is_local_def realsign then error "Inductive equalities with local definitions in arity not supported."; let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in let _,constrargs = decompose_app ccl in - if not (Int.equal (rel_context_length constrsign) (rel_context_length mib.mind_params_ctxt)) then + if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then error "Constructor must have no arguments"; (* This can be relaxed... *) let params,constrargs = List.chop mib.mind_nparams constrargs in if mip.mind_nrealargs > mib.mind_nparams then @@ -139,11 +140,11 @@ let get_non_sym_eq_data env (ind,u) = error "Not an inductive type with a single constructor."; let arityctxt = Vars.subst_instance_context u mip.mind_arity_ctxt in let realsign,_ = List.chop mip.mind_nrealdecls arityctxt in - if List.exists (fun (_,b,_) -> not (Option.is_empty b)) realsign then + if List.exists is_local_def realsign then error "Inductive equalities with local definitions in arity not supported"; let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in let _,constrargs = decompose_app ccl in - if not (Int.equal (rel_context_length constrsign) (rel_context_length mib.mind_params_ctxt)) then + if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then error "Constructor must have no arguments"; let _,constrargs = List.chop mib.mind_nparams constrargs in let constrargs = List.map (Vars.subst_instance_constr u) constrargs in @@ -169,11 +170,11 @@ let build_sym_scheme env ind = let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 = get_sym_eq_data env indu in let cstr n = - mkApp (mkConstructUi(indu,1),extended_rel_vect n mib.mind_params_ctxt) in + mkApp (mkConstructUi(indu,1),Context.Rel.to_extended_vect n mib.mind_params_ctxt) in let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in let applied_ind = build_dependent_inductive indu specif in let realsign_ind = - name_context env ((Name varH,None,applied_ind)::realsign) in + name_context env ((LocalAssum (Name varH,applied_ind))::realsign) in let ci = make_case_info (Global.env()) ind RegularStyle in let c = (my_it_mkLambda_or_LetIn paramsctxt @@ -182,7 +183,7 @@ let build_sym_scheme env ind = my_it_mkLambda_or_LetIn_name (lift_rel_context (nrealargs+1) realsign_ind) (mkApp (mkIndU indu,Array.concat - [extended_rel_vect (3*nrealargs+2) paramsctxt1; + [Context.Rel.to_extended_vect (3*nrealargs+2) paramsctxt1; rel_vect 1 nrealargs; rel_vect (2*nrealargs+2) nrealargs])), mkRel 1 (* varH *), @@ -223,16 +224,16 @@ let build_sym_involutive_scheme env ind = get_sym_eq_data env indu in let eq,eqrefl,ctx = get_coq_eq ctx in let sym, ctx, eff = const_of_scheme sym_scheme_kind env ind ctx in - let cstr n = mkApp (mkConstructUi (indu,1),extended_rel_vect n paramsctxt) in + let cstr n = mkApp (mkConstructUi (indu,1),Context.Rel.to_extended_vect n paramsctxt) in let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in let applied_ind = build_dependent_inductive indu specif in let applied_ind_C = mkApp (mkIndU indu, Array.append - (extended_rel_vect (nrealargs+1) mib.mind_params_ctxt) + (Context.Rel.to_extended_vect (nrealargs+1) mib.mind_params_ctxt) (rel_vect (nrealargs+1) nrealargs)) in let realsign_ind = - name_context env ((Name varH,None,applied_ind)::realsign) in + name_context env ((LocalAssum (Name varH,applied_ind))::realsign) in let ci = make_case_info (Global.env()) ind RegularStyle in let c = (my_it_mkLambda_or_LetIn paramsctxt @@ -243,15 +244,15 @@ let build_sym_involutive_scheme env ind = (mkApp (eq,[| mkApp (mkIndU indu, Array.concat - [extended_rel_vect (3*nrealargs+2) paramsctxt1; + [Context.Rel.to_extended_vect (3*nrealargs+2) paramsctxt1; rel_vect (2*nrealargs+2) nrealargs; rel_vect 1 nrealargs]); mkApp (sym,Array.concat - [extended_rel_vect (3*nrealargs+2) paramsctxt1; + [Context.Rel.to_extended_vect (3*nrealargs+2) paramsctxt1; rel_vect 1 nrealargs; rel_vect (2*nrealargs+2) nrealargs; [|mkApp (sym,Array.concat - [extended_rel_vect (3*nrealargs+2) paramsctxt1; + [Context.Rel.to_extended_vect (3*nrealargs+2) paramsctxt1; rel_vect (2*nrealargs+2) nrealargs; rel_vect 1 nrealargs; [|mkRel 1|]])|]]); @@ -334,7 +335,7 @@ let build_l2r_rew_scheme dep env ind kind = let eq,eqrefl,ctx = get_coq_eq ctx in let cstr n p = mkApp (mkConstructUi(indu,1), - Array.concat [extended_rel_vect n paramsctxt1; + Array.concat [Context.Rel.to_extended_vect n paramsctxt1; rel_vect p nrealargs]) in let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in let varHC = fresh env (Id.of_string "HC") in @@ -342,26 +343,26 @@ let build_l2r_rew_scheme dep env ind kind = let applied_ind = build_dependent_inductive indu specif in let applied_ind_P = mkApp (mkIndU indu, Array.concat - [extended_rel_vect (3*nrealargs) paramsctxt1; + [Context.Rel.to_extended_vect (3*nrealargs) paramsctxt1; rel_vect 0 nrealargs; rel_vect nrealargs nrealargs]) in let applied_ind_G = mkApp (mkIndU indu, Array.concat - [extended_rel_vect (3*nrealargs+3) paramsctxt1; + [Context.Rel.to_extended_vect (3*nrealargs+3) paramsctxt1; rel_vect (nrealargs+3) nrealargs; rel_vect 0 nrealargs]) in let realsign_P = lift_rel_context nrealargs realsign in let realsign_ind_P = - name_context env ((Name varH,None,applied_ind_P)::realsign_P) in + name_context env ((LocalAssum (Name varH,applied_ind_P))::realsign_P) in let realsign_ind_G = - name_context env ((Name varH,None,applied_ind_G):: + name_context env ((LocalAssum (Name varH,applied_ind_G)):: lift_rel_context (nrealargs+3) realsign) in let applied_sym_C n = mkApp(sym, - Array.append (extended_rel_vect n mip.mind_arity_ctxt) [|mkVar varH|]) in + Array.append (Context.Rel.to_extended_vect n mip.mind_arity_ctxt) [|mkVar varH|]) in let applied_sym_G = mkApp(sym, - Array.concat [extended_rel_vect (nrealargs*3+4) paramsctxt1; + Array.concat [Context.Rel.to_extended_vect (nrealargs*3+4) paramsctxt1; rel_vect (nrealargs+4) nrealargs; rel_vect 1 nrealargs; [|mkRel 1|]]) in @@ -371,7 +372,7 @@ let build_l2r_rew_scheme dep env ind kind = let ci = make_case_info (Global.env()) ind RegularStyle in let cieq = make_case_info (Global.env()) (fst (destInd eq)) RegularStyle in let applied_PC = - mkApp (mkVar varP,Array.append (extended_rel_vect 1 realsign) + mkApp (mkVar varP,Array.append (Context.Rel.to_extended_vect 1 realsign) (if dep then [|cstr (2*nrealargs+1) 1|] else [||])) in let applied_PG = mkApp (mkVar varP,Array.append (rel_vect 1 nrealargs) @@ -381,11 +382,11 @@ let build_l2r_rew_scheme dep env ind kind = (if dep then [|mkRel 2|] else [||])) in let applied_sym_sym = mkApp (sym,Array.concat - [extended_rel_vect (2*nrealargs+4) paramsctxt1; + [Context.Rel.to_extended_vect (2*nrealargs+4) paramsctxt1; rel_vect 4 nrealargs; rel_vect (nrealargs+4) nrealargs; [|mkApp (sym,Array.concat - [extended_rel_vect (2*nrealargs+4) paramsctxt1; + [Context.Rel.to_extended_vect (2*nrealargs+4) paramsctxt1; rel_vect (nrealargs+4) nrealargs; rel_vect 4 nrealargs; [|mkRel 2|]])|]]) in @@ -408,7 +409,7 @@ let build_l2r_rew_scheme dep env ind kind = mkApp (eq,[|lift 4 applied_ind;applied_sym_sym;mkRel 1|]), applied_PR)), mkApp (sym_involutive, - Array.append (extended_rel_vect 3 mip.mind_arity_ctxt) [|mkVar varH|]), + Array.append (Context.Rel.to_extended_vect 3 mip.mind_arity_ctxt) [|mkVar varH|]), [|main_body|]) else main_body)))))) @@ -447,7 +448,7 @@ let build_l2r_forward_rew_scheme dep env ind kind = get_sym_eq_data env indu in let cstr n p = mkApp (mkConstructUi(indu,1), - Array.concat [extended_rel_vect n paramsctxt1; + Array.concat [Context.Rel.to_extended_vect n paramsctxt1; rel_vect p nrealargs]) in let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in let varHC = fresh env (Id.of_string "HC") in @@ -455,19 +456,19 @@ let build_l2r_forward_rew_scheme dep env ind kind = let applied_ind = build_dependent_inductive indu specif in let applied_ind_P = mkApp (mkIndU indu, Array.concat - [extended_rel_vect (4*nrealargs+2) paramsctxt1; + [Context.Rel.to_extended_vect (4*nrealargs+2) paramsctxt1; rel_vect 0 nrealargs; rel_vect (nrealargs+1) nrealargs]) in let applied_ind_P' = mkApp (mkIndU indu, Array.concat - [extended_rel_vect (3*nrealargs+1) paramsctxt1; + [Context.Rel.to_extended_vect (3*nrealargs+1) paramsctxt1; rel_vect 0 nrealargs; rel_vect (2*nrealargs+1) nrealargs]) in let realsign_P n = lift_rel_context (nrealargs*n+n) realsign in let realsign_ind = - name_context env ((Name varH,None,applied_ind)::realsign) in + name_context env ((LocalAssum (Name varH,applied_ind))::realsign) in let realsign_ind_P n aP = - name_context env ((Name varH,None,aP)::realsign_P n) in + name_context env ((LocalAssum (Name varH,aP))::realsign_P n) in let s, ctx' = Universes.fresh_sort_in_family (Global.env ()) kind in let ctx = Univ.ContextSet.union ctx ctx' in let s = mkSort s in @@ -538,14 +539,14 @@ let build_r2l_forward_rew_scheme dep env ind kind = let ((mib,mip as specif),constrargs,realsign,paramsctxt,nrealargs) = get_non_sym_eq_data env indu in let cstr n = - mkApp (mkConstructUi(indu,1),extended_rel_vect n mib.mind_params_ctxt) in + mkApp (mkConstructUi(indu,1),Context.Rel.to_extended_vect n mib.mind_params_ctxt) in let constrargs_cstr = constrargs@[cstr 0] in let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in let varHC = fresh env (Id.of_string "HC") in let varP = fresh env (Id.of_string "P") in let applied_ind = build_dependent_inductive indu specif in let realsign_ind = - name_context env ((Name varH,None,applied_ind)::realsign) in + name_context env ((LocalAssum (Name varH,applied_ind))::realsign) in let s, ctx' = Universes.fresh_sort_in_family (Global.env ()) kind in let ctx = Univ.ContextSet.union ctx ctx' in let s = mkSort s in @@ -554,8 +555,8 @@ let build_r2l_forward_rew_scheme dep env ind kind = applist (mkVar varP,if dep then constrargs_cstr else constrargs) in let applied_PG = mkApp (mkVar varP, - if dep then extended_rel_vect 0 realsign_ind - else extended_rel_vect 1 realsign) in + if dep then Context.Rel.to_extended_vect 0 realsign_ind + else Context.Rel.to_extended_vect 1 realsign) in let c = (my_it_mkLambda_or_LetIn paramsctxt (my_it_mkLambda_or_LetIn_name realsign_ind @@ -599,12 +600,12 @@ let fix_r2l_forward_rew_scheme (c, ctx') = | hp :: p :: ind :: indargs -> let c' = my_it_mkLambda_or_LetIn indargs - (mkLambda_or_LetIn (map_rel_declaration (liftn (-1) 1) p) - (mkLambda_or_LetIn (map_rel_declaration (liftn (-1) 2) hp) - (mkLambda_or_LetIn (map_rel_declaration (lift 2) ind) + (mkLambda_or_LetIn (map_constr (liftn (-1) 1) p) + (mkLambda_or_LetIn (map_constr (liftn (-1) 2) hp) + (mkLambda_or_LetIn (map_constr (lift 2) ind) (Reductionops.whd_beta Evd.empty (applist (c, - extended_rel_list 3 indargs @ [mkRel 1;mkRel 3;mkRel 2])))))) + Context.Rel.to_extended_list 3 indargs @ [mkRel 1;mkRel 3;mkRel 2])))))) in c', ctx' | _ -> anomaly (Pp.str "Ill-formed non-dependent left-to-right rewriting scheme") @@ -630,9 +631,10 @@ let fix_r2l_forward_rew_scheme (c, ctx') = (**********************************************************************) let build_r2l_rew_scheme dep env ind k = - let sigma, indu = Evd.fresh_inductive_instance env (Evd.from_env env) ind in - let sigma', c = build_case_analysis_scheme env sigma indu dep k in - c, Evd.evar_universe_context sigma' + let sigma = Sigma.Unsafe.of_evar_map (Evd.from_env env) in + let Sigma (indu, sigma, _) = Sigma.fresh_inductive_instance env sigma ind in + let Sigma (c, sigma, _) = build_case_analysis_scheme env sigma indu dep k in + c, Evd.evar_universe_context (Sigma.to_evar_map sigma) let build_l2r_rew_scheme = build_l2r_rew_scheme let build_l2r_forward_rew_scheme = build_l2r_forward_rew_scheme @@ -736,13 +738,13 @@ let build_congr env (eq,refl,ctx) ind = let arityctxt = Vars.subst_instance_context u mip.mind_arity_ctxt in let paramsctxt = Vars.subst_instance_context u mib.mind_params_ctxt in let realsign,_ = List.chop mip.mind_nrealdecls arityctxt in - if List.exists (fun (_,b,_) -> not (Option.is_empty b)) realsign then + if List.exists is_local_def realsign then error "Inductive equalities with local definitions in arity not supported."; let env_with_arity = push_rel_context arityctxt env in - let (_,_,ty) = lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity in + let ty = get_type (lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity) in let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in let _,constrargs = decompose_app ccl in - if Int.equal (rel_context_length constrsign) (rel_context_length mib.mind_params_ctxt) then + if Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt) then error "Constructor must have no arguments"; let b = List.nth constrargs (i + mib.mind_nparams - 1) in let varB = fresh env (Id.of_string "B") in @@ -758,8 +760,8 @@ let build_congr env (eq,refl,ctx) ind = (mkNamedLambda varH (applist (mkIndU indu, - extended_rel_list (mip.mind_nrealargs+2) paramsctxt @ - extended_rel_list 0 realsign)) + Context.Rel.to_extended_list (mip.mind_nrealargs+2) paramsctxt @ + Context.Rel.to_extended_list 0 realsign)) (mkCase (ci, my_it_mkLambda_or_LetIn_name (lift_rel_context (mip.mind_nrealargs+3) realsign) @@ -767,9 +769,9 @@ let build_congr env (eq,refl,ctx) ind = (Anonymous, applist (mkIndU indu, - extended_rel_list (2*mip.mind_nrealdecls+3) + Context.Rel.to_extended_list (2*mip.mind_nrealdecls+3) paramsctxt - @ extended_rel_list 0 realsign), + @ Context.Rel.to_extended_list 0 realsign), mkApp (eq, [|mkVar varB; mkApp (mkVar varf, [|lift (2*mip.mind_nrealdecls+4) b|]); |