← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to benchmark/Syntacticosmos/Inst.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
benchmark/Syntacticosmos/Inst.agda
1
 
module Inst (Gnd : Set)(U : Set)(El : U -> Set) where
2
 
 
3
 
open import Basics
4
 
open import Pr
5
 
open import Nom
6
 
import Kind
7
 
open Kind Gnd U El
8
 
import Cxt
9
 
open Cxt Kind
10
 
import Loc
11
 
open Loc Kind
12
 
import Term
13
 
open Term Gnd U El
14
 
import Shift
15
 
open Shift Gnd U El
16
 
 
17
 
mutual
18
 
  winst : {G : Cxt}{C : Kind}{L : Loc}{I : Kind}
19
 
          (x : L ! I) -> G [ L bar x / Term C ]- I ->
20
 
          {T : Kind}(t : L [ Term C ]- T) -> [| Good G t |] ->
21
 
          G [ L bar x / Term C ]- T
22
 
  winst x i [ s ]     sg = G[ winsts x i s sg ]
23
 
  winst x i (fn A f)  fg = Gfn A \ a -> winst x i (f a) (fg a)
24
 
  winst x i (\\ b)    bg = G\\ (winst (pop x) (shift popH i) b bg)
25
 
  winst x i (h $ s)   pg = wing x i h (fst pg) (winsts x i s (snd pg)) 
26
 
 
27
 
  winsts : {G : Cxt}{C : Kind}{L : Loc}{Z : Gnd}{I : Kind}
28
 
           (x : L ! I) -> G [ L bar x / Term C ]- I ->
29
 
           {T : Kind}(s : L [ Args C Z ]- T) -> [| Good G s |] ->
30
 
           G [ L bar x / Args C Z ]- T
31
 
  winsts x i (a ^ s)   sg = a G^ winsts x i s sg
32
 
  winsts x i (r & s)   pg = winst x i r (fst pg) G& winsts x i s (snd pg)
33
 
  winsts x i nil       _  = Gnil
34
 
 
35
 
  wing : {G : Cxt}{C : Kind}{L : Loc}{Z : Gnd}{I : Kind}
36
 
         (x : L ! I) -> G [ L bar x / Term C ]- I ->
37
 
         {T : Kind}(h : L [ Head ]- T) -> [| Good G h |] ->
38
 
         G [ L bar x / Args C Z ]- T ->
39
 
         G [ L bar x / Term C ]- Ty Z
40
 
  wing x i (` k)     kg s = (` k -! kg) G$ s
41
 
  wing x i (# y)     _  s with varQV x y
42
 
  wing x i (# .x)    _  s  | vSame = go i s
43
 
  wing x i (# .(x thin y)) _ s | vDiff y = (# y -! _) G$ s
44
 
 
45
 
  go : {G : Cxt}{C : Kind}{L : Loc}{Z : Gnd}{I : Kind} ->
46
 
       G [ L / Term C ]- I -> G [ L / Args C Z ]- I ->
47
 
       G [ L / Term C ]- Ty Z
48
 
  go (fn A f -! fg) ((a ^ s) -! sg) = go (f a -! fg a) (s -! sg)
49
 
  go (\\ b -! bg) ((r & s) -! pg) =
50
 
    go (winst top (r -! fst pg) b bg) (s -! snd pg)
51
 
  go t (nil -! _) = t
52
 
 
53
 
inst : {G : Cxt}{C : Kind}{L : Loc}{I : Kind}
54
 
       (x : L ! I) -> G [ L bar x / Term C ]- I ->
55
 
       {T : Kind} -> G [ L / Term C ]- T -> G [ L bar x / Term C ]- T
56
 
inst x i (t -! tg) = winst x i t tg
57
 
 
58
 
_$$_ : {G : Cxt}{C S T : Kind}{L : Loc} ->
59
 
       G [! C !]- (S |> T) -> G [! C !]- S -> G [! C !]- T
60
 
(\\ b -! bg) $$ sg = inst top sg (b -! bg)
61