added scanning of if-then-else expressions
authorboehmes
Sun Aug 08 04:28:51 2010 +0200 (2010-08-08)
changeset 3824527da291ee202
parent 38244 59484a20c48f
child 38246 130d89f79ac1
added scanning of if-then-else expressions
src/HOL/Boogie/Tools/boogie_loader.ML
     1.1 --- a/src/HOL/Boogie/Tools/boogie_loader.ML	Fri Aug 06 18:14:18 2010 +0200
     1.2 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Sun Aug 08 04:28:51 2010 +0200
     1.3 @@ -341,7 +341,7 @@
     1.4    in
     1.5      (case Scan.error (Scan.finite (stopper i) scan) ts of
     1.6        (x, []) => x
     1.7 -    | (_, ts) => error (scan_err "unparsed input" ts))
     1.8 +    | (_, ts') => error (scan_err "unparsed input" ts'))
     1.9    end
    1.10  
    1.11  fun read_int' s = (case read_int (explode s) of (i, []) => SOME i | _ => NONE)
    1.12 @@ -499,6 +499,11 @@
    1.13          mk_nary (curry HOLogic.mk_conj) @{term True} ||
    1.14        scan_line "or" num :|-- scan_count exp >>
    1.15          mk_nary (curry HOLogic.mk_disj) @{term False} ||
    1.16 +      scan_line' "ite" |-- exp -- exp -- exp >> (fn ((c, t1), t2) =>
    1.17 +        let val T = Term.fastype_of t1
    1.18 +        in
    1.19 +          Const (@{const_name If}, [@{typ bool}, T, T] ---> T) $ c $ t1 $ t2
    1.20 +        end) ||
    1.21        binexp "implies" (binop @{term "op -->"}) ||
    1.22        scan_line "distinct" num :|-- scan_count exp >>
    1.23          (fn [] => @{term True}