add option -lem_sequential for producing shallow embedding that refers to state monad, library fixes

8 files changed, 116 insertions, 58 deletions

diff --git a/src/Makefile b/src/Makefile
index 8af30456..7d255cfa 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -25,9 +25,17 @@ LEMLIBOCAML = $(BITBUCKET_ROOT)/lem/ocaml-lib
 ELFDIR= $(BITBUCKET_ROOT)/linksem
 
 MIPS_SAIL_DIR:=$(BITBUCKET_ROOT)/sail/mips
-MIPS_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail $(BITBUCKET_ROOT)/sail/etc/regfp.sail $(MIPS_SAIL_DIR)/mips_regfp.sail
-MIPS_NOTLB_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb_stub.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail $(BITBUCKET_ROOT)/sail/etc/regfp.sail $(MIPS_SAIL_DIR)/mips_regfp.sail
+
+MIPS_SAILS_PRE:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
+
+MIPS_SAILS:=$(MIPS_SAILS) $(BITBUCKET_ROOT)/sail/etc/regfp.sail $(MIPS_SAIL_DIR)/mips_regfp.sail
+
+MIPS_NOTLB_SAILS_PRE:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb_stub.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
+
+MIPS_NOTLB_SAILS:=$(MIPS_NOTLB_SAILS_PRE) $(BITBUCKET_ROOT)/sail/etc/regfp.sail $(MIPS_SAIL_DIR)/mips_regfp.sail
+
 CHERI_SAIL_DIR:=$(BITBUCKET_ROOT)/sail/cheri
+
 CHERI_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_prelude.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
 
 elf:
@@ -54,6 +62,11 @@ _build/mips_embedded.lem: $(MIPS_SAILS) ./sail.native
 	cd _build ;\
 	../sail.native -lem_lib "Mips_extras_embed" -lem -o mips $(MIPS_NOTLB_SAILS)
 
+_build/mips_sequential_embedded.lem: $(MIPS_SAILS) ./sail.native
+	mkdir -p _build
+	cd _build ;\
+	../sail.native -lem_lib "Mips_extras_sequential_embed" -lem_sequential -o mips $(MIPS_NOTLB_SAILS)
+
 _build/mips_notlb.lem: $(MIPS_NOTLB_SAILS) ./sail.native
 	mkdir -p _build
 	cd _build ; \
@@ -85,7 +98,7 @@ run_mips.native: _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml int
 run_cheri.native:  _build/cheri.ml _build/mips_extras.ml _build/run_with_elf_cheri.ml interpreter
 	env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(LEMLIBOCAML)/dependencies/zarith -I _build/lem_interp/ -I $(ELFDIR)/src  -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(LEMLIBOCAML)/dependencies/zarith/zarith.cmxa $(LEMLIBOCAML)/extract.cmxa $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa  _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/cheri.ml _build/mips_extras.ml _build/run_with_elf_cheri.ml  -o run_cheri.native
 
-mips_notlb: _build/mips_notlb.ml  _build/mips_embedded.lem _build/mips_extras.ml
+mips_notlb: _build/mips_notlb.ml  _build/mips_embedded.lem _build/mips_sequential_embedded.lem _build/mips_extras.ml
 	true
 
 mips: elf run_mips.native
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 4018fd54..5532089d 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -40,7 +40,7 @@ let read_mem endian dir rk addr sz =
   let addr = address_lifted_of_bitv addr in
   let sz = natFromInteger sz in
   let k memory_value =
-    let bitv = intern_mem_value endian dir memory_value in
+    let bitv = internal_mem_value endian dir memory_value in
     (Done bitv,Nothing) in
   Read_mem (rk,addr,sz) k
 
@@ -52,49 +52,49 @@ let write_mem_ea wk addr sz =
 
 val write_mem_val : end_flag -> vector bitU -> M bool
 let write_mem_val endian v =
-  let v = extern_mem_value endian v in
+  let v = external_mem_value endian v in
   let k successful = (return successful,Nothing) in
   Write_memv v k
 
 val read_reg_aux : reg_name -> M (vector bitU)
 let read_reg_aux reg = 
   let k reg_value =
-    let v = intern_reg_value reg_value in
+    let v = internal_reg_value reg_value in
     (Done v,Nothing) in
   Read_reg reg k
 
 let read_reg reg =
-  read_reg_aux (extern_reg_whole reg)
+  read_reg_aux (external_reg_whole reg)
 let read_reg_range reg i j =
-  read_reg_aux (extern_reg_slice reg (natFromInteger i,natFromInteger j))
+  read_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger j))
 let read_reg_bit reg i =
-  read_reg_aux (extern_reg_slice reg (natFromInteger i,natFromInteger i)) >>= fun v ->
+  read_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger i)) >>= fun v ->
   return (extract_only_bit v)
 let read_reg_field reg regfield =
-  read_reg_aux (extern_reg_field_whole reg regfield)
+  read_reg_aux (external_reg_field_whole reg regfield)
 let read_reg_bitfield reg regfield =
-  read_reg_aux (extern_reg_field_whole reg regfield) >>= fun v ->
+  read_reg_aux (external_reg_field_whole reg regfield) >>= fun v ->
   return (extract_only_bit v)
 
 val write_reg_aux : reg_name -> vector bitU -> M unit
 let write_reg_aux reg_name v =
-  let regval = extern_reg_value reg_name v in
+  let regval = external_reg_value reg_name v in
   Write_reg (reg_name,regval) (Done (), Nothing)
 
 let write_reg reg v =
-  write_reg_aux (extern_reg_whole reg) v
+  write_reg_aux (external_reg_whole reg) v
 let write_reg_range reg i j v =
-  write_reg_aux (extern_reg_slice reg (natFromInteger i,natFromInteger j)) v
+  write_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger j)) v
 let write_reg_bit reg i bit =
   let iN = natFromInteger i in
-  write_reg_aux (extern_reg_slice reg (iN,iN)) (Vector [bit] i (is_inc_of_reg reg))
+  write_reg_aux (external_reg_slice reg (iN,iN)) (Vector [bit] i (is_inc_of_reg reg))
 let write_reg_field reg regfield v =
-  write_reg_aux (extern_reg_field_whole reg regfield) v
+  write_reg_aux (external_reg_field_whole reg regfield) v
 let write_reg_bitfield reg regfield bit =
-  write_reg_aux (extern_reg_field_whole reg regfield)
+  write_reg_aux (external_reg_field_whole reg regfield)
                 (Vector [bit] 0 (is_inc_of_reg reg))
 let write_reg_field_range reg regfield i j v =
-  write_reg_aux (extern_reg_field_slice reg regfield (natFromInteger i,natFromInteger j)) v
+  write_reg_aux (external_reg_field_slice reg regfield (natFromInteger i,natFromInteger j)) v
 
 
 
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 2b270e65..2ad25110 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -33,7 +33,7 @@ instance (Show bitU)
 end
 
 
-let to_bool = function
+let bitU_to_bool = function
   | O -> false
   | I  -> true
   | Undef -> failwith "to_bool applied to Undef"
@@ -75,12 +75,12 @@ val is_one : integer -> bitU
 let is_one i =
   if i = 1 then I else O
 
-let bool_to_bit b = if b then I else O
+let bool_to_bitU b = if b then I else O
 
 let bitwise_binop_bit op = function
   | (Undef,_) -> Undef (*Do we want to do this or to respect | of I and & of B0 rules?*)
   | (_,Undef) -> Undef (*Do we want to do this or to respect | of I and & of B0 rules?*)
-  | (x,y) -> bool_to_bit (op (to_bool x) (to_bool y))
+  | (x,y) -> bool_to_bitU (op (bitU_to_bool x) (bitU_to_bool y))
   end
 
 val bitwise_and_bit : bitU * bitU -> bitU
@@ -595,7 +595,7 @@ let duplicate bit length =
   Vector (repeat [bit] length) (if dir then 0 else length - 1) dir
  *)
 
-let compare_op op (l,r) = bool_to_bit (op l r)
+let compare_op op (l,r) = bool_to_bitU (op l r)
 
 let lt = compare_op (<)
 let gt = compare_op (>)
@@ -637,10 +637,10 @@ let gt_range_vec = compare_op_range_vec (>) true
 let lteq_range_vec = compare_op_range_vec (<=) true
 let gteq_range_vec = compare_op_range_vec (>=) true
 
-let eq (l,r) = bool_to_bit (l = r)
-let eq_range (l,r) = bool_to_bit (l = r)
-let eq_vec (l,r) = bool_to_bit (l = r)
-let eq_bit (l,r) = bool_to_bit (l = r)
+let eq (l,r) = bool_to_bitU (l = r)
+let eq_range (l,r) = bool_to_bitU (l = r)
+let eq_vec (l,r) = bool_to_bitU (l = r)
+let eq_bit (l,r) = bool_to_bitU (l = r)
 let eq_vec_range (l,r) = eq (to_num false l,r)
 let eq_range_vec (l,r) = eq (l, to_num false r)
 let eq_vec_vec (l,r) = eq (to_num true l, to_num true r)
@@ -793,7 +793,7 @@ let register_field_indices_nat reg regfield=
   let (i,j) = register_field_indices reg regfield in
   (natFromInteger i,natFromInteger j)
 
-let rec extern_reg_value reg_name v = 
+let rec external_reg_value reg_name v = 
   let (internal_start, external_start, direction) =
     match reg_name with 
      | Reg _ start size dir ->
@@ -814,14 +814,14 @@ let rec extern_reg_value reg_name v =
      rv_start          = external_start;
      rv_start_internal = internal_start |>
 
-val intern_reg_value : register_value -> vector bitU
-let intern_reg_value v =
+val internal_reg_value : register_value -> vector bitU
+let internal_reg_value v =
   Vector (List.map bitU_of_bit_lifted v.rv_bits)
          (integerFromNat v.rv_start_internal)
          (v.rv_dir = D_increasing)
 
 
-let extern_slice (d:direction) (start:nat) ((i,j):(nat*nat)) =
+let external_slice (d:direction) (start:nat) ((i,j):(nat*nat)) =
   match d with
   (*This is the case the thread/concurrecny model expects, so no change needed*)
   | D_increasing -> (i,j)
@@ -830,33 +830,33 @@ let extern_slice (d:direction) (start:nat) ((i,j):(nat*nat)) =
                     (slice_i,slice_j)
   end 
 
-let extern_reg_whole reg =
+let external_reg_whole reg =
   Reg (name_of_reg reg) (start_of_reg_nat reg) (size_of_reg_nat reg) (dir_of_reg reg)
       
-let extern_reg_slice reg (i,j) =
+let external_reg_slice reg (i,j) =
   let start = start_of_reg_nat reg in
   let dir = dir_of_reg reg in
-  Reg_slice (name_of_reg reg) start dir (extern_slice dir start (i,j))
+  Reg_slice (name_of_reg reg) start dir (external_slice dir start (i,j))
 
-let extern_reg_field_whole reg rfield = 
+let external_reg_field_whole reg rfield = 
   let (m,n) = register_field_indices_nat reg rfield in
   let start = start_of_reg_nat reg in
   let dir = dir_of_reg reg in
-  Reg_field (name_of_reg reg) start dir rfield (extern_slice dir start (m,n))
+  Reg_field (name_of_reg reg) start dir rfield (external_slice dir start (m,n))
             
-let extern_reg_field_slice reg rfield (i,j) = 
+let external_reg_field_slice reg rfield (i,j) = 
   let (m,n) = register_field_indices_nat reg rfield in
   let start = start_of_reg_nat reg in
   let dir = dir_of_reg reg in
   Reg_f_slice (name_of_reg reg) start dir rfield
-              (extern_slice dir start (m,n))
-              (extern_slice dir start (i,j))
+              (external_slice dir start (m,n))
+              (external_slice dir start (i,j))
 
-let extern_mem_value endian v =
+let external_mem_value endian v =
   let bytes = byte_lifteds_of_bitv v in 
   if endian = E_big_endian then bytes else List.reverse bytes
 
-let intern_mem_value endian direction bytes = 
+let internal_mem_value endian direction bytes = 
   let v = if endian = E_big_endian then bytes else List.reverse bytes in
   bitv_of_byte_lifteds direction v
 
@@ -885,7 +885,7 @@ let assert' b msg_opt =
   | Just msg -> msg
   | Nothing  -> "unspecified error"
   end in
-  if to_bool b then () else failwith msg
+  if bitU_to_bool b then () else failwith msg
 
 
 
@@ -1441,16 +1441,16 @@ let regfp_to_reg (reg_info : string -> maybe string -> (nat * nat * direction *
      let i = natFromInteger i in
      let j = natFromInteger j in
      let (start,length,direction,_) = reg_info name Nothing in
-     let slice = extern_slice direction start (i,j) in
+     let slice = external_slice direction start (i,j) in
      Reg_slice name start direction slice
   | RSliceBit (name,i) ->
      let i = natFromInteger i in
      let (start,length,direction,_) = reg_info name Nothing in
-     let slice = extern_slice direction start (i,i) in
+     let slice = external_slice direction start (i,i) in
      Reg_slice name start direction slice
   | RField (name,field_name) ->
      let (start,length,direction,span) = reg_info name (Just field_name) in
-     let slice = extern_slice direction start span in
+     let slice = external_slice direction start span in
      Reg_field name start direction field_name slice
 end
 
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index da2decd6..98596b6d 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -8,23 +8,24 @@ type State 's 'a = 's -> (either 'a string * 's)
 type memstate = map integer memory_byte
 type regstate = map string (vector bitU)
 
-type state = <| regstate : regstate;
-                memstate : memstate; 
-                write_ea : integer * integer |>
+type sequential_state = <| regstate : regstate;
+                           memstate : memstate; 
+                           write_ea : maybe (integer * integer) |>
 
-type M 'a = State state 'a
+type M 'a = State sequential_state 'a
                      
 val return : forall 's 'a. 'a -> State 's 'a
 let return a s = (Left a,s)
 
-val (>>=) : forall 's 'a 'b. State 's 'a -> ('a -> State 's 'b) -> State 's 'b
-let (>>=) m f s = match m s with
+val bind : forall 's 'a 'b. State 's 'a -> ('a -> State 's 'b) -> State 's 'b
+let bind m f s = match m s with
   | (Left a,s') -> f a s'
   | (Right error,s') -> (Right error,s')
   end
 
+let inline (>>=) = bind
 val (>>): forall 's 'b. State 's unit -> State 's 'b -> State 's 'b
-let (>>) m n = m >>= fun _ -> n
+let inline (>>) m n = m >>= fun _ -> n
 
 val exit : forall 's 'e 'a. 'e -> State 's 'a
 let exit _ s = (Right "exit",s)
@@ -35,25 +36,45 @@ let rec range i j =
   if i = j then [i]
   else i :: range (i+1) j
 
+val get_reg : sequential_state -> string -> vector bitU
+let get_reg state reg = Map_extra.find reg state.regstate
+
+val set_reg : sequential_state -> string -> vector bitU -> sequential_state
+let set_reg state reg bitv =
+  <| state with regstate = Map.insert reg bitv state.regstate |>
+
+
 val read_mem : end_flag -> bool -> read_kind -> vector bitU -> integer -> M (vector bitU)
 let read_mem endian dir _ addr sz state =
   let addr = integer_of_address (address_of_bitv addr) in
   let addrs = range addr (addr+sz-1) in
   let memory_value = List.map (fun addr -> Map_extra.find addr state.memstate) addrs in
-  let value = intern_mem_value endian dir memory_value in
+  let value = Sail_values.internal_mem_value endian dir memory_value in
   (Left value,state)
 
+
+val write_mem_address_value : write_kind -> address -> integer -> end_flag -> vector bitU -> M bool
+let write_mem_address_value _ addr sz endian v state = 
+  let addr = integer_of_address addr in
+  let addrs = range addr (addr+sz-1) in
+  let v = external_mem_value endian v in
+  let addresses_with_value = List.zip addrs v in
+  let mem = List.foldl (fun mem (addr,v) -> Map.insert addr v mem)
+                       state.memstate addresses_with_value in
+  (Left true,<| state with memstate = mem |>)
+
 val write_mem_ea : write_kind -> vector bitU -> integer -> M unit
 let write_mem_ea _ addr sz state = 
   let addr = integer_of_address (address_of_bitv addr) in
-  let sz = sz in
-  (Left (), <| state with write_ea = (addr,sz) |>)
+  (Left (), <| state with write_ea = Just (addr,sz) |>)
 
 val write_mem_val : end_flag -> vector bitU -> M bool
 let write_mem_val endian v state =
-  let (addr,sz) = state.write_ea in
+  let (addr,sz) = match state.write_ea with
+    | Nothing -> failwith "write ea has not been announced yet"
+    | Just write_ea -> write_ea end in
   let addrs = range addr (addr+sz-1) in
-  let v = extern_mem_value endian v in
+  let v = external_mem_value endian v in
   let addresses_with_value = List.zip addrs v in
   let mem = List.foldl (fun mem (addr,v) -> Map.insert addr v mem)
                        state.memstate addresses_with_value in
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 88b19627..52e34a38 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -2318,7 +2318,7 @@ let doc_exp_lem, doc_let_lem =
     | E_if(c,t,e) ->
        let (E_aux (_,(_,cannot))) = c in
        let epp =
-         separate space [string "if";group (align (string "to_bool" ^//^ group (expY c)))] ^^
+         separate space [string "if";group (align (string "bitU_to_bool" ^//^ group (expY c)))] ^^
            break 1 ^^
              (prefix 2 1 (string "then") (expN t)) ^^ (break 1) ^^
                (prefix 2 1 (string "else") (expN e)) in
diff --git a/src/process_file.ml b/src/process_file.ml
index 3012b288..6270cb66 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -49,6 +49,7 @@ open Type_internal
 type out_type =
   | Lem_ast_out
   | Lem_out of string option
+  | Lem_sequential_out of string option
   | Ocaml_out of string option
 
 let get_lexbuf fn =
@@ -185,6 +186,18 @@ let output1 libpath out_arg filename defs  =
 	 (Pretty_print.pp_defs_lem o defs (generated_line filename))
            ["Pervasives_extra";"Sail_impl_base";"Prompt";"Sail_values";lib];
          close_output_with_check ext_o;
+      | Lem_sequential_out None ->
+         let ((o,_, _) as ext_o) =
+           open_output_with_check_unformatted (f' ^ "_sequential_embedded.lem") in
+         (Pretty_print.pp_defs_lem o defs (generated_line filename))
+           ["Pervasives_extra";"Sail_impl_base";"State";"Sail_values"];
+         close_output_with_check ext_o
+      | Lem_sequential_out (Some lib) ->
+         let ((o,_, _) as ext_o) =
+           open_output_with_check_unformatted (f' ^ "_sequential_embedded.lem") in
+	 (Pretty_print.pp_defs_lem o defs (generated_line filename))
+           ["Pervasives_extra";"Sail_impl_base";"State";"Sail_values";lib];
+         close_output_with_check ext_o;
       | Ocaml_out None ->
         let ((o,temp_file_name, _) as ext_o) = open_output_with_check_unformatted (f' ^ ".ml") in
 	begin Pretty_print.pp_defs_ocaml o defs (generated_line filename) ["Big_int_Z";"Sail_values"];
diff --git a/src/process_file.mli b/src/process_file.mli
index 66b1d8af..52c5474e 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -55,6 +55,7 @@ val rewrite_ast_ocaml : Type_internal.tannot Ast.defs -> Type_internal.tannot As
 type out_type =
   | Lem_ast_out
   | Lem_out of string option (* If present, the string is a file to open in the lem backend*)
+  | Lem_sequential_out of string option (* If present, the string is a file to open in the lem backend*)
   | Ocaml_out of string option (* If present, the string is a file to open in the ocaml backend*)
 
 val output :
diff --git a/src/sail.ml b/src/sail.ml
index 12e90dd9..0464fc22 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -52,6 +52,7 @@ let opt_print_version = ref false
 let opt_print_verbose = ref false
 let opt_print_lem_ast = ref false
 let opt_print_lem = ref false
+let opt_print_lem_sequential = ref false
 let opt_print_ocaml = ref false
 let opt_libs_lem = ref ([]:string list)
 let opt_libs_ocaml = ref ([]:string list)
@@ -68,7 +69,10 @@ let options = Arg.align ([
     " pretty-print a Lem AST representation of the file");
   ( "-lem",
     Arg.Set opt_print_lem,
-    " print a Lem translated version of the specification");
+    " print a Lem translated version of the specification to integrate with a concurrency model");
+  ( "-lem_sequential",
+    Arg.Set opt_print_lem_sequential,
+    " print a Lem translated version of the specification as a sequential model");
   ( "-ocaml",
     Arg.Set opt_print_ocaml,
     " print an Ocaml translated version of the specification");
@@ -133,6 +137,12 @@ let main() =
          if !(opt_libs_lem) = []
          then output "" (Lem_out None) [out_name,ast_lem]
          else output "" (Lem_out (Some (List.hd !opt_libs_lem))) [out_name,ast_lem]
+       else ());
+      (if !(opt_print_lem_sequential)
+       then let ast_lem = rewrite_ast_lem ast in
+         if !(opt_libs_lem) = []
+         then output "" (Lem_sequential_out None) [out_name,ast_lem]
+         else output "" (Lem_sequential_out (Some (List.hd !opt_libs_lem))) [out_name,ast_lem]
        else ())
     end