exemple complet de parser

changement de syntaxe des scope:   expr % id
ex:  (10 + 5 * 4)%N  ou  4%N


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3451 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 393 insertions, 73 deletions

diff --git a/doc/Makefile b/doc/Makefile
index 47a102fd9..9d8ea2ee3 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -1,7 +1,38 @@
 
 # Makefile for doc/
 
-all: newsyntax.dvi minicoq.dvi
+all:: newparse 
+#newsyntax.dvi minicoq.dvi
+
+
+OBJS=lex.cmo ast.cmo parse.cmo syntax.cmo
+
+newparse: $(OBJS) syntax.mli lex.ml syntax.ml
+	ocamlc -o newparse $(OBJS)
+
+.ml.cmo:
+	ocamlc -c $<
+
+.mli.cmi:
+	ocamlc -c $<
+
+.mll.ml:
+	ocamllex $<
+
+.mly.ml:
+	ocamlyacc -v $<
+
+.mly.mli:
+	ocamlyacc -v $<
+
+clean::
+	rm -f *.cm* *.output syntax.ml syntax.mli lex.ml newparse
+
+parse.cmo: ast.cmo
+syntax.cmi: parse.cmo
+syntax.cmo: lex.cmo parse.cmo syntax.cmi
+lex.cmo: syntax.cmi
+ast.cmo: ast.ml
 
 newsyntax.dvi: newsyntax.tex
 	latex $<
@@ -26,7 +57,7 @@ depend:: kernel.dep.ps library.dep.ps pretyping.dep.ps parsing.dep.ps \
 clean::
 	rm -f *~ *.log *.aux
 
-.SUFFIXES: .tex .dvi .ps
+.SUFFIXES: .tex .dvi .ps .cmo .cmi .mli .ml .mll .mly
 
 .tex.dvi:
 	latex $< && latex $<
