diff options
-rw-r--r-- | contrib/interface/ascent.mli | 10 | ||||
-rw-r--r-- | contrib/interface/vtp.ml | 27 | ||||
-rw-r--r-- | contrib/interface/xlate.ml | 54 |
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 |