# HG changeset patch # User wenzelm # Date 1300804367 -3600 # Node ID 34f1d2d812843493eab3282653f38b586417c181 # Parent dbdd4790da343dd44cc13667701a3c84be95909e statespace syntax: strip positions -- type constraints are unexpected here; diff -r dbdd4790da34 -r 34f1d2d81284 src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Tue Mar 22 14:45:48 2011 +0100 +++ b/src/HOL/Statespace/state_space.ML Tue Mar 22 15:32:47 2011 +0100 @@ -623,7 +623,11 @@ then Syntax.const "StateFun.lookup" $ Syntax.const "undefined" $ Syntax.free n $ s else raise TERM ("StateSpace.gen_lookup_tr: component " ^ n ^ " not defined",[])); -fun lookup_tr ctxt [s,Free (n,_)] = gen_lookup_tr ctxt s n; +fun lookup_tr ctxt [s, x] = + (case Syntax.strip_positions x of + Free (n,_) => gen_lookup_tr ctxt s n + | _ => raise Match); + fun lookup_swap_tr ctxt [Free (n,_),s] = gen_lookup_tr ctxt s n; fun lookup_tr' ctxt [_$Free (prj,_),n as (_$Free (name,_)),s] = @@ -651,7 +655,10 @@ else raise TERM ("StateSpace.gen_update_tr: component " ^ n ^ " not defined",[])) end; -fun update_tr ctxt [s,Free (n,_),v] = gen_update_tr false ctxt n v s; +fun update_tr ctxt [s, x, v] = + (case Syntax.strip_positions x of + Free (n, _) => gen_update_tr false ctxt n v s + | _ => raise Match); fun update_tr' ctxt [_$Free (prj,_),_$Free (inj,_),n as (_$Free (name,_)),(Const (k,_)$v),s] = if Long_Name.base_name k = Long_Name.base_name KN then diff -r dbdd4790da34 -r 34f1d2d81284 src/Pure/Syntax/type_ext.ML --- a/src/Pure/Syntax/type_ext.ML Tue Mar 22 14:45:48 2011 +0100 +++ b/src/Pure/Syntax/type_ext.ML Tue Mar 22 15:32:47 2011 +0100 @@ -10,6 +10,7 @@ val term_sorts: term -> (indexname * sort) list val typ_of_term: (indexname -> sort) -> term -> typ val strip_positions: term -> term + val strip_positions_ast: Ast.ast -> Ast.ast val decode_term: (((string * int) * sort) list -> string * int -> sort) -> (string -> bool * string) -> (string -> string option) -> term -> term val term_of_typ: bool -> typ -> term @@ -115,6 +116,13 @@ | strip_positions (Abs (x, T, t)) = Abs (x, T, strip_positions t) | strip_positions t = t; +fun strip_positions_ast (Ast.Appl ((t as Ast.Constant c) :: u :: (v as Ast.Variable x) :: asts)) = + if (c = "_constrain" orelse c = "_constrainAbs") andalso is_some (Lexicon.decode_position x) + then Ast.mk_appl (strip_positions_ast u) (map strip_positions_ast asts) + else Ast.Appl (map strip_positions_ast (t :: u :: v :: asts)) + | strip_positions_ast (Ast.Appl asts) = Ast.Appl (map strip_positions_ast asts) + | strip_positions_ast ast = ast; + (* decode_term -- transform parse tree into raw term *)