diff options
author | 2001-04-04 12:59:26 +0000 | |
---|---|---|
committer | 2001-04-04 12:59:26 +0000 | |
commit | 917e4b5b1f334282350278d53f3d94ecefb51b3a (patch) | |
tree | 54834c37dfb8a0b62bf60a6f5951ce6e78bb789f /contrib/interface | |
parent | 5f42f80fb84f8fa8137eb73531bcdbebc1057270 (diff) |
These files are loaded coq-interface to make a process that is "pcoq" enabled.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1539 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface')
-rw-r--r-- | contrib/interface/AddDad.v | 19 | ||||
-rw-r--r-- | contrib/interface/Centaur.v | 84 |
2 files changed, 103 insertions, 0 deletions
diff --git a/contrib/interface/AddDad.v b/contrib/interface/AddDad.v new file mode 100644 index 000000000..d22b7ed16 --- /dev/null +++ b/contrib/interface/AddDad.v @@ -0,0 +1,19 @@ +Grammar vernac vernac : ast := + add_dad_rule00 ["AddDadRule" stringarg($name) constrarg($pat) + "first_path" "second_path" tacarg($tac) "."] -> + [(AddDadRule $name $pat (NUMBERLIST) (NUMBERLIST) (TACTIC $tac))]. +Grammar vernac vernac:ast := +| add_dad_rule01 ["AddDadRule" stringarg($name) constrarg($pat) + "first_path" "second_path" ne_numarg_list($l) tacarg($tac) "."] -> + [(AddDadRule $name $pat (NUMBERLIST) (NUMBERLIST ($LIST $l)) (TACTIC $tac))] +| add_dad_rule10 ["AddDadRule" stringarg($name) constrarg($pat) + "first_path" ne_numarg_list($l) "second_path" tacarg($tac) "."] -> + [(AddDadRule $name $pat (NUMBERLIST ($LIST $l))(NUMBERLIST) (TACTIC $tac))] +| add_dad_rule11 ["AddDadRule" stringarg($name) constrarg($pat) + "first_path" ne_numarg_list($l) "second_path" ne_numarg_list($l1) + tacarg($tac) "."] -> + [(AddDadRule $name $pat (NUMBERLIST ($LIST $l))(NUMBERLIST ($LIST $l1)) + (TACTIC $tac))]. + +Grammar vernac vernac : ast := + start_dad [ "StartDad" "."] -> [(StartDad)]. diff --git a/contrib/interface/Centaur.v b/contrib/interface/Centaur.v new file mode 100644 index 000000000..ffd7d5b86 --- /dev/null +++ b/contrib/interface/Centaur.v @@ -0,0 +1,84 @@ +Declare ML Module "paths". +Declare ML Module "name_to_ast". +Declare ML Module "xlate". +Declare ML Module "vtp". +Declare ML Module "translate". +Declare ML Module "pbp". +Declare ML Module "dad". +(* +Declare ML Module "showproofutil". +Declare ML Module "showproof_ct". +Declare ML Module "showproof". +Declare ML Module "fine_search". +*) +Declare ML Module "debug_tac". +Declare ML Module "paths". +Declare ML Module "history". +Declare ML Module "centaur". +(* Require Export Illustrations. *) +Require Export AddDad. + +Grammar vernac vernac : ast := + goal_cmd [ "Goal" "Cmd" numarg($n) "with" tacarg($tac) "." ] -> + [(GOAL_CMD $n (TACTIC $tac))] +| kill_proof_after [ "Kill" "Proof" "after" numarg($n)"." ] -> [(KILL_NODE $n)] +| kill_proof_at [ "Kill" "Proof" "at" numarg($n)"." ] -> [(KILL_NODE $n)] +| kill_sub_proof [ "Kill" "SubProof" numarg($n) "." ] -> [(KILL_SUB_PROOF $n)] + +| print_past_goal [ "Print" "Past" "Goal" numarg($n) "." ] -> + [(PRINT_GOAL_AT $n) ] + +| check_in_goal [ "CHECK_IN_GOAL" numarg($n) constrarg($c) "." ] -> + [(CHECK_IN_GOAL "CHECK" $n $c)] +| eval_in_goal [ "EVAL_IN_GOAL" numarg($n) constrarg($c) "." ] -> + [(CHECK_IN_GOAL "EVAL" $n $c)] +| compute_in_goal [ "COMPUTE_IN_GOAL" numarg($n) constrarg($c) "." ] -> + [(CHECK_IN_GOAL "COMPUTE" $n $c)] +| centaur_reset [ "Centaur" "Reset" identarg($id) "." ] -> [(Centaur_Reset $id)] +| show_dad_rules [ "Show" "Dad" "Rules" "." ] -> [(Show_dad_rules)] +| start_pcoq [ "Start" "Pcoq" "Mode" "." ] -> [ (START_PCOQ) ] +| start_pcoq [ "Start" "Pcoq" "Debug" "Mode" "." ] -> [ (START_PCOQ_DEBUG) ]. +Grammar vernac ne_id_list : List := + id_one [ identarg($id)] -> [$id] + | id_more [identarg($id) ne_id_list($others)] -> [$id ($LIST $others)]. + +Grammar tactic ne_num_list : List := + ne_last [ numarg($n) ] -> [ $n ] +| ne_num_ste [ numarg($n) ne_num_list($ns) ] -> [ $n ($LIST $ns)]. + +Grammar tactic two_numarg_list : List := + two_single_and_ne [ numarg($n) "to" ne_num_list($ns)] -> + [$n (TACTIC (to)) ($LIST $ns)] +| two_rec [ numarg($n) two_numarg_list($ns)] -> [ $n ($LIST $ns)]. + +Grammar tactic simple_tactic : ast := + pbp0 [ "Pbp" ] -> [(PcoqPbp)] +| pbp1 [ "Pbp" ne_num_list($ns) ] -> + [ (PcoqPbp ($LIST $ns)) ] +| pbp2 [ "Pbp" identarg($id) ] -> [ (PcoqPbp $id) ] +| pbp3 [ "Pbp" identarg($id) ne_num_list($ns)] -> + [ (PcoqPbp $id ($LIST $ns)) ] +| dad00 [ "Dad" "to" ] -> [(Dad (TACTIC (to)))] +| dad01 [ "Dad" "to" ne_num_list($ns) ] -> + [(Dad (TACTIC (to)) ($LIST $ns))] +| dadnn [ "Dad" two_numarg_list($ns) ] -> [ (Dad ($LIST $ns)) ] +| debug_tac [ "DebugTac" tactic($tac) ] -> + [(CtDebugTac (TACTIC $tac))] +| on_then_empty [ "OnThen" tactic($tac1) tactic($tac2) ] -> + [(OnThen (TACTIC $tac1) (TACTIC $tac2))] +| on_then_ne [ "OnThen" tactic($tac1) tactic($tac2) ne_num_list($l) ] -> + [(OnThen (TACTIC $tac1) (TACTIC $tac2) ($LIST $l))] +| debug_tac2 [ "DebugTac2" tactic($tac) ] -> + [(CtDebugTac2 (TACTIC $tac))]. + + +(* Maybe we should have syntactic rules to make sur that syntax errors are + displayed with a readable syntax. It is not sure, since the error reporting + procedure changed from V6.1 and does not reprint the command anymore. *) +Grammar vernac vernac : ast := + text_proof_flag_on [ "Text" "Mode" "On" "." ] -> + [(TEXT_MODE (AST {on}))] +| text_proof_flag_on [ "Text" "Mode" "Off" "." ] -> + [(TEXT_MODE (AST {off}))]. + + |