diff options
Diffstat (limited to 'tactics/tacticals.ml')
| -rw-r--r-- | tactics/tacticals.ml | 70 |
1 files changed, 35 insertions, 35 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 2b69d7233..a20fe72ef 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -86,7 +86,7 @@ let rec tclFIRST_PROGRESS_ON tac = function (************************************************************************) let nthDecl m gl = - try List.nth (pf_hyps gl) (m-1) + try List.nth (pf_hyps gl) (m-1) with Failure _ -> error "No such assumption." let nthHypId m gl = pi1 (nthDecl m gl) @@ -129,7 +129,7 @@ let afterHyp id gl = or (Some id), where id is an identifier. This type is useful for defining tactics that may be used either to transform the conclusion (None) or to transform a hypothesis id (Some id). -- - --Eduardo (8/8/97) + --Eduardo (8/8/97) *) (* A [simple_clause] is a set of hypotheses, possibly extended with @@ -156,7 +156,7 @@ let simple_clause_of cl gls = let error_body_selection () = error "This tactic does not support body selection" in let hyps = - match cl.onhyps with + match cl.onhyps with | None -> List.map Option.make (pf_ids_of_hyps gls) | Some l -> @@ -186,7 +186,7 @@ let onClauseLR tac cl gls = tclMAP tac (List.rev (simple_clause_of cl gls)) gls let ifOnHyp pred tac1 tac2 id gl = if pred (id,pf_get_hyp_typ gl id) then tac1 id gl - else + else tac2 id gl @@ -225,14 +225,14 @@ type concrete_clause = clause_atom list let concrete_clause_of cl gls = let hyps = - match cl.onhyps with + match cl.onhyps with | None -> let f id = OnHyp (id,all_occurrences_expr,InHyp) in List.map f (pf_ids_of_hyps gls) | Some l -> List.map (fun ((occs,id),w) -> OnHyp (id,occs,w)) l in if cl.concl_occs = no_occurrences_expr then hyps - else + else OnConcl cl.concl_occs :: hyps (************************************************************************) @@ -241,10 +241,10 @@ let concrete_clause_of cl gls = (* The following tacticals allow to apply a tactic to the branches generated by the application of an elimination - tactic. + tactic. Two auxiliary types --branch_args and branch_assumptions-- are - used to keep track of some information about the ``branches'' of + used to keep track of some information about the ``branches'' of the elimination. *) type branch_args = { @@ -262,18 +262,18 @@ type branch_assumptions = { assums : named_context} (* the list of assumptions introduced *) let fix_empty_or_and_pattern nv l = - (* 1- The syntax does not distinguish between "[ ]" for one clause with no + (* 1- The syntax does not distinguish between "[ ]" for one clause with no names and "[ ]" for no clause at all *) - (* 2- More generally, we admit "[ ]" for any disjunctive pattern of + (* 2- More generally, we admit "[ ]" for any disjunctive pattern of arbitrary length *) if l = [[]] then list_make nv [] else l let check_or_and_pattern_size loc names n = if List.length names <> n then - if n = 1 then + if n = 1 then user_err_loc (loc,"",str "Expects a conjunctive pattern.") - else - user_err_loc (loc,"",str "Expects a disjunctive pattern with " ++ int n + else + user_err_loc (loc,"",str "Expects a disjunctive pattern with " ++ int n ++ str " branches.") let compute_induction_names n = function @@ -288,7 +288,7 @@ let compute_induction_names n = function let compute_construtor_signatures isrec (_,k as ity) = let rec analrec c recargs = - match kind_of_term c, recargs with + match kind_of_term c, recargs with | Prod (_,_,c), recarg::rest -> let b = match dest_recarg recarg with | Norec | Imbr _ -> false @@ -297,7 +297,7 @@ let compute_construtor_signatures isrec (_,k as ity) = | LetIn (_,_,_,c), rest -> false :: (analrec c rest) | _, [] -> [] | _ -> anomaly "compute_construtor_signatures" - in + in let (mib,mip) = Global.lookup_inductive ity in let n = mib.mind_nparams in let lc = @@ -305,27 +305,27 @@ let compute_construtor_signatures isrec (_,k as ity) = let lrecargs = dest_subterms mip.mind_recargs in array_map2 analrec lc lrecargs -let elimination_sort_of_goal gl = +let elimination_sort_of_goal gl = pf_apply Retyping.get_sort_family_of gl (pf_concl gl) -let elimination_sort_of_hyp id gl = +let elimination_sort_of_hyp id gl = pf_apply Retyping.get_sort_family_of gl (pf_get_hyp_typ gl id) let elimination_sort_of_clause = function - | None -> elimination_sort_of_goal + | None -> elimination_sort_of_goal | Some id -> elimination_sort_of_hyp id (* Find the right elimination suffix corresponding to the sort of the goal *) (* c should be of type A1->.. An->B with B an inductive definition *) -let general_elim_then_using mk_elim - isrec allnames tac predicate (indbindings,elimbindings) +let general_elim_then_using mk_elim + isrec allnames tac predicate (indbindings,elimbindings) ind indclause gl = let elim = mk_elim ind gl in (* applying elimination_scheme just a little modified *) let indclause' = clenv_match_args indbindings indclause in let elimclause = mk_clenv_from gl (elim,pf_type_of gl elim) in - let indmv = + let indmv = match kind_of_term (last_arg elimclause.templval.Evd.rebus) with | Meta mv -> mv | _ -> anomaly "elimination" @@ -341,7 +341,7 @@ let general_elim_then_using mk_elim | Var id -> string_of_id id | _ -> "\b" in - error ("The elimination combinator " ^ name_elim ^ " is unknown.") + error ("The elimination combinator " ^ name_elim ^ " is unknown.") in let elimclause' = clenv_fchain indmv elimclause indclause' in let elimclause' = clenv_match_args elimbindings elimclause' in @@ -351,15 +351,15 @@ let general_elim_then_using mk_elim let (hd,largs) = decompose_app ce.templtyp.Evd.rebus in let ba = { branchsign = branchsigns.(i); branchnames = brnames.(i); - nassums = - List.fold_left + nassums = + List.fold_left (fun acc b -> if b then acc+2 else acc+1) 0 branchsigns.(i); branchnum = i+1; ity = ind; largs = List.map (clenv_nf_meta ce) largs; pred = clenv_nf_meta ce hd } - in + in tac ba gl in let branchtacs ce = Array.init (Array.length branchsigns) (after_tac ce) in @@ -368,7 +368,7 @@ let general_elim_then_using mk_elim | None -> elimclause' | Some p -> clenv_unify true Reduction.CONV (mkMeta pmv) p elimclause' - in + in elim_res_pf_THEN_i elimclause' branchtacs gl (* computing the case/elim combinators *) @@ -382,7 +382,7 @@ let gl_make_case_dep ind gl = let gl_make_case_nodep ind gl = pf_apply Indrec.make_case_nodep gl ind (elimination_sort_of_goal gl) -let elimination_then_using tac predicate bindings c gl = +let elimination_then_using tac predicate bindings c gl = let (ind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in let indclause = mk_clenv_from gl (c,t) in general_elim_then_using gl_make_elim @@ -394,14 +394,14 @@ let case_then_using = let case_nodep_then_using = general_elim_then_using gl_make_case_nodep false -let elimination_then tac = elimination_then_using tac None +let elimination_then tac = elimination_then_using tac None let simple_elimination_then tac = elimination_then tac ([],[]) -let make_elim_branch_assumptions ba gl = +let make_elim_branch_assumptions ba gl = let rec makerec (assums,cargs,constargs,recargs,indargs) lb lc = - match lb,lc with - | ([], _) -> + match lb,lc with + | ([], _) -> { ba = ba; assums = assums} | ((true::tl), ((idrec,_,_ as recarg)::(idind,_,_ as indarg)::idtl)) -> @@ -417,7 +417,7 @@ let make_elim_branch_assumptions ba gl = recargs, indargs) tl idtl | (_, _) -> anomaly "make_elim_branch_assumptions" - in + in makerec ([],[],[],[],[]) ba.branchsign (try list_firstn ba.nassums (pf_hyps gl) with Failure _ -> anomaly "make_elim_branch_assumptions") @@ -426,8 +426,8 @@ let elim_on_ba tac ba gl = tac (make_elim_branch_assumptions ba gl) gl let make_case_branch_assumptions ba gl = let rec makerec (assums,cargs,constargs,recargs) p_0 p_1 = - match p_0,p_1 with - | ([], _) -> + match p_0,p_1 with + | ([], _) -> { ba = ba; assums = assums} | ((true::tl), ((idrec,_,_ as recarg)::idtl)) -> @@ -441,7 +441,7 @@ let make_case_branch_assumptions ba gl = recargs, id::constargs) tl idtl | (_, _) -> anomaly "make_case_branch_assumptions" - in + in makerec ([],[],[],[]) ba.branchsign (try list_firstn ba.nassums (pf_hyps gl) with Failure _ -> anomaly "make_case_branch_assumptions") |