diff options
-rw-r--r-- | contrib/interface/Centaur.v | 3 | ||||
-rw-r--r-- | contrib/interface/ascent.mli | 23 | ||||
-rwxr-xr-x | contrib/interface/blast.ml | 627 | ||||
-rw-r--r-- | contrib/interface/blast.mli | 5 | ||||
-rw-r--r-- | contrib/interface/centaur.ml | 124 | ||||
-rw-r--r-- | contrib/interface/parse.ml | 202 | ||||
-rw-r--r-- | contrib/interface/pbp.ml | 50 | ||||
-rw-r--r-- | contrib/interface/vernacrc | 1 | ||||
-rw-r--r-- | contrib/interface/vtp.ml | 48 | ||||
-rw-r--r-- | contrib/interface/xlate.ml | 248 |
10 files changed, 1039 insertions, 292 deletions
diff --git a/contrib/interface/Centaur.v b/contrib/interface/Centaur.v index 5cca616a5..654cf123f 100644 --- a/contrib/interface/Centaur.v +++ b/contrib/interface/Centaur.v @@ -5,6 +5,7 @@ Declare ML Module "xlate". Declare ML Module "vtp". Declare ML Module "translate". Declare ML Module "pbp". +Declare ML Module "blast". Declare ML Module "dad". Declare ML Module "showproof_ct". Declare ML Module "showproof". @@ -55,6 +56,8 @@ Grammar tactic simple_tactic : ast := | pbp2 [ "Pbp" identarg($id) ] -> [ (PcoqPbp $id) ] | pbp3 [ "Pbp" identarg($id) ne_num_list($ns)] -> [ (PcoqPbp $id ($LIST $ns)) ] +| blast1 [ "Blast" ne_num_list($ns) ] -> + [ (PcoqBlast ($LIST $ns)) ] | dad00 [ "Dad" "to" ] -> [(Dad (TACTIC (to)))] | dad01 [ "Dad" "to" ne_num_list($ns) ] -> [(Dad (TACTIC (to)) ($LIST $ns))] diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli index 3b9d742e2..4527f6608 100644 --- a/contrib/interface/ascent.mli +++ b/contrib/interface/ascent.mli @@ -1,4 +1,3 @@ - type ct_ASSOC = CT_coerce_NONE_to_ASSOC of ct_NONE | CT_lefta @@ -169,7 +168,9 @@ and ct_CONTEXT_RULE = and ct_CONVERSION_FLAG = CT_beta | CT_delta + | CT_evar | CT_iota + | CT_zeta and ct_CONVERSION_FLAG_LIST = CT_conversion_flag_list of ct_CONVERSION_FLAG list and ct_CONV_SET = @@ -183,8 +184,8 @@ and ct_DEFN_OR_THM = CT_coerce_DEFN_to_DEFN_OR_THM of ct_DEFN | CT_coerce_THM_to_DEFN_OR_THM of ct_THM and ct_DEF_BODY = - CT_coerce_EVAL_CMD_to_DEF_BODY of ct_EVAL_CMD - | CT_coerce_FORMULA_to_DEF_BODY of ct_FORMULA + CT_coerce_CONTEXT_PATTERN_to_DEF_BODY of ct_CONTEXT_PATTERN + | CT_coerce_EVAL_CMD_to_DEF_BODY of ct_EVAL_CMD and ct_DEP = CT_dep of string and ct_DESTRUCTING = @@ -226,7 +227,6 @@ and ct_FORMULA = | CT_int_encapsulator of ct_INT | CT_lambdac of ct_BINDER * ct_FORMULA | CT_letin of ct_ID * ct_FORMULA * ct_FORMULA - | CT_metac of ct_INT | CT_prodc of ct_BINDER * ct_FORMULA and ct_FORMULA_LIST = CT_formula_list of ct_FORMULA list @@ -245,6 +245,7 @@ and ct_HINT_EXPRESSION = | CT_unfold_hint of ct_ID and ct_ID = CT_ident of string + | CT_metac of ct_INT and ct_IDENTITY_OPT = CT_coerce_NONE_to_IDENTITY_OPT of ct_NONE | CT_identity @@ -307,6 +308,13 @@ and ct_IN_OR_OUT_MODULES = CT_coerce_NONE_to_IN_OR_OUT_MODULES of ct_NONE | CT_in_modules of ct_ID_NE_LIST | CT_out_modules of ct_ID_NE_LIST +and ct_LET_CLAUSE = + CT_let_clause of ct_ID * ct_LET_VALUE +and ct_LET_CLAUSES = + CT_let_clauses of ct_LET_CLAUSE * ct_LET_CLAUSE list +and ct_LET_VALUE = + CT_coerce_DEF_BODY_to_LET_VALUE of ct_DEF_BODY + | CT_coerce_TACTIC_COM_to_LET_VALUE of ct_TACTIC_COM and ct_LOCAL_OPT = CT_coerce_NONE_to_LOCAL_OPT of ct_NONE | CT_local @@ -318,6 +326,10 @@ and ct_MATCH_PATTERN = | CT_pattern_as of ct_MATCH_PATTERN * ct_ID_OPT and ct_MATCH_PATTERN_NE_LIST = CT_match_pattern_ne_list of ct_MATCH_PATTERN * ct_MATCH_PATTERN list +and ct_MATCH_TAC_RULE = + CT_match_tac_rule of ct_CONTEXT_PATTERN * ct_LET_VALUE +and ct_MATCH_TAC_RULES = + CT_match_tac_rules of ct_MATCH_TAC_RULE * ct_MATCH_TAC_RULE list and ct_NATURAL_FEATURE = CT_contractible | CT_implicit @@ -460,8 +472,9 @@ and ct_TACTIC_COM = | CT_intros_until of ct_ID | CT_inversion of ct_INV_TYPE * ct_ID * ct_ID_LIST | CT_left of ct_SPEC_LIST - | CT_lettac of ct_ID * ct_FORMULA * ct_UNFOLD_NE_LIST + | CT_lettac of ct_LET_CLAUSES * ct_LET_VALUE | CT_match_context of ct_CONTEXT_RULE * ct_CONTEXT_RULE list + | CT_match_tac of ct_LET_VALUE * ct_MATCH_TAC_RULES | CT_move_after of ct_ID * ct_ID | CT_omega | CT_orelse of ct_TACTIC_COM * ct_TACTIC_COM diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml new file mode 100755 index 000000000..104051b2d --- /dev/null +++ b/contrib/interface/blast.ml @@ -0,0 +1,627 @@ +(* Une tactique qui tente de démontrer toute seule le but courant, + interruptible par pcoq (si dans le fichier C:\WINDOWS\free il y a un A) +*) +open Ctast;; +open Termops;; +open Nameops;; +open Astterm;; +open Auto;; +open Clenv;; +open Command;; +open Ctast;; +open Declarations;; +open Declare;; +open Eauto;; +open Environ;; +open Equality;; +open Evd;; +open Hipattern;; +open Inductive;; +open Names;; +open Pattern;; +open Pbp;; +open Pfedit;; +open Pp;; +open Printer +open Proof_trees;; +open Proof_type;; +open Rawterm;; +open Reduction;; +open Refiner;; +open Sign;; +open String;; +open Tacmach;; +open Tacred;; +open Tacticals;; +open Tactics;; +open Term;; +open Typing;; +open Util;; +open Vernacentries;; +open Vernacinterp;; +open Evar_refiner;; + + +let parse_com = Pcoq.parse_string Pcoq.Constr.constr;; +let parse_tac t = + try (Pcoq.parse_string Pcoq.Tactic.tactic t) + with _ -> (msgnl (hov 0 (str"pas parsé: " ++ str t)); + failwith "tactic") +;; + +let is_free () = + let st =open_in_bin ((Sys.getenv "HOME")^"/.free") in + let c=input_char st in + close_in st; + c = 'A' +;; + +(* marche pas *) +(* +let is_free () = + msgnl (hov 0 [< 'str"Isfree========= "; 'fNL >]); + let s = Stream.of_channel stdin in + msgnl (hov 0 [< 'str"Isfree s "; 'fNL >]); + try (Stream.empty s; + msgnl (hov 0 [< 'str"Isfree empty "; 'fNL >]); + true) + with _ -> (msgnl (hov 0 [< 'str"Isfree not empty "; 'fNL >]); + false) +;; +*) +let free_try tac g = + if is_free() + then (tac g) + else (failwith "not free") +;; +let adrel (x,t) e = + match x with + Name(xid) -> Environ.push_rel (x,None,t) e + | Anonymous -> Environ.push_rel (x,None,t) e +(* les constantes ayant une définition apparaissant dans x *) +let rec def_const_in_term_rec vl x = + match (kind_of_term x) with + Prod(n,t,c)-> + let vl = (adrel (n,t) vl) in def_const_in_term_rec vl c + | Lambda(n,t,c) -> + let vl = (adrel (n,t) vl) in def_const_in_term_rec vl c + | App(f,args) -> def_const_in_term_rec vl f + | Sort(Prop(Null)) -> Prop(Null) + | Sort(c) -> c + | Ind(ind) -> + let (mib, mip) = Global.lookup_inductive ind in + mip.mind_sort + | Construct(c) -> + def_const_in_term_rec vl (mkInd (inductive_of_constructor c)) + | Case(_,x,t,a) + -> def_const_in_term_rec vl x + | Cast(x,t)-> def_const_in_term_rec vl t + | Const(c) -> def_const_in_term_rec vl (lookup_constant c vl).const_type + | _ -> def_const_in_term_rec vl (type_of vl Evd.empty x) +;; +let def_const_in_term_ x = + def_const_in_term_rec (Global.env()) (strip_outer_cast x) +;; +(************************************************************************* + recopiés de refiner.ml, car print_subscript pas exportée dans refiner.mli + modif de print_info_script avec pr_bar +*) + +let pr_bar () = str "|" + +let rec print_info_script sigma osign pf = + let {evar_hyps=sign; evar_concl=cl} = pf.goal in + match pf.ref with + | None -> [< >] + | Some(r,spfl) -> + pr_rule r ++ + match spfl with + | [] -> + (str " " ++ fnl()) + | [pf1] -> + if pf1.ref = None then + (str " " ++ fnl()) + else + (str";" ++ brk(1,3) ++ + print_info_script sigma sign pf1) + | _ -> ( str";[" ++ fnl() ++ + prlist_with_sep pr_bar + (print_info_script sigma sign) spfl ++ + str"]") + +let format_print_info_script sigma osign pf = + hov 0 (print_info_script sigma osign pf) + +let print_subscript sigma sign pf = + (* if is_tactic_proof pf then + format_print_info_script sigma sign (subproof_of_proof pf) + else *) + format_print_info_script sigma sign pf +(****************) + +let pp_string x = + msgnl_with Format.str_formatter x; + Format.flush_str_formatter () +;; + +(*********************************************************************** + copié de tactics/eauto.ml +*) + +(***************************************************************************) +(* A tactic similar to Auto, but using EApply, Assumption and e_give_exact *) +(***************************************************************************) + +let unify_e_resolve (c,clenv) gls = + let (wc,kONT) = startWalk gls in + let clenv' = connect_clenv wc clenv in + let _ = clenv_unique_resolver false clenv' gls in + vernac_e_resolve_constr c gls + +let rec e_trivial_fail_db db_list local_db goal = + let tacl = + registered_e_assumption :: + (tclTHEN Tactics.intro + (function g'-> + let d = pf_last_hyp g' in + let hintl = make_resolve_hyp (pf_env g') (project g') d in + (e_trivial_fail_db db_list + (Hint_db.add_list hintl local_db) g'))) :: + (List.map fst (e_trivial_resolve db_list local_db (pf_concl goal)) ) + in + tclFIRST (List.map tclCOMPLETE tacl) goal + +and e_my_find_search db_list local_db hdc concl = + let hdc = head_of_constr_reference hdc in + let hintl = + if occur_existential concl then + list_map_append (Hint_db.map_all hdc) (local_db::db_list) + else + list_map_append (Hint_db.map_auto (hdc,concl)) (local_db::db_list) + in + let tac_of_hint = + fun ({pri=b; pat = p; code=t} as patac) -> + (b, + let tac = + match t with + | Res_pf (term,cl) -> unify_resolve (term,cl) + | ERes_pf (term,cl) -> unify_e_resolve (term,cl) + | Give_exact (c) -> e_give_exact_constr c + | Res_pf_THEN_trivial_fail (term,cl) -> + tclTHEN (unify_e_resolve (term,cl)) + (e_trivial_fail_db db_list local_db) + | Unfold_nth c -> unfold_constr c + | Extern tacast -> Tacticals.conclPattern concl + (out_some p) tacast + in + (free_try tac,fmt_autotactic t)) + (*i + fun gls -> pPNL (fmt_autotactic t); Format.print_flush (); + try tac gls + with e when Logic.catchable_exception(e) -> + (Format.print_string "Fail\n"; + Format.print_flush (); + raise e) + i*) + in + List.map tac_of_hint hintl + +and e_trivial_resolve db_list local_db gl = + try + Auto.priority + (e_my_find_search db_list local_db + (List.hd (head_constr_bound gl [])) gl) + with Bound | Not_found -> [] + +let e_possible_resolve db_list local_db gl = + try List.map snd (e_my_find_search db_list local_db + (List.hd (head_constr_bound gl [])) gl) + with Bound | Not_found -> [] + +let assumption_tac_list id = apply_tac_list (e_give_exact_constr (mkVar id)) + +let find_first_goal gls = + try first_goal gls with UserError _ -> assert false + +(*s The following module [SearchProblem] is used to instantiate the generic + exploration functor [Explore.Make]. *) + +module MySearchProblem = struct + + type state = { + depth : int; (*r depth of search before failing *) + tacres : goal list sigma * validation; + last_tactic : std_ppcmds; + dblist : Auto.Hint_db.t list; + localdb : Auto.Hint_db.t list } + + let success s = (sig_it (fst s.tacres)) = [] + + let rec filter_tactics (glls,v) = function + | [] -> [] + | (tac,pptac) :: tacl -> + try + let (lgls,ptl) = apply_tac_list tac glls in + let v' p = v (ptl p) in + ((lgls,v'),pptac) :: filter_tactics (glls,v) tacl + with e when Logic.catchable_exception e -> + filter_tactics (glls,v) tacl + + let rec list_addn n x l = + if n = 0 then l else x :: (list_addn (pred n) x l) + + (* Ordering of states is lexicographic on depth (greatest first) then + number of remaining goals. *) + let compare s s' = + let d = s'.depth - s.depth in + let nbgoals s = List.length (sig_it (fst s.tacres)) in + if d <> 0 then d else nbgoals s - nbgoals s' + + let branching s = + if s.depth = 0 then + [] + else + let lg = fst s.tacres in + let nbgl = List.length (sig_it lg) in + assert (nbgl > 0); + let g = find_first_goal lg in + let assumption_tacs = + let l = + filter_tactics s.tacres + (List.map + (fun id -> (e_give_exact_constr (mkVar id), + (str "Exact" ++ spc()++ pr_id id))) + (pf_ids_of_hyps g)) + in + List.map (fun (res,pp) -> { depth = s.depth; tacres = res; + last_tactic = pp; dblist = s.dblist; + localdb = List.tl s.localdb }) l + in + let intro_tac = + List.map + (fun ((lgls,_) as res,pp) -> + let g' = first_goal lgls in + let hintl = + make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g') + in + let ldb = Hint_db.add_list hintl (List.hd s.localdb) in + { depth = s.depth; tacres = res; + last_tactic = pp; dblist = s.dblist; + localdb = ldb :: List.tl s.localdb }) + (filter_tactics s.tacres [Tactics.intro,(str "Intro" )]) + in + let rec_tacs = + let l = + filter_tactics s.tacres + (e_possible_resolve s.dblist (List.hd s.localdb) (pf_concl g)) + in + List.map + (fun ((lgls,_) as res, pp) -> + let nbgl' = List.length (sig_it lgls) in + if nbgl' < nbgl then + { depth = s.depth; tacres = res; last_tactic = pp; + dblist = s.dblist; localdb = List.tl s.localdb } + else + { depth = pred s.depth; tacres = res; + dblist = s.dblist; last_tactic = pp; + localdb = + list_addn (nbgl'-nbgl) (List.hd s.localdb) s.localdb }) + l + in + List.sort compare (assumption_tacs @ intro_tac @ rec_tacs) + + let pp s = + msg (hov 0 (str " depth="++ int s.depth ++ spc() ++ + s.last_tactic ++ str "\n")) + +end + +module MySearch = Explore.Make(MySearchProblem) + +let make_initial_state n gl dblist localdb = + { MySearchProblem.depth = n; + MySearchProblem.tacres = tclIDTAC gl; + MySearchProblem.last_tactic = [< >]; + MySearchProblem.dblist = dblist; + MySearchProblem.localdb = [localdb] } + +let e_depth_search debug p db_list local_db gl = + try + let tac = if debug then MySearch.debug_depth_first else MySearch.depth_first in + let s = tac (make_initial_state p gl db_list local_db) in + s.MySearchProblem.tacres + with Not_found -> error "EAuto: depth first search failed" + +let e_breadth_search debug n db_list local_db gl = + try + let tac = + if debug then MySearch.debug_breadth_first else MySearch.breadth_first + in + let s = tac (make_initial_state n gl db_list local_db) in + s.MySearchProblem.tacres + with Not_found -> error "EAuto: breadth first search failed" + +let e_search_auto debug (n,p) db_list gl = + let local_db = make_local_hint_db gl in + if n = 0 then + e_depth_search debug p db_list local_db gl + else + e_breadth_search debug n db_list local_db gl + +let eauto debug np dbnames = + let db_list = + List.map + (fun x -> + try Stringmap.find x !searchtable + with Not_found -> error ("EAuto: "^x^": No such Hint database")) + ("core"::dbnames) + in + tclTRY (e_search_auto debug np db_list) + +let full_eauto debug n gl = + let dbnames = stringmap_dom !searchtable in + let dbnames = list_subtract dbnames ["v62"] in + let db_list = List.map (fun x -> Stringmap.find x !searchtable) dbnames in + let local_db = make_local_hint_db gl in + tclTRY (e_search_auto debug n db_list) gl + +let my_full_eauto n gl = full_eauto false (n,0) gl + +(********************************************************************** + copié de tactics/auto.ml on a juste modifié search_gen +*) +let searchtable_map name = + Stringmap.find name !searchtable + +(* local_db is a Hint database containing the hypotheses of current goal *) +(* Papageno : cette fonction a été pas mal simplifiée depuis que la base + de Hint impérative a été remplacée par plusieurs bases fonctionnelles *) + +let rec trivial_fail_db db_list local_db gl = + let intro_tac = + tclTHEN intro + (fun g'-> + let hintl = make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g') + in trivial_fail_db db_list (Hint_db.add_list hintl local_db) g') + in + tclFIRST + (assumption::intro_tac:: + (List.map tclCOMPLETE + (trivial_resolve db_list local_db (pf_concl gl)))) gl + +and my_find_search db_list local_db hdc concl = + let tacl = + if occur_existential concl then + list_map_append (fun db -> Hint_db.map_all hdc db) (local_db::db_list) + else + list_map_append (fun db -> Hint_db.map_auto (hdc,concl) db) + (local_db::db_list) + in + List.map + (fun ({pri=b; pat=p; code=t} as patac) -> + (b, + match t with + | Res_pf (term,cl) -> unify_resolve (term,cl) + | ERes_pf (_,c) -> (fun gl -> error "eres_pf") + | Give_exact c -> exact_no_check c + | Res_pf_THEN_trivial_fail (term,cl) -> + tclTHEN + (unify_resolve (term,cl)) + (trivial_fail_db db_list local_db) + | Unfold_nth c -> unfold_constr c + | Extern tacast -> + conclPattern concl (out_some p) tacast)) + tacl + +and trivial_resolve db_list local_db cl = + try + let hdconstr = List.hd (head_constr_bound cl []) in + priority + (my_find_search db_list local_db (head_of_constr_reference hdconstr) cl) + with Bound | Not_found -> + [] + +(**************************************************************************) +(* The classical Auto tactic *) +(**************************************************************************) + +let possible_resolve db_list local_db cl = + try + let hdconstr = List.hd (head_constr_bound cl []) in + List.map snd + (my_find_search db_list local_db (head_of_constr_reference hdconstr) cl) + with Bound | Not_found -> + [] + +let decomp_unary_term c gls = + let typc = pf_type_of gls c in + let hd = List.hd (head_constr typc) in + if Hipattern.is_conjunction hd then + simplest_case c gls + else + errorlabstrm "Auto.decomp_unary_term" (str "not a unary type") + +let decomp_empty_term c gls = + let typc = pf_type_of gls c in + let (hd,_) = decompose_app typc in + if Hipattern.is_empty_type hd then + simplest_case c gls + else + errorlabstrm "Auto.decomp_empty_term" (str "not an empty type") + + +(* decomp is an natural number giving an indication on decomposition + of conjunction in hypotheses, 0 corresponds to no decomposition *) +(* n is the max depth of search *) +(* local_db contains the local Hypotheses *) + +let rec search_gen decomp n db_list local_db extra_sign goal = + if n=0 then error "BOUND 2"; + let decomp_tacs = match decomp with + | 0 -> [] + | p -> + (tclTRY_sign decomp_empty_term extra_sign) + :: + (List.map + (fun id -> tclTHEN (decomp_unary_term (mkVar id)) + (tclTHEN + (clear_one id) + (free_try (search_gen decomp p db_list local_db [])))) + (pf_ids_of_hyps goal)) + in + let intro_tac = + tclTHEN intro + (fun g' -> + let (hid,_,htyp as d) = pf_last_hyp g' in + let hintl = + try + [make_apply_entry (pf_env g') (project g') + (true,false) + hid (mkVar hid,body_of_type htyp)] + with Failure _ -> [] + in + (free_try + (search_gen decomp n db_list (Hint_db.add_list hintl local_db) [d]) + g')) + in + let rec_tacs = + List.map + (fun ntac -> + tclTHEN ntac + (free_try + (search_gen decomp (n-1) db_list local_db empty_named_context))) + (possible_resolve db_list local_db (pf_concl goal)) + in + tclFIRST (assumption::(decomp_tacs@(intro_tac::rec_tacs))) goal + + +let search = search_gen 0 + +let default_search_depth = ref 5 + +let full_auto n gl = + let dbnames = stringmap_dom !searchtable in + let dbnames = list_subtract dbnames ["v62"] in + let db_list = List.map (fun x -> searchtable_map x) dbnames in + let hyps = pf_hyps gl in + tclTRY (search n db_list (make_local_hint_db gl) hyps) gl + +let default_full_auto gl = full_auto !default_search_depth gl +(***********************************************************************) + +let blast_tactic = ref (free_try default_full_auto) +;; + +let blast_auto = (free_try default_full_auto) +(* (tclTHEN (free_try default_full_auto) + (free_try (my_full_eauto 2))) +*) +;; +let blast_simpl = (free_try (reduce Simpl [])) +;; +let blast_induction1 = + (free_try (tclTHEN (tclTRY intro) + (tclTRY (tclLAST_HYP simplest_elim)))) +;; +let blast_induction2 = + (free_try (tclTHEN (tclTRY (tclTHEN intro intro)) + (tclTRY (tclLAST_HYP simplest_elim)))) +;; +let blast_induction3 = + (free_try (tclTHEN (tclTRY (tclTHEN intro (tclTHEN intro intro))) + (tclTRY (tclLAST_HYP simplest_elim)))) +;; + +blast_tactic := + (tclORELSE (tclCOMPLETE blast_auto) + (tclORELSE (tclCOMPLETE (tclTHEN blast_simpl blast_auto)) + (tclORELSE (tclCOMPLETE (tclTHEN blast_induction1 + (tclTHEN blast_simpl blast_auto))) + (tclORELSE (tclCOMPLETE (tclTHEN blast_induction2 + (tclTHEN blast_simpl blast_auto))) + (tclCOMPLETE (tclTHEN blast_induction3 + (tclTHEN blast_simpl blast_auto))))))) +;; +(* +blast_tactic := (tclTHEN (free_try default_full_auto) + (free_try (my_full_eauto 4))) +;; +*) + +let vire_extvar s = + let interro = ref false in + let interro_pos = ref 0 in + for i=0 to (length s)-1 do + if get s i = '?' + then (interro := true; + interro_pos := i) + else if (!interro && + (List.mem (get s i) + ['0';'1';'2';'3';'4';'5';'6';'7';'8';'9'])) + then set s i ' ' + else interro:=false + done; + s +;; + +let blast gls = + let leaf g = { + status = Incomplete_proof; + subproof = None; + goal = g; + ref = None } in + try (let (sgl,v) as res = !blast_tactic gls in + let {it=lg} = sgl in + if lg = [] + then (let pf = v (List.map leaf (sig_it sgl)) in + let sign = (sig_it gls).evar_hyps in + let x = print_subscript + (sig_sig gls) sign pf in + msgnl (hov 0 (str"Blast ==> " ++ x)); + let x = print_subscript + (sig_sig gls) sign pf in + let tac_string = + pp_string (hov 0 x ) in + (* on remplace les ?1 ?2 ... de refine par ? *) + parse_tac ((vire_extvar tac_string) + ^ ".") + ) + else (msgnl (hov 0 (str"Blast failed to prove the goal...")); + failwith "echec de blast")) + with _ -> failwith "echec de blast" +;; + +let blast_tac display_function = function + | ((Integer n)::_) as l -> + (function g -> + let exp_ast = (blast g) in + (display_function (ast_to_ct exp_ast); + tclIDTAC g)) + | _ -> failwith "expecting other arguments";; + +let blast_tac_txt = + blast_tac (function x -> msgnl(Printer.gentacpr (ct_to_ast x)));; + +overwriting_add_tactic "Blast1" blast_tac_txt;; + +(* +Grammar tactic ne_numarg_list : list := + ne_numarg_single [numarg($n)] ->[$n] +| ne_numarg_cons [numarg($n) ne_numarg_list($ns)] -> [ $n ($LIST $ns) ]. +Grammar tactic simple_tactic : ast := + blast1 [ "Blast1" ne_numarg_list($ns) ] -> + [ (Blast1 ($LIST $ns)) ]. + + + +PATH=/usr/local/bin:/usr/bin:$PATH +COQTOP=d:/Tools/coq-7.0-3mai +CAMLLIB=/usr/local/lib/ocaml +CAMLP4LIB=/usr/local/lib/camlp4 +export CAMLLIB +export COQTOP +export CAMLP4LIB +d:/Tools/coq-7.0-3mai/bin/coqtop.byte.exe +Drop. +#use "/cygdrive/D/Tools/coq-7.0-3mai/dev/base_include";; +*) diff --git a/contrib/interface/blast.mli b/contrib/interface/blast.mli new file mode 100644 index 000000000..e8bcf95c6 --- /dev/null +++ b/contrib/interface/blast.mli @@ -0,0 +1,5 @@ +val blast_tac : (Ctast.t -> 'a) -> + Proof_type.tactic_arg list -> + Proof_type.goal Tacmach.sigma -> + Proof_type.goal list Proof_type.sigma * Proof_type.validation;; + diff --git a/contrib/interface/centaur.ml b/contrib/interface/centaur.ml index 00db51adf..fd60e1e61 100644 --- a/contrib/interface/centaur.ml +++ b/contrib/interface/centaur.ml @@ -1,7 +1,7 @@ (*Toplevel loop for the communication between Coq and Centaur *) open Names;; -open Nameops +open Nameops;; open Util;; open Ast;; open Term;; @@ -34,6 +34,7 @@ open Ascent;; open Translate;; open Name_to_ast;; open Pbp;; +open Blast;; open Dad;; open Debug_tac;; open Search;; @@ -67,7 +68,7 @@ let rec string_of_path p = | i::p -> (string_of_int i)^" "^ (string_of_path p) ;; let print_path p = - output_results_nl (str "Path:" ++ str (string_of_path p)) + output_results_nl (str "Path:" ++ str (string_of_path p)) ;; let kill_proof_node index = @@ -83,8 +84,8 @@ let kill_proof_node index = (*Message functions, the text of these messages is recognized by the protocols *) (*of CtCoq *) let ctf_header message_name request_id = - fnl () ++ str "message" ++ fnl () ++ str message_name ++ fnl () ++ - int request_id ++ fnl ();; + fnl () ++ str "message" ++ fnl() ++ str message_name ++ fnl() ++ + int request_id ++ fnl();; let ctf_acknowledge_command request_id command_count opt_exn = let goal_count, goal_index = @@ -95,14 +96,14 @@ let ctf_acknowledge_command request_id command_count opt_exn = g_count, (min g_count !current_goal_index) else (0, 0) in - (ctf_header "acknowledge" request_id ++ - int command_count ++ fnl () ++ - int goal_count ++ fnl () ++ - int goal_index ++ fnl () ++ - str !current_proof_name ++ fnl () ++ - (match opt_exn with - Some e -> Errors.explain_exn e - | None -> mt ()) ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ());; + (ctf_header "acknowledge" request_id ++ + int command_count ++ fnl() ++ + int goal_count ++ fnl () ++ + int goal_index ++ fnl () ++ + str !current_proof_name ++ fnl() ++ + (match opt_exn with + Some e -> Errors.explain_exn e + | None -> mt ()) ++ fnl() ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ());; let ctf_undoResults = ctf_header "undo_results";; @@ -117,37 +118,36 @@ let ctf_Location = ctf_header "location";; let ctf_StateMessage = ctf_header "state";; let ctf_PathGoalMessage () = - fnl () ++ str "message" ++ fnl () ++ str "single_goal" ++ fnl ();; + fnl () ++ str "message" ++ fnl () ++ str "single_goal" ++ fnl ();; let ctf_GoalReqIdMessage = ctf_header "single_goal_state";; let ctf_NewStateMessage = ctf_header "fresh_state";; -let ctf_SavedMessage () = fnl () ++ str "message" ++ fnl () ++ str "saved" ++ fnl ();; +let ctf_SavedMessage () = fnl () ++ str "message" ++ fnl () ++ + str "saved" ++ fnl();; let ctf_KilledMessage req_id ngoals = ctf_header "killed" req_id ++ int ngoals ++ fnl ();; let ctf_AbortedAllMessage () = - fnl () ++ str "message" ++ fnl () ++ str "aborted_all" ++ fnl ();; + fnl() ++ str "message" ++ fnl() ++ str "aborted_all" ++ fnl();; let ctf_AbortedMessage request_id na = - fnl () ++ str "message" ++ fnl () ++ str "aborted_proof" ++ fnl () ++ - int request_id ++ fnl () ++ - str na ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ();; + ctf_header "aborted_proof" request_id ++ str na ++ fnl () ++ + str "E-n-d---M-e-s-s-a-g-e" ++ fnl ();; let ctf_UserErrorMessage request_id stream = - let stream = guarded_force_eval_stream stream in - fnl () ++ str "message" ++ fnl () ++ str "user_error" ++ fnl () ++ - int request_id ++ fnl () ++ - stream ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ();; + let stream = guarded_force_eval_stream stream in + ctf_header "user_error" request_id ++ stream ++ fnl() ++ + str "E-n-d---M-e-s-s-a-g-e" ++ fnl();; let ctf_ResetInitialMessage () = - fnl () ++ str "message" ++ fnl () ++ str "reset_initial" ++ fnl ();; + fnl () ++ str "message" ++ fnl () ++ str "reset_initial" ++ fnl ();; let ctf_ResetIdentMessage request_id s = - fnl () ++ str "message" ++ fnl () ++ str "reset_ident" ++ fnl () ++ int request_id ++ fnl () ++ - str s ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ();; + ctf_header "reset_ident" request_id ++ str s ++ fnl () ++ + str "E-n-d---M-e-s-s-a-g-e" ++ fnl();; type vtp_tree = | P_rl of ct_RULE_LIST @@ -219,7 +219,6 @@ let show_nth n = try let pf = proof_of_pftreestate (get_pftreestate()) in if (!text_proof_flag<>"off") then -(* errorlabstrm "debug" [< str "text printing unplugged" >]*) (if n=0 then output_results (ctf_TextMessage !global_request_id) (Some (P_text (show_proof !text_proof_flag []))) @@ -248,9 +247,10 @@ let filter_by_module_from_varg_list (l:vernac_arg list) = let add_search (global_reference:global_reference) assumptions cstr = try let env = Global.env() in - let id_string = - string_of_qualid (Nametab.shortest_qualid_of_global env global_reference) in - let ast = + let id_string = + string_of_qualid (Nametab.shortest_qualid_of_global env + global_reference) in + let ast = try CT_premise (CT_ident id_string, translate_constr assumptions cstr) with Not_found -> @@ -275,16 +275,13 @@ let print_check (ast, judg) = with UserError(f,str) -> raise(UserError(f, Ast.print_ast - (ast_of_constr true (Global.env()) value) ++ - fnl () ++ str))) - in + (ast_of_constr true (Global.env()) value) ++ + fnl () ++ str ))) in let type_ct_ast = (try translate_constr (Global.env()) typ with UserError(f,str) -> raise(UserError(f, Ast.print_ast (ast_of_constr true (Global.env()) - value) ++ - fnl () ++ str))) - in + value) ++ fnl() ++ str))) in ((ctf_SearchResults !global_request_id), (Some (P_pl (CT_premises_list @@ -309,30 +306,36 @@ and ntyp = nf_betaiota typ in (* The following function is copied from globpr in env/printer.ml *) -let globcv = function - | Node(_,"MUTIND", (Path(_,sp))::(Num(_,tyi))::_) -> - let env = Global.env() in - convert_qualid - (Nametab.shortest_qualid_of_global env (IndRef(sp,tyi))) - | Node(_,"MUTCONSTRUCT",(Path(_,sp))::(Num(_,tyi))::(Num(_,i))::_) -> - let env = Global.env() in - convert_qualid - (Nametab.shortest_qualid_of_global env (ConstructRef ((sp, tyi), i))) +let globcv x = + let env = Global.env() in + match x with + | Node(_,"MUTIND", (Path(_,sp))::(Num(_,tyi))::_) -> + let env = Global.env() in + convert_qualid + (Nametab.shortest_qualid_of_global env (IndRef(sp,tyi))) + | Node(_,"MUTCONSTRUCT",(Path(_,sp))::(Num(_,tyi))::(Num(_,i))::_) -> + convert_qualid + (Nametab.shortest_qualid_of_global env + (ConstructRef ((sp, tyi), i))) | _ -> failwith "globcv : unexpected value";; let pbp_tac_pcoq = - pbp_tac (function x -> + pbp_tac (function (x:Ctast.t) -> output_results - (fnl () ++ str "message" ++ fnl () ++ str "pbp_results" ++ fnl () ++ - int !global_request_id ++ fnl ()) - (Some (P_t(xlate_tactic x))));; + (ctf_header "pbp_results" !global_request_id) + (Some (P_t(xlate_tactic x))));; + +let blast_tac_pcoq = + blast_tac (function (x:Ctast.t) -> + output_results + (ctf_header "pbp_results" !global_request_id) + (Some (P_t(xlate_tactic x))));; let dad_tac_pcoq = dad_tac(function x -> output_results - (fnl () ++ str "message" ++ fnl () ++ str "pbp_results" ++ fnl () ++ - int !global_request_id ++ fnl ()) + (ctf_header "pbp_results" !global_request_id) (Some (P_t(xlate_tactic x))));; let search_output_results () = @@ -351,8 +354,9 @@ let debug_tac2_pcoq = function try let result = report_error ast the_goal the_ast the_path [] g in (errorlabstrm "DEBUG TACTIC" - (str "no error here " ++ fnl () ++ pr_goal (sig_it g) ++ - fnl () ++ str "the tactic is" ++ fnl () ++ Printer.gentacpr ast); + (str "no error here " ++ fnl () ++ pr_goal (sig_it g) ++ + fnl () ++ str "the tactic is" ++ fnl () ++ + Printer.gentacpr ast); result) with e -> @@ -487,7 +491,7 @@ let command_changes = [ if kind = "LETTOP" && not(refining ()) then errorlabstrm "StartProof" (str - "Let declarations can only be used in proof editing mode" + "Let declarations can only be used in proof editing mode" ); let str = (string_of_id s) in start_proof_com (Some s) stre c; @@ -600,12 +604,12 @@ let command_changes = [ function (VARG_QUALID qid)::l -> (fun () -> - ctv_SEARCH_LIST:=[]; + ctv_SEARCH_LIST:=[]; let global_ref = Nametab.global dummy_loc qid in - filtered_search - (filter_by_module_from_varg_list l) - add_search (Nametab.locate qid); - search_output_results()) + filtered_search + (filter_by_module_from_varg_list l) + add_search (Nametab.locate qid); + search_output_results()) | _ -> failwith "bad form of arguments"); ("SearchRewrite", @@ -697,8 +701,7 @@ let command_changes = [ (fun () -> let results = dad_rule_names() in output_results - (fnl () ++ str "message" ++ fnl () ++ str "dad_rule_names" ++ fnl () ++ - int !global_request_id ++ fnl ()) + (ctf_header "dad_rule_names" !global_request_id) (Some (P_ids (CT_id_list (List.map (fun s -> CT_ident s) results))))) @@ -741,6 +744,7 @@ let start_pcoq_mode debug = set_xlate_mut_stuff (fun x ->Ctast.ast_to_ct (globcv (Ctast.ct_to_ast x))); declare_in_coq(); add_tactic "PcoqPbp" pbp_tac_pcoq; + add_tactic "PcoqBlast" blast_tac_pcoq; add_tactic "Dad" dad_tac_pcoq; add_tactic "CtDebugTac" debug_tac2_pcoq; add_tactic "CtDebugTac2" debug_tac2_pcoq; diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml index fad5c1e34..671338002 100644 --- a/contrib/interface/parse.ml +++ b/contrib/interface/parse.ml @@ -43,24 +43,29 @@ let print_parse_results n msg = flush stdout;; let ctf_SyntaxErrorMessage reqid pps = - (fnl () ++ str "message" ++ fnl () ++ str "syntax_error" ++ fnl () ++ int reqid ++ fnl () ++ - pps ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ());; + fnl () ++ str "message" ++ fnl () ++ str "syntax_error" ++ fnl () ++ + int reqid ++ fnl () ++ + pps ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ();; let ctf_SyntaxWarningMessage reqid pps = - (fnl () ++ str "message" ++ fnl () ++ str "syntax_warning" ++ fnl () ++ int reqid ++ fnl () ++ - pps ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ());; + fnl () ++ str "message" ++ fnl () ++ str "syntax_warning" ++ fnl () ++ + int reqid ++ fnl () ++ pps ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl();; let ctf_FileErrorMessage reqid pps = - (fnl () ++ str "message" ++ fnl () ++ str "file_error" ++ fnl () ++ int reqid ++ fnl () ++ - pps ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ());; + fnl () ++ str "message" ++ fnl () ++ str "file_error" ++ fnl () ++ + int reqid ++ fnl () ++ pps ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ + fnl ();; (*In the code for CoqV6.2, the require_module call is encapsulated in a function "without_mes_ambig". Here I have supposed that this function has no effect on parsing *) let try_require_module import specif name fname = - try Library.require_module (if specif = "UNSPECIFIED" then None - else Some (specif = "SPECIFICATION")) (Nametab.make_short_qualid (Names.id_of_string name)) fname (import = "IMPORT") + try Library.require_module + (if specif = "UNSPECIFIED" then None + else Some (specif = "SPECIFICATION")) + (Nametab.make_short_qualid (Names.id_of_string name)) + fname (import = "IMPORT") with - | e -> msgnl (str "Reinterning of " ++ str name ++ str " failed");; + | e -> msgnl (str "Reinterning of " ++ str name ++ str " failed");; let execute_when_necessary ast = (match ast with @@ -82,20 +87,24 @@ let parse_to_dot = let rec dot st = match Stream.next st with | ("", ".") -> () | ("EOI", "") -> raise End_of_file - | _ -> dot st - in - Gram.Entry.of_parser "Coqtoplevel.dot" dot;; + | _ -> dot st in + Gram.Entry.of_parser "Coqtoplevel.dot" dot;; let rec discard_to_dot stream = try Gram.Entry.parse parse_to_dot (Gram.parsable stream) with | Stdpp.Exc_located(_, Token.Error _) -> discard_to_dot stream;; -let rec decompose_string s n = +let rec decompose_string_aux s n = try let index = String.index_from s n '\n' in (Ctast.str (String.sub s n (index - n))):: - (decompose_string s (index + 1)) + (decompose_string_aux s (index + 1)) with Not_found -> [Ctast.str(String.sub s n ((String.length s) - n))];; +let decompose_string s n = + match decompose_string_aux s n with + (Ctast.Str(_,""))::tl -> tl + | a -> a;; + let make_string_list file_chan fst_pos snd_pos = let len = (snd_pos - fst_pos) in let s = String.create len in @@ -146,15 +155,17 @@ let parse_command_list reqid stream string_list = let rec parse_whole_stream () = let this_pos = Stream.count stream in let first_ast = - try option_app Ctast.ast_to_ct (Gram.Entry.parse Pcoq.main_entry (Gram.parsable stream)) + try option_app + Ctast.ast_to_ct (Gram.Entry.parse + Pcoq.main_entry (Gram.parsable stream)) with | (Stdpp.Exc_located(l, Stream.Error txt)) as e -> begin msgnl (ctf_SyntaxWarningMessage reqid (Errors.explain_exn e)); try discard_to_dot stream; - msgnl (str "debug" ++ fnl () ++ int this_pos ++ fnl () ++ int - (Stream.count stream)); + msgnl (str "debug" ++ fnl () ++ int this_pos ++ fnl () ++ + int (Stream.count stream)); Some( Node(l, "PARSING_ERROR", List.map Ctast.str (get_substring_list string_list this_pos @@ -172,7 +183,13 @@ let parse_command_list reqid stream string_list = match first_ast with | Some ast -> let ast0 = (execute_when_necessary ast) in - xlate_vernac ast::parse_whole_stream() + (try xlate_vernac ast + with e -> + xlate_vernac + (Node((0,0), "PARSING_ERROR2", + List.map Ctast.str + (get_substring_list string_list this_pos + (Stream.count stream)))))::parse_whole_stream() | None -> [] in match parse_whole_stream () with | first_one::tail -> (P_cl (CT_command_list(first_one, tail))) @@ -239,56 +256,75 @@ let parse_file_action reqid file_name = let file_chan_err = open_in file_name in let stream = Stream.of_channel file_chan in let stream_err = Stream.of_channel file_chan_err in - match let rec parse_whole_file () = - let this_pos = Stream.count stream in - match - try - let this_ast = - option_app Ctast.ast_to_ct (Gram.Entry.parse Pcoq.main_entry (Gram.parsable stream)) in - this_ast - with - | Stdpp.Exc_located(l,Stream.Error txt ) -> - msgnl (ctf_SyntaxWarningMessage reqid - (str "Error with file" ++ spc () ++ str file_name ++ fnl () ++ - Errors.explain_exn - (Stdpp.Exc_located(l,Stream.Error txt)))); - let rec discard_to_dot () = - try Gram.Entry.parse parse_to_dot (Gram.parsable stream) - with Stdpp.Exc_located(_,Token.Error _) -> discard_to_dot() - in (try - discard_to_dot (); - Some( Node(l, "PARSING_ERROR", - (make_string_list file_chan_err this_pos - (Stream.count stream)))) - with End_of_file -> None) - | e -> - begin - Gram.Entry.parse parse_to_dot (Gram.parsable stream); - Some( Node((0,0), "PARSING_ERROR2", - (make_string_list file_chan this_pos - (Stream.count stream)))) - end - - with - | Some ast -> let ast0=(execute_when_necessary ast) in - xlate_vernac ast::parse_whole_file () - | None -> [] in - parse_whole_file () with - | first_one :: tail -> - print_parse_results reqid - (P_cl (CT_command_list (first_one, tail))) - | [] -> raise (UserError ("parse_file_action", (str "empty file."))) - with - | Stdpp.Exc_located(l,Match_failure(_,_,_)) -> - msgnl - (ctf_SyntaxErrorMessage reqid - (str "Error with file" ++ spc () ++ str file_name ++ fnl () ++ - Errors.explain_exn (Stdpp.Exc_located(l,Stream.Error "match failure")))) - | e -> - msgnl - (ctf_SyntaxErrorMessage reqid - (str "Error with file" ++ spc () ++ str file_name ++ fnl () ++ - Errors.explain_exn e));; + let rec discard_to_dot () = + try Gram.Entry.parse parse_to_dot (Gram.parsable stream) + with Stdpp.Exc_located(_,Token.Error _) -> discard_to_dot() in + match let rec parse_whole_file () = + let this_pos = Stream.count stream in + match + try + let this_ast = + option_app Ctast.ast_to_ct + (Gram.Entry.parse Pcoq.main_entry (Gram.parsable stream)) in + this_ast + with + | Stdpp.Exc_located(l,Stream.Error txt) -> + msgnl (ctf_SyntaxWarningMessage reqid + (str "Error with file" ++ spc () ++ + str file_name ++ fnl () ++ + Errors.explain_exn + (Stdpp.Exc_located(l,Stream.Error txt)))); + (try + begin + discard_to_dot (); + Some( Node(l, "PARSING_ERROR", + (make_string_list file_chan_err this_pos + (Stream.count stream)))) + end + with End_of_file -> None) + | e -> + begin + Gram.Entry.parse parse_to_dot (Gram.parsable stream); + Some(Node((0,0), "PARSING_ERROR2", + (make_string_list file_chan this_pos + (Stream.count stream)))) + end + + with + | Some ast -> + let ast0=(execute_when_necessary ast) in + let term = + (try xlate_vernac ast + with e -> + print_string ("translation error between " ^ + (string_of_int this_pos) ^ + " " ^ + (string_of_int (Stream.count stream)) ^ + "\n"); + xlate_vernac + (Node((0,0), "PARSING_ERROR2", + (make_string_list file_chan_err this_pos + (Stream.count stream))))) in + term::parse_whole_file () + | None -> [] in + parse_whole_file () with + | first_one :: tail -> + print_parse_results reqid + (P_cl (CT_command_list (first_one, tail))) + | [] -> raise (UserError ("parse_file_action", str "empty file.")) + with + | Stdpp.Exc_located(l,Match_failure(_,_,_)) -> + msgnl + (ctf_SyntaxErrorMessage reqid + (str "Error with file" ++ spc () ++ str file_name ++ + fnl () ++ + Errors.explain_exn + (Stdpp.Exc_located(l,Stream.Error "match failure")))) + | e -> + msgnl + (ctf_SyntaxErrorMessage reqid + (str "Error with file" ++ spc () ++ str file_name ++ + fnl () ++ Errors.explain_exn e));; (* This function is taken from Mltop.add_path *) @@ -302,7 +338,7 @@ let add_path dir coq_dirpath = let convert_string d = try Names.id_of_string d - with _ -> failwith "caught" + with _ -> failwith ("could not convert " ^ d) let add_rec_path dir coq_dirpath = let dirs = all_subdirs dir in @@ -345,11 +381,12 @@ let load_syntax_action reqid module_name = msgnl (mt ()); msgnl (fnl () ++ str "error while loading syntax module " ++ str module_name ++ - str ": " ++ str label ++ fnl () ++ pp_stream) + str ": " ++ str label ++ fnl () ++ pp_stream) | e -> msgnl (mt ()); msgnl - (fnl () ++ str "message" ++ fnl () ++ str "load_error" ++ fnl () ++ int reqid ++ fnl ()); + (fnl () ++ str "message" ++ fnl () ++ str "load_error" ++ fnl () ++ + int reqid ++ fnl ()); ();; let coqparser_loop inchan = @@ -373,25 +410,14 @@ Libobject.relax true; else (msgnl (str "could not find the value of COQDIR"); exit 1) in begin - add_rec_path (Filename.concat coqdir "theories") (Names.make_dirpath [Nameops.coq_root]); - add_path (Filename.concat coqdir "tactics") (Names.make_dirpath [Nameops.coq_root]); - add_rec_path (Filename.concat coqdir "contrib") (Names.make_dirpath [Nameops.coq_root]); + add_rec_path (Filename.concat coqdir "theories") + (Names.make_dirpath [Nameops.coq_root]); + add_path (Filename.concat coqdir "tactics") + (Names.make_dirpath [Nameops.coq_root]); + add_rec_path (Filename.concat coqdir "contrib") + (Names.make_dirpath [Nameops.coq_root]); List.iter (fun a -> msgnl (str a)) (get_load_path()) end; -(try - (match create_entry (get_univ "nat") "number" ETast with - (Ast number) -> - Gram.extend number None - [None, None, - [[Gramext.Stoken ("INT", "")], - Gramext.action - (fun s loc -> - Node((0,0),"XTRA",[Str((0,0),"omega_integer_for_ctcoq"); - Num((0,0),int_of_string s)]))]] - | _ -> msgnl (str "unpredicted behavior of Grammar.extend")) - - with - e -> msgnl (str "could not add a parser for numbers")); (let vernacrc = try Sys.getenv "VERNACRC" diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml index 13e307a47..2e92dd7c9 100644 --- a/contrib/interface/pbp.ml +++ b/contrib/interface/pbp.ml @@ -1,6 +1,4 @@ (* A proof by pointing algorithm. *) - - open Util;; open Names;; open Term;; @@ -20,14 +18,21 @@ open Typing;; open Pp;; (* get_hyp_by_name : goal sigma -> string -> constr, - looks up for an hypothesis, from its name *) + looks up for an hypothesis (or a global constant), from its name *) let get_hyp_by_name g name = let evd = project g in let env = pf_env g in - let judgment = - Pretyping.understand_judgment - evd env (RVar(dummy_loc, id_of_string name)) in - judgment.uj_type;; + try (let judgment = + Pretyping.understand_judgment + evd env (RVar(dummy_loc, id_of_string name)) in + ("hyp",judgment.uj_type)) +(* je sais, c'est pas beau, mais je ne sais pas trop me servir de look_up... + Loïc *) + with _ -> (let parse_ast = Pcoq.parse_string Pcoq.Constr.constr in + let parse s = Astterm.interp_constr Evd.empty (Global.env()) + (parse_ast s) in + ("cste",type_of (Global.env()) Evd.empty (parse name))) +;; type pbp_rule = (identifier list * string list * @@ -62,8 +67,9 @@ let get_name_from_intro = function let make_clears = function [] -> Node(zz, "Idtac",[]) | str_list -> - Node(zz,"Clear", - [Node(zz, "CLAUSE", List.map (function s -> Nvar(zz,s)) str_list)]);; + Node(zz, "TRY", [Node(zz,"Clear", + [Node(zz, "CLAUSE", List.map (function s -> Nvar(zz,s)) str_list)]) + ]);; let add_clear_names_if_necessary tactic clear_names = match clear_names with @@ -176,7 +182,7 @@ let (imply_elim2: pbp_rule) = function | _ -> None;; let reference dir s = - let dir = make_dirpath + let dir = make_dirpath (List.map id_of_string (List.rev ("Coq"::"Init"::[dir]))) in let id = id_of_string s in try @@ -185,9 +191,7 @@ let reference dir s = anomaly ("Coqlib: cannot find "^ (Nametab.string_of_qualid (Nametab.make_qualid dir id))) -let constant dir s = - Declare.constr_of_reference (reference dir s);; - +let constant dir s = Declare.constr_of_reference (reference dir s);; let andconstr: unit -> constr = Coqlib.build_coq_and;; let prodconstr () = constant "Datatypes" "prod";; @@ -544,6 +548,9 @@ let default_ast optname constr path = [Node(zz, "Exact",[Node(zz,"COMMAND",[Nvar(zz,a)])])]);; (* This is the main proof by pointing function. *) +(* avoid: les noms a ne pas utiliser *) +(* final_cmd: la fonction appelee par defaut *) +(* opt_name: eventuellement le nom de l'hypothese sur laquelle on agit *) let rec pbpt final_cmd avoid clear_names clear_flag opt_name constr path = let rec try_all_rules rl = @@ -645,7 +652,7 @@ let cleanup_clears empty_allowed names str_list other = [] else [Node(zz,"Idtac",[])] | _ -> other) - | l -> Node(zz, "Clear", [Node(zz,"CLAUSE", l)])::other;; + | l -> Node(zz, "TRY", [Node(zz, "Clear", [Node(zz,"CLAUSE", l)])])::other;; (* This function takes care of compacting instanciations of universal @@ -661,7 +668,7 @@ let rec optim3 str_list = function | Some s -> optim3_aux true (s::str_list) (Node(a, "Generalize", [merge_ast_in_command com1 com2])::others)) - |( Node(a,"Clear", [Node(_,"CLAUSE", names)]))::other -> + |( Node(zz, "TRY", [Node(a,"Clear", [Node(_,"CLAUSE", names)])]))::other -> cleanup_clears empty_allowed names str_list other | [Node(a,"TACLIST",branches)] -> [Node(a,"TACLIST",List.map (optim3 str_list) branches)] @@ -686,9 +693,16 @@ let pbp_tac display_function = function (Identifier a)::l -> (function g -> let str = (string_of_id a) in + let (ou,tstr) = (get_hyp_by_name g str) in let exp_ast = - pbpt default_ast (pf_ids_of_hyps g) - [] false (Some str) (kind_of_term (get_hyp_by_name g str)) + pbpt default_ast + (match ou with + "hyp" ->(pf_ids_of_hyps g) + |_ -> (a::(pf_ids_of_hyps g))) + [] + false + (Some str) + (kind_of_term tstr) (tactic_args_to_ints l) in (display_function (optim exp_ast); tclIDTAC g)) @@ -704,3 +718,5 @@ let pbp_tac display_function = function (display_function (default_ast None (pf_concl g) []); tclIDTAC g)) | _ -> failwith "expecting other arguments";; + + diff --git a/contrib/interface/vernacrc b/contrib/interface/vernacrc index 092bc0709..b66f1e4c1 100644 --- a/contrib/interface/vernacrc +++ b/contrib/interface/vernacrc @@ -10,6 +10,7 @@ load_syntax_file 21 Equality load_syntax_file 22 Inv load_syntax_file 26 Tauto load_syntax_file 34 Omega +load_syntax_file 27 Ring quiet_parse_string Goal a. && END--OF--DATA diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml index 778220322..597553cd5 100644 --- a/contrib/interface/vtp.ml +++ b/contrib/interface/vtp.ml @@ -457,7 +457,9 @@ and fCONTEXT_RULE = function and fCONVERSION_FLAG = function | CT_beta -> fNODE "beta" 0 | CT_delta -> fNODE "delta" 0 +| CT_evar -> fNODE "evar" 0 | CT_iota -> fNODE "iota" 0 +| CT_zeta -> fNODE "zeta" 0 and fCONVERSION_FLAG_LIST = function | CT_conversion_flag_list l -> (List.iter fCONVERSION_FLAG l); @@ -479,8 +481,8 @@ and fCO_IND = function | CT_coerce_DEFN_to_DEFN_OR_THM x -> fDEFN x | CT_coerce_THM_to_DEFN_OR_THM x -> fTHM x and fDEF_BODY = function +| CT_coerce_CONTEXT_PATTERN_to_DEF_BODY x -> fCONTEXT_PATTERN x | CT_coerce_EVAL_CMD_to_DEF_BODY x -> fEVAL_CMD x -| CT_coerce_FORMULA_to_DEF_BODY x -> fFORMULA x and fDEP = function | CT_dep x -> fATOM "dep"; (f_atom_string x); @@ -590,9 +592,6 @@ and fFORMULA = function fFORMULA x2; fFORMULA x3; fNODE "letin" 3 -| CT_metac(x1) -> - fINT x1; - fNODE "metac" 1 | CT_prodc(x1, x2) -> fBINDER x1; fFORMULA x2; @@ -632,7 +631,10 @@ and fHINT_EXPRESSION = function and fID = function | CT_ident x -> fATOM "ident"; (f_atom_string x); - print_string "\n"and fIDENTITY_OPT = function + print_string "\n"| CT_metac(x1) -> + fINT x1; + fNODE "metac" 1 +and fIDENTITY_OPT = function | CT_coerce_NONE_to_IDENTITY_OPT x -> fNONE x | CT_identity -> fNODE "identity" 0 and fID_LIST = function @@ -728,6 +730,19 @@ and fIN_OR_OUT_MODULES = function | CT_out_modules(x1) -> fID_NE_LIST x1; fNODE "out_modules" 1 +and fLET_CLAUSE = function +| CT_let_clause(x1, x2) -> + fID x1; + fLET_VALUE x2; + fNODE "let_clause" 2 +and fLET_CLAUSES = function +| CT_let_clauses(x,l) -> + fLET_CLAUSE x; + (List.iter fLET_CLAUSE l); + fNODE "let_clauses" (1 + (List.length l)) +and fLET_VALUE = function +| CT_coerce_DEF_BODY_to_LET_VALUE x -> fDEF_BODY x +| CT_coerce_TACTIC_COM_to_LET_VALUE x -> fTACTIC_COM x and fLOCAL_OPT = function | CT_coerce_NONE_to_LOCAL_OPT x -> fNONE x | CT_local -> fNODE "local" 0 @@ -749,6 +764,16 @@ and fMATCH_PATTERN_NE_LIST = function fMATCH_PATTERN x; (List.iter fMATCH_PATTERN l); fNODE "match_pattern_ne_list" (1 + (List.length l)) +and fMATCH_TAC_RULE = function +| CT_match_tac_rule(x1, x2) -> + fCONTEXT_PATTERN x1; + fLET_VALUE x2; + fNODE "match_tac_rule" 2 +and fMATCH_TAC_RULES = function +| CT_match_tac_rules(x,l) -> + fMATCH_TAC_RULE x; + (List.iter fMATCH_TAC_RULE l); + fNODE "match_tac_rules" (1 + (List.length l)) and fNATURAL_FEATURE = function | CT_contractible -> fNODE "contractible" 0 | CT_implicit -> fNODE "implicit" 0 @@ -1088,15 +1113,18 @@ and fTACTIC_COM = function | CT_left(x1) -> fSPEC_LIST x1; fNODE "left" 1 -| CT_lettac(x1, x2, x3) -> - fID x1; - fFORMULA x2; - fUNFOLD_NE_LIST x3; - fNODE "lettac" 3 +| CT_lettac(x1, x2) -> + fLET_CLAUSES x1; + fLET_VALUE x2; + fNODE "lettac" 2 | CT_match_context(x,l) -> fCONTEXT_RULE x; (List.iter fCONTEXT_RULE l); fNODE "match_context" (1 + (List.length l)) +| CT_match_tac(x1, x2) -> + fLET_VALUE x1; + fMATCH_TAC_RULES x2; + fNODE "match_tac" 2 | CT_move_after(x1, x2) -> fID x1; fID x2; diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index c7552847f..7f38ca0d2 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -42,16 +42,12 @@ Hashtbl.add type_table "Coq.Init.Datatypes.prod" Hashtbl.add type_table "Coq.Init.Datatypes.nat" [|[|"";"O"; "S"|]|];; -(* //menage a faire....*) -Hashtbl.add type_table "Coq.Zarith.fast_integer.Z" -[|[|"";"ZERO";"POS";"NEG"|]|];; Hashtbl.add type_table "Coq.ZArith.fast_integer.Z" [|[|"";"ZERO";"POS";"NEG"|]|];; -(*//itou *) -Hashtbl.add type_table "Coq.Zarith.fast_integer.positive" -[|[|"";"xI";"xO";"XH"|]|];; + + Hashtbl.add type_table "Coq.ZArith.fast_integer.positive" -[|[|"";"xI";"xO";"XH"|]|];; +[|[|"";"xI";"xO";"xH"|]|];; (*The following two codes are added to cope with the distinction between ocaml and caml-light syntax while using ctcaml to @@ -71,7 +67,7 @@ let string_of_node_loc the_node = match loc the_node with (a,b) -> "(" ^ (string_of_int a) ^ ", " ^ (string_of_int b) ^ ")";; -let xlate_error s = error ("Translation error: " ^ s);; +let xlate_error s = failwith ("Translation error: " ^ s);; type astrecurse = Rbinder of ct_ID_OPT * astrecurse | Rform of ct_FORMULA @@ -98,6 +94,10 @@ let ctv_ID_OPT_OR_ALL_ALL = CT_all;; let ctv_SPEC_OPT_NONE = CT_coerce_NONE_to_SPEC_OPT CT_none;; +let ct_coerce_FORMULA_to_DEF_BODY x = + CT_coerce_CONTEXT_PATTERN_to_DEF_BODY + (CT_coerce_FORMULA_to_CONTEXT_PATTERN x);; + let castc x = CT_coerce_TYPED_FORMULA_to_FORMULA x;; let varc x = CT_coerce_ID_to_FORMULA x;; @@ -310,6 +310,7 @@ let qualid_to_ct_ID = | (Nvar(_,s))::l -> s ^ "." ^ (f l) | _ -> assert false in Some(CT_ident (f l)) + | Node(_, "QUALIDMETA",[Num(_,n)]) -> Some(CT_metac (CT_int n)) | _ -> None;; @@ -322,7 +323,7 @@ let xlate_op the_node opn a b = match opn with | "META" -> (match a, b with - | ((Num (_, n)) :: []), [] -> CT_metac (CT_int n) + | ((Num (_, n)) :: []), [] -> CT_coerce_ID_to_FORMULA(CT_metac (CT_int n)) | _, _ -> xlate_error "xlate_op : META ") | "ISEVAR" -> CT_existvarc | "FORCEIF" -> @@ -403,15 +404,15 @@ let xlate_op the_node opn a b = CT_ident(Names.string_of_id (Nameops.basename (section_path sl)))) | _, _ -> xlate_error "xlate_op : MUTIND") - | "MUTCASE" - | "CASE" -> - let compute_flag s = - match s with "REC" -> "Match" | "NOREC" -> "Case" | _ -> assert false in - (match a, b with - | [Str(_,v)], tl -> make_casec (compute_flag v) tl - | [Str(_,v); Str(_,"SYNTH")], tl -> - make_casec (compute_flag v) (Rform CT_existvarc::tl) - | _, _ -> xlate_error "xlate_op : MUTCASE") + | "CASE" + | "MATCH" -> + (let compute_flag s = + match s with "CASE" -> "Case" | "MATCH" -> "Match" | _ -> assert false in + match a, b with + | [], tl -> make_casec (compute_flag opn) tl + | [Str(_, "SYNTH")], tl -> + make_casec (compute_flag opn) (Rform CT_existvarc::tl) + | _, _ -> assert false) | (** string_of_path needs to be investigated. *) "MUTCONSTRUCT" -> @@ -465,7 +466,8 @@ let id_to_pattern_var ctid = CT_coerce_ID_OPT_to_MATCH_PATTERN (CT_coerce_NONE_to_ID_OPT CT_none) | CT_ident id_string -> CT_coerce_ID_OPT_to_MATCH_PATTERN - (CT_coerce_ID_to_ID_OPT (CT_ident id_string));; + (CT_coerce_ID_to_ID_OPT (CT_ident id_string)) + | _ -> assert false;; let rec xlate_cases_pattern cont_function = function @@ -491,6 +493,13 @@ let rec xlate_cases_pattern cont_function = | CT_coerce_ID_to_FORMULA id -> id_to_pattern_var id | _ -> assert false) | Node(_, s, _) -> xlate_error ("error for a pattern " ^ s) + | Path(_,sl) -> + id_to_pattern_var (CT_ident (List.fold_right + (fun a b -> + if b = "" then + a + else + a ^ "." ^ b) sl "")) | _ -> xlate_error "Unexpected data while translating a pattern";; (*This function recognizes and translates let constructs @@ -504,82 +513,6 @@ let special_case_let_construct cont_function = strip_Rform (cont_function body)))) | _ -> None;; -(*This function recognizes and translates the integers introduced by P.Cregut. - However, it relies on the patterns given in our our version of integer_gram *) -let compile_decomposed_number cont_function ast = - (*cdn_rec returns a list of strings that represent the bits in a - binary representation of the number. 1 is represented by "xI" and 0 by "xO" *) - let rec cdn_rec = - function - | Node (_, "APPLIST", ((Nvar (_, s)) :: args)) as t -> - (match s with - | "xI" | "xO" -> - (match args with - | arg :: [] -> - let digit_list, head = cdn_rec arg in - s::digit_list, head - | _ -> xlate_error "bad number of arguments for xI or XO") - | it -> [], Some t) - | Nvar (_, s) as t -> - (match s with - | "xH" -> ["xI"], None - | _ -> [], Some t) - | t -> [], Some t in - (*when the number will appear as a binary number, we fake it by using base - 10 when reconstructing the number (A binary number looks like a decimal number - written only with ones and zeros). Otherwise, we use base 2, respecting - the true meaning of each bit. *) - let rec convert_to_number base = - function - | [] -> 0 - | "xI" :: tail -> 1 + base * convert_to_number base tail - | "xO" :: tail -> base * convert_to_number base tail - | _ -> xlate_error "compile_decomposed_number" in - match cdn_rec ast with - | (*binary representation is only used when constructing an incomplete number *) - digit_list, (Some formula) -> - CT_incomplete_binary - (strip_Rform (cont_function formula), - CT_binary (convert_to_number 10 digit_list)) - | digit_list, None -> - CT_int_encapsulator (CT_int (convert_to_number 2 digit_list));; - -let special_case_omega_integer cont_function = - function - | Node (_, "XTRA", - ((Str (_, "omega_integer_for_ctcoq")) :: ((Num (_, n)) :: []))) -> - Some (Rform (CT_int_encapsulator (CT_int n))) - | Node (_, "XTRA", - ((Str (_, "omega_binary_for_ctcoq")) :: ((Num (_, n)) :: []))) -> - Some (Rform (CT_coerce_BINARY_to_FORMULA (CT_binary n))) - | Node (_, "XTRA", - ((Str (_, "omega_variable_binary_for_ctcoq")) :: - (formula :: ((Num (_, n)) :: [])))) -> - Some - (Rform - (CT_incomplete_binary (strip_Rform (cont_function formula), CT_binary n))) - | Node (_, "APPLIST", - ((Nvar (_, pos_or_neg_string)) :: - ((Node (_, "APPLIST", ((Nvar (_, id)) :: (_ :: []))) as number) - :: []))) -> - (match pos_or_neg_string with - | "POS" -> - (match id with - | "xI" | "xO" | "xH" -> - Some (Rform (compile_decomposed_number cont_function number)) - | _ -> None) - | "NEG" -> - (match id with - | "xI" | "xO" | "xH" -> - Some - (Rform - (CT_appc - (CT_coerce_ID_to_FORMULA (CT_ident "NEG"), - CT_formula_ne_list (compile_decomposed_number cont_function number, [])))) - | _ -> None) - | _ -> None) - | _ -> None;; - let cvt_binder cont_function = function | Node (_,"BINDER", (c :: idl)) -> @@ -796,7 +729,6 @@ let special_case_S cont_function ast = let xlate_formula_special_cases = [special_case_qualid; special_case_let_construct; - special_case_omega_integer; special_case_fix; special_case_cofix; special_case_cases; @@ -920,18 +852,23 @@ let strip_targ_intropatt = let rec get_flag_rec = function | n1 :: tail -> + let conv_id_fun = (fun x -> match qualid_to_ct_ID x with + Some y -> y + | None -> assert false) in let conv_flags, red_ids = get_flag_rec tail in (match n1 with | Node (_, "Beta", []) -> CT_beta::conv_flags, red_ids | Node (_, "Delta", []) -> CT_delta::conv_flags, red_ids | Node (_, "Iota", []) -> CT_iota::conv_flags, red_ids + | Node (_, "Zeta", []) -> CT_zeta::conv_flags, red_ids + | Node (_, "Evar", []) -> CT_evar::conv_flags, red_ids | Node (_, "Unf", l) -> (match red_ids with - | CT_unf [] -> conv_flags, CT_unf (List.map xlate_id l) + | CT_unf [] -> conv_flags, CT_unf (List.map conv_id_fun l) | _ -> error "Cannot specify identifiers to unfold twice") | Node (_, "UnfBut", l) -> (match red_ids with - | CT_unf [] -> conv_flags, CT_unfbut (List.map xlate_id l) + | CT_unf [] -> conv_flags, CT_unfbut (List.map conv_id_fun l) | _ -> error "Cannot specify identifiers to unfold twice") | Node (_, a, _) -> error ("get_flag_rec : unexpected flag " ^ a) | _ -> error "get_flag_rec : unexpected flag") @@ -974,6 +911,8 @@ let tactic_special_case cont_function cvt_arg = function let xlate_context_pattern = function Node(_,"TERM", [Node(_, "COMMAND", [v])]) -> CT_coerce_FORMULA_to_CONTEXT_PATTERN (xlate_formula v) + | Node(_,"SUBTERM", [Node(_,"COMMAND",[v])]) -> + CT_context(ctv_ID_OPT_NONE, xlate_formula v) | Node(_,"SUBTERM", [Nvar(_, s); Node(_, "COMMAND", [v])]) -> CT_context(ctf_ID_OPT_SOME (CT_ident s), xlate_formula v) | _ -> assert false;; @@ -1028,17 +967,29 @@ let rec cvt_arg = | Node (_, "COFIXEXP", ((Nvar (_, id)) :: ((Node (_, "COMMAND", (c :: []))) :: []))) -> Targ_cofixtac (CT_cofixtac (CT_ident id, xlate_formula c)) - | Node (_, "CLAUSE", l) -> Targ_id_list (CT_id_list (List.map (function - | Nvar (_, x) -> CT_ident x - | _ -> - xlate_error - "expected identifiers in a CLAUSE") l)) + | Node ((l1,l2), "CLAUSE", l) -> + Targ_id_list (CT_id_list + (List.map + (function + | Node(_, "INHYP", [Nvar (_, x)]) -> CT_ident x + | Node(_, "INHYP", + [Node(_, "COMMAND", + [Node(_, "META", + [Num (_, x)])])]) -> + CT_metac (CT_int x) + | _ -> + xlate_error + ("expected identifiers in a CLAUSE " ^ + (string_of_int l1) ^ " " ^ + (string_of_int l2))) l)) | Node (_, "REDEXP", (tac :: [])) -> Targ_redexp (xlate_red_tactic tac) | Node (_, "INTROPATTERN", [Node(_,"LISTPATTERN", l)]) -> Targ_intropatt (CT_intro_patt_list(List.map xlate_intro_pattern l)) | Node(_, "Str", [x]) -> cvt_arg x - | Node (_, a, _) -> failwith ("cvt_arg on node " ^ a) + | Node ((l1,l2), a, _) -> failwith ("cvt_arg on node " ^ a ^ " at " ^ + (string_of_int l1) ^ " " ^ + (string_of_int l2)) | _ -> failwith "cvt_arg" and xlate_red_tactic = function @@ -1049,13 +1000,15 @@ and xlate_red_tactic = | "Simpl" -> CT_simpl | "Fold" -> CT_fold(CT_formula_list[]) | _ -> xlate_error ("xlate_red_tactic, unexpected singleton " ^ s)) - | Node (_, "Unfold", unf_list) -> + | Node ((l1,l2), "Unfold", unf_list) -> let ct_unf_list = List.map (function | Node (_, "UNFOLD", qid::nums) -> (match qualid_to_ct_ID qid with Some x -> CT_unfold_occ (CT_int_list (List.map xlate_int nums), x) - | _ -> assert false) + | _ -> failwith ("bad form in Unfold at characters " ^ + (string_of_int l1) ^ " " ^ + (string_of_int l2)) ) | n -> xlate_error ("xlate_red_tactic, expected unfold occurrence at " ^ (string_of_node_loc n))) @@ -1128,19 +1081,66 @@ and xlate_tactic = | ((s, l) as it) when (is_tactic_special_case s) -> tactic_special_case xlate_tactic cvt_arg it | "APP", (Nvar(_,s))::l -> - let f = fun x -> CT_coerce_FORMULA_to_TACTIC_ARG x in let args = List.map (function - Node(_, "COMMAND", [x]) -> f (xlate_formula x) - | x -> f (xlate_formula x)) l in + | Node(_, "COMMAND", [x]) -> + CT_coerce_FORMULA_to_TACTIC_ARG (xlate_formula x) + | x -> + CT_coerce_TACTIC_COM_to_TACTIC_ARG(xlate_tactic x)) + l in let fst,args2 = match args with fst::args2 -> fst, args2 | _ -> assert false in CT_simple_user_tac(CT_ident s, CT_tactic_arg_list(fst, args2)) + | "MATCH", exp::rules -> + CT_match_tac(mk_let_value exp, + match List.map + (function + | Node(_,"MATCHRULE", + [Node(_,"TERM", [Node(_,"COMMAND", [p])]); + tac]) -> + CT_match_tac_rule( + CT_coerce_FORMULA_to_CONTEXT_PATTERN + (xlate_formula p), + mk_let_value tac) + | Node(_,"MATCHRULE", [tac]) -> + CT_match_tac_rule + (CT_coerce_FORMULA_to_CONTEXT_PATTERN + CT_existvarc, + mk_let_value tac) + | Node((l1,l2),s,_) -> + failwith ("problem with match_tac at " ^ + (string_of_int l1) ^ + " " ^ + (string_of_int l2) ^ + ": " ^ s) + | _ -> assert false) rules with + | [] -> assert false + | fst::others -> + CT_match_tac_rules(fst, others)) | "MATCHCONTEXT", rule1::rules -> CT_match_context(xlate_context_rule rule1, List.map xlate_context_rule rules) + | "LET", [Node(_, "LETDECL",l); + t] -> + let cvt_clause = + function + | Node(_, "LETCLAUSE", [Nvar(_, s);Node(_,"COMMAND",[v])]) -> + CT_let_clause(CT_ident s, + CT_coerce_DEF_BODY_to_LET_VALUE + (formula_to_def_body v)) + | Node(_, "LETCLAUSE", [Nvar(_, s); v]) -> + CT_let_clause(CT_ident s, + CT_coerce_TACTIC_COM_to_LET_VALUE + (xlate_tactic v)) + | Node(_, s, _) -> failwith ("cvt_clause : unexpected " ^ s) + | _ -> assert false in + let cl_l = List.map cvt_clause l in + (match cl_l with + | [] -> assert false + | fst::others -> + CT_lettac (CT_let_clauses(fst, others), mk_let_value t)) | s, l -> xlate_tac (s, List.map cvt_arg l)) | Nvar(_, s) -> ident_tac s | the_node -> xlate_error ("xlate_tactic at " ^ @@ -1349,7 +1349,7 @@ and xlate_tac = CT_clear (CT_id_ne_list (id, idl)) | _ -> xlate_error "Clear expects a non empty list of identifiers") | (*For translating tactics/Inv.v *) - "Inv", [Targ_ident (CT_ident s); Targ_ident id] -> + "Inv", [Targ_string (CT_string s); Targ_ident id] -> CT_inversion (compute_INV_TYPE_from_string s, id, CT_id_list []) | "InvIn", ((Targ_ident (CT_ident s))::((Targ_ident id) :: idlist)) -> CT_inversion @@ -1383,7 +1383,31 @@ and (xlate_context_rule: Ctast.t -> ct_CONTEXT_RULE) = | _ -> assert false in let hyps, cpat, tactic = xlate_ctxt_rule_aux parts in CT_context_rule(CT_context_hyp_list hyps, cpat, tactic) - | _ -> assert false;; + | _ -> assert false +and (formula_to_def_body : Ctast.t -> ct_DEF_BODY) = + function + | Node(_, "EVAL", [f;Node(_, "REDEXP", [tac])]) -> + (try + CT_coerce_EVAL_CMD_to_DEF_BODY( + CT_eval(CT_coerce_NONE_to_INT_OPT CT_none, + xlate_red_tactic tac, + xlate_formula f)) + with Failure s -> + failwith ("error raised inside formula_to_def_body " ^ + s)) + | f -> (try ct_coerce_FORMULA_to_DEF_BODY(xlate_formula f) + with Failure s -> + match f with + Node(_,s1, _) -> + failwith ("error raised inside formula_to_def_body (2) " ^ + s1 ^ " " ^ s) + | _ -> + failwith("error raised inside formula_to_def_body (3) " ^ + s)) +and mk_let_value = function + Node(_, "COMMAND", [v]) -> + CT_coerce_DEF_BODY_to_LET_VALUE(formula_to_def_body v) + | v -> CT_coerce_TACTIC_COM_to_LET_VALUE(xlate_tactic v);; let strip_varg_int = function @@ -1532,7 +1556,7 @@ let get_require_flags impexp spec = let cvt_optional_eval_for_definition c1 optional_eval = match optional_eval with - None -> CT_coerce_FORMULA_to_DEF_BODY c1 + None -> ct_coerce_FORMULA_to_DEF_BODY c1 | Some (Targ_redexp red_com) -> CT_coerce_EVAL_CMD_to_DEF_BODY( CT_eval(CT_coerce_NONE_to_INT_OPT CT_none, |