From 91dc4798571fa99d68ced7ba098c958fca94c477 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sun, 10 Feb 2019 10:55:37 +0100
Subject: restructure library

---
 typing.ML | 104 ++------------------------------------------------------------
 1 file changed, 3 insertions(+), 101 deletions(-)

(limited to 'typing.ML')

diff --git a/typing.ML b/typing.ML
index 2a049d4..8c3d42c 100644
--- a/typing.ML
+++ b/typing.ML
@@ -6,73 +6,6 @@ Functionality for object-level type inference.
 
 ********)
 
-(* ====================================== Helper functions ====================================== *)
-
-signature TYPING_LIB =
-sig
-  (* Lexical functions *)
-  val unmark: string -> string
-  
-  (* General functions *)
-  val get_all_thms: Proof.context -> (string * thm) list
-  val find_thm: Proof.context -> string -> (string * thm) list
-  
-  (* Get specific theorems *)
-  val get_this: Proof.context -> thm list
-  val get_assms: Proof.context -> thm list
-end
-
-structure Typing_Lib: TYPING_LIB =
-struct
-
-fun unmark s =
-  Lexicon.unmark_class s
-  handle Fail "unprefix" =>
-  Lexicon.unmark_type s
-  handle Fail "unprefix" =>
-  Lexicon.unmark_const s
-  handle Fail "unprefix" =>
-  Lexicon.unmark_fixed s
-  handle Fail "unprefix" =>
-  s
-
-fun name_and_thm (fact, thm) =
-  ((case fact of
-    Facts.Named ((name, _), _) => name
-  | Facts.Fact name => name),
-  thm)
-
-fun get_all_thms ctxt =
-  let val (_, ref_thms) = Find_Theorems.find_theorems ctxt NONE NONE true []
-  in ref_thms |> (map name_and_thm)
-  end
-
-(* Search all visible theorems (including local assumptions) containing a given name *)
-fun find_thm ctxt name =
-  let val (_, ref_thms) =
-    Find_Theorems.find_theorems ctxt NONE NONE true [(true, Find_Theorems.Name name)]
-  in
-    ref_thms |> (map name_and_thm)
-  end
-
-(* Get the fact corresponding to the Isar term "this" in the current proof scope *)
-fun get_this ctxt =
-  Proof_Context.get_fact ctxt (Facts.named "local.this")
-  handle ERROR "Undefined fact: \"local.this\"" => (
-    if (Config.get ctxt trace) then warning "\"this\" undefined in the context" else ();
-    []
-  )
-
-(* Get all visible assumptions in the current proof scope.
-   This includes the facts introduced in the statement of the goal using "assumes",
-   as well as all facts introduced using "assume" that are visible in the current block.
- *)
-val get_assms = Assumption.all_prems_of
-
-end
-
-(* ================================ Type inference functionality ================================ *)
-
 signature TYPING =
 sig
   type jmt = term
@@ -91,8 +24,6 @@ sig
   val put_declared_typing: term -> theory -> theory
 
   val get_typing: Proof.context -> term -> term option
-
-  val prep_term: Proof.context -> term -> term
 end
 
 structure Typing: TYPING =
@@ -112,14 +43,14 @@ fun type_of_jmt (@{const HoTT_Base.has_type} $ _ $ T) = T
   | type_of_jmt _ = Exn.error "Not a typing judgment"
 
 (* Get typing assumptions in "this" *)
-fun typing_this ctxt = Typing_Lib.get_this ctxt |> map Thm.prop_of |> filter is_typing_jmt
+fun typing_this ctxt = Util.get_this ctxt |> map Thm.prop_of |> filter is_typing_jmt
 
 (* Get the typing assumptions in the current context *)
-val typing_assms = Typing_Lib.get_assms #> map Thm.prop_of #> filter is_typing_jmt
+val typing_assms = Util.get_assms #> map Thm.prop_of #> filter is_typing_jmt
 
 (* Get all visible typing judgments—Quick hack for now; should record them separately *)
 fun typing_all ctxt =
-  Typing_Lib.get_all_thms ctxt |> map (Thm.prop_of o snd) |> filter is_typing_jmt
+  Util.get_all_thms ctxt |> map (Thm.prop_of o snd) |> filter is_typing_jmt
 
 (* Search for a term typing in a list of judgments, and return the type if found.
    --
@@ -185,33 +116,4 @@ fun get_typing ctxt tm =
     NONE => get_declared_typing (Proof_Context.theory_of ctxt) tm
   | res => res
 
-(* Prepare a Pure pre-term, converting it partway to a (unchecked) term *)
-fun prep_term ctxt ptm =
-  let val ptm = Term_Position.strip_positions ptm
-  in
-  (case ptm of
-    Const ("_constrain", _) $ Free (t, _) $
-    (Const ("\<^type>fun", _) $ Const(typ1, _) $ Const (typ2, _)) =>
-      let
-        val typ1 = Lexicon.unmark_type typ1
-        val typ2 = Lexicon.unmark_type typ2
-        val typ = typ1 ^ "\<Rightarrow>" ^ typ2 |> Syntax.read_typ ctxt
-      in Free (t, typ) end
-  | Const ("_constrain", _) $ t $ Const (typ, _) =>
-      let 
-        val T = Syntax.read_typ ctxt (Lexicon.unmark_type typ)
-      in
-        case t of
-          Free (s, _) => Free (s, T)
-        | Const (s, _) => Const (Lexicon.unmark_const s, T)
-        | _ => Exn.error "Unimplemented term constraint handler"
-      end
-  | ptm1 $ ptm2 =>
-      (prep_term ctxt ptm1) $ (prep_term ctxt ptm2)
-  | Abs (t, T, ptm') =>
-      Abs (t, T, prep_term ctxt ptm')
-  | Const (t, T) => Const (Typing_Lib.unmark t, T)
-  | t => t)
-  end
-
 end
-- 
cgit v1.2.3