Commit b7a611ed authored by Mário Pereira's avatar Mário Pereira

Code extraction (wip)

parent 786dc9d8
...@@ -197,7 +197,7 @@ module mach.array.Array32 ...@@ -197,7 +197,7 @@ module mach.array.Array32
end end
module mach.array.Array63 module mach.array.Array63
(* FIXME syntax type array63 "(%1 array)" *) syntax type array "(%1 array)"
syntax val make "Array.make" syntax val make "Array.make"
syntax val ([]) "Array.get" syntax val ([]) "Array.get"
...@@ -210,20 +210,7 @@ module mach.array.Array63 ...@@ -210,20 +210,7 @@ module mach.array.Array63
syntax val blit "Array.blit" syntax val blit "Array.blit"
syntax val self_blit "Array.blit" syntax val self_blit "Array.blit"
end end
module mach.array.Array63
(* FIXME syntax type array63 "(%1 array)" *)
syntax val make "Array.make"
syntax val ([]) "Array.get"
syntax val ([]<-) "Array.set"
syntax val length "Array.length"
syntax val append "Array.append"
syntax val sub "Array.sub"
syntax val copy "Array.copy"
syntax val fill "Array.fill"
syntax val blit "Array.blit"
syntax val self_blit "Array.blit"
end
module mach.matrix.Matrix63 module mach.matrix.Matrix63
syntax type matrix "(%1 array array)" syntax type matrix "(%1 array array)"
......
...@@ -66,7 +66,7 @@ module Array32 ...@@ -66,7 +66,7 @@ module Array32
ensures { result.length = a.length } ensures { result.length = a.length }
ensures { forall i:int. 0 <= i < to_int result.length -> result[i] = a[i] } ensures { forall i:int. 0 <= i < to_int result.length -> result[i] = a[i] }
val fill (a: array 'a) (ofs: int32) (len: int32) (v: 'a) : unit val fill (a: array 'a) (ofs: int32) (len: int32) (v: 'a) : unit writes {a}
requires { 0 <= to_int ofs /\ 0 <= to_int len } requires { 0 <= to_int ofs /\ 0 <= to_int len }
requires { to_int ofs + to_int len <= to_int a.length } requires { to_int ofs + to_int len <= to_int a.length }
ensures { forall i:int. ensures { forall i:int.
...@@ -265,6 +265,7 @@ module Array63 ...@@ -265,6 +265,7 @@ module Array63
ensures { forall i:int. 0 <= i < to_int result.length -> result[i] = a[i] } ensures { forall i:int. 0 <= i < to_int result.length -> result[i] = a[i] }
val fill (a: array 'a) (ofs: int63) (len: int63) (v: 'a) : unit val fill (a: array 'a) (ofs: int63) (len: int63) (v: 'a) : unit
writes { a }
requires { 0 <= to_int ofs /\ 0 <= to_int len } requires { 0 <= to_int ofs /\ 0 <= to_int len }
requires { to_int ofs + to_int len <= to_int a.length } requires { to_int ofs + to_int len <= to_int a.length }
ensures { forall i:int. ensures { forall i:int.
......
...@@ -86,6 +86,8 @@ module ML = struct ...@@ -86,6 +86,8 @@ module ML = struct
type var = ident * ty * is_ghost type var = ident * ty * is_ghost
type for_direction = To | DownTo
type pat = type pat =
| Pwild | Pwild
| Pident of ident | Pident of ident
...@@ -99,8 +101,6 @@ module ML = struct ...@@ -99,8 +101,6 @@ module ML = struct
type binop = Band | Bor | Beq type binop = Band | Bor | Beq
type for_direction = To | DownTo
type exn = type exn =
| Xident of ident | Xident of ident
| Xexit (* Pervasives.Exit *) | Xexit (* Pervasives.Exit *)
...@@ -194,6 +194,13 @@ type info = { ...@@ -194,6 +194,13 @@ type info = {
info_fname : string option; info_fname : string option;
} }
let has_syntax cxt id =
(* Mid.iter *)
(* (fun id' _ -> Format.printf "id': %s@\n" id'.id_string) *)
(* cxt.info_syn; *)
query_syntax cxt.info_syn id <> None ||
query_syntax cxt.info_convert id <> None
(** Translation from Mlw to ML *) (** Translation from Mlw to ML *)
module Translate = struct module Translate = struct
...@@ -382,7 +389,7 @@ module Translate = struct ...@@ -382,7 +389,7 @@ module Translate = struct
let al pv = pv_name pv, ML.tunit, false in let al pv = pv_name pv, ML.tunit, false in
let args = filter2_ghost_params pv_not_ghost def al cty.cty_args in let args = filter2_ghost_params pv_not_ghost def al cty.cty_args in
ML.mk_expr (ML.Efun (args, expr info e)) (ML.I e.e_ity) eff ML.mk_expr (ML.Efun (args, expr info e)) (ML.I e.e_ity) eff
| Eexec _ -> assert false | Eexec ({c_node = Cany}, _) -> assert false
| Eabsurd -> | Eabsurd ->
ML.mk_expr ML.Eabsurd (ML.I e.e_ity) eff ML.mk_expr ML.Eabsurd (ML.I e.e_ity) eff
| Ecase (e1, _) when e_ghost e1 -> | Ecase (e1, _) when e_ghost e1 ->
...@@ -398,13 +405,19 @@ module Translate = struct ...@@ -398,13 +405,19 @@ module Translate = struct
let e2 = expr info e2 in let e2 = expr info e2 in
let e3 = expr info e3 in let e3 = expr info e3 in
ML.mk_expr (ML.Eif (e1, e2, e3)) (ML.I e.e_ity) eff ML.mk_expr (ML.Eif (e1, e2, e3)) (ML.I e.e_ity) eff
| Ewhile (e1, _, _, e2) ->
let e1 = expr info e1 in
let e2 = expr info e2 in
ML.mk_expr (ML.Ewhile (e1, e2)) (ML.I e.e_ity) eff
| Efor (pv1, (pv2, direction, pv3), _, efor) ->
let e = expr info e in
let direction = for_direction direction in
ML.mk_expr (ML.Efor (pv1, pv2, direction, pv3, e)) (ML.I efor.e_ity) eff
| Eghost eg -> | Eghost eg ->
expr info eg (* it keeps its ghost status *) expr info eg (* it keeps its ghost status *)
| Eassign [(_, rs, pv)] -> | Eassign [(_, rs, pv)] ->
ML.mk_expr (ML.Eassign [(rs, pv)]) (ML.I e.e_ity) eff ML.mk_expr (ML.Eassign [(rs, pv)]) (ML.I e.e_ity) eff
| Epure _ -> assert false | Epure _ -> assert false
| Efor _ -> assert false
| Ewhile _ -> assert false
| Etry _ -> assert false | Etry _ -> assert false
| Eraise _ -> assert false | Eraise _ -> assert false
| _ -> (* TODO *) assert false | _ -> (* TODO *) assert false
...@@ -416,7 +429,7 @@ module Translate = struct ...@@ -416,7 +429,7 @@ module Translate = struct
let itd_name td = td.itd_its.its_ts.ts_name let itd_name td = td.itd_its.its_ts.ts_name
(* type declarations/definitions *) (* type declarations/definitions *)
let tdef itd = let tdef info itd =
let s = itd.itd_its in let s = itd.itd_its in
let ddata_constructs = (* point-free *) let ddata_constructs = (* point-free *)
List.map (fun ({rs_cty = rsc} as rs) -> List.map (fun ({rs_cty = rsc} as rs) ->
...@@ -446,11 +459,18 @@ module Translate = struct ...@@ -446,11 +459,18 @@ module Translate = struct
ML.mk_its_defn id args is_private (Some (ML.Dalias (ity t))) ML.mk_its_defn id args is_private (Some (ML.Dalias (ity t)))
end end
let is_val e =
match e.e_node with
| Eexec ({c_node = Cany}, _) -> true
| _ -> false
(* program declarations *) (* program declarations *)
let pdecl info pd = let pdecl info pd =
match pd.pd_node with match pd.pd_node with
| PDlet (LDsym (rs, _)) when rs_ghost rs -> | PDlet (LDsym (rs, _)) when rs_ghost rs ->
[] []
| PDlet (LDsym (rs, {c_node = Cfun e})) when is_val e ->
[]
| PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cfun e})) -> | PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cfun e})) ->
let args_filter = let args_filter =
let p (_, _, is_ghost) = not is_ghost in let p (_, _, is_ghost) = not is_ghost in
...@@ -471,11 +491,11 @@ module Translate = struct ...@@ -471,11 +491,11 @@ module Translate = struct
in in
[ML.Dlet (true, rec_def)] [ML.Dlet (true, rec_def)]
| PDlet (LDsym _) | PDlet (LDsym _)
| PDlet (LDvar (_, _)) | PDpure
| PDpure -> | PDlet (LDvar (_, _)) ->
[] []
| PDtype itl -> | PDtype itl ->
[ML.Dtype (List.map tdef itl)] [ML.Dtype (List.map (tdef info) itl)]
| PDexn xs -> | PDexn xs ->
if ity_equal xs.xs_ity ity_unit then if ity_equal xs.xs_ity ity_unit then
[ML.Dexn (xs, None)] [ML.Dexn (xs, None)]
......
...@@ -183,6 +183,13 @@ module Print = struct ...@@ -183,6 +183,13 @@ module Print = struct
List.filter (fun e -> not (rs_ghost e)) itd.itd_fields List.filter (fun e -> not (rs_ghost e)) itd.itd_fields
| _ -> [] | _ -> []
let args_syntax s tl =
try
ignore (Str.search_forward (Str.regexp "[%]\\([tv]?\\)[0-9]+") s 0);
with Not_found ->
tl
let rec print_apply info fmt rs pvl = let rec print_apply info fmt rs pvl =
let isfield = let isfield =
match rs.rs_field with match rs.rs_field with
...@@ -224,8 +231,16 @@ module Print = struct ...@@ -224,8 +231,16 @@ module Print = struct
fprintf fmt "@[<hov 2>{ %a}@]" fprintf fmt "@[<hov 2>{ %a}@]"
(print_list2 semi equal (print_rs info) (print_expr info)) (pjl, tl) (print_list2 semi equal (print_rs info) (print_expr info)) (pjl, tl)
| _, tl -> | _, tl ->
fprintf fmt "@[<hov 2>%a %a@]" let open Printer in
print_ident rs.rs_name (print_list space (print_expr info)) tl match query_syntax info.info_convert rs.rs_name,
query_syntax info.info_syn rs.rs_name with
| Some s, _
| _, Some s ->
fprintf fmt "@[<hov 2>%s %a@]"
s (print_list space (print_expr info)) tl
| _ ->
fprintf fmt "@[<hov 2>%a %a@]"
print_ident rs.rs_name (print_list space (print_expr info)) tl
and print_enode info fmt = function and print_enode info fmt = function
| Econst c -> | Econst c ->
...@@ -325,7 +340,7 @@ module Print = struct ...@@ -325,7 +340,7 @@ module Print = struct
let print_decl info fmt = function let print_decl info fmt = function
| Dlet (isrec, [rs, pvl, e]) -> | Dlet (isrec, [rs, pvl, e]) ->
fprintf fmt "@[<hov 2>%s %a@ %a =@ @[%a@]@]" fprintf fmt "@[<hov 2>%s %a@ %a =@ %a@]"
(if isrec then "let rec" else "let") (if isrec then "let rec" else "let")
print_ident rs.rs_name print_ident rs.rs_name
(print_list space print_vs_arg) pvl (print_list space print_vs_arg) pvl
...@@ -378,6 +393,7 @@ let fg ?fname m = ...@@ -378,6 +393,7 @@ let fg ?fname m =
try Filename.chop_extension s try Filename.chop_extension s
with Invalid_argument _ -> s with Invalid_argument _ -> s
in in
let f = Filename.basename f in
(remove_extension f) ^ "__" ^ mod_name ^ ".ml" (remove_extension f) ^ "__" ^ mod_name ^ ".ml"
let () = Pdriver.register_printer "ocaml" let () = Pdriver.register_printer "ocaml"
......
...@@ -129,7 +129,6 @@ let rec use_iter f l = ...@@ -129,7 +129,6 @@ let rec use_iter f l =
List.iter (function Uuse t -> f t | Uscope (_,_,l) -> use_iter f l | _ -> ()) l List.iter (function Uuse t -> f t | Uscope (_,_,l) -> use_iter f l | _ -> ()) l
let rec do_extract_module ?fname m = let rec do_extract_module ?fname m =
(* test_extract ?fname m; *)
let _extract_use m' = let _extract_use m' =
let fname = let fname =
if m'.mod_theory.Theory.th_path = [] then fname else None if m'.mod_theory.Theory.th_path = [] then fname else None
...@@ -158,9 +157,10 @@ let do_local_extract fname cin tlist = ...@@ -158,9 +157,10 @@ let do_local_extract fname cin tlist =
let format = !opt_parser in let format = !opt_parser in
let mm = let mm =
Env.read_channel ?format mlw_language env fname cin in Env.read_channel ?format mlw_language env fname cin in
if Queue.is_empty tlist then if Queue.is_empty tlist then begin
let do_m _ m = do_extract_module ~fname m in let do_m _ m = do_extract_module ~fname m in
Mstr.iter do_m mm Mstr.iter do_m mm;
end
else else
Queue.iter (do_extract_module_from fname mm) tlist Queue.iter (do_extract_module_from fname mm) tlist
...@@ -170,7 +170,8 @@ let do_input = function ...@@ -170,7 +170,8 @@ let do_input = function
| Some f, tlist -> | Some f, tlist ->
let fname, cin = match f with let fname, cin = match f with
| "-" -> "stdin", stdin | "-" -> "stdin", stdin
| f -> f, open_in f in | f ->
f, open_in f in
do_local_extract fname cin tlist; do_local_extract fname cin tlist;
close_in cin close_in cin
......
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