theory Very_Deep_Interpretation
  imports "Isabelle_DOF.Isa_COL"
          Metalogic_ProofChecker.ProofTerm

begin

subsection\<open> Syntax \<close>

\<comment> \<open>and others in the future : file, http, thy, ...\<close> 

(* Delete shallow interpretation notations (mixfixes) of the term anti-quotations,
  so we can use them for the deep interpretation *)
no_notation "ISA_typ" ("@{typ _}")
no_notation "ISA_term" ("@{term _}")
no_notation "ISA_thm" ("@{thm _}")
no_notation "ISA_file" ("@{file _}")
no_notation "ISA_thy" ("@{thy _}")
no_notation "ISA_docitem" ("@{docitem _}")
no_notation "ISA_docitem_attr" ("@{docitemattr (_) :: (_)}")
no_notation "ISA_trace_attribute" ("@{trace-attribute _}")

consts ISA_typ :: "string \<Rightarrow> typ" ("@{typ _}")
consts ISA_term :: "string \<Rightarrow> term" ("@{term _}")
consts ISA_term_repr    :: "string \<Rightarrow> term"              ("@{termrepr _}")
datatype "thm" = ISA_thm string ("@{thm _}") | Thm_content ("proof":proofterm)
datatype "thms_of" = ISA_thms_of string ("@{thms-of _}")
datatype "file" = ISA_file string  ("@{file _}")
datatype "thy" = ISA_thy string  ("@{thy _}")
consts ISA_docitem      :: "string \<Rightarrow> 'a"                ("@{docitem _}")
datatype "docitem_attr" = ISA_docitem_attr string  string ("@{docitemattr (_) :: (_)}")
consts ISA_trace_attribute :: "string \<Rightarrow> (string * string) list" ("@{trace-attribute _}")

subsection\<open> Semantics \<close>

ML\<open>
structure ISA_core = 
struct

fun check_path check_file ctxt dir (name, pos) =
  let
    val _ = Context_Position.report ctxt pos (Markup.language_path true); (* TODO: pos should be 
                                                                                   "lifted" to 
                                                                                   type source *)

    val path = Path.append dir (Path.explode name) handle ERROR msg => ISA_core.err msg pos;
    val _ = Path.expand path handle ERROR msg => ISA_core.err msg pos;
    val _ = Context_Position.report ctxt pos (Markup.path (Path.implode_symbolic path));
    val _ =
      (case check_file of
        NONE => path
      | SOME check => (check path handle ERROR msg => ISA_core.err msg pos));
  in path end;


fun ML_isa_antiq check_file thy (name, _, pos) =
  let val path = check_path check_file (Proof_Context.init_global thy) Path.current (name, pos);
  in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end;


fun ML_isa_check_generic check thy (term, pos) =
  let val name = (HOLogic.dest_string term
                  handle TERM(_,[t]) => error ("wrong term format: must be string constant: " 
                                               ^ Syntax.string_of_term_global thy t ))
      val _ = check thy (name,pos)
  in  SOME term end;  

fun check_identity _ (term, _, _) _ = SOME term

fun ML_isa_check_typ thy (term, _, pos) _ =
  let fun check thy (name, _) = let val ctxt = (Proof_Context.init_global thy)
                                in (Syntax.check_typ ctxt o Syntax.parse_typ ctxt) name end
  in  ML_isa_check_generic check thy (term, pos) end


fun ML_isa_check_term thy (term, _, pos) _ =
  let fun check thy (name, _) = let val ctxt = (Proof_Context.init_global thy)
                                in (Syntax.check_term ctxt o Syntax.parse_term ctxt) name end 
  in  ML_isa_check_generic check thy (term, pos) end


fun ML_isa_check_thm thy (term, _, pos) _ =
  (* this works for long-names only *)
  let fun check thy (name, _) = case Proof_Context.lookup_fact (Proof_Context.init_global thy) name of
                                  NONE => ISA_core.err ("No Theorem:" ^name) pos
                                | SOME X => X
  in   ML_isa_check_generic check thy (term, pos) end


fun ML_isa_check_file thy (term, _, pos) _ =
  let fun check thy (name, pos) = check_path (SOME File.check_file) 
                                             (Proof_Context.init_global thy) 
                                             (Path.current) 
                                             (name, pos);
  in  ML_isa_check_generic check thy (term, pos) end;

fun ML_isa_id thy (term,pos) = SOME term


