37 structure Nominal_Function : NOMINAL_FUNCTION = |
37 structure Nominal_Function : NOMINAL_FUNCTION = |
38 struct |
38 struct |
39 |
39 |
40 open Function_Lib |
40 open Function_Lib |
41 open Function_Common |
41 open Function_Common |
|
42 |
|
43 |
|
44 |
|
45 (* Check for all sorts of errors in the input - nominal needs a different checking function *) |
|
46 fun nominal_check_defs ctxt fixes eqs = |
|
47 let |
|
48 val fnames = map (fst o fst) fixes |
|
49 |
|
50 fun check geq = |
|
51 let |
|
52 fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq]) |
|
53 |
|
54 fun check_head fname = |
|
55 member (op =) fnames fname orelse |
|
56 input_error ("Illegal equation head. Expected " ^ commas_quote fnames) |
|
57 |
|
58 val (fname, qs, gs, args, rhs) = split_def ctxt check_head geq |
|
59 |
|
60 val _ = length args > 0 orelse input_error "Function has no arguments:" |
|
61 |
|
62 fun add_bvs t is = add_loose_bnos (t, 0, is) |
|
63 val rvs = (subtract (op =) (fold add_bvs args []) (add_bvs rhs [])) |
|
64 |> map (fst o nth (rev qs)) |
|
65 |
|
66 val _ = forall (not o Term.exists_subterm |
|
67 (fn Free (n, _) => member (op =) fnames n | _ => false)) (gs @ args) |
|
68 orelse input_error "Defined function may not occur in premises or arguments" |
|
69 |
|
70 val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args |
|
71 val funvars = filter (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs |
|
72 val _ = null funvars orelse (warning (cat_lines |
|
73 ["Bound variable" ^ plural " " "s " funvars ^ |
|
74 commas_quote (map fst funvars) ^ " occur" ^ plural "s" "" funvars ^ |
|
75 " in function position.", "Misspelled constructor???"]); true) |
|
76 in |
|
77 (fname, length args) |
|
78 end |
|
79 |
|
80 val grouped_args = AList.group (op =) (map check eqs) |
|
81 val _ = grouped_args |
|
82 |> map (fn (fname, ars) => |
|
83 length (distinct (op =) ars) = 1 |
|
84 orelse error ("Function " ^ quote fname ^ |
|
85 " has different numbers of arguments in different equations")) |
|
86 |
|
87 val not_defined = subtract (op =) (map fst grouped_args) fnames |
|
88 val _ = null not_defined |
|
89 orelse error ("No defining equations for function" ^ |
|
90 plural " " "s " not_defined ^ commas_quote not_defined) |
|
91 |
|
92 fun check_sorts ((fname, fT), _) = |
|
93 Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS) |
|
94 orelse error (cat_lines |
|
95 ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":", |
|
96 Syntax.string_of_typ (Config.put show_sorts true ctxt) fT]) |
|
97 |
|
98 val _ = map check_sorts fixes |
|
99 in |
|
100 () |
|
101 end |
|
102 |
|
103 |
42 |
104 |
43 val simp_attribs = map (Attrib.internal o K) |
105 val simp_attribs = map (Attrib.internal o K) |
44 [Simplifier.simp_add, |
106 [Simplifier.simp_add, |
45 Code.add_default_eqn_attribute, |
107 Code.add_default_eqn_attribute, |
46 Nitpick_Simps.add] |
108 Nitpick_Simps.add] |
76 let |
138 let |
77 val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx)) |
139 val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx)) |
78 val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy |
140 val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy |
79 val fixes = map (apfst (apfst Binding.name_of)) fixes0; |
141 val fixes = map (apfst (apfst Binding.name_of)) fixes0; |
80 val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0; |
142 val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0; |
81 val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec |
143 val (eqs, post, sort_cont, cnames) = empty_preproc nominal_check_defs config ctxt' fixes spec (* nominal *) |
82 |
144 |
83 val defname = mk_defname fixes |
145 val defname = mk_defname fixes |
84 val FunctionConfig {partials, default, ...} = config |
146 val FunctionConfig {partials, default, ...} = config |
85 val _ = |
147 val _ = |
86 if is_some default then Output.legacy_feature |
148 if is_some default then Output.legacy_feature |