structural clock calculus tested and produces code for automata

.gitignore

 _build
+limusync
+.*.bak

Makefile

+all: limusync
+
+limusync:
+	dune build src/bin/$@.exe
+	cp _build/default/src/bin/$@.exe $@
+
+doc:
+	dune build @doc
+
+install: all
+	dune build @install
+	dune install
+
+clean:
+	dune clean
+	rm ./limusync
+
+tests: all
+	dune runtest -f
+
+.PHONY: all limusync doc install clean tests

dune-project

+(lang dune 2.7)
+(cram enable)
+
+(name limusyn)
+(version 0.0.1)
+(using menhir 2.0)

src/bin/dune

+(executables
+  (names limusync)
+  (public_names limusync)
+  (libraries limusyn)
+  (flags (:standard "-g")))
\ No newline at end of file

src/bin/limusync.ml

+open Limusyn
+
+exception Done
+
+let node = ref ""
+
+type process =
+  | All
+  | PrintFlat
+  | PrintAnf
+  | PrintTyped
+  | PrintSClocked
+  | PrintRClocked
+
+let process : process ref  = ref All
+
+let set_process s =
+  match s with
+  | "print_flat" -> process := PrintFlat
+  | "print_anf" -> process := PrintAnf
+  | "print_typed" -> process := PrintTyped
+  | "print_sclocked" -> process := PrintSClocked
+  | "print_rclocked" -> process := PrintRClocked
+  | _ -> () (* unreachable *)
+
+let usage = "Usage: limusync [options] -node <node> <source-file>"
+
+let options : (string * Arg.spec * string) list =
+  [
+    "-node", Arg.Set_string node, "Set main node";
+    "-process", Arg.Symbol (["print_flat";"print_anf";"print_typed";"print_sclocked";"print_rclocked"], set_process), "Set processing mode";
+    "-vdebug", Arg.Set Print.print_vdebug, "Print verbose debug messages"
+  ]
+
+let compile file =
+  let main_node = !node in
+  let prog = Parse.parse file in
+  let prog = Flatlang.Make.of_parsed prog in
+  if !process = PrintFlat then
+    begin
+      Format.printf "%a" Flatlang.PP.prog prog;
+      raise Done
+    end;
+  let prog = Anflang.Make.of_flat prog in
+  if !process = PrintAnf then
+    begin
+      Format.printf "%a" Anflang.PP.prog prog;
+      raise Done;
+    end;
+  let prog = Typedlang.Make.of_anf main_node prog in
+  if !process = PrintTyped then
+    begin
+      Format.printf "%a" Typedlang.PP.prog prog;
+      raise Done
+    end;
+  let prog = Sclockedlang.Make.of_typed main_node prog in
+  if !process = PrintSClocked then
+    begin
+      Format.printf "%a" Sclockedlang.PP.prog prog;
+      raise Done;
+    end;
+  let prog = Rclockedlang.Make.of_sclocked main_node prog in
+  if !process = PrintRClocked then
+    begin
+      Format.printf "%a" Rclockedlang.PP.prog prog;
+      raise Done;
+    end
+
+let try_compile file =
+  match compile file with
+  | () -> ()
+  | exception Done -> Format.fprintf Format.std_formatter "@."
+
+let anonymous file =
+  if Filename.check_suffix file ".plu" then
+    try_compile file
+  else
+    raise (Arg.Bad ("Can only compile *.plu files"))
+
+let () =
+  Arg.parse options anonymous usage

src/limusynlib/common.ml

+module StringMap = Map.Make(String)
+module IntMap = Map.Make(Int)
+
+module StringSet = Set.Make(String)
+
+let string_sub =
+  fun base sub ->
+  if String.length sub > String.length base then
+    false
+  else
+    let base_sub = String.sub base 0 (String.length base) in
+    String.equal base_sub sub
+
+let list_transpose =
+  fun m ->
+  let inner_len = List.length (List.hd m) in
+  let start = List.init inner_len (fun _ -> []) in
+  let step =
+    List.fold_left
+      (fun acc l ->
+         List.map2
+           (fun acc x -> x::acc)
+           acc l)
+      start m
+  in
+  List.map List.rev step

