Large diffs are not rendered by default.

BIN +13.1 KB (100%) MAlonzo/Code/Qaggycal.o
Binary file not shown.
Binary file not shown.

Large diffs are not rendered by default.

Binary file not shown.
BIN +0 Bytes (100%) MAlonzo/Code/QaggycalZ45Zmain.hi
Binary file not shown.
@@ -30,10 +30,10 @@ name12 = "aggycal-main.parsem.pderiv.insert-front-id"
d12 v0 v1 v2 v3 = coe MAlonzo.Code.Qparse.du164 v2 v3
name14 = "aggycal-main.parsem.pderiv.parse"
d14
= coe MAlonzo.Code.Qparse.du190 MAlonzo.Code.QaggycalZ45Ztypes.d580
= coe MAlonzo.Code.Qparse.du190 MAlonzo.Code.QaggycalZ45Ztypes.d610
name16 = "aggycal-main.parsem.pderiv.parse-filter"
d16
= coe MAlonzo.Code.Qparse.du204 MAlonzo.Code.QaggycalZ45Ztypes.d580
= coe MAlonzo.Code.Qparse.du204 MAlonzo.Code.QaggycalZ45Ztypes.d610
name18 = "aggycal-main.parsem.pderiv.re-to-run"
d18 v0 v1 v2 v3 = coe MAlonzo.Code.Qparse.du140 v2 v3
name20 = "aggycal-main.parsem.pderiv.rewrite-main"
@@ -42,7 +42,7 @@ name22 = "aggycal-main.parsem.pderiv.rewriteRun"
d22 v0 v1 v2 v3 = coe MAlonzo.Code.Qparse.du604 v0 v3
name26 = "aggycal-main.parsem.pderiv.runRtn"
d26
= coe MAlonzo.Code.Qparse.du484 MAlonzo.Code.QaggycalZ45Ztypes.d580
= coe MAlonzo.Code.Qparse.du484 MAlonzo.Code.QaggycalZ45Ztypes.d610
name36 = "aggycal-main.parsem.pnoderiv.RE"
d36 a0 a1 = ()
name40 = "aggycal-main.parsem.pnoderiv.insert-back-id"
@@ -51,10 +51,10 @@ name42 = "aggycal-main.parsem.pnoderiv.insert-front-id"
d42 v0 v1 v2 v3 = coe MAlonzo.Code.Qparse.du662 v2 v3
name44 = "aggycal-main.parsem.pnoderiv.parse"
d44
= coe MAlonzo.Code.Qparse.du688 MAlonzo.Code.QaggycalZ45Ztypes.d580
= coe MAlonzo.Code.Qparse.du688 MAlonzo.Code.QaggycalZ45Ztypes.d610
name46 = "aggycal-main.parsem.pnoderiv.parse-filter"
d46
= coe MAlonzo.Code.Qparse.du702 MAlonzo.Code.QaggycalZ45Ztypes.d580
= coe MAlonzo.Code.Qparse.du702 MAlonzo.Code.QaggycalZ45Ztypes.d610
name48 = "aggycal-main.parsem.pnoderiv.re-to-run"
d48 v0 v1 v2 v3 = coe MAlonzo.Code.Qparse.du644 v2 v3
name50 = "aggycal-main.parsem.pnoderiv.rewrite-main"
@@ -63,19 +63,19 @@ name52 = "aggycal-main.parsem.pnoderiv.rewriteRun"
d52 v0 v1 v2 = coe MAlonzo.Code.Qparse.du1096 v0 v2
name56 = "aggycal-main.parsem.pnoderiv.runRtn"
d56
= coe MAlonzo.Code.Qparse.du982 MAlonzo.Code.QaggycalZ45Ztypes.d580
= coe MAlonzo.Code.Qparse.du982 MAlonzo.Code.QaggycalZ45Ztypes.d610
name82 = "aggycal-main._.rewriteRun"
d82 = coe MAlonzo.Code.Qparse.du1096 MAlonzo.Code.Qaggycal.d740
d82 = coe MAlonzo.Code.Qparse.du1096 MAlonzo.Code.Qaggycal.d758
name86 = "aggycal-main._.runRtn"
d86
= coe
MAlonzo.Code.Qparse.du982 MAlonzo.Code.QaggycalZ45Ztypes.d580
erased MAlonzo.Code.Qaggycal.d154
MAlonzo.Code.Qparse.du982 MAlonzo.Code.QaggycalZ45Ztypes.d610
erased MAlonzo.Code.Qaggycal.d156
name154 = "aggycal-main._.noderiv.Run"
d154 = erased
name156 = "aggycal-main._.noderiv.Run-to-string"
d156
= coe MAlonzo.Code.Qrun.d134 MAlonzo.Code.QaggycalZ45Ztypes.d580
= coe MAlonzo.Code.Qrun.d134 MAlonzo.Code.QaggycalZ45Ztypes.d610
name182 = "aggycal-main.process-strt"
d182 v0 = du182
du182 = coe Data.Text.pack ""
@@ -91,7 +91,7 @@ d186 v0
-> case coe v2 of
MAlonzo.Code.Qrun.C112 v4
-> case coe v4 of
MAlonzo.Code.QaggycalZ45Ztypes.C114 v5
MAlonzo.Code.QaggycalZ45Ztypes.C122 v5
-> case coe v3 of
MAlonzo.Code.Qlist.C12 -> coe du182
_ -> coe v1
@@ -107,7 +107,7 @@ d192 v0 v1
(coe
MAlonzo.Code.Qio.d14
(coe
MAlonzo.Code.Qrun.d134 MAlonzo.Code.QaggycalZ45Ztypes.d580 v1))
MAlonzo.Code.Qrun.d134 MAlonzo.Code.QaggycalZ45Ztypes.d610 v1))
(coe MAlonzo.Code.Qio.d14 (coe Data.Text.pack "\n"))
False -> coe MAlonzo.Code.Qio.d6 erased erased
_ -> coe MAlonzo.RTE.mazUnreachableError
@@ -143,8 +143,8 @@ d214 v0 v1 v2 v3 = du214 v0 v1 v3
du214 v0 v1 v2
= let v3
= coe
MAlonzo.Code.Qparse.du982 MAlonzo.Code.QaggycalZ45Ztypes.d580
erased MAlonzo.Code.Qaggycal.d154
MAlonzo.Code.Qparse.du982 MAlonzo.Code.QaggycalZ45Ztypes.d610
erased MAlonzo.Code.Qaggycal.d156
(coe MAlonzo.Code.Qstring.d14 v2) in
case coe v3 of
MAlonzo.Code.Qsum.C22 v4
@@ -162,7 +162,7 @@ du214 v0 v1 v2
MAlonzo.Code.Qsum.C26 v4
-> let v5 = coe d192 v0 v4 in
let v6
= coe MAlonzo.Code.Qparse.du1096 MAlonzo.Code.Qaggycal.d740 v4 in
= coe MAlonzo.Code.Qparse.du1096 MAlonzo.Code.Qaggycal.d758 v4 in
let v7 = coe d192 v1 v6 in
coe
MAlonzo.Code.Qio.du86 (coe MAlonzo.Code.Qio.du86 v5 v7)
BIN +0 Bytes (100%) MAlonzo/Code/QaggycalZ45Zmain.o
Binary file not shown.
BIN +2.38 KB (100%) MAlonzo/Code/QaggycalZ45Ztypes.hi
Binary file not shown.

