diff options
| -rw-r--r-- | .depend | 13 | ||||
| -rw-r--r-- | Makefile | 3 | ||||
| -rw-r--r-- | parsing/.cvsignore | 1 | ||||
| -rw-r--r-- | parsing/g_minicoq.g4 | 53 | ||||
| -rw-r--r-- | parsing/g_minicoq.mli | 13 | ||||
| -rw-r--r-- | parsing/lexer.mll | 11 | ||||
| -rw-r--r-- | toplevel/minicoq.ml | 17 |
7 files changed, 106 insertions, 5 deletions
@@ -31,7 +31,8 @@ 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 +parsing/g_minicoq.cmi: /usr/local/lib/camlp4/grammar.cmi kernel/names.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 \ @@ -148,5 +149,11 @@ 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.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 +toplevel/minicoq.cmo: parsing/g_minicoq.cmi kernel/generic.cmi \ + /usr/local/lib/camlp4/grammar.cmi kernel/names.cmi \ + /usr/local/lib/camlp4/stdpp.cmi +toplevel/minicoq.cmx: parsing/g_minicoq.cmi kernel/generic.cmx \ + /usr/local/lib/camlp4/grammar.cmi kernel/names.cmx \ + /usr/local/lib/camlp4/stdpp.cmi +parsing/g_minicoq.cmo: parsing/g_minicoq.cmi +parsing/g_minicoq.cmx: parsing/g_minicoq.cmi @@ -140,5 +140,8 @@ cleanconfig:: depend: $(OCAMLDEP) $(DEPFLAGS) */*.mli */*.ml > .depend + for f in */*.g4; do \ + $(CAMLP4EXTEND) $(DEPFLAGS) pr_depend.cmo -impl $$f >> .depend; \ + done include .depend diff --git a/parsing/.cvsignore b/parsing/.cvsignore index c1104f3ab..87551eece 100644 --- a/parsing/.cvsignore +++ b/parsing/.cvsignore @@ -1 +1,2 @@ lexer.ml +*.ppo diff --git a/parsing/g_minicoq.g4 b/parsing/g_minicoq.g4 index 8ee3d5425..4f8e14571 100644 --- a/parsing/g_minicoq.g4 +++ b/parsing/g_minicoq.g4 @@ -2,6 +2,7 @@ (* $Id$ *) open Names +open Univ open Generic open Term @@ -12,12 +13,62 @@ let lexer = { Token.tparse = Lexer.tparse; Token.text = Lexer.token_text } +type command = + | Definition of identifier * constr option * constr + | Parameter of identifier * constr + | Variable of identifier * constr + | Inductive of + (identifier * constr) list * + (identifier * constr * (identifier * constr) list) list + | Check of constr + let gram = Grammar.create lexer let term = Grammar.Entry.create gram "term" let command = Grammar.Entry.create gram "command" +let new_univ = + let uc = ref 0 in + let univ = id_of_string "univ" in + fun () -> incr uc; { u_sp = make_path [] univ CCI; u_num = !uc } + +let path_of_string s = make_path [] (id_of_string s) CCI + EXTEND - term: [ [ id = IDENT -> VAR (id_of_string id) ] ]; + term: [ + [ id = IDENT -> + VAR (id_of_string id) + | "Set" -> + DOP0 (Sort (Prop Pos)) + | "Prop" -> + DOP0 (Sort (Prop Null)) + | "Type" -> + DOP0 (Sort (Type (new_univ()))) + | IDENT "Const"; id = IDENT -> + DOPN (Const (path_of_string id), [||]) + | IDENT "Ind"; id = IDENT; n = INT -> + let n = int_of_string n in + DOPN (MutInd (path_of_string id, n), [||]) + | IDENT "Construct"; id = IDENT; n = INT; i = INT -> + let n = int_of_string n and i = int_of_string i in + DOPN (MutConstruct ((path_of_string id, n), i), [||]) + | "["; id = IDENT; ":"; t = term; "]"; c = term -> + DOP2 (Lambda, t, DLAM (Name (id_of_string id), c)) + | "("; id = IDENT; ":"; t = term; ")"; c = term -> + DOP2 (Prod, t, DLAM (Name (id_of_string id), c)) + ] ]; + command: [ + [ "Definition"; id = IDENT; ":="; c = term; "." -> + Definition (id_of_string id, None, c) + | "Definition"; id = IDENT; ":"; t = term; ":="; c = term; "." -> + Definition (id_of_string id, Some t, c) + | "Parameter"; id = IDENT; ":"; t = term; "." -> + Parameter (id_of_string id, t) + | "Variable"; id = IDENT; ":"; t = term; "." -> + Variable (id_of_string id, t) + | IDENT "Check"; c = term; "." -> + Check c + | EOI -> raise End_of_file + ] ]; END diff --git a/parsing/g_minicoq.mli b/parsing/g_minicoq.mli index 0b2ceb1e8..ef47c4f89 100644 --- a/parsing/g_minicoq.mli +++ b/parsing/g_minicoq.mli @@ -1,4 +1,17 @@ +open Names open Term val term : constr Grammar.Entry.e + +type command = + | Definition of identifier * constr option * constr + | Parameter of identifier * constr + | Variable of identifier * constr + | Inductive of + (identifier * constr) list * + (identifier * constr * (identifier * constr) list) list + | Check of constr + +val command : command Grammar.Entry.e + diff --git a/parsing/lexer.mll b/parsing/lexer.mll index c0cbca3ba..08ec04091 100644 --- a/parsing/lexer.mll +++ b/parsing/lexer.mll @@ -64,6 +64,10 @@ let identchar = ['A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9'] let symbolchar = ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] +let decimal_literal = ['0'-'9']+ +let hex_literal = '0' ['x' 'X'] ['0'-'9' 'A'-'F' 'a'-'f']+ +let oct_literal = '0' ['o' 'O'] ['0'-'7']+ +let bin_literal = '0' ['b' 'B'] ['0'-'1']+ rule token = parse | blank+ @@ -71,6 +75,11 @@ rule token = parse | firstchar identchar* { let s = Lexing.lexeme lexbuf in if is_keyword s then ("",s) else ("IDENT",s) } + | decimal_literal | hex_literal | oct_literal | bin_literal + { ("INT", Lexing.lexeme lexbuf) } + | ":=" { ("COLONEQUAL","") } + | ":" { ("COLON","") } + | "." { ("DOT","") } | symbolchar+ { ("SPECIAL", Lexing.lexeme lexbuf) } | '`' [^'`']* '`' @@ -86,6 +95,8 @@ rule token = parse comment_start_pos := Lexing.lexeme_start lexbuf; comment lexbuf; token lexbuf } + | eof + { ("EOI","") } and comment = parse "(*" diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml index e4b1496a3..79be85fad 100644 --- a/toplevel/minicoq.ml +++ b/toplevel/minicoq.ml @@ -23,4 +23,19 @@ let rec globalize bv = function | Rel _ | DOP0 _ as c -> c let main () = - failwith "todo" + let cs = Stream.of_channel stdin in + while true do + try + let c = Grammar.Entry.parse G_minicoq.command cs in + Printf.printf "ok\n"; flush stdout + with + | End_of_file | Stdpp.Exc_located (_, End_of_file) -> + exit 0 + | Stdpp.Exc_located (_,e) -> + Printf.printf "error: %s\n" (Printexc.to_string e); flush stdout + | exn -> + Printf.printf "error: %s\n" (Printexc.to_string exn); flush stdout + done + +let _ = Printexc.catch main () + |