content: module Logic where
  
  data Prop =
      Pred Ident [Exp] 
    | And Prop Prop
    | Or  Prop Prop
    | If  Prop Prop
    | Not Prop
    | All   Prop
    | Exist Prop
   deriving Show
  
  data Exp = 
      App Ident [Exp]
    | Var Int -- de Bruijn index
   deriving Show
  
  type Ident = String
  
  data Model a = Model {
    app  :: Ident -> [a] -> a,
    prd  :: Ident -> [a] -> Bool,
    dom  :: [a]
    }
  
  type Assignment a = [a]
  
  update :: a -> Assignment a -> Assignment a
  update x assign = x : assign
  
  look :: Int -> Assignment a -> a
  look i assign = assign !! i
  
  valExp :: Model a -> Assignment a -> Exp -> a
  valExp model assign exp = case exp of
    App f xs -> app model f (map (valExp model assign) xs)
    Var i    -> look i assign
  
  valProp :: Model a -> Assignment a -> Prop -> Bool
  valProp model assign prop = case prop of
    Pred f xs -> prd model f (map (valExp model assign) xs)
    And  a b  -> v a && v b
    Or   a b  -> v a || v b
    If   a b  -> if v a then v b else True
    Not  a    -> not (v a)
    All   p   -> all (\x -> valProp model (update x assign) p) (dom model)
    Exist p   -> any (\x -> valProp model (update x assign) p) (dom model)
   where
     v = valProp model assign
  
  liftProp :: Int -> Prop -> Prop
  liftProp i p = case p of
    Pred f xs -> Pred f (map liftExp xs)
    And a b   -> And (lift a) (lift b)
    Or  a b   -> Or (lift a) (lift b)
    If  a b   -> If (lift a) (lift b)
    Not a     -> Not (lift a)
    All p     -> All (liftProp (i+1) p)
    Exist p   -> Exist (liftProp (i+1) p)
   where
     lift = liftProp i
     liftExp e = case e of
       App f xs -> App f (map liftExp xs)
       Var j    -> Var (j + i)
       _ -> e
  
  
  -- example: initial segments of integers
  
  intModel :: Int -> Model Int
  intModel mx = Model {
    app = \f xs -> case (f,xs) of
      ("+",_) -> sum xs
      (_,[])  -> read f,
    prd = \f xs -> case (f,xs) of
      ("E",[x])   -> even x
      ("<",[x,y]) -> x < y
      ("=",[x,y]) -> x == y
      _ -> error "undefined val",
    dom = [0 .. mx]
    }
  
  exModel = intModel 100
  
  ev x   = Pred "E" [x]
  lt x y = Pred "<" [x,y]
  eq x y = Pred "=" [x,y]
  int i = App (show i) []
  
  ex1 :: Prop
  ex1 = Exist (ev (Var 0))
  
  ex2 :: Prop
  ex2 = All (Exist (lt (Var 1) (Var 0)))
  
  ex3 :: Prop
  ex3 = All (If (lt (Var 0) (int 100)) (Exist (lt (Var 1) (Var 0))))
  
  ex4 :: Prop
  ex4 = All (All (If (lt (Var 1) (Var 0)) (Not (lt (Var 0) (Var 1)))))
  
  