diff options
Diffstat (limited to 'proofs')
-rw-r--r-- | proofs/clenvtac.ml | 24 | ||||
-rw-r--r-- | proofs/decl_expr.mli | 22 | ||||
-rw-r--r-- | proofs/decl_mode.ml | 40 | ||||
-rw-r--r-- | proofs/decl_mode.mli | 6 | ||||
-rw-r--r-- | proofs/evar_refiner.ml | 12 | ||||
-rw-r--r-- | proofs/evar_refiner.mli | 4 | ||||
-rw-r--r-- | proofs/logic.ml | 166 | ||||
-rw-r--r-- | proofs/logic.mli | 4 | ||||
-rw-r--r-- | proofs/pfedit.ml | 78 | ||||
-rw-r--r-- | proofs/pfedit.mli | 4 | ||||
-rw-r--r-- | proofs/proof_trees.ml | 16 | ||||
-rw-r--r-- | proofs/proof_type.ml | 6 | ||||
-rw-r--r-- | proofs/proof_type.mli | 18 | ||||
-rw-r--r-- | proofs/redexpr.ml | 20 | ||||
-rw-r--r-- | proofs/refiner.ml | 248 | ||||
-rw-r--r-- | proofs/refiner.mli | 12 | ||||
-rw-r--r-- | proofs/tacexpr.ml | 28 | ||||
-rw-r--r-- | proofs/tacmach.ml | 44 | ||||
-rw-r--r-- | proofs/tacmach.mli | 4 | ||||
-rw-r--r-- | proofs/tactic_debug.ml | 6 |
20 files changed, 381 insertions, 381 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 87dd26779..bdc1f6b66 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -30,24 +30,24 @@ open Pattern open Tacexpr open Clenv - + (* This function put casts around metavariables whose type could not be * infered by the refiner, that is head of applications, predicates and * subject of Cases. * Does check that the casted type is closed. Anyway, the refiner would * fail in this case... *) -let clenv_cast_meta clenv = +let clenv_cast_meta clenv = let rec crec u = match kind_of_term u with | App _ | Case _ -> crec_hd u | Cast (c,_,_) when isMeta c -> u | _ -> map_constr crec u - + and crec_hd u = match kind_of_term (strip_outer_cast u) with | Meta mv -> - (try + (try let b = Typing.meta_type clenv.evd mv in assert (not (occur_meta b)); if occur_meta b then u @@ -57,7 +57,7 @@ let clenv_cast_meta clenv = | Case(ci,p,c,br) -> mkCase (ci, crec_hd p, crec_hd c, Array.map crec br) | _ -> u - in + in crec let clenv_value_cast_meta clenv = @@ -73,14 +73,14 @@ let clenv_pose_dependent_evars with_evars clenv = let clenv_refine with_evars ?(with_classes=true) clenv gls = let clenv = clenv_pose_dependent_evars with_evars clenv in - let evd' = - if with_classes then - Typeclasses.resolve_typeclasses ~fail:(not with_evars) - clenv.env clenv.evd + let evd' = + if with_classes then + Typeclasses.resolve_typeclasses ~fail:(not with_evars) + clenv.env clenv.evd else clenv.evd in tclTHEN - (tclEVARS evd') + (tclEVARS evd') (refine (clenv_cast_meta clenv (clenv_value clenv))) gls @@ -105,7 +105,7 @@ let e_res_pf clenv = res_pf clenv ~with_evars:true ~allow_K:false ~flags:dft open Unification let fail_quick_unif_flags = { - modulo_conv_on_closed_terms = Some full_transparent_state; + modulo_conv_on_closed_terms = Some full_transparent_state; use_metas_eagerly = false; modulo_delta = empty_transparent_state; resolve_evars = false; @@ -113,7 +113,7 @@ let fail_quick_unif_flags = { } (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *) -let unifyTerms ?(flags=fail_quick_unif_flags) m n gls = +let unifyTerms ?(flags=fail_quick_unif_flags) m n gls = let env = pf_env gls in let evd = create_goal_evar_defs (project gls) in let evd' = w_unify false env CONV ~flags m n evd in diff --git a/proofs/decl_expr.mli b/proofs/decl_expr.mli index d02060fc0..20a95dabf 100644 --- a/proofs/decl_expr.mli +++ b/proofs/decl_expr.mli @@ -12,7 +12,7 @@ open Names open Util open Tacexpr -type 'it statement = +type 'it statement = {st_label:name; st_it:'it} @@ -41,12 +41,12 @@ type ('it,'constr,'tac) cut = cut_by: 'constr list option; cut_using: 'tac option} -type ('var,'constr) hyp = - Hvar of 'var +type ('var,'constr) hyp = + Hvar of 'var | Hprop of 'constr statement -type ('constr,'tac) casee = - Real of 'constr +type ('constr,'tac) casee = + Real of 'constr | Virtual of ('constr statement,'constr,'tac) cut type ('hyp,'constr,'pat,'tac) bare_proof_instr = @@ -64,9 +64,9 @@ type ('hyp,'constr,'pat,'tac) bare_proof_instr = | Pfocus of 'constr statement | Pdefine of identifier * 'hyp list * 'constr | Pcast of identifier or_thesis * 'constr - | Psuppose of ('hyp,'constr) hyp list - | Pcase of 'hyp list*'pat*(('hyp,'constr or_thesis) hyp list) - | Ptake of 'constr list + | Psuppose of ('hyp,'constr) hyp list + | Pcase of 'hyp list*'pat*(('hyp,'constr or_thesis) hyp list) + | Ptake of 'constr list | Pper of elim_type * ('constr,'tac) casee | Pend of block_type | Pescape @@ -86,11 +86,11 @@ type raw_proof_instr = type glob_proof_instr = ((identifier*(Genarg.rawconstr_and_expr option)) located, - Genarg.rawconstr_and_expr, + Genarg.rawconstr_and_expr, Topconstr.cases_pattern_expr, Tacexpr.glob_tactic_expr) gen_proof_instr -type proof_pattern = +type proof_pattern = {pat_vars: Term.types statement list; pat_aliases: (Term.constr*Term.types) statement list; pat_constr: Term.constr; @@ -100,6 +100,6 @@ type proof_pattern = type proof_instr = (Term.constr statement, - Term.constr, + Term.constr, proof_pattern, Tacexpr.glob_tactic_expr) gen_proof_instr diff --git a/proofs/decl_mode.ml b/proofs/decl_mode.ml index cdb7b0675..a32b9777b 100644 --- a/proofs/decl_mode.ml +++ b/proofs/decl_mode.ml @@ -15,9 +15,9 @@ open Util let daimon_flag = ref false -let set_daimon_flag () = daimon_flag:=true +let set_daimon_flag () = daimon_flag:=true let clear_daimon_flag () = daimon_flag:=false -let get_daimon_flag () = !daimon_flag +let get_daimon_flag () = !daimon_flag type command_mode = Mode_tactic @@ -27,12 +27,12 @@ type command_mode = let mode_of_pftreestate pts = let goal = sig_it (Refiner.top_goal_of_pftreestate pts) in if goal.evar_extra = None then - Mode_tactic + Mode_tactic else Mode_proof - + let get_current_mode () = - try + try mode_of_pftreestate (Pfedit.get_pftreestate ()) with _ -> Mode_none @@ -42,7 +42,7 @@ let check_not_proof_mode str = type split_tree= Skip_patt of Idset.t * split_tree - | Split_patt of Idset.t * inductive * + | Split_patt of Idset.t * inductive * (bool array * (Idset.t * split_tree) option) array | Close_patt of split_tree | End_patt of (identifier * int) @@ -54,7 +54,7 @@ type elim_kind = type recpath = int option*Declarations.wf_paths -type per_info = +type per_info = {per_casee:constr; per_ctype:types; per_ind:inductive; @@ -64,7 +64,7 @@ type per_info = per_nparams:int; per_wf:recpath} -type stack_info = +type stack_info = Per of Decl_expr.elim_type * per_info * elim_kind * identifier list | Suppose_case | Claim @@ -73,7 +73,7 @@ type stack_info = type pm_info = { pm_stack : stack_info list} -let pm_in,pm_out = Dyn.create "pm_info" +let pm_in,pm_out = Dyn.create "pm_info" let get_info gl= match gl.evar_extra with @@ -81,30 +81,30 @@ let get_info gl= | Some extra -> try pm_out extra with _ -> invalid_arg "get_info" -let get_stack pts = +let get_stack pts = let info = get_info (sig_it (Refiner.nth_goal_of_pftreestate 1 pts)) in info.pm_stack -let get_top_stack pts = +let get_top_stack pts = let info = get_info (sig_it (Refiner.top_goal_of_pftreestate pts)) in info.pm_stack let get_end_command pts = - match mode_of_pftreestate pts with + match mode_of_pftreestate pts with Mode_proof -> - Some + Some begin match get_top_stack pts with [] -> "\"end proof\"" | Claim::_ -> "\"end claim\"" | Focus_claim::_-> "\"end focus\"" - | (Suppose_case :: Per (et,_,_,_) :: _ - | Per (et,_,_,_) :: _ ) -> + | (Suppose_case :: Per (et,_,_,_) :: _ + | Per (et,_,_,_) :: _ ) -> begin match et with - Decl_expr.ET_Case_analysis -> + Decl_expr.ET_Case_analysis -> "\"end cases\" or start a new case" - | Decl_expr.ET_Induction -> + | Decl_expr.ET_Induction -> "\"end induction\" or start a new case" end | _ -> anomaly "lonely suppose" @@ -112,7 +112,7 @@ let get_end_command pts = | Mode_tactic -> begin try - ignore + ignore (Refiner.up_until_matching_rule Proof_trees.is_proof_instr pts); Some "\"return\"" with Not_found -> None @@ -120,7 +120,7 @@ let get_end_command pts = | Mode_none -> error "no proof in progress" -let get_last env = - try +let get_last env = + try let (id,_,_) = List.hd (Environ.named_context env) in id with Invalid_argument _ -> error "no previous statement to use" diff --git a/proofs/decl_mode.mli b/proofs/decl_mode.mli index 6be3abdfe..e225c828d 100644 --- a/proofs/decl_mode.mli +++ b/proofs/decl_mode.mli @@ -23,7 +23,7 @@ type command_mode = | Mode_none val mode_of_pftreestate : pftreestate -> command_mode - + val get_current_mode : unit -> command_mode val check_not_proof_mode : string -> unit @@ -42,7 +42,7 @@ type elim_kind = type recpath = int option*Declarations.wf_paths -type per_info = +type per_info = {per_casee:constr; per_ctype:types; per_ind:inductive; @@ -52,7 +52,7 @@ type per_info = per_nparams:int; per_wf:recpath} -type stack_info = +type stack_info = Per of Decl_expr.elim_type * per_info * elim_kind * Names.identifier list | Suppose_case | Claim diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index d7a1232ad..25c668f5d 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -29,7 +29,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = (Pretyping.OfType (Some evi.evar_concl)) rawc with _ -> let loc = Rawterm.loc_of_rawconstr rawc in - user_err_loc + user_err_loc (loc,"",Pp.str ("Instance is not well-typed in the environment of " ^ string_of_existential evk)) in @@ -37,10 +37,10 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = (* vernac command Existential *) -let instantiate_pf_com n com pfts = +let instantiate_pf_com n com pfts = let gls = top_goal_of_pftreestate pfts in - let sigma = gls.sigma in - let (evk,evi) = + let sigma = gls.sigma in + let (evk,evi) = let evl = Evarutil.non_instantiated sigma in if (n <= 0) then error "incorrect existential variable index" @@ -48,8 +48,8 @@ let instantiate_pf_com n com pfts = error "not so many uninstantiated existential variables" else List.nth evl (n-1) - in + in let env = Evd.evar_env evi in - let rawc = Constrintern.intern_constr sigma env com in + let rawc = Constrintern.intern_constr sigma env com in let sigma' = w_refine (evk,evi) (([],[]),rawc) sigma in change_constraints_pftreestate sigma' pfts diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index a35a9b58b..ab0fdf831 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -20,10 +20,10 @@ open Rawterm (* Refinement of existential variables. *) -val w_refine : evar * evar_info -> +val w_refine : evar * evar_info -> (var_map * unbound_ltac_var_map) * rawconstr -> evar_defs -> evar_defs val instantiate_pf_com : int -> Topconstr.constr_expr -> pftreestate -> pftreestate -(* the instantiate tactic was moved to [tactics/evar_tactics.ml] *) +(* the instantiate tactic was moved to [tactics/evar_tactics.ml] *) diff --git a/proofs/logic.ml b/proofs/logic.ml index f1f33930e..eddf387f9 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -28,7 +28,7 @@ open Type_errors open Retyping open Evarutil open Tacexpr - + type refiner_error = (* Errors raised by the refiner *) @@ -50,7 +50,7 @@ open Pretype_errors let rec catchable_exception = function | Stdpp.Exc_located(_,e) -> catchable_exception e | LtacLocated(_,e) -> catchable_exception e - | Util.UserError _ | TypeError _ + | Util.UserError _ | TypeError _ | RefinerError _ | Indrec.RecursionSchemeError _ | Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _) (* unification errors *) @@ -58,7 +58,7 @@ let rec catchable_exception = function |NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _ |CannotFindWellTypedAbstraction _ |UnsolvableImplicit _)) -> true - | Typeclasses_errors.TypeClassError + | Typeclasses_errors.TypeClassError (_, Typeclasses_errors.UnsatisfiableConstraints _) -> true | _ -> false @@ -73,19 +73,19 @@ let with_check = Flags.with_option check (* [apply_to_hyp sign id f] splits [sign] into [tail::[id,_,_]::head] and returns [tail::(f head (id,_,_) (rev tail))] *) let apply_to_hyp sign id f = - try apply_to_hyp sign id f - with Hyp_not_found -> + try apply_to_hyp sign id f + with Hyp_not_found -> if !check then error "No such assumption." else sign let apply_to_hyp_and_dependent_on sign id f g = - try apply_to_hyp_and_dependent_on sign id f g - with Hyp_not_found -> + try apply_to_hyp_and_dependent_on sign id f g + with Hyp_not_found -> if !check then error "No such assumption." else sign let check_typability env sigma c = - if !check then let _ = type_of env sigma c in () + if !check then let _ = type_of env sigma c in () (************************************************************************) (************************************************************************) @@ -111,7 +111,7 @@ let recheck_typability (what,id) env sigma t = | Some id -> "hypothesis "^(string_of_id id) in error ("The correctness of "^s^" relies on the body of "^(string_of_id id)) - + let remove_hyp_body env sigma id = let sign = apply_to_hyp_and_dependent_on (named_context_val env) id @@ -121,7 +121,7 @@ let remove_hyp_body env sigma id = | Some c ->(id,None,t)) (fun (id',c,t as d) sign -> (if !check then - begin + begin let env = reset_with_named_context sign env in match c with | None -> recheck_typability (Some id',id) env sigma t @@ -130,7 +130,7 @@ let remove_hyp_body env sigma id = recheck_typability (Some id',id) env sigma b' end;d)) in - reset_with_named_context sign env + reset_with_named_context sign env (* Reordering of the context *) @@ -138,7 +138,7 @@ let remove_hyp_body env sigma id = (* sous-ordre du resultat. Par exemple, 2 hyps non mentionnee ne sont *) (* pas echangees. Choix: les hyps mentionnees ne peuvent qu'etre *) (* reculees par rapport aux autres (faire le contraire!) *) - + let mt_q = (Idmap.empty,[]) let push_val y = function (_,[] as q) -> q @@ -211,8 +211,8 @@ let check_decl_position env sign (x,_,_ as d) = (* Auxiliary functions for primitive MOVE tactic * * [move_hyp with_dep toleft (left,(hfrom,typfrom),right) hto] moves - * hyp [hfrom] at location [hto] which belongs to the hyps on the - * left side [left] of the full signature if [toleft=true] or to the hyps + * hyp [hfrom] at location [hto] which belongs to the hyps on the + * left side [left] of the full signature if [toleft=true] or to the hyps * on the right side [right] if [toleft=false]. * If [with_dep] then dependent hypotheses are moved accordingly. *) @@ -228,17 +228,17 @@ let split_sign hfrom hto l = let rec splitrec left toleft = function | [] -> error_no_such_hypothesis hfrom | (hyp,c,typ) as d :: right -> - if hyp = hfrom then + if hyp = hfrom then (left,right,d, toleft or hto = MoveToEnd true) else - splitrec (d::left) + splitrec (d::left) (toleft or hto = MoveAfter hyp or hto = MoveBefore hyp) right - in + in splitrec [] false l let hyp_of_move_location = function - | MoveAfter id -> id + | MoveAfter id -> id | MoveBefore id -> id | _ -> assert false @@ -258,12 +258,12 @@ let move_hyp with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto = List.rev first @ List.rev middle @ right | (hyp,_,_) as d :: right -> let (first',middle') = - if List.exists (test_dep d) middle then - if with_dep & hto <> MoveAfter hyp then + if List.exists (test_dep d) middle then + if with_dep & hto <> MoveAfter hyp then (first, d::middle) - else + else errorlabstrm "" (str "Cannot move " ++ pr_id idfrom ++ - pr_move_location pr_id hto ++ + pr_move_location pr_id hto ++ str (if toleft then ": it occurs in " else ": it depends on ") ++ pr_id hyp ++ str ".") else @@ -271,16 +271,16 @@ let move_hyp with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto = in if hto = MoveAfter hyp then List.rev first' @ List.rev middle' @ right - else + else moverec first' middle' right in - if toleft then - let right = + if toleft then + let right = List.fold_right push_named_context_val right empty_named_context_val in List.fold_left (fun sign d -> push_named_context_val d sign) - right (moverec [] [declfrom] left) - else - let right = + right (moverec [] [declfrom] left) + else + let right = List.fold_right push_named_context_val (moverec [] [declfrom] right) empty_named_context_val in List.fold_left (fun sign d -> push_named_context_val d sign) @@ -295,7 +295,7 @@ let rename_hyp id1 id2 sign = (************************************************************************) (* Implementation of the logical rules *) -(* Will only be used on terms given to the Refine rule which have meta +(* Will only be used on terms given to the Refine rule which have meta variables only in Application and Case *) let error_unsupported_deep_meta c = @@ -303,7 +303,7 @@ let error_unsupported_deep_meta c = strbrk "form contains metavariables deep inside the term is not " ++ strbrk "supported; try \"refine\" instead.") -let collect_meta_variables c = +let collect_meta_variables c = let rec collrec deep acc c = match kind_of_term c with | Meta mv -> if deep then error_unsupported_deep_meta () else mv::acc | Cast(c,_,_) -> collrec deep acc c @@ -312,12 +312,12 @@ let collect_meta_variables c = in List.rev (collrec false [] c) -let check_meta_variables c = +let check_meta_variables c = if not (list_distinct (collect_meta_variables c)) then raise (RefinerError (NonLinearProof c)) let check_conv_leq_goal env sigma arg ty conclty = - if !check & not (is_conv_leq env sigma ty conclty) then + if !check & not (is_conv_leq env sigma ty conclty) then raise (RefinerError (BadType (arg,ty,conclty))) let goal_type_of env sigma c = @@ -329,7 +329,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = let mk_goal hyps concl = mk_goal hyps concl goal.evar_extra in (* if not (occur_meta trm) then - let t'ty = (unsafe_machine env sigma trm).uj_type in + let t'ty = (unsafe_machine env sigma trm).uj_type in let _ = conv_leq_goal env sigma trm t'ty conclty in (goalacc,t'ty) else @@ -352,9 +352,9 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | Ind _ | Const _ when (isInd f or has_polymorphic_type (destConst f)) -> (* Sort-polymorphism of definition and inductive types *) - goalacc, + goalacc, type_of_global_reference_knowing_conclusion env sigma f conclty - | _ -> + | _ -> mk_hdgoals sigma goal goalacc f in let (acc'',conclty') = @@ -365,14 +365,14 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | Case (_,p,c,lf) -> let (acc',lbrty,conclty') = mk_casegoals sigma goal goalacc p c in check_conv_leq_goal env sigma trm conclty' conclty; - let acc'' = + let acc'' = array_fold_left2 (fun lacc ty fi -> fst (mk_refgoals sigma goal lacc ty fi)) - acc' lbrty lf + acc' lbrty lf in (acc'',conclty') - | _ -> + | _ -> if occur_meta trm then anomaly "refiner called with a meta in non app/case subterm"; @@ -397,8 +397,8 @@ and mk_hdgoals sigma goal goalacc trm = mk_refgoals sigma goal goalacc ty t | App (f,l) -> - let (acc',hdty) = - if isInd f or isConst f + let (acc',hdty) = + if isInd f or isConst f & not (array_exists occur_meta l) (* we could be finer *) then (goalacc,type_of_global_reference_knowing_parameters env sigma f l) @@ -408,10 +408,10 @@ and mk_hdgoals sigma goal goalacc trm = | Case (_,p,c,lf) -> let (acc',lbrty,conclty') = mk_casegoals sigma goal goalacc p c in - let acc'' = + let acc'' = array_fold_left2 (fun lacc ty fi -> fst (mk_refgoals sigma goal lacc ty fi)) - acc' lbrty lf + acc' lbrty lf in (acc'',conclty') @@ -434,7 +434,7 @@ and mk_arggoals sigma goal goalacc funty = function and mk_casegoals sigma goal goalacc p c = let env = evar_env goal in - let (acc',ct) = mk_hdgoals sigma goal goalacc c in + let (acc',ct) = mk_hdgoals sigma goal goalacc c in let (acc'',pt) = mk_hdgoals sigma goal acc' p in let indspec = try find_mrectype env sigma ct @@ -466,7 +466,7 @@ let norm_goal sigma gl = let red_fun = Evarutil.nf_evar sigma in let ncl = red_fun gl.evar_concl in let ngl = - { gl with + { gl with evar_concl = ncl; evar_hyps = map_named_val red_fun gl.evar_hyps } in if Evd.eq_evar_info ngl gl then None else Some ngl @@ -499,7 +499,7 @@ let prim_refiner r sigma goal = ([sg], sigma) | _ -> raise (RefinerError IntroNeedsProduct)) - + | Cut (b,replace,id,t) -> let sg1 = mk_goal sign (nf_betaiota sigma t) in let sign,cl,sigma = @@ -517,52 +517,52 @@ let prim_refiner r sigma goal = if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma) | FixRule (f,n,rest,j) -> - let rec check_ind env k cl = - match kind_of_term (strip_outer_cast cl) with - | Prod (na,c1,b) -> - if k = 1 then - try + let rec check_ind env k cl = + match kind_of_term (strip_outer_cast cl) with + | Prod (na,c1,b) -> + if k = 1 then + try fst (find_inductive env sigma c1) - with Not_found -> + with Not_found -> error "Cannot do a fixpoint on a non inductive type." - else + else check_ind (push_rel (na,None,c1) env) (k-1) b | _ -> error "Not enough products." in let (sp,_) = check_ind env n cl in let firsts,lasts = list_chop j rest in let all = firsts@(f,n,cl)::lasts in - let rec mk_sign sign = function + let rec mk_sign sign = function | (f,n,ar)::oth -> - let (sp',_) = check_ind env n ar in - if not (sp=sp') then - error ("Fixpoints should be on the same " ^ + let (sp',_) = check_ind env n ar in + if not (sp=sp') then + error ("Fixpoints should be on the same " ^ "mutual inductive declaration."); if !check && mem_named_context f (named_context_of_val sign) then error ("Name "^string_of_id f^" already used in the environment"); mk_sign (push_named_context_val (f,None,ar) sign) oth - | [] -> + | [] -> List.map (fun (_,_,c) -> mk_goal sign c) all - in + in (mk_sign sign all, sigma) - + | Cofix (f,others,j) -> - let rec check_is_coind env cl = + let rec check_is_coind env cl = let b = whd_betadeltaiota env sigma cl in match kind_of_term b with | Prod (na,c1,b) -> check_is_coind (push_rel (na,None,c1) env) b - | _ -> - try + | _ -> + try let _ = find_coinductive env sigma b in () - with Not_found -> + with Not_found -> error ("All methods must construct elements " ^ "in coinductive types.") in let firsts,lasts = list_chop j others in let all = firsts@(f,cl)::lasts in List.iter (fun (_,c) -> check_is_coind env c) all; - let rec mk_sign sign = function + let rec mk_sign sign = function | (f,ar)::oth -> (try (let _ = lookup_named_val f sign in @@ -571,7 +571,7 @@ let prim_refiner r sigma goal = | Not_found -> mk_sign (push_named_context_val (f,None,ar) sign) oth) | [] -> List.map (fun (_,c) -> mk_goal sign c) all - in + in (mk_sign sign all, sigma) | Refine c -> @@ -586,17 +586,17 @@ let prim_refiner r sigma goal = if (not !check) || is_conv_leq env sigma cl' cl then let sg = mk_goal sign cl' in ([sg], sigma) - else + else error "convert-concl rule passed non-converting term" | Convert_hyp (id,copt,ty) -> ([mk_goal (convert_hyp sign sigma (id,copt,ty)) cl], sigma) (* And now the structural rules *) - | Thin ids -> + | Thin ids -> let (hyps,concl,nsigma) = clear_hyps sigma ids sign cl in ([mk_goal hyps concl], nsigma) - + | ThinBody ids -> let clear_aux env id = let env' = remove_hyp_body env sigma id in @@ -608,9 +608,9 @@ let prim_refiner r sigma goal = ([sg], sigma) | Move (withdep, hfrom, hto) -> - let (left,right,declfrom,toleft) = + let (left,right,declfrom,toleft) = split_sign hfrom hto (named_context_of_val sign) in - let hyps' = + let hyps' = move_hyp withdep toleft (left,declfrom,right) hto in ([mk_goal hyps' cl], sigma) @@ -641,7 +641,7 @@ type variable_proof_status = ProofVar | SectionVar of identifier type proof_variable = name * variable_proof_status -let subst_proof_vars = +let subst_proof_vars = let rec aux p vars = let _,subst = List.fold_left (fun (n,l) var -> @@ -652,22 +652,22 @@ let subst_proof_vars = (n+1,t)) (p,[]) vars in replace_vars (List.rev subst) in aux 1 - + let rec rebind id1 id2 = function | [] -> [Name id2,SectionVar id1] - | (na,k as x)::l -> + | (na,k as x)::l -> if na = Name id1 then (Name id2,k)::l else let l' = rebind id1 id2 l in if na = Name id2 then (Anonymous,k)::l' else x::l' let add_proof_var id vl = (Name id,ProofVar)::vl -let proof_variable_index x = +let proof_variable_index x = let rec aux n = function | (Name id,ProofVar)::l when x = id -> n | _::l -> aux (n+1) l | [] -> raise Not_found - in + in aux 1 let prim_extractor subfun vl pft = @@ -683,7 +683,7 @@ let prim_extractor subfun vl pft = let cty = subst_proof_vars vl ty in mkLetIn (Name id, cb, cty, subfun (add_proof_var id vl) spf) | _ -> error "Incomplete proof!") - + | Some (Prim (Cut (b,_,id,t)),[spf1;spf2]) -> let spf1, spf2 = if b then spf1, spf2 else spf2, spf1 in mkLetIn (Name id,subfun vl spf1,subst_proof_vars vl t, @@ -698,7 +698,7 @@ let prim_extractor subfun vl pft = let newvl = List.fold_left (fun vl (id,_,_) -> add_proof_var id vl) (add_proof_var f vl) others in let lfix = Array.map (subfun newvl) (Array.of_list spfl) in - mkFix ((vn,j),(names,lcty,lfix)) + mkFix ((vn,j),(names,lcty,lfix)) | Some (Prim (Cofix (f,others,j)),spfl) -> let firsts,lasts = list_chop j others in @@ -706,14 +706,14 @@ let prim_extractor subfun vl pft = let lcty = Array.map (fun (_,ar) -> subst_proof_vars vl ar) all in let names = Array.map (fun (f,_) -> Name f) all in let newvl = List.fold_left (fun vl (id,_)-> add_proof_var id vl) - (add_proof_var f vl) others in + (add_proof_var f vl) others in let lfix = Array.map (subfun newvl) (Array.of_list spfl) in mkCoFix (j,(names,lcty,lfix)) - + | Some (Prim (Refine c),spfl) -> let mvl = collect_meta_variables c in let metamap = List.combine mvl (List.map (subfun vl) spfl) in - let cc = subst_proof_vars vl c in + let cc = subst_proof_vars vl c in plain_instance metamap cc (* Structural and conversion rules do not produce any proof *) @@ -726,10 +726,10 @@ let prim_extractor subfun vl pft = | Some (Prim (Thin _),[pf]) -> (* No need to make ids Anon in vl: subst_proof_vars take the most recent*) subfun vl pf - + | Some (Prim (ThinBody _),[pf]) -> subfun vl pf - + | Some (Prim (Move _|Order _),[pf]) -> subfun vl pf @@ -742,4 +742,4 @@ let prim_extractor subfun vl pft = | Some _ -> anomaly "prim_extractor" | None-> error "prim_extractor handed incomplete proof" - + diff --git a/proofs/logic.mli b/proofs/logic.mli index 8bc48ed54..0d56da382 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -26,9 +26,9 @@ val with_check : tactic -> tactic [Intro]: no check that the name does not exist\\ [Intro_after]: no check that the name does not exist and that variables in its type does not escape their scope\\ - [Intro_replacing]: no check that the name does not exist and that + [Intro_replacing]: no check that the name does not exist and that variables in its type does not escape their scope\\ - [Convert_hyp]: + [Convert_hyp]: no check that the name exist and that its type is convertible\\ *) diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 62668f7f3..11324ede9 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -81,26 +81,26 @@ let get_current_goal_context () = get_goal_context 1 let set_current_proof = Edit.focus proof_edits -let resume_proof (loc,id) = - try +let resume_proof (loc,id) = + try Edit.focus proof_edits id with Invalid_argument "Edit.focus" -> user_err_loc(loc,"Pfedit.set_proof",str"No such proof" ++ msg_proofs false) let suspend_proof () = - try + try Edit.unfocus proof_edits with Invalid_argument "Edit.unfocus" -> errorlabstrm "Pfedit.suspend_current_proof" (str"No active proof" ++ (msg_proofs true)) - + let resume_last_proof () = match (Edit.last_focused proof_edits) with | None -> errorlabstrm "resume_last" (str"No proof-editing in progress.") - | Some p -> + | Some p -> Edit.focus proof_edits p - + let get_current_proof_name () = match Edit.read proof_edits with | None -> @@ -114,14 +114,14 @@ let add_proof (na,pfs,ts) = let delete_proof_gen = Edit.delete proof_edits let delete_proof (loc,id) = - try + try delete_proof_gen id with (UserError ("Edit.delete",_)) -> user_err_loc (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs false) - + let mutate f = - try + try Edit.mutate proof_edits (fun _ pfs -> f pfs) with Invalid_argument "Edit.mutate" -> errorlabstrm "Pfedit.mutate" @@ -131,31 +131,31 @@ let start (na,ts) = let pfs = mk_pftreestate ts.top_goal in let pfs = Option.fold_right solve_pftreestate ts.top_init_tac pfs in add_proof(na,pfs,ts) - + let restart_proof () = match Edit.read proof_edits with - | None -> + | None -> errorlabstrm "Pfedit.restart" (str"No focused proof to restart" ++ msg_proofs true) - | Some(na,_,ts) -> + | Some(na,_,ts) -> delete_proof_gen na; start (na,ts); set_current_proof na let proof_term () = extract_pftreestate (get_pftreestate()) - + (* Detect is one has completed a subtree of the initial goal *) -let subtree_solved () = +let subtree_solved () = let pts = get_pftreestate () in - is_complete_proof (proof_of_pftreestate pts) & + is_complete_proof (proof_of_pftreestate pts) & not (is_top_pftreestate pts) -let tree_solved () = +let tree_solved () = let pts = get_pftreestate () in is_complete_proof (proof_of_pftreestate pts) -let top_tree_solved () = +let top_tree_solved () = let pts = get_pftreestate () in is_complete_proof (proof_of_pftreestate (top_of_tree pts)) @@ -165,19 +165,19 @@ let top_tree_solved () = let set_undo = function | None -> undo_limit := undo_default - | Some n -> - if n>=0 then + | Some n -> + if n>=0 then undo_limit := n - else + else error "Cannot set a negative undo limit" let get_undo () = Some !undo_limit let undo n = - try - Edit.undo proof_edits n; - (* needed because the resolution of a subtree is done in 2 steps - then a sequence of undo can lead to a focus on a completely solved + try + Edit.undo proof_edits n; + (* needed because the resolution of a subtree is done in 2 steps + then a sequence of undo can lead to a focus on a completely solved subtree - this solution only works properly if undoing one step *) if subtree_solved() then Edit.undo proof_edits 1 with (Invalid_argument "Edit.undo") -> @@ -186,14 +186,14 @@ let undo n = (* Undo current focused proof to reach depth [n]. This is used in [vernac_backtrack]. *) let undo_todepth n = - try + try Edit.undo_todepth proof_edits n with (Invalid_argument "Edit.undo") -> errorlabstrm "Pfedit.undo" (str"No focused proof" ++ msg_proofs true) (* Return the depth of the current focused proof stack, this is used to put informations in coq prompt (in emacs mode). *) -let current_proof_depth() = +let current_proof_depth() = try Edit.depth proof_edits with (Invalid_argument "Edit.depth") -> -1 @@ -206,7 +206,7 @@ let xml_cook_proof = ref (fun _ -> ()) let set_xml_cook_proof f = xml_cook_proof := f let cook_proof k = - let (pfs,ts) = get_state() + let (pfs,ts) = get_state() and ident = get_current_proof_name () in let {evar_concl=concl} = ts.top_goal and strength = ts.top_strength in @@ -220,19 +220,19 @@ let cook_proof k = const_entry_boxed = false}, ts.top_compute_guard, strength, ts.top_hook)) -let current_proof_statement () = +let current_proof_statement () = let ts = get_topstate() in - (get_current_proof_name (), ts.top_strength, + (get_current_proof_name (), ts.top_strength, ts.top_goal.evar_concl, ts.top_hook) (*********************************************************************) (* Abort functions *) (*********************************************************************) - + let refining () = [] <> (Edit.dom proof_edits) let check_no_pending_proofs () = - if refining () then + if refining () then errorlabstrm "check_no_pending_proofs" (str"Proof editing in progress" ++ (msg_proofs false) ++ fnl() ++ str"Use \"Abort All\" first or complete proof(s).") @@ -254,7 +254,7 @@ let set_end_tac tac = let start_proof na str sign concl ?init_tac ?(compute_guard=false) hook = let top_goal = mk_goal sign concl None in - let ts = { + let ts = { top_end_tac = None; top_init_tac = init_tac; top_compute_guard = compute_guard; @@ -269,7 +269,7 @@ let solve_nth k tac = let pft = get_pftreestate () in if not (List.mem (-1) (cursor_of_pftreestate pft)) then mutate (solve_nth_pftreestate k tac) - else + else error "cannot apply a tactic when we are descended behind a tactic-node" let by tac = mutate (solve_pftreestate tac) @@ -278,7 +278,7 @@ let instantiate_nth_evar_com n c = mutate (Evar_refiner.instantiate_pf_com n c) let traverse n = mutate (traverse n) - + (* [traverse_to path] Traverses the current proof to get to the location specified by @@ -296,7 +296,7 @@ let common_ancestor l1 l2 = | _, _ -> List.rev l1, List.length l2 in common_aux (List.rev l1) (List.rev l2) - + let rec traverse_up = function | 0 -> (function pf -> pf) | n -> (function pf -> Refiner.traverse 0 (traverse_up (n - 1) pf)) @@ -326,11 +326,11 @@ let make_focus n = focus_n := n let focus () = !focus_n let focused_goal () = let n = !focus_n in if n=0 then 1 else n -let reset_top_of_tree () = +let reset_top_of_tree () = mutate top_of_tree - -let reset_top_of_script () = - mutate (fun pts -> + +let reset_top_of_script () = + mutate (fun pts -> try up_until_matching_rule is_proof_instr pts with Not_found -> top_of_tree pts) diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 9a40ba319..8dcd8edc2 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -78,7 +78,7 @@ val get_undo : unit -> int option systematically apply at initialization time (e.g. to start the proof of mutually dependent theorems) *) -val start_proof : +val start_proof : identifier -> goal_kind -> named_context_val -> constr -> ?init_tac:tactic -> ?compute_guard:bool -> declaration_hook -> unit @@ -107,7 +107,7 @@ val suspend_proof : unit -> unit it fails if there is no current proof of if it is not completed; it also tells if the guardness condition has to be inferred. *) -val cook_proof : (Refiner.pftreestate -> unit) -> +val cook_proof : (Refiner.pftreestate -> unit) -> identifier * (Entries.definition_entry * bool * goal_kind * declaration_hook) (* To export completed proofs to xml *) diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml index 2e2f23065..b5f46d788 100644 --- a/proofs/proof_trees.ml +++ b/proofs/proof_trees.ml @@ -33,8 +33,8 @@ let is_bind = function (* Functions on goals *) -let mk_goal hyps cl extra = - { evar_hyps = hyps; evar_concl = cl; +let mk_goal hyps cl extra = + { evar_hyps = hyps; evar_concl = cl; evar_filter = List.map (fun _ -> true) (named_context_of_val hyps); evar_body = Evar_empty; evar_extra = extra } @@ -48,9 +48,9 @@ let ref_of_proof pf = let rule_of_proof pf = let (r,_) = ref_of_proof pf in r -let children_of_proof pf = +let children_of_proof pf = let (_,cl) = ref_of_proof pf in cl - + let goal_of_proof pf = pf.goal let subproof_of_proof pf = match pf.ref with @@ -74,7 +74,7 @@ let pf_lookup_name_as_renamed env ccl s = let pf_lookup_index_as_renamed env ccl n = Detyping.lookup_index_as_renamed env ccl n -(* Functions on rules (Proof mode) *) +(* Functions on rules (Proof mode) *) let is_dem_rule = function Decl_proof _ -> true @@ -85,9 +85,9 @@ let is_proof_instr = function | _ -> false let is_focussing_command = function - Decl_proof b -> b - | Nested (Proof_instr (b,_),_) -> b - | _ -> false + Decl_proof b -> b + | Nested (Proof_instr (b,_),_) -> b + | _ -> false (*********************************************************************) diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 8a466d8df..29417e8b6 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -48,11 +48,11 @@ type proof_tree = { and rule = | Prim of prim_rule - | Nested of compound_rule * proof_tree + | Nested of compound_rule * proof_tree | Decl_proof of bool | Daimon -and compound_rule= +and compound_rule= | Tactic of tactic_expr * bool | Proof_instr of bool*proof_instr (* the boolean is for focus restrictions *) @@ -92,7 +92,7 @@ and tactic_arg = glob_tactic_expr) Tacexpr.gen_tactic_arg -type ltac_call_kind = +type ltac_call_kind = | LtacNotationCall of string | LtacNameCall of ltac_constant | LtacAtomCall of glob_atomic_tactic_expr * atomic_tactic_expr option ref diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 9db87d22e..4a7cb2f93 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -32,7 +32,7 @@ type prim_rule = | FixRule of identifier * int * (identifier * int * constr) list * int | Cofix of identifier * (identifier * constr) list * int | Refine of constr - | Convert_concl of types * cast_kind + | Convert_concl of types * cast_kind | Convert_hyp of named_declaration | Thin of identifier list | ThinBody of identifier list @@ -58,7 +58,7 @@ type prim_rule = lc : [Set of evars occurring in the type of evar] } }; ... - number of last evar, + number of last evar, it = { evar_concl = [the type of evar] evar_hyps = [the context of the evar] evar_body = [the body of the Evar if any] @@ -69,11 +69,11 @@ type prim_rule = \end{verbatim} *) -(*s Proof trees. - [ref] = [None] if the goal has still to be proved, +(*s Proof trees. + [ref] = [None] if the goal has still to be proved, and [Some (r,l)] if the rule [r] was applied to the goal - and gave [l] as subproofs to be completed. - if [ref = (Some(Nested(Tactic t,p),l))] then [p] is the proof + and gave [l] as subproofs to be completed. + if [ref = (Some(Nested(Tactic t,p),l))] then [p] is the proof that the goal can be proven if the goals in [l] are solved. *) type proof_tree = { open_subgoals : int; @@ -82,11 +82,11 @@ type proof_tree = { and rule = | Prim of prim_rule - | Nested of compound_rule * proof_tree + | Nested of compound_rule * proof_tree | Decl_proof of bool | Daimon -and compound_rule= +and compound_rule= (* the boolean of Tactic tells if the default tactic is used *) | Tactic of tactic_expr * bool | Proof_instr of bool * proof_instr @@ -127,7 +127,7 @@ and tactic_arg = glob_tactic_expr) Tacexpr.gen_tactic_arg -type ltac_call_kind = +type ltac_call_kind = | LtacNotationCall of string | LtacNameCall of ltac_constant | LtacAtomCall of glob_atomic_tactic_expr * atomic_tactic_expr option ref diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 8efc26631..880efc2d0 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -40,14 +40,14 @@ let set_strategy_one ref l = let cb = Global.lookup_constant sp in if cb.const_body <> None & cb.const_opaque then errorlabstrm "set_transparent_const" - (str "Cannot make" ++ spc () ++ + (str "Cannot make" ++ spc () ++ Nametab.pr_global_env Idset.empty (ConstRef sp) ++ spc () ++ str "transparent because it was declared opaque."); Csymtable.set_transparent_const sp | _ -> () let cache_strategy (_,str) = - List.iter + List.iter (fun (lev,ql) -> List.iter (fun q -> set_strategy_one q lev) ql) str @@ -62,7 +62,7 @@ let subst_strategy (_,subs,(local,obj)) = let map_strategy f l = let l' = List.fold_right - (fun (lev,ql) str -> + (fun (lev,ql) str -> let ql' = List.fold_right (fun q ql -> match f q with @@ -77,12 +77,12 @@ let export_strategy (local,obj) = EvalVarRef _ -> None | EvalConstRef _ as q -> Some q) obj -let classify_strategy (local,_ as obj) = +let classify_strategy (local,_ as obj) = if local then Dispose else Substitute obj let disch_ref ref = match ref with - EvalConstRef c -> + EvalConstRef c -> let c' = Lib.discharge_con c in if c==c' then Some ref else Some (EvalConstRef c') | _ -> Some ref @@ -104,7 +104,7 @@ let (inStrategy,outStrategy) = let set_strategy local str = Lib.add_anonymous_leaf (inStrategy (local,str)) -let _ = +let _ = Summary.declare_summary "Transparent constants and variables" { Summary.freeze_function = Conv_oracle.freeze; Summary.unfreeze_function = Conv_oracle.unfreeze; @@ -139,13 +139,13 @@ let make_flag f = f.rConst red in red -let is_reference c = +let is_reference c = try let _ref = global_of_constr c in true with _ -> false let red_expr_tab = ref Stringmap.empty let declare_red_expr s f = - try + try let _ = Stringmap.find s !red_expr_tab in error ("There is already a reduction expression of name "^s) with Not_found -> @@ -159,8 +159,8 @@ let out_with_occurrences ((b,l),c) = ((b,List.map out_arg l), c) let reduction_of_red_expr = function - | Red internal -> - if internal then (try_red_product,DEFAULTcast) + | Red internal -> + if internal then (try_red_product,DEFAULTcast) else (red_product,DEFAULTcast) | Hnf -> (hnf_constr,DEFAULTcast) | Simpl (Some (_,c as lp)) -> diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 8b3789c3b..c66e9c84b 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -49,7 +49,7 @@ let descend n p = | None -> error "It is a leaf." | Some(r,pfl) -> if List.length pfl >= n then - (match list_chop (n-1) pfl with + (match list_chop (n-1) pfl with | left,(wanted::right) -> (wanted, (fun pfl' -> @@ -58,11 +58,11 @@ let descend n p = let pf' = List.hd pfl' in let spfl = left@(pf'::right) in let newstatus = and_status (List.map pf_status spfl) in - { p with + { p with open_subgoals = newstatus; ref = Some(r,spfl) })) | _ -> assert false) - else + else error "Too few subproofs" @@ -72,28 +72,28 @@ let descend n p = (vk [ p_(l1+...+l(k-1)+1) ... p_(l1+...lk) ]) ] *) -let rec mapshape nl (fl : (proof_tree list -> proof_tree) list) +let rec mapshape nl (fl : (proof_tree list -> proof_tree) list) (l : proof_tree list) = match nl with | [] -> [] | h::t -> - let m,l = list_chop h l in + let m,l = list_chop h l in (List.hd fl m) :: (mapshape t (List.tl fl) l) (* [frontier : proof_tree -> goal list * validation] given a proof [p], [frontier p] gives [(l,v)] where [l] is the list of goals - to be solved to complete the proof, and [v] is the corresponding + to be solved to complete the proof, and [v] is the corresponding validation *) - + let rec frontier p = match p.ref with - | None -> + | None -> ([p.goal], - (fun lp' -> + (fun lp' -> let p' = List.hd lp' in - if Evd.eq_evar_info p'.goal p.goal then + if Evd.eq_evar_info p'.goal p.goal then p' - else + else errorlabstrm "Refiner.frontier" (str"frontier was handed back a ill-formed proof."))) | Some(r,pfl) -> @@ -115,14 +115,14 @@ let set_solve_hook = (:=) solve_hook let rec frontier_map_rec f n p = if n < 1 || n > p.open_subgoals then p else match p.ref with - | None -> + | None -> let p' = f p in if Evd.eq_evar_info p'.goal p.goal then begin !solve_hook p'; p' end - else + else errorlabstrm "Refiner.frontier_map" (str"frontier_map was handed back a ill-formed proof.") | Some(r,pfl) -> @@ -139,20 +139,20 @@ let frontier_map f n p = let nmax = p.open_subgoals in let n = if n < 0 then nmax + n + 1 else n in if n < 1 || n > nmax then - errorlabstrm "Refiner.frontier_map" (str "No such subgoal"); + errorlabstrm "Refiner.frontier_map" (str "No such subgoal"); frontier_map_rec f n p let rec frontier_mapi_rec f i p = if p.open_subgoals = 0 then p else match p.ref with - | None -> + | None -> let p' = f i p in if Evd.eq_evar_info p'.goal p.goal then begin !solve_hook p'; p' end - else + else errorlabstrm "Refiner.frontier_mapi" (str"frontier_mapi was handed back a ill-formed proof.") | Some(r,pfl) -> @@ -161,7 +161,7 @@ let rec frontier_mapi_rec f i p = (fun (n,acc) p -> (n+p.open_subgoals,frontier_mapi_rec f n p::acc)) (i,[]) pfl in let pfl' = List.rev rpfl' in - { p with + { p with open_subgoals = and_status (List.map pf_status pfl'); ref = Some(r,pfl')} @@ -176,7 +176,7 @@ let rec nb_unsolved_goals pf = pf.open_subgoals (* leaf g is the canonical incomplete proof of a goal g *) -let leaf g = +let leaf g = { open_subgoals = 1; goal = g; ref = None } @@ -197,20 +197,20 @@ let abstract_operation syntax semantics gls = ref = Some(Nested(syntax,hidden_proof),spfl)}) let abstract_tactic_expr ?(dflt=false) te tacfun gls = - abstract_operation (Tactic(te,dflt)) tacfun gls + abstract_operation (Tactic(te,dflt)) tacfun gls let abstract_tactic ?(dflt=false) te = !abstract_tactic_box := Some te; abstract_tactic_expr ~dflt (Tacexpr.TacAtom (dummy_loc,te)) -let abstract_extended_tactic ?(dflt=false) s args = +let abstract_extended_tactic ?(dflt=false) s args = abstract_tactic ~dflt (Tacexpr.TacExtend (dummy_loc, s, args)) let refiner = function | Prim pr as r -> let prim_fun = prim_refiner pr in (fun goal_sigma -> - let (sgl,sigma') = prim_fun goal_sigma.sigma goal_sigma.it in + let (sgl,sigma') = prim_fun goal_sigma.sigma goal_sigma.it in ({it=sgl; sigma = sigma'}, (fun spfl -> assert (check_subproof_connection sgl spfl); @@ -219,15 +219,15 @@ let refiner = function ref = Some(r,spfl) }))) - | Nested (_,_) | Decl_proof _ -> + | Nested (_,_) | Decl_proof _ -> failwith "Refiner: should not occur" - + (* Daimon is a canonical unfinished proof *) - | Daimon -> - fun gls -> - ({it=[];sigma=gls.sigma}, - fun spfl -> + | Daimon -> + fun gls -> + ({it=[];sigma=gls.sigma}, + fun spfl -> assert (spfl=[]); { open_subgoals = 0; goal = gls.it; @@ -250,10 +250,10 @@ let norm_evar_proof sigma pf = Their proof should be completed in order to complete the initial proof *) let extract_open_proof sigma pf = - let next_meta = + let next_meta = let meta_cnt = ref 0 in let rec f () = - incr meta_cnt; + incr meta_cnt; if Evd.mem sigma (existential_of_int !meta_cnt) then f () else !meta_cnt in f @@ -261,14 +261,14 @@ let extract_open_proof sigma pf = let open_obligations = ref [] in let rec proof_extractor vl = function | {ref=Some(Prim _,_)} as pf -> prim_extractor proof_extractor vl pf - + | {ref=Some(Nested(_,hidden_proof),spfl)} -> let sgl,v = frontier hidden_proof in let flat_proof = v spfl in proof_extractor vl flat_proof - + | {ref=Some(Decl_proof _,[pf])} -> (proof_extractor vl) pf - + | {ref=(None|Some(Daimon,[]));goal=goal} -> let visible_rels = map_succeed @@ -287,13 +287,13 @@ let extract_open_proof sigma pf = let inst = List.filter (fun (_,(_,b,_)) -> b = None) sorted_env in let meta = next_meta () in open_obligations := (meta,abs_concl):: !open_obligations; - applist (mkMeta meta, List.map (fun (n,_) -> mkRel n) inst) - + applist (mkMeta meta, List.map (fun (n,_) -> mkRel n) inst) + | _ -> anomaly "Bug: a case has been forgotten in proof_extractor" in let pfterm = proof_extractor [] pf in (pfterm, List.rev !open_obligations) - + (*********************) (* Tacticals *) (*********************) @@ -301,7 +301,7 @@ let extract_open_proof sigma pf = (* unTAC : tactic -> goal sigma -> proof sigma *) let unTAC tac g = - let (gl_sigma,v) = tac g in + let (gl_sigma,v) = tac g in { it = v (List.map leaf gl_sigma.it); sigma = gl_sigma.sigma } let unpackage glsig = (ref (glsig.sigma)),glsig.it @@ -309,8 +309,8 @@ let unpackage glsig = (ref (glsig.sigma)),glsig.it let repackage r v = {it=v;sigma = !r} let apply_sig_tac r tac g = - check_for_interrupt (); (* Breakpoint *) - let glsigma,v = tac (repackage r g) in + check_for_interrupt (); (* Breakpoint *) + let glsigma,v = tac (repackage r g) in r := glsigma.sigma; (glsigma.it,v) @@ -328,7 +328,7 @@ let tclNORMEVAR = norm_evar_tac let tclIDTAC gls = (goal_goal_list gls, idtac_valid) (* the message printing identity tactic *) -let tclIDTAC_MESSAGE s gls = +let tclIDTAC_MESSAGE s gls = msg (hov 0 s); tclIDTAC gls (* General failure tactic *) @@ -356,7 +356,7 @@ let thens3parts_tac tacfi tac tacli (sigr,gs,p) = if ng<nf+nl then errorlabstrm "Refiner.thensn_tac" (str "Not enough subgoals."); let gll,pl = List.split - (list_map_i (fun i -> + (list_map_i (fun i -> apply_sig_tac sigr (if i<nf then tacfi.(i) else if i>=ng-nl then tacli.(nl-ng+i) else tac)) 0 gs) in (sigr, List.flatten gll, @@ -390,7 +390,7 @@ let theni_tac i tac ((_,gl,_) as subgoals) = thensf_tac (Array.init k (fun i -> if i+1 = k then tac else tclIDTAC)) tclIDTAC subgoals - else non_existent_goal k + else non_existent_goal k (* [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls] applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to @@ -448,17 +448,17 @@ let rec tclTHENLIST = function | t1::tacl -> tclTHEN t1 (tclTHENLIST tacl) (* [tclMAP f [x1..xn]] builds [(f x1);(f x2);...(f xn)] *) -let tclMAP tacfun l = +let tclMAP tacfun l = List.fold_right (fun x -> (tclTHEN (tacfun x))) l tclIDTAC (* various progress criterions *) -let same_goal gl subgoal = +let same_goal gl subgoal = eq_constr (conclusion subgoal) (conclusion gl) && eq_named_context_val (hypotheses subgoal) (hypotheses gl) let weak_progress gls ptree = - (List.length gls.it <> 1) || + (List.length gls.it <> 1) || (not (same_goal (List.hd gls.it) ptree.it)) let progress gls ptree = @@ -473,7 +473,7 @@ let tclPROGRESS tac ptree = if progress (fst rslt) ptree then rslt else errorlabstrm "Refiner.PROGRESS" (str"Failed to progress.") -(* weak_PROGRESS tac ptree applies tac to the goal ptree and fails +(* weak_PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves the goal unchanged, possibly modifying sigma *) let tclWEAK_PROGRESS tac ptree = let rslt = tac ptree in @@ -487,14 +487,14 @@ let tclNOTSAMEGOAL (tac : tactic) goal = let rslt = tac goal in let gls = (fst rslt).it in if List.exists (same_goal goal.it) gls - then errorlabstrm "Refiner.tclNOTSAMEGOAL" + then errorlabstrm "Refiner.tclNOTSAMEGOAL" (str"Tactic generated a subgoal identical to the original goal.") else rslt let catch_failerror e = if catchable_exception e then check_for_interrupt () else match e with - | FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_)) + | FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_)) | Stdpp.Exc_located(_, LtacLocated (_,FailError (0,_))) -> check_for_interrupt () | FailError (lvl,s) -> raise (FailError (lvl - 1, s)) @@ -507,18 +507,18 @@ let catch_failerror e = (* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *) let tclORELSE0 t1 t2 g = - try + try t1 g with (* Breakpoint *) | e -> catch_failerror e; t2 g -(* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress, +(* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress, then applies t2 *) let tclORELSE t1 t2 = tclORELSE0 (tclPROGRESS t1) t2 (* applies t1;t2then if t1 succeeds or t2else if t1 fails t2* are called in terminal position (unless t1 produces more than - 1 subgoal!) *) + 1 subgoal!) *) let tclORELSE_THEN t1 t2then t2else gls = match try Some(tclPROGRESS t1 gls) @@ -526,7 +526,7 @@ let tclORELSE_THEN t1 t2then t2else gls = with | None -> t2else gls | Some (sgl,v) -> - let (sigr,gl) = unpackage sgl in + let (sigr,gl) = unpackage sgl in finish_tac (then_tac t2then (sigr,gl,v)) (* TRY f tries to apply f, and if it fails, leave the goal unchanged *) @@ -546,16 +546,16 @@ let ite_gen tcal tac_if continue tac_else gl= let result=tac_if gl in success:=true;result in let tac_else0 e gl= - if !success then - raise e - else + if !success then + raise e + else tac_else gl in - try + try tcal tac_if0 continue gl with (* Breakpoint *) | e -> catch_failerror e; tac_else0 e gl -(* Try the first tactic and, if it succeeds, continue with +(* Try the first tactic and, if it succeeds, continue with the second one, and if it fails, use the third one *) let tclIFTHENELSE=ite_gen tclTHEN @@ -566,7 +566,7 @@ let tclIFTHENSELSE=ite_gen tclTHENS let tclIFTHENSVELSE=ite_gen tclTHENSV -let tclIFTHENTRYELSEMUST tac1 tac2 gl = +let tclIFTHENTRYELSEMUST tac1 tac2 gl = tclIFTHENELSE tac1 (tclTRY tac2) tac2 gl (* Fails if a tactic did not solve the goal *) @@ -575,17 +575,17 @@ let tclCOMPLETE tac = tclTHEN tac (tclFAIL_s "Proof is not complete.") (* Try the first thats solves the current goal *) let tclSOLVE tacl = tclFIRST (List.map tclCOMPLETE tacl) - + (* Iteration tacticals *) -let tclDO n t = - let rec dorec k = +let tclDO n t = + let rec dorec k = if k < 0 then errorlabstrm "Refiner.tclDO" (str"Wrong argument : Do needs a positive integer."); if k = 0 then tclIDTAC else if k = 1 then t else (tclTHEN t (dorec (k-1))) - in - dorec n + in + dorec n (* Beware: call by need of CAML, g is needed *) @@ -612,52 +612,52 @@ let tclIDTAC_list gls = (gls, fun x -> x) (* first_goal : goal list sigma -> goal sigma *) -let first_goal gls = - let gl = gls.it and sig_0 = gls.sigma in - if gl = [] then error "first_goal"; +let first_goal gls = + let gl = gls.it and sig_0 = gls.sigma in + if gl = [] then error "first_goal"; { it = List.hd gl; sigma = sig_0 } (* goal_goal_list : goal sigma -> goal list sigma *) -let goal_goal_list gls = +let goal_goal_list gls = let gl = gls.it and sig_0 = gls.sigma in { it = [gl]; sigma = sig_0 } (* tactic -> tactic_list : Apply a tactic to the first goal in the list *) -let apply_tac_list tac glls = +let apply_tac_list tac glls = let (sigr,lg) = unpackage glls in match lg with | (g1::rest) -> let (gl,p) = apply_sig_tac sigr tac g1 in - let n = List.length gl in - (repackage sigr (gl@rest), + let n = List.length gl in + (repackage sigr (gl@rest), fun pfl -> let (pfg,pfrest) = list_chop n pfl in (p pfg)::pfrest) | _ -> error "apply_tac_list" - -let then_tactic_list tacl1 tacl2 glls = + +let then_tactic_list tacl1 tacl2 glls = let (glls1,pl1) = tacl1 glls in let (glls2,pl2) = tacl2 glls1 in (glls2, compose pl1 pl2) (* Transform a tactic_list into a tactic *) -let tactic_list_tactic tac gls = +let tactic_list_tactic tac gls = let (glres,vl) = tac (goal_goal_list gls) in (glres, compose idtac_valid vl) -(* The type of proof-trees state and a few utilities +(* The type of proof-trees state and a few utilities A proof-tree state is built from a proof-tree, a set of global constraints, and a stack which allows to navigate inside the proof-tree remembering how to rebuild the global proof-tree possibly after modification of one of the focused children proof-tree. - The number in the stack corresponds to + The number in the stack corresponds to either the selected subtree and the validation is a function from a proof-tree list consisting only of one proof-tree to the global - proof-tree + proof-tree or -1 when the move is done behind a registered tactic in which - case the validation corresponds to a constant function giving back + case the validation corresponds to a constant function giving back the original proof-tree. *) type pftreestate = { @@ -666,11 +666,11 @@ type pftreestate = { tstack : (int * validation) list } let proof_of_pftreestate pts = pts.tpf -let is_top_pftreestate pts = pts.tstack = [] +let is_top_pftreestate pts = pts.tstack = [] let cursor_of_pftreestate pts = List.map fst pts.tstack let evc_of_pftreestate pts = pts.tpfsigma -let top_goal_of_pftreestate pts = +let top_goal_of_pftreestate pts = { it = goal_of_proof pts.tpf; sigma = pts.tpfsigma } let nth_goal_of_pftreestate n pts = @@ -678,7 +678,7 @@ let nth_goal_of_pftreestate n pts = try {it = List.nth goals (n-1); sigma = pts.tpfsigma } with Invalid_argument _ | Failure _ -> non_existent_goal n -let traverse n pts = match n with +let traverse n pts = match n with | 0 -> (* go to the parent *) (match pts.tstack with | [] -> error "traverse: no ancestors" @@ -691,13 +691,13 @@ let traverse n pts = match n with | -1 -> (* go to the hidden tactic-proof, if any, otherwise fail *) (match pts.tpf.ref with | Some (Nested (_,spf),_) -> - let v = (fun pfl -> pts.tpf) in + let v = (fun pfl -> pts.tpf) in { tpf = spf; tstack = (-1,v)::pts.tstack; tpfsigma = pts.tpfsigma } | _ -> error "traverse: not a tactic-node") | n -> (* when n>0, go to the nth child *) - let (npf,v) = descend n pts.tpf in + let (npf,v) = descend n pts.tpf in { tpf = npf; tpfsigma = pts.tpfsigma; tstack = (n,v):: pts.tstack } @@ -723,9 +723,9 @@ let map_pftreestate f pts = (* solve the nth subgoal with tactic tac *) let solve_nth_pftreestate n tac = - map_pftreestate + map_pftreestate (fun sigr pt -> frontier_map (app_tac sigr tac) n pt) - + let solve_pftreestate = solve_nth_pftreestate 1 (* This function implements a poor man's undo at the current goal. @@ -771,78 +771,78 @@ let extract_pftreestate pts = (* Focus on the first leaf proof in a proof-tree state *) let rec first_unproven pts = - let pf = (proof_of_pftreestate pts) in + let pf = (proof_of_pftreestate pts) in if is_complete_proof pf then errorlabstrm "first_unproven" (str"No unproven subgoals"); if is_leaf_proof pf then pts else let childnum = - list_try_find_i - (fun n pf -> + list_try_find_i + (fun n pf -> if not(is_complete_proof pf) then n else failwith "caught") 1 (children_of_proof pf) - in + in first_unproven (traverse childnum pts) (* Focus on the last leaf proof in a proof-tree state *) let rec last_unproven pts = - let pf = proof_of_pftreestate pts in + let pf = proof_of_pftreestate pts in if is_complete_proof pf then errorlabstrm "last_unproven" (str"No unproven subgoals"); if is_leaf_proof pf then pts - else + else let children = (children_of_proof pf) in let nchilds = List.length children in let childnum = - list_try_find_i + list_try_find_i (fun n pf -> if not(is_complete_proof pf) then n else failwith "caught") 1 (List.rev children) - in + in last_unproven (traverse (nchilds-childnum+1) pts) - + let rec nth_unproven n pts = - let pf = proof_of_pftreestate pts in + let pf = proof_of_pftreestate pts in if is_complete_proof pf then errorlabstrm "nth_unproven" (str"No unproven subgoals"); if is_leaf_proof pf then - if n = 1 then - pts + if n = 1 then + pts else errorlabstrm "nth_unproven" (str"Not enough unproven subgoals") - else + else let children = children_of_proof pf in let rec process i k = function - | [] -> + | [] -> errorlabstrm "nth_unproven" (str"Not enough unproven subgoals") - | pf1::rest -> - let k1 = nb_unsolved_goals pf1 in - if k1 < k then + | pf1::rest -> + let k1 = nb_unsolved_goals pf1 in + if k1 < k then process (i+1) (k-k1) rest - else + else nth_unproven k (traverse i pts) - in + in process 1 n children let rec node_prev_unproven loc pts = - let pf = proof_of_pftreestate pts in + let pf = proof_of_pftreestate pts in match cursor_of_pftreestate pts with | [] -> last_unproven pts | n::l -> if is_complete_proof pf or loc = 1 then node_prev_unproven n (traverse 0 pts) - else + else let child = List.nth (children_of_proof pf) (loc - 2) in if is_complete_proof child then node_prev_unproven (loc - 1) pts - else + else first_unproven (traverse (loc - 1) pts) let rec node_next_unproven loc pts = - let pf = proof_of_pftreestate pts in + let pf = proof_of_pftreestate pts in match cursor_of_pftreestate pts with | [] -> first_unproven pts | n::l -> @@ -851,35 +851,35 @@ let rec node_next_unproven loc pts = node_next_unproven n (traverse 0 pts) else if is_complete_proof (List.nth (children_of_proof pf) loc) then node_next_unproven (loc + 1) pts - else + else last_unproven(traverse (loc + 1) pts) let next_unproven pts = - let pf = proof_of_pftreestate pts in + let pf = proof_of_pftreestate pts in if is_leaf_proof pf then match cursor_of_pftreestate pts with | [] -> error "next_unproven" | n::_ -> node_next_unproven n (traverse 0 pts) - else + else node_next_unproven (List.length (children_of_proof pf)) pts let prev_unproven pts = - let pf = proof_of_pftreestate pts in + let pf = proof_of_pftreestate pts in if is_leaf_proof pf then match cursor_of_pftreestate pts with | [] -> error "prev_unproven" | n::_ -> node_prev_unproven n (traverse 0 pts) - else + else node_prev_unproven 1 pts -let rec top_of_tree pts = +let rec top_of_tree pts = if is_top_pftreestate pts then pts else top_of_tree(traverse 0 pts) (* FIXME: cette fonction n'est (as of October 2007) appelée nulle part *) let change_rule f pts = let mark_top _ pt = match pt.ref with - Some (oldrule,l) -> + Some (oldrule,l) -> {pt with ref=Some (f oldrule,l)} | _ -> invalid_arg "change_rule" in map_pftreestate mark_top pts @@ -889,21 +889,21 @@ let match_rule p pts = Some (r,_) -> p r | None -> false -let rec up_until_matching_rule p pts = - if is_top_pftreestate pts then +let rec up_until_matching_rule p pts = + if is_top_pftreestate pts then raise Not_found else let one_up = traverse 0 pts in - if match_rule p one_up then + if match_rule p one_up then pts else up_until_matching_rule p one_up -let rec up_to_matching_rule p pts = - if match_rule p pts then +let rec up_to_matching_rule p pts = + if match_rule p pts then pts else - if is_top_pftreestate pts then + if is_top_pftreestate pts then raise Not_found else let one_up = traverse 0 pts in @@ -917,14 +917,14 @@ let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma} let pp_info = ref (fun _ _ _ -> assert false) let set_info_printer f = pp_info := f -let tclINFO (tac : tactic) gls = - let (sgl,v) as res = tac gls in - begin try +let tclINFO (tac : tactic) gls = + let (sgl,v) as res = tac gls in + begin try let pf = v (List.map leaf (sig_it sgl)) in let sign = named_context_of_val (sig_it gls).evar_hyps in msgnl (hov 0 (str" == " ++ !pp_info (project gls) sign pf)) - with e when catchable_exception e -> + with e when catchable_exception e -> msgnl (hov 0 (str "Info failed to apply validation")) end; res @@ -935,7 +935,7 @@ let set_proof_printer f = pp_proof := f let print_pftreestate {tpf = pf; tpfsigma = sigma; tstack = stack } = (if stack = [] then str "Rooted proof tree is:" - else (str "Proof tree at occurrence [" ++ + else (str "Proof tree at occurrence [" ++ prlist_with_sep (fun () -> str ";") (fun (n,_) -> int n) (List.rev stack) ++ str "] is:")) ++ fnl() ++ !pp_proof sigma (Global.named_context()) pf ++ diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 9a587a965..ff902d880 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -159,14 +159,14 @@ val tclNOTSAMEGOAL : tactic -> tactic val tclINFO : tactic -> tactic (* [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then, - if it succeeds, applies [tac2] to the resulting subgoals, + if it succeeds, applies [tac2] to the resulting subgoals, and if not applies [tac3] to the initial goal [gls] *) val tclIFTHENELSE : tactic -> tactic -> tactic -> tactic val tclIFTHENSELSE : tactic -> tactic list -> tactic ->tactic val tclIFTHENSVELSE : tactic -> tactic array -> tactic ->tactic (* [tclIFTHENTRYELSEMUST tac1 tac2 gls] applies [tac1] then [tac2]. If [tac1] - has been successful, then [tac2] may fail. Otherwise, [tac2] must succeed. + has been successful, then [tac2] may fail. Otherwise, [tac2] must succeed. Equivalent to [(tac1;try tac2)||tac2] *) val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic @@ -199,7 +199,7 @@ val top_goal_of_pftreestate : pftreestate -> goal sigma val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma val traverse : int -> pftreestate -> pftreestate -val map_pftreestate : +val map_pftreestate : (evar_map ref -> proof_tree -> proof_tree) -> pftreestate -> pftreestate val solve_nth_pftreestate : int -> tactic -> pftreestate -> pftreestate val solve_pftreestate : tactic -> pftreestate -> pftreestate @@ -221,12 +221,12 @@ val next_unproven : pftreestate -> pftreestate val prev_unproven : pftreestate -> pftreestate val top_of_tree : pftreestate -> pftreestate val match_rule : (rule -> bool) -> pftreestate -> bool -val up_until_matching_rule : (rule -> bool) -> +val up_until_matching_rule : (rule -> bool) -> pftreestate -> pftreestate -val up_to_matching_rule : (rule -> bool) -> +val up_to_matching_rule : (rule -> bool) -> pftreestate -> pftreestate val change_rule : (rule -> rule) -> pftreestate -> pftreestate -val change_constraints_pftreestate +val change_constraints_pftreestate : evar_map -> pftreestate -> pftreestate diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index f53327249..ba3c27e63 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -51,12 +51,12 @@ let make_red_flag = if red.rConst <> [] & not red.rDelta then error "Cannot set both constants to unfold and constants not to unfold"; - add_flag + add_flag { red with rConst = list_union red.rConst l; rDelta = true } lf in add_flag - {rBeta = false; rIota = false; rZeta = false; rDelta = false; rConst = []} + {rBeta = false; rIota = false; rZeta = false; rDelta = false; rConst = []} type 'a raw_hyp_location = 'a with_occurrences * Termops.hyp_location_flag @@ -85,7 +85,7 @@ type inversion_kind = | FullInversionClear type ('c,'id) inversion_strength = - | NonDepInversion of + | NonDepInversion of inversion_kind * 'id list * intro_pattern_expr located option | DepInversion of inversion_kind * 'c option * intro_pattern_expr located option @@ -115,12 +115,12 @@ let goal_location_of = function | _ -> error "Not a simple \"in\" clause (one hypothesis or the conclusion)" -type ('constr,'id) induction_clause = - ('constr with_bindings induction_arg list * 'constr with_bindings option * +type ('constr,'id) induction_clause = + ('constr with_bindings induction_arg list * 'constr with_bindings option * (intro_pattern_expr located option * intro_pattern_expr located option) * 'id gclause option) -type multi = +type multi = | Precisely of int | UpTo of int | RepeatStar @@ -150,15 +150,15 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = | TacExact of 'constr | TacExactNoCheck of 'constr | TacVmCastNoCheck of 'constr - | TacApply of advanced_flag * evars_flag * 'constr with_bindings list * + | TacApply of advanced_flag * evars_flag * 'constr with_bindings list * ('id * intro_pattern_expr located option) option - | TacElim of evars_flag * 'constr with_bindings * + | TacElim of evars_flag * 'constr with_bindings * 'constr with_bindings option | TacElimType of 'constr | TacCase of evars_flag * 'constr with_bindings | TacCaseType of 'constr | TacFix of identifier option * int - | TacMutualFix of hidden_flag * identifier * int * (identifier * int * + | TacMutualFix of hidden_flag * identifier * int * (identifier * int * 'constr) list | TacCofix of identifier option | TacMutualCofix of hidden_flag * identifier * (identifier * 'constr) list @@ -211,10 +211,10 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = | TacTransitivity of 'constr option (* Equality and inversion *) - | TacRewrite of + | TacRewrite of evars_flag * (bool * multi * 'constr with_bindings) list * 'id gclause * 'tac option | TacInversion of ('constr,'id) inversion_strength * quantified_hypothesis - + (* For ML extensions *) | TacExtend of loc * string * 'constr generic_argument list @@ -225,11 +225,11 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr = | TacAtom of loc * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr - | TacThen of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * + | TacThen of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr array * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr array - | TacThens of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * + | TacThens of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list | TacFirst of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list | TacComplete of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr @@ -263,7 +263,7 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg = | Integer of int | TacCall of loc * 'ref * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg list - | TacExternal of loc * string * string * + | TacExternal of loc * string * string * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg list | TacFreshId of string or_var list | Tacexp of 'tac diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 40917b085..0faba52ea 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -55,10 +55,10 @@ let pf_nth_hyp_id gls n = let (id,c,t) = List.nth (pf_hyps gls) (n-1) in id let pf_last_hyp gl = List.hd (pf_hyps gl) -let pf_get_hyp gls id = - try +let pf_get_hyp gls id = + try Sign.lookup_named id (pf_hyps gls) - with Not_found -> + with Not_found -> error ("No such hypothesis: " ^ (string_of_id id)) let pf_get_hyp_typ gls id = @@ -67,7 +67,7 @@ let pf_get_hyp_typ gls id = let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls) -let pf_get_new_id id gls = +let pf_get_new_id id gls = next_ident_away id (pf_ids_of_hyps gls) let pf_get_new_ids ids gls = @@ -77,19 +77,19 @@ let pf_get_new_ids ids gls = ids [] let pf_interp_constr gls c = - let evc = project gls in + let evc = project gls in Constrintern.interp_constr evc (pf_env gls) c let pf_interp_type gls c = - let evc = project gls in + let evc = project gls in Constrintern.interp_type evc (pf_env gls) c let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id let pf_parse_const gls = compose (pf_global gls) id_of_string -let pf_reduction_of_red_expr gls re c = - (fst (reduction_of_red_expr re)) (pf_env gls) (project gls) c +let pf_reduction_of_red_expr gls re c = + (fst (reduction_of_red_expr re)) (pf_env gls) (project gls) c let pf_apply f gls = f (pf_env gls) (project gls) let pf_reduce = pf_apply @@ -113,7 +113,7 @@ let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind let pf_hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_get_type_of gls) -let pf_check_type gls c1 c2 = +let pf_check_type gls c1 c2 = ignore (pf_type_of gls (mkCast (c1, DEFAULTcast, c2))) let pf_is_matching = pf_apply Matching.is_matching_conv @@ -179,16 +179,16 @@ let refiner = refiner let introduction_no_check id = refiner (Prim (Intro id)) -let internal_cut_no_check replace id t gl = +let internal_cut_no_check replace id t gl = refiner (Prim (Cut (true,replace,id,t))) gl -let internal_cut_rev_no_check replace id t gl = +let internal_cut_rev_no_check replace id t gl = refiner (Prim (Cut (false,replace,id,t))) gl -let refine_no_check c gl = +let refine_no_check c gl = refiner (Prim (Refine c)) gl -let convert_concl_no_check c sty gl = +let convert_concl_no_check c sty gl = refiner (Prim (Convert_concl (c,sty))) gl let convert_hyp_no_check d gl = @@ -202,16 +202,16 @@ let thin_no_check ids gl = let thin_body_no_check ids gl = if ids = [] then tclIDTAC gl else refiner (Prim (ThinBody ids)) gl -let move_hyp_no_check with_dep id1 id2 gl = +let move_hyp_no_check with_dep id1 id2 gl = refiner (Prim (Move (with_dep,id1,id2))) gl let order_hyps idl gl = refiner (Prim (Order idl)) gl -let rec rename_hyp_no_check l gl = match l with - | [] -> tclIDTAC gl - | (id1,id2)::l -> - tclTHEN (refiner (Prim (Rename (id1,id2)))) +let rec rename_hyp_no_check l gl = match l with + | [] -> tclIDTAC gl + | (id1,id2)::l -> + tclTHEN (refiner (Prim (Rename (id1,id2)))) (rename_hyp_no_check l) gl let mutual_fix f n others j gl = @@ -219,10 +219,10 @@ let mutual_fix f n others j gl = let mutual_cofix f others j gl = with_check (refiner (Prim (Cofix (f,others,j)))) gl - + (* Versions with consistency checks *) -let introduction id = with_check (introduction_no_check id) +let introduction id = with_check (introduction_no_check id) let internal_cut b d t = with_check (internal_cut_no_check b d t) let internal_cut_rev b d t = with_check (internal_cut_rev_no_check b d t) let refine c = with_check (refine_no_check c) @@ -230,7 +230,7 @@ let convert_concl d sty = with_check (convert_concl_no_check d sty) let convert_hyp d = with_check (convert_hyp_no_check d) let thin c = with_check (thin_no_check c) let thin_body c = with_check (thin_body_no_check c) -let move_hyp b id id' = with_check (move_hyp_no_check b id id') +let move_hyp b id id' = with_check (move_hyp_no_check b id id') let rename_hyp l = with_check (rename_hyp_no_check l) (* Pretty-printers *) @@ -249,4 +249,4 @@ let pr_gls gls = let pr_glls glls = hov 0 (pr_evar_defs (sig_sig glls) ++ fnl () ++ prlist_with_sep pr_fnl db_pr_goal (sig_it glls)) - + diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 581933c83..a808ca419 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -67,12 +67,12 @@ val pf_reduction_of_red_expr : goal sigma -> red_expr -> constr -> constr val pf_apply : (env -> evar_map -> 'a) -> goal sigma -> 'a -val pf_reduce : +val pf_reduce : (env -> evar_map -> constr -> constr) -> goal sigma -> constr -> constr val pf_whd_betadeltaiota : goal sigma -> constr -> constr -val pf_whd_betadeltaiota_stack : goal sigma -> constr -> constr * constr list +val pf_whd_betadeltaiota_stack : goal sigma -> constr -> constr * constr list val pf_hnf_constr : goal sigma -> constr -> constr val pf_red_product : goal sigma -> constr -> constr val pf_nf : goal sigma -> constr -> constr diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index 6674d04ea..ea8ab5b62 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -68,11 +68,11 @@ let skip = ref 0 (* Prints the run counter *) let run ini = - if not ini then + if not ini then for i=1 to 2 do print_char (Char.chr 8);print_char (Char.chr 13) done; - msg (str "Executed expressions: " ++ int (!allskip - !skip) ++ + msg (str "Executed expressions: " ++ int (!allskip - !skip) ++ fnl() ++ fnl()) (* Prints the prompt *) @@ -168,7 +168,7 @@ let db_matching_failure debug = let db_eval_failure debug s = if debug <> DebugOff & !skip = 0 then let s = str "message \"" ++ s ++ str "\"" in - msgnl + msgnl (str "This rule has failed due to \"Fail\" tactic (" ++ s ++ str ", level 0)!" ++ fnl() ++ str "Let us try the next one...") |