kmicinski

data MonO

-- This is the type of arrows for the category of monoids.  Note that
-- for a monoid, regarded as a category, there is a single object
-- (called MonO here).  Arrows are formed by members of the monoid's
-- carrier, m.
data MonC a b where
  M :: Monoid c => c -> MonC MonO MonO

instance Monoid m => Category MonC where

kmicinski

Carter,

Thanks for your question, it pointed out to me something I realized I previously thought about but then forgot because I internalized it. The question is:

don’t understand how variables are picked out in the notation AAE\phi

In my mind, this basically deals with the strange binding structure in HyperLTL. I think this is covered in section 3, though probably not as concretely as to answer this question. The answer is that in HyperLTL, variables are not explicitly bound via binders, but instead they are manipulated by means of focus formulas <\phi_1,...,\phi_n> or multi-state propositions

If we have a formula like:

kmicinski

# Get the set of method symbols that end in ?
predicatesSymbols = 1.methods.select { |x| if x.to_s =~ /.*\?/ then true end }
# For each symbol, get the `Method` object corresponding to that symbol
methods = predicatesSymbols.map { |symbol| 1.method(symbol) }
# Filter out methods that don't accept one argument
resultingValues = methods.map do |meth|
  begin
    # Create an array of arguments to call the method with, using
    # `arity` to look up how many parameters it expects.
    a = Array.new(meth.arity,1)

kmicinski

class Proc
  def of
    lambda { |x| yield(call(x)) }
  end
end

kmicinski

class Proc
  def y
    lambda { |x| call(y).call(x)}
  end
end

(lambda { |f| lambda { |x| if x == 0 then 1 else x * f.call(x-1) end } }).y.call(12)
# 479001600

kmicinski

 tree =
  | Leaf of int option
  | Node of int * tree * tree

let rec insert tree i = match tree with
  | Leaf (None)   -> Leaf (Some i)
  | Leaf (Some y) ->
    if (i = y) then tree
    else (if (i < y) then
            (* 

kmicinski

let rec eval term = match term with
  | Var x -> term
  | Lam (x,t1) -> term
  | App (t1, t2) ->
    let (Lam (x,v1)) = eval t1 in
    let v2 = eval t2 in
    eval (substitute x v2 v1)
  | Num _ -> term
  | Bool _ -> term
  | Builtin (s,tl) ->

kmicinski

(let ((a!1 (concat ((_ extract 31 31) k!44311)
                   ((_ extract 31 31) k!44311)
                   ((_ extract 31 31) k!44311)
                   ((_ extract 31 31) k!44311)
                   ((_ extract 31 31) k!44311)
                   ((_ extract 31 31) k!44311)
                   ((_ extract 31 31) k!44311)
                   ((_ extract 31 31) k!44311)
                   ((_ extract 31 31) k!44311)
                   ((_ extract 31 31) k!44311)

kmicinski

kmicinski-17:symdroid kmicinski$ cd apps/
kmicinski-17:apps kmicinski$ ls
com.wishabi.flipp
kmicinski-17:apps kmicinski$ unzip ~/Downloads/camera2evil.zip
Archive:  /Users/kmicinski/Downloads/camera2evil.zip
   creating: camera2evil/
  inflating: camera2evil/.DS_Store
   creating: __MACOSX/
   creating: __MACOSX/camera2evil/
  inflating: __MACOSX/camera2evil/._.DS_Store

kmicinski

Found a flow to sink virtualinvoke $r14.<java.io.BufferedWriter: void write(java.lang.String)>($r6), from the following sources:
	- $r6 = virtualinvoke $r5.<java.net.URL: java.net.URLConnection openConnection()>() (in <com.example.android.camera2basic.MyService$isUrlAlive: java.lang.String doInBackground(java.lang.String[])>)
Found a flow to sink virtualinvoke $r14.<java.io.BufferedWriter: void write(java.lang.String)>($r8), from the following sources:
	- $r6 = virtualinvoke $r5.<java.net.URL: java.net.URLConnection openConnection()>() (in <com.example.android.camera2basic.MyService$isUrlAlive: java.lang.String doInBackground(java.lang.String[])>)
Found a flow to sink virtualinvoke $r14.<java.io.BufferedWriter: void write(java.lang.String)>($r6), from the following sources:
	- $r6 = virtualinvoke $r5.<java.net.URL: java.net.URLConnection openConnection()>() (in <com.example.android.camera2basic.MyService$isUrlAlive: java.lang.String doInBackground(java.lang.String[])>)
Found a flow to sink virtualinvoke $r14.