Commit 6eeaccb3 authored by Mário Pereira's avatar Mário Pereira

Code extraction (wip): patterns, let rec definitions, match expressions, executable expressions

parent 74d6bb5b
...@@ -44,6 +44,17 @@ ...@@ -44,6 +44,17 @@
*) *)
(*
Questions pour Jean-Christophe et Andreï :
- est-ce qu'il y a des utilisations particulières du champ
[itd_fields], vis-à-vis du champ [itd_constructors] ?
- comme l'AST [expr] est déjà en forme normale-A, est-ce que je
peux utiliser des applications de la forme [Eapp ident * ident list] ?
*)
(** Abstract syntax of ML *) (** Abstract syntax of ML *)
open Ident open Ident
...@@ -80,6 +91,8 @@ module ML = struct ...@@ -80,6 +91,8 @@ module ML = struct
| Xsyntax of string | Xsyntax of string
| Xexit (* Pervasives.Exit *) | Xexit (* Pervasives.Exit *)
type ity = I of Ity.ity | C of Ity.cty (* TODO: keep like this? *)
type expr = { type expr = {
e_node : expr_node; e_node : expr_node;
e_ity : ity; e_ity : ity;
...@@ -90,7 +103,7 @@ module ML = struct ...@@ -90,7 +103,7 @@ module ML = struct
| Econst of Number.integer_constant | Econst of Number.integer_constant
| Ebool of bool | Ebool of bool
| Eident of ident | Eident of ident
| Eapp of expr * expr list | Eapp of ident * ident list
| Efun of var list * expr | Efun of var list * expr
| Elet of ident * expr * expr | Elet of ident * expr * expr
| Eletrec of is_rec * (ident * var list * expr) list * expr | Eletrec of is_rec * (ident * var list * expr) list * expr
...@@ -125,7 +138,7 @@ module ML = struct ...@@ -125,7 +138,7 @@ module ML = struct
let mk_expr e_node e_ity e_effect = let mk_expr e_node e_ity e_effect =
{ e_node = e_node; e_ity = e_ity; e_effect = e_effect } { e_node = e_node; e_ity = e_ity; e_effect = e_effect }
(* TODO add here some smart constructors for ML expressions *) (* smart constructors *)
let ml_let id e1 e2 = let ml_let id e1 e2 =
Elet (id, e1, e2) Elet (id, e1, e2)
...@@ -158,6 +171,21 @@ module Translate = struct ...@@ -158,6 +171,21 @@ module Translate = struct
let type_args = (* point-free *) let type_args = (* point-free *)
List.map (fun x -> x.tv_name) List.map (fun x -> x.tv_name)
let rec pat p =
match p.pat_node with
| Pwild ->
ML.Pwild
| Pvar vs ->
ML.Pident vs.vs_name
| Por (p1, p2) ->
ML.Por (pat p1, pat p2)
| Pas (p, vs) ->
ML.Pas (pat p, vs.vs_name)
| Papp (ls, pl) when is_fs_tuple ls ->
ML.Ptuple (List.map pat pl)
| Papp (ls, pl) ->
ML.Papp (ls.ls_name, List.map pat pl)
(** programs *) (** programs *)
(* individual types *) (* individual types *)
...@@ -165,6 +193,8 @@ module Translate = struct ...@@ -165,6 +193,8 @@ module Translate = struct
match t.ity_node with match t.ity_node with
| Ityvar ({tv_name = tv}, _) -> | Ityvar ({tv_name = tv}, _) ->
ML.Tvar tv ML.Tvar tv
| Ityapp ({its_ts = ts}, itl, _) when is_ts_tuple ts ->
ML.Ttuple (List.map ity itl)
| Ityapp ({its_ts = ts}, itl, _) -> | Ityapp ({its_ts = ts}, itl, _) ->
ML.Tapp (ts.ts_name, List.map ity itl) ML.Tapp (ts.ts_name, List.map ity itl)
| _ -> (* TODO *) assert false | _ -> (* TODO *) assert false
...@@ -175,6 +205,10 @@ module Translate = struct ...@@ -175,6 +205,10 @@ module Translate = struct
if pv.pv_ghost then (pv_name pv, ML.tunit) if pv.pv_ghost then (pv_name pv, ML.tunit)
else vsty pv.pv_vs else vsty pv.pv_vs
let for_direction = function
| To -> ML.To
| DownTo -> ML.DownTo
(* function arguments *) (* function arguments *)
let args = (* point-free *) let args = (* point-free *)
List.map pvty List.map pvty
...@@ -184,12 +218,25 @@ module Translate = struct ...@@ -184,12 +218,25 @@ module Translate = struct
match e.e_node with match e.e_node with
| Evar pvs -> | Evar pvs ->
let pv_id = pv_name pvs in let pv_id = pv_name pvs in
ML.mk_expr (ML.Eident pv_id) e.e_ity e.e_effect ML.mk_expr (ML.Eident pv_id) (ML.I e.e_ity) e.e_effect
| Elet (LDvar (pvs, e1), e2) -> | Elet (LDvar (pvs, e1), e2) ->
let ml_let = ML.ml_let (pv_name pvs) (expr e1) (expr e2) in let ml_let = ML.ml_let (pv_name pvs) (expr e1) (expr e2) in
ML.mk_expr ml_let e.e_ity e.e_effect ML.mk_expr ml_let (ML.I e.e_ity) e.e_effect
| Eexec ({c_node = Capp (rs, pvl)}, _) ->
let rs_id = rs.rs_name in
let pv_id = List.map pv_name pvl in
ML.mk_expr (ML.Eapp (rs_id, pv_id)) (ML.I e.e_ity) e.e_effect
| Eabsurd ->
ML.mk_expr ML.Eabsurd (ML.I e.e_ity) e.e_effect
| Ecase (e1, pl) ->
let e1 = expr e1 in
let pl = List.map ebranch pl in
ML.mk_expr (ML.Ematch (e1, pl)) (ML.I e.e_ity) e.e_effect
| _ -> (* TODO *) assert false | _ -> (* TODO *) assert false
and ebranch ({pp_pat = p}, e) =
pat p, expr e
let its_args ts = ts.its_ts.ts_args let its_args ts = ts.its_ts.ts_args
let itd_name td = td.itd_its.its_ts.ts_name let itd_name td = td.itd_its.its_ts.ts_name
...@@ -203,16 +250,6 @@ module Translate = struct ...@@ -203,16 +250,6 @@ module Translate = struct
List.map (fun ({rs_cty = rsc} as rs) -> List.map (fun ({rs_cty = rsc} as rs) ->
rs.rs_name, List.map (fun {pv_vs = pv} -> type_ pv.vs_ty) rsc.cty_args) rs.rs_name, List.map (fun {pv_vs = pv} -> type_ pv.vs_ty) rsc.cty_args)
(** Question pour Jean-Christophe et Andreï :
est-ce que vous pouriez m'expliquer le champ [itd_fields],
utilisé dans une définition de type ([its_defn]) ?
MIS-À-JOUR : je viens de coder l'extraction d'une définition
d'un type enregistrement et je comprends maintenant que che
champ est utilisé pour stocker les champs d'une définition de
type enregistrement. Je veux toujours savoir s'il y a des
cas particulaires d'utilisation, en particulier vis-à-vis du
champ [itd_constructors] *)
(* type declarations/definitions *) (* type declarations/definitions *)
let tdef itd = let tdef itd =
let s = itd.itd_its in let s = itd.itd_its in
...@@ -245,23 +282,27 @@ module Translate = struct ...@@ -245,23 +282,27 @@ module Translate = struct
| PDlet (LDsym ({rs_name = rsn}, {c_node = Cany})) -> | PDlet (LDsym ({rs_name = rsn}, {c_node = Cany})) ->
Format.printf "LDsym Cany--> %s@." rsn.id_string; Format.printf "LDsym Cany--> %s@." rsn.id_string;
[] []
| PDlet (LDrec _) -> | PDlet (LDrec rl) ->
[] let rec_def =
List.map (fun {rec_fun = e; rec_rsym = rs} ->
let e = match e.c_node with Cfun e -> e | _ -> assert false in
rs.rs_name, args rs.rs_cty.cty_args, expr e) rl in
[ML.Dlet (true, rec_def)]
| PDpure -> | PDpure ->
[] []
| PDtype itl -> | PDtype itl ->
List.map tdef itl List.map tdef itl
| _ -> (* TODO *) assert false | PDexn ({xs_name = xsn} as xs) ->
if ity_equal xs.xs_ity ity_unit then
[ML.Dexn (xsn, None)]
else
[ML.Dexn (xsn, Some (ity xs.xs_ity))]
(* unit module declarations *) (* unit module declarations *)
let mdecl = function let mdecl = function
| Udecl pd -> | Udecl pd ->
pdecl pd pdecl pd
| Uuse _ -> | _ -> (* TODO *) []
[]
| Uscope _ ->
[]
| _ -> (* TODO *) assert false
(* modules *) (* modules *)
let module_ m = let module_ m =
......
...@@ -49,20 +49,21 @@ module Print = struct ...@@ -49,20 +49,21 @@ module Print = struct
let print_tv fmt tv = let print_tv fmt tv =
fprintf fmt "'%s" (id_unique aprinter tv) fprintf fmt "'%s" (id_unique aprinter tv)
(** Types *)
let protect_on b s = let protect_on b s =
if b then "(" ^^ s ^^ ")" else s if b then "(" ^^ s ^^ ")" else s
let star fmt () = fprintf fmt " *@ " let star fmt () = fprintf fmt " *@ "
(** Types *)
let rec print_ty ?(paren=false) fmt = function let rec print_ty ?(paren=false) fmt = function
| Tvar id -> | Tvar id ->
print_tv fmt id print_tv fmt id
| Ttuple [] -> | Ttuple [] ->
fprintf fmt "unit" fprintf fmt "unit"
| Ttuple tl -> | Ttuple tl ->
fprintf fmt (protect_on paren "%a") (print_list star (print_ty ~paren:false)) tl fprintf fmt (protect_on paren "@[%a@]")
(print_list star (print_ty ~paren:false)) tl
| Tapp (ts, []) -> | Tapp (ts, []) ->
print_ident fmt ts print_ident fmt ts
| Tapp (ts, [ty]) -> | Tapp (ts, [ty]) ->
...@@ -98,16 +99,48 @@ module Print = struct ...@@ -98,16 +99,48 @@ module Print = struct
let print_module_name fmt m = let print_module_name fmt m =
print_theory_name fmt m.mod_theory print_theory_name fmt m.mod_theory
let rec print_pat fmt = function
| Pwild ->
fprintf fmt "_"
| Pident id ->
print_ident fmt id
| Pas (p, id) ->
fprintf fmt "%a as %a" print_pat p print_ident id
| Por (p1, p2) ->
fprintf fmt "%a | %a" print_pat p1 print_pat p2
| Ptuple pl ->
fprintf fmt "(%a)" (print_list comma print_pat) pl
| Papp (id, []) ->
print_ident fmt id
| Papp (id, [p]) ->
fprintf fmt "%a %a" print_ident id print_pat p
| Papp (id, pl) ->
fprintf fmt "%a (%a)" print_ident id (print_list comma print_pat) pl
| Precord fl ->
let print_field fmt (id, p) =
fprintf fmt "%a = %a" print_ident id print_pat p
in
fprintf fmt "{ %a }" (print_list semi print_field) fl
let rec print_enode fmt = function let rec print_enode fmt = function
| Eident id -> | Eident id ->
print_ident fmt id print_ident fmt id
| Elet (id, e1, e2) -> | Elet (id, e1, e2) ->
fprintf fmt "@[<hov 2>let @[%a@] =@ @[%a@]@] in@ %a" fprintf fmt "@[<hov 2>let @[%a@] =@ @[%a@]@] in@ %a"
print_ident id print_ident id print_expr e1 print_expr e2
print_expr e1 | Eabsurd ->
print_expr e2 fprintf fmt "assert false (* absurd *)"
| Eapp (e, el) ->
fprintf fmt "@[<hov 2>%a %a@]"
print_ident e (print_list space print_ident) el
| Ematch (e, pl) ->
fprintf fmt "@[begin match @[%a@] with@\n@[<hov>%a@] end@]"
print_expr e (print_list newline print_branch) pl
| _ -> (* TODO *) assert false | _ -> (* TODO *) assert false
and print_branch fmt (p, e) =
fprintf fmt "@[<hov 4>| %a ->@ %a@]" print_pat p print_expr e
and print_expr fmt e = and print_expr fmt e =
print_enode fmt e.e_node print_enode fmt e.e_node
...@@ -157,6 +190,11 @@ module Print = struct ...@@ -157,6 +190,11 @@ module Print = struct
| Dtype dl -> | Dtype dl ->
print_list newline print_type_decl fmt dl; print_list newline print_type_decl fmt dl;
fprintf fmt "@\n@\n" fprintf fmt "@\n@\n"
| Dexn (id, None) ->
fprintf fmt "exception %a@\n@\n" print_ident id
| Dexn (id, Some t) ->
fprintf fmt "@[<hov 2>exception %a of %a@]@\n@\n"
print_ident id (print_ty ~paren:true) t
| _ -> (* TODO *) assert false | _ -> (* TODO *) assert false
end end
......
...@@ -31,6 +31,24 @@ module M ...@@ -31,6 +31,24 @@ module M
ghost mutable v : seq 'a; ghost mutable v : seq 'a;
} }
exception Empty (list int, int)
exception Out_of_bounds int
let rec length (x: int) (l: list 'a) : int
variant { l }
= match l with
| Nil -> x
| Cons _ r -> length x r
end
let t (x:int) : int
requires { false }
= absurd
let rec ff (x: int) : int
diverges
= ff x
end end
(* (*
......
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