From e7492417f54a4210da1cdf909699621e4f9b890c Mon Sep 17 00:00:00 2001 From: msozeau Date: Mon, 12 Feb 2007 10:16:15 +0000 Subject: Fix matching on dependent types, taking a safe stand. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9641 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/subtac/subtac_cases.ml | 124 ++++++++++++++++++----------------- contrib/subtac/subtac_pretyping_F.ml | 30 ++++----- 2 files changed, 80 insertions(+), 74 deletions(-) diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml index b289afaa1..9a1ebd480 100644 --- a/contrib/subtac/subtac_cases.ml +++ b/contrib/subtac/subtac_cases.ml @@ -1500,7 +1500,7 @@ let set_arity_signature dep n arsign tomatchl pred x = in decomp_block [] pred (tomatchl,arsign) -let prepare_predicate_from_tycon loc dep env isevars tomatchs sign c = +let oldprepare_predicate_from_tycon loc dep env isevars tomatchs sign c = let cook (n, l, env, signs) = function | c,IsInd (_,IndType(indf,realargs)) -> let indf' = lift_inductive_family n indf in @@ -1685,7 +1685,7 @@ let rec is_included x y = else false let build_ineqs prevpatterns pats liftsign patargs = - let tomatchs = List.length pats in + let _tomatchs = List.length pats in let diffs = List.fold_left (fun c eqnpats -> @@ -1851,15 +1851,18 @@ let prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs sign tycon let arsign = extract_arity_signature env tomatchs sign in let env = List.fold_right push_rels arsign env in let allnames = List.rev (List.map (List.map pi1) arsign) in - let predcclj = typing_fun (mk_tycon (new_Type ())) env rtntyp in -(* let _ = *) -(* option_map (fun tycon -> *) -(* isevars := Coercion.inh_conv_coerces_to loc env !isevars predcclj.uj_val *) -(* (lift_tycon_type (List.length arsign) tycon)) *) -(* tycon *) -(* in *) - let predccl = (j_nf_isevar !isevars predcclj).uj_val in - Some (build_initial_predicate true allnames predccl) + match rtntyp with + | Some rtntyp -> + let predcclj = typing_fun (mk_tycon (new_Type ())) env rtntyp in + let predccl = (j_nf_isevar !isevars predcclj).uj_val in + Some (build_initial_predicate true allnames predccl) + | None -> + match valcon_of_tycon tycon with + | Some ty -> + let names,pred = + oldprepare_predicate_from_tycon loc false env isevars tomatchs sign ty + in Some (build_initial_predicate true names pred) + | None -> None let lift_ctx n ctx = let ctx', _ = @@ -1882,6 +1885,10 @@ let abstract_tomatch env tomatchs = ([], [], []) tomatchs in List.rev prev, ctx +let is_dependent_ind = function + IsInd (_, IndType (indf, args)) when List.length args > 0 -> true + | _ -> false + (**************************************************************************) (* Main entry of the matching compilation *) @@ -1897,55 +1904,54 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e let tomatchs_len = List.length tomatchs_lets in let tycon = lift_tycon tomatchs_len tycon in let env = push_rel_context tomatchs_lets env in - match predopt with - None -> - let lets, matx = constrs_of_pats typing_fun tycon env isevars matx tomatchs in - let matx = List.rev matx in - let len = List.length lets in - let sign = - let arsign = extract_arity_signature env tomatchs (List.map snd tomatchl) in - List.map (lift_rel_context len) arsign - in - let env = push_rels lets env in - let matx = List.map (fun eqn -> { eqn with rhs = { eqn.rhs with rhs_env = env } }) matx in - let tycon = lift_tycon len tycon in - let tomatchs = List.map (fun (x, y) -> lift len x, lift_tomatch_type len y) tomatchs in - let args = List.map (fun (tm,ty) -> mk_refl (type_of_tomatch ty) tm) tomatchs in - - (* We build the elimination predicate if any and check its consistency *) - (* with the type of arguments to match *) - let pred, opred = prepare_predicate_from_tycon loc typing_fun isevars env tomatchs sign tycon in - (* We push the initial terms to match and push their alias to rhs' envs *) - (* names of aliases will be recovered from patterns (hence Anonymous here) *) - let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in - - let pb = - { env = env; - isevars = isevars; - pred = Some pred; - tomatch = initial_pushed; - history = start_history (List.length initial_pushed); - mat = matx; - caseloc = loc; - typing_function = typing_fun } in - - let _, j = compile pb in - (* We check for unused patterns *) - List.iter (check_unused_pattern env) matx; - let ty = out_some (valcon_of_tycon tycon0) in - let body = it_mkLambda_or_LetIn (applistc j.uj_val args) lets in - let j = - { uj_val = it_mkLambda_or_LetIn body tomatchs_lets; - uj_type = ty; } - in - inh_conv_coerce_to_tycon loc env isevars j tycon0 - - | Some rtntyp -> - (* We build the elimination predicate if any and check its consistency *) - (* with the type of arguments to match *) - let tmsign = List.map snd tomatchl in - let pred = prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs tmsign tycon rtntyp in + let isdep = List.exists (fun (x, y) -> is_dependent_ind y) tomatchs in + if predopt = None && not isdep then + let lets, matx = constrs_of_pats typing_fun tycon env isevars matx tomatchs in + let matx = List.rev matx in + let len = List.length lets in + let sign = + let arsign = extract_arity_signature env tomatchs (List.map snd tomatchl) in + List.map (lift_rel_context len) arsign + in + let env = push_rels lets env in + let matx = List.map (fun eqn -> { eqn with rhs = { eqn.rhs with rhs_env = env } }) matx in + let tycon = lift_tycon len tycon in + let tomatchs = List.map (fun (x, y) -> lift len x, lift_tomatch_type len y) tomatchs in + let args = List.map (fun (tm,ty) -> mk_refl (type_of_tomatch ty) tm) tomatchs in + (* We build the elimination predicate if any and check its consistency *) + (* with the type of arguments to match *) + let pred, opred = prepare_predicate_from_tycon loc typing_fun isevars env tomatchs sign tycon in + (* We push the initial terms to match and push their alias to rhs' envs *) + (* names of aliases will be recovered from patterns (hence Anonymous here) *) + let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in + + let pb = + { env = env; + isevars = isevars; + pred = Some pred; + tomatch = initial_pushed; + history = start_history (List.length initial_pushed); + mat = matx; + caseloc = loc; + typing_function = typing_fun } in + + let _, j = compile pb in + (* We check for unused patterns *) + List.iter (check_unused_pattern env) matx; + let ty = out_some (valcon_of_tycon tycon0) in + let body = it_mkLambda_or_LetIn (applistc j.uj_val args) lets in + let j = + { uj_val = it_mkLambda_or_LetIn body tomatchs_lets; + uj_type = ty; } + in + inh_conv_coerce_to_tycon loc env isevars j tycon0 + else + (* We build the elimination predicate if any and check its consistency *) + (* with the type of arguments to match *) + let tmsign = List.map snd tomatchl in + let pred = prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs tmsign tycon predopt in + (* We push the initial terms to match and push their alias to rhs' envs *) (* names of aliases will be recovered from patterns (hence Anonymous here) *) let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml index 9e44c9096..dc199c1d0 100644 --- a/contrib/subtac/subtac_pretyping_F.ml +++ b/contrib/subtac/subtac_pretyping_F.ml @@ -364,21 +364,21 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct error_case_not_inductive_loc cloc env (evars_of !isevars) cj in let cstrs = get_constructors env indf in - if Array.length cstrs <> 1 then - user_err_loc (loc,"",str "Destructing let is only for inductive types with one constructor"); - let cs = cstrs.(0) in - if List.length nal <> cs.cs_nargs then - user_err_loc (loc,"", str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables"); - let fsign = List.map2 (fun na (_,c,t) -> (na,c,t)) - (List.rev nal) cs.cs_args in - let env_f = push_rels fsign env in - (* Make dependencies from arity signature impossible *) - let arsgn = - let arsgn,_ = get_arity env indf in - if not !allow_anonymous_refs then - List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn - else arsgn - in + if Array.length cstrs <> 1 then + user_err_loc (loc,"",str "Destructing let is only for inductive types with one constructor"); + let cs = cstrs.(0) in + if List.length nal <> cs.cs_nargs then + user_err_loc (loc,"", str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables"); + let fsign = List.map2 (fun na (_,c,t) -> (na,c,t)) + (List.rev nal) cs.cs_args in + let env_f = push_rels fsign env in + (* Make dependencies from arity signature impossible *) + let arsgn = + let arsgn,_ = get_arity env indf in + if not !allow_anonymous_refs then + List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn + else arsgn + in let psign = (na,None,build_dependent_inductive env indf)::arsgn in let nar = List.length arsgn in (match po with -- cgit v1.2.3