module Hutton where open import Vec open import AlgOrn data HOp : Set where PUSH : HOp SEQ : HOp ADD : HOp HCode : Desc (Nat * Nat) HCode = sg HOp args where args : HOp -> Desc (Nat * Nat) args PUSH = sg Nat \ _ -> sg Nat \ i -> say (i , su i) args SEQ = sg Nat \ k -> sg Nat \ l -> sg Nat \ m -> ask (k , l) * ask (l , m) * say (k , m) args ADD = sg Nat \ i -> say (su (su i) , su i) HSem : Nat * Nat -> Set HSem ij = Vec (fst ij) Nat -> Vec (snd ij) Nat HAlg : [ HCode ] HSem :-> HSem HAlg (PUSH , n , i , refl) ns = n :: ns HAlg (SEQ , k , l , m , f , g , refl) ns = g (f ns) HAlg (ADD , i , refl) < step , x , .(su i) , < step , y , .i , stk , refl > , refl > = (y + x) :: stk HAlg (ADD , i , refl) < step , _ , ._ , < base , () > , refl > HAlg (ADD , i , refl) < base , () > HCodeSem : Desc (Sg (Nat * Nat) HSem) HCodeSem = ornD (algOrn HCode HAlg) data HCon : Set where val : HCon add : HCon HExp : Desc One HExp = sg HCon args where args : HCon -> Desc One args val = sg Nat \ _ -> say _ args add = ask _ * ask _ * say _ hEval : Data HExp _ -> Nat hEval = fold evAlg where evAlg : [ HExp ] (k Nat) :-> k Nat evAlg ( val , n , refl ) = n evAlg ( add , a , b , refl ) = a + b hCompileSem : (e : Data HExp _) -> {i : Nat} -> Data HCodeSem ((i , su i) , _::_ (hEval e)) hCompileSem = induction HExp (\e -> {i : Nat} -> Data HCodeSem ((i , su i) , _::_ (hEval e))) help where help : (d : [ HExp ] (Data HExp) _) -> All HExp (\ e -> {i : Nat} -> Data HCodeSem ((i , su i) , _::_ (hEval e))) d -> {i : Nat} -> Data HCodeSem ((i , su i) , _::_ (hEval < d >)) help ( val , n , refl ) H = < PUSH , _ , _ , refl > help ( add , a , b , refl ) ( ca , cb , _ ) = < SEQ , _ , _ , _ , _ , ca , _ , < SEQ , _ , _ , _ , _ , cb , _ , < ADD , _ , refl > , refl > , refl > hCompile : Data HExp _ -> {i : Nat} -> Data HCode (i , su i) hCompile e = fold (ornAlg (algOrn HCode HAlg)) (hCompileSem e) hTheorem : (e : Data HExp _){i : Nat} -> fold HAlg (hCompile e {i}) == _::_ (hEval e) hTheorem e = AOOAThm HCode HAlg (hCompileSem e)