acl2/ml/functionEncodeLib.sml

1564 (*     constructors determined by applying the function is complete, ie.     *)
1565 (*     contains all the constructors for that type:                          *)
1567 (*     Notes: All arguments to constructors must be free variables           *)
1577 (*          --> For a type with n constructors should have n clauses         *)
1603 (*     constructors are processed. Eg.                                       *)
1608 (*     If the list given does not correctly split the constructors then      *)
1744 let val constructors = map (fn x => outermost (mk_eq (x,x))) missing
1747    (case (mk_set (map (base_type o type_of) constructors))
1750                     "Types of constructors do not match!")
1752     if all (all is_var o snd o strip_comb) constructors andalso
1754                          constructors) (constructors_of x)
1755        then let val var = case (total (tryfind (hd o free_vars)) constructors)
1761             in [subst (map (fn c => c |-> var) constructors) (hd missing)]
1776                 "Two or more function clauses do not differ by constructors")
2073 (*     Returns a theorem that resolves nested constructors:                  *)
2084                       (mkDebugExn "mk_initial" "Invalid list of constructors")
2364     val constructors = constructors_of t handle e =>
2370                    (enumerate 0 (fst (strip_fun (type_of c))))) constructors;
2373                 vars constructors
2377                        (enumerate 0 constructors) vars) handle e => wrap e
2391                                case_defs3) constructors
2501 (* Add rewrites to encode constructors, case theorems, and encoding of       *)
3000 let val (fconst,constructors) = strip_comb missing
3001     val fvs = free_varsl constructors
3002     val arg_names = map (implode o base26 o fst) (enumerate 0 constructors)
3004                     arg_names constructors
3008         (zip args constructors)
3013                     " has no constructors."))
3162 (*               of constructors, rather than their absense, eg.:            *)
3164 (*         5) Generation of extra limit theorems for nested constructors     *)