Large diffs are not rendered by default.

BIN +7.95 KB (100%) MAlonzo/Code/QaggycalZ45Ztypes.o
Binary file not shown.
BIN -2.45 KB (66%) MAlonzo/Code/QevtZ45Zinfo.hi
Binary file not shown.

Large diffs are not rendered by default.

BIN +24.9 KB (340%) MAlonzo/Code/QevtZ45Zinfo.o
Binary file not shown.
@@ -12,20 +12,24 @@ aTime = hour × minute
datetime : Set
datetime = aDate × aTime

{-aDateRange : Set
aDateRange = aDate × aDate
aTimeRange : Set
aTimeRange = aTime × aTime-}

data addit-evt-info : Set where {- additional parameters -}
allday : 𝔹 addit-evt-info
desc : words addit-evt-info

{- for all-day indication -}
midnight : aTime
midnight = "00" , "00"

aDate-to-string : aDate string
aDate-to-string (y , m , d) = y ^ m ^ d

aTime-to-string : aTime string
aTime-to-string (hour , min) = hour ^ min

datetime-to-string : datetime string
datetime-to-string ((y , m , d) , (hour , min)) =
y ^ m ^ d ^ "T" ^ hour ^ min ^ "00"

addit-evt-info-to-string : addit-evt-info string
addit-evt-info-to-string (allday yes) with yes
... | tt = "All-day: YES" {- need to fix -}
... | ff = "All-day: NO"
addit-evt-info-to-string (desc d) = "DESCRIPTION:" ^ d ^ "\n"

addit-evt-info-list-to-string : 𝕃 addit-evt-info string
BIN +2.76 KB (100%) addit-evt-info.agdai
Binary file not shown.
BIN +37.9 KB (100%) aggycal-create
Binary file not shown.
@@ -20,13 +20,6 @@ extract-addit-evt-info : other → 𝕃 addit-evt-info
extract-addit-evt-info (Description d o) = (desc d) :: (extract-addit-evt-info o)
extract-addit-evt-info OtherNil = []

add-allday : 𝔹 addit-evt-info
add-allday b = allday b

{- for all-day substitute -}
midnight : aTime
midnight = "00" , "00"

