--
-- Copyright 2016, NICTA
--
-- This software may be distributed and modified according to the terms of
-- the GNU General Public License version 2. Note that NO WARRANTY is provided.
-- See "LICENSE_GPLv2.txt" for details.
--
-- @TAG(NICTA_GPL)
--

{-# LANGUAGE QuasiQuotes #-}
module Isabelle.TestTH where

import Text.PrettyPrint.ANSI.Leijen
import Isabelle.InnerAST
import Isabelle.OuterAST
import Isabelle.ExprTH

val :: Theory Type Term
val = let theoryName = "Test"
          defName = "deffo"
          typ = [isaType| int \<times> int \<Rightarrow> int |]
          term = [isaTerm| (\<lambda>x. x) y |]

        in [isaTheory|
         theory $theoryName
         imports Main
         begin
           type_synonym n = "nat"
           definition "(B \<or> C) \<and> D"
           definition "B \<or> (C \<and> D)"
           definition "(A \<equiv> B) \<longrightarrow> C"
           definition "A \<equiv> (B \<longrightarrow> C)"
           definition "\<exists> a b c. (A \<longrightarrow> C)"
           definition "(\<exists> a b c. A) \<longrightarrow> C"
           definition "True"
           definition "A x \<equiv> B x"
           definition "\<lambda>x. (x y)"
           definition "$term"
           definition "((\<lambda>x. x) y) \<equiv> (B (x y))"

           definition x :: "'a \<Rightarrow> 'b" where "A"
           definition $defName :: "$typ" where "A"
           definition x :: "int \<times> (int \<Rightarrow> int)" where "A"
           definition x :: "'a option \<Rightarrow> 'b" where "A"
           definition x :: "('a, ('b \<times> 'e) \<times> 'd) test \<Rightarrow> 'c" where "A"
           definition "A :: bool \<equiv> B"

           lemma lemma1[attribute1, attribute2 with args]: "A \<and> B"
             apply clarsimp
             done

           lemma "A \<longrightarrow> B"
             apply (clarsimp simp: blah foo bar dest: baz, clarsimp, (clarsimp | clarsimp))?
             sorry

         end
       |]

main :: IO ()
main = putDoc . pretty $ val