diff options
author | Samuel Mimram <smimram@debian.org> | 2007-02-13 13:48:12 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2007-02-13 13:48:12 +0000 |
commit | 55ce117e8083477593cf1ff2e51a3641c7973830 (patch) | |
tree | a82defb4105f175c71b0d13cae42831ce608c4d6 /proofs | |
parent | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (diff) |
Imported Upstream version 8.1+dfsgupstream/8.1+dfsg
Diffstat (limited to 'proofs')
-rw-r--r-- | proofs/decl_expr.mli | 18 | ||||
-rw-r--r-- | proofs/decl_mode.ml | 9 | ||||
-rw-r--r-- | proofs/decl_mode.mli | 5 | ||||
-rw-r--r-- | proofs/evar_refiner.ml | 11 | ||||
-rw-r--r-- | proofs/logic.ml | 236 | ||||
-rw-r--r-- | proofs/logic.mli | 4 | ||||
-rw-r--r-- | proofs/proof_type.ml | 4 | ||||
-rw-r--r-- | proofs/proof_type.mli | 4 | ||||
-rw-r--r-- | proofs/refiner.ml | 81 | ||||
-rw-r--r-- | proofs/tacexpr.ml | 3 | ||||
-rw-r--r-- | proofs/tacmach.ml | 5 |
11 files changed, 176 insertions, 204 deletions
diff --git a/proofs/decl_expr.mli b/proofs/decl_expr.mli index 24af3842..a8b7c0d6 100644 --- a/proofs/decl_expr.mli +++ b/proofs/decl_expr.mli @@ -6,16 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id:$ *) +(* $Id$ *) open Names open Util open Tacexpr -type ('constr,'tac) justification = - By_tactic of 'tac -| Automated of 'constr list - type 'it statement = {st_label:name; st_it:'it} @@ -42,8 +38,9 @@ type block_type = | B_elim of elim_type type ('it,'constr,'tac) cut = - {cut_stat: 'it statement; - cut_by: ('constr,'tac) justification} + {cut_stat: 'it; + cut_by: 'constr list option; + cut_using: 'tac option} type ('var,'constr) hyp = Hvar of 'var @@ -51,14 +48,15 @@ type ('var,'constr) hyp = type ('constr,'tac) casee = Real of 'constr - | Virtual of ('constr,'constr,'tac) cut + | Virtual of ('constr statement,'constr,'tac) cut type ('hyp,'constr,'pat,'tac) bare_proof_instr = | Pthen of ('hyp,'constr,'pat,'tac) bare_proof_instr | Pthus of ('hyp,'constr,'pat,'tac) bare_proof_instr | Phence of ('hyp,'constr,'pat,'tac) bare_proof_instr - | Pcut of ('constr or_thesis,'constr,'tac) cut - | Prew of side * ('constr,'constr,'tac) cut + | Pcut of ('constr or_thesis statement,'constr,'tac) cut + | Prew of side * ('constr statement,'constr,'tac) cut + | Psuffices of ((('hyp,'constr) hyp list * 'constr or_thesis),'constr,'tac) cut | Passume of ('hyp,'constr) hyp list | Plet of ('hyp,'constr) hyp list | Pgiven of ('hyp,'constr) hyp list diff --git a/proofs/decl_mode.ml b/proofs/decl_mode.ml index 094c5625..8d8fb745 100644 --- a/proofs/decl_mode.ml +++ b/proofs/decl_mode.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id:$ *) +(* $Id$ *) open Names open Term @@ -67,11 +67,10 @@ type stack_info = | Focus_claim type pm_info = - { pm_last: Names.name (* anonymous if none *); - pm_hyps: Idset.t; - pm_partial_goal : constr ; (* partial goal construction *) + { pm_last: (Names.identifier * bool) option (* anonymous if none *); + pm_partial_goal : constr; (* partial goal construction *) pm_subgoals : (metavariable*constr) list; - pm_stack : stack_info list } + pm_stack : stack_info list} let pm_in,pm_out = Dyn.create "pm_info" diff --git a/proofs/decl_mode.mli b/proofs/decl_mode.mli index 0dd1cb33..81fab168 100644 --- a/proofs/decl_mode.mli +++ b/proofs/decl_mode.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id:$ *) +(* $Id$ *) open Names open Term @@ -56,8 +56,7 @@ type stack_info = | Focus_claim type pm_info = - { pm_last: Names.name (* anonymous if none *); - pm_hyps: Idset.t; + { pm_last: (Names.identifier * bool) option (* anonymous if none *); pm_partial_goal : constr ; (* partial goal construction *) pm_subgoals : (metavariable*constr) list; pm_stack : stack_info list } diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 79f01ba1..132fa2b9 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evar_refiner.ml 9154 2006-09-20 17:18:18Z corbinea $ *) +(* $Id: evar_refiner.ml 9583 2007-02-01 19:35:03Z notin $ *) open Util open Names @@ -28,9 +28,12 @@ let w_refine ev rawc evd = let e_info = Evd.find (evars_of evd) ev in let env = Evd.evar_env e_info in let sigma,typed_c = - Pretyping.Default.understand_tcc (evars_of evd) env - ~expected_type:e_info.evar_concl rawc in - evar_define ev typed_c (evars_reset_evd sigma evd) + try Pretyping.Default.understand_tcc (evars_of evd) env + ~expected_type:e_info.evar_concl rawc + with _ -> error ("The term is not well-typed in the environment of " ^ + string_of_existential ev) + in + evar_define ev typed_c (evars_reset_evd sigma evd) (* vernac command Existential *) diff --git a/proofs/logic.ml b/proofs/logic.ml index e40d1232..92225948 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: logic.ml 9323 2006-10-30 23:05:29Z herbelin $ *) +(* $Id: logic.ml 9601 2007-02-06 21:37:59Z herbelin $ *) open Pp open Util @@ -69,26 +69,10 @@ let with_check = Options.with_option check (* The Clear tactic: it scans the context for hypotheses to be removed (instead of iterating on the list of identifier to be removed, which forces the user to give them in order). *) -let clear_hyps ids gl = - let env = Global.env() in - let (nhyps,cleared_ids) = - let fcheck cleared_ids (id,_,_ as d) = - if !check && cleared_ids<>[] then - Idset.iter - (fun id' -> - if List.mem id' cleared_ids then - error (string_of_id id'^ - " is used in hypothesis "^string_of_id id)) - (global_vars_set_of_decl env d) in - clear_hyps ids fcheck gl.evar_hyps in - let ncl = gl.evar_concl in - if !check && cleared_ids<>[] then - Idset.iter - (fun id' -> - if List.mem id' cleared_ids then - error (string_of_id id'^" is used in conclusion")) - (global_vars_set_drop_evar env ncl); - mk_goal nhyps ncl gl.evar_extra +let clear_hyps sigma ids gl = + let evd = ref (Evd.create_evar_defs sigma) in + let ngl = Evarutil.clear_hyps_in_evi evd gl ids in + (ngl, evars_of !evd) (* The ClearBody tactic *) @@ -216,7 +200,7 @@ let check_forward_dependencies id tail = let check_goal_dependency id cl = let env = Global.env() in - if Idset.mem id (global_vars_set_drop_evar env cl) then + if Idset.mem id (global_vars_set env cl) then error (string_of_id id^" is used in conclusion") let rename_hyp id1 id2 sign = @@ -398,6 +382,19 @@ let convert_hyp sign sigma (id,b,bt as d) = error ("Incorrect change of the body of "^(string_of_id id)); d) +(* Normalizing evars in a goal. Called by tactic Local_constraints + (i.e. when the sigma of the proof tree changes). Detect if the + goal is unchanged *) +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 + 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 + + (************************************************************************) (************************************************************************) @@ -418,13 +415,13 @@ let prim_refiner r sigma goal = if occur_meta c1 then error_use_instantiate(); let sg = mk_goal (push_named_context_val (id,None,c1) sign) (subst1 (mkVar id) b) in - [sg] + ([sg], sigma) | LetIn (_,c1,t1,b) -> if occur_meta c1 or occur_meta t1 then error_use_instantiate(); let sg = mk_goal (push_named_context_val (id,Some c1,t1) sign) (subst1 (mkVar id) b) in - [sg] + ([sg], sigma) | _ -> raise (RefinerError IntroNeedsProduct)) @@ -434,12 +431,12 @@ let prim_refiner r sigma goal = if occur_meta c1 then error_use_instantiate(); let sign' = replace_hyp sign id (id,None,c1) cl in let sg = mk_goal sign' (subst1 (mkVar id) b) in - [sg] + ([sg], sigma) | LetIn (_,c1,t1,b) -> if occur_meta c1 then error_use_instantiate(); let sign' = replace_hyp sign id (id,Some c1,t1) cl in let sg = mk_goal sign' (subst1 (mkVar id) b) in - [sg] + ([sg], sigma) | _ -> raise (RefinerError IntroNeedsProduct)) @@ -449,7 +446,7 @@ let prim_refiner r sigma goal = if occur_meta t then error_use_instantiate(); let sg1 = mk_goal sign (nf_betaiota t) in let sg2 = mk_goal (push_named_context_val (id,None,t) sign) cl in - if b then [sg1;sg2] else [sg2;sg1] + if b then ([sg1;sg2],sigma) else ([sg2;sg1], sigma) | FixRule (f,n,rest) -> let rec check_ind env k cl = @@ -478,7 +475,7 @@ let prim_refiner r sigma goal = | [] -> List.map (fun (_,_,c) -> mk_goal sign c) all in - mk_sign sign all + (mk_sign sign all, sigma) | Cofix (f,others) -> let rec check_is_coind env cl = @@ -505,47 +502,48 @@ e types") mk_sign (push_named_context_val (f,None,ar) sign) oth) | [] -> List.map (fun (_,c) -> mk_goal sign c) all in - mk_sign sign all + (mk_sign sign all, sigma) | Refine c -> if not (list_distinct (collect_meta_variables c)) then raise (RefinerError (NonLinearProof c)); let (sgl,cl') = mk_refgoals sigma goal [] cl c in let sgl = List.rev sgl in - sgl + (sgl, sigma) (* Conversion rules *) | Convert_concl (cl',_) -> check_typability env sigma cl'; if (not !check) || is_conv_leq env sigma cl' cl then let sg = mk_goal sign cl' in - [sg] + ([sg], sigma) else error "convert-concl rule passed non-converting term" | Convert_hyp (id,copt,ty) -> - [mk_goal (convert_hyp sign sigma (id,copt,ty)) cl] + ([mk_goal (convert_hyp sign sigma (id,copt,ty)) cl], sigma) (* And now the structural rules *) | Thin ids -> - [clear_hyps ids goal] - + let (ngl, nsigma) = clear_hyps sigma ids goal in + ([ngl], nsigma) + | ThinBody ids -> let clear_aux env id = let env' = remove_hyp_body env sigma id in - if !check then recheck_typability (None,id) env' sigma cl; - env' + if !check then recheck_typability (None,id) env' sigma cl; + env' in let sign' = named_context_val (List.fold_left clear_aux env ids) in let sg = mk_goal sign' cl in - [sg] + ([sg], sigma) | Move (withdep, hfrom, hto) -> let (left,right,declfrom,toleft) = split_sign hfrom hto (named_context_of_val sign) in let hyps' = move_after withdep toleft (left,declfrom,right) hto in - [mk_goal hyps' cl] + ([mk_goal hyps' cl], sigma) | Rename (id1,id2) -> if !check & id1 <> id2 && @@ -553,7 +551,12 @@ e types") error ((string_of_id id2)^" is already used"); let sign' = rename_hyp id1 id2 sign in let cl' = replace_vars [id1,mkVar id2] cl in - [mk_goal sign' cl'] + ([mk_goal sign' cl'], sigma) + + | Change_evars -> + match norm_goal sigma goal with + Some ngl -> ([ngl],sigma) + | None -> ([goal], sigma) (************************************************************************) (************************************************************************) @@ -596,80 +599,83 @@ let proof_variable_index x = let prim_extractor subfun vl pft = let cl = pft.goal.evar_concl in - match pft.ref with - | Some (Prim (Intro id), [spf]) -> - (match kind_of_term (strip_outer_cast cl) with - | Prod (_,ty,_) -> - let cty = subst_proof_vars vl ty in - mkLambda (Name id, cty, subfun (add_proof_var id vl) spf) - | LetIn (_,b,ty,_) -> - let cb = subst_proof_vars vl b in - 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 (Intro_replacing id),[spf]) -> - (match kind_of_term (strip_outer_cast cl) with - | Prod (_,ty,_) -> - let cty = subst_proof_vars vl ty in - mkLambda (Name id, cty, subfun (add_proof_var id vl) spf) - | LetIn (_,b,ty,_) -> - let cb = subst_proof_vars vl b in - 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, - subfun (add_proof_var id vl) spf2) - - | Some (Prim (FixRule (f,n,others)),spfl) -> - let all = Array.of_list ((f,n,cl)::others) in - let lcty = Array.map (fun (_,_,ar) -> subst_proof_vars vl ar) all in - let names = Array.map (fun (f,_,_) -> Name f) all in - let vn = Array.map (fun (_,n,_) -> n-1) all in - 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,0),(names,lcty,lfix)) - - | Some (Prim (Cofix (f,others)),spfl) -> - let all = Array.of_list ((f,cl)::others) in - 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 - let lfix = Array.map (subfun newvl) (Array.of_list spfl) in - mkCoFix (0,(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 - plain_instance metamap cc - - (* Structural and conversion rules do not produce any proof *) - | Some (Prim (Convert_concl (t,k)),[pf]) -> - if k = DEFAULTcast then subfun vl pf - else mkCast (subfun vl pf,k,subst_proof_vars vl cl) - | Some (Prim (Convert_hyp _),[pf]) -> - subfun vl pf - - | 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 _),[pf]) -> - subfun vl pf - - | Some (Prim (Rename (id1,id2)),[pf]) -> - subfun (rebind id1 id2 vl) pf - - | Some _ -> anomaly "prim_extractor" - - | None-> error "prim_extractor handed incomplete proof" + match pft.ref with + | Some (Prim (Intro id), [spf]) -> + (match kind_of_term (strip_outer_cast cl) with + | Prod (_,ty,_) -> + let cty = subst_proof_vars vl ty in + mkLambda (Name id, cty, subfun (add_proof_var id vl) spf) + | LetIn (_,b,ty,_) -> + let cb = subst_proof_vars vl b in + 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 (Intro_replacing id),[spf]) -> + (match kind_of_term (strip_outer_cast cl) with + | Prod (_,ty,_) -> + let cty = subst_proof_vars vl ty in + mkLambda (Name id, cty, subfun (add_proof_var id vl) spf) + | LetIn (_,b,ty,_) -> + let cb = subst_proof_vars vl b in + 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, + subfun (add_proof_var id vl) spf2) + + | Some (Prim (FixRule (f,n,others)),spfl) -> + let all = Array.of_list ((f,n,cl)::others) in + let lcty = Array.map (fun (_,_,ar) -> subst_proof_vars vl ar) all in + let names = Array.map (fun (f,_,_) -> Name f) all in + let vn = Array.map (fun (_,n,_) -> n-1) all in + 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,0),(names,lcty,lfix)) + + | Some (Prim (Cofix (f,others)),spfl) -> + let all = Array.of_list ((f,cl)::others) in + 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 + let lfix = Array.map (subfun newvl) (Array.of_list spfl) in + mkCoFix (0,(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 + plain_instance metamap cc + + (* Structural and conversion rules do not produce any proof *) + | Some (Prim (Convert_concl (t,k)),[pf]) -> + if k = DEFAULTcast then subfun vl pf + else mkCast (subfun vl pf,k,subst_proof_vars vl cl) + | Some (Prim (Convert_hyp _),[pf]) -> + subfun vl pf + + | 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 _),[pf]) -> + subfun vl pf + + | Some (Prim (Rename (id1,id2)),[pf]) -> + subfun (rebind id1 id2 vl) pf + + | Some (Prim Change_evars, [pf]) -> + subfun vl pf + + | Some _ -> anomaly "prim_extractor" + + | None-> error "prim_extractor handed incomplete proof" diff --git a/proofs/logic.mli b/proofs/logic.mli index ab65b1d5..2b6c6b4a 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: logic.mli 8107 2006-03-01 17:34:36Z herbelin $ i*) +(*i $Id: logic.mli 9573 2007-01-31 20:18:18Z notin $ i*) (*i*) open Names @@ -34,7 +34,7 @@ val with_check : tactic -> tactic (* The primitive refiner. *) -val prim_refiner : prim_rule -> evar_map -> goal -> goal list +val prim_refiner : prim_rule -> evar_map -> goal -> goal list * evar_map type proof_variable diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index abe31624..6f8b0686 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: proof_type.ml 9244 2006-10-16 17:11:44Z barras $ *) +(*i $Id: proof_type.ml 9573 2007-01-31 20:18:18Z notin $ *) (*i*) open Environ @@ -39,6 +39,7 @@ type prim_rule = | ThinBody of identifier list | Move of bool * identifier * identifier | Rename of identifier * identifier + | Change_evars type proof_tree = { open_subgoals : int; @@ -50,7 +51,6 @@ and rule = | Nested of compound_rule * proof_tree | Decl_proof of bool | Daimon - | Change_evars and compound_rule= | Tactic of tactic_expr * bool diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index d87c1298..26d9eb2e 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: proof_type.mli 9244 2006-10-16 17:11:44Z barras $ i*) +(*i $Id: proof_type.mli 9573 2007-01-31 20:18:18Z notin $ i*) (*i*) open Environ @@ -39,6 +39,7 @@ type prim_rule = | ThinBody of identifier list | Move of bool * identifier * identifier | Rename of identifier * identifier + | Change_evars (* The type [goal sigma] is the type of subgoal. It has the following form \begin{verbatim} @@ -84,7 +85,6 @@ and rule = | Nested of compound_rule * proof_tree | Decl_proof of bool | Daimon - | Change_evars and compound_rule= (* the boolean of Tactic tells if the default tactic is used *) diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 70a0e3db..a1d7e011 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: refiner.ml 9261 2006-10-23 10:01:40Z barras $ *) +(* $Id: refiner.ml 9573 2007-01-31 20:18:18Z notin $ *) open Pp open Util @@ -68,18 +68,6 @@ let descend n p = else error "Too few subproofs" -(* Normalizing evars in a goal. Called by tactic Local_constraints - (i.e. when the sigma of the proof tree changes). Detect if the - goal is unchanged *) -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 - 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 - (* [mapshape [ l1 ; ... ; lk ] [ v1 ; ... ; vk ] [ p_1 ; .... ; p_(l1+...+lk) ]] gives @@ -192,11 +180,11 @@ let abstract_operation syntax semantics gls = let (sgl_sigma,validation) = semantics gls in let hidden_proof = validation (List.map leaf sgl_sigma.it) in (sgl_sigma, - fun spfl -> - assert (check_subproof_connection sgl_sigma.it spfl); - { open_subgoals = and_status (List.map pf_status spfl); - goal = gls.it; - ref = Some(Nested(syntax,hidden_proof),spfl)}) + fun spfl -> + assert (check_subproof_connection sgl_sigma.it spfl); + { open_subgoals = and_status (List.map pf_status spfl); + goal = gls.it; + ref = Some(Nested(syntax,hidden_proof),spfl)}) let abstract_tactic_expr ?(dflt=false) te tacfun gls = abstract_operation (Tactic(te,dflt)) tacfun gls @@ -210,14 +198,14 @@ let abstract_extended_tactic ?(dflt=false) s args = let refiner = function | Prim pr as r -> let prim_fun = prim_refiner pr in - (fun goal_sigma -> - let sgl = prim_fun goal_sigma.sigma goal_sigma.it in - ({it=sgl; sigma = goal_sigma.sigma}, - (fun spfl -> - assert (check_subproof_connection sgl spfl); - { open_subgoals = and_status (List.map pf_status spfl); - goal = goal_sigma.it; - ref = Some(r,spfl) }))) + (fun goal_sigma -> + let (sgl,sigma') = prim_fun goal_sigma.sigma goal_sigma.it in + ({it=sgl; sigma = sigma'}, + (fun spfl -> + assert (check_subproof_connection sgl spfl); + { open_subgoals = and_status (List.map pf_status spfl); + goal = goal_sigma.it; + ref = Some(r,spfl) }))) | Nested (_,_) | Decl_proof _ -> @@ -234,44 +222,23 @@ let refiner = function goal = gls.it; ref = Some(Daimon,[])}) - (* [Local_constraints lc] makes the local constraints be [lc] and - normalizes evars *) - - | Change_evars as r -> - (fun goal_sigma -> - let gl = goal_sigma.it in - (match norm_goal goal_sigma.sigma gl with - Some ngl -> - ({it=[ngl];sigma=goal_sigma.sigma}, - (fun spfl -> - assert (check_subproof_connection [ngl] spfl); - { open_subgoals = (List.hd spfl).open_subgoals; - goal = gl; - ref = Some(r,spfl) })) - (* if the evar change does not affect the goal, leave the - proof tree unchanged *) - | None -> ({it=[gl];sigma=goal_sigma.sigma}, - (fun spfl -> - assert (List.length spfl = 1); - List.hd spfl)))) - - -let local_Constraints gl = refiner Change_evars gl + +let local_Constraints gl = refiner (Prim Change_evars) gl let norm_evar_tac = local_Constraints let norm_evar_proof sigma pf = let nf_subgoal i sgl = let (gll,v) = norm_evar_tac {it=sgl.goal;sigma=sigma} in - v (List.map leaf gll.it) in - frontier_mapi nf_subgoal pf + v (List.map leaf gll.it) in + frontier_mapi nf_subgoal pf (* [extract_open_proof : proof_tree -> constr * (int * constr) list] - takes a (not necessarly complete) proof and gives a pair (pfterm,obl) - where pfterm is the constr corresponding to the proof - and [obl] is an [int*constr list] [ (m1,c1) ; ... ; (mn,cn)] - where the mi are metavariables numbers, and ci are their types. - Their proof should be completed in order to complete the initial proof *) + takes a (not necessarly complete) proof and gives a pair (pfterm,obl) + where pfterm is the constr corresponding to the proof + and [obl] is an [int*constr list] [ (m1,c1) ; ... ; (mn,cn)] + where the mi are metavariables numbers, and ci are their types. + Their proof should be completed in order to complete the initial proof *) let extract_open_proof sigma pf = let next_meta = @@ -291,8 +258,6 @@ let extract_open_proof sigma pf = let flat_proof = v spfl in proof_extractor vl flat_proof - | {ref=Some(Change_evars,[pf])} -> (proof_extractor vl) pf - | {ref=Some(Decl_proof _,[pf])} -> (proof_extractor vl) pf | {ref=(None|Some(Daimon,[]));goal=goal} -> diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index 0fe21552..0bcc7d16 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tacexpr.ml 9267 2006-10-24 12:55:46Z herbelin $ i*) +(*i $Id: tacexpr.ml 9551 2007-01-29 15:13:35Z bgregoir $ i*) open Names open Topconstr @@ -121,6 +121,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = | TacAssumption | TacExact of 'constr | TacExactNoCheck of 'constr + | TacVmCastNoCheck of 'constr | TacApply of 'constr with_bindings | TacElim of 'constr with_bindings * 'constr with_bindings option | TacElimType of 'constr diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index b426f75d..baf8c859 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacmach.ml 7682 2005-12-21 15:06:11Z herbelin $ *) +(* $Id: tacmach.ml 9511 2007-01-22 08:27:31Z herbelin $ *) open Util open Names @@ -102,6 +102,7 @@ let pf_nf_betaiota = pf_reduce (fun _ _ -> nf_betaiota) let pf_compute = pf_reduce compute let pf_unfoldn ubinds = pf_reduce (unfoldn ubinds) let pf_type_of = pf_reduce type_of +let pf_get_type_of = pf_reduce Retyping.get_type_of let pf_conv_x = pf_reduce is_conv let pf_conv_x_leq = pf_reduce is_conv_leq @@ -109,7 +110,7 @@ let pf_const_value = pf_reduce (fun env _ -> constant_value env) let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind -let hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_type_of gls) +let hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_get_type_of gls) let pf_check_type gls c1 c2 = ignore (pf_type_of gls (mkCast (c1, DEFAULTcast, c2))) |