# HG changeset patch # User haftmann # Date 1399616006 -7200 # Node ID d651b944c67ee035d70959b45f98bf2927ede2f3 # Parent 6389a8c1268a82ec803d4f33304126e3a24455b9 normalizing of type variables before evaluation with explicit resubstitution function: make nbe work with funny type variables like \; tuned naming; dropped dead parameters; diff -r 6389a8c1268a -r d651b944c67e src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu May 08 21:17:23 2014 +0200 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri May 09 08:13:26 2014 +0200 @@ -305,9 +305,9 @@ fun dynamic_value_strict opts cookie ctxt postproc t = let - fun evaluator program ((_, vs_ty), t) deps = + fun evaluator program _ vs_ty_t deps = Exn.interruptible_capture (value opts ctxt cookie) - (Code_Target.evaluator ctxt target program deps true (vs_ty, t)); + (Code_Target.evaluator ctxt target program deps true vs_ty_t); in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_result o postproc) evaluator t) end; (** counterexample generator **) diff -r 6389a8c1268a -r d651b944c67e src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML Thu May 08 21:17:23 2014 +0200 +++ b/src/Tools/Code/code_preproc.ML Fri May 09 08:13:26 2014 +0200 @@ -24,14 +24,14 @@ val pretty: Proof.context -> code_graph -> Pretty.T val obtain: bool -> theory -> string list -> term list -> code_algebra * code_graph val dynamic_conv: Proof.context - -> (code_algebra -> code_graph -> (string * sort) list -> term -> conv) -> conv + -> (code_algebra -> code_graph -> term -> conv) -> conv val dynamic_value: Proof.context -> ((term -> term) -> 'a -> 'a) - -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a + -> (code_algebra -> code_graph -> term -> 'a) -> term -> 'a val static_conv: Proof.context -> string list - -> (code_algebra -> code_graph -> Proof.context -> (string * sort) list -> term -> conv) + -> (code_algebra -> code_graph -> Proof.context -> term -> conv) -> Proof.context -> conv val static_value: Proof.context -> ((term -> term) -> 'a -> 'a) -> string list - -> (code_algebra -> code_graph -> Proof.context -> (string * sort) list -> term -> 'a) + -> (code_algebra -> code_graph -> Proof.context -> term -> 'a) -> Proof.context -> term -> 'a val setup: theory -> theory @@ -462,17 +462,15 @@ (Wellsorted.change_yield (if ignore_cache then NONE else SOME thy) (extend_arities_eqngr (Proof_Context.init_global thy) consts ts)); -fun dest_cterm ct = let val t = Thm.term_of ct in (Term.add_tfrees t [], t) end; - fun dynamic_conv ctxt conv = no_variables_conv ctxt (fn ct => let val thm1 = preprocess_conv ctxt ctxt ct; val ct' = Thm.rhs_of thm1; - val (vs', t') = dest_cterm ct'; + val t' = Thm.term_of ct'; val consts = fold_aterms (fn Const (c, _) => insert (op =) c | _ => I) t' []; val (algebra', eqngr') = obtain false (Proof_Context.theory_of ctxt) consts [t']; - val thm2 = conv algebra' eqngr' vs' t' ct'; + val thm2 = conv algebra' eqngr' t' ct'; val thm3 = postprocess_conv ctxt ctxt (Thm.rhs_of thm2); in Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ => @@ -483,13 +481,12 @@ fun dynamic_value ctxt postproc evaluator t = let val (resubst, t') = preprocess_term ctxt ctxt t; - val vs' = Term.add_tfrees t' []; val consts = fold_aterms (fn Const (c, _) => insert (op =) c | _ => I) t' []; val (algebra', eqngr') = obtain false (Proof_Context.theory_of ctxt) consts [t']; in t' - |> evaluator algebra' eqngr' vs' + |> evaluator algebra' eqngr' |> postproc (postprocess_term ctxt ctxt o resubst) end; @@ -500,7 +497,7 @@ val conv' = conv algebra eqngr; val post_conv = postprocess_conv ctxt; in fn ctxt' => no_variables_conv ctxt' ((pre_conv ctxt') - then_conv (fn ct => uncurry (conv' ctxt') (dest_cterm ct) ct) + then_conv (fn ct => conv' ctxt' (Thm.term_of ct) ct) then_conv (post_conv ctxt')) end; @@ -513,7 +510,7 @@ in fn ctxt' => preproc ctxt' #-> (fn resubst => fn t => t - |> evaluator' ctxt' (Term.add_tfrees t []) + |> evaluator' ctxt' |> postproc (postproc' ctxt' o resubst)) end; diff -r 6389a8c1268a -r d651b944c67e src/Tools/Code/code_runtime.ML --- a/src/Tools/Code/code_runtime.ML Thu May 08 21:17:23 2014 +0200 +++ b/src/Tools/Code/code_runtime.ML Fri May 09 08:13:26 2014 +0200 @@ -112,8 +112,8 @@ val _ = if ! trace then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term ctxt t)) else () - fun evaluator program ((_, vs_ty), t) deps = - evaluation cookie ctxt (obtain_evaluator ctxt some_target program deps) (vs_ty, t) args; + fun evaluator program _ vs_ty_t deps = + evaluation cookie ctxt (obtain_evaluator ctxt some_target program deps) vs_ty_t args; in Code_Thingol.dynamic_value ctxt (Exn.map_result o postproc) evaluator t end; fun dynamic_value_strict cookie ctxt some_target postproc t args = @@ -126,7 +126,7 @@ let val evaluator = obtain_evaluator ctxt some_target program (map Constant consts'); val evaluation' = evaluation cookie ctxt evaluator; - in fn _ => fn ((_, vs_ty), t) => fn _ => evaluation' (vs_ty, t) [] end; + in fn _ => fn _ => fn vs_ty_t => fn _ => evaluation' vs_ty_t [] end; fun static_value_exn cookie ctxt some_target postproc consts = let @@ -175,14 +175,14 @@ (Thm.add_oracle (@{binding holds_by_evaluation}, fn (ctxt, evaluator, vs_t, ct) => check_holds ctxt evaluator vs_t ct))); -fun check_holds_oracle ctxt evaluator ((_, vs_ty), t) deps ct = - raw_check_holds_oracle (ctxt, evaluator, (vs_ty, t), ct); +fun check_holds_oracle ctxt evaluator vs_ty_t ct = + raw_check_holds_oracle (ctxt, evaluator, vs_ty_t, ct); in fun dynamic_holds_conv ctxt = Code_Thingol.dynamic_conv ctxt - (fn program => fn vs_t => fn deps => - check_holds_oracle ctxt (obtain_evaluator ctxt NONE program deps) vs_t deps) + (fn program => fn _ => fn vs_t => fn deps => + check_holds_oracle ctxt (obtain_evaluator ctxt NONE program deps) vs_t) o reject_vars ctxt; fun static_holds_conv ctxt consts = @@ -190,7 +190,7 @@ let val evaluator' = obtain_evaluator ctxt NONE program (map Constant consts') in - fn ctxt' => fn vs_t => fn deps => check_holds_oracle ctxt' evaluator' vs_t deps o reject_vars ctxt' + fn ctxt' => fn _ => fn vs_t => fn _ => check_holds_oracle ctxt' evaluator' vs_t o reject_vars ctxt' end); (* o reject_vars ctxt'*) diff -r 6389a8c1268a -r d651b944c67e src/Tools/Code/code_simp.ML --- a/src/Tools/Code/code_simp.ML Thu May 08 21:17:23 2014 +0200 +++ b/src/Tools/Code/code_simp.ML Fri May 09 08:13:26 2014 +0200 @@ -76,7 +76,7 @@ (* evaluation with dynamic code context *) fun dynamic_conv ctxt = Code_Thingol.dynamic_conv ctxt - (fn program => fn _ => fn _ => rewrite_modulo ctxt NONE program ctxt); + (fn program => fn _ => fn _ => fn _ => rewrite_modulo ctxt NONE program ctxt); fun dynamic_tac ctxt = CONVERSION (dynamic_conv ctxt) THEN' conclude_tac ctxt NONE ctxt; @@ -96,7 +96,7 @@ fun static_conv ctxt some_ss consts = Code_Thingol.static_conv_simple ctxt consts (fn program => let val conv' = rewrite_modulo ctxt some_ss program - in fn ctxt' => fn _ => fn _ => conv' ctxt' end); + in fn ctxt' => fn _ => conv' ctxt' end); fun static_tac ctxt some_ss consts = let diff -r 6389a8c1268a -r d651b944c67e src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Thu May 08 21:17:23 2014 +0200 +++ b/src/Tools/Code/code_target.ML Fri May 09 08:13:26 2014 +0200 @@ -428,7 +428,7 @@ else Isabelle_System.with_tmp_dir "Code_Test" ext_check end; -fun evaluation mounted_serializer prepared_program syms all_public ((vs, ty), t) = +fun subevaluator mounted_serializer prepared_program syms all_public ((vs, ty), t) = let val _ = if Code_Thingol.contains_dict_var t then error "Term to be evaluated contains free dictionaries" else (); @@ -449,7 +449,7 @@ let val (mounted_serializer, (_, prepared_program)) = mount_serializer ctxt target NONE generatedN [] program syms; - in evaluation mounted_serializer prepared_program syms end; + in subevaluator mounted_serializer prepared_program syms end; end; (* local *) diff -r 6389a8c1268a -r d651b944c67e src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Thu May 08 21:17:23 2014 +0200 +++ b/src/Tools/Code/code_thingol.ML Fri May 09 08:13:26 2014 +0200 @@ -86,20 +86,20 @@ val read_const_exprs: Proof.context -> string list -> string list val consts_program: theory -> string list -> program val dynamic_conv: Proof.context -> (program - -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> conv) + -> (string -> (string * sort)) -> typscheme * iterm -> Code_Symbol.T list -> conv) -> conv val dynamic_value: Proof.context -> ((term -> term) -> 'a -> 'a) -> (program - -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> 'a) + -> (string -> (string * sort)) -> typscheme * iterm -> Code_Symbol.T list -> 'a) -> term -> 'a val static_conv: Proof.context -> string list -> (program -> string list - -> Proof.context -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> conv) + -> Proof.context -> (string -> (string * sort)) -> typscheme * iterm -> Code_Symbol.T list -> conv) -> Proof.context -> conv val static_conv_simple: Proof.context -> string list - -> (program -> Proof.context -> (string * sort) list -> term -> conv) + -> (program -> Proof.context -> term -> conv) -> Proof.context -> conv val static_value: Proof.context -> ((term -> term) -> 'a -> 'a) -> string list -> (program -> string list - -> Proof.context -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> 'a) + -> Proof.context -> (string -> (string * sort)) -> typscheme * iterm -> Code_Symbol.T list -> 'a) -> Proof.context -> term -> 'a end; @@ -388,7 +388,7 @@ exception PERMISSIVE of unit; -fun translation_error ctxt program permissive some_thm deps msg sub_msg = +fun translation_error ctxt permissive some_thm deps msg sub_msg = if permissive then raise PERMISSIVE () else @@ -408,14 +408,14 @@ fun maybe_permissive f prgrm = f prgrm |>> SOME handle PERMISSIVE () => (NONE, prgrm); -fun not_wellsorted ctxt program permissive some_thm deps ty sort e = +fun not_wellsorted ctxt permissive some_thm deps ty sort e = let val err_class = Sorts.class_error (Context.pretty ctxt) e; val err_typ = "Type " ^ Syntax.string_of_typ ctxt ty ^ " not of sort " ^ Syntax.string_of_sort ctxt sort; in - translation_error ctxt program permissive some_thm deps + translation_error ctxt permissive some_thm deps "Wellsortedness error" (err_typ ^ "\n" ^ err_class) end; @@ -483,7 +483,7 @@ {class_relation = K (Sorts.classrel_derivation algebra class_relation), type_constructor = type_constructor, type_variable = type_variable} (ty, proj_sort sort) - handle Sorts.CLASS_ERROR e => not_wellsorted ctxt program permissive some_thm deps ty sort e; + handle Sorts.CLASS_ERROR e => not_wellsorted ctxt permissive some_thm deps ty sort e; in (typarg_witnesses, (deps, program)) end; @@ -630,7 +630,7 @@ val thy = Proof_Context.theory_of ctxt; val _ = if (case some_abs of NONE => true | SOME abs => not (c = abs)) andalso Code.is_abstr thy c - then translation_error ctxt program permissive some_thm deps + then translation_error ctxt permissive some_thm deps "Abstraction violation" ("constant " ^ Code.string_of_const thy c) else () in translate_const_proper ctxt algbr eqngr permissive some_thm (c, ty) (deps, program) end @@ -795,11 +795,18 @@ (* value evaluation *) -fun ensure_value ctxt algbr eqngr t = +fun normalize_tvars t = let val ty = fastype_of t; - val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =) + val vs_original = fold_term_types (K (fold_atyps (insert (eq_fst op =) o dest_TFree))) t []; + val vs_normalized = Name.invent_names Name.context Name.aT (map snd vs_original); + val normalize = map_type_tfree (TFree o the o AList.lookup (op =) (vs_original ~~ vs_normalized)); + in ((vs_original, (vs_normalized, normalize ty)), map_types normalize t) end; + +fun ensure_value ctxt algbr eqngr t_original = + let + val ((vs_original, (vs, ty)), t) = normalize_tvars t_original; val t' = annotate ctxt algbr eqngr (@{const_name Pure.dummy_pattern}, ty) [] t; val dummy_constant = Constant @{const_name Pure.dummy_pattern}; val stmt_value = @@ -808,29 +815,27 @@ ##>> translate_term ctxt algbr eqngr false NONE (t', NONE) #>> (fn ((vs, ty), t) => Fun (((vs, ty), [(([], t), (NONE, true))]), NONE)); - fun term_value (deps, program1) = + fun term_value (_, program1) = let - val Fun ((vs_ty, [(([], t), _)]), _) = + val Fun ((vs_ty as (vs, _), [(([], t), _)]), _) = Code_Symbol.Graph.get_node program1 dummy_constant; val deps' = Code_Symbol.Graph.immediate_succs program1 dummy_constant; val program2 = Code_Symbol.Graph.del_node dummy_constant program1; val deps_all = Code_Symbol.Graph.all_succs program2 deps'; val program3 = Code_Symbol.Graph.restrict (member (op =) deps_all) program2; - in ((program3, ((vs_ty, t), deps')), (deps, program2)) end; + val vs_mapping = map fst vs ~~ vs_original; + in (((the o AList.lookup (op =) vs_mapping), (program3, ((vs_ty, t), deps'))), (deps', program2)) end; in ensure_stmt Constant stmt_value @{const_name Pure.dummy_pattern} #> snd #> term_value end; -fun original_sorts vs = - map (fn (v, _) => (v, (the o AList.lookup (op =) vs o prefix "'") v)); - -fun dynamic_evaluator ctxt evaluator algebra eqngr vs t = +fun dynamic_evaluator ctxt evaluator algebra eqngr t = let - val ((program, (((vs', ty'), t'), deps)), _) = + val ((resubst_tvar, (program, ((vs_ty', t'), deps))), _) = invoke_generation false (Proof_Context.theory_of ctxt) (algebra, eqngr) ensure_value t; - in evaluator program ((original_sorts vs vs', (vs', ty')), t') deps end; + in evaluator program resubst_tvar (vs_ty', t') deps end; fun dynamic_conv ctxt conv = Code_Preproc.dynamic_conv ctxt (dynamic_evaluator ctxt conv); @@ -838,22 +843,22 @@ fun dynamic_value ctxt postproc evaluator = Code_Preproc.dynamic_value ctxt postproc (dynamic_evaluator ctxt evaluator); -fun lift_evaluation ctxt evaluation algebra eqngr program vs t = +fun static_subevaluator ctxt subevaluator algebra eqngr program t = let - val ((_, (((vs', ty'), t'), deps)), _) = + val ((resubst_tvar, (_, ((vs_ty', t'), deps))), _) = ensure_value ctxt algebra eqngr t ([], program); - in evaluation ctxt ((original_sorts vs vs', (vs', ty')), t') deps end; + in subevaluator ctxt resubst_tvar (vs_ty', t') deps end; -fun lift_evaluator ctxt evaluator consts algebra eqngr = +fun static_evaluator ctxt evaluator consts algebra eqngr = let fun generate_consts ctxt algebra eqngr = fold_map (ensure_const ctxt algebra eqngr false); val (consts', program) = invoke_generation true (Proof_Context.theory_of ctxt) (algebra, eqngr) generate_consts consts; - val evaluation = evaluator program consts'; - in fn ctxt' => lift_evaluation ctxt' evaluation algebra eqngr program end; + val subevaluator = evaluator program consts'; + in fn ctxt' => static_subevaluator ctxt' subevaluator algebra eqngr program end; -fun lift_evaluator_simple ctxt evaluator consts algebra eqngr = +fun static_evaluator_simple ctxt evaluator consts algebra eqngr = let fun generate_consts ctxt algebra eqngr = fold_map (ensure_const ctxt algebra eqngr false); @@ -862,13 +867,13 @@ in evaluator program end; fun static_conv ctxt consts conv = - Code_Preproc.static_conv ctxt consts (lift_evaluator ctxt conv consts); + Code_Preproc.static_conv ctxt consts (static_evaluator ctxt conv consts); fun static_conv_simple ctxt consts conv = - Code_Preproc.static_conv ctxt consts (lift_evaluator_simple ctxt conv consts); + Code_Preproc.static_conv ctxt consts (static_evaluator_simple ctxt conv consts); fun static_value ctxt postproc consts evaluator = - Code_Preproc.static_value ctxt postproc consts (lift_evaluator ctxt evaluator consts); + Code_Preproc.static_value ctxt postproc consts (static_evaluator ctxt evaluator consts); (** constant expressions **) diff -r 6389a8c1268a -r d651b944c67e src/Tools/nbe.ML --- a/src/Tools/nbe.ML Thu May 08 21:17:23 2014 +0200 +++ b/src/Tools/nbe.ML Fri May 09 08:13:26 2014 +0200 @@ -502,10 +502,11 @@ (* reconstruction *) -fun typ_of_itype vs (tyco `%% itys) = - Type (tyco, map (typ_of_itype vs) itys) - | typ_of_itype vs (ITyVar v) = - TFree ("'" ^ v, (the o AList.lookup (op =) vs) v); +fun typ_of_itype resubst_tvar = + let + fun typ_of (tyco `%% itys) = Type (tyco, map typ_of itys) + | typ_of (ITyVar v) = TFree (resubst_tvar v); + in typ_of end; fun term_of_univ ctxt (idx_tab : Code_Symbol.T Inttab.table) t = let @@ -542,11 +543,11 @@ (* evaluation with type reconstruction *) -fun eval_term raw_ctxt (nbe_program, idx_tab) ((vs0, (vs, ty)), t) deps = +fun eval_term raw_ctxt (nbe_program, idx_tab) resubst_tvar ((vs, ty), t) deps = let val ctxt = Syntax.init_pretty_global (Proof_Context.theory_of raw_ctxt); val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt); - val ty' = typ_of_itype vs0 ty; + val ty' = typ_of_itype resubst_tvar ty; fun type_infer t = Syntax.check_term (Config.put Type_Infer_Context.const_sorts false ctxt) (Type.constraint ty' t); @@ -592,11 +593,11 @@ val (_, raw_oracle) = Context.>>> (Context.map_theory_result (Thm.add_oracle (@{binding normalization_by_evaluation}, - fn (ctxt, nbe_program_idx_tab, vsp_ty_t, deps, ct) => - mk_equals ctxt ct (eval_term ctxt nbe_program_idx_tab vsp_ty_t deps)))); + fn (ctxt, nbe_program_idx_tab, resubst_tvars, vs_ty_t, deps, ct) => + mk_equals ctxt ct (eval_term ctxt nbe_program_idx_tab resubst_tvars vs_ty_t deps)))); -fun oracle ctxt nbe_program_idx_tab vsp_ty_t deps ct = - raw_oracle (ctxt, nbe_program_idx_tab, vsp_ty_t, deps, ct); +fun oracle ctxt nbe_program_idx_tab resubst_tvars vs_ty_t deps ct = + raw_oracle (ctxt, nbe_program_idx_tab, resubst_tvars, vs_ty_t, deps, ct); fun dynamic_conv ctxt = lift_triv_classes_conv ctxt (Code_Thingol.dynamic_conv ctxt (oracle ctxt o compile false ctxt));