ajout de l'inlining

Makefile.in

@@ -112,8 +112,7 @@ PARSER_CMO := parser.cmo lexer.cmo typing.cmo
 
 PARSER_CMO := $(addprefix src/parser/,$(PARSER_CMO))
 
-TRANSFORM_CMO := transform.cmo simplify_recursive_definition.cmo 
-#	inlining.cmo
+TRANSFORM_CMO := transform.cmo simplify_recursive_definition.cmo inlining.cmo
 
 TRANSFORM_CMO := $(addprefix src/transform/,$(TRANSFORM_CMO))
 

src/pretty.ml

@@ -52,7 +52,7 @@ let rec print_term fmt t = match t.t_node with
   | Tconst _ ->
       fprintf fmt "[const]"
   | Tapp (s, tl) ->
-      fprintf fmt "(%a(%a)@ : %a)" 
+      fprintf fmt "@[<hov>(%a(%a)@ : %a)@]" 
 	print_ident s.fs_name (print_list comma print_term) tl
 	print_ty t.t_ty
   | Tlet (t1,tbound) -> 
@@ -62,18 +62,18 @@ let rec print_term fmt t = match t.t_node with
   | Tcase _ -> assert false (*TODO*)
   | Teps _ -> assert false
 
-let print_vs fmt vs = 
+let print_vsymbol fmt vs = 
   fprintf fmt "%a :@ %a" print_ident vs.vs_name print_ty vs.vs_ty
 
 let rec print_fmla fmt f = match f.f_node with
   | Fapp (s,tl) -> 
-      fprintf fmt "(%a(%a))" 
+      fprintf fmt "@[<hov>(%a(%a))@]" 
 	print_ident s.ps_name (print_list comma print_term) tl
   | Fquant (q,fquant) ->
       let vl,tl,f = f_open_quant fquant in
       fprintf fmt "(%s %a %a.@ %a)"
         (match q with Fforall -> "forall" | Fexists -> "exists")
-        (print_list comma print_vs) vl print_tl tl print_fmla f
+        (print_list comma print_vsymbol) vl print_tl tl print_fmla f
   | Ftrue -> fprintf fmt "true"
   | Ffalse -> fprintf fmt "false)"
   | Fbinop (b,f1,f2) -> 
@@ -106,14 +106,14 @@ let print_psymbol fmt {ps_name = ps_name; ps_scheme = tyl} =
     (print_list_paren comma print_ty) tyl 
 
 let print_ty_decl fmt (ts,tydef) = match tydef,ts.ts_def with
-  | Tabstract,None -> fprintf fmt "type %a %a" 
+  | Tabstract,None -> fprintf fmt "@[<hov>type %a %a@]" 
       (print_list_paren comma print_typevar) ts.ts_args
       print_ident ts.ts_name
-  | Tabstract,Some f -> fprintf fmt "type %a %a =@ %a" 
+  | Tabstract,Some f -> fprintf fmt "@[<hov>type %a %a =@ @[<hov>%a@]@]" 
       (print_list_paren comma print_typevar) ts.ts_args
       print_ident ts.ts_name
       print_ty f
-  | Talgebraic d, None -> fprintf fmt "type %a %a =@ %a" 
+  | Talgebraic d, None -> fprintf fmt "@[<hov>type %a %a =@ @[<hov>%a@]@]" 
       (print_list_paren comma print_typevar) ts.ts_args
       print_ident ts.ts_name
       (print_list newline print_fsymbol) d
@@ -134,8 +134,8 @@ let print_logic_decl fmt = function
   | Linductive _ -> assert false (*TODO*)
 
 let print_decl fmt d = match d.d_node with
-  | Dtype tl -> fprintf fmt "(* *)@\n%a" (print_list newline print_ty_decl) tl
-  | Dlogic ldl -> fprintf fmt "(* *)@\n%a" 
+  | Dtype tl -> fprintf fmt "@[<hov>%a@]@ (* *)" (print_list newline print_ty_decl) tl
+  | Dlogic ldl -> fprintf fmt "@[<hov>%a@]@ (* *)" 
       (print_list newline print_logic_decl) ldl 
   | Dprop (k,id,fmla) -> 
       fprintf fmt "%s %a :@ %a@\n" 
