aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/interface/Centaur.v3
-rw-r--r--contrib/interface/ascent.mli23
-rwxr-xr-xcontrib/interface/blast.ml627
-rw-r--r--contrib/interface/blast.mli5
-rw-r--r--contrib/interface/centaur.ml124
-rw-r--r--contrib/interface/parse.ml202
-rw-r--r--contrib/interface/pbp.ml50
-rw-r--r--contrib/interface/vernacrc1
-rw-r--r--contrib/interface/vtp.ml48
-rw-r--r--contrib/interface/xlate.ml248
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,
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-25 07:22:27 +0000