source: driver/exec.ml @ 2773

Last change on this file since 2773 was 2773, checked in by sacerdot, 8 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 910 bytes
Line 
1open Extracted.Errors
2
3let rec run g s =
4  (match Extracted.Cexec.is_final s with
5  | Extracted.Types.None ->
6    (match Extracted.Cexec.exec_step g s with
7    | Extracted.IOMonad.Value x -> run g (Extracted.Types.snd x)
8    | Extracted.IOMonad.Wrong m -> failwith (Error.errormsg m)
9    | _ -> failwith "unexpected interaction")
10  | Extracted.Types.Some r -> r)
11
12let convBool = function
13| Extracted.Bool.True -> true
14| Extracted.Bool.False -> false
15
16let bv_to_int v =
17  let rec aux i v =
18    match v with
19    | Extracted.Vector.VEmpty -> i
20    | Extracted.Vector.VCons (_,b,t) -> aux (2*i + (if convBool b then 1 else 0)) t
21  in aux 0 v
22;;
23
24let cl = ClightParser.process Sys.argv.(1) in
25let OK mid = Extracted.Compiler.front_end cl in
26let rtlabs = Extracted.Types.snd mid in
27let g = Extracted.Cexec.make_global cl in
28let OK s0 = Extracted.Cexec.make_initial_state cl in
29let r = run g s0 in
30exit (bv_to_int r)
Note: See TracBrowser for help on using the repository browser.