aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/interface
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/interface')
-rw-r--r--contrib/interface/ascent.mli10
-rw-r--r--contrib/interface/vtp.ml27
-rw-r--r--contrib/interface/xlate.ml54
3 files changed, 60 insertions, 31 deletions
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index 3b45f86a5..829972ecf 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -173,6 +173,7 @@ and ct_CONTEXT_PATTERN =
| CT_context of ct_ID_OPT * ct_FORMULA
and ct_CONTEXT_RULE =
CT_context_rule of ct_CONTEXT_HYP_LIST * ct_CONTEXT_PATTERN * ct_TACTIC_COM
+ | CT_def_context_rule of ct_TACTIC_COM
and ct_CONVERSION_FLAG =
CT_beta
| CT_delta
@@ -196,6 +197,7 @@ and ct_DEFN_OR_THM =
and ct_DEF_BODY =
CT_coerce_CONTEXT_PATTERN_to_DEF_BODY of ct_CONTEXT_PATTERN
| CT_coerce_EVAL_CMD_to_DEF_BODY of ct_EVAL_CMD
+ | CT_type_of of ct_FORMULA
and ct_DEF_BODY_OPT =
CT_coerce_DEF_BODY_to_DEF_BODY_OPT of ct_DEF_BODY
| CT_coerce_FORMULA_OPT_to_DEF_BODY_OPT of ct_FORMULA_OPT
@@ -231,7 +233,7 @@ and ct_FORMULA =
| CT_coerce_TYPED_FORMULA_to_FORMULA of ct_TYPED_FORMULA
| CT_appc of ct_FORMULA * ct_FORMULA_NE_LIST
| CT_arrowc of ct_FORMULA * ct_FORMULA
- | CT_bang of ct_INT_OPT * ct_FORMULA
+ | CT_bang of ct_FORMULA
| CT_cases of ct_MATCHED_FORMULA_NE_LIST * ct_FORMULA_OPT * ct_EQN_LIST
| CT_cofixc of ct_ID * ct_COFIX_REC_LIST
| CT_elimc of ct_CASE * ct_FORMULA_OPT * ct_FORMULA * ct_FORMULA_LIST
@@ -239,6 +241,7 @@ and ct_FORMULA =
| CT_fixc of ct_ID * ct_FIX_BINDER_LIST
| CT_if of ct_FORMULA * ct_ID_OPT * ct_FORMULA_OPT * ct_FORMULA * ct_FORMULA
| CT_inductive_let of ct_FORMULA_OPT * ct_ID_OPT_NE_LIST * ct_FORMULA * ct_FORMULA
+ | CT_labelled_arg of ct_ID * ct_FORMULA
| CT_lambdac of ct_BINDER_NE_LIST * ct_FORMULA
| CT_let_tuple of ct_ID_OPT_NE_LIST * ct_ID_OPT * ct_FORMULA_OPT * ct_FORMULA * ct_FORMULA
| CT_letin of ct_DEF * ct_FORMULA
@@ -538,7 +541,7 @@ and ct_TACTIC_COM =
| CT_induction of ct_ID_OR_INT
| CT_info of ct_TACTIC_COM
| CT_injection_eq of ct_ID_OR_INT_OPT
- | CT_instantiate of ct_INT * ct_FORMULA
+ | CT_instantiate of ct_INT * ct_FORMULA * ct_CLAUSE
| CT_intro of ct_ID_OPT
| CT_intro_after of ct_ID_OPT * ct_ID
| CT_intros of ct_INTRO_PATT_LIST
@@ -552,7 +555,7 @@ and ct_TACTIC_COM =
| CT_match_tac of ct_TACTIC_COM * ct_MATCH_TAC_RULES
| CT_move_after of ct_ID * ct_ID
| CT_new_destruct of ct_FORMULA_OR_INT * ct_USING * ct_ID_LIST_LIST
- | CT_new_induction of ct_FORMULA_OR_INT * ct_USING * ct_ID_LIST_LIST
+ | CT_new_induction of ct_FORMULA_OR_INT * ct_USING * ct_INTRO_PATT_LIST
| CT_omega
| CT_orelse of ct_TACTIC_COM * ct_TACTIC_COM
| CT_parallel of ct_TACTIC_COM * ct_TACTIC_COM list
@@ -561,6 +564,7 @@ and ct_TACTIC_COM =
| CT_prolog of ct_FORMULA_LIST * ct_INT
| CT_rec_tactic_in of ct_REC_TACTIC_FUN_LIST * ct_TACTIC_COM
| CT_reduce of ct_RED_COM * ct_CLAUSE
+ | CT_refine of ct_FORMULA
| CT_reflexivity
| CT_rename of ct_ID * ct_ID
| CT_repeat of ct_TACTIC_COM
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index f04c4beaf..eeb09b2a9 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -477,6 +477,9 @@ and fCONTEXT_RULE = function
fCONTEXT_PATTERN x2;
fTACTIC_COM x3;
fNODE "context_rule" 3
+| CT_def_context_rule(x1) ->
+ fTACTIC_COM x1;
+ fNODE "def_context_rule" 1
and fCONVERSION_FLAG = function
| CT_beta -> fNODE "beta" 0
| CT_delta -> fNODE "delta" 0
@@ -511,6 +514,9 @@ and fDEFN = function
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_type_of(x1) ->
+ fFORMULA x1;
+ fNODE "type_of" 1
and fDEF_BODY_OPT = function
| CT_coerce_DEF_BODY_to_DEF_BODY_OPT x -> fDEF_BODY x
| CT_coerce_FORMULA_OPT_to_DEF_BODY_OPT x -> fFORMULA_OPT x
@@ -585,10 +591,9 @@ and fFORMULA = function
fFORMULA x1;
fFORMULA x2;
fNODE "arrowc" 2
-| CT_bang(x1, x2) ->
- fINT_OPT x1;
- fFORMULA x2;
- fNODE "bang" 2
+| CT_bang(x1) ->
+ fFORMULA x1;
+ fNODE "bang" 1
| CT_cases(x1, x2, x3) ->
fMATCHED_FORMULA_NE_LIST x1;
fFORMULA_OPT x2;
@@ -622,6 +627,10 @@ and fFORMULA = function
fFORMULA x3;
fFORMULA x4;
fNODE "inductive_let" 4
+| CT_labelled_arg(x1, x2) ->
+ fID x1;
+ fFORMULA x2;
+ fNODE "labelled_arg" 2
| CT_lambdac(x1, x2) ->
fBINDER_NE_LIST x1;
fFORMULA x2;
@@ -1267,10 +1276,11 @@ and fTACTIC_COM = function
| CT_injection_eq(x1) ->
fID_OR_INT_OPT x1;
fNODE "injection_eq" 1
-| CT_instantiate(x1, x2) ->
+| CT_instantiate(x1, x2, x3) ->
fINT x1;
fFORMULA x2;
- fNODE "instantiate" 2
+ fCLAUSE x3;
+ fNODE "instantiate" 3
| CT_intro(x1) ->
fID_OPT x1;
fNODE "intro" 1
@@ -1325,7 +1335,7 @@ and fTACTIC_COM = function
| CT_new_induction(x1, x2, x3) ->
fFORMULA_OR_INT x1;
fUSING x2;
- fID_LIST_LIST x3;
+ fINTRO_PATT_LIST x3;
fNODE "new_induction" 3
| CT_omega -> fNODE "omega" 0
| CT_orelse(x1, x2) ->
@@ -1355,6 +1365,9 @@ and fTACTIC_COM = function
fRED_COM x1;
fCLAUSE x2;
fNODE "reduce" 2
+| CT_refine(x1) ->
+ fFORMULA x1;
+ fNODE "refine" 1
| CT_reflexivity -> fNODE "reflexivity" 0
| CT_rename(x1, x2) ->
fID x1;
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index a11d75d4d..2d6cca540 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -348,10 +348,10 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
let l', last = decompose_last l in
CT_proj(xlate_formula last,
CT_formula_ne_list
- (CT_bang(xlate_int_opt None, varc (xlate_reference r)),
+ (CT_bang(varc (xlate_reference r)),
List.map xlate_formula l'))
| CAppExpl(_, (None, r), l) ->
- CT_appc(CT_bang(xlate_int_opt None, varc (xlate_reference r)),
+ CT_appc(CT_bang(varc (xlate_reference r)),
xlate_formula_ne_list l)
| CApp(_, (Some n,f), l) ->
let l', last = decompose_last l in
@@ -407,8 +407,11 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
(CT_typed_formula(xlate_formula e, xlate_formula t))
| CPatVar (_, (_,i)) when is_int_meta i ->
CT_coerce_ID_to_FORMULA(CT_metac (CT_int (int_of_meta i)))
- | CPatVar (_, _) -> xlate_error "TODO: meta as ident"
- | CEvar (_, _) -> xlate_error "TODO: evars"
+ | CPatVar (_, (false, s)) ->
+ CT_coerce_ID_to_FORMULA(CT_metaid (string_of_id s))
+ | CPatVar (_, (true, s)) ->
+ xlate_error "Second order variable not supported"
+ | CEvar (_, _) -> xlate_error "CEvar not supported"
| CCoFix (_, (_, id), lm::lmi) ->
let strip_mutcorec (fid, arf, ardef) =
CT_cofix_rec (xlate_ident fid, xlate_formula arf, xlate_formula ardef) in
@@ -445,9 +448,9 @@ and xlate_matched_formula = function
and xlate_formula_expl = function
(a, None) -> xlate_formula a
| (a, Some (_,ExplByPos i)) ->
- CT_bang(xlate_int_opt (Some i), xlate_formula a)
+ xlate_error "explicitation of implicit by rank not supported"
| (a, Some (_,ExplByName i)) ->
- xlate_error "TODO: explicitation of implicit by name"
+ CT_labelled_arg(CT_ident (string_of_id i), xlate_formula a)
and xlate_formula_expl_ne_list = function
[] -> assert false
| a::l -> CT_formula_ne_list(xlate_formula_expl a, List.map xlate_formula_expl l)
@@ -859,6 +862,9 @@ and xlate_tactic =
and xlate_tac =
function
+ | TacExtend (_, "refine", [c]) ->
+ CT_refine
+ (xlate_formula (out_gen rawwit_casted_open_constr c))
| TacExtend (_,"Absurd",[c]) ->
CT_absurd (xlate_formula (out_gen rawwit_constr c))
| TacChange (None, f, b) -> CT_change (xlate_formula f, xlate_clause b)
@@ -908,7 +914,6 @@ and xlate_tac =
| TacMove (true, id1, id2) ->
CT_move_after(xlate_hyp id1, xlate_hyp id2)
| TacMove (false, id1, id2) -> xlate_error "Non dep Move is only internal"
- | TacIntroPattern [] -> CT_intros (CT_intro_patt_list [])
| TacIntroPattern patt_list ->
CT_intros (CT_intro_patt_list (List.map xlate_intro_pattern patt_list))
| TacIntroMove (Some id, None) ->
@@ -1094,12 +1099,15 @@ and xlate_tac =
(List.map (fun l -> CT_id_list(List.map xlate_newind_names l)) c))
| TacNewInduction(a,b,(c,_)) ->
CT_new_induction
- (xlate_int_or_constr a, xlate_using b,
- CT_id_list_list
- (List.map (fun l -> CT_id_list(List.map xlate_newind_names l)) c))
- | TacInstantiate (a, b, _) ->
- xlate_error "TODO: Instantiate ... <clause>"
-
+ (xlate_int_or_constr a, xlate_using b,
+ (CT_intro_patt_list
+ (List.map (fun l ->
+ CT_conj_pattern
+ (CT_intro_patt_list
+ (List.map xlate_intro_pattern l))) c)))
+ | TacInstantiate (a, b, cl) ->
+ CT_instantiate(CT_int a, xlate_formula b,
+ xlate_clause cl)
| TacLetTac (na, c, cl) ->
CT_lettac(xlate_id_opt ((0,0),na), xlate_formula c,
(* TODO LATER: This should be shared with Unfold,
@@ -1124,7 +1132,7 @@ and xlate_tac =
(out_gen (wit_list0 rawwit_constr) arg)))
| TacExtend (_,id, l) ->
CT_user_tac (CT_ident id, CT_targ_list (List.map coerce_genarg_to_TARG l))
- | TacAlias _ -> xlate_error "TODO LATER: aliases"
+ | TacAlias _ -> xlate_error "Alias not supported"
and coerce_genarg_to_TARG x =
match Genarg.genarg_tag x with
@@ -1190,19 +1198,23 @@ and coerce_genarg_to_TARG x =
and xlate_context_rule =
function
| Pat (hyps, concl_pat, tactic) ->
- CT_context_rule(
- CT_context_hyp_list (List.map xlate_match_context_hyps hyps),
- xlate_context_pattern concl_pat, xlate_tactic tactic)
- | All te ->
- xlate_error "TODO: wildcard match_context_rule"
+ CT_context_rule
+ (CT_context_hyp_list (List.map xlate_match_context_hyps hyps),
+ xlate_context_pattern concl_pat, xlate_tactic tactic)
+ | All tactic ->
+ CT_def_context_rule (xlate_tactic tactic)
and formula_to_def_body =
function
| ConstrEval (red, f) ->
CT_coerce_EVAL_CMD_to_DEF_BODY(
CT_eval(CT_coerce_NONE_to_INT_OPT CT_none,
xlate_red_tactic red, xlate_formula f))
- | ConstrContext _ -> xlate_error "TODO: Inst"
- | ConstrTypeOf _ -> xlate_error "TODO: Check"
+ | ConstrContext((_, id), f) ->
+ CT_coerce_CONTEXT_PATTERN_to_DEF_BODY
+ (CT_context
+ (CT_coerce_ID_to_ID_OPT (CT_ident (string_of_id id)),
+ xlate_formula f))
+ | ConstrTypeOf f -> CT_type_of (xlate_formula f)
| ConstrTerm c -> ct_coerce_FORMULA_to_DEF_BODY(xlate_formula c)
and mk_let_value = function
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 02:37:12 +0000