diff options
Diffstat (limited to 'dev/ocamlweb-doc/syntax.mly')
| -rw-r--r-- | dev/ocamlweb-doc/syntax.mly | 224 |
1 files changed, 0 insertions, 224 deletions
diff --git a/dev/ocamlweb-doc/syntax.mly b/dev/ocamlweb-doc/syntax.mly deleted file mode 100644 index bfc7d5cc..00000000 --- a/dev/ocamlweb-doc/syntax.mly +++ /dev/null @@ -1,224 +0,0 @@ -%{ -open Ast -open Parse -%} - -%token <string> META INT IDENT -%token <string> OPER -%token LPAR RPAR BAR COMMA COLON BANG FUN DOT RARROW LET COLONEQ IN IF -%token THEN ELSE EVAL AT FOR PROP SET TYPE WILDCARD FIX -%token COFIX MATCH WITH END AND LBRACE RBRACE STRUCT AS SIMPL PERCENT -%token EOF - -%start main -%type <Ast.constr_ast> main - -%start constr -%type <Ast.constr_ast> constr - -%start simple_constr -%type <Ast.constr_ast> simple_constr - -%% - -main: - constr EOF { $1 } -; - - -paren_constr: - constr COMMA paren_constr { Pair($1,$3) } - | constr { $1 } -; - -constr: - binder_constr { $1 } - | oper_constr { close_stack $1 } -; - -binder_constr: - BANG ne_binders DOT constr { Prod($2, $4) } - | FUN ne_binders type_cstr RARROW constr { Lambda($2,mk_cast $5 $3) } - | LET IDENT binders type_cstr COLONEQ constr IN constr - { Let($2,mk_lambda $3 (mk_cast $6 $4),$8) } - | LET LPAR comma_binders RPAR COLONEQ constr IN constr - { LetCase($3,$6,$8) } - | IF constr THEN constr ELSE constr { IfCase($2,$4,$6) } - | fix_constr { $1 } - | EVAL rfun IN constr { Eval($2,$4) } -; - -comma_binders: - ne_comma_binders { $1 } - | { [] } -; - -ne_comma_binders: - binder COMMA ne_comma_binders { $1 :: $3 } - | binder { [$1] } -; - -rfun: - SIMPL { Simpl } -; - - -/* 2 Conflits shift/reduce */ -oper_constr: - oper_constr oper appl_constr - { parse_term $3 (parse_oper $2 $1) } - | oper_constr oper binder_constr - { parse_term $3 (parse_oper $2 $1) } - | oper_constr oper { parse_oper $2 $1 } - | { empty } - | appl_constr { parse_term $1 empty } -; - -oper: - OPER {$1} - | COLON {":"} -; - -appl_constr: - simple_constr ne_appl_args { Appl($1,$2) } - | AT global simple_constrs { ApplExpl($2,$3) } - | simple_constr { $1 } -; - -appl_arg: - AT INT COLONEQ simple_constr { (Some $2,$4) } - | simple_constr { (None,$1) } -; - -ne_appl_args: - appl_arg { [$1] } - | appl_arg ne_appl_args { $1::$2 } -; - -simple_constr: - atomic_constr { $1 } - | match_constr { $1 } - | LPAR paren_constr RPAR { $2 } - | simple_constr PERCENT IDENT { Scope($3,$1) } -; - -simple_constrs: - simple_constr simple_constrs { $1::$2 } - | { [] } -; - -atomic_constr: - global { Qualid $1 } - | PROP { Prop } - | SET { Set } - | TYPE { Type } - | INT { Int $1 } - | WILDCARD { Hole } - | META { Meta $1 } -; - -global: - IDENT DOT global { $1 :: $3 } - | IDENT { [$1] } -; - -/* Conflit normal */ -fix_constr: - fix_kw fix_decl - { let (id,_,_,_,_ as fx) = $2 in Fixp($1,[fx],id) } - | fix_kw fix_decl fix_decls FOR IDENT { Fixp($1, $2::$3, $5) } -; - -fix_kw: FIX {Fix} | COFIX {CoFix} -; - -fix_decl: - IDENT binders type_cstr annot COLONEQ constr { ($1,$2,$3,$4,$6) } -; - -fix_decls: - AND fix_decl fix_decls { $2::$3 } - | AND fix_decl { [$2] } -; - -annot: - LBRACE STRUCT IDENT RBRACE { Some $3 } - | { None } -; - -match_constr: - MATCH case_items case_type WITH branches END { Match($2,$3,$5) } -; - -case_items: - case_item { [$1] } - | case_item COMMA case_items { $1::$3 } -; - -case_item: - constr pred_pattern { ($1,$2) } -; - -case_type: - RARROW constr { Some $2 } - | { None } -; - -pred_pattern: - AS IDENT COLON constr { (Some $2, Some $4) } - | AS IDENT { (Some $2, None) } - | COLON constr { (None, Some $2) } - | { (None,None) } -; - -branches: - BAR branch_list { $2 } - | branch_list { $1 } - | { [] } -; - -branch_list: - patterns RARROW constr { [$1, $3] } - | patterns RARROW constr BAR branch_list { ($1,$3)::$5 } -; - -patterns: - pattern { [$1] } - | pattern COMMA patterns { $1::$3 } -; - -pattern: - pattern AS IDENT { PatAs($1,$3) } - | pattern COLON constr { PatType($1,$3) } - | IDENT simple_patterns { PatConstr($1,$2) } - | simple_pattern { $1 } -; - -simple_pattern: - IDENT { PatVar $1 } - | LPAR pattern RPAR { $2 } -; - -simple_patterns: - simple_pattern { [$1] } - | simple_pattern simple_patterns { $1::$2 } -; - -binder: - IDENT { ($1,Hole) } - | LPAR IDENT type_cstr RPAR { ($2,$3) } -; - -binders: - ne_binders { $1 } - | { [] } - -ne_binders: - binder { [$1] } - | binder ne_binders { $1::$2 } -; - -type_cstr: - COLON constr { $2 } - | { Hole } -; |