summaryrefslogtreecommitdiff
path: root/dev/ocamlweb-doc/ast.ml
blob: 2153ef47c0f834bf482ce350b738b5eb3a1b073e (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

type constr_ast =
  Pair of constr_ast * constr_ast
| Prod of binder list * constr_ast
| Lambda of binder list * constr_ast
| Let of string * constr_ast * constr_ast
| LetCase of binder list * constr_ast * constr_ast
| IfCase of constr_ast * constr_ast * constr_ast
| Eval of red_fun * constr_ast
| Infix of string * constr_ast * constr_ast
| Prefix of string * constr_ast
| Postfix of string * constr_ast
| Appl of constr_ast * constr_arg list
| ApplExpl of string list * constr_ast list
| Scope of string * constr_ast
| Qualid of string list
| Prop | Set | Type
| Int of string
| Hole
| Meta of string
| Fixp of fix_kind *
      (string * binder list * constr_ast * string option * constr_ast) list *
      string
| Match of case_item list * constr_ast option *
           (pattern list * constr_ast) list 

and red_fun = Simpl

and binder = string * constr_ast

and constr_arg = string option * constr_ast

and fix_kind = Fix | CoFix

and case_item = constr_ast * (string option * constr_ast option)

and pattern = 
  PatAs of pattern * string
| PatType of pattern * constr_ast
| PatConstr of string * pattern list
| PatVar of string

let mk_cast c t =
  if t=Hole then c else Infix(":",c,t)

let mk_lambda bl t =
  if bl=[] then t else Lambda(bl,t)