IDRIS(1) Idris man page IDRIS(1) نام (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) + وب‌سایت ادریس: + کانال IRC ادریس با شناسه ‎#idris در سرور chat.freenode.net + ویکی ادریس حاوی اطلاعات ارائه‌شده کاربران ()، به‌ویژه: – – نویسندگان (AUTHORS) جامعه توسعه‌دهندگان ادریس (The Idris Community) 1.3.3 23 May 2020 IDRIS(1)