another refactoring in Term (and Explicit_polymorphism)

src/core/term.ml

@@ -74,6 +74,13 @@ let create_lsymbol name args value = {
 let create_fsymbol nm al vl = create_lsymbol nm al (Some vl)
 let create_psymbol nm al    = create_lsymbol nm al (None)
 
+let ls_ty_freevars ls =
+  let acc = match ls.ls_value with
+    | None -> Stv.empty
+    | Some ty -> ty_freevars Stv.empty ty
+  in
+  List.fold_left ty_freevars acc ls.ls_args
+
 (** Patterns *)
 
 type pattern = {
@@ -950,29 +957,28 @@ let f_open_quant_cb fq =
 
 (* constructors with type checking *)
 
-let t_app_inst fs tl ty =
-  let s = match fs.ls_value with
-    | Some vty -> ty_match Mtv.empty vty ty
-    | _ -> raise (FunctionSymbolExpected fs)
+let ls_app_inst ls tl ty =
+  let s = match ls.ls_value, ty with
+    | Some _, None -> raise (PredicateSymbolExpected ls)
+    | None, Some _ -> raise (FunctionSymbolExpected ls)
+    | Some vty, Some ty -> ty_match Mtv.empty vty ty
+    | None, None -> Mtv.empty
   in
-  let mtch s ty t = ty_match s ty t.t_ty in
-  try List.fold_left2 mtch s fs.ls_args tl
-  with Invalid_argument _ -> raise (BadArity
-    (fs, List.length fs.ls_args, List.length tl))
-
-let f_app_inst ps tl =
-  let s = match ps.ls_value with
-    | None -> Mtv.empty
-    | _ -> raise (PredicateSymbolExpected ps)
+  let s =
+    let mtch s ty t = ty_match s ty t.t_ty in
+    try List.fold_left2 mtch s ls.ls_args tl
+    with Invalid_argument _ -> raise (BadArity
+     (ls, List.length ls.ls_args, List.length tl))
   in
-  let mtch s ty t = ty_match s ty t.t_ty in
-  try List.fold_left2 mtch s ps.ls_args tl
-  with Invalid_argument _ -> raise (BadArity
-    (ps, List.length ps.ls_args, List.length tl))
+  let add v acc = Mtv.add v (ty_inst s (ty_var v)) acc in
+  Stv.fold add (ls_ty_freevars ls) Mtv.empty
+
+let fs_app_inst fs tl ty = ls_app_inst fs tl (Some ty)
+let ps_app_inst ps tl    = ls_app_inst ps tl None
 
-let t_app fs tl ty = ignore (t_app_inst fs tl ty); t_app fs tl ty
+let t_app fs tl ty = ignore (fs_app_inst fs tl ty); t_app fs tl ty
 
-let f_app ps tl = ignore (f_app_inst ps tl); f_app ps tl
+let f_app ps tl = ignore (ps_app_inst ps tl); f_app ps tl
 
 let t_app_infer fs tl =
   let mtch s ty t = ty_match s ty t.t_ty in

src/core/term.mli

@@ -55,6 +55,8 @@ val create_lsymbol : preid -> ty list -> ty option -> lsymbol
 val create_fsymbol : preid -> ty list -> ty -> lsymbol
 val create_psymbol : preid -> ty list -> lsymbol
 
+val ls_ty_freevars : lsymbol -> Stv.t
+
 (** {2 Exceptions} *)
 
 exception EmptyCase
@@ -221,6 +223,12 @@ val f_open_quant_cb :
   fmla_quant -> vsymbol list * trigger list * fmla *
               (vsymbol list -> trigger list -> fmla -> fmla_quant)
 
+(** compute type instance *)
+
+val ls_app_inst : lsymbol -> term list -> ty option -> ty Mtv.t
+val fs_app_inst : lsymbol -> term list -> ty -> ty Mtv.t
+val ps_app_inst : lsymbol -> term list -> ty Mtv.t
+
 (** smart constructors for term *)
 
 val t_var : vsymbol -> term
@@ -237,7 +245,6 @@ val t_let_close : vsymbol -> term -> term -> term
 val t_eps_close : vsymbol -> fmla -> term
 
 val t_app_infer : lsymbol -> term list -> term
-val t_app_inst : lsymbol -> term list -> ty -> ty Mtv.t
 
 val t_label : label list -> term -> term
 val t_label_add : label -> term -> term
@@ -266,8 +273,6 @@ val f_quant_close : quant -> vsymbol list -> trigger list -> fmla -> fmla
 val f_forall_close : vsymbol list -> trigger list -> fmla -> fmla
 val f_exists_close : vsymbol list -> trigger list -> fmla -> fmla
 
-val f_app_inst : lsymbol -> term list -> ty Mtv.t
-
 val f_label : label list -> fmla -> fmla
 val f_label_add : label -> fmla -> fmla
 val f_label_copy : fmla -> fmla -> fmla

src/transform/explicit_polymorphism.ml

@@ -64,28 +64,17 @@ module Transform = struct
       Hashtbl.add tbl id new_image;
       new_image
 
-  (** returns all type vars in given lsymbol *)
-  let l_find_type_vars l =
-    let acc = match l.ls_value with
-      | None -> Stv.empty
-      | Some ty -> ty_freevars Stv.empty ty in
-    let s = List.fold_left ty_freevars acc l.ls_args in
-    Stv.elements s
-
   (** creates a new logic symbol, with a different type if the
   given symbol was polymorphic *)
   let logic_to_logic lsymbol =
     if ls_equal lsymbol ps_equ || ls_equal lsymbol ps_neq then lsymbol else
-    let new_ty = l_find_type_vars lsymbol in
+    let new_ty = ls_ty_freevars lsymbol in
     (* as many t as type vars *)
-    if new_ty = [] then lsymbol (* same type *) else
-      let new_ty = List.map (const my_t) new_ty in
-      let all_new_ty = new_ty @ lsymbol.ls_args in
+    if Stv.is_empty new_ty then lsymbol (* same type *) else
+      let add _ acc = my_t :: acc in
+      let args = Stv.fold add new_ty lsymbol.ls_args in
       (* creates a new lsymbol with the same name but a different type *)
-      let new_lsymbol =
-        Term.create_lsymbol (id_clone lsymbol.ls_name)
-          all_new_ty lsymbol.ls_value in
-      new_lsymbol
+      Term.create_lsymbol (id_clone lsymbol.ls_name) args lsymbol.ls_value
 
   (** creates a lsymbol associated with the given tysymbol *)
   let type_to_logic ty =
@@ -116,38 +105,29 @@ module Transform = struct
   (** translation of terms *)
   let rec term_transform tblT tblL varM t = match t.t_node with
     | Tapp(f, terms) ->
-      let new_f = findL tblL f in
-      (* first, remember an order for type vars of new_f *)
-      let type_vars = l_find_type_vars f in
-      (* Debug.print_list Pretty.print_ty Format.std_formatter type_vars; *)
-      let tv_to_ty = t_app_inst f terms t.t_ty in
-      (* Debug.print_mtv Pretty.print_ty Format.err_formatter tv_to_ty; *)
-      (* fresh terms to be added at the beginning of the list of arguments *)
-      let find_ty v = ty_to_term tblT varM (ty_inst tv_to_ty (ty_var v)) in
-      let new_terms = List.map find_ty type_vars in
-      let transformed_terms = List.map (term_transform tblT tblL varM) terms in
-      t_app new_f (new_terms @ transformed_terms) t.t_ty
+      let terms = args_transform tblT tblL varM f terms (Some t.t_ty) in
+      t_app (findL tblL f) terms t.t_ty
     | _ -> (* default case : traverse *)
       t_map (term_transform tblT tblL varM) (fmla_transform tblT tblL varM) t
 
   (** translation of formulae *)
   and fmla_transform tblT tblL varM f = match f.f_node with
-      (* first case : predicate (not = or <>), we must translate it and its args *)
-    | Fapp(p,terms) when (not (ls_equal p ps_equ)) && not(ls_equal p ps_neq) ->
-      let new_p = findL tblL p in
-      (* first, remember an order for type vars of new_f *)
-      let type_vars = l_find_type_vars p in
-      (* Debug.print_list Pretty.print_ty Format.std_formatter type_vars; *)
-      let tv_to_ty = f_app_inst p terms in
-      (* Debug.print_mtv Pretty.print_ty Format.err_formatter tv_to_ty; *)
-      (* fresh terms to be added at the beginning of the list of arguments *)
-      let find_ty v = ty_to_term tblT varM (ty_inst tv_to_ty (ty_var v)) in
-      let new_terms = List.map find_ty type_vars in
-      let transformed_terms = List.map (term_transform tblT tblL varM) terms in
-      f_app new_p (new_terms @ transformed_terms)
+      (* first case : predicate (not =), we must translate it and its args *)
+    | Fapp(p,terms) when not (ls_equal p ps_equ || ls_equal p ps_neq) ->
+      let terms = args_transform tblT tblL varM p terms None in
+      f_app (findL tblL p) terms
     | _ -> (* otherwise : just traverse and translate *)
       f_map (term_transform tblT tblL varM) (fmla_transform tblT tblL varM) f
 
+  and args_transform tblT tblL varM ls args ty =
+    (* Debug.print_list Pretty.print_ty Format.std_formatter type_vars; *)
+    let tv_to_ty = ls_app_inst ls args ty in
+    (* Debug.print_mtv Pretty.print_ty Format.err_formatter tv_to_ty; *)
+    let args = List.map (term_transform tblT tblL varM) args in
+    (* fresh args to be added at the beginning of the list of arguments *)
+    let add _ ty acc = ty_to_term tblT varM ty :: acc in
+    Mtv.fold add tv_to_ty args
+
   (** transforms a list of logic declarations into another.
   Declares new lsymbols with explicit polymorphic signatures.
   @param tblT binds type symbols to logic symbols
@@ -157,20 +137,19 @@ module Transform = struct
     let helper = function
     | (lsymbol, Some ldef) ->
       let new_lsymbol = findL tblL lsymbol in (* new lsymbol *)
-      let polymorphic_vars = l_find_type_vars lsymbol in
-      let new_vars = List.map
-        (fun _ -> Term.create_vsymbol (id_fresh "t") my_t)
-        polymorphic_vars in (* new vars for polymorphism *)
-      let varM = List.fold_left2 (fun m x v -> Mtv.add x v m)
-        Mtv.empty polymorphic_vars new_vars in
       let vars,expr = open_ls_defn ldef in
+      let add v (vl,vm) =
+        let vs = Term.create_vsymbol (id_fresh "t") my_t in
+        vs :: vl, Mtv.add v vs vm
+      in
+      let vars,varM = Stv.fold add (ls_ty_freevars lsymbol) (vars,Mtv.empty) in
       (match expr with
       | Term t ->
           let t = term_transform tblT tblL varM t in
-          Decl.make_fs_defn new_lsymbol (new_vars @ vars) t
+          Decl.make_fs_defn new_lsymbol vars t
       | Fmla f ->
           let f = fmla_transform tblT tblL varM f in
-          Decl.make_ps_defn new_lsymbol (new_vars @ vars) f)
+          Decl.make_ps_defn new_lsymbol vars f)
     | (lsymbol, None) ->
       let new_lsymbol = findL tblL lsymbol in
       (new_lsymbol, None) in