adjust-time-with-ampm : time aTime
adjust-time-with-ampm (MilitaryTime hour min) = hour , min
adjust-time-with-ampm (RegTime hour min ampm) with ampm
@@ -48,19 +41,19 @@ extract-datetimes dates times | GlobalDateRange y1 m1 d1 y2 m2 d2 with times
... | AllDayRange = ((y1 , m1 , d1) , midnight) , ((y2 , m2 , d2) , midnight)
... | (TimeRange sTime eTime) = ((y1 , m1 , d1) , adjust-time-with-ampm sTime) , ((y2 , m2 , d2) , adjust-time-with-ampm eTime)

strt-to-evt-info : strt evt-info
strt-to-evt-info (Strt name dates times addit-info) with extract-datetimes dates times
... | sDT , eDT with times
... | AllDayRange = evt name sDT eDT ((add-allday tt) :: (extract-addit-evt-info addit-info))
... | (TimeRange x x₁) = evt name sDT eDT (extract-addit-evt-info addit-info)
event-to-𝕃evt-info : event 𝕃 evt-info
event-to-𝕃evt-info (EventCons name start end other l) with extract-datetimes start end
... | sDT , eDT = (evt name sDT eDT (extract-addit-evt-info other)) :: (event-to-𝕃evt-info l)
event-to-𝕃evt-info (EventFinal name start end other) with extract-datetimes start end
... | sDT , eDT = (evt name sDT eDT (extract-addit-evt-info other)) :: []

process-strt : strt string
process-strt s =
process-strt (Strt e) =
"BEGIN:VCALENDAR\n" ^
"PRODID:aggycal woot\n" ^
"VERSION:2.0\n" ^
"CALSCALE:GREGORIAN\n" ^
evt-info-to-string (strt-to-evt-info s) ^
𝕃evt-info-to-string (event-to-𝕃evt-info e) ^
"END:VCALENDAR\n"

process : Run IO ⊤
BIN +1.09 KB (100%) aggycal-create.agdai
Binary file not shown.
BIN +12.1 KB (100%) aggycal-main
Binary file not shown.
BIN +1.26 KB (100%) aggycal-main.agdai
Binary file not shown.
@@ -50,12 +50,16 @@ mutual
GlobalDate : year month day daterange
GlobalDateRange : year month day year month day daterange

data event : Set where
EventCons : words daterange timerange other event event
EventFinal : words daterange timerange other event

data other : Set where
Description : words other other
OtherNil : other

data strt : Set where
Strt : words daterange timerange other strt
Strt : event strt

data time : Set where
MilitaryTime : hour minute time
@@ -73,6 +77,7 @@ mutual

data ParseTreeT : Set where
parsed-daterange : daterange ParseTreeT
parsed-event : event ParseTreeT
parsed-other : other ParseTreeT
parsed-strt : strt ParseTreeT
parsed-time : time ParseTreeT
@@ -217,12 +222,16 @@ mutual
daterangeToString (GlobalDate x0 x1 x2) = "(GlobalDate" ^ " " ^ (yearToString x0) ^ " " ^ (monthToString x1) ^ " " ^ (dayToString x2) ^ ")"
daterangeToString (GlobalDateRange x0 x1 x2 x3 x4 x5) = "(GlobalDateRange" ^ " " ^ (yearToString x0) ^ " " ^ (monthToString x1) ^ " " ^ (dayToString x2) ^ " " ^ (yearToString x3) ^ " " ^ (monthToString x4) ^ " " ^ (dayToString x5) ^ ")"

eventToString : event string
eventToString (EventCons x0 x1 x2 x3 x4) = "(EventCons" ^ " " ^ (wordsToString x0) ^ " " ^ (daterangeToString x1) ^ " " ^ (timerangeToString x2) ^ " " ^ (otherToString x3) ^ " " ^ (eventToString x4) ^ ")"
eventToString (EventFinal x0 x1 x2 x3) = "(EventFinal" ^ " " ^ (wordsToString x0) ^ " " ^ (daterangeToString x1) ^ " " ^ (timerangeToString x2) ^ " " ^ (otherToString x3) ^ ")"

otherToString : other string
otherToString (Description x0 x1) = "(Description" ^ " " ^ (wordsToString x0) ^ " " ^ (otherToString x1) ^ ")"
otherToString (OtherNil) = "OtherNil" ^ ""

strtToString : strt string
strtToString (Strt x0 x1 x2 x3) = "(Strt" ^ " " ^ (wordsToString x0) ^ " " ^ (daterangeToString x1) ^ " " ^ (timerangeToString x2) ^ " " ^ (otherToString x3) ^ ")"
strtToString (Strt x0) = "(Strt" ^ " " ^ (eventToString x0) ^ ")"

timeToString : time string
timeToString (MilitaryTime x0 x1) = "(MilitaryTime" ^ " " ^ (hourToString x0) ^ " " ^ (minuteToString x1) ^ ")"
@@ -238,6 +247,7 @@ mutual