diff --git a/doc/ast.ml b/doc/ast.ml
new file mode 100644
index 000000000..2153ef47c
--- /dev/null
+++ b/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)
diff --git a/doc/lex.mll b/doc/lex.mll
new file mode 100644
index 000000000..617163e7e
--- /dev/null
+++ b/doc/lex.mll
@@ -0,0 +1,81 @@
+
+{
+ open Lexing
+ open Syntax
+
+ let chan_out = ref stdout
+
+ let comment_depth = ref 0
+ let print s = output_string !chan_out s
+ 
+ exception Fin_fichier
+
+}
+
+let space = [' ' '\t' '\n']
+let letter = ['a'-'z' 'A'-'Z']
+let digit = ['0'-'9']
+
+let identifier = letter (letter | digit | ['_' '\''])*
+let number = digit+
+let oper = ['-' '+' '/' '*' '|' '>' '<' '=' '%' '#' '$' ':' '\\' '?'
+            '.' '!' '@' ]+
+
+rule token = parse
+  | "let" {LET}
+  | "in" {IN}
+  | "match" {MATCH}
+  | "with" {WITH}
+  | "end" {END}
+  | "and" {AND}
+  | "fun" {FUN}
+  | "if" {IF}
+  | "then" {THEN}
+  | "else" {ELSE}
+  | "eval" {EVAL}
+  | "for" {FOR}
+  | "Prop" {PROP}
+  | "Set" {SET}
+  | "Type" {TYPE}
+  | "fix" {FIX}
+  | "cofix" {COFIX}
+  | "struct" {STRUCT}
+  | "as" {AS}
+
+  | "Simpl" {SIMPL}
+
+  | "_" {WILDCARD}
+  | "(" {LPAR}
+  | ")" {RPAR}
+  | "{" {LBRACE}
+  | "}" {RBRACE}
+  | "!" {BANG}
+  | "@" {AT}
+  | ":" {COLON}
+  | ":=" {COLONEQ}
+  | "." {DOT}
+  | "," {COMMA}
+  | "->" {OPER "->"}
+  | "=>" {RARROW}
+  | "|" {BAR}
+  | "%" {PERCENT}
+
+  | '?' { META(ident lexbuf)}
+  | number { INT(Lexing.lexeme lexbuf) }
+  | oper { OPER(Lexing.lexeme lexbuf) }
+  | identifier { IDENT (Lexing.lexeme lexbuf) }
+  | "(*" (*"*)"*)       { comment_depth := 1;
+                          comment lexbuf;
+		          token lexbuf }
+  | space+     { token lexbuf}
+  | eof        { EOF }
+
+and ident = parse
+  | identifier { Lexing.lexeme lexbuf }
+
+and comment = parse
+  | "(*" (*"*)"*)  { incr comment_depth; comment lexbuf }
+  | (*"(*"*) "*)"
+      { decr comment_depth; if !comment_depth > 0 then comment lexbuf }
+  | eof   { raise Fin_fichier } 
+  | _     { comment lexbuf }
diff --git a/doc/parse.ml b/doc/parse.ml
new file mode 100644
index 000000000..e537b1f2f
--- /dev/null
+++ b/doc/parse.ml
@@ -0,0 +1,183 @@
+
+open Ast
+
+type assoc = L | R | N
+
+let level = function
+  | "--" -> 70,L
+  | "=" -> 70,N
+  | "+" -> 60,L
+  | "++" -> 60,R
+  | "+++" -> 60,R
+  | "-" -> 60,L
+  | "*" -> 50,L
+  | "/" -> 50,L
+  | "**" -> 40,R
+  | ":" -> (100,R)
+  | "->" -> (90,R)
+  | s -> failwith ("unknowm operator '"^s^"'")
+
+let fixity = function
+  | "--" -> [L]
+  | "=" -> [N]
+  | ("+"|"-"|"*"|"/") -> [L;N]
+  | "++" -> [R]
+  | _ -> [L;N;R]
+
+let ground_oper = function
+    ("-"|"+") -> true
+  | _ -> false
+
+let is_prefix op = List.mem L (fixity op)
+let is_infix op = List.mem N (fixity op)
+let is_postfix op = List.mem R (fixity op)
+
+let mk_inf op t1 t2 =
+  if not (is_infix op) then failwith (op^" not infix");
+  Infix(op,t1,t2)
+
+let mk_post op t =
+  if not (is_postfix op) then failwith (op^" not postfix");
+  Postfix(op,t)
+
+
+(* Pb avec ground_oper: pas de diff entre -1 et -(1) *)
+let mk_pre op t =
+  if not (is_prefix op) then failwith (op^" not prefix");
+  if ground_oper op then
+    match t with
+    | Int i -> Int (op^i)
+    | _     -> Prefix(op,t)
+  else Prefix(op,t)
+
+(* teste si on peut reduire op suivi d'un op de niveau (n,a)
+   si la reponse est false, c'est que l'op (n,a) doit se reduire
+   avant *)
+let red_left_op (nl,al) (nr,ar) =
+  if nl < nr then true
+  else
+    if nl = nr then
+      match al,ar with
+        | (L|N), L -> true
+        | R, (R|N) -> false
+        | R, L ->  failwith "conflit d'assoc: ambigu"
+        | (L|N), (R|N) -> failwith "conflit d'assoc: blocage"
+    else false
+
+
+type level = int * assoc
+type stack =
+  | PrefixOper of string list
+  | Term of constr_ast * stack
+  | Oper of string list * string * constr_ast * stack
+
+let rec str_ast = function
+  | Infix(op,t1,t2) -> str_ast t1 ^ " " ^ op ^ " " ^ str_ast t2
+  | Postfix(op,t) -> str_ast t ^ " " ^ op
+  | Prefix(op,t) -> op ^ " " ^ str_ast t
+  | _ -> "_"
+
+let rec str_stack = function
+  | PrefixOper ops -> String.concat " " (List.rev ops)
+  | Term (t,s) -> str_stack s ^ " (" ^ str_ast t ^ ")"
+  | Oper(ops,lop,t,s) ->
+      str_stack (Term(t,s)) ^ " " ^ lop ^ " " ^
+      String.concat " " (List.rev ops) 
+
+let pps s = prerr_endline (str_stack s)
+let err s stk = failwith (s^": "^str_stack stk)
+
+
+let empty = PrefixOper []
+
+let check_fixity_term stk =
+  match stk with
+      Term _ -> err "2 termes successifs" stk
+    | _ -> ()
+
+let shift_term t stk =
+  check_fixity_term stk;
+  Term(t,stk)
+
+let shift_oper op stk =
+  match stk with
+    | Oper(ops,lop,t,s) -> Oper(op::ops,lop,t,s)
+    | Term(t,s) -> Oper([],op,t,s)
+    | PrefixOper ops -> PrefixOper (op::ops)
+
+let is_reducible lv stk =
+  match stk with
+    | Oper([],iop,_,_)  -> red_left_op (level iop) lv
+    | Oper(op::_,_,_,_) -> red_left_op (level op) lv
+    | PrefixOper(op::_) -> red_left_op (level op) lv
+    | _                 -> false
+
+let reduce_head (t,stk) =
+  match stk with
+    | Oper([],iop,t1,s) ->
+        (Infix(iop,t1,t), s)
+    | Oper(op::ops,lop,t',s) ->
+        (mk_pre op t, Oper(ops,lop,t',s))
+    | PrefixOper(op::ops) ->
+        (Prefix(op,t), PrefixOper ops)
+    | _ -> assert false
+
+let rec reduce_level lv (t,s) =
+  if is_reducible lv s then reduce_level lv (reduce_head (t, s))
+  else (t, s)
+
+let reduce_post op (t,s) =
+  let (t',s') = reduce_level (level op) (t,s) in
+  (mk_post op t', s')
+
+let reduce_posts stk =
+  match stk with
+      Oper(ops,iop,t,s) ->
+        let pts1 = reduce_post iop (t,s) in
+        List.fold_right reduce_post ops pts1
+    | Term(t,s) -> (t,s)
+    | PrefixOper _ -> failwith "reduce_posts"
+
+
+let shift_infix op stk =
+  let (t,s) = reduce_level (level op) (reduce_posts stk) in
+  Oper([],op,t,s)
+
+let is_better_infix op stk =
+  match stk with
+    | Oper(ops,iop,t,s) ->
+        is_postfix iop &&
+        List.for_all is_postfix ops &&
+        (not (is_prefix op) || red_left_op (level iop) (level op))
+    | Term _ -> false
+    | _ -> assert false
+
+let parse_oper op stk =
+  match stk with
+    | PrefixOper _ ->
+        if is_prefix op then shift_oper op stk else failwith "prefix_oper"
+    | Oper _ ->
+        if is_infix op then
+          if is_better_infix op stk then shift_infix op stk
+          else shift_oper op stk
+        else if is_prefix op then shift_oper op stk
+        else if is_postfix op then
+          let (t,s) = reduce_post op (reduce_posts stk) in
+          Term(t,s)
+        else assert false
+    | Term(t,s) ->
+        if is_infix op then shift_infix op stk
+        else if is_postfix op then
+          let (t2,s2) = reduce_post op (t,s) in Term(t2,s2)
+        else failwith "infix/postfix"
+
+let parse_term = shift_term
+
+let rec close_stack stk =
+  match stk with
+      Term(t,PrefixOper []) -> t
+    | PrefixOper _ -> failwith "expression sans atomes"
+    | _ ->
+        let (t,s) = reduce_head (reduce_posts stk) in
+        close_stack (Term(t,s))
+
diff --git a/doc/syntax.mly b/doc/syntax.mly
index 2785e7ca0..bfc7d5ccf 100644
--- a/doc/syntax.mly
+++ b/doc/syntax.mly
@@ -1,61 +1,31 @@
 %{
-
-type constr_ast =
-  Pair of constr_ast * constr_ast
-| Prod of binder list * constr_ast
-| Lambda of binder list * constr_ast
-| Cast of constr_ast * 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 constr_ast * 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 redfun = 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
+open Ast
+open Parse
 %}
 
-%token <string> META
-%token <string> INT
-%token <string> IDENT
-%token <string> INFIX
-%token <string> PREFIX
-%token <string> POSTFIX
-%token LPAR RPAR BAR COMMA COLON BANG FUN DOT RARROW LET COLONEQ IN IF THEN ELSE EVAL AT FOR BQUOTE PROP SET TYPE WILDCARD FIX COFIX MATCH WITH ENDKW AND LBRACE RBRACE STRUCT AS SIMPL
+%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 <constr_ast> 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 }
@@ -63,20 +33,19 @@ paren_constr:
 
 constr:
           binder_constr  { $1 }
-        | oper_constr    { $1}
+        | oper_constr    { close_stack $1 }
 ;
 
 binder_constr:
-          BANG ne_binders DOT constr                  { Prod($2, $4) }
-        | FUN ne_binders type RARROW constr
-            { Lambda($2,Cast($5,$3)) }
-        | LET IDENT binders type COLONEQ constr IN constr
-            { Let($2,$6,Lambda($3,Cast($8,4))) }
+          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) }
+        | IF constr THEN constr ELSE constr       { IfCase($2,$4,$6) }
+        | fix_constr                              { $1 }
+        | EVAL rfun IN constr                     { Eval($2,$4) }
 ;
 
 comma_binders:
