summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Fri, 28 Oct 2011 15:38:41 +0200 | |

changeset 45289 | 25e9e7f527b4 |

parent 45288 | fc3c7db5bb2f |

child 45290 | f599ac41e7f5 |

slightly more explicit/syntactic modelling of morphisms;

--- a/src/Pure/Isar/element.ML Fri Oct 28 14:10:19 2011 +0200 +++ b/src/Pure/Isar/element.ML Fri Oct 28 15:38:41 2011 +0200 @@ -397,10 +397,10 @@ fun instT_morphism thy env = let val thy_ref = Theory.check_thy thy in Morphism.morphism - {binding = I, - typ = instT_type env, - term = instT_term env, - fact = map (fn th => instT_thm (Theory.deref thy_ref) env th)} + {binding = [I], + typ = [instT_type env], + term = [instT_term env], + fact = [map (fn th => instT_thm (Theory.deref thy_ref) env th)]} end; @@ -446,10 +446,10 @@ fun inst_morphism thy envs = let val thy_ref = Theory.check_thy thy in Morphism.morphism - {binding = I, - typ = instT_type (#1 envs), - term = inst_term envs, - fact = map (fn th => inst_thm (Theory.deref thy_ref) envs th)} + {binding = [], + typ = [instT_type (#1 envs)], + term = [inst_term envs], + fact = [map (fn th => inst_thm (Theory.deref thy_ref) envs th)]} end; @@ -467,10 +467,10 @@ (* rewriting with equalities *) fun eq_morphism thy thms = if null thms then NONE else SOME (Morphism.morphism - {binding = I, - typ = I, - term = Raw_Simplifier.rewrite_term thy thms [], - fact = map (Raw_Simplifier.rewrite_rule thms)}); + {binding = [], + typ = [], + term = [Raw_Simplifier.rewrite_term thy thms []], + fact = [map (Raw_Simplifier.rewrite_rule thms)]}); (* transfer to theory using closure *)

--- a/src/Pure/Isar/expression.ML Fri Oct 28 14:10:19 2011 +0200 +++ b/src/Pure/Isar/expression.ML Fri Oct 28 15:38:41 2011 +0200 @@ -501,7 +501,8 @@ val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export; val exp_term = Term_Subst.zero_var_indexes o Morphism.term export; val exp_typ = Logic.type_map exp_term; - val export' = Morphism.morphism {binding = I, typ = exp_typ, term = exp_term, fact = exp_fact}; + val export' = + Morphism.morphism {binding = [], typ = [exp_typ], term = [exp_term], fact = [exp_fact]}; in ((propss, deps, export'), goal_ctxt) end; in

--- a/src/Pure/assumption.ML Fri Oct 28 14:10:19 2011 +0200 +++ b/src/Pure/assumption.ML Fri Oct 28 15:38:41 2011 +0200 @@ -124,6 +124,6 @@ val thm = export false inner outer; val term = export_term inner outer; val typ = Logic.type_map term; - in Morphism.morphism {binding = I, typ = typ, term = term, fact = map thm} end; + in Morphism.morphism {binding = [], typ = [typ], term = [term], fact = [map thm]} end; end;

--- a/src/Pure/morphism.ML Fri Oct 28 14:10:19 2011 +0200 +++ b/src/Pure/morphism.ML Fri Oct 28 15:38:41 2011 +0200 @@ -16,6 +16,7 @@ signature MORPHISM = sig include BASIC_MORPHISM + type 'a funs = ('a -> 'a) list val binding: morphism -> binding -> binding val typ: morphism -> typ -> typ val term: morphism -> term -> term @@ -23,10 +24,10 @@ val thm: morphism -> thm -> thm val cterm: morphism -> cterm -> cterm val morphism: - {binding: binding -> binding, - typ: typ -> typ, - term: term -> term, - fact: thm list -> thm list} -> morphism + {binding: binding funs, + typ: typ funs, + term: term funs, + fact: thm list funs} -> morphism val binding_morphism: (binding -> binding) -> morphism val typ_morphism: (typ -> typ) -> morphism val term_morphism: (term -> term) -> morphism @@ -41,36 +42,39 @@ structure Morphism: MORPHISM = struct +type 'a funs = ('a -> 'a) list; +fun apply fs = fold_rev (fn f => fn x => f x) fs; + datatype morphism = Morphism of - {binding: binding -> binding, - typ: typ -> typ, - term: term -> term, - fact: thm list -> thm list}; + {binding: binding funs, + typ: typ funs, + term: term funs, + fact: thm list funs}; type declaration = morphism -> Context.generic -> Context.generic; -fun binding (Morphism {binding, ...}) = binding; -fun typ (Morphism {typ, ...}) = typ; -fun term (Morphism {term, ...}) = term; -fun fact (Morphism {fact, ...}) = fact; +fun binding (Morphism {binding, ...}) = apply binding; +fun typ (Morphism {typ, ...}) = apply typ; +fun term (Morphism {term, ...}) = apply term; +fun fact (Morphism {fact, ...}) = apply fact; val thm = singleton o fact; val cterm = Drule.cterm_rule o thm; val morphism = Morphism; -fun binding_morphism binding = morphism {binding = binding, typ = I, term = I, fact = I}; -fun typ_morphism typ = morphism {binding = I, typ = typ, term = I, fact = I}; -fun term_morphism term = morphism {binding = I, typ = I, term = term, fact = I}; -fun fact_morphism fact = morphism {binding = I, typ = I, term = I, fact = fact}; -fun thm_morphism thm = morphism {binding = I, typ = I, term = I, fact = map thm}; +fun binding_morphism binding = morphism {binding = [binding], typ = [], term = [], fact = []}; +fun typ_morphism typ = morphism {binding = [], typ = [typ], term = [], fact = []}; +fun term_morphism term = morphism {binding = [], typ = [], term = [term], fact = []}; +fun fact_morphism fact = morphism {binding = [], typ = [], term = [], fact = [fact]}; +fun thm_morphism thm = morphism {binding = [], typ = [], term = [], fact = [map thm]}; -val identity = morphism {binding = I, typ = I, term = I, fact = I}; +val identity = morphism {binding = [], typ = [], term = [], fact = []}; fun compose (Morphism {binding = binding1, typ = typ1, term = term1, fact = fact1}) (Morphism {binding = binding2, typ = typ2, term = term2, fact = fact2}) = - morphism {binding = binding1 o binding2, typ = typ1 o typ2, - term = term1 o term2, fact = fact1 o fact2}; + morphism {binding = binding1 @ binding2, typ = typ1 @ typ2, + term = term1 @ term2, fact = fact1 @ fact2}; fun phi1 $> phi2 = compose phi2 phi1;

--- a/src/Pure/variable.ML Fri Oct 28 14:10:19 2011 +0200 +++ b/src/Pure/variable.ML Fri Oct 28 15:38:41 2011 +0200 @@ -456,7 +456,7 @@ val fact = export inner outer; val term = singleton (export_terms inner outer); val typ = Logic.type_map term; - in Morphism.morphism {binding = I, typ = typ, term = term, fact = fact} end; + in Morphism.morphism {binding = [], typ = [typ], term = [term], fact = [fact]} end;