summaryrefslogtreecommitdiff
path: root/contrib/interface
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/interface')
-rw-r--r--contrib/interface/ascent.mli2
-rw-r--r--contrib/interface/blast.ml28
-rw-r--r--contrib/interface/centaur.ml422
-rw-r--r--contrib/interface/dad.ml2
-rw-r--r--contrib/interface/depends.ml6
-rw-r--r--contrib/interface/name_to_ast.ml8
-rw-r--r--contrib/interface/parse.ml4
-rw-r--r--contrib/interface/paths.ml2
-rw-r--r--contrib/interface/pbp.ml2
-rw-r--r--contrib/interface/showproof.ml3
-rw-r--r--contrib/interface/vtp.ml2
-rw-r--r--contrib/interface/xlate.ml114
12 files changed, 118 insertions, 77 deletions
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index 32338523..2eb2c381 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -76,7 +76,7 @@ and ct_COMMAND =
| CT_go of ct_INT_OR_LOCN
| CT_guarded
| CT_hint_destruct of ct_ID * ct_INT * ct_DESTRUCT_LOCATION * ct_FORMULA * ct_TACTIC_COM * ct_ID_LIST
- | CT_hint_extern of ct_INT * ct_FORMULA * ct_TACTIC_COM * ct_ID_LIST
+ | CT_hint_extern of ct_INT * ct_FORMULA_OPT * ct_TACTIC_COM * ct_ID_LIST
| CT_hintrewrite of ct_ORIENTATION * ct_FORMULA_NE_LIST * ct_ID * ct_TACTIC_COM
| CT_hints of ct_ID * ct_ID_NE_LIST * ct_ID_LIST
| CT_hints_immediate of ct_FORMULA_NE_LIST * ct_ID_LIST
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 767a7dd6..483453cb 100644
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -148,6 +148,8 @@ let pp_string x =
(* A tactic similar to Auto, but using EApply, Assumption and e_give_exact *)
(***************************************************************************)
+let priority l = List.map snd (List.filter (fun (pr,_) -> pr = 0) l)
+
let unify_e_resolve (c,clenv) gls =
let clenv' = connect_clenv gls clenv in
let _ = clenv_unique_resolver false clenv' gls in
@@ -190,12 +192,11 @@ and e_my_find_search db_list local_db hdc concl =
tclTHEN (unify_e_resolve (term,cl))
(e_trivial_fail_db db_list local_db)
| Unfold_nth c -> unfold_in_concl [all_occurrences,c]
- | Extern tacast -> Auto.conclPattern concl
- (Option.get p) tacast
+ | Extern tacast -> Auto.conclPattern concl p tacast
in
- (free_try tac,fmt_autotactic t))
+ (free_try tac,pr_autotactic t))
(*i
- fun gls -> pPNL (fmt_autotactic t); Format.print_flush ();
+ fun gls -> pPNL (pr_autotactic t); Format.print_flush ();
try tac gls
with e when Logic.catchable_exception(e) ->
(Format.print_string "Fail\n";
@@ -207,14 +208,14 @@ and e_my_find_search db_list local_db hdc concl =
and e_trivial_resolve db_list local_db gl =
try
- Auto.priority
+ priority
(e_my_find_search db_list local_db
- (List.hd (head_constr_bound gl [])) gl)
+ (fst (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)
+ (fst (head_constr_bound gl)) gl)
with Bound | Not_found -> []
let assumption_tac_list id = apply_tac_list (e_give_exact_constr (mkVar id))
@@ -406,13 +407,12 @@ and my_find_search db_list local_db hdc concl =
(unify_resolve st (term,cl))
(trivial_fail_db db_list local_db)
| Unfold_nth c -> unfold_in_concl [all_occurrences,c]
- | Extern tacast ->
- conclPattern concl (Option.get p) tacast))
+ | Extern tacast -> conclPattern concl p tacast))
tacl
and trivial_resolve db_list local_db cl =
try
- let hdconstr = List.hd (head_constr_bound cl []) in
+ let hdconstr = fst (head_constr_bound cl) in
priority
(my_find_search db_list local_db (head_of_constr_reference hdconstr) cl)
with Bound | Not_found ->
@@ -424,7 +424,7 @@ and trivial_resolve db_list local_db cl =
let possible_resolve db_list local_db cl =
try
- let hdconstr = List.hd (head_constr_bound cl []) in
+ let hdconstr = fst (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 ->
@@ -432,8 +432,8 @@ let possible_resolve db_list local_db cl =
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
+ let t = head_constr typc in
+ if Hipattern.is_conjunction (applist t) then
simplest_case c gls
else
errorlabstrm "Auto.decomp_unary_term" (str "not a unary type")
@@ -473,7 +473,7 @@ let rec search_gen decomp n db_list local_db extra_sign goal =
let hintl =
try
[make_apply_entry (pf_env g') (project g')
- (true,false)
+ (true,true,false)
None
(mkVar hid,htyp)]
with Failure _ -> []
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index a4dc0eac..51dce4f7 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -545,8 +545,12 @@ let solve_hook n =
let abort_hook s = output_results_nl (ctf_AbortedMessage !global_request_id s)
let interp_search_about_item = function
- | SearchRef qid -> GlobSearchRef (Nametab.global qid)
- | SearchString s -> GlobSearchString s
+ | SearchSubPattern pat ->
+ let _,pat = Constrintern.intern_constr_pattern Evd.empty (Global.env()) pat in
+ GlobSearchSubPattern pat
+ | SearchString (s,_) ->
+ warning "Notation case not taken into account";
+ GlobSearchString s
let pcoq_search s l =
(* LEM: I don't understand why this is done in this way (redoing the
@@ -559,12 +563,12 @@ let pcoq_search s l =
begin match s with
| SearchAbout sl ->
raw_search_about (filter_by_module_from_list l) add_search
- (List.map interp_search_about_item sl)
+ (List.map (on_snd interp_search_about_item) sl)
| SearchPattern c ->
- let _,pat = interp_constrpattern Evd.empty (Global.env()) c in
+ let _,pat = intern_constr_pattern Evd.empty (Global.env()) c in
raw_pattern_search (filter_by_module_from_list l) add_search pat
| SearchRewrite c ->
- let _,pat = interp_constrpattern Evd.empty (Global.env()) c in
+ let _,pat = intern_constr_pattern Evd.empty (Global.env()) c in
raw_search_rewrite (filter_by_module_from_list l) add_search pat;
| SearchHead locqid ->
filtered_search
@@ -579,7 +583,7 @@ let rec hyp_pattern_filter pat name a c =
| Prod(_, hyp, c2) ->
(try
(* let _ = msgnl ((str "WHOLE ") ++ (Printer.pr_lconstr c)) in
- let _ = msgnl ((str "PAT ") ++ (Printer.pr_pattern pat)) in *)
+ let _ = msgnl ((str "PAT ") ++ (Printer.pr_constr_pattern pat)) in *)
if Matching.is_matching pat hyp then
(msgnl (str "ok"); true)
else
@@ -589,7 +593,7 @@ let rec hyp_pattern_filter pat name a c =
| _ -> false;;
let hyp_search_pattern c l =
- let _, pat = interp_constrpattern Evd.empty (Global.env()) c in
+ let _, pat = intern_constr_pattern Evd.empty (Global.env()) c in
ctv_SEARCH_LIST := [];
gen_filtered_search
(fun s a c -> (filter_by_module_from_list l s a c &&
@@ -638,8 +642,8 @@ let pcoq_term_pr = {
* Except with right bool/env which I'll get :)
*)
pr_lconstr_expr = (fun c -> fFORMULA (xlate_formula c) ++ str "(pcoq_lconstr_expr of " ++ (default_term_pr.pr_lconstr_expr c) ++ str ")");
- pr_pattern_expr = (fun c -> str "pcoq_pattern_expr\n" ++ (default_term_pr.pr_pattern_expr c));
- pr_lpattern_expr = (fun c -> str "pcoq_constr_expr\n" ++ (default_term_pr.pr_lpattern_expr c))
+ pr_constr_pattern_expr = (fun c -> str "pcoq_pattern_expr\n" ++ (default_term_pr.pr_constr_pattern_expr c));
+ pr_lconstr_pattern_expr = (fun c -> str "pcoq_constr_expr\n" ++ (default_term_pr.pr_lconstr_pattern_expr c))
}
let start_pcoq_trees () =
diff --git a/contrib/interface/dad.ml b/contrib/interface/dad.ml
index 8096bc31..c2ab2dc8 100644
--- a/contrib/interface/dad.ml
+++ b/contrib/interface/dad.ml
@@ -99,7 +99,7 @@ let rec find_cmd (l:(string * dad_rule) list) env constr p p1 p2 =
with
Failure s -> failwith "internal" in
let _, constr_pat =
- interp_constrpattern Evd.empty (Global.env())
+ intern_constr_pattern Evd.empty (Global.env())
((*ct_to_ast*) pat) in
let subst = matches constr_pat term_to_match in
if (is_prefix p_f (p_r@p1)) & (is_prefix p_l (p_r@p2)) then
diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml
index 203bc9e3..e59de34a 100644
--- a/contrib/interface/depends.ml
+++ b/contrib/interface/depends.ml
@@ -67,6 +67,7 @@ let explore_tree pfs =
| Move (bool, identifier, identifier') -> "Move"
| Rename (identifier, identifier') -> "Rename"
| Change_evars -> "Change_evars"
+ | Order _ -> "Order"
in
let pt = proof_of_pftreestate pfs in
(* We expect 0 *)
@@ -280,8 +281,8 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of
| TacExact c
| TacExactNoCheck c
| TacVmCastNoCheck c -> depends_of_'constr c acc
- | TacApply (_, _, [cb]) -> depends_of_'constr_with_bindings cb acc
- | TacApply (_, _, _) -> failwith "TODO"
+ | TacApply (_, _, [cb], None) -> depends_of_'constr_with_bindings cb acc
+ | TacApply (_, _, _, _) -> failwith "TODO"
| TacElim (_, cwb, cwbo) ->
depends_of_'constr_with_bindings cwb
(Option.fold_right depends_of_'constr_with_bindings cwbo acc)
@@ -420,6 +421,7 @@ and depends_of_prim_rule pr acc = match pr with
| Move _ -> acc
| Rename _ -> acc
| Change_evars -> acc
+ | Order _ -> acc
let rec depends_of_pftree pt acc =
match pt.ref with
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index 6b17e739..0dc8f024 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -107,10 +107,10 @@ let convert_one_inductive sp tyi =
let env = Global.env () in
let envpar = push_rel_context params env in
let sp = sp_of_global (IndRef (sp, tyi)) in
- (((dummy_loc,basename sp),
+ (((false,(dummy_loc,basename sp)),
convert_env(List.rev params),
- (extern_constr true envpar arity),
- convert_constructors envpar cstrnames cstrtypes), None);;
+ Some (extern_constr true envpar arity), Vernacexpr.Inductive_kw ,
+ Constructors (convert_constructors envpar cstrnames cstrtypes)), None);;
(* This function converts a Mutual inductive definition to a Coqast.t.
It is obtained directly from print_mutual in pretty.ml. However, all
@@ -121,7 +121,7 @@ let mutual_to_ast_list sp mib =
let _, l =
Array.fold_right
(fun mi (n,l) -> (n+1, (convert_one_inductive sp n)::l)) mipv (0, []) in
- VernacInductive (mib.mind_finite, l)
+ VernacInductive ((if mib.mind_finite then Decl_kinds.Finite else Decl_kinds.CoFinite), l)
:: (implicit_args_to_ast_list sp mipv);;
let constr_to_ast v =
diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index bf8614b4..1bbab5fe 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/parse.ml
@@ -330,7 +330,7 @@ let add_path_action reqid string_arg =
let print_version_action () =
msgnl (mt ());
- msgnl (str "$Id: parse.ml 9476 2007-01-10 15:44:44Z lmamane $");;
+ msgnl (str "$Id: parse.ml 11749 2009-01-05 14:01:04Z notin $");;
let load_syntax_action reqid module_name =
msg (str "loading " ++ str module_name ++ str "... ");
@@ -370,7 +370,7 @@ Libobject.relax true;
(let coqdir =
try Sys.getenv "COQDIR"
with Not_found ->
- let coqdir = Coq_config.coqlib in
+ let coqdir = Envars.coqlib () in
if Sys.file_exists coqdir then
coqdir
else
diff --git a/contrib/interface/paths.ml b/contrib/interface/paths.ml
index b1244d15..a157ca92 100644
--- a/contrib/interface/paths.ml
+++ b/contrib/interface/paths.ml
@@ -23,4 +23,4 @@ let rec lex_smaller p1 p2 = match p1,p2 with
[], _ -> true
| a::tl1, b::tl2 when a < b -> true
| a::tl1, b::tl2 when a = b -> lex_smaller tl1 tl2
-| _ -> false;; \ No newline at end of file
+| _ -> false;;
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index 65eadf13..01747aa5 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -171,7 +171,7 @@ let make_pbp_atomic_tactic = function
| PbpRight -> TacAtom (zz, TacRight (false,NoBindings))
| PbpIntros l -> TacAtom (zz, TacIntroPattern l)
| PbpLApply h -> TacAtom (zz, TacLApply (make_var h))
- | PbpApply h -> TacAtom (zz, TacApply (true,false,[make_var h,NoBindings]))
+ | PbpApply h -> TacAtom (zz, TacApply (true,false,[make_var h,NoBindings],None))
| PbpElim (hyp_name, names) ->
let bind = List.map (fun s ->(zz,NamedHyp s,make_pbp_pattern s)) names in
TacAtom
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index 4b9c1332..cf861642 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -1202,7 +1202,8 @@ let rec natural_ntree ig ntree =
| TacExtend (_,"InductionIntro",[a]) ->
let id=(out_gen wit_ident a) in
natural_induction ig lh g gs ge id ltree true
- | TacApply (_,false,[c,_]) -> natural_apply ig lh g gs (snd c) ltree
+ | TacApply (_,false,[c,_],None) ->
+ natural_apply ig lh g gs (snd c) ltree
| TacExact c -> natural_exact ig lh g gs (snd c) ltree
| TacCut c -> natural_cut ig lh g gs (snd c) ltree
| TacExtend (_,"CutIntro",[a]) ->
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 551ad3a3..94609009 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -246,7 +246,7 @@ and fCOMMAND = function
fNODE "hint_destruct" 6
| CT_hint_extern(x1, x2, x3, x4) ->
fINT x1 ++
- fFORMULA x2 ++
+ fFORMULA_OPT x2 ++
fTACTIC_COM x3 ++
fID_LIST x4 ++
fNODE "hint_extern" 4
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index da4908e5..e3cd56a0 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -7,6 +7,7 @@ open Names;;
open Ascent;;
open Genarg;;
open Rawterm;;
+open Termops;;
open Tacexpr;;
open Vernacexpr;;
open Decl_kinds;;
@@ -274,9 +275,11 @@ let rec xlate_match_pattern =
CT_coerce_NUM_to_MATCH_PATTERN
(CT_int_encapsulator(Bigint.to_string n))
| CPatPrim (_,String _) -> xlate_error "CPatPrim (String): TODO"
- | CPatNotation(_, s, l) ->
+ | CPatNotation(_, s, (l,[])) ->
CT_pattern_notation(CT_string s,
CT_match_pattern_list(List.map xlate_match_pattern l))
+ | CPatNotation(_, s, (l,_)) ->
+ xlate_error "CPatNotation (recursive notation): TODO"
;;
@@ -373,6 +376,7 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
(xlate_formula f, List.map xlate_formula_expl l'))
| CApp(_, (_,f), l) ->
CT_appc(xlate_formula f, xlate_formula_expl_ne_list l)
+ | CRecord (_,_,_) -> xlate_error "CRecord: TODO"
| CCases (_, _, _, [], _) -> assert false
| CCases (_, _, ret_type, tm::tml, eqns)->
CT_cases(CT_matched_formula_ne_list(xlate_matched_formula tm,
@@ -392,7 +396,9 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
xlate_formula b1, xlate_formula b2)
| CSort(_, s) -> CT_coerce_SORT_TYPE_to_FORMULA(xlate_sort s)
- | CNotation(_, s, l) -> notation_to_formula s (List.map xlate_formula l)
+ | CNotation(_, s,(l,[])) -> notation_to_formula s (List.map xlate_formula l)
+ | CNotation(_, s,(l,_)) -> xlate_error "CNotation (recursive): TODO"
+ | CGeneralization(_,_,_,_) -> xlate_error "CGeneralization: TODO"
| CPrim (_, Numeral i) ->
CT_coerce_NUM_to_FORMULA(CT_int_encapsulator(Bigint.to_string i))
| CPrim (_, String _) -> xlate_error "CPrim (String): TODO"
@@ -642,12 +648,14 @@ let is_tactic_special_case = function
let xlate_context_pattern = function
| Term v ->
CT_coerce_FORMULA_to_CONTEXT_PATTERN (xlate_formula v)
- | Subterm (idopt, v) ->
+ | Subterm (b, idopt, v) -> (* TODO: application pattern *)
CT_context(xlate_ident_opt idopt, xlate_formula v)
let xlate_match_context_hyps = function
- | Hyp (na,b) -> CT_premise_pattern(xlate_id_opt na, xlate_context_pattern b);;
+ | Hyp (na,b) -> CT_premise_pattern(xlate_id_opt na, xlate_context_pattern b)
+ | Def (na,b,t) -> xlate_error "TODO: Let hyps"
+ (* CT_premise_pattern(xlate_id_opt na, xlate_context_pattern b, xlate_context_pattern t);; *)
let xlate_arg_to_id_opt = function
Some id -> CT_coerce_ID_to_ID_OPT(CT_ident (string_of_id id))
@@ -1155,12 +1163,12 @@ and xlate_tac =
xlate_error "TODO: trivial using"
| TacReduce (red, l) ->
CT_reduce (xlate_red_tactic red, xlate_clause l)
- | TacApply (true,false,[c,bindl]) ->
+ | TacApply (true,false,[c,bindl],None) ->
CT_apply (xlate_formula c, xlate_bindings bindl)
- | TacApply (true,true,[c,bindl]) ->
+ | TacApply (true,true,[c,bindl],None) ->
CT_eapply (xlate_formula c, xlate_bindings bindl)
- | TacApply (_,_,_) ->
- xlate_error "TODO: simple (e)apply and iterated apply"
+ | TacApply (_,_,_,_) ->
+ xlate_error "TODO: simple (e)apply and iterated apply and apply in"
| TacConstructor (false,n_or_meta, bindl) ->
let n = match n_or_meta with AI n -> n | MetaId _ -> xlate_error ""
in CT_constructor (CT_int n, xlate_bindings bindl)
@@ -1248,13 +1256,13 @@ and xlate_tac =
but the structures are different *)
xlate_clause cl)
| TacLetTac (na, c, cl, false) -> xlate_error "TODO: remember"
- | TacAssert (None, (_,IntroIdentifier id), c) ->
+ | TacAssert (None, Some (_,IntroIdentifier id), c) ->
CT_assert(xlate_id_opt ((0,0),Name id), xlate_formula c)
- | TacAssert (None, (_,IntroAnonymous), c) ->
+ | TacAssert (None, None, c) ->
CT_assert(xlate_id_opt ((0,0),Anonymous), xlate_formula c)
- | TacAssert (Some (TacId []), (_,IntroIdentifier id), c) ->
+ | TacAssert (Some (TacId []), Some (_,IntroIdentifier id), c) ->
CT_truecut(xlate_id_opt ((0,0),Name id), xlate_formula c)
- | TacAssert (Some (TacId []), (_,IntroAnonymous), c) ->
+ | TacAssert (Some (TacId []), None, c) ->
CT_truecut(xlate_id_opt ((0,0),Anonymous), xlate_formula c)
| TacAssert _ ->
xlate_error "TODO: assert with 'as' and 'by' and pose proof with 'as'"
@@ -1302,11 +1310,13 @@ and coerce_genarg_to_TARG x =
(CT_coerce_ID_to_ID_OR_INT id))
| IntroPatternArgType ->
xlate_error "TODO"
- | IdentArgType ->
+ | IdentArgType true ->
let id = xlate_ident (out_gen rawwit_ident x) in
CT_coerce_FORMULA_OR_INT_to_TARG
(CT_coerce_ID_OR_INT_to_FORMULA_OR_INT
(CT_coerce_ID_to_ID_OR_INT id))
+ | IdentArgType false ->
+ xlate_error "TODO"
| VarArgType ->
let id = xlate_ident (snd (out_gen rawwit_var x)) in
CT_coerce_FORMULA_OR_INT_to_TARG
@@ -1400,11 +1410,13 @@ let coerce_genarg_to_VARG x =
(CT_coerce_ID_to_ID_OPT id))
| IntroPatternArgType ->
xlate_error "TODO"
- | IdentArgType ->
+ | IdentArgType true ->
let id = xlate_ident (out_gen rawwit_ident x) in
CT_coerce_ID_OPT_OR_ALL_to_VARG
(CT_coerce_ID_OPT_to_ID_OPT_OR_ALL
(CT_coerce_ID_to_ID_OPT id))
+ | IdentArgType false ->
+ xlate_error "TODO"
| VarArgType ->
let id = xlate_ident (snd (out_gen rawwit_var x)) in
CT_coerce_ID_OPT_OR_ALL_to_VARG
@@ -1489,7 +1501,7 @@ let build_constructors l =
CT_constr_list (List.map f l)
let build_record_field_list l =
- let build_record_field (coe,d) = match d with
+ let build_record_field ((coe,d),not) = match d with
| AssumExpr (id,c) ->
if coe then CT_recconstr_coercion (xlate_id_opt id, xlate_formula c)
else
@@ -1735,6 +1747,8 @@ let rec xlate_vernac =
(fst::rest) -> CT_formula_ne_list(fst,rest)
| _ -> assert false in
CT_hintrewrite(ct_orient, f_ne_list, CT_ident base, xlate_tactic t)
+ | VernacCreateHintDb (local,dbname,b) ->
+ xlate_error "TODO: VernacCreateHintDb"
| VernacHints (local,dbnames,h) ->
let dblist = CT_id_list(List.map (fun x -> CT_ident x) dbnames) in
(match h with
@@ -1749,7 +1763,10 @@ let rec xlate_vernac =
CT_hints(CT_ident "Constructors",
CT_id_ne_list(n1, names), dblist)
| HintsExtern (n, c, t) ->
- CT_hint_extern(CT_int n, xlate_formula c, xlate_tactic t, dblist)
+ let pat = match c with
+ | None -> CT_coerce_ID_OPT_to_FORMULA_OPT (CT_coerce_NONE_to_ID_OPT CT_none)
+ | Some c -> CT_coerce_FORMULA_to_FORMULA_OPT (xlate_formula c)
+ in CT_hint_extern(CT_int n, pat, xlate_tactic t, dblist)
| HintsImmediate l ->
let f1, formulas = match List.map xlate_formula l with
a :: tl -> a, tl
@@ -1768,7 +1785,7 @@ let rec xlate_vernac =
| HintsImmediate _ -> CT_hints_immediate(l', dblist)
| _ -> assert false)
| HintsResolve l ->
- let f1, formulas = match List.map xlate_formula (List.map snd l) with
+ let f1, formulas = match List.map xlate_formula (List.map pi3 l) with
a :: tl -> a, tl
| _ -> failwith "" in
let l' = CT_formula_ne_list(f1, formulas) in
@@ -1793,6 +1810,16 @@ let rec xlate_vernac =
CT_id_ne_list(n1, names), dblist)
else
CT_hints(CT_ident "Unfold", CT_id_ne_list(n1, names), dblist)
+ | HintsTransparency (l,b) ->
+ let n1, names = match List.map loc_qualid_to_ct_ID l with
+ n1 :: names -> n1, names
+ | _ -> failwith "" in
+ let ty = if b then "Transparent" else "Opaque" in
+ if local then
+ CT_local_hints(CT_ident ty,
+ CT_id_ne_list(n1, names), dblist)
+ else
+ CT_hints(CT_ident ty, CT_id_ne_list(n1, names), dblist)
| HintsDestruct(id, n, loc, f, t) ->
let dl = match loc with
ConclLocation() -> CT_conclusion_location
@@ -1859,7 +1886,8 @@ let rec xlate_vernac =
| PrintHint id ->
CT_print_hint (CT_coerce_ID_to_ID_OPT (loc_qualid_to_ct_ID id))
| PrintHintGoal -> CT_print_hint ctv_ID_OPT_NONE
- | PrintLoadPath -> CT_print_loadpath
+ | PrintLoadPath None -> CT_print_loadpath
+ | PrintLoadPath _ -> xlate_error "TODO: Print LoadPath dir"
| PrintMLLoadPath -> CT_ml_print_path
| PrintMLModules -> CT_ml_print_modules
| PrintGraph -> CT_print_graph
@@ -1878,7 +1906,6 @@ let rec xlate_vernac =
xlate_error "TODO: Print TypeClasses"
| PrintInspect n -> CT_inspect (CT_int n)
| PrintUniverses opt_s -> CT_print_universes(ctf_STRING_OPT opt_s)
- | PrintSetoids -> CT_print_setoids
| PrintTables -> CT_print_tables
| PrintModuleType a -> CT_print_module_type (loc_qualid_to_ct_ID a)
| PrintModule a -> CT_print_module (loc_qualid_to_ct_ID a)
@@ -1927,37 +1954,44 @@ let rec xlate_vernac =
| SearchRewrite c ->
CT_search_rewrite(xlate_formula c, translated_restriction)
| SearchAbout (a::l) ->
- let xlate_search_about_item it =
+ let xlate_search_about_item (b,it) =
+ if not b then xlate_error "TODO: negative searchabout constraint";
match it with
- SearchRef x ->
+ SearchSubPattern (CRef x) ->
CT_coerce_ID_to_ID_OR_STRING(loc_qualid_to_ct_ID x)
- | SearchString s ->
- CT_coerce_STRING_to_ID_OR_STRING(CT_string s) in
+ | SearchString (s,None) ->
+ CT_coerce_STRING_to_ID_OR_STRING(CT_string s)
+ | SearchString _ | SearchSubPattern _ ->
+ xlate_error
+ "TODO: search subpatterns or notation with explicit scope"
+ in
CT_search_about
(CT_id_or_string_ne_list(xlate_search_about_item a,
List.map xlate_search_about_item l),
translated_restriction)
| SearchAbout [] -> assert false)
- | (*Record from tactics/Record.v *)
- VernacRecord
- (_, (add_coercion, (_,s)), binders, c1,
- rec_constructor_or_none, field_list) ->
- let record_constructor =
- xlate_ident_opt (Option.map snd rec_constructor_or_none) in
- CT_record
- ((if add_coercion then CT_coercion_atm else
- CT_coerce_NONE_to_COERCION_OPT(CT_none)),
- xlate_ident s, xlate_binder_list binders,
- xlate_formula c1, record_constructor,
- build_record_field_list field_list)
+(* | (\*Record from tactics/Record.v *\) *)
+(* VernacRecord *)
+(* (_, (add_coercion, (_,s)), binders, c1, *)
+(* rec_constructor_or_none, field_list) -> *)
+(* let record_constructor = *)
+(* xlate_ident_opt (Option.map snd rec_constructor_or_none) in *)
+(* CT_record *)
+(* ((if add_coercion then CT_coercion_atm else *)
+(* CT_coerce_NONE_to_COERCION_OPT(CT_none)), *)
+(* xlate_ident s, xlate_binder_list binders, *)
+(* xlate_formula (Option.get c1), record_constructor, *)
+(* build_record_field_list field_list) *)
| VernacInductive (isind, lmi) ->
- let co_or_ind = if isind then "Inductive" else "CoInductive" in
- let strip_mutind (((_,s), parameters, c, constructors), notopt) =
+ let co_or_ind = if Decl_kinds.recursivity_flag_of_kind isind then "Inductive" else "CoInductive" in
+ let strip_mutind = function
+ (((_, (_,s)), parameters, c, _, Constructors constructors), notopt) ->
CT_ind_spec
- (xlate_ident s, xlate_binder_list parameters, xlate_formula c,
+ (xlate_ident s, xlate_binder_list parameters, xlate_formula (Option.get c),
build_constructors constructors,
- translate_opt_notation_decl notopt) in
+ translate_opt_notation_decl notopt)
+ | _ -> xlate_error "TODO: Record notation in (Co)Inductive" in
CT_mind_decl
(CT_co_ind co_or_ind, CT_ind_spec_list (List.map strip_mutind lmi))
| VernacFixpoint ([],_) -> xlate_error "mutual recursive"
@@ -2116,7 +2150,7 @@ let rec xlate_vernac =
(* Type Classes *)
| VernacDeclareInstance _|VernacContext _|
- VernacInstance (_, _, _, _, _)|VernacClass (_, _, _, _, _) ->
+ VernacInstance (_, _, _, _, _) ->
xlate_error "TODO: Type Classes commands"
| VernacResetName id -> CT_reset (xlate_ident (snd id))
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-19 06:34:26 +0000