diff options
29 files changed, 249 insertions, 263 deletions
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml index 7385bf652f..aaa1b466da 100644 --- a/contrib/funind/indfun.ml +++ b/contrib/funind/indfun.ml @@ -224,11 +224,9 @@ let rec is_rec names = ) b | RApp(_,f,args) -> List.exists (lookup names) (f::args) - | RCases(_,_,el,brl) -> + | RCases(_,_,_,el,brl) -> List.exists (fun (e,_) -> lookup names e) el || List.exists (lookup_br names) brl - | RLetPattern (_,(c,_),p) -> - lookup names c || lookup_br names p and lookup_br names (_,idl,_,rt) = let new_names = List.fold_right Idset.remove idl names in lookup new_names rt @@ -590,8 +588,8 @@ let rec add_args id new_args b = | CApp(loc,(pf,b),bl) -> CApp(loc,(pf,add_args id new_args b), List.map (fun (e,o) -> add_args id new_args e,o) bl) - | CCases(loc,b_option,cel,cal) -> - CCases(loc,Option.map (add_args id new_args) b_option, + | CCases(loc,sty,b_option,cel,cal) -> + CCases(loc,sty,Option.map (add_args id new_args) b_option, List.map (fun (b,(na,b_option)) -> add_args id new_args b, (na,Option.map (add_args id new_args) b_option)) cel, @@ -603,9 +601,6 @@ let rec add_args id new_args b = add_args id new_args b2 ) - | CLetPattern(loc,p,b,c) -> - CLetPattern(loc,p,add_args id new_args b,add_args id new_args c) - | CIf(loc,b1,(na,b_option),b2,b3) -> CIf(loc,add_args id new_args b1, (na,Option.map (add_args id new_args) b_option), diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml index 9276898e18..08a97fd221 100644 --- a/contrib/funind/rawterm_to_relation.ml +++ b/contrib/funind/rawterm_to_relation.ml @@ -567,7 +567,7 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return = funnames avoid (mkRLetIn(new_n,t,mkRApp(new_b,args))) - | RCases _ | RLambda _ | RIf _ | RLetTuple _ | RLetPattern _ -> + | RCases _ | RLambda _ | RIf _ | RLetTuple _ -> (* we have [(match e1, ...., en with ..... end) t1 tn] we first compute the result from the case and then combine each of them with each of args one @@ -627,14 +627,12 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return = in let b_res = build_entry_lc new_env funnames avoid b in combine_results (combine_letin n) v_res b_res - | RCases(_,_,el,brl) -> + | RCases(_,_,_,el,brl) -> (* we create the discrimination function and treat the case itself *) let make_discr = make_discr_match brl in build_entry_lc_from_case env funnames make_discr el brl avoid - | RLetPattern (loc,c,p) -> - build_entry_lc env funnames avoid (RCases (loc, None, [c], [p])) | RIf(_,b,(na,e_option),lhs,rhs) -> let b_as_constr = Pretyping.Default.understand Evd.empty env b in let b_typ = Typing.type_of env Evd.empty b_as_constr in @@ -1021,7 +1019,7 @@ let rec compute_cst_params relnames params = function | RLambda(_,_,_,t,b) | RProd(_,_,_,t,b) | RLetIn(_,_,t,b) | RLetTuple(_,_,_,t,b) -> let t_params = compute_cst_params relnames params t in compute_cst_params relnames t_params b - | RCases _ | RLetPattern _ -> + | RCases _ -> params (* If there is still cases at this point they can only be discriminitation ones *) | RSort _ -> params diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml index c9341ba998..92396af590 100644 --- a/contrib/funind/rawtermops.ml +++ b/contrib/funind/rawtermops.ml @@ -15,7 +15,7 @@ let mkRApp(rt,rtl) = RApp(dummy_loc,rt,rtl) let mkRLambda(n,t,b) = RLambda(dummy_loc,n,Explicit,t,b) let mkRProd(n,t,b) = RProd(dummy_loc,n,Explicit,t,b) let mkRLetIn(n,t,b) = RLetIn(dummy_loc,n,t,b) -let mkRCases(rto,l,brl) = RCases(dummy_loc,rto,l,brl) +let mkRCases(rto,l,brl) = RCases(dummy_loc,Term.RegularStyle,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,CastConv (Term.DEFAULTcast,t)) @@ -163,14 +163,12 @@ let change_vars = change_vars mapping b, change_vars new_mapping e ) - | RCases(loc,infos,el,brl) -> - RCases(loc, + | RCases(loc,sty,infos,el,brl) -> + RCases(loc,sty, infos, List.map (fun (e,x) -> (change_vars mapping e,x)) el, List.map (change_vars_br mapping) brl ) - | RLetPattern(loc, (e,x), br) -> - RLetPattern(loc, (change_vars mapping e, x), change_vars_br mapping br) | RIf(loc,b,(na,e_option),lhs,rhs) -> RIf(loc, change_vars mapping b, @@ -348,13 +346,11 @@ let rec alpha_rt excluded rt = let new_b = alpha_rt new_excluded new_b in let new_rto = Option.map (alpha_rt new_excluded) new_rto in RLetTuple(loc,new_nal,(na,new_rto),new_t,new_b) - | RCases(loc,infos,el,brl) -> + | RCases(loc,sty,infos,el,brl) -> let new_el = List.map (function (rt,i) -> alpha_rt excluded rt, i) el in - RCases(loc,infos,new_el,List.map (alpha_br excluded) brl) - | RLetPattern(loc,(rt,i),br) -> - RLetPattern(loc, (alpha_rt excluded rt, i), alpha_br excluded br) + RCases(loc,sty,infos,new_el,List.map (alpha_br excluded) brl) | RIf(loc,b,(na,e_o),lhs,rhs) -> RIf(loc,alpha_rt excluded b, (na,Option.map (alpha_rt excluded) e_o), @@ -402,10 +398,9 @@ let is_free_in id = | _ -> true in is_free_in t || (check_in_b && is_free_in b) - | RCases(_,_,el,brl) -> + | RCases(_,_,_,el,brl) -> (List.exists (fun (e,_) -> is_free_in e) el) || List.exists is_free_in_br brl - | RLetPattern(_,(e,_),br) -> is_free_in e || is_free_in_br br | RLetTuple(_,nal,_,b,t) -> let check_in_nal = not (List.exists (function Name id' -> id'= id | _ -> false) nal) @@ -499,14 +494,12 @@ let replace_var_by_term x_id term = replace_var_by_pattern def, replace_var_by_pattern b ) - | RCases(loc,infos,el,brl) -> - RCases(loc, + | RCases(loc,sty,infos,el,brl) -> + RCases(loc,sty, infos, List.map (fun (e,x) -> (replace_var_by_pattern e,x)) el, List.map replace_var_by_pattern_br brl ) - | RLetPattern(loc,(e,x),br) -> - RLetPattern(loc,(replace_var_by_pattern e, x), replace_var_by_pattern_br br) | RIf(loc,b,(na,e_option),lhs,rhs) -> RIf(loc, replace_var_by_pattern b, (na,Option.map replace_var_by_pattern e_option), @@ -608,10 +601,8 @@ let ids_of_rawterm c = | 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 - | RCases (loc,rtntypopt,tml,brchl) -> + | RCases (loc,sty,rtntypopt,tml,brchl) -> List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_rawterm [] c) brchl) - | RLetPattern (loc,tm,(_,idl,patl,c)) -> - idl @ ids_of_rawterm [] c | RRec _ -> failwith "Fix inside a constructor branch" | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> [] in @@ -658,17 +649,12 @@ let zeta_normalize = zeta_normalize_term def, zeta_normalize_term b ) - | RCases(loc,infos,el,brl) -> - RCases(loc, + | RCases(loc,sty,infos,el,brl) -> + RCases(loc,sty, infos, List.map (fun (e,x) -> (zeta_normalize_term e,x)) el, List.map zeta_normalize_br brl ) - | RLetPattern(loc,(e,x),br) -> - RLetPattern(loc, - (zeta_normalize_term e,x), - zeta_normalize_br br - ) | RIf(loc,b,(na,e_option),lhs,rhs) -> RIf(loc, zeta_normalize_term b, (na,Option.map zeta_normalize_term e_option), @@ -723,14 +709,10 @@ let expand_as = | RDynamic _ -> error "Not handled RDynamic" | 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, + | RCases(loc,sty,po,el,brl) -> + RCases(loc, sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el, List.map (expand_as_br map) brl) - | RLetPattern(loc,(rt,t),br) -> - RLetPattern(loc, (expand_as map rt,t), - expand_as_br map br) - and expand_as_br map (loc,idl,cpl,rt) = - (loc,idl,cpl, expand_as (List.fold_left add_as map cpl) rt) + (loc,idl,cpl, expand_as (List.fold_left add_as map cpl) rt) in expand_as Idmap.empty diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml index 16357fc472..39eaa0b98b 100644 --- a/contrib/interface/depends.ml +++ b/contrib/interface/depends.ml @@ -210,7 +210,7 @@ let rec depends_of_rawconstr rc acc = match rc with | RLambda (_, _, _, rct, rcb) | RProd (_, _, _, rct, rcb) | RLetIn (_, _, rct, rcb) -> depends_of_rawconstr rcb (depends_of_rawconstr rct acc) - | RCases (_, rco, tmt, cc) -> + | RCases (_, _, rco, tmt, cc) -> (* LEM TODO: handle the cc *) (Option.fold_right depends_of_rawconstr rco (list_union_map @@ -221,13 +221,6 @@ let rec depends_of_rawconstr rc acc = match rc with acc)) | RLetTuple (_,_,(_,rco),rc0,rc1) -> depends_of_rawconstr rc1 (depends_of_rawconstr rc0 (Option.fold_right depends_of_rawconstr rco acc)) - | RLetPattern (_, tmt, cc) -> - (* LEM TODO: handle the cc *) - (fun (rc, pp) acc -> - Option.fold_right (fun (_,ind,_,_) acc -> (IndRef ind)::acc) (snd pp) - (depends_of_rawconstr rc acc)) - tmt - acc | RIf (_, rcC, (_, rco), rcT, rcF) -> let dorc = depends_of_rawconstr in dorc rcF (dorc rcT (dorc rcF (dorc rcC (Option.fold_right dorc rco acc)))) | RRec (_, _, _, rdla, rca0, rca1) -> let dorca = array_union_map depends_of_rawconstr in diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 2219e327ca..aa7a50dce2 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -360,8 +360,6 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function | CLambdaN(_,ll,b)-> CT_lambdac(xlate_binder_ne_list ll, xlate_formula b) | CLetIn(_, v, a, b) -> CT_letin(CT_def(xlate_id_opt v, xlate_formula a), xlate_formula b) - | CLetPattern(_, v, a, b) -> - error "TODO: xlate_formula let | pattern" | CAppExpl(_, (Some n, r), l) -> let l', last = decompose_last l in CT_proj(xlate_formula last, @@ -379,8 +377,8 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function (xlate_formula f, List.map xlate_formula_expl l')) | CApp(_, (_,f), l) -> CT_appc(xlate_formula f, xlate_formula_expl_ne_list l) - | CCases (_, _, [], _) -> assert false - | CCases (_, ret_type, tm::tml, eqns)-> + | CCases (_, _, _, [], _) -> assert false + | CCases (_, _, ret_type, tm::tml, eqns)-> CT_cases(CT_matched_formula_ne_list(xlate_matched_formula tm, List.map xlate_matched_formula tml), xlate_formula_opt ret_type, diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4 index dd776088cc..8d9bfdbc51 100644 --- a/contrib/recdef/recdef.ml4 +++ b/contrib/recdef/recdef.ml4 @@ -1070,7 +1070,7 @@ let (value_f:constr list -> global_reference -> constr) = in let fun_body = RCases - (d0,None, + (d0,RegularStyle,None, [RApp(d0, RRef(d0,fterm), List.rev_map (fun x_id -> RVar(d0, x_id)) rev_x_id_l), (Anonymous,None)], [d0, [v_id], [PatCstr(d0,(ind_of_ref diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml index 54ed30a5dc..5b8bb9c0f8 100644 --- a/contrib/subtac/subtac_cases.ml +++ b/contrib/subtac/subtac_cases.ml @@ -241,6 +241,7 @@ type pattern_matching_problem = history : pattern_continuation; mat : matrix; caseloc : loc; + casestyle: case_style; typing_function: type_constraint -> env -> rawconstr -> unsafe_judgment } (*--------------------------------------------------------------------------* @@ -1263,7 +1264,7 @@ and match_current pb tomatch = let (pred,typ,s) = find_predicate pb.caseloc pb.env pb.isevars pb.pred brtyps cstrs current indt pb.tomatch in - let ci = make_case_info pb.env mind RegularStyle in + let ci = make_case_info pb.env mind pb.casestyle in let case = mkCase (ci,nf_betaiota pred,current,brvals) in let inst = List.map mkRel deps in { uj_val = applist (case, inst); @@ -2081,7 +2082,7 @@ let nf_evars_env evar_defs (env : env) : env = Environ.fold_rel_context (fun e (na, b, t) e' -> Environ.push_rel (na, Option.map nf b, nf t) e') ~init:env' env -let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns) = +let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns) = (* We build the matrix of patterns and right-hand-side *) let matx = matx_of_eqns env eqns in @@ -2151,6 +2152,7 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e history = start_history (List.length initial_pushed); mat = matx; caseloc = loc; + casestyle= style; typing_function = typing_fun } in let j = compile pb in @@ -2180,6 +2182,7 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e history = start_history (List.length initial_pushed); mat = matx; caseloc = loc; + casestyle= style; typing_function = typing_fun } in let j = compile pb in diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml index 730b12605e..d3edb6e3cd 100644 --- a/contrib/subtac/subtac_pretyping_F.ml +++ b/contrib/subtac/subtac_pretyping_F.ml @@ -488,22 +488,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct in { uj_val = v; uj_type = p } - | RLetPattern (loc, c, p) -> - (* Just use cases typing *) - let j = - pretype tycon env isevars lvar - (RCases (loc, None, [c], [p])) - in - (* Change case info *) - let j' = match kind_of_term j.uj_val with - Case (ci, po, c, br) -> - let pp_info = { ci.ci_pp_info with style = LetPatternStyle } in - { j with uj_val = mkCase ({ ci with ci_pp_info = pp_info }, po, c, br) } - | _ -> j - in j' - - | RCases (loc,po,tml,eqns) -> - Cases.compile_cases loc + | RCases (loc,sty,po,tml,eqns) -> + Cases.compile_cases loc sty ((fun vtyc env -> pretype vtyc env isevars lvar),isevars) tycon env (* loc *) (po,tml,eqns) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index eb69e12257..11cd87763f 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -195,7 +195,7 @@ let rec check_same_type ty1 ty2 = List.iter2 (fun (a1,e1) (a2,e2) -> if e1<>e2 then failwith "not same expl"; check_same_type a1 a2) al1 al2 - | CCases(_,_,a1,brl1), CCases(_,_,a2,brl2) -> + | CCases(_,_,_,a1,brl1), CCases(_,_,_,a2,brl2) -> List.iter2 (fun (tm1,_) (tm2,_) -> check_same_type tm1 tm2) a1 a2; List.iter2 (fun (_,pl1,r1) (_,pl2,r2) -> List.iter2 (located_iter2 (List.iter2 check_same_pattern)) pl1 pl2; @@ -264,7 +264,7 @@ let rec same_raw c d = | RLetIn(_,na1,t1,m1), RLetIn(_,na2,t2,m2) -> if na1 <> na2 then failwith "RLetIn"; same_raw t1 t2; same_raw m1 m2 - | RCases(_,_,c1,b1), RCases(_,_,c2,b2) -> + | RCases(_,_,_,c1,b1), RCases(_,_,_,c2,b2) -> List.iter2 (fun (t1,(al1,oind1)) (t2,(al2,oind2)) -> same_raw t1 t2; @@ -690,7 +690,7 @@ let rec extern inctx scopes vars r = let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) t c in CLambdaN (loc,[(dummy_loc,na)::idl,Default bk,t],c) - | RCases (loc,rtntypopt,tml,eqns) -> + | RCases (loc,sty,rtntypopt,tml,eqns) -> let vars' = List.fold_right (name_fold Idset.add) (cases_predicate_names tml) vars in @@ -713,7 +713,7 @@ let rec extern inctx scopes vars r = let t = RApp (dummy_loc,RRef (dummy_loc,IndRef ind),params@args) in (extern_typ scopes vars t)) x))) tml in let eqns = List.map (extern_eqn (rtntypopt<>None) scopes vars) eqns in - CCases (loc,rtntypopt',tml,eqns) + CCases (loc,sty,rtntypopt',tml,eqns) | RLetTuple (loc,nal,(na,typopt),tm,b) -> CLetTuple (loc,nal, @@ -722,15 +722,6 @@ let rec extern inctx scopes vars r = sub_extern false scopes vars tm, extern false scopes (List.fold_left add_vname vars nal) b) - | RLetPattern (loc,(tm,_), eqn) -> - let p, c = - match extern_eqn false scopes vars eqn with - (loc,[loc',[p]], c) -> p,c - | _ -> assert false - in - let t = extern inctx scopes vars tm in - CLetPattern(loc, p, t, c) - | RIf (loc,c,(na,typopt),b1,b2) -> CIf (loc,sub_extern false scopes vars c, (Option.map (fun _ -> na) typopt, @@ -948,7 +939,7 @@ let rec raw_of_pat env = function let nal,b = it_destRLambda_or_LetIn_names n (raw_of_pat env b) in RLetTuple (loc,nal,(Anonymous,None),raw_of_pat env tm,b) | PCase (_,PMeta None,tm,[||]) -> - RCases (loc,None,[raw_of_pat env tm,(Anonymous,None)],[]) + RCases (loc,RegularStyle,None,[raw_of_pat env tm,(Anonymous,None)],[]) | PCase ((_,cstr_nargs,indo,ind_nargs),p,tm,bv) -> let brs = Array.to_list (Array.map (raw_of_pat env) bv) in let brns = Array.to_list cstr_nargs in @@ -960,7 +951,7 @@ let rec raw_of_pat env = function else let nparams,n = Option.get ind_nargs in return_type_of_predicate ind nparams n (raw_of_pat env p) in - RCases (loc,rtn,[raw_of_pat env tm,indnames],mat) + RCases (loc,RegularStyle,rtn,[raw_of_pat env tm,indnames],mat) | PFix f -> Detyping.detype false [] env (mkFix f) | PCoFix c -> Detyping.detype false [] env (mkCoFix c) | PSort s -> RSort (loc,s) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index ce445c3f6d..9e962267db 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -901,7 +901,7 @@ let internalise sigma globalenv env allow_patvar lvar c = (* Now compact "(f args') args" *) | RApp (loc', f', args') -> RApp (join_loc loc' loc, f',args'@args) | _ -> RApp (loc, c, args)) - | CCases (loc, rtnpo, tms, eqns) -> + | CCases (loc, sty, rtnpo, tms, eqns) -> let tms,env' = List.fold_right (fun citm (inds,env) -> let (tm,ind),nal = intern_case_item env citm in @@ -909,7 +909,7 @@ let internalise sigma globalenv env allow_patvar lvar c = tms ([],env) in let rtnpo = Option.map (intern_type env') rtnpo in let eqns' = List.map (intern_eqn (List.length tms) env) eqns in - RCases (loc, rtnpo, tms, List.flatten eqns') + RCases (loc, sty, rtnpo, tms, List.flatten eqns') | CLetTuple (loc, nal, (na,po), b, c) -> let env' = reset_tmp_scope env in let ((b',(na',_)),ids) = intern_case_item env' (b,(na,None)) in @@ -917,11 +917,6 @@ let internalise sigma globalenv env allow_patvar lvar c = let p' = Option.map (intern_type env'') po in RLetTuple (loc, nal, (na', p'), b', intern (List.fold_left (push_name_env lvar) env nal) c) - | CLetPattern (loc, p, c, b) -> - let loc' = cases_pattern_expr_loc p in - let (tm,ind), nal = intern_case_item env (c,(None,None)) in - let eqn' = intern_eqn 1 env (loc, [loc',[p]], b) in - RLetPattern (loc, (tm,ind), List.hd eqn') | CIf (loc, c, (na,po), b1, b2) -> let env' = reset_tmp_scope env in let ((c',(na',_)),ids) = intern_case_item env' (c,(na,None)) in diff --git a/interp/reserve.ml b/interp/reserve.ml index 082db5a390..f49c42a55d 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -57,15 +57,13 @@ let rec unloc = function | RLambda (_,na,bk,ty,c) -> RLambda (dummy_loc,na,bk,unloc ty,unloc c) | RProd (_,na,bk,ty,c) -> RProd (dummy_loc,na,bk,unloc ty,unloc c) | RLetIn (_,na,b,c) -> RLetIn (dummy_loc,na,unloc b,unloc c) - | RCases (_,rtntypopt,tml,pl) -> - RCases (dummy_loc, + | RCases (_,sty,rtntypopt,tml,pl) -> + RCases (dummy_loc,sty, (Option.map unloc rtntypopt), List.map (fun (tm,x) -> (unloc tm,x)) tml, List.map (fun (_,idl,p,c) -> (dummy_loc,idl,p,unloc c)) pl) | RLetTuple (_,nal,(na,po),b,c) -> RLetTuple (dummy_loc,nal,(na,Option.map unloc po),unloc b,unloc c) - | RLetPattern (_,(tm,x),(_,idl,p,c)) -> - RLetPattern (dummy_loc,(unloc tm,x),(dummy_loc,idl,p,unloc c)) | RIf (_,c,(na,po),b1,b2) -> RIf (dummy_loc,unloc c,(na,Option.map unloc po),unloc b1,unloc b2) | RRec (_,fk,idl,bl,tyl,bv) -> diff --git a/interp/topconstr.ml b/interp/topconstr.ml index c9a33c7eba..05a1465ac8 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -37,7 +37,7 @@ type aconstr = | ALambda of name * aconstr * aconstr | AProd of name * aconstr * aconstr | ALetIn of name * aconstr * aconstr - | ACases of aconstr option * + | ACases of case_style * aconstr option * (aconstr * (name * (inductive * int * name list) option)) list * (cases_pattern list * aconstr) list | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr @@ -79,7 +79,7 @@ let rawconstr_of_aconstr_with_binders loc g f e = function let e,na = name_fold_map g e na in RProd (loc,na,Explicit,f e ty,f e c) | ALetIn (na,b,c) -> let e,na = name_fold_map g e na in RLetIn (loc,na,f e b,f e c) - | ACases (rtntypopt,tml,eqnl) -> + | ACases (sty,rtntypopt,tml,eqnl) -> let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') -> let e',t' = match t with | None -> e',None @@ -94,7 +94,7 @@ let rawconstr_of_aconstr_with_binders loc g f e = function let ((idl,e),patl) = list_fold_map (cases_pattern_fold_map loc fold) ([],e) patl in (loc,idl,patl,f e rhs)) eqnl in - RCases (loc,Option.map (f e') rtntypopt,tml',eqnl') + RCases (loc,sty,Option.map (f e') rtntypopt,tml',eqnl') | ALetTuple (nal,(na,po),b,c) -> let e,nal = list_fold_map (name_fold_map g) e nal in let e,na = name_fold_map g e na in @@ -138,9 +138,9 @@ let compare_rawconstr f t1 t2 = match t1,t2 with | RHole _, RHole _ -> true | RSort (_,s1), RSort (_,s2) -> s1 = s2 | (RLetIn _ | RCases _ | RRec _ | RDynamic _ - | RPatVar _ | REvar _ | RLetTuple _ | RLetPattern _ | RIf _ | RCast _),_ + | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _),_ | _,(RLetIn _ | RCases _ | RRec _ | RDynamic _ - | RPatVar _ | REvar _ | RLetTuple _ | RLetPattern _ | RIf _ | RCast _) + | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _) -> error "Unsupported construction in recursive notations" | (RRef _ | RVar _ | RApp _ | RLambda _ | RProd _ | RHole _ | RSort _), _ -> false @@ -183,9 +183,9 @@ let aconstr_and_vars_of_rawconstr a = | RLambda (_,na,bk,ty,c) -> add_name found na; ALambda (na,aux ty,aux c) | RProd (_,na,bk,ty,c) -> add_name found na; AProd (na,aux ty,aux c) | RLetIn (_,na,b,c) -> add_name found na; ALetIn (na,aux b,aux c) - | RCases (_,rtntypopt,tml,eqnl) -> + | RCases (_,sty,rtntypopt,tml,eqnl) -> let f (_,idl,pat,rhs) = found := idl@(!found); (pat,aux rhs) in - ACases (Option.map aux rtntypopt, + ACases (sty,Option.map aux rtntypopt, List.map (fun (tm,(na,x)) -> add_name found na; Option.iter @@ -196,7 +196,6 @@ let aconstr_and_vars_of_rawconstr a = add_name found na; List.iter (add_name found) nal; ALetTuple (nal,(na,Option.map aux po),aux b,aux c) - | RLetPattern (loc, c, p) -> error "TODO: aconstr of letpattern" | RIf (loc,c,(na,po),b1,b2) -> add_name found na; AIf (aux c,(na,Option.map aux po),aux b1,aux b2) @@ -208,8 +207,7 @@ let aconstr_and_vars_of_rawconstr a = | RRef (_,r) -> ARef r | RPatVar (_,(_,n)) -> APatVar n | RDynamic _ | RRec _ | REvar _ -> - error "Fixpoints, cofixpoints, existential variables and pattern-matching not \ -allowed in abbreviatable expressions" + error "Fixpoints, cofixpoints and existential variables not allowed in abbreviatable expressions" (* Recognizing recursive notations *) and terminator_of_pat f1 ll1 lr1 = function @@ -305,7 +303,7 @@ let rec subst_aconstr subst bound raw = if r1' == r1 && r2' == r2 then raw else ALetIn (n,r1',r2') - | ACases (rtntypopt,rl,branches) -> + | ACases (sty,rtntypopt,rl,branches) -> let rtntypopt' = Option.smartmap (subst_aconstr subst bound) rtntypopt and rl' = list_smartmap (fun (a,(n,signopt) as x) -> @@ -325,7 +323,7 @@ let rec subst_aconstr subst bound raw = in if rtntypopt' == rtntypopt && rtntypopt == rtntypopt' & rl' == rl && branches' == branches then raw else - ACases (rtntypopt',rl',branches') + ACases (sty,rtntypopt',rl',branches') | ALetTuple (nal,(na,po),b,c) -> let po' = Option.smartmap (subst_aconstr subst bound) po @@ -447,8 +445,9 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2 | RLetIn (_,na1,t1,b1), ALetIn (na2,t2,b2) -> match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2 - | RCases (_,rtno1,tml1,eqnl1), ACases (rtno2,tml2,eqnl2) - when List.length tml1 = List.length tml2 + | RCases (_,sty1,rtno1,tml1,eqnl1), ACases (sty2,rtno2,tml2,eqnl2) + when sty1 = sty2 + & List.length tml1 = List.length tml2 & List.length eqnl1 = List.length eqnl2 -> let rtno1' = abstract_return_type_context_rawconstr tml1 rtno1 in let rtno2' = abstract_return_type_context_aconstr tml2 rtno2 in @@ -559,12 +558,11 @@ type constr_expr = | CAppExpl of loc * (proj_flag * reference) * constr_expr list | CApp of loc * (proj_flag * constr_expr) * (constr_expr * explicitation located option) list - | CCases of loc * constr_expr option * + | CCases of loc * case_style * constr_expr option * (constr_expr * (name option * constr_expr option)) list * (loc * cases_pattern_expr list located list * constr_expr) list | CLetTuple of loc * name list * (name option * constr_expr option) * constr_expr * constr_expr - | CLetPattern of loc * cases_pattern_expr * constr_expr * constr_expr | CIf of loc * constr_expr * (name option * constr_expr option) * constr_expr * constr_expr | CHole of loc * Evd.hole_kind option @@ -577,7 +575,6 @@ type constr_expr = | CDelimiters of loc * string * constr_expr | CDynamic of loc * Dyn.t - and fixpoint_expr = identifier * (int option * recursion_order_expr) * local_binder list * constr_expr * constr_expr @@ -632,9 +629,8 @@ let constr_loc = function | CLetIn (loc,_,_,_) -> loc | CAppExpl (loc,_,_) -> loc | CApp (loc,_,_) -> loc - | CCases (loc,_,_,_) -> loc + | CCases (loc,_,_,_,_) -> loc | CLetTuple (loc,_,_,_,_) -> loc - | CLetPattern (loc,_,_,_) -> loc | CIf (loc,_,_,_,_) -> loc | CHole (loc, _) -> loc | CPatVar (loc,_) -> loc @@ -726,7 +722,7 @@ let fold_constr_expr_with_binders g f n acc = function | CDelimiters (loc,_,a) -> f n acc a | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CDynamic _ | CRef _ -> acc - | CCases (loc,rtnpo,al,bl) -> + | CCases (loc,sty,rtnpo,al,bl) -> let ids = ids_of_cases_tomatch al in let acc = Option.fold_left (f (List.fold_right g ids n)) acc rtnpo in let acc = List.fold_left (f n) acc (List.map fst al) in @@ -736,10 +732,6 @@ let fold_constr_expr_with_binders g f n acc = function | CLetTuple (loc,nal,(ona,po),b,c) -> let n' = List.fold_right (name_fold g) nal n in f (Option.fold_right (name_fold g) ona n') (f n acc b) c - | CLetPattern (loc,p,b,c) -> - let acc = f n acc b in - let ids = cases_pattern_fold_names Idset.add Idset.empty p in - f (Idset.fold g ids n) acc c | CIf (_,c,(ona,po),b1,b2) -> let acc = f n (f n (f n acc b1) b2) c in Option.fold_left (f (Option.fold_right (name_fold g) ona n)) acc po @@ -841,19 +833,16 @@ let map_constr_expr_with_binders g f e = function | CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a) | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CDynamic _ | CRef _ as x -> x - | CCases (loc,rtnpo,a,bl) -> + | CCases (loc,sty,rtnpo,a,bl) -> (* TODO: apply g on the binding variables in pat... *) let bl = List.map (fun (loc,pat,rhs) -> (loc,pat,f e rhs)) bl in let ids = ids_of_cases_tomatch a in let po = Option.map (f (List.fold_right g ids e)) rtnpo in - CCases (loc, po, List.map (fun (tm,x) -> (f e tm,x)) a,bl) + CCases (loc, sty, po, List.map (fun (tm,x) -> (f e tm,x)) a,bl) | CLetTuple (loc,nal,(ona,po),b,c) -> let e' = List.fold_right (name_fold g) nal e in let e'' = Option.fold_right (name_fold g) ona e in CLetTuple (loc,nal,(ona,Option.map (f e'') po),f e b,f e' c) - | CLetPattern (loc, p, b, c) -> - (* TODO: apply g on the binding variables in pat... *) - CLetPattern (loc, p, f e b,f e c) | CIf (loc,c,(ona,po),b1,b2) -> let e' = Option.fold_right (name_fold g) ona e in CIf (loc,f e c,(ona,Option.map (f e') po),f e b1,f e b2) diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 26805aa13e..4e46d95902 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -33,7 +33,7 @@ type aconstr = | ALambda of name * aconstr * aconstr | AProd of name * aconstr * aconstr | ALetIn of name * aconstr * aconstr - | ACases of aconstr option * + | ACases of case_style * aconstr option * (aconstr * (name * (inductive * int * name list) option)) list * (cases_pattern list * aconstr) list | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr @@ -117,13 +117,12 @@ type constr_expr = | CLetIn of loc * name located * constr_expr * constr_expr | CAppExpl of loc * (proj_flag * reference) * constr_expr list | CApp of loc * (proj_flag * constr_expr) * - (constr_expr * explicitation located option) list - | CCases of loc * constr_expr option * + (constr_expr * explicitation located option) list + | CCases of loc * case_style * constr_expr option * (constr_expr * (name option * constr_expr option)) list * (loc * cases_pattern_expr list located list * constr_expr) list | CLetTuple of loc * name list * (name option * constr_expr option) * constr_expr * constr_expr - | CLetPattern of loc * cases_pattern_expr * constr_expr * constr_expr | CIf of loc * constr_expr * (name option * constr_expr option) * constr_expr * constr_expr | CHole of loc * Evd.hole_kind option diff --git a/kernel/term.mli b/kernel/term.mli index 8d6c20a353..70c5ceded9 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -439,8 +439,8 @@ val noccurn : int -> constr -> bool val noccur_between : int -> int -> constr -> bool (* Checking function for terms containing existential- or - meta-variables. The function [noccur_with_meta] considers only - meta-variable applied to some terms (intented to be its local + meta-variables. The function [noccur_with_meta] does not consider + meta-variables applied to some terms (intented to be its local context) (for existential variables, it is necessarily the case) *) val noccur_with_meta : int -> int -> constr -> bool diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 423ade8b6d..0e7c92a6ce 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -125,6 +125,8 @@ let ident_eq = | _ -> raise Stream.Failure) | _ -> raise Stream.Failure) +let aliasvar = function CPatAlias (_, _, id) -> Some (Name id) | _ -> None + GEXTEND Gram GLOBAL: binder_constr lconstr constr operconstr sort global constr_pattern lconstr_pattern Constr.ident @@ -228,15 +230,16 @@ GEXTEND Gram ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> CLetTuple (loc,List.map snd lb,po,c1,c2) - | "let"; "|"; p=pattern; ":="; c1 = operconstr LEVEL "200"; + | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> - CLetPattern (loc, p, c1, c2) - | "dest"; c1 = operconstr LEVEL "200"; - "as"; p=pattern; + CCases (loc, LetPatternStyle, None, [(c1,(None,None))], [(loc, [(loc,[p])], c2)]) + | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; + rt = case_type; "in"; c2 = operconstr LEVEL "200" -> + CCases (loc, LetPatternStyle, Some rt, [(c1, (aliasvar p, None))], [(loc, [(loc, [p])], c2)]) + | "let"; "'"; p=pattern; "in"; t = operconstr LEVEL "200"; + ":="; c1 = operconstr LEVEL "200"; rt = case_type; "in"; c2 = operconstr LEVEL "200" -> - let loc' = cases_pattern_expr_loc p in - CCases (loc, None, [(c1, (None, None))], - [loc, [loc',[p]], c2]) + CCases (loc, LetPatternStyle, Some rt, [(c1, (aliasvar p, Some t))], [(loc, [(loc, [p])], c2)]) | "if"; c=operconstr LEVEL "200"; po = return_type; "then"; b1=operconstr LEVEL "200"; "else"; b2=operconstr LEVEL "200" -> @@ -283,7 +286,7 @@ GEXTEND Gram (* ; *) match_constr: [ [ "match"; ci=LIST1 case_item SEP ","; ty=OPT case_type; "with"; - br=branches; "end" -> CCases(loc,ty,ci,br) ] ] + br=branches; "end" -> CCases(loc,RegularStyle,ty,ci,br) ] ] ; case_item: [ [ c=operconstr LEVEL "100"; p=pred_pattern -> (c,p) ] ] diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index 47725cbd65..a9f3fd487c 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -171,7 +171,7 @@ let rec interp_xml_constr = function let mat = simple_cases_matrix_of_branches ind brns brs in let nparams,n = compute_inductive_nargs ind in let nal,rtn = return_type_of_predicate ind nparams n p in - RCases (loc,rtn,[tm,nal],mat) + RCases (loc,RegularStyle,rtn,[tm,nal],mat) | XmlTag (loc,"MUTIND",al,[]) -> RRef (loc, IndRef (get_xml_inductive al)) | XmlTag (loc,"MUTCONSTRUCT",al,[]) -> diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 7d0d085938..21c5a343b4 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -434,27 +434,16 @@ let tm_clash = function -> Some id | _ -> None -let pr_case_item pr (tm,(na,indnalopt)) = - hov 0 (pr (lcast,E) tm ++ -(* - (match na with - | Name id when not (is_var id tm) -> spc () ++ str "as " ++ pr_id id - | Anonymous when tm_clash (tm,indnalopt) <> None -> - (* hide [tm] name to avoid conflicts *) - spc () ++ str "as _" (* ++ pr_id (Option.get (tm_clash (tm,indnalopt)))*) - | _ -> mt ()) ++ -*) +let pr_asin pr (na,indnalopt) = (match na with (* Decision of printing "_" or not moved to constrextern.ml *) | Some na -> spc () ++ str "as " ++ pr_name na | None -> mt ()) ++ (match indnalopt with | None -> mt () -(* - | Some (_,ind,nal) -> - spc () ++ str "in " ++ - hov 0 (pr_reference ind ++ prlist (pr_arg pr_name) nal)) -*) - | Some t -> spc () ++ str "in " ++ pr lsimple t)) + | Some t -> spc () ++ str "in " ++ pr lsimple t) + +let pr_case_item pr (tm,asin) = + hov 0 (pr (lcast,E) tm ++ pr_asin pr asin) let pr_case_type pr po = match po with @@ -551,15 +540,24 @@ let rec pr sep inherited a = else p, lproj | CApp (_,(None,a),l) -> pr_app (pr mt) a l, lapp - | CCases (_,rtntypopt,c,eqns) -> + | CCases (_,LetPatternStyle,rtntypopt,[c,asin],[(_,[(loc,[p])],b)]) -> + hv 0 ( + str "let '" ++ + hov 0 (pr_patt ltop p ++ + pr_asin (pr_dangling_with_for mt) asin ++ + str " :=" ++ pr spc ltop c ++ + pr_case_type (pr_dangling_with_for mt) rtntypopt ++ + str " in" ++ pr spc ltop b)), + lletpattern + | CCases(_,_,rtntypopt,c,eqns) -> v 0 (hv 0 (str "match" ++ brk (1,2) ++ - hov 0 ( - prlist_with_sep sep_v - (pr_case_item (pr_dangling_with_for mt)) c - ++ pr_case_type (pr_dangling_with_for mt) rtntypopt) ++ - spc () ++ str "with") ++ - prlist (pr_eqn (pr mt)) eqns ++ spc() ++ str "end"), + hov 0 ( + prlist_with_sep sep_v + (pr_case_item (pr_dangling_with_for mt)) c + ++ pr_case_type (pr_dangling_with_for mt) rtntypopt) ++ + spc () ++ str "with") ++ + prlist (pr_eqn (pr mt)) eqns ++ spc() ++ str "end"), latom | CLetTuple (_,nal,(na,po),c,b) -> hv 0 ( @@ -571,11 +569,6 @@ let rec pr sep inherited a = pr spc ltop c ++ str " in") ++ pr spc ltop b), lletin - | CLetPattern (_, p, c, b) -> - hv 0 ( - str "let| " ++ - hov 0 (pr_patt ltop p ++ str " :=" ++ pr spc ltop c ++ str " in") ++ - pr spc ltop b), lletpattern | CIf (_,c,(na,po),b1,b2) -> (* On force les parenthèses autour d'un "if" sous-terme (même si le parsing est lui plus tolérant) *) diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index b5ad753afc..922c7af163 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -153,7 +153,7 @@ let rec mlexpr_of_constr = function | Topconstr.CLetIn (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO" | Topconstr.CAppExpl (loc,a,l) -> <:expr< Topconstr.CAppExpl $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_reference a$ $mlexpr_of_list mlexpr_of_constr l$ >> | Topconstr.CApp (loc,a,l) -> <:expr< Topconstr.CApp $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_constr a$ $mlexpr_of_list (mlexpr_of_pair mlexpr_of_constr (mlexpr_of_option (mlexpr_of_located mlexpr_of_explicitation))) l$ >> - | Topconstr.CCases (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO" + | Topconstr.CCases (loc,_,_,_,_) -> failwith "mlexpr_of_constr: TODO" | Topconstr.CHole (loc, None) -> <:expr< Topconstr.CHole $dloc$ None >> | Topconstr.CHole (loc, Some _) -> failwith "mlexpr_of_constr: TODO CHole (Some _)" | Topconstr.CNotation(_,ntn,l) -> diff --git a/pretyping/cases.ml b/pretyping/cases.ml index b7317b5be0..e1c5beeea2 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -65,7 +65,7 @@ let error_needs_inversion env x t = module type S = sig val compile_cases : - loc -> + loc -> case_style -> (type_constraint -> env -> rawconstr -> unsafe_judgment) * Evd.evar_defs ref -> type_constraint -> @@ -275,13 +275,14 @@ let push_history_pattern n current cont = *) type pattern_matching_problem = - { env : env; - evdref : Evd.evar_defs ref; - pred : predicate_signature option; - tomatch : tomatch_stack; - history : pattern_continuation; - mat : matrix; - caseloc : loc; + { env : env; + evdref : Evd.evar_defs ref; + pred : predicate_signature option; + tomatch : tomatch_stack; + history : pattern_continuation; + mat : matrix; + caseloc : loc; + casestyle : case_style; typing_function: type_constraint -> env -> rawconstr -> unsafe_judgment } (*--------------------------------------------------------------------------* @@ -1275,7 +1276,7 @@ and match_current pb tomatch = let (pred,typ,s) = find_predicate pb.caseloc pb.env pb.evdref pb.pred brtyps cstrs current indt pb.tomatch in - let ci = make_case_info pb.env mind RegularStyle in + let ci = make_case_info pb.env mind pb.casestyle in let case = mkCase (ci,nf_betaiota pred,current,brvals) in let inst = List.map mkRel deps in { uj_val = applist (case, inst); @@ -1504,7 +1505,7 @@ let extract_arity_signature env0 tomatchl tmsign = | Some (loc,_,_,_) -> user_err_loc (loc,"", str "Unexpected type annotation for a term of non inductive type")) - | IsInd (_,IndType(indf,realargs)) -> + | IsInd (term,IndType(indf,realargs)) -> let indf' = lift_inductive_family n indf in let (ind,params) = dest_ind_family indf' in let nrealargs = List.length realargs in @@ -1519,6 +1520,14 @@ let extract_arity_signature env0 tomatchl tmsign = List.rev realnal | None -> list_tabulate (fun _ -> Anonymous) nrealargs in let arsign = fst (get_arity env0 indf') in +(* let na = *) +(* match na with *) +(* | Name _ -> na *) +(* | Anonymous -> *) +(* match kind_of_term term with *) +(* | Rel n -> pi1 (lookup_rel n (Environ.rel_context env0)) *) +(* | _ -> Anonymous *) +(* in *) (na,None,build_dependent_inductive env0 indf') ::(List.map2 (fun x (_,c,t) ->(x,c,t)) realnal arsign) in let rec buildrec n = function @@ -1537,6 +1546,34 @@ let inh_conv_coerce_to_tycon loc env evdref j tycon = j | None -> j +(* We put the tycon inside the arity signature, possibly discovering dependencies. *) + +let prepare_predicate_from_arsign_tycon loc env evdref tomatchs sign arsign c = + let nar = List.fold_left (fun n sign -> List.length sign + n) 0 arsign in + let subst, len = + List.fold_left2 (fun (subst, len) (tm, tmtype) sign -> + let signlen = List.length sign in + match kind_of_term tm with + | Rel n when dependent tm c + && signlen = 1 (* The term to match is not of a dependent type itself *) -> + ((n, len) :: subst, len - signlen) + | _ -> (subst, len - signlen)) + ([], nar) tomatchs arsign + in + let rec predicate lift c = + match kind_of_term c with + | Rel n when n > lift -> + (try + (* Make the predicate dependent on the matched variable *) + let idx = List.assoc (n - lift) subst in + mkRel (idx + lift) + with Not_found -> + (* A variable that is not matched, lift over the arsign. *) + mkRel (n + nar)) + | _ -> + map_constr_with_binders succ predicate lift c + in predicate 0 c + (* Builds the predicate. If the predicate is dependent, its context is * made of 1+nrealargs assumptions for each matched term in an inductive @@ -1545,7 +1582,8 @@ let inh_conv_coerce_to_tycon loc env evdref j tycon = * Each matched terms are independently considered dependent or not. - * A type constraint but no annotation case: it is assumed non dependent. + * A type constraint but no annotation case: we try to specialize the + * tycon to make the predicate if it is not closed. *) let prepare_predicate loc typing_fun evdref env tomatchs sign tycon = function @@ -1553,9 +1591,23 @@ let prepare_predicate loc typing_fun evdref env tomatchs sign tycon = function | None -> (match tycon with | Some (None, t) -> - let names,pred = - prepare_predicate_from_tycon loc false env evdref tomatchs sign t - in Some (build_initial_predicate false names pred) + if noccur_with_meta 0 max_int t then + let names,pred = + prepare_predicate_from_tycon loc false env evdref tomatchs sign t + in + Some (build_initial_predicate false names pred) + else + let arsign = extract_arity_signature env tomatchs sign in + let env' = List.fold_right push_rels arsign env in + let names = List.rev (List.map (List.map pi1) arsign) in + let pred = prepare_predicate_from_arsign_tycon loc env' evdref tomatchs sign arsign t in + if eq_constr pred t then + let names,pred = + prepare_predicate_from_tycon loc false env evdref tomatchs sign t + in + Some (build_initial_predicate false names pred) + else + Some (build_initial_predicate true names pred) | _ -> None) (* Some type annotation *) @@ -1577,7 +1629,7 @@ let prepare_predicate loc typing_fun evdref env tomatchs sign tycon = function (**************************************************************************) (* Main entry of the matching compilation *) -let compile_cases loc (typing_fun, evdref) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns)= +let compile_cases loc style (typing_fun, evdref) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns)= (* We build the matrix of patterns and right-hand-side *) let matx = matx_of_eqns env tomatchl eqns in @@ -1596,13 +1648,14 @@ let compile_cases loc (typing_fun, evdref) (tycon : Evarutil.type_constraint) en let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in let pb = - { env = env; - evdref = evdref; - pred = pred; - tomatch = initial_pushed; - history = start_history (List.length initial_pushed); - mat = matx; - caseloc = loc; + { env = env; + evdref = evdref; + pred = pred; + tomatch = initial_pushed; + history = start_history (List.length initial_pushed); + mat = matx; + caseloc = loc; + casestyle = style; typing_function = typing_fun } in let j = compile pb in diff --git a/pretyping/cases.mli b/pretyping/cases.mli index d105ca2d0f..a2015c2b17 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -50,7 +50,7 @@ val error_needs_inversion : env -> constr -> types -> 'a module type S = sig val compile_cases : - loc -> + loc -> case_style -> (type_constraint -> env -> rawconstr -> unsafe_judgment) * evar_defs ref -> type_constraint -> env -> rawconstr option * tomatch_tuples * cases_clauses -> diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 34e6945584..164043cf7c 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -349,8 +349,6 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = let bl' = Array.map detype bl in let (nal,d) = it_destRLambda_or_LetIn_names consnargsl.(0) bl'.(0) in RLetTuple (dl,nal,(alias,pred),tomatch,d) - | LetPatternStyle when List.length eqnl = 1 -> (* If irrefutable due to some inversion, print as match *) - RLetPattern (dl,(tomatch,(alias,aliastyp)),List.hd eqnl) | IfStyle when aliastyp = None -> let bl' = Array.map detype bl in let nondepbrs = @@ -359,9 +357,9 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = RIf (dl,tomatch,(alias,pred), Option.get nondepbrs.(0),Option.get nondepbrs.(1)) else - RCases (dl,pred,[tomatch,(alias,aliastyp)],eqnl) + RCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl) | _ -> - RCases (dl,pred,[tomatch,(alias,aliastyp)],eqnl) + RCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl) let detype_sort = function | Prop c -> RProp c @@ -605,7 +603,7 @@ let rec subst_rawconstr subst raw = if r1' == r1 && r2' == r2 then raw else RLetIn (loc,n,r1',r2') - | RCases (loc,rtno,rl,branches) -> + | RCases (loc,sty,rtno,rl,branches) -> let rtno' = Option.smartmap (subst_rawconstr subst) rtno and rl' = list_smartmap (fun (a,x as y) -> let a' = subst_rawconstr subst a in @@ -625,7 +623,7 @@ let rec subst_rawconstr subst raw = branches in if rtno' == rtno && rl' == rl && branches' == branches then raw else - RCases (loc,rtno',rl',branches') + RCases (loc,sty,rtno',rl',branches') | RLetTuple (loc,nal,(na,po),b,c) -> let po' = Option.smartmap (subst_rawconstr subst) po @@ -633,28 +631,6 @@ let rec subst_rawconstr subst raw = and c' = subst_rawconstr subst c in if po' == po && b' == b && c' == c then raw else RLetTuple (loc,nal,(na,po'),b',c') - - | RLetPattern (loc, (a,x as c), (loc',idl,cpl,r as branch)) -> - let c' = - let a' = subst_rawconstr subst a in - let (n,topt) = x in - let topt' = Option.smartmap - (fun (loc,(sp,i),x,y as t) -> - let sp' = subst_kn subst sp in - if sp == sp' then t else (loc,(sp',i),x,y)) - topt - in - if a == a' && topt == topt' then c else (a',(n,topt')) - in - let p' = - let cpl' = - list_smartmap (subst_cases_pattern subst) cpl - and r' = subst_rawconstr subst r in - if cpl' == cpl && r' == r then branch else - (loc',idl,cpl',r') - in - if c' == c && p' == branch then raw else - RLetPattern (loc, c', p') | RIf (loc,c,(na,po),b1,b2) -> let po' = Option.smartmap (subst_rawconstr subst) po diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 845f9fae1f..90a3728ebb 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -245,7 +245,7 @@ let rec pat_of_raw metas vars = function let c = List.fold_left mkRLambda c nal in PCase ((LetStyle,[|1|],None,None),PMeta None,pat_of_raw metas vars b, [|pat_of_raw metas vars c|]) - | RCases (loc,p,[c,(na,indnames)],brs) -> + | RCases (loc,sty,p,[c,(na,indnames)],brs) -> let pred,ind_nargs, ind = match p,indnames with | Some p, Some (_,ind,n,nal) -> rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas vars p)), @@ -259,7 +259,7 @@ let rec pat_of_raw metas vars = function Array.init (List.length brs) (pat_of_raw_branch loc metas vars ind brs) in let cstr_nargs,brs = (Array.map fst cbrs, Array.map snd cbrs) in - PCase ((RegularStyle,cstr_nargs,ind,ind_nargs), pred, + PCase ((sty,cstr_nargs,ind,ind_nargs), pred, pat_of_raw metas vars c, brs) | r -> diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index f9fcdb7b63..83381710d3 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -582,23 +582,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct mkCase (ci, pred, cj.uj_val, [|b1;b2|]) in { uj_val = v; uj_type = p } - - | RLetPattern (loc, c, p) -> - (* Just use cases typing *) - let j = - pretype tycon env evdref lvar - (RCases (loc, None, [c], [p])) - in - (* Change case info *) - let j' = match kind_of_term j.uj_val with - Case (ci, po, c, br) -> - let pp_info = { ci.ci_pp_info with style = LetPatternStyle } in - { j with uj_val = mkCase ({ ci with ci_pp_info = pp_info }, po, c, br) } - | _ -> j - in j' - | RCases (loc,po,tml,eqns) -> - Cases.compile_cases loc + | RCases (loc,sty,po,tml,eqns) -> + Cases.compile_cases loc sty ((fun vtyc env -> pretype vtyc env evdref lvar),evdref) tycon env (* loc *) (po,tml,eqns) diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index e7f5de028f..fe48cd4fa7 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -62,10 +62,9 @@ type rawconstr = | RLambda of loc * name * binding_kind * rawconstr * rawconstr | RProd of loc * name * binding_kind * rawconstr * rawconstr | RLetIn of loc * name * rawconstr * rawconstr - | RCases of loc * rawconstr option * tomatch_tuples * cases_clauses + | RCases of loc * case_style * rawconstr option * tomatch_tuples * cases_clauses | RLetTuple of loc * name list * (name * rawconstr option) * rawconstr * rawconstr - | RLetPattern of loc * tomatch_tuple * cases_clause | RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr | RRec of loc * fix_kind * identifier array * rawdecl list array * rawconstr array * rawconstr array @@ -115,14 +114,12 @@ let map_rawconstr f = function | RLambda (loc,na,bk,ty,c) -> RLambda (loc,na,bk,f ty,f c) | RProd (loc,na,bk,ty,c) -> RProd (loc,na,bk,f ty,f c) | RLetIn (loc,na,b,c) -> RLetIn (loc,na,f b,f c) - | RCases (loc,rtntypopt,tml,pl) -> - RCases (loc,Option.map f rtntypopt, + | RCases (loc,sty,rtntypopt,tml,pl) -> + RCases (loc,sty,Option.map f rtntypopt, List.map (fun (tm,x) -> (f tm,x)) tml, List.map (fun (loc,idl,p,c) -> (loc,idl,p,f c)) pl) | RLetTuple (loc,nal,(na,po),b,c) -> RLetTuple (loc,nal,(na,Option.map f po),f b,f c) - | RLetPattern (loc,(b,x),(loc',idl,p,c)) -> - RLetPattern (loc,(f b,x),(loc',idl,p,f c)) | RIf (loc,c,(na,po),b1,b2) -> RIf (loc,f c,(na,Option.map f po),f b1,f b2) | RRec (loc,fk,idl,bl,tyl,bv) -> @@ -177,14 +174,13 @@ let occur_rawconstr id = | RLambda (loc,na,bk,ty,c) -> (occur ty) or ((na <> Name id) & (occur c)) | RProd (loc,na,bk,ty,c) -> (occur ty) or ((na <> Name id) & (occur c)) | RLetIn (loc,na,b,c) -> (occur b) or ((na <> Name id) & (occur c)) - | RCases (loc,rtntypopt,tml,pl) -> + | RCases (loc,sty,rtntypopt,tml,pl) -> (occur_option rtntypopt) or (List.exists (fun (tm,_) -> occur tm) tml) or (List.exists occur_pattern pl) | RLetTuple (loc,nal,rtntyp,b,c) -> occur_return_type rtntyp id or (occur b) or (not (List.mem (Name id) nal) & (occur c)) - | RLetPattern (loc, (b, _), p) -> (occur b) or (occur_pattern p) | RIf (loc,c,rtntyp,b1,b2) -> occur_return_type rtntyp id or (occur c) or (occur b1) or (occur b2) | RRec (loc,fk,idl,bl,tyl,bv) -> @@ -224,7 +220,7 @@ let free_rawvars = let vs' = vars bounded vs ty in let bounded' = add_name_to_ids bounded na in vars bounded' vs' c - | RCases (loc,rtntypopt,tml,pl) -> + | RCases (loc,sty,rtntypopt,tml,pl) -> let vs1 = vars_option bounded vs rtntypopt in let vs2 = List.fold_left (fun vs (tm,_) -> vars bounded vs tm) vs1 tml in List.fold_left (vars_pattern bounded) vs2 pl @@ -233,7 +229,6 @@ let free_rawvars = let vs2 = vars bounded vs1 b in let bounded' = List.fold_left add_name_to_ids bounded nal in vars bounded' vs2 c - | RLetPattern (loc, (c, _), p) -> vars_pattern bounded (vars bounded vs c) p | RIf (loc,c,rtntyp,b1,b2) -> let vs1 = vars_return_type bounded vs rtntyp in let vs2 = vars bounded vs1 c in @@ -285,8 +280,7 @@ let loc_of_rawconstr = function | RLambda (loc,_,_,_,_) -> loc | RProd (loc,_,_,_,_) -> loc | RLetIn (loc,_,_,_) -> loc - | RLetPattern (loc,_,_) -> loc - | RCases (loc,_,_,_) -> loc + | RCases (loc,_,_,_,_) -> loc | RLetTuple (loc,_,_,_,_) -> loc | RIf (loc,_,_,_,_) -> loc | RRec (loc,_,_,_,_,_) -> loc diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 7b342c4115..ab67a0922b 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -66,10 +66,9 @@ type rawconstr = | RLambda of loc * name * binding_kind * rawconstr * rawconstr | RProd of loc * name * binding_kind * rawconstr * rawconstr | RLetIn of loc * name * rawconstr * rawconstr - | RCases of loc * rawconstr option * tomatch_tuples * cases_clauses + | RCases of loc * case_style * rawconstr option * tomatch_tuples * cases_clauses | RLetTuple of loc * name list * (name * rawconstr option) * rawconstr * rawconstr - | RLetPattern of loc * tomatch_tuple * cases_clause | RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr | RRec of loc * fix_kind * identifier array * rawdecl list array * rawconstr array * rawconstr array diff --git a/test-suite/success/LetPat.v b/test-suite/success/LetPat.v new file mode 100644 index 0000000000..72c7cc1553 --- /dev/null +++ b/test-suite/success/LetPat.v @@ -0,0 +1,55 @@ +(* Simple let-patterns *) +Variable A B : Type. + +Definition l1 (t : A * B * B) : A := let '(x, y, z) := t in x. +Print l1. +Definition l2 (t : (A * B) * B) : A := let '((x, y), z) := t in x. +Definition l3 (t : A * (B * B)) : A := let '(x, (y, z)) := t in x. +Print l3. + +Record someT (A : Type) := mkT { a : nat; b: A }. + +Definition l4 A (t : someT A) : nat := let 'mkT x y := t in x. +Print l4. +Print sigT. + +Definition l5 A (B : A -> Type) (t : sigT B) : B (projT1 t) := + let 'existT x y := t return B (projT1 t) in y. + +Definition l6 A (B : A -> Type) (t : sigT B) : B (projT1 t) := + let 'existT x y as t' := t return B (projT1 t') in y. + +Definition l7 A (B : A -> Type) (t : sigT B) : B (projT1 t) := + let 'existT x y as t' in sigT _ := t return B (projT1 t') in y. + +Definition l8 A (B : A -> Type) (t : sigT B) : B (projT1 t) := + match t with + existT x y => y + end. + +(** An example from algebra, using let' and inference of return clauses + to deconstruct contexts. *) + +Record a_category (A : Type) (hom : A -> A -> Type) := { }. + +Definition category := { A : Type & { hom : A -> A -> Type & a_category A hom } }. + +Record a_functor (A : Type) (hom : A -> A -> Type) (C : a_category A hom) := { }. + +Notation " x :& y " := (@existT _ _ x y) (right associativity, at level 55) : core_scope. + +Definition functor (c d : category) := + let ' A :& homA :& CA := c in + let ' B :& homB :& CB := d in + A -> B. + +Definition identity_functor (c : category) : functor c c := + let 'A :& homA :& CA := c in + fun x => x. + +Definition functor_composition (a b c : category) : functor a b -> functor b c -> functor a c := + let ' (A :& homA :& CA) := a in + let ' (B :& homB :& CB) := b in + let ' (C :& homB :& CB) := c in + fun f g => + fun x : A => g (f x). diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v index 0850237202..d215bccb9e 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -97,8 +97,8 @@ Program Instance unit_eqdec : ! EqDec unit eq := Program Instance [ EqDec A eq, EqDec B eq ] => prod_eqdec : ! EqDec (prod A B) eq := equiv_dec x y := - dest x as (x1, x2) in - dest y as (y1, y2) in + let '(x1, x2) := x in + let '(y1, y2) := y in if x1 == y1 then if x2 == y2 then in_left else in_right diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v index 835294ce32..842d32fdbc 100644 --- a/theories/Classes/SetoidDec.v +++ b/theories/Classes/SetoidDec.v @@ -98,8 +98,8 @@ Program Instance unit_eqdec : EqDec (@eq_setoid unit) := Program Instance [ ! EqDec (@eq_setoid A), ! EqDec (@eq_setoid B) ] => prod_eqdec : EqDec (@eq_setoid (prod A B)) := equiv_dec x y := - dest x as (x1, x2) in - dest y as (y1, y2) in + let '(x1, x2) := x in + let '(y1, y2) := y in if x1 == y1 then if x2 == y2 then in_left else in_right diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index 8396987ff9..d76c281be1 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -164,7 +164,7 @@ let rec uri_of_constr c = uri_of_constr b; url_string " in "; uri_of_constr c | RCast (_,c, CastConv (_,t)) -> uri_of_constr c; url_string ":"; uri_of_constr t - | RRec _ | RIf _ | RLetTuple _ | RLetPattern _ | RCases _ -> + | RRec _ | RIf _ | RLetTuple _ | RCases _ -> error "Whelp does not support pattern-matching and (co-)fixpoint" | RVar _ | RRef _ | RHole _ | REvar _ | RSort _ | RCast (_,_, CastCoerce) -> anomaly "Written w/o parenthesis" |