[ example ] Drasticly simplify expressions generation in pil-reg

Author: buzden

examples/pil-reg/src/Example/Pil/Gens.idr

@@ -35,26 +35,31 @@ lookupGen vars = elements $ mapLk vars where
 
 --- Expressions ---
 
-export
-varExprGen : {a : Type'} -> {vars : Variables} -> {regs : Registers rc} -> Gen0 $ Expression vars regs a
+varExprGen : {ops : Ops} -> {a : Type'} -> {vars : Variables} -> {regs : Registers rc} -> Gen0 $ Expression ops vars regs a
 varExprGen = do Element (n ** _) prf <- lookupGen vars `suchThat_invertedEq` a $ \(_ ** lk) => reveal lk
                 pure $ rewrite prf in V n
 
 ||| Generator of non-recursive expressions (thus those that can be used with zero recursion bound).
-nonRec_exprGen : {a : Type'} -> {vars : Variables} -> {regs : Registers rc} -> Gen0 (idrTypeOf a) -> Gen0 $ Expression vars regs a
-nonRec_exprGen g = oneOf $ [| C' g |] :: alternativesOf varExprGen
-                   -- TODO to add the register access expression
+nonRec_exprGen : Gen0 Int => Gen0 String =>
+                 {ops : Ops} -> {a : Type'} -> {vars : Variables} -> {regs : Registers rc} -> Gen0 $ Expression ops vars regs a
+nonRec_exprGen = do
+  let g = case a of
+            Bool'   => elements {em=MaybeEmpty} [True, False]
+            Int'    => %search
+            String' => %search
+  oneOf $ [| C' g |] :: alternativesOf varExprGen
+  -- TODO to add the register access expression
 
 export
 exprGen : (fuel : Fuel) ->
+          Gen0 Int => Gen0 String =>
+          {ops : Ops} ->
           {a : Type'} ->
-          ({b : Type'} -> Gen0 $ idrTypeOf b) ->
           {vars : Variables} ->
           {regs : Registers rc} ->
-          ((subGen : {x : Type'} -> Gen0 $ Expression vars regs x) -> {b : Type'} -> Gen0 $ Expression vars regs b) ->
-          Gen0 (Expression vars regs a)
-exprGen Dry      g _   = nonRec_exprGen g
-exprGen (More f) g rec = oneOf $ alternativesOf (nonRec_exprGen g) ++ alternativesOf (rec $ exprGen f g rec)
+          Gen0 (Expression ops vars regs a)
+exprGen Dry      = nonRec_exprGen
+exprGen (More f) = oneOf $ alternativesOf nonRec_exprGen ++ alternativesOf (exprGen f)
 
 --- General methodology of writing autogenerated-like generators ---
 
@@ -131,7 +136,8 @@ SpecGen res =
   (fuel : Fuel) ->
   Gen0 Type' =>
   Gen0 Name =>
-  ({ty : Type'} -> {vars : Variables} -> {rc : Nat} -> {regs : Registers rc} -> Gen0 (Expression vars regs ty)) =>
+  Gen0 String =>
+  Gen0 Int =>
   res
 
 namespace Equal_registers
@@ -193,8 +199,9 @@ namespace Statements_given_preV_preR_postV_postR
 
   public export
   0 Statement_no_Gen : Type
-  Statement_no_Gen = SpecGen $ {rc : Nat} -> (preV : Variables) -> (preR : Registers rc) -> (postV : Variables) -> (postR : Registers rc) ->
-                               Gen0 (Statement preV preR postV postR)
+  Statement_no_Gen = SpecGen $ {ops : _} -> {rc : Nat} ->
+                               (preV : Variables) -> (preR : Registers rc) -> (postV : Variables) -> (postR : Registers rc) ->
+                               Gen0 (Statement ops preV preR postV postR)
 
   nop_gen   : Statement_no_Gen
   dot_gen   : Statement_no_Gen
@@ -231,8 +238,8 @@ namespace Statements_given_preV_preR_postR
 
   public export
   0 Statement_postV_Gen : Type
-  Statement_postV_Gen = SpecGen $ {rc : Nat} -> (preV : Variables) -> (preR : Registers rc) -> (postR : Registers rc) ->
-                                  Gen0 (postV ** Statement preV preR postV postR)
+  Statement_postV_Gen = SpecGen $ {ops : _} -> {rc : Nat} -> (preV : Variables) -> (preR : Registers rc) -> (postR : Registers rc) ->
+                                  Gen0 (postV ** Statement ops preV preR postV postR)
 
   nop_gen   : Statement_postV_Gen
   dot_gen   : Statement_postV_Gen
@@ -269,8 +276,8 @@ namespace Statements_given_preV_preR
 
   public export
   0 Statement_postV_postR_Gen : Type
-  Statement_postV_postR_Gen = SpecGen $ {rc : Nat} -> (preV : Variables) -> (preR : Registers rc) ->
-                                        Gen0 (postV ** postR ** Statement preV preR postV postR)
+  Statement_postV_postR_Gen = SpecGen $ {ops : _} -> {rc : Nat} -> (preV : Variables) -> (preR : Registers rc) ->
+                                        Gen0 (postV ** postR ** Statement ops preV preR postV postR)
 
   nop_gen   : Statement_postV_postR_Gen
   dot_gen   : Statement_postV_postR_Gen
@@ -309,11 +316,11 @@ namespace Statements_given_preV_preR -- implementations
 
   dot_gen _ preV preR = pure (_ ** _ ** !external_gen. !external_gen)
 
-  v_ass_gen _ preV preR = do
+  v_ass_gen f preV preR = do
     (n ** lk) <- lookupGen preV
-    pure (_ ** _ ** n #= !external_gen)
+    pure (_ ** _ ** n #= !(exprGen f))
 
-  r_ass_gen _ preV preR = pure (_ ** _ ** !external_gen %= !(external_gen {ty = Expression _ _ !external_gen}))
+  r_ass_gen f preV preR = pure (_ ** _ ** !external_gen %= !(exprGen f {a = !external_gen}))
 
   for_gen f preV preR = do
     (insideV ** insideR ** init) <- statement_gen f preV preR
@@ -324,12 +331,12 @@ namespace Statements_given_preV_preR -- implementations
     (bodyR ** _) <- eq_registers_gen f insideR
     (_ ** body)  <- statement_gen f insideV insideR bodyR
     --
-    pure (_ ** _ ** for init !external_gen upd body)
+    pure (_ ** _ ** for init !(exprGen f) upd body)
 
   if_gen f preV preR = do
     (_ ** _ ** th) <- statement_gen f preV preR
     (_ ** _ ** el) <- statement_gen f preV preR
-    pure (_ ** _ ** if__ !external_gen th el)
+    pure (_ ** _ ** if__ !(exprGen f) th el)
 
   seq_gen f preV preR = do
     (midV ** midR ** l) <- statement_gen f preV preR
@@ -340,7 +347,7 @@ namespace Statements_given_preV_preR -- implementations
     (_ ** _ ** s) <- statement_gen f preV preR
     pure (_ ** _ ** block s)
 
-  print_gen _ preV preR = pure (_ ** _ ** print !(external_gen {ty=Expression _ _ String'}))
+  print_gen f preV preR = pure (_ ** _ ** print !(exprGen f {a=String'}))
 
 namespace Statements_given_preV_preR_postV_postR -- implementations
 
@@ -355,15 +362,15 @@ namespace Statements_given_preV_preR_postV_postR -- implementations
     (_, No _) => empty
     (Yes Refl, Yes Refl) => pure $ ty. n
 
-  v_ass_gen _ preV preR postV postR = case (decEq postV preV, decEq postR preR) of
+  v_ass_gen f preV preR postV postR = case (decEq postV preV, decEq postR preR) of
     (No _, _) => empty
     (_, No _) => empty
     (Yes Refl, Yes Refl) => do
       (n ** lk) <- lookupGen preV
-      pure $ n #= !external_gen
+      pure $ n #= !(exprGen f)
 
-  r_ass_gen _ preV preR postV (rs `With` (reg, Just ty)) = case (decEq postV preV, decEq rs preR) of
-    (Yes Refl, Yes Refl) => pure $ reg %= !external_gen
+  r_ass_gen f preV preR postV (rs `With` (reg, Just ty)) = case (decEq postV preV, decEq rs preR) of
+    (Yes Refl, Yes Refl) => pure $ reg %= !(exprGen f)
     (No _, _)     => empty
     (_, No _)     => empty
   r_ass_gen _ preV preR postV _ = empty
@@ -379,13 +386,13 @@ namespace Statements_given_preV_preR_postV_postR -- implementations
       (bodyR ** _) <- eq_registers_gen f postR
       (_ ** body)  <- statement_gen f insideV postR bodyR
       --
-      pure $ for init !external_gen upd body
+      pure $ for init !(exprGen f) upd body
 
   if_gen f preV preR postV (Merge thR elR) = case decEq postV preV of
     Yes Refl => do
       (_ ** th) <- statement_gen f preV preR thR
       (_ ** el) <- statement_gen f preV preR elR
-      pure $ if__ !external_gen th el
+      pure $ if__ !(exprGen f) th el
     No _ => empty
   if_gen f preV preR postV _ = empty
 
@@ -400,10 +407,10 @@ namespace Statements_given_preV_preR_postV_postR -- implementations
       (_ ** stmt) <- statement_gen f preV preR postR
       pure $ block stmt
 
-  print_gen _ preV preR postV postR = case (decEq postV preV, decEq postR preR) of
+  print_gen f preV preR postV postR = case (decEq postV preV, decEq postR preR) of
     (No _, _) => empty
     (_, No _) => empty
-    (Yes Refl, Yes Refl) => pure $ print !(external_gen {ty=Expression _ _ String'})
+    (Yes Refl, Yes Refl) => pure $ print !(exprGen f {a=String'})
 
 namespace Statements_given_preV_preR_postR -- implementations
 
@@ -415,14 +422,14 @@ namespace Statements_given_preV_preR_postR -- implementations
     No _ => empty
     Yes Refl => pure (_ ** !external_gen. !external_gen)
 
-  v_ass_gen _ preV preR postR = case decEq postR preR of
+  v_ass_gen f preV preR postR = case decEq postR preR of
     No _ => empty
     Yes Refl => do
       (n ** lk) <- lookupGen preV
-      pure (_ ** n #= !external_gen)
+      pure (_ ** n #= !(exprGen f))
 
-  r_ass_gen _ preV preR (rs `With` (reg, Just ty)) = case decEq rs preR of
-    Yes Refl => pure $ (_ ** reg %= !external_gen)
+  r_ass_gen f preV preR (rs `With` (reg, Just ty)) = case decEq rs preR of
+    Yes Refl => pure $ (_ ** reg %= !(exprGen f))
     No _ => empty
   r_ass_gen _ preV preR _ = empty
 
@@ -435,12 +442,12 @@ namespace Statements_given_preV_preR_postR -- implementations
     (bodyR ** _) <- eq_registers_gen f postR
     (_ ** body)  <- statement_gen f insideV postR bodyR
     --
-    pure (_ ** for init !external_gen upd body)
+    pure (_ ** for init !(exprGen f) upd body)
 
   if_gen f preV preR (Merge thR elR) = do
       (_ ** th) <- statement_gen f preV preR thR
       (_ ** el) <- statement_gen f preV preR elR
-      pure (_ ** if__ !external_gen th el)
+      pure (_ ** if__ !(exprGen f) th el)
   if_gen f preV preR _ = empty
 
   seq_gen f preV preR postR = do
@@ -452,6 +459,6 @@ namespace Statements_given_preV_preR_postR -- implementations
     (_ ** stmt) <- statement_gen f preV preR postR
     pure $ (_ ** block stmt)
 
-  print_gen _ preV preR postR = case decEq postR preR of
+  print_gen f preV preR postR = case decEq postR preR of
     No _ => empty
-    Yes Refl => pure $ (_ ** print !(external_gen {ty=Expression _ _ String'}))
+    Yes Refl => pure $ (_ ** print !(exprGen f {a=String'}))

examples/pil-reg/src/Example/Pil/Lang.idr

@@ -5,3 +5,19 @@ import public Data.List.Lookup
 
 import public Example.Pil.Lang.Expression
 import public Example.Pil.Lang.Statement
+
+public export
+SomeOps : Ops
+SomeOps = MkOps
+  {unary = [ (Int', "inc", Int')
+           , (String', "as_str", Int')
+           , (Bool', "!", Bool')
+           ]}
+  {binary = [ (Int', "+", Int', Int')
+            , (Int', "*", Int', Int')
+            , (String', "concat", String', String')
+            , (Bool', "&&", Bool', Bool')
+            , (Bool', "||", Bool', Bool')
+            , (Bool', "<", Int', Int')
+            , (Bool', "<=", Int', Int')
+            ]}

examples/pil-reg/src/Example/Pil/Lang/Expression.idr

@@ -9,40 +9,44 @@ import public Example.Pil.Lang.Aspects.Registers
 %default total
 
 public export
-data Expression : (vars : Variables) -> (regs : Registers rc) -> (res : Type') -> Type where
+record Ops where
+  constructor MkOps
+  unary  : List (Type', String, Type')
+  binary : List (Type', String, Type', Type')
+
+public export
+data Expression : Ops -> (vars : Variables) -> (regs : Registers rc) -> (res : Type') -> Type where
   -- Constant expression
-  C' : {ty : Type'} -> (x : idrTypeOf ty) -> Expression vars regs ty
+  C' : {ty : Type'} -> (x : idrTypeOf ty) -> Expression ops vars regs ty
 
   -- Value of the variable
-  V : (n : Name) -> (0 lk : Lookup n vars) => Expression vars regs lk.reveal
+  V : (n : Name) -> (0 lk : Lookup n vars) => Expression ops vars regs lk.reveal
 
   -- Value of the register
-  R : (r : Fin rc) -> (0 _ : IsJust $ index r regs) => Expression vars regs $ fromJust $ index r regs
+  R : (r : Fin rc) -> (0 _ : IsJust $ index r regs) => Expression ops vars regs $ fromJust $ index r regs
 
   -- Unary operation over the result of another expression
-  U : {default "?func" opName : String} ->
-      (f : idrTypeOf a -> idrTypeOf b) ->
-      Expression vars regs a -> Expression vars regs b
+  U : (lk : Lookup res ops.unary) =>
+      Expression ops vars regs (snd lk.reveal) -> Expression ops vars regs res
 
   -- Binary operation over the results of two another expressions
-  B : {default "??" opName : String} ->
-      (f : idrTypeOf a -> idrTypeOf b -> idrTypeOf c) ->
-      Expression vars regs a -> Expression vars regs b -> Expression vars regs c
+  B : (lk : Lookup res ops.binary) =>
+      Expression ops vars regs (fst $ snd lk.reveal) -> Expression ops vars regs (snd $ snd lk.reveal) -> Expression ops vars regs res
 
 namespace Int
 
   public export %inline
-  C : Int -> Expression vars regs Int'
+  C : Int -> Expression ops vars regs Int'
   C x = C' x
 
 namespace Bool
 
   public export %inline
-  C : Bool -> Expression vars regs Bool'
+  C : Bool -> Expression ops vars regs Bool'
   C x = C' x
 
 namespace String
 
   public export %inline
-  C : String -> Expression vars regs String'
+  C : String -> Expression ops vars regs String'
   C x = C' x

examples/pil-reg/src/Example/Pil/Lang/ShowC.idr

@@ -17,20 +17,21 @@ makeFuncName : String -> String
 makeFuncName = pack . map (\k => if isAlphaNum k then k else '_') . unpack
 
 export
-Show (Expression vars regs a) where
+Show (Expression ops vars regs a) where
   show (C' {ty=Bool'}   x) = show x
   show (C' {ty=Int'}    x) = show x
   show (C' {ty=String'} x) = show x
   show (V n)              = show n
   show (R r)              = "[[" ++ show (finToNat r) ++ "]]"
-  show (U {opName} _ e)   = opName ++ "(" ++ show e ++ ")"
-  show (B {opName} _ l r) = if looksLikeInfixOperator opName
+  show (U @{lk} e)   = let opName = fst lk.reveal in opName ++ "(" ++ show e ++ ")"
+  show (B @{lk} l r) = let opName = fst lk.reveal in
+    if looksLikeInfixOperator opName
       then wr l ++ " " ++ opName ++ " " ++ wr r
       else makeFuncName opName ++ "(" ++ show l ++ ", " ++ show r ++ ")"
     where
-    wr : Expression vars regs x -> String
-    wr e@(B _ _ _) = "(" ++ show e ++ ")"
-    wr e           = show e
+    wr : Expression ops vars regs x -> String
+    wr e@(B _ _) = "(" ++ show e ++ ")"
+    wr e         = show e
 
 --- Statements ---
 
@@ -39,7 +40,7 @@ Show Type' where
   show Int'    = "int"
   show String' = "char *"
 
-isNopDeeply : Statement preV preR postV postR -> Bool
+isNopDeeply : Statement ops preV preR postV postR -> Bool
 isNopDeeply Nop      = True
 isNopDeeply (x >> y) = isNopDeeply x && isNopDeeply y
 isNopDeeply _        = False
@@ -48,7 +49,7 @@ isNopDeeply _        = False
 n : Nat -> Nat
 n = (+ 2)
 
-showInd : (indent : Nat) -> Statement preV preR postV postR -> String
+showInd : (indent : Nat) -> Statement ops preV preR postV postR -> String
 showInd i Nop = ""
 showInd i (ty . n) = indent i $ show ty ++ " " ++ show n ++ ";"
 showInd i (n #= v) = indent i $ show n ++ " = " ++ show v ++ ";"
@@ -82,5 +83,5 @@ showInd i (Block x) = indent i "{\n" ++ showInd (n i) x ++ "\n" ++ indent i "}"
 showInd i (Print x) = indent i $ "puts(" ++ show x ++ ");"
 
 export
-Show (Statement preV preR postV postR) where
+Show (Statement ops preV preR postV postR) where
   show = showInd 0