fun ML_isa_check_docitem thy (term, req_ty, pos) _ =
  let fun check thy (name, _) s =
           if DOF_core.is_declared_oid_global name thy 
           then case DOF_core.get_object_global name thy of
                    NONE => warning("oid declared, but not yet defined --- "^
                                    " type-check incomplete")
                 |  SOME {pos=pos_decl,cid,id,...} => 
                         let val ctxt = (Proof_Context.init_global thy)
                             val req_class = case req_ty of 
                                         \<^Type>\<open>fun _ T\<close> => DOF_core.typ_to_cid T
                                       | _ => error("can not infer type for: "^ name)
                         in if cid <> DOF_core.default_cid 
                               andalso not(DOF_core.is_subclass ctxt cid req_class)
                            then error("reference ontologically inconsistent: "
                                       ^cid^" vs. "^req_class^ Position.here pos_decl)
                            else ()
                         end
           else ISA_core.err ("faulty reference to docitem: "^name) pos
  in  ML_isa_check_generic check thy (term, pos) end

fun ML_isa_check_trace_attribute thy (term, _, pos) s =
  let
    fun check thy (name, _)  =
      case DOF_core.get_object_global name thy of
          NONE =>  ISA_core.err ("No class instance: " ^ name) pos
        | SOME(_) => ()
  in ML_isa_check_generic check thy (term, pos) end

fun ML_isa_elaborate_generic (_:theory) isa_name ty term_option _ =
  case term_option of
      NONE => error("Wrong term option. You must use a defined term")
    | SOME term => Const (isa_name, ty) $ term

fun reify_typ (Type (s, typ_list)) =
      \<^Const>\<open>Ty\<close> $ HOLogic.mk_literal s $ HOLogic.mk_list \<^Type>\<open>typ\<close> (map reify_typ typ_list)
  | reify_typ (TFree (name, sort)) =
      \<^Const>\<open>Tv\<close> $(\<^Const>\<open>Free\<close> $ HOLogic.mk_literal name)
      $ (HOLogic.mk_set \<^typ>\<open>class\<close> (map HOLogic.mk_literal sort))
  | reify_typ (TVar (indexname, sort)) =
      let val (name, index_value) = indexname
      in  \<^Const>\<open>Tv\<close>
          $ (\<^Const>\<open>Var\<close>
             $ HOLogic.mk_prod (HOLogic.mk_literal name, HOLogic.mk_number \<^Type>\<open>int\<close> index_value))
          $ (HOLogic.mk_set \<^typ>\<open>class\<close> (map HOLogic.mk_literal sort)) end

fun ML_isa_elaborate_typ (thy:theory) _ _ term_option _ =
  case term_option of
      NONE => error("Wrong term option. You must use a defined term")
    | SOME term => let 
                     val typ_name = HOLogic.dest_string term
                     val typ = Syntax.read_typ_global thy typ_name
                   in reify_typ typ end

fun reify_term (Const (name, typ)) =\<^Const>\<open>Ct\<close> $ HOLogic.mk_literal name $ reify_typ typ
  | reify_term (Free (name, typ)) =
      \<^Const>\<open>Fv\<close> $ (\<^Const>\<open>Free\<close> $ HOLogic.mk_literal name) $ reify_typ typ
  | reify_term (Var (indexname, typ)) =
      let val (name, index_value) = indexname
      in  \<^Const>\<open>Fv\<close>
          $ (\<^Const>\<open>Var\<close>
             $ HOLogic.mk_prod (HOLogic.mk_literal name, HOLogic.mk_number \<^Type>\<open>int\<close> index_value))
          $ reify_typ typ end
  | reify_term (Bound i) = \<^Const>\<open>Bv\<close> $ HOLogic.mk_nat i
  | reify_term (Abs (_, typ, term)) = \<^Const>\<open>Abs\<close> $ reify_typ typ $ reify_term term
  | reify_term (Term.$ (t1, t2)) = \<^Const>\<open>App\<close> $ reify_term t1 $ reify_term t2

fun ML_isa_elaborate_term (thy:theory) _ _ term_option _ =
  case term_option of
      NONE => error("Wrong term option. You must use a defined term")
    | SOME term => let 
                     val term_name = HOLogic.dest_string term
                     val term = Syntax.read_term_global thy term_name
                   in reify_term term end

