syntax pour symbol defini

lib/drivers/alt_ergo.drv

@@ -6,7 +6,12 @@ prelude "(* this is a prelude for Alt-Ergo*)"
 printer "alt-ergo"
 
 call_on_file  "alt-ergo %s"
-
+(*
+tranformations
+  "simplify_recursive_definition"      
+  "inlining" ("trivial")
+end
+*)
 
 theory BuiltIn
   syntax type int "int"

src/output/alt_ergo.ml

@@ -148,43 +148,46 @@ let print_type_decl drv fmt = function
 let ac_th = ["algebra";"AC"]
 
 let print_logic_decl drv ctxt fmt = function
-  | Lfunction (ls, None) ->
+  | Lfunction (ls, def) ->
       begin
         match Driver.query_ident drv ls.ls_name with
           | Driver.Remove | Driver.Syntax _ -> false
-          | Driver.Tag s -> 
+          | Driver.Tag s ->
               let sac = if Snm.mem "AC" s then "ac " else "" in
-              let tyl = ls.ls_args in
               let ty = match ls.ls_value with None -> assert false | Some ty -> ty in
-              fprintf fmt "@[<hov 2>logic %s%a : %a -> %a@]@\n"
-                sac
-                print_ident ls.ls_name
-	        (print_list comma (print_type drv)) tyl (print_type drv) ty;
-              true
+              match def with
+                | None ->
+                    let tyl = ls.ls_args in
+                    fprintf fmt "@[<hov 2>logic %s%a : %a -> %a@]@\n"
+                      sac
+                      print_ident ls.ls_name
+	              (print_list comma (print_type drv)) tyl (print_type drv) ty;
+                    true
+                | Some defn ->
+                    let id = ls.ls_name in
+                    let _, vl, t = open_fs_defn defn in
+                    (* TODO AC? *)
+                    fprintf fmt "@[<hov 2>function %a(%a) : %a =@ %a@]@\n" print_ident id
+                      (print_list comma (print_logic_binder drv)) vl (print_type drv) ty (print_term drv) t;
+                    List.iter forget_var vl;true
       end
-  | Lfunction (ls, Some defn) ->
-      let id = ls.ls_name in
-      let _, vl, t = open_fs_defn defn in
-      let ty = match ls.ls_value with None -> assert false | Some ty -> ty in
-      fprintf fmt "@[<hov 2>function %a(%a) : %a =@ %a@]@\n" print_ident id
-        (print_list comma (print_logic_binder drv)) vl (print_type drv) ty (print_term drv) t;
-      List.iter forget_var vl;true
-  | Lpredicate (ls, None) ->
+  | Lpredicate (ls, def) ->
       begin
         match Driver.query_ident drv ls.ls_name with
           | Driver.Remove | Driver.Syntax _ -> false
-          | Driver.Tag s -> 
-              let sac = if Snm.mem "AC" s then "ac " else "" in
-              fprintf fmt "@[<hov 2>logic %s%a : %a -> prop@]" sac
-	        print_ident ls.ls_name (print_list comma (print_type drv)) ls.ls_args;
-              true
+          | Driver.Tag _ -> 
+              match def with
+                | None ->
+                    fprintf fmt "@[<hov 2>logic %a : %a -> prop@]"
+	              print_ident ls.ls_name (print_list comma (print_type drv)) ls.ls_args;
+                    true
+                | Some fd -> 
+                    let _,vl,f = open_ps_defn fd in
+                    fprintf fmt "@[<hov 2>predicate %a(%a) = %a@]"
+	              print_ident ls.ls_name 
+                      (print_list comma (print_logic_binder drv)) vl (print_fmla drv) f;
+                    true
       end
-  | Lpredicate (ls, Some fd) ->
-      let _,vl,f = open_ps_defn fd in
-      fprintf fmt "@[<hov 2>predicate %a(%a) = %a@]"
-	print_ident ls.ls_name 
-        (print_list comma (print_logic_binder drv)) vl (print_fmla drv) f;
-      true
 
 let print_decl drv ctxt fmt d = match d.d_node with
   | Dtype dl ->