.\" Manpage for Idris. .\" Contact <> to correct errors or typos. .TH IDRIS 1 "23 May 2020" "1.3.3" "Idris man page" .SH "نام (NAME)" idris \- زبان برنامه‌نویسی تابعی محض همه‌منظوره با انواع وابسته .SH "خلاصه دستور (SYNOPSIS)" .B idris [\fIگزینه‌ها\fR] [\fIفایل‌ها\fR] .SH "توضیحات (DESCRIPTION)" ادریس (Idris) یک زبان برنامه‌نویسی همه‌منظوره و تابعی محض با انواع وابسته (Dependent Types) است. انواع وابسته امکان مشروط‌سازی انواع داده بر مقادیر را فراهم می‌آورند؛ بدین معنا که برخی جنبه‌های رفتار برنامه را می‌توان دقیقاً در تعریف نوع مشخص کرد. این زبان کامپایل‌شونده است و از ارزیابی مشتاق (Eager Evaluation) استفاده می‌کند. ویژگی‌های آن تحت تاثیر زبان‌های Haskell و ML شکل گرفته است. .PP + انواع وابسته کامل با الگوی تطبیق وابسته (Dependent Pattern Matching) .PP + عبارات case ساده، بندهای where و قاعده with .PP + تطبیق الگو در اتصال‌های let و لانمبدا .PP + سربارگذاری از طریق رابط‌ها (مشابه Type Class) و عبارات جامع موناد (Monad Comprehensions) .PP + نشانه‌گذاری do و براکت‌های اصطلاحی (Idiom Brackets) .PP + تسهیلات نگارشی برای فهرست‌ها، چندتایی‌ها و جفت‌های وابسته .PP + بررسی جامعیت و خاتمه‌پذیری تابع (Totality Checking) .PP + انواع هم‌استقرایی (Coinductive Types) .PP + نحو حساس به تورفتگی، نحو قابل توسعه .PP + اثبات قضایا مبتنی بر تاکتیک (تحت تاثیر Coq) .PP + جهان‌های تجمعی (Cumulative Universes) .PP + رابط ساده برای توابع خارجی (FFI) .PP + محیط تعاملی به سبک Hugs .PP توجه به این نکته حائز اهمیت است که Idris در درجه نخست یک ابزار و پروژه پژوهشی است؛ بنابراین ابزارهای ارائه‌شده و برنامه‌های ایجادشده لزوماً نباید آماده محیط عملیاتی و استفاده صنعتی تلقی شوند. .SH "گزینه‌ها (OPTIONS)" .TP .B \-\-nobanner عدم نمایش بنر آغازین .TP .BR \-q , " \-\-quiet" کاهش جزئیات خروجی (حالت بی‌صدا) .TP .B \-\-ide\-mode اجرای REPL ادریس با نحو قابل خواندن توسط ماشین .TP .B \-\-ide\-mode\-socket انتخاب یک سوکت برای گوش دادن حالت IDE .TP .B \-\-ideslave نسخه منسوخ‌شده برای \-\-ide\-mode .TP .B \-\-ideslave\-socket نسخه منسوخ‌شده برای \-\-ide\-mode\-socket .TP .BI \-\-log " LEVEL" سطح لاگ اشکال‌زدایی .TP .BI \-\-logging\-categories " CATS" دسته‌بندی‌های لاگ‌گیری جداشده با دونقطه. برای مشاهده فهرست از \-\-listlogcats استفاده کنید. .TP .B \-\-nobasepkgs عدم استفاده از بسته پایه مشخص‌شده .TP .B \-\-noprelude عدم استفاده از پیش‌درآمد (prelude) مشخص‌شده .TP .B \-\-nobuiltins عدم استفاده از توابع توکار .TP .B \-\-check فقط بررسی نوع (Typecheck) بدون راه‌اندازی REPL .TP .BI \-o , " \-\-output " FILE مشخص کردن فایل خروجی .TP .B \-\-interface تولید فایل‌های رابط از ExportLists .TP .B \-\-typeintype غیرفعال کردن بررسی جهان (Universe checking) .TP .B \-\-total الزام پیش‌فرض توابع به جامع بودن (Total) .TP .B \-\-warnpartial هشدار درباره توابع جزئی اعلام‌نشده .TP .B \-\-warnreach هشدار درباره آرگومان‌های قابل دسترس اما غیرقابل دستیابی .TP .B \-\-listlogcats نمایش دسته‌بندی‌های لاگ‌گیری .TP .B \-\-link نمایش فلگ‌های پیونددهی (Link) .TP .B \-\-listlibs نمایش کتابخانه‌های نصب‌شده .TP .B \-\-libdir نمایش دایرکتوری کتابخانه‌ها .TP .B \-\-include نمایش فلگ‌های include .TP .B \-\-V2 بیشترین میزان جزئیات خروجی .TP .B \-\-V1 جزئیات بیشتر خروجی .TP .BR \-V , " \-\-V0" , " \-\-verbose" نمایش خروجی پرجزئیات .TP .BI \-\-ibcsubdir " FILE" نوشتن فایل‌های IBC در زیردایرکتوری .TP .BI \-i , " \-\-idrispath " ARG افزودن دایرکتوری به فهرست مسیرهای واردسازی .TP .BI \-\-sourcepath " ARG" افزودن دایرکتوری به فهرست مسیرهای جستجوی سورس .TP .BI \-p , " \-\-package " ARG افزودن بسته به‌عنوان یک وابستگی .TP .BI \-\-port " PORT" درگاه TCP برای REPL .TP .BI \-\-build " IPKG" ساخت بسته .TP .BI \-\-install " IPKG" نصب بسته .TP .BI \-\-repl " IPKG" راه‌اندازی REPL (فقط برای فایل‌های اجرایی) .TP .BI \-\-clean " IPKG" پاک‌سازی بسته .TP .BI \-\-mkdoc " IPKG" تولید IdrisDoc برای بسته .TP .BI \-\-checkpkg " IPKG" تنها بررسی بسته .TP .BI \-\-testpkg " IPKG" اجرای آزمون‌ها برای بسته .TP .BR \-S , " \-\-codegenonly" عدم کامپایل بیشتر خروجی تولیدکننده کد .TP .BR \-c , " \-\-compileonly" کامپایل به فایل‌های شیء (Object) به‌جای فایل اجرایی .TP .BI \-\-codegen " TARGET" انتخاب تولیدکننده کد: همراه Idris گزینه‌های C و Javascript و Node و بایت‌کد گنجانده شده‌اند .TP .BI \-\-cg\-opt " ARG" آرگومان‌های ارسالی به تولیدکننده کد .TP .BI \-e , " \-\-eval " EXPR ارزیابی یک عبارت بدون بارگذاری REPL .TP .B \-\-execute اجرا با عنوان idris .TP .BI \-\-exec " EXPR" اجرا با عنوان idris .TP .BI \-X , " \-\-extension " EXT فعال کردن افزونه زبانی (TypeProviders یا ErrorReflection) .TP .B \-\-partial\-eval فعال‌سازی ارزیابی جزئی .TP .BI \-\-target " TRIPLE" در صورت پشتیبانی، تولیدکننده کد بر سه‌گانه هدف متمرکز می‌شود .TP .BI \-\-cpu " CPU" در صورت پشتیبانی، تولیدکننده کد بر پردازنده نام‌برده شده متمرکز می‌شود (مانند corei7 یا cortex-m3) .TP .BR \-\-color , " \-\-colour" اجبار به خروجی رنگی .TP .BR \-\-nocolor , " \-\-nocolour" غیرفعال کردن خروجی رنگی .TP .BR \-\-optimise\-nat\-like\-types , " \-\-optimize\-nat\-like\-types" کامپایل انواع شبیه Nat به اعداد بزرگ (Big Ints) .TP .BR \-\-no\-optimise\-nat\-like\-types , " \-\-no\-optimize\-nat\-like\-types" عدم کامپایل انواع شبیه Nat به اعداد بزرگ .TP .BI \-\-consolewidth " WIDTH" انتخاب عرض کنسول: auto ، infinite ، nat .TP .B \-\-highlight تولید هایلایت برای کد مبدأ .TP .B \-\-no\-tactic\-deprecation\-warnings غیرفعال کردن هشدارهای منسوخ‌شدن برای زیرزبان تاکتیک قدیمی .TP .BR \-v , " \-\-version" چاپ اطلاعات نسخه .TP .BR \-h , " \-\-help" نمایش این راهنما .SH "همچنین ببینید (SEE ALSO)" .PP + وب‌سایت ادریس: .PP + کانال IRC ادریس با شناسه ‎#idris در سرور chat.freenode.net .PP + ویکی ادریس حاوی اطلاعات ارائه‌شده کاربران ()، به‌ویژه: .PP – .PP – .SH "نویسندگان (AUTHORS)" جامعه توسعه‌دهندگان ادریس (The Idris Community)