2017-12-26 41 views
5

कोक में, ... के बीच क्या अंतर है?आवश्यकता, आयात, आयात की आवश्यकता है

  • आवश्यकता एक्स
  • आयात एक्स
  • आवश्यकता आयात एक्स

मैं मूल रूप से कुछ आम पैटर्न याद है। मैं आमतौर पर आयात आयात एक्स का उपयोग कर कोड देखता हूं। फिर सूची सूचीकरण आयात होता है। और मैंने अभी देखा है कि केवल एक्स की आवश्यकता है लिखना भी संभव है। क्या अंतर है? कुछ व्यावहारिक उदाहरणों की सराहना की जाएगी।

उत्तर

8

Require लाइब्रेरी लोड करता है जबकि Import इसकी परिभाषाओं को दायरे में लाता है। Require Import दोनों करता है। यदि आपके पास केवल लाइब्रेरी लोड है, तो आपको पूरी तरह योग्य नामों का संदर्भ देना होगा। कोक मॉड्यूल को परिभाषित करने के लिए फ़ाइलों के अनुरूप शीर्ष-स्तरीय मॉड्यूल की अनुमति देता है; इन्हें अलग से आयात किया है करने के लिए जा दायरे में उनकी परिभाषा के सभी लाने के लिए, और वे नहीं किया जा सकता Require घ - कि क्या ListNotations साथ हो रहा है है:

(* List is not loaded by default *) 
Fail Check List.map. 

(* the full name is technically Coq.Lists.List *) 
Require List. 

(* note that lists are actually defined in Coq.Init.Datatypes which is 
imported by default, so [list] is unqualified and the [x::xs] notation is 
already defined *) 
Print List.map. 
(* 
List.map = 
fun (A B : Type) (f : A -> B) => 
fix map (l : list A) : list B := 
    match l with 
    | nil => nil 
    | (a :: t)%list => (f a :: map t)%list 
    end 
    : forall A B : Type, (A -> B) -> list A -> list B 
*) 

(* bring everything in List into scope *) 
Import List. 
(* this includes the ListNotations submodule *) 
Import ListNotations. 

(* note that now list notations are available, and the list notation scope is 
open (from importing List) *) 
Print List.map. 
(* 
map = 
fun (A B : Type) (f : A -> B) => 
fix map (l : list A) : list B := 
    match l with 
    | [] => [] 
    | a :: t => f a :: map t 
    end 
    : forall A B : Type, (A -> B) -> list A -> list B 
*) 

नोट के साथ कैसे Coq मॉड्यूल संभालती कुछ quirks, देखते हैं विशेष रूप से अन्य भाषाओं की तुलना में:

  • कोक को मॉड्यूल के लिए पूर्ण पथ की आवश्यकता नहीं है, केवल एक स्पष्ट प्रत्यय। वास्तव में मैं शायद ही कभी मानक पुस्तकालय मॉड्यूल तक, पूर्ण आयात पथ देखता हूं।
  • मॉड्यूल आयात करने के अलावा नोटेशन का उपयोग नहीं किया जा सकता है, और अधिकांश वस्तुओं के विपरीत कोई नोटेशन, पूरी तरह योग्य या अन्यथा संदर्भित करने का कोई तरीका नहीं है।
  • मॉड्यूल आयात करने से दुष्प्रभाव हो सकते हैं, उदाहरण के लिए यदि आप आयात किए जा रहे मॉड्यूल में Global Set का उपयोग करते हैं तो नोटेशन व्याख्या स्कोप या सेटिंग विकल्प बदलना।
  • आयात काफी सीमित है (विशेष रूप से हास्केल की तुलना में) - आयात समय पर मॉड्यूल का नाम बदलने का कोई तरीका नहीं है, या कुछ परिभाषाओं को चुनिंदा आयात करें।
संबंधित मुद्दे