drivers

Makefile.in

@@ -178,7 +178,7 @@ bin/gwhy.byte: $(GCMO)
 WHYVO=lib/coq/Why.vo
 
 bench:: $(BINARY) 
-	cd bench; sh ./bench "../$(BINARY) -I ../lib/prelude/"
+	sh bench/bench "$(BINARY) -I lib/prelude/"
 
 # installation
 ##############

bench/bench.in

@@ -6,50 +6,6 @@ export WHYLIB=../lib
 
 pgm=$1
 option=$2
-coqc="coqc -I ../lib/coq"
-
-pvstc () {
-    context=`dirname $1`
-    theory=`basename $1`
-    cd $context
-    echo "(typecheck "'"'$theory'"'")" > pvstc.el
-    pvs -q -batch -l pvstc.el
-    cd ..
-}
-
-provers () {
-    file=$1
-    base=$2
-    dir=`dirname $1`
-    # running Coq
-    if ! $coqc "$base"_why.v > /dev/null 2>&1; then
-	echo "coq FAILED"
-	$coqc "$base"_why.v
-	exit 1
-    fi
-#      if ! $coqc -I $dir "$base"_valid.v > /dev/null 2>&1; then
-#  	echo "coq validation FAILED"
-#  	$coqc -I $dir "$base"_valid.v
-#  	exit 1
-#      fi
-    echo -n "coq ok... "
-    # running PVS
-    if ! $pgm --pvs $f > /dev/null 2>&1; then
-	echo "pvs generation FAILED"
-	$pgm --pvs $f
-	exit 1
-    fi
-    if test "$option" = "pvs"; then 
-    if ! pvstc "$base"_why > /dev/null 2>&1; then
-	echo "pvs typecheck FAILED"
-	pvs -q -v 3 -batch -l pvstc.el
-	exit 1
-    fi
-    echo "pvs ok"
-    else
-    echo
-    fi
-}
 
 goods () {
     for f in $1/*.why; do
@@ -65,28 +21,6 @@ goods () {
     done
 }
 
-good_ml () {
-    for f in $1/*.why; do
-	echo -n "  "$f"... "
-	base=$1/`basename $f .why`
-	# running Why
-	if ! $pgm --coq-@COQVER@ $f > /dev/null 2>&1; then
-	    echo "why FAILED"
-	    $pgm --coq-@COQVER@ $f
-	    exit 1
-	fi
-	echo -n "why ok... "
-	provers $f $base
-#  		echo -n "coq ok..."
-#  		$pgm --ocaml --ocaml-ext $f > $base.ml 2>/dev/null
-#  		if ocamlc -c $base.ml > /dev/null 2>&1; then
-#  		    echo "ocaml ok"
-#  		else
-#  		    echo "ocaml FAILED"
-#  		fi
-    done
-}
-
 bads () {
     for f in $1/*.why; do
 	echo -n "  "$f"... "
@@ -100,21 +34,39 @@ bads () {
     done
 }
 
+drivers () {
+    for f in $1/*.drv; do
+	echo -n "  "$f"... "
+	base=$1/`basename $f .why`
+	# running Why
+	if ! $pgm $2 $f > /dev/null 2>&1; then
+	    echo "why FAILED"
+	    $pgm $2 $f
+	    exit 1
+	fi
+	echo "why ok... "
+    done
+}
+
 # 1. Syntax
 echo "=== Parsing good files  ==="
-goods typing/bad --parse-only
+goods bench/typing/bad --parse-only
 echo ""
 
 # 2. Typing
 echo "=== Type-checking bad files ==="
-bads typing/bad --type-only
+bads bench/typing/bad --type-only
 echo ""
 
 echo "=== Type-checking good files ==="
-goods typing/good --type-only
+goods bench/typing/good --type-only
 echo ""
 
 echo "=== Type-checking lib/prelude ==="
-goods ../lib/prelude --type-only
+goods lib/prelude --type-only
+echo ""
+
+echo "=== Checking lib/drivers ==="
+drivers lib/drivers
 echo ""
 

configure.in

@@ -483,6 +483,7 @@ AC_SUBST(PDFVIEWER)
 dnl AC_OUTPUT(Makefile)
 AC_OUTPUT(Makefile bench/bench)
 chmod a-w Makefile
+chmod a-w bench/bench
 chmod a+x bench/bench
 
 # Summary

lib/drivers/alt_ergo.drv

+
+(* Why driver for Alt-Ergo *)
+
+"(* this is a prelude for Alt-Ergo*)"
+
+theory prelude.Int
+
+  "(* this is a prelude for Alt-Ergo arithmetic *)"
+
+  syntax zero "0"
+  syntax (_+_) "(%1 + %2)"
+  syntax (_-_) "(%1 - %2)"
+  syntax (_*_) "(%1 * %2)"
+  syntax (_/_) "(%1 / %2)"
+  syntax (-_)  "(-%1)"
+
+  syntax (_<=_) "(%1 <= %2)"
+  syntax (_< _) "(%1 <  %2)"
+  syntax (_>=_) "(%1 >= %2)"
+  syntax (_> _) "(%1 >  %2)"
+
+  remove Mul_comm
+  remove One_neutral
+end
+
+(*
+Local Variables: 
+mode: why
+compile-command: "make -C ../.. bench"
+End: 
+*)

src/main.ml

@@ -101,10 +101,21 @@ let transform env l =
       end	
     | [] -> ()
 
+let handle_file env file =
+  if Filename.check_suffix file ".why" then
+    type_file env file
+  else if Filename.check_suffix file ".drv" then begin
+    ignore (Driver.load file);
+    env
+  end else begin
+    eprintf "%s: don't know what to do with file %s@." Sys.argv.(0) file;
+    exit 1
+  end
+
 let () =
   try
     let env = Typing.create !loadpath in
-    let l = List.fold_left type_file env !files in
+    let l = List.fold_left handle_file env !files in
     transform env l
   with e when not !debug ->
     eprintf "%a@." report e;

src/output/driver.ml

@@ -17,7 +17,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-
 type t
 
 type translation = 
@@ -25,5 +24,19 @@ type translation =
   | Syntax of string
   | Tag of string list
 
+type rules = unit
+    
+let load file =
+  let c = open_in file in
+  let lb = Lexing.from_channel c in
+  Loc.set_file file lb;
+  let f = Driver_lexer.parse_file lb in 
+  close_in c;
+  ()
+
+let create rules ctxt =
+  assert false (*TODO*)
+
 let ident dr id =
   assert false (*TODO*)
+

src/output/driver.mli

@@ -18,6 +18,7 @@
 (**************************************************************************)
 
 open Ident
+open Theory
 
 type t
 
@@ -28,3 +29,9 @@ type translation =
 
 val ident : t -> ident -> translation
 
+type rules
+
+val load : string -> rules
+
+val create : rules -> context -> t
+

src/output/driver_lexer.mll

@@ -18,10 +18,110 @@
 (**************************************************************************)
 
 {
+  open Format
   open Lexing
   open Driver_parser
+
+  type error = 
+    | IllegalCharacter of char
+    | UnterminatedComment
+    | UnterminatedString
+
+  exception Error of error
+
+  let report fmt = function
+    | IllegalCharacter c -> fprintf fmt "illegal character %c" c
+    | UnterminatedComment -> fprintf fmt "unterminated comment"
+    | UnterminatedString -> fprintf fmt "unterminated string"
+
+  let keywords = Hashtbl.create 97
+  let () = 
+    List.iter 
+      (fun (x,y) -> Hashtbl.add keywords x y)
+      [ "theory", THEORY;
+	"end", END;
+	"syntax", SYNTAX;
+	"remove", REMOVE;
+	"tag", TAG;
+      ]
+
+  let newline lexbuf =
+    let pos = lexbuf.lex_curr_p in
+    lexbuf.lex_curr_p <- 
+      { pos with pos_lnum = pos.pos_lnum + 1; pos_bol = pos.pos_cnum }
+
+  let string_buf = Buffer.create 1024
+
+  let char_for_backslash = function
+    | 'n' -> '\n'
+    | 't' -> '\t'
+    | c -> c
+
 }
 
+let space = [' ' '\t' '\r']
+let alpha = ['a'-'z' 'A'-'Z' '_']
+let digit = ['0'-'9']
+let ident = alpha (alpha | digit | '\'')*
+
 rule token = parse
-  | eof { EOF }
+  | '\n'
+      { newline lexbuf; token lexbuf }
+  | space+  
+      { token lexbuf }
+  | "(*"
+      { comment lexbuf; token lexbuf }
+  | '_' 
+      { UNDERSCORE }
+  | ident as id
+      { try Hashtbl.find keywords id with Not_found -> IDENT id }
+  | "<>" | "<" | "<=" | ">" | ">=" 
+  | "="
+  | "+" | "-"
+  | "*" | "/" | "%" as op
+      { OPERATOR op }
+  | "("
+      { LEFTPAR }
+  | ")"
+      { RIGHTPAR }
+  | "."
+      { DOT }
+  | "\""
+      { Buffer.clear string_buf; string lexbuf }
+  | eof 
+      { EOF }
+  | _ as c
+      { raise (Error (IllegalCharacter c)) }
+
+and comment = parse
+  | "*)" 
+      { () }
+  | "(*" 
+      { comment lexbuf; comment lexbuf }
+  | '\n'
+      { newline lexbuf; comment lexbuf }
+  | eof
+      { raise (Error UnterminatedComment) }
+  | _ 
+      { comment lexbuf }
 
+and string = parse
+  | "\""
+      { STRING (Buffer.contents string_buf) }
+  | "\\" (_ as c)
+      { Buffer.add_char string_buf (char_for_backslash c); string lexbuf }
+  | '\n'
+      { newline lexbuf; Buffer.add_char string_buf '\n'; string lexbuf }
+  | eof
+      { raise (Error UnterminatedString) }
+  | _ as c
+      { Buffer.add_char string_buf c; string lexbuf }
+
+{
+  let loc lb = (lexeme_start_p lb, lexeme_end_p lb)
+
+  let with_location f lb =
+    try f lb with e -> raise (Loc.Located (loc lb, e))
+
+  let parse_file = with_location (Driver_parser.file token)
+}

src/output/driver_parser.mly

@@ -21,12 +21,15 @@
   open Driver_ast
   open Parsing
   let loc () = (symbol_start_pos (), symbol_end_pos ())
+  let infix s = "infix " ^ s
+  let prefix s = "prefix " ^ s
 %}
 
 %token <string> IDENT
 %token <string> STRING
+%token <string> OPERATOR
 %token THEORY END SYNTAX REMOVE TAG
-%token STAR DOT EOF
+%token UNDERSCORE LEFTPAR RIGHTPAR STAR DOT EOF
 
 %type <Driver_ast.file> file
 %start file
@@ -59,7 +62,8 @@ list0_trule:
 ;
 
 trule:
-| REMOVE star qualid { Rremove ($2, $3) }
+| REMOVE star qualid   { Rremove ($2, $3) }
+| SYNTAX qualid STRING { Rsyntax ($2, $3) }
 ;
 
 star:
@@ -73,7 +77,13 @@ qualid:
 ;
 
 ident:
-| IDENT  { { id = $1; loc = loc () } }
-| STRING { { id = $1; loc = loc () } }
+| IDENT  
+    { { id = $1; loc = loc () } }
+| STRING 
+    { { id = $1; loc = loc () } }
+| LEFTPAR UNDERSCORE OPERATOR UNDERSCORE RIGHTPAR 
+    { { id = infix $3; loc = loc () } }
+| LEFTPAR OPERATOR UNDERSCORE RIGHTPAR 
+    { { id = prefix $2; loc = loc () } }
 ;