mise en place grammaire minicoq

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

6 files changed, 125 insertions, 9 deletions

diff --git a/.depend b/.depend
index d4a67cce11..67e83aa8f2 100644
--- a/.depend
+++ b/.depend
@@ -31,6 +31,7 @@ lib/pp.cmi: lib/pp_control.cmi
 lib/util.cmi: lib/pp.cmi 
 library/libobject.cmi: kernel/names.cmi 
 library/summary.cmi: kernel/names.cmi 
+parsing/g_minicoq.cmi: /usr/local/lib/camlp4/grammar.cmi kernel/term.cmi 
 config/coq_config.cmo: config/coq_config.cmi 
 config/coq_config.cmx: config/coq_config.cmi 
 kernel/abstraction.cmo: kernel/generic.cmi kernel/names.cmi kernel/sosub.cmi \
@@ -145,7 +146,7 @@ library/summary.cmo: lib/dyn.cmi kernel/names.cmi lib/pp.cmi lib/util.cmi \
     library/summary.cmi 
 library/summary.cmx: lib/dyn.cmx kernel/names.cmx lib/pp.cmx lib/util.cmx \
     library/summary.cmi 
-parsing/lexer.cmo: lib/util.cmi 
-parsing/lexer.cmx: lib/util.cmx 
+parsing/lexer.cmo: lib/util.cmi parsing/lexer.cmi 
+parsing/lexer.cmx: lib/util.cmx parsing/lexer.cmi 
 toplevel/minicoq.cmo: kernel/generic.cmi kernel/names.cmi 
 toplevel/minicoq.cmx: kernel/generic.cmx kernel/names.cmx 
diff --git a/Makefile b/Makefile
index 9b2060b3a0..1f254b0eaf 100644
--- a/Makefile
+++ b/Makefile
@@ -16,12 +16,18 @@ OPTFLAGS=$(INCLUDES) $(CAMLTIMEPROF)
 OCAMLDEP=ocamldep
 DEPFLAGS=$(INCLUDES)
 
-INCLUDES=-I config -I lib -I kernel -I library
+INCLUDES=-I config -I lib -I kernel -I library -I parsing -I $(CAMLP4LIB)
+
+CAMLP4EXTEND=camlp4o pa_extend.cmo
+OCAMLC_P4O=$(OCAMLC) -pp camlp4o $(BYTEFLAGS)
+OCAMLOPT_P4O=$(OCAMLOPT) -pp camlp4o $(OPTFLAGS)
 
 # Objects files 
 
 CLIBS=unix.cma
 
+CAMLP4OBJS=gramlib.cma
+
 CONFIG=config/coq_config.cmo
 
 LIB=lib/pp_control.cmo lib/pp.cmo lib/util.cmo lib/hashcons.cmo \
@@ -43,15 +49,21 @@ OBJS=$(CONFIG) $(LIB) $(KERNEL) $(LIBRARY) $(PARSING)
 
 # Targets
 
-world: $(OBJS)
-	#$(OCAMLC) -o coqtop.byte $(OBJS)
+world: minicoq
+
+# coqtop
+
+coqtop: $(OBJS)
 	ocamlmktop -o coqtop -custom $(CLIBS) $(OBJS) $(OSDEPLIBS)
 
-MINICOQOBJS=$(CONFIG) $(LIB) $(KERNEL) $(PARSING) toplevel/minicoq.cmo
+# minicoq
+
+MINICOQOBJS=$(CONFIG) $(LIB) $(KERNEL) $(PARSING) \
+	    parsing/g_minicoq.cmo toplevel/minicoq.cmo
 
 minicoq: $(OBJS) $(MINICOQOBJS)
-	$(OCAMLC) -o minicoq -custom $(CLIBS) $(OBJS) $(MINICOQOBJS) \
-	  $(OSDEPLIBS)
+	$(OCAMLC) $(INCLUDES) -o minicoq -custom $(CLIBS) $(CAMLP4OBJS) \
+	  $(OBJS) $(MINICOQOBJS) $(OSDEPLIBS)
 
 # Literate programming (with ocamlweb)
 
@@ -77,9 +89,14 @@ tags:
 	      "--regex=/val[ \t]+\([^ \t]+\)/\1/" \
 	      "--regex=/module[ \t]+\([^ \t]+\)/\1/"
 
+# Special rules
+
+parsing/lexer.cmo: parsing/lexer.ml
+	$(OCAMLC_P4O) -c $<
+
 # Default rules
 
-.SUFFIXES: .ml .mli .cmo .cmi .cmx .mll
+.SUFFIXES: .ml .mli .cmo .cmi .cmx .mll .g4
 
 .ml.cmo:
 	$(OCAMLC) $(BYTEFLAGS) -c $<
@@ -93,18 +110,28 @@ tags:
 .mll.ml:
 	ocamllex $<
 
