CristalCaveGem » LustreC

(*                                                                  *) 

(*                                                                  *) 

  destructive unification. Uses a bit of subtyping for periodic clocks. *)

(* Though it shares similarities with the typing module, no code

    is shared.  Simple environments, very limited identifier scoping, no

    identifier redefinition allowed. *)

    { e with Lexing.pos_cnum = e.Lexing.pos_cnum - (String.length id) }

(** [occurs cvar ck] returns true if the clock variable [cvar] occurs in

    clock [ck]. False otherwise. *)

      (occurs cvar ck1) || (occurs cvar ck2)

      List.exists (occurs cvar) ckl

  | Con (ck',_,_) -> occurs cvar ck'

  | Cvar  -> ck=cvar

  | Cunivar   -> false

  | Clink ck' -> occurs cvar ck'

  | Ccarrying (_,ck') -> occurs cvar ck'

  | Carry_const _

  | Carry_name ->

    if cr.carrier_scoped then

      raise (Scope_carrier cr);

  | Carry_var -> ()

  | Carry_link cr' -> generalize_carrier cr'

(** Promote monomorphic clock variables to polymorphic clock variables. *)

  | Carrow (ck1,ck2) ->

    generalize ck1; generalize ck2

  | Con (ck',cr,_) -> generalize ck'; generalize_carrier cr

    if ck.cscoped then

      raise (Scope_clock ck);

  | Cunivar -> ()

  | Ccarrying (cr,ck') ->

    generalize_carrier cr; generalize ck'

  try 

    generalize ck_node

  with

  | Carry_const _

  | Carry_name -> cr

      failwith "Internal error"

  | Carry_var ->

      try

        List.assoc cr.carrier_id !inst_cr_vars

      with Not_found ->            

        let cr_var = new_carrier Carry_name true in

        inst_cr_vars := (cr.carrier_id,cr_var)::!inst_cr_vars;

        cr_var

(* inst_ck_vars ensures that a polymorphic variable is instanciated with

   the same monomorphic variable if it occurs several times in the same

   type. inst_cr_vars is the same for carriers. *)

  | Carrow (ck1,ck2) ->

      {ck with cdesc =

       Carrow ((instantiate inst_ck_vars inst_cr_vars ck1),

               (instantiate inst_ck_vars inst_cr_vars ck2))}

      {ck with cdesc = Ctuple 

         (List.map (instantiate inst_ck_vars inst_cr_vars) cklist)}

  | Con (ck',c,l) ->

      let c' = instantiate_carrier c inst_cr_vars in

      {ck with cdesc = Con ((instantiate inst_ck_vars inst_cr_vars ck'),c',l)}

  | Cvar  -> ck

      {ck with cdesc = Clink (instantiate inst_ck_vars inst_cr_vars ck')}

  | Ccarrying (cr,ck') ->

      let cr' = instantiate_carrier cr inst_cr_vars in

        {ck with cdesc =

         Ccarrying (cr',instantiate inst_ck_vars inst_cr_vars ck')}

  | Cunivar ->

      try

        List.assoc ck.cid !inst_ck_vars

      with Not_found ->

        let var = new_ck Cvar true in

	inst_ck_vars := (ck.cid, var)::!inst_ck_vars;

	var

  if (not scoped) then

    begin

      cr.carrier_scoped <- scoped;

      match cr.carrier_desc with

	| Carry_const _ | Carry_name | Carry_var -> ()

      | Carry_link cr' -> update_scope_carrier scoped cr'

    end

  if (not scoped) then

    begin

      ck.cscoped <- scoped;

      match ck.cdesc with

      | Carrow (ck1,ck2) ->

          update_scope scoped ck1; update_scope scoped ck2

      | Ctuple clist ->

          List.iter (update_scope scoped) clist

      | Con (ck', _, _) -> update_scope scoped ck'(*; update_scope_carrier scoped cr*)

      | Cvar | Cunivar -> ()

      | Clink ck' ->

          update_scope scoped ck'

      | Ccarrying (cr,ck') ->

          update_scope_carrier scoped cr; update_scope scoped ck'

    end

  if cr1==cr2 then ()

      begin

	cr2.carrier_desc <- Carry_link cr1;

	update_scope_carrier cr2.carrier_scoped cr1

      end

      begin

        cr1.carrier_desc <- Carry_link cr2;

        update_scope_carrier cr1.carrier_scoped cr2

      end

      if cr1.carrier_id < cr2.carrier_id then

        begin

          cr2.carrier_desc <- Carry_link cr1;

          update_scope_carrier cr2.carrier_scoped cr1

        end

      else

        begin

          cr1.carrier_desc <- Carry_link cr2;

          update_scope_carrier cr1.carrier_scoped cr2

        end

    | _,_ -> assert false

  if cr1==cr2 then ()

      begin

	cr2.carrier_desc <- Carry_link cr1;

	update_scope_carrier cr2.carrier_scoped cr1

      end

    | Carry_name, Carry_const _ -> raise (Mismatch (cr1, cr2))

      if cr1.carrier_id < cr2.carrier_id then

        begin

          cr2.carrier_desc <- Carry_link cr1;

          update_scope_carrier cr2.carrier_scoped cr1

        end

      else

        begin

          cr1.carrier_desc <- Carry_link cr2;

          update_scope_carrier cr1.carrier_scoped cr2

        end

    | _,_ -> assert false

  try

    unify_carrier ck1 ck2

  with

  | Unify (ck1',ck2') ->

    raise (Error (loc, Clock_clash (ck1',ck2')))

  | Mismatch (cr1,cr2) ->

    raise (Error (loc, Carrier_mismatch (cr1,cr2)))

(** [unify ck1 ck2] unifies clocks [ck1] and [ck2]. Raises [Unify

    (ck1,ck2)] if the clocks are not unifiable.*)

  if ck1==ck2 then

    ()

    match ck1.cdesc,ck2.cdesc with

      if ck1.cid < ck2.cid then

        begin

          ck2.cdesc <- Clink (simplify ck1);

          update_scope ck2.cscoped ck1

        end

      else

        begin

          ck1.cdesc <- Clink (simplify ck2);

          update_scope ck1.cscoped ck2

        end

    | (Cvar, _) when (not (occurs ck1 ck2)) ->

    | (_, Cvar) when (not (occurs ck2 ck1)) ->

    | Ccarrying (cr1,ck1'),Ccarrying (cr2,ck2') ->

    | Ccarrying (_,_),_ | _,Ccarrying (_,_) ->

      raise (Unify (ck1,ck2))

    | Carrow (c1,c2), Carrow (c1',c2') ->

      unify c1 c1'; unify c2 c2'

      if (List.length ckl1) <> (List.length ckl2) then

        raise (Unify (ck1,ck2));

    | Con (ck',c1,l1), Con (ck'',c2,l2) when l1=l2 ->

    | Cunivar, _ | _, Cunivar -> ()

    | _,_ -> raise (Unify (ck1,ck2))

  if ck1==ck2 then

    ()

      match ck1.cdesc,ck2.cdesc with

      | Cvar, Cvar ->

          if ck1.cid < ck2.cid then

            begin

              ck2.cdesc <- Clink (simplify ck1);

              update_scope ck2.cscoped ck1

            end

          else

            begin

              ck1.cdesc <- Clink (simplify ck2);

              update_scope ck1.cscoped ck2

            end

      | (Cvar, _) -> raise (Unify (ck1,ck2))

      | (_, Cvar) when (not (occurs ck2 ck1)) ->

          update_scope ck2.cscoped ck1;

          ck2.cdesc <- Clink (simplify ck1)

      | Ccarrying (cr1,ck1'),Ccarrying (cr2,ck2') ->

          semi_unify_carrier cr1 cr2;

          semi_unify ck1' ck2'

      | Ccarrying (_,_),_ | _,Ccarrying (_,_) ->

          raise (Unify (ck1,ck2))

      | Carrow (c1,c2), Carrow (c1',c2') ->

	begin

          semi_unify c1 c1';

	  semi_unify c2 c2'

	end

      | Ctuple ckl1, Ctuple ckl2 ->

          if (List.length ckl1) <> (List.length ckl2) then

            raise (Unify (ck1,ck2));

          List.iter2 semi_unify ckl1 ckl2

      | Con (ck',c1,l1), Con (ck'',c2,l2) when l1=l2 ->

          semi_unify_carrier c1 c2;

          semi_unify ck' ck''

      | Cunivar, _ | _, Cunivar -> ()

      | _,_ -> raise (Unify (ck1,ck2))

(* Returns the value corresponding to a pclock (integer) factor

   expression. Expects a constant expression (checked by typing). *)

  match e.expr_desc with 

  | Expr_const

      (Const_int i) -> i

  | _ -> failwith "Internal error: int_factor_of_expr"

  | Ccarrying (_, ck') -> ck'

  | Con(ck', cr, l)    -> clock_on (clock_uncarry ck') cr l

  | Ctuple ckl         -> clock_of_clock_list (List.map clock_uncarry ckl)

  | _                  -> ck

  try

    unify ck1 ck2

  with

  | Unify (ck1',ck2') ->

    raise (Error (loc, Clock_clash (ck1',ck2')))

  | Mismatch (cr1,cr2) ->

    raise (Error (loc, Carrier_mismatch (cr1,cr2)))

  try

    semi_unify ck1 ck2

  with

  | Unify (ck1',ck2') ->

    raise (Error (loc, Clock_clash (ck1',ck2')))

  | Mismatch (cr1,cr2) ->

    raise (Error (loc, Carrier_mismatch (cr1,cr2)))

  | Ctuple cl1         , Ctuple cl2         ->

    if List.length cl1 <> List.length cl2

    then raise (Unify (ck1, ck2))

  | Ctuple [c1]        , _                  -> sub_unify sub c1 ck2

  | _                  , Ctuple [c2]        -> sub_unify sub ck1 c2

  | Con (c1, cr1, t1)  , Con (c2, cr2, t2) when t1=t2 ->

    begin

      unify_carrier cr1 cr2;

      sub_unify sub c1 c2

    end

  | Ccarrying (cr1, c1), Ccarrying (cr2, c2)->

    begin

      unify_carrier cr1 cr2;

      sub_unify sub c1 c2

    end

  | _, Ccarrying (_, c2)           when sub -> sub_unify sub ck1 c2

  | _                                       -> unify ck1 ck2

  try

    sub_unify sub ck1 ck2

  with

  | Unify (ck1',ck2') ->

    raise (Error (loc, Clock_clash (ck1',ck2')))

  | Mismatch (cr1,cr2) ->

    raise (Error (loc, Carrier_mismatch (cr1,cr2)))

(* Unifies all the clock variables in the clock type of a tuple 

   expression, so that the clock type only uses at most one clock variable *)

(*(match ref_ck_opt with

| None     -> Format.eprintf "unify_tuple_clock None %a@." Clocks.print_ck ck

  | Some ck' -> Format.eprintf "unify_tuple_clock (Some %a) %a@." Clocks.print_ck ck' Clocks.print_ck ck);*)

    | Con _

    | Cvar ->

        begin

          match !ck_var with

          | None ->

              ck_var:=Some ck

          | Some v ->

              (* may fail *)

              try_unify ck v loc

        end

        List.iter aux cl

    | Carrow _ -> assert false (* should not occur *)

        aux ck1

    | _ -> ()

  in aux ck

(* Unifies all the clock variables in the clock type of an imported

   node, so that the clock type only uses at most one base clock variable,

   that is, the activation clock of the node *)

    | Cvar ->

      begin

        match !ck_var with

        | None ->

          ck_var := Some ck

        | Some v ->

          (* cannot fail *)

          try_unify ck v loc

      end

    | Carrow (ck1,ck2) ->

      aux ck1; aux ck2

    | Con (ck1, _, _) -> aux ck1

    | _ -> ()

(* Computes the root clock of a tuple or a node clock,

   which is not the same as the base clock.

   Root clock will be used as the call clock 

   of a given node instance *)

        List.iter aux cl

    | Carrow (ck1,ck2) ->

        aux ck1; aux ck2

    | _ ->

        begin

          match !branch with

          | None ->

              branch := Some (Clocks.branch ck)

          | Some br ->

              (* cannot fail *)

              branch := Some (Clocks.common_prefix br (Clocks.branch ck))

        end

  begin

    aux ck;

    Clocks.clock_of_root_branch root (Utils.desome !branch)

  end

(* Clocks a list of arguments of Lustre builtin operators:

   - type each expression, remove carriers of clocks as

     carriers may only denote variables, not arbitrary expr.

   - try to unify these clocks altogether

*)

  let ck_list = List.map (fun e -> clock_uncarry (clock_expr env e)) expr_list in

(* emulates a subtyping relation between clocks c and (cr : c),

   used during node application only *)

and clock_subtyping_arg env ?(sub=true) real_arg formal_clock =

 let args = expr_list_of_expr args in

  if Basic_library.is_homomorphic_fun f && List.exists is_tuple_expr args

  then

      let args = Utils.transpose_list (List.map expr_list_of_expr args) in

      Clocks.clock_of_clock_list (List.map (fun args -> clock_call env f args clock_reset loc) args)

  else

    clock_call env f args clock_reset loc

  clock_expr ~nocarrier:nocarrier env (expr_of_ident id loc)

and clock_expr ?(nocarrier=true) env expr =

  let resulting_ck = 

        try

          Env.lookup_value env v

        with Not_found -> 

          failwith ("Internal error, variable \""^v^"\" not found")

      let ck = clock_standard_args env [e1] in

      let ck = clock_standard_args env [e1] in

      let ck_c = clock_standard_args env [c] in

      let ck = clock_standard_args env [t; e] in

    | Expr_appl (id, args, r) ->

      (try

         (* for a modular compilation scheme, all inputs/outputs must share the same clock !

            this is also the reset clock !

         *)

         let cr =

           match r with

           | None        -> new_var true

           | Some c      -> clock_standard_args env [c] in

         let couts = clock_appl env id args (clock_uncarry cr) expr.expr_loc in

         expr.expr_clock <- couts;

         couts

       with exn -> (

           Format.eprintf "Current expr: %a@." Printers.pp_expr expr;

           raise exn

         ))

    | Expr_fby (e1,e2)

    | Expr_arrow (e1,e2) ->

      let ck = clock_standard_args env [e1; e2] in

    | Expr_pre e -> (* todo : deal with phases as in tail ? *)

      let ck = clock_standard_args env [e] in

    | Expr_when (e,c,l) ->

      let ce = clock_standard_args env [e] in

    | Expr_merge (c,hl) ->

      List.iter (fun (t, h) ->

          unify_tuple_clock (Some (new_ck (Con (cvar,crvar,t)) true)) ckh h.expr_loc) hl;

      let cres = clock_current ((snd (List.hd hl)).expr_clock) in

  Log.report ~level:4 (fun fmt -> Format.fprintf fmt "Clock of expr %a: %a@ "

                          Printers.pp_expr expr Clocks.print_ck resulting_ck);

  let expr_lhs = expr_of_expr_list eq.eq_loc

      (List.map (fun v -> expr_of_ident v eq.eq_loc) eq.eq_lhs) in

    declaration [cck] *)

  | Ckdec_any -> new_var scoped

      let temp_env = Env.add_value env id (new_var true) in

      (* We just want the id to be present in the environment *)

      let dummy_id_expr = expr_of_ident id loc in

      let when_expr =

        List.fold_left

          (fun expr (x,l) ->

                {expr_tag = new_tag ();

                 expr_desc = Expr_when (expr,x,l);

                 expr_type = Types.new_var ();

                 expr_clock = new_var scoped;

                 expr_delay = Delay.new_var ();

                 expr_loc = loc;

		 expr_annot = None})

          dummy_id_expr cl

      in

      clock_expr temp_env when_expr

  let ck = clock_coreclock env vdecl.var_dec_clock vdecl.var_id vdecl.var_loc scoped in

(* WTF ????

    if vdecl.var_dec_const

    then

      (try_generalize ck vdecl.var_loc; ck)

    else

 *)

      if Types.get_clock_base_type vdecl.var_type <> None

      then new_ck (Ccarrying (new_carrier Carry_name scoped, ck)) scoped

      else ck in

  (if vdecl.var_dec_const

   then match vdecl.var_dec_value with

   | None   -> ()

     begin

       let ck_static = clock_expr env v in

       try_unify ck ck_static v.expr_loc

     end);

(** [clock_node env nd] performs the clock-calculus for node [nd] in

    environment [env].

    Generalization of clocks wrt scopes follows this rule:

    - generalize inputs (unscoped).

    - generalize outputs. As they are scoped, only clocks coming from inputs

      are allowed to be generalized.

    - generalize locals. As outputs don't depend on them (checked the step before),

      they can be generalized. 

 *)

  let eqs, _ = get_node_eqs nd in (* TODO XXX: perform the clocking on auts.

					For the moment, it is ignored *)

  Log.report ~level:3 (fun fmt -> Format.fprintf fmt "Clock of %s: %a@ " nd.node_id print_ck ck_node);

  (* Local variables may contain first-order carrier variables that should be generalized.

     That's not the case for types. *)

  (*

    List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_inputs;

    List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_outputs;*)

  (*List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_locals;*)

  (*  if (is_main && is_polymorphic ck_node) then

      raise (Error (loc,(Cannot_be_polymorphic ck_node)));

  *)

  Log.report ~level:3 (fun fmt -> Format.fprintf fmt "Generalized clock of %s: %a@ @ " nd.node_id print_ck ck_node);

    | Carrow (ck1,ck2) -> aux ck1; aux ck2

    | Ctuple cl -> List.iter aux cl

    | Con (ck',_,_) -> aux ck'

    | Clink ck' -> aux ck'

    | Ccarrying (_,ck') -> aux ck'

    | Cvar | Cunivar  ->

        match !pck with

        | None -> ()

        | Some (_,_) ->

            raise (Error (loc, (Invalid_imported_clock ck_node)))

  ignore(clock_var_decl_list new_env false nd.nodei_outputs);

  let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in

let clock_top_const env cdecl=

let clock_top_consts env clist =

  List.fold_left clock_top_const env clist

  | TypeDef _ -> List.fold_left clock_top_decl env (consts_of_enum_type decl)

  | Include _ | Open _    -> env

let clock_prog env decls =

  List.fold_left clock_top_decl env decls

(* Once the Lustre program is fully clocked,

   we must get back to the original description of clocks,

   with constant parameters, instead of unifiable internal variables. *)

(* The following functions aims at 'unevaluating' carriers occuring in clock expressions,

   i.e. replacing unifiable second_order variables with the original carrier names.

   Once restored in this formulation, clocks may be meaningfully printed.

*)

 (*Format.eprintf "Clock_calculus.uneval_vdecl_generics %a@." Printers.pp_node_var vdecl;*)

 if Types.get_clock_base_type vdecl.var_type <> None

 then

   match get_carrier_name vdecl.var_clock with

   | None    -> (Format.eprintf "internal error: %a@." print_ck vdecl.var_clock; assert false)

   | Some cr -> Clocks.uneval vdecl.var_id cr

let uneval_node_generics vdecls =

  List.iter uneval_vdecl_generics vdecls

      (* A node could contain first-order carrier variable in local vars. This is not the case for types. *)

      uneval_node_generics (nd.node_inputs @ nd.node_locals @ nd.node_outputs)

      uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)

  | Const _

  | Include _ | Open _

  | TypeDef _ -> ()

let uneval_prog_generics prog =

 List.iter uneval_top_generics prog

        let computed_c = instantiate (ref []) (ref []) (Env.lookup_value computed k) in

      with Not_found -> (* If the lookup failed then either an actual

                           required element should have been declared

                           and is missing but typing should have catch

                           it, or it was a contract and does not

                           require this additional check.  *)

          ()

    )