summaryrefslogtreecommitdiff
path: root/isabelle-dump/src/calc.y
blob: 2dd3bd31d65a9c8c30afec95967cb4898a076739 (plain)
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
%start AbbrList

%%

AbbrList -> Result<Vec<Isabelle>, ()>:
   Text { Ok(vec![Isabelle::Text($1?)]) }
   | Abbr { Ok(vec![Isabelle::Symbol($1?)]) }
   | AbbrList Abbr
      {
          let mut $1 = $1?;
          $1.push(Isabelle::Symbol($2?));
          Ok($1)
      }
   | AbbrList Text
     {
          let mut $1 = $1?;
          $1.push(Isabelle::Text($2?));
          Ok($1)
     }
   ;

Abbr -> Result<String, ()>:
      'AOPEN' Name  { Ok($2?) }
    ;

Text -> Result<String, ()>:
  'TEXT'
      {
        let v = $1.map_err(|_| ())?;
        Ok($lexer.span_str(v.span()).to_string())
      }
  | 'AOPEN'
      {
        //let v = $2.map_err(|_| ())?;
        Ok("\\".to_string())
      }
  | 'LT'
      {
        //let v = $2.map_err(|_| ())?;
        Ok("<".to_string()) //format!("<{}", $lexer.span_str(v.span())))
      }
  ;

Name -> Result<String, ()>:
  'NAME'
      {
        let v = $1.map_err(|_| ())?;
        let name = $lexer.span_str(v.span());
        Ok(name[1..name.len()-1].to_string())
      }
  ;
%%

use crate::Isabelle;