Commits

Anonymous committed 34bad40

some changes to SimpleFunction

  • Participants
  • Parent commits a808761

Comments (0)

Files changed (1)

Examples/SimpleFunction.agda

 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)
   ... | 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
+
+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.strName  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
 
+funcName = "twice"
+
 addition : Global
-addition = mkFunction Double "twice" (((Double , parName) ∷ []) , false) blocks
+addition = mkFunction Double funcName (((Double , parName) ∷ []) , false) blocks
   where
     open AST hiding (Double)
-    parName = name (toCostring "a")
+    parName = strName "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 ]
+    blocks = [ b ]
+
+mkModule : (moduleName : String) →   List Global → AST.Module
+mkModule mname lst with emptyModule mname
+... | AST.mkModule _ dataLayout targetTriple definitions = AST.mkModule (toCostring mname) nothing nothing (Data.Colist.fromList (Data.List.map AST.global lst))
+moduleWithAddition : AST.Module
+moduleWithAddition = mkModule "addition" (addition ∷ [])
+