نام (NAME)

idris - زبان برنامه‌نویسی تابعی محض همه‌منظوره با انواع وابسته

خلاصه دستور (SYNOPSIS)

idris [گزینه‌ها] [فایل‌ها]

توضیحات (DESCRIPTION)

ادریس (Idris) یک زبان برنامه‌نویسی همه‌منظوره و تابعی محض با انواع وابسته (Dependent Types) است. انواع وابسته امکان مشروط‌سازی انواع داده بر مقادیر را فراهم می‌آورند؛ بدین معنا که برخی جنبه‌های رفتار برنامه را می‌توان دقیقاً در تعریف نوع مشخص کرد. این زبان کامپایل‌شونده است و از ارزیابی مشتاق (Eager Evaluation) استفاده می‌کند. ویژگی‌های آن تحت تاثیر زبان‌های Haskell و ML شکل گرفته است.

+ انواع وابسته کامل با الگوی تطبیق وابسته (Dependent Pattern Matching)

+ عبارات case ساده، بندهای where و قاعده with

+ تطبیق الگو در اتصال‌های let و لانمبدا

+ سربارگذاری از طریق رابط‌ها (مشابه Type Class) و عبارات جامع موناد (Monad Comprehensions)

+ نشانه‌گذاری do و براکت‌های اصطلاحی (Idiom Brackets)

+ تسهیلات نگارشی برای فهرست‌ها، چندتایی‌ها و جفت‌های وابسته

+ بررسی جامعیت و خاتمه‌پذیری تابع (Totality Checking)

+ انواع هم‌استقرایی (Coinductive Types)

+ نحو حساس به تورفتگی، نحو قابل توسعه

+ اثبات قضایا مبتنی بر تاکتیک (تحت تاثیر Coq)

+ جهان‌های تجمعی (Cumulative Universes)

+ رابط ساده برای توابع خارجی (FFI)

+ محیط تعاملی به سبک Hugs

توجه به این نکته حائز اهمیت است که Idris در درجه نخست یک ابزار و پروژه پژوهشی است؛ بنابراین ابزارهای ارائه‌شده و برنامه‌های ایجادشده لزوماً نباید آماده محیط عملیاتی و استفاده صنعتی تلقی شوند.

گزینه‌ها (OPTIONS)

--nobanner: عدم نمایش بنر آغازین
-q, --quiet: کاهش جزئیات خروجی (حالت بی‌صدا)
--ide-mode: اجرای REPL ادریس با نحو قابل خواندن توسط ماشین
--ide-mode-socket: انتخاب یک سوکت برای گوش دادن حالت IDE
--ideslave: نسخه منسوخ‌شده برای --ide-mode
--ideslave-socket: نسخه منسوخ‌شده برای --ide-mode-socket
--log LEVEL: سطح لاگ اشکال‌زدایی
--logging-categories CATS: دسته‌بندی‌های لاگ‌گیری جداشده با دونقطه. برای مشاهده فهرست از --listlogcats استفاده کنید.
--nobasepkgs: عدم استفاده از بسته پایه مشخص‌شده
--noprelude: عدم استفاده از پیش‌درآمد (prelude) مشخص‌شده
--nobuiltins: عدم استفاده از توابع توکار
--check: فقط بررسی نوع (Typecheck) بدون راه‌اندازی REPL
-o, --output FILE: مشخص کردن فایل خروجی
--interface: تولید فایل‌های رابط از ExportLists
--typeintype: غیرفعال کردن بررسی جهان (Universe checking)
--total: الزام پیش‌فرض توابع به جامع بودن (Total)
--warnpartial: هشدار درباره توابع جزئی اعلام‌نشده
--warnreach: هشدار درباره آرگومان‌های قابل دسترس اما غیرقابل دستیابی
--listlogcats: نمایش دسته‌بندی‌های لاگ‌گیری
--link: نمایش فلگ‌های پیونددهی (Link)
--listlibs: نمایش کتابخانه‌های نصب‌شده
--libdir: نمایش دایرکتوری کتابخانه‌ها
--include: نمایش فلگ‌های include
--V2: بیشترین میزان جزئیات خروجی
--V1: جزئیات بیشتر خروجی
-V, --V0, --verbose: نمایش خروجی پرجزئیات
--ibcsubdir FILE: نوشتن فایل‌های IBC در زیردایرکتوری
-i, --idrispath ARG: افزودن دایرکتوری به فهرست مسیرهای واردسازی
--sourcepath ARG: افزودن دایرکتوری به فهرست مسیرهای جستجوی سورس
-p, --package ARG: افزودن بسته به‌عنوان یک وابستگی
--port PORT: درگاه TCP برای REPL
--build IPKG: ساخت بسته
--install IPKG: نصب بسته
--repl IPKG: راه‌اندازی REPL (فقط برای فایل‌های اجرایی)
--clean IPKG: پاک‌سازی بسته
--mkdoc IPKG: تولید IdrisDoc برای بسته
--checkpkg IPKG: تنها بررسی بسته
--testpkg IPKG: اجرای آزمون‌ها برای بسته
-S, --codegenonly: عدم کامپایل بیشتر خروجی تولیدکننده کد
-c, --compileonly: کامپایل به فایل‌های شیء (Object) به‌جای فایل اجرایی
--codegen TARGET: انتخاب تولیدکننده کد: همراه Idris گزینه‌های C و Javascript و Node و بایت‌کد گنجانده شده‌اند
--cg-opt ARG: آرگومان‌های ارسالی به تولیدکننده کد
-e, --eval EXPR: ارزیابی یک عبارت بدون بارگذاری REPL
--execute: اجرا با عنوان idris
--exec EXPR: اجرا با عنوان idris
-X, --extension EXT: فعال کردن افزونه زبانی (TypeProviders یا ErrorReflection)
--partial-eval: فعال‌سازی ارزیابی جزئی
--target TRIPLE: در صورت پشتیبانی، تولیدکننده کد بر سه‌گانه هدف متمرکز می‌شود
--cpu CPU: در صورت پشتیبانی، تولیدکننده کد بر پردازنده نام‌برده شده متمرکز می‌شود (مانند corei7 یا cortex-m3)
--color, --colour: اجبار به خروجی رنگی
--nocolor, --nocolour: غیرفعال کردن خروجی رنگی
--optimise-nat-like-types, --optimize-nat-like-types: کامپایل انواع شبیه Nat به اعداد بزرگ (Big Ints)
--no-optimise-nat-like-types, --no-optimize-nat-like-types: عدم کامپایل انواع شبیه Nat به اعداد بزرگ
--consolewidth WIDTH: انتخاب عرض کنسول: auto ، infinite ، nat
--highlight: تولید هایلایت برای کد مبدأ
--no-tactic-deprecation-warnings: غیرفعال کردن هشدارهای منسوخ‌شدن برای زیرزبان تاکتیک قدیمی
-v, --version: چاپ اطلاعات نسخه
-h, --help: نمایش این راهنما

همچنین ببینید (SEE ALSO)

+ وب‌سایت ادریس: https://idris-lang.org

+ کانال IRC ادریس با شناسه ‎#idris در سرور chat.freenode.net

+ ویکی ادریس حاوی اطلاعات ارائه‌شده کاربران (https://github.com/idris-lang/Idris-dev/wiki)، به‌ویژه:

– https://github.com/idris-lang/Idris-dev/wiki/Manual

– https://github.com/idris-lang/Idris-dev/wiki/Language-Features

نویسندگان (AUTHORS)

جامعه توسعه‌دهندگان ادریس (The Idris Community)