@@ -148,11 +148,10 @@ let print_decl_or_use fmt = function
   | Use u -> fprintf fmt "use export %a@\n" print_ident u.th_name
 
 let print_decl_or_use_list fmt de = 
-  fprintf fmt "@[<hov>%a@]"
-    (Pp.print_list Pp.newline print_decl_or_use) de
+  fprintf fmt "@[<hov>%a@]" (print_list newline print_decl_or_use) de
 
 let print_theory fmt t =
   fprintf fmt "@[@[<hov 2>theory %a@\n%a@]@\nend@]@\n@\n" print_ident t.th_name 
-    (print_list newline print_decl_or_use) t.th_decls;
+    print_decl_or_use_list t.th_decls;
   fprintf fmt "@?"
 

src/pretty.mli

@@ -22,6 +22,12 @@ open Ty
 open Term
 open Theory
 
+val print_vsymbol : formatter -> vsymbol -> unit
+
+val print_fsymbol : formatter -> fsymbol -> unit
+
+val print_psymbol : formatter -> psymbol -> unit
+
 val print_ty : formatter -> ty -> unit
 
 val print_term : formatter -> term -> unit

src/transform/inlining.ml

+open Ident
+open Term
+open Theory
+
+let ttrue _ = true
+let ffalse _ = false
+
+type env = { fs : (vsymbol list * term) Mfs.t;
+             ps : (vsymbol list * fmla) Mps.t}
+
+let empty_env = { fs = Mfs.empty;
+                  ps = Mps.empty}
+open Format
+
+let print_env fmt env =
+  let print_map iter pterm pfs = Pp.print_iter2 iter Pp.newline Pp.comma pfs
+    (Pp.print_pair (Pp.print_list Pp.comma Pretty.print_vsymbol) pterm) in
+  fprintf fmt "fs:@[<hov>%a@]@\nps:@[<hov>%a@]@\n"
+    (print_map Mfs.iter Pretty.print_term Pretty.print_fsymbol) env.fs
+    (print_map Mps.iter Pretty.print_fmla Pretty.print_psymbol) env.ps
+
+let rec replacet env t = 
+  let t = substt env t in
+  match t.t_node with
+    | Tapp (fs,tl) ->
+        begin try 
+          let (vs,t) = Mfs.find fs env.fs in
+          let m = List.fold_left2 (fun acc x y -> Mvs.add x y acc)
+            Mvs.empty vs tl in
+          t_subst m t
+        with Not_found -> t end
+    | _ -> t
+
+and replacep env f = 
+  let f = substp env f in
+  match f.f_node with
+    | Fapp (ps,tl) ->
+        begin try 
+          let (vs,t) = Mps.find ps env.ps in
+          let m = List.fold_left2 (fun acc x y -> Mvs.add x y acc) 
+            Mvs.empty vs tl in
+          f_subst m f
+        with Not_found -> f end
+    | _ -> f
+
+and substt env d = t_map (replacet env) (replacep env) d
+and substp env d = f_map (replacet env) (replacep env) d
+
+let fold env d = 
+  match d.d_node with
+    | Dlogic [l] -> begin
+        match l with
+          | Lfunction (fs,None) -> env,[d] 
+          | Lfunction (fs,Some fmla) -> 
+              let _,vs,t = open_fs_defn fmla in
+              let t = replacet env t in
+              if t_s_any ffalse ((==) fs) ffalse t 
+              then  env,[create_logic [Lfunction(fs,Some (make_fs_defn fs vs t))]]
+              else {env with fs = Mfs.add fs (vs,t) env.fs},[]
+          | Lpredicate (ps,None) -> env,[d]
+          | Lpredicate (ps,Some fmla) -> 
+              let _,vs,f = open_ps_defn fmla in
+              let f = replacep env f in
+              if f_s_any ffalse ffalse ((==) ps) f 
+              then  env,[create_logic [Lpredicate(ps,Some (make_ps_defn ps vs f))]]
+              else {env with ps = Mps.add ps (vs,f) env.ps},[]
+          | Linductive (ps,fmlal) -> 
+              let fmlal = List.map (fun (id,fmla) -> id,replacep env fmla) fmlal in
+              env,[create_logic [Linductive (ps,fmlal)]]
+      end
+    | Dlogic dl -> env,
+        [create_logic 
+           (List.map 
+              (function
+                 | Lfunction (fs,None) as a -> a 
+                 | Lfunction (fs,Some fmla) -> 
+                     let _,vs,t = open_fs_defn fmla in
+                     let t = replacet env t in
+                     Lfunction (fs,Some (make_fs_defn fs vs t))
+                 | Lpredicate (ps,None) as a -> a
+                 | Lpredicate (ps,Some fmla) ->
+                     let _,vs,t = open_ps_defn  fmla in
+                     let t = replacep env t in
+                     Lpredicate (ps,Some (make_ps_defn ps vs t))
+                 | Linductive (ps,fmlal) ->
+                     let fmlal = List.map 
+                       (fun (id,fmla) -> id,replacep env fmla) fmlal in
+                     Linductive (ps,fmlal)
+              ) dl)]
+    | Dtype dl -> env,[d]
+    | Dprop (k,i,fmla) -> env,[create_prop k (id_dup i) (replacep env fmla)]
+        
+let t = Transform.TDecl.fold_map_left fold empty_env
+  
+let t_use = Transform.TDecl_or_Use.fold_map_left 
+  (fun env d -> match d with 
+     | Decl d -> let env,l = (fold env d) in
+       env,List.map (fun d -> Decl d) l 
+     | Use _ as u -> env,[u]) empty_env
+  

