content: module StrategoProp where
  import StrategoTerm
  import StrategoPattern
  import StrategoType
  import Parentheses
  
  --signature  sorts Sequent Rule
  
  data Sequent
    = Valid
    | Consequence ([Prop], [Prop])
    deriving (Show{-,Read-})
  
  data Rule
     = Conclude ([Sequent], Sequent)
    deriving (Show{-,Read-})
  
  
  --signature   sorts Prop PropDecl Qvar
  
  data Prop
    = True                                         {- truth value -}
    | False                                        {- truth value -}
    | PropVar     (P String)                       {- Propositional variable -}
    | Has         (Term, Pred)                     {- Unary predicate applic. -}
    | HasMult     ([Term], Pred)                   {- k-ary predicate applic. -}
    | Equal       (Term, Term)                     {- equality assertion -}
    | Conj        (P [Prop])                       {- propositional conjunct -}
    | Disj        (P [Prop])                       {- propositional disjunct -}
    | Implies     ([Prop], Prop)                   {- implication chain -}
    | Equiv       (Prop, Prop)                     {- equivalence -}
    | Neg         (P Prop)                         {- negation -}
    | Quant       ([Qvar], Prop)                   {- quantified proposition -}
    deriving (Show{-,Read-})
  
  propVar = PropVar . P
  propConj = Conj . P
  propDisj = Disj . P
  propNeg = Neg . P
  
  data Qvar
    = All         (String, Type)                   {- universal quantification -}
    | Exists      (String, Type)                   {- existential  quantification -}
    deriving (Show{-,Read-})
  
  type Identifier = String -- ??
  
  data PropDecl
    = PropDecl   (Identifier, Prop)                {- prop. declaration -}
    deriving (Show{-,Read-})
  
  
  --signature sorts Pred PredPat PredFormula PredDecl
  
  data Pred
  {-  PredConst : String -> Pred -}           {- predicate constant -}
    = Univ
    | UnDef
  --  Just        Pred                          {- case match predicate -}
  --  Nothing                                   {- match failure predicate -}
    | Arrow       (Pred, Pred)                  {- arrow predicate -}
    | LfpPred     (String, Pred)                {- least fixed-point predicate -}
    | GfpPred     (String, Pred)               {- greatest fixed-point predicate-}
  --  PredRef     Identifier                    {- predicate reference ? -}
    | PredVar     (P Identifier)                {- predicate variable -}
    | LiftedSec   (P Term)                      {- lifted section predicate -}
  --  PredSect    Pred * Int                    {- predicate section  (1 or 2) -}
    | PredNeg     (P Pred)                      {- negated predicate -}
    | Strong      (P Pred)                      {- strengthened predicate -}
  --  TypedPred   Pred * Type                   {- explicitly typed predicate -}
    | TuplePred   (P [Pred])                    {- tuple predicate -}
    | LitPred     (P Int)                       {- literal predicate -}
    | DataCong    (String, [PredArg])           {- constructor congruence pred. -}
  --  PredInst    String * [Term]               {- predicate instance -}
    | Comprehension ([Pattern], Prop)           {- set comprehension -}
    | PredDisj    (P [Pred])                    {- pred. disjunction -}
    | PredConj    (P [Pred])                    {- pred. conjunction -}
    | PredImpl    ([Pred], Pred)                {- pred. implication chain -}
    | PredEquiv   (Pred, Pred)                  {- pred. equivalence -}
    deriving (Show{-,Read-})
  
  predVar = PredVar . P
  liftedSec = LiftedSec . P
  predNeg = PredNeg . P
  strong = Strong . P
  tuplePred = TuplePred . P
  litPred = LitPred . P
  predDisj = PredDisj . P
  predConj = PredConj . P
  
  data PredArg
    = TermArg (P Term)
    | PredArg (P Pred)
    deriving (Show)
  
  termArg = TermArg . P
  predArg = PredArg . P
  
  data PredPat
    = PredAbs    (String, [Param])  {- pred. abstraction -}
    deriving (Show{-,Read-})
  
  data Param
    = TermParam (P String)
    | PredParam (P String)
    deriving (Show)
  
  termParam = TermParam . P
  predParam = PredParam . P
  
  data PredDecl
    = PredDecl   (PredPat, Pred)            {- pred. declaration -}
    deriving (Show{-,Read-})
  