Attention une mise à jour du service Gitlab va être effectuée le mardi 14 décembre entre 13h30 et 14h00. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

Commit 3ea313fd authored by Mário Pereira's avatar Mário Pereira
Browse files

Extraction of polymorphic recursion (printing)

parent ea4e31ba
...@@ -29,7 +29,6 @@ open Ident ...@@ -29,7 +29,6 @@ open Ident
open Ity open Ity
open Ty open Ty
open Term open Term
open Stdlib
let clean_name fname = let clean_name fname =
(* TODO: replace with Filename.remove_extension (* TODO: replace with Filename.remove_extension
...@@ -54,13 +53,6 @@ module ML = struct ...@@ -54,13 +53,6 @@ module ML = struct
| Tapp of ident * ty list | Tapp of ident * ty list
| Ttuple of ty list | Ttuple of ty list
module Vvar = MakeMSHW (struct
type t = tvsymbol
let tag tvs = tvs.tv_name.id_tag
end)
module Svar = Vvar.S
type is_ghost = bool type is_ghost = bool
type var = ident * ty * is_ghost type var = ident * ty * is_ghost
...@@ -117,7 +109,7 @@ module ML = struct ...@@ -117,7 +109,7 @@ module ML = struct
rec_args : var list; rec_args : var list;
rec_exp : expr; rec_exp : expr;
rec_res : ty; rec_res : ty;
rec_svar : Svar.t; rec_svar : Stv.t;
} }
type is_mutable = bool type is_mutable = bool
...@@ -527,7 +519,7 @@ module Translate = struct ...@@ -527,7 +519,7 @@ module Translate = struct
let for_rec_def = { let for_rec_def = {
ML.rec_sym = for_rs; ML.rec_args = args; ML.rec_sym = for_rs; ML.rec_args = args;
ML.rec_rsym = for_rs; ML.rec_exp = for_expr; ML.rec_rsym = for_rs; ML.rec_exp = for_expr;
ML.rec_res = ML.tunit; ML.rec_svar = ML.Svar.empty; ML.rec_res = ML.tunit; ML.rec_svar = Stv.empty;
} in } in
let for_let = ML.Elet (ML.Lrec [for_rec_def], for_call_expr) in let for_let = ML.Elet (ML.Lrec [for_rec_def], for_call_expr) in
ML.mk_expr for_let ML.ity_unit eff ML.mk_expr for_let ML.ity_unit eff
...@@ -548,7 +540,7 @@ module Translate = struct ...@@ -548,7 +540,7 @@ module Translate = struct
(* build the set of type variables from functions arguments *) (* build the set of type variables from functions arguments *)
let rec add_tvar acc = function let rec add_tvar acc = function
| ML.Tvar tv -> ML.Svar.add tv acc | ML.Tvar tv -> Stv.add tv acc
| ML.Tapp (_, tyl) | ML.Ttuple tyl -> | ML.Tapp (_, tyl) | ML.Ttuple tyl ->
List.fold_left add_tvar acc tyl List.fold_left add_tvar acc tyl
...@@ -611,7 +603,7 @@ module Translate = struct ...@@ -611,7 +603,7 @@ module Translate = struct
let args = params cty.cty_args in let args = params cty.cty_args in
let svar = let svar =
let args' = List.map (fun (_, ty, _) -> ty) args in let args' = List.map (fun (_, ty, _) -> ty) args in
let svar = List.fold_left add_tvar ML.Svar.empty args' in let svar = List.fold_left add_tvar Stv.empty args' in
add_tvar svar res in add_tvar svar res in
let ef = expr info ef in let ef = expr info ef in
{ ML.rec_sym = rs1; ML.rec_rsym = rs2; { ML.rec_sym = rs1; ML.rec_rsym = rs2;
...@@ -772,7 +764,7 @@ module Translate = struct ...@@ -772,7 +764,7 @@ module Translate = struct
let res = ity rs1.rs_cty.cty_result in let res = ity rs1.rs_cty.cty_result in
let svar = let svar =
let args' = List.map (fun (_, ty, _) -> ty) args in let args' = List.map (fun (_, ty, _) -> ty) args in
let svar = List.fold_left add_tvar ML.Svar.empty args' in let svar = List.fold_left add_tvar Stv.empty args' in
add_tvar svar res in add_tvar svar res in
{ ML.rec_sym = rs1; ML.rec_rsym = rs2; { ML.rec_sym = rs1; ML.rec_rsym = rs2;
ML.rec_args = args; ML.rec_exp = expr info e; ML.rec_args = args; ML.rec_exp = expr info e;
......
...@@ -315,17 +315,17 @@ module Print = struct ...@@ -315,17 +315,17 @@ module Print = struct
(* (print_list space (print_expr ~paren:true info)) tl *) (* (print_list space (print_expr ~paren:true info)) tl *)
and print_svar fmt s = and print_svar fmt s =
Svar.iter (fun tv -> fprintf fmt "%a" print_tv tv) s Stv.iter (fun tv -> fprintf fmt "%a" print_tv tv) s
and print_fun_type_args info fmt (args, s, res) = and print_fun_type_args info fmt (args, s, res) =
if Svar.is_empty s then if Stv.is_empty s then
fprintf fmt "@[%a@] :@ %a@ =@" fprintf fmt "@[%a@] :@ %a@ ="
(print_list space (print_vs_arg info)) args (print_list space (print_vs_arg info)) args
(print_ty info) res (print_ty info) res
else else
let ty_args = List.map (fun (_, ty, _) -> ty) args in let ty_args = List.map (fun (_, ty, _) -> ty) args in
let id_args = List.map (fun (id, _, _) -> id) args in let id_args = List.map (fun (id, _, _) -> id) args in
fprintf fmt ": @[%a@]. @[%a@] ->@ %a@ =@ fun @[%a@]@ ->@\n" fprintf fmt ": @[%a@]. @[%a@] ->@ %a@ =@ fun @[%a@]@ ->"
print_svar s print_svar s
(print_list arrow (print_ty info)) ty_args (print_list arrow (print_ty info)) ty_args
(print_ty info) res (print_ty info) res
...@@ -345,7 +345,7 @@ module Print = struct ...@@ -345,7 +345,7 @@ module Print = struct
let print_one fst fmt = function let print_one fst fmt = function
| { rec_sym = rs1; rec_args = args; rec_exp = e; | { rec_sym = rs1; rec_args = args; rec_exp = e;
rec_res = res; rec_svar = s } -> rec_res = res; rec_svar = s } ->
fprintf fmt "@[<hov 2>%s %a @[%a@] %a@]" fprintf fmt "@[<hov 2>%s %a @[%a@]@ %a@]"
(if fst then "let rec" else "and") (if fst then "let rec" else "and")
(print_lident info) rs1.rs_name (print_lident info) rs1.rs_name
(print_fun_type_args info) (args, s, res) (print_fun_type_args info) (args, s, res)
......
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