Re: [isabelle] [isabelle-dev] Syntax.read_term ctxt



On Fri, 4 Mar 2011, e0726734 at student.tuwien.ac.at wrote:

structure Data = Proof_Data
  (type T = term list
   fun init _ = []);
val ctxt =
  ProofContext.init_global @{theory} |>
  Data.map (fn ts => @{term "x::int"}::ts);
#############################------######
Data.get ctxt;

Syntax.read_term ctxt "x + 1 = 2";
(* we get Free ("x", "'a") etc, but would expect ...
##############################----------------##
val it =
   Const ("HOL.eq", "Int.int \<Rightarrow> Int.int \<Rightarrow>
HOL.bool") $
     (Const ("Groups.plus_class.plus", "Int.int \<Rightarrow> Int.int
\<Rightarrow> Int.int") $
Free ("x", "Int.int") $ Const ("Groups.one_class.one", "Int.int")) $
#################------###################

###########################################################################-----####
(we would like to have Int.int here
##################################################################################

This is getting increasingly hard to read. Note that he private Data slot is really just a list of terms that the system maintains for you in Proof.context. Its meaning is determined by what you do with it in user code -- the system ignores it.

This means the Syntax.read_term produces a term according to the regular context, and there "x" is undeclared. So "x + 1 = 2" gets a very general type.


Here is an example (in Isabelle2011) that illustrates how to use the context for locally fixed variables, potentially with type constraints (these are two different things):

notepad
begin
  term "x + 1 = 2"  -- {* x undeclared; general type *}

  fix x :: int  -- {* x locally fixed, with type constraint *}
  term "x + 1 = 2"
end

notepad
begin
  ML_val {*
    val ctxt = @{context};
    val (_, ctxt') = ProofContext.add_fixes [(@{binding x}, SOME @{typ int}, NoSyn)] ctxt;
    val t = Syntax.read_term ctxt "x + 1 = 2";
    val t' = Syntax.read_term ctxt' "x + 1 = 2";
  *}
end

As a general principle, whenever there is some surprise about results it is often due to "bad context", cf. ctxt vs. ctxt' above.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.