fun reify_proofterm (PBound i) =\<^Const>\<open>PBound\<close> $ (HOLogic.mk_nat i)
  | reify_proofterm (Abst (_, typ_option, proof)) =
      \<^Const>\<open>Abst\<close> $ reify_typ (the typ_option) $ reify_proofterm proof
  | reify_proofterm (AbsP (_, term_option, proof)) =
      \<^Const>\<open>AbsP\<close> $ reify_term (the term_option) $ reify_proofterm proof
  | reify_proofterm (op % (proof, term_option)) =
      \<^Const>\<open>Appt\<close> $ reify_proofterm proof $ reify_term (the term_option)
  | reify_proofterm (op %% (proof1, proof2)) =
      \<^Const>\<open>AppP\<close> $ reify_proofterm proof1 $ reify_proofterm proof2
  | reify_proofterm (Hyp term) = \<^Const>\<open>Hyp\<close> $ (reify_term term)
  | reify_proofterm (PAxm (_, term, typ_list_option)) =
      let 
          val tvars = rev (Term.add_tvars term [])
          val meta_tvars = map (fn ((name, index_value), sort) =>
                HOLogic.mk_prod
                  (\<^Const>\<open>Var\<close>                    
                   $ HOLogic.mk_prod
                      (HOLogic.mk_literal name, HOLogic.mk_number \<^Type>\<open>int\<close> index_value)
                       , HOLogic.mk_set \<^typ>\<open>class\<close> (map HOLogic.mk_literal sort))) tvars
          val meta_typ_list = 
            HOLogic.mk_list @{typ "tyinst"} (map2 (fn x => fn y => HOLogic.mk_prod (x, y))
                                              meta_tvars (map reify_typ (the typ_list_option)))
      in \<^Const>\<open>PAxm\<close> $ reify_term term $ meta_typ_list end
  | reify_proofterm (PClass (typ, class)) =
      \<^Const>\<open>OfClass\<close> $ reify_typ typ $ HOLogic.mk_literal class
  | reify_proofterm (PThm ({prop = prop, types = types, ...}, _)) =
      let
        val tvars = rev (Term.add_tvars prop [])
        val meta_tvars = map (fn ((name, index_value), sort) =>
                HOLogic.mk_prod
                  (\<^Const>\<open>Var\<close>                    
                  $ HOLogic.mk_prod
                      (HOLogic.mk_literal name, HOLogic.mk_number \<^Type>\<open>int\<close> index_value)
                  , HOLogic.mk_set \<^typ>\<open>class\<close> (map HOLogic.mk_literal sort))) tvars
        val meta_typ_list = 
            HOLogic.mk_list \<^typ>\<open>tyinst\<close> (map2 (fn x => fn y => HOLogic.mk_prod (x, y))
                                          meta_tvars (map reify_typ (the types)))
      in \<^Const>\<open>PAxm\<close> $ reify_term prop $ meta_typ_list end

fun ML_isa_elaborate_thm (thy:theory) _ _ term_option pos =
  case term_option of
      NONE => ISA_core.err ("Malformed term annotation") pos
    | SOME term =>
        let
          val thm_name = HOLogic.dest_string term
          val _ = writeln ("In ML_isa_elaborate_thm thm_name: " ^ \<^make_string> thm_name)
          val thm = Proof_Context.get_thm (Proof_Context.init_global thy) thm_name
          val _ = writeln ("In ML_isa_elaborate_thm thm: " ^ \<^make_string> thm)
          val body = Proofterm.strip_thm_body (Thm.proof_body_of thm);
          val prf = Proofterm.proof_of body;
          (* Proof_Syntax.standard_proof_of reconstructs the proof and seems to rewrite
             the option arguments (with a value NONE) of the proof datatype constructors,
             at least for PAxm, with "SOME (typ/term)",
             allowing us the use the projection function "the".
             Maybe the function can deal with
             all the option types of the proof datatype constructors *)
          val proof = Proof_Syntax.standard_proof_of
                                   {full = true, expand_name = Thm.expand_name thm} thm
          val _ = writeln ("In ML_isa_elaborate_thm proof: " ^ \<^make_string> proof)
          (* After a small discussion with Simon Roßkopf, It seems preferable to use
             Thm.reconstruct_proof_of instead of Proof_Syntax.standard_proof_of
             whose operation is not well known.
             Thm.reconstruct_proof_of seems sufficient to have a reifiable PAxm
             in the metalogic. *)
          val proof' = Thm.reconstruct_proof_of thm 
        (*in \<^Const>\<open>Thm_content\<close> $ reify_proofterm prf end*)        
        (*in \<^Const>\<open>Thm_content\<close> $ reify_proofterm proof end*)
        in \<^Const>\<open>Thm_content\<close> $ reify_proofterm proof' end