src/transform/inlining.mli

+(* Inline the definition not recursive *)
+
+
+val t : (Theory.decl,Theory.decl) Transform.t
+
+val t_use : (Theory.decl_or_use,Theory.decl_or_use) Transform.t

src/transform/simplify_recursive_definition.ml

@@ -78,7 +78,7 @@ let connexe (m:Sid.t Mid.t)  =
         l::acc
       end
   in
-  Hid.fold (fun _ -> visit) ce []
+  List.rev (Hid.fold (fun _ -> visit) ce [])
 
 
 

src/transform/transform.ml

@@ -92,7 +92,7 @@ let compose f g = {all = (fun x -> g.all (f.all x));
                    from_list = f.from_list;
                    to_list = g.to_list}
 
-let apply f x = f.to_list (f.all (f.from_list (List.rev x)))
+let apply f x = (List.rev (f.to_list (f.all (f.from_list x))))
     
 let clear f = f.clear ()
 

src/util/pp.mli

@@ -35,13 +35,16 @@ val print_list_delim :
   (Format.formatter -> unit -> unit) ->
   (Format.formatter -> unit -> unit) ->
   (Format.formatter -> 'b -> unit) -> Format.formatter -> 'b list -> unit
+
 val print_pair_delim :
   (Format.formatter -> unit -> unit) ->
   (Format.formatter -> unit -> unit) ->
   (Format.formatter -> unit -> unit) ->
   (Format.formatter -> 'a -> unit) -> 
   (Format.formatter -> 'b -> unit) -> Format.formatter -> 'a * 'b -> unit
-
+val print_pair :
+  (Format.formatter -> 'a -> unit) -> 
+  (Format.formatter -> 'b -> unit) -> Format.formatter -> 'a * 'b -> unit
 
 val print_iter1 : 
   (('a -> unit) -> 'b -> unit) ->
@@ -57,11 +60,6 @@ val print_iter2:
   (Format.formatter -> 'b -> unit) -> 
   Format.formatter -> 'c -> unit
 
-
-val print_pair :
-  (Format.formatter -> 'a -> unit) -> 
-  (Format.formatter -> 'b -> unit) -> Format.formatter -> 'a * 'b -> unit
-
 val space : formatter -> unit -> unit
 val alt : formatter -> unit -> unit
 val newline : formatter -> unit -> unit