BARReL/POGReader/Schema.lean at master · VTrelat/BARReL · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
import Std.Data.DHashMap
import Std.Data.HashMap
import B.Syntax

namespace B.POG.Schema
  open B.Syntax

  structure Set : Type _ where
    name : String
    values : Array String
  deriving Repr

  inductive DefineType : Type _
    | ctx | seext | inv | ass
    | lprp | inprp | inext | cst | sets | mchcst
    | aprp | abs | imlprp | imprp | imext
    deriving BEq, Hashable, Repr, ReflBEq, LawfulBEq

  inductive Define : DefineType → Type _
    | ctx : Array Set → Array Term → Define .ctx
    | seext : Array Term → Define .seext
    | inv : Array Term → Define .inv
    | ass : Array Term → Define .ass
    | lprp : Array Set → Array Term → Define .lprp
    | inprp : Array Set → Array Term → Define .inprp
    | inext : Array Term → Define .inext
    | cst : Array Term → Define .cst
    | sets : Array Set → Define .sets
    | mchcst : Array Term → Define .mchcst
    | aprp : Array Set → Array Term → Define .aprp
    | abs : Array Term → Define .abs
    | imlprp : Array Set → Array Term → Define .imlprp
    | imprp : Array Set → Array Term → Define .imprp
    | imext : Array Term → Define .imext
  deriving Repr

  instance {k} : Inhabited (Define k) := ⟨match k with
      | .ctx => .ctx #[] #[]
      | .seext => .seext #[]
      | .inv => .inv #[]
      | .ass => .ass #[]
      | .lprp => .lprp #[] #[]
      | .inprp => .inprp #[] #[]
      | .inext => .inext #[]
      | .cst => .cst #[]
      | .sets => .sets #[]
      | .mchcst => .mchcst #[]
      | .aprp => .aprp #[] #[]
      | .abs => .abs #[]
      | .imlprp => .imlprp #[] #[]
      | .imprp => .imprp #[] #[]
      | .imext => .imext #[]
    ⟩

  structure SimpleGoal : Type _ where
    name : String
    refHyps : Array Nat
    goal : Term
  deriving Repr

  structure ProofObligation : Type _ where
    name : String
    uses : Array DefineType
    hypotheses : Array Term
    localHyps : Std.HashMap Nat Term
    simpleGoals : Array SimpleGoal
  deriving Repr

  instance : EmptyCollection ProofObligation where
    emptyCollection := ⟨"", ∅, ∅, ∅, ∅⟩

  structure ProofObligations : Type _ where
    defines : Std.DHashMap DefineType Define
    obligations : Array ProofObligation
    vars : Array (String × Syntax.Typ)
    -- typeInfos : Std.HashMap Nat Typ
  deriving Repr
end B.POG.Schema