एक कॉक रणनीति

Question

लेफ्टैक में एक जटिल रणनीति को लागू करते समय, कुछ एलटीएसी कमांड या सामरिक आमंत्रण जो मैं विफल होने की उम्मीद करता हूं और जहां इसकी अपेक्षा की जाती है (उदाहरण के लिए repeat को समाप्त करने के लिए, या बैकट्रैकिंग का कारण बनने के लिए)। इन असफलताओं आमतौर पर विफलता के स्तर पर उठाया जाता है 0.

विफलताओं उच्च स्तर पर उठाया "पलायन" आसपास के try या repeat ब्लॉक, और अप्रत्याशित विफलताओं संकेत करने के लिए उपयोगी होते हैं।

जो मैं खो रहा हूं वह एक रणनीति tac चलाने का एक तरीका है और विफलता के संदेश को बनाए रखते हुए, उच्च स्तर पर होने के लिए, स्तर 0 पर भी इसकी विफलता का इलाज करता है। यह मुझे यह सुनिश्चित करने देगा कि repeat मेरी तरफ एक Ltac प्रोग्रामिंग त्रुटि के कारण समाप्त नहीं होता है।

क्या मैं लेटाक में ऐसी विफलता-बढ़ाने-स्तर उच्च-आदेश रणनीति को कार्यान्वित कर सकता हूं?

Answer 1

आप ओकंपल में इसे प्राप्त करने के लिए एक रणनीति लिख सकते हैं। मैंने इसे गिटहब here पर रखा।

उदाहरण के लिए निम्नलिखित चुपचाप सफल होने के बजाय एक त्रुटि उठाना चाहिए:

repeat (match goal with 
      | [ |- _ ] => 
      raise_error_level (assert (3 = 3) by idtac) 
     end). 

Answer 2

अगर यह संभव है कि आप क्या चाहते वास्तव में प्राप्त करने के लिए मैं नहीं जानता, लेकिन मैं कभी कभी निम्नलिखित मुहावरा का उपयोग करें: पहली रणनीति स्तर 0 के साथ विफल रहता है

tactic_expression_that_may_fail_with_level_0 
|| fail 1000 "There was some problem here" 

, || चलाने का प्रयास करेंगे दूसरा, जो एक बहुत ही उच्च स्तर के साथ असफल हो जाएगा और आपको इसकी रिपोर्ट करेगा।

यह मदद करेगा यदि आप एक ठोस उपयोग केस प्रदान कर सकते हैं यह देखने के लिए कि कोई अन्य तकनीक बेहतर अनुकूल होगी या नहीं।