rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

"abstract" ⇒ "postulate"

Browse source 
abstracts still have a body, just not always visible. which i will deal
with Later
This commit is contained in:
rhiannon morris 2023-03-13 19:31:05 +01:00
parent 8e9b0abb34
commit 7f46537cbc
3 changed files with 39 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
lib/Quox/Definition.idr
View file

@ -12,12 +12,18 @@ record AnyTerm q where
constructor T
get : forall d, n. Term q d n
public export
data DefBody q =
Concrete (AnyTerm q)
| Postulate
public export
record Definition' q (isGlobal : Pred q) where
constructor MkDef'
constructor MkDef
qty : q
type : AnyTerm q
term : Maybe $ AnyTerm q
body : DefBody q
{auto 0 qtyGlobal : isGlobal qty}
public export
@ -27,12 +33,12 @@ Definition q = Definition' q IsGlobal
public export %inline
mkDef : IsQty q => (qty : q) -> (0 _ : IsGlobal qty) =>
(type, term : forall d, n. Term q d n) -> Definition q
mkDef qty type term = MkDef' {qty, type = T type, term = Just (T term)}
mkDef qty type term = MkDef {qty, type = T type, body = Concrete (T term)}
public export %inline
mkAbstract : IsQty q => (qty : q) -> (0 _ : IsGlobal qty) =>
mkPostulate : IsQty q => (qty : q) -> (0 _ : IsGlobal qty) =>
(type : forall d, n. Term q d n) -> Definition q
mkAbstract qty type = MkDef' {qty, type = T type, term = Nothing}
mkPostulate qty type = MkDef {qty, type = T type, body = Postulate}
public export %inline
@ -43,9 +49,15 @@ public export %inline
(.type0) : Definition' q _ -> Term q 0 0
g.type0 = g.type.get
public export %inline
(.term) : Definition' q _ -> Maybe (AnyTerm q)
g.term = case g.body of
Concrete t => Just t
Postulate => Nothing
public export %inline
(.term0) : Definition' q _ -> Maybe (Term q 0 0)
g.term0 = map (\t => t.get) g.term
g.term0 = map (\x => x.get) g.term
public export %inline
(.qtyP) : forall q, isGlobal. Definition' q isGlobal -> Subset q isGlobal

16
tests/Tests/Equal.idr
View file

@ -10,14 +10,14 @@ M = ReaderT (Definitions Three) (Either (Error Three))
defGlobals : Definitions Three
defGlobals = fromList
[("A", mkAbstract Zero $ TYPE 0),
("B", mkAbstract Zero $ TYPE 0),
("a", mkAbstract Any $ FT "A"),
("a'", mkAbstract Any $ FT "A"),
("b", mkAbstract Any $ FT "B"),
("f", mkAbstract Any $ Arr One (FT "A") (FT "A")),
[("A", mkPostulate Zero $ TYPE 0),
("B", mkPostulate Zero $ TYPE 0),
("a", mkPostulate Any $ FT "A"),
("a'", mkPostulate Any $ FT "A"),
("b", mkPostulate Any $ FT "B"),
("f", mkPostulate Any $ Arr One (FT "A") (FT "A")),
("id", mkDef Any (Arr One (FT "A") (FT "A")) (["x"] :\\ BVT 0)),
("eq-AB", mkAbstract Zero $ Eq0 (TYPE 0) (FT "A") (FT "B"))]
("eq-AB", mkPostulate Zero $ Eq0 (TYPE 0) (FT "A") (FT "B"))]
parameters (label : String) (act : Lazy (M ()))
{default defGlobals globals : Definitions Three}
@ -176,7 +176,7 @@ tests = "equality & subtyping" :- [
testEq "p : (a ≡ a' : A), q : (a ≡ a' : A) ∥ ⊢ p = q (free)"
{globals =
let def = mkAbstract Zero $ Eq0 (FT "A") (FT "a") (FT "a'") in
let def = mkPostulate Zero $ Eq0 (FT "A") (FT "a") (FT "a'") in
defGlobals `mergeLeft` fromList [("p", def), ("q", def)]} $
equalE empty (F "p") (F "q"),

26
tests/Tests/Typechecker.idr
View file

@ -72,19 +72,19 @@ sndDef =
defGlobals : Definitions Three
defGlobals = fromList
[("A", mkAbstract Zero $ TYPE 0),
("B", mkAbstract Zero $ TYPE 0),
("C", mkAbstract Zero $ TYPE 1),
("D", mkAbstract Zero $ TYPE 1),
("P", mkAbstract Zero $ Arr Any (FT "A") (TYPE 0)),
("a", mkAbstract Any $ FT "A"),
("a'", mkAbstract Any $ FT "A"),
("b", mkAbstract Any $ FT "B"),
("f", mkAbstract Any $ Arr One (FT "A") (FT "A")),
("g", mkAbstract Any $ Arr One (FT "A") (FT "B")),
("f2", mkAbstract Any $ Arr One (FT "A") $ Arr One (FT "A") (FT "B")),
("p", mkAbstract Any $ Pi_ One "x" (FT "A") $ E $ F "P" :@ BVT 0),
("q", mkAbstract Any $ Pi_ One "x" (FT "A") $ E $ F "P" :@ BVT 0),
[("A", mkPostulate Zero $ TYPE 0),
("B", mkPostulate Zero $ TYPE 0),
("C", mkPostulate Zero $ TYPE 1),
("D", mkPostulate Zero $ TYPE 1),
("P", mkPostulate Zero $ Arr Any (FT "A") (TYPE 0)),
("a", mkPostulate Any $ FT "A"),
("a'", mkPostulate Any $ FT "A"),
("b", mkPostulate Any $ FT "B"),
("f", mkPostulate Any $ Arr One (FT "A") (FT "A")),
("g", mkPostulate Any $ Arr One (FT "A") (FT "B")),
("f2", mkPostulate Any $ Arr One (FT "A") $ Arr One (FT "A") (FT "B")),
("p", mkPostulate Any $ Pi_ One "x" (FT "A") $ E $ F "P" :@ BVT 0),
("q", mkPostulate Any $ Pi_ One "x" (FT "A") $ E $ F "P" :@ BVT 0),
("refl", mkDef Any reflTy reflDef),
("fst", mkDef Any fstTy fstDef),
("snd", mkDef Any sndTy sndDef)]