fun ML_isa_elaborate_thms_of (thy:theory) _ _ term_option pos =
  case term_option of
      NONE => ISA_core.err ("Malformed term annotation") pos
    | SOME term =>
        let
          val thm_name = HOLogic.dest_string term
          val thm = Proof_Context.get_thm (Proof_Context.init_global thy) thm_name
          val body = Proofterm.strip_thm_body (Thm.proof_body_of thm)
          val all_thms_name = Proofterm.fold_body_thms (fn {name, ...} => insert (op =) name) [body] []
          (*val all_thms = map (Proof_Context.get_thm (Proof_Context.init_global thy)) all_thms_name*)
          (*val all_proofs = map (Proof_Syntax.standard_proof_of
                                   {full = true, expand_name = Thm.expand_name thm}) all_thms*)
        (*in HOLogic.mk_list \<^Type>\<open>thm\<close> (map (fn proof => \<^Const>\<open>Thm_content\<close> $ reify_proofterm proof) all_proofs) end*)
        in HOLogic.mk_list \<^typ>\<open>string\<close> (map HOLogic.mk_string all_thms_name) end

fun ML_isa_elaborate_trace_attribute (thy:theory) _ _ term_option pos =
case term_option of
    NONE => ISA_core.err ("Malformed term annotation") pos
  | SOME term => 
      let
        val oid = HOLogic.dest_string term
        val traces = ISA_core.compute_attr_access (Context.Theory thy) "trace" oid NONE pos
        fun conv (\<^Const>\<open>Pair \<^typ>\<open>doc_class rexp\<close> \<^typ>\<open>string\<close>\<close>
                    $ (\<^Const>\<open>Atom \<^typ>\<open>doc_class\<close>\<close> $ (\<^Const>\<open>mk\<close> $ s)) $ S) =
          let val s' =  DOF_core.read_cid (Proof_Context.init_global thy) (HOLogic.dest_string s)
          in \<^Const>\<open>Pair \<^typ>\<open>string\<close> \<^typ>\<open>string\<close>\<close> $ HOLogic.mk_string s' $ S end
        val traces' = map conv (HOLogic.dest_list traces)
      in HOLogic.mk_list \<^Type>\<open>prod \<^typ>\<open>string\<close> \<^typ>\<open>string\<close>\<close> traces' end

(* utilities *)

fun property_list_dest ctxt X =
  map (fn \<^Const_>\<open>ISA_term for s\<close> => HOLogic.dest_string s
         |\<^Const_>\<open>ISA_term_repr for s\<close> => holstring_to_bstring ctxt (HOLogic.dest_string s))
    (HOLogic.dest_list X)

end; (* struct *)

\<close>

ML\<open>
val ty1 = ISA_core.reify_typ @{typ "int"}
val ty2 = ISA_core.reify_typ @{typ "int \<Rightarrow> bool"}
val ty3 = ISA_core.reify_typ @{typ "prop"}
val ty4 = ISA_core.reify_typ @{typ "'a list"}
\<close>

ML\<open>
val t1 = ISA_core.reify_term @{term "1::int"}
val t2 = ISA_core.reify_term @{term "\<lambda>x. x = 1"}
val t3 = ISA_core.reify_term @{term "[2, 3::int]"}
\<close>

subsection\<open> Isar - Setup\<close>

setup\<open>DOF_core.update_isa_global("Very_Deep_Interpretation.typ",
                  {check=ISA_core.ML_isa_check_typ, elaborate=ISA_core.ML_isa_elaborate_typ}) \<close>
setup\<open>DOF_core.update_isa_global("Very_Deep_Interpretation.term",
                  {check=ISA_core.ML_isa_check_term, elaborate=ISA_core.ML_isa_elaborate_term}) \<close>
setup\<open>DOF_core.update_isa_global("Very_Deep_Interpretation.term_repr",
                    {check=ISA_core.check_identity, elaborate=ISA_core.ML_isa_elaborate_generic}) \<close>
setup\<open>DOF_core.update_isa_global("Very_Deep_Interpretation.thm.thm",
                  {check=ISA_core.ML_isa_check_thm, elaborate=ISA_core.ML_isa_elaborate_thm}) \<close>
setup\<open>DOF_core.update_isa_global("Very_Deep_Interpretation.thms_of.thms_of",
                  {check=ISA_core.ML_isa_check_thm, elaborate=ISA_core.ML_isa_elaborate_thms_of}) \<close>
setup\<open>DOF_core.update_isa_global("Very_Deep_Interpretation.file.file",
                  {check=ISA_core.ML_isa_check_file, elaborate=ISA_core.ML_isa_elaborate_generic}) \<close>
setup\<open>DOF_core.update_isa_global("Very_Deep_Interpretation.docitem",
              {check=ISA_core.ML_isa_check_docitem, elaborate=ISA_core.ML_isa_elaborate_generic}) \<close>
setup\<open>DOF_core.update_isa_global("Very_Deep_Interpretation.trace_attribute",
              {check=ISA_core.ML_isa_check_trace_attribute, elaborate=ISA_core.ML_isa_elaborate_trace_attribute}) \<close>

end