blob: 2882423700cf90fd1d2b4c04a8db1ccf5e4c1f93 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
|
// This project type requires the F# PowerPack at http://fsharppowerpack.codeplex.com/releases
// Learn more about F# at http://fsharp.net
// Original project template by Jomo Fisher based on work of Brian McNamara, Don Syme and Matt Valerio
// This posting is provided "AS IS" with no warranties, and confers no rights.
module Main
open System
open System.IO
open Microsoft.FSharp.Text.Lexing
open Ast
open Lexer
open Parser
open Printer
open TypeChecker
open Analyzer
let readAndProcess tracing analyzing (filename: string) =
try
printfn "// Jennisys, Copyright (c) 2011, Microsoft."
// lex
let f = if filename = null then Console.In else new StreamReader(filename) :> TextReader
let lexbuf = LexBuffer<char>.FromTextReader(f)
lexbuf.EndPos <- { pos_bol = 0;
pos_fname=if filename = null then "stdin" else filename;
pos_cnum=0;
pos_lnum=1 }
try
// parse
let sprog = Parser.start Lexer.tokenize lexbuf
// print the given Jennisys program
if tracing then
printfn "---------- Given Jennisys program ----------"
printfn "%s" (Print sprog)
else ()
match TypeCheck sprog with
| None -> () // errors have already been reported
| Some(prog) ->
if analyzing then
// output a Dafny program with the constraints to be solved
Analyze prog
else ()
// that's it
if tracing then printfn "----------" else ()
with
| ex ->
let pos = lexbuf.EndPos
printfn "%s(%d,%d): %s" pos.FileName pos.Line pos.Column ex.Message
with
| ex ->
printfn "Unhandled Exception: %s" ex.Message
let rec start n (args: string []) tracing analyzing filename =
if n < args.Length then
let arg = args.[n]
if arg = "/break" then ignore (System.Diagnostics.Debugger.Launch()) else ()
let filename = if arg.StartsWith "/" then filename else arg
start (n+1) args (tracing || arg = "/trace") (analyzing && arg <> "/noAnalysis") filename
else
readAndProcess tracing analyzing filename
let args = Environment.GetCommandLineArgs()
try
start 1 args false true null
with
| e -> printfn "%s" e.StackTrace
|
