Select Git revision
Forked from
Polito Guillermo / tofork
Source project has a limited visibility.
rclockedlang.ml 34.52 KiB
open Common
type prog = decl list
and decl =
{
decl_desc: decl_desc;
decl_loc: Location.t;
}
and decl_desc =
| Node of node_desc
| Enum of String.t * StringSet.t * Types.ty_enum
and eq = expr eq_base
and node_desc =
{
node_name: String.t;
node_inputs: vdecl list;
node_outputs: vdecl list;
node_locals: vdecl list;
node_eqs: eq list;
node_ty: Types.ty_expr;
node_ck: Refclocks.ck_fn;
}
and 'expr eq_base =
{
eq_lhs: String.t list;
eq_rhs: 'expr;
eq_loc: Location.t;
}
and ('desc,'ck) expr_base =
{
expr_desc: 'desc;
expr_loc: Location.t;
expr_ty: Types.ty_expr;
expr_ck: 'ck;
}
and expr = (expr_desc,Refclocks.ck_out) expr_base
and full_atom_expr = (atom_expr_desc,Refclocks.ck_out) expr_base
and atom_expr = (atom_expr_desc,Refclocks.ck_r) expr_base
and ident_expr = (ident_expr_desc,Refclocks.ck_r) expr_base
and const_expr = (const_expr_desc,Refclocks.ck_r) expr_base
and ident_fn_expr = (ident_expr_desc,Refclocks.ck_fn) expr_base
and expr_desc =
[
| `ExprConst of const
| `ExprIdent of String.t
| `ExprApply of ident_fn_expr * ident_expr List.t
| `ExprPckUp of rate_op_desc
| `ExprFby of const_expr*rate_op_desc
| `ExprWhen of when_desc
| `ExprMerge of merge_desc
| `ExprITE of ite_desc
]
and atom_expr_desc =
[
| `ExprConst of const
| `ExprIdent of String.t ]
and ident_expr_desc =
[
| `ExprIdent of String.t
]
and const_expr_desc =
[
| `ExprConst of const
]
and vdecl = Refclocks.ck_r vdecl_base
(* and vdecl_f = Refclocks.fck_r vdecl_base *)
(* and vdecl_a = Refclocks.ack_r vdecl_base *)
and 'ck vdecl_base =
{
vdecl_name: String.t;
vdecl_ty_decl: Types.decl;
vdecl_ck_decl: Commonclocks.decl;
vdecl_dl: Int.t Option.t;
vdecl_ty: Types.ty_expr;
vdecl_ck: 'ck;
}
and rate_op_desc =
{
rate_expr: ident_expr;
rate_factor: Int.t;
rate_ty: Types.ty_fn;
rate_ck: Refclocks.ck_fn;
}
and const =
[
| `ConstInt of Int.t
| `ConstChar of Char.t
| `ConstFloat of Float.t
| `ConstEnum of enum_value
]
and enum_value = {variant: String.t; enum: String.t}
and when_desc =
{
when_expr: ident_expr;
case: String.t;
cond_expr: ident_expr;
when_ty: Types.ty_fn;
when_ck: Refclocks.ck_fn;
}
and merge_desc =
{
merge_var: ident_expr;
merge_exprs: (String.t*ident_expr) list;
merge_ty: Types.ty_fn;
merge_ck: Refclocks.ck_fn
}
and ite_desc =
{
if_expr: ident_expr;
then_expr: ident_expr;
else_expr: ident_expr;
ite_ty: Types.ty_fn;
ite_ck: Refclocks.ck_fn; }
module PP =
struct
let rec prog =
fun ff p ->
Print.list "@[<v>" "@ @ " "@]" decl ff p
and decl =
fun ff (d:decl) ->
match d.decl_desc with
| Node ndesc ->
node ff ndesc
| Enum (ename,evariants,_) ->
enum ff ename evariants
and node =
fun ff ({node_name;node_inputs;node_outputs;node_locals;node_eqs;node_ty;node_ck}: node_desc) ->
Format.fprintf ff "@[<v>";
Format.fprintf ff "@[<v>@[<hov 2>node@ %s@ :@ %a@ rate@ %a"
node_name Types.PP.ty node_ty Refclocks.PP.ck_fn node_ck;
Print.list "@ @[<hov 2>(" ";@ " ")@]@]" vdecl ff node_inputs;
Format.fprintf ff "@ returns@ ";
Print.list "@[<hov 2>(" ";@ " ")@]" vdecl ff node_outputs;
Format.fprintf ff "@]@ ";
Print.list "var @[<hov>" "@ " "@]@ " (Print.post "%a;" vdecl) ff node_locals;
Print.list "@[<v 2>let@ " "@ " "@]@ tel" eq ff node_eqs;
Format.fprintf ff "@]"
and enum =
fun ff ename evariants ->
Format.fprintf ff "@[<v>@[<h>type@ %s@ =@]%a@]"
ename
(Print.seq "@ | " "@ | " "" Format.pp_print_string)
(StringSet.to_seq evariants)
and eq =
fun ff {eq_lhs;eq_rhs;_} ->
Format.fprintf ff "@[<hov 2>%a@ =@ %a;@]"
(Print.list "@[<hov>" ",@," "@]" Format.pp_print_string) eq_lhs
expr eq_rhs
and expr =
let pp_ident_fn_expr : Format.formatter -> ident_fn_expr -> unit =
fun ff {expr_desc=`ExprIdent f;expr_ty;expr_ck;_} ->
Format.fprintf ff "@[<hov 2>%s(%a@ rate@ %a)@]"
f
Types.PP.ty expr_ty
Refclocks.PP.ck_fn expr_ck
in
let aux =
fun ff (e:expr) ->
match e.expr_desc with
| `ExprConst `ConstInt i -> Format.fprintf ff "%i" i
| `ExprConst `ConstChar c -> Format.fprintf ff "%c" c
| `ExprConst `ConstFloat f -> Format.fprintf ff "%f" f
| `ExprConst `ConstEnum {variant;_} -> Format.fprintf ff "%s" variant
| `ExprIdent id -> Format.fprintf ff "%s" id
| `ExprApply (f,args) ->
Format.fprintf ff "@[<hov 2>%a@,(%a)@]"
pp_ident_fn_expr f
(Print.list "@[<hov 2>" ",@ " "@]" expr)
(args :> expr List.t)
| `ExprPckUp {rate_expr;rate_factor;rate_ty;rate_ck} ->
Format.fprintf ff "@[<hov 2>(%a)@ @[<hov 2>*^%i(%a@ rate@ %a)@]@]"
expr (rate_expr :> expr)
rate_factor
Types.PP.ty (rate_ty :> Types.ty_expr)
Refclocks.PP.ck_fn rate_ck | `ExprFby (cst,{rate_expr;rate_ty;rate_ck;rate_factor=_}) ->
Format.fprintf ff "@[<hov 2>%a@ @[<hov 2>fby(%a@ rate@ %a)@]@ %a@]"
expr (cst :> expr)
Types.PP.ty (rate_ty :> Types.ty_expr)
Refclocks.PP.ck_fn rate_ck
expr (rate_expr :> expr)
| `ExprWhen {when_expr;case;cond_expr;when_ty;when_ck} ->
Format.fprintf ff "@[<hov 2>(%a)@ @[<hov 2>when(%a@ rate@ %a)@]@ @[<hov 2>%s->%a@]@]"
expr (when_expr :> expr)
Types.PP.ty (when_ty :> Types.ty_expr)
Refclocks.PP.ck_fn when_ck
case
expr (cond_expr :> expr)
| `ExprMerge {merge_var;merge_exprs;merge_ty;merge_ck} ->
Format.fprintf ff "@[<hov 2>merge(%a@ rate@ %a)(%a,@ %a)@]"
Types.PP.ty (merge_ty :> Types.ty_expr)
Refclocks.PP.ck_fn merge_ck
expr (merge_var :> expr)
(Print.list
"" ",@ " ""
(fun ff (case,e) ->
Format.fprintf ff "%s->%a"
case expr (e :> expr)))
merge_exprs
| `ExprITE {if_expr;then_expr;else_expr;ite_ty;ite_ck} ->
Format.fprintf ff "@[<hov 2>if(%a@ rate@ %a)@ %a@ then@ %a@ else@ %a@]"
Types.PP.ty (ite_ty :> Types.ty_expr)
Refclocks.PP.ck_fn ite_ck
expr (if_expr :> expr)
expr (then_expr :> expr)
expr (else_expr :> expr)
in
fun ff e ->
Format.fprintf ff "@[<hov>%a@,:@ %a@ rate@ %a@]"
aux e Types.PP.ty e.expr_ty Refclocks.PP.ck (e.expr_ck :> Refclocks.ck)
and vdecl =
fun ff v ->
Format.fprintf ff "@[<hov>%s:@ %a@ rate@ %a@ %a@]"
v.vdecl_name
Types.PP.ty v.vdecl_ty
Refclocks.PP.ck (v.vdecl_ck :> Refclocks.ck)
dl v.vdecl_dl
and dl =
fun ff d ->
Print.option
(fun ff i -> Format.fprintf ff "due %i" i)
""
ff d
end
module UtilsTypes =
struct
type enve =
| CkArrow of Refclocks.ck_fn
| CkRef of Refclocks.ck_r
type env = enve Env.String.t
type state =
{
typer_state: Refclocks.state;
main_node: String.t;
z3: Z3.t;
}
type node_state =
{
state: state;
env: env;
made_vars: Refclocks.Make.made_vars;
substitutions: Refclocks.ck_r IntMap.t
}
end
module Utils =
struct
open UtilsTypes
let typer_state = Refclocks.Predef.init_state
let init_prog = Env.String.empty
let init_state main_node =
{
typer_state;
main_node;
z3 = Z3.make ();
}
let with_ty_state_1 : type a o. (Refclocks.state -> a -> (Refclocks.state * o)) -> node_state -> a -> (node_state * o) =
fun fn node_state x ->
let state = node_state.state in
let typer_state = state.typer_state in
let typer_state,out = fn typer_state x in
let state = {state with typer_state} in
let node_state = {node_state with state} in
node_state,out
let with_ty_state_2 : type a b o. (Refclocks.state -> a -> b -> (Refclocks.state * o)) -> node_state -> a -> b -> (node_state * o) =
fun fn node_state x y ->
let state = node_state.state in
let typer_state = state.typer_state in
let typer_state,out = fn typer_state x y in
let state = {state with typer_state} in
let node_state = {node_state with state} in
node_state,out
let with_ty_state_3 : type a b c o. (Refclocks.state -> a -> b -> c -> (Refclocks.state * o)) -> node_state -> a -> b -> c -> (node_state * o) =
fun fn node_state x y z ->
let state = node_state.state in
let typer_state = state.typer_state in
let typer_state,out = fn typer_state x y z in
let state = {state with typer_state} in
let node_state = {node_state with state} in
node_state,out
let new_ck_r : node_state -> Refclocks.ck_r_desc -> bool -> node_state * Refclocks.ck_r =
with_ty_state_2 Refclocks.new_ck
let new_ck_out : node_state -> Refclocks.ck_out_desc -> bool -> node_state * Refclocks.ck_out =
with_ty_state_2 Refclocks.new_ck
let new_ck_fn : node_state -> Refclocks.ck_fn_desc -> bool -> node_state * Refclocks.ck_fn =
with_ty_state_2 Refclocks.new_ck
let refine_pck_up : Refclocks.state -> Int.t -> Structclocks.ck_arrow_expr -> Refclocks.state * Refclocks.ck_fn =
let refine_arg_ck_c: Refclocks.state -> Structclocks.ck_c -> Refclocks.state * Refclocks.ck_c =
fun typer_state ->
function
| {ck_desc=`Pck;_} -> typer_state,Refclocks.Predef.pck
| {ck_desc=`On _;_} -> failwith "Unimplemented"
| {ck_desc=`CkVar|`CkUnivar|`Zeta _;_} -> failwith "Internal error" in
let refine_out_ck_c: Refclocks.state -> Structclocks.ck_c -> Refclocks.state * Refclocks.ck_c =
fun typer_state ->
function
| {ck_desc=`Pck;_} -> typer_state,Refclocks.Predef.pck
| {ck_desc=`On _;_} -> failwith "Unimplemented"
| {ck_desc=`CkVar|`CkUnivar|`Zeta _;_} -> failwith "Internal error"
in
fun typer_state rate_factor {ck_desc=`CkArrow (ck_args,ck_out);ck_scoped;_} ->
let typer_state,ck_args,arg =
match ck_args with
| [arg,
{Structclocks.ck_desc=`CkRefine (ck_c,RefHole);
ck_scoped=ref_scoped;_}
]
->
let typer_state,ck_c = refine_arg_ck_c typer_state ck_c in
let refinement = Refclocks.RefRel (RefPDv, RefCst rate_factor) in
let typer_state,ck_r = Refclocks.new_ck typer_state (`CkRefine (ck_c,refinement)) ref_scoped in
typer_state,[arg,ck_r],arg
| _ -> failwith "Internal error"
in
let typer_state,ck_out =
match ck_out with
| {Structclocks.ck_desc=`CkRefine (ck_c,RefHole);ck_scoped=ref_scoped;_} ->
let typer_state,ck_c = refine_out_ck_c typer_state ck_c in
let refinement = Refclocks.RefCon
(
RefRel (RefPEq, (RefBin (RefDiv, RefPer (AVVar arg), RefCst rate_factor))),
RefRel (RefOEq, RefOff (AVVar arg))
)
in
Refclocks.new_ck typer_state (`CkRefine (ck_c,refinement)) ref_scoped
| _ -> failwith "Internal error"
in
Refclocks.new_ck typer_state (`CkArrow (ck_args,ck_out)) ck_scoped
let refine_pck_up = with_ty_state_2 refine_pck_up
let subs_refinement_ck_r = with_ty_state_3 Refclocks.RSubstitute.of_ck_r
let subs_refinement_ck_out = with_ty_state_3 Refclocks.RSubstitute.of_ck_out
end
module Make =
struct
open UtilsTypes
let rec of_sclocked: String.t -> Sclockedlang.prog -> prog =
fun main_node sprog ->
let state = Utils.init_state main_node in
Env.String.st_map decl_of_sclocked Utils.init_prog state sprog
and decl_of_sclocked env state (decl: Sclockedlang.decl) =
let decl_loc = decl.decl_loc in
match decl.decl_desc with
| Node ndesc ->
let state,ndesc = node_of_sclocked env state decl_loc ndesc in
let ck = ndesc.node_ck in
let kvs = [ndesc.node_name, CkArrow ck] in
kvs,state,{decl_desc=Node ndesc; decl_loc}
| Enum (ename,evariants,etype) ->
[],state,{decl_desc=Enum (ename,evariants,etype); decl_loc}
and node_of_sclocked env state _loc ndesc =
let node_state =
{
state;
env; made_vars=Refclocks.Make.no_made_vars;
substitutions=IntMap.empty
}
in
let node_state,node_inputs = vdecls_of_sclocked node_state ndesc.node_inputs in
let node_state,node_outputs = vdecls_of_sclocked node_state ndesc.node_outputs in
let node_state,node_locals = vdecls_of_sclocked node_state ndesc.node_locals in
let env =
List.to_seq node_inputs
|> Seq.append (List.to_seq node_outputs)
|> Seq.append (List.to_seq node_locals)
|> Seq.fold_left
(fun acc {vdecl_name;vdecl_ck;_} ->
let ck = vdecl_ck in
Env.String.add vdecl_name (CkRef ck) acc)
env
in
let node_state = {node_state with env} in
let node_state,node_eqs = eqs_of_sclocked node_state ndesc.node_eqs in
let node_state = init_substitutions node_state node_eqs node_inputs node_outputs node_locals in
let node_state = refine_chk_eqs node_state node_eqs in
let node_state,node_inputs = vdecls_ck_subs node_state node_inputs in
let node_state,node_outputs = vdecls_ck_subs node_state node_outputs in
let node_state,node_locals = vdecls_ck_subs node_state node_locals in
let node_state,node_eqs = eqs_ck_subs node_state node_eqs in
let node_state,node_ck = node_clock_of_vars node_state node_inputs node_outputs in
let ndesc =
{
node_name=ndesc.node_name;
node_inputs;
node_outputs;
node_locals;
node_eqs;
node_ty=ndesc.node_ty;
node_ck;
}
in
let state = node_state.state in
state,ndesc
and eqs_of_sclocked: node_state -> Sclockedlang.eq List.t -> node_state * eq List.t =
fun node_state eqs ->
List.fold_left_map
(fun node_state eq ->
eq_of_sclocked node_state eq)
node_state eqs
and eq_of_sclocked: node_state -> Sclockedlang.eq -> node_state * eq =
fun node_state {eq_lhs;eq_rhs;eq_loc} ->
let node_state,eq_rhs = expr_of_sclocked node_state eq_rhs in
node_state,{eq_lhs;eq_rhs;eq_loc}
and expr_of_sclocked: node_state -> Sclockedlang.expr -> node_state * expr =
fun node_state ->
function
| ({expr_desc=`ExprConst _;_} as expr) ->
let node_state,expr = const_expr_of_sclocked node_state expr in
node_state,(expr :> expr)
| ({expr_desc=`ExprIdent _;_} as expr) ->
let node_state,expr = ident_expr_of_sclocked node_state expr in
node_state,(expr :> expr)
| {expr_desc=`ExprApply (_f,_args);expr_ty=_;expr_ck={ck_id=_;_};expr_loc=_} ->
failwith "apply"
| {expr_desc=`ExprPckUp {rate_expr;rate_factor;rate_ty;rate_ck};
expr_ty;expr_ck;expr_loc} ->
let node_state,rate_expr = ident_expr_of_sclocked node_state rate_expr in
let node_state,rate_ck = Utils.refine_pck_up node_state rate_factor rate_ck in
let rate_op_desc = {rate_expr;rate_factor;rate_ty;rate_ck} in
let expr_ck = refine_env_ck_r node_state expr_ck in
let expr_ck = (expr_ck :> Refclocks.ck_out) in node_state,{expr_desc=`ExprPckUp rate_op_desc; expr_ty;expr_ck;expr_loc}
| {expr_desc=`ExprFby _;_} ->
failwith "fby"
| {expr_desc=`ExprWhen _;_} ->
failwith "when"
| {expr_desc=`ExprMerge _;_} ->
failwith "merge"
| {expr_desc=`ExprITE _;_} ->
failwith "ite"
and ident_expr_of_sclocked: node_state -> Sclockedlang.ident_expr -> node_state * ident_expr =
fun node_state ->
function
| ({expr_desc=(`ExprIdent _) as expr_desc;expr_ck;expr_ty;expr_loc}) ->
let expr_ck = refine_env_ck_r node_state expr_ck in
node_state,{expr_desc;expr_ck;expr_ty;expr_loc}
and const_expr_of_sclocked: node_state -> Sclockedlang.const_expr -> node_state * const_expr =
fun node_state ->
function
| {expr_desc=`ExprConst cst;expr_ty;expr_ck;expr_loc} ->
let cst =
match cst with
| (`ConstInt _|`ConstChar _|`ConstFloat _) as cst -> cst
| `ConstEnum {variant;enum} -> `ConstEnum {variant;enum}
in
let expr_desc = `ExprConst cst in
let expr_ck = refine_env_ck_r node_state expr_ck in
node_state,{expr_desc;expr_ty;expr_ck;expr_loc}
and refine_env_ck_r: node_state -> Structclocks.ck_r -> Refclocks.ck_r =
fun node_state {ck_id;_} ->
IntMap.find ck_id node_state.made_vars.mck_r
and vdecls_of_sclocked node_state vdecls =
List.fold_left_map
(fun state v ->
let v,state = vdecl_of_sclocked state v in
state,v)
node_state vdecls
and refine_chk_eqs : node_state -> eq List.t -> node_state =
fun node_state eqs ->
List.fold_left
(fun node_state eq -> refine_chk_eq node_state eq)
node_state eqs
and refine_chk_eq =
fun node_state {eq_rhs;eq_lhs;_} ->
let node_state,ck_chk = clock_of_var_list node_state eq_lhs in
refine_chk_expr node_state eq_rhs ck_chk
and refine_chk_expr =
fun node_state expr ck_chk ->
let node_state, ck_syn = refine_syn_expr node_state expr in
refine_sub_ck node_state ck_syn ck_chk
and refine_syn_expr: node_state -> expr -> node_state * Refclocks.ck_out =
let subs_ck: node_state -> Refclocks.ck_out -> node_state * Refclocks.ck_out =
let subs_ck_r: _ -> Refclocks.ck_r -> _ =
fun node_state {ck_id;_} ->
IntMap.find ck_id node_state.substitutions
in
fun node_state ->
function
| {ck_desc=`CkRefine _;ck_id;_} ->
node_state,(IntMap.find ck_id node_state.substitutions :> Refclocks.ck_out)
| {ck_desc=`CkTuple ckl;ck_scoped;_} ->
let ckl = List.map (subs_ck_r node_state) ckl in Utils.new_ck_out node_state (`CkTuple ckl) ck_scoped
in
let rec refine_syn_fn_like: node_state -> ident_expr List.t -> (String.t * Refclocks.ck_r) List.t -> Refclocks.ck_out -> Refclocks.ck_out -> node_state * Refclocks.ck_out =
fun node_state args ck_args expr_ck ck_out ->
match args,ck_args with
| [],[] ->
let node_state = refine_sub_ck node_state expr_ck ck_out in
subs_ck node_state expr_ck
| arg::args,(var,ck_arg)::ck_args ->
let node_state = refine_chk_expr node_state (arg :> expr) (ck_arg :> Refclocks.ck_out) in
let {expr_desc=`ExprIdent arg;_} = arg in
let node_state,ck_args =
List.fold_left_map
(fun node_state (var_arg,ck_arg) ->
let node_state,ck_arg =
Utils.subs_refinement_ck_r node_state var arg ck_arg
in
node_state,(var_arg,ck_arg))
node_state ck_args
in
let node_state,ck_out =
Utils.subs_refinement_ck_out node_state var arg ck_out
in
refine_syn_fn_like node_state args ck_args expr_ck ck_out
| [],_::_ | _::_,[] -> failwith "Internal error"
in
fun node_state expr ->
match expr with
| {expr_desc=`ExprConst _|`ExprIdent _;expr_ck;_} ->
subs_ck node_state expr_ck
| ({expr_desc=`ExprApply _|`ExprPckUp _|`ExprFby _|`ExprWhen _|`ExprMerge _|`ExprITE _;
expr_ck;_} as expr) ->
let {Refclocks.ck_desc=`CkArrow (ck_args,ck_out);_} =
match expr.expr_desc with
| (`ExprApply ({expr_ck=ck_fn;_},_)
|`ExprPckUp {rate_ck=ck_fn;_}|`ExprFby (_,{rate_ck=ck_fn;_})
|`ExprWhen {when_ck=ck_fn;_}|`ExprMerge {merge_ck=ck_fn;_}
|`ExprITE {ite_ck=ck_fn;_})
->
ck_fn
in
let args =
match expr.expr_desc with
| `ExprApply (_,args) -> (args :> ident_expr List.t)
| `ExprPckUp {rate_expr;_} -> [(rate_expr :> ident_expr)]
| `ExprFby (_cst,{rate_expr;_}) ->
[(failwith "todo" :> ident_expr); (rate_expr :> ident_expr)]
| `ExprWhen {when_expr;cond_expr;_} ->
([when_expr; cond_expr] :> ident_expr List.t)
| `ExprMerge {merge_var;merge_exprs;_} ->
(merge_var::(List.map snd merge_exprs) :> ident_expr List.t)
| `ExprITE {if_expr;then_expr;else_expr;_} ->
([if_expr; then_expr; else_expr] :> ident_expr List.t)
in
refine_syn_fn_like node_state args ck_args expr_ck ck_out
and refine_sub_ck: node_state -> Refclocks.ck_out -> Refclocks.ck_out -> node_state =
fun node_state ck_to_chk ck_is_chk ->
match ck_to_chk,ck_is_chk with
| ({ck_desc=`CkRefine _;_} as ck_to_chk),
({ck_desc=`CkRefine _;_} as ck_is_chk)
->
refine_sub_ck_r node_state ck_to_chk ck_is_chk
| ({ck_desc=`CkTuple _;_} as _ck_to_chk),
({ck_desc=`CkTuple _;_} as _ck_is_chk)
->
failwith "todo"
| {ck_desc=`CkRefine _;_},{ck_desc=`CkTuple _;_}
| {ck_desc=`CkTuple _;_},{ck_desc=`CkRefine _;_}
-> failwith "Internal error"
and refine_sub_ck_r: node_state -> Refclocks.ck_r -> Refclocks.ck_r -> node_state =
(* Check zeta, ons, etc. *)
let rec aux =
fun node_state lower higher ->
let get_env =
let map = Env.String.curr node_state.env in
fun v ->
match Env.String.Map.find v map with
| CkRef ck_r -> ck_r
| CkArrow _ -> failwith "Internal error"
in
let smt_state = Refclocks.SMT.init_smt_state in
let smt_state = Refclocks.SMT.state_with_ck_r smt_state get_env lower in
let smt_state = Refclocks.SMT.state_with_ck_r smt_state get_env higher in
let smt_state, smt_lower = Refclocks.SMT.of_ck_r smt_state lower in
let smt_state, smt_higher = Refclocks.SMT.of_ck_r smt_state higher in
let all_vars =
smt_state.vars_of_cks
|> IntMap.to_seq
|> Seq.map snd
|> Seq.flat_map (fun (v1,v2) -> List.to_seq [v1;v2])
|> Seq.map (fun v -> Smtlib.DeclareFun {fname=v;domain=[];range=Smtlib.IntSort})
|> List.of_seq
in
let ty_link = Refclocks.SMT.link_tys_ck_r smt_state lower higher in
Z3.push node_state.state.z3;
Z3.send node_state.state.z3 all_vars;
Z3.send node_state.state.z3 [Smtlib.Assert smt_lower];
if (Z3.check_sat node_state.state.z3) <> SAT then
failwith "type inconsistent";
Z3.send node_state.state.z3 [
Smtlib.Assert ty_link;
Smtlib.Assert (Smtlib.lnot smt_higher);
];
let unsat = Z3.check_sat node_state.state.z3 = UNSAT in
Z3.pop node_state.state.z3;
if unsat then
Some node_state
else
let {Refclocks.ck_desc=`CkRefine(_,r_h);_} = higher in
let {Refclocks.ck_desc=`CkRefine(ck_c,r_l);ck_scoped;_} = lower in
let node_state,lower' =
Utils.new_ck_r node_state
(`CkRefine (ck_c, Refclocks.RefCon(r_l,r_h)))
ck_scoped
in
match aux node_state lower' higher with
| Some node_state ->
let substitutions =
IntMap.add lower.ck_id lower' node_state.substitutions
in
Some {node_state with substitutions}
| None -> failwith "none"
in
fun node_state lower higher ->
match aux node_state lower higher with
| Some node_state -> node_state
| None ->
failwith @@ Format.asprintf "subtype fail %a %a"
Refclocks.PP.ck_r lower
Refclocks.PP.ck_r higher
(* and refine_sub_ck_e: node_state -> Refclocks.ck_e -> Refclocks.ck_e -> Bool.t = *)
(* fun node_state lower higher -> *)
(* match lower, higher with *)
(* | ({ck_desc=`CkRefine _;_} as lower),({ck_desc=`CkRefine _;_} as higher) *)
(* -> *)
(* refine_sub_ck_r node_state lower higher *) (* | ({ck_desc=`CkTuple _;_}),({ck_desc=`CkTuple _;_}) *)
(* -> *)
(* failwith "Unimplemented" *)
(* | _ -> failwith "Internal error" *)
and init_substitutions: node_state -> eq List.t -> vdecl List.t -> vdecl List.t -> vdecl List.t -> node_state =
let subs_of_ck_out: node_state -> Refclocks.ck_out -> node_state =
fun node_state ->
function
| ({ck_desc=`CkRefine _;ck_id;_} as ck_r) ->
let substitutions = IntMap.add ck_id ck_r node_state.substitutions in
{node_state with substitutions}
| {ck_desc=`CkTuple ckl;_} ->
let substitutions =
List.fold_left
(fun substitutions ({Refclocks.ck_id;_} as ck_r) ->
IntMap.add ck_id ck_r substitutions)
node_state.substitutions ckl
in
{node_state with substitutions}
in
let subs_of_atom_expr: node_state -> atom_expr -> node_state =
fun node_state {expr_ck;_} ->
subs_of_ck_out node_state (expr_ck :> Refclocks.ck_out)
in
let subs_of_expr node_state (e: expr) =
match e with
| {expr_desc=(`ExprConst _|`ExprIdent _);expr_ck;_} ->
subs_of_ck_out node_state expr_ck
| {expr_desc=(`ExprApply _|`ExprPckUp _|`ExprFby _|`ExprWhen _|`ExprMerge _|`ExprITE _) as expr_desc;expr_ck;_} ->
let node_state = subs_of_ck_out node_state expr_ck in
let ck_args =
match expr_desc with
| `ExprApply (_,args) -> (args :> atom_expr List.t)
| (`ExprPckUp {rate_expr;_}|`ExprFby (_,{rate_expr;_})) ->
([rate_expr] :> atom_expr List.t)
| `ExprWhen {when_expr;cond_expr;_} ->
([when_expr; cond_expr] :> atom_expr List.t)
| `ExprMerge {merge_var;merge_exprs;_} ->
(merge_var::(List.map snd merge_exprs) :> atom_expr List.t)
| `ExprITE {if_expr;then_expr;else_expr;_} ->
([if_expr; then_expr; else_expr] :> atom_expr List.t)
in
List.fold_left subs_of_atom_expr node_state ck_args
in
let subs_of_eq node_state {eq_rhs;_} =
subs_of_expr node_state eq_rhs
in
let subs_of_vdecl node_state (vdecl: vdecl) =
subs_of_ck_out node_state (vdecl.vdecl_ck :> Refclocks.ck_out)
in
fun node_state eqs inputs outputs locals ->
let node_state = List.fold_left subs_of_eq node_state eqs in
let node_state = List.fold_left subs_of_vdecl node_state inputs in
let node_state = List.fold_left subs_of_vdecl node_state outputs in
List.fold_left subs_of_vdecl node_state locals
and vdecl_of_sclocked node_state (v: Sclockedlang.vdecl) =
let
{
Sclockedlang.vdecl_name;
vdecl_ty_decl;
vdecl_ck_decl;
vdecl_dl;
vdecl_ty;
vdecl_ck;
} =
v
in
let make_state = node_state.state.typer_state, node_state.made_vars in let (typer_state,made_vars),vdecl_ck =
Refclocks.Make.of_struct_ck_r make_state vdecl_ck vdecl_ck_decl
in
let node_state = {node_state with
state={node_state.state with typer_state};
made_vars}
in
{
vdecl_name;
vdecl_ty_decl;
vdecl_ck_decl;
vdecl_dl;
vdecl_ty;
vdecl_ck;
},node_state
and vdecls_ck_subs node_state vdecls =
List.fold_left_map
vdecl_ck_subs
node_state vdecls
and vdecl_ck_subs node_state v =
let state,vdecl_ck = ck_r_ck_subs node_state v.vdecl_ck in
state,{v with vdecl_ck}
and eqs_ck_subs node_state eqs =
List.fold_left_map
eq_ck_subs
node_state eqs
and eq_ck_subs node_state eq =
let node_state,eq_rhs = expr_ck_subs node_state eq.eq_rhs in
node_state,{eq with eq_rhs}
and expr_ck_subs : node_state -> expr -> node_state * expr =
fun node_state expr ->
match expr with
| ({expr_desc=`ExprConst _|`ExprIdent _;expr_ck;_} as expr) ->
let node_state,expr_ck = ck_out_ck_subs node_state expr_ck in
node_state,{expr with expr_ck}
| ({expr_desc=(`ExprApply _|`ExprPckUp _|`ExprFby _|`ExprWhen _|`ExprMerge _|`ExprITE _) as expr_desc;
expr_ck;_} as expr) ->
let ck_fn =
match expr_desc with
| `ExprApply (f,_) ->
f.expr_ck
| `ExprPckUp {rate_ck;_} | `ExprFby (_,{rate_ck;_}) ->
rate_ck
| `ExprWhen {when_ck;_} -> when_ck
| `ExprMerge {merge_ck;_} -> merge_ck
| `ExprITE {ite_ck;_} -> ite_ck
in
let node_state,ck_fn = ck_fn_ck_subs node_state ck_fn in
let node_state,expr_desc =
match expr_desc with
| `ExprApply (f,args) ->
let state,f = ident_fn_expr_ck_subs node_state f in
let state,args =
List.fold_left_map
(fun node_state arg -> ident_expr_ck_subs node_state arg)
state args
in
state,`ExprApply (f,args)
| `ExprPckUp ({rate_expr;_} as rate_desc) ->
let node_state,rate_expr = ident_expr_ck_subs node_state rate_expr in
node_state,`ExprPckUp {rate_desc with rate_ck=ck_fn;rate_expr}
| `ExprFby (cst,({rate_expr;_} as rate_desc)) ->
let node_state,rate_expr = ident_expr_ck_subs node_state rate_expr in
node_state,`ExprFby (cst,{rate_desc with rate_ck=ck_fn;rate_expr})
| `ExprWhen ({when_expr;cond_expr;_} as when_desc) -> let node_state,when_expr = ident_expr_ck_subs node_state when_expr in
let node_state,cond_expr = ident_expr_ck_subs node_state cond_expr in
node_state,`ExprWhen {when_desc with when_expr;cond_expr;when_ck=ck_fn}
| `ExprMerge ({merge_var;merge_exprs;_} as merge_desc) ->
let node_state,merge_var = ident_expr_ck_subs node_state merge_var in
let node_state,merge_exprs =
List.fold_left_map
(fun node_state (case,e) ->
let state,e = ident_expr_ck_subs node_state e in
state,(case,e))
node_state merge_exprs
in
node_state,`ExprMerge {merge_desc with merge_var;merge_exprs;merge_ck=ck_fn}
| `ExprITE ({if_expr;then_expr;else_expr;_} as if_desc) ->
let node_state,if_expr = ident_expr_ck_subs node_state if_expr in
let node_state,then_expr = ident_expr_ck_subs node_state then_expr in
let node_state,else_expr = ident_expr_ck_subs node_state else_expr in
node_state,`ExprITE {if_desc with if_expr;then_expr;else_expr;ite_ck=ck_fn}
in
let node_state,expr_ck = ck_out_ck_subs node_state expr_ck in
node_state,{expr with expr_ck;expr_desc}
and const_expr_ck_subs : node_state -> const_expr -> node_state * const_expr =
fun node_state expr ->
let node_state,expr_ck = ck_r_ck_subs node_state expr.expr_ck in
node_state,{expr with expr_ck}
and ident_expr_ck_subs : node_state -> ident_expr -> node_state * ident_expr =
fun node_state expr ->
let node_state,expr_ck = ck_r_ck_subs node_state expr.expr_ck in
node_state,{expr with expr_ck}
and ident_fn_expr_ck_subs : node_state -> ident_fn_expr -> node_state * ident_fn_expr =
fun node_state expr ->
let node_state,expr_ck = ck_fn_ck_subs node_state expr.expr_ck in
node_state,{expr with expr_ck}
and ck_fn_ck_subs_aux: node_state -> Refclocks.ck_fn -> (node_state * Refclocks.ck_fn) option =
fun node_state ck_arrow ->
let {Refclocks.ck_desc=`CkArrow (ck_args,ck_out);_} = ck_arrow in
let node_state,ck_out,changed =
match ck_out_ck_subs_aux node_state ck_out with
| Some (node_state,ck_out) -> node_state,ck_out,true
| None -> node_state,ck_out,false
in
let (node_state,changed),ck_args =
List.fold_left_map
(fun (node_state,changed) (var,ck) ->
match ck_r_ck_subs_aux node_state ck with
| Some (node_state,ck) -> (node_state,true),(var,ck)
| None -> (node_state,changed),(var,ck))
(node_state,changed) ck_args
in
if changed then
let node_state,ck_arrow = Utils.new_ck_fn node_state (`CkArrow (ck_args,ck_out)) ck_arrow.ck_scoped in
Some(node_state,ck_arrow)
else
None
and ck_out_ck_subs_aux: node_state -> Refclocks.ck_out -> (node_state * Refclocks.ck_out) option =
fun node_state ck_e ->
match ck_e with
| ({Refclocks.ck_desc=`CkRefine _;_} as ck_r) ->
((ck_r_ck_subs_aux node_state ck_r) :> ((node_state * Refclocks.ck_out) option))
| _ -> failwith "f"
and ck_out_ck_subs: node_state -> Refclocks.ck_out -> node_state * Refclocks.ck_out =
fun node_state ck_out ->
match ck_out_ck_subs_aux node_state ck_out with
| Some(node_state,ck_out) -> node_state,ck_out | None -> node_state,ck_out
and ck_fn_ck_subs node_state ck_e =
match ck_fn_ck_subs_aux node_state ck_e with
| Some (node_state,ck_e) -> node_state,ck_e
| None -> node_state,ck_e
and ck_r_ck_subs_aux: node_state -> Refclocks.ck_r -> (node_state * Refclocks.ck_r) option =
fun node_state ck_r ->
match IntMap.find_opt ck_r.ck_id node_state.substitutions with
| Some ck_r ->
Some(node_state,ck_r)
| None -> None
and ck_r_ck_subs: node_state -> Refclocks.ck_r -> (node_state * Refclocks.ck_r) =
fun node_state ck_r ->
match ck_r_ck_subs_aux node_state ck_r with
| Some(node_state,ck_r) -> node_state,ck_r
| None -> node_state,ck_r
and node_clock_of_vars: node_state -> vdecl List.t -> vdecl List.t -> node_state * Refclocks.ck_fn =
fun node_state inputs outputs ->
let ck_args =
List.map
(fun v ->
v.vdecl_name,v.vdecl_ck)
inputs
in
let node_state,ck_out = clock_of_vdecls node_state outputs in
let typer_state,ck_arrow =
Refclocks.new_ck
node_state.state.typer_state (`CkArrow (ck_args,ck_out)) false
in
let state = {node_state.state with typer_state} in
let node_state = {node_state with state} in
node_state,ck_arrow
and clock_of_vdecls: node_state -> vdecl List.t -> node_state * Refclocks.ck_out =
fun node_state ->
function
| [] -> failwith "Internal error"
| [{vdecl_ck;_}] ->
let vdecl_ck = (vdecl_ck :> Refclocks.ck_out) in
node_state, vdecl_ck
| vdecls ->
let cks = List.map (fun v -> v.vdecl_ck) vdecls in
Utils.new_ck_out node_state (`CkTuple cks) false
and clock_of_var_list: node_state -> String.t List.t -> node_state * Refclocks.ck_out =
fun node_state ->
function
| [] -> failwith "Internal error"
| [v] ->
begin
match Env.String.Map.find v (Env.String.curr node_state.env) with
| CkRef ck_r -> node_state,(ck_r :> Refclocks.ck_out)
| _ -> failwith "Internal error"
end
| vdecls ->
let map = Env.String.curr node_state.env in
let ckl,scopeds =
List.map
(fun v ->
match Env.String.Map.find v map with
| CkRef ({ck_scoped;_} as ck_r) -> ck_r,ck_scoped
| CkArrow _ -> failwith "Internal error")
vdecls
|> List.split
in
let scoped = List.mem true scopeds in Utils.new_ck_out node_state (`CkTuple ckl) scoped
end