wenzelm@21476: (*  Title:      Pure/morphism.ML
wenzelm@21476:     Author:     Makarius
wenzelm@21476: 
wenzelm@21476: Abstract morphisms on formal entities.
wenzelm@21476: *)
wenzelm@21476: 
wenzelm@21476: infix 1 $>
wenzelm@21476: 
wenzelm@21476: signature BASIC_MORPHISM =
wenzelm@21476: sig
wenzelm@21476:   type morphism
wenzelm@24031:   type declaration = morphism -> Context.generic -> Context.generic
wenzelm@21476:   val $> : morphism * morphism -> morphism
wenzelm@21476: end
wenzelm@21476: 
wenzelm@21476: signature MORPHISM =
wenzelm@21476: sig
wenzelm@21476:   include BASIC_MORPHISM
haftmann@28965:   val var: morphism -> Binding.T * mixfix -> Binding.T * mixfix
haftmann@28965:   val binding: morphism -> Binding.T -> Binding.T
wenzelm@21476:   val typ: morphism -> typ -> typ
wenzelm@21476:   val term: morphism -> term -> term
wenzelm@21521:   val fact: morphism -> thm list -> thm list
wenzelm@21476:   val thm: morphism -> thm -> thm
wenzelm@22235:   val cterm: morphism -> cterm -> cterm
wenzelm@21476:   val morphism:
haftmann@28965:    {binding: Binding.T -> Binding.T,
haftmann@28965:     var: Binding.T * mixfix -> Binding.T * mixfix,
wenzelm@21476:     typ: typ -> typ,
wenzelm@21476:     term: term -> term,
wenzelm@21521:     fact: thm list -> thm list} -> morphism
haftmann@28965:   val binding_morphism: (Binding.T -> Binding.T) -> morphism
haftmann@28965:   val var_morphism: (Binding.T * mixfix -> Binding.T * mixfix) -> morphism
wenzelm@21492:   val typ_morphism: (typ -> typ) -> morphism
wenzelm@21492:   val term_morphism: (term -> term) -> morphism
wenzelm@21521:   val fact_morphism: (thm list -> thm list) -> morphism
wenzelm@21492:   val thm_morphism: (thm -> thm) -> morphism
wenzelm@21476:   val identity: morphism
wenzelm@22571:   val compose: morphism -> morphism -> morphism
wenzelm@22670:   val transform: morphism -> (morphism -> 'a) -> morphism -> 'a
wenzelm@22670:   val form: (morphism -> 'a) -> 'a
wenzelm@21476: end;
wenzelm@21476: 
wenzelm@21476: structure Morphism: MORPHISM =
wenzelm@21476: struct
wenzelm@21476: 
wenzelm@21476: datatype morphism = Morphism of
haftmann@28965:  {binding: Binding.T -> Binding.T,
haftmann@28965:   var: Binding.T * mixfix -> Binding.T * mixfix,
wenzelm@21476:   typ: typ -> typ,
wenzelm@21476:   term: term -> term,
wenzelm@21521:   fact: thm list -> thm list};
wenzelm@21476: 
wenzelm@24031: type declaration = morphism -> Context.generic -> Context.generic;
wenzelm@24031: 
haftmann@28965: fun binding (Morphism {binding, ...}) = binding;
wenzelm@21476: fun var (Morphism {var, ...}) = var;
wenzelm@21476: fun typ (Morphism {typ, ...}) = typ;
wenzelm@21476: fun term (Morphism {term, ...}) = term;
wenzelm@21521: fun fact (Morphism {fact, ...}) = fact;
wenzelm@21521: val thm = singleton o fact;
wenzelm@22235: val cterm = Drule.cterm_rule o thm;
wenzelm@21476: 
wenzelm@21476: val morphism = Morphism;
wenzelm@21476: 
haftmann@28965: fun binding_morphism binding = morphism {binding = binding, var = I, typ = I, term = I, fact = I};
haftmann@28965: fun var_morphism var = morphism {binding = I, var = var, typ = I, term = I, fact = I};
haftmann@28965: fun typ_morphism typ = morphism {binding = I, var = I, typ = typ, term = I, fact = I};
haftmann@28965: fun term_morphism term = morphism {binding = I, var = I, typ = I, term = term, fact = I};
haftmann@28965: fun fact_morphism fact = morphism {binding = I, var = I, typ = I, term = I, fact = fact};
haftmann@28965: fun thm_morphism thm = morphism {binding = I, var = I, typ = I, term = I, fact = map thm};
wenzelm@21492: 
haftmann@28965: val identity = morphism {binding = I, var = I, typ = I, term = I, fact = I};
wenzelm@21492: 
wenzelm@22571: fun compose
haftmann@28965:     (Morphism {binding = binding1, var = var1, typ = typ1, term = term1, fact = fact1})
haftmann@28965:     (Morphism {binding = binding2, var = var2, typ = typ2, term = term2, fact = fact2}) =
haftmann@28965:   morphism {binding = binding1 o binding2, var = var1 o var2,
wenzelm@21521:     typ = typ1 o typ2, term = term1 o term2, fact = fact1 o fact2};
wenzelm@21476: 
wenzelm@22571: fun phi1 $> phi2 = compose phi2 phi1;
wenzelm@21476: 
wenzelm@22670: fun transform phi f = fn psi => f (phi $> psi);
wenzelm@22670: fun form f = f identity;
wenzelm@22670: 
wenzelm@21476: end;
wenzelm@21476: 
wenzelm@21476: structure BasicMorphism: BASIC_MORPHISM = Morphism;
wenzelm@21476: open BasicMorphism;