(* Title:          mei.ml
   Author:         Jian Xu
   Affiliation:    Department of Computing and Software
                   McMaster University
   Date:           May 2007
*)

module type IDENT = sig
  type t

  val create: string -> t
  val name: t -> string
  val equal: t -> t -> bool
end

module Ident:IDENT = struct
  type t = {name: string; stamp: int}

  let currstamp = ref 0
  let create s = currstamp := !currstamp + 1;
                {name = s; stamp = !currstamp}
  let name id = id.name
  let equal id1 id2 = (id1.stamp = id2.stamp)
end

module type MMS_SYN = sig
  type language
  type mapping
  type sentence
  type proof

  val is_language: language -> bool
  val is_sentence: language -> sentence -> bool
  val is_mapping_of: language -> mapping -> bool
  val is_proof: language -> sentence list -> sentence*proof -> bool
  val empty_lang: language
  val merge_lang: language -> language -> language
  val is_sublang: language -> language -> bool
  val lift: language -> mapping -> mapping
  val inv: mapping -> mapping
  val find_ren_ext: language*language -> language*language -> mapping
  val find_ren_union: language*language -> language*language
                    -> mapping*mapping
  val language_translate: language -> mapping -> language
  val sentence_translate: sentence -> mapping -> sentence
  val proof_translate: proof -> mapping -> proof

  (*pretty printer*)
  val print_lang: language -> unit
  val print_mapping: mapping ->unit
  val print_sentence: sentence -> unit
  val print_proof: proof -> unit
end

module type MEICORE = sig
  module Mms:MMS_SYN
  type thy_type = {
    lang_type: Mms.language;
    axioms_type: (Ident.t * Mms.sentence) list}
  type mod_type =
    Base of thy_type
   |Arrow of mod_type * mod_type
  type spec = {
    lang_spec:Mms.language;
    axioms_spec:(Ident.t * Mms.sentence) list;
    thms_spec:(Ident.t * Mms.sentence * Mms.proof) list}
  type mod_expr =
     Ident of Ident.t
   | Theory of spec * thy_type
   | Cast of mod_expr * thy_type
   | Extension of mod_expr * spec
   | Rename of mod_expr * Mms.mapping
   | Union of mod_expr * mod_expr
   | Functor of Ident.t * mod_type * mod_expr
   | Apply of mod_expr * mod_expr

  val is_subtype: mod_type -> mod_type -> bool
  val is_thytype: thy_type -> bool
  val is_thy: spec -> bool
  val subst: mod_expr -> (Ident.t * mod_expr) -> mod_expr
  val is_thytype_of: spec -> thy_type -> bool
  val merge_thytype: thy_type -> thy_type -> thy_type
  val merge_spec: spec -> spec -> spec
  val amal_ext: spec * thy_type -> spec -> spec * thy_type
  val amal_union: (spec*thy_type) -> (spec*thy_type) -> (spec*thy_type)
  val thy_type_translate: thy_type -> Mms.mapping -> thy_type
  val spec_translate: spec -> Mms.mapping -> spec
  val print_thy_type: thy_type -> unit
  val print_type: mod_type -> unit
  val print_spec: spec -> unit
  val print_mod_expr: mod_expr -> unit
end

