liquid-fixpoint-0.1.0.0: external/fixpoint/toplevel.ml
module BS = BNstats
module SM = Ast.Symbol.SMap
module Co = Constants
module C = FixConstraint
module F = Format
module Misc = FixMisc open Misc.Ops
(*
let parse_string str =
let lb = Lexing.from_string str in
ArithParser.aexpr ArithLexer.token lb
let token_list_of_string s =
let lb = Lexing.from_string s in
let rec helper l =
try
let t = ArithLexer.token lb in
if t = ArithParser.EOF then List.rev l else helper (t::l)
with _ -> List.rev l
in helper []
let eval_string env str = ArithInterpreter.eval env (parse_string str)
*)
(*****************************************************************)
(********************* Command line options **********************)
(*****************************************************************)
let parse f =
let _ = Errorline.startFile f in
let ic = open_in f in
let rv = Lexing.from_channel ic |> FixParse.defs FixLex.token in
let _ = close_in ic in
rv
let read_inputs usage =
Co.bprintflush true "\n\n";
Co.bprintflush true "========================================================\n";
Co.bprintflush true "© Copyright 2009 Regents of the University of California.\n";
Co.bprintflush true "All Rights Reserved.\n";
Co.bprintflush true "========================================================\n";
Co.bprintflush false (Sys.argv |> Array.to_list |> String.concat " ");
Co.bprintflush false "\n========================================================\n";
let fs = ref [] in
let _ = Arg.parse Co.arg_spec (fun s -> fs := s::!fs) usage in
let fq = !fs |> BS.time "parse" (Misc.flap parse) |> FixConfig.create in
(!fs, fq)