# HG changeset patch # User Shinji KONO # Date 1552638946 -32400 # Node ID 776f851a03a378a51cbc807302bfc2b3578f4a22 reflection and tactics diff -r 000000000000 -r 776f851a03a3 hello.agda --- /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!") + diff -r 000000000000 -r 776f851a03a3 reflection-ex.agda --- /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′ diff -r 000000000000 -r 776f851a03a3 tactics.agda --- /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 ) + + +