\import Logic.Rewriting.TRS.HRS
\import Logic.Rewriting.TRS.MetaContexts
\import Logic.Rewriting.TRS.Utils
\import Data.List (nil, ::)

\data SingularSort | lc-term

\data LC-Symbols : \Set | abstraction | application

\instance LC-FSignature : FSignature SingularSort \cowith
  | symbol sort => LC-Symbols
  | domain symb => \case \elim symb \with {
    | abstraction => (lc-term :: nil, lc-term) :: nil
    | application => (nil, lc-term) :: (nil, lc-term) :: nil
  }

\data MetaVariables | metavar-a | metavar-b

\func BetaRedexContext : MetaContext SingularSort \cowith
  | metaname sort => MetaVariables
  | m-domain var => \case \elim var \with {
    | metavar-a => lc-term :: nil
    | metavar-b => nil
  }

\func BetaRedex : Term LC-FSignature nil lc-term BetaRedexContext =>
  func application
      (\lam i => \case \elim i \with {
        |  => func abstraction (\lam  => metavar metavar-a (\lam  => var  idp))
        |  => metavar metavar-b impossible-lambda
      })

\func BetaResult : Term LC-FSignature nil lc-term BetaRedexContext =>
  metavar metavar-a (\lam  => metavar metavar-b impossible-lambda)

\func beta-reduction : RewriteRule lc-term \cowith
  | rr-mc => BetaRedexContext
  | rr-l => BetaRedex
  | rr-r => BetaResult
  | rr-l-func-root => T-has-functional-root {LC-FSignature}

\func LC-rules : RuleRegistry LC-FSignature \cowith
  | rule-J (lc-term) => \Sigma
  | rule-container {(lc-term)} () => beta-reduction

\instance UntypedLambdaCalculus  : SimpleHigherOrderTermRewritingSystem \cowith
  | env => LC-FSignature
  | set-of-rules => LC-rules
  | meta-context => EmptyMetaContext {LC-FSignature}


-- \x.\y.x
\func K : Term LC-FSignature nil lc-term (EmptyMetaContext {LC-FSignature})
  => func abstraction
      (\lam  => func abstraction (\lam  => var  idp))

-- \x.x
\func I : Term LC-FSignature nil lc-term (EmptyMetaContext {LC-FSignature})
  => func abstraction
      (\lam  => var  idp)

-- (\x.x) (\x.x)
\func I_I : PureTerm LC-FSignature nil lc-term =>
  func application (\lam i => \case \elim i \with { |  => I |  => I })

\func suitable-substitution : MetaSubstitution LC-FSignature nil BetaRedexContext (EmptyMetaContext {LC-FSignature}) =>
  \lam {(lc-term)} mvar => \case \elim mvar \with {
    | metavar-a => var  idp
    | metavar-b => I
  }

\func I_I~>I : RewriteRelation LC-rules I_I I =>
  rewrite-with-rule () suitable-substitution (Term.fext (\lam index => \case \elim index \with {
    |  => Term.fext (\lam  => idp)
    |  => Term.fext (\lam  => idp)
  })
  ) (Term.fext (\lam  => idp))