source: driver/frontend.ml @ 2636

Last change on this file since 2636 was 2636, checked in by campbell, 7 years ago

Extracted front-end.

File size: 898 bytes
Line 
1open Extracted.Errors
2
3let rec run g s =
4  (match Extracted.RTLabs_semantics.rTLabs_is_final s with
5  | Extracted.Types.None ->
6    (match Extracted.RTLabs_semantics.eval_statement g s with
7    | Extracted.IOMonad.Value x -> run g (Extracted.Types.snd x)
8    | _ -> failwith "oh dear")
9  | Extracted.Types.Some r -> r)
10
11let convBool = function
12| Extracted.Bool.True -> true
13| Extracted.Bool.False -> false
14
15let bv_to_int v =
16  let rec aux i v =
17    match v with
18    | Extracted.Vector.VEmpty -> i
19    | Extracted.Vector.VCons (_,b,t) -> aux (2*i + (if convBool b then 1 else 0)) t
20  in aux 0 v
21;;
22
23let cl = ClightParser.process Sys.argv.(1) in
24let OK mid = Extracted.Compiler.front_end cl in
25let rtlabs = Extracted.Types.snd mid in
26let g = Extracted.RTLabs_semantics.make_global0 rtlabs in
27let OK s0 = Extracted.RTLabs_semantics.make_initial_state0 rtlabs in
28let r = run g s0 in
29exit (bv_to_int r)
Note: See TracBrowser for help on using the repository browser.