diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/logic.ml | 3 | ||||
| -rw-r--r-- | proofs/logic.mli | 1 | ||||
| -rw-r--r-- | proofs/tacinterp.ml | 75 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 4 |
4 files changed, 31 insertions, 52 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index fdece93e21..3b7c85b405 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -28,6 +28,7 @@ type refiner_error = | CannotGeneralize of constr | NotWellTyped of constr | BadTacticArgs of string * tactic_arg list + | IntroNeedsProduct exception RefinerError of refiner_error @@ -310,7 +311,7 @@ let prim_refiner r sigma goal = mk_goal info (push_var_def (id,c1,a) env) (subst1 v b) in [sg] | _ -> - if !check then error "Introduction needs a product" + if !check then raise (RefinerError IntroNeedsProduct) else anomaly "Intro: expects a product") | { name = Intro_after; newids = [id]; hypspecs = [whereid] } -> diff --git a/proofs/logic.mli b/proofs/logic.mli index 9247d4ff6e..eade902bab 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -43,6 +43,7 @@ type refiner_error = | CannotGeneralize of constr | NotWellTyped of constr | BadTacticArgs of string * tactic_arg list + | IntroNeedsProduct exception RefinerError of refiner_error diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml index 7375947f16..6a6a019fed 100644 --- a/proofs/tacinterp.ml +++ b/proofs/tacinterp.ml @@ -71,7 +71,7 @@ let rec constr_list goalopt = function | None -> constr_list goalopt tl | Some goal -> if mem_var_context id (pf_hyps goal) then - (id_of_string str,VAR id)::(constr_list goalopt tl) + (id_of_string str,mkVar id)::(constr_list goalopt tl) else constr_list goalopt tl)) | _::tl -> constr_list goalopt tl @@ -356,7 +356,7 @@ let apply_one_mhyp_context lmatch mhyp lhyps noccopt = (* Prepares the lfun list for constr substitutions *) let rec make_subs_list = function | (id,VArg (Identifier i))::tl -> - (id_of_string id,VAR i)::(make_subs_list tl) + (id_of_string id,mkVar i)::(make_subs_list tl) | (id,VArg (Constr c))::tl -> (id_of_string id,c)::(make_subs_list tl) | e::tl -> make_subs_list tl @@ -748,57 +748,34 @@ and cvt_fold (evc,env,lfun,lmatch,goalopt) = function (* Interprets the reduction flags *) and flag_of_ast (evc,env,lfun,lmatch,goalopt) lf = - let beta = ref false in - let delta = ref false in - let iota = ref false in - let idents = ref (None: (sorts oper -> bool) option) in - let set_flag = function - | Node(_,"Beta",[]) -> beta := true - | Node(_,"Delta",[]) -> delta := true - | Node(_,"Iota",[]) -> iota := true - | Node(loc,"Unf",l) -> - if !delta then - if !idents = None then - let idl= - List.map (fun v -> glob_nvar (id_of_Identifier (unvarg - (val_interp (evc,env,lfun,lmatch,goalopt) v)))) l - in - idents := Some - (function - | Const sp -> List.mem sp idl - | _ -> false) - else user_err_loc(loc,"flag_of_ast", - [<'sTR "Cannot specify identifiers to unfold twice">]) - else user_err_loc(loc,"flag_of_ast", - [<'sTR "Delta must be specified before">]) - | Node(loc,"UnfBut",l) -> - if !delta then - if !idents = None then - let idl= - List.map (fun v -> glob_nvar (id_of_Identifier (unvarg - (val_interp (evc,env,lfun,lmatch,goalopt) v)))) l - in - idents := Some - (function - | Const sp -> not (List.mem sp idl) - | _ -> false) - else user_err_loc(loc,"flag_of_ast", - [<'sTR "Cannot specify identifiers to unfold twice">]) - else user_err_loc(loc,"flag_of_ast", - [<'sTR "Delta must be specified before">]) - | arg -> invalid_arg_loc (Ast.loc arg,"flag_of_ast") + let rec add_flag red = function + | [] -> red + | Node(_,"Beta",[])::lf -> add_flag (red_add red BETA) lf + | Node(_,"Delta",[])::lf -> + (match lf with + | Node(loc,"Unf",l)::lf -> + let idl= + List.map (fun v -> glob_nvar (id_of_Identifier (unvarg + (val_interp (evc,env,lfun,lmatch,goalopt) v)))) l + in add_flag (red_add red (CONST idl)) lf + | Node(loc,"UnfBut",l)::lf -> + let idl= + List.map (fun v -> glob_nvar (id_of_Identifier (unvarg + (val_interp (evc,env,lfun,lmatch,goalopt) v)))) l + in add_flag (red_add red (CONSTBUT idl)) lf + | _ -> add_flag (red_add red DELTA) lf) + | Node(_,"Iota",[])::lf -> add_flag (red_add red IOTA) lf + | Node(loc,("Unf"|"UnfBut"),l)::_ -> + user_err_loc(loc,"flag_of_ast", + [<'sTR "Delta must be specified before">]) + + | arg::_ -> invalid_arg_loc (Ast.loc arg,"flag_of_ast") in - List.iter set_flag lf; - { r_beta = !beta; - r_iota = !iota; - r_delta = match (!delta,!idents) with - (false,_) -> (fun _ -> false) - | (true,None) -> (fun _ -> true) - | (true,Some p) -> p } + add_flag no_red lf; (* Interprets a reduction expression *) and redexp_of_ast (evc,env,lfun,lmatch,goalopt) = function - | ("Red", []) -> Red + | ("Red", []) -> Red false | ("Hnf", []) -> Hnf | ("Simpl", []) -> Simpl | ("Unfold", ul) -> diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index ae2ebc9eec..9234d90a27 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -74,7 +74,7 @@ val pf_compute : goal sigma -> constr -> constr val pf_unfoldn : (int list * section_path) list -> goal sigma -> constr -> constr -val pf_const_value : goal sigma -> constr -> constr +val pf_const_value : goal sigma -> constant -> constr val pf_conv_x : goal sigma -> constr -> constr -> bool val pf_conv_x_leq : goal sigma -> constr -> constr -> bool @@ -205,7 +205,7 @@ val ctxt_type_of : readable_constraints -> constr -> constr val w_whd_betadeltaiota : walking_constraints -> constr -> constr val w_hnf_constr : walking_constraints -> constr -> constr val w_conv_x : walking_constraints -> constr -> constr -> bool -val w_const_value : walking_constraints -> constr -> constr +val w_const_value : walking_constraints -> constant -> constr val w_defined_const : walking_constraints -> constr -> bool val w_defined_evar : walking_constraints -> int -> bool |