Pythag.idr:
module Main
pythag : Int -> List (Int, Int, Int)
pythag max = [(x, y, z) | z <- [1..max], y <- [1..z], x <- [1..y],
x * x + y *y == z * z]
main : IO ()
main = print (pythag 50)
$ idris Pythag.idr --codegen lw -o Pythag.lisp
$ ls -l Pythag.*
-rw-r--r-- 1 mimimimi staff 4346 Dec 18 15:59 Pythag.ibc
-rw-r--r-- 1 mimimimi staff 195 Dec 18 10:32 Pythag.idr
-rw-r--r-- 1 mimimimi staff 41640 Dec 18 15:59 Pythag.lisp
Pythag.lisp:
CL-USER 1 > (load (compile-file "Pythag.lisp"))
;;; Compiling file Pythag.lisp ...
;;; Safety = 3, Speed = 1, Space = 1, Float = 1, Interruptible = 1
;;; Compilation speed = 1, Debug = 2, Fixnum safety = 3
;;; Source level debugging is on
;;; Source file recording is on
;;; Cross referencing is on
; (TOP-LEVEL-FORM 0)
; (DEFPACKAGE "IDRIS.RTS")
; (TOP-LEVEL-FORM 2)
; (SUBFUNCTION (DEFCLASS IDRIS.RTS:IDRIS-ERROR) (DEFINE-CONDITION IDRIS.RTS:IDRIS-ERROR))
; (DEFINE-CONDITION IDRIS.RTS:IDRIS-ERROR)
; (SUBFUNCTION (DEFCLASS IDRIS.RTS::SIMPLE-IDRIS-ERROR) (DEFINE-CONDITION IDRIS.RTS::SIMPLE-IDRIS-ERROR))
; (DEFINE-CONDITION IDRIS.RTS::SIMPLE-IDRIS-ERROR)
; IDRIS.RTS:IDRIS-ERROR
; (SUBFUNCTION (DEFCLASS IDRIS.RTS:NOT-IMPLEMENTED-IDRIS-ERROR) (DEFINE-CONDITION IDRIS.RTS:NOT-IMPLEMENTED-IDRIS-ERROR))
; (DEFINE-CONDITION IDRIS.RTS:NOT-IMPLEMENTED-IDRIS-ERROR)
; (DEFINE-CONDITION IDRIS.RTS:NOT-IMPLEMENTED-IDRIS-ERROR)
; (DEFVAR IDRIS.RTS::*GLOBAL-LOCK*)
; IDRIS.RTS::WITH-GLOBAL-LOCK
; IDRIS.RTS:IDRIS-INIT
; IDRIS.RTS:IDRIS-SYSTEM-INFO
; (SUBFUNCTION (DEFSETF IDRIS.RTS:IDRIS-CON-VALS) (DEFSTRUCT IDRIS.RTS:IDRIS-CON))
; (SUBFUNCTION (DEFSETF IDRIS.RTS:IDRIS-CON-TAG) (DEFSTRUCT IDRIS.RTS:IDRIS-CON))
; (SUBFUNCTION IDRIS.RTS:MAKE-IDRIS-CON (DEFSTRUCT IDRIS.RTS:IDRIS-CON))
; IDRIS.RTS:IDRIS-NULL-P
; IDRIS.RTS:IDRIS-STRING-BUILDER
; IDRIS.RTS:IDRIS-SUBSTRING
; IDRIS.RTS:IDRIS-STRING->INTEGER
; IDRIS.RTS:IDRIS-INTEGER->STRING
; IDRIS.RTS:IDRIS-STRING->FLOAT
; IDRIS.RTS:IDRIS-FLOAT->STRING
; IDRIS.RTS:IDRIS-STRING->LIST
; IDRIS.RTS:IDRIS-LIST->STRING
; IDRIS.RTS:IDRIS-BITWISE-SHIFT-LEFT
; IDRIS.RTS:IDRIS-BITWISE-SHIFT-RIGHT
; IDRIS.RTS:CURRENT-IDRIS-INPUT
; IDRIS.RTS:CURRENT-IDRIS-OUTPUT
; IDRIS.RTS:CURRENT-IDRIS-ERROR
; (DEFVAR IDRIS.RTS::*FLUSH-BUFFERS-P*)
; IDRIS.RTS:IDRIS-DISABLE-BUFFERING
; IDRIS.RTS::WITH-BUFFERING-CONTROL
; IDRIS.RTS:IDRIS-GET-LINE
; IDRIS.RTS:IDRIS-GET-STRING-N
; IDRIS.RTS:IDRIS-PUT-STRING
; (DEFPACKAGE "Pythag")
; (TOP-LEVEL-FORM 33)
; (TOP-LEVEL-FORM 34)
; |Pythag|::|Prelude.Bool.&&|
; |Pythag|::|Prelude.List.++|
; |Pythag|::|Prelude.Algebra.<+>|
; |Pythag|::|Force|
; |Pythag|::|PE_concatMap_8faac41f|
; |Pythag|::|PE_constructor of Prelude.Algebra.Monoid?Semigroup ty_3b7d03e2|
; |Pythag|::|PE_neutral_3b7d03e2|
; |Pythag|::|assert_unreachable|
; |Pythag|::|call__IO|
;;;*** Warning in |Pythag|::|Prelude.Applicative.empty|: V3 is bound but not referenced
; |Pythag|::|Prelude.Applicative.empty|
;;;*** Warning in |Pythag|::|Prelude.Applicative.guard|: V5 is bound but not referenced
;;;*** Warning in |Pythag|::|Prelude.Applicative.guard|: V3 is bound but not referenced
; |Pythag|::|Prelude.Applicative.guard|
; |Pythag|::|idris_crash|
; |Pythag|::|Prelude.Bool.ifThenElse|
; |Pythag|::|Prelude.Interfaces.intToBool|
; |Pythag|::|io_bind|
; |Pythag|::|io_pure|
; |Pythag|::|Main.main|
; |Pythag|::|mkForeignPrim|
; |Pythag|::|Prelude.Bool.not|
;;;*** Warning in |Pythag|::|Prelude.Show.precCon|: V1 is bound but not referenced
; |Pythag|::|Prelude.Show.precCon|
; |Pythag|::|Prelude.Show.primNumShow|
; |Pythag|::|prim__addInt|
; |Pythag|::|prim__asPtr|
; |Pythag|::|prim__concat|
; |Pythag|::|prim__eqBigInt|
; |Pythag|::|prim__eqChar|
; |Pythag|::|prim__eqInt|
; |Pythag|::|prim__eqManagedPtr|
; |Pythag|::|prim__eqPtr|
; |Pythag|::|prim__eqString|
; |Pythag|::|prim__mulInt|
; |Pythag|::|prim__null|
; |Pythag|::|prim__peek16|
; |Pythag|::|prim__peek32|
; |Pythag|::|prim__peek64|
; |Pythag|::|prim__peek8|
; |Pythag|::|prim__peekDouble|
; |Pythag|::|prim__peekPtr|
; |Pythag|::|prim__peekSingle|
; |Pythag|::|prim__poke16|
; |Pythag|::|prim__poke32|
; |Pythag|::|prim__poke64|
; |Pythag|::|prim__poke8|
; |Pythag|::|prim__pokeDouble|
; |Pythag|::|prim__pokePtr|
; |Pythag|::|prim__pokeSingle|
; |Pythag|::|prim__ptrOffset|
; |Pythag|::|prim__readChars|
; |Pythag|::|prim__readFile|
; |Pythag|::|prim__registerPtr|
; |Pythag|::|prim__sextInt_BigInt|
; |Pythag|::|prim__sizeofPtr|
; |Pythag|::|prim__sltBigInt|
; |Pythag|::|prim__sltInt|
; |Pythag|::|prim__stderr|
; |Pythag|::|prim__stdin|
; |Pythag|::|prim__stdout|
; |Pythag|::|prim__strHead|
; |Pythag|::|prim__subInt|
; |Pythag|::|prim__toStrInt|
; |Pythag|::|prim__vm|
; |Pythag|::|prim__writeFile|
; |Pythag|::|prim__writeString|
; |Pythag|::|prim_io_bind|
; |Pythag|::|prim_write|
; |Pythag|::|Prelude.Applicative.pure|
; |Pythag|::|Prelude.Interactive.putStr'|
; |Pythag|::|Main.pythag|
; |Pythag|::|run__IO|
; |Pythag|::|Prelude.Show.show|
; |Pythag|::|Prelude.Show.showParens|
; |Pythag|::|Prelude.Strings.strM|
; |Pythag|::|unsafePerformPrimIO|
; |Pythag|::|world|
; |Pythag|::|Prelude.Bool.??|
; |Pythag|::{APPLY_0}
; |Pythag|::{APPLY2_0}
; |Pythag|::{EVAL_0}
; |Pythag|::|{PE_concatMap_8faac41f_0}|
; |Pythag|::|Prelude.Interfaces.{Prelude.Interfaces.@Prelude.Interfaces.Ord$Int:!<=:0_lam_0}|
; |Pythag|::|Prelude.Interfaces.{Prelude.Show.@Prelude.Interfaces.Ord$Prec:!>=:0_lam_0}|
; |Pythag|::|{io_bind_0}|
; |Pythag|::|Main.{main_0}|
; |Pythag|::|Prelude.Show.{primNumShow_0}|
; |Pythag|::|Prelude.Interactive.{putStr'_0}|
; |Pythag|::|Main.{pythag_0}|
; |Pythag|::|{runMain_0}|
; |Pythag|::|{io_bind_1}|
; |Pythag|::|Main.{main_1}|
; |Pythag|::|Prelude.Show.{primNumShow_1}|
; |Pythag|::|Main.{pythag_1}|
; |Pythag|::|{io_bind_2}|
; |Pythag|::|Main.{main_2}|
; |Pythag|::|Prelude.Show.{primNumShow_2}|
; |Pythag|::|Main.{pythag_2}|
; |Pythag|::|Main.{main_3}|
; |Pythag|::|Main.{pythag_3}|
; |Pythag|::|Main.{main_4}|
; |Pythag|::|Main.{pythag_4}|
; |Pythag|::|Main.{pythag_5}|
; |Pythag|::|Main.{pythag_6}|
; |Pythag|::|Prelude.List.reverse:reverse':0|
; |Pythag|::|Decidable.Equality.Decidable.Equality.@Decidable.Equality.DecEq$Char:!decEq:0:primitiveNotEq:0|
; |Pythag|::|Decidable.Equality.Decidable.Equality.@Decidable.Equality.DecEq$Int:!decEq:0:primitiveNotEq:0|
; |Pythag|::|Decidable.Equality.Decidable.Equality.@Decidable.Equality.DecEq$Integer:!decEq:0:primitiveNotEq:0|
; |Pythag|::|Decidable.Equality.Decidable.Equality.@Decidable.Equality.DecEq$ManagedPtr:!decEq:0:primitiveNotEq:0|
; |Pythag|::|Decidable.Equality.Decidable.Equality.@Decidable.Equality.DecEq$Ptr:!decEq:0:primitiveNotEq:0|
; |Pythag|::|Decidable.Equality.Decidable.Equality.@Decidable.Equality.DecEq$String:!decEq:0:primitiveNotEq:0|
; |Pythag|::|Prelude.Prelude.@Prelude.Enum$Int:!enumFromTo:0:go:0|
; |Pythag|::|Prelude.Prelude.@Prelude.Enum$Int:!enumFromTo:0:go':0|
; |Pythag|::|Prelude.Show.Prelude.Show.@Prelude.Show.Show$List a:!show:0:show':0|
; |Pythag|::|Decidable.Equality.Decidable.Equality.@Decidable.Equality.DecEq$Bool:!decEq:0|
; |Pythag|::|Prelude.Prelude.@Prelude.Enum$Int:!enumFromTo:0|
; |Pythag|::|Prelude.Interfaces.Prelude.Nat.@Prelude.Interfaces.Eq$Nat:!==:0|
; |Pythag|::|Prelude.Interfaces.Prelude.Show.@Prelude.Interfaces.Eq$Prec:!==:0|
; |Pythag|::|Prelude.Foldable.Prelude.List.@Prelude.Foldable.Foldable$List:!foldr:0|
; |Pythag|::|Prelude.Monad.Prelude.@Prelude.Monad.Monad$List:!>>=:0|
; |Pythag|::|Prelude.Interfaces.Prelude.Interfaces.@Prelude.Interfaces.Ord$Int:!<=:0|
; |Pythag|::|Prelude.Interfaces.Prelude.Interfaces.@Prelude.Interfaces.Ord$Int:!compare:0|
; |Pythag|::|Prelude.Interfaces.Prelude.Interfaces.@Prelude.Interfaces.Ord$Integer:!compare:0|
;;;*** Warning in |Pythag|::|Prelude.Interfaces.Prelude.Nat.@Prelude.Interfaces.Ord$Nat:!compare:0|: V2 is bound but not referenced
; |Pythag|::|Prelude.Interfaces.Prelude.Nat.@Prelude.Interfaces.Ord$Nat:!compare:0|
; |Pythag|::|Prelude.Interfaces.Prelude.Show.@Prelude.Interfaces.Ord$Prec:!>=:0|
; |Pythag|::|Prelude.Interfaces.Prelude.Show.@Prelude.Interfaces.Ord$Prec:!compare:0|
; |Pythag|::|Prelude.Show.Prelude.Show.@Prelude.Show.Show$(a, b):!show:0|
; |Pythag|::|Prelude.Show.Prelude.Show.@Prelude.Show.Show$List a:!show:0|
; |Pythag|::|_Prelude.Interfaces.Prelude.Show.@Prelude.Interfaces.Ord$Prec:!>:0_with_27|
; |Pythag|::|_Prelude.Strings.strM_with_32|
; |Pythag|::|_Prelude.Show.firstCharIs_with_45|
; |Pythag|::|_Prelude.Interfaces.Prelude.Interfaces.@Prelude.Interfaces.Ord$Int:!<:0_with_107|
;;;*** Warning in |Pythag|::|Prelude.Applicative.Alternative_ictor?"Applicative f"|: V3 is bound but not referenced
; |Pythag|::|Prelude.Applicative.Alternative_ictor?"Applicative f"|
; |Pythag|::|io_bind_IO__idr_107_34_case|
; |Pythag|::|Void___casefun__Void___case|
; |Pythag|::|Void_elim|
; |Pythag|:|runMain|
;; Processing Cross Reference Information
The following functions are undefined:
|Pythag|::FOREIGN-REF which is referenced by |Pythag|::|prim__peekSingle|, |Pythag|::|prim__peekPtr|, |Pythag|::|prim__peekDouble|, |Pythag|::|prim__peek8|, |Pythag|::|prim__peek64|, |Pythag|::|prim__peek32|, and |Pythag|::|prim__peek16|
|Pythag|::FOREIGN-SIZEOF which is referenced by |Pythag|::|prim__sizeofPtr|
|Pythag|::FOREIGN-SET! which is referenced by |Pythag|::|prim__pokeSingle|, |Pythag|::|prim__pokePtr|, |Pythag|::|prim__pokeDouble|, |Pythag|::|prim__poke8|, |Pythag|::|prim__poke64|, |Pythag|::|prim__poke32|, and |Pythag|::|prim__poke16|
; Loading fasl file /Users/mimimimi/projects/idris-lw/example/Pythag.64xfasl
#P"/Users/mimimimi/projects/idris-lw/example/Pythag.64xfasl"
CL-USER 2 > (|Pythag|:|runMain|)
[(3, (4, 5)), (6, (8, 10)), (5, (12, 13)), (9, (12, 15)), (8, (15, 17)), (12, (16, 20)), (15, (20, 25)), (7, (24, 25)), (10, (24, 26)), (20, (21, 29)), (18, (24, 30)), (16, (30, 34)), (21, (28, 35)), (12, (35, 37)), (15, (36, 39)), (24, (32, 40)), (9, (40, 41)), (27, (36, 45)), (30, (40, 50)), (14, (48, 50))]
#S(IDRIS.RTS:IDRIS-CON :TAG 0 :VALS NIL)
