helm/hbugs/tutors/INDEX.xml

   1 <!--
   2   Data used to fill template "hbugs_tutor.TPL.ml"
   3
   4   @ADDR@              tutor ip address
   5   @PORT@              tutor tcp port
   6   @TACTIC@            tactic to use (OCaml function, must have type
   7                       ProofEngineTypes.tactic)
   8   @HINT@              hint to be sent to client (content of Hbugs_types.Eureka
   9                       type constructor, must have type Hbugs_types.hint, see
  10                       hbugs_types.ml)
  11   @HINT_TYPE@         hint type (3rd argument of Hbugs_types.Register_tutor type
  12                       constructor, must have type Hbugs_types.hint_type)
  13   @DESCRIPTION@       human readable tutor description
  14
  15   "source" attribute  corresponding OCaml source file
  16
  17   INVARIANT:  XML element name below are lowercase version of @TAGS@ used in
  18               template
  19
  20   TODO: hint type isn't yet well formalized
  21 -->
  22
  23 <tutors>
  24
  25   <!-- DEBUGGING -->
  26 <!--
  27   <tutor source="wait_tutor.ml">
  28     <addr>127.0.0.1</addr>
  29     <port>50111</port>
  30     <tactic>Wait.wait_tac</tactic>
  31     <hint>Hbugs_types.Use_ring_Luke</hint>
  32     <hint_type>Use Ring Luke</hint_type>
  33     <description>WAIT FOREVER tutor</description>
  34   </tutor>
  35 -->
  36
  37   <tutor source="ring_tutor.ml">
  38     <addr>127.0.0.1</addr>
  39     <port>50001</port>
  40     <tactic>Ring.ring_tac</tactic>
  41     <hint>Hbugs_types.Use_ring_Luke</hint>
  42     <hint_type>Use Ring Luke</hint_type>
  43     <description>Ring tutor</description>
  44   </tutor>
  45   <tutor source="fourier_tutor.ml">
  46     <addr>127.0.0.1</addr>
  47     <port>50002</port>
  48     <tactic>FourierR.fourier_tac</tactic>
  49     <hint>Hbugs_types.Use_fourier_Luke</hint>
  50     <hint_type>Use Fourier Luke</hint_type>
  51     <description>Fourier tutor</description>
  52   </tutor>
  53   <tutor source="reflexivity_tutor.ml">
  54     <addr>127.0.0.1</addr>
  55     <port>50003</port>
  56     <tactic>EqualityTactics.reflexivity_tac</tactic>
  57     <hint>Hbugs_types.Use_reflexivity_Luke</hint>
  58     <hint_type>Use Reflexivity Luke</hint_type>
  59     <description>Reflexivity tutor</description>
  60   </tutor>
  61   <tutor source="symmetry_tutor.ml">
  62     <addr>127.0.0.1</addr>
  63     <port>50004</port>
  64     <tactic>EqualityTactics.symmetry_tac</tactic>
  65     <hint>Hbugs_types.Use_symmetry_Luke</hint>
  66     <hint_type>Use Symmetry Luke</hint_type>
  67     <description>Symmetry tutor</description>
  68   </tutor>
  69   <tutor source="assumption_tutor.ml">
  70     <addr>127.0.0.1</addr>
  71     <port>50005</port>
  72     <tactic>VariousTactics.assumption_tac</tactic>
  73     <hint>Hbugs_types.Use_assumption_Luke</hint>
  74     <hint_type>Use Assumption Luke</hint_type>
  75     <description>Assumption tutor</description>
  76   </tutor>
  77   <tutor source="contradiction_tutor.ml">
  78     <addr>127.0.0.1</addr>
  79     <port>50006</port>
  80     <tactic>NegationTactics.contradiction_tac</tactic>
  81     <hint>Hbugs_types.Use_contradiction_Luke</hint>
  82     <hint_type>Use Contradiction Luke</hint_type>
  83     <description>Contradiction tutor</description>
  84   </tutor>
  85   <tutor source="exists_tutor.ml">
  86     <addr>127.0.0.1</addr>
  87     <port>50007</port>
  88     <tactic>IntroductionTactics.exists_tac</tactic>
  89     <hint>Hbugs_types.Use_exists_Luke</hint>
  90     <hint_type>Use Exists Luke</hint_type>
  91     <description>Exists tutor</description>
  92   </tutor>
  93   <tutor source="split_tutor.ml">
  94     <addr>127.0.0.1</addr>
  95     <port>50008</port>
  96     <tactic>IntroductionTactics.split_tac</tactic>
  97     <hint>Hbugs_types.Use_split_Luke</hint>
  98     <hint_type>Use Split Luke</hint_type>
  99     <description>Split tutor</description>
 100   </tutor>
 101   <tutor source="left_tutor.ml">
 102     <addr>127.0.0.1</addr>
 103     <port>50009</port>
 104     <tactic>IntroductionTactics.left_tac</tactic>
 105     <hint>Hbugs_types.Use_left_Luke</hint>
 106     <hint_type>Use Left Luke</hint_type>
 107     <description>Left tutor</description>
 108   </tutor>
 109   <tutor source="right_tutor.ml">
 110     <addr>127.0.0.1</addr>
 111     <port>50010</port>
 112     <tactic>IntroductionTactics.right_tac</tactic>
 113     <hint>Hbugs_types.Use_right_Luke</hint>
 114     <hint_type>Use Right Luke</hint_type>
 115     <description>Right tutor</description>
 116   </tutor>
 117   <tutor source="search_pattern_apply_tutor.ml">
 118     <no_auto />
 119     <addr>127.0.0.1</addr>
 120     <port>50011</port>
 121     <tactic>PrimitiveTactics.apply_tac</tactic>
 122     <hint>Hbugs_types.Use_apply_Luke</hint>
 123     <hint_type>Use Apply Luke (with argument)</hint_type>
 124     <description>Search pattern apply tutor</description>
 125   </tutor>
 126 </tutors>
 127