parse_csiho.mly 2.55 KB
Newer Older
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
%{

  type var = string

  type term =
    | Lam of (var * term * term)
    | App of term * term list
    | Var of var
    | Pi of (var * term * term)
    | Arr of (term * term)

  let app t l = match t with
    | App (t', l') -> App (t', List.append l l')
    | t -> if l = [] then t else App (t, l)

  let rec print_term out = function
    | Lam (x, ty, t) ->
       Printf.fprintf out "%s : %a => %a"
                      x
                      print_term_par ty
                      print_term t
    | Pi (x, ty, t) ->
       Printf.fprintf out "%s : %a -> %a"
                      x
                      print_term_par ty
                      print_term t
    | Arr (ty, t) ->
       Printf.fprintf out "%a -> %a"
                      print_term_par ty
                      print_term t
    | App (t, l) ->
       Printf.fprintf out "%a%a"
                      print_term_par t
                      (fun out -> List.iter (Printf.fprintf out " %a" print_term_par)) l
    | Var x -> Printf.fprintf out "%s" x
  and print_term_par out = function
    | Var x -> Printf.fprintf out "%s" x
    | t -> Printf.fprintf out "(%a)" print_term t

  let print_file out (rules, rules', peaks, t1, t2, t3, t4) =
    assert (rules = rules');
    Printf.fprintf out "%s critical peaks\n" peaks;
    if t1 = t2 then
      Printf.fprintf out "%a\n" print_term t1
    else
      Printf.fprintf out "%a\n *<-\n%a\n" print_term t1 print_term t2;
    Printf.fprintf out " ==\n";
    if t3 = t4 then
      Printf.fprintf out "%a\n" print_term t3
    else
      Printf.fprintf out "%a\n ->*\n%a\n" print_term t3 print_term t4

%}

%token NO PROBLEM PROOF PROCESSOR CRITPEAKS NONJOIN QED BETA
%token APP LAM PI LPAREN RPAREN ARR BACKSLASH DOT LARRS ARRS PEAK UNKNOWNMETA NOVAR
%token <string> VAR CONST META NUM

%start <unit> file

%%

file: NO PROBLEM BETA rules PROOF PROCESSOR BETA rules CRITPEAKS NUM peaks PROCESSOR NONJOIN term LARRS term PEAK term ARRS term QED
         { Printf.printf "%a" print_file ($4, $8, $10, $14, $16, $18, $20) }

rules: { [] }
     | rule rules
         { $1 :: $2 }

rule: term ARR term { ($1, 3) }

term: APP term term { app $2 [$3] }
    | LPAREN term RPAREN { $2 }
    | LAM term LPAREN BACKSLASH VAR DOT term RPAREN { Lam ($5, $2, $7) }
    | VAR { Var $1 }
    | CONST { Var $1 }
    | META { Var $1 }
    | UNKNOWNMETA { Var "_" }
    | NUM { Var "_" }
    | PI term LPAREN BACKSLASH VAR DOT term RPAREN { Pi ($5, $2, $7) }
    | PI term LPAREN BACKSLASH NOVAR DOT term RPAREN { Arr ($2, $7) }

peaks: { [] }
     | peak peaks { $1 :: $2 }

peak: term PEAK term { ($1, $3) }

%%