Commits

Anonymous committed 7fb9870

the first function example

Comments (0)

Files changed (1)

Examples/SimpleFunction.agda

+module Examples.SimpleFunction where
+import LLVM.AST as AST
+open import Data.String
+open import Data.List
+open import Data.Colist hiding (map ; [_])
+open import Data.Maybe
+open import Data.Product
+open import Data.Fin
+Word32 = Fin 4294967296
+open AST using (Module; Type ; Name ; BasicBlock; Global ; Parameter)
+module _ where
+  open AST using (defaultModule ; mkModule)
+  emptyModule : String → Module
+  emptyModule s with defaultModule
+  ... | mkModule n dataLayout targetTriple definitions = mkModule (toCostring s) dataLayout targetTriple definitions
+
+
+
+
+private 
+  postulate  
+    trustMe :  {A : Set} → A
+  open import Coinduction
+  open import Function
+  {-# NO_TERMINATION_CHECK #-}
+  colist2list : {A : Set} → Colist A → List A
+  colist2list [] = []
+  colist2list (x ∷ xs) = x ∷ colist2list (♭ xs)
+  
+  costring2string = Data.String.fromList ∘ colist2list
+  open AST using  () renaming (_×_ to _x_ ; _,_ to _,,_)
+  x2× : {A B : _} → A x B → A × B
+  x2× (proj₁ ,, proj₂) = proj₁ , proj₂
+
+  ×2x : {A B : _}  → A × B → A x B
+  ×2x c = proj₁ c ,, proj₂ c
+
+  postulate Integer : Set
+  {-# BUILTIN INTEGER Integer #-}
+  {-# COMPILED_TYPE Integer Integer #-}
+  open import Data.Nat
+  primitive
+      primNatToInteger    : ℕ -> Integer
+
+  module _ (i : Integer) where
+    postulate
+      word : AST.Word 
+      w32 : AST.Word32
+  {-# COMPILED word fromInteger #-}
+  {-# COMPILED w32 fromInteger #-}
+  conv : {A : Set} → (Integer → A) → ℕ → A
+  conv f = f ∘ primNatToInteger
+  
+
+  
+open import Data.Bool
+module _ where
+  mkFunction : Type → String → List (Type × Name)  × Bool → List BasicBlock → Global
+  mkFunction  t s (args , pb) blocks with AST.functionDefaults 
+  ... | AST.function linkage visibility callingConvention returnAttributes returnType n (l ,, b) functionAttributes section alignment garbageCollectorName basicBlocks = 
+                             AST.function linkage visibility callingConvention  returnAttributes
+                                          t (AST.name (toCostring s))  (pars ,, pb) functionAttributes section
+                                          alignment garbageCollectorName (Data.Colist.fromList blocks) 
+        where
+          pars : Colist Parameter
+          pars = Data.Colist.fromList ∘ Data.List.map (λ { (t , n) → AST.parameter t n (Data.Colist.fromList [])}) $ args
+  ... | _ = trustMe
+
+Double : Type
+Double  = floating (conv w32 32) ieee
+  where 
+    open AST
+
+addition : Global
+addition = mkFunction Double "twice" (((Double , parName) ∷ []) , false) blocks
+  where
+    open AST hiding (Double)
+    parName = name (toCostring "a")
+    ref = localReference parName 
+    tmpName = unName $ conv word 2
+    insts = (tmpName ≔ fadd ref ref [] ) ∷ []
+    term = do (ret (just (localReference tmpName)) [])
+    b = block (unName (conv word 1)) (Data.Colist.fromList insts) term 
+    blocks = [ b ]