@@ -94,11 +63,20 @@ rfun:
 ;
 
 
+/* 2 Conflits shift/reduce */
 oper_constr:
-          oper_constr INFIX oper_constr  { Infix($2,$1,$3) }
-        | PREFIX oper_constr             { Prefix($1,$2) }
-        | oper_constr POSTFIX            { Postfix($2,$1) }
-        | appl_constr                    { $1 }
+          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:
@@ -121,7 +99,7 @@ simple_constr:
           atomic_constr                           { $1 }
         | match_constr                            { $1 }
         | LPAR paren_constr RPAR                  { $2 }
-        | BQUOTE IDENT COLON paren_constr BQUOTE  { Scope($2,$4) }
+        | simple_constr PERCENT IDENT { Scope($3,$1) }
 ;
 
 simple_constrs:
@@ -144,17 +122,18 @@ global:
         | 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  { ($1, $2::$3, $5) }
+        | fix_kw fix_decl fix_decls FOR IDENT  { Fixp($1, $2::$3, $5) }
 ;
 
 fix_kw: FIX {Fix} | COFIX {CoFix}
 ;
 
 fix_decl:
-          IDENT binders type annot COLONEQ constr  { ($1,$2,$3,$4,$6) }
+          IDENT binders type_cstr annot COLONEQ constr  { ($1,$2,$3,$4,$6) }
 ;
 
 fix_decls:
@@ -168,7 +147,7 @@ annot:
 ;
 
 match_constr:
-          MATCH case_items case_type WITH branches ENDKW  { Match($2,$3,$5) }
+          MATCH case_items case_type WITH branches END  { Match($2,$3,$5) }
 ;
 
 case_items:
@@ -227,7 +206,7 @@ simple_patterns:
 
 binder:
           IDENT                 { ($1,Hole) }
-        | LPAR IDENT type RPAR  { ($2,$3) }
+        | LPAR IDENT type_cstr RPAR  { ($2,$3) }
 ;
 
 binders:
@@ -235,12 +214,11 @@ binders:
         |             { [] }
 
 ne_binders:
-          binder             { $1 }
+          binder             { [$1] }
         | binder ne_binders  { $1::$2 }
 ;
 
-type:
+type_cstr:
           COLON constr  { $2 }
         |               { Hole }
 ;
-