summaryrefslogtreecommitdiff
path: root/dev/ocamlweb-doc/ast.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
commite978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch)
tree0de2a907ee93c795978f3c843155bee91c11ed60 /dev/ocamlweb-doc/ast.ml
parent3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff)
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
Diffstat (limited to 'dev/ocamlweb-doc/ast.ml')
-rw-r--r--dev/ocamlweb-doc/ast.ml47
1 files changed, 47 insertions, 0 deletions
diff --git a/dev/ocamlweb-doc/ast.ml b/dev/ocamlweb-doc/ast.ml
new file mode 100644
index 00000000..2153ef47
--- /dev/null
+++ b/dev/ocamlweb-doc/ast.ml
@@ -0,0 +1,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)