module MeiCore(TheMms: MMS_SYN) = struct
  module Mms = TheMms

  (*type definition is the same as in MEICORE*)
  type thy_type = {
     lang_type: Mms.language;
     axioms_type: (Ident.t * Mms.sentence) list}
  type mod_type =
     Base of thy_type
   | Arrow of mod_type * mod_type
  type spec = {
     lang_spec: Mms.language;
     axioms_spec: (Ident.t * Mms.sentence) list;
     thms_spec: (Ident.t * Mms.sentence * Mms.proof) list}
  type mod_expr =
     Ident of Ident.t
   | Theory of spec * thy_type
   | Cast of mod_expr * thy_type
   | Extension of mod_expr * spec
   | Rename of mod_expr * Mms.mapping
   | Union of mod_expr * mod_expr
   | Functor of Ident.t * mod_type * mod_expr
   | Apply of mod_expr * mod_expr

  (*auxiliary functions*)
  let subset l1 l2 = let p x = List.mem x l2 in List.for_all p l1
  let union l1 l2 = let p x = not (List.mem x l2)
                    in (List.filter p l1) @ l2
  let remove x l = let p y = not (x = y) in List.filter p l
  let empty l = match l with [] -> true | _ -> false

  (*functions for types*)
  let rec is_subtype modtype modtype' =
    match (modtype, modtype') with
      (Base thytype, Base thytype') ->
        Mms.is_sublang thytype'.lang_type thytype'.lang_type
        && subset thytype'.axioms_type thytype.axioms_type
    | (Arrow (modtype1, modtype2), Arrow (modtype1', modtype2')) ->
       is_subtype modtype1' modtype1 && is_subtype modtype2 modtype2'
    | _ -> false
  let is_thytype thytype =
    let (_, axioms) = List.split thytype.axioms_type in
    Mms.is_language thytype.lang_type &&
    List.for_all (Mms.is_sentence thytype.lang_type) axioms
  let merge_thytype thytype1 thytype2 =
    {lang_type = Mms.merge_lang thytype1.lang_type thytype2.lang_type;
    axioms_type = union thytype1.axioms_type thytype2.axioms_type}
  let thy_type_translate thytype rho =
    let new_lang = Mms.language_translate thytype.lang_type rho in
    let translate (id, phi) = (id, Mms.sentence_translate phi rho) in
    let new_axioms = List.map translate thytype.axioms_type in
    {lang_type = new_lang; axioms_type = new_axioms}

  (*functions for modules*)
  let is_thy spec =
    let (_, axioms) = List.split spec.axioms_spec in
    let is_thm (_, phi, pf) =
        Mms.is_proof spec.lang_spec axioms (phi, pf) in
        Mms.is_language spec.lang_spec &&
        List.for_all (Mms.is_sentence spec.lang_spec) axioms &&
        List.for_all is_thm spec.thms_spec
  let is_thytype_of spec thytype =
    let sen_of (n,thm,_) = (n,thm) in
    let thms = List.map sen_of spec.thms_spec in
    is_subtype (Base {lang_type = spec.lang_spec;
        axioms_type = spec.axioms_spec @ thms}) (Base thytype)
  let type_of_thy thy =
    Base {lang_type = thy.lang_spec;axioms_type = thy.axioms_spec}
  let merge_spec spec1 spec2 =
    {lang_spec = Mms.merge_lang spec1.lang_spec spec2.lang_spec;
    axioms_spec = union spec1.axioms_spec spec2.axioms_spec;
    thms_spec = union spec1.thms_spec spec2.thms_spec}
  let spec_translate spec rho =
    let new_lang = Mms.language_translate spec.lang_spec rho in
    let translate (id, phi) = (id, Mms.sentence_translate phi rho) in
    let new_axioms = List.map translate spec.axioms_spec in
    let translate' (id, phi, pf) =
        (id, Mms.sentence_translate phi rho,
        Mms.proof_translate pf rho) in
    let new_thms = List.map translate' spec.thms_spec in
    {lang_spec = new_lang; axioms_spec = new_axioms;
    thms_spec = new_thms}
  let amal_union (spec1, thytype1) (spec2, thytype2) =
    let (rho1, rho2) =
        Mms.find_ren_union (spec1.lang_spec, thytype1.lang_type)
        (spec2.lang_spec, thytype2.lang_type) in
    let (spec1', spec2') =
        (spec_translate spec1 rho1, spec_translate spec2 rho2) in
    (merge_spec spec1' spec2', merge_thytype thytype1 thytype2)
  let amal_ext (spec1, thytype1) spec2 =
    let sen_of (n,thm,_) = (n,thm) in
    let thms = List.map sen_of spec2.thms_spec in
    let thytype2 = {lang_type = spec2.lang_spec;
        axioms_type = union spec2.axioms_spec thms} in
    let rho1 = Mms.find_ren_ext (spec1.lang_spec, thytype1.lang_type)
        (spec2.lang_spec, thytype2.lang_type) in
    let spec1' = spec_translate spec1 rho1 in
    (merge_spec spec1' spec2, merge_thytype thytype1 thytype2)

  (*substitution function*)
  let rec subst me (id, me_sub) =
    match me with
     Ident id' -> if Ident.equal id id' then me_sub else me
   | Theory (thy,tp) -> me
   | Cast(me', tp) ->
       let me'' = subst me' (id, me_sub) in Cast(me'',tp)
   | Extension(me', spec) ->
       let me'' = subst me' (id, me_sub) in Extension(me'', spec)
   | Rename(me', rho) ->
       let me'' = subst me' (id, me_sub) in Rename(me'',rho)
   | Union(me1,me2) ->
       let me1' = subst me1 (id, me_sub) in
       let me2' = subst me2 (id, me_sub) in
       Union(me1',me2')
   | Functor(id', tp, me') ->
       if Ident.equal id id' then me
       else let me'' = subst me' (id, me_sub) in
       Functor(id', tp, me'')
   | Apply(me_f, me_p) ->
       let me_f' = subst me_f (id, me_sub) in
       let me_p' = subst me_p (id, me_sub) in
       Apply(me_f',me_p')

  (*pretty printer*)
  let print_thy_type thytype =
    print_string "{"; Mms.print_lang thytype.lang_type;
    print_string "\n"; print_string "Axioms:"; print_newline();
    let print_axiom (id, phi) =
      (print_string "\t";print_string (Ident.name id);print_string ":";
      Mms.print_sentence phi; print_newline() ) in
    List.iter print_axiom thytype.axioms_type;
    print_string "}"; print_newline()
  let rec print_type tp =
      match tp with
      Base thytype -> print_thy_type thytype
    | Arrow (tp1, tp2) -> print_string "{"; print_type tp1;
       print_string "}"; print_newline(); print_string " -> ";
       print_newline(); print_string "{"; print_type tp2;
       print_string "}"
  let print_spec spec =
    print_string "{"; Mms.print_lang spec.lang_spec; print_newline();
    print_string "Axioms:"; print_newline();
    let print_axiom (id, phi) = (print_string "\t";
      print_string (Ident.name id);print_string ": ";
      Mms.print_sentence phi; print_newline() ) in
    List.iter print_axiom spec.axioms_spec; print_newline();
    print_string "Theorems:";
    let print_theorem (id, phi, pf) = (print_string "\t";
      print_string (Ident.name id);print_string ": ";
      Mms.print_sentence phi; Mms.print_proof pf; print_newline()) in
    List.iter print_theorem spec.thms_spec; print_string "}";
    print_newline()
  let rec print_mod_expr me =
      match me with
      Ident id -> print_string (Ident.name id)
    | Theory (spec, thytype) -> print_spec spec; print_newline()
    | Cast (me',tp) -> print_string "(";
       print_thy_type tp; print_string ") "; print_string " ";
       print_mod_expr me'; print_newline()
    | Extension (me', spec) -> print_mod_expr me';
       print_string " extended by "; print_newline();
       print_spec spec; print_newline()
    | Rename (me', mp) -> print_mod_expr me';
       print_string " "; Mms.print_mapping mp; print_newline()
    | Union (me1, me2) -> print_mod_expr me1;  print_string " + ";
       print_mod_expr me2; print_newline()
    | Functor (id, tp, me') -> print_string "Functor ";
       print_string (Ident.name id); print_string ":";
       print_type tp; print_string ". ";
       print_mod_expr me'; print_newline()
    | Apply (me1, me2) -> print_string "("; print_mod_expr me1;
       print_string " @ "; print_mod_expr me2; print_string ")";
       print_newline()
end

module type ENV = sig
  type mod_expr
  type mod_type
  type content
  type t = (Ident.t * content) list

  val empty: t
  val add_expr: Ident.t -> mod_expr -> t -> t
  val find_expr: Ident.t -> t -> mod_expr
  val mem_expr: Ident.t -> t -> bool
  val add_type: Ident.t -> mod_type -> t -> t
  val find_type: Ident.t -> t -> mod_type
  val mem_type: Ident.t -> t -> bool
end

module Env (TheMod:MEICORE) = struct
  type mod_expr = TheMod.mod_expr
  type mod_type = TheMod.mod_type
  type content = Mod of mod_expr | Type of mod_type
  type t = (Ident.t * content) list

  let empty = []
  let add_expr id modu env = (id, Mod modu)::env
  let add_type id tp env = (id, Type tp)::env
  let rec find id env = match env with
      [] -> raise Not_found
    | (id', cont) :: tl ->
        if Ident.equal id id' then cont else find id tl
  let find_expr id env =
    match find id env with
      Mod modu -> modu
    | _ -> raise Not_found
  let find_type id env =
    match find id env with
      Type tp -> tp
    | _ -> raise Not_found
  let rec mem_expr id env = match env with
      [] -> false
    | (id', Mod modu) :: tl ->
        if Ident.equal id id' then true else mem_expr id tl
    | (id', Type tp) :: tl -> mem_expr id tl
  let rec mem_type id env = match env with
      [] -> false
    | (id', Mod modu) :: tl -> mem_expr id tl
    | (id', Type tp) :: tl ->
        if Ident.equal id id' then true else mem_expr id tl
end

module type CTX = sig
  type mod_type
  type t = (Ident.t * mod_type) list

  val empty: t
  val add: Ident.t -> mod_type -> t -> t
  val find: Ident.t -> t -> mod_type
  val mem: Ident.t -> t -> bool
end

module Ctx (TheMod:MEICORE) = struct
  type mod_type = TheMod.mod_type
  type t = (Ident.t * mod_type) list

  let empty = []
  let add id modtype ctx = (id, modtype)::ctx
  let rec find id ctx = match ctx with
      [] -> raise Not_found
    | (id', modtype) :: tl ->
        if Ident.equal id id' then modtype else find id tl
  let rec mem id ctx = match ctx with
      [] -> false
    | (id', modtype) :: tl ->
        if Ident.equal id id' then true else mem id tl
end

module type MEICORE_EVAL = sig
  module Mms:MMS_SYN
  module Mod:MEICORE
  module Env:ENV with type mod_expr = Mod.mod_expr and
                    type mod_type = Mod.mod_type
  module Ctx:CTX with type mod_type = Mod.mod_type

  val type_of: Mod.mod_expr -> Ctx.t -> Env.t -> Mod.mod_type
  val eval: Mod.mod_expr -> Env.t -> Mod.mod_expr
  val print_type: Mod.mod_type -> unit
  val print_mod_expr: Mod.mod_expr -> unit
end

module MeiCore_Eval
  (TheMms:MMS_SYN)
  (TheModFunc: functor (TheMms:MMS_SYN) ->
    MEICORE with module Mms = TheMms)
  (TheEnvFunc: functor (TheMod:MEICORE) ->
    ENV with type mod_expr =  TheMod.mod_expr and
    type mod_type = TheMod.mod_type)
  (TheCtxFunc: functor (TheMod:MEICORE) ->
    CTX with type mod_type = TheMod.mod_type)
= struct
  module Mms = TheMms
  module Mod = TheModFunc(TheMms)
  module Env = TheEnvFunc(Mod)
  module Ctx = TheCtxFunc(Mod)
  exception MEICORE_EVAL of string

  (*auxiliary functions*)
  let subset l1 l2 = let p x = List.mem x l2 in List.for_all p l1
  let union l1 l2 = let p x = not (List.mem x l2) in
    (List.filter p l1) @ l2
  let remove x l = let p y = not (x = y) in List.filter p l
  let empty l = match l with [] -> true | _ -> false

  (*type checking function*)
  let rec type_of te ctx env =
     match te with
     Mod.Ident id -> if Ctx.mem id ctx then Ctx.find id ctx
       else (if Env.mem_expr id env
       then type_of (Env.find_expr id env) ctx env
       else raise (MEICORE_EVAL "Module identity not defined."))
   | Mod.Theory (thy, thytype) ->
       if ((Mod.is_thy thy) && (Mod.is_thytype thytype)
        && Mod.is_thytype_of thy thytype)
       then Mod.Base thytype
       else raise(MEICORE_EVAL "Theory definition not closed.")
   | Mod.Cast(te', thytype) -> if Mod.is_thytype thytype then
       (match type_of te' ctx env with
         Mod.Base thytype' ->
           if (Mod.is_subtype (Mod.Base thytype') (Mod.Base thytype))
           then Mod.Base thytype
           else raise (MEICORE_EVAL "Invalid casting.")
       | _ -> raise (MEICORE_EVAL "Funtors cannot be casted."))
        else raise (MEICORE_EVAL "Theory type definition not closed.")
   | Mod.Extension(te',spec) -> (match type_of te' ctx env with
         Mod.Base thytype ->
           let thy_of_thytype = {Mod.lang_spec = thytype.Mod.lang_type;
             Mod.axioms_spec = thytype.Mod.axioms_type;
             Mod.thms_spec = []} in
           if (Mod.is_thy (Mod.merge_spec thy_of_thytype spec))
           then let get_axiom (id, phi, pf) = (id, phi) in
             let thytype' = {Mod.lang_type = spec.Mod.lang_spec;
               Mod.axioms_type = union spec.Mod.axioms_spec
               (List.map get_axiom spec.Mod.thms_spec)} in
             Mod.Base (Mod.merge_thytype thytype thytype')
           else raise (MEICORE_EVAL "The result theory is not closed")
       | _ -> raise (MEICORE_EVAL "Functor cannot be extended."))
   | Mod.Rename (te', rho) -> (match type_of te' ctx env with
         Mod.Base thytype ->
           if Mms.is_mapping_of thytype.Mod.lang_type rho
           then Mod.Base (Mod.thy_type_translate thytype rho)
           else raise (MEICORE_EVAL "Bad renaming.")
       | _ -> raise (MEICORE_EVAL "Functors cannot be renamed."))
   | Mod.Union(te1,te2) ->
       (match (type_of te1 ctx env, type_of te2 ctx env) with
         (Mod.Base thytype1, Mod.Base thytype2) ->
            Mod.Base (Mod.merge_thytype thytype1 thytype2)
       | _ -> raise (MEICORE_EVAL "Functors cannot be merged."))
   | Mod.Functor(id, tp, te') -> let ctx' = Ctx.add id tp ctx in
        Mod.Arrow (tp, type_of te' ctx' env)
   | Mod.Apply(te_f, te_p) -> (match type_of te_f ctx env with
         Mod.Arrow(tp_1,tp_2) ->
           if Mod.is_subtype (type_of te_p ctx env) tp_1
           then tp_2
           else raise (MEICORE_EVAL
             "Type mismatched in functor application.")
       | _ -> raise (MEICORE_EVAL
         "Functor required for functor application."))

  let rec eval te env =
    match te with
     Mod.Ident id -> if Env.mem_expr id env
       then let te' = Env.find_expr id env in eval te' env
       else Mod.Ident id
   | Mod.Theory (thy,tp) -> te
   | Mod.Cast(te', tp) -> let te_eval = eval te' env in
        (match  te_eval with
         Mod.Theory (spec,typtype) -> Mod.Theory (spec,tp)
       | _ -> Mod.Cast(te_eval, tp))
   | Mod.Extension(te',spec) -> let te_eval = eval te' env in
        (match te_eval with
          Mod.Theory (spec_eval, tp) -> let (new_spec, new_tp) =
            Mod.amal_ext (spec_eval,tp) spec in
            Mod.Theory (new_spec, new_tp)
       | _ -> Mod.Extension(te_eval, spec))
   | Mod.Rename(te', rho) -> let te_eval = eval te' env in
        (match te_eval with
          Mod.Theory (spec, thytype) -> Mod.Theory
            (Mod.spec_translate spec rho,
                Mod.thy_type_translate thytype rho)
       | _ -> Mod.Rename(te_eval, rho))
   | Mod.Union(te1,te2) -> let te1_eval = eval te1 env in
       let te2_eval = eval te2 env in
        (match (te1_eval, te2_eval) with
          (Mod.Theory (spec1,tp1), Mod.Theory (spec2,tp2)) ->
            let (new_spec, new_tp) =
              Mod.amal_union (spec1,tp1) (spec2,tp2)
            in Mod.Theory (new_spec, new_tp)
       | (_, _) -> Mod.Union(te1_eval, te2_eval))
   | Mod.Functor(id, tp, te') -> (match te' with
          Mod.Apply(te'', Mod.Ident id') -> if Ident.equal id id'
          then eval te'' env else Mod.Functor(id, tp, te')
       | _ -> Mod.Functor(id, tp, te'))
   | Mod.Apply(te_f, te_p) -> (match eval te_f env with
          Mod.Functor(id, tp, te') ->
            eval (Mod.subst te' (id, te_p)) env
       | _ -> raise (MEICORE_EVAL
         "Funtor required for functor application."))

  (*pretty printer*)
  let print_type = Mod.print_type
  let print_mod_expr = Mod.print_mod_expr
end

module type TRAN = sig
  module Mms: MMS_SYN
  module Mod: MEICORE

  val thm_from_obl: Mod.thy_type -> Mod.thy_type ->
    Mms.mapping -> (Ident.t * Mms.sentence * Mms.proof) list
end

module Tran
  (TheMms:MMS_SYN)
  (TheModFunc: functor (TheMms:MMS_SYN) ->
    MEICORE with module Mms = TheMms)
= struct
  module Mms = TheMms
  module Mod = TheModFunc(TheMms)

  let thm_from_obl thytype1 thytype rho = []
end

module type MEI = sig
  module Mms:MMS_SYN
  module Mod: MEICORE
  module Tran: TRAN

  type mappings = Single of Mms.mapping | Pair of mappings * mappings
  type view = Mod.mod_type * Mod.mod_type * mappings
  type mod_expr =
     Ident of Ident.t
   | Theory of Mod.spec * Mod.thy_type
   | Cast of mod_expr * Mod.thy_type
   | Extension of mod_expr * Mod.spec
   | Rename of mod_expr * Mms.mapping
   | Union of mod_expr * mod_expr
   | Functor of Ident.t * Mod.mod_type * mod_expr
   | Apply of mod_expr * mod_expr
   | V_Apply of mod_expr * mod_expr * view

  val coerce: mod_expr -> Mod.mod_expr
  val print_mod_expr: mod_expr -> unit
end

module Mei
  (TheMms: MMS_SYN)
  (TheModFunc: functor (TheMms:MMS_SYN) ->
    MEICORE with module Mms = TheMms)
  (TheTranFunc: functor (TheMms:MMS_SYN)
    -> functor (TheModFunc: functor (TheMms:MMS_SYN) ->
      MEICORE with module Mms = TheMms)
    -> TRAN with module Mms = TheMms and
      module Mod = TheModFunc(TheMms))
= struct
  exception MEI of string
  module Mms = TheMms
  module Mod = TheModFunc(TheMms)
  module Tran = TheTranFunc(TheMms)(TheModFunc)

  (*type definition is the same as in MEI*)
  type mappings = Single of Mod.Mms.mapping
    | Pair of mappings * mappings
  type view = Mod.mod_type * Mod.mod_type * mappings
  type mod_expr =
      Ident of Ident.t
    | Theory of Mod.spec * Mod.thy_type
    | Cast of mod_expr * Mod.thy_type
    | Extension of mod_expr * Mod.spec
    | Rename of mod_expr * Mms.mapping
    | Union of mod_expr * mod_expr
    | Functor of Ident.t * Mod.mod_type * mod_expr
    | Apply of mod_expr * mod_expr
    | V_Apply of mod_expr * mod_expr * view

  let rec functor_of_view v = match v with
      (Mod.Base thytype1, Mod.Base thytype2, Single rho) ->
        let rho' = Mod.Mms.lift thytype2.Mod.lang_type
          (Mod.Mms.inv rho) in
        let del = Tran.thm_from_obl thytype1 thytype2 rho in
        let idX = Ident.create("X") in
        let spec = {Mod.lang_spec = Mms.empty_lang;
          Mod.axioms_spec = []; Mod.thms_spec = del} in
        let me1 = Mod.Extension(Mod.Ident idX, spec) in
        let me2 = Mod.Rename(me1, rho') in
        let me3 = Mod.Cast(me2, thytype1) in
        Mod.Functor (idX, Mod.Base thytype2, me3)
    | (Mod.Arrow (type1, type2), Mod.Arrow (type1', type2'),
      Pair (rhos1, rhos2)) ->
        let c1 = functor_of_view (type1', type1,rhos1) in
        let c2 = functor_of_view (type2, type2',rhos2) in
        let idX = Ident.create("X") in
        let idF = Ident.create("F") in
        let me1 = Mod.Apply (c1, Mod.Ident idX) in
        let me2 = Mod.Apply (Mod.Ident idF, me1) in
        let me3 = Mod.Apply (c2, me2) in
        let me4 = Mod.Functor (idX, type1, me3) in
        Mod.Functor (idF, Mod.Arrow (type1', type2'), me4)
    | _ -> raise (MEI "Bad view")

  let rec coerce me = match me with
      Ident id -> Mod.Ident id
    | Theory (spec, tp) -> Mod.Theory (spec,tp)
    | Cast (me', btyp) -> Mod.Cast (coerce me', btyp)
    | Extension (me', spec) -> Mod.Extension (coerce me', spec)
    | Rename (me', rho) -> Mod.Rename (coerce me', rho)
    | Union (me1, me2) -> Mod.Union (coerce me1, coerce me2)
    | Functor (id, tp, me') -> Mod.Functor (id, tp, coerce me')
    | Apply (me_f, me_p) -> Mod.Apply (coerce me_f, coerce me_p)
    | V_Apply (me_f, me_p, v) ->
        Mod.Apply (coerce me_f,
          Mod.Apply (functor_of_view v, coerce me_p))

  (*pretty printer*)
  let rec print_mappings rhos = match rhos with
      Single rho -> Mms.print_mapping rho
    | Pair (rhos1, rhos2) -> print_string "(" ;
        print_mappings rhos1; print_string ", ";
        print_mappings rhos2;print_string ")"
  let print_view (tp1, tp2, mps) = (print_string "{";
    Mod.print_type tp2; print_string "}"; print_newline();
    print_string " as "; print_newline();
    print_string "{"; Mod.print_type tp1; print_string "}";
    print_string " by "; print_mappings mps)
  let rec print_mod_expr me =
      match me with
      Ident id -> print_string (Ident.name id)
    | Theory (spec, thytype) -> Mod.print_spec spec; print_newline()
    | Cast (me',tp) -> Mod.print_thy_type tp; print_string " ";
        print_mod_expr me'; print_newline()
    | Extension (me', spec) -> print_mod_expr me';
      print_string " extended by "; print_newline();
      Mod.print_spec spec; print_newline()
    | Rename (me', mp) -> print_mod_expr me';  print_string " ";
        Mms.print_mapping mp; print_newline()
    | Union (me1, me2) -> print_mod_expr me1;  print_string " + ";
        print_mod_expr me2; print_newline()
    | Functor (id, tp, me') -> print_string "Functor ";
        print_string (Ident.name id); print_string ":";
        Mod.print_type tp; print_string ". ";
        print_mod_expr me'; print_newline()
    | Apply (me1, me2) -> print_string "("; print_mod_expr me1;
        print_string " @ "; print_mod_expr me2;
        print_string ")"; print_newline()
    | V_Apply (me_f, me_p, v) -> print_string "("; print_mod_expr me_f;
        print_string " @ ";
        print_mod_expr me_p; print_string " with "; print_newline();
        print_view v; print_string "()"; print_newline()
end

module type NAME = sig
  type t

  val create: string -> t
  val generate_name: string -> t
  val name: t -> string
  val equal: t -> t -> bool
end

module Name : NAME = struct
  type t = string

  let newnum = ref 0
  let create s = s
  let generate_name s = newnum := !newnum + 1; s^(string_of_int !newnum)
  let name n = n
  let equal n1 n2 = (n1 = n2)
end

module Fol = struct
  exception FIRST_ORDER of string
  type sort = Name.t
  type const = Name.t * sort
  type func = Name.t * sort list * sort
  type pred = Name.t * sort list
  type variable = Ident.t * sort
  type term =
      Var of variable
    | Const of const
    | App of func * term list
  type formula =
      Eq of term * term
    | PredApp of pred * term list
    | And of formula * formula
    | Or of formula * formula
    | Imply of formula * formula
    | Nega of formula
    | Forall of variable * formula
    | Exist of variable * formula
  type language = {sorts: sort list; consts: const list;
    funcs: func list; preds: pred list}
  type mapping = {sm: (sort * sort) list; cm: (const * const) list;
    fm: (func * func) list; pm: (pred * pred) list}
  type sentence = formula
  type proof

  (*auxiliary functions*)
  let subset l1 l2 = let p x = List.mem x l2 in List.for_all p l1
  let union l1 l2 = let p x = not (List.mem x l2)
    in (List.filter p l1) @ l2
  let inter l1 l2 = let p x = (List.mem x l2) in (List.filter p l1)
  let diff l1 l2 = let p x = not (List.mem x l2) in (List.filter p l1)
  let remove x l = let p y = not (x = y) in List.filter p l
  let empty l = match l with [] -> true | _ -> false

  (*functions for language*)
  let empty_lang = {sorts = []; consts = []; funcs = []; preds = []}
  let is_lang sorts consts functions predicates =
    let is_const (name, s) = List.mem s sorts in
    let is_func (name, sl, s) = List.mem s sorts && subset sl sorts in
    let is_pred (name, sl) = subset sl sorts in
    List.for_all is_const consts && List.for_all is_func functions
        && List.for_all is_pred predicates
  let is_language lang =
    is_lang lang.sorts lang.consts lang.funcs lang.preds
  let is_sublang lang_1 lang_2 = is_language lang_1
    && is_language lang_2
    && (subset lang_1.sorts lang_2.sorts)
    && (subset lang_1.consts lang_2.consts)
    && (subset lang_1.funcs lang_2.funcs)
    && (subset lang_1.preds lang_2.preds)
  let eq_lang lang_1 lang_2 = (is_sublang lang_1 lang_2)
    && (is_sublang lang_2 lang_1)
  let rec merge_lang lang1 lang2 =
    let new_sorts = union lang1.sorts lang2.sorts in
    let new_consts = union lang1.consts lang2.consts in
    let new_funcs = union lang1.funcs lang2.funcs in
    let new_preds = union lang1.preds lang2.preds in
    {sorts = new_sorts; consts = new_consts;
      funcs = new_funcs; preds = new_preds}
  let language_translate lang rho =
    let image pair_list x = List.assoc x pair_list in {
    sorts = List.map (image rho.sm) lang.sorts;
    consts = List.map (image rho.cm) lang.consts;
    funcs = List.map (image rho.fm) lang.funcs;
    preds = List.map (image rho.pm) lang.preds}

  (*functions for mapping*)
  let sub_mapping rho1 rho2 = subset rho1.sm rho2.sm
    && subset rho1.cm rho2.cm && subset rho1.fm rho2.fm
    && subset rho1.pm rho2.pm
  let eq_mapping rho1 rho2 = sub_mapping rho1 rho2 && sub_mapping rho2 rho1
  let is_mapping rho =
    let sort_compatible s1 s2 = let s1' = List.assoc s1 rho.sm in
        Name.equal s1' s2 in
    let const_compatible ((name1, s1), (name2, s2)) =
      sort_compatible s1 s2 in
    let func_compatible ((name1,sl1,s1), (name2,sl2,s2)) =
      List.for_all2 sort_compatible sl1 sl2
        && sort_compatible s1 s2 in
    let pred_compatible ((name1,sl1), (name2,sl2)) =
        List.for_all2 sort_compatible sl1 sl2 in
    List.for_all const_compatible rho.cm
      && List.for_all func_compatible rho.fm
      && List.for_all pred_compatible rho.pm
  let source_of rho =
    let fst pair_list = let (sl,_) = List.split pair_list in sl
    in {sorts = fst rho.sm; consts = fst rho.cm;
      funcs = fst rho.fm; preds = fst rho.pm}
  let is_mapping_of lang rho = is_mapping rho
    && eq_lang lang (source_of rho)
  let rec lift lang rho =
    let find_diff list pair_list =
      let (sl,_) = List.split pair_list in
      let p x = not (List.mem x sl) in
      List.filter p list in
    let s_diff = find_diff lang.sorts rho.sm in
    let c_diff = find_diff lang.consts rho.cm in
    let f_diff = find_diff lang.funcs rho.fm in
    let p_diff = find_diff lang.preds rho.pm in
    let sm_diff = List.combine s_diff s_diff in
    let new_sm = rho.sm @ sm_diff in
    let find_image sort = List.assoc sort new_sm in
    let cm_diff =
      let make_const_pair (name, sort) =
        ((name,sort),(name, find_image sort)) in
      List.map make_const_pair c_diff in
    let fm_diff =
      let make_func_pair (name, sorts, sort) =
        ((name,sorts,sort),
          (name, List.map find_image sorts,find_image sort)) in
      List.map make_func_pair f_diff in
    let pm_diff =
      let make_pred_pair (name, sorts) =
        ((name,sorts),(name, List.map find_image sorts)) in
      List.map make_pred_pair p_diff in
    let new_cm = rho.cm @ cm_diff in
    let new_fm = rho.fm @ fm_diff in
    let new_pm = rho.pm @ pm_diff in
    {sm = new_sm; cm = new_cm; fm = new_fm; pm = new_pm}
  let inv rho = let rev (a,b) = (b,a) in
    {sm = List.map rev rho.sm;cm = List.map rev rho.cm;
    fm = List.map rev rho.fm;pm = List.map rev rho.pm}
  let find_ren_sort (sort_diff1, sort_comm1) (sort_diff2, sort_comm2)=
    let sort_candidate =
      diff (inter sort_diff1 sort_diff2)
        (inter sort_comm1 sort_comm2) in
    let make_pair s = (s, Name.generate_name (Name.name s)) in
    (List.map make_pair sort_candidate,
      List.map make_pair sort_candidate)
  let find_ren_const (const_diff1, const_comm1, rho_sm1)
    (const_diff2, const_comm2, rho_sm2) =
    let find_image s rho_sm = if List.mem_assoc s rho_sm
      then List.assoc s rho_sm else s in
    let change_const_sort rho_sm (n, s) = (n,find_image s rho_sm) in
    let new_const_diff1 =
      List.map (change_const_sort rho_sm1) const_diff1 in
    let new_const_diff2 =
      List.map (change_const_sort rho_sm2) const_diff2 in
    let const_candidate =
      diff (inter new_const_diff1 new_const_diff2)
        (inter const_comm1 const_comm2) in
    let make_pair (n, s) =
      ((n,s), (Name.generate_name (Name.name n), s)) in
    (List.map make_pair const_candidate,
      List.map make_pair const_candidate)
  let find_ren_func (func_diff1, func_comm1, rho_sm1)
    (func_diff2, func_comm2, rho_sm2) =
    let find_image s rho_sm = if List.mem_assoc s rho_sm
      then List.assoc s rho_sm else s in
    let change_func_sort rho_sm (n, sl, s) =
      (n, List.map (function s -> find_image s rho_sm)
        sl,find_image s rho_sm) in
    let new_func_diff1 =
      List.map (change_func_sort rho_sm1) func_diff1 in
    let new_func_diff2 =
      List.map (change_func_sort rho_sm2) func_diff2 in
    let func_candidate =
      diff (inter new_func_diff1 new_func_diff2)
        (inter func_comm1 func_comm2) in
    let make_pair (n, sl, s) =
      ((n,sl,s), (Name.generate_name (Name.name n), sl, s)) in
    (List.map make_pair func_candidate,
      List.map make_pair func_candidate)
  let find_ren_pred (pred_diff1, pred_comm1, rho_sm1)
    (pred_diff2, pred_comm2, rho_sm2) =
    let find_image s rho_sm = if List.mem_assoc s rho_sm
      then List.assoc s rho_sm else s in
    let change_pred_sort rho_sm (n, sl) =
      (n,List.map (function s -> find_image s rho_sm) sl) in
    let new_pred_diff1 =
      List.map (change_pred_sort rho_sm1) pred_diff1 in
    let new_pred_diff2 =
      List.map (change_pred_sort rho_sm2) pred_diff2 in
    let pred_candidate =
      diff (inter new_pred_diff1 new_pred_diff2)
        (inter pred_comm1 pred_comm2) in
    let make_pair (n, sl) =
      ((n,sl), (Name.generate_name (Name.name n), sl)) in
    (List.map make_pair pred_candidate,
      List.map make_pair pred_candidate)
  let find_ren_ext (lang_diff1, lang_comm1) (lang_diff2, lang_comm2)=
    let (rho_sm1, rho_sm2) =
      find_ren_sort (lang_diff1.sorts, lang_comm1.sorts)
        (lang_diff2.sorts, lang_comm2.sorts) in
    let (rho_cm1, rho_cm2) =
      find_ren_const (lang_diff1.consts, lang_comm1.consts, rho_sm1)
        (lang_diff2.consts, lang_comm2.consts, rho_sm2) in
    let (rho_fm1, rho_fm2) =
      find_ren_func (lang_diff1.funcs, lang_comm1.funcs, rho_sm1)
        (lang_diff2.funcs, lang_comm2.funcs, rho_sm2) in
    let (rho_pm1, rho_pm2) =
      find_ren_pred (lang_diff1.preds, lang_comm1.preds, rho_sm1)
        (lang_diff2.preds, lang_comm2.preds, rho_sm2) in
    lift lang_diff1 {sm=rho_sm1;cm=rho_cm1;fm=rho_fm1;pm=rho_pm1}
  let find_ren_union (lang_diff1,lang_comm1) (lang_diff2,lang_comm2) =
    let (rho_sm1, rho_sm2) =
      find_ren_sort (lang_diff1.sorts, lang_comm1.sorts)
        (lang_diff2.sorts, lang_comm2.sorts) in
    let (rho_cm1, rho_cm2) =
      find_ren_const (lang_diff1.consts, lang_comm1.consts, rho_sm1)
        (lang_diff2.consts, lang_comm2.consts, rho_sm2) in
    let (rho_fm1, rho_fm2) =
      find_ren_func (lang_diff1.funcs, lang_comm1.funcs, rho_sm1)
        (lang_diff2.funcs, lang_comm2.funcs, rho_sm2) in
    let (rho_pm1, rho_pm2) =
      find_ren_pred (lang_diff1.preds, lang_comm1.preds, rho_sm1)
        (lang_diff2.preds, lang_comm2.preds, rho_sm2) in
    (lift lang_diff1 {sm=rho_sm1;cm=rho_cm1;fm=rho_fm1;pm=rho_pm1},
      lift lang_diff2 {sm=rho_sm2;cm=rho_cm2;fm=rho_fm2;pm=rho_pm2})

  (*functions for sentence*)
  let rec is_term_of_lang lang t = match t with
      Var v -> true
    | Const c -> List.mem c lang.consts
    | App (f, t_list) -> List.mem f lang.funcs
      && List.for_all (is_term_of_lang lang) t_list
  let rec sort_of_term t = match t with
      Var (id, s) -> s
    | Const (name, s) -> s
    | App ((name, sl, s), t_list) ->
        if List.for_all2 sort_match sl t_list then s
        else raise (FIRST_ORDER
          "Arguments mismatched in function application.")
  and sort_match s t = Name.equal s (sort_of_term t)
  let is_sort_safe t = match t with
      Var v -> true
    | Const c -> true
    | App ((name, sl, s), t_list) ->
      List.for_all2 sort_match sl t_list
  let is_addmitted_term lang t =
    (is_term_of_lang lang t) && (is_sort_safe t)
  let rec var_of_term t = match t with
      Var v -> [v]
    | Const c -> []
    | App (f, t_list) -> let v_list = List.map var_of_term t_list in
        List.fold_left union [] v_list
  let rec term_translate t rho = match t with
      Var (id, s) -> Var (id, List.assoc s rho.sm)
    | Const c -> Const (List.assoc c rho.cm)
    | App (f, t_list) ->
        let t'_list =
          List.map (function tm -> term_translate tm rho) t_list in
        let f' = List.assoc f rho.fm in
        App (f', t'_list)
  let rec is_formula_of_lang lang phi = match phi with
      Eq (t,t') -> is_addmitted_term lang t
        && is_addmitted_term lang t'
        && Name.equal (sort_of_term t) (sort_of_term t')
    | PredApp ((name, sl), t_list) -> List.mem (name,sl) lang.preds
        && List.for_all (is_addmitted_term lang) t_list
        && List.for_all2 sort_match sl t_list
    | And (phi', phi'') -> is_formula_of_lang lang phi'
        && is_formula_of_lang lang phi''
    | Or (phi', phi'') -> is_formula_of_lang lang phi'
        && is_formula_of_lang lang phi''
    | Imply (phi', phi'') -> is_formula_of_lang lang phi'
        && is_formula_of_lang lang phi''
    | Nega phi' -> is_formula_of_lang lang phi'
    | Forall (x, phi') -> is_formula_of_lang lang phi'
    | Exist (x, phi') -> is_formula_of_lang lang phi'
  let rec var_of_formula phi = match phi with
      Eq (t,t') -> let var_set = var_of_term t in
        let var_set' = var_of_term t' in union var_set var_set'
    | PredApp (p, t_list) ->
        let var_set = List.map var_of_term t_list in
        List.fold_left union [] var_set
    | And (phi', phi'') -> let var_set' = var_of_formula phi' in
        let var_set'' = var_of_formula phi'' in
        union var_set' var_set''
    | Or (phi', phi'') -> let var_set' = var_of_formula phi' in
        let var_set'' = var_of_formula phi'' in
        union var_set' var_set''
    | Imply (phi', phi'') -> let var_set' = var_of_formula phi' in
        let var_set'' = var_of_formula phi'' in
        union var_set' var_set''
    | Nega phi' ->  var_of_formula phi'
    | Forall (x, phi') -> let var_set' = var_of_formula phi' in
        remove x var_set'
    | Exist (x, phi') ->  let var_set' = var_of_formula phi' in
        remove x var_set'
  let is_closed_formula lang phi =
    (is_formula_of_lang lang phi) && empty (var_of_formula phi)
  let is_sentence = is_closed_formula
  let rec formula_translate phi rho = match phi with
      Eq (t,t') -> let t_new = term_translate t rho in
        let t'_new = term_translate t' rho in Eq (t_new, t'_new)
    | PredApp (p, t_list) ->
        let t'_list =
          List.map (function t'' -> term_translate t'' rho) t_list in
        let p' = List.assoc p rho.pm in PredApp (p', t'_list)
    | And (phi', phi'') ->
        let phi'_new = formula_translate phi' rho in
        let phi''_new = formula_translate phi'' rho in
        And (phi'_new, phi''_new)
    | Or (phi', phi'') ->
        let phi'_new = formula_translate phi' rho in
        let phi''_new = formula_translate phi'' rho in
        Or (phi'_new, phi''_new)
    | Imply (phi', phi'') ->
        let phi'_new = formula_translate phi' rho in
        let phi''_new = formula_translate phi'' rho in
        Imply (phi'_new, phi''_new)
    | Nega phi' -> Nega (formula_translate phi' rho)
    | Forall ((id, s), phi') -> let s' = List.assoc s rho.sm in
        Forall ((id,s'), formula_translate phi' rho)
    | Exist ((id,s), phi') -> let s' = List.assoc s rho.sm in
        Exist ((id,s'), formula_translate phi' rho)
  let sentence_translate = formula_translate
  let is_proof lang axioms (phi, pf) = true
  let proof_translate pf rho = pf

  (*pretty printer*)
  let print_prod_sorts sorts =
    let rec print_help ss =
      match ss with
      [] -> ()
      | hd :: tl -> print_string (" * " ^ (Name.name hd));
          print_help tl
    in
    match sorts with
      [] -> ()
    | hd :: tl -> print_string (Name.name hd); print_help tl
  let print_lang lang =
    print_string "Language: "; print_newline();
    print_string("    ");print_string "Sorts:"; print_newline();
      let print_sort s =
        (print_string ("        " ^ (Name.name s));
        print_newline()) in
    List.iter print_sort lang.sorts;
    print_string("    ");print_string "Constants:"; print_newline();
      let print_const (name,s) =
        (print_string ("        " ^ (Name.name name) ^ "
          : " ^ (Name.name s));
        print_newline()) in
    List.iter print_const lang.consts;
    print_string("    ");print_string "Functions:"; print_newline();
      let print_func (name, sl, s) =
        (print_string ("        " ^ (Name.name name) ^ " : ");
        print_prod_sorts sl; print_string (" -> " ^ (Name.name s));
         print_newline())
      in
    List.iter print_func lang.funcs;
    print_string("    ");print_string "Predicates:"; print_newline();
      let print_pred (name, sl) =
        (print_string ("        " ^ (Name.name name) ^ " : ");
        print_prod_sorts sl; print_newline())
      in
    List.iter print_pred lang.preds
  let print_mapping rho =
    print_string "[";
      let print_sm (s1, s2) = (print_string (Name.name s1);
        print_string " |-> "; print_string (Name.name s2);
        print_string ",") in
    List.iter print_sm rho.sm;
      let print_const (name,s) = (print_string (Name.name name);
        print_string ": "; print_string (Name.name s)) in
      let print_cm (c1, c2) = print_const c1; print_string " |-> ";
        print_const c2; print_string "," in
    List.iter print_cm rho.cm;
      let print_func (name,sl,s) = (print_string (Name.name name);
        print_string ": "; print_prod_sorts sl;
        print_string " -> "; print_string (Name.name s))in
      let print_fm (f1, f2) = print_func f1; print_string " |-> ";
        print_func f2; print_string "," in
    List.iter print_fm rho.fm;
      let print_pred (name,sl) = (print_string (Name.name name);
        print_string ": "; print_prod_sorts sl) in
      let print_pm (p1, p2) = print_pred p1; print_string " |-> ";
        print_pred p2; print_string "," in
    List.iter print_pm rho.pm;
    print_string "]"
  let rec print_term t = match t with
       Var(v_id, _) -> print_string (Ident.name v_id)
     | Const(c_name, _) -> print_string (Name.name c_name)
     | App (f, ts) -> let (f_name, _, _) = f in
         print_string (Name.name f_name); print_string " ";
         print_string "("; print_terms ts; print_string ")"
  and print_terms ts = match ts with
       [] -> print_string ""
     | t :: tail -> print_term t;
     if List.length tail = 0 then ()
     else print_string ", "; print_terms tail
  let print_formula phi =
    let open_paren prec op_prec =
      if prec > op_prec then print_string "(" in
    let close_paren prec op_prec =
      if prec > op_prec then print_string ")" in
    let rec print prec phii =  (* prec is the current precedence *)
       match phii with
        Eq (t1, t2) -> print_term t1; print_string " = ";
          print_term t2
      | PredApp (pred, t_list) -> let (p_name, _) = pred in
          print_string (Name.name p_name); print_string " ";
          print_string "("; print_terms t_list; print_string ")"
      | And (phi1, phi2) ->
          open_paren prec 1;
          print 1 phi1; print_string " && "; print 1 phi2;
          close_paren prec 1
      | Or (phi1, phi2) ->
          open_paren prec 2;
          print 2 phi1; print_string " || "; print 2 phi2;
          close_paren prec 2
      | Imply (phi1, phi2) ->
          open_paren prec 0;
          print 0 phi1; print_string " --> "; print 0 phi2;
          close_paren prec 0
      | Nega phi1 ->
          open_paren prec 3;
          print_string " ! "; print 3 phi1;
          close_paren prec 3
      | Forall (v, phi1) ->
          let (id,_) = v in
          print_string " forall "; print_string (Ident.name id);
            print_string ". "; print 0 phi1
      | Exist (v, phi1) ->
          let (id,_) = v in
          print_string " exist "; print_string (Ident.name id);
          print_string ". "; print 0 phi1
    in
    print 0 phi
  let print_sentence = print_formula
  let print_proof pf = print_string "pseudo-proof"
end

module Fol_MeiCore = MeiCore(Fol) module Fol_MeiCore_Eval =

MeiCore_Eval(Fol)(MeiCore)(Env)(Ctx) module Fol_Mei =

Mei(Fol)(MeiCore)(Tran)


(*---------------------------------------------------------------------------------------*)
  (* The following is testing*)

  (*sort and multiplication symbol for "Mul"*)
  let mm_s = Name.create("mm")
  let mul_f_mul = (Name.create("mul"),[mm_s;mm_s],mm_s)

  (*sort, identity, multiplication, and inverse symbol for "group"*)
  let gg_s = Name.create("gg")
  let e_c = (Name.create("e"), gg_s)
  let mul_f_group = (Name.create("mul"),[gg_s;gg_s],gg_s)
  let inv_f_group = (Name.create("inv"),[gg_s],gg_s)

  let mul_lang =
    { Fol.sorts = [mm_s];
      Fol.consts = [];
      Fol.funcs = [mul_f_mul];
      Fol.preds = []
    }

  let group_lang =
    { Fol.sorts = [gg_s];
      Fol.consts = [e_c];
      Fol.funcs = [mul_f_group;inv_f_group];
      Fol.preds = []
    }

  let assoc_axiom =
        let x_var = (Ident.create("x"),gg_s) in
        let y_var = (Ident.create("y"),gg_s) in
        let z_var = (Ident.create("z"),gg_s) in
        (Ident.create("assoc"),
            Fol.Forall(x_var,
                Fol.Forall(y_var,
                    Fol.Forall(z_var,
                        Fol.Eq(
                            Fol.App(mul_f_group,[Fol.Var x_var;Fol.App(mul_f_group,[Fol.Var y_var;Fol.Var z_var])]),
                            Fol.App(mul_f_group,[Fol.App(mul_f_group,[Fol.Var x_var;Fol.Var y_var]);Fol.Var z_var])
                        )
                    )
                )
            )
        )

  let ident1_axiom =
        let x_var = (Ident.create("x"),gg_s) in
        (Ident.create("ident1"),
            Fol.Forall(x_var,
                Fol.Eq(
                    Fol.App(mul_f_group,[Fol.Var x_var;Fol.Const e_c]),
                    Fol.Var x_var
                )
            )
        )

  let ident2_axiom =
        let x_var = (Ident.create("x"),gg_s) in
        (Ident.create("ident2"),
            Fol.Forall(x_var,
                Fol.Eq(
                    Fol.App(mul_f_group,[Fol.Const e_c;Fol.Var x_var]),
                    Fol.Var x_var
                )
            )
        )

  let inv1_axiom =
        let x_var = (Ident.create("x"),gg_s) in
        (Ident.create("inv1"),
            Fol.Forall(x_var,
                Fol.Eq(
                    Fol.App(mul_f_group,[Fol.Var x_var;Fol.App(inv_f_group,[Fol.Var x_var])]),
                    Fol.Const e_c
                )
            )
        )

  let inv2_axiom =
        let x_var = (Ident.create("x"),gg_s) in
        (Ident.create("inv2"),
            Fol.Forall(x_var,
                Fol.Eq(
                    Fol.App(mul_f_group,[Fol.App(inv_f_group,[Fol.Var x_var]);Fol.Var x_var]),
                    Fol.Const e_c
                )
            )
        )

  let comm_axiom =
        let x_var = (Ident.create("x"),mm_s) in
        let y_var = (Ident.create("y"),mm_s) in
        (Ident.create("comm"),
            Fol.Forall(x_var,
                Fol.Forall(y_var,
                    Fol.Eq(
                        Fol.App(mul_f_mul,[Fol.Var x_var;Fol.Var y_var]),
                        Fol.App(mul_f_mul,[Fol.Var y_var;Fol.Var x_var])
                    )
                )
            )
        )

  let group_axioms = [assoc_axiom;ident1_axiom;ident2_axiom;inv1_axiom;inv2_axiom]
  let map_group_mul = {Fol.sm = [(mm_s,gg_s)]; Fol.cm = [];
        Fol.fm = [(mul_f_mul,mul_f_group)]; Fol.pm = []}

  (*Definition of group type*)
  let group_type_spec = {Fol_MeiCore.lang_type = group_lang; Fol_MeiCore.axioms_type = group_axioms}
  let group_type = Fol_MeiCore.Base group_type_spec

  (*Definition of group theory*)
  let group_spec = {Fol_MeiCore.lang_spec = group_lang;Fol_MeiCore.axioms_spec = group_axioms; Fol_MeiCore.thms_spec = []}
  let group = Fol_Mei.Theory (group_spec, group_type_spec)

  (*Definition of mul type*)
  let mul_type_spec = {Fol_MeiCore.lang_type = mul_lang; Fol_MeiCore.axioms_type = []}
  let mul_type = Fol_MeiCore.Base mul_type_spec

  (*Definition of commutative functor*)
  let ext_comm = {Fol_MeiCore.lang_spec = Fol.empty_lang; Fol_MeiCore.axioms_spec = [comm_axiom]; Fol_MeiCore.thms_spec = []}
  let comm_functor = let mul_id = Ident.create("Mul") in
    Fol_Mei.Functor(mul_id, mul_type, Fol_Mei.Extension(Fol_Mei.Ident mul_id, ext_comm))

  (*Coerced group theory*)
  let group_coerced = Fol_Mei.coerce group

  (*Add coerced group theory to the env*)
  let id_g = Ident.create("Group")
  let env = Fol_MeiCore_Eval.Env.add_expr id_g group_coerced []

  (*Definition of view from mul type to group type*)
  let view_group_mul = (mul_type, group_type, Fol_Mei.Single map_group_mul)

  (*Definition of commutative group theory from functor application*)
  let comm_group = Fol_Mei.V_Apply(comm_functor, Fol_Mei.Ident id_g, view_group_mul)

  (*Coerced commutative group theory expression*)
  let comm_group_coerced = Fol_Mei.coerce comm_group

  (*Evaluated commutative group theory*)
  let comm_group_eval = Fol_MeiCore_Eval.eval comm_group_coerced env

(*  let print3 = Fol_MeiCore_Eval.print_mod_expr comm_group_eval; print_newline(); print_newline()*)

  (*Definition of funtor type of comm_functor*)
  let comm_mul_type_spec = {Fol_MeiCore.lang_type = mul_lang; Fol_MeiCore.axioms_type = [comm_axiom]}
  let comm_mul_type = Fol_MeiCore.Base comm_mul_type_spec
  let comm_functor_type = Fol_MeiCore.Arrow (mul_type, comm_mul_type)

  (*Definition of second order funtor apply_funtor*)
  let apply_functor = let comm_id = Ident.create("Comm") in
    let group_id = Ident.create("Group") in
    Fol_Mei.Functor(comm_id, comm_functor_type,
    Fol_Mei.Functor(group_id, group_type,
    Fol_Mei.V_Apply(Fol_Mei.Ident comm_id, Fol_Mei.Ident group_id, view_group_mul)))

  (*Definition of commutative group theory from second-order functor application*)
  let comm_group_2 = Fol_Mei.Apply(Fol_Mei.Apply(apply_functor, comm_functor), Fol_Mei.Ident id_g)
  (*Coerced commutative group theory expression*)
  let comm_group_coerced_2 = Fol_Mei.coerce comm_group_2
(*  let print1 = Fol_MeiCore_Eval.print_mod_expr comm_group_coerced_2; print_newline(); print_newline()*)

  let type_comm_group_coerced_2 = Fol_MeiCore_Eval.type_of comm_group_coerced_2 [] env
(*  let print2 = Fol_MeiCore_Eval.print_type type_comm_group_coerced_2; print_newline(); print_newline()*)

  (*Evaluated commutative group theory*)
  let comm_group_eval_2 = Fol_MeiCore_Eval.eval comm_group_coerced_2 env
(*  let print3 = Fol_MeiCore_Eval.print_mod_expr comm_group_eval_2; print_newline(); print_newline() *)


  (*identifier for sort ss for theory of set*)
  let set_s = Name.create("ss")
  (*set language*)
  let set_lang =
    { Fol.sorts = [set_s];
      Fol.consts = [];
      Fol.funcs = [];
      Fol.preds = []
    }

  (*Definition of set type*)
  let set_type_spec = {Fol_MeiCore.lang_type = set_lang; Fol_MeiCore.axioms_type = []}
  let set_type = Fol_MeiCore.Base set_type_spec

  (*Definition of set theory*)
  let set_spec = {Fol_MeiCore.lang_spec = set_lang; Fol_MeiCore.axioms_spec = [];Fol_MeiCore.thms_spec = []}
  let set_thy = Fol_Mei.Theory (set_spec, set_type_spec)

  (*the action function and axioms*)
  let act_f = (Name.create("act"),[gg_s;set_s],set_s)
  let act_ident_axiom =
        let x_var = (Ident.create("x"),set_s) in
        (Ident.create("act_ident"),
            Fol.Forall(x_var,
                Fol.Eq(
                    Fol.App(act_f,[Fol.Const e_c;Fol.Var x_var]),
                    Fol.Var x_var
                )
            )
        )

  let act_assoc_axiom =
        let x_var = (Ident.create("x"),set_s) in
        let g_var = (Ident.create("g"),gg_s) in
        let h_var = (Ident.create("h"),gg_s) in
        (Ident.create("act_assoc"),
            Fol.Forall(x_var,
                Fol.Forall(g_var,
                    Fol.Forall(h_var,
                        Fol.Eq(
                            Fol.App(act_f,[Fol.Var g_var;Fol.App(act_f,[Fol.Var h_var;Fol.Var x_var])]),
                            Fol.App(act_f,[Fol.App(mul_f_group,[Fol.Var g_var;Fol.Var h_var]);Fol.Var x_var])
                        )
                    )
                )
            )
        )

  (*Definition of extension for group action*)
  let ext_act_lang =
    { Fol.sorts = [];
      Fol.consts = [];
      Fol.funcs = [act_f];
      Fol.preds = []
    }
  let ext_act = {Fol_MeiCore.lang_spec = ext_act_lang; Fol_MeiCore.axioms_spec = [act_ident_axiom;act_assoc_axiom]; Fol_MeiCore.thms_spec = []}

  (*group action functor*)
  let act_functor = let group_id = Ident.create("Group") in
    let set_id = Ident.create("Set") in
    Fol_Mei.Functor(group_id, group_type, Fol_Mei.Functor(set_id, set_type,Fol_Mei.Extension(Fol_Mei.Union(Fol_Mei.Ident group_id,Fol_Mei.Ident set_id), ext_act)))
(*  let print4 = Fol_Mei.print_mod_expr act_functor; print_newline(); print_newline()*)

  (*Partially instantiated group action theory*)
  let group_act_partial = Fol_Mei.Apply (act_functor, (Fol_Mei.Ident id_g))
(*  let print5 = Fol_Mei.print_mod_expr group_act_partial; print_newline(); print_newline()*)

  (*Coerced partially instantiated group action theory*)
  let partial_act_functor_coerced = Fol_Mei.coerce group_act_partial
  let partial_act_functor_evaled = Fol_MeiCore_Eval.eval partial_act_functor_coerced env
(*  let print6 = Fol_MeiCore_Eval.print_mod_expr partial_act_functor_evaled; print_newline(); print_newline()*)

  (*Fully instantiated group action theory*)
  let group_act = Fol_Mei.Apply (group_act_partial, set_thy)
(*  let print7 = Fol_Mei.print_mod_expr group_act; print_newline(); print_newline()*)

  (*Coerced group action theory*)
  let group_act_coerced = Fol_Mei.coerce group_act
(*  let print8 = Fol_MeiCore_Eval.print_mod_expr group_act_coerced; print_newline(); print_newline()*)
  let group_act_evaled = Fol_MeiCore_Eval.eval group_act_coerced env
(*  let print9 = Fol_MeiCore_Eval.print_mod_expr group_act_evaled; print_newline(); print_newline()*)

  let map_group_set = {Fol.sm = [(set_s,gg_s)]; Fol.cm = [];
        Fol.fm = []; Fol.pm = []}
  let view_group_set = (set_type, group_type, Fol_Mei.Single map_group_set)
  let group_act_on_group = Fol_Mei.V_Apply(Fol_Mei.Apply (act_functor, (Fol_Mei.Ident id_g)), (Fol_Mei.Ident id_g), view_group_set)
  let group_act_on_group_coerced = Fol_Mei.coerce group_act_on_group
  let group_act_on_group_evaled = Fol_MeiCore_Eval.eval group_act_on_group_coerced env
(*  let print10 = Fol_MeiCore_Eval.print_mod_expr group_act_on_group_evaled; print_newline(); print_newline()*)

    (*COMMUTATIVE GROUP*)
  let print = Fol_Mei.print_mod_expr group; print_newline(); print_newline()
  let print = Fol_Mei.print_mod_expr comm_functor; print_newline(); print_newline()
  (*let comm_group = Fol_Mei.V_Apply(comm_functor, Fol_Mei.Ident id_g, view_group_mul)*)
(*  let print = Fol_Mei.print_mod_expr comm_group; print_newline(); print_newline()*)
  (*let comm_group_coerced = Fol_Mei.coerce comm_group*)
  (*let comm_group_eval = Fol_MeiCore_Eval.eval comm_group_coerced env*)
  let print = Fol_MeiCore_Eval.print_mod_expr comm_group_eval; print_newline(); print_newline()

    (*COMMUTATIVE GROUP -- 2nd FUNCTOR*)
(*  let print = Fol_Mei.print_mod_expr apply_functor; print_newline(); print_newline()*)
  (*let comm_group_2 = Fol_Mei.Apply(Fol_Mei.Apply(apply_functor, comm_functor), Fol_Mei.Ident id_g)*)
  (*let comm_group_coerced_2 = Fol_Mei.coerce comm_group_2*)
  (*let type_comm_group_coerced_2 = Fol_MeiCore_Eval.type_of comm_group_coerced_2 [] env*)
(*  let print = Fol_MeiCore_Eval.print_type type_comm_group_coerced_2; print_newline(); print_newline()*)
  (*let comm_group_eval_2 = Fol_MeiCore_Eval.eval comm_group_coerced_2 env*)
(*  let print = Fol_MeiCore_Eval.print_mod_expr comm_group_eval_2; print_newline(); print_newline()*)
  let type_comm_group_eval_2 = Fol_MeiCore_Eval.type_of comm_group_eval_2 [] env
(*  let print = Fol_MeiCore_Eval.print_type type_comm_group_eval_2; print_newline(); print_newline()*)


    (*GROUP ACTION*)
(*  let print = Fol_Mei.print_mod_expr act_functor; print_newline(); print_newline()*)
  (*let group_act_partial = Fol_Mei.Apply (act_functor, (Fol_Mei.Ident id_g))*)
  (*let partial_act_functor_coerced = Fol_Mei.coerce group_act_partial*)
  (*let partial_act_functor_evaled = Fol_MeiCore_Eval.eval partial_act_functor_coerced env*)
(*  let print = Fol_MeiCore_Eval.print_mod_expr partial_act_functor_evaled; print_newline(); print_newline()*)
  (*let group_act = Fol_Mei.Apply (group_act_partial, set_thy)*)
(*  let print = Fol_Mei.print_mod_expr group_act; print_newline(); print_newline()*)
  (*let group_act_coerced = Fol_Mei.coerce group_act*)
  (*let group_act_evaled = Fol_MeiCore_Eval.eval group_act_coerced env*)
(*  let print = Fol_MeiCore_Eval.print_mod_expr group_act_evaled; print_newline(); print_newline()*)


    (*GROUP ACTION OVER GROUPS*)
(*  let print = Fol_Mei.print_mod_expr group_act_on_group; print_newline(); print_newline()*)
  (*let group_act_on_group_coerced = Fol_Mei.coerce group_act_on_group*)
  (*let group_act_on_group_evaled = Fol_MeiCore_Eval.eval group_act_on_group_coerced env*)
(*  let print = Fol_MeiCore_Eval.print_mod_expr group_act_on_group_evaled; print_newline(); print_newline()*)