diff options
Diffstat (limited to 'plugins/subtac/subtac_cases.ml')
| -rw-r--r-- | plugins/subtac/subtac_cases.ml | 110 |
1 files changed, 0 insertions, 110 deletions
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml index 26507a1ca..1e5722ef1 100644 --- a/plugins/subtac/subtac_cases.ml +++ b/plugins/subtac/subtac_cases.ml @@ -50,9 +50,6 @@ let make_anonymous_patvars = (* Environment management *) let push_rels vars env = List.fold_right push_rel vars env -let push_rel_defs = - List.fold_right (fun (x,d,t) e -> push_rel (x,Some d,t) e) - (* We have x1:t1...xn:tn,xi':ti,y1..yk |- c and re-generalize over xi:ti to get x1:t1...xn:tn,xi':ti,y1..yk |- c[xi:=xi'] *) @@ -152,8 +149,6 @@ and pattern_continuation = let start_history n = Continuation (n, [], Top) -let initial_history = function Continuation (_,[],Top) -> true | _ -> false - let feed_history arg = function | Continuation (n, l, h) when n>=1 -> Continuation (n-1, arg :: l, h) @@ -392,9 +387,6 @@ let map_tomatch_type f = function let liftn_tomatch_type n depth = map_tomatch_type (liftn n depth) let lift_tomatch_type n = liftn_tomatch_type n 1 -let lift_tomatch n ((current,typ),info) = - ((lift n current,lift_tomatch_type n typ),info) - (**********************************************************************) (* Utilities on patterns *) @@ -407,12 +399,6 @@ let alias_of_pat = function | PatVar (_,name) -> name | PatCstr(_,_,_,name) -> name -let unalias_pat = function - | PatVar (c,name) as p -> - if name = Anonymous then p else PatVar (c,Anonymous) - | PatCstr(a,b,c,name) as p -> - if name = Anonymous then p else PatCstr (a,b,c,Anonymous) - let remove_current_pattern eqn = match eqn.patterns with | pat::pats -> @@ -581,9 +567,6 @@ let replace_tomatch n c = ::(replrec (depth+1) rest) in replrec 0 -let liftn_rel_declaration n k = map_rel_declaration (liftn n k) -let substnl_rel_declaration sigma k = map_rel_declaration (substnl sigma k) - let rec liftn_tomatch_stack n depth = function | [] -> [] | Pushed ((c,tm),l)::rest -> @@ -1319,99 +1302,6 @@ let matx_of_eqns env eqns = (************************************************************************) (* preparing the elimination predicate if any *) -let build_expected_arity env isevars isdep tomatchl = - let cook n = function - | _,IsInd (_,IndType(indf,_)) -> - let indf' = lift_inductive_family n indf in - Some (build_dependent_inductive env indf', fst (get_arity env indf')) - | _,NotInd _ -> None - in - let rec buildrec n env = function - | [] -> new_Type () - | tm::ltm -> - match cook n tm with - | None -> buildrec n env ltm - | Some (ty1,aritysign) -> - let rec follow n env = function - | d::sign -> - mkProd_or_LetIn_name env - (follow (n+1) (push_rel d env) sign) d - | [] -> - if isdep then - mkProd (Anonymous, ty1, - buildrec (n+1) - (push_rel_assum (Anonymous, ty1) env) - ltm) - else buildrec n env ltm - in follow n env (List.rev aritysign) - in buildrec 0 env tomatchl - -let extract_predicate_conclusion isdep tomatchl pred = - let cook = function - | _,IsInd (_,IndType(_,args)) -> Some (List.length args) - | _,NotInd _ -> None in - let rec decomp_lam_force n l p = - if n=0 then (l,p) else - match kind_of_term p with - | Lambda (na,_,c) -> decomp_lam_force (n-1) (na::l) c - | _ -> (* eta-expansion *) - let na = Name (id_of_string "x") in - decomp_lam_force (n-1) (na::l) (applist (lift 1 p, [mkRel 1])) in - let rec buildrec allnames p = function - | [] -> (List.rev allnames,p) - | tm::ltm -> - match cook tm with - | None -> - let p = - (* adjust to a sign containing the NotInd's *) - if isdep then lift 1 p else p in - let names = if isdep then [Anonymous] else [] in - buildrec (names::allnames) p ltm - | Some n -> - let n = if isdep then n+1 else n in - let names,p = decomp_lam_force n [] p in - buildrec (names::allnames) p ltm - in buildrec [] pred tomatchl - -let set_arity_signature dep n arsign tomatchl pred x = - (* avoid is not exhaustive ! *) - let rec decomp_lam_force n avoid l p = - if n = 0 then (List.rev l,p,avoid) else - match p with - | RLambda (_,(Name id as na),k,_,c) -> - decomp_lam_force (n-1) (id::avoid) (na::l) c - | RLambda (_,(Anonymous as na),k,_,c) -> decomp_lam_force (n-1) avoid (na::l) c - | _ -> - let x = next_ident_away (id_of_string "x") avoid in - decomp_lam_force (n-1) (x::avoid) (Name x :: l) - (* eta-expansion *) - (let a = RVar (dummy_loc,x) in - match p with - | RApp (loc,p,l) -> RApp (loc,p,l@[a]) - | _ -> (RApp (dummy_loc,p,[a]))) in - let rec decomp_block avoid p = function - | ([], _) -> x := Some p - | ((_,IsInd (_,IndType(indf,realargs)))::l),(y::l') -> - let (ind,params) = dest_ind_family indf in - let (nal,p,avoid') = decomp_lam_force (List.length realargs) avoid [] p - in - let na,p,avoid' = - if dep then decomp_lam_force 1 avoid' [] p else [Anonymous],p,avoid' - in - y := - (List.hd na, - if List.for_all ((=) Anonymous) nal then - None - else - Some (dummy_loc, ind, (List.map (fun _ -> Anonymous) params)@nal)); - decomp_block avoid' p (l,l') - | (_::l),(y::l') -> - y := (Anonymous,None); - decomp_block avoid p (l,l') - | _ -> anomaly "set_arity_signature" - in - decomp_block [] pred (tomatchl,arsign) - let oldprepare_predicate_from_tycon loc dep env isevars tomatchs sign c = let cook (n, l, env, signs) = function | c,IsInd (_,IndType(indf,realargs)) -> |