use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
authorblanchet
Thu Apr 29 10:25:26 2010 +0200 (2010-04-29 ago)
changeset 3655681dc2c20f052
parent 36555 8ff45c2076da
child 36557 3c2438efe224
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
src/HOL/Tools/Sledgehammer/metis_tactics.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Apr 29 01:17:14 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Apr 29 10:25:26 2010 +0200
     1.3 @@ -123,14 +123,16 @@
     1.4        in  (map (hol_literal_to_fol mode) lits, types_sorts) end;
     1.5  
     1.6  (*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
     1.7 -fun metis_of_typeLit pos (LTVar (s,x))  = metis_lit pos s [Metis.Term.Var x]
     1.8 -  | metis_of_typeLit pos (LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])];
     1.9 +fun metis_of_type_literals pos (TyLitVar (s, (s', _))) =
    1.10 +    metis_lit pos s [Metis.Term.Var s']
    1.11 +  | metis_of_type_literals pos (TyLitFree (s, (s', _))) =
    1.12 +    metis_lit pos s [Metis.Term.Fn (s',[])]
    1.13  
    1.14  fun default_sort _ (TVar _) = false
    1.15    | default_sort ctxt (TFree (x, s)) = (s = the_default [] (Variable.def_sort ctxt (x, ~1)));
    1.16  
    1.17  fun metis_of_tfree tf =
    1.18 -  Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_typeLit true tf));
    1.19 +  Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_type_literals true tf));
    1.20  
    1.21  fun hol_thm_to_fol is_conjecture ctxt mode th =
    1.22    let val thy = ProofContext.theory_of ctxt
    1.23 @@ -138,11 +140,12 @@
    1.24               (literals_of_hol_thm thy mode o HOLogic.dest_Trueprop o prop_of) th
    1.25    in
    1.26        if is_conjecture then
    1.27 -          (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), add_typs types_sorts)
    1.28 +          (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits),
    1.29 +           add_type_literals types_sorts)
    1.30        else
    1.31 -        let val tylits = add_typs (filter (not o default_sort ctxt) types_sorts)
    1.32 +        let val tylits = add_type_literals (filter (not o default_sort ctxt) types_sorts)
    1.33              val mtylits = if Config.get ctxt type_lits
    1.34 -                          then map (metis_of_typeLit false) tylits else []
    1.35 +                          then map (metis_of_type_literals false) tylits else []
    1.36          in
    1.37            (Metis.Thm.axiom (Metis.LiteralSet.fromList(mtylits @ mlits)), [])
    1.38          end
    1.39 @@ -598,7 +601,9 @@
    1.40  (*Extract TFree constraints from context to include as conjecture clauses*)
    1.41  fun init_tfrees ctxt =
    1.42    let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts
    1.43 -  in  add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end;
    1.44 +  in
    1.45 +    add_type_literals (Vartab.fold add (#2 (Variable.constraints_of ctxt)) [])
    1.46 +  end;
    1.47  
    1.48  (*transform isabelle type / arity clause to metis clause *)
    1.49  fun add_type_thm [] lmap = lmap
    1.50 @@ -669,7 +674,7 @@
    1.51        val (mode, {axioms,tfrees}) = build_map mode ctxt cls ths
    1.52        val _ = if null tfrees then ()
    1.53                else (trace_msg (fn () => "TFREE CLAUSES");
    1.54 -                    app (fn tf => trace_msg (fn _ => tptp_of_typeLit true tf)) tfrees)
    1.55 +                    app (fn tf => trace_msg (fn _ => tptp_of_type_literal true tf NONE |> fst)) tfrees)
    1.56        val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
    1.57        val thms = map #1 axioms
    1.58        val _ = app (fn th => trace_msg (fn () => Metis.Thm.toString th)) thms
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Thu Apr 29 01:17:14 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Thu Apr 29 10:25:26 2010 +0200
     2.3 @@ -44,9 +44,11 @@
     2.4      TyConstr of name * fol_type list
     2.5    val string_of_fol_type :
     2.6      fol_type -> name_pool option -> string * name_pool option
     2.7 -  datatype type_literal = LTVar of string * string | LTFree of string * string
     2.8 +  datatype type_literal =
     2.9 +    TyLitVar of string * name |
    2.10 +    TyLitFree of string * name
    2.11    exception CLAUSE of string * term
    2.12 -  val add_typs : typ list -> type_literal list
    2.13 +  val add_type_literals : typ list -> type_literal list
    2.14    val get_tvar_strs: typ list -> string list
    2.15    datatype arLit =
    2.16        TConsLit of class * string * string list
    2.17 @@ -68,7 +70,7 @@
    2.18      arity_clause -> int Symtab.table -> int Symtab.table
    2.19    val init_functab: int Symtab.table
    2.20    val dfg_sign: bool -> string -> string
    2.21 -  val dfg_of_typeLit: bool -> type_literal -> string
    2.22 +  val dfg_of_type_literal: bool -> type_literal -> string
    2.23    val gen_dfg_cls: int * string * kind * string list * string list * string list -> string
    2.24    val string_of_preds: (string * Int.int) list -> string
    2.25    val string_of_funcs: (string * int) list -> string
    2.26 @@ -79,7 +81,8 @@
    2.27    val dfg_classrel_clause: classrel_clause -> string
    2.28    val dfg_arity_clause: arity_clause -> string
    2.29    val tptp_sign: bool -> string -> string
    2.30 -  val tptp_of_typeLit : bool -> type_literal -> string
    2.31 +  val tptp_of_type_literal :
    2.32 +    bool -> type_literal -> name_pool option -> string * name_pool option
    2.33    val gen_tptp_cls : int * string * kind * string list * string list -> string
    2.34    val tptp_tfree_clause : string -> string
    2.35    val tptp_arity_clause : arity_clause -> string
    2.36 @@ -173,9 +176,7 @@
    2.37  fun paren_pack [] = ""   (*empty argument list*)
    2.38    | paren_pack strings = "(" ^ commas strings ^ ")";
    2.39  
    2.40 -(*TSTP format uses (...) rather than the old [...]*)
    2.41 -fun tptp_pack strings = "(" ^ space_implode " | " strings ^ ")";
    2.42 -
    2.43 +fun tptp_clause strings = "(" ^ space_implode " | " strings ^ ")"
    2.44  
    2.45  (*Remove the initial ' character from a type variable, if it is present*)
    2.46  fun trim_type_var s =
    2.47 @@ -230,9 +231,9 @@
    2.48  fun empty_name_pool readable_names =
    2.49    if readable_names then SOME (`I Symtab.empty) else NONE
    2.50  
    2.51 +fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs
    2.52  fun pool_map f xs =
    2.53 -  fold_rev (fn x => fn (ys, pool) => f x pool |>> (fn y => y :: ys)) xs
    2.54 -  o pair []
    2.55 +  pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs []
    2.56  
    2.57  fun add_nice_name full_name nice_prefix j the_pool =
    2.58    let
    2.59 @@ -306,8 +307,10 @@
    2.60        val (ss, pool) = pool_map string_of_fol_type tys pool
    2.61      in (s ^ paren_pack ss, pool) end
    2.62  
    2.63 -(*First string is the type class; the second is a TVar or TFfree*)
    2.64 -datatype type_literal = LTVar of string * string | LTFree of string * string;
    2.65 +(* The first component is the type class; the second is a TVar or TFree. *)
    2.66 +datatype type_literal =
    2.67 +  TyLitVar of string * name |
    2.68 +  TyLitFree of string * name
    2.69  
    2.70  exception CLAUSE of string * term;
    2.71  
    2.72 @@ -317,21 +320,21 @@
    2.73        let val sorts = sorts_on_typs_aux ((x,i), ss)
    2.74        in
    2.75            if s = "HOL.type" then sorts
    2.76 -          else if i = ~1 then LTFree(make_type_class s, make_fixed_type_var x) :: sorts
    2.77 -          else LTVar(make_type_class s, make_schematic_type_var (x,i)) :: sorts
    2.78 +          else if i = ~1 then TyLitFree (make_type_class s, `make_fixed_type_var x) :: sorts
    2.79 +          else TyLitVar (make_type_class s, (make_schematic_type_var (x,i), x)) :: sorts
    2.80        end;
    2.81  
    2.82  fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s)
    2.83    | sorts_on_typs (TVar (v,s))  = sorts_on_typs_aux (v,s);
    2.84  
    2.85 -fun pred_of_sort (LTVar (s,ty)) = (s,1)
    2.86 -  | pred_of_sort (LTFree (s,ty)) = (s,1)
    2.87 +fun pred_of_sort (TyLitVar (s, _)) = (s, 1)
    2.88 +  | pred_of_sort (TyLitFree (s, _)) = (s, 1)
    2.89  
    2.90  (*Given a list of sorted type variables, return a list of type literals.*)
    2.91 -fun add_typs Ts = fold (union (op =)) (map sorts_on_typs Ts) []
    2.92 +fun add_type_literals Ts = fold (union (op =)) (map sorts_on_typs Ts) []
    2.93  
    2.94  (*The correct treatment of TFrees like 'a in lemmas (axiom clauses) is not clear.
    2.95 -  * Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a
    2.96 +  *  Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a
    2.97      in a lemma has the same sort as 'a in the conjecture.
    2.98    * Deleting such clauses will lead to problems with locales in other use of local results
    2.99      where 'a is fixed. Probably we should delete clauses unless the sorts agree.
   2.100 @@ -499,8 +502,10 @@
   2.101  fun dfg_sign true s = s
   2.102    | dfg_sign false s = "not(" ^ s ^ ")"
   2.103  
   2.104 -fun dfg_of_typeLit pos (LTVar (s,ty))  = dfg_sign pos (s ^ "(" ^ ty ^ ")")
   2.105 -  | dfg_of_typeLit pos (LTFree (s,ty)) = dfg_sign pos (s ^ "(" ^ ty ^ ")");
   2.106 +fun dfg_of_type_literal pos (TyLitVar (s, (s', _))) =
   2.107 +    dfg_sign pos (s ^ "(" ^ s' ^ ")")
   2.108 +  | dfg_of_type_literal pos (TyLitFree (s, (s', _))) =
   2.109 +    dfg_sign pos (s ^ "(" ^ s' ^ ")");
   2.110  
   2.111  (*Enclose the clause body by quantifiers, if necessary*)
   2.112  fun dfg_forall [] body = body
   2.113 @@ -563,21 +568,23 @@
   2.114  fun tptp_sign true s = s
   2.115    | tptp_sign false s = "~ " ^ s
   2.116  
   2.117 -fun tptp_of_typeLit pos (LTVar (s, ty))  = tptp_sign pos (s ^ "(" ^ ty ^ ")")
   2.118 -  | tptp_of_typeLit pos (LTFree (s, ty)) = tptp_sign pos (s ^ "(" ^ ty ^ ")")
   2.119 +fun tptp_of_type_literal pos (TyLitVar (s, name)) =
   2.120 +    nice_name name #>> (fn s' => tptp_sign pos (s ^ "(" ^ s' ^ ")"))
   2.121 +  | tptp_of_type_literal pos (TyLitFree (s, name)) =
   2.122 +    nice_name name #>> (fn s' => tptp_sign pos (s ^ "(" ^ s' ^ ")"))
   2.123  
   2.124  fun tptp_cnf name kind formula =
   2.125    "cnf(" ^ name ^ ", " ^ kind ^ ",\n    " ^ formula ^ ").\n"
   2.126  
   2.127  fun gen_tptp_cls (cls_id, ax_name, Axiom, lits, tylits) =
   2.128        tptp_cnf (string_of_clausename (cls_id, ax_name)) "axiom"
   2.129 -               (tptp_pack (tylits @ lits))
   2.130 +               (tptp_clause (tylits @ lits))
   2.131    | gen_tptp_cls (cls_id, ax_name, Conjecture, lits, _) =
   2.132        tptp_cnf (string_of_clausename (cls_id, ax_name)) "negated_conjecture"
   2.133 -               (tptp_pack lits)
   2.134 +               (tptp_clause lits)
   2.135  
   2.136  fun tptp_tfree_clause tfree_lit =
   2.137 -    tptp_cnf "tfree_tcs" "negated_conjecture" (tptp_pack [tfree_lit])
   2.138 +    tptp_cnf "tfree_tcs" "negated_conjecture" (tptp_clause [tfree_lit])
   2.139  
   2.140  fun tptp_of_arLit (TConsLit (c,t,args)) =
   2.141        tptp_sign true (make_type_class c ^ "(" ^ t ^ paren_pack args ^ ")")
   2.142 @@ -586,11 +593,11 @@
   2.143  
   2.144  fun tptp_arity_clause (ArityClause{axiom_name,conclLit,premLits,...}) =
   2.145    tptp_cnf (string_of_ar axiom_name) "axiom"
   2.146 -           (tptp_pack (map tptp_of_arLit (conclLit :: premLits)))
   2.147 +           (tptp_clause (map tptp_of_arLit (conclLit :: premLits)))
   2.148  
   2.149  fun tptp_classrelLits sub sup =
   2.150    let val tvar = "(T)"
   2.151 -  in  tptp_pack [tptp_sign false (sub^tvar), tptp_sign true (sup^tvar)]  end;
   2.152 +  in  tptp_clause [tptp_sign false (sub^tvar), tptp_sign true (sup^tvar)]  end;
   2.153  
   2.154  fun tptp_classrel_clause (ClassrelClause {axiom_name,subclass,superclass,...}) =
   2.155    tptp_cnf axiom_name "axiom" (tptp_classrelLits subclass superclass)
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Thu Apr 29 01:17:14 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Thu Apr 29 10:25:26 2010 +0200
     3.3 @@ -302,9 +302,13 @@
     3.4   
     3.5  (* Given a clause, returns its literals paired with a list of literals
     3.6     concerning TFrees; the latter should only occur in conjecture clauses. *)
     3.7 -fun tptp_type_literals params pos (HOLClause {literals, ctypes_sorts, ...}) =
     3.8 -  pool_map (tptp_literal params) literals
     3.9 -  #>> rpair (map (tptp_of_typeLit pos) (add_typs ctypes_sorts))
    3.10 +fun tptp_type_literals params pos (HOLClause {literals, ctypes_sorts, ...})
    3.11 +                       pool =
    3.12 +  let
    3.13 +    val (lits, pool) = pool_map (tptp_literal params) literals pool
    3.14 +    val (tylits, pool) = pool_map (tptp_of_type_literal pos)
    3.15 +                                  (add_type_literals ctypes_sorts) pool
    3.16 +  in ((lits, tylits), pool) end
    3.17  
    3.18  fun tptp_clause params (cls as HOLClause {axiom_name, clause_id, kind, ...})
    3.19                  pool =
    3.20 @@ -323,7 +327,7 @@
    3.21  
    3.22  fun dfg_type_literals params pos (HOLClause {literals, ctypes_sorts, ...}) =
    3.23    pool_map (dfg_literal params) literals
    3.24 -  #>> rpair (map (dfg_of_typeLit pos) (add_typs ctypes_sorts))
    3.25 +  #>> rpair (map (dfg_of_type_literal pos) (add_type_literals ctypes_sorts))
    3.26  
    3.27  fun get_uvars (CombConst _) vars pool = (vars, pool)
    3.28    | get_uvars (CombVar (name, _)) vars pool =
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Apr 29 01:17:14 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Apr 29 10:25:26 2010 +0200
     4.3 @@ -377,16 +377,18 @@
     4.4  
     4.5  (*Update TVars/TFrees with detected sort constraints.*)
     4.6  fun repair_sorts vt =
     4.7 -  let fun tysubst (Type (a, Ts)) = Type (a, map tysubst Ts)
     4.8 -        | tysubst (TVar (xi, s)) = TVar (xi, the_default s (Vartab.lookup vt xi))
     4.9 -        | tysubst (TFree (x, s)) = TFree (x, the_default s (Vartab.lookup vt (x, ~1)))
    4.10 -      fun tmsubst (Const (a, T)) = Const (a, tysubst T)
    4.11 -        | tmsubst (Free (a, T)) = Free (a, tysubst T)
    4.12 -        | tmsubst (Var (xi, T)) = Var (xi, tysubst T)
    4.13 -        | tmsubst (t as Bound _) = t
    4.14 -        | tmsubst (Abs (a, T, t)) = Abs (a, tysubst T, tmsubst t)
    4.15 -        | tmsubst (t1 $ t2) = tmsubst t1 $ tmsubst t2
    4.16 -  in not (Vartab.is_empty vt) ? tmsubst end
    4.17 +  let
    4.18 +    fun do_type (Type (a, Ts)) = Type (a, map do_type Ts)
    4.19 +      | do_type (TVar (xi, s)) = TVar (xi, the_default s (Vartab.lookup vt xi))
    4.20 +      | do_type (TFree (x, s)) =
    4.21 +        TFree (x, the_default s (Vartab.lookup vt (x, ~1)))
    4.22 +    fun do_term (Const (a, T)) = Const (a, do_type T)
    4.23 +      | do_term (Free (a, T)) = Free (a, do_type T)
    4.24 +      | do_term (Var (xi, T)) = Var (xi, do_type T)
    4.25 +      | do_term (t as Bound _) = t
    4.26 +      | do_term (Abs (a, T, t)) = Abs (a, do_type T, do_term t)
    4.27 +      | do_term (t1 $ t2) = do_term t1 $ do_term t2
    4.28 +  in not (Vartab.is_empty vt) ? do_term end
    4.29  
    4.30  fun unskolemize_term t =
    4.31    fold forall_of (Term.add_consts t []
    4.32 @@ -414,7 +416,7 @@
    4.33    let val (vt, t) = lits_of_nodes (ProofContext.theory_of ctxt) (vt, []) us in
    4.34      t |> repair_sorts vt
    4.35    end
    4.36 -fun check_clause ctxt =
    4.37 +fun check_formula ctxt =
    4.38    TypeInfer.constrain HOLogic.boolT
    4.39    #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
    4.40  
    4.41 @@ -450,7 +452,7 @@
    4.42        val t2 = clause_of_nodes ctxt vt us
    4.43        val (t1, t2) =
    4.44          HOLogic.eq_const HOLogic.typeT $ t1 $ t2
    4.45 -        |> unvarify_args |> uncombine_term |> check_clause ctxt
    4.46 +        |> unvarify_args |> uncombine_term |> check_formula ctxt
    4.47          |> HOLogic.dest_eq
    4.48      in
    4.49        (Definition (num, t1, t2),
    4.50 @@ -459,7 +461,7 @@
    4.51    | decode_line vt (Inference (num, us, deps)) ctxt =
    4.52      let
    4.53        val t = us |> clause_of_nodes ctxt vt
    4.54 -                 |> unskolemize_term |> uncombine_term |> check_clause ctxt
    4.55 +                 |> unskolemize_term |> uncombine_term |> check_formula ctxt
    4.56      in
    4.57        (Inference (num, t, deps),
    4.58         fold Variable.declare_term (OldTerm.term_frees t) ctxt)
    4.59 @@ -655,12 +657,13 @@
    4.60     "drop_ls" are those that should be dropped in a case split. *)
    4.61  type backpatches = (label * facts) list * (label list * label list)
    4.62  
    4.63 -fun using_of_step (Have (_, _, _, by)) =
    4.64 +fun used_labels_of_step (Have (_, _, _, by)) =
    4.65      (case by of
    4.66         Facts (ls, _) => ls
    4.67 -     | CaseSplit (proofs, (ls, _)) => fold (union (op =) o using_of) proofs ls)
    4.68 -  | using_of_step _ = []
    4.69 -and using_of proof = fold (union (op =) o using_of_step) proof []
    4.70 +     | CaseSplit (proofs, (ls, _)) =>
    4.71 +       fold (union (op =) o used_labels_of) proofs ls)
    4.72 +  | used_labels_of_step _ = []
    4.73 +and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof []
    4.74  
    4.75  fun new_labels_of_step (Fix _) = []
    4.76    | new_labels_of_step (Let _) = []
    4.77 @@ -681,7 +684,7 @@
    4.78            if forall (fn Have ([], l', t', _) :: _ => (l, t) = (l', t')
    4.79                        | _ => false) (tl proofs) andalso
    4.80               not (exists (member (op =) (maps new_labels_of proofs))
    4.81 -                         (using_of proof_tail)) then
    4.82 +                         (used_labels_of proof_tail)) then
    4.83              SOME (l, t, map rev proofs, proof_tail)
    4.84            else
    4.85              NONE
    4.86 @@ -823,17 +826,17 @@
    4.87  
    4.88  fun kill_useless_labels_in_proof proof =
    4.89    let
    4.90 -    val used_ls = using_of proof
    4.91 +    val used_ls = used_labels_of proof
    4.92      fun do_label l = if member (op =) used_ls l then l else no_label
    4.93 -    fun kill (Assume (l, t)) = Assume (do_label l, t)
    4.94 -      | kill (Have (qs, l, t, by)) =
    4.95 +    fun do_step (Assume (l, t)) = Assume (do_label l, t)
    4.96 +      | do_step (Have (qs, l, t, by)) =
    4.97          Have (qs, do_label l, t,
    4.98                case by of
    4.99                  CaseSplit (proofs, facts) =>
   4.100 -                CaseSplit (map (map kill) proofs, facts)
   4.101 +                CaseSplit (map (map do_step) proofs, facts)
   4.102                | _ => by)
   4.103 -      | kill step = step
   4.104 -  in map kill proof end
   4.105 +      | do_step step = step
   4.106 +  in map do_step proof end
   4.107  
   4.108  fun prefix_for_depth n = replicate_string (n + 1)
   4.109  
   4.110 @@ -891,11 +894,9 @@
   4.111         else
   4.112           if member (op =) qs Show then "show" else "have")
   4.113      val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
   4.114 -    fun do_using [] = ""
   4.115 -      | do_using ls = "using " ^ (space_implode " " (map do_raw_label ls)) ^ " "
   4.116 -    fun do_by_facts [] = "by metis"
   4.117 -      | do_by_facts ss = "by (metis " ^ space_implode " " ss ^ ")"
   4.118 -    fun do_facts (ls, ss) = do_using ls ^ do_by_facts ss
   4.119 +    fun do_facts ([], []) = "by metis"
   4.120 +      | do_facts (ls, ss) =
   4.121 +        "by (metis " ^ space_implode " " (map do_raw_label ls @ ss) ^ ")"
   4.122      and do_step ind (Fix xs) =
   4.123          do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
   4.124        | do_step ind (Let (t1, t2)) =