src/limusynlib/dune

+(library
+  (name limusyn)
+  (libraries menhirLib)
+  (flags (:standard "-g")))
+
+(ocamllex
+  (modules lexer))
+
+(menhir
+  (modules tokens)
+  (flags --only-tokens))
+
+(menhir
+  (modules tokens parser)
+  (merge_into parser)
+  (flags
+    --external-tokens Tokens
+    --table
+    --explain))
\ No newline at end of file

src/limusynlib/env.ml

+(** Generic inference environments *)
+
+module type S =
+sig
+  type key
+
+  type 'a t
+
+  module Map : Map.S
+
+  val empty: 'a t
+
+  val add: key -> 'a -> 'a t -> 'a t
+
+  val curr: 'a t -> 'a Map.t
+
+  val rollback_until: key -> 'a t -> 'a t
+
+  val iter_from_list: ('a t -> 'b -> ((key * 'a) list)) -> 'b list -> 'a t -> unit
+
+  val at_point: ('a t -> 'b -> (key * 'a) list) -> ('a -> 'a t -> 'c) -> key -> 'b list -> 'a t -> 'c
+
+  val st_map: ('a t -> 'b -> 'c -> ((key * 'a) list * 'b * 'd)) -> 'a t -> 'b -> 'c list -> 'd list
+end
+
+module Make (Key: Map.OrderedType) = struct
+  type key = Key.t
+
+  module Map = Map.Make(Key)
+
+  type 'a t = {
+    current: 'a Map.t;
+    histories: (key * ('a Map.t)) list;
+  }
+
+  exception Shadow of key
+
+  let empty = {current = Map.empty; histories = []}
+
+  let add k v env =
+    if List.mem k (List.map fst env.histories) then
+      raise (Shadow k)
+    else
+      {current = Map.add k v env.current; histories = (k,env.current)::env.histories}
+
+  let curr env = env.current
+
+  let rollback_until k env =
+    let rec aux k histories =
+      match histories with
+      | (x,e)::envs when x=k -> {current = e; histories = envs}
+      | _::envs -> aux k envs
+      | [] -> raise Not_found
+    in
+    aux k env.histories
+
+  let iter_from_list f l env =
+    let rec aux f l env =
+      match l with
+      | [] -> ()
+      | x::xs ->
+        let kvs = f env x in
+        let env = List.fold_left
+            (fun acc (k,v) -> add k v acc) env kvs
+        in
+        aux f xs env
+    in
+    aux f l env
+
+  let at_point fenv fpoint k l env =
+    let rec aux fenv fpoint k l env =
+      match l with
+      | [] -> raise Not_found
+      | x::xs ->
+        let kvs = fenv env x in
+        match List.assoc_opt k kvs with
+        | Some v -> fpoint v env
+        | None ->
+          let map = List.fold_left
+              (fun acc (k,v) -> add k v acc) env kvs
+          in
+          aux fenv fpoint k xs map
+    in
+    aux fenv fpoint k l env
+
+  let st_map =
+    let rec aux f env st l acc =
+      match l with
+      | [] -> List.rev acc
+      | x::xs ->
+        let kvs,st,mapped = f env st x in
+        let env = List.fold_left (fun acc (k,v) -> add k v acc) env kvs in
+        aux f env st xs (mapped::acc)
+    in
+    fun f env st l ->
+      aux f env st l []
+
+end
+
+module String = Make(String)

src/limusynlib/env.mli

+module type S =
+sig
+  type key
+
+  type 'a t
+
+  module Map : Map.S
+
+  val empty: 'a t
+
+  val add: key -> 'a -> 'a t -> 'a t
+
+  val curr: 'a t -> 'a Map.t
+
+  val rollback_until: key -> 'a t -> 'a t
+
+  val iter_from_list: ('a t -> 'b -> ((key * 'a) list)) -> 'b list -> 'a t -> unit
+
+  val at_point: ('a t -> 'b -> (key * 'a) list) -> ('a -> 'a t -> 'c) -> key -> 'b list -> 'a t -> 'c
+
+  val st_map: ('a t -> 'b -> 'c -> ((key * 'a) list * 'b * 'd)) -> 'a t -> 'b -> 'c list -> 'd list
+end
+
+module Make (Key: Map.OrderedType) : S with
+  type key = Key.t and type Map.key = Key.t
+
+module String : S with
+  type key = String.t and type Map.key = String.t

src/limusynlib/lexer.mll

+{
+open Tokens
+open Common
+
+
+let incr_line = MenhirLib.LexerUtil.newline
+
+let keywords =
+  [
+      "int", TINT;
+      "bool", TBOOL;
+      "char", TCHAR;
+      "float", TFLOAT;
+      "on", ON;
+      "var", VAR;
+      "end", END;
+      "node", NODE;
+      "returns", RETURNS;
+      "let", LET;
+      "tel", TEL;
+      "due", DUE;
+      "fby", FBY;
+      "when", WHEN;
+      "merge", MERGE;
+      "automaton", AUTOMATON;
+      "then", THEN;
+      "unless", UNLESS;
+      "until", UNTIL;
+      "rate", RATE;
+  ]
+  |> List.to_seq
+  |> StringMap.of_seq
+
+let try_keyword s =
+  match StringMap.find_opt s keywords with
+  | Some k -> k
+  | None -> IDENT s
+
+
+let ops =
+  [
+    "*^", PCKUP;
+    ":", COL;
+    ",", COMMA;
+    ";", SCOL;
+    "=", EQ;
+    "|", PIPE;
+    "->", ARROW;
+  ]
+  |> List.to_seq
+  |> StringMap.of_seq
+
+  let try_op s =
+    match StringMap.find_opt s ops with
+    | Some op -> op
+    | None -> failwith (Format.asprintf "unknown operator ``%s''" s)
+
+}
+
+let newline = ('\010' | '\013' | "\013\010")
+let blank = [' ' '\009' '\012']
+let ident = ['_' 'A'-'Z' 'a'-'z']['_' 'A'-'Z' 'a'-'z' '0'-'9']*
+let dec = ['0'-'9']+
+let fp = ['0'-'9'] '.' ['0'-'9']*
+let op = ['*' '^' ':' ',' ';' '=' '|' '-' '>']+
+
+rule token = parse
+| "--" [^ '\n']* ['\n']
+  { incr_line lexbuf;
+    token lexbuf }
+| "--" [^ '\n']* eof
+  { token lexbuf }
+| newline
+  { incr_line lexbuf;
+    token lexbuf }
+| blank +
+  {token lexbuf}
+| "(" { LPAR }
+| ")" { RPAR }
+| "[" { LBRACK }
+| "]" { RBRACK }
+| ident as s { try_keyword s }
+| dec as s { INT (int_of_string s) }
+| op as s { try_op s }
+| eof { EOF }
+| _ as c { failwith (Format.asprintf "Unknown token: ``%c''" c) }

src/limusynlib/location.ml

+type t = Lexing.position * Lexing.position
+
+let dummy = Lexing.dummy_pos, Lexing.dummy_pos

src/limusynlib/parse.ml

+module LexerUtil = MenhirLib.LexerUtil
+
+module E = MenhirLib.ErrorReports
+module I = Parser.MenhirInterpreter
+
+let parse =
+  let succeed prog =
+    prog
+  in
+  let fail lexbuf _checkpoint =
+    failwith
+      (Format.asprintf "Parse error at %s"
+         (LexerUtil.range
+            (Lexing.lexeme_start_p lexbuf,
+            (Lexing.lexeme_end_p lexbuf))))
+  in
+  let loop lexbuf result =
+    let supplier = I.lexer_lexbuf_to_supplier Lexer.token lexbuf in
+    I.loop_handle succeed (fail lexbuf) supplier result
+  in
+  fun file ->
+  let lexbuf =
+    LexerUtil.init
+      file
+      (Lexing.from_channel (open_in file))
+  in
+  loop lexbuf (Parser.Incremental.prog lexbuf.lex_curr_p)

src/limusynlib/parsedlang.ml

+open Common
+
+type prog = top_decl list
+
+and top_decl =
+  {
+    top_decl_desc: top_decl_desc;
+    top_decl_loc: Location.t;
+  }
+
+and top_decl_desc =
+  | Node of node_desc
+  | EnumDecl of enum_desc
+
+and node_desc =
+  {
+    node_name: String.t;
+    node_inputs: vdecl list;
+    node_outputs: vdecl list;
+    node_locals: vdecl list;
+    node_defs: def list;
+  }
+
+and enum_desc = String.t * StringSet.t
+
+and def =
+  {
+    def_desc: def_desc;
+    def_loc: Location.t;
+  }
+
+and def_desc =
+  | Eq of eq_desc
+  | Automaton of auto_desc
+
+and eq_desc = {eq_lhs: String.t list; eq_rhs: expr}
+
+and auto_desc = {states: state list}
+
+and 'desc expr_base =
+  {
+    expr_desc: 'desc;
+    expr_loc: Location.t
+  }
+
+and expr = expr_desc expr_base
+
+and atom_expr = atom_expr_desc expr_base
+
+and ident_expr = ident_expr_desc expr_base
+
+and state =
+  {
+    state_name: String.t;
+    state_strong_trans: trans list;
+    state_defs: eq_desc list;
+    state_weak_trans: trans list;
+    state_loc: Location.t;
+  }
+
+and trans =
+  {
+    trans_cond: expr;
+    trans_state: String.t;
+  }
+
+and expr_desc =
+  [
+    | `ExprAtom of atom
+    | `ExprApply of ident_expr * expr list
+    | `ExprPckUp of rate_op_desc
+    | `ExprFby of atom_expr * rate_op_desc
+    | `ExprWhen of when_desc
+    | `ExprMerge of merge_desc
+  ]
+
+and atom_expr_desc =
+  [
+    | `ExprAtom of atom
+  ]
+
+and ident_expr_desc =
+  [
+    | `ExprAtom of ident_desc
+  ]
+
+and vdecl =
+  {
+    vdecl_name: String.t;
+    vdecl_ty_decl: Types.decl;
+    vdecl_ck_decl: Structclocks.decl;
+    vdecl_dl: Int.t Option.t;
+  }
+
+and atom =
+  [
+    | `AtomInt of Int.t
+    | `AtomChar of Char.t
+    | `AtomBool of Bool.t
+    | `AtomFloat of Float.t
+    | `AtomIdent of String.t
+  ]
+
+and ident_desc =
+  [
+    | `AtomIdent of String.t
+  ]
+
+and rate_op_desc = {rate_expr: expr; rate_factor: Int.t}
+
+and when_desc = {when_expr: expr; case: String.t; cond_expr: ident_expr;}
+
+and merge_desc = {merge_var: ident_expr; merge_exprs: (String.t*expr) list}
+
+let init_prog =
+  [
+    {
+      top_decl_desc=EnumDecl ("bool",StringSet.of_list ["false"; "true"]);
+      top_decl_loc=Location.dummy
+    }
+  ]

src/limusynlib/parser.mly

+%{
+  open Parsedlang
+
+  let mk_node_decl node_name node_inputs node_outputs node_locals node_defs top_decl_loc =
+    {
+      top_decl_desc =
+        Node
+          {
+            node_name;
+            node_inputs;
+            node_outputs;
+            node_locals;
+            node_defs;
+          };
+      top_decl_loc;
+    }
+
+  let mk_def def_desc def_loc = { def_desc; def_loc }
+
+  let mk_eq eq_lhs eq_rhs = {eq_lhs; eq_rhs}
+
+  let mk_expr: 'a -> _ -> 'a expr_base =
+        fun expr_desc expr_loc -> {expr_desc; expr_loc}
+
+  let mk_state state_name state_strong_trans state_defs state_weak_trans state_loc =
+    {state_name; state_strong_trans; state_defs; state_weak_trans; state_loc}
+%}
+
+%start prog
+%type <top_decl list> prog
+
+%%
+
+let prog := decls=list(top_decl); EOF; { init_prog @ decls}
+
+let top_decl :=
+  | NODE; id=IDENT;
+    LPAR; inputs=node_vdecls; RPAR;
+    RETURNS; LPAR; outputs=node_vdecls; RPAR;
+     ~=locals;
+    LET; ~=defs; TEL;
+    {mk_node_decl id inputs outputs locals defs $loc}
+
+let node_vdecls :=
+  | ~=flatten(separated_nonempty_list(SCOL, node_vdecl)); <>
+
+let locals :=
+  | locs=option(preceded(VAR, local_vdecls)); {Option.value locs ~default:[]}
+
+let local_vdecls :=
+  | ~=flatten(nonempty_list(terminated(node_vdecl, SCOL))); <>
+
+let defs := ~=nonempty_list(def); <>
+
+let eqs := ~=nonempty_list(eq); <>
+
+let def :=
+  | ~=eq; {mk_def (Eq eq) $loc}
+  | ~=automaton; {mk_def (Automaton automaton) $loc}
+
+let eq :=
+  | ids=ident_list; EQ; e=expr; SCOL; {mk_eq ids e}
+
+let automaton :=
+  | AUTOMATON; states=nonempty_list(auto_state); END; {{states}}
+
+let auto_state :=
+  | PIPE; name=IDENT; ARROW;
+    strong_trans=list(strong_trans);
+    ~=eqs;
+    weak_trans=list(weak_trans);
+    {mk_state name strong_trans eqs weak_trans $loc}
+
+let strong_trans :=
+  UNLESS; trans_cond=expr; THEN; trans_state=IDENT; SCOL; {{trans_cond;trans_state}}
+
+let weak_trans :=
+  UNTIL; trans_cond=expr; THEN; trans_state=IDENT; SCOL; {{trans_cond;trans_state}}
+
+let expr := ~=l2_expr; <>
+
+let l2_expr :=
+  | rate_expr=l2_expr; PCKUP; rate_factor=INT;
+    {mk_expr (`ExprPckUp {rate_expr;rate_factor}) $loc}
+  | when_expr=l2_expr; WHEN; case=IDENT; LPAR; cond_expr=ident_expr; RPAR;
+    {mk_expr (`ExprWhen {when_expr;case;cond_expr}) $loc}
+  | ~=l1_expr; <>
+
+let l1_expr :=
+/* fby, concat, tail */
+  | ~=atom_expr; FBY; rate_expr=l1_expr;
+    {mk_expr (`ExprFby (atom_expr,{rate_expr;rate_factor=1})) $loc}
+  | ~=l0_expr; <>
+
+let l0_expr :=
+  | ~=atom_expr; {(atom_expr :> Parsedlang.expr)}
+  | f=ident_expr; LPAR; args=separated_nonempty_list(COMMA, expr); RPAR;
+    {mk_expr (`ExprApply (f,args)) $loc}
+  | MERGE; LPAR; merge_var=ident_expr; COMMA; merge_exprs=separated_nonempty_list(COMMA, merge_fragment); RPAR;
+    {mk_expr (`ExprMerge {merge_var;merge_exprs}) $loc}
+  | LPAR; ~=expr; RPAR; <>
+
+let atom :=
+  | a=INT; {`AtomInt a}
+  | a=IDENT; {`AtomIdent a}
+  | a=CHAR; {`AtomChar a}
+
+let ident_expr :=
+  | a=IDENT; {mk_expr (`ExprAtom (`AtomIdent a)) $loc}
+
+let atom_expr :=
+  | ~=atom; {mk_expr (`ExprAtom atom) $loc}
+
+let merge_fragment :=
+  | ~=IDENT; ARROW; ~=expr; <>
+
+let node_vdecl :=
+  | ids=ident_list; spec=opt_vdecl_spec;
+    {
+      let vdecl_ty_decl,vdecl_ck_decl,vdecl_dl = spec in
+      List.map
+        (fun v ->
+          {vdecl_name=v;
+           vdecl_ty_decl;
+           vdecl_ck_decl;
+           vdecl_dl})
+        ids
+    }
+
+let opt_vdecl_spec :=
+  | x=option(preceded(COL, vdecl_spec));
+    {Option.value x ~default:(Types.DeclAny,Structclocks.DeclAny,None)}
+
+let vdecl_spec :=
+  | ty=typ; ckdl=opt_ckdl; {let ck,dl = ckdl in ty,ck,dl}
+  | ckdl=obl_ckdl; {let ck,dl = ckdl in Types.DeclAny,ck,dl}
+
+let opt_ckdl :=
+  | ~=ck; dl=opt_dl; {ck,dl}
+  | dl=opt_dl; {Structclocks.DeclAny,dl}
+
+let obl_ckdl :=
+  | ~=ck; dl=opt_dl; {ck,dl}
+  | dl=obl_dl; {Structclocks.DeclAny,dl}
+
+let opt_dl :=
+  | ~=dl; {Some dl}
+  | {None}
+
+let obl_dl :=
+  | ~=dl; {Some dl}
+
+let dl := DUE; i=INT; {i}
+
+let typ :=
+  | TINT; {Types.Decl Types.Int}
+  | TCHAR; {Types.Decl Types.Char}
+  | id=IDENT; {Types.Decl (Types.Usertype id)}
+  | TFLOAT; {Types.Decl Types.Float}
+  | TBOOL; {Types.Decl Types.Bool}
+  | t=typ; LBRACK; i=INT; RBRACK; {Types.Decl (Types.Array (t,i))}
+
+let ck :=
+  | RATE; ~=pck; {Structclocks.Decl (Pck pck)}
+  | decl=ck; ON; decl_case=IDENT; decl_cond=IDENT; {Structclocks.Decl (On {decl;decl_case;decl_cond})}
+
+let pck := LPAR; period=INT; COMMA; offset=INT; RPAR; {{Structclocks.period;offset}}
+
+let ident_list == ~=separated_nonempty_list(COMMA,IDENT); <>

src/limusynlib/print.ml

+let list =
+  let rec aux mid_fmt end_fmt pp ff l =
+    match l with
+    | [] ->
+      Format.fprintf ff end_fmt
+    | x::xs ->
+      Format.fprintf ff mid_fmt;
+      Format.fprintf ff "%a" pp x;
+      aux mid_fmt end_fmt pp ff xs
+  in
+  fun beg_fmt mid_fmt end_fmt pp ff l ->
+  match l with
+  | [] -> ()
+  | [x] ->
+    Format.fprintf ff beg_fmt;
+    Format.fprintf ff "%a" pp x;
+    Format.fprintf ff end_fmt
+  | x::xs ->
+    Format.fprintf ff beg_fmt;
+    Format.fprintf ff "%a" pp x;
+    aux mid_fmt end_fmt pp ff xs
+
+let seq =
+  let rec aux mid_fmt end_fmt pp ff (n: _ Seq.node) =
+    match n with
+    | Nil -> Format.fprintf ff end_fmt
+    | Cons (x,s) ->
+      Format.fprintf ff mid_fmt;
+      Format.fprintf ff "%a" pp x;
+      aux mid_fmt end_fmt pp ff (s ())
+  in
+  fun beg_fmt mid_fmt end_fmt pp ff (s: _ Seq.t) ->
+  match s () with
+  | Nil -> ()
+  | Cons (x,s) ->
+    Format.fprintf ff beg_fmt;
+    Format.fprintf ff "%a" pp x;
+    aux mid_fmt end_fmt pp ff (s ())
+
+let int_map =
+  fun beg_fmt mid_fmt end_fmt pp ff (m: _ Common.IntMap.t) ->
+  seq beg_fmt mid_fmt end_fmt pp ff (Common.IntMap.to_seq m)
+
+let option =
+  fun pp_some none_fmt ff o ->
+  match o with
+  | Some x -> Format.fprintf ff "%a" pp_some x
+  | None -> Format.fprintf ff none_fmt
+
+let post =
+  fun fmt pp ff x ->
+  Format.fprintf ff fmt pp x
+
+let print_vdebug = ref false
+
+let vdebug : ('a, Format.formatter, unit) format -> 'a =
+  fun x ->
+  if !print_vdebug then
+    Format.eprintf x
+  else
+    Format.ifprintf Format.err_formatter x