changeset 0:776f851a03a3

reflection and tactics
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 15 Mar 2019 17:35:46 +0900
parents
children 6f01428aaf2d
files hello.agda reflection-ex.agda tactics.agda
diffstat 3 files changed, 443 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/hello.agda	Fri Mar 15 17:35:46 2019 +0900
@@ -0,0 +1,10 @@
+
+module hello where
+
+open import IO
+open import Data.Bool
+open import Data.String
+open import Data.Nat
+
+main = run (putStrLn "Hello, World!")
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/reflection-ex.agda	Fri Mar 15 17:35:46 2019 +0900
@@ -0,0 +1,380 @@
+module reflection-ex where
+
+open import Data.Bool
+open import Data.String
+open import Data.Nat
+
+postulate Name : Set
+{-# BUILTIN QNAME Name #-}
+
+primitive
+  primQNameEquality : Name → Name → Bool
+  primQNameLess     : Name → Name → Bool
+  primShowQName     : Name → String
+
+nameOfNat : Name
+nameOfNat = quote ℕ
+
+isNat : Name → Bool
+isNat (quote ℕ) = true
+isNat _           = false
+
+postulate Meta : Set
+{-# BUILTIN AGDAMETA Meta #-}
+
+primitive
+  primMetaEquality : Meta → Meta → Bool
+  primMetaLess     : Meta → Meta → Bool
+  primShowMeta     : Meta → String
+
+open import Data.Word 
+open import Data.Float 
+open import Data.Char 
+
+data Literal : Set where
+  nat    : (n : ℕ)    → Literal
+  word64 : (n : Word64) → Literal
+  float  : (x : Float)  → Literal
+  char   : (c : Char)   → Literal
+  string : (s : String) → Literal
+  name   : (x : Name)   → Literal
+  meta   : (x : Meta)   → Literal
+
+{-# BUILTIN AGDALITERAL   Literal #-}
+{-# BUILTIN AGDALITNAT    nat     #-}
+{-# BUILTIN AGDALITWORD64 word64  #-}
+{-# BUILTIN AGDALITFLOAT  float   #-}
+{-# BUILTIN AGDALITCHAR   char    #-}
+{-# BUILTIN AGDALITSTRING string  #-}
+{-# BUILTIN AGDALITQNAME  name    #-}
+{-# BUILTIN AGDALITMETA   meta    #-}
+
+data Visibility : Set where
+  visible hidden instance′ : Visibility
+
+{-# BUILTIN HIDING   Visibility #-}
+{-# BUILTIN VISIBLE  visible    #-}
+{-# BUILTIN HIDDEN   hidden     #-}
+{-# BUILTIN INSTANCE instance′  #-}
+
+data Relevance : Set where
+  relevant irrelevant : Relevance
+
+{-# BUILTIN RELEVANCE  Relevance  #-}
+{-# BUILTIN RELEVANT   relevant   #-}
+{-# BUILTIN IRRELEVANT irrelevant #-}
+
+data ArgInfo : Set where
+  arg-info : (v : Visibility) (r : Relevance) → ArgInfo
+
+data Arg (A : Set) : Set where
+  arg : (i : ArgInfo) (x : A) → Arg A
+
+{-# BUILTIN ARGINFO    ArgInfo  #-}
+{-# BUILTIN ARGARGINFO arg-info #-}
+{-# BUILTIN ARG        Arg      #-}
+{-# BUILTIN ARGARG     arg      #-}
+
+
+open import Data.List
+
+data Pattern : Set where
+  con    : (c : Name) (ps : List (Arg Pattern)) → Pattern
+  dot    : Pattern
+  var    : (s : String)  → Pattern
+  lit    : (l : Literal) → Pattern
+  proj   : (f : Name)    → Pattern
+  absurd : Pattern
+
+{-# BUILTIN AGDAPATTERN   Pattern #-}
+{-# BUILTIN AGDAPATCON    con     #-}
+{-# BUILTIN AGDAPATDOT    dot     #-}
+{-# BUILTIN AGDAPATVAR    var     #-}
+{-# BUILTIN AGDAPATLIT    lit     #-}
+{-# BUILTIN AGDAPATPROJ   proj    #-}
+{-# BUILTIN AGDAPATABSURD absurd  #-}
+
+data Abs (A : Set) : Set where
+  abs : (s : String) (x : A) → Abs A
+
+{-# BUILTIN ABS    Abs #-}
+{-# BUILTIN ABSABS abs #-}
+
+data Term : Set
+data Sort : Set
+data Clause : Set
+Type = Term
+
+data Term where
+  var       : (x : ℕ) (args : List (Arg Term)) → Term
+  con       : (c : Name) (args : List (Arg Term)) → Term
+  def       : (f : Name) (args : List (Arg Term)) → Term
+  lam       : (v : Visibility) (t : Abs Term) → Term
+  pat-lam   : (cs : List Clause) (args : List (Arg Term)) → Term
+  pi        : (a : Arg Type) (b : Abs Type) → Term
+  agda-sort : (s : Sort) → Term
+  lit       : (l : Literal) → Term
+  meta      : (x : Meta) → List (Arg Term) → Term
+  unknown   : Term -- Treated as '_' when unquoting.
+
+data Sort where
+  set     : (t : Term) → Sort -- A Set of a given (possibly neutral) level.
+  lit     : (n : ℕ) → Sort  -- A Set of a given concrete level.
+  unknown : Sort
+
+data Clause where
+  clause        : (ps : List (Arg Pattern)) (t : Term) → Clause
+  absurd-clause : (ps : List (Arg Pattern)) → Clause
+
+{-# BUILTIN AGDASORT    Sort   #-}
+{-# BUILTIN AGDATERM    Term   #-}
+{-# BUILTIN AGDACLAUSE  Clause #-}
+
+{-# BUILTIN AGDATERMVAR         var       #-}
+{-# BUILTIN AGDATERMCON         con       #-}
+{-# BUILTIN AGDATERMDEF         def       #-}
+{-# BUILTIN AGDATERMMETA        meta      #-}
+{-# BUILTIN AGDATERMLAM         lam       #-}
+{-# BUILTIN AGDATERMEXTLAM      pat-lam   #-}
+{-# BUILTIN AGDATERMPI          pi        #-}
+{-# BUILTIN AGDATERMSORT        agda-sort #-}
+{-# BUILTIN AGDATERMLIT         lit       #-}
+{-# BUILTIN AGDATERMUNSUPPORTED unknown   #-}
+
+{-# BUILTIN AGDASORTSET         set     #-}
+{-# BUILTIN AGDASORTLIT         lit     #-}
+{-# BUILTIN AGDASORTUNSUPPORTED unknown #-}
+
+{-# BUILTIN AGDACLAUSECLAUSE clause        #-}
+{-# BUILTIN AGDACLAUSEABSURD absurd-clause #-}
+
+data Definition : Set where
+  function    : (cs : List Clause) → Definition
+  data-type   : (pars : ℕ) (cs : List Name) → Definition  -- parameters and constructors
+  record-type : (c : Name) (fs : List (Arg Name)) →         -- c: name of record constructor
+                Definition                                  -- fs: fields
+  data-cons   : (d : Name) → Definition                     -- d: name of data type
+  axiom       : Definition
+  prim-fun    : Definition
+
+{-# BUILTIN AGDADEFINITION                Definition  #-}
+{-# BUILTIN AGDADEFINITIONFUNDEF          function    #-}
+{-# BUILTIN AGDADEFINITIONDATADEF         data-type   #-}
+{-# BUILTIN AGDADEFINITIONRECORDDEF       record-type #-}
+{-# BUILTIN AGDADEFINITIONDATACONSTRUCTOR data-cons   #-}
+{-# BUILTIN AGDADEFINITIONPOSTULATE       axiom       #-}
+{-# BUILTIN AGDADEFINITIONPRIMITIVE       prim-fun    #-}
+
+-- Error messages can contain embedded names and terms.
+data ErrorPart : Set where
+  strErr  : String → ErrorPart
+  termErr : Term → ErrorPart
+  nameErr : Name → ErrorPart
+
+{-# BUILTIN AGDAERRORPART       ErrorPart #-}
+{-# BUILTIN AGDAERRORPARTSTRING strErr    #-}
+{-# BUILTIN AGDAERRORPARTTERM   termErr   #-}
+{-# BUILTIN AGDAERRORPARTNAME   nameErr   #-}
+
+postulate
+  TC       : ∀ {a} → Set a → Set a
+  returnTC : ∀ {a} {A : Set a} → A → TC A
+  bindTC   : ∀ {a b} {A : Set a} {B : Set b} → TC A → (A → TC B) → TC B
+
+
+{-# BUILTIN AGDATCM       TC       #-}
+{-# BUILTIN AGDATCMRETURN returnTC #-}
+{-# BUILTIN AGDATCMBIND   bindTC   #-}
+
+open import Data.Unit
+open import Data.Product
+
+postulate
+  -- Unify two terms, potentially solving metavariables in the process.
+  unify : Term → Term → TC ⊤
+
+  -- Throw a type error. Can be caught by catchTC.
+  typeError : ∀ {a} {A : Set a} → List ErrorPart → TC A
+
+  -- Block a type checking computation on a metavariable. This will abort
+  -- the computation and restart it (from the beginning) when the
+  -- metavariable is solved.
+  blockOnMeta : ∀ {a} {A : Set a} → Meta → TC A
+
+  -- Prevent current solutions of metavariables from being rolled back in
+  -- case 'blockOnMeta' is called.
+  commitTC : TC ⊤
+
+  -- Backtrack and try the second argument if the first argument throws a
+  -- type error.
+  catchTC : ∀ {a} {A : Set a} → TC A → TC A → TC A
+
+  -- Infer the type of a given term
+  inferType : Term → TC Type
+
+  -- Check a term against a given type. This may resolve implicit arguments
+  -- in the term, so a new refined term is returned. Can be used to create
+  -- new metavariables: newMeta t = checkType unknown t
+  checkType : Term → Type → TC Term
+
+  -- Compute the normal form of a term.
+  normalise : Term → TC Term
+
+  -- Compute the weak head normal form of a term.
+  reduce : Term → TC Term
+-- Get the current context. Returns the context in reverse order, so that
+  -- it is indexable by deBruijn index. Note that the types in the context are
+  -- valid in the rest of the context. To use in the current context they need
+  -- to be weakened by 1 + their position in the list.
+  getContext : TC (List (Arg Type))
+
+  -- Extend the current context with a variable of the given type.
+  extendContext : ∀ {a} {A : Set a} → Arg Type → TC A → TC A
+
+  -- Set the current context. Takes a context telescope with the outer-most
+  -- entry first, in contrast to 'getContext'. Each type should be valid in the
+  -- context formed by the preceding elements in the list.
+  inContext : ∀ {a} {A : Set a} → List (Arg Type) → TC A → TC A
+
+  -- Quote a value, returning the corresponding Term.
+  quoteTC : ∀ {a} {A : Set a} → A → TC Term
+
+  -- Unquote a Term, returning the corresponding value.
+  unquoteTC : ∀ {a} {A : Set a} → Term → TC A
+
+  -- Create a fresh name.
+  freshName : String → TC Name
+
+  -- Declare a new function of the given type. The function must be defined
+  -- later using 'defineFun'. Takes an Arg Name to allow declaring instances
+  -- and irrelevant functions. The Visibility of the Arg must not be hidden.
+  declareDef : Arg Name → Type → TC ⊤
+
+  -- Declare a new postulate of the given type. The Visibility of the Arg
+  -- must not be hidden. It fails when executed from command-line with --safe
+  -- option.
+  declarePostulate : Arg Name → Type → TC ⊤
+
+  -- Define a declared function. The function may have been declared using
+  -- 'declareDef' or with an explicit type signature in the program.
+  defineFun : Name → List Clause → TC ⊤
+
+  -- Get the type of a defined name. Replaces 'primNameType'.
+  getType : Name → TC Type
+
+  -- Get the definition of a defined name. Replaces 'primNameDefinition'.
+  getDefinition : Name → TC Definition
+
+  -- Check if a name refers to a macro
+  isMacro : Name → TC Bool
+
+  -- Change the behaviour of inferType, checkType, quoteTC, getContext
+  -- to normalise (or not) their results. The default behaviour is no
+  -- normalisation.
+  withNormalisation : ∀ {a} {A : Set a} → Bool → TC A → TC A
+
+  -- Prints the third argument if the corresponding verbosity level is turned
+  -- on (with the -v flag to Agda).
+  debugPrint : String → ℕ → List ErrorPart → TC ⊤
+
+  -- Fail if the given computation gives rise to new, unsolved
+  -- "blocking" constraints.
+  noConstraints : ∀ {a} {A : Set a} → TC A → TC A
+
+  -- Run the given TC action and return the first component. Resets to
+  -- the old TC state if the second component is 'false', or keep the
+  -- new TC state if it is 'true'.
+  runSpeculative : ∀ {a} {A : Set a} → TC (Σ A λ _ → Bool) → TC A
+
+{-# BUILTIN AGDATCMUNIFY              unify              #-}
+{-# BUILTIN AGDATCMTYPEERROR          typeError          #-}
+{-# BUILTIN AGDATCMBLOCKONMETA        blockOnMeta        #-}
+{-# BUILTIN AGDATCMCATCHERROR         catchTC            #-}
+{-# BUILTIN AGDATCMINFERTYPE          inferType          #-}
+{-# BUILTIN AGDATCMCHECKTYPE          checkType          #-}
+{-# BUILTIN AGDATCMNORMALISE          normalise          #-}
+{-# BUILTIN AGDATCMREDUCE             reduce             #-}
+{-# BUILTIN AGDATCMGETCONTEXT         getContext         #-}
+{-# BUILTIN AGDATCMEXTENDCONTEXT      extendContext      #-}
+{-# BUILTIN AGDATCMINCONTEXT          inContext          #-}
+{-# BUILTIN AGDATCMQUOTETERM          quoteTC            #-}
+{-# BUILTIN AGDATCMUNQUOTETERM        unquoteTC          #-}
+{-# BUILTIN AGDATCMFRESHNAME          freshName          #-}
+{-# BUILTIN AGDATCMDECLAREDEF         declareDef         #-}
+{-# BUILTIN AGDATCMDECLAREPOSTULATE   declarePostulate   #-}
+{-# BUILTIN AGDATCMDEFINEFUN          defineFun          #-}
+{-# BUILTIN AGDATCMGETTYPE            getType            #-}
+{-# BUILTIN AGDATCMGETDEFINITION      getDefinition      #-}
+{-# BUILTIN AGDATCMCOMMIT             commitTC           #-}
+{-# BUILTIN AGDATCMISMACRO            isMacro            #-}
+{-# BUILTIN AGDATCMWITHNORMALISATION  withNormalisation  #-}
+{-# BUILTIN AGDATCMDEBUGPRINT         debugPrint         #-}
+{-# BUILTIN AGDATCMNOCONSTRAINTS      noConstraints      #-}
+{-# BUILTIN AGDATCMRUNSPECULATIVE     runSpeculative     #-}
+
+macro
+    plus-to-times : Term → Term → TC ⊤
+    plus-to-times (def (quote _+_) (a ∷ b ∷ [])) hole = unify hole (def (quote _*_) (a ∷ b ∷ []))
+    plus-to-times v hole = unify hole v
+
+open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym )
+
+thm : (a b : ℕ) → plus-to-times (a + b) ≡ a * b
+thm a b = refl
+
+postulate magic : Type → Term
+
+macro
+  by-magic : Term → TC ⊤
+  by-magic hole =
+    bindTC (inferType hole) λ goal →
+    unify hole (magic goal)
+
+open import Relation.Nullary
+
+-- thm1 : {P NP : Set} → ¬ P ≡ NP
+-- thm1 = ? by-magic
+
+--unquoteDecl x₁ .. x ₙ = m
+--unquoteDef  x₁ .. x ₙ = m
+
+-- Defining: id-name {A} x = x
+defId : (id-name : Name) → TC ⊤
+defId id-name = do
+  defineFun id-name
+    [ clause
+      ( arg (arg-info hidden relevant) (var "A")
+      ∷ arg (arg-info visible relevant) (var "x")
+      ∷ [] )
+      (var 0 [])
+    ]
+
+id : {A : Set} (x : A) → A
+unquoteDef id = defId id
+
+open import Level  renaming  ( suc to succ ; zero  to Zero )
+
+mkId : (id-name : Name) → TC ⊤
+mkId id-name = 
+  do
+    ty ← quoteTC ({A : Set} (x : A) → A)
+    declareDef (arg (arg-info visible relevant) id-name) ty
+    defId id-name   
+  where
+        _>>=_  : {a : Level} {B A : Set a} (m : TC B) (f : (x : B) → TC A) → TC A
+        _>>=_  = bindTC
+        _>>_  : {a : Level} {B A : Set a} (m : TC B) (m' : TC A) → TC A
+        _>>_  x y = bindTC x ( λ _ → y )
+
+
+mkId' : (id-name : Name) → TC ⊤
+mkId' id-name = 
+    bindTC
+        ( quoteTC ({A : Set} (x : A) → A) )
+        ( λ ty → bindTC (declareDef (arg (arg-info visible relevant) id-name) ty )
+        ( λ _ → defId id-name) )
+
+lemma1 : ( x : Name  ) → mkId x ≡ mkId' x
+lemma1 x = refl
+
+unquoteDecl id′ = mkId id′
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tactics.agda	Fri Mar 15 17:35:46 2019 +0900
@@ -0,0 +1,53 @@
+module tactics where
+
+open  import  Ataca.Tactics
+open  import  Relation.Binary.PropositionalEquality
+open ≡-Reasoning
+                                                  
+open import Level
+
+
+postulate a : Set
+postulate b : Set
+postulate c : Set
+
+
+infixr 40 _::_
+data  List {a} (A : Set a) : Set a where
+   [] : List A
+   _::_ : A → List A → List A
+
+
+infixl 30 _++_
+-- _++_ : {a : Level } → {A : Set a} → List A → List A → List A
+_++_ : ∀ {a} {A : Set a} → List A → List A → List A
+[]        ++ ys = ys
+(x :: xs) ++ ys = x :: (xs ++ ys)
+
+
+l1 = a :: []
+l2 = a :: b :: a :: c ::  []
+
+l3 = l1 ++ l2
+
+test1 : {a : Level} → {A : Set a } → List {a} A
+test1 = []
+
+list-id-l : { A : Set } → { x : List A} →  [] ++ x ≡ x
+list-id-l = refl
+
+list-id-r : { A : Set } → ( x : List A ) →  x ++ [] ≡ x
+list-id-r [] =   refl
+list-id-r (x :: xs) =  cong ( _::_ x ) ( list-id-r xs )
+
+
+-- listAssoc : { A : Set } → { a b c : List A} →  ( ( a ++ b ) ++ c ) ≡ ( a ++ ( b ++ c ) )
+-- listAssoc   = eq-reflection
+
+list-assoc : {A : Set } → ( xs ys zs : List A ) →
+     ( ( xs ++ ys ) ++ zs ) ≡ ( xs ++ ( ys ++ zs ) )
+list-assoc  [] ys zs = refl
+list-assoc  (x :: xs)  ys zs = cong  ( _::_ x ) ( list-assoc xs ys zs )
+
+
+