diff options
-rw-r--r-- | contrib/interface/ascent.mli | 551 | ||||
-rw-r--r-- | contrib/interface/centaur.ml | 810 | ||||
-rw-r--r-- | contrib/interface/dad.ml | 357 | ||||
-rw-r--r-- | contrib/interface/dad.mli | 10 | ||||
-rw-r--r-- | contrib/interface/debug_tac.ml | 474 | ||||
-rw-r--r-- | contrib/interface/debug_tac.mli | 6 | ||||
-rw-r--r-- | contrib/interface/history.ml | 373 | ||||
-rw-r--r-- | contrib/interface/history.mli | 12 | ||||
-rw-r--r-- | contrib/interface/name_to_ast.ml | 247 | ||||
-rw-r--r-- | contrib/interface/name_to_ast.mli | 2 | ||||
-rw-r--r-- | contrib/interface/paths.ml | 26 | ||||
-rw-r--r-- | contrib/interface/paths.mli | 4 | ||||
-rw-r--r-- | contrib/interface/pbp.ml | 705 | ||||
-rw-r--r-- | contrib/interface/pbp.mli | 4 | ||||
-rw-r--r-- | contrib/interface/translate.ml | 160 | ||||
-rw-r--r-- | contrib/interface/translate.mli | 8 | ||||
-rw-r--r-- | contrib/interface/vtp.ml | 1282 | ||||
-rw-r--r-- | contrib/interface/vtp.mli | 14 | ||||
-rw-r--r-- | contrib/interface/xlate.ml | 2026 | ||||
-rw-r--r-- | contrib/interface/xlate.mli | 14 |
20 files changed, 7085 insertions, 0 deletions
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli new file mode 100644 index 000000000..07487e82b --- /dev/null +++ b/contrib/interface/ascent.mli @@ -0,0 +1,551 @@ +type ct_ASSOC = + CT_coerce_NONE_to_ASSOC of ct_NONE + | CT_lefta + | CT_nona + | CT_righta +and ct_AST = + CT_coerce_ID_OR_INT_to_AST of ct_ID_OR_INT + | CT_coerce_ID_OR_STRING_to_AST of ct_ID_OR_STRING + | CT_astnode of ct_ID * ct_AST_LIST + | CT_astpath of ct_ID_LIST * ct_ID + | CT_astslam of ct_ID_OPT * ct_AST +and ct_AST_LIST = + CT_ast_list of ct_AST list +and ct_BINARY = + CT_binary of int +and ct_BINDER = + CT_binder of ct_ID_OPT_NE_LIST * ct_FORMULA +and ct_BINDER_LIST = + CT_binder_list of ct_BINDER list +and ct_BINDER_NE_LIST = + CT_binder_ne_list of ct_BINDER * ct_BINDER list +and ct_BINDING = + CT_binding of ct_ID_OR_INT * ct_FORMULA +and ct_BINDING_LIST = + CT_binding_list of ct_BINDING list +and ct_BOOL = + CT_false + | CT_true +and ct_CASE = + CT_case of string +and ct_COERCION_OPT = + CT_coerce_NONE_to_COERCION_OPT of ct_NONE + | CT_coercion_atm +and ct_COFIXTAC = + CT_cofixtac of ct_ID * ct_FORMULA +and ct_COFIX_REC = + CT_cofix_rec of ct_ID * ct_FORMULA * ct_FORMULA +and ct_COFIX_REC_LIST = + CT_cofix_rec_list of ct_COFIX_REC * ct_COFIX_REC list +and ct_COFIX_TAC_LIST = + CT_cofix_tac_list of ct_COFIXTAC list +and ct_COMMAND = + CT_coerce_COMMAND_LIST_to_COMMAND of ct_COMMAND_LIST + | CT_coerce_EVAL_CMD_to_COMMAND of ct_EVAL_CMD + | CT_coerce_IMPEXP_to_COMMAND of ct_IMPEXP + | CT_coerce_SECTION_BEGIN_to_COMMAND of ct_SECTION_BEGIN + | CT_coerce_THEOREM_GOAL_to_COMMAND of ct_THEOREM_GOAL + | CT_abort of ct_ID_OPT_OR_ALL + | CT_abstraction of ct_ID * ct_FORMULA * ct_INT_LIST + | CT_add_natural_feature of ct_NATURAL_FEATURE * ct_ID + | CT_addpath of ct_STRING + | CT_cd of ct_STRING_OPT + | CT_check of ct_FORMULA + | CT_class of ct_ID + | CT_coercion of ct_LOCAL_OPT * ct_IDENTITY_OPT * ct_ID * ct_ID * ct_ID + | CT_cofix_decl of ct_COFIX_REC_LIST + | CT_compile_module of ct_VERBOSE_OPT * ct_ID * ct_STRING_OPT + | CT_definition of ct_DEFN * ct_ID * ct_DEF_BODY * ct_FORMULA_OPT + | CT_delpath of ct_STRING + | CT_derive_depinversion of ct_INV_TYPE * ct_ID * ct_FORMULA * ct_SORT_TYPE + | CT_derive_inversion of ct_INV_TYPE * ct_INT_OPT * ct_ID * ct_ID + | CT_derive_inversion_with of ct_INV_TYPE * ct_ID * ct_FORMULA * ct_SORT_TYPE + | CT_explain_proof of ct_INT_LIST + | CT_explain_prooftree of ct_INT_LIST + | CT_fix_decl of ct_FIX_REC_LIST + | CT_focus of ct_INT_OPT + | CT_go of ct_INT_OR_LOCN + | CT_guarded + | CT_hint of ct_ID * ct_ID_LIST * ct_HINT_EXPRESSION + | 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_ind_scheme of ct_SCHEME_SPEC_LIST + | CT_infix of ct_ASSOC * ct_INT * ct_STRING * ct_ID + | CT_inspect of ct_INT + | CT_kill_node of ct_INT + | CT_load of ct_VERBOSE_OPT * ct_ID_OR_STRING + | CT_mind_decl of ct_CO_IND * ct_IND_SPEC_LIST + | CT_ml_add_path of ct_STRING + | CT_ml_declare_modules of ct_STRING_NE_LIST + | CT_ml_print_modules + | CT_ml_print_path + | CT_module of ct_ID + | CT_omega_flag of ct_OMEGA_MODE * ct_OMEGA_FEATURE + | CT_opaque of ct_ID_NE_LIST + | CT_parameter of ct_BINDER + | CT_print_all + | CT_print_classes + | CT_print_coercions + | CT_print_grammar of ct_GRAMMAR + | CT_print_graph + | CT_print_hint of ct_ID_OPT + | CT_print_hintdb of ct_ID + | CT_print_id of ct_ID + | CT_print_loadpath + | CT_print_modules + | CT_print_natural of ct_ID + | CT_print_natural_feature of ct_NATURAL_FEATURE + | CT_print_opaqueid of ct_ID + | CT_print_path of ct_ID * ct_ID + | CT_print_proof of ct_ID + | CT_print_section of ct_ID + | CT_print_states + | CT_proof of ct_FORMULA + | CT_proof_no_op + | CT_pwd + | CT_quit + | CT_read_module of ct_ID + | CT_rec_ml_add_path of ct_STRING + | CT_rec_tactic_definition of ct_REC_TACTIC_FUN_LIST + | CT_recaddpath of ct_STRING + | CT_record of ct_COERCION_OPT * ct_ID * ct_BINDER_LIST * ct_SORT_TYPE * ct_ID_OPT * ct_RECCONSTR_LIST + | CT_remove_natural_feature of ct_NATURAL_FEATURE * ct_ID + | CT_require of ct_IMPEXP * ct_SPEC_OPT * ct_ID * ct_STRING_OPT + | CT_reset of ct_ID + | CT_reset_section of ct_ID + | CT_restart + | CT_restore_state of ct_ID + | CT_resume of ct_ID_OPT + | CT_save of ct_THM_OPT * ct_ID_OPT + | CT_search of ct_ID * ct_IN_OR_OUT_MODULES + | CT_section_end of ct_ID + | CT_section_struct of ct_SECTION_BEGIN * ct_SECTION_BODY * ct_COMMAND + | CT_set_natural of ct_ID + | CT_set_natural_default + | CT_sethyp of ct_INT + | CT_setundo of ct_INT + | CT_show_goal of ct_INT_OPT + | CT_show_implicits + | CT_show_node + | CT_show_proof + | CT_show_proofs + | CT_show_script + | CT_show_tree + | CT_solve of ct_INT * ct_TACTIC_COM + | CT_suspend + | CT_syntax_macro of ct_ID * ct_FORMULA * ct_INT_OPT + | CT_tactic_definition of ct_ID * ct_ID_LIST * ct_TACTIC_COM + | CT_test_natural_feature of ct_NATURAL_FEATURE * ct_ID + | CT_theorem_struct of ct_THEOREM_GOAL * ct_PROOF_SCRIPT + | CT_token of ct_STRING + | CT_transparent of ct_ID_NE_LIST + | CT_undo of ct_INT_OPT + | CT_unfocus + | CT_unsethyp + | CT_unsetundo + | CT_user_vernac of ct_ID * ct_VARG_LIST + | CT_variable of ct_VAR * ct_BINDER_LIST + | CT_write_module of ct_ID * ct_STRING_OPT +and ct_COMMAND_LIST = + CT_command_list of ct_COMMAND * ct_COMMAND list +and ct_COMMENT = + CT_comment of string +and ct_COMMENT_S = + CT_comment_s of ct_COMMENT list +and ct_CONSTR = + CT_constr of ct_ID * ct_FORMULA +and ct_CONSTR_LIST = + CT_constr_list of ct_CONSTR list +and ct_CONTEXT_HYP_LIST = + CT_context_hyp_list of ct_PREMISE_PATTERN list +and ct_CONTEXT_PATTERN = + CT_coerce_FORMULA_to_CONTEXT_PATTERN of ct_FORMULA + | 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 +and ct_CONVERSION_FLAG = + CT_beta + | CT_delta + | CT_iota +and ct_CONVERSION_FLAG_LIST = + CT_conversion_flag_list of ct_CONVERSION_FLAG list +and ct_CONV_SET = + CT_unf of ct_ID list + | CT_unfbut of ct_ID list +and ct_CO_IND = + CT_co_ind of string +and ct_DEFN = + CT_defn of string +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 +and ct_DEP = + CT_dep of string +and ct_DESTRUCTING = + CT_coerce_NONE_to_DESTRUCTING of ct_NONE + | CT_destructing +and ct_EQN = + CT_eqn of ct_MATCH_PATTERN_NE_LIST * ct_FORMULA +and ct_EQN_LIST = + CT_eqn_list of ct_EQN list +and ct_EVAL_CMD = + CT_eval of ct_INT_OPT * ct_RED_COM * ct_FORMULA +and ct_FIXTAC = + CT_fixtac of ct_ID * ct_INT * ct_FORMULA +and ct_FIX_BINDER = + CT_coerce_FIX_REC_to_FIX_BINDER of ct_FIX_REC + | CT_fix_binder of ct_ID * ct_INT * ct_FORMULA * ct_FORMULA +and ct_FIX_BINDER_LIST = + CT_fix_binder_list of ct_FIX_BINDER * ct_FIX_BINDER list +and ct_FIX_REC = + CT_fix_rec of ct_ID * ct_BINDER_NE_LIST * ct_FORMULA * ct_FORMULA +and ct_FIX_REC_LIST = + CT_fix_rec_list of ct_FIX_REC * ct_FIX_REC list +and ct_FIX_TAC_LIST = + CT_fix_tac_list of ct_FIXTAC list +and ct_FORMULA = + CT_coerce_BINARY_to_FORMULA of ct_BINARY + | CT_coerce_ID_to_FORMULA of ct_ID + | CT_coerce_SORT_TYPE_to_FORMULA of ct_SORT_TYPE + | 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_cases of ct_FORMULA_OPT * ct_FORMULA_NE_LIST * ct_EQN_LIST + | CT_cofixc of ct_ID * ct_COFIX_REC_LIST + | CT_elimc of ct_CASE * ct_FORMULA * ct_FORMULA * ct_FORMULA_LIST + | CT_existvarc + | CT_fixc of ct_ID * ct_FIX_BINDER_LIST + | CT_incomplete_binary of ct_FORMULA * ct_BINARY + | 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 +and ct_FORMULA_NE_LIST = + CT_formula_ne_list of ct_FORMULA * ct_FORMULA list +and ct_FORMULA_OPT = + CT_coerce_FORMULA_to_FORMULA_OPT of ct_FORMULA + | CT_coerce_ID_OPT_to_FORMULA_OPT of ct_ID_OPT +and ct_GRAMMAR = + CT_grammar_none +and ct_HINT_EXPRESSION = + CT_constructors of ct_ID + | CT_extern of ct_INT * ct_FORMULA * ct_TACTIC_COM + | CT_immediate of ct_FORMULA + | CT_resolve of ct_FORMULA + | CT_unfold_hint of ct_ID +and ct_ID = + CT_ident of string +and ct_IDENTITY_OPT = + CT_coerce_NONE_to_IDENTITY_OPT of ct_NONE + | CT_identity +and ct_ID_LIST = + CT_id_list of ct_ID list +and ct_ID_NE_LIST = + CT_id_ne_list of ct_ID * ct_ID list +and ct_ID_NE_LIST_OR_STAR = + CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR of ct_ID_NE_LIST + | CT_star +and ct_ID_OPT = + CT_coerce_ID_to_ID_OPT of ct_ID + | CT_coerce_NONE_to_ID_OPT of ct_NONE +and ct_ID_OPT_NE_LIST = + CT_id_opt_ne_list of ct_ID_OPT * ct_ID_OPT list +and ct_ID_OPT_OR_ALL = + CT_coerce_ID_OPT_to_ID_OPT_OR_ALL of ct_ID_OPT + | CT_all +and ct_ID_OR_INT = + CT_coerce_ID_to_ID_OR_INT of ct_ID + | CT_coerce_INT_to_ID_OR_INT of ct_INT +and ct_ID_OR_STRING = + CT_coerce_ID_to_ID_OR_STRING of ct_ID + | CT_coerce_STRING_to_ID_OR_STRING of ct_STRING +and ct_ID_UNIT = + CT_coerce_ID_to_ID_UNIT of ct_ID + | CT_unit +and ct_ID_UNIT_LIST = + CT_id_unit_list of ct_ID_UNIT * ct_ID_UNIT list +and ct_IMPEXP = + CT_export + | CT_import +and ct_IND_SPEC = + CT_ind_spec of ct_ID * ct_BINDER_LIST * ct_FORMULA * ct_CONSTR_LIST +and ct_IND_SPEC_LIST = + CT_ind_spec_list of ct_IND_SPEC list +and ct_INT = + CT_int of int +and ct_INTRO_PATT = + CT_coerce_ID_to_INTRO_PATT of ct_ID + | CT_conj_pattern of ct_INTRO_PATT_LIST + | CT_disj_pattern of ct_INTRO_PATT_LIST +and ct_INTRO_PATT_LIST = + CT_intro_patt_list of ct_INTRO_PATT list +and ct_INT_LIST = + CT_int_list of ct_INT list +and ct_INT_NE_LIST = + CT_int_ne_list of ct_INT * ct_INT list +and ct_INT_OPT = + CT_coerce_INT_to_INT_OPT of ct_INT + | CT_coerce_NONE_to_INT_OPT of ct_NONE +and ct_INT_OR_LOCN = + CT_coerce_INT_to_INT_OR_LOCN of ct_INT + | CT_coerce_LOCN_to_INT_OR_LOCN of ct_LOCN +and ct_INV_TYPE = + CT_inv_clear + | CT_inv_regular + | CT_inv_simple +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_LOCAL_OPT = + CT_coerce_NONE_to_LOCAL_OPT of ct_NONE + | CT_local +and ct_LOCN = + CT_locn of string +and ct_MATCH_PATTERN = + CT_coerce_ID_OPT_to_MATCH_PATTERN of ct_ID_OPT + | CT_pattern_app of ct_MATCH_PATTERN * ct_MATCH_PATTERN_NE_LIST + | 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_NATURAL_FEATURE = + CT_contractible + | CT_implicit + | CT_nat_transparent +and ct_NONE = + CT_none +and ct_OMEGA_FEATURE = + CT_coerce_STRING_to_OMEGA_FEATURE of ct_STRING + | CT_flag_action + | CT_flag_system + | CT_flag_time +and ct_OMEGA_MODE = + CT_set + | CT_switch + | CT_unset +and ct_ORIENTATION = + CT_lr + | CT_rl +and ct_PATTERN = + CT_pattern_occ of ct_INT_LIST * ct_FORMULA +and ct_PATTERN_NE_LIST = + CT_pattern_ne_list of ct_PATTERN * ct_PATTERN list +and ct_PREMISE = + CT_coerce_TYPED_FORMULA_to_PREMISE of ct_TYPED_FORMULA + | CT_eval_result of ct_FORMULA * ct_FORMULA * ct_FORMULA + | CT_premise of ct_ID * ct_FORMULA +and ct_PREMISES_LIST = + CT_premises_list of ct_PREMISE list +and ct_PREMISE_PATTERN = + CT_premise_pattern of ct_ID_OPT * ct_CONTEXT_PATTERN +and ct_PROOF_SCRIPT = + CT_proof_script of ct_COMMAND list +and ct_RECCONSTR = + CT_coerce_CONSTR_to_RECCONSTR of ct_CONSTR + | CT_constr_coercion of ct_ID * ct_FORMULA +and ct_RECCONSTR_LIST = + CT_recconstr_list of ct_RECCONSTR list +and ct_REC_TACTIC_FUN = + CT_rec_tactic_fun of ct_ID * ct_ID_UNIT_LIST * ct_TACTIC_COM +and ct_REC_TACTIC_FUN_LIST = + CT_rec_tactic_fun_list of ct_REC_TACTIC_FUN * ct_REC_TACTIC_FUN list +and ct_RED_COM = + CT_cbv of ct_CONVERSION_FLAG_LIST * ct_CONV_SET + | CT_fold of ct_FORMULA_LIST + | CT_hnf + | CT_lazy of ct_CONVERSION_FLAG_LIST * ct_CONV_SET + | CT_pattern of ct_PATTERN_NE_LIST + | CT_red + | CT_simpl + | CT_unfold of ct_UNFOLD_NE_LIST +and ct_RULE = + CT_rule of ct_PREMISES_LIST * ct_FORMULA +and ct_RULE_LIST = + CT_rule_list of ct_RULE list +and ct_SCHEME_SPEC = + CT_scheme_spec of ct_ID * ct_DEP * ct_FORMULA * ct_SORT_TYPE +and ct_SCHEME_SPEC_LIST = + CT_scheme_spec_list of ct_SCHEME_SPEC * ct_SCHEME_SPEC list +and ct_SECTION_BEGIN = + CT_section of ct_ID +and ct_SECTION_BODY = + CT_section_body of ct_COMMAND list +and ct_SIGNED_INT = + CT_coerce_INT_to_SIGNED_INT of ct_INT + | CT_minus of ct_INT +and ct_SIGNED_INT_LIST = + CT_signed_int_list of ct_SIGNED_INT list +and ct_SORT_TYPE = + CT_sortc of string +and ct_SPEC_LIST = + CT_coerce_BINDING_LIST_to_SPEC_LIST of ct_BINDING_LIST + | CT_coerce_FORMULA_LIST_to_SPEC_LIST of ct_FORMULA_LIST +and ct_SPEC_OPT = + CT_coerce_NONE_to_SPEC_OPT of ct_NONE + | CT_spec +and ct_STRING = + CT_string of string +and ct_STRING_NE_LIST = + CT_string_ne_list of ct_STRING * ct_STRING list +and ct_STRING_OPT = + CT_coerce_NONE_to_STRING_OPT of ct_NONE + | CT_coerce_STRING_to_STRING_OPT of ct_STRING +and ct_TACTIC_ARG = + CT_coerce_FORMULA_to_TACTIC_ARG of ct_FORMULA + | CT_coerce_ID_OR_INT_to_TACTIC_ARG of ct_ID_OR_INT + | CT_coerce_TACTIC_COM_to_TACTIC_ARG of ct_TACTIC_COM + | CT_void +and ct_TACTIC_ARG_LIST = + CT_tactic_arg_list of ct_TACTIC_ARG * ct_TACTIC_ARG list +and ct_TACTIC_COM = + CT_abstract of ct_ID_OPT * ct_TACTIC_COM + | CT_absurd of ct_FORMULA + | CT_apply of ct_FORMULA * ct_SPEC_LIST + | CT_assumption + | CT_auto of ct_INT_OPT + | CT_auto_with of ct_INT_OPT * ct_ID_NE_LIST_OR_STAR + | CT_autorewrite of ct_ID_NE_LIST * ct_TACTIC_OPT + | CT_autotdb of ct_INT_OPT + | CT_case_type of ct_FORMULA + | CT_casetac of ct_FORMULA * ct_SPEC_LIST + | CT_cdhyp of ct_ID + | CT_change of ct_FORMULA * ct_ID_LIST + | CT_clear of ct_ID_NE_LIST + | CT_cofixtactic of ct_ID_OPT * ct_COFIX_TAC_LIST + | CT_condrewrite_lr of ct_TACTIC_COM * ct_FORMULA * ct_SPEC_LIST * ct_ID_OPT + | CT_condrewrite_rl of ct_TACTIC_COM * ct_FORMULA * ct_SPEC_LIST * ct_ID_OPT + | CT_constructor of ct_INT * ct_SPEC_LIST + | CT_contradiction + | CT_cut of ct_FORMULA + | CT_cutrewrite_lr of ct_FORMULA * ct_ID_OPT + | CT_cutrewrite_rl of ct_FORMULA * ct_ID_OPT + | CT_dconcl + | CT_decompose_list of ct_ID_NE_LIST * ct_FORMULA + | CT_depinversion of ct_INV_TYPE * ct_ID * ct_FORMULA_OPT + | CT_deprewrite_lr of ct_ID + | CT_deprewrite_rl of ct_ID + | CT_destruct of ct_ID_OR_INT + | CT_dhyp of ct_ID + | CT_discriminate_eq of ct_ID_OPT + | CT_do of ct_INT * ct_TACTIC_COM + | CT_eapply of ct_FORMULA * ct_SPEC_LIST + | CT_eauto of ct_INT_OPT + | CT_eauto_with of ct_INT_OPT * ct_ID_NE_LIST_OR_STAR + | CT_elim of ct_FORMULA * ct_SPEC_LIST * ct_USING + | CT_elim_type of ct_FORMULA + | CT_exact of ct_FORMULA + | CT_exists of ct_SPEC_LIST + | CT_fail + | CT_first of ct_TACTIC_COM * ct_TACTIC_COM list + | CT_fixtactic of ct_ID_OPT * ct_INT * ct_FIX_TAC_LIST + | CT_generalize of ct_FORMULA_NE_LIST + | CT_generalize_dependent of ct_FORMULA + | CT_idtac + | CT_induction of ct_ID_OR_INT + | CT_info of ct_TACTIC_COM + | CT_injection_eq of ct_ID_OPT + | CT_intro of ct_ID_OPT + | CT_intro_after of ct_ID_OPT * ct_ID + | CT_intros of ct_INTRO_PATT_LIST + | 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_match_context of ct_CONTEXT_RULE * ct_CONTEXT_RULE list + | CT_move_after of ct_ID * ct_ID + | CT_omega + | CT_orelse of ct_TACTIC_COM * ct_TACTIC_COM + | CT_parallel of ct_TACTIC_COM * ct_TACTIC_COM list + | 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_ID_LIST + | CT_reflexivity + | CT_repeat of ct_TACTIC_COM + | CT_replace_with of ct_FORMULA * ct_FORMULA + | CT_rewrite_lr of ct_FORMULA * ct_SPEC_LIST * ct_ID_OPT + | CT_rewrite_rl of ct_FORMULA * ct_SPEC_LIST * ct_ID_OPT + | CT_right of ct_SPEC_LIST + | CT_simple_user_tac of ct_ID * ct_TACTIC_ARG_LIST + | CT_simplify_eq of ct_ID_OPT + | CT_specialize of ct_INT_OPT * ct_FORMULA * ct_SPEC_LIST + | CT_split of ct_SPEC_LIST + | CT_superauto of ct_INT_OPT * ct_ID_LIST * ct_DESTRUCTING * ct_USINGTDB + | CT_symmetry + | CT_tac_double of ct_INT * ct_INT + | CT_tacsolve of ct_TACTIC_COM * ct_TACTIC_COM list + | CT_tactic_fun of ct_ID_UNIT_LIST * ct_TACTIC_COM + | CT_then of ct_TACTIC_COM * ct_TACTIC_COM list + | CT_transitivity of ct_FORMULA + | CT_trivial + | CT_trivial_with of ct_ID_NE_LIST_OR_STAR + | CT_try of ct_TACTIC_COM + | CT_use of ct_FORMULA + | CT_use_inversion of ct_ID * ct_FORMULA * ct_ID_LIST + | CT_user_tac of ct_ID * ct_TARG_LIST +and ct_TACTIC_OPT = + CT_coerce_NONE_to_TACTIC_OPT of ct_NONE + | CT_coerce_TACTIC_COM_to_TACTIC_OPT of ct_TACTIC_COM +and ct_TARG = + CT_coerce_BINDING_to_TARG of ct_BINDING + | CT_coerce_COFIXTAC_to_TARG of ct_COFIXTAC + | CT_coerce_FIXTAC_to_TARG of ct_FIXTAC + | CT_coerce_FORMULA_to_TARG of ct_FORMULA + | CT_coerce_ID_OR_INT_to_TARG of ct_ID_OR_INT + | CT_coerce_ID_OR_STRING_to_TARG of ct_ID_OR_STRING + | CT_coerce_PATTERN_to_TARG of ct_PATTERN + | CT_coerce_SIGNED_INT_LIST_to_TARG of ct_SIGNED_INT_LIST + | CT_coerce_SPEC_LIST_to_TARG of ct_SPEC_LIST + | CT_coerce_TACTIC_COM_to_TARG of ct_TACTIC_COM + | CT_coerce_UNFOLD_to_TARG of ct_UNFOLD + | CT_coerce_UNFOLD_NE_LIST_to_TARG of ct_UNFOLD_NE_LIST +and ct_TARG_LIST = + CT_targ_list of ct_TARG list +and ct_THEOREM_GOAL = + CT_goal of ct_FORMULA + | CT_theorem_goal of ct_DEFN_OR_THM * ct_ID * ct_FORMULA +and ct_THM = + CT_thm of string +and ct_THM_OPT = + CT_coerce_NONE_to_THM_OPT of ct_NONE + | CT_coerce_THM_to_THM_OPT of ct_THM +and ct_TYPED_FORMULA = + CT_typed_formula of ct_FORMULA * ct_FORMULA +and ct_UNFOLD = + CT_unfold_occ of ct_INT_LIST * ct_ID +and ct_UNFOLD_NE_LIST = + CT_unfold_ne_list of ct_UNFOLD * ct_UNFOLD list +and ct_USING = + CT_coerce_NONE_to_USING of ct_NONE + | CT_using of ct_FORMULA * ct_SPEC_LIST +and ct_USINGTDB = + CT_coerce_NONE_to_USINGTDB of ct_NONE + | CT_usingtdb +and ct_VAR = + CT_var of string +and ct_VARG = + CT_coerce_AST_to_VARG of ct_AST + | CT_coerce_AST_LIST_to_VARG of ct_AST_LIST + | CT_coerce_BINDER_to_VARG of ct_BINDER + | CT_coerce_BINDER_LIST_to_VARG of ct_BINDER_LIST + | CT_coerce_BINDER_NE_LIST_to_VARG of ct_BINDER_NE_LIST + | CT_coerce_FORMULA_LIST_to_VARG of ct_FORMULA_LIST + | CT_coerce_FORMULA_OPT_to_VARG of ct_FORMULA_OPT + | CT_coerce_ID_OPT_OR_ALL_to_VARG of ct_ID_OPT_OR_ALL + | CT_coerce_INT_LIST_to_VARG of ct_INT_LIST + | CT_coerce_INT_OPT_to_VARG of ct_INT_OPT + | CT_coerce_STRING_OPT_to_VARG of ct_STRING_OPT + | CT_coerce_TACTIC_OPT_to_VARG of ct_TACTIC_OPT + | CT_coerce_VARG_LIST_to_VARG of ct_VARG_LIST +and ct_VARG_LIST = + CT_varg_list of ct_VARG list +and ct_VERBOSE_OPT = + CT_coerce_NONE_to_VERBOSE_OPT of ct_NONE + | CT_verbose +;; diff --git a/contrib/interface/centaur.ml b/contrib/interface/centaur.ml new file mode 100644 index 000000000..24e3db2b0 --- /dev/null +++ b/contrib/interface/centaur.ml @@ -0,0 +1,810 @@ + +(*Toplevel loop for the communication between Coq and Centaur *) +open Names;; +open Util;; +open Ast;; +open Term;; +open Pp;; +open Libobject;; +open Library;; +open Vernacinterp;; +open Evd;; +open Proof_trees;; +open Termast;; +open Tacmach;; +open Pfedit;; +open Proof_type;; +open Parsing;; +open Environ;; +open Declare;; +open Declarations;; +open Rawterm;; +open Reduction;; +open Classops;; +open Vernacinterp;; +open Vernac;; +open Command;; +open Protectedtoplevel;; +open Coqast;; +open Line_oriented_parser;; +open Xlate;; +open Vtp;; +open Ascent;; +open Translate;; +open Name_to_ast;; +open Pbp;; +open Dad;; +open Debug_tac;; +open Search;; +open Astterm;; +open Nametab;; + + +let text_proof_flag = ref false;; + +let current_proof_name = ref "";; + +let current_goal_index = ref 0;; + +set_flags := (function () -> + if List.mem "G_natsyntax" (Mltop.get_loaded_modules()) then + (g_nat_syntax_flag := true; ()) + else ());; + +let guarded_force_eval_stream s = + let l = ref [] in + let f elt = l:= elt :: !l in + (try Stream.iter f s with + | _ -> f (sTR "error guarded_force_eval_stream")); + Stream.of_list (List.rev !l);; + + +let rec string_of_path p = + match p with [] -> "\n" + | i::p -> (string_of_int i)^" "^ (string_of_path p) +;; +let print_path p = + output_results_nl [< 'sTR "Path:"; 'sTR (string_of_path p)>] +;; + +let kill_proof_node index = + let paths = History.historical_undo !current_proof_name index in + let _ = List.iter + (fun path -> (traverse_to path; + Pfedit.mutate weak_undo_pftreestate; + traverse_to [])) + paths in + History.border_length !current_proof_name;; + + +(*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 >];; + +let ctf_acknowledge_command request_id command_count opt_exn = + let goal_count, goal_index = + if refining() then + let g_count = + List.length + (fst (frontier (proof_of_pftreestate (get_pftreestate ())))) in + 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 -> [< >]); 'fNL; 'sTR "E-n-d---M-e-s-s-a-g-e"; 'fNL >];; + +let ctf_undoResults = ctf_header "undo_results";; + +let ctf_TextMessage = ctf_header "text_proof";; + +let ctf_SearchResults = ctf_header "search_results";; + +let ctf_OtherGoal = ctf_header "other_goal";; + +let ctf_Location = ctf_header "location";; + +let ctf_StateMessage = ctf_header "state";; + +let ctf_PathGoalMessage () = + [< '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_KilledMessage req_id ngoals = + [< ctf_header "killed" req_id; 'iNT ngoals; 'fNL >];; + +let ctf_AbortedAllMessage () = + [< '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 >];; + +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 ctf_ResetInitialMessage () = + [< 'fNL; 'sTR "message"; 'fNL; 'sTR "reset_initial"; 'fNL >];; + +let ctf_ResetIdentMessage request_id str = + [< 'fNL; 'sTR "message"; 'fNL; 'sTR "reset_ident"; 'fNL; 'iNT request_id; 'fNL; + 'sTR str; 'fNL; 'sTR "E-n-d---M-e-s-s-a-g-e"; 'fNL >];; + +type vtp_tree = + | P_rl of ct_RULE_LIST + | P_r of ct_RULE + | P_s_int of ct_SIGNED_INT_LIST + | P_pl of ct_PREMISES_LIST + | P_cl of ct_COMMAND_LIST + | P_t of ct_TACTIC_COM + | P_ids of ct_ID_LIST;; + +let print_tree t = + (match t with + | P_rl x -> fRULE_LIST x + | P_r x -> fRULE x + | P_s_int x -> fSIGNED_INT_LIST x + | P_pl x -> fPREMISES_LIST x + | P_cl x -> fCOMMAND_LIST x + | P_t x -> fTACTIC_COM x + | P_ids x -> fID_LIST x); + print_string "e\nblabla\n";; + + + +let break_happened = ref false;; + +let output_results stream vtp_tree = + let _ = Sys.signal Sys.sigint + (Sys.Signal_handle(fun i -> (break_happened := true;()))) in + mSG stream; + match vtp_tree with + Some t -> print_tree t + | None -> ();; + +let output_results_nl stream = + let _ = Sys.signal Sys.sigint + (Sys.Signal_handle(fun i -> break_happened := true;())) + in + mSGNL stream;; + + +let rearm_break () = + let _ = Sys.signal Sys.sigint (Sys.Signal_handle(fun i -> raise Sys.Break)) + in ();; + +let check_break () = + if (!break_happened) then + begin + break_happened := false; + raise Sys.Break + end + else ();; + +let print_past_goal index = + let path = History.get_path_for_rank !current_proof_name index in + try traverse_to path; + let pf = proof_of_pftreestate (get_pftreestate ()) in + output_results (ctf_PathGoalMessage ()) + (Some (P_r (translate_goal pf.goal))) + with + | Invalid_argument s -> error "No focused proof (No proof-editing in progress)" +;; + +let show_nth n = + try + let pf = proof_of_pftreestate (get_pftreestate()) in + if (!text_proof_flag) then + errorlabstrm "debug" [< 'sTR "text printing unplugged" >] +(* + (if n=0 + then output_results (ctf_TextMessage !global_request_id) + (Some (P_t (show_proof []))) + else + let path = History.get_nth_open_path !current_proof_name n in + output_results (ctf_TextMessage !global_request_id) + (Some (P_t (show_proof path)))) +*) + else + output_results (ctf_GoalReqIdMessage !global_request_id) + (let goal = List.nth (fst (frontier pf)) + (n - 1) in + (Some (P_r (translate_goal goal)))) + with + | Invalid_argument s -> + error "No focused proof (No proof-editing in progress)";; + +(* The rest of the file contains commands that are changed from the plain + Coq distribution *) + +let ctv_SEARCH_LIST = ref ([] : ct_PREMISE list);; + +let filter_by_module_from_varg_list (l:vernac_arg list) = + let dir_list, b = Vernacentries.inside_outside l in + Search.filter_by_module_from_list (dir_list, b);; + +let add_search (global_reference:global_reference) assumptions cstr = + mSGNL [< 'sTR "DEBUG: entering add_search" >]; + try + let id_string = string_of_qualid (Global.qualid_of_global global_reference) in + let _ = mSGNL [< 'sTR "DEBUG: " ; 'sTR id_string >] in + let ast = + try + CT_premise (CT_ident id_string, translate_constr assumptions cstr) + with Not_found -> + CT_premise (CT_ident id_string, + CT_coerce_ID_to_FORMULA( + CT_ident ("Error printing" ^ id_string))) in + ctv_SEARCH_LIST:= ast::!ctv_SEARCH_LIST + with e -> mSGNL [< 'sTR "add_search raised an exception" >]; raise e;; + +let make_error_stream node_string = + [< 'sTR "The syntax of "; 'sTR node_string; + 'sTR " is inconsistent with the vernac interpreter entry" >];; + +let ctf_EmptyGoalMessage id = + [< 'fNL; 'sTR "Empty Goal is a no-op. Fun oh fun."; 'fNL >];; + + +let print_check (ast, judg) = + let {uj_val=value; uj_type=typ} = judg in + let value_ct_ast = + (try translate_constr (Global.env()) value + with UserError(f,str) -> + raise(UserError(f, + [< Ast.print_ast + (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 + ((ctf_SearchResults !global_request_id), + (Some (P_pl + (CT_premises_list + [CT_coerce_TYPED_FORMULA_to_PREMISE + (CT_typed_formula(value_ct_ast,type_ct_ast) + )]))));; + +let ct_print_eval ast red_fun env evd judg = +((if refining() then traverse_to []); +let {uj_val=value; uj_type=typ} = judg in +let nvalue = red_fun value +(* // Attention , ici il faut peut être utiliser des environnemenst locaux *) +and ntyp = nf_betaiota env evd typ in +(ctf_SearchResults !global_request_id, + Some (P_pl + (CT_premises_list + [CT_eval_result + (xlate_formula ast, + translate_constr env nvalue, + translate_constr env ntyp)]))));; + + + +(* The following function is copied from globpr in env/printer.ml *) +let globcv = function + | Node(_,"MUTIND", (Path(_,sl,s))::(Num(_,tyi))::_) -> + convert_qualid + (Global.qualid_of_global (IndRef(section_path sl s,tyi))) + | Node(_,"MUTCONSTRUCT",(Path(_,sl,s))::(Num(_,tyi))::(Num(_,i))::_) -> + convert_qualid + (Global.qualid_of_global (ConstructRef ((section_path sl s, tyi), i))) + | _ -> failwith "globcv : unexpected value";; + +let pbp_tac_pcoq = + pbp_tac (function x -> + output_results + [< 'fNL; 'sTR "message"; 'fNL; 'sTR "pbp_results"; 'fNL; + 'iNT !global_request_id; 'fNL>] + (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 >] + (Some (P_t(xlate_tactic x))));; + +let search_output_results () = + output_results + (ctf_SearchResults !global_request_id) + (Some (P_pl (CT_premises_list + (List.rev !ctv_SEARCH_LIST))));; + + +let debug_tac2_pcoq = function + [Tacexp ast] -> + (fun g -> + let the_goal = ref (None : goal sigma option) in + let the_ast = ref ast in + let the_path = ref ([] : int list) in + 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 >]; + result) + with + e -> + match !the_goal with + None -> raise e + | Some g -> + (output_results + (ctf_Location !global_request_id) + (Some (P_s_int + (CT_signed_int_list + (List.map + (fun n -> CT_coerce_INT_to_SIGNED_INT + (CT_int n)) + (clean_path 0 ast + (List.rev !the_path))))))); + (output_results + (ctf_OtherGoal !global_request_id) + (Some (P_r (translate_goal (sig_it g))))); + raise e) + | _ -> error "wrong arguments for debug_tac2_pcoq";; + +let rec selectinspect n env = + match env with + [] -> [] + | a::tl -> + if n = 0 then + [] + else + match a with + (sp, Lib.Leaf lobj) -> a::(selectinspect (n -1 ) tl) + | _ -> (selectinspect n tl);; + +open Term;; + +let inspect n = + let env = Global.env() in + let add_search2 x y = add_search x env y in + let l = selectinspect n (Lib.contents_after None) in + ctv_SEARCH_LIST := []; + List.iter + (fun a -> + try + (match a with + sp, Lib.Leaf lobj -> + (match sp, object_tag lobj with + _, "VARIABLE" -> + let ((_, _, v), _, _) = get_variable sp in + add_search2 (Nametab.locate (qualid_of_sp sp)) v + | sp, ("CONSTANT"|"PARAMETER") -> + let {const_type=typ} = Global.lookup_constant sp in + add_search2 (Nametab.locate (qualid_of_sp sp)) typ + | sp, "MUTUALINDUCTIVE" -> + add_search2 (Nametab.locate (qualid_of_sp sp)) + (Pretyping.understand Evd.empty (Global.env()) + (RRef(dummy_loc, IndRef(sp,0)))) + | _ -> failwith ("unexpected value 1 for "^ + (string_of_id (basename sp)))) + | _ -> failwith "unexpected value") + with e -> ()) + l; + output_results + (ctf_SearchResults !global_request_id) + (Some + (P_pl (CT_premises_list (List.rev !ctv_SEARCH_LIST))));; + +let ct_int_to_TARG n = + CT_coerce_ID_OR_INT_to_TARG + (CT_coerce_INT_to_ID_OR_INT (CT_int n));; + +let pair_list_to_ct l = + CT_user_tac(CT_ident "pair_int_list", + CT_targ_list + (List.map (fun (a,b) -> + CT_coerce_TACTIC_COM_to_TARG + (CT_user_tac + (CT_ident "pair_int", + CT_targ_list + [ct_int_to_TARG a; ct_int_to_TARG b]))) + l));; + +let logical_kill n = + let path = History.get_path_for_rank !current_proof_name n in + begin + traverse_to path; + Pfedit.mutate weak_undo_pftreestate; + (let kept_cmds, undone_cmds, remaining_goals, current_goal = + History.logical_undo !current_proof_name n in + output_results (ctf_undoResults !global_request_id) + (Some + (P_t + (CT_user_tac + (CT_ident "log_undo_result", + CT_targ_list + [CT_coerce_TACTIC_COM_to_TARG (pair_list_to_ct kept_cmds); + CT_coerce_TACTIC_COM_to_TARG(pair_list_to_ct undone_cmds); + ct_int_to_TARG remaining_goals; + ct_int_to_TARG current_goal]))))); + traverse_to [] + end;; + +let command_changes = [ + ("TEXT_MODE", + (function + | [VARG_AST (Id(_,x))] -> + (match x with + "on" -> (function () -> text_proof_flag := true) + | "off" -> (function () -> text_proof_flag := false) + | s -> errorlabstrm "TEXT_MODE" (make_error_stream + ("Unexpected flag " ^ s))) + | _ -> errorlabstrm "TEXT_MODE" + (make_error_stream "Unexpected argument"))); + + ("StartProof", + (function + | (VARG_STRING kind) :: + ((VARG_IDENTIFIER s) :: + ((VARG_CONSTR c) :: [])) -> + let stre = + match kind with + | "THEOREM" -> NeverDischarge + | "LEMMA" -> NeverDischarge + | "FACT" -> make_strength_1 () + | "REMARK" -> make_strength_0 () + | "DEFINITION" -> NeverDischarge + | "LET" -> make_strength_2 () + | "LETTOP" -> NotDeclare + | "LOCAL" -> make_strength_0 () + | _ -> errorlabstrm "StartProof" (make_error_stream "StartProof") in + fun () -> + begin + if kind = "LETTOP" && not(refining ()) then + errorlabstrm "StartProof" + [< 'sTR + "Let declarations can only be used in proof editing mode" + >]; + let str = (string_of_id s) in + start_proof_com (Some s) stre c; + History.start_proof str; + current_proof_name := str; + current_goal_index := 1 + end + | _ -> errorlabstrm "StartProof" (make_error_stream "StartProof"))); + + ("GOAL", + (function + | (VARG_CONSTR c) :: [] -> + (fun () -> + if not (refining ()) then + begin + start_proof_com None NeverDischarge c; + History.start_proof "Unnamed_thm"; + current_proof_name := "Unnamed_thm"; + current_goal_index := 1 + end) + | [] -> + (function () -> output_results_nl(ctf_EmptyGoalMessage "")) + | _ -> errorlabstrm "Goal" (make_error_stream "Goal"))); + + ("SOLVE", + (function + | [VARG_NUMBER n; VARG_TACTIC tcom] -> + (fun () -> + if not (refining ()) then + error "Unknown command of the non proof-editing mode"; + solve_nth n (Tacinterp.hide_interp tcom); + let old_n_count = History.border_length !current_proof_name in + let pf = proof_of_pftreestate (get_pftreestate ()) in + let n_goals = (List.length (fst (frontier pf))) + 1 - old_n_count in + begin + current_goal_index := n; + History.push_command !current_proof_name n n_goals + end) + | _ -> errorlabstrm "SOLVE" (make_error_stream "SOLVE"))); + + ("GOAL_CMD", + (function + | (VARG_NUMBER n) :: + ((VARG_TACTIC tac) :: []) -> + (function () -> + let path = History.get_nth_open_path !current_proof_name n in + solve_nth n (Tacinterp.hide_interp tac); + traverse_to path; + Pfedit.mutate weak_undo_pftreestate; + traverse_to []) + | _ -> errorlabstrm "GOAL_CMD" (make_error_stream "GOAL_CMD"))); + + ("KILL_NODE", + (function + | (VARG_NUMBER n) :: [] -> + (function () -> + let ngoals = kill_proof_node n in + output_results_nl + (ctf_KilledMessage !global_request_id ngoals)) + | _ -> errorlabstrm "KILL_NODE" (make_error_stream "KILL_NODE"))); + ("KILL_SUB_PROOF", + (function + | [VARG_NUMBER n] -> + (function () -> logical_kill n) + | _ -> errorlabstrm "KILL_SUB_PROOF" (make_error_stream "KILL_SUB_PROOF"))); + + ("RESUME", + (function [VARG_IDENTIFIER id] -> + (fun () -> + let str = (string_of_id id) in + resume_proof id; + current_proof_name := str) + | _ -> errorlabstrm "RESUME" (make_error_stream "RESUME"))); + + ("BeginSilent", + (function + | [] -> + (function + () -> + errorlabstrm "Begin Silent" + [< 'sTR "not available in Centaur mode" >]) + | _ -> errorlabstrm "BeginSilent" (make_error_stream "BeginSilent"))); + + ("EndSilent", + (function + | [] -> + (function + () -> + errorlabstrm "End Silent" + [< 'sTR "not available in Centaur mode" >]) + | _ -> errorlabstrm "EndSilent" (make_error_stream "EndSilent"))); + + ("SaveNamed", + (function + | [] -> + (function () -> traverse_to []; save_named false) + | _ -> errorlabstrm "SaveNamed" (make_error_stream "SaveNamed"))); + + ("DefinedNamed", + (function + | [] -> + (function () -> traverse_to []; save_named false) + | _ -> errorlabstrm "DefinedNamed" (make_error_stream "DefinedNamed"))); + + ("DefinedAnonymous", + (function + | (VARG_IDENTIFIER id) :: [] -> + (function () -> + traverse_to []; + save_anonymous_thm true (string_of_id id)) + | _ -> + errorlabstrm "DefinedAnonymous" + (make_error_stream "DefinedAnonymous"))); + + ("SaveAnonymous", + (function + | (VARG_IDENTIFIER id) :: [] -> + (function () -> + traverse_to []; + save_anonymous_thm true (string_of_id id)) + | _ -> + errorlabstrm "SaveAnonymous" + (make_error_stream "SaveAnonymous"))); + + ("SaveAnonymousThm", + (function + | (VARG_IDENTIFIER id) :: [] -> + (function () -> + traverse_to []; + save_anonymous_thm true (string_of_id id)) + | _ -> + errorlabstrm "SaveAnonymousThm" + (make_error_stream "SaveAnonymousThm"))); + + ("SaveAnonymousRmk", + (function + | (VARG_IDENTIFIER id) :: [] -> + (function + () -> traverse_to []; + save_anonymous_remark true (string_of_id id)) + | _ -> + errorlabstrm "SaveAnonymousRmk" + (make_error_stream "SaveAnonymousRmk"))); + + ("ABORT", + (function + | (VARG_IDENTIFIER id) :: [] -> + (function + () -> + delete_proof id; + current_proof_name := ""; + output_results_nl + (ctf_AbortedMessage !global_request_id (string_of_id id))) + | [] -> + (function + () -> delete_current_proof (); + current_proof_name := ""; + output_results_nl + (ctf_AbortedMessage !global_request_id "")) + | _ -> errorlabstrm "ABORT" (make_error_stream "ABORT"))); + ("SEARCH", + function + (VARG_QUALID qid)::l -> + (fun () -> + ctv_SEARCH_LIST:=[]; + let global_ref = Vernacentries.global dummy_loc qid in + filtered_search + (filter_by_module_from_varg_list l) + add_search (Nametab.locate qid); + search_output_results()) + | _ -> failwith "bad form of arguments"); + + ("SearchRewrite", + function + (VARG_CONSTR c)::l -> + (fun () -> + ctv_SEARCH_LIST:=[]; + let _,pat = interp_constrpattern Evd.empty (Global.env()) c in + raw_search_rewrite + (filter_by_module_from_varg_list l) + add_search pat; + search_output_results()) + | _ -> failwith "bad form of arguments"); + + ("SearchPattern", + function + (VARG_CONSTR c)::l -> + (fun () -> + ctv_SEARCH_LIST := []; + let _,pat = interp_constrpattern Evd.empty (Global.env()) c in + raw_pattern_search + (filter_by_module_from_varg_list l) + add_search pat; + search_output_results()) + | _ -> failwith "bad form of arguments"); + + ("PrintId", + (function + | [VARG_QUALID qid] -> + (function () -> + let results = xlate_vernac_list (name_to_ast qid) in + output_results + [<'fNL; 'sTR "message"; 'fNL; 'sTR "PRINT_VALUE"; 'fNL >] + (Some (P_cl results))) + | _ -> errorlabstrm "PrintId" (make_error_stream "PrintId"))); + + ("Check", + (function + | (VARG_STRING kind) :: ((VARG_CONSTR c) :: g) -> + let evmap, env = + Vernacentries.get_current_context_of_args g in + let f = + match kind with + | "CHECK" -> print_check + | "PRINTTYPE" -> + errorlabstrm "PrintType" [< 'sTR "Not yet supported in CtCoq" >] + | _ -> errorlabstrm "CHECK" (make_error_stream "CHECK") in + (function () -> + let a,b = f (c, judgment_of_rawconstr evmap env c) in + output_results a b) + | _ -> errorlabstrm "CHECK" (make_error_stream "CHECK"))); + + ("Eval", + (function + | VARG_TACTIC_ARG(Redexp redexp):: VARG_CONSTR c :: g -> + let evmap, env = Vernacentries.get_current_context_of_args g in + let redfun = + ct_print_eval c (Tacred.reduction_of_redexp redexp env evmap) env in + fun () -> + let strm, vtp = redfun evmap (judgment_of_rawconstr evmap env c) in + output_results strm vtp + | _ -> errorlabstrm "Eval" (make_error_stream "Eval"))); + + ("Centaur_Reset", + (function + | (VARG_IDENTIFIER c) :: [] -> + if refining () then + output_results (ctf_AbortedAllMessage ()) None; + current_proof_name := ""; + (match string_of_id c with + | "CtCoqInitialState" -> + (function + () -> + current_proof_name := ""; + Vernacentries.abort_refine Lib.reset_initial (); + output_results (ctf_ResetInitialMessage ()) None) + | _ -> + (function + () -> + current_proof_name := ""; + Vernacentries.abort_refine Lib.reset_name c; + output_results + (ctf_ResetIdentMessage + !global_request_id (string_of_id c)) None)) + | _ -> errorlabstrm "Centaur_Reset" (make_error_stream "Centaur_Reset"))); + ("Show_dad_rules", + (function + | [] -> + (fun () -> + let results = dad_rule_names() in + output_results + [< 'fNL; 'sTR "message"; 'fNL; 'sTR "dad_rule_names"; 'fNL; + 'iNT !global_request_id; 'fNL >] + (Some (P_ids + (CT_id_list + (List.map (fun s -> CT_ident s) results))))) + | _ -> + errorlabstrm + "Show_dad_rules" (make_error_stream "Show_dad_rules"))); + ("INSPECT", + (function + | [VARG_NUMBER n] -> + (function () -> inspect n) + | _ -> errorlabstrm "INSPECT" (make_error_stream "INSPECT"))) + +];; + +let non_debug_changes = [ + ("SHOW", + (function + | [VARG_NUMBER n] -> (function () -> show_nth n) + | _ -> errorlabstrm "SHOW" (make_error_stream "SHOW")))];; + +let command_creations = [ + ("Comments", + function l -> (fun () -> message ("Comments ok\n"))); + ("CommentsBold", + function l -> (fun () -> message ("CommentsBold ok\n"))); + ("Title", + function l -> (fun () -> message ("Title ok\n"))); + ("Author", + function l -> (fun () -> message ("Author ok\n"))); + ("Note", + function l -> (fun () -> message ("Note ok\n"))); + ("NL", + function l -> (fun () -> message ("Newline ok\n")))];; + + + +let start_pcoq_mode debug = + begin + start_dad(); + set_xlate_mut_stuff globcv; + declare_in_coq(); + add_tactic "PcoqPbp" pbp_tac_pcoq; + add_tactic "Dad" dad_tac_pcoq; + add_tactic "CtDebugTac" debug_tac2_pcoq; + add_tactic "CtDebugTac2" debug_tac2_pcoq; +(* The following ones are added to enable rich comments in pcoq *) + add_tactic "Image" (fun _ -> tclIDTAC); + List.iter (fun (a,b) -> vinterp_add a b) command_creations; + List.iter (fun (a,b) -> overwriting_vinterp_add a b) command_changes; + if not debug then + List.iter (fun (a,b) -> overwriting_vinterp_add a b) non_debug_changes; + end;; + +vinterp_add "START_PCOQ" + (function _ -> + (function () -> + start_pcoq_mode false; + set_acknowledge_command ctf_acknowledge_command; + set_start_marker "CENTAUR_RESERVED_TOKEN_start_command"; + set_end_marker "CENTAUR_RESERVED_TOKEN_end_command"; + raise Vernacinterp.ProtectedLoop));; + +vinterp_add "START_PCOQ_DEBUG" + (function _ -> + (function () -> + start_pcoq_mode true; + set_acknowledge_command ctf_acknowledge_command; + set_start_marker "--->"; + set_end_marker "<---"; + raise Vernacinterp.ProtectedLoop));; + diff --git a/contrib/interface/dad.ml b/contrib/interface/dad.ml new file mode 100644 index 000000000..1fefb6c44 --- /dev/null +++ b/contrib/interface/dad.ml @@ -0,0 +1,357 @@ +(* This file contains an ml version of drag-and-drop. *) + +(* #use "/net/home/bertot/experiments/pcoq/src/dad/dad.ml" *) + +open Names;; +open Term;; +open Rawterm;; +open Util;; +open Environ;; +open Tactics;; +open Tacticals;; +open Pattern;; +open Reduction;; +open Coqast;; +open Termast;; +open Astterm;; +open Vernacinterp;; + +open Proof_type;; +open Proof_trees;; +open Tacmach;; +open Typing;; +open Pp;; + +open Paths;; + +(* In a first approximation, drag-and-drop rules are like in CtCoq + 1/ a pattern, + 2,3/ Two paths: start and end positions, + 4/ the degree: the number of steps the algorithm should go up from the + longest common prefix, + 5/ the tail path: the suffix of the longest common prefix of length the + degree, + 6/ the command pattern, where meta variables are represented by objects + of the form Node(_,"META"; [Num(_,i)]) +*) + + +type dad_rule = Coqast.t * int list * int list * int * int list * Coqast.t;; + +(* This value will be used systematically when constructing objects of + type Coqast.t, the value is stupid and meaningless, but it is needed + to construct well-typed terms. *) + +let zz = (0,0);; + +(* This function receives a length n, a path p, and a term and returns a + couple whose first component is the subterm designated by the prefix + of p of length n, and the second component is the rest of the path *) + +let rec get_subterm (depth:int) (path: int list) (constr:constr) = + match depth, path, kind_of_term constr with + 0, l, c -> (constr,l) + | n, 2::a::tl, IsApp(func,arr) -> + get_subterm (n - 2) tl arr.(a-1) + | _,l,_ -> failwith (int_list_to_string + "wrong path or wrong form of term" + l);; + +(* This function maps a substitution on an abstract syntax tree. The + first argument, an object of type env, is necessary to + transform constr terms into abstract syntax trees. The second argument is + the substitution, a list of pairs linking an integer and a constr term. *) +let map_subst (env :env) + (subst:(int * Term.constr) list) = + let rec map_subst_aux = function + Node(_, "META", [Num(_, i)]) -> + let constr = List.assoc i subst in + ast_of_constr false env constr + | Node(loc, s, l) -> Node(loc, s, List.map map_subst_aux l) + | ast -> ast in + map_subst_aux;; + + +(* This function is really the one that is important. *) +let rec find_cmd (l:(string * dad_rule) list) env constr p p1 p2 = + match l with + [] -> failwith "nothing happens" + | (name, (pat, p_f, p_l, deg, p_r, cmd))::tl -> + let length = List.length p in + try + if deg > length then + failwith "internal" + else + let term_to_match, p_r = + try + get_subterm (length - deg) p constr + with + Failure s -> failwith "internal" in + let _, constr_pat = + interp_constrpattern Evd.empty (Global.env()) + 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 + map_subst env subst cmd + else + failwith "internal" + with + Failure "internal" -> find_cmd tl env constr p p1 p2 + | PatternMatchingFailure -> find_cmd tl env constr p p1 p2;; + + +let dad_rule_list = ref ([]: (string * dad_rule) list);; + + +(* \\ This function is also used in pbp. *) +let rec tactic_args_to_ints = function + [] -> [] + | (Integer n)::l -> n::(tactic_args_to_ints l) + | _ -> failwith "expecting only numbers";; + +(* We assume that the two lists of integers for the tactic are simply + given in one list, separated by a dummy tactic. *) +let rec part_tac_args l = function + [] -> l,[] + | (Tacexp a)::tl -> l, (tactic_args_to_ints tl) + | (Integer n)::tl -> part_tac_args (n::l) tl + | _ -> failwith "expecting only numbers and the word \"to\"";; + + +(* The dad_tac tactic takes a display_function as argument. This makes + it possible to use it in pcoq, but also in other contexts, just by + changing the output routine. *) +let dad_tac display_function = function + l -> let p1, p2 = part_tac_args [] l in + (function g -> + let (p_a, p1prime, p2prime) = decompose_path (List.rev p1,p2) in + (display_function + (find_cmd (!dad_rule_list) (pf_env g) + (pf_concl g) p_a p1prime p2prime)); + tclIDTAC g);; + +(* Now we enter dad rule list management. *) + +let add_dad_rule name patt p1 p2 depth pr command = + dad_rule_list := (name, + (patt, p1, p2, depth, pr, command))::!dad_rule_list;; + +let rec remove_if_exists name = function + [] -> false, [] + | ((a,b) as rule1)::tl -> if a = name then + let result1, l = (remove_if_exists name tl) in + true, l + else + let result1, l = remove_if_exists name tl in + result1, (rule1::l);; + +let remove_dad_rule name = + let result1, result2 = remove_if_exists name !dad_rule_list in + if result1 then + failwith("No such name among the drag and drop rules " ^ name) + else + dad_rule_list := result2;; + +let dad_rule_names () = + List.map (function (s,_) -> s) !dad_rule_list;; + +(* this function is inspired from matches_core in pattern.ml *) +let constrain ((n : int),(pat : constr_pattern)) sigma = + if List.mem_assoc n sigma then + if pat = (List.assoc n sigma) then sigma + else failwith "internal" + else + (n,pat)::sigma + +(* This function is inspired from matches_core in pattern.ml *) +let more_general_pat pat1 pat2 = + let rec match_rec sigma p1 p2 = + match p1, p2 with + | PMeta (Some n), m -> constrain (n,m) sigma + + | PMeta None, m -> sigma + + | PRef (VarRef sp1), PRef(VarRef sp2) when sp1 = sp2 -> sigma + + | PVar v1, PVar v2 when v1 = v2 -> sigma + + | PRef ref1, PRef ref2 when ref1 = ref2 -> sigma + + | PRel n1, PRel n2 when n1 = n2 -> sigma + + | PSort (RProp c1), PSort (RProp c2) when c1 = c2 -> sigma + + | PSort RType, PSort RType -> sigma + + | PApp (c1,arg1), PApp (c2,arg2) -> + (try array_fold_left2 match_rec (match_rec sigma c1 c2) arg1 arg2 + with Invalid_argument _ -> failwith "internal") + | _ -> failwith "unexpected case in more_general_pat" in + try let _ = match_rec [] pat1 pat2 in true + with Failure "internal" -> false;; + +let more_general r1 r2 = + match r1,r2 with + (_,(patt1,p11,p12,_,_,_)), + (_,(patt2,p21,p22,_,_,_)) -> + (more_general_pat patt1 patt2) & + (is_prefix p11 p21) & (is_prefix p12 p22);; + +let not_less_general r1 r2 = + not (match r1,r2 with + (_,(patt1,p11,p12,_,_,_)), + (_,(patt2,p21,p22,_,_,_)) -> + (more_general_pat patt1 patt2) & + (is_prefix p21 p11) & (is_prefix p22 p12));; + +let rec add_in_list_sorting rule1 = function + [] -> [rule1] + | (b::tl) as this_list -> + if more_general rule1 b then + b::(add_in_list_sorting rule1 tl) + else if not_less_general rule1 b then + let tl2 = add_in_list_sorting_aux rule1 tl in + (match tl2 with + [] -> rule1::this_list + | _ -> b::tl2) + else + rule1::this_list +and add_in_list_sorting_aux rule1 = function + [] -> [] + | b::tl -> + if more_general rule1 b then + b::(add_in_list_sorting rule1 tl) + else + let tl2 = add_in_list_sorting_aux rule1 tl in + (match tl2 with + [] -> [] + | _ -> rule1::tl2);; + +let rec sort_list = function + [] -> [] + | a::l -> add_in_list_sorting a (sort_list l);; + +let mk_dad_meta n = Node(zz,"META",[Num(zz, n)]);; +let mk_rewrite1 ast = + Node(zz,"TACTICLIST", + [Node(zz,"RewriteLR", + [Node(zz, "COMMAND", ast);Node(zz,"BINDINGS",[])])]);; + +let mk_rewrite2 ast = + Node(zz,"TACTICLIST", + [Node(zz,"RewriteRL", + [Node(zz, "COMMAND", ast);Node(zz,"BINDINGS",[])])]);; + + + +let start_dad () = +vinterp_add "AddDadRule" + (function + | [VARG_STRING name; VARG_CONSTR pat; VARG_NUMBERLIST p1; + VARG_NUMBERLIST p2; VARG_TACTIC com] -> + (function () -> + let pr = match decompose_path (p1, p2) with pr, _, _ -> pr in + (add_dad_rule name pat p1 p2 (List.length pr) pr com)) + | _ -> errorlabstrm "AddDadRule1" + [< 'sTR "AddDadRule2">]); +add_dad_rule "distributivity-inv" +(Node(zz,"APPLIST",[Nvar(zz,"mult");Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,4)]);Node(zz,"META",[Num(zz,3)])]);Node(zz,"META",[Num(zz,2)])])) +[2; 2] +[2; 1] +1 +[2] +(mk_rewrite1 ([Node(zz, "APPLIST", [Nvar(zz, "mult_plus_distr");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])])); + +add_dad_rule "distributivity1-r" +(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"APPLIST",[Nvar(zz,"mult");Node(zz,"META",[Num(zz,4)]);Node(zz,"META",[Num(zz,2)])]);Node(zz,"APPLIST",[Nvar(zz,"mult");Node(zz,"META",[Num(zz,3)]);Node(zz,"META",[Num(zz,2)])])])) +[2; 2; 2; 2] +[] +0 +[] +(mk_rewrite2 ([Node(zz, "APPLIST", [Nvar(zz, "mult_plus_distr");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])])); + +add_dad_rule "distributivity1-l" +(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"APPLIST",[Nvar(zz,"mult");Node(zz,"META",[Num(zz,4)]);Node(zz,"META",[Num(zz,2)])]);Node(zz,"APPLIST",[Nvar(zz,"mult");Node(zz,"META",[Num(zz,3)]);Node(zz,"META",[Num(zz,2)])])])) +[2; 1; 2; 2] +[] +0 +[] +(mk_rewrite2 ([Node(zz, "APPLIST", [Nvar(zz, "mult_plus_distr");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])])); + +add_dad_rule "associativity" +(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,4)]);Node(zz,"META",[Num(zz,3)])]);Node(zz,"META",[Num(zz,2)])])) +[2; 1] +[] +0 +[] +(mk_rewrite1 ([Node(zz, "APPLIST", [Nvar(zz, "plus_assoc_r");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])])); + +add_dad_rule "minus-identity-lr" +(Node(zz,"APPLIST",[Nvar(zz,"minus");Node(zz,"META",[Num(zz,2)]);Node(zz,"META",[Num(zz,2)])])) +[2; 1] +[2; 2] +1 +[2] +(mk_rewrite2 ([Node(zz, "APPLIST", [Nvar(zz, "minus_n_n");(mk_dad_meta 2) ])])); + +add_dad_rule "minus-identity-rl" +(Node(zz,"APPLIST",[Nvar(zz,"minus");Node(zz,"META",[Num(zz,2)]);Node(zz,"META",[Num(zz,2)])])) +[2; 2] +[2; 1] +1 +[2] +(mk_rewrite2 ([Node(zz, "APPLIST", [Nvar(zz, "minus_n_n");(mk_dad_meta 2) ])])); + +add_dad_rule "plus-sym-rl" +(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,3)]);Node(zz,"META",[Num(zz,2)])])) +[2; 2] +[2; 1] +1 +[2] +(mk_rewrite1 ([Node(zz, "APPLIST", [Nvar(zz, "plus_sym");(mk_dad_meta 3) ;(mk_dad_meta 2) ])])); + +add_dad_rule "plus-sym-lr" +(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,3)]);Node(zz,"META",[Num(zz,2)])])) +[2; 1] +[2; 2] +1 +[2] +(mk_rewrite1 ([Node(zz, "APPLIST", [Nvar(zz, "plus_sym");(mk_dad_meta 3) ;(mk_dad_meta 2) ])])); + +add_dad_rule "absorb-0-r-rl" +(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,2)]);Nvar(zz,"O")])) +[2; 2] +[1] +0 +[] +(mk_rewrite2 ([Node(zz, "APPLIST", [Nvar(zz, "plus_n_O");(mk_dad_meta 2) ])])); + +add_dad_rule "absorb-0-r-lr" +(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,2)]);Nvar(zz,"O")])) +[1] +[2; 2] +0 +[] +(mk_rewrite2 ([Node(zz, "APPLIST", [Nvar(zz, "plus_n_O");(mk_dad_meta 2) ])])); + +add_dad_rule "plus-permute-lr" +(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,4)]);Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,3)]);Node(zz,"META",[Num(zz,2)])])])) +[2; 1] +[2; 2; 2; 1] +1 +[2] +(mk_rewrite1 ([Node(zz, "APPLIST", [Nvar(zz, "plus_permute");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])])); + +add_dad_rule "plus-permute-rl" +(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,4)]);Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,3)]);Node(zz,"META",[Num(zz,2)])])])) +[2; 2; 2; 1] +[2; 1] +1 +[2] +(mk_rewrite1 ([Node(zz, "APPLIST", [Nvar(zz, "plus_permute");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])]));; + +vinterp_add "StartDad" + (function + | [] -> + (function () -> start_dad()) + | _ -> errorlabstrm "StartDad" [< >]);; diff --git a/contrib/interface/dad.mli b/contrib/interface/dad.mli new file mode 100644 index 000000000..1d097804a --- /dev/null +++ b/contrib/interface/dad.mli @@ -0,0 +1,10 @@ +open Proof_type;; +open Tacmach;; + + +val dad_rule_names : unit -> string list;; +val start_dad : unit -> unit;; +val dad_tac : (Coqast.t -> 'a) -> tactic_arg list -> goal sigma -> + goal list sigma * validation;; +val add_dad_rule : string -> Coqast.t -> (int list) -> (int list) -> + int -> (int list) -> Coqast.t -> unit;; diff --git a/contrib/interface/debug_tac.ml b/contrib/interface/debug_tac.ml new file mode 100644 index 000000000..b7542fa74 --- /dev/null +++ b/contrib/interface/debug_tac.ml @@ -0,0 +1,474 @@ +open Ast;; +open Coqast;; +open Tacmach;; +open Proof_trees;; +open Pp;; +open Printer;; +open Util;; +open Proof_type;; + +(* Compacting and uncompacting proof commands *) + +type report_tree = + Report_node of bool *int * report_tree list + | Mismatch of int * int + | Tree_fail of report_tree + | Failed of int;; + +type report_card = + Ngoals of int + | Goals_mismatch of int + | Recursive_fail of report_tree + | Fail;; + +type card_holder = report_card ref;; +type report_holder = report_tree list ref;; + +(* This tactical receives an integer and a tactic and checks that the + tactic produces that number of goals. It never fails but signals failure + by updating the boolean reference given as third argument to false. + It is especially suited for use in checked_thens below. *) + +let check_subgoals_count : card_holder -> int -> bool ref -> tactic -> tactic = + fun card_holder count flag t g -> + try + let (gls, v) as result = t g in + let len = List.length (sig_it gls) in + card_holder := + (if len = count then + (flag := true; + Ngoals count) + else + (flag := false; + Goals_mismatch len)); + result + with + e -> card_holder := Fail; + flag := false; + tclIDTAC g;; + +let no_failure = function + [Report_node(true,_,_)] -> true + | _ -> false;; + +let check_subgoals_count2 + : card_holder -> int -> bool ref -> (report_holder -> tactic) -> tactic = + fun card_holder count flag t g -> + let new_report_holder = ref ([] : report_tree list) in + let (gls, v) as result = t new_report_holder g in + let succeeded = no_failure !new_report_holder in + let len = List.length (sig_it gls) in + card_holder := + (if (len = count) & succeeded then + (flag := true; + Ngoals count) + else + (flag := false; + Recursive_fail (List.hd !new_report_holder))); + result;; + +let traceable = function + Node(_, "TACTICLIST", a::b::tl) -> true + | _ -> false;; + +let rec collect_status = function + Report_node(true,_,_)::tl -> collect_status tl + | [] -> true + | _ -> false;; + +(* This tactical receives a tactic and executes it, reporting information + about success in the report holder and a boolean reference. *) + +let count_subgoals : card_holder -> bool ref -> tactic -> tactic = + fun card_holder flag t g -> + try + let (gls, _) as result = t g in + card_holder := (Ngoals(List.length (sig_it gls))); + flag := true; + result + with + e -> card_holder := Fail; + flag := false; + tclIDTAC g;; + +let count_subgoals2 + : card_holder -> bool ref -> (report_holder -> tactic) -> tactic = + fun card_holder flag t g -> + let new_report_holder = ref([] : report_tree list) in + let (gls, v) as result = t new_report_holder g in + let succeeded = no_failure !new_report_holder in + if succeeded then + (flag := true; + card_holder := Ngoals (List.length (sig_it gls))) + else + (flag := false; + card_holder := Recursive_fail(List.hd !new_report_holder)); + result;; + +let rec local_interp : Coqast.t -> report_holder -> tactic = function + Node(_, "TACTICLIST", [a;Node(_, "TACLIST", l)]) -> + (fun report_holder -> checked_thens report_holder a l) + | Node(_, "TACTICLIST", a::((Node(_, "TACLIST", l))as b)::c::tl) -> + local_interp(ope ("TACTICLIST", (ope("TACTICLIST", [a;b]))::c::tl)) + | Node(_, "TACTICLIST", [a;b]) -> + (fun report_holder -> checked_then report_holder a b) + | Node(_, "TACTICLIST", a::b::c::tl) -> + local_interp(ope ("TACTICLIST", (ope("TACTICLIST", [a;b]))::c::tl)) + | ast -> + (fun report_holder g -> + try + let (gls, _) as result = Tacinterp.interp ast g in + report_holder := (Report_node(true, List.length (sig_it gls), [])) + ::!report_holder; + result + with e -> (report_holder := (Failed 1)::!report_holder; + tclIDTAC g)) + + +(* This tactical receives a tactic and a list of tactics as argument. + It applies the first tactic and then maps the list of tactics to + various produced sub-goals. This tactic will never fail, but reports + are added in the report_holder in the following way: + - In case of partial success, a new report_tree is added to the report_holder + - In case of failure of the first tactic, with no more indications + then Failed 0 is added to the report_holder, + - In case of partial failure of the first tactic then (Failed n) is added to + the report holder. + - In case of success of the first tactic, but count mismatch, then + Mismatch n is added to the report holder. *) + +and checked_thens: report_holder -> Coqast.t -> Coqast.t list -> tactic = + (fun report_holder t1 l g -> + let flag = ref true in + let traceable_t1 = traceable t1 in + let card_holder = ref Fail in + let new_holder = ref ([]:report_tree list) in + let tac_t1 = + if traceable_t1 then + (check_subgoals_count2 card_holder (List.length l) + flag (local_interp t1)) + else + (check_subgoals_count card_holder (List.length l) + flag (Tacinterp.interp t1)) in + let (gls, _) as result = + tclTHEN_i tac_t1 + (fun i -> + if !flag then + (fun g -> + let tac_i = (List.nth l i) in + if traceable tac_i then + local_interp tac_i new_holder g + else + try + let (gls,_) as result = Tacinterp.interp tac_i g in + let len = List.length (sig_it gls) in + new_holder := + (Report_node(true, len, []))::!new_holder; + result + with + e -> (new_holder := (Failed 1)::!new_holder; + tclIDTAC g)) + else + tclIDTAC) g in + let new_goal_list = sig_it gls in + (if !flag then + report_holder := + (Report_node(collect_status !new_holder, + (List.length new_goal_list), + List.rev !new_holder))::!report_holder + else + report_holder := + (match !card_holder with + Goals_mismatch(n) -> Mismatch(n, List.length l) + | Recursive_fail tr -> Tree_fail tr + | Fail -> Failed 1 + | _ -> errorlabstrm "check_thens" + [< 'sTR "this case should not happen in check_thens">]):: + !report_holder); + result) + +(* This tactical receives two tactics as argument, it executes the + first tactic and applies the second one to all the produced goals, + reporting information about the success of all tactics in the report + holder. It never fails. *) + +and checked_then: report_holder -> Coqast.t -> Coqast.t -> tactic = + (fun report_holder t1 t2 g -> + let flag = ref true in + let card_holder = ref Fail in + let tac_t1 = + if traceable t1 then + (count_subgoals2 card_holder flag (local_interp t1)) + else + (count_subgoals card_holder flag (Tacinterp.interp t1)) in + let new_tree_holder = ref ([] : report_tree list) in + let (gls, _) as result = + tclTHEN tac_t1 + (fun (g:goal sigma) -> + if !flag then + if traceable t2 then + local_interp t2 new_tree_holder g + else + try + let (gls, _) as result = Tacinterp.interp t2 g in + new_tree_holder := + (Report_node(true, List.length (sig_it gls),[])):: + !new_tree_holder; + result + with + e -> + (new_tree_holder := ((Failed 1)::!new_tree_holder); + tclIDTAC g) + else + tclIDTAC g) g in + (if !flag then + report_holder := + (Report_node(collect_status !new_tree_holder, + List.length (sig_it gls), + List.rev !new_tree_holder))::!report_holder + else + report_holder := + (match !card_holder with + Recursive_fail tr -> Tree_fail tr + | Fail -> Failed 1 + | _ -> error "this case should not happen in check_then")::!report_holder); + result);; + +(* This tactic applies the given tactic only to those subgoals designated + by the list of integers given as extra arguments. + *) + +let on_then : tactic_arg list -> tactic = function + (Tacexp t1)::(Tacexp t2)::l -> + tclTHEN_i (Tacinterp.interp t1) + (fun i -> + if List.mem (Integer (i + 1)) l then + (Tacinterp.interp t2) + else + tclIDTAC) + | _ -> error "bad arguments for on_then";; + +(* Analyzing error reports *) + +let rec select_success n = function + [] -> [] + | Report_node(true,_,_)::tl -> (Num((0,0),n))::select_success (n+1) tl + | _::tl -> select_success (n+1) tl;; + +let rec expand_tactic = function + Node(loc1, "TACTICLIST", [a;Node(loc2,"TACLIST", l)]) -> + Node(loc1, "TACTICLIST", + [expand_tactic a; + Node(loc2, "TACLIST", List.map expand_tactic l)]) + | Node(loc1, "TACTICLIST", a::((Node(loc2, "TACLIST", l))as b)::c::tl) -> + expand_tactic (Node(loc1, "TACTICLIST", + (Node(loc1, "TACTICLIST", [a;b]))::c::tl)) + | Node(loc1, "TACTICLIST", [a;b]) -> + Node(loc1, "TACTICLIST",[expand_tactic a;expand_tactic b]) + | Node(loc1, "TACTICLIST", a::b::c::tl) -> + expand_tactic (Node(loc1, "TACTICLIST", + (Node(loc1, "TACTICLIST", [a;b]))::c::tl)) + | any -> any;; + +let rec reconstruct_success_tac ast = + match ast with + Node(_, "TACTICLIST", [a;Node(_,"TACLIST",l)]) -> + (function + Report_node(true, n, l) -> ast + | Report_node(false, n, rl) -> + ope("TACTICLIST",[a;ope("TACLIST", + List.map2 reconstruct_success_tac l rl)]) + | Failed n -> ope("Idtac",[]) + | Tree_fail r -> reconstruct_success_tac a r + | Mismatch (n,p) -> a) + | Node(_, "TACTICLIST", [a;b]) -> + (function + Report_node(true, n, l) -> ast + | Report_node(false, n, rl) -> + let selected_indices = select_success 1 rl in + ope("OnThen", a::b::selected_indices) + | Failed n -> ope("Idtac",[]) + | Tree_fail r -> reconstruct_success_tac a r + | _ -> error "this error case should not happen in a THEN tactic") + | _ -> + (function + Report_node(true, n, l) -> ast + | Failed n -> ope("Idtac",[]) + | _ -> + errorlabstrm + "this error case should not happen on an unknown tactic" + [< 'sTR "error in reconstruction with "; 'fNL; + (gentacpr ast) >]);; + + +let rec path_to_first_error = function +| Report_node(true, _, l) -> + let rec find_first_error n = function + | (Report_node(true, _, _))::tl -> find_first_error (n + 1) tl + | it::tl -> n, it + | [] -> error "no error detected" in + let p, t = find_first_error 1 l in + p::(path_to_first_error t) +| _ -> [];; + +let rec flatten_then_list tail = function + | Node(_, "TACTICLIST", [a;b]) -> + flatten_then_list ((flatten_then b)::tail) a + | ast -> ast::tail +and flatten_then = function + Node(_, "TACTICLIST", [a;b]) -> + ope("TACTICLIST", flatten_then_list [flatten_then b] a) + | Node(_, "TACLIST", l) -> + ope("TACLIST", List.map flatten_then l) + | Node(_, "OnThen", t1::t2::l) -> + ope("OnThen", (flatten_then t1)::(flatten_then t2)::l) + | ast -> ast;; + +let debug_tac = function + [(Tacexp ast)] -> + (fun g -> + let report = ref ([] : report_tree list) in + let result = local_interp ast report g in + let clean_ast = expand_tactic ast in + let report_tree = + try List.hd !report with + Failure "hd" -> (mSGNL [< 'sTR "report is empty" >]; Failed 1) in + let success_tac = + reconstruct_success_tac clean_ast report_tree in + let compact_success_tac = + flatten_then success_tac in + mSGNL [< 'fNL; 'sTR "========= Successful tactic ============="; + 'fNL; + gentacpr compact_success_tac; 'fNL; + 'sTR "========= End of successful tactic ============">]; + result) + | _ -> error "wrong arguments for debug_tac";; + +add_tactic "DebugTac" debug_tac;; + +hide_tactic "OnThen" on_then;; + +let rec clean_path p ast l = + match ast, l with + Node(_, "TACTICLIST", ([_;_] as tacs)), fst::tl -> + fst::(clean_path 0 (List.nth tacs (fst - 1)) tl) + | Node(_, "TACTICLIST", tacs), 2::tl -> + let rank = (List.length tacs) - p in + rank::(clean_path 0 (List.nth tacs (rank - 1)) tl) + | Node(_, "TACTICLIST", tacs), 1::tl -> + clean_path (p+1) ast tl + | Node(_, "TACLIST", tacs), fst::tl -> + fst::(clean_path 0 (List.nth tacs (fst - 1)) tl) + | _, [] -> [] + | _, _ -> failwith "this case should not happen in clean_path";; + + + +let rec report_error + : Coqast.t -> goal sigma option ref -> Coqast.t ref -> int list ref -> + int list -> tactic = + fun ast the_goal the_ast returned_path path -> + match ast with + Node(loc1, "TACTICLIST", [a;(Node(loc2, "TACLIST", l)) as tail]) -> + let the_card_holder = ref Fail in + let the_flag = ref false in + let the_exn = ref (Failure "") in + tclTHENS + (fun g -> + let result = + check_subgoals_count + the_card_holder + (List.length l) + the_flag + (fun g2 -> + try + (report_error a the_goal the_ast returned_path (1::path) g2) + with + e -> (the_exn := e; raise e)) + g in + if !the_flag then + result + else + (match !the_card_holder with + Fail -> + the_ast := ope("TACTICLIST", [!the_ast; tail]); + raise !the_exn + | Goals_mismatch p -> + the_ast := ast; + returned_path := path; + error ("Wrong number of tactics: expected " ^ + (string_of_int (List.length l)) ^ " received " ^ + (string_of_int p)) + | _ -> error "this should not happen")) + (let rec fold_num n = function + [] -> [] + | t::tl -> (report_error t the_goal the_ast returned_path (n::2::path)):: + (fold_num (n + 1) tl) in + fold_num 1 l) + | Node(_, "TACTICLIST", a::((Node(_, "TACLIST", l)) as b)::c::tl) -> + report_error(ope("TACTICLIST", (ope("TACTICLIST", [a;b]))::c::tl)) + the_goal the_ast returned_path path + | Node(_, "TACTICLIST", [a;b]) -> + let the_count = ref 1 in + tclTHEN + (fun g -> + try + report_error a the_goal the_ast returned_path (1::path) g + with + e -> + (the_ast := ope("TACTICLIST", [!the_ast; b]); + raise e)) + (fun g -> + try + let result = + report_error b the_goal the_ast returned_path (2::path) g in + the_count := !the_count + 1; + result + with + e -> + if !the_count > 1 then + mSGNL + [< 'sTR "in branch no "; 'iNT !the_count; + 'sTR " after tactic "; + gentacpr a >]; + raise e) + | Node(_, "TACTICLIST", a::b::c::tl) -> + report_error (ope("TACTICLIST", (ope("TACTICLIST", [a;b]))::c::tl)) + the_goal the_ast returned_path path + | ast -> + (fun g -> + try + Tacinterp.interp ast g + with + e -> + (the_ast := ast; + the_goal := Some g; + returned_path := path; + raise e));; + +let strip_some = function + Some n -> n + | None -> failwith "No optional value";; + +let descr_first_error = function + [(Tacexp ast)] -> + (fun g -> + let the_goal = ref (None : goal sigma option) in + let the_ast = ref ast in + let the_path = ref ([] : int list) in + try + let result = report_error ast the_goal the_ast the_path [] g in + mSGNL [< 'sTR "no Error here" >]; + result + with + e -> + (mSGNL [< 'sTR "Execution of this tactic raised message " ; 'fNL; + 'fNL; Errors.explain_exn e; 'fNL; + 'fNL; 'sTR "on goal" ; 'fNL; + pr_goal (sig_it (strip_some !the_goal)); 'fNL; + 'sTR "faulty tactic is"; 'fNL; 'fNL; + gentacpr (flatten_then !the_ast); 'fNL >]; + tclIDTAC g)) + | _ -> error "wrong arguments for descr_first_error";; + +add_tactic "DebugTac2" descr_first_error;; diff --git a/contrib/interface/debug_tac.mli b/contrib/interface/debug_tac.mli new file mode 100644 index 000000000..a582b029e --- /dev/null +++ b/contrib/interface/debug_tac.mli @@ -0,0 +1,6 @@ + +val report_error : Coqast.t -> + Proof_type.goal Proof_type.sigma option ref -> + Coqast.t ref -> int list ref -> int list -> Tacmach.tactic;; + +val clean_path : int -> Coqast.t -> int list -> int list;; diff --git a/contrib/interface/history.ml b/contrib/interface/history.ml new file mode 100644 index 000000000..f73c20849 --- /dev/null +++ b/contrib/interface/history.ml @@ -0,0 +1,373 @@ +open Paths;; + +type tree = {mutable index : int; + parent : tree option; + path_to_root : int list; + mutable is_open : bool; + mutable sub_proofs : tree list};; + +type prf_info = { + mutable prf_length : int; + mutable ranks_and_goals : (int * int * tree) list; + mutable border : tree list; + prf_struct : tree};; + +let theorem_proofs = ((Hashtbl.create 17): + (string, prf_info) Hashtbl.t);; + + +let rec mk_trees_for_goals path tree rank k n = + if k = (n + 1) then + [] + else + { index = rank; + parent = tree; + path_to_root = k::path; + is_open = true; + sub_proofs = [] } ::(mk_trees_for_goals path tree rank (k+1) n);; + + +let push_command s rank ngoals = + let ({prf_length = this_length; + ranks_and_goals = these_ranks; + border = this_border} as proof_info) = + Hashtbl.find theorem_proofs s in + let rec push_command_aux n = function + [] -> failwith "the given rank was too large" + | a::l -> + if n = 1 then + let {path_to_root = p} = a in + let new_trees = mk_trees_for_goals p (Some a) (this_length + 1) 1 ngoals in + new_trees,(new_trees@l),a + else + let new_trees, res, this_tree = push_command_aux (n-1) l in + new_trees,(a::res),this_tree in + let new_trees, new_border, this_tree = + push_command_aux rank this_border in + let new_length = this_length + 1 in + begin + proof_info.border <- new_border; + proof_info.prf_length <- new_length; + proof_info.ranks_and_goals <- (rank, ngoals, this_tree)::these_ranks; + this_tree.index <- new_length; + this_tree.is_open <- false; + this_tree.sub_proofs <- new_trees + end;; + +let get_tree_for_rank thm_name rank = + let {ranks_and_goals=l;prf_length=n} = + Hashtbl.find theorem_proofs thm_name in + let rec get_tree_aux = function + [] -> + failwith + "inconsistent values for thm_name and rank in get_tree_for_rank" + | (_,_,({index=i} as tree))::tl -> + if i = rank then + tree + else + get_tree_aux tl in + get_tree_aux l;; + +let get_path_for_rank thm_name rank = + let {path_to_root=l}=get_tree_for_rank thm_name rank in + l;; + +let rec list_descendants_aux l tree = + let {index = i; is_open = open_status; sub_proofs = tl} = tree in + let res = (List.fold_left list_descendants_aux l tl) in + if open_status then i::res else res;; + +let list_descendants thm_name rank = + list_descendants_aux [] (get_tree_for_rank thm_name rank);; + +let parent_from_rank thm_name rank = + let {parent=mommy} = get_tree_for_rank thm_name rank in + match mommy with + Some x -> Some x.index + | None -> None;; + +let first_child_command thm_name rank = + let {sub_proofs = l} = get_tree_for_rank thm_name rank in + let rec first_child_rec = function + [] -> None + | {index=i;is_open=b}::l -> + if b then + (first_child_rec l) + else + Some i in + first_child_rec l;; + +type index_or_rank = Is_index of int | Is_rank of int;; + +let first_child_command_or_goal thm_name rank = + let proof_info = Hashtbl.find theorem_proofs thm_name in + let {sub_proofs=l}=get_tree_for_rank thm_name rank in + match l with + [] -> None + | ({index=i;is_open=b} as t)::_ -> + if b then + let rec get_rank n = function + [] -> failwith "A goal is lost in first_child_command_or_goal" + | a::l -> + if a==t then + n + else + get_rank (n + 1) l in + Some(Is_rank(get_rank 1 proof_info.border)) + else + Some(Is_index i);; + +let next_sibling thm_name rank = + let ({parent=mommy} as t)=get_tree_for_rank thm_name rank in + match mommy with + None -> None + | Some real_mommy -> + let {sub_proofs=l}=real_mommy in + let rec next_sibling_aux b = function + (opt_first, []) -> + if b then + opt_first + else + failwith "inconsistency detected in next_sibling" + | (opt_first, {is_open=true}::l) -> + next_sibling_aux b (opt_first, l) + | (Some(first),({index=i; is_open=false} as t')::l) -> + if b then + Some i + else + next_sibling_aux (t == t') (Some first,l) + | None,({index=i;is_open=false} as t')::l -> + next_sibling_aux (t == t') ((Some i), l) + in + Some (next_sibling_aux false (None, l));; + + +let prefix l1 l2 = + let l1rev = List.rev l1 in + let l2rev = List.rev l2 in + is_prefix l1rev l2rev;; + +let rec remove_all_prefixes p = function + [] -> [] + | a::l -> + if is_prefix p a then + (remove_all_prefixes p l) + else + a::(remove_all_prefixes p l);; + +let recompute_border tree = + let rec recompute_border_aux tree acc = + let {is_open=b;sub_proofs=l}=tree in + if b then + tree::acc + else + List.fold_right recompute_border_aux l acc in + recompute_border_aux tree [];; + + +let historical_undo thm_name rank = + let ({ranks_and_goals=l} as proof_info)= + Hashtbl.find theorem_proofs thm_name in + let rec undo_aux acc = function + [] -> failwith "bad rank provided for undoing in historical_undo" + | (r, n, ({index=i} as tree))::tl -> + let this_path_reversed = List.rev tree.path_to_root in + let res = remove_all_prefixes this_path_reversed acc in + if i = rank then + begin + proof_info.prf_length <- i-1; + proof_info.ranks_and_goals <- tl; + tree.is_open <- true; + tree.sub_proofs <- []; + proof_info.border <- recompute_border proof_info.prf_struct; + this_path_reversed::res + end + else + begin + tree.is_open <- true; + tree.sub_proofs <- []; + undo_aux (this_path_reversed::res) tl + end + in + List.map List.rev (undo_aux [] l);; + +(* The following function takes a list of trees and compute the + number of elements whose path is lexically smaller or a suffixe of + the path given as a first argument. This works under the precondition that + the list is lexicographically order. *) + +let rec logical_undo_on_border the_tree rev_path = function + [] -> (0,[the_tree]) + | ({path_to_root=p}as tree)::tl -> + let p_rev = List.rev p in + if is_prefix rev_path p_rev then + let (k,res) = (logical_undo_on_border the_tree rev_path tl) in + (k+1,res) + else if lex_smaller p_rev rev_path then + let (k,res) = (logical_undo_on_border the_tree rev_path tl) in + (k,tree::res) + else + (0, the_tree::tree::tl);; + + +let logical_undo thm_name rank = + let ({ranks_and_goals=l; border=last_border} as proof_info)= + Hashtbl.find theorem_proofs thm_name in + let ({path_to_root=ref_path} as ref_tree)=get_tree_for_rank thm_name rank in + let rev_ref_path = List.rev ref_path in + let rec logical_aux lex_smaller_offset family_width = function + [] -> failwith "this case should never happen in logical_undo" + | (r,n,({index=i;path_to_root=this_path; sub_proofs=these_goals} as tree)):: + tl -> + let this_path_rev = List.rev this_path in + let new_rank, new_offset, new_width, kept = + if is_prefix rev_ref_path this_path_rev then + (r + lex_smaller_offset), lex_smaller_offset, + (family_width + 1 - n), false + else if lex_smaller this_path_rev rev_ref_path then + r, (lex_smaller_offset - 1 + n), family_width, true + else + (r + 1 - family_width+ lex_smaller_offset), + lex_smaller_offset, family_width, true in + if i=rank then + [i,new_rank],[], tl, rank + else + let ranks_undone, ranks_kept, ranks_and_goals, current_rank = + (logical_aux new_offset new_width tl) in + begin + if kept then + begin + tree.index <- current_rank; + ranks_undone, ((i,new_rank)::ranks_kept), + ((new_rank, n, tree)::ranks_and_goals), + (current_rank + 1) + end + else + ((i,new_rank)::ranks_undone), ranks_kept, + ranks_and_goals, current_rank + end in + let number_suffix, new_border = + logical_undo_on_border ref_tree rev_ref_path last_border in + let changed_ranks_undone, changed_ranks_kept, new_ranks_and_goals, + new_length_plus_one = logical_aux 0 number_suffix l in + let the_goal_index = + let rec compute_goal_index n = function + [] -> failwith "this case should never happen in logical undo (2)" + | {path_to_root=path}::tl -> + if List.rev path = (rev_ref_path) then + n + else + compute_goal_index (n+1) tl in + compute_goal_index 1 new_border in + begin + ref_tree.is_open <- true; + ref_tree.sub_proofs <- []; + proof_info.border <- new_border; + proof_info.ranks_and_goals <- new_ranks_and_goals; + proof_info.prf_length <- new_length_plus_one - 1; + changed_ranks_undone, changed_ranks_kept, proof_info.prf_length, + the_goal_index + end;; + +let start_proof thm_name = + let the_tree = + {index=0;parent=None;path_to_root=[];is_open=true;sub_proofs=[]} in + Hashtbl.add theorem_proofs thm_name + {prf_length=0; + ranks_and_goals=[]; + border=[the_tree]; + prf_struct=the_tree};; + +let dump_sequence chan s = + match (Hashtbl.find theorem_proofs s) with + {ranks_and_goals=l}-> + let rec dump_rec = function + [] -> () + | (r,n,_)::tl -> + dump_rec tl; + output_string chan (string_of_int r); + output_string chan ","; + output_string chan (string_of_int n); + output_string chan "\n" in + begin + dump_rec l; + output_string chan "end\n" + end;; + + +let proof_info_as_string s = + let res = ref "" in + match (Hashtbl.find theorem_proofs s) with + {prf_struct=tree} -> + let open_goal_counter = ref 0 in + let rec dump_rec = function + {index=i;sub_proofs=trees;parent=the_parent;is_open=op} -> + begin + (match the_parent with + None -> + if op then + res := !res ^ "\"open goal\"\n" + | Some {index=j} -> + begin + res := !res ^ (string_of_int j); + res := !res ^ " -> "; + if op then + begin + res := !res ^ "\"open goal "; + open_goal_counter := !open_goal_counter + 1; + res := !res ^ (string_of_int !open_goal_counter); + res := !res ^ "\"\n"; + end + else + begin + res := !res ^ (string_of_int i); + res := !res ^ "\n" + end + end); + List.iter dump_rec trees + end in + dump_rec tree; + !res;; + + +let dump_proof_info chan s = + match (Hashtbl.find theorem_proofs s) with + {prf_struct=tree} -> + let open_goal_counter = ref 0 in + let rec dump_rec = function + {index=i;sub_proofs=trees;parent=the_parent;is_open=op} -> + begin + (match the_parent with + None -> + if op then + output_string chan "\"open goal\"\n" + | Some {index=j} -> + begin + output_string chan (string_of_int j); + output_string chan " -> "; + if op then + begin + output_string chan "\"open goal "; + open_goal_counter := !open_goal_counter + 1; + output_string chan (string_of_int !open_goal_counter); + output_string chan "\"\n"; + end + else + begin + output_string chan (string_of_int i); + output_string chan "\n" + end + end); + List.iter dump_rec trees + end in + dump_rec tree;; + +let get_nth_open_path s n = + match Hashtbl.find theorem_proofs s with + {border=l} -> + let {path_to_root=p}=List.nth l (n - 1) in + p;; + +let border_length s = + match Hashtbl.find theorem_proofs s with + {border=l} -> List.length l;; diff --git a/contrib/interface/history.mli b/contrib/interface/history.mli new file mode 100644 index 000000000..053883f0d --- /dev/null +++ b/contrib/interface/history.mli @@ -0,0 +1,12 @@ +type prf_info;; + +val start_proof : string -> unit;; +val historical_undo : string -> int -> int list list +val logical_undo : string -> int -> (int * int) list * (int * int) list * int * int +val dump_sequence : out_channel -> string -> unit +val proof_info_as_string : string -> string +val dump_proof_info : out_channel -> string -> unit +val push_command : string -> int -> int -> unit +val get_path_for_rank : string -> int -> int list +val get_nth_open_path : string -> int -> int list +val border_length : string -> int diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml new file mode 100644 index 000000000..09cefb2d9 --- /dev/null +++ b/contrib/interface/name_to_ast.ml @@ -0,0 +1,247 @@ +open Sign;; +open Classops;; +open Names;; +open Coqast;; +open Ast;; +open Termast;; +open Term;; +open Impargs;; +open Reduction;; +open Libobject;; +open Environ;; +open Declarations;; +open Pretty;; +open Inductive;; +open Util;; +open Pp;; +open Declare;; + + +(* This function converts the parameter binders of an inductive definition, + in particular you have to be careful to handle each element in the + context containing all previously defined variables. This squeleton + of this procedure is taken from the function print_env in pretty.ml *) +let convert_env = + let convert_binder env (na, _, c) = + match na with + | Name id -> + ope("BINDER", + [ast_of_constr true env c;nvar(string_of_id id)]) + | Anonymous -> failwith "anomaly: Anonymous variables in inductives" in + let rec cvrec env = function + [] -> [] + | b::rest -> (convert_binder env b)::(cvrec (push_rel b env) rest) in + cvrec (Global.env());; + +(* let mib string = + let sp = Nametab.sp_of_id CCI (id_of_string string) in + let lobj = Lib.map_leaf (objsp_of sp) in + let (cmap, _) = outMutualInductive lobj in + Listmap.map cmap CCI;; *) + +(* This function is directly inspired by print_impl_args in pretty.ml *) + +let impl_args_to_string = function + [] -> None + | [i] -> Some(" position " ^ (string_of_int i) ^ " is implicit.") + | l -> Some (" positions " ^ + (List.fold_right (fun i s -> (string_of_int i) ^ " " ^ s) + l + " are implicit."));; + +(* This function is directly inspired by implicit_args_id in pretty.ml *) + +let implicit_args_id_to_ast_list id l ast_list = + (match impl_args_to_string l with + None -> ast_list + | Some(s) -> (str("For " ^ (string_of_id id))):: + (str s):: + ast_list);; + +(* This function construct an ast to enumerate the implicit positions for an + inductive type and its constructors. It is obtained directly from + implicit_args_msg in pretty.ml. *) + +let implicit_args_to_ast_list sp mipv = + let implicit_args_descriptions = + let ast_list = ref ([]:Coqast.t list) in + (Array.iteri + (fun i mip -> + let imps = inductive_implicits_list(sp, i) in + (ast_list := + implicit_args_id_to_ast_list mip.mind_typename imps !ast_list; + Array.iteri + (fun j idc -> + let impls = constructor_implicits_list ((sp,i), succ j) in + ast_list := + implicit_args_id_to_ast_list idc impls !ast_list) + mip.mind_consnames)) + mipv; + !ast_list) in + match implicit_args_descriptions with + [] -> [] + | _ -> [ope("COMMENT", List.rev implicit_args_descriptions)];; + +let convert_qualid qid = + let d, id = Nametab.repr_qualid qid in + match d with + [] -> nvar(string_of_id id) + | _ -> ope("QUALID", List.fold_right (fun s l -> (nvar s)::l) d + [nvar (string_of_id id)]);; + +(* This function converts constructors for an inductive definition to a + Coqast.t. It is obtained directly from print_constructors in pretty.ml *) + +let convert_constructors envpar names types = + let array_idC = + array_map2 + (fun n t -> ope("BINDER", + [ast_of_constr true envpar t; nvar(string_of_id n)])) + names types in + Node((0,0), "BINDERLIST", Array.to_list array_idC);; + +(* this function converts one inductive type in a possibly multiple inductive + definition *) + +let convert_one_inductive sp tyi = + let (ref, params, arity, cstrnames, cstrtypes) = build_inductive sp tyi in + let env = Global.env () in + let envpar = push_rels params env in + ope("VERNACARGLIST", + [convert_qualid (Global.qualid_of_global(IndRef (sp, tyi))); + ope("CONSTR", [ast_of_constr true envpar arity]); + ope("BINDERLIST", convert_env(List.rev params)); + convert_constructors envpar cstrnames cstrtypes]);; + +(* This function converts a Mutual inductive definition to a Coqast.t. + It is obtained directly from print_mutual in pretty.ml. However, all + references to kinds have been removed and it treats only CCI stuff. *) + +let mutual_to_ast_list sp mib = + let mipv = (Global.lookup_mind sp).mind_packets in + let _, ast_list = + Array.fold_right + (fun mi (n,l) -> (n+1, (convert_one_inductive sp n)::l)) mipv (0, []) in + (ope("MUTUALINDUCTIVE", + [str (if (mipv.(0)).mind_finite then "Inductive" else "CoInductive"); + ope("VERNACARGLIST", ast_list)]):: + (implicit_args_to_ast_list sp mipv));; + +let constr_to_ast v = + ast_of_constr true (Global.env()) v;; + +let implicits_to_ast_list implicits = + (match (impl_args_to_string implicits) with + None -> [] + | Some s -> [ope("COMMENT", [str s])]);; + +let make_variable_ast name typ implicits = + (ope("VARIABLE", + [str "VARIABLE"; + ope("BINDERLIST", + [ope("BINDER", + [(constr_to_ast (body_of_type typ)); + nvar name])])]))::(implicits_to_ast_list implicits) + ;; + +let make_definition_ast name c typ implicits = + (ope("DEFINITION", + [str "DEFINITION"; + nvar name; + ope("COMMAND", + [ope("CAST", + [(constr_to_ast c); + (constr_to_ast (body_of_type typ))])])])):: + (implicits_to_ast_list implicits);; + +(* This function is inspired by print_constant *) +let constant_to_ast_list sp = + let cb = Global.lookup_constant sp in + if kind_of_path sp = CCI then + let c = cb.const_body in + let typ = cb.const_type in + let l = constant_implicits_list sp in + (match c with + None -> + make_variable_ast (string_of_id (basename sp)) typ l + | Some c1 -> + make_definition_ast (string_of_id (basename sp)) c1 typ l) + else + errorlabstrm "print" [< 'sTR "printing of FW terms not implemented" >];; + +let variable_to_ast_list sp = + let ((id, c, v), _, _) = get_variable sp in + let l = implicits_of_var sp in + (match c with + None -> + make_variable_ast (string_of_id id) v l + | Some c1 -> + make_definition_ast (string_of_id id) c1 v l);; + +(* this function is taken from print_inductive in file pretty.ml *) + +let inductive_to_ast_list sp = + let mib = Global.lookup_mind sp in + if kind_of_path sp = CCI then + mutual_to_ast_list sp mib + else + errorlabstrm "print" + [< 'sTR "printing of FW not implemented" >];; + +(* this function is inspired by print_leaf_entry from pretty.ml *) + +let leaf_entry_to_ast_list (sp,lobj) = + let tag = object_tag lobj in + match (sp,tag) with + | (_, "VARIABLE") -> variable_to_ast_list sp + | (_, ("CONSTANT"|"PARAMETER")) -> constant_to_ast_list sp + | (_, "INDUCTIVE") -> inductive_to_ast_list sp + | (_, s) -> + errorlabstrm + "print" [< 'sTR ("printing of unrecognized object " ^ + s ^ " has been required") >];; + + + + +(* this function is inspired by print_name *) +let name_to_ast (qid:Nametab.qualid) = + let l = + try + let sp,_ = Nametab.locate_obj qid in + let (sp,lobj) = + let (sp,entry) = + List.find (fun en -> (fst en) = sp) (Lib.contents_after None) + in + match entry with + | Lib.Leaf obj -> (sp,obj) + | _ -> raise Not_found + in + leaf_entry_to_ast_list (sp,lobj) + with Not_found -> + try + match Nametab.locate qid with + | ConstRef sp -> constant_to_ast_list sp + | IndRef (sp,_) -> inductive_to_ast_list sp + | ConstructRef ((sp,_),_) -> inductive_to_ast_list sp + | VarRef sp -> variable_to_ast_list sp + with Not_found -> + try (* Var locale de but, pas var de section... donc pas d'implicits *) + let dir,name = Nametab.repr_qualid qid in + if dir <> [] then raise Not_found; + let (c,typ) = Global.lookup_named name in + (match c with + None -> make_variable_ast (string_of_id name) typ [] + | Some c1 -> make_definition_ast + (string_of_id name) c1 typ []) + with Not_found -> + try + let sp = Syntax_def.locate_syntactic_definition qid in + errorlabstrm "print" + [< 'sTR "printing of syntax definitions not implemented" >] + with Not_found -> + errorlabstrm "print" + [< Nametab.pr_qualid qid; + 'sPC; 'sTR "not a defined object" >] in + ope("vernac_list", l);; + diff --git a/contrib/interface/name_to_ast.mli b/contrib/interface/name_to_ast.mli new file mode 100644 index 000000000..894b27392 --- /dev/null +++ b/contrib/interface/name_to_ast.mli @@ -0,0 +1,2 @@ +val name_to_ast : Nametab.qualid -> Coqast.t;; +val convert_qualid : Nametab.qualid -> Coqast.t;; diff --git a/contrib/interface/paths.ml b/contrib/interface/paths.ml new file mode 100644 index 000000000..b1244d158 --- /dev/null +++ b/contrib/interface/paths.ml @@ -0,0 +1,26 @@ +let int_list_to_string s l = + List.fold_left + (fun s -> (fun v -> s ^ " " ^ (string_of_int v))) + s + l;; + +(* Given two paths, this function returns the longest common prefix and the + two suffixes. *) +let rec decompose_path + : (int list * int list) -> (int list * int list * int list) = + function + (a::l,b::m) when a = b -> + let (c,p1,p2) = decompose_path (l,m) in + (a::c,p1,p2) + | p1,p2 -> [], p1, p2;; + +let rec is_prefix p1 p2 = match p1,p2 with + [], _ -> true +| a::tl1, b::tl2 when a = b -> is_prefix tl1 tl2 +| _ -> false;; + +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 diff --git a/contrib/interface/paths.mli b/contrib/interface/paths.mli new file mode 100644 index 000000000..266207238 --- /dev/null +++ b/contrib/interface/paths.mli @@ -0,0 +1,4 @@ +val decompose_path : (int list * int list) -> (int list * int list * int list);; +val int_list_to_string : string -> int list -> string;; +val is_prefix : int list -> int list -> bool;; +val lex_smaller : int list -> int list -> bool;; diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml new file mode 100644 index 000000000..7d3c4400c --- /dev/null +++ b/contrib/interface/pbp.ml @@ -0,0 +1,705 @@ +(* A proof by pointing algorithm. *) + + +open Util;; +open Names;; +open Term;; +open Tactics;; +open Tacticals;; +open Hipattern;; +open Pattern;; +open Reduction;; +open Coqast;; +open Rawterm;; +open Environ;; + +open Proof_trees;; +open Proof_type;; +open Tacmach;; +open Typing;; +open Pp;; + +(* get_hyp_by_name : goal sigma -> string -> constr, + looks up for an hypothesis, 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;; + +type pbp_rule = (identifier list * + string list * + bool * + string option * + (types, constr) kind_of_term * + int list * + (identifier list -> + string list -> + bool -> + string option -> (types, constr) kind_of_term -> int list -> Coqast.t)) -> + Coqast.t option;; + +let zz = (0,0);; + +let make_named_intro s = + Node(zz, "Intros", + [Node(zz,"INTROPATTERN", + [Node(zz,"LISTPATTERN", + [Node(zz, "IDENTIFIER", + [Nvar(zz, s)])])])]);; + +let get_name_from_intro = function + Node(a, "Intros", + [Node(b,"INTROPATTERN", + [Node(c,"LISTPATTERN", + [Node(d, "IDENTIFIER", + [Nvar(e, s)])])])]) -> + Some s + | _ -> None;; + +let make_clears = function + [] -> Node(zz, "Idtac",[]) + | str_list -> + 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 + [] -> tactic + | l -> Node(zz, "TACTICLIST", [make_clears l; tactic]);; + +let make_final_cmd f optname clear_names constr path = + let tactic = f optname constr path in + add_clear_names_if_necessary (f optname constr path) clear_names;; + +let (rem_cast:pbp_rule) = function + (a,c,cf,o, IsCast(f,_), p, func) -> + Some(func a c cf o (kind_of_term f) p) + | _ -> None;; + +let (forall_intro: pbp_rule) = function + (avoid, + clear_names, + clear_flag, + None, + IsProd(Name x, _, body), + (2::path), + f) -> + let x' = next_global_ident_away x avoid in + Some(Node(zz, "TACTICLIST", + [make_named_intro (string_of_id x'); f (x'::avoid) + clear_names clear_flag None (kind_of_term body) path])) +| _ -> None;; + +let (imply_intro2: pbp_rule) = function + avoid, clear_names, + clear_flag, None, IsProd(Anonymous, _, body), 2::path, f -> + let h' = next_global_ident_away (id_of_string "H") avoid in + Some(Node(zz, "TACTICLIST", + [make_named_intro (string_of_id h'); + f (h'::avoid) clear_names clear_flag None (kind_of_term body) path])) + | _ -> None;; + + +let (imply_intro1: pbp_rule) = function + avoid, clear_names, + clear_flag, None, IsProd(Anonymous, prem, body), 1::path, f -> + let h' = next_global_ident_away (id_of_string "H") avoid in + let str_h' = (string_of_id h') in + Some(Node(zz, "TACTICLIST", + [make_named_intro str_h'; + f (h'::avoid) clear_names clear_flag (Some str_h') + (kind_of_term prem) path])) + | _ -> None;; + + +let (forall_elim: pbp_rule) = function + avoid, clear_names, clear_flag, + Some h, IsProd(Name x, _, body), 2::path, f -> + let h' = next_global_ident_away (id_of_string "H") avoid in + let clear_names' = if clear_flag then h::clear_names else clear_names in + let str_h' = (string_of_id h') in + Some(Node(zz, "TACTICLIST", + [Node(zz,"Generalize",[Node + (zz, "COMMAND", + [Node + (zz, "APPLIST", + [Nvar (zz, h); + Node(zz,"APPLIST", [Nvar (zz, "PBP_META"); + Nvar(zz, "Value_for_" ^ (string_of_id x))])])])]); + make_named_intro str_h'; + f (h'::avoid) clear_names' true (Some str_h') (kind_of_term body) path])) + | _ -> None;; + +let (imply_elim1: pbp_rule) = function + avoid, clear_names, clear_flag, + Some h, IsProd(Anonymous, prem, body), 1::path, f -> + let clear_names' = if clear_flag then h::clear_names else clear_names in + let h' = next_global_ident_away (id_of_string "H") avoid in + let str_h' = (string_of_id h') in + Some(Node + (zz, "TACTICLIST", + [Node + (zz, "CutAndApply", + [Node (zz, "COMMAND", [Nvar (zz, h)])]); + Node(zz, "TACLIST", + [Node + (zz, "TACTICLIST", + [Node (zz, "Intro", [Nvar (zz, str_h')]); + make_clears (h::clear_names)]); + Node (zz, "TACTICLIST", + [f avoid clear_names' false None + (kind_of_term prem) path])])])) + | _ -> None;; + +let (imply_elim2: pbp_rule) = function + avoid, clear_names, clear_flag, + Some h, IsProd(Anonymous, prem, body), 2::path, f -> + let clear_names' = if clear_flag then h::clear_names else clear_names in + let h' = next_global_ident_away (id_of_string "H") avoid in + let str_h' = (string_of_id h') in + Some(Node + (zz, "TACTICLIST", + [Node + (zz, "CutAndApply", + [Node (zz, "COMMAND", [Nvar (zz, h)])]); + Node(zz, "TACLIST", + [Node + (zz, "TACTICLIST", + [Node (zz, "Intro", [Nvar (zz, str_h')]); + f (h'::avoid) clear_names' false (Some str_h') + (kind_of_term body) path]); + Node (zz, "TACTICLIST", + [make_clears clear_names])])])) + | _ -> None;; + +let reference dir s = + let dir = "Coq"::"Init"::[dir] in + let id = id_of_string s in + try + Nametab.locate_in_absolute_module dir id + with Not_found -> + anomaly ("Coqlib: cannot find "^ + (Nametab.string_of_qualid (Nametab.make_qualid dir id))) + +let constant dir s = + Declare.constr_of_reference Evd.empty (Global.env()) (reference dir s);; + + +let andconstr: unit -> constr = Coqlib.build_coq_and;; +let prodconstr () = constant "Datatypes" "prod";; +let exconstr () = constant "Logic" "ex";; +let exTconstr () = constant "Logic_Type" "exT";; +let sigconstr () = constant "Specif" "sig";; +let sigTconstr () = constant "Logic_type" "sigT";; +let orconstr = Coqlib.build_coq_or;; +let sumboolconstr = Coqlib.build_coq_sumbool;; +let sumconstr() = constant "Datatypes" "sum";; +let notconstr = Coqlib.build_coq_not;; +let notTconstr () = constant "Logic_type" "notT";; + +let is_matching_local a b = is_matching (pattern_of_constr a) b;; + +let (and_intro: pbp_rule) = function + avoid, clear_names, clear_flag, + None, IsApp(and_oper, [|c1; c2|]), 2::a::path, f + -> + if ((is_matching_local (andconstr()) and_oper) or + (is_matching_local (prodconstr ()) and_oper)) & (a = 1 or a = 2) then + let cont_term = if a = 1 then c1 else c2 in + let cont_cmd = f avoid clear_names false None + (kind_of_term cont_term) path in + let clear_cmd = make_clears clear_names in + let cmds = List.map + (function tac -> + Node (zz, "TACTICLIST", [tac])) + (if a = 1 + then [cont_cmd;clear_cmd] + else [clear_cmd;cont_cmd]) in + Some + (Node + (zz, "TACTICLIST", + [Node (zz, "Split", [Node (zz, "BINDINGS", [])]); + Node + (zz, "TACLIST", cmds)])) + else None + | _ -> None;; + +let (ex_intro: pbp_rule) = function + avoid, clear_names, clear_flag, None, + IsApp(oper, [| c1; c2|]), 2::2::2::path, f + when (is_matching_local (exconstr ()) oper) or (is_matching_local (exTconstr ()) oper) + or (is_matching_local (sigconstr ()) oper) + or (is_matching_local (sigTconstr ()) oper) -> + (match kind_of_term c2 with + IsLambda(Name x, _, body) -> + Some(Node(zz, "Split", + [Node(zz, "BINDINGS", + [Node(zz, "BINDING", + [Node(zz, "COMMAND", + [Node(zz, "APPLIST", + [Nvar(zz, "PBP_META"); + Nvar(zz, + ("Value_for_" ^ + (string_of_id x)))]) + ])])])])) + | _ -> None) + | _ -> None;; + +let (or_intro: pbp_rule) = function + avoid, clear_names, clear_flag, None, + IsApp(or_oper, [|c1; c2 |]), 2::a::path, f -> + if ((is_matching_local (orconstr ()) or_oper) or + (is_matching_local (sumboolconstr ()) or_oper) or + (is_matching_local (sumconstr ()) or_oper)) + & (a = 1 or a = 2) then + let cont_term = if a = 1 then c1 else c2 in + let fst_cmd = Node(zz, (if a = 1 then "Left" else "Right"), + [Node(zz, "BINDINGS",[])]) in + let cont_cmd = f avoid clear_names false None + (kind_of_term cont_term) path in + Some(Node(zz, "TACTICLIST", + [fst_cmd;cont_cmd])) + else + None + | _ -> None;; + +let dummy_id = id_of_string "Dummy";; + +let (not_intro: pbp_rule) = function + avoid, clear_names, clear_flag, None, + IsApp(not_oper, [|c1|]), 2::1::path, f -> + if(is_matching_local (notconstr ()) not_oper) or + (is_matching_local (notTconstr ()) not_oper) then + let h' = next_global_ident_away (id_of_string "H") avoid in + let str_h' = (string_of_id h') in + Some(Node(zz,"TACTICLIST", + [Node(zz,"Reduce",[Node(zz,"REDEXP",[Node(zz,"Red",[])]); + Node(zz,"CLAUSE",[])]); + make_named_intro str_h'; + f (h'::avoid) clear_names false (Some str_h') + (kind_of_term c1) path])) + else + None + | _ -> None;; + + + +let elim_with_bindings hyp_name names = + Node(zz,"Elim", + [Node(zz, "COMMAND", [Nvar(zz,hyp_name)]); + Node(zz,"BINDINGS", + List.map + (function s -> + Node(zz,"BINDING", + [Nvar(zz,s); + Node + (zz,"COMMAND", + [Node + (zz,"APPLIST", + [Nvar(zz,"PBP_META"); + Nvar(zz, + "value_for_" ^ s)])])])) names)]);; + +let auxiliary_goals clear_names clear_flag this_name n_aux = + let clear_cmd = + make_clears (if clear_flag then (this_name ::clear_names) else clear_names) in + let rec clear_list = function + 0 -> [] + | n -> clear_cmd::(clear_list (n - 1)) in + clear_list n_aux;; + +(* This function is used to follow down a path, while staying on the spine of + successive products (universal quantifications or implications). + Arguments are the current observed constr object and the path that remains + to be followed, and an integer indicating how many products have already been + crossed. + Result is: + - a list of string indicating the names of universally quantified variables. + - a list of integers indicating the positions of the successive + universally quantified variables. + - an integer indicating the number of non-dependent products. + - the last constr object encountered during the walk down, and + - the remaining path. + + For instance the following session should happen: + let tt = raw_constr_of_com (Evd.mt_evd())(gLOB(initial_sign())) + (parse_com "(P:nat->Prop)(x:nat)(P x)->(P x)") in + down_prods (tt, [2;2;2], 0) + ---> ["P","x"],[0;1], 1, <<(P x)>>, [] +*) + + +let rec down_prods: (types, constr) kind_of_term * (int list) * int -> + string list * (int list) * int * (types, constr) kind_of_term * + (int list) = + function + IsProd(Name x, _, body), 2::path, k -> + let res_sl, res_il, res_i, res_cstr, res_p + = down_prods (kind_of_term body, path, k+1) in + (string_of_id x)::res_sl, (k::res_il), res_i, res_cstr, res_p + | IsProd(Anonymous, _, body), 2::path, k -> + let res_sl, res_il, res_i, res_cstr, res_p + = down_prods (kind_of_term body, path, k+1) in + res_sl, res_il, res_i+1, res_cstr, res_p + | cstr, path, _ -> [], [], 0, cstr, path;; + +exception Pbp_internal of int list;; + +(* This function should be usable to check that a type can be used by the + Apply command. Basically, c is supposed to be the head of some + type, where l gives the ranks of all universally quantified variables. + It check that these universally quantified variables occur in the head. + + The knowledge I have on constr structures is incomplete. +*) +let (check_apply: (types, constr) kind_of_term -> (int list) -> bool) = + function c -> function l -> + let rec delete n = function + | [] -> [] + | p::tl -> if n = p then tl else p::(delete n tl) in + let rec check_rec l = function + | IsApp(f, array) -> + Array.fold_left (fun l c -> check_rec l (kind_of_term c)) + (check_rec l (kind_of_term f)) array + | IsConst _ -> l + | IsMutInd _ -> l + | IsMutConstruct _ -> l + | IsVar _ -> l + | IsRel p -> + let result = delete p l in + if result = [] then + raise (Pbp_internal []) + else + result + | _ -> raise (Pbp_internal l) in + try + (check_rec l c) = [] + with Pbp_internal l -> l = [];; + +let (mk_db_indices: int list -> int -> int list) = + function int_list -> function nprems -> + let total = (List.length int_list) + nprems in + let rec mk_db_aux = function + [] -> [] + | a::l -> (total - a)::(mk_db_aux l) in + mk_db_aux int_list;; + + +(* This proof-by-pointing rule is quite complicated, as it attempts to foresee + usages of head tactics. A first operation is to follow the path as far + as possible while staying on the spine of products (function down_prods) + and then to check whether the next step will be an elim step. If the + answer is true, then the built command takes advantage of the power of + head tactics. *) + +let (head_tactic_patt: pbp_rule) = function + avoid, clear_names, clear_flag, Some h, cstr, path, f -> + (match down_prods (cstr, path, 0) with + | (str_list, _, nprems, + IsApp(oper,[|c1|]), 2::1::path) + when + (is_matching_local (notconstr ()) oper) or + (is_matching_local (notTconstr ()) oper) -> + Some(Node(zz, "TACTICLIST", + [elim_with_bindings h str_list; + f avoid clear_names false None (kind_of_term c1) path])) + | (str_list, _, nprems, + IsApp(oper, [|c1; c2|]), 2::a::path) + when ((is_matching_local (andconstr()) oper) or + (is_matching_local (prodconstr()) oper)) & (a = 1 or a = 2) -> + let h1 = next_global_ident_away (id_of_string "H") avoid in + let str_h1 = (string_of_id h1) in + let h2 = next_global_ident_away (id_of_string "H") (h1::avoid) in + let str_h2 = (string_of_id h2) in + Some(Node(zz,"TACTICLIST", + [elim_with_bindings h str_list; + make_named_intro str_h1; + make_named_intro str_h2; + let cont_body = + if a = 1 then c1 else c2 in + let cont_tac = + f (h2::h1::avoid) (h::clear_names) + false (Some (if 1 = a then str_h1 else str_h2)) + (kind_of_term cont_body) path in + if nprems = 0 then + cont_tac + else + Node(zz,"TACLIST", + cont_tac::(auxiliary_goals + clear_names clear_flag + h nprems))])) + | (str_list, _, nprems, IsApp(oper,[|c1; c2|]), 2::a::path) + when ((is_matching_local (exconstr ()) oper) or + (is_matching_local (exTconstr ()) oper) or + (is_matching_local (sigconstr ()) oper) or + (is_matching_local (sigTconstr()) oper)) & a = 2 -> + (match (kind_of_term c2),path with + IsLambda(Name x, _,body), (2::path) -> + Some(Node(zz,"TACTICLIST", + [elim_with_bindings h str_list; + let x' = next_global_ident_away x avoid in + let cont_body = + IsProd(Name x', c1, + mkProd(Anonymous, body, + mkVar(dummy_id))) in + let cont_tac + = f avoid (h::clear_names) false None + cont_body (2::1::path) in + if nprems = 0 then + cont_tac + else + Node(zz,"TACLIST", + cont_tac::(auxiliary_goals + clear_names clear_flag + h nprems))])) + | _ -> None) + | (str_list, _, nprems, IsApp(oper,[|c1; c2|]), 2::a::path) + when ((is_matching_local (orconstr ()) oper) or + (is_matching_local (sumboolconstr ()) oper) or + (is_matching_local (sumconstr ()) oper)) & + (a = 1 or a = 2) -> + Some(Node(zz, "TACTICLIST", + [elim_with_bindings h str_list; + let cont_body = + if a = 1 then c1 else c2 in + (* h' is the name for the new intro *) + let h' = next_global_ident_away (id_of_string "H") avoid in + let str_h' = (string_of_id h') in + let cont_tac = + Node(zz,"TACTICLIST", + [make_named_intro str_h'; + f + (* h' should not be used again *) + (h'::avoid) + (* the disjunct itself can be discarded *) + (h::clear_names) false (Some str_h') + (kind_of_term cont_body) path]) in + let snd_tac = + Node(zz, "TACTICLIST", + [make_named_intro str_h'; + make_clears (h::clear_names)]) in + let tacs1 = + if a = 1 then + [cont_tac; snd_tac] + else + [snd_tac; cont_tac] in + Node(zz,"TACLIST", + tacs1@(auxiliary_goals (h::clear_names) + false "dummy" nprems))])) + | (str_list, int_list, nprems, c, []) + when (check_apply c (mk_db_indices int_list nprems)) & + (match c with IsProd(_,_,_) -> false + | _ -> true) & + (List.length int_list) + nprems > 0 -> + Some(add_clear_names_if_necessary + (Node(zz,"Apply", [Node(zz,"COMMAND",[Nvar(zz, h)]); + Node(zz,"BINDINGS", [])])) + clear_names) + | _ -> None) + | _ -> None;; + + +let pbp_rules = ref [rem_cast;head_tactic_patt;forall_intro;imply_intro2; + forall_elim; imply_intro1; imply_elim1; imply_elim2; + and_intro; or_intro; not_intro; ex_intro];; + + +(* The tactic traced_try was intended to be used in tactics instead of + Try, with an argument Node(zz, "TACTIC", [b]) where b is the tactic to + try. However, the current design is not very robust to the fact that + Traced_Try may occur several times in the executed command! *) + +let try_trace = ref true;; + +let traced_try (f1:tactic) g = + try (try_trace := true; tclPROGRESS f1 g) + with e when Logic.catchable_exception e -> + (try_trace := false; tclIDTAC g);; + +let traced_try_entry = function + [Tacexp t] -> + traced_try (Tacinterp.interp t) + | _ -> failwith "traced_try_entry received wrong arguments";; + + +let rec clean_trace flag = + function + Node(a,"Traced_Try", [Node(_,_,[b])]) -> + if flag then b else Node(zz,"Idtac",[]) + | Node(a,b,c) -> Node(a,b,List.map (clean_trace flag) c) + | t -> t;; + +(* When the recursive descent along the path is over, one includes the + command requested by the point-and-shoot strategy. Default is + Try Assumption--Try Exact. *) + +let default_ast optname constr path = + match optname with + None -> Node(zz, "TRY", [Node(zz, "Assumption",[])]) + | Some(a) -> Node(zz, "TRY", + [Node(zz, "Exact",[Node(zz,"COMMAND",[Nvar(zz,a)])])]);; + +(* This is the main proof by pointing function. *) + +let rec pbpt final_cmd avoid clear_names clear_flag opt_name constr path = + let rec try_all_rules rl = + match rl with + f::tl -> + (match f (avoid, clear_names, clear_flag, + opt_name, constr, path, pbpt final_cmd) with + Some(ast) -> ast + | None -> try_all_rules tl) + | [] -> make_final_cmd final_cmd opt_name clear_names constr path + in try_all_rules (!pbp_rules);; + +(* these are the optimisation functions. *) +(* This function takes care of flattening successive intro commands. *) + +let rec optim1 = + function + Node(a,"TACTICLIST",b) -> + let tacs = List.map optim1 b in + let rec flatten = function + | [Node(a, "TACTICLIST", b')] -> + let rec last = function + [] -> failwith "function last is called on an empty list" + | [b] -> b + | a::b -> last b in + (match last b' with + Node(a, "TACLIST",_) -> [Node(a,"TACTICLIST", b')] + | _ -> flatten b') + | Node(a, "TACTICLIST", b')::others -> List.append (flatten b') + (flatten others) + | Node(a, "Idtac",[])::others -> (flatten others) + | [Node(a, "TACLIST",tacs)] -> + [Node(a, "TACLIST", List.map optim1 tacs)] + | t1::others -> t1::(flatten others) + | [] -> [] in + (match (flatten tacs) with + [] -> Node(zz,"Idtac", []) + | [t] -> t + | args -> Node(zz,"TACTICLIST", args)) + | t -> t;; + + +(* This optimization function takes care of compacting successive Intro commands + together. *) +let rec optim2 = + function + Node(a,"TACTICLIST",b) -> + let get_ids = + List.map (function Node(_,"IDENTIFIER", [Nvar(_,s)])->s + | Node(_,s,_) -> (failwith "unexpected node " ^ s) + | _ -> failwith "get_ids expected an identifier") in + let put_ids ids = + Node(zz,"Intros", + [Node(zz,"INTROPATTERN", + [Node(zz,"LISTPATTERN", + List.map + (function s -> Node(zz,"IDENTIFIER",[Nvar(zz,s)])) + ids)])]) in + let rec group_intros names = function + [] -> (match names with + [] -> [] + | l -> [put_ids l]) + | Node(_,"Intros", + [Node(_,"INTROPATTERN",[Node(_,"LISTPATTERN", ids)])])::others -> + group_intros (names@(get_ids ids)) others + | [Node(a,"TACLIST",b')] -> + [Node(a,"TACLIST", List.map optim2 b')] + | t1::others -> + (match names with + [] -> t1::(group_intros [] others) + | l -> (put_ids l)::t1::(group_intros [] others)) in + Node(a,"TACTICLIST",group_intros [] b) + | t -> t;; + +let rec merge_ast_in_command com1 com2 = + let args1 = + (match com1 with + Node(_, "APPLIST", args) -> args + | _ -> failwith "unexpected com1 in merge_ast_in_command") in + let args2 = + (match com2 with + Node(_, "APPLIST", hyp::args) -> args + | _ -> failwith "unexpected com2 in merge_ast_in_command") in + Node(zz, "COMMAND", [Node(zz, "APPLIST", args1@args2)]);; + +let cleanup_clears empty_allowed names str_list other = + let rec clean_aux = function + [] -> [] + | (Nvar(_,x) as fst_one)::tail -> + if List.mem x str_list then + clean_aux tail + else + fst_one::(clean_aux tail) + | _ -> failwith "unexpected argument in clean_aux" in + match clean_aux names with + [] -> (match other with + [] -> + if empty_allowed then + [] + else [Node(zz,"Idtac",[])] + | _ -> other) + | l -> Node(zz, "Clear", [Node(zz,"CLAUSE", l)])::other;; + + +(* This function takes care of compacting instanciations of universal + quantifications. *) +let rec optim3 str_list = function + Node(a,"TACTICLIST", b) -> + let rec optim3_aux empty_allowed str_list = function + ((Node(a, "Generalize", [Node(_, "COMMAND", [com1])])) as t1):: + intro:: + (Node(b, "Generalize", [Node(_, "COMMAND", [com2])]) as t2)::others -> + (match get_name_from_intro intro with + None -> t1::intro::(optim3_aux true str_list (t2::others)) + | 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 -> + cleanup_clears empty_allowed names str_list other + | [Node(a,"TACLIST",branches)] -> + [Node(a,"TACLIST",List.map (optim3 str_list) branches)] + | a::l -> a::(optim3_aux true str_list l) + | [] -> if empty_allowed then + [] + else failwith "strange value in optim3_aux" in + Node(a, "TACTICLIST", optim3_aux false str_list b) + | t -> t;; + +let optim x = optim3 [] (optim2 (optim1 x));; + +add_tactic "Traced_Try" traced_try_entry;; + +let rec tactic_args_to_ints = function + [] -> [] + | (Integer n)::l -> n::(tactic_args_to_ints l) + | _ -> failwith "expecting only numbers";; + + +let pbp_tac display_function = function + (Identifier a)::l -> + (function g -> + let str = (string_of_id a) in + let exp_ast = + pbpt default_ast (pf_ids_of_hyps g) + [] false (Some str) (kind_of_term (get_hyp_by_name g str)) + (tactic_args_to_ints l) in + (display_function (optim exp_ast); + tclIDTAC g)) + | ((Integer n)::_) as l -> + (function g -> + let exp_ast = + (pbpt default_ast (pf_ids_of_hyps g) [] false + None (kind_of_term (pf_concl g)) + (tactic_args_to_ints l)) in + (display_function (optim exp_ast); + tclIDTAC g)) + | [] -> (function g -> + (display_function (default_ast None (pf_concl g) []); + tclIDTAC g)) + | _ -> failwith "expecting other arguments";; diff --git a/contrib/interface/pbp.mli b/contrib/interface/pbp.mli new file mode 100644 index 000000000..649954019 --- /dev/null +++ b/contrib/interface/pbp.mli @@ -0,0 +1,4 @@ +val pbp_tac : (Coqast.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/translate.ml b/contrib/interface/translate.ml new file mode 100644 index 000000000..d40fee26a --- /dev/null +++ b/contrib/interface/translate.ml @@ -0,0 +1,160 @@ +open Names;; +open Sign;; +open Util;; +open Ast;; +open Term;; +open Pp;; +open Libobject;; +open Library;; +open Vernacinterp;; +(* dead code: open Proof_trees;; *) +open Termast;; +open Tacmach;; +open Pfedit;; +open Parsing;; +open Evd;; +open Evarutil;; + +open Xlate;; +open Coqast;; +open Vtp;; +open Ascent;; +open Environ;; +open Proof_type;; + +(* dead code: let rel_reference gt k oper = + if is_existential_oper oper then ope("XTRA", [str "ISEVAR"]) + else begin + let id = id_of_global oper in + let oper', _ = global_operator (Nametab.sp_of_id k id) id in + if oper = oper' then nvar (string_of_id id) + else failwith "xlate" +end;; +*) + +(* dead code: +let relativize relfun = + let rec relrec = + function + | Nvar (_, id) -> nvar id + | Slam (l, na, ast) -> Slam (l, na, relrec ast) + | Node (loc, nna, l) as ast -> begin + try relfun ast + with + | Failure _ -> Node (loc, nna, List.map relrec l) + end + | a -> a in + relrec;; +*) + +(* dead code: +let dbize_sp = + function + | Path (loc, sl, s) -> begin + try section_path sl s + with + | Invalid_argument _ | Failure _ -> + anomaly_loc + (loc, "Translate.dbize_sp (taken from Astterm)", + [< 'sTR "malformed section-path" >]) + end + | ast -> + anomaly_loc + (Ast.loc ast, "Translate.dbize_sp (taken from Astterm)", + [< 'sTR "not a section-path" >]);; +*) + +(* dead code: +let relativize_cci gt = relativize (function + | Node (_, "CONST", (p :: _)) as gt -> + rel_reference gt CCI (Const (dbize_sp p)) + | Node (_, "MUTIND", (p :: ((Num (_, tyi)) :: _))) as gt -> + rel_reference gt CCI (MutInd (dbize_sp p, tyi)) + | Node (_, "MUTCONSTRUCT", (p :: ((Num (_, tyi)) :: ((Num (_, i)) :: _)))) as gt -> + rel_reference gt CCI (MutConstruct ( + (dbize_sp p, tyi), i)) + | _ -> failwith "caught") gt;; +*) + +let coercion_description_holder = ref (function _ -> None : t -> int option);; + +let coercion_description t = !coercion_description_holder t;; + +let set_coercion_description f = + coercion_description_holder:=f; ();; + +let rec nth_tl l n = if n = 0 then l + else (match l with + | a :: b -> nth_tl b (n - 1) + | [] -> failwith "list too short for nth_tl");; + +let rec discard_coercions = + function + | Slam (l, na, ast) -> Slam (l, na, discard_coercions ast) + | Node (l, ("APPLIST" as nna), (f :: args as all_sons)) -> + (match coercion_description f with + | Some n -> + let new_args = + try nth_tl args n + with + | Failure "list too short for nth_tl" -> [] in + (match new_args with + | a :: (b :: c) -> Node (l, nna, List.map discard_coercions new_args) + | a :: [] -> discard_coercions a + | [] -> Node (l, nna, List.map discard_coercions all_sons)) + | None -> Node (l, nna, List.map discard_coercions all_sons)) + | Node (l, nna, all_sons) -> + Node (l, nna, List.map discard_coercions all_sons) + | it -> it;; + +(*translates a formula into a centaur-tree --> FORMULA *) +let translate_constr assumptions c = + let com = ast_of_constr true assumptions c in +(* dead code: let rcom = relativize_cci (discard_coercions com) in *) + xlate_formula com (* dead code: rcom *);; + +(*translates a named_context into a centaur-tree --> PREMISES_LIST *) +(* this code is inspired from printer.ml (function pr_named_context_of) *) +let translate_sign env = + let l = + fold_named_context + (fun env (id,v,c) l -> + (CT_premise(CT_ident(string_of_id id), translate_constr env c))::l) + env [] in + CT_premises_list l;; + +(* the function rev_and_compact performs two operations: + 1- it reverses the list of integers given as argument + 2- it replaces sequences of "1" by a negative number that is + the length of the sequence. *) +let rec rev_and_compact l = function + [] -> l + | 1::tl -> + (match l with + n::tl' -> + if n < 0 then + rev_and_compact ((n - 1)::tl') tl + else + rev_and_compact ((-1)::l) tl + | [] -> rev_and_compact [-1] tl) + | a::tl -> + if a < 0 then + (match l with + n::tl' -> + if n < 0 then + rev_and_compact ((n + a)::tl') tl + else + rev_and_compact (a::l) tl + | [] -> rev_and_compact (a::l) tl) + else + rev_and_compact (a::l) tl;; + +(*translates an int list into a centaur-tree --> SIGNED_INT_LIST *) +let translate_path l = + CT_signed_int_list + (List.map (function n -> CT_coerce_INT_to_SIGNED_INT (CT_int n)) + (rev_and_compact [] l));; + +(*translates a path and a goal into a centaur-tree --> RULE *) +let translate_goal (g:goal) = + CT_rule(translate_sign (evar_env g), translate_constr (evar_env g) g.evar_concl);; diff --git a/contrib/interface/translate.mli b/contrib/interface/translate.mli new file mode 100644 index 000000000..41c33d5a3 --- /dev/null +++ b/contrib/interface/translate.mli @@ -0,0 +1,8 @@ +open Ascent;; +open Evd;; +open Proof_type;; +open Environ;; +open Term;; + +val translate_goal : goal -> ct_RULE;; +val translate_constr : env -> constr -> ct_FORMULA;; diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml new file mode 100644 index 000000000..79d4d68ad --- /dev/null +++ b/contrib/interface/vtp.ml @@ -0,0 +1,1282 @@ +open Ascent;; + +let fNODE s n = + print_string "n\n"; + print_string ("vernac$" ^ s); + print_string "\n"; + print_int n; + print_string "\n";; + +let fATOM s1 = + print_string "a\n"; + print_string ("vernac$" ^ s1); + print_string "\n";; + +let f_atom_string = print_string;; +let f_atom_int = print_int;; +let rec fASSOC = function +| CT_coerce_NONE_to_ASSOC x -> fNONE x +| CT_lefta -> fNODE "lefta" 0 +| CT_nona -> fNODE "nona" 0 +| CT_righta -> fNODE "righta" 0 +and fAST = function +| CT_coerce_ID_OR_INT_to_AST x -> fID_OR_INT x +| CT_coerce_ID_OR_STRING_to_AST x -> fID_OR_STRING x +| CT_astnode(x1, x2) -> + fID x1; + fAST_LIST x2; + fNODE "astnode" 2 +| CT_astpath(x1, x2) -> + fID_LIST x1; + fID x2; + fNODE "astpath" 2 +| CT_astslam(x1, x2) -> + fID_OPT x1; + fAST x2; + fNODE "astslam" 2 +and fAST_LIST = function +| CT_ast_list l -> + (List.iter fAST l); + fNODE "ast_list" (List.length l) +and fBINARY = function +| CT_binary x -> fATOM "binary"; + (f_atom_int x); + print_string "\n"and fBINDER = function +| CT_binder(x1, x2) -> + fID_OPT_NE_LIST x1; + fFORMULA x2; + fNODE "binder" 2 +and fBINDER_LIST = function +| CT_binder_list l -> + (List.iter fBINDER l); + fNODE "binder_list" (List.length l) +and fBINDER_NE_LIST = function +| CT_binder_ne_list(x,l) -> + fBINDER x; + (List.iter fBINDER l); + fNODE "binder_ne_list" (1 + (List.length l)) +and fBINDING = function +| CT_binding(x1, x2) -> + fID_OR_INT x1; + fFORMULA x2; + fNODE "binding" 2 +and fBINDING_LIST = function +| CT_binding_list l -> + (List.iter fBINDING l); + fNODE "binding_list" (List.length l) +and fBOOL = function +| CT_false -> fNODE "false" 0 +| CT_true -> fNODE "true" 0 +and fCASE = function +| CT_case x -> fATOM "case"; + (f_atom_string x); + print_string "\n"and fCOERCION_OPT = function +| CT_coerce_NONE_to_COERCION_OPT x -> fNONE x +| CT_coercion_atm -> fNODE "coercion_atm" 0 +and fCOFIXTAC = function +| CT_cofixtac(x1, x2) -> + fID x1; + fFORMULA x2; + fNODE "cofixtac" 2 +and fCOFIX_REC = function +| CT_cofix_rec(x1, x2, x3) -> + fID x1; + fFORMULA x2; + fFORMULA x3; + fNODE "cofix_rec" 3 +and fCOFIX_REC_LIST = function +| CT_cofix_rec_list(x,l) -> + fCOFIX_REC x; + (List.iter fCOFIX_REC l); + fNODE "cofix_rec_list" (1 + (List.length l)) +and fCOFIX_TAC_LIST = function +| CT_cofix_tac_list l -> + (List.iter fCOFIXTAC l); + fNODE "cofix_tac_list" (List.length l) +and fCOMMAND = function +| CT_coerce_COMMAND_LIST_to_COMMAND x -> fCOMMAND_LIST x +| CT_coerce_EVAL_CMD_to_COMMAND x -> fEVAL_CMD x +| CT_coerce_IMPEXP_to_COMMAND x -> fIMPEXP x +| CT_coerce_SECTION_BEGIN_to_COMMAND x -> fSECTION_BEGIN x +| CT_coerce_THEOREM_GOAL_to_COMMAND x -> fTHEOREM_GOAL x +| CT_abort(x1) -> + fID_OPT_OR_ALL x1; + fNODE "abort" 1 +| CT_abstraction(x1, x2, x3) -> + fID x1; + fFORMULA x2; + fINT_LIST x3; + fNODE "abstraction" 3 +| CT_add_natural_feature(x1, x2) -> + fNATURAL_FEATURE x1; + fID x2; + fNODE "add_natural_feature" 2 +| CT_addpath(x1) -> + fSTRING x1; + fNODE "addpath" 1 +| CT_cd(x1) -> + fSTRING_OPT x1; + fNODE "cd" 1 +| CT_check(x1) -> + fFORMULA x1; + fNODE "check" 1 +| CT_class(x1) -> + fID x1; + fNODE "class" 1 +| CT_coercion(x1, x2, x3, x4, x5) -> + fLOCAL_OPT x1; + fIDENTITY_OPT x2; + fID x3; + fID x4; + fID x5; + fNODE "coercion" 5 +| CT_cofix_decl(x1) -> + fCOFIX_REC_LIST x1; + fNODE "cofix_decl" 1 +| CT_compile_module(x1, x2, x3) -> + fVERBOSE_OPT x1; + fID x2; + fSTRING_OPT x3; + fNODE "compile_module" 3 +| CT_definition(x1, x2, x3, x4) -> + fDEFN x1; + fID x2; + fDEF_BODY x3; + fFORMULA_OPT x4; + fNODE "definition" 4 +| CT_delpath(x1) -> + fSTRING x1; + fNODE "delpath" 1 +| CT_derive_depinversion(x1, x2, x3, x4) -> + fINV_TYPE x1; + fID x2; + fFORMULA x3; + fSORT_TYPE x4; + fNODE "derive_depinversion" 4 +| CT_derive_inversion(x1, x2, x3, x4) -> + fINV_TYPE x1; + fINT_OPT x2; + fID x3; + fID x4; + fNODE "derive_inversion" 4 +| CT_derive_inversion_with(x1, x2, x3, x4) -> + fINV_TYPE x1; + fID x2; + fFORMULA x3; + fSORT_TYPE x4; + fNODE "derive_inversion_with" 4 +| CT_explain_proof(x1) -> + fINT_LIST x1; + fNODE "explain_proof" 1 +| CT_explain_prooftree(x1) -> + fINT_LIST x1; + fNODE "explain_prooftree" 1 +| CT_fix_decl(x1) -> + fFIX_REC_LIST x1; + fNODE "fix_decl" 1 +| CT_focus(x1) -> + fINT_OPT x1; + fNODE "focus" 1 +| CT_go(x1) -> + fINT_OR_LOCN x1; + fNODE "go" 1 +| CT_guarded -> fNODE "guarded" 0 +| CT_hint(x1, x2, x3) -> + fID x1; + fID_LIST x2; + fHINT_EXPRESSION x3; + fNODE "hint" 3 +| CT_hintrewrite(x1, x2, x3, x4) -> + fORIENTATION x1; + fFORMULA_NE_LIST x2; + fID x3; + fTACTIC_COM x4; + fNODE "hintrewrite" 4 +| CT_hints(x1, x2, x3) -> + fID x1; + fID_NE_LIST x2; + fID_LIST x3; + fNODE "hints" 3 +| CT_ind_scheme(x1) -> + fSCHEME_SPEC_LIST x1; + fNODE "ind_scheme" 1 +| CT_infix(x1, x2, x3, x4) -> + fASSOC x1; + fINT x2; + fSTRING x3; + fID x4; + fNODE "infix" 4 +| CT_inspect(x1) -> + fINT x1; + fNODE "inspect" 1 +| CT_kill_node(x1) -> + fINT x1; + fNODE "kill_node" 1 +| CT_load(x1, x2) -> + fVERBOSE_OPT x1; + fID_OR_STRING x2; + fNODE "load" 2 +| CT_mind_decl(x1, x2) -> + fCO_IND x1; + fIND_SPEC_LIST x2; + fNODE "mind_decl" 2 +| CT_ml_add_path(x1) -> + fSTRING x1; + fNODE "ml_add_path" 1 +| CT_ml_declare_modules(x1) -> + fSTRING_NE_LIST x1; + fNODE "ml_declare_modules" 1 +| CT_ml_print_modules -> fNODE "ml_print_modules" 0 +| CT_ml_print_path -> fNODE "ml_print_path" 0 +| CT_module(x1) -> + fID x1; + fNODE "module" 1 +| CT_omega_flag(x1, x2) -> + fOMEGA_MODE x1; + fOMEGA_FEATURE x2; + fNODE "omega_flag" 2 +| CT_opaque(x1) -> + fID_NE_LIST x1; + fNODE "opaque" 1 +| CT_parameter(x1) -> + fBINDER x1; + fNODE "parameter" 1 +| CT_print_all -> fNODE "print_all" 0 +| CT_print_classes -> fNODE "print_classes" 0 +| CT_print_coercions -> fNODE "print_coercions" 0 +| CT_print_grammar(x1) -> + fGRAMMAR x1; + fNODE "print_grammar" 1 +| CT_print_graph -> fNODE "print_graph" 0 +| CT_print_hint(x1) -> + fID_OPT x1; + fNODE "print_hint" 1 +| CT_print_hintdb(x1) -> + fID x1; + fNODE "print_hintdb" 1 +| CT_print_id(x1) -> + fID x1; + fNODE "print_id" 1 +| CT_print_loadpath -> fNODE "print_loadpath" 0 +| CT_print_modules -> fNODE "print_modules" 0 +| CT_print_natural(x1) -> + fID x1; + fNODE "print_natural" 1 +| CT_print_natural_feature(x1) -> + fNATURAL_FEATURE x1; + fNODE "print_natural_feature" 1 +| CT_print_opaqueid(x1) -> + fID x1; + fNODE "print_opaqueid" 1 +| CT_print_path(x1, x2) -> + fID x1; + fID x2; + fNODE "print_path" 2 +| CT_print_proof(x1) -> + fID x1; + fNODE "print_proof" 1 +| CT_print_section(x1) -> + fID x1; + fNODE "print_section" 1 +| CT_print_states -> fNODE "print_states" 0 +| CT_proof(x1) -> + fFORMULA x1; + fNODE "proof" 1 +| CT_proof_no_op -> fNODE "proof_no_op" 0 +| CT_pwd -> fNODE "pwd" 0 +| CT_quit -> fNODE "quit" 0 +| CT_read_module(x1) -> + fID x1; + fNODE "read_module" 1 +| CT_rec_ml_add_path(x1) -> + fSTRING x1; + fNODE "rec_ml_add_path" 1 +| CT_rec_tactic_definition(x1) -> + fREC_TACTIC_FUN_LIST x1; + fNODE "rec_tactic_definition" 1 +| CT_recaddpath(x1) -> + fSTRING x1; + fNODE "recaddpath" 1 +| CT_record(x1, x2, x3, x4, x5, x6) -> + fCOERCION_OPT x1; + fID x2; + fBINDER_LIST x3; + fSORT_TYPE x4; + fID_OPT x5; + fRECCONSTR_LIST x6; + fNODE "record" 6 +| CT_remove_natural_feature(x1, x2) -> + fNATURAL_FEATURE x1; + fID x2; + fNODE "remove_natural_feature" 2 +| CT_require(x1, x2, x3, x4) -> + fIMPEXP x1; + fSPEC_OPT x2; + fID x3; + fSTRING_OPT x4; + fNODE "require" 4 +| CT_reset(x1) -> + fID x1; + fNODE "reset" 1 +| CT_reset_section(x1) -> + fID x1; + fNODE "reset_section" 1 +| CT_restart -> fNODE "restart" 0 +| CT_restore_state(x1) -> + fID x1; + fNODE "restore_state" 1 +| CT_resume(x1) -> + fID_OPT x1; + fNODE "resume" 1 +| CT_save(x1, x2) -> + fTHM_OPT x1; + fID_OPT x2; + fNODE "save" 2 +| CT_search(x1, x2) -> + fID x1; + fIN_OR_OUT_MODULES x2; + fNODE "search" 2 +| CT_section_end(x1) -> + fID x1; + fNODE "section_end" 1 +| CT_section_struct(x1, x2, x3) -> + fSECTION_BEGIN x1; + fSECTION_BODY x2; + fCOMMAND x3; + fNODE "section_struct" 3 +| CT_set_natural(x1) -> + fID x1; + fNODE "set_natural" 1 +| CT_set_natural_default -> fNODE "set_natural_default" 0 +| CT_sethyp(x1) -> + fINT x1; + fNODE "sethyp" 1 +| CT_setundo(x1) -> + fINT x1; + fNODE "setundo" 1 +| CT_show_goal(x1) -> + fINT_OPT x1; + fNODE "show_goal" 1 +| CT_show_implicits -> fNODE "show_implicits" 0 +| CT_show_node -> fNODE "show_node" 0 +| CT_show_proof -> fNODE "show_proof" 0 +| CT_show_proofs -> fNODE "show_proofs" 0 +| CT_show_script -> fNODE "show_script" 0 +| CT_show_tree -> fNODE "show_tree" 0 +| CT_solve(x1, x2) -> + fINT x1; + fTACTIC_COM x2; + fNODE "solve" 2 +| CT_suspend -> fNODE "suspend" 0 +| CT_syntax_macro(x1, x2, x3) -> + fID x1; + fFORMULA x2; + fINT_OPT x3; + fNODE "syntax_macro" 3 +| CT_tactic_definition(x1, x2, x3) -> + fID x1; + fID_LIST x2; + fTACTIC_COM x3; + fNODE "tactic_definition" 3 +| CT_test_natural_feature(x1, x2) -> + fNATURAL_FEATURE x1; + fID x2; + fNODE "test_natural_feature" 2 +| CT_theorem_struct(x1, x2) -> + fTHEOREM_GOAL x1; + fPROOF_SCRIPT x2; + fNODE "theorem_struct" 2 +| CT_token(x1) -> + fSTRING x1; + fNODE "token" 1 +| CT_transparent(x1) -> + fID_NE_LIST x1; + fNODE "transparent" 1 +| CT_undo(x1) -> + fINT_OPT x1; + fNODE "undo" 1 +| CT_unfocus -> fNODE "unfocus" 0 +| CT_unsethyp -> fNODE "unsethyp" 0 +| CT_unsetundo -> fNODE "unsetundo" 0 +| CT_user_vernac(x1, x2) -> + fID x1; + fVARG_LIST x2; + fNODE "user_vernac" 2 +| CT_variable(x1, x2) -> + fVAR x1; + fBINDER_LIST x2; + fNODE "variable" 2 +| CT_write_module(x1, x2) -> + fID x1; + fSTRING_OPT x2; + fNODE "write_module" 2 +and fCOMMAND_LIST = function +| CT_command_list(x,l) -> + fCOMMAND x; + (List.iter fCOMMAND l); + fNODE "command_list" (1 + (List.length l)) +and fCOMMENT = function +| CT_comment x -> fATOM "comment"; + (f_atom_string x); + print_string "\n"and fCOMMENT_S = function +| CT_comment_s l -> + (List.iter fCOMMENT l); + fNODE "comment_s" (List.length l) +and fCONSTR = function +| CT_constr(x1, x2) -> + fID x1; + fFORMULA x2; + fNODE "constr" 2 +and fCONSTR_LIST = function +| CT_constr_list l -> + (List.iter fCONSTR l); + fNODE "constr_list" (List.length l) +and fCONTEXT_HYP_LIST = function +| CT_context_hyp_list l -> + (List.iter fPREMISE_PATTERN l); + fNODE "context_hyp_list" (List.length l) +and fCONTEXT_PATTERN = function +| CT_coerce_FORMULA_to_CONTEXT_PATTERN x -> fFORMULA x +| CT_context(x1, x2) -> + fID_OPT x1; + fFORMULA x2; + fNODE "context" 2 +and fCONTEXT_RULE = function +| CT_context_rule(x1, x2, x3) -> + fCONTEXT_HYP_LIST x1; + fCONTEXT_PATTERN x2; + fTACTIC_COM x3; + fNODE "context_rule" 3 +and fCONVERSION_FLAG = function +| CT_beta -> fNODE "beta" 0 +| CT_delta -> fNODE "delta" 0 +| CT_iota -> fNODE "iota" 0 +and fCONVERSION_FLAG_LIST = function +| CT_conversion_flag_list l -> + (List.iter fCONVERSION_FLAG l); + fNODE "conversion_flag_list" (List.length l) +and fCONV_SET = function +| CT_unf l -> + (List.iter fID l); + fNODE "unf" (List.length l) +| CT_unfbut l -> + (List.iter fID l); + fNODE "unfbut" (List.length l) +and fCO_IND = function +| CT_co_ind x -> fATOM "co_ind"; + (f_atom_string x); + print_string "\n"and fDEFN = function +| CT_defn x -> fATOM "defn"; + (f_atom_string x); + print_string "\n"and fDEFN_OR_THM = 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_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); + print_string "\n"and fDESTRUCTING = function +| CT_coerce_NONE_to_DESTRUCTING x -> fNONE x +| CT_destructing -> fNODE "destructing" 0 +and fEQN = function +| CT_eqn(x1, x2) -> + fMATCH_PATTERN_NE_LIST x1; + fFORMULA x2; + fNODE "eqn" 2 +and fEQN_LIST = function +| CT_eqn_list l -> + (List.iter fEQN l); + fNODE "eqn_list" (List.length l) +and fEVAL_CMD = function +| CT_eval(x1, x2, x3) -> + fINT_OPT x1; + fRED_COM x2; + fFORMULA x3; + fNODE "eval" 3 +and fFIXTAC = function +| CT_fixtac(x1, x2, x3) -> + fID x1; + fINT x2; + fFORMULA x3; + fNODE "fixtac" 3 +and fFIX_BINDER = function +| CT_coerce_FIX_REC_to_FIX_BINDER x -> fFIX_REC x +| CT_fix_binder(x1, x2, x3, x4) -> + fID x1; + fINT x2; + fFORMULA x3; + fFORMULA x4; + fNODE "fix_binder" 4 +and fFIX_BINDER_LIST = function +| CT_fix_binder_list(x,l) -> + fFIX_BINDER x; + (List.iter fFIX_BINDER l); + fNODE "fix_binder_list" (1 + (List.length l)) +and fFIX_REC = function +| CT_fix_rec(x1, x2, x3, x4) -> + fID x1; + fBINDER_NE_LIST x2; + fFORMULA x3; + fFORMULA x4; + fNODE "fix_rec" 4 +and fFIX_REC_LIST = function +| CT_fix_rec_list(x,l) -> + fFIX_REC x; + (List.iter fFIX_REC l); + fNODE "fix_rec_list" (1 + (List.length l)) +and fFIX_TAC_LIST = function +| CT_fix_tac_list l -> + (List.iter fFIXTAC l); + fNODE "fix_tac_list" (List.length l) +and fFORMULA = function +| CT_coerce_BINARY_to_FORMULA x -> fBINARY x +| CT_coerce_ID_to_FORMULA x -> fID x +| CT_coerce_SORT_TYPE_to_FORMULA x -> fSORT_TYPE x +| CT_coerce_TYPED_FORMULA_to_FORMULA x -> fTYPED_FORMULA x +| CT_appc(x1, x2) -> + fFORMULA x1; + fFORMULA_NE_LIST x2; + fNODE "appc" 2 +| CT_arrowc(x1, x2) -> + fFORMULA x1; + fFORMULA x2; + fNODE "arrowc" 2 +| CT_bang(x1, x2) -> + fINT_OPT x1; + fFORMULA x2; + fNODE "bang" 2 +| CT_cases(x1, x2, x3) -> + fFORMULA_OPT x1; + fFORMULA_NE_LIST x2; + fEQN_LIST x3; + fNODE "cases" 3 +| CT_cofixc(x1, x2) -> + fID x1; + fCOFIX_REC_LIST x2; + fNODE "cofixc" 2 +| CT_elimc(x1, x2, x3, x4) -> + fCASE x1; + fFORMULA x2; + fFORMULA x3; + fFORMULA_LIST x4; + fNODE "elimc" 4 +| CT_existvarc -> fNODE "existvarc" 0 +| CT_fixc(x1, x2) -> + fID x1; + fFIX_BINDER_LIST x2; + fNODE "fixc" 2 +| CT_incomplete_binary(x1, x2) -> + fFORMULA x1; + fBINARY x2; + fNODE "incomplete_binary" 2 +| CT_int_encapsulator(x1) -> + fINT x1; + fNODE "int_encapsulator" 1 +| CT_lambdac(x1, x2) -> + fBINDER x1; + fFORMULA x2; + fNODE "lambdac" 2 +| CT_letin(x1, x2, x3) -> + fID x1; + fFORMULA x2; + fFORMULA x3; + fNODE "letin" 3 +| CT_metac(x1) -> + fINT x1; + fNODE "metac" 1 +| CT_prodc(x1, x2) -> + fBINDER x1; + fFORMULA x2; + fNODE "prodc" 2 +and fFORMULA_LIST = function +| CT_formula_list l -> + (List.iter fFORMULA l); + fNODE "formula_list" (List.length l) +and fFORMULA_NE_LIST = function +| CT_formula_ne_list(x,l) -> + fFORMULA x; + (List.iter fFORMULA l); + fNODE "formula_ne_list" (1 + (List.length l)) +and fFORMULA_OPT = function +| CT_coerce_FORMULA_to_FORMULA_OPT x -> fFORMULA x +| CT_coerce_ID_OPT_to_FORMULA_OPT x -> fID_OPT x +and fGRAMMAR = function +| CT_grammar_none -> fNODE "grammar_none" 0 +and fHINT_EXPRESSION = function +| CT_constructors(x1) -> + fID x1; + fNODE "constructors" 1 +| CT_extern(x1, x2, x3) -> + fINT x1; + fFORMULA x2; + fTACTIC_COM x3; + fNODE "extern" 3 +| CT_immediate(x1) -> + fFORMULA x1; + fNODE "immediate" 1 +| CT_resolve(x1) -> + fFORMULA x1; + fNODE "resolve" 1 +| CT_unfold_hint(x1) -> + fID x1; + fNODE "unfold_hint" 1 +and fID = function +| CT_ident x -> fATOM "ident"; + (f_atom_string x); + print_string "\n"and fIDENTITY_OPT = function +| CT_coerce_NONE_to_IDENTITY_OPT x -> fNONE x +| CT_identity -> fNODE "identity" 0 +and fID_LIST = function +| CT_id_list l -> + (List.iter fID l); + fNODE "id_list" (List.length l) +and fID_NE_LIST = function +| CT_id_ne_list(x,l) -> + fID x; + (List.iter fID l); + fNODE "id_ne_list" (1 + (List.length l)) +and fID_NE_LIST_OR_STAR = function +| CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR x -> fID_NE_LIST x +| CT_star -> fNODE "star" 0 +and fID_OPT = function +| CT_coerce_ID_to_ID_OPT x -> fID x +| CT_coerce_NONE_to_ID_OPT x -> fNONE x +and fID_OPT_NE_LIST = function +| CT_id_opt_ne_list(x,l) -> + fID_OPT x; + (List.iter fID_OPT l); + fNODE "id_opt_ne_list" (1 + (List.length l)) +and fID_OPT_OR_ALL = function +| CT_coerce_ID_OPT_to_ID_OPT_OR_ALL x -> fID_OPT x +| CT_all -> fNODE "all" 0 +and fID_OR_INT = function +| CT_coerce_ID_to_ID_OR_INT x -> fID x +| CT_coerce_INT_to_ID_OR_INT x -> fINT x +and fID_OR_STRING = function +| CT_coerce_ID_to_ID_OR_STRING x -> fID x +| CT_coerce_STRING_to_ID_OR_STRING x -> fSTRING x +and fID_UNIT = function +| CT_coerce_ID_to_ID_UNIT x -> fID x +| CT_unit -> fNODE "unit" 0 +and fID_UNIT_LIST = function +| CT_id_unit_list(x,l) -> + fID_UNIT x; + (List.iter fID_UNIT l); + fNODE "id_unit_list" (1 + (List.length l)) +and fIMPEXP = function +| CT_export -> fNODE "export" 0 +| CT_import -> fNODE "import" 0 +and fIND_SPEC = function +| CT_ind_spec(x1, x2, x3, x4) -> + fID x1; + fBINDER_LIST x2; + fFORMULA x3; + fCONSTR_LIST x4; + fNODE "ind_spec" 4 +and fIND_SPEC_LIST = function +| CT_ind_spec_list l -> + (List.iter fIND_SPEC l); + fNODE "ind_spec_list" (List.length l) +and fINT = function +| CT_int x -> fATOM "int"; + (f_atom_int x); + print_string "\n"and fINTRO_PATT = function +| CT_coerce_ID_to_INTRO_PATT x -> fID x +| CT_conj_pattern(x1) -> + fINTRO_PATT_LIST x1; + fNODE "conj_pattern" 1 +| CT_disj_pattern(x1) -> + fINTRO_PATT_LIST x1; + fNODE "disj_pattern" 1 +and fINTRO_PATT_LIST = function +| CT_intro_patt_list l -> + (List.iter fINTRO_PATT l); + fNODE "intro_patt_list" (List.length l) +and fINT_LIST = function +| CT_int_list l -> + (List.iter fINT l); + fNODE "int_list" (List.length l) +and fINT_NE_LIST = function +| CT_int_ne_list(x,l) -> + fINT x; + (List.iter fINT l); + fNODE "int_ne_list" (1 + (List.length l)) +and fINT_OPT = function +| CT_coerce_INT_to_INT_OPT x -> fINT x +| CT_coerce_NONE_to_INT_OPT x -> fNONE x +and fINT_OR_LOCN = function +| CT_coerce_INT_to_INT_OR_LOCN x -> fINT x +| CT_coerce_LOCN_to_INT_OR_LOCN x -> fLOCN x +and fINV_TYPE = function +| CT_inv_clear -> fNODE "inv_clear" 0 +| CT_inv_regular -> fNODE "inv_regular" 0 +| CT_inv_simple -> fNODE "inv_simple" 0 +and fIN_OR_OUT_MODULES = function +| CT_coerce_NONE_to_IN_OR_OUT_MODULES x -> fNONE x +| CT_in_modules(x1) -> + fID_NE_LIST x1; + fNODE "in_modules" 1 +| CT_out_modules(x1) -> + fID_NE_LIST x1; + fNODE "out_modules" 1 +and fLOCAL_OPT = function +| CT_coerce_NONE_to_LOCAL_OPT x -> fNONE x +| CT_local -> fNODE "local" 0 +and fLOCN = function +| CT_locn x -> fATOM "locn"; + (f_atom_string x); + print_string "\n"and fMATCH_PATTERN = function +| CT_coerce_ID_OPT_to_MATCH_PATTERN x -> fID_OPT x +| CT_pattern_app(x1, x2) -> + fMATCH_PATTERN x1; + fMATCH_PATTERN_NE_LIST x2; + fNODE "pattern_app" 2 +| CT_pattern_as(x1, x2) -> + fMATCH_PATTERN x1; + fID_OPT x2; + fNODE "pattern_as" 2 +and fMATCH_PATTERN_NE_LIST = function +| CT_match_pattern_ne_list(x,l) -> + fMATCH_PATTERN x; + (List.iter fMATCH_PATTERN l); + fNODE "match_pattern_ne_list" (1 + (List.length l)) +and fNATURAL_FEATURE = function +| CT_contractible -> fNODE "contractible" 0 +| CT_implicit -> fNODE "implicit" 0 +| CT_nat_transparent -> fNODE "nat_transparent" 0 +and fNONE = function +| CT_none -> fNODE "none" 0 +and fOMEGA_FEATURE = function +| CT_coerce_STRING_to_OMEGA_FEATURE x -> fSTRING x +| CT_flag_action -> fNODE "flag_action" 0 +| CT_flag_system -> fNODE "flag_system" 0 +| CT_flag_time -> fNODE "flag_time" 0 +and fOMEGA_MODE = function +| CT_set -> fNODE "set" 0 +| CT_switch -> fNODE "switch" 0 +| CT_unset -> fNODE "unset" 0 +and fORIENTATION = function +| CT_lr -> fNODE "lr" 0 +| CT_rl -> fNODE "rl" 0 +and fPATTERN = function +| CT_pattern_occ(x1, x2) -> + fINT_LIST x1; + fFORMULA x2; + fNODE "pattern_occ" 2 +and fPATTERN_NE_LIST = function +| CT_pattern_ne_list(x,l) -> + fPATTERN x; + (List.iter fPATTERN l); + fNODE "pattern_ne_list" (1 + (List.length l)) +and fPREMISE = function +| CT_coerce_TYPED_FORMULA_to_PREMISE x -> fTYPED_FORMULA x +| CT_eval_result(x1, x2, x3) -> + fFORMULA x1; + fFORMULA x2; + fFORMULA x3; + fNODE "eval_result" 3 +| CT_premise(x1, x2) -> + fID x1; + fFORMULA x2; + fNODE "premise" 2 +and fPREMISES_LIST = function +| CT_premises_list l -> + (List.iter fPREMISE l); + fNODE "premises_list" (List.length l) +and fPREMISE_PATTERN = function +| CT_premise_pattern(x1, x2) -> + fID_OPT x1; + fCONTEXT_PATTERN x2; + fNODE "premise_pattern" 2 +and fPROOF_SCRIPT = function +| CT_proof_script l -> + (List.iter fCOMMAND l); + fNODE "proof_script" (List.length l) +and fRECCONSTR = function +| CT_coerce_CONSTR_to_RECCONSTR x -> fCONSTR x +| CT_constr_coercion(x1, x2) -> + fID x1; + fFORMULA x2; + fNODE "constr_coercion" 2 +and fRECCONSTR_LIST = function +| CT_recconstr_list l -> + (List.iter fRECCONSTR l); + fNODE "recconstr_list" (List.length l) +and fREC_TACTIC_FUN = function +| CT_rec_tactic_fun(x1, x2, x3) -> + fID x1; + fID_UNIT_LIST x2; + fTACTIC_COM x3; + fNODE "rec_tactic_fun" 3 +and fREC_TACTIC_FUN_LIST = function +| CT_rec_tactic_fun_list(x,l) -> + fREC_TACTIC_FUN x; + (List.iter fREC_TACTIC_FUN l); + fNODE "rec_tactic_fun_list" (1 + (List.length l)) +and fRED_COM = function +| CT_cbv(x1, x2) -> + fCONVERSION_FLAG_LIST x1; + fCONV_SET x2; + fNODE "cbv" 2 +| CT_fold(x1) -> + fFORMULA_LIST x1; + fNODE "fold" 1 +| CT_hnf -> fNODE "hnf" 0 +| CT_lazy(x1, x2) -> + fCONVERSION_FLAG_LIST x1; + fCONV_SET x2; + fNODE "lazy" 2 +| CT_pattern(x1) -> + fPATTERN_NE_LIST x1; + fNODE "pattern" 1 +| CT_red -> fNODE "red" 0 +| CT_simpl -> fNODE "simpl" 0 +| CT_unfold(x1) -> + fUNFOLD_NE_LIST x1; + fNODE "unfold" 1 +and fRULE = function +| CT_rule(x1, x2) -> + fPREMISES_LIST x1; + fFORMULA x2; + fNODE "rule" 2 +and fRULE_LIST = function +| CT_rule_list l -> + (List.iter fRULE l); + fNODE "rule_list" (List.length l) +and fSCHEME_SPEC = function +| CT_scheme_spec(x1, x2, x3, x4) -> + fID x1; + fDEP x2; + fFORMULA x3; + fSORT_TYPE x4; + fNODE "scheme_spec" 4 +and fSCHEME_SPEC_LIST = function +| CT_scheme_spec_list(x,l) -> + fSCHEME_SPEC x; + (List.iter fSCHEME_SPEC l); + fNODE "scheme_spec_list" (1 + (List.length l)) +and fSECTION_BEGIN = function +| CT_section(x1) -> + fID x1; + fNODE "section" 1 +and fSECTION_BODY = function +| CT_section_body l -> + (List.iter fCOMMAND l); + fNODE "section_body" (List.length l) +and fSIGNED_INT = function +| CT_coerce_INT_to_SIGNED_INT x -> fINT x +| CT_minus(x1) -> + fINT x1; + fNODE "minus" 1 +and fSIGNED_INT_LIST = function +| CT_signed_int_list l -> + (List.iter fSIGNED_INT l); + fNODE "signed_int_list" (List.length l) +and fSORT_TYPE = function +| CT_sortc x -> fATOM "sortc"; + (f_atom_string x); + print_string "\n"and fSPEC_LIST = function +| CT_coerce_BINDING_LIST_to_SPEC_LIST x -> fBINDING_LIST x +| CT_coerce_FORMULA_LIST_to_SPEC_LIST x -> fFORMULA_LIST x +and fSPEC_OPT = function +| CT_coerce_NONE_to_SPEC_OPT x -> fNONE x +| CT_spec -> fNODE "spec" 0 +and fSTRING = function +| CT_string x -> fATOM "string"; + (f_atom_string x); + print_string "\n"and fSTRING_NE_LIST = function +| CT_string_ne_list(x,l) -> + fSTRING x; + (List.iter fSTRING l); + fNODE "string_ne_list" (1 + (List.length l)) +and fSTRING_OPT = function +| CT_coerce_NONE_to_STRING_OPT x -> fNONE x +| CT_coerce_STRING_to_STRING_OPT x -> fSTRING x +and fTACTIC_ARG = function +| CT_coerce_FORMULA_to_TACTIC_ARG x -> fFORMULA x +| CT_coerce_ID_OR_INT_to_TACTIC_ARG x -> fID_OR_INT x +| CT_coerce_TACTIC_COM_to_TACTIC_ARG x -> fTACTIC_COM x +| CT_void -> fNODE "void" 0 +and fTACTIC_ARG_LIST = function +| CT_tactic_arg_list(x,l) -> + fTACTIC_ARG x; + (List.iter fTACTIC_ARG l); + fNODE "tactic_arg_list" (1 + (List.length l)) +and fTACTIC_COM = function +| CT_abstract(x1, x2) -> + fID_OPT x1; + fTACTIC_COM x2; + fNODE "abstract" 2 +| CT_absurd(x1) -> + fFORMULA x1; + fNODE "absurd" 1 +| CT_apply(x1, x2) -> + fFORMULA x1; + fSPEC_LIST x2; + fNODE "apply" 2 +| CT_assumption -> fNODE "assumption" 0 +| CT_auto(x1) -> + fINT_OPT x1; + fNODE "auto" 1 +| CT_auto_with(x1, x2) -> + fINT_OPT x1; + fID_NE_LIST_OR_STAR x2; + fNODE "auto_with" 2 +| CT_autorewrite(x1, x2) -> + fID_NE_LIST x1; + fTACTIC_OPT x2; + fNODE "autorewrite" 2 +| CT_autotdb(x1) -> + fINT_OPT x1; + fNODE "autotdb" 1 +| CT_case_type(x1) -> + fFORMULA x1; + fNODE "case_type" 1 +| CT_casetac(x1, x2) -> + fFORMULA x1; + fSPEC_LIST x2; + fNODE "casetac" 2 +| CT_cdhyp(x1) -> + fID x1; + fNODE "cdhyp" 1 +| CT_change(x1, x2) -> + fFORMULA x1; + fID_LIST x2; + fNODE "change" 2 +| CT_clear(x1) -> + fID_NE_LIST x1; + fNODE "clear" 1 +| CT_cofixtactic(x1, x2) -> + fID_OPT x1; + fCOFIX_TAC_LIST x2; + fNODE "cofixtactic" 2 +| CT_condrewrite_lr(x1, x2, x3, x4) -> + fTACTIC_COM x1; + fFORMULA x2; + fSPEC_LIST x3; + fID_OPT x4; + fNODE "condrewrite_lr" 4 +| CT_condrewrite_rl(x1, x2, x3, x4) -> + fTACTIC_COM x1; + fFORMULA x2; + fSPEC_LIST x3; + fID_OPT x4; + fNODE "condrewrite_rl" 4 +| CT_constructor(x1, x2) -> + fINT x1; + fSPEC_LIST x2; + fNODE "constructor" 2 +| CT_contradiction -> fNODE "contradiction" 0 +| CT_cut(x1) -> + fFORMULA x1; + fNODE "cut" 1 +| CT_cutrewrite_lr(x1, x2) -> + fFORMULA x1; + fID_OPT x2; + fNODE "cutrewrite_lr" 2 +| CT_cutrewrite_rl(x1, x2) -> + fFORMULA x1; + fID_OPT x2; + fNODE "cutrewrite_rl" 2 +| CT_dconcl -> fNODE "dconcl" 0 +| CT_decompose_list(x1, x2) -> + fID_NE_LIST x1; + fFORMULA x2; + fNODE "decompose_list" 2 +| CT_depinversion(x1, x2, x3) -> + fINV_TYPE x1; + fID x2; + fFORMULA_OPT x3; + fNODE "depinversion" 3 +| CT_deprewrite_lr(x1) -> + fID x1; + fNODE "deprewrite_lr" 1 +| CT_deprewrite_rl(x1) -> + fID x1; + fNODE "deprewrite_rl" 1 +| CT_destruct(x1) -> + fID_OR_INT x1; + fNODE "destruct" 1 +| CT_dhyp(x1) -> + fID x1; + fNODE "dhyp" 1 +| CT_discriminate_eq(x1) -> + fID_OPT x1; + fNODE "discriminate_eq" 1 +| CT_do(x1, x2) -> + fINT x1; + fTACTIC_COM x2; + fNODE "do" 2 +| CT_eapply(x1, x2) -> + fFORMULA x1; + fSPEC_LIST x2; + fNODE "eapply" 2 +| CT_eauto(x1) -> + fINT_OPT x1; + fNODE "eauto" 1 +| CT_eauto_with(x1, x2) -> + fINT_OPT x1; + fID_NE_LIST_OR_STAR x2; + fNODE "eauto_with" 2 +| CT_elim(x1, x2, x3) -> + fFORMULA x1; + fSPEC_LIST x2; + fUSING x3; + fNODE "elim" 3 +| CT_elim_type(x1) -> + fFORMULA x1; + fNODE "elim_type" 1 +| CT_exact(x1) -> + fFORMULA x1; + fNODE "exact" 1 +| CT_exists(x1) -> + fSPEC_LIST x1; + fNODE "exists" 1 +| CT_fail -> fNODE "fail" 0 +| CT_first(x,l) -> + fTACTIC_COM x; + (List.iter fTACTIC_COM l); + fNODE "first" (1 + (List.length l)) +| CT_fixtactic(x1, x2, x3) -> + fID_OPT x1; + fINT x2; + fFIX_TAC_LIST x3; + fNODE "fixtactic" 3 +| CT_generalize(x1) -> + fFORMULA_NE_LIST x1; + fNODE "generalize" 1 +| CT_generalize_dependent(x1) -> + fFORMULA x1; + fNODE "generalize_dependent" 1 +| CT_idtac -> fNODE "idtac" 0 +| CT_induction(x1) -> + fID_OR_INT x1; + fNODE "induction" 1 +| CT_info(x1) -> + fTACTIC_COM x1; + fNODE "info" 1 +| CT_injection_eq(x1) -> + fID_OPT x1; + fNODE "injection_eq" 1 +| CT_intro(x1) -> + fID_OPT x1; + fNODE "intro" 1 +| CT_intro_after(x1, x2) -> + fID_OPT x1; + fID x2; + fNODE "intro_after" 2 +| CT_intros(x1) -> + fINTRO_PATT_LIST x1; + fNODE "intros" 1 +| CT_intros_until(x1) -> + fID x1; + fNODE "intros_until" 1 +| CT_inversion(x1, x2, x3) -> + fINV_TYPE x1; + fID x2; + fID_LIST x3; + fNODE "inversion" 3 +| 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_match_context(x,l) -> + fCONTEXT_RULE x; + (List.iter fCONTEXT_RULE l); + fNODE "match_context" (1 + (List.length l)) +| CT_move_after(x1, x2) -> + fID x1; + fID x2; + fNODE "move_after" 2 +| CT_omega -> fNODE "omega" 0 +| CT_orelse(x1, x2) -> + fTACTIC_COM x1; + fTACTIC_COM x2; + fNODE "orelse" 2 +| CT_parallel(x,l) -> + fTACTIC_COM x; + (List.iter fTACTIC_COM l); + fNODE "parallel" (1 + (List.length l)) +| CT_prolog(x1, x2) -> + fFORMULA_LIST x1; + fINT x2; + fNODE "prolog" 2 +| CT_rec_tactic_in(x1, x2) -> + fREC_TACTIC_FUN_LIST x1; + fTACTIC_COM x2; + fNODE "rec_tactic_in" 2 +| CT_reduce(x1, x2) -> + fRED_COM x1; + fID_LIST x2; + fNODE "reduce" 2 +| CT_reflexivity -> fNODE "reflexivity" 0 +| CT_repeat(x1) -> + fTACTIC_COM x1; + fNODE "repeat" 1 +| CT_replace_with(x1, x2) -> + fFORMULA x1; + fFORMULA x2; + fNODE "replace_with" 2 +| CT_rewrite_lr(x1, x2, x3) -> + fFORMULA x1; + fSPEC_LIST x2; + fID_OPT x3; + fNODE "rewrite_lr" 3 +| CT_rewrite_rl(x1, x2, x3) -> + fFORMULA x1; + fSPEC_LIST x2; + fID_OPT x3; + fNODE "rewrite_rl" 3 +| CT_right(x1) -> + fSPEC_LIST x1; + fNODE "right" 1 +| CT_simple_user_tac(x1, x2) -> + fID x1; + fTACTIC_ARG_LIST x2; + fNODE "simple_user_tac" 2 +| CT_simplify_eq(x1) -> + fID_OPT x1; + fNODE "simplify_eq" 1 +| CT_specialize(x1, x2, x3) -> + fINT_OPT x1; + fFORMULA x2; + fSPEC_LIST x3; + fNODE "specialize" 3 +| CT_split(x1) -> + fSPEC_LIST x1; + fNODE "split" 1 +| CT_superauto(x1, x2, x3, x4) -> + fINT_OPT x1; + fID_LIST x2; + fDESTRUCTING x3; + fUSINGTDB x4; + fNODE "superauto" 4 +| CT_symmetry -> fNODE "symmetry" 0 +| CT_tac_double(x1, x2) -> + fINT x1; + fINT x2; + fNODE "tac_double" 2 +| CT_tacsolve(x,l) -> + fTACTIC_COM x; + (List.iter fTACTIC_COM l); + fNODE "tacsolve" (1 + (List.length l)) +| CT_tactic_fun(x1, x2) -> + fID_UNIT_LIST x1; + fTACTIC_COM x2; + fNODE "tactic_fun" 2 +| CT_then(x,l) -> + fTACTIC_COM x; + (List.iter fTACTIC_COM l); + fNODE "then" (1 + (List.length l)) +| CT_transitivity(x1) -> + fFORMULA x1; + fNODE "transitivity" 1 +| CT_trivial -> fNODE "trivial" 0 +| CT_trivial_with(x1) -> + fID_NE_LIST_OR_STAR x1; + fNODE "trivial_with" 1 +| CT_try(x1) -> + fTACTIC_COM x1; + fNODE "try" 1 +| CT_use(x1) -> + fFORMULA x1; + fNODE "use" 1 +| CT_use_inversion(x1, x2, x3) -> + fID x1; + fFORMULA x2; + fID_LIST x3; + fNODE "use_inversion" 3 +| CT_user_tac(x1, x2) -> + fID x1; + fTARG_LIST x2; + fNODE "user_tac" 2 +and fTACTIC_OPT = function +| CT_coerce_NONE_to_TACTIC_OPT x -> fNONE x +| CT_coerce_TACTIC_COM_to_TACTIC_OPT x -> fTACTIC_COM x +and fTARG = function +| CT_coerce_BINDING_to_TARG x -> fBINDING x +| CT_coerce_COFIXTAC_to_TARG x -> fCOFIXTAC x +| CT_coerce_FIXTAC_to_TARG x -> fFIXTAC x +| CT_coerce_FORMULA_to_TARG x -> fFORMULA x +| CT_coerce_ID_OR_INT_to_TARG x -> fID_OR_INT x +| CT_coerce_ID_OR_STRING_to_TARG x -> fID_OR_STRING x +| CT_coerce_PATTERN_to_TARG x -> fPATTERN x +| CT_coerce_SIGNED_INT_LIST_to_TARG x -> fSIGNED_INT_LIST x +| CT_coerce_SPEC_LIST_to_TARG x -> fSPEC_LIST x +| CT_coerce_TACTIC_COM_to_TARG x -> fTACTIC_COM x +| CT_coerce_UNFOLD_to_TARG x -> fUNFOLD x +| CT_coerce_UNFOLD_NE_LIST_to_TARG x -> fUNFOLD_NE_LIST x +and fTARG_LIST = function +| CT_targ_list l -> + (List.iter fTARG l); + fNODE "targ_list" (List.length l) +and fTHEOREM_GOAL = function +| CT_goal(x1) -> + fFORMULA x1; + fNODE "goal" 1 +| CT_theorem_goal(x1, x2, x3) -> + fDEFN_OR_THM x1; + fID x2; + fFORMULA x3; + fNODE "theorem_goal" 3 +and fTHM = function +| CT_thm x -> fATOM "thm"; + (f_atom_string x); + print_string "\n"and fTHM_OPT = function +| CT_coerce_NONE_to_THM_OPT x -> fNONE x +| CT_coerce_THM_to_THM_OPT x -> fTHM x +and fTYPED_FORMULA = function +| CT_typed_formula(x1, x2) -> + fFORMULA x1; + fFORMULA x2; + fNODE "typed_formula" 2 +and fUNFOLD = function +| CT_unfold_occ(x1, x2) -> + fINT_LIST x1; + fID x2; + fNODE "unfold_occ" 2 +and fUNFOLD_NE_LIST = function +| CT_unfold_ne_list(x,l) -> + fUNFOLD x; + (List.iter fUNFOLD l); + fNODE "unfold_ne_list" (1 + (List.length l)) +and fUSING = function +| CT_coerce_NONE_to_USING x -> fNONE x +| CT_using(x1, x2) -> + fFORMULA x1; + fSPEC_LIST x2; + fNODE "using" 2 +and fUSINGTDB = function +| CT_coerce_NONE_to_USINGTDB x -> fNONE x +| CT_usingtdb -> fNODE "usingtdb" 0 +and fVAR = function +| CT_var x -> fATOM "var"; + (f_atom_string x); + print_string "\n"and fVARG = function +| CT_coerce_AST_to_VARG x -> fAST x +| CT_coerce_AST_LIST_to_VARG x -> fAST_LIST x +| CT_coerce_BINDER_to_VARG x -> fBINDER x +| CT_coerce_BINDER_LIST_to_VARG x -> fBINDER_LIST x +| CT_coerce_BINDER_NE_LIST_to_VARG x -> fBINDER_NE_LIST x +| CT_coerce_FORMULA_LIST_to_VARG x -> fFORMULA_LIST x +| CT_coerce_FORMULA_OPT_to_VARG x -> fFORMULA_OPT x +| CT_coerce_ID_OPT_OR_ALL_to_VARG x -> fID_OPT_OR_ALL x +| CT_coerce_INT_LIST_to_VARG x -> fINT_LIST x +| CT_coerce_INT_OPT_to_VARG x -> fINT_OPT x +| CT_coerce_STRING_OPT_to_VARG x -> fSTRING_OPT x +| CT_coerce_TACTIC_OPT_to_VARG x -> fTACTIC_OPT x +| CT_coerce_VARG_LIST_to_VARG x -> fVARG_LIST x +and fVARG_LIST = function +| CT_varg_list l -> + (List.iter fVARG l); + fNODE "varg_list" (List.length l) +and fVERBOSE_OPT = function +| CT_coerce_NONE_to_VERBOSE_OPT x -> fNONE x +| CT_verbose -> fNODE "verbose" 0 +;; diff --git a/contrib/interface/vtp.mli b/contrib/interface/vtp.mli new file mode 100644 index 000000000..6fe256ab2 --- /dev/null +++ b/contrib/interface/vtp.mli @@ -0,0 +1,14 @@ +open Ascent;; + +val fCOMMAND_LIST : ct_COMMAND_LIST -> unit;; +val fCOMMAND : ct_COMMAND -> unit;; +val fTACTIC_COM : ct_TACTIC_COM -> unit;; +val fFORMULA : ct_FORMULA -> unit;; +val fID : ct_ID -> unit;; +val fSTRING : ct_STRING -> unit;; +val fINT : ct_INT -> unit;; +val fRULE_LIST : ct_RULE_LIST -> unit;; +val fRULE : ct_RULE -> unit;; +val fSIGNED_INT_LIST : ct_SIGNED_INT_LIST -> unit;; +val fPREMISES_LIST : ct_PREMISES_LIST -> unit;; +val fID_LIST : ct_ID_LIST -> unit;; diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml new file mode 100644 index 000000000..8d4d952b5 --- /dev/null +++ b/contrib/interface/xlate.ml @@ -0,0 +1,2026 @@ + +(** Translation from coq abstract syntax trees to centaur vernac + *) +open String;; +open Char;; +open Util;; +open Ast;; +open Names;; +open Ascent;; +open Coqast;; + +let in_coq_ref = ref false;; + +let xlate_mut_stuff = ref ((fun _ -> + Nvar((0,0), "function xlate_mut_stuff should not be used here")): + Coqast.t -> Coqast.t);; + +let set_xlate_mut_stuff v = xlate_mut_stuff := v;; + +let declare_in_coq () = in_coq_ref:=true;; + +let in_coq () = !in_coq_ref;; + +(* // Verify whether this is dead code, as of coq version 7 *) +(* The following three sentences have been added to cope with a change +of strategy from the Coq team in the way rules construct ast's. The +problem is that now grammar rules will refer to identifiers by giving +their absolute name, using the mutconstruct when needed. Unfortunately, +when you have a mutconstruct structure, you don't have a way to guess +the corresponding identifier without an environment, and the parser +does not have an environment. We add one, only for the constructs +that are always loaded. *) +let type_table = ((Hashtbl.create 17) : + (string, ((string array) array)) Hashtbl.t);; + +Hashtbl.add type_table "Coq.Init.Logic.and" + [|[|"dummy";"conj"|]|];; + +Hashtbl.add type_table "Coq.Init.Datatypes.prod" + [|[|"dummy";"pair"|]|];; + +(*The following two codes are added to cope with the distinction + between ocaml and caml-light syntax while using ctcaml to + manipulate the program *) +let code_plus = code (get "+" 0);; + +let code_minus = code (get "-" 0);; + +let coercion_description_holder = ref (function _ -> None : t -> int option);; + +let coercion_description t = !coercion_description_holder t;; + +let set_coercion_description f = + coercion_description_holder:=f; ();; + +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);; + +type astrecurse = Rbinder of ct_ID_OPT * astrecurse + | Rform of ct_FORMULA + | Rform_list of ct_FORMULA list;; + +let ctf_STRING_OPT_NONE = CT_coerce_NONE_to_STRING_OPT CT_none;; + +let ctf_STRING_OPT_SOME s = CT_coerce_STRING_to_STRING_OPT s;; + +let ctv_ID_OPT_NONE = CT_coerce_NONE_to_ID_OPT CT_none;; + +let ctf_ID_OPT_SOME s = CT_coerce_ID_to_ID_OPT s;; + +let ctv_ID_OPT_OR_ALL_NONE = + CT_coerce_ID_OPT_to_ID_OPT_OR_ALL (CT_coerce_NONE_to_ID_OPT CT_none);; + +let ctv_FORMULA_OPT_NONE = + CT_coerce_ID_OPT_to_FORMULA_OPT(CT_coerce_NONE_to_ID_OPT CT_none);; + +let ctf_ID_OPT_OR_ALL_SOME s = + CT_coerce_ID_OPT_to_ID_OPT_OR_ALL (ctf_ID_OPT_SOME s);; + +let ctv_ID_OPT_OR_ALL_ALL = CT_all;; + +let ctv_SPEC_OPT_NONE = CT_coerce_NONE_to_SPEC_OPT CT_none;; + +let castc x = CT_coerce_TYPED_FORMULA_to_FORMULA x;; + +let varc x = CT_coerce_ID_to_FORMULA x;; + +let ident_tac s = CT_user_tac (CT_ident s, CT_targ_list []);; + +let ident_vernac s = CT_user_vernac (CT_ident s, CT_varg_list []);; + +type iTARG = Targ_command of ct_FORMULA + | Targ_intropatt of ct_INTRO_PATT_LIST + | Targ_id_list of ct_ID_LIST + | Targ_spec_list of ct_SPEC_LIST + | Targ_binding_com of ct_FORMULA + | Targ_ident of ct_ID + | Targ_int of ct_INT + | Targ_binding of ct_BINDING + | Targ_pattern of ct_PATTERN + | Targ_unfold of ct_UNFOLD + | Targ_unfold_ne_list of ct_UNFOLD_NE_LIST + | Targ_string of ct_STRING + | Targ_fixtac of ct_FIXTAC + | Targ_cofixtac of ct_COFIXTAC + | Targ_tacexp of ct_TACTIC_COM + | Targ_redexp of ct_RED_COM;; + +type iVARG = Varg_binder of ct_BINDER + | Varg_binderlist of ct_BINDER_LIST + | Varg_bindernelist of ct_BINDER_NE_LIST + | Varg_call of ct_ID * iVARG list + | Varg_constr of ct_FORMULA + | Varg_sorttype of ct_SORT_TYPE + | Varg_constrlist of ct_FORMULA list + | Varg_ident of ct_ID + | Varg_int of ct_INT + | Varg_intlist of ct_INT_LIST + | Varg_none + | Varg_string of ct_STRING + | Varg_tactic of ct_TACTIC_COM + | Varg_ast of ct_AST + | Varg_astlist of ct_AST_LIST + | Varg_tactic_arg of iTARG + | Varg_varglist of iVARG list;; + +let coerce_iTARG_to_TARG = + function + | Targ_intropatt x -> xlate_error "coerce_iTARG_to_TARG (3)" + | Targ_command x -> CT_coerce_FORMULA_to_TARG x + | Targ_id_list x -> xlate_error "coerce_iTARG_to_TARG" + | Targ_spec_list x -> CT_coerce_SPEC_LIST_to_TARG x + | Targ_binding_com x -> CT_coerce_FORMULA_to_TARG x + | Targ_ident x -> CT_coerce_ID_OR_INT_to_TARG (CT_coerce_ID_to_ID_OR_INT x) + | Targ_int x -> CT_coerce_ID_OR_INT_to_TARG (CT_coerce_INT_to_ID_OR_INT x) + | Targ_binding x -> CT_coerce_BINDING_to_TARG x + | Targ_pattern x -> CT_coerce_PATTERN_to_TARG x + | Targ_unfold_ne_list x -> CT_coerce_UNFOLD_NE_LIST_to_TARG x + | Targ_unfold x -> CT_coerce_UNFOLD_to_TARG x + | Targ_string x -> + CT_coerce_ID_OR_STRING_to_TARG (CT_coerce_STRING_to_ID_OR_STRING x) + | Targ_fixtac x -> CT_coerce_FIXTAC_to_TARG x + | Targ_cofixtac x -> CT_coerce_COFIXTAC_to_TARG x + | Targ_tacexp x -> CT_coerce_TACTIC_COM_to_TARG x + | Targ_redexp x -> xlate_error "coerce_iTarg_to_TARG(2)";; + +let rec coerce_iVARG_to_VARG = + function + | Varg_binder x -> CT_coerce_BINDER_to_VARG x + | Varg_binderlist x -> CT_coerce_BINDER_LIST_to_VARG x + | Varg_bindernelist x -> CT_coerce_BINDER_NE_LIST_to_VARG x + | Varg_call (id, l) -> xlate_error "coerce_iVARG_to_VARG: CALL as varg" + | Varg_constr x -> + CT_coerce_FORMULA_OPT_to_VARG (CT_coerce_FORMULA_to_FORMULA_OPT x) + | Varg_sorttype x -> + CT_coerce_FORMULA_OPT_to_VARG + (CT_coerce_FORMULA_to_FORMULA_OPT (CT_coerce_SORT_TYPE_to_FORMULA x)) + | Varg_constrlist x -> CT_coerce_FORMULA_LIST_to_VARG (CT_formula_list x) + | Varg_ident x -> + CT_coerce_ID_OPT_OR_ALL_to_VARG + (CT_coerce_ID_OPT_to_ID_OPT_OR_ALL (CT_coerce_ID_to_ID_OPT x)) + | Varg_int x -> CT_coerce_INT_OPT_to_VARG (CT_coerce_INT_to_INT_OPT x) + | Varg_intlist x -> CT_coerce_INT_LIST_to_VARG x + | Varg_none -> CT_coerce_FORMULA_OPT_to_VARG ctv_FORMULA_OPT_NONE + | Varg_string x -> + CT_coerce_STRING_OPT_to_VARG (CT_coerce_STRING_to_STRING_OPT x) + | Varg_tactic x -> + CT_coerce_TACTIC_OPT_to_VARG (CT_coerce_TACTIC_COM_to_TACTIC_OPT x) + | Varg_astlist x -> CT_coerce_AST_LIST_to_VARG x + | Varg_ast x -> CT_coerce_AST_to_VARG x + | Varg_varglist x -> + CT_coerce_VARG_LIST_to_VARG + (CT_varg_list (List.map coerce_iVARG_to_VARG x)) + | _ -> xlate_error "coerce_iVARG_to_VARG: leftover case";; + +let coerce_iVARG_to_FORMULA = + function + | Varg_constr x -> x + | Varg_sorttype x -> CT_coerce_SORT_TYPE_to_FORMULA x + | _ -> xlate_error "coerce_iVARG_to_FORMULA: unexpected argument";; + +let coerce_iVARG_to_ID = + function Varg_ident id -> id + | _ -> xlate_error "coerce_iVARG_to_ID";; + +let coerce_VARG_to_ID = + function + | CT_coerce_ID_OPT_OR_ALL_to_VARG (CT_coerce_ID_OPT_to_ID_OPT_OR_ALL (CT_coerce_ID_to_ID_OPT x)) -> + x + | _ -> xlate_error "coerce_VARG_to_ID";; + +let xlate_id = + function + | Nvar (_, id) -> + (match id with + | "_" -> xlate_error "xlate_id: '_' is ident option" + | s -> CT_ident s) + | Id (_, id) -> + (match id with + | "_" -> xlate_error "xlate_id: '_' is ident option" + | s -> CT_ident s) + | _ -> xlate_error "xlate_id: not an identifier";; + +let xlate_id_unit = function + Node(_, "VOID", []) -> CT_unit + | x -> CT_coerce_ID_to_ID_UNIT (xlate_id x);; + +let xlate_id_opt = + function + | Nvar (_, id) -> + (match id with + | "_" -> ctv_ID_OPT_NONE + | s -> ctf_ID_OPT_SOME (CT_ident s)) + | _ -> xlate_error "xlate_id: not an identifier";; + +let xlate_int = + function + | Num (_, n) -> CT_int n + | _ -> xlate_error "xlate_int: not an int";; + +let xlate_string = + function + | Str (_, s) -> CT_string s + | _ -> xlate_error "xlate_string: not a string";; + +(** Formulae + *) +let strip_Rform = + function + | Rform body -> body + | _ -> xlate_error "strip_Rform: binder expression as formula";; + +let make_lambdac dom boundcod = + let rec gather = + function + | Rbinder (x, body) -> + let l, body' = gather body in + x::l, body' + | Rform body -> [], body + | _ -> xlate_error "make_lambdac : not Rbinder or Rform" in + let varlist, cod = gather boundcod in + match varlist with + | [] -> xlate_error "make_lamdac: empty binder list" + | id :: l -> CT_lambdac (CT_binder (CT_id_opt_ne_list (id, l), dom), cod);; + +let rec make_prodc dom = + let rec gather = + function + | Rbinder (id_opt, body) -> + let l, body' = gather body in + id_opt::l, body' + | Rform body -> [], body + | _ -> xlate_error "gather for make_prodc : not Rbinder or Rform" in + function + | Rform body -> xlate_error "make_prodc: empty binder list in make_binder" + | boundrange -> + let varlist, range = gather boundrange in + (match varlist with + | [] -> range + | id :: l -> CT_prodc (CT_binder (CT_id_opt_ne_list (id, l), dom), range));; + +let make_appln = + function + | [] -> xlate_error "make_appln: empty application list" + | (Rform m) :: [] -> m + | (Rform m) :: ((Rform n) :: l) -> + CT_appc (m, CT_formula_ne_list (n, List.map strip_Rform l)) + | _ -> xlate_error "make_appln: binder expression in application";; + +let make_casec casety = + function + | [] -> xlate_error "bad case expression" + | x :: [] -> xlate_error "bad case expression" + | (Rform a) :: ((Rform m) :: l) -> + CT_elimc (CT_case casety, a, m, CT_formula_list (List.map strip_Rform l)) + | _ -> xlate_error "make_casec: binder expression as formula";; + +let qualid_to_ct_ID = + function + Nvar(_, s) -> Some(CT_ident s) + | Node(_, ("QUALID"|"QUALIDARG"), l) -> + (* // to be modified when qualified identifiers are introducted. *) + let rec f = + function + [] -> xlate_error "empty list in qualified identifier" + | [Nvar(_,a)] -> a + | (Nvar(_,s))::l -> s ^ "." ^ (f l) + | _ -> assert false in + Some(CT_ident (f l)) + | _ -> None;; + + +let special_case_qualid cont_function astnode = + match qualid_to_ct_ID astnode with + Some(id) -> Some(Rform(CT_coerce_ID_to_FORMULA id)) + | None -> None;; + +let xlate_op the_node opn a b = + match opn with + | "META" -> + (match a, b with + | ((Num (_, n)) :: []), [] -> CT_metac (CT_int n) + | _, _ -> xlate_error "xlate_op : META ") + | "ISEVAR" -> CT_existvarc + | "FORCEIF" -> + (match a,b with + | [], l -> + make_casec "Case" l + | _,_ -> xlate_error "xlate_op : FORCEIF") + | "PROP" -> + (match a, b with + | [], [] -> + CT_coerce_SORT_TYPE_to_FORMULA (CT_sortc "Prop") + | _, _ -> xlate_error "xlate_op : PROP ") + | "SET" -> + (match a, b with + | [], [] -> + CT_coerce_SORT_TYPE_to_FORMULA (CT_sortc "Set") + | _, _ -> xlate_error "xlate_op : PROP ") + | (*The number of elements in the argument list is left unspecified: this list + varies when the object is type-checked <Yves Bertot 21/3/95> *) + "TYPE" -> + (match a, b with + | _, _ -> CT_coerce_SORT_TYPE_to_FORMULA (CT_sortc "Type")) + | "CAST" -> + (match a, b with + | [], ((Rform c1) :: ((Rform c2) :: [])) -> castc (CT_typed_formula (c1, c2)) + | _, _ -> xlate_error "xlate_op : CAST ") + | "PROD" -> + (match a, b with + | [], + ((Rform c1) :: + ((Rbinder ((CT_coerce_NONE_to_ID_OPT CT_none), (Rform c2))) :: [])) -> + CT_arrowc (c1, c2) + | [], + ((Rform c1) :: ((Rbinder ((CT_coerce_ID_to_ID_OPT id), (Rform c2))) :: [])) -> + CT_prodc + (CT_binder (CT_id_opt_ne_list (CT_coerce_ID_to_ID_OPT id, []), c1), c2) + | _, _ -> xlate_error "xlate_op : PROD") + | "LAMBDA" -> + (match a, b with + | [], [Rform c1;Rbinder (b, (Rform c2))] -> + CT_lambdac (CT_binder (CT_id_opt_ne_list (b, []), c1), c2) + | _, _ -> xlate_error "xlate_op : LAMBDA") + | "PRODLIST" -> + (match a, b with + | [], ((Rform c1) :: (c2 :: [])) -> make_prodc c1 c2 + | _, _ -> xlate_error "xlate_op : PRODLIST") + | "LAMBDALIST" -> + (match a, b with + | [], ((Rform c1) :: (c2 :: [])) -> make_lambdac c1 c2 + | _, _ -> xlate_error "xlate_op : LAMBDALIST") + | "APPLIST" -> + (match a, b with + | [], tl -> make_appln tl + | _, _ -> xlate_error "xlate_op : APPLIST") + | (** string_of_path needs to be investigated. + *) + "CONST" -> + (match a, b with + | ((Path (_, sl, kind)) :: []), [] -> + CT_coerce_ID_to_FORMULA(CT_ident + (Names.string_of_id (Names.basename (Ast.section_path sl kind)))) + | ((Path (_, sl, kind)) :: []), tl -> + CT_coerce_ID_to_FORMULA(CT_ident + (Names.string_of_id(Names.basename (Ast.section_path sl kind)))) + | _, _ -> xlate_error "xlate_op : CONST") + | (** string_of_path needs to be investigated. + *) + "MUTIND" -> + (match a, b with + | [Path(_, sl, kind); Num(_, tyi)], [] -> + if !in_coq_ref then + match special_case_qualid () + (!xlate_mut_stuff (Node((0,0),"MUTIND", a))) with + Some (Rform x) -> x + | _ -> assert false + else + CT_coerce_ID_to_FORMULA( + CT_ident(Names.string_of_id + (Names.basename + (Ast.section_path sl kind)))) + | _, _ -> 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") + | (** string_of_path needs to be investigated. + *) + "MUTCONSTRUCT" -> + (match a, b with + | [Path(_, sl, kind);Num(_, tyi);Num(_, n)], cl -> + if !in_coq_ref then + match + special_case_qualid () + (!xlate_mut_stuff (Node((0,0),"MUTCONSTRUCT",a))) with + | Some(Rform x) -> x + | _ -> assert false + else + let name = Names.string_of_path (Ast.section_path sl kind) in + (* This is rather a patch to cope with the fact that identifier + names have disappeared from the vo files for grammar rules *) + let type_desc = (try Some (Hashtbl.find type_table name) with + Not_found -> None) in + (match type_desc with + None -> + xlate_error + ("MUTCONSTRUCT:" ^ + " can't describe a constructor without its name " ^ + name) + | Some type_desc' -> + let type_desc'' = type_desc'.(tyi) in + let ident = type_desc''.(n) in + CT_coerce_ID_to_FORMULA(CT_ident ident)) + | _, _ -> xlate_error "xlate_op : MUTCONSTRUCT") + + | opn -> xlate_error ("xlate_op : " ^ opn ^ " doesn't exist (" ^ + (string_of_node_loc the_node) ^ ")");; + +let split_params = + let rec sprec acc = + function + | (Id _ as p) :: l -> sprec (p::acc) l + | (Str _ as p) :: l -> sprec (p::acc) l + | (Num _ as p) :: l -> sprec (p::acc) l + | (Path _ as p) :: l -> sprec (p::acc) l + | l -> List.rev acc, l in + sprec [];; + +let id_to_pattern_var ctid = + match ctid with + | CT_ident "_" -> + 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));; + +let rec xlate_cases_pattern cont_function = + function + | Nvar(_, s) -> id_to_pattern_var (CT_ident s) + | Node (_, "QUALID", l) as it -> + (match qualid_to_ct_ID it with + Some x -> id_to_pattern_var x + | None -> assert false) + | Node (_, "PATTCONSTRUCT", (f1 :: (arg1 :: args))) -> + CT_pattern_app + (xlate_cases_pattern cont_function f1, + CT_match_pattern_ne_list + (xlate_cases_pattern cont_function arg1, + List.map (xlate_cases_pattern cont_function) args)) + | Node (_, "PATTAS", [Nvar (_, id); pattern]) -> + CT_pattern_as + (xlate_cases_pattern + cont_function pattern, CT_coerce_ID_to_ID_OPT (CT_ident id)) + | Node (_, "PATTCONSTRUCT", [f]) -> xlate_cases_pattern cont_function f + | Node (_, ("MUTCONSTRUCT" as s), args) as it -> + let pl, tl = split_params args in + (match xlate_op it s pl (List.map cont_function tl) with + | CT_coerce_ID_to_FORMULA id -> id_to_pattern_var id + | _ -> assert false) + | Node(_, s, _) -> xlate_error ("error for a pattern " ^ s) + | _ -> xlate_error "Unexpected data while translating a pattern";; + +(*This function recognizes and translates let constructs + // I think this code should be adapted to build a real let construct *) +let special_case_let_construct cont_function = + function + | Node (_, "LETIN", [val_arg;Slam(_, (Some b), body)]) -> + Some + (Rform + (CT_letin(CT_ident b, strip_Rform (cont_function val_arg), + 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)) -> + (match idl with + | [] -> xlate_error "cvt_binder empty identifier list" + | id :: l -> + CT_binder + (CT_id_opt_ne_list (xlate_id_opt id, + List.map xlate_id_opt l), + cont_function c)) + | _ -> failwith "cvt_binder";; + +let cvt_binders cont_function = + function + | Node(_,name, args) when name = "BINDERLIST" or name = "BINDERS" -> + CT_binder_list(List.map (cvt_binder cont_function) args) + | _ -> failwith "cvt_binders";; + + +(*This function recognizes and translates the Fix construct *) +let special_case_fix cont_function = + function + | Node (_, "FIX", ((Nvar (_, iddef)) :: (l :: ldecl))) -> + let xlate_fixbinder = + function + | Node (_, "NUMFDECL", + ((Nvar (_, fi)) :: + ((Num (_, ni)) :: (v_Type :: (v_Value :: []))))) -> + let v_Type' = strip_Rform (cont_function v_Type) in + let v_Value' = strip_Rform (cont_function v_Value) in + CT_fix_binder (CT_ident fi, CT_int ni, v_Type', v_Value') + | Node (_, "FDECL", + ((Nvar (_, fi)) :: + (binder :: (v_Type :: (v_Value :: []))))) -> + let v_Type' = strip_Rform (cont_function v_Type) in + let v_Value' = strip_Rform (cont_function v_Value) in + (match cvt_binders (compose strip_Rform cont_function) binder with + | CT_binder_list(a::tl) -> + CT_coerce_FIX_REC_to_FIX_BINDER + (CT_fix_rec (CT_ident fi, CT_binder_ne_list(a,tl), + v_Type', v_Value')) + | _ -> xlate_error ("special_case_fix : " ^ + "empty list of binders")) + | _ -> + xlate_error + ("special_case_fix : " ^ "FIX, unexpected form in xlate_fixbinder") + in + Some + (Rform + (CT_fixc + (CT_ident iddef, + CT_fix_binder_list (xlate_fixbinder l, List.map xlate_fixbinder ldecl)))) + | _ -> None;; + +(*This function recognizes and translates cofix constructs *) +let special_case_cofix cont_function = + function + | Node (_, "COFIX", ((Nvar (_, iddef)) :: (l :: ldecl))) -> + let xlate_cofixbinder = + function + | Node (_, "CFDECL", ((Nvar (_, fi)) :: (v_Type :: (v_Value :: [])))) -> + let v_Type' = strip_Rform (cont_function v_Type) in + let v_Value' = strip_Rform (cont_function v_Value) in + CT_cofix_rec (CT_ident fi, v_Type', v_Value') + | _ -> + xlate_error + ("special_case_cofix : " ^ + "COFIX, unexpected form in xlate_fixbinder") in + Some + (Rform + (CT_cofixc + (CT_ident iddef, + CT_cofix_rec_list (xlate_cofixbinder l, List.map xlate_cofixbinder ldecl)))) + | _ -> None;; + + + +let rec list_last = function + | [a] -> a + | a::l -> list_last l + | [] -> failwith "list_last called on an empty list";; + +let rec slam_body = function + | Slam(_, _, b) -> slam_body b + | c -> c;; + +let translate_one_equation cont_function = function + | Node (_, "EQN", body::first_pattern::patterns) -> + let translated_patterns = List.map + (xlate_cases_pattern cont_function) + patterns in + CT_eqn + (CT_match_pattern_ne_list + (xlate_cases_pattern + cont_function first_pattern, translated_patterns), + strip_Rform (cont_function body)) + | _ -> + xlate_error "Unexpected equation shape while translating a Cases" + +(*this function recognizes and translates Cases constructs *) +let special_case_cases cont_function = + function + | Node(_, s, + type_returned::matched_arg::equations) when + (s = "CASES") or (s = "FORCELET") or (s = "FORCEIF") -> + let simple_type_returned = + match type_returned with + | (Str (_, "SYNTH")) -> ctv_FORMULA_OPT_NONE + | _ -> + CT_coerce_FORMULA_to_FORMULA_OPT + (strip_Rform (cont_function type_returned)) in + let extract_equation = (function + | Node(_, "EQN", l) as it -> it + | _ -> xlate_error "equation is not an EQN") in + let translated_equations = + List.map + (fun x -> translate_one_equation cont_function (extract_equation x)) + equations in + let first_value, translated_matched_values = + match matched_arg with + | Node (_, "TOMATCH", matched_values) -> + (match + List.map (function x -> strip_Rform (cont_function x)) matched_values + with + | a :: b -> a, b + | _ -> xlate_error "Empty list of match values while translating a Cases") + | one_matched_value -> strip_Rform (cont_function one_matched_value), [] + in + Some + (Rform + (CT_cases + (simple_type_returned, + CT_formula_ne_list (first_value, translated_matched_values), + CT_eqn_list translated_equations))) + | _ -> None;; + +(*These functions are auxiliary to the function that translate annotated + formulas for the natural language presentation of proofs *) +let xlate_ID = + function + | Node (_, "ident", ((Str (_, str)) :: [])) -> CT_ident str + | Node (_, str, l) -> + xlate_error ("xlate_ID:" ^ str ^ ":" ^ string_of_int (List.length l)) + | _ -> xlate_error "xlate_ID";; + +let xlate_STRING = + function + | Str (_, str) -> CT_string str + | Node (_, str, l) -> + xlate_error ("xlate_STRING:" ^ str ^ ":" ^ string_of_int (List.length l)) + | _ -> xlate_error "xlate_STRING";; + +let rec strip_bang cont_function = + function + | [] -> [], false + | a :: tl -> + (match a with + | Node (_, "XTRA", ((Str (_, "!")) :: ((Num (_, n)) :: (f :: [])))) -> + if in_coq () then + strip_bang cont_function tl + else + begin + let l, b = strip_bang cont_function tl in + strip_Rform (cont_function f)::l, b + end + | Node (_, "EXPL", [Num(_, n); f]) -> + let l, _ = strip_bang cont_function tl in + strip_Rform (cont_function f)::l, true + | _ -> + let l, b = strip_bang cont_function tl in + strip_Rform (cont_function a)::l, b);; + +let special_case_bang cont_function = + function + | Node (_, "APPLISTEXPL", f::tl) -> + let l, b = strip_bang cont_function tl in + let compiled_f = strip_Rform (cont_function f) in + let + real_function = + if in_coq () then + (if b then CT_bang (CT_coerce_NONE_to_INT_OPT CT_none, compiled_f) + else compiled_f) + else CT_bang (CT_coerce_NONE_to_INT_OPT CT_none, compiled_f) in + (match l with + | [] -> xlate_error "special_case_bang: empty argument list?" + | elnt :: l' -> + Some (Rform (CT_appc (real_function, CT_formula_ne_list (elnt, l'))))) + | _ -> None;; + +exception Not_natural;; + +let rec nat_to_number = + function + | Node (_, "APPLIST", ((Nvar (_, "S")) :: (v :: []) as v0)) -> + 1 + nat_to_number v + | Nvar (_, "O") -> 0 + | _ -> raise Not_natural;; + +let g_nat_syntax_flag = ref false;; + +let set_flags = ref (function () -> ());; + +let special_case_S cont_function ast = + if !g_nat_syntax_flag then (match ast with + | Node (_, "APPLIST", ((Nvar (_, "S")) :: (v :: []))) as v0 -> begin + try Some (Rform (CT_int_encapsulator (CT_int (nat_to_number v0)))) + with + | Not_natural -> None + end + | Nvar (_, "O") -> Some (Rform (CT_int_encapsulator (CT_int 0))) + | _ -> None) + else None;; + +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; + special_case_bang; special_case_S];; + +let xlate_special_cases cont_function arg = + let rec xlate_rec = + function + | f :: tl -> + (match f cont_function arg with + | Some _ as it -> it + | None -> xlate_rec tl) + | [] -> None in + xlate_rec xlate_formula_special_cases;; + +let xlate_formula a = + !set_flags (); + let rec ctrec = + function + | Nvar (_, id) -> Rform (varc (CT_ident id)) + | Slam (_, na, t) -> + let id = + match na with + | None -> ctv_ID_OPT_NONE + | Some id -> if id = "_" then ctv_ID_OPT_NONE + else ctf_ID_OPT_SOME (CT_ident id) in + let body = ctrec t in + Rbinder (id, body) + | Node (_, opn, tl) as it -> + (match xlate_special_cases ctrec it with + | Some result -> result + | None -> + let pl, tl' = split_params tl in + Rform (xlate_op it opn pl (List.map ctrec tl'))) + | _ -> xlate_error "xlate_formula" in + strip_Rform (ctrec a);; + +let xlate_formula_opt = + function + | Node (_, "None", []) -> ctv_FORMULA_OPT_NONE + | e -> CT_coerce_FORMULA_to_FORMULA_OPT (xlate_formula e);; + +(** Tactics + *) +let strip_targ_spec_list = + function + | Targ_spec_list x -> x + | _ -> xlate_error "strip tactic: non binding-list argument";; + +let strip_targ_binding = + function + | Targ_binding x -> x + | _ -> xlate_error "strip tactic: non-binding argument";; + +let strip_targ_command = + function + | Targ_command x -> x + | Targ_binding_com x -> x + | _ -> xlate_error "strip tactic: non-command argument";; + +let strip_targ_ident = + function + | Targ_ident x -> x + | _ -> xlate_error "strip tactic: non-ident argument";; + +let strip_targ_int = + function + | Targ_int x -> x + | _ -> xlate_error "strip tactic: non-int argument";; + +let strip_targ_pattern = + function + | Targ_pattern x -> x + | _ -> xlate_error "strip tactic: non-pattern argument";; + +let strip_targ_unfold = + function + | Targ_unfold x -> x + | _ -> xlate_error "strip tactic: non-unfold argument";; + +let strip_targ_fixtac = + function + | Targ_fixtac x -> x + | _ -> xlate_error "strip tactic: non-fixtac argument";; + +let strip_targ_cofixtac = + function + | Targ_cofixtac x -> x + | _ -> xlate_error "strip tactic: non-cofixtac argument";; + +(*Need to transform formula to id for "Prolog" tactic problem *) +let make_ID_from_FORMULA = + function + | CT_coerce_ID_to_FORMULA id -> id + | _ -> xlate_error "make_ID_from_FORMULA: non-formula argument";; + +let make_ID_from_iTARG_FORMULA x = make_ID_from_FORMULA (strip_targ_command x);; + +let filter_binding_or_command_list bl = + match bl with + | (Targ_binding_com cmd) :: bl' -> + CT_coerce_FORMULA_LIST_to_SPEC_LIST + (CT_formula_list (List.map strip_targ_command bl)) + | (Targ_binding b) :: bl' -> + CT_coerce_BINDING_LIST_to_SPEC_LIST + (CT_binding_list (List.map strip_targ_binding bl)) + | [] -> CT_coerce_FORMULA_LIST_to_SPEC_LIST (CT_formula_list []) + | _ -> xlate_error "filter_binding_or_command_list";; + +let strip_targ_spec_list = + function + | Targ_spec_list x -> x + | _ -> xlate_error "strip_tar_spec_list";; + +let strip_targ_intropatt = + function + | Targ_intropatt x -> x + | _ -> xlate_error "strip_targ_intropatt";; + + +let rec get_flag_rec = + function + | n1 :: tail -> + 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 (_, "Unf", l) -> + (match red_ids with + | CT_unf [] -> conv_flags, CT_unf (List.map xlate_id 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) + | _ -> error "Cannot specify identifiers to unfold twice") + | Node (_, a, _) -> error ("get_flag_rec : unexpected flag " ^ a) + | _ -> error "get_flag_rec : unexpected flag") + | [] -> [], CT_unf [];; + +let rec xlate_intro_pattern = + function + | Node(_,"CONJPATTERN",[Node(_, "LISTPATTERN", l)]) -> + CT_conj_pattern(CT_intro_patt_list (List.map xlate_intro_pattern l)) + | Node(_, "DISJPATTERN", [Node(_,"LISTPATTERN",l)]) -> + CT_disj_pattern(CT_intro_patt_list (List.map xlate_intro_pattern l)) + | Node(_, "IDENTIFIER", [Nvar(_,c)]) -> + CT_coerce_ID_to_INTRO_PATT(CT_ident c) + | Node(_, a, _) -> failwith ("xlate_intro_pattern on node " ^ a) + | _ -> failwith "xlate_intro_pattern";; + +let compute_INV_TYPE_from_string = function + "InversionClear" -> CT_inv_clear + | "HalfInversion" -> CT_inv_simple + | "Inversion" -> CT_inv_regular + | _ -> failwith "unexpected Inversion type";; + +let is_tactic_special_case = function + "AutoRewrite" -> true + | _ -> false;; + +let tactic_special_case cont_function cvt_arg = function + "AutoRewrite", (tac::v::bl) -> + CT_autorewrite + (CT_id_ne_list(xlate_id v, List.map xlate_id bl), + CT_coerce_TACTIC_COM_to_TACTIC_OPT(cont_function tac)) + | "AutoRewrite", (v::bl) -> + CT_autorewrite + (CT_id_ne_list(xlate_id v, List.map xlate_id bl), + CT_coerce_NONE_to_TACTIC_OPT CT_none) + | _ -> assert false;; + +let xlate_context_pattern = function + Node(_,"TERM", [Node(_, "COMMAND", [v])]) -> + CT_coerce_FORMULA_to_CONTEXT_PATTERN (xlate_formula v) + | Node(_,"SUBTERM", [Nvar(_, s); Node(_, "COMMAND", [v])]) -> + CT_context(ctf_ID_OPT_SOME (CT_ident s), xlate_formula v) + | _ -> assert false;; + +let xlate_match_context_hyps = function + [b] -> CT_premise_pattern(ctv_ID_OPT_NONE, xlate_context_pattern b) + | [Nvar(_,s);b] -> CT_premise_pattern(ctf_ID_OPT_SOME (CT_ident s), + xlate_context_pattern b) + | _ -> assert false;; + + +let xlate_largs_to_id_unit largs = + match List.map xlate_id_unit largs with + fst::rest -> fst, rest + | _ -> assert false;; + +let rec cvt_arg = + function + | Nvar (_, id) -> Targ_ident (CT_ident id) + | Str (_, s) -> Targ_string (CT_string s) + | Num (_, n) -> Targ_int (CT_int n) + | Node (_, "LETPATTERNS", fst::l) -> + let mk_unfold_occ = function + Node(_, "HYPPATTERN", Nvar(_, name)::ints) -> + CT_unfold_occ( + CT_int_list (List.map xlate_int ints), CT_ident name) + | Node(_, "CCLPATTERN", ints) -> + CT_unfold_occ( + CT_int_list (List.map xlate_int ints), CT_ident "Goal") + | _ -> xlate_error "unexpected argument in mk_unfold_occ" in + Targ_unfold_ne_list( + CT_unfold_ne_list(mk_unfold_occ fst, List.map mk_unfold_occ l)) + | Node (_, "COMMAND", (c :: [])) -> Targ_command (xlate_formula c) + | Node (_, "CASTEDCOMMAND", (c :: [])) -> Targ_command (xlate_formula c) + | Node (_, "BINDINGS", bl) -> + Targ_spec_list (filter_binding_or_command_list (List.map cvt_arg bl)) + | Node (_, "BINDING", ((Node (_, "COMMAND", (c :: []))) :: [])) -> + Targ_binding_com (xlate_formula c) + | Node (_, "BINDING", + ((Num (_, n)) :: ((Node (_, "COMMAND", (c :: []))) :: []))) -> + Targ_binding + (CT_binding (CT_coerce_INT_to_ID_OR_INT (CT_int n), xlate_formula c)) + | Node (_, "BINDING", + ((Nvar (_, id)) :: ((Node (_, "COMMAND", (c :: []))) :: []))) -> + Targ_binding + (CT_binding (CT_coerce_ID_to_ID_OR_INT (CT_ident id), xlate_formula c)) + | Node (_, "TACTIC", (t :: [])) -> Targ_tacexp (xlate_tactic t) + | Node (_, "FIXEXP", + ((Nvar (_, id)) :: + ((Num (_, n)) :: ((Node (_, "COMMAND", (c :: []))) :: [])))) -> + Targ_fixtac (CT_fixtac (CT_ident id, CT_int n, xlate_formula c)) + | 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 (_, "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) + | _ -> failwith "cvt_arg" +and xlate_red_tactic = + function + | Node (loc, s, []) -> + (match s with + | "Red" -> CT_red + | "Hnf" -> CT_hnf + | "Simpl" -> CT_simpl + | "Fold" -> CT_fold(CT_formula_list[]) + | _ -> xlate_error ("xlate_red_tactic, unexpected singleton " ^ s)) + | Node (_, "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) + | n -> + xlate_error ("xlate_red_tactic, expected unfold occurrence at " ^ + (string_of_node_loc n))) + unf_list in + (match ct_unf_list with + | first :: others -> CT_unfold (CT_unfold_ne_list (first, others)) + | [] -> error "there should be at least one thing to unfold") + | Node (_, "Cbv", flag_list) -> + let conv_flags, red_ids = get_flag_rec flag_list in + CT_cbv (CT_conversion_flag_list conv_flags, red_ids) + | Node (_, "Lazy", flag_list) -> + let conv_flags, red_ids = get_flag_rec flag_list in + CT_lazy (CT_conversion_flag_list conv_flags, red_ids) + | Node (_, "Pattern", l) -> + let pat_list = List.map (function + | Node (_, "PATTERN", ((Node (_, "COMMAND", (c :: []))) :: nums)) -> + CT_pattern_occ + (CT_int_list (List.map xlate_int nums), xlate_formula c) + | _ -> error "Expecting patterns in a Pattern command") l in + (match pat_list with + | first :: others -> CT_pattern (CT_pattern_ne_list (first, others)) + | [] -> error "Expecting at least one pattern in a Pattern command") + | Node (_, "Fold", formula_list) -> + CT_fold(CT_formula_list(List.map + (function Node(_,"COMMAND", [c]) -> xlate_formula c + | _ -> error("xlate_red_tactic expected a COMMAND")) + formula_list)) + | Node (_, a, _) -> error ("xlate_red_tactic: unexpected argument " ^ a) + | _ -> error "xlate_red_tactic : unexpected argument" +and xlate_tactic = + function + | Node (_, s, l) -> + (match s, l with + | "FUN", [Node(_, "FUNVAR", largs); t] -> + let fst, rest = xlate_largs_to_id_unit largs in + CT_tactic_fun + (CT_id_unit_list(fst, rest), xlate_tactic t) + | "TACTICLIST", (t :: tl) -> + (match List.map xlate_tactic (t::tl) with + | [] -> xlate_error "xlate_tactic: internal xlate_error" + | xt :: [] -> xt + | CT_then(xt,xtl1) :: xtl -> CT_then (xt, xtl1@xtl) + | xt :: xtl -> CT_then (xt, xtl)) + | "TACTICLIST", _ -> + xlate_error "xlate_tactic: malformed tactic-expression TACTICLIST" + | "TACLIST", (t :: tl) -> + (match List.map xlate_tactic (t::tl) with + | [] -> xlate_error "xlate_tactic: internal xlate_error" + | xt :: [] -> xt + | xt :: xtl -> CT_parallel (xt, xtl)) + | "FIRST", (a::l) -> + CT_first(xlate_tactic a,List.map xlate_tactic l) + | "TCLSOLVE", (a::l) -> + CT_tacsolve(xlate_tactic a, List.map xlate_tactic l) + | "DO", ((Num (_, n)) :: (t :: [])) -> CT_do (CT_int n, xlate_tactic t) + | "DO", _ -> xlate_error "xlate_tactic: malformed tactic-expression DO" + | "TRY", (t :: []) -> CT_try (xlate_tactic t) + | "TRY", _ -> xlate_error "xlate_tactic: malformed tactic-expression TRY" + | "REPEAT", (t :: []) -> CT_repeat (xlate_tactic t) + | "ABSTRACT", (Node(_,_,[t]) :: []) -> CT_abstract(ctv_ID_OPT_NONE, (xlate_tactic t)) + | "ABSTRACT", (Nvar(_, id)::(Node(_,"TACTIC",[t]) :: [])) -> + CT_abstract(ctf_ID_OPT_SOME (CT_ident id), (xlate_tactic t)) + | "INFO", (t :: []) -> CT_info (xlate_tactic t) + | "REPEAT", _ -> + xlate_error "xlate_tactic: malformed tactic-expression REPEAT" + | "ORELSE", (t1 :: (t2 :: [])) -> + CT_orelse (xlate_tactic t1, xlate_tactic t2) + | "ORELSE", _ -> + xlate_error "xlate_tactic: malformed tactic-expression ORELSE" + | ((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 + 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)) + | "MATCHCONTEXT", rule1::rules -> + CT_match_context(xlate_context_rule rule1, + List.map xlate_context_rule rules) + | s, l -> xlate_tac (s, List.map cvt_arg l)) + | Nvar(_, s) -> ident_tac s + | the_node -> xlate_error ("xlate_tactic at " ^ + (string_of_node_loc the_node) ) + +and xlate_tac = + function + | "Absurd", ((Targ_command c) :: []) -> CT_absurd c + | "Change", [Targ_command f; Targ_id_list b] -> CT_change(f,b) + | "Contradiction", [] -> CT_contradiction + | "DoubleInd", ((Targ_int n1) :: ((Targ_int n2) :: [])) -> + CT_tac_double (n1, n2) + | "Discr", [] -> CT_discriminate_eq ctv_ID_OPT_NONE + | "DiscrHyp", ((Targ_ident id) :: []) -> + CT_discriminate_eq (ctf_ID_OPT_SOME id) + | "DEqConcl", [] -> CT_simplify_eq ctv_ID_OPT_NONE + | "DEqHyp", ((Targ_ident id) :: []) -> CT_simplify_eq (ctf_ID_OPT_SOME id) + | "Inj", [] -> CT_injection_eq ctv_ID_OPT_NONE + | "InjHyp", ((Targ_ident id) :: []) -> CT_injection_eq (ctf_ID_OPT_SOME id) + | "Fix", ((Targ_int n) :: []) -> + CT_fixtactic (ctv_ID_OPT_NONE, n, CT_fix_tac_list []) + | "Fix", ((Targ_ident id) :: ((Targ_int n) :: fixtac_list)) -> + CT_fixtactic + (ctf_ID_OPT_SOME id, n, + CT_fix_tac_list (List.map strip_targ_fixtac fixtac_list)) + | "Cofix", [] -> CT_cofixtactic (ctv_ID_OPT_NONE, CT_cofix_tac_list []) + | "Cofix", ((Targ_ident id) :: cofixtac_list) -> + CT_cofixtactic + (CT_coerce_ID_to_ID_OPT id, + CT_cofix_tac_list (List.map strip_targ_cofixtac cofixtac_list)) + | "IntrosUntil", ((Targ_ident id) :: []) -> CT_intros_until id + | "IntroMove", [Targ_ident id1;Targ_ident id2] -> + CT_intro_after(CT_coerce_ID_to_ID_OPT id1, id2) + | "IntroMove", [Targ_ident id2] -> + CT_intro_after(CT_coerce_NONE_to_ID_OPT CT_none, id2) + | "MoveDep", [Targ_ident id1;Targ_ident id2] -> + CT_move_after(id1, id2) + | "Intros", [] -> CT_intros (CT_intro_patt_list []) + | "Intros", [patt_list] -> + CT_intros (strip_targ_intropatt patt_list) + | "Intro", [Targ_ident (CT_ident id)] -> + CT_intros (CT_intro_patt_list [CT_coerce_ID_to_INTRO_PATT(CT_ident id)]) + | "Left", (bindl :: []) -> CT_left (strip_targ_spec_list bindl) + | "Right", (bindl :: []) -> CT_right (strip_targ_spec_list bindl) + | "Split", (bindl :: []) -> CT_split (strip_targ_spec_list bindl) + | "Replace", ((Targ_command c1) :: ((Targ_command c2) :: [])) -> + CT_replace_with (c1, c2) + | (*Changes to Equality.v some more rewrite possibilities *) + "RewriteLR", [(Targ_command c); bindl] -> + CT_rewrite_lr (c, strip_targ_spec_list bindl, ctv_ID_OPT_NONE) + | "RewriteLRin", ((Targ_ident id) :: ((Targ_command c) :: (bindl::[]))) -> + CT_rewrite_lr (c, strip_targ_spec_list bindl, ctf_ID_OPT_SOME id) + | "RewriteRL", [Targ_command c; bindl] -> + CT_rewrite_rl (c, strip_targ_spec_list bindl, ctv_ID_OPT_NONE) + | "RewriteRLin", [Targ_ident id; Targ_command c; bindl] -> + CT_rewrite_rl (c, strip_targ_spec_list bindl, ctf_ID_OPT_SOME id) + | "CondRewriteLR", [Targ_tacexp t; Targ_command c; bindl] -> + CT_condrewrite_lr (t, c, strip_targ_spec_list bindl, ctv_ID_OPT_NONE) + | "CondRewriteRL", [Targ_tacexp t; Targ_command c; bindl] -> + CT_condrewrite_rl (t, c, strip_targ_spec_list bindl, ctv_ID_OPT_NONE) + | "CondRewriteLRin", [Targ_tacexp t; Targ_ident id; Targ_command c; bindl] -> + CT_condrewrite_lr (t, c, strip_targ_spec_list bindl, ctf_ID_OPT_SOME id) + | "CondRewriteRLin", [Targ_tacexp t; Targ_ident id; Targ_command c; bindl] -> + CT_condrewrite_rl (t, c, strip_targ_spec_list bindl, ctf_ID_OPT_SOME id) + | "SubstConcl_LR", ((Targ_command c) :: []) -> + CT_cutrewrite_lr (c, ctv_ID_OPT_NONE) + | "SubstHyp_LR", ((Targ_command c) :: ((Targ_ident id) :: [])) -> + CT_cutrewrite_lr (c, ctf_ID_OPT_SOME id) + | "SubstConcl_RL", ((Targ_command c) :: []) -> + CT_cutrewrite_rl (c, ctv_ID_OPT_NONE) + | "SubstHyp_RL", ((Targ_command c) :: ((Targ_ident id) :: [])) -> + CT_cutrewrite_rl (c, ctf_ID_OPT_SOME id) + | "SubstHypInConcl_LR", ((Targ_ident id) :: []) -> CT_deprewrite_lr id + | "SubstHypInConcl_RL", ((Targ_ident id) :: []) -> CT_deprewrite_rl id + | "Reflexivity", [] -> CT_reflexivity + | "Symmetry", [] -> CT_symmetry + | "Transitivity", ((Targ_command c) :: []) -> CT_transitivity c + | "Assumption", [] -> CT_assumption + | "FAIL", [] -> CT_fail + | "IDTAC", [] -> CT_idtac + | "Exact", ((Targ_command c) :: []) -> CT_exact c + | "DHyp", [Targ_ident id] -> CT_dhyp id + | "CDHyp", [Targ_ident id] -> CT_cdhyp id + | "DConcl", [] -> CT_dconcl + | "SuperAuto", [a1;a2;a3;a4] -> + CT_superauto( + (match a1 with + | Targ_int n -> (CT_coerce_INT_to_INT_OPT n) + | _ -> (CT_coerce_NONE_to_INT_OPT CT_none)), + (match a2 with + | Targ_id_list l -> l + | _ -> xlate_error + "SuperAuto expects a list of identifiers as second argument"), + (match a3 with + | Targ_string (CT_string "Destructing") -> CT_destructing + | _ -> (CT_coerce_NONE_to_DESTRUCTING CT_none)), + (match a4 with + | Targ_string (CT_string "UsingTDB") -> CT_usingtdb + | _ -> (CT_coerce_NONE_to_USINGTDB CT_none))) + + + | "AutoTDB", [Targ_int n] -> CT_autotdb (CT_coerce_INT_to_INT_OPT n) + | "AutoTDB", [] -> CT_autotdb (CT_coerce_NONE_to_INT_OPT CT_none) + | "Auto", ((Targ_int n) :: []) -> CT_auto (CT_coerce_INT_to_INT_OPT n) + | "Auto", ((Targ_string (CT_string "*"))::[]) + -> CT_auto_with((CT_coerce_NONE_to_INT_OPT CT_none), CT_star) + | "Auto", [] -> CT_auto (CT_coerce_NONE_to_INT_OPT CT_none) + | "Auto", ((Targ_int n) :: ((Targ_ident id1) :: idl)) -> + CT_auto_with ((CT_coerce_INT_to_INT_OPT n), + CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR( + CT_id_ne_list(id1, List.map (function Targ_ident(x) -> x + | _ -> xlate_error + "Auto expects identifiers") + idl))) + | "Auto", ((Targ_ident id1) :: idl) -> + CT_auto_with ((CT_coerce_NONE_to_INT_OPT CT_none), + CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR( + CT_id_ne_list(id1, List.map (function Targ_ident(x) -> x + | _ -> xlate_error + "Auto expects identifiers") + idl))) + | "Auto", ((Targ_int n) :: ((Targ_string (CT_string "*")) :: [])) -> + CT_auto_with ((CT_coerce_INT_to_INT_OPT n), CT_star) + | "EAuto", ((Targ_int n) :: []) -> CT_eauto (CT_coerce_INT_to_INT_OPT n) + | "EAuto", [] -> CT_eauto (CT_coerce_NONE_to_INT_OPT CT_none) + | "EAuto", ((Targ_int n) :: ((Targ_ident id1) :: idl)) -> + CT_eauto_with ((CT_coerce_INT_to_INT_OPT n), + CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR( + CT_id_ne_list(id1, List.map (function Targ_ident(x) -> x + | _ -> xlate_error + "Auto expects identifiers") + idl))) + | "EAuto", ((Targ_ident id1) :: idl) -> + CT_eauto_with ((CT_coerce_NONE_to_INT_OPT CT_none), + CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR( + CT_id_ne_list(id1, List.map (function Targ_ident(x) -> x + | _ -> xlate_error + "Auto expects identifiers") + idl))) + | "EAuto", ((Targ_int n) :: ((Targ_string (CT_string "*")) :: [])) -> + CT_eauto_with ((CT_coerce_INT_to_INT_OPT n), CT_star) + | "EAuto", ((Targ_string (CT_string "*"))::[]) + -> CT_eauto_with((CT_coerce_NONE_to_INT_OPT CT_none), CT_star) + | "Prolog", ((Targ_int n) :: idlist) -> + (*according to coqdev the code is right, they want formula *) + CT_prolog (CT_formula_list (List.map strip_targ_command idlist), n) + | (**) + "EApplyWithBindings", ((Targ_command c) :: (bindl :: [])) -> + CT_eapply (c, strip_targ_spec_list bindl) + | "Trivial", [] -> CT_trivial + | "Trivial", ((Targ_string (CT_string "*"))::[]) -> + CT_trivial_with(CT_star) + | "Trivial", ((Targ_ident id1):: idl) -> + CT_trivial_with(CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR( + (CT_id_ne_list(id1, + List.map (function Targ_ident x -> x + | _ -> xlate_error "Trivial expects identifiers") + idl)))) + | "Reduce", ((Targ_redexp id) :: ((Targ_id_list l) :: [])) -> + CT_reduce (id, l) + | "Apply", ((Targ_command c) :: (bindl :: [])) -> + CT_apply (c, strip_targ_spec_list bindl) + | "Constructor", ((Targ_int n) :: bindl) -> + CT_constructor (n, filter_binding_or_command_list bindl) + | "Specialize", + ((Targ_int n) :: ((Targ_command c) :: ((Targ_spec_list sl) :: []))) -> + CT_specialize (CT_coerce_INT_to_INT_OPT n, c, sl) + | "Specialize", ((Targ_command c) :: ((Targ_spec_list sl) :: [])) -> + CT_specialize (CT_coerce_NONE_to_INT_OPT CT_none, c, sl) + | "Generalize", (first :: cl) -> + CT_generalize + (CT_formula_ne_list + (strip_targ_command first, List.map strip_targ_command cl)) + | "GeneralizeDep", [Targ_command c] -> + CT_generalize_dependent c + | "ElimType", ((Targ_command c) :: []) -> CT_elim_type c + | "CaseType", ((Targ_command c) :: []) -> CT_case_type c + | "Elim", ((Targ_command c1) :: ((Targ_spec_list sl) :: [])) -> + CT_elim (c1, sl, CT_coerce_NONE_to_USING CT_none) + | "Elim", + ((Targ_command c1) :: + ((Targ_spec_list sl) :: + ((Targ_command c2) :: ((Targ_spec_list sl2) :: [])))) -> + CT_elim (c1, sl, CT_using (c2, sl2)) + | "Case", ((Targ_command c1) :: ((Targ_spec_list sl) :: [])) -> + CT_casetac (c1, sl) + | "Induction", ((Targ_ident id) :: []) -> + CT_induction (CT_coerce_ID_to_ID_OR_INT id) + | "Induction", ((Targ_int n) :: []) -> + CT_induction (CT_coerce_INT_to_ID_OR_INT n) + | "Destruct", ((Targ_ident id) :: []) -> + CT_destruct (CT_coerce_ID_to_ID_OR_INT id) + | "Destruct", ((Targ_int n) :: []) -> + CT_destruct (CT_coerce_INT_to_ID_OR_INT n) + | "Cut", ((Targ_command c) :: []) -> CT_cut c + | "CutAndApply", ((Targ_command c) :: []) -> CT_use c + | "DecomposeThese", ((Targ_id_list l) :: ((Targ_command c) :: [])) -> + (match l with + CT_id_list (id :: l') -> + CT_decompose_list( + CT_id_ne_list(id,l'),c) + | _ -> xlate_error "DecomposeThese : empty list of identifiers?") + | "Clear", [id_list] -> + (match id_list with + Targ_id_list(CT_id_list(id::idl)) -> + 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] -> + CT_inversion (compute_INV_TYPE_from_string s, id, CT_id_list []) + | "InvIn", ((Targ_ident (CT_ident s))::((Targ_ident id) :: idlist)) -> + CT_inversion + (compute_INV_TYPE_from_string s, id, + CT_id_list (List.map strip_targ_ident idlist)) + | "DInv", ((Targ_ident (CT_ident s))::((Targ_ident id) :: [])) -> + CT_depinversion + (compute_INV_TYPE_from_string s, id, ctv_FORMULA_OPT_NONE) + | "DInvWith", ((Targ_ident (CT_ident s)):: + ((Targ_ident id) :: ((Targ_command c) :: []))) -> + CT_depinversion + (compute_INV_TYPE_from_string s, id, CT_coerce_FORMULA_to_FORMULA_OPT c) + | "UseInversionLemma", ((Targ_ident id) :: ((Targ_command c) :: [])) -> + CT_use_inversion (id, c, CT_id_list []) + | "UseInversionLemmaIn", ((Targ_ident id) :: ((Targ_command c) :: idlist)) -> + CT_use_inversion (id, c, CT_id_list (List.map strip_targ_ident idlist)) + | "Omega", [] -> CT_omega + | "APP", (Targ_ident id)::l -> + CT_user_tac (id, CT_targ_list (List.map coerce_iTARG_to_TARG l)) + | s, l -> + CT_user_tac (CT_ident s, CT_targ_list (List.map coerce_iTARG_to_TARG l)) +and (xlate_context_rule: Coqast.t -> ct_CONTEXT_RULE) = + function + | Node(_, "MATCHCONTEXTRULE", parts) -> + let rec xlate_ctxt_rule_aux = function + [concl_pat; tac] -> + [], xlate_context_pattern concl_pat, xlate_tactic tac + | Node(_,"MATCHCONTEXTHYPS", hyp_parts)::b -> + let hyps, cpat, tactic = xlate_ctxt_rule_aux b in + (xlate_match_context_hyps hyp_parts)::hyps, cpat, tactic + | _ -> 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;; + +let strip_varg_int = + function + | Varg_int n -> n + | _ -> xlate_error "strip vernac: non-integer argument";; + +let strip_varg_string = + function + | Varg_string str -> str + | _ -> xlate_error "strip vernac: non-string argument";; + +let strip_varg_ident = + function + | Varg_ident id -> id + | _ -> xlate_error "strip vernac: non-ident argument";; + +let strip_varg_binder = + function + | Varg_binder n -> n + | _ -> xlate_error "strip vernac: non-binder argument";; + +let xlate_thm x = CT_thm (match x with + | "THEOREM" -> "Theorem" + | "REMARK" -> "Remark" + | "LEMMA" -> "Lemma" + | "FACT" -> "Fact" + | _ -> xlate_error "xlate_thm");; + +let xlate_defn x = CT_defn (match x with + | "DEFINITION" -> "Definition" + | "LOCAL" -> "Local" + | "OBJECT" -> "@Definition" + | "LOBJECT" -> "@Local" + | "OBJCOERCION" -> "@Coercion" + | "LOBJCOERCION" -> "LOBJCOERCION" + | "SUBCLASS" -> "SubClass" + | "LSUBCLASS" -> "LSUBCLASS" + | "COERCION" -> "Coercion" + | "LCOERCION" -> "LCOERCION" + | _ -> xlate_error "xlate_defn");; + +let xlate_defn_or_thm s = + try CT_coerce_THM_to_DEFN_OR_THM (xlate_thm s) + with + | _ -> CT_coerce_DEFN_to_DEFN_OR_THM (xlate_defn s);; + +let xlate_var x = CT_var (match x with + | "HYPOTHESES" -> "Hypothesis" + | "HYPOTHESIS" -> "Hypothesis" + | "VARIABLE" -> "Variable" + | "VARIABLES" -> "Variable" + | "AXIOM" -> "Axiom" + | "PARAMETER" -> "Parameter" + | "PARAMETERS" -> "Parameter" + | (*backwards compatible with 14a leave for now *) + "Axiom" as s -> s + | "Parameter" as s -> s + | _ -> xlate_error "xlate_var");; + +let xlate_dep = + function + | "DEP" -> CT_dep "Induction for" + | "NODEP" -> CT_dep "Minimality for" + | _ -> xlate_error "xlate_dep";; + +let xlate_locn = + function + | Varg_int n -> CT_coerce_INT_to_INT_OR_LOCN n + | Varg_string (CT_string "top") -> + CT_coerce_LOCN_to_INT_OR_LOCN (CT_locn "top") + | Varg_string (CT_string "prev") -> + CT_coerce_LOCN_to_INT_OR_LOCN (CT_locn "prev") + | Varg_string (CT_string "next") -> + CT_coerce_LOCN_to_INT_OR_LOCN (CT_locn "next") + | _ -> xlate_error "xlate_locn";; + +let xlate_check = + function + | "CHECK" -> "Check" + | "PRINTTYPE" -> "Type" + | _ -> xlate_error "xlate_check";; + +let build_constructors l = + let strip_coerce = + function + | CT_coerce_ID_to_ID_OPT id -> id + | _ -> xlate_error "build_constructors" in + let rec rebind = + function + | [] -> [] + | (CT_binder ((CT_id_opt_ne_list (id, ids)), c)) :: l -> + (List.map (function id_opt -> CT_constr (strip_coerce id_opt, c)) + (id::ids)) @ rebind l in + CT_constr_list (rebind l);; + +let build_record_field_list l = + let build_record_field = + function + | Varg_varglist ((Varg_string (CT_string "")) :: + ((Varg_ident id) :: (c :: []))) -> + CT_coerce_CONSTR_to_RECCONSTR (CT_constr (id, coerce_iVARG_to_FORMULA c)) + | Varg_varglist ((Varg_string (CT_string "COERCION")) :: + ((Varg_ident id) :: (c :: []))) -> + CT_constr_coercion (id, coerce_iVARG_to_FORMULA c) + | _ -> xlate_error "unexpected field in build_record_field_list" in + CT_recconstr_list (List.map build_record_field l);; + +let xlate_ast = + let rec xlate_ast_aux = + function + | Node (_, s, tl) -> + CT_astnode (CT_ident s, CT_ast_list (List.map xlate_ast_aux tl)) + | Nvar (_, s) -> + CT_coerce_ID_OR_STRING_to_AST + (CT_coerce_STRING_to_ID_OR_STRING (CT_string s)) + | Slam (_, (Some s), t) -> + CT_astslam (CT_coerce_ID_to_ID_OPT (CT_ident s), xlate_ast_aux t) + | Slam (_, None, t) -> CT_astslam (ctv_ID_OPT_NONE, xlate_ast_aux t) + | Num (_, i) -> failwith "Numbers not treated in xlate_ast" + | Id (_, s) -> + CT_coerce_ID_OR_STRING_to_AST + (CT_coerce_STRING_to_ID_OR_STRING (CT_string s)) + | Str (_, s) -> + CT_coerce_ID_OR_STRING_to_AST + (CT_coerce_STRING_to_ID_OR_STRING (CT_string s)) + | Dynamic(_,_) -> failwith "Dynamics not treated in xlate_ast" + | Path (_, sl, s) -> + CT_astpath + (CT_id_list (List.map (function s -> CT_ident s) sl), CT_ident s) in + xlate_ast_aux;; + +let get_require_flags impexp spec = + let ct_impexp = + match impexp with + | CT_string "IMPORT" -> CT_import + | CT_string "EXPORT" -> CT_export + | CT_string s -> xlate_error ("unexpected Require import flag " ^ s) in + let ct_spec = + match spec with + | CT_string "UNSPECIFIED" -> ctv_SPEC_OPT_NONE + | CT_string "SPECIFICATION" -> CT_spec + | CT_string "IMPLEMENTATION" -> ctv_SPEC_OPT_NONE + | CT_string s -> xlate_error ("unexpected Require specification flag " ^ s) in + ct_impexp, ct_spec;; + +let cvt_optional_eval_for_definition c1 optional_eval = + match optional_eval with + 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, + red_com, + c1)) + | _ -> xlate_error + "bad extra argument (tactic?) for Definition";; + +let rec cvt_varg = + function + | Node (_, "VERNACARGLIST", l) -> Varg_varglist (List.map cvt_varg l) + | Node (_, "VERNACCALL", ((Str (_, na)) :: l)) -> + Varg_call (CT_ident na, List.map cvt_varg l) + | Node (_, "VERNACCALL", ((Id (_, na)) :: l)) -> + Varg_call (CT_ident na, List.map cvt_varg l) + | Node (_, "QUALIDARG", _) as it -> + (match qualid_to_ct_ID it with + Some x -> Varg_ident x + | None -> assert false) + | Nvar (_, id) -> Varg_ident (CT_ident id) + | Str (_, s) -> Varg_string (CT_string s) + | Num (_, n) -> Varg_int (CT_int n) + | Node (_, "NONE", []) -> Varg_none + | Node (_, "CONSTR", ((Node (_, "PROP", ((Id (_, c)) :: []))) :: [])) -> + (match c with + | "Pos" -> Varg_sorttype (CT_sortc "Set") + | "Null" -> Varg_sorttype (CT_sortc "Prop") + | _ -> xlate_error "cvt_varg : PROP : Failed match ") + | Node (_, "CONSTR", ((Node (_, "TYPE", [])) :: [])) -> + Varg_sorttype (CT_sortc "Type") + | Node (_, "CONSTR", [c]) -> Varg_constr (xlate_formula c) + | Node (_, "CONSTRLIST", cs) -> Varg_constrlist (List.map xlate_formula cs) + | Node (_, "TACTIC", [c]) -> Varg_tactic (xlate_tactic c) + | Node (_, "BINDER", args) as arg -> + Varg_binder(cvt_binder xlate_formula arg) + | Node (_, "BINDERLIST", l) as arg -> + Varg_binderlist(cvt_binders xlate_formula arg) + | Node (_, "BINDERS", l) as arg -> + Varg_binderlist(cvt_binders xlate_formula arg) + | Node (_, "NUMBERLIST", ln) -> + Varg_intlist (CT_int_list (List.map xlate_int ln)) + | Node (_, "AST", [Node(_, "ASTACT", [ + Node(_, "ASTLIST", [Node(_, "TACTICLIST", _) as it])])]) -> + Varg_tactic(xlate_tactic it) + | Node (_, "AST", (a :: [])) -> Varg_ast (xlate_ast a) + | Node (_, "ASTLIST", al) -> + Varg_astlist (CT_ast_list (List.map xlate_ast al)) + | Node (_, "TACTIC_ARG", (targ :: [])) -> Varg_tactic_arg (cvt_arg targ) + | Node (_, s, _) as it -> failwith ("cvt_varg : " ^ s ^ " at location " ^ + (string_of_node_loc it)) + | the_node -> failwith ("cvt_varg : " ^ (string_of_node_loc the_node)) +and xlate_vernac = + function + | Node(_, "TACDEF", [Nvar(_,id); + Node(_,"AST", + [Node(_,"FUN", + [Node(_,"FUNVAR", + largs); + tac])])]) -> + CT_tactic_definition(CT_ident id, + CT_id_list(List.map xlate_id largs), + xlate_tactic tac) + | Node(_, "TACDEF", Nvar(_, id):: + ((Node(_, "AST",[Node(_, "REC", [vc])])::tl) as the_list)) -> + let x_rec_tacs = + List.fold_right + (fun e res -> match e with + Node(_,"AST", + [Node(_,"REC", + [Node(_,"RECCLAUSE", [Nvar(_,x); + Node(_, "FUNVAR", argl); + tac])])]) -> + let fst, rest = xlate_largs_to_id_unit argl in + CT_rec_tactic_fun(CT_ident x, + CT_id_unit_list(fst, rest), + xlate_tactic tac)::res + | _ -> res) the_list [] in + let fst, others = match x_rec_tacs with + fst::others -> fst, others + | _ -> assert false in + CT_rec_tactic_definition(CT_rec_tactic_fun_list(fst, others)) + | Node(_, "TACDEF", [Nvar(_,id);Node(_,"AST",[tac])]) -> + CT_tactic_definition(CT_ident id, CT_id_list[], xlate_tactic tac) + | Node (_, s, l) -> + (match s, List.map cvt_varg l with + | "LoadFile", ((Varg_string verbose) :: ((Varg_string s) :: [])) -> + CT_load ( + (match verbose with + | CT_string "" -> CT_coerce_NONE_to_VERBOSE_OPT CT_none + | CT_string "Verbose" as it -> CT_verbose + | CT_string s -> + xlate_error ("expecting the keyword Verbose only :" ^ s)), + CT_coerce_STRING_to_ID_OR_STRING s) + | "Eval", + ((Varg_tactic_arg (Targ_redexp tac)) :: ((Varg_constr f) :: tail)) -> + let numopt = + match tail with + | (Varg_int i) :: [] -> CT_coerce_INT_to_INT_OPT i + | [] -> CT_coerce_NONE_to_INT_OPT CT_none + | _ -> xlate_error "Eval expects an optional integer" in + CT_coerce_EVAL_CMD_to_COMMAND(CT_eval (numopt, tac, f)) + | "PWD", [] -> CT_pwd + | "CD", ((Varg_string str) :: []) -> CT_cd (ctf_STRING_OPT_SOME str) + | "CD", [] -> CT_cd ctf_STRING_OPT_NONE + | "ADDPATH", ((Varg_string str) :: []) -> CT_addpath str + | "RECADDPATH", ((Varg_string str) :: []) -> CT_recaddpath str + | "DELPATH", ((Varg_string str) :: []) -> CT_delpath str + | "PrintPath", [] -> CT_print_loadpath + | "QUIT", [] -> CT_quit + | (*ML commands *) + "AddMLPath", ((Varg_string str) :: []) -> CT_ml_add_path str + | "RecAddMLPath", ((Varg_string str) :: []) -> CT_rec_ml_add_path str + | "PrintMLPath", [] -> CT_ml_print_path + | "PrintMLModules", [] -> CT_ml_print_modules + | "DeclareMLModule", (str :: l) -> + CT_ml_declare_modules + (CT_string_ne_list (strip_varg_string str, List.map strip_varg_string l)) + | "GOAL", [] -> CT_proof_no_op + | "GOAL", (c :: []) -> CT_coerce_THEOREM_GOAL_to_COMMAND (CT_goal (coerce_iVARG_to_FORMULA c)) + | (*My attempt at getting all variants of Abort to use abort node *) + "ABORT", ((Varg_ident id) :: []) -> CT_abort (ctf_ID_OPT_OR_ALL_SOME id) + | "ABORT", [] -> CT_abort ctv_ID_OPT_OR_ALL_NONE + | "ABORTALL", [] -> CT_abort ctv_ID_OPT_OR_ALL_ALL + | (*formerly | ("ABORTALL", []) -> ident_vernac "Abort All" *) + "RESTART", [] -> CT_restart + | "PROOF", (c :: []) -> CT_proof (coerce_iVARG_to_FORMULA c) + | "SOLVE", ((Varg_int n) :: ((Varg_tactic tcom) :: [])) -> + CT_solve (n, tcom) + | "FOCUS", [] -> CT_focus (CT_coerce_NONE_to_INT_OPT CT_none) + | "FOCUS", [Varg_int n] -> CT_focus (CT_coerce_INT_to_INT_OPT n) + | "UNFOCUS", [] -> CT_unfocus + | "HintRewrite", [orient; formula_list; Varg_ident base; Varg_tactic t] -> + let ct_orient = match orient with + | Varg_string (CT_string "LR") -> CT_lr + | Varg_string (CT_string "Rl") -> CT_rl + | _ -> assert false in + let f_ne_list = match formula_list with + Varg_constrlist (fst::rest) -> CT_formula_ne_list(fst,rest) + | _ -> assert false in + CT_hintrewrite(ct_orient, f_ne_list, base, t) + | "HintResolve", + ((Varg_ident id_name) :: + ((Varg_varglist dbnames) :: ((Varg_constr c)::[]))) -> + CT_hint(id_name, + CT_id_list(List.map coerce_iVARG_to_ID + dbnames), CT_resolve(c)) + | "HintUnfold", + ((Varg_ident id_name) :: + ((Varg_varglist dbnames) :: ((Varg_ident c)::[]))) -> + CT_hint(id_name, + CT_id_list(List.map coerce_iVARG_to_ID + dbnames), CT_unfold_hint(c)) + | "HintConstructors", + ((Varg_ident id_name) :: + ((Varg_varglist dbnames) :: ((Varg_ident c)::[]))) -> + CT_hint(id_name, + CT_id_list(List.map coerce_iVARG_to_ID + dbnames), CT_constructors(c)) + | "HintImmediate", + ((Varg_ident id_name) :: + ((Varg_varglist dbnames) :: ((Varg_constr c)::[]))) -> + CT_hint(id_name, + CT_id_list(List.map coerce_iVARG_to_ID + dbnames), CT_immediate(c)) + | "HintExtern", + [Varg_ident id_name; + Varg_varglist dbnames; + Varg_int n; + Varg_constr c; + Varg_tactic t] -> + CT_hint(id_name, CT_id_list (List.map coerce_iVARG_to_ID dbnames), + CT_extern(n, c, t)) + | "HintsResolve", + (Varg_varglist(dbnames)::(Varg_ident n1) :: names) -> + CT_hints(CT_ident "Resolve", + CT_id_ne_list(n1, List.map coerce_iVARG_to_ID names), + CT_id_list(List.map coerce_iVARG_to_ID dbnames)) + | "HintsImmediate", + (Varg_varglist(dbnames)::(Varg_ident n1) :: names) -> + CT_hints(CT_ident "Immediate", + CT_id_ne_list(n1, List.map coerce_iVARG_to_ID names), + CT_id_list(List.map coerce_iVARG_to_ID dbnames)) + | "HintsUnfold", + (Varg_varglist(dbnames)::(Varg_ident n1) :: names) -> + CT_hints(CT_ident "Unfold", + CT_id_ne_list(n1, List.map coerce_iVARG_to_ID names), + CT_id_list(List.map coerce_iVARG_to_ID dbnames)) + | "BY", ((Varg_tactic tcom) :: []) -> xlate_error "BY not implemented" + | (*My attempt to get all variants of Save to use the same node *) + "SaveNamed", [] -> + CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Theorem"), ctv_ID_OPT_NONE) + | "DefinedNamed", [] -> + CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Definition"), ctv_ID_OPT_NONE) + | "SaveAnonymousThm", ((Varg_ident s) :: []) -> + CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Theorem"), ctf_ID_OPT_SOME s) + | "SaveAnonymousRmk", ((Varg_ident s) :: []) -> + CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Remark"), ctf_ID_OPT_SOME s) + | "TRANSPARENT", (id :: idl) -> + CT_transparent(CT_id_ne_list(strip_varg_ident id, + List.map strip_varg_ident idl)) + | "OPAQUE", (id :: idl) + -> CT_opaque (CT_id_ne_list(strip_varg_ident id, + List.map strip_varg_ident idl)) + | "WriteModule", ((Varg_ident id) :: []) -> + CT_write_module (id, CT_coerce_NONE_to_STRING_OPT CT_none) + | "UNDO", ((Varg_int n) :: []) -> CT_undo (CT_coerce_INT_to_INT_OPT n) + | "SHOW", [] -> CT_show_goal (CT_coerce_NONE_to_INT_OPT CT_none) + | "SHOW", ((Varg_int n) :: []) -> CT_show_goal (CT_coerce_INT_to_INT_OPT n) + | "ShowNode", [] -> CT_show_node + | "ShowProof", [] -> CT_show_proof + | "ShowTree", [] -> CT_show_tree + | "ShowScript", [] -> CT_show_script + | "ShowProofs", [] -> CT_show_proofs + | "SHOWIMPL", [] -> CT_show_implicits + | "Go", (arg :: []) -> CT_go (xlate_locn arg) + | "ExplainProof", l -> + CT_explain_proof (CT_int_list (List.map strip_varg_int l)) + | "ExplainProofTree", l -> + CT_explain_prooftree (CT_int_list (List.map strip_varg_int l)) + | "PrintHint", [] -> CT_print_hint (CT_coerce_NONE_to_ID_OPT CT_none) + | "PrintHintDb", [Varg_ident id] -> CT_print_hintdb id + | "CheckGuard", [] -> CT_guarded + | "PrintHintId", ((Varg_ident id) :: []) -> + CT_print_hint (CT_coerce_ID_to_ID_OPT id) + | "PrintAll", [] -> CT_print_all + | "PrintId", ((Varg_ident id) :: []) -> CT_print_id id + | "PrintOpaqueId", ((Varg_ident id) :: []) -> CT_print_opaqueid id + | "PrintSec", ((Varg_ident id) :: []) -> CT_print_section id + | "PrintStates", [] -> CT_print_states + | "PrintModules", [] -> CT_print_modules + | "PrintGrammar", ((Varg_ident phylum) :: ((Varg_ident name) :: [])) -> + CT_print_grammar CT_grammar_none + | "BeginModule", ((Varg_ident id) :: []) -> CT_module id + | "BeginSection", ((Varg_ident id) :: []) -> + CT_coerce_SECTION_BEGIN_to_COMMAND (CT_section id) + | "EndSection", ((Varg_ident id) :: []) -> CT_section_end id + | "StartProof", + ((Varg_string (CT_string kind)) :: ((Varg_ident s) :: (c :: []))) -> + CT_coerce_THEOREM_GOAL_to_COMMAND( + CT_theorem_goal (xlate_defn_or_thm kind, s, coerce_iVARG_to_FORMULA c)) + | (*My attempt: suspend and resume as separate nodes *) + "SUSPEND", [] -> CT_suspend + | "RESUME", ((Varg_ident id) :: []) -> CT_resume (ctf_ID_OPT_SOME id) + | "RESUME", [] -> CT_resume ctv_ID_OPT_NONE + | (*formerly | ("SUSPEND", []) -> suspend(CT_true) + | ("RESUME", []) -> suspend(CT_false) + *) + "DEFINITION", + (* reference : toplevel/vernacentries.ml *) + (Varg_string (CT_string kind):: Varg_ident s :: Varg_constr c :: rest) -> + let typ_opt, red_option = match rest with + | [] -> ctv_FORMULA_OPT_NONE, None + | [Varg_constr b] -> CT_coerce_FORMULA_to_FORMULA_OPT b, None + | [Varg_tactic_arg r] -> ctv_FORMULA_OPT_NONE, Some r + | [Varg_constr b; Varg_tactic_arg r] -> + CT_coerce_FORMULA_to_FORMULA_OPT b, Some r + | _ -> assert false in + CT_definition + (xlate_defn kind, s, + cvt_optional_eval_for_definition c red_option, typ_opt) + | "VARIABLE", + ((Varg_string (CT_string kind)) :: ((Varg_binderlist b) :: [])) -> + CT_variable (xlate_var kind, b) + | "PARAMETER", + ((Varg_string (CT_string kind)) :: ((Varg_binderlist b) :: [])) -> + CT_variable (xlate_var kind, b) + | "Check", ((Varg_string (CT_string kind)) :: (c :: [])) -> + CT_check (coerce_iVARG_to_FORMULA c) + | "SEARCH", (Varg_ident id):: l -> + (match l with + | [] -> CT_search(id, CT_coerce_NONE_to_IN_OR_OUT_MODULES CT_none) + | (Varg_string (CT_string x))::(Varg_ident m1)::l1 -> + let l2 = CT_id_ne_list(m1, List.map coerce_iVARG_to_ID l1) in + let modifier = + (match x with + | "inside" -> CT_in_modules l2 + | "outside" -> CT_out_modules l2 + | _ -> xlate_error "bad extra argument for Search") in + CT_search(id, modifier) + | _ -> xlate_error "bad argument list for Search") + | "INSPECT", ((Varg_int n) :: []) -> CT_inspect n + | (*Record from tactics/Record.v *) + "RECORD", + ((Varg_string coercion_or_not) :: ((Varg_ident s) :: + ((Varg_binderlist binders) :: + ((Varg_sorttype c) :: + ((Varg_varglist rec_constructor_or_none) :: + ((Varg_varglist field_list) :: [])))))) -> + let record_constructor = + match rec_constructor_or_none with + | [] -> CT_coerce_NONE_to_ID_OPT CT_none + | (Varg_ident id) :: [] -> CT_coerce_ID_to_ID_OPT id + | _ -> xlate_error "unexpected record constructor" in + CT_record + ((match coercion_or_not with CT_string "" -> + CT_coerce_NONE_to_COERCION_OPT(CT_none) + | _ -> CT_coercion_atm), + s, binders, c, record_constructor, + build_record_field_list field_list) + | (*Inversions from tactics/Inv.v *) + "MakeSemiInversionLemmaFromHyp", + ((Varg_int n) :: ((Varg_ident id1) :: ((Varg_ident id2) :: []))) -> + CT_derive_inversion + (CT_inv_regular, CT_coerce_INT_to_INT_OPT n, id1, id2) + | "MakeInversionLemmaFromHyp", + ((Varg_int n) :: ((Varg_ident id1) :: ((Varg_ident id2) :: []))) -> + CT_derive_inversion + (CT_inv_clear, + CT_coerce_INT_to_INT_OPT n, id1, id2) + | "MakeSemiInversionLemma", + ((Varg_ident id) :: (c :: ((Varg_sorttype sort) :: []))) -> + CT_derive_inversion_with + (CT_inv_regular, id, coerce_iVARG_to_FORMULA c, sort) + | "MakeInversionLemma", + ((Varg_ident id) :: (c :: ((Varg_sorttype sort) :: []))) -> + CT_derive_inversion_with + (CT_inv_clear, id, + coerce_iVARG_to_FORMULA c, sort) + | "MakeDependentSemiInversionLemma", + ((Varg_ident id) :: (c :: ((Varg_sorttype sort) :: []))) -> + CT_derive_depinversion + (CT_inv_regular, id, coerce_iVARG_to_FORMULA c, sort) + | "MakeDependentInversionLemma", + ((Varg_ident id) :: (c :: ((Varg_sorttype sort) :: []))) -> + CT_derive_depinversion + (CT_inv_clear, id, coerce_iVARG_to_FORMULA c, sort) + | + "ONEINDUCTIVE", + ((Varg_string (CT_string f)) :: + ((Varg_ident s) :: + (c :: + ((Varg_binderlist binders) :: + ((Varg_binderlist (CT_binder_list constructors)) :: []))))) -> + CT_mind_decl + (CT_co_ind f, + CT_ind_spec_list( + [CT_ind_spec(s,binders, coerce_iVARG_to_FORMULA c, + build_constructors constructors)])) + | "OLDMUTUALINDUCTIVE", + [Varg_binderlist binders; Varg_string(CT_string f); + Varg_varglist lmi] -> + let strip_mutind = + function + | Varg_varglist([Varg_ident s;c; + Varg_binderlist (CT_binder_list constructors)]) -> + CT_ind_spec(s, binders, coerce_iVARG_to_FORMULA c, + build_constructors constructors) + | _ -> xlate_error "mutual inductive, old style" in + CT_mind_decl(CT_co_ind f, CT_ind_spec_list(List.map strip_mutind lmi)) + | "MUTUALINDUCTIVE", + ((Varg_string (CT_string co_or_ind)) :: + ((Varg_varglist lmi) ::[])) -> + let strip_mutind = + function + | Varg_varglist ((Varg_ident s) :: + (c :: + ((Varg_binderlist parameters) :: + ((Varg_binderlist (CT_binder_list constructors)) + :: [])))) -> + CT_ind_spec + (s, parameters, coerce_iVARG_to_FORMULA c, + build_constructors constructors) + | _ -> xlate_error "mutual inductive" in + CT_mind_decl + (CT_co_ind co_or_ind, CT_ind_spec_list (List.map strip_mutind lmi)) + | "MUTUALRECURSIVE", ((Varg_varglist (lm :: lmi)) :: []) -> + let strip_mutrec = + function + | Varg_varglist ((Varg_ident fid) :: + ((Varg_binderlist (CT_binder_list (b :: bl))) :: + (arf :: (ardef :: [])))) -> + CT_fix_rec + (fid, CT_binder_ne_list (b, bl), coerce_iVARG_to_FORMULA arf, + coerce_iVARG_to_FORMULA ardef) + | _ -> xlate_error "mutual recursive" in + CT_fix_decl + (CT_fix_rec_list (strip_mutrec lm, List.map strip_mutrec lmi)) + | "MUTUALCORECURSIVE", ((Varg_varglist (lm :: lmi)) :: []) -> + let strip_mutcorec = + function + | Varg_varglist ((Varg_ident fid) :: (arf :: (ardef :: []))) -> + CT_cofix_rec + (fid, coerce_iVARG_to_FORMULA arf, coerce_iVARG_to_FORMULA ardef) + | _ -> xlate_error "mutual corecursive" in + CT_cofix_decl + (CT_cofix_rec_list (strip_mutcorec lm, List.map strip_mutcorec lmi)) + | "INDUCTIONSCHEME", ((Varg_varglist (lm :: lmi)) :: []) -> + let strip_ind = + function + | Varg_varglist ((Varg_ident fid) :: + ((Varg_string (CT_string depstr)) :: + (inde :: ((Varg_sorttype sort) :: [])))) -> + CT_scheme_spec + (fid, xlate_dep depstr, coerce_iVARG_to_FORMULA inde, sort) + | _ -> xlate_error "induction scheme" in + CT_ind_scheme + (CT_scheme_spec_list (strip_ind lm, List.map strip_ind lmi)) + | + "SyntaxMacro", ((Varg_ident id) :: (c :: [])) -> + CT_syntax_macro + (id, coerce_iVARG_to_FORMULA c, CT_coerce_NONE_to_INT_OPT CT_none) + | "SyntaxMacro", ((Varg_ident id) :: (c :: ((Varg_int n) :: []))) -> + CT_syntax_macro + (id, coerce_iVARG_to_FORMULA c, CT_coerce_INT_to_INT_OPT n) + | "ABSTRACTION", ((Varg_ident id) :: (c :: l)) -> + CT_abstraction + (id, coerce_iVARG_to_FORMULA c, CT_int_list (List.map strip_varg_int l)) + | "Require", + ((Varg_string impexp) :: + ((Varg_string spec) :: ((Varg_ident id) :: []))) -> + let ct_impexp, ct_spec = get_require_flags impexp spec in + CT_require (ct_impexp, ct_spec, id, CT_coerce_NONE_to_STRING_OPT CT_none) + | "RequireFrom", + ((Varg_string impexp) :: + ((Varg_string spec) :: + ((Varg_ident id) :: ((Varg_string filename) :: [])))) -> + let ct_impexp, ct_spec = get_require_flags impexp spec in + CT_require + (ct_impexp, ct_spec, id, CT_coerce_STRING_to_STRING_OPT filename) + | "SYNTAX", ((Varg_ident phylum) :: ((Varg_ident s) :: (x :: (y :: l)))) -> + xlate_error "SYNTAX not implemented" + | (*Two versions of the syntax node with and without the binder list. *) + (*Need to update the metal file and ascent.mli first! + | ("SYNTAX", [Varg_ident phy; Varg_ident s; spatarg; unparg; blist]) -> + (syntaxop phy s spatarg unparg blist) + | ("SYNTAX", [Varg_ident phy; Varg_ident s; spatarg; unparg]) -> + (syntaxop phy s spatarg unparg + coerce_ID_OPT_to_FORMULA_OPT(CT_coerce_NONE_to_ID_OPT(CT_none)))*) + "TOKEN", ((Varg_string str) :: []) -> CT_token str + | "INFIX", + ((Varg_ast (CT_coerce_ID_OR_STRING_to_AST + (CT_coerce_STRING_to_ID_OR_STRING + (CT_string str_assoc)))) :: + ((Varg_int n) :: ((Varg_string str) :: ((Varg_ident id) :: [])))) -> + CT_infix ( + (match str_assoc with + | "LEFTA" -> CT_lefta + | "RIGHTA" -> CT_righta + | "NONA" -> CT_nona + | "NONE" -> CT_coerce_NONE_to_ASSOC CT_none + | _ -> xlate_error "infix1"), n, str, id) + | "GRAMMAR", (ge :: []) -> xlate_error "GRAMMAR not implemented" + | "SETUNDO", ((Varg_int n) :: []) -> CT_setundo n + | "UNSETUNDO", [] -> CT_unsetundo + | "SETHYPSLIMIT", ((Varg_int n) :: []) -> CT_sethyp n + | "UNSETHYPSLIMIT", [] -> CT_unsethyp + | "COERCION", + ((Varg_string s) :: + ((Varg_string (CT_string str)) :: + ((Varg_ident id1) :: ((Varg_ident id2) :: ((Varg_ident id3) :: []))))) -> + let id_opt = + match str with + | "IDENTITY" -> CT_identity + | "" -> CT_coerce_NONE_to_IDENTITY_OPT CT_none + | _ -> xlate_error "unknown flag for a coercion" in + let local_opt = + match str with + | "LOCAL" -> CT_local + | "" -> CT_coerce_NONE_to_LOCAL_OPT CT_none + | _ -> xlate_error "unknown flag for a coercion" in + CT_coercion (local_opt, id_opt, id1, id2, id3) + | "CLASS", (_ :: ((Varg_ident id1) :: [])) -> CT_class id1 + | "PrintGRAPH", [] -> CT_print_graph + | "PrintCLASSES", [] -> CT_print_classes + | "PrintCOERCIONS", [] -> CT_print_coercions + | "PrintPATH", ((Varg_ident id1) :: ((Varg_ident id2) :: [])) -> + CT_print_path (id1, id2) + | "SelectLanguageText", ((Varg_ident id) :: []) -> CT_set_natural id + | "PrintText", ((Varg_ident id) :: []) -> CT_print_natural id + | "AddTextParamOmit", ((Varg_ident id) :: []) -> + CT_add_natural_feature (CT_implicit, id) + | "MemTextParamOmit", ((Varg_ident id) :: []) -> + CT_test_natural_feature (CT_implicit, id) + | "RemoveTextParamOmit", ((Varg_ident id) :: []) -> + CT_remove_natural_feature (CT_implicit, id) + | "PrintTextParamOmit", [] -> CT_print_natural_feature CT_implicit + | "AddTextParamRecSub", ((Varg_ident id) :: []) -> + CT_add_natural_feature (CT_contractible, id) + | "MemTextParamRecSub", ((Varg_ident id) :: []) -> + CT_test_natural_feature (CT_contractible, id) + | "RemoveTextParamRecSub", ((Varg_ident id) :: []) -> + CT_remove_natural_feature (CT_contractible, id) + | "PrintTextParamRecSub", [] -> CT_print_natural_feature CT_contractible + | "AddTextParamImmediate", ((Varg_ident id) :: []) -> + CT_add_natural_feature (CT_nat_transparent, id) + | "MemTextParamImmediate", ((Varg_ident id) :: []) -> + CT_test_natural_feature (CT_nat_transparent, id) + | "RemoveTextParamImmediate", ((Varg_ident id) :: []) -> + CT_remove_natural_feature (CT_nat_transparent, id) + | "PrintTextParamImmediate", [] -> + CT_print_natural_feature CT_nat_transparent + | "ResetName", ((Varg_ident id) :: []) -> CT_reset id + | "ResetSection", ((Varg_ident id) :: []) -> CT_reset_section id + | "ResetInitial", [] -> CT_restore_state (CT_ident "Initial") + | "OmegaFlag", ((Varg_string (CT_string s)) :: []) -> + let fst_code = code (get s 0) in + let + set_or_unset, tail = + if fst_code = code_plus then (CT_set, sub s 1 (length s - 1)) + else if fst_code = code_minus then (CT_unset, sub s 1 (length s - 1)) + else (CT_switch, s) in + (match tail with + | "time" -> CT_omega_flag (set_or_unset, CT_flag_time) + | "action" -> CT_omega_flag (set_or_unset, CT_flag_action) + | "system" -> CT_omega_flag (set_or_unset, CT_flag_system) + | _ -> + CT_omega_flag + (set_or_unset, CT_coerce_STRING_to_OMEGA_FEATURE (CT_string s))) + | s, l -> + CT_user_vernac + (CT_ident s, CT_varg_list (List.map coerce_iVARG_to_VARG l))) + | _ -> xlate_error "xlate_vernac";; + +let xlate_vernac_list = + function + | Node (_, "vernac_list", (v :: l)) -> + CT_command_list (xlate_vernac v, List.map xlate_vernac l) + | _ -> xlate_error "xlate_command_list";; diff --git a/contrib/interface/xlate.mli b/contrib/interface/xlate.mli new file mode 100644 index 000000000..5613dd095 --- /dev/null +++ b/contrib/interface/xlate.mli @@ -0,0 +1,14 @@ +open Ascent;; + +val xlate_vernac : Coqast.t -> ct_COMMAND;; +val xlate_tactic : Coqast.t -> ct_TACTIC_COM;; +val xlate_formula : Coqast.t -> ct_FORMULA;; +val xlate_int : Coqast.t -> ct_INT;; +val xlate_string : Coqast.t -> ct_STRING;; +val xlate_id : Coqast.t -> ct_ID;; +val xlate_vernac_list : Coqast.t -> ct_COMMAND_LIST;; + +val g_nat_syntax_flag : bool ref;; +val set_flags : (unit -> unit) ref;; +val set_xlate_mut_stuff : (Coqast.t -> Coqast.t) -> unit;; +val declare_in_coq : (unit -> unit);; |