diff options
| -rw-r--r-- | proofs/clenv.ml | 1 | ||||
| -rw-r--r-- | proofs/proof_type.ml | 10 | ||||
| -rw-r--r-- | proofs/proof_type.mli | 6 | ||||
| -rw-r--r-- | proofs/tacinterp.ml | 778 | ||||
| -rw-r--r-- | proofs/tacinterp.mli | 3 | ||||
| -rw-r--r-- | tactics/auto.ml | 2 | ||||
| -rw-r--r-- | tactics/eauto.ml | 3 |
7 files changed, 400 insertions, 403 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index e643f02a4..827618856 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -281,7 +281,6 @@ let unifyTerms m n = walking (fun wc -> fst (w_Unify m n [] wc)) let unify m gls = let n = pf_concl gls in unifyTerms m n gls - (* collects all metavar occurences, in left-to-right order, preserving * repetitions and all. *) diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index eaebd6b99..462b038a1 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -7,8 +7,8 @@ open Term open Util (*i*) -(*This module defines the structure of proof tree and the tactic type. So, it - is used by Proof_tree and Refiner*) +(* This module defines the structure of proof tree and the tactic type. So, it + is used by Proof_tree and Refiner *) type bindOcc = | Dep of identifier @@ -17,7 +17,9 @@ type bindOcc = type 'a substitution = (bindOcc * 'a) list -type pf_status = Complete_proof | Incomplete_proof +type pf_status = + | Complete_proof + | Incomplete_proof type prim_rule_name = | Intro @@ -50,7 +52,7 @@ type evar_declarations = ctxtty evar_map with some extra information for the program tactic *) type global_constraints = evar_declarations timestamped -(*Signature useful to define the tactic type*) +(* Signature useful to define the tactic type *) type 'a sigma = { it : 'a ; sigma : global_constraints } diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index a722335d5..5ef9416b3 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -20,7 +20,9 @@ type bindOcc = type 'a substitution = (bindOcc * 'a) list -type pf_status = Complete_proof | Incomplete_proof +type pf_status = + | Complete_proof + | Incomplete_proof type prim_rule_name = | Intro @@ -53,7 +55,7 @@ type evar_declarations = ctxtty evar_map with some extra information for the program tactic *) type global_constraints = evar_declarations timestamped -(*Signature useful to define the tactic type*) +(* Signature useful to define the tactic type *) type 'a sigma = { it : 'a ; sigma : global_constraints } diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml index af784dcf5..4340aa31d 100644 --- a/proofs/tacinterp.ml +++ b/proofs/tacinterp.ml @@ -22,12 +22,12 @@ open Term let err_msg_tactic_not_found macro_loc macro = user_err_loc (macro_loc,"macro_expand", - [< 'sTR"Tactic macro ";'sTR macro; 'sPC; 'sTR"not found" >]) + [<'sTR "Tactic macro "; 'sTR macro; 'sPC; 'sTR "not found">]) (* Values for interpretation *) -type value= +type value = | VTactic of tactic - | VFTactic of tactic_arg list * (tactic_arg list -> tactic) + | VFTactic of tactic_arg list * (tactic_arg list->tactic) | VRTactic of (goal list sigma * validation) | VArg of tactic_arg | VFun of (string * value) list * string option list * Coqast.t @@ -37,54 +37,56 @@ type value= (* Gives the identifier corresponding to an Identifier tactic_arg *) let id_of_Identifier = function | Identifier id -> id - |_ -> + | _ -> anomalylabstrm "id_of_IDENTIFIER" [<'sTR "Not an IDENTIFIER tactic_arg">] (* Gives the constr corresponding to a Constr tactic_arg *) -let constr_of_Constr=function - Constr c -> c - |_ -> anomalylabstrm "constr_of_Constr" [<'sTR "Not a CONSTR tactic_arg">] +let constr_of_Constr = function + | Constr c -> c + | _ -> anomalylabstrm "constr_of_Constr" [<'sTR "Not a CONSTR tactic_arg">] (* Signature for interpretation: val_interp and interpretation functions *) -type interp_sign= - evar_declarations*Environ.env*(string*value) list*(int*constr) list* - goal sigma option +type interp_sign = + evar_declarations * Environ.env * (string * value) list * + (int * constr) list * goal sigma option (* Table of interpretation functions *) -let interp_tab= - (Hashtbl.create 17:(string,interp_sign->Coqast.t->value) Hashtbl.t) +let interp_tab = + (Hashtbl.create 17 : (string , interp_sign -> Coqast.t -> value) Hashtbl.t) (* Adds an interpretation function *) -let interp_add (ast_typ,interp_fun)= +let interp_add (ast_typ,interp_fun) = try Hashtbl.add interp_tab ast_typ interp_fun with - Failure _ -> - errorlabstrm "interp_add" [<'sTR - "Cannot add the interpretation function for "; 'sTR ast_typ; 'sTR - " twice">] + Failure _ -> + errorlabstrm "interp_add" + [<'sTR "Cannot add the interpretation function for "; 'sTR ast_typ; + 'sTR " twice">] (* Adds a possible existing interpretation function *) -let overwriting_interp_add (ast_typ,interp_fun)= +let overwriting_interp_add (ast_typ,interp_fun) = if Hashtbl.mem interp_tab ast_typ then - (Hashtbl.remove interp_tab ast_typ; - warning ("Overwriting definition of tactic interpreter command "^ast_typ)); + begin + Hashtbl.remove interp_tab ast_typ; + warning ("Overwriting definition of tactic interpreter command " ^ ast_typ) + end; Hashtbl.add interp_tab ast_typ interp_fun (* Finds the interpretation function corresponding to a given ast type *) -let look_for_interp=Hashtbl.find interp_tab +let look_for_interp = Hashtbl.find interp_tab (* Globalizes the identifier *) -let glob_nvar id= +let glob_nvar id = try Nametab.sp_of_id CCI id with - Not_found -> error ("unbound variable "^(string_of_id id)) + | Not_found -> error ("unbound variable " ^ (string_of_id id)) (* Summary and Object declaration *) -let mactab=ref Gmap.empty +let mactab = ref Gmap.empty -let lookup id=Gmap.find id !mactab +let lookup id = Gmap.find id !mactab let _ = let init () = mactab := Gmap.empty in @@ -95,137 +97,137 @@ let _ = Summary.unfreeze_function = unfreeze; Summary.init_function = init } -let (inMD,outMD)= - let add (na,td)=mactab:=Gmap.add na td !mactab in - let cache_md (_,(na,td))=add (na,td) in +let (inMD,outMD) = + let add (na,td) = mactab := Gmap.add na td !mactab in + let cache_md (_,(na,td)) = add (na,td) in declare_object ("TACTIC-DEFINITION", - {cache_function=cache_md; - load_function=(fun _ -> ()); - open_function=(fun _ -> ()); - specification_function=(fun x -> x)}) + {cache_function = cache_md; + load_function = (fun _ -> ()); + open_function = (fun _ -> ()); + specification_function = (fun x -> x)}) (* Adds a Tactic Definition in the table *) let add_tacdef na vbody = - if Gmap.mem na !mactab then - errorlabstrm "Tacdef.add_tacdef" - [< 'sTR "There is already a Tactic Definition named "; 'sTR na >]; - let _ = Lib.add_leaf (id_of_string na) OBJ (inMD (na,vbody)) in - if Options.is_verbose() then mSGNL [< 'sTR (na^" is defined") >] + begin + if Gmap.mem na !mactab then + errorlabstrm "Tacdef.add_tacdef" + [<'sTR "There is already a Tactic Definition named "; 'sTR na>]; + let _ = Lib.add_leaf (id_of_string na) OBJ (inMD (na,vbody)) in + if Options.is_verbose() then mSGNL [< 'sTR (na ^ " is defined") >] + end (* Unboxes the tactic_arg *) -let unvarg=function - VArg a -> a - |_ -> errorlabstrm "unvarg" [<'sTR "Not a tactic argument">] +let unvarg = function + | VArg a -> a + | _ -> errorlabstrm "unvarg" [<'sTR "Not a tactic argument">] (* Unboxes VRec *) -let unrec=function - VRec v -> !v - |a -> a +let unrec = function + | VRec v -> !v + | a -> a (* Unboxes REDEXP *) -let unredexp=function - Redexp c -> c - |_ -> errorlabstrm "unredexp" [<'sTR "Not a REDEXP tactic_arg">] +let unredexp = function + | Redexp c -> c + | _ -> errorlabstrm "unredexp" [<'sTR "Not a REDEXP tactic_arg">] (* Reads the head of Fun *) -let read_fun ast= - let rec read_fun_rec=function - Node(_,"VOID",[])::tl -> None::(read_fun_rec tl) - |Nvar(_,s)::tl -> (Some s)::(read_fun_rec tl) - |[] -> [] - |_ -> +let read_fun ast = + let rec read_fun_rec = function + | Node(_,"VOID",[])::tl -> None::(read_fun_rec tl) + | Nvar(_,s)::tl -> (Some s)::(read_fun_rec tl) + | [] -> [] + | _ -> anomalylabstrm "Tacinterp.read_fun_rec" [<'sTR "Fun not well formed">] in match ast with - Node(_,"FUNVAR",l) -> read_fun_rec l - |_ -> + | Node(_,"FUNVAR",l) -> read_fun_rec l + | _ -> anomalylabstrm "Tacinterp.read_fun" [<'sTR "Fun not well formed">] (* Reads the clauses of a Rec *) -let rec read_rec_clauses=function - [] -> [] - |Node(_,"RECCLAUSE",[Nvar(_,name);it;body])::tl -> +let rec read_rec_clauses = function + | [] -> [] + | Node(_,"RECCLAUSE",[Nvar(_,name);it;body])::tl -> (name,it,body)::(read_rec_clauses tl) |_ -> - anomalylabstrm "Tacinterp.read_rec_clauses" [<'sTR - "Rec not well formed">] + anomalylabstrm "Tacinterp.read_rec_clauses" + [<'sTR "Rec not well formed">] (* Associates variables with values and gives the remaining variables and - values *) -let head_with_value (lvar,lval)= - let rec head_with_value_rec lacc=function - ([],[]) -> (lacc,[],[]) - |(vr::tvr,ve::tve) -> + values *) +let head_with_value (lvar,lval) = + let rec head_with_value_rec lacc = function + | ([],[]) -> (lacc,[],[]) + | (vr::tvr,ve::tve) -> (match vr with - None -> head_with_value_rec lacc (tvr,tve) - |Some v -> head_with_value_rec ((v,ve)::lacc) (tvr,tve)) - |(vr,[]) -> (lacc,vr,[]) - |([],ve) -> (lacc,[],ve) + | None -> head_with_value_rec lacc (tvr,tve) + | Some v -> head_with_value_rec ((v,ve)::lacc) (tvr,tve)) + | (vr,[]) -> (lacc,vr,[]) + | ([],ve) -> (lacc,[],ve) in head_with_value_rec [] (lvar,lval) (* Type of hypotheses for a Match Context rule *) -type match_context_hyps= - NoHypId of constr_pattern - |Hyp of string*constr_pattern +type match_context_hyps = + | NoHypId of constr_pattern + | Hyp of string * constr_pattern (* Type of a Match rule for Match Context and Match *) type match_rule= - Pat of match_context_hyps list*constr_pattern*Coqast.t - |All of Coqast.t + | Pat of match_context_hyps list * constr_pattern * Coqast.t + | All of Coqast.t (* Gives the ast of a COMMAND ast node *) -let ast_of_command=function - Node(_,"COMMAND",[c]) -> c - |ast -> +let ast_of_command = function + | Node(_,"COMMAND",[c]) -> c + | ast -> anomaly_loc (Ast.loc ast, "Tacinterp.ast_of_command",[<'sTR - "Not a COMMAND ast node: ";print_ast ast>]) + "Not a COMMAND ast node: "; print_ast ast>]) (* Reads the hypotheses of a Match Context rule *) let rec read_match_context_hyps evc env=function - Node(_,"MATCHCONTEXTHYPS",[pc])::tl -> - (NoHypId (snd (interp_constrpattern evc env (ast_of_command - pc))))::(read_match_context_hyps evc env tl) - |Node(_,"MATCHCONTEXTHYPS",[Nvar(_,s);pc])::tl -> - (Hyp (s,snd (interp_constrpattern evc env (ast_of_command - pc))))::(read_match_context_hyps evc env tl) - |ast::tl -> + | Node(_,"MATCHCONTEXTHYPS",[pc])::tl -> + (NoHypId (snd (interp_constrpattern evc env (ast_of_command + pc))))::(read_match_context_hyps evc env tl) + | Node(_,"MATCHCONTEXTHYPS",[Nvar(_,s);pc])::tl -> + (Hyp (s,snd (interp_constrpattern evc env (ast_of_command + pc))))::(read_match_context_hyps evc env tl) + | ast::tl -> anomaly_loc (Ast.loc ast, "Tacinterp.read_match_context_hyp",[<'sTR - "Not a MATCHCONTEXTHYP ast node: ";print_ast ast>]) - |[] -> [] + "Not a MATCHCONTEXTHYP ast node: "; print_ast ast>]) + | [] -> [] (* Reads the rules of a Match Context *) -let rec read_match_context_rule evc env=function - Node(_,"MATCHCONTEXTRULE",[tc])::tl -> - (All tc)::(read_match_context_rule evc env tl) - |Node(_,"MATCHCONTEXTRULE",l)::tl -> - let rl=List.rev l - in - (Pat (read_match_context_hyps evc env (List.tl (List.tl rl)),snd - (interp_constrpattern evc env (ast_of_command (List.nth rl - 1))),List.hd rl))::(read_match_context_rule evc env tl) - |ast::tl -> +let rec read_match_context_rule evc env = function + | Node(_,"MATCHCONTEXTRULE",[tc])::tl -> + (All tc)::(read_match_context_rule evc env tl) + | Node(_,"MATCHCONTEXTRULE",l)::tl -> + let rl=List.rev l in + (Pat (read_match_context_hyps evc env (List.tl (List.tl rl)),snd + (interp_constrpattern evc env (ast_of_command (List.nth rl + 1))),List.hd rl))::(read_match_context_rule evc env tl) + | ast::tl -> anomaly_loc (Ast.loc ast, "Tacinterp.read_match_context_rule",[<'sTR - "Not a MATCHCONTEXTRULE ast node: ";print_ast ast>]) - |[] -> [] + "Not a MATCHCONTEXTRULE ast node: "; print_ast ast>]) + | [] -> [] (* Reads the rules of a Match *) -let rec read_match_rule evc env=function - Node(_,"MATCHRULE",[te])::tl -> - (All te)::(read_match_rule evc env tl) - |Node(_,"MATCHRULE",[com;te])::tl -> - (Pat ([],snd (interp_constrpattern evc env (ast_of_command - com)),te))::(read_match_rule evc env tl) - |ast::tl -> +let rec read_match_rule evc env = function + | Node(_,"MATCHRULE",[te])::tl -> + (All te)::(read_match_rule evc env tl) + | Node(_,"MATCHRULE",[com;te])::tl -> + (Pat ([],snd (interp_constrpattern evc env (ast_of_command com)),te)) :: + (read_match_rule evc env tl) + | ast::tl -> anomaly_loc (Ast.loc ast, "Tacinterp.read_match_context_rule",[<'sTR - "Not a MATCHRULE ast node: ";print_ast ast>]) - |[] -> [] + "Not a MATCHRULE ast node: "; print_ast ast>]) + | [] -> [] -(* Transforms a type_judgment signature into a (string*constr) list *) -let make_hyps hyps= - let lid=List.map string_of_id (ids_of_sign hyps) - and lhyp=List.map body_of_type (vals_of_sign hyps) - in +(* Transforms a type_judgment signature into a (string * constr) list *) +let make_hyps hyps = + let lid = List.map string_of_id (ids_of_sign hyps) + and lhyp = List.map body_of_type (vals_of_sign hyps) in List.combine lid lhyp (* For Match Context and Match *) @@ -233,381 +235,372 @@ exception No_match exception Not_coherent_metas (* Verifies if the matched list is coherent with respect to lcm *) -let rec verify_metas_coherence lcm=function - (num,csr)::tl -> - if (List.for_all - (fun (a,b) -> - if a=num then - eq_constr b csr - else - true) lcm) then - (num,csr)::(verify_metas_coherence lcm tl) - else - raise Not_coherent_metas - |[] -> [] +let rec verify_metas_coherence lcm = function + | (num,csr)::tl -> + if (List.for_all + (fun (a,b) -> + if a=num then + eq_constr b csr + else + true) lcm) then + (num,csr)::(verify_metas_coherence lcm tl) + else + raise Not_coherent_metas + | [] -> [] (* Tries to match a pattern and a constr *) -let apply_matching pat csr= +let apply_matching pat csr = try (Pattern.matches pat csr) with PatternMatchingFailure -> raise No_match (* Tries to match one hypothesis with a list of hypothesis patterns *) -let apply_one_hyp_context lmatch mhyps (idhyp,hyp)= - let rec apply_one_hyp_context_rec (idhyp,hyp) mhyps_acc=function - (Hyp (idpat,pat))::tl -> - (try - ([idpat,VArg (Identifier - (id_of_string idhyp))],verify_metas_coherence lmatch - (Pattern.matches pat hyp),mhyps_acc@tl) - with - PatternMatchingFailure|Not_coherent_metas -> - apply_one_hyp_context_rec (idhyp,hyp) (mhyps_acc@[Hyp - (idpat,pat)]) tl) - |(NoHypId pat)::tl -> +let apply_one_hyp_context lmatch mhyps (idhyp,hyp) = + let rec apply_one_hyp_context_rec (idhyp,hyp) mhyps_acc = function + | (Hyp (idpat,pat))::tl -> + (try + ([idpat,VArg (Identifier + (id_of_string idhyp))],verify_metas_coherence lmatch + (Pattern.matches pat hyp),mhyps_acc@tl) + with + PatternMatchingFailure | Not_coherent_metas -> + apply_one_hyp_context_rec (idhyp,hyp) (mhyps_acc@[Hyp + (idpat,pat)]) tl) + | (NoHypId pat)::tl -> (try ([],verify_metas_coherence lmatch (Pattern.matches pat hyp),mhyps_acc@tl) with - PatternMatchingFailure|Not_coherent_metas -> + PatternMatchingFailure | Not_coherent_metas -> apply_one_hyp_context_rec (idhyp,hyp) (mhyps_acc@[NoHypId pat]) tl) - |[] -> raise No_match - in - apply_one_hyp_context_rec (idhyp,hyp) [] mhyps + | [] -> raise No_match in + apply_one_hyp_context_rec (idhyp,hyp) [] mhyps (* 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,VArg (Constr c))::tl -> +let rec make_subs_list = function + | (id,VArg (Identifier i))::tl -> + (id_of_string id,VAR 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 - |[] -> [] + | e::tl -> make_subs_list tl + | [] -> [] (* Interprets any expression *) -let rec val_interp (evc,env,lfun,lmatch,goalopt) ast= -(* mSGNL [<print_ast ast>]; *) - +let rec val_interp (evc,env,lfun,lmatch,goalopt) ast = +(* mSGNL [<print_ast ast>]; *) (* mSGNL [<print_ast (Termast.bdize false (Pretty.assumptions_for_print []) ((reduction_of_redexp redexp) env evc c))>]; *) match ast with - Node(_,"APP",l) -> - let fv=val_interp (evc,env,lfun,lmatch,goalopt) (List.hd l) - and largs= - List.map (val_interp (evc,env,lfun,lmatch,goalopt)) (List.tl l) - in - app_interp evc env lfun lmatch goalopt fv largs ast - |Node(_,"FUN",l) -> VFun (lfun,read_fun (List.hd l),List.nth l 1) - |Node(_,"REC",l) -> rec_interp evc env lfun lmatch goalopt ast l - |Node(_,"LET",[Node(_,"LETDECL",l);u]) -> - let addlfun=let_interp evc env lfun lmatch goalopt ast l - in + | Node(_,"APP",l) -> + let fv = val_interp (evc,env,lfun,lmatch,goalopt) (List.hd l) + and largs = List.map (val_interp (evc,env,lfun,lmatch,goalopt)) (List.tl + l) in + app_interp evc env lfun lmatch goalopt fv largs ast + | Node(_,"FUN",l) -> VFun (lfun,read_fun (List.hd l),List.nth l 1) + | Node(_,"REC",l) -> rec_interp evc env lfun lmatch goalopt ast l + | Node(_,"LET",[Node(_,"LETDECL",l);u]) -> + let addlfun=let_interp evc env lfun lmatch goalopt ast l in val_interp (evc,env,(lfun@addlfun),lmatch,goalopt) u - |Node(_,"MATCHCONTEXT",lmr) -> + | Node(_,"MATCHCONTEXT",lmr) -> match_context_interp evc env lfun lmatch goalopt ast lmr - |Node(_,"MATCH",lmr) -> + | Node(_,"MATCH",lmr) -> match_interp evc env lfun lmatch goalopt ast lmr - |Node(_,"IDTAC",[]) -> VTactic tclIDTAC - |Node(_,"FAIL",[]) -> VTactic tclFAIL - |Node(_,"TACTICLIST",l) -> + | Node(_,"IDTAC",[]) -> VTactic tclIDTAC + | Node(_,"FAIL",[]) -> VTactic tclFAIL + | Node(_,"TACTICLIST",l) -> VTactic (interp_semi_list tclIDTAC lfun lmatch l) - |Node(_,"DO",[n;tac]) -> + | Node(_,"DO",[n;tac]) -> VTactic (tclDO (num_of_ast n) (tac_interp lfun lmatch tac)) - |Node(_,"TRY",[tac]) -> + | Node(_,"TRY",[tac]) -> VTactic (tclTRY (tac_interp lfun lmatch tac)) - |Node(_,"INFO",[tac]) -> + | Node(_,"INFO",[tac]) -> VTactic (tclINFO (tac_interp lfun lmatch tac)) - |Node(_,"REPEAT",[tac]) -> + | Node(_,"REPEAT",[tac]) -> VTactic (tclREPEAT (tac_interp lfun lmatch tac)) - |Node(_,"ORELSE",[tac1;tac2]) -> + | Node(_,"ORELSE",[tac1;tac2]) -> VTactic (tclORELSE (tac_interp lfun lmatch tac1) (tac_interp lfun lmatch tac2)) - |Node(_,"FIRST",l) -> + | Node(_,"FIRST",l) -> VTactic (tclFIRST (List.map (tac_interp lfun lmatch) l)) - |Node(_,"TCLSOLVE",l) -> + | Node(_,"TCLSOLVE",l) -> VTactic (tclSOLVE (List.map (tac_interp lfun lmatch) l)) - |Node(loc0,"APPTACTIC",[Node(loc1,s,l)]) -> + | Node(loc0,"APPTACTIC",[Node(loc1,s,l)]) -> val_interp (evc,env,lfun,lmatch,goalopt) (Node(loc0,"APP",[Node(loc1, "PRIM-TACTIC",[Node(loc1,s,[])])]@l)) - |Node(_,"PRIM-TACTIC",[Node(loc,opn,[])]) -> + | Node(_,"PRIM-TACTIC",[Node(loc,opn,[])]) -> VFTactic ([],(interp_atomic loc opn)) - |Node(_,"VOID",[]) -> VVoid - |Nvar(_,s) -> - (try - (unrec (List.assoc s (List.rev lfun))) - with + | Node(_,"VOID",[]) -> VVoid + | Nvar(_,s) -> + (try + (unrec (List.assoc s (List.rev lfun))) + with Not_found -> (try (lookup s) with - Not_found -> VArg (Identifier (id_of_string s)))) - |Str(_,s) -> VArg (Quoted_string s) - |Num(_,n) -> VArg (Integer n) - |Node(_,"COMMAND",[c]) -> com_interp (evc,env,lfun,lmatch,goalopt) c - |Node(_,"CASTEDCOMMAND",[c]) -> + Not_found -> VArg (Identifier (id_of_string s)))) + | Str(_,s) -> VArg (Quoted_string s) + | Num(_,n) -> VArg (Integer n) + | Node(_,"COMMAND",[c]) -> com_interp (evc,env,lfun,lmatch,goalopt) c + | Node(_,"CASTEDCOMMAND",[c]) -> cast_com_interp (evc,env,lfun,lmatch,goalopt) c - |Node(_,"BINDINGS",astl) -> + | Node(_,"BINDINGS",astl) -> VArg (Cbindings (List.map (bind_interp evc env lfun lmatch goalopt) astl)) - |Node(_,"REDEXP",[Node(_,redname,args)]) -> + | Node(_,"REDEXP",[Node(_,redname,args)]) -> VArg (Redexp (redexp_of_ast (evc,env,lfun,lmatch,goalopt) (redname,args))) - |Node(_,"CLAUSE",cl) -> + | Node(_,"CLAUSE",cl) -> VArg (Clause (List.map (fun ast -> id_of_Identifier (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) ast))) cl)) - |Node(_,"TACTIC",[ast]) -> VArg (Tac (tac_interp lfun lmatch ast)) -(* Remains to treat *) - |Node(_,"FIXEXP", [Nvar(_,s); Num(_,n);Node(_,"COMMAND",[c])]) -> + | Node(_,"TACTIC",[ast]) -> VArg (Tac (tac_interp lfun lmatch ast)) +(*Remains to treat*) + | Node(_,"FIXEXP", [Nvar(_,s); Num(_,n);Node(_,"COMMAND",[c])]) -> VArg ((Fixexp (id_of_string s,n,c))) - |Node(_,"COFIXEXP", [Nvar(_,s); Node(_,"COMMAND",[c])]) -> + | Node(_,"COFIXEXP", [Nvar(_,s); Node(_,"COMMAND",[c])]) -> VArg ((Cofixexp (id_of_string s,c))) -(* End of Remains to treat *) - |Node(_,"INTROPATTERN", [ast]) -> +(*End of Remains to treat*) + | Node(_,"INTROPATTERN", [ast]) -> VArg ((Intropattern (cvt_intro_pattern (evc,env,lfun,lmatch,goalopt) ast))) - |Node(_,"LETPATTERNS",astl) -> + | Node(_,"LETPATTERNS",astl) -> VArg (Letpatterns (List.fold_left (cvt_letpattern (evc,env,lfun,lmatch,goalopt)) (None,[]) astl)) - |Node(loc,s,l) -> + | Node(loc,s,l) -> (try ((look_for_interp s) (evc,env,lfun,lmatch,goalopt) ast) with - Not_found -> - val_interp (evc,env,lfun,lmatch,goalopt) - (Node(dummy_loc,"APPTACTIC",[ast]))) - |_ -> + Not_found -> + val_interp (evc,env,lfun,lmatch,goalopt) + (Node(dummy_loc,"APPTACTIC",[ast]))) + | _ -> anomaly_loc (Ast.loc ast, "Tacinterp.val_interp",[<'sTR - "Unrecognizable ast: ";print_ast ast>]) + "Unrecognizable ast: "; print_ast ast>]) + (* Interprets an application node *) -and app_interp evc env lfun lmatch goalopt fv largs ast= +and app_interp evc env lfun lmatch goalopt fv largs ast = match fv with - VFTactic(l,f) -> VFTactic(l@(List.map unvarg largs),f) - |VFun(olfun,var,body) -> - let (newlfun,lvar,lval)=head_with_value (var,largs) - in - if lvar=[] then - if lval=[] then - val_interp (evc,env,(olfun@newlfun),lmatch,goalopt) body - else - app_interp evc env lfun lmatch goalopt (val_interp (evc,env, - (olfun@newlfun),lmatch,goalopt) body) lval ast + | VFTactic(l,f) -> VFTactic(l@(List.map unvarg largs),f) + | VFun(olfun,var,body) -> + let (newlfun,lvar,lval)=head_with_value (var,largs) in + if lvar=[] then + if lval=[] then + val_interp (evc,env,(olfun@newlfun),lmatch,goalopt) body else - VFun(olfun@newlfun,lvar,body) - |_ -> + app_interp evc env lfun lmatch goalopt (val_interp (evc,env, + (olfun@newlfun),lmatch,goalopt) body) lval ast + else + VFun(olfun@newlfun,lvar,body) + | _ -> anomaly_loc (Ast.loc ast, "Tacinterp.app_interp",[<'sTR "Illegal application: "; print_ast ast>]) + (* Interprets recursive expressions *) -and rec_interp evc env lfun lmatch goalopt ast=function - [Node(_,"RECCLAUSE",_)] as l -> - let (name,var,body)=List.hd (read_rec_clauses l) - and ve=ref VVoid - in - let newve= - VFun(lfun@[(name,VRec ve)],read_fun var,body) - in +and rec_interp evc env lfun lmatch goalopt ast = function + | [Node(_,"RECCLAUSE",_)] as l -> + let (name,var,body) = List.hd (read_rec_clauses l) + and ve = ref VVoid in + let newve = VFun(lfun@[(name,VRec ve)],read_fun var,body) in + begin ve:=newve; !ve - |[Node(_,"RECDECL",l);u] -> - let lrc=read_rec_clauses l - in - let lref=Array.to_list (Array.make (List.length lrc) (ref VVoid)) - in - let lenv= - List.fold_right2 (fun (name,_,_) vref l -> (name,VRec vref)::l) lrc - lref [] - in - let lve= - List.map (fun (name,var,body) -> (name,VFun(lfun@lenv,read_fun - var,body))) lrc - in - List.iter2 (fun vref (_,ve) -> vref:=ve) lref lve; - val_interp (evc,env,(lfun@lve),lmatch,goalopt) u - |_ -> + end + | [Node(_,"RECDECL",l);u] -> + let lrc = read_rec_clauses l in + let lref = Array.to_list (Array.make (List.length lrc) (ref VVoid)) in + let lenv = List.fold_right2 (fun (name,_,_) vref l -> (name,VRec vref)::l) + lrc lref [] in + let lve = List.map (fun (name,var,body) -> (name,VFun(lfun@lenv,read_fun + var,body))) lrc in + begin + List.iter2 (fun vref (_,ve) -> vref:=ve) lref lve; + val_interp (evc,env,(lfun@lve),lmatch,goalopt) u + end + | _ -> anomaly_loc (Ast.loc ast, "Tacinterp.rec_interp",[<'sTR "Rec not well formed: "; print_ast ast>]) + (* Interprets the clauses of a let *) -and let_interp evc env lfun lmatch goalopt ast=function - [] -> [] - |Node(_,"LETCLAUSE",[Nvar(_,id);t])::tl -> +and let_interp evc env lfun lmatch goalopt ast = function + | [] -> [] + | Node(_,"LETCLAUSE",[Nvar(_,id);t])::tl -> (id,val_interp (evc,env,lfun,lmatch,goalopt) t)::(let_interp evc env lfun lmatch goalopt ast tl) - |_ -> + | _ -> anomaly_loc (Ast.loc ast, "Tacinterp.let_interp",[<'sTR "Let not well formed: "; print_ast ast>]) + (* Interprets the Match Context expressions *) -and match_context_interp evc env lfun lmatch goalopt ast lmr= - let rec apply_match_context evc env lfun lmatch goalopt=function - (All t)::tl -> val_interp (evc,env,lfun,lmatch,goalopt) t - |(Pat (mhyps,mgoal,mt))::tl -> +and match_context_interp evc env lfun lmatch goalopt ast lmr = + let rec apply_match_context evc env lfun lmatch goalopt = function + | (All t)::tl -> val_interp (evc,env,lfun,lmatch,goalopt) t + | (Pat (mhyps,mgoal,mt))::tl -> (match goalopt with - None -> - errorlabstrm "Tacinterp.apply_match_context" [<'sTR - "No goal available">] - |Some g -> - let hyps=make_hyps (pf_hyps g) - and concl=pf_concl g - in + | None -> + errorlabstrm "Tacinterp.apply_match_context" [< 'sTR + "No goal available" >] + | Some g -> + let hyps = make_hyps (pf_hyps g) + and concl = pf_concl g in try - (let lgoal=apply_matching mgoal concl - in - if mhyps=[] then + (let lgoal = apply_matching mgoal concl in + if mhyps = [] then val_interp (evc,env,lfun,lgoal@lmatch,goalopt) mt else apply_hyps_context evc env lfun lmatch g mt lgoal mhyps hyps) with - No_match -> - apply_match_context evc env lfun lmatch goalopt tl) - |_ -> + No_match -> + apply_match_context evc env lfun lmatch goalopt tl) + | _ -> errorlabstrm "Tacinterp.apply_match_context" [<'sTR - "No matching clauses for Match Context">] - in - apply_match_context evc env lfun lmatch goalopt (read_match_context_rule - evc env lmr) + "No matching clauses for Match Context">] in + apply_match_context evc env lfun lmatch goalopt (read_match_context_rule evc + env lmr) + (* Tries to match the hypotheses in a Match Context *) and apply_hyps_context evc env lfun_glob lmatch_glob goal mt lgmatch mhyps - hyps= + hyps = let rec apply_hyps_context_rec evc env lfun_glob lmatch_glob goal mt lfun - lmatch mhyps hyps hyps_acc= + lmatch mhyps hyps hyps_acc = match hyps with - hd::tl -> + | hd::tl -> (try - (let (lid,lm,newmhyps)=apply_one_hyp_context lmatch mhyps hd - in - if newmhyps=[] then + (let (lid,lm,newmhyps) = apply_one_hyp_context lmatch mhyps hd in + if newmhyps = [] then match (val_interp (evc,env,(lfun@lid@lfun_glob), (lmatch@lm@lmatch_glob),Some goal) mt) with - VTactic tac -> VRTactic (tac goal) - |VFTactic (largs,f) -> VRTactic (f largs goal) - |a -> a + | VTactic tac -> VRTactic (tac goal) + | VFTactic (largs,f) -> VRTactic (f largs goal) + | a -> a else apply_hyps_context_rec evc env lfun_glob lmatch_glob goal mt (lfun@lid) (lmatch@lm) newmhyps (hyps_acc@tl) []) with - No_match | _ -> - apply_hyps_context_rec evc env lfun_glob lmatch_glob goal mt - lfun lmatch mhyps tl (hyps_acc@[hd])) - |[] -> raise No_match - in - apply_hyps_context_rec evc env lfun_glob lmatch_glob goal mt [] lgmatch - mhyps hyps [] + No_match | _ -> + apply_hyps_context_rec evc env lfun_glob lmatch_glob goal mt + lfun lmatch mhyps tl (hyps_acc@[hd])) + | [] -> raise No_match in + apply_hyps_context_rec evc env lfun_glob lmatch_glob goal mt [] lgmatch mhyps + hyps [] + (* Interprets the Match expressions *) -and match_interp evc env lfun lmatch goalopt ast lmr= - let rec apply_match evc env lfun lmatch goalopt csr=function - (All t)::tl -> val_interp (evc,env,lfun,lmatch,goalopt) t - |(Pat ([],mc,mt))::tl -> +and match_interp evc env lfun lmatch goalopt ast lmr = + let rec apply_match evc env lfun lmatch goalopt csr = function + | (All t)::tl -> val_interp (evc,env,lfun,lmatch,goalopt) t + | (Pat ([],mc,mt))::tl -> (try - (let lcsr=apply_matching mc csr - in + (let lcsr = apply_matching mc csr in val_interp (evc,env,lfun,(apply_matching mc csr)@lmatch,goalopt) mt) with - No_match -> apply_match evc env lfun lmatch goalopt csr tl) - |_ -> + No_match -> apply_match evc env lfun lmatch goalopt csr tl) + | _ -> errorlabstrm "Tacinterp.apply_match" [<'sTR - "No matching clauses for Match">] - in - let csr= - constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) - (List.hd lmr))) - and ilr=read_match_rule evc env (List.tl lmr) - in - apply_match evc env lfun lmatch goalopt csr ilr + "No matching clauses for Match">] in + let csr = constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) + (List.hd lmr))) + and ilr = read_match_rule evc env (List.tl lmr) in + apply_match evc env lfun lmatch goalopt csr ilr + (* Interprets tactic expressions *) -and tac_interp lfun lmatch ast g= - let evc=project g - and env=pf_env g - in +and tac_interp lfun lmatch ast g = + let evc = project g + and env = pf_env g in match (val_interp (evc,env,lfun,lmatch,(Some g)) ast) with - VTactic tac -> (tac g) - |VFTactic (largs,f) -> (f largs g) - |VRTactic res -> res - |_ -> + | VTactic tac -> (tac g) + | VFTactic (largs,f) -> (f largs g) + | VRTactic res -> res + | _ -> errorlabstrm "Tacinterp.interp_rec" [<'sTR "Interpretation gives a non-tactic value">] + (* Interprets a primitive tactic *) -and interp_atomic loc opn args=vernac_tactic(opn,args) +and interp_atomic loc opn args = vernac_tactic(opn,args) + (* Interprets sequences of tactics *) -and interp_semi_list acc lfun lmatch=function - (Node(_,"TACLIST",seq))::l -> - interp_semi_list (tclTHENS acc (List.map (tac_interp lfun lmatch) seq)) - lfun lmatch l - |t::l -> +and interp_semi_list acc lfun lmatch = function + | (Node(_,"TACLIST",seq))::l -> + interp_semi_list (tclTHENS acc (List.map (tac_interp lfun lmatch) seq)) + lfun lmatch l + | t::l -> interp_semi_list (tclTHEN acc (tac_interp lfun lmatch t)) lfun lmatch l - |[] -> acc + | [] -> acc + (* Interprets bindings for tactics *) -and bind_interp evc env lfun lmatch goalopt=function - Node(_,"BINDING", [Num(_,n);Node(loc,"COMMAND",[c])]) -> - (NoDep n,constr_of_Constr (unvarg (val_interp - (evc,env,lfun,lmatch,goalopt) (Node(loc,"COMMAND",[c]))))) - |Node(_,"BINDING", [Nvar(loc0,s); Node(loc1,"COMMAND",[c])]) -> - (Dep (id_of_Identifier (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) +and bind_interp evc env lfun lmatch goalopt = function + | Node(_,"BINDING", [Num(_,n);Node(loc,"COMMAND",[c])]) -> + (NoDep n,constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) + (Node(loc,"COMMAND",[c]))))) + | Node(_,"BINDING", [Nvar(loc0,s); Node(loc1,"COMMAND",[c])]) -> + (Dep (id_of_Identifier (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) (Nvar(loc0,s))))),constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) (Node(loc1,"COMMAND",[c]))))) - |Node(_,"BINDING", [Node(loc,"COMMAND",[c])]) -> + | Node(_,"BINDING", [Node(loc,"COMMAND",[c])]) -> (Com,constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) - (Node(loc,"COMMAND",[c]))))) - |x -> + (Node(loc,"COMMAND",[c]))))) + | x -> errorlabstrm "bind_interp" [<'sTR "Not the expected form in binding"; print_ast x>] + (* Interprets a COMMAND expression *) -and com_interp (evc,env,lfun,lmatch,goalopt)=function - Node(_,"EVAL",[c;rtc]) -> - let redexp= - unredexp (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) rtc)) - in - VArg (Constr ((reduction_of_redexp redexp) env evc (interp_constr1 evc - env (make_subs_list lfun) lmatch c))) - |c -> VArg (Constr (interp_constr1 evc env (make_subs_list lfun) lmatch c)) +and com_interp (evc,env,lfun,lmatch,goalopt) = function + | Node(_,"EVAL",[c;rtc]) -> + let redexp = unredexp (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) + rtc)) in + VArg (Constr ((reduction_of_redexp redexp) env evc (interp_constr1 evc env + (make_subs_list lfun) lmatch c))) + | c -> VArg (Constr (interp_constr1 evc env (make_subs_list lfun) lmatch c)) + (* Interprets a CASTEDCOMMAND expression *) -and cast_com_interp (evc,env,lfun,lmatch,goalopt) com= +and cast_com_interp (evc,env,lfun,lmatch,goalopt) com = match goalopt with Some gl -> (match com with - Node(_,"EVAL",[c;rtc]) -> - let redexp= - unredexp (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) rtc)) - in - VArg (Constr ((reduction_of_redexp redexp) env evc - (interp_casted_constr1 evc env (make_subs_list lfun) lmatch - c (pf_concl gl)))) - |c -> + | Node(_,"EVAL",[c;rtc]) -> + let redexp = unredexp (unvarg (val_interp + (evc,env,lfun,lmatch,goalopt) rtc)) in + VArg (Constr ((reduction_of_redexp redexp) env evc + (interp_casted_constr1 evc env (make_subs_list lfun) lmatch c + (pf_concl gl)))) + | c -> VArg (Constr (interp_casted_constr1 evc env (make_subs_list lfun) lmatch c (pf_concl gl)))) - |None -> + | None -> errorlabstrm "val_interp" [<'sTR "Cannot cast a constr without goal">] -and cvt_pattern (evc,env,lfun,lmatch,goalopt)=function - Node(_,"PATTERN", Node(loc,"COMMAND",[com])::nums) -> - let occs=List.map num_of_ast nums - and csr= - constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) - (Node(loc,"COMMAND",[com])))) - in - let jdt=Typing.unsafe_machine env evc csr - in - (occs, jdt.Environ.uj_val, body_of_type jdt.Environ.uj_type) - |arg -> invalid_arg_loc (Ast.loc arg,"cvt_pattern") -and cvt_unfold (evc,env,lfun,lmatch,goalopt)=function - Node(_,"UNFOLD", com::nums) -> - (List.map num_of_ast nums,glob_nvar (id_of_Identifier (unvarg (val_interp + +and cvt_pattern (evc,env,lfun,lmatch,goalopt) = function + | Node(_,"PATTERN", Node(loc,"COMMAND",[com])::nums) -> + let occs = List.map num_of_ast nums + and csr = constr_of_Constr (unvarg (val_interp + (evc,env,lfun,lmatch,goalopt) (Node(loc,"COMMAND",[com])))) in + let jdt = Typing.unsafe_machine env evc csr in + (occs, jdt.Environ.uj_val, body_of_type jdt.Environ.uj_type) + | arg -> invalid_arg_loc (Ast.loc arg,"cvt_pattern") + +and cvt_unfold (evc,env,lfun,lmatch,goalopt) = function + | Node(_,"UNFOLD", com::nums) -> + (List.map num_of_ast nums,glob_nvar (id_of_Identifier (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) com)))) - |arg -> invalid_arg_loc (Ast.loc arg,"cvt_unfold") + | arg -> invalid_arg_loc (Ast.loc arg,"cvt_unfold") + (* Interprets the arguments of Fold *) -and cvt_fold (evc,env,lfun,lmatch,goalopt)=function - Node(_,"COMMAND",[c]) as ast -> - constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) ast)) - |arg -> invalid_arg_loc (Ast.loc arg,"cvt_fold") +and cvt_fold (evc,env,lfun,lmatch,goalopt) = function + | Node(_,"COMMAND",[c]) as ast -> + constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) ast)) + | arg -> invalid_arg_loc (Ast.loc arg,"cvt_fold") + (* Interprets the reduction flags *) -and flag_of_ast (evc,env,lfun,lmatch,goalopt) lf= +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(_,"Beta",[]) -> beta := true | Node(_,"Delta",[]) -> delta := true | Node(_,"Iota",[]) -> iota := true | Node(loc,"Unf",l) -> @@ -623,9 +616,9 @@ and flag_of_ast (evc,env,lfun,lmatch,goalopt) lf= | Abst sp -> List.mem sp idl | _ -> false) else user_err_loc(loc,"flag_of_ast", - [< 'sTR"Cannot specify identifiers to unfold twice" >]) + [<'sTR "Cannot specify identifiers to unfold twice">]) else user_err_loc(loc,"flag_of_ast", - [< 'sTR"Delta must be specified before" >]) + [<'sTR "Delta must be specified before">]) | Node(loc,"UnfBut",l) -> if !delta then if !idents = None then @@ -639,9 +632,9 @@ and flag_of_ast (evc,env,lfun,lmatch,goalopt) lf= | Abst sp -> not (List.mem sp idl) | _ -> false) else user_err_loc(loc,"flag_of_ast", - [< 'sTR"Cannot specify identifiers to unfold twice" >]) + [<'sTR "Cannot specify identifiers to unfold twice">]) else user_err_loc(loc,"flag_of_ast", - [< 'sTR"Delta must be specified before" >]) + [<'sTR "Delta must be specified before">]) | arg -> invalid_arg_loc (Ast.loc arg,"flag_of_ast") in List.iter set_flag lf; @@ -651,51 +644,54 @@ and flag_of_ast (evc,env,lfun,lmatch,goalopt) lf= (false,_) -> (fun _ -> false) | (true,None) -> (fun _ -> true) | (true,Some p) -> p } + (* Interprets a reduction expression *) -and redexp_of_ast (evc,env,lfun,lmatch,goalopt)=function - |("Red", []) -> Red - |("Hnf", []) -> Hnf - |("Simpl", []) -> Simpl - |("Unfold", ul) -> +and redexp_of_ast (evc,env,lfun,lmatch,goalopt) = function + | ("Red", []) -> Red + | ("Hnf", []) -> Hnf + | ("Simpl", []) -> Simpl + | ("Unfold", ul) -> Unfold (List.map (cvt_unfold (evc,env,lfun,lmatch,goalopt)) ul) - |("Fold", cl) -> Fold (List.map (cvt_fold (evc,env,lfun,lmatch,goalopt)) cl) - |("Cbv",lf) -> Cbv(UNIFORM, flag_of_ast (evc,env,lfun,lmatch,goalopt) lf) - |("Lazy",lf) -> Lazy(UNIFORM, flag_of_ast (evc,env,lfun,lmatch,goalopt) lf) - |("Pattern",lp) -> + | ("Fold", cl) -> Fold (List.map (cvt_fold (evc,env,lfun,lmatch,goalopt)) cl) + | ("Cbv",lf) -> Cbv(UNIFORM, flag_of_ast (evc,env,lfun,lmatch,goalopt) lf) + | ("Lazy",lf) -> Lazy(UNIFORM, flag_of_ast (evc,env,lfun,lmatch,goalopt) lf) + | ("Pattern",lp) -> Pattern (List.map (cvt_pattern (evc,env,lfun,lmatch,goalopt)) lp) - |(s,_) -> invalid_arg ("malformed reduction-expression: "^s) + | (s,_) -> invalid_arg ("malformed reduction-expression: "^s) + (* Interprets the patterns of Intro *) -and cvt_intro_pattern (evc,env,lfun,lmatch,goalopt)=function - Node(_,"IDENTIFIER", [Nvar(loc,s)]) -> - IdPat (id_of_Identifier (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) - (Nvar (loc,s))))) - |Node(_,"DISJPATTERN", l) -> +and cvt_intro_pattern (evc,env,lfun,lmatch,goalopt) = function + | Node(_,"IDENTIFIER", [Nvar(loc,s)]) -> + IdPat (id_of_Identifier (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) + (Nvar (loc,s))))) + | Node(_,"DISJPATTERN", l) -> DisjPat (List.map (cvt_intro_pattern (evc,env,lfun,lmatch,goalopt)) l) - |Node(_,"CONJPATTERN", l) -> + | Node(_,"CONJPATTERN", l) -> ConjPat (List.map (cvt_intro_pattern (evc,env,lfun,lmatch,goalopt)) l) - |Node(_,"LISTPATTERN", l) -> + | Node(_,"LISTPATTERN", l) -> ListPat (List.map (cvt_intro_pattern (evc,env,lfun,lmatch,goalopt)) l) - |x -> + | x -> errorlabstrm "cvt_intro_pattern" - [<'sTR "Not the expected form for an introduction pattern!";print_ast - x>] + [<'sTR "Not the expected form for an introduction pattern!"; print_ast + x>] + (* Interprets a pattern of Let *) -and cvt_letpattern (evc,env,lfun,lmatch,goalopt) (o,l)=function - Node(_,"HYPPATTERN", Nvar(loc,s)::nums) -> - (o,(id_of_Identifier (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) +and cvt_letpattern (evc,env,lfun,lmatch,goalopt) (o,l) = function + | Node(_,"HYPPATTERN", Nvar(loc,s)::nums) -> + (o,(id_of_Identifier (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) (Nvar (loc,s)))),List.map num_of_ast nums)::l) - |Node(_,"CCLPATTERN", nums) -> - if o<>None then + | Node(_,"CCLPATTERN", nums) -> + if o <> None then error "\"Goal\" occurs twice" else (Some (List.map num_of_ast nums), l) - |arg -> invalid_arg_loc (Ast.loc arg,"cvt_hyppattern") + | arg -> invalid_arg_loc (Ast.loc arg,"cvt_hyppattern") (* Interprets tactic arguments *) -let interp_tacarg sign ast=unvarg (val_interp sign ast) +let interp_tacarg sign ast = unvarg (val_interp sign ast) (* Initial call for interpretation *) -let interp=tac_interp [] [] +let interp = tac_interp [] [] let is_just_undef_macro ast = match ast with @@ -725,4 +721,4 @@ let vernac_interp_atomic = let bad_tactic_args s = anomalylabstrm s - [< 'sTR"Tactic "; 'sTR s; 'sTR" called with bad arguments" >] + [<'sTR "Tactic "; 'sTR s; 'sTR " called with bad arguments">] diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli index 9f82d30e7..4405f0d22 100644 --- a/proofs/tacinterp.mli +++ b/proofs/tacinterp.mli @@ -30,13 +30,12 @@ type interp_sign = (* Adds a Tactic Definition in the table *) val add_tacdef : string -> value -> unit -(*Interprets any expression *) +(* Interprets any expression *) val val_interp : interp_sign -> Coqast.t -> value (* Interprets tactic arguments *) val interp_tacarg : interp_sign -> Coqast.t -> tactic_arg - val interp : Coqast.t -> tactic val vernac_interp : Coqast.t -> tactic val vernac_interp_atomic : identifier -> tactic_arg list -> tactic diff --git a/tactics/auto.ml b/tactics/auto.ml index 2a98b8e2f..067d610fe 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -510,7 +510,7 @@ let fmt_hint_term cl = in if valid_dbs = [] then [<'sTR "No hint applicable for current goal" >] - else + else [< 'sTR "Applicable Hints :"; prlist (fun (name,db,hintlist) -> [< 'sTR " In the database "; 'sTR name; diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 69d4e59c6..74d49114b 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -16,8 +16,7 @@ open Pattern open Clenv open Auto -let e_give_exact c gl = - tclTHEN (unify (pf_type_of gl c)) (Tactics.exact c) gl +let e_give_exact c gl = tclTHEN (unify (pf_type_of gl c)) (Tactics.exact c) gl let assumption id = e_give_exact (VAR id) |