ParseTreeToString : ParseTreeT string
ParseTreeToString (parsed-daterange t) = daterangeToString t
ParseTreeToString (parsed-event t) = eventToString t
ParseTreeToString (parsed-other t) = otherToString t
ParseTreeToString (parsed-strt t) = strtToString t
ParseTreeToString (parsed-time t) = timeToString t
@@ -332,6 +342,10 @@ mutual
norm-other : (x : other) other
norm-other x = x

{-# TERMINATING #-}
norm-event : (x : event) event
norm-event x = x

{-# TERMINATING #-}
norm-daterange : (x : daterange) daterange
norm-daterange x = x
BIN +3.73 KB (100%) aggycal-types.agdai
Binary file not shown.
@@ -52,6 +52,7 @@ data gratr2-nt : Set where
_month : gratr2-nt
_minute : gratr2-nt
_hour : gratr2-nt
_event : gratr2-nt
_digit-range-28 : gratr2-nt
_digit : gratr2-nt
_day : gratr2-nt
@@ -119,6 +120,7 @@ gratr2-nt-eq _other _other = tt
gratr2-nt-eq _month _month = tt
gratr2-nt-eq _minute _minute = tt
gratr2-nt-eq _hour _hour = tt
gratr2-nt-eq _event _event = tt
gratr2-nt-eq _digit-range-28 _digit-range-28 = tt
gratr2-nt-eq _digit _digit = tt
gratr2-nt-eq _day _day = tt
@@ -178,7 +180,7 @@ aggycal-start _symbol-bar-12 = (just "P26" , nothing , just _symbol-bar-12 , inj
aggycal-start _symbol-bar-11 = (just "P24" , nothing , just _symbol-bar-11 , inj₁ _symbol-bar-10 :: []) :: (just "P23" , nothing , just _symbol-bar-11 , inj₂ '_' :: []) :: []
aggycal-start _symbol-bar-10 = (just "P22" , nothing , just _symbol-bar-10 , inj₁ _symbol-bar-9 :: []) :: (just "P21" , nothing , just _symbol-bar-10 , inj₂ '%' :: []) :: []
aggycal-start _symbol = (just "P51" , nothing , just _symbol , inj₁ _symbol-bar-24 :: []) :: []
aggycal-start _strt = (just "Strt" , nothing , just _strt , inj₁ _ows :: inj₁ _words :: inj₂ '\n' :: inj₁ _daterange :: inj₁ _ws :: inj₁ _timerange :: inj₁ _ows :: inj₁ _other :: inj₁ _ows :: []) :: []
aggycal-start _strt = (just "Strt" , nothing , just _strt , inj₁ _ows :: inj₁ _event :: inj₁ _ows :: []) :: []
aggycal-start _sep-bar-34 = (just "P150" , nothing , just _sep-bar-34 , inj₂ '-' :: []) :: (just "P149" , nothing , just _sep-bar-34 , inj₂ 't' :: inj₂ 'o' :: []) :: []
aggycal-start _sep = (just "P151" , nothing , just _sep , inj₁ _sep-bar-34 :: []) :: []
aggycal-start _posinfo = (just "Posinfo" , nothing , just _posinfo , []) :: []
@@ -190,6 +192,7 @@ aggycal-start _other = (just "OtherNil" , nothing , just _other , []) :: (just "
aggycal-start _month = (just "P131" , nothing , just _month , inj₁ _twodigit :: []) :: []
aggycal-start _minute = (just "P142" , nothing , just _minute , inj₁ _twodigit :: []) :: []
aggycal-start _hour = (just "P141" , nothing , just _hour , inj₁ _twodigit :: []) :: []
aggycal-start _event = (just "EventFinal" , nothing , just _event , inj₁ _words :: inj₂ '\n' :: inj₁ _daterange :: inj₁ _ws :: inj₁ _timerange :: inj₁ _ows :: inj₁ _other :: []) :: (just "EventCons" , nothing , just _event , inj₁ _words :: inj₂ '\n' :: inj₁ _daterange :: inj₁ _ws :: inj₁ _timerange :: inj₁ _ows :: inj₁ _other :: inj₁ _ows :: inj₂ '\n' :: inj₁ _ows :: inj₂ '\n' :: inj₁ _ows :: inj₁ _event :: []) :: []
aggycal-start _digit-range-28 = (just "P128" , nothing , just _digit-range-28 , inj₂ '9' :: []) :: (just "P127" , nothing , just _digit-range-28 , inj₂ '8' :: []) :: (just "P126" , nothing , just _digit-range-28 , inj₂ '7' :: []) :: (just "P125" , nothing , just _digit-range-28 , inj₂ '6' :: []) :: (just "P124" , nothing , just _digit-range-28 , inj₂ '5' :: []) :: (just "P123" , nothing , just _digit-range-28 , inj₂ '4' :: []) :: (just "P122" , nothing , just _digit-range-28 , inj₂ '3' :: []) :: (just "P121" , nothing , just _digit-range-28 , inj₂ '2' :: []) :: (just "P120" , nothing , just _digit-range-28 , inj₂ '1' :: []) :: (just "P119" , nothing , just _digit-range-28 , inj₂ '0' :: []) :: []
aggycal-start _digit = (just "P129" , nothing , just _digit , inj₁ _digit-range-28 :: []) :: []
aggycal-start _day = (just "P132" , nothing , just _day , inj₁ _twodigit :: []) :: []
@@ -231,6 +234,8 @@ len-dec-rewrite {- AllDayRange-} ((Id "AllDayRange") :: _::_(ParseTree parsed-al
len-dec-rewrite {- AmericanDate-} ((Id "AmericanDate") :: (ParseTree (parsed-month x0)) :: (ParseTree parsed-datesep) :: (ParseTree (parsed-day x1)) :: (ParseTree parsed-datesep) :: _::_(ParseTree (parsed-year x2)) rest) = just (ParseTree (parsed-daterange (norm-daterange (AmericanDate x0 x1 x2))) ::' rest , 6)
len-dec-rewrite {- AmericanDateRange-} ((Id "AmericanDateRange") :: (ParseTree (parsed-month x0)) :: (ParseTree parsed-datesep) :: (ParseTree (parsed-day x1)) :: (ParseTree parsed-datesep) :: (ParseTree (parsed-year x2)) :: (ParseTree parsed-ows) :: (ParseTree parsed-sep) :: (ParseTree parsed-ows) :: (ParseTree (parsed-month x3)) :: (ParseTree parsed-datesep) :: (ParseTree (parsed-day x4)) :: (ParseTree parsed-datesep) :: _::_(ParseTree (parsed-year x5)) rest) = just (ParseTree (parsed-daterange (norm-daterange (AmericanDateRange x0 x1 x2 x3 x4 x5))) ::' rest , 14)
len-dec-rewrite {- Description-} ((Id "Description") :: (ParseTree (parsed-words x0)) :: (ParseTree parsed-ws) :: _::_(ParseTree (parsed-other x1)) rest) = just (ParseTree (parsed-other (norm-other (Description x0 x1))) ::' rest , 4)
len-dec-rewrite {- EventCons-} ((Id "EventCons") :: (ParseTree (parsed-words x0)) :: (InputChar '\n') :: (ParseTree (parsed-daterange x1)) :: (ParseTree parsed-ws) :: (ParseTree (parsed-timerange x2)) :: (ParseTree parsed-ows) :: (ParseTree (parsed-other x3)) :: (ParseTree parsed-ows) :: (InputChar '\n') :: (ParseTree parsed-ows) :: (InputChar '\n') :: (ParseTree parsed-ows) :: _::_(ParseTree (parsed-event x4)) rest) = just (ParseTree (parsed-event (norm-event (EventCons x0 x1 x2 x3 x4))) ::' rest , 14)
len-dec-rewrite {- EventFinal-} ((Id "EventFinal") :: (ParseTree (parsed-words x0)) :: (InputChar '\n') :: (ParseTree (parsed-daterange x1)) :: (ParseTree parsed-ws) :: (ParseTree (parsed-timerange x2)) :: (ParseTree parsed-ows) :: _::_(ParseTree (parsed-other x3)) rest) = just (ParseTree (parsed-event (norm-event (EventFinal x0 x1 x2 x3))) ::' rest , 8)
len-dec-rewrite {- GlobalDate-} ((Id "GlobalDate") :: (ParseTree (parsed-year x0)) :: (ParseTree parsed-datesep) :: (ParseTree (parsed-month x1)) :: (ParseTree parsed-datesep) :: _::_(ParseTree (parsed-day x2)) rest) = just (ParseTree (parsed-daterange (norm-daterange (GlobalDate x0 x1 x2))) ::' rest , 6)
len-dec-rewrite {- GlobalDateRange-} ((Id "GlobalDateRange") :: (ParseTree (parsed-year x0)) :: (ParseTree parsed-datesep) :: (ParseTree (parsed-month x1)) :: (ParseTree parsed-datesep) :: (ParseTree (parsed-day x2)) :: (ParseTree parsed-ows) :: (ParseTree parsed-sep) :: (ParseTree parsed-ows) :: (ParseTree (parsed-year x3)) :: (ParseTree parsed-datesep) :: (ParseTree (parsed-month x4)) :: (ParseTree parsed-datesep) :: _::_(ParseTree (parsed-day x5)) rest) = just (ParseTree (parsed-daterange (norm-daterange (GlobalDateRange x0 x1 x2 x3 x4 x5))) ::' rest , 14)
len-dec-rewrite {- MilitaryTime-} ((Id "MilitaryTime") :: (ParseTree (parsed-hour x0)) :: (InputChar ':') :: _::_(ParseTree (parsed-minute x1)) rest) = just (ParseTree (parsed-time (norm-time (MilitaryTime x0 x1))) ::' rest , 4)
@@ -398,7 +403,7 @@ len-dec-rewrite {- P98-} ((Id "P98") :: _::_(InputChar 'k') rest) = just (ParseT
len-dec-rewrite {- P99-} ((Id "P99") :: _::_(InputChar 'l') rest) = just (ParseTree (parsed-words-range-25 (string-append 0 (char-to-string 'l'))) ::' rest , 2)
len-dec-rewrite {- PM-} ((Id "PM") :: _::_(ParseTree parsed-pm) rest) = just (ParseTree (parsed-whichm (norm-whichm PM)) ::' rest , 2)
len-dec-rewrite {- RegTime-} ((Id "RegTime") :: (ParseTree (parsed-hour x0)) :: (InputChar ':') :: (ParseTree (parsed-minute x1)) :: (ParseTree parsed-ows) :: _::_(ParseTree (parsed-whichm x2)) rest) = just (ParseTree (parsed-time (norm-time (RegTime x0 x1 x2))) ::' rest , 6)
len-dec-rewrite {- Strt-} ((Id "Strt") :: (ParseTree parsed-ows) :: (ParseTree (parsed-words x0)) :: (InputChar '\n') :: (ParseTree (parsed-daterange x1)) :: (ParseTree parsed-ws) :: (ParseTree (parsed-timerange x2)) :: (ParseTree parsed-ows) :: (ParseTree (parsed-other x3)) :: _::_(ParseTree parsed-ows) rest) = just (ParseTree (parsed-strt (norm-strt (Strt x0 x1 x2 x3))) ::' rest , 10)
len-dec-rewrite {- Strt-} ((Id "Strt") :: (ParseTree parsed-ows) :: (ParseTree (parsed-event x0)) :: _::_(ParseTree parsed-ows) rest) = just (ParseTree (parsed-strt (norm-strt (Strt x0))) ::' rest , 4)
len-dec-rewrite {- TimeRange-} ((Id "TimeRange") :: (ParseTree (parsed-time x0)) :: (ParseTree parsed-ows) :: (ParseTree parsed-sep) :: (ParseTree parsed-ows) :: _::_(ParseTree (parsed-time x1)) rest) = just (ParseTree (parsed-timerange (norm-timerange (TimeRange x0 x1))) ::' rest , 6)
len-dec-rewrite {- OtherNil-} (_::_(Id "OtherNil") rest) = just (ParseTree (parsed-other (norm-other OtherNil)) ::' rest , 1)
len-dec-rewrite {- P8-} (_::_(Id "P8") rest) = just (ParseTree parsed-ows-star-4 ::' rest , 1)
BIN +6.22 KB (100%) aggycal.agdai
Binary file not shown.
@@ -6,7 +6,10 @@ strt

Syntactic

Strt : strt -> ows words '\n' daterange ws timerange ows other ows .
Strt : strt -> ows event ows .

EventCons : event -> words '\n' daterange ws timerange ows other ows '\n' ows '\n' ows event .
EventFinal : event -> words '\n' daterange ws timerange ows other .

AmericanDate : daterange -> month datesep day datesep year .
GlobalDate : daterange -> year datesep month datesep day .
@@ -1,5 +1,5 @@
Beginning processing of grammar aggycal.
(Time elapsed: 0.001)
(Time elapsed: 0.002)
Converted grammar to AST for grammars.
aggycal

@@ -12,7 +12,9 @@ strt
Syntactic

Posinfo : posinfo -> .
Strt : strt -> ows words '\n' daterange ws timerange ows other ows .
Strt : strt -> ows event ows .
EventCons : event -> words '\n' daterange ws timerange ows other ows '\n' ows '\n' ows event .
EventFinal : event -> words '\n' daterange ws timerange ows other .
AmericanDate : daterange -> month datesep day datesep year .
GlobalDate : daterange -> year datesep month datesep day .
AmericanDateRange : daterange -> month datesep day datesep year ows sep ows month datesep day datesep year .
@@ -203,7 +205,7 @@ Rules


Syntactic non-terminals (defined by syntactic productions):
whichm timerange time strt posinfo other daterange
whichm timerange time strt posinfo other event daterange

Reading non-terminals (defined by lexical ->-productions):
year words-range-25 words-plus-27 words-bar-26 words twodigit symbol-bar-9 symbol-bar-8 symbol-bar-7 symbol-bar-6 symbol-bar-5 symbol-bar-24 symbol-bar-23 symbol-bar-22 symbol-bar-21 symbol-bar-20 symbol-bar-19 symbol-bar-18 symbol-bar-17 symbol-bar-16 symbol-bar-15 symbol-bar-14 symbol-bar-13 symbol-bar-12 symbol-bar-11 symbol-bar-10 symbol month minute hour digit-range-28 digit day
@@ -223,6 +225,8 @@ AllDayRange: #allday -> timerange[AllDayRange]
AmericanDate: month[0] #datesep day[1] #datesep year[2] -> daterange[AmericanDate(x0, x1, x2)]
AmericanDateRange: month[0] #datesep day[1] #datesep year[2] #ows #sep #ows month[3] #datesep day[4] #datesep year[5] -> daterange[AmericanDateRange(x0, x1, x2, x3, x4, x5)]
Description: words[0] #ws other[1] -> other[Description(x0, x1)]
EventCons: words[0] #'\n' daterange[1] #ws timerange[2] #ows other[3] #ows #'\n' #ows #'\n' #ows event[4] -> event[EventCons(x0, x1, x2, x3, x4)]
EventFinal: words[0] #'\n' daterange[1] #ws timerange[2] #ows other[3] -> event[EventFinal(x0, x1, x2, x3)]
GlobalDate: year[0] #datesep month[1] #datesep day[2] -> daterange[GlobalDate(x0, x1, x2)]
GlobalDateRange: year[0] #datesep month[1] #datesep day[2] #ows #sep #ows year[3] #datesep month[4] #datesep day[5] -> daterange[GlobalDateRange(x0, x1, x2, x3, x4, x5)]
MilitaryTime: hour[0] #':' minute[1] -> time[MilitaryTime(x0, x1)]
@@ -393,7 +397,7 @@ P99: 'l' -> words-range-25[string-append(0, char-to-string('l'))]
PM: #pm -> whichm[PM]
Posinfo: -> posinfo[Posinfo]
RegTime: hour[0] #':' minute[1] #ows whichm[2] -> time[RegTime(x0, x1, x2)]
Strt: #ows words[0] #'\n' daterange[1] #ws timerange[2] #ows other[3] #ows -> strt[Strt(x0, x1, x2, x3)]
Strt: #ows event[0] #ows -> strt[Strt(x0)]
TimeRange: time[0] #ows #sep #ows time[1] -> timerange[TimeRange(x0, x1)]
)
)
@@ -414,6 +418,8 @@ AllDayRange: #allday -> timerange[AllDayRange]
AmericanDate: month[0] #datesep day[1] #datesep year[2] -> daterange[AmericanDate(x0, x1, x2)]
AmericanDateRange: month[0] #datesep day[1] #datesep year[2] #ows #sep #ows month[3] #datesep day[4] #datesep year[5] -> daterange[AmericanDateRange(x0, x1, x2, x3, x4, x5)]
Description: words[0] #ws other[1] -> other[Description(x0, x1)]
EventCons: words[0] #'\n' daterange[1] #ws timerange[2] #ows other[3] #ows #'\n' #ows #'\n' #ows event[4] -> event[EventCons(x0, x1, x2, x3, x4)]
EventFinal: words[0] #'\n' daterange[1] #ws timerange[2] #ows other[3] -> event[EventFinal(x0, x1, x2, x3)]
GlobalDate: year[0] #datesep month[1] #datesep day[2] -> daterange[GlobalDate(x0, x1, x2)]
GlobalDateRange: year[0] #datesep month[1] #datesep day[2] #ows #sep #ows year[3] #datesep month[4] #datesep day[5] -> daterange[GlobalDateRange(x0, x1, x2, x3, x4, x5)]
MilitaryTime: hour[0] #':' minute[1] -> time[MilitaryTime(x0, x1)]
@@ -584,7 +590,7 @@ P99: 'l' -> words-range-25[string-append(0, char-to-string('l'))]
PM: #pm -> whichm[PM]
Posinfo: -> posinfo[Posinfo]
RegTime: hour[0] #':' minute[1] #ows whichm[2] -> time[RegTime(x0, x1, x2)]
Strt: #ows words[0] #'\n' daterange[1] #ws timerange[2] #ows other[3] #ows -> strt[Strt(x0, x1, x2, x3)]
Strt: #ows event[0] #ows -> strt[Strt(x0)]
TimeRange: time[0] #ows #sep #ows time[1] -> timerange[TimeRange(x0, x1)]
)
)
@@ -594,6 +600,8 @@ AllDayRange: AllDayRange . allday . x1 -> timerange(AllDayRange) . x1
AmericanDate: AmericanDate . month(x0) . datesep . day(x1) . datesep . year(x2) . x3 -> daterange(AmericanDate(x0, x1, x2)) . x3
AmericanDateRange: AmericanDateRange . month(x0) . datesep . day(x1) . datesep . year(x2) . ows . sep . ows . month(x3) . datesep . day(x4) . datesep . year(x5) . x6 -> daterange(AmericanDateRange(x0, x1, x2, x3, x4, x5)) . x6
Description: Description . words(x0) . ws . other(x1) . x2 -> other(Description(x0, x1)) . x2
EventCons: EventCons . words(x0) . '\n' . daterange(x1) . ws . timerange(x2) . ows . other(x3) . ows . '\n' . ows . '\n' . ows . event(x4) . x5 -> event(EventCons(x0, x1, x2, x3, x4)) . x5
EventFinal: EventFinal . words(x0) . '\n' . daterange(x1) . ws . timerange(x2) . ows . other(x3) . x4 -> event(EventFinal(x0, x1, x2, x3)) . x4
GlobalDate: GlobalDate . year(x0) . datesep . month(x1) . datesep . day(x2) . x3 -> daterange(GlobalDate(x0, x1, x2)) . x3
GlobalDateRange: GlobalDateRange . year(x0) . datesep . month(x1) . datesep . day(x2) . ows . sep . ows . year(x3) . datesep . month(x4) . datesep . day(x5) . x6 -> daterange(GlobalDateRange(x0, x1, x2, x3, x4, x5)) . x6
MilitaryTime: MilitaryTime . hour(x0) . ':' . minute(x1) . x2 -> time(MilitaryTime(x0, x1)) . x2
@@ -764,7 +772,7 @@ P99: P99 . 'l' . x1 -> words-range-25(string-append(0, char-to-string('l'))) . x
PM: PM . pm . x1 -> whichm(PM) . x1
Posinfo: Posinfo . x1 -> posinfo(Posinfo) . x1
RegTime: RegTime . hour(x0) . ':' . minute(x1) . ows . whichm(x2) . x3 -> time(RegTime(x0, x1, x2)) . x3
Strt: Strt . ows . words(x0) . '\n' . daterange(x1) . ws . timerange(x2) . ows . other(x3) . ows . x4 -> strt(Strt(x0, x1, x2, x3)) . x4
Strt: Strt . ows . event(x0) . ows . x1 -> strt(Strt(x0)) . x1
TimeRange: TimeRange . time(x0) . ows . sep . ows . time(x1) . x2 -> timerange(TimeRange(x0, x1)) . x2
)
(No reorganizing critical pairs found.)
@@ -0,0 +1,4 @@
Study for PLC Final Quiz!
2017/05/01 - 2017/05/04
Allday
What is a rewrite???
@@ -10,15 +10,24 @@ data evt-info : Set where
datetime {- end DT -}
𝕃 addit-evt-info {- other not required event info -}
evt-info

{- used for testing purposes -}

evt-info-to-string : evt-info string
evt-info-to-string (evt name ((sYear , sMonth , sDay) , (sHour , sMin)) ((eYear , eMonth , eDay) , (eHour , eMin)) l) =
evt-info-to-string (evt name (sDate , sTime) (eDate , eTime) l) with sTime , eTime
... | midnight , ("00" , "00") = {- repeat variable error if 'midnight' is used twice -}
"BEGIN:VEVENT\n" ^
"SUMMARY:" ^ name ^ "\n" ^
"DTSTART;VALUE=DATE:" ^ (aDate-to-string sDate) ^ "\n" ^
"DTEND;VALUE=DATE:" ^ (aDate-to-string eDate) ^ "\n" ^
(addit-evt-info-list-to-string l) ^
"END:VEVENT\n"
... | _ , _ =
"BEGIN:VEVENT\n" ^
"SUMMARY:" ^ name ^ "\n" ^
"DTSTART:" ^ sYear ^ sMonth ^ sDay ^ "T" ^ sHour ^ sMin ^ "00\n" ^
"DTEND:" ^ eYear ^ eMonth ^ eDay ^ "T" ^ eHour ^ eMin ^ "00\n" ^
"DTSTART:" ^ (aDate-to-string sDate) ^ "T" ^ (aTime-to-string sTime) ^ "00\n" ^
"DTEND:" ^ (aDate-to-string eDate) ^ "T" ^ (aTime-to-string eTime) ^ "00\n" ^
(addit-evt-info-list-to-string l) ^
"END:VEVENT\n"


𝕃evt-info-to-string : 𝕃 evt-info string
𝕃evt-info-to-string [] = ""
𝕃evt-info-to-string (x :: l) = (evt-info-to-string x) ^ (𝕃evt-info-to-string l)
BIN +3.8 KB (100%) evt-info.agdai
Binary file not shown.
@@ -1,4 +1,4 @@
Aye this is a kewl event
04/20/2017
20:02 to 23:45
Aye this is a description.
Programming Language Concepts Presentation
05/02/2017
2:30pm - 2:40pm
Presenting our lit project, aggycal
@@ -3,9 +3,9 @@ PRODID:aggycal woot
VERSION:2.0
CALSCALE:GREGORIAN
BEGIN:VEVENT
SUMMARY:Aye this is a kewl event
DTSTART:20170420T200200
DTEND:20170420T234500
DESCRIPTION:Aye this is a description.
SUMMARY:All-day Event Test
DTSTART;VALUE=DATE:20170502
DTEND;VALUE=DATE:20170504
DESCRIPTION:Woot. Yeet. All things.
END:VEVENT
END:VCALENDAR
@@ -0,0 +1,9 @@
Aye this is a kewl event
04/20/2017
20:02 to 23:45
Description: Aye this is a description.

All-day Event Test
05/02/2017 - 05/04/2017
Allday
Description: Woot. Yeet. All things.