Linearity annotations in the AST
This commit is contained in:
Cédric Pasteur
parent
0b9dc1fc01
commit
6c9d9e90d1
11 changed files with 141 additions and 44 deletions
67
compiler/global/linearity.ml
Normal file
67
compiler/global/linearity.ml
Normal file
|
|
@ -0,0 +1,67 @@
|
|||
open Format
|
||||
open Names
|
||||
open Misc
|
||||
|
||||
type linearity_var = name
|
||||
|
||||
type linearity =
|
||||
| Ltop
|
||||
| Lat of linearity_var
|
||||
| Lvar of linearity_var (*a linearity var, used in functions sig *)
|
||||
| Ltuple of linearity list
|
||||
|
||||
module LinearitySet = Set.Make(struct
|
||||
type t = linearity
|
||||
let compare = compare
|
||||
end)
|
||||
|
||||
(** Returns a linearity object from a linearity list. *)
|
||||
let prod = function
|
||||
| [l] -> l
|
||||
| l -> Ltuple l
|
||||
|
||||
let linearity_list_of_linearity = function
|
||||
| Ltuple l -> l
|
||||
| l -> [l]
|
||||
|
||||
let rec lin_skeleton lin = function
|
||||
| Types.Tprod l -> Ltuple (List.map (lin_skeleton lin) l)
|
||||
| _ -> lin
|
||||
|
||||
(** Same as Misc.split_last but on a linearity. *)
|
||||
let split_last_lin = function
|
||||
| Ltuple l ->
|
||||
let l, acc = split_last l in
|
||||
Ltuple l, acc
|
||||
| l ->
|
||||
Ltuple [], l
|
||||
|
||||
let rec is_not_linear = function
|
||||
| Ltop -> true
|
||||
| Ltuple l -> List.for_all is_not_linear l
|
||||
| _ -> false
|
||||
|
||||
exception UnifyFailed
|
||||
|
||||
(** Unifies lin with expected_lin and returns the result
|
||||
of the unification. Applies subtyping and instantiate linearity vars. *)
|
||||
let rec unify_lin expected_lin lin =
|
||||
match expected_lin,lin with
|
||||
| Ltop, Lat _ -> Ltop
|
||||
| Ltop, Lvar _ -> Ltop
|
||||
| Lat r1, Lat r2 when r1 = r2 -> Lat r1
|
||||
| Ltop, Ltop -> Ltop
|
||||
| Ltuple l1, Ltuple l2 -> Ltuple (List.map2 unify_lin l1 l2)
|
||||
| Lvar _, Lat r -> Lat r
|
||||
| Lat r, Lvar _ -> Lat r
|
||||
| _, _ -> raise UnifyFailed
|
||||
|
||||
let rec lin_to_string = function
|
||||
| Ltop -> "at T"
|
||||
| Lat r -> "at "^r
|
||||
| Lvar r -> "at _"^r
|
||||
| Ltuple l_list -> String.concat ", " (List.map lin_to_string l_list)
|
||||
|
||||
let print_linearity ff l =
|
||||
fprintf ff " %s" (lin_to_string l)
|
||||
|
||||
|
|
@ -9,13 +9,14 @@
|
|||
(* global data in the symbol tables *)
|
||||
open Names
|
||||
open Types
|
||||
open Linearity
|
||||
|
||||
(** Warning: Whenever these types are modified,
|
||||
interface_format_version should be incremented. *)
|
||||
let interface_format_version = "20"
|
||||
|
||||
(** Node argument *)
|
||||
type arg = { a_name : name option; a_type : ty }
|
||||
type arg = { a_name : name option; a_type : ty; a_linearity : linearity }
|
||||
|
||||
(** Node static parameters *)
|
||||
type param = { p_name : name; p_type : ty }
|
||||
|
|
@ -49,7 +50,7 @@ let names_of_arg_list l = List.map (fun ad -> ad.a_name) l
|
|||
|
||||
let types_of_arg_list l = List.map (fun ad -> ad.a_type) l
|
||||
|
||||
let mk_arg name ty = { a_type = ty; a_name = name }
|
||||
let mk_arg ?(linearity = Ltop) name ty = { a_type = ty; a_linearity = linearity; a_name = name }
|
||||
|
||||
let mk_param name ty = { p_name = name; p_type = ty }
|
||||
|
||||
|
|
|
|||
|
|
@ -18,6 +18,7 @@ open Format
|
|||
open Global_printer
|
||||
open Pp_tools
|
||||
open Types
|
||||
open Linearity
|
||||
open Signature
|
||||
open Heptagon
|
||||
|
||||
|
|
@ -37,10 +38,10 @@ let rec print_pat ff = function
|
|||
| Etuplepat pat_list ->
|
||||
fprintf ff "@[<2>(%a)@]" (print_list_r print_pat """,""") pat_list
|
||||
|
||||
let rec print_vd ff { v_ident = n; v_type = ty; v_last = last } =
|
||||
fprintf ff "%a%a : %a%a"
|
||||
let rec print_vd ff { v_ident = n; v_type = ty; v_linearity = lin; v_last = last } =
|
||||
fprintf ff "%a%a : %a%a%a"
|
||||
print_last last print_ident n
|
||||
print_type ty print_last_value last
|
||||
print_type ty print_linearity lin print_last_value last
|
||||
|
||||
and print_last ff = function
|
||||
| Last _ -> fprintf ff "last "
|
||||
|
|
@ -90,8 +91,8 @@ and print_exps ff e_list =
|
|||
|
||||
and print_exp ff e =
|
||||
if !Compiler_options.full_type_info then
|
||||
fprintf ff "(%a : %a)"
|
||||
print_exp_desc e.e_desc print_type e.e_ty
|
||||
fprintf ff "(%a : %a%a)"
|
||||
print_exp_desc e.e_desc print_type e.e_ty print_linearity e.e_linearity
|
||||
else fprintf ff "%a" print_exp_desc e.e_desc
|
||||
|
||||
and print_exp_desc ff = function
|
||||
|
|
|
|||
|
|
@ -14,6 +14,7 @@ open Idents
|
|||
open Static
|
||||
open Signature
|
||||
open Types
|
||||
open Linearity
|
||||
open Clocks
|
||||
open Initial
|
||||
|
||||
|
|
@ -29,6 +30,7 @@ type iterator_type =
|
|||
type exp = {
|
||||
e_desc : desc;
|
||||
e_ty : ty;
|
||||
mutable e_linearity : linearity;
|
||||
e_ct_annot : ct;
|
||||
e_base_ck : ck;
|
||||
e_loc : location }
|
||||
|
|
@ -118,6 +120,7 @@ and present_handler = {
|
|||
and var_dec = {
|
||||
v_ident : var_ident;
|
||||
v_type : ty;
|
||||
v_linearity : linearity;
|
||||
v_clock : ck;
|
||||
v_last : last;
|
||||
v_loc : location }
|
||||
|
|
@ -190,8 +193,8 @@ and interface_desc =
|
|||
| Isignature of signature
|
||||
(*
|
||||
(* Helper functions to create AST. *)
|
||||
let mk_exp desc ?(ct_annot = Clocks.invalid_clock) ?(loc = no_location) ty =
|
||||
{ e_desc = desc; e_ty = ty; e_ct_annot = ct_annot;
|
||||
let mk_exp desc ?(linearity = Ltop) ?(ct_annot = Clocks.invalid_clock) ?(loc = no_location) ty =
|
||||
{ e_desc = desc; e_ty = ty; e_linearity = linearity; e_ct_annot = ct_annot;
|
||||
e_base_ck = Cbase; e_loc = loc; }
|
||||
|
||||
let mk_app ?(params=[]) ?(unsafe=false) op =
|
||||
|
|
@ -206,8 +209,8 @@ let mk_type_dec name desc =
|
|||
let mk_equation stateful desc =
|
||||
{ eq_desc = desc; eq_stateful = stateful; eq_loc = no_location; }
|
||||
|
||||
let mk_var_dec ?(last = Var) ?(clock = fresh_clock()) name ty =
|
||||
{ v_ident = name; v_type = ty; v_clock = clock;
|
||||
let mk_var_dec ?(last = Var) ?(linearity = Ltop) ?(clock = fresh_clock()) name ty =
|
||||
{ v_ident = name; v_type = ty; v_linearity = linearity; v_clock = clock;
|
||||
v_last = last; v_loc = no_location }
|
||||
|
||||
let mk_block stateful ?(defnames = Env.empty) ?(locals = []) eqs =
|
||||
|
|
|
|||
|
|
@ -60,6 +60,7 @@ List.iter (fun (str,tok) -> Hashtbl.add keyword_table str tok) [
|
|||
"fold", FOLD;
|
||||
"foldi", FOLDI;
|
||||
"mapfold", MAPFOLD;
|
||||
"at", AT;
|
||||
"quo", INFIX3("quo");
|
||||
"mod", INFIX3("mod");
|
||||
"land", INFIX3("land");
|
||||
|
|
|
|||
|
|
@ -4,6 +4,7 @@ open Signature
|
|||
open Location
|
||||
open Names
|
||||
open Types
|
||||
open Linearity
|
||||
open Hept_parsetree
|
||||
|
||||
|
||||
|
|
@ -47,6 +48,7 @@ open Hept_parsetree
|
|||
%token AROBASE
|
||||
%token DOUBLE_LESS DOUBLE_GREATER
|
||||
%token MAP MAPI FOLD FOLDI MAPFOLD
|
||||
%token AT
|
||||
%token <string> PREFIX
|
||||
%token <string> INFIX0
|
||||
%token <string> INFIX1
|
||||
|
|
@ -193,8 +195,9 @@ nonmt_params:
|
|||
;
|
||||
|
||||
param:
|
||||
| ident_list COLON ty_ident
|
||||
{ List.map (fun id -> mk_var_dec id $3 Var (Loc($startpos,$endpos))) $1 }
|
||||
| ident_list COLON located_ty_ident
|
||||
{ List.map (fun id -> mk_var_dec ~linearity:(snd $3)
|
||||
id (fst $3) Var (Loc($startpos,$endpos))) $1 }
|
||||
;
|
||||
|
||||
out_params:
|
||||
|
|
@ -248,12 +251,13 @@ loc_params:
|
|||
|
||||
|
||||
var_last:
|
||||
| ident_list COLON ty_ident
|
||||
{ List.map (fun id -> mk_var_dec id $3 Var (Loc($startpos,$endpos))) $1 }
|
||||
| LAST IDENT COLON ty_ident EQUAL exp
|
||||
{ [ mk_var_dec $2 $4 (Last(Some($6))) (Loc($startpos,$endpos)) ] }
|
||||
| LAST IDENT COLON ty_ident
|
||||
{ [ mk_var_dec $2 $4 (Last(None)) (Loc($startpos,$endpos)) ] }
|
||||
| ident_list COLON located_ty_ident
|
||||
{ List.map (fun id -> mk_var_dec ~linearity:(snd $3)
|
||||
id (fst $3) Var (Loc($startpos,$endpos))) $1 }
|
||||
| LAST IDENT COLON located_ty_ident EQUAL exp
|
||||
{ [ mk_var_dec ~linearity:(snd $4) $2 (fst $4) (Last(Some($6))) (Loc($startpos,$endpos)) ] }
|
||||
| LAST IDENT COLON located_ty_ident
|
||||
{ [ mk_var_dec ~linearity:(snd $4) $2 (fst $4) (Last(None)) (Loc($startpos,$endpos)) ] }
|
||||
;
|
||||
|
||||
ident_list:
|
||||
|
|
@ -261,6 +265,13 @@ ident_list:
|
|||
| IDENT COMMA ident_list { $1 :: $3 }
|
||||
;
|
||||
|
||||
located_ty_ident:
|
||||
| ty_ident
|
||||
{ $1, Ltop }
|
||||
| ty_ident AT ident
|
||||
{ $1, Lat $3 }
|
||||
;
|
||||
|
||||
ty_ident:
|
||||
| qualname
|
||||
{ Tid $1 }
|
||||
|
|
@ -626,8 +637,8 @@ nonmt_params_signature:
|
|||
;
|
||||
|
||||
param_signature:
|
||||
| IDENT COLON ty_ident { mk_arg (Some $1) $3 }
|
||||
| ty_ident { mk_arg None $1 }
|
||||
| IDENT COLON located_ty_ident { mk_arg (Some $1) $3 }
|
||||
| located_ty_ident { mk_arg None $1 }
|
||||
;
|
||||
|
||||
%%
|
||||
|
|
|
|||
|
|
@ -141,6 +141,7 @@ and present_handler =
|
|||
and var_dec =
|
||||
{ v_name : var_name;
|
||||
v_type : ty;
|
||||
v_linearity : Linearity.linearity;
|
||||
v_last : last;
|
||||
v_loc : location; }
|
||||
|
||||
|
|
@ -193,6 +194,7 @@ and program_desc =
|
|||
|
||||
type arg =
|
||||
{ a_type : ty;
|
||||
a_linearity : Linearity.linearity;
|
||||
a_name : var_name option }
|
||||
|
||||
type signature =
|
||||
|
|
@ -250,8 +252,8 @@ let mk_equation desc loc =
|
|||
let mk_interface_decl desc loc =
|
||||
{ interf_desc = desc; interf_loc = loc }
|
||||
|
||||
let mk_var_dec name ty last loc =
|
||||
{ v_name = name; v_type = ty;
|
||||
let mk_var_dec ?(linearity=Linearity.Ltop) name ty last loc =
|
||||
{ v_name = name; v_type = ty; v_linearity = linearity;
|
||||
v_last = last; v_loc = loc }
|
||||
|
||||
let mk_block locals eqs loc =
|
||||
|
|
@ -261,8 +263,8 @@ let mk_block locals eqs loc =
|
|||
let mk_const_dec id ty e loc =
|
||||
{ c_name = id; c_type = ty; c_value = e; c_loc = loc }
|
||||
|
||||
let mk_arg name ty =
|
||||
{ a_type = ty; a_name = name }
|
||||
let mk_arg name (ty,lin) =
|
||||
{ a_type = ty; a_linearity = lin; a_name = name }
|
||||
|
||||
let ptrue = Q Initial.ptrue
|
||||
let pfalse = Q Initial.pfalse
|
||||
|
|
|
|||
|
|
@ -237,6 +237,7 @@ let rec translate_exp env e =
|
|||
try
|
||||
{ Heptagon.e_desc = translate_desc e.e_loc env e.e_desc;
|
||||
Heptagon.e_ty = Types.invalid_type;
|
||||
Heptagon.e_linearity = Linearity.Ltop;
|
||||
Heptagon.e_base_ck = Clocks.Cbase;
|
||||
Heptagon.e_ct_annot = e.e_ct_annot;
|
||||
Heptagon.e_loc = e.e_loc }
|
||||
|
|
@ -372,6 +373,7 @@ and translate_var_dec env vd =
|
|||
(* env is initialized with the declared vars before their translation *)
|
||||
{ Heptagon.v_ident = Rename.var vd.v_loc env vd.v_name;
|
||||
Heptagon.v_type = translate_type vd.v_loc vd.v_type;
|
||||
Heptagon.v_linearity = vd.v_linearity;
|
||||
Heptagon.v_last = translate_last vd.v_last;
|
||||
Heptagon.v_clock = Clocks.fresh_clock(); (* TODO add clock annotations *)
|
||||
Heptagon.v_loc = vd.v_loc }
|
||||
|
|
@ -397,7 +399,7 @@ let params_of_var_decs =
|
|||
(translate_type vd.v_loc vd.v_type))
|
||||
|
||||
let args_of_var_decs =
|
||||
List.map (fun vd -> Signature.mk_arg
|
||||
List.map (fun vd -> Signature.mk_arg ~linearity:vd.v_linearity
|
||||
(Some vd.v_name)
|
||||
(translate_type vd.v_loc vd.v_type))
|
||||
|
||||
|
|
|
|||
|
|
@ -52,8 +52,9 @@ let equation locals eqs e =
|
|||
(mk_equation (Evarpat n) e):: eqs
|
||||
|
||||
let translate_var { Heptagon.v_ident = n; Heptagon.v_type = ty;
|
||||
Heptagon.v_linearity = linearity;
|
||||
Heptagon.v_loc = loc } =
|
||||
mk_var_dec ~loc:loc n ty
|
||||
mk_var_dec ~loc:loc ~linearity:linearity n ty
|
||||
|
||||
let translate_reset = function
|
||||
| Some { Heptagon.e_desc = Heptagon.Evar n } -> Some n
|
||||
|
|
@ -90,7 +91,9 @@ let translate_app app =
|
|||
~unsafe:app.Heptagon.a_unsafe (translate_op app.Heptagon.a_op)
|
||||
|
||||
let rec translate_extvalue e =
|
||||
let mk_extvalue = mk_extvalue ~loc:e.Heptagon.e_loc ~ty:e.Heptagon.e_ty in
|
||||
let mk_extvalue =
|
||||
mk_extvalue ~loc:e.Heptagon.e_loc ~linearity:e.Heptagon.e_linearity ~ty:e.Heptagon.e_ty
|
||||
in
|
||||
match e.Heptagon.e_desc with
|
||||
| Heptagon.Econst c -> mk_extvalue (Wconst c)
|
||||
| Heptagon.Evar x -> mk_extvalue (Wvar x)
|
||||
|
|
@ -105,9 +108,9 @@ let rec translate_extvalue e =
|
|||
| _ -> Error.message e.Heptagon.e_loc Error.Enormalization
|
||||
|
||||
let translate
|
||||
({ Heptagon.e_desc = desc; Heptagon.e_ty = ty;
|
||||
({ Heptagon.e_desc = desc; Heptagon.e_ty = ty; Heptagon.e_linearity = linearity;
|
||||
Heptagon.e_loc = loc } as e) =
|
||||
let mk_exp = mk_exp ~loc:loc in
|
||||
let mk_exp = mk_exp ~loc:loc ~linearity:linearity in
|
||||
match desc with
|
||||
| Heptagon.Econst _
|
||||
| Heptagon.Evar _
|
||||
|
|
|
|||
|
|
@ -15,6 +15,7 @@ open Idents
|
|||
open Signature
|
||||
open Static
|
||||
open Types
|
||||
open Linearity
|
||||
open Clocks
|
||||
|
||||
(** Warning: Whenever Minils ast is modified,
|
||||
|
|
@ -43,6 +44,7 @@ and extvalue = {
|
|||
w_desc : extvalue_desc;
|
||||
mutable w_ck: ck;
|
||||
w_ty : ty;
|
||||
w_linearity : linearity;
|
||||
w_loc : location }
|
||||
|
||||
and extvalue_desc =
|
||||
|
|
@ -54,6 +56,7 @@ and extvalue_desc =
|
|||
and exp = {
|
||||
e_desc : edesc;
|
||||
mutable e_ck: ck;
|
||||
e_linearity : linearity;
|
||||
e_ty : ty;
|
||||
e_loc : location }
|
||||
|
||||
|
|
@ -103,6 +106,7 @@ type eq = {
|
|||
type var_dec = {
|
||||
v_ident : var_ident;
|
||||
v_type : ty;
|
||||
v_linearity : linearity;
|
||||
v_clock : ck;
|
||||
v_loc : location }
|
||||
|
||||
|
|
@ -147,19 +151,20 @@ and program_desc =
|
|||
|
||||
(*Helper functions to build the AST*)
|
||||
|
||||
let mk_extvalue ~ty ?(clock = fresh_clock()) ?(loc = no_location) desc =
|
||||
{ w_desc = desc; w_ty = ty;
|
||||
let mk_extvalue ~ty ?(linearity = Ltop) ?(clock = fresh_clock()) ?(loc = no_location) desc =
|
||||
{ w_desc = desc; w_ty = ty; w_linearity = linearity;
|
||||
w_ck = clock; w_loc = loc }
|
||||
|
||||
let mk_exp ty ?(clock = fresh_clock()) ?(loc = no_location) desc =
|
||||
{ e_desc = desc; e_ty = ty;
|
||||
let mk_exp ty ?(linearity = Ltop) ?(clock = fresh_clock()) ?(loc = no_location) desc =
|
||||
{ e_desc = desc; e_ty = ty; e_linearity = linearity;
|
||||
e_ck = clock; e_loc = loc }
|
||||
|
||||
let mk_extvalue_exp ?(clock = fresh_clock()) ?(loc = no_location) ty desc =
|
||||
mk_exp ~clock:clock ~loc:loc ty (Eextvalue (mk_extvalue ~clock:clock ~loc:loc ~ty:ty desc))
|
||||
let mk_extvalue_exp ?(linearity = Ltop) ?(clock = fresh_clock()) ?(loc = no_location) ty desc =
|
||||
mk_exp ~clock:clock ~loc:loc ty
|
||||
(Eextvalue (mk_extvalue ~clock:clock ~loc:loc ~linearity:linearity ~ty:ty desc))
|
||||
|
||||
let mk_var_dec ?(loc = no_location) ?(clock = fresh_clock()) ident ty =
|
||||
{ v_ident = ident; v_type = ty; v_clock = clock; v_loc = loc }
|
||||
let mk_var_dec ?(loc = no_location) ?(linearity = Ltop) ?(clock = fresh_clock()) ident ty =
|
||||
{ v_ident = ident; v_type = ty; v_linearity = linearity; v_clock = clock; v_loc = loc }
|
||||
|
||||
let mk_equation ?(loc = no_location) pat exp =
|
||||
{ eq_lhs = pat; eq_rhs = exp; eq_loc = loc }
|
||||
|
|
|
|||
|
|
@ -2,6 +2,7 @@ open Misc
|
|||
open Names
|
||||
open Idents
|
||||
open Types
|
||||
open Linearity
|
||||
open Clocks
|
||||
open Static
|
||||
open Format
|
||||
|
|
@ -40,9 +41,9 @@ let rec print_clock ff = function
|
|||
| Cprod ct_list ->
|
||||
fprintf ff "@[<2>(%a)@]" (print_list_r print_clock """ *""") ct_list
|
||||
|
||||
let print_vd ff { v_ident = n; v_type = ty; v_clock = ck } =
|
||||
let print_vd ff { v_ident = n; v_type = ty; v_linearity = lin; v_clock = ck } =
|
||||
if !Compiler_options.full_type_info then
|
||||
fprintf ff "%a : %a :: %a" print_ident n print_type ty print_ck ck
|
||||
fprintf ff "%a : %a%a :: %a" print_ident n print_type ty print_linearity lin print_ck ck
|
||||
else fprintf ff "%a : %a" print_ident n print_type ty
|
||||
|
||||
let print_local_vars ff = function
|
||||
|
|
@ -85,8 +86,8 @@ and print_trunc_index ff idx =
|
|||
|
||||
and print_exp ff e =
|
||||
if !Compiler_options.full_type_info then
|
||||
fprintf ff "(%a : %a :: %a)"
|
||||
print_exp_desc e.e_desc print_type e.e_ty print_ck e.e_ck
|
||||
fprintf ff "(%a : %a%a :: %a)"
|
||||
print_exp_desc e.e_desc print_type e.e_ty print_linearity e.e_linearity print_ck e.e_ck
|
||||
else fprintf ff "%a" print_exp_desc e.e_desc
|
||||
|
||||
and print_every ff reset =
|
||||
|
|
@ -94,8 +95,8 @@ and print_every ff reset =
|
|||
|
||||
and print_extvalue ff w =
|
||||
if !Compiler_options.full_type_info then
|
||||
fprintf ff "(%a : %a :: %a)"
|
||||
print_extvalue_desc w.w_desc print_type w.w_ty print_ck w.w_ck
|
||||
fprintf ff "(%a : %a%a :: %a)"
|
||||
print_extvalue_desc w.w_desc print_type w.w_ty print_linearity w.w_linearity print_ck w.w_ck
|
||||
else fprintf ff "%a" print_extvalue_desc w.w_desc
|
||||
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue