Inlining: put [@inline:trivial] over an lsymbol to force inlining

src/transform/inlining.ml

@@ -9,13 +9,15 @@
 (*                                                                  *)
 (********************************************************************)
 
+open Ident
 open Ty
 open Term
 open Decl
 open Theory
 open Task
 
-let intro_attr = Ident.create_attribute "introduced"
+let intro_attr = create_attribute "introduced"
+let inline_trivial_attr = create_attribute "inline:trivial"
 
 let meta_get_counterexmp =
   Theory.register_meta_excl "get_counterexmp" [Theory.MTstring]
@@ -25,7 +27,6 @@ let get_counterexmp task =
   let ce_meta = Task.find_meta_tds task meta_get_counterexmp in
   not (Theory.Stdecl.is_empty ce_meta.tds_set)
 
-
 let rec relocate loc t =
   t_map (relocate loc) (t_attr_set ?loc t.t_attrs t)
 
@@ -53,7 +54,7 @@ let rec f_replace_top env f = match f.t_node with
   | Tapp (ps,_) when ls_equal ps ps_equ ->
       t_map (f_replace_top env) f
   | Tapp (ls,tl) ->
-    t_attr_copy f (t_unfold f.t_loc env ls tl f.t_ty)
+      t_attr_copy f (t_unfold f.t_loc env ls tl f.t_ty)
   | _ when f.t_ty = None ->
       TermTF.t_map (fun t -> t) (f_replace_top env) f
   | _ ->
@@ -61,7 +62,7 @@ let rec f_replace_top env f = match f.t_node with
 
 (* treat a declaration *)
 
-let fold in_goal notdeft notdeff notls d (env, task) =
+let fold in_goal notls notdef d (env, task) =
   let d = match d.d_node with
     | Dprop (Pgoal,_,_) when in_goal ->
         decl_map (f_replace_top env) d
@@ -71,23 +72,21 @@ let fold in_goal notdeft notdeff notls d (env, task) =
         decl_map (t_replace_all env) d
   in
   match d.d_node with
-    | Dlogic [ls,ld] when not (notls ls) ->
+    | Dlogic [ls,ld]
+      when not (Sid.mem ls.ls_name d.d_syms || notls ls) ->
         let vl,e = open_ls_defn ld in
-        let inline =
-          not (TermTF.t_select notdeft notdeff e
-            || t_s_any Util.ffalse (ls_equal ls) e) in
-        let env = if inline then Mls.add ls (vl,e) env else env in
-        let task =
-          if inline && not in_goal then task else Task.add_decl task d
-        in
-        env, task
+        let attrs = Sattr.union e.t_attrs ls.ls_name.id_attrs in
+        let e_ls_attrs = t_attr_set ?loc:e.t_loc attrs e in
+        if notdef e_ls_attrs then env, Task.add_decl task d
+        else Mls.add ls (vl,e) env,
+             if in_goal then Task.add_decl task d else task
     | _ ->
         env, Task.add_decl task d
 
-let fold in_goal notdeft notdeff notls task_hd (env, task) =
+let fold in_goal notls notdef task_hd (env, task) =
   match task_hd.task_decl.td_node with
     | Decl d ->
-        fold in_goal notdeft notdeff notls d (env, task)
+        fold in_goal notls notdef d (env, task)
     | _ ->
         env, add_tdecl task task_hd.task_decl
 
@@ -96,24 +95,23 @@ let fold in_goal notdeft notdeff notls task_hd (env, task) =
 let meta = Theory.register_meta "inline:no" [Theory.MTlsymbol]
   ~desc:"Disallow@ the@ inlining@ of@ the@ given@ function/predicate@ symbol."
 
-let t ?(use_meta=true) ?(in_goal=false) ~notdeft ~notdeff ~notls =
-  Trans.bind (Trans.store get_counterexmp)
-  (fun for_counterexample ->
+let t ?(use_meta=true) ?(in_goal=false) ~notls ~notdef =
+  Trans.bind (Trans.store get_counterexmp) (fun for_counterexample ->
     let trans notls =
-      Trans.fold_map (fold in_goal notdeft notdeff notls) Mls.empty None in
+      Trans.fold_map (fold in_goal notls notdef) Mls.empty None in
     if use_meta then
       Trans.on_tagged_ls meta (fun sls ->
-          let notls ls = Sls.mem ls sls || notls ~for_counterexample ls in
-          trans notls)
+        let notls ls = Sls.mem ls sls || notls ~for_counterexample ls in
+        trans notls)
     else
       trans (notls ~for_counterexample))
 
 let all =
-  t ~use_meta:true ~in_goal:false ~notdeft:Util.ffalse ~notdeff:Util.ffalse
+  t ~use_meta:true ~in_goal:false ~notdef:Util.ffalse
     ~notls:(fun ~for_counterexample:_ _ -> false)
 
 let goal =
-  t ~use_meta:true ~in_goal:true ~notdeft:Util.ffalse ~notdeff:Util.ffalse
+  t ~use_meta:true ~in_goal:true ~notdef:Util.ffalse
     ~notls:(fun ~for_counterexample:_ _ -> false)
 
 (* inline_trivial *)
@@ -129,7 +127,8 @@ let trivial tl =
   try ignore (List.fold_left add Svs.empty tl); true
   with Util.FoldSkip -> false
 
-let notdeft t = match t.t_node with
+let notdef t = match t.t_node with
+  | _ when Sattr.mem inline_trivial_attr t.t_attrs -> false
   | Tvar _ | Tconst _ -> false
   | Ttrue  | Tfalse   -> false
   | Tapp (_,tl) -> not (trivial tl)
@@ -141,8 +140,8 @@ let trivial =
        when counterexamples are wanted. These are recognized
        as having the attribute `introduced` *)
     for_counterexample && ls.ls_args = [] &&
-      Ident.(Sattr.mem intro_attr ls.ls_name.id_attrs) in
-  t ~use_meta:true ~in_goal:false ~notdeft:notdeft ~notdeff:notdeft ~notls
+      Sattr.mem intro_attr ls.ls_name.id_attrs in
+  t ~use_meta:true ~in_goal:false ~notls ~notdef
 
 let () =
   Trans.register_transform "inline_all" all
@@ -150,4 +149,5 @@ let () =
   Trans.register_transform "inline_goal" goal
     ~desc:"Same@ as@ 'inline_all', but@ only@ inline in@ goals.";
   Trans.register_transform "inline_trivial" trivial
-    ~desc:"Inline@ trivial@ definitions@ like@ @[f(x,y) = g(y,x,0)@]."
+    ~desc:"Inline@ trivial@ definitions@ like@ @[f(x,y) = g(y,x,0)@]. \
+           Add@ the@ \"inline:trivial\"@ attribute@ to@ force@ inlining."

src/transform/inlining.mli

@@ -26,23 +26,21 @@ val get_counterexmp : Task.task -> bool
 val t :
   ?use_meta:bool ->
   ?in_goal:bool ->
-  notdeft:(Term.term -> bool) ->
-  notdeff:(Term.term -> bool) ->
-  notls  :(for_counterexample:bool -> Term.lsymbol -> bool) ->
+  notls:(for_counterexample:bool -> Term.lsymbol -> bool) ->
+  notdef:(Term.term -> bool) ->
   Task.task Trans.trans
 
-(** [t ~use_meta ~in_goal ~notdeft ~notdeff ~notls] returns a transformation
+(** [t ~use_meta ~in_goal ~notls ~notdef] returns a transformation
     that expands a symbol [ls] in the subsequent declarations unless [ls]
     satisfies one of the following conditions:
     - [ls] is defined via a (mutually) recursive definition;
     - [ls] is an inductive predicate or an algebraic type constructor;
-    - [ls] is a function symbol and [notdeft] returns true on its definition;
-    - [ls] is a predicate symbol and [notdeff] returns true on its definition;
     - [notls ls] returns [true];
+    - [notdef] returns [true] on the definition of [ls];
     - [use_meta] is set and [ls] is tagged by "inline:no"
 
-    Notice that [use_meta], [notdeft], [notdeff], [notls] restrict only which
-    symbols are inlined not when.
+    Notice that [use_meta], [notls], [notdef] restrict only which
+    symbols are inlined, not when.
 
     If [in_goal] is set, only the top-most symbols in the goal are expanded.
 *)