pawer 0.2.0

A rust library to doc Calculus of Construction
Documentation 
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
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124

WHITESPACE = _{ " " | NEWLINE | "\t" | "\r" }
COMMENT    = _{
    "/*" ~ (!"*/" ~ ANY)* ~ "*/"
  | "//" ~ (!NEWLINE ~ ANY)* ~ NEWLINE
}

tokens = @{ ("as" | "in" | "return" | "with" | "fun" | "|" | "=>" | "=" | ":=" | "end") ~ !name } 

lowercase_string = @{ ASCII_ALPHA_LOWER ~ ASCII_ALPHA* }
uppercase_string = @{ ASCII_ALPHA_UPPER ~ ASCII_ALPHA* }
number           = @{ (ASCII_NONZERO_DIGIT ~ ASCII_DIGIT*) | "0" }
name             = @{ (ASCII_ALPHANUMERIC | "_")+ }
variable         = !{ !tokens ~ name }
not_dot          = @{ (!"." ~ ANY)* }

typed_vars = !{ variable+ ~ ":" ~ lambda }
typed_vars_list = !{ ("(" ~ typed_vars ~ ")")+ }

commands_top = _{ SOI ~ command* ~ EOI }
commands = _{ command* }
command_top = _{ SOI ~ command ~ EOI }
command = _{ ( goal | qed | goal | theorem | define | cancel | check | reduce | inductive | fixpoint | tactic | print_proof | print | search | clean ) ~ "."+ }
  qed   = !{ "Qed" }
  goal  = !{ "Goal" ~ lambda }
  define  = !{ define_token ~ variable ~ define_vars ~ ":=" ~ lambda }
    define_token  = _{ "Define" | "Definition" | "Def" }
    define_vars = !{ typed_vars_list? }
  theorem  = !{ thm_token ~ variable ~ ":" ~ lambda }
    thm_token = _{ "Theorem" | "Lemma" | "Fact" | "Remark" | "Corollary" | "Proposition" | "Property" }
  check  = !{ "Check" ~ lambda }
  reduce  = !{ reduce_token ~ lambda }
    reduce_token = _{"Reduce" | "Compute"}
  cancel  = !{ "Cancel" | "Abort" }
  inductive = !{ "Inductive" ~ variable ~ i_params ~ ":" ~ lambda ~ ":=" ~ ("|"? ~ i_case)? ~ ("|" ~ i_case)* }
    i_params = !{ typed_vars_list? }
    i_case = !{ variable ~ ":" ~ lambda }
  fixpoint = !{ "Fixpoint" ~ variable ~ typed_vars_list ~ "{" ~ "struct" ~ variable ~ "}" ~ ":" ~ lambda ~ ":=" ~ lambda }
  print    = !{ "Print" ~ lambda }
  search   = !{ "Search" ~ not_dot }
  print_proof = !{ "PrintProof" }
  clean = !{ "Clean" }


tactic = !{ exact | intro | intros | apply | cut | unfold | simpl | induction }
  exact = !{ "exact" ~ lambda }
  intros = !{ "intros" ~ variable* }
  intro = !{ "intro " ~ variable? }
  apply = !{ "apply " ~ lambda }
  cut = !{ "cut " ~ lambda }
  unfold = !{ "unfold " ~ variable }
  simpl = !{ "simpl" }
  induction = !{ "induction" ~ variable }


lambda = _{ top_expr }
lambda_top = _{ SOI ~ top_expr ~ EOI }

forall     = !{ ("forall" | "∀") ~ many_vars ~ "," ~ top_expr }
  many_vars = _{ typed_vars | typed_vars_list } // we must have parenthesis if we have several inputs
func       = !{ "fun" ~ many_vars ~ "=>" ~ top_expr }
fix         = !{ "fix" ~ variable ~ typed_vars_list ~ "{" ~ "struct" ~ variable ~ "}" ~ ":" ~ let_case ~ ":=" ~ top_expr }
match_      = !{ "match" ~ let_case ~ "as" ~ variable ~ "in" ~ pattern ~ "return" ~ let_case ~ "with" ~ m_cases ~ "end" }
  m_cases   = !{ ("|" ~ match_in)* }
  match_in  = !{ pattern ~ "=>" ~ let_case }
  pattern   = !{ (p_wild | p_in | variable)* }
    p_wild  = !{ "_" }
    p_in    = _{ "(" ~ pattern ~")" }
implies    = !{ or_case ~ "->" ~ implies_case }
app        = !{ !tokens ~ litteral ~ (!tokens ~ litteral)+ }
let        = !{ "let" ~ "(" ~ variable ~ ":" ~ top_expr ~ ")" ~ "=" ~ let_case ~ "in" ~ let_case }

// prio of 10
top_expr = _{
  | forall | func
  | implies_case
}

// prio of 20
implies_case = _{
  implies | or_case
}

// prio of 30
or_case = _{
  and_case
}

// prio of 40
and_case = _{
  not_case
}

// prio of 50
not_case = _{
  func_case
}

// prio of 60
func_case = _{
  fix | func | match_ | let_case
}

// prio of 70
let_case = _{
  let | app_case
}

// prio of 90
app_case = _{
  app | litteral
}

// prio of 100
litteral = _{
    "(" ~ top_expr ~ ")"
  | lprop
  | lset
  | ltype
  | variable 
}

lprop     = !{ "Prop" }
lset      = !{ "Set" }
ltype     = !{ "Type" ~ "(" ~ number ~ ")" }