equal
deleted
inserted
replaced
43 |
43 |
44 |
44 |
45 (* Check for all sorts of errors in the input - nominal needs a different checking function *) |
45 (* Check for all sorts of errors in the input - nominal needs a different checking function *) |
46 fun nominal_check_defs ctxt fixes eqs = |
46 fun nominal_check_defs ctxt fixes eqs = |
47 let |
47 let |
|
48 val _ = tracing ("fixes: " ^ @{make_string} fixes) |
|
49 |
48 val fnames = map (fst o fst) fixes |
50 val fnames = map (fst o fst) fixes |
49 |
51 |
50 fun check geq = |
52 fun check geq = |
51 let |
53 let |
52 fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq]) |
54 fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq]) |
66 val _ = forall (not o Term.exists_subterm |
68 val _ = forall (not o Term.exists_subterm |
67 (fn Free (n, _) => member (op =) fnames n | _ => false)) (gs @ args) |
69 (fn Free (n, _) => member (op =) fnames n | _ => false)) (gs @ args) |
68 orelse input_error "Defined function may not occur in premises or arguments" |
70 orelse input_error "Defined function may not occur in premises or arguments" |
69 |
71 |
70 val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args |
72 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 |
73 val funvars = filter (fn q => |
|
74 exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs |
72 val _ = null funvars orelse (warning (cat_lines |
75 val _ = null funvars orelse (warning (cat_lines |
73 ["Bound variable" ^ plural " " "s " funvars ^ |
76 ["Bound variable" ^ plural " " "s " funvars ^ |
74 commas_quote (map fst funvars) ^ " occur" ^ plural "s" "" funvars ^ |
77 commas_quote (map fst funvars) ^ " occur" ^ plural "s" "" funvars ^ |
75 " in function position.", "Misspelled constructor???"]); true) |
78 " in function position.", "Misspelled constructor???"]); true) |
76 in |
79 in |
88 val _ = null not_defined |
91 val _ = null not_defined |
89 orelse error ("No defining equations for function" ^ |
92 orelse error ("No defining equations for function" ^ |
90 plural " " "s " not_defined ^ commas_quote not_defined) |
93 plural " " "s " not_defined ^ commas_quote not_defined) |
91 |
94 |
92 fun check_sorts ((fname, fT), _) = |
95 fun check_sorts ((fname, fT), _) = |
93 Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS) |
96 Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, @{sort "pt"}) |
94 orelse error (cat_lines |
97 orelse error (cat_lines |
95 ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":", |
98 ["Type of " ^ quote fname ^ " is not of sort " ^ quote "pt" ^ ":", |
96 Syntax.string_of_typ (Config.put show_sorts true ctxt) fT]) |
99 Syntax.string_of_typ (Config.put show_sorts true ctxt) fT]) |
97 |
100 |
98 val _ = map check_sorts fixes |
101 val _ = map check_sorts fixes |
99 in |
102 in |
100 () |
103 () |
142 val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0; |
145 val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0; |
143 val (eqs, post, sort_cont, cnames) = |
146 val (eqs, post, sort_cont, cnames) = |
144 empty_preproc nominal_check_defs config ctxt' fixes spec (* nominal *) |
147 empty_preproc nominal_check_defs config ctxt' fixes spec (* nominal *) |
145 |
148 |
146 val defname = mk_defname fixes |
149 val defname = mk_defname fixes |
147 val NominalFunctionConfig {partials, default, ...} = config |
150 val NominalFunctionConfig {partials, ...} = config |
148 val _ = |
|
149 if is_some default then Output.legacy_feature |
|
150 "'function (default)'. Use 'partial_function'." |
|
151 else () |
|
152 |
151 |
153 val ((goal_state, cont), lthy') = |
152 val ((goal_state, cont), lthy') = |
154 Nominal_Function_Mutual.prepare_nominal_function_mutual config defname fixes eqs lthy |
153 Nominal_Function_Mutual.prepare_nominal_function_mutual config defname fixes eqs lthy |
155 |
154 |
156 fun afterqed [[proof]] lthy = |
155 fun afterqed [[proof]] lthy = |