+.g4.cmo:
+	$(OCAMLC) $(BYTEFLAGS) -I $(CAMLP4LIB) -pp "$(CAMLP4EXTEND) -impl" -c -impl $<
+
+.g4.cmx:
+	$(OCAMLOPT) $(OPTFLAGS) -I $(CAMLP4LIB) -pp "$(CAMLP4EXTEND) -impl" -c -impl $<
+
 # Cleaning
 
 archclean::
 	rm -f config/*.cmx config/*.[so]
 	rm -f lib/*.cmx lib/*.[so]
 	rm -f kernel/*.cmx kernel/*.[so]
+	rm -f library/*.cmx library/*.[so]
+	rm -f parsing/*.cmx parsing/*.[so]
 
 cleanall:: archclean
 	rm -f *~
 	rm -f config/*.cm[io] config/*~
 	rm -f lib/*.cm[io] lib/*~
 	rm -f kernel/*.cm[io] kernel/*~
+	rm -f library/*.cm[io] library/*~
+	rm -f parsing/*.cm[io] parsing/*~
 
 cleanconfig::
 	rm -f config/Makefile config/coq_config.ml
diff --git a/parsing/g_minicoq.g4 b/parsing/g_minicoq.g4
new file mode 100644
index 0000000000..8ee3d54256
--- /dev/null
+++ b/parsing/g_minicoq.g4
@@ -0,0 +1,23 @@
+
+(* $Id$ *)
+
+open Names
+open Generic
+open Term
+
+let lexer = {
+  Token.func = Lexer.func;
+  Token.using = (fun _ -> ());
+  Token.removing = (fun _ -> ());
+  Token.tparse = Lexer.tparse;
+  Token.text = Lexer.token_text }
+  
+let gram = Grammar.create lexer
+
+let term = Grammar.Entry.create gram "term"
+let command = Grammar.Entry.create gram "command"
+
+EXTEND
+  term: [ [ id = IDENT -> VAR (id_of_string id) ] ];
+END
+
diff --git a/parsing/g_minicoq.mli b/parsing/g_minicoq.mli
new file mode 100644
index 0000000000..0b2ceb1e80
--- /dev/null
+++ b/parsing/g_minicoq.mli
@@ -0,0 +1,4 @@
+
+open Term
+
+val term : constr Grammar.Entry.e
diff --git a/parsing/lexer.mli b/parsing/lexer.mli
new file mode 100644
index 0000000000..670acaa254
--- /dev/null
+++ b/parsing/lexer.mli
@@ -0,0 +1,9 @@
+
+(* $Id$ *)
+
+val func : char Stream.t -> (string * string) Stream.t * (int -> int * int)
+
+val tparse : string * string -> (string * string) Stream.t -> string
+
+val token_text : string * string -> string
+
diff --git a/parsing/lexer.mll b/parsing/lexer.mll
index bdd8d80160..c0cbca3ba1 100644
--- a/parsing/lexer.mll
+++ b/parsing/lexer.mll
@@ -131,3 +131,55 @@ and string = parse
       { Buffer.add_char string_buffer (Lexing.lexeme_char lexbuf 0);
         string lexbuf }
 
+{
+
+let create_loc_table () = ref (Array.create 1024 None)
+
+let find_loc t i = 
+  if i < 0 || i >= Array.length !t then invalid_arg "find_loc";
+  match Array.unsafe_get !t i with 
+    | None -> invalid_arg "find_loc" 
+    | Some l -> l
+
+let add_loc t i l =
+  while i >= Array.length !t do
+    let new_t = Array.create (2 * Array.length !t) None in
+    Array.blit !t 0 new_t 0 (Array.length !t);
+    t := new_t
+  done;
+  !t.(i) <- Some l
+  
+let func cs =
+  let loct = create_loc_table () in
+  let lexbuf = 
+    Lexing.from_function 
+      (fun s _ -> match cs with parser 
+	 | [< 'c >] -> String.unsafe_set s 0 c; 1
+	 | [< >] -> 0)
+  in
+  let next_token i = 
+    let tok = token lexbuf in
+    let loc = (Lexing.lexeme_start lexbuf, Lexing.lexeme_end lexbuf) in
+    add_loc loct i loc; Some tok
+  in
+  let ts = Stream.from next_token in
+  (ts, find_loc loct)
+	 
+let token_text = function
+  | ("", t) -> "'" ^ t ^ "'"
+  | ("IDENT", "") -> "identifier"
+  | ("IDENT", t) -> "'" ^ t ^ "'"
+  | ("INT", "") -> "integer"
+  | ("INT", s) -> "'" ^ s ^ "'"
+  | ("STRING", "") -> "string"
+  | ("EOI", "") -> "end of input"
+  | (con, "") -> con
+  | (con, prm) -> con ^ " \"" ^ prm ^ "\""
+
+let tparse (p_con, p_prm) =
+  if p_prm = "" then
+    parser [< '(con, prm) when con = p_con >] -> prm
+  else
+    parser [< '(con, prm) when con = p_con && prm = p_prm >] -> prm
+
+}