Commit 13d586e6 authored by Mário Pereira's avatar Mário Pereira

Extraction: new dependencies computation for program symbols.

This breaks extraction of multiprecision/wmpn.mlw.

Need some code refactoring, especially to avoid some (likely) unecessary module
translations.
parent 8017de9c
......@@ -236,6 +236,7 @@ module mach.int.Int63
end
module mach.int.Random63
syntax val s "REMOVE"
syntax val init "Random.init %1"
syntax val self_init "Random.self_init %1"
syntax val random_bool "Random.bool %1"
......@@ -246,26 +247,26 @@ module mach.int.State63
(* the most appropriate way to do this would be to have
something similar to [remove] from smt drivers:
remove val create *)
syntax val create "SHOULD_NOT_BE_HERE"
syntax val init "SHOULD_NOT_BE_HERE"
syntax val self_init "SHOULD_NOT_BE_HERE"
syntax val random_bool "SHOULD_NOT_BE_HERE"
syntax val random_int63 "SHOULD_NOT_BE_HERE"
syntax val create "REMOVE"
syntax val init "REMOVE"
syntax val self_init "REMOVE"
syntax val random_bool "REMOVE"
syntax val random_int63 "REMOVE"
end
module set.Fset
syntax val mem "SHOULD_NOT_BE_HERE"
syntax val (==) "SHOULD_NOT_BE_HERE"
syntax val subset "SHOULD_NOT_BE_HERE"
syntax val is_empty "SHOULD_NOT_BE_HERE"
syntax val empty "SHOULD_NOT_BE_HERE"
syntax val add "SHOULD_NOT_BE_HERE"
syntax val remove "SHOULD_NOT_BE_HERE"
syntax val union "SHOULD_NOT_BE_HERE"
syntax val inter "SHOULD_NOT_BE_HERE"
syntax val diff "SHOULD_NOT_BE_HERE"
syntax val choose "SHOULD_NOT_BE_HERE"
syntax val cardinal "SHOULD_NOT_BE_HERE"
syntax val mem "REMOVE"
syntax val (==) "REMOVE"
syntax val subset "REMOVE"
syntax val is_empty "REMOVE"
syntax val empty "REMOVE"
syntax val add "REMOVE"
syntax val remove "REMOVE"
syntax val union "REMOVE"
syntax val inter "REMOVE"
syntax val diff "REMOVE"
syntax val choose "REMOVE"
syntax val cardinal "REMOVE"
end
module mach.peano.Peano
......@@ -352,19 +353,24 @@ module mach.int.MinMax63
end
module mach.array.Array63
syntax type array "(%1 array)"
syntax val make "Array.make %1 %2"
syntax val ([]) "%1.(%2)"
syntax val ([]<-) "%1.(%2) <- %3"
syntax val length "Array.length %1"
syntax val append "Array.append %1 %2"
syntax val sub "Array.sub %1 %2 %3"
syntax val copy "Array.copy %1"
syntax val fill "Array.fill %1 %2 %3 %4"
syntax val blit "Array.blit %1 %2 %3 %4 %5"
syntax val self_blit "Array.blit %1 %2 %1 %3 %4"
syntax type array "(%1 array)"
syntax exception OutOfBounds "Invalid_argument \"index out of bounds\""
syntax val make "Array.make %1 %2"
syntax val ([]) "%1.(%2)"
syntax val ([]<-) "%1.(%2) <- %3"
syntax val defensive_get "%1.(%2)"
syntax val defensive_set "%1.(%2) <- %3"
syntax val length "Array.length %1"
syntax val append "Array.append %1 %2"
syntax val sub "Array.sub %1 %2 %3"
syntax val copy "Array.copy %1"
syntax val fill "Array.fill %1 %2 %3 %4"
syntax val blit "Array.blit %1 %2 %3 %4 %5"
syntax val self_blit "Array.blit %1 %2 %1 %3 %4"
syntax val init "Array.init %1 %2"
end
module mach.array.ArrayInt63
syntax type array63 "(int array)"
syntax val make "Array.make %1 %2"
......
......@@ -21,8 +21,12 @@ why3:
dir:
mkdir -p build
MLWFILES= $(addsuffix .mlw, toom logical div mul sub add compare util)
cfiles: why3 dir
$(WHY3) extract -D c -L . --recursive --modular --interface -o build/ wmpn.mlw
$(WHY3) extract -D c -L . --recursive --modular --interface -o build/ \
wmpn.mlw
#$(MLWFILES)
extract: why3 dir cfiles
......
......@@ -512,7 +512,7 @@ module Translate = struct
else let unit_ = pv (* create_pvsymbol (id_fresh "_") ity_unit *) in
[ML.Dlet (ML.Lvar (unit_, expr info Stv.empty MaskGhost e))]
| PDlet (LDvar (pv, {e_node = Eexec ({c_node = Cany}, cty)})) ->
Debug.dprintf debug_compile "compiling undifined constant %a@"
Debug.dprintf debug_compile "compiling undefined constant %a@"
print_pv pv;
let ty = mlty_of_ity cty.cty_mask cty.cty_result in
[ML.Dval (pv, ty)]
......
......@@ -184,7 +184,8 @@ and iter_deps_pat f = function
| Pas (p, _) -> iter_deps_pat f p
and iter_deps_expr f e = match e.e_node with
| Econst _ | Evar _ | Eabsurd -> ()
| Econst _ | Eabsurd -> ()
| Evar pv -> f pv.pv_vs.vs_name
| Eapp (rs, exprl) ->
f rs.rs_name; List.iter (iter_deps_expr f) exprl
| Efun (args, e) ->
......
This diff is collapsed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment