# HG changeset patch # User paulson # Date 1676234979 0 # Node ID d19c45c7195bdf650d32008fc2796171e06d4dcb # Parent 6bdd125d932b1364e8fbee784b9c80469b06ae37# Parent 61fba09a3456a57c660d45da2bf49d97ce2559c6 merged diff -r 61fba09a3456 -r d19c45c7195b src/HOL/Imperative_HOL/Heap_Monad.thy --- a/src/HOL/Imperative_HOL/Heap_Monad.thy Sun Feb 12 20:49:31 2023 +0000 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Sun Feb 12 20:49:39 2023 +0000 @@ -646,8 +646,8 @@ val unitT = \<^type_name>\unit\ `%% []; val unitt = IConst { sym = Code_Symbol.Constant \<^const_name>\Unity\, typargs = [], dicts = [], dom = [], - annotation = NONE }; - fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t) + annotation = NONE, range = unitT }; + fun dest_abs ((v, ty) `|=> (t, _), _) = ((v, ty), t) | dest_abs (t, ty) = let val vs = fold_varnames cons t []; @@ -667,18 +667,18 @@ else force t | _ => force t; fun imp_monad_bind'' ts = (SOME dummy_name, unitT) `|=> - ICase { term = IVar (SOME dummy_name), typ = unitT, clauses = [(unitt, tr_bind'' ts)], primitive = dummy_case_term } + (ICase { term = IVar (SOME dummy_name), typ = unitT, clauses = [(unitt, tr_bind'' ts)], primitive = dummy_case_term }, unitT) fun imp_monad_bind' (const as { sym = Code_Symbol.Constant c, dom = dom, ... }) ts = if is_bind c then case (ts, dom) of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] | ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] `$ t3 - | (ts, _) => imp_monad_bind (eta_expand 2 (const, ts)) + | (ts, _) => imp_monad_bind (satisfied_application 2 (const, ts)) else IConst const `$$ map imp_monad_bind ts and imp_monad_bind (IConst const) = imp_monad_bind' const [] | imp_monad_bind (t as IVar _) = t | imp_monad_bind (t as _ `$ _) = (case unfold_app t of (IConst const, ts) => imp_monad_bind' const ts | (t, ts) => imp_monad_bind t `$$ map imp_monad_bind ts) - | imp_monad_bind (v_ty `|=> t) = v_ty `|=> imp_monad_bind t + | imp_monad_bind (v_ty `|=> t) = v_ty `|=> apfst imp_monad_bind t | imp_monad_bind (ICase { term = t, typ = ty, clauses = clauses, primitive = t0 }) = ICase { term = imp_monad_bind t, typ = ty, clauses = (map o apply2) imp_monad_bind clauses, primitive = imp_monad_bind t0 }; diff -r 61fba09a3456 -r d19c45c7195b src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Sun Feb 12 20:49:31 2023 +0000 +++ b/src/Tools/Code/code_haskell.ML Sun Feb 12 20:49:39 2023 +0000 @@ -241,18 +241,18 @@ str "=", print_app tyvars (SOME thm) reserved NOBR (const, []) ] - | SOME (k, Code_Printer.Complex_printer _) => + | SOME (wanted, Code_Printer.Complex_printer _) => let - val { sym = Constant c, dom, ... } = const; + val { sym = Constant c, dom, range, ... } = const; val (vs, rhs) = (apfst o map) fst - (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, []))); + (Code_Thingol.unfold_abs (Code_Thingol.satisfied_application wanted (const, []))); val s = if (is_some o const_syntax) c then NONE else (SOME o Long_Name.base_name o deresolve_const) c; val vars = reserved |> intro_vars (map_filter I (s :: vs)); val lhs = IConst { sym = Constant classparam, typargs = [], - dicts = [], dom = dom, annotation = NONE } `$$ map IVar vs; - (*dictionaries are not relevant at this late stage, + dicts = [], dom = dom, range = range, annotation = NONE } `$$ map IVar vs; + (*dictionaries are not relevant in Haskell, and these consts never need type annotations for disambiguation *) in semicolon [ diff -r 61fba09a3456 -r d19c45c7195b src/Tools/Code/code_ml.ML --- a/src/Tools/Code/code_ml.ML Sun Feb 12 20:49:31 2023 +0000 +++ b/src/Tools/Code/code_ml.ML Sun Feb 12 20:49:39 2023 +0000 @@ -123,17 +123,17 @@ then print_case is_pseudo_fun some_thm vars fxy case_expr else print_app is_pseudo_fun some_thm vars fxy app | NONE => print_case is_pseudo_fun some_thm vars fxy case_expr) - and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts = dss, dom = dom, ... }, ts)) = + and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts, dom, ... }, ts)) = if is_constr sym then - let val k = length dom in - if k < 2 orelse length ts = k + let val wanted = length dom in + if wanted < 2 orelse length ts = wanted then (str o deresolve) sym :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts) - else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)] + else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.satisfied_application wanted app)] end else if is_pseudo_fun sym then (str o deresolve) sym @@ str "()" - else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dss + else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dicts @ map (print_term is_pseudo_fun some_thm vars BR) ts and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun) (print_term is_pseudo_fun) const_syntax some_thm vars @@ -446,17 +446,17 @@ then print_case is_pseudo_fun some_thm vars fxy case_expr else print_app is_pseudo_fun some_thm vars fxy app | NONE => print_case is_pseudo_fun some_thm vars fxy case_expr) - and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts = dss, dom = dom, ... }, ts)) = + and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts, dom, ... }, ts)) = if is_constr sym then - let val k = length dom in - if length ts = k + let val wanted = length dom in + if length ts = wanted then (str o deresolve) sym :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts) - else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)] + else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.satisfied_application wanted app)] end else if is_pseudo_fun sym then (str o deresolve) sym @@ str "()" - else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dss + else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dicts @ map (print_term is_pseudo_fun some_thm vars BR) ts and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun) (print_term is_pseudo_fun) const_syntax some_thm vars diff -r 61fba09a3456 -r d19c45c7195b src/Tools/Code/code_printer.ML --- a/src/Tools/Code/code_printer.ML Sun Feb 12 20:49:31 2023 +0000 +++ b/src/Tools/Code/code_printer.ML Sun Feb 12 20:49:39 2023 +0000 @@ -325,17 +325,17 @@ NONE => brackify fxy (print_app_expr some_thm vars app) | SOME (_, Plain_printer s) => brackify fxy (str s :: map (print_term some_thm vars BR) ts) - | SOME (k, Complex_printer print) => + | SOME (wanted, Complex_printer print) => let fun print' fxy ts = - print (print_term some_thm) some_thm vars fxy (ts ~~ take k dom); + print (print_term some_thm) some_thm vars fxy (ts ~~ take wanted dom); in - if k = length ts + if wanted = length ts then print' fxy ts - else if k < length ts - then case chop k ts of (ts1, ts2) => + else if wanted < length ts + then case chop wanted ts of (ts1, ts2) => brackify fxy (print' APP ts1 :: map (print_term some_thm vars BR) ts2) - else print_term some_thm vars fxy (Code_Thingol.eta_expand k app) + else print_term some_thm vars fxy (Code_Thingol.satisfied_application wanted app) end) | _ => brackify fxy (print_app_expr some_thm vars app); diff -r 61fba09a3456 -r d19c45c7195b src/Tools/Code/code_scala.ML --- a/src/Tools/Code/code_scala.ML Sun Feb 12 20:49:31 2023 +0000 +++ b/src/Tools/Code/code_scala.ML Sun Feb 12 20:49:39 2023 +0000 @@ -117,7 +117,6 @@ and print_app tyvars is_pat some_thm vars fxy (app as ({ sym, typargs, dom, dicts, ... }, ts)) = let - val k = length ts; val typargs' = if is_pat then [] else typargs; val syntax = case sym of Constant const => const_syntax const @@ -127,7 +126,7 @@ orelse Code_Thingol.unambiguous_dictss dicts then fn p => K p else applify_dictss tyvars; - val (l, print') = case syntax of + val (wanted, print') = case syntax of NONE => (args_num sym, fn fxy => fn ts => applify_dicts (gen_applify (is_constr sym) "(" ")" (print_term tyvars is_pat some_thm vars NOBR) fxy @@ -141,11 +140,11 @@ | SOME (k, Complex_printer print) => (k, fn fxy => fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy (ts ~~ take k dom)) - in if k = l then print' fxy ts - else if k < l then - print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app) + in if length ts = wanted then print' fxy ts + else if length ts < wanted then + print_term tyvars is_pat some_thm vars fxy (Code_Thingol.satisfied_application wanted app) else let - val (ts1, ts23) = chop l ts; + val (ts1, ts23) = chop wanted ts; in Pretty.block (print' BR ts1 :: map (fn t => Pretty.block [str ".apply(", print_term tyvars is_pat some_thm vars NOBR t, str ")"]) ts23) diff -r 61fba09a3456 -r d19c45c7195b src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Sun Feb 12 20:49:31 2023 +0000 +++ b/src/Tools/Code/code_thingol.ML Sun Feb 12 20:49:39 2023 +0000 @@ -9,6 +9,7 @@ infix 4 `$; infix 4 `$$; infixr 3 `->; +infixr 3 `-->; infixr 3 `|=>; infixr 3 `|==>; @@ -24,16 +25,17 @@ `%% of string * itype list | ITyVar of vname; type const = { sym: Code_Symbol.T, typargs: itype list, dicts: dict list list, - dom: itype list, annotation: itype option }; + dom: itype list, range: itype, annotation: itype option }; datatype iterm = IConst of const | IVar of vname option | `$ of iterm * iterm - | `|=> of (vname option * itype) * iterm + | `|=> of (vname option * itype) * (iterm * itype) | ICase of { term: iterm, typ: itype, clauses: (iterm * iterm) list, primitive: iterm }; val `-> : itype * itype -> itype; + val `--> : itype list * itype -> itype; val `$$ : iterm * iterm list -> iterm; - val `|==> : (vname option * itype) list * iterm -> iterm; + val `|==> : (vname option * itype) list * (iterm * itype) -> iterm; type typscheme = (vname * sort) list * itype; end; @@ -46,6 +48,7 @@ val unfold_fun_n: int -> itype -> itype list * itype val unfold_app: iterm -> iterm * iterm list val unfold_abs: iterm -> (vname option * itype) list * iterm + val unfold_abs_typed: iterm -> ((vname option * itype) list * (iterm * itype)) option val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option val split_let_no_pat: iterm -> (((string option * itype) * iterm) * iterm) option val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm @@ -53,10 +56,9 @@ val split_pat_abs: iterm -> ((iterm * itype) * iterm) option val unfold_pat_abs: iterm -> (iterm * itype) list * iterm val unfold_const_app: iterm -> (const * iterm list) option - val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm val is_IVar: iterm -> bool val is_IAbs: iterm -> bool - val eta_expand: int -> const * iterm list -> iterm + val satisfied_application: int -> const * iterm list -> iterm val contains_dict_var: iterm -> bool val unambiguous_dictss: dict list list -> bool val add_constsyms: iterm -> Code_Symbol.T list -> Code_Symbol.T list @@ -144,6 +146,8 @@ fun ty1 `-> ty2 = "fun" `%% [ty1, ty2]; +val op `--> = Library.foldr (op `->); + val unfold_fun = unfoldr (fn "fun" `%% [ty1, ty2] => SOME (ty1, ty2) | _ => NONE); @@ -152,17 +156,16 @@ let val (tys1, ty1) = unfold_fun ty; val (tys3, tys2) = chop n tys1; - val ty3 = Library.foldr (op `->) (tys2, ty1); - in (tys3, ty3) end; + in (tys3, tys2 `--> ty1) end; type const = { sym: Code_Symbol.T, typargs: itype list, dicts: dict list list, - dom: itype list, annotation: itype option }; + dom: itype list, range: itype, annotation: itype option }; datatype iterm = IConst of const | IVar of vname option | `$ of iterm * iterm - | `|=> of (vname option * itype) * iterm + | `|=> of (vname option * itype) * (iterm * itype) | ICase of { term: iterm, typ: itype, clauses: (iterm * iterm) list, primitive: iterm }; (*see also signature*) @@ -173,23 +176,33 @@ | is_IAbs _ = false; val op `$$ = Library.foldl (op `$); -val op `|==> = Library.foldr (op `|=>); +fun vs_tys `|==> body = Library.foldr + (fn (v_ty as (_, ty), body as (_, rty)) => (v_ty `|=> body, ty `-> rty)) (vs_tys, body) + |> fst; val unfold_app = unfoldl - (fn op `$ t => SOME t + (fn op `$ t_t => SOME t_t | _ => NONE); val unfold_abs = unfoldr - (fn op `|=> t => SOME t + (fn (v `|=> (t, _)) => SOME (v, t) | _ => NONE); -val split_let = - (fn ICase { term = t, typ = ty, clauses = [(p, body)], ... } => SOME (((p, ty), t), body) - | _ => NONE); +fun unfold_abs_typed (v_ty `|=> body) = + unfoldr + (fn (v_ty `|=> body, _) => SOME (v_ty, body) + | _ => NONE) body + |> apfst (cons v_ty) + |> SOME + | unfold_abs_typed _ = NONE -val split_let_no_pat = - (fn ICase { term = t, typ = ty, clauses = [(IVar v, body)], ... } => SOME (((v, ty), t), body) - | _ => NONE); +fun split_let (ICase { term = t, typ = ty, clauses = [(p, body)], ... }) = + SOME (((p, ty), t), body) + | split_let _ = NONE; + +fun split_let_no_pat (ICase { term = t, typ = ty, clauses = [(IVar v, body)], ... }) = + SOME (((v, ty), t), body) + | split_let_no_pat _ = NONE; val unfold_let = unfoldr split_let; @@ -205,9 +218,9 @@ fun fold' (IConst c) = f c | fold' (IVar _) = I | fold' (t1 `$ t2) = fold' t1 #> fold' t2 - | fold' (_ `|=> t) = fold' t - | fold' (ICase { term = t, clauses = clauses, ... }) = fold' t - #> fold (fn (p, body) => fold' p #> fold' body) clauses + | fold' (_ `|=> (t, _)) = fold' t + | fold' (ICase { term = t, clauses = clauses, ... }) = + fold' t #> fold (fn (p, body) => fold' p #> fold' body) clauses in fold' end; val add_constsyms = fold_constexprs (fn { sym, ... } => insert (op =) sym); @@ -225,8 +238,8 @@ | fold_term vs (IVar (SOME v)) = if member (op =) vs v then I else f v | fold_term _ (IVar NONE) = I | fold_term vs (t1 `$ t2) = fold_term vs t1 #> fold_term vs t2 - | fold_term vs ((SOME v, _) `|=> t) = fold_term (insert (op =) v vs) t - | fold_term vs ((NONE, _) `|=> t) = fold_term vs t + | fold_term vs ((SOME v, _) `|=> (t, _)) = fold_term (insert (op =) v vs) t + | fold_term vs ((NONE, _) `|=> (t, _)) = fold_term vs t | fold_term vs (ICase { term = t, clauses = clauses, ... }) = fold_term vs t #> fold (fold_clause vs) clauses and fold_clause vs (p, t) = fold_term (add_vars p vs) t; @@ -240,8 +253,11 @@ fun exists_var t v = fold_varnames (fn w => fn b => v = w orelse b) t false; -fun split_pat_abs ((NONE, ty) `|=> t) = SOME ((IVar NONE, ty), t) - | split_pat_abs ((SOME v, ty) `|=> t) = SOME (case t +fun invent_params used tys = + (map o apfst) SOME (Name.invent_names (Name.build_context used) "a" tys); + +fun split_pat_abs ((NONE, ty) `|=> (t, _)) = SOME ((IVar NONE, ty), t) + | split_pat_abs ((SOME v, ty) `|=> (t, _)) = SOME (case t of ICase { term = IVar (SOME w), clauses = [(p, body)], ... } => if v = w andalso (exists_var p v orelse not (exists_var body v)) then ((p, ty), body) @@ -252,33 +268,30 @@ val unfold_pat_abs = unfoldr split_pat_abs; fun unfold_abs_eta [] t = ([], t) - | unfold_abs_eta (_ :: tys) (v_ty `|=> t) = + | unfold_abs_eta (_ :: tys) ((v, _) `|=> (t, _)) = let - val (vs_tys, t') = unfold_abs_eta tys t; - in (v_ty :: vs_tys, t') end + val (vs, t') = unfold_abs_eta tys t; + in (v :: vs, t') end | unfold_abs_eta tys t = let - val ctxt = Name.build_context (declare_varnames t); - val vs_tys = (map o apfst) SOME (Name.invent_names ctxt "a" tys); - in (vs_tys, t `$$ map (IVar o fst) vs_tys) end; + val vs = map fst (invent_params (declare_varnames t) tys); + in (vs, t `$$ map IVar vs) end; -fun eta_expand k (const as { dom = tys, ... }, ts) = +fun satisfied_application wanted (const as { dom, range, ... }, ts) = let - val j = length ts; - val l = k - j; - val _ = if l > length tys - then error "Impossible eta-expansion" else (); - val vars = Name.build_context (fold declare_varnames ts); - val vs_tys = (map o apfst) SOME - (Name.invent_names vars "a" ((take l o drop j) tys)); - in vs_tys `|==> IConst const `$$ ts @ map (IVar o fst) vs_tys end; + val given = length ts; + val delta = wanted - given; + val vs_tys = invent_params (fold declare_varnames ts) + (((take delta o drop given) dom)); + val (_, rty) = unfold_fun_n wanted range; + in vs_tys `|==> (IConst const `$$ ts @ map (IVar o fst) vs_tys, rty) end; fun map_terms_bottom_up f (t as IConst _) = f t | map_terms_bottom_up f (t as IVar _) = f t | map_terms_bottom_up f (t1 `$ t2) = f (map_terms_bottom_up f t1 `$ map_terms_bottom_up f t2) - | map_terms_bottom_up f ((v, ty) `|=> t) = f - ((v, ty) `|=> map_terms_bottom_up f t) + | map_terms_bottom_up f ((v, ty) `|=> (t, rty)) = f + ((v, ty) `|=> (map_terms_bottom_up f t, rty)) | map_terms_bottom_up f (ICase { term = t, typ = ty, clauses = clauses, primitive = t0 }) = f (ICase { term = map_terms_bottom_up f t, typ = ty, clauses = (map o apply2) (map_terms_bottom_up f) clauses, @@ -316,8 +329,7 @@ |> the_default [(pat_args, body)] | NONE => [(pat_args, body)]) | distill vs_map pat_args body = [(pat_args, body)]; - val (vTs, body) = unfold_abs_eta tys t; - val vs = map fst vTs; + val (vs, body) = unfold_abs_eta tys t; val vs_map = build (fold_index (fn (i, SOME v) => cons (v, i) | _ => I) vs); in distill vs_map (map IVar vs) body end; @@ -330,7 +342,7 @@ fun contains_dict_var (IConst { dicts = dss, ... }) = exists_dictss_var (K true) dss | contains_dict_var (IVar _) = false | contains_dict_var (t1 `$ t2) = contains_dict_var t1 orelse contains_dict_var t2 - | contains_dict_var (_ `|=> t) = contains_dict_var t + | contains_dict_var (_ `|=> (t, _)) = contains_dict_var t | contains_dict_var (ICase { primitive = t, ... }) = contains_dict_var t; val unambiguous_dictss = not o exists_dictss_var (fn { unique, ... } => not unique); @@ -639,7 +651,7 @@ fun translate_classparam_instance (c, ty) = let val raw_const = Const (c, map_type_tfree (K arity_typ') ty); - val dom_length = length (fst (strip_type ty)) + val dom_length = length (binder_types ty); val thm = Axclass.unoverload_conv ctxt (Thm.cterm_of ctxt raw_const); val const = (apsnd Logic.unvarifyT_global o dest_Const o snd o Logic.dest_equals o Thm.prop_of) thm; @@ -673,10 +685,12 @@ let val ((v', _), t') = Term.dest_abs_global (Abs (Name.desymbolize (SOME false) v, ty, t)); val v'' = if Term.used_free v' t' then SOME v' else NONE + val rty = fastype_of_tagged_term t' in translate_typ ctxt algbr eqngr permissive ty + ##>> translate_typ ctxt algbr eqngr permissive rty ##>> translate_term ctxt algbr eqngr permissive some_thm (t', some_abs) - #>> (fn (ty, t) => (v'', ty) `|=> t) + #>> (fn ((ty, rty), t) => (v'', ty) `|=> (t, rty)) end | translate_term ctxt algbr eqngr permissive some_thm (t as _ $ _, some_abs) = case strip_comb t @@ -712,11 +726,11 @@ ensure_const ctxt algbr eqngr permissive c ##>> fold_map (translate_typ ctxt algbr eqngr permissive) typargs ##>> fold_map (translate_dicts ctxt algbr eqngr permissive some_thm) (typargs ~~ sorts) - ##>> fold_map (translate_typ ctxt algbr eqngr permissive) (ty' :: dom) - #>> (fn (((c, typargs), dss), annotation :: dom) => + ##>> fold_map (translate_typ ctxt algbr eqngr permissive) (range :: dom) + #>> (fn (((c, typargs), dss), range :: dom) => IConst { sym = Constant c, typargs = typargs, dicts = dss, - dom = dom, annotation = - if annotate then SOME annotation else NONE }) + dom = dom, range = range, annotation = + if annotate then SOME (dom `--> range) else NONE }) end and translate_app_const ctxt algbr eqngr permissive some_thm ((c_ty, ts), some_abs) = translate_const ctxt algbr eqngr permissive some_thm (c_ty, some_abs) @@ -766,21 +780,24 @@ clauses = (filter_out (is_undefined_clause ctxt) o distill_clauses constrs o project_cases) ts, primitive = t_app `$$ ts }) end -and translate_app_case ctxt algbr eqngr permissive some_thm (num_args, pattern_schema) ((c, ty), ts) = - if length ts < num_args then +and translate_app_case ctxt algbr eqngr permissive some_thm (wanted, pattern_schema) ((c, ty), ts) = + if length ts < wanted then let - val k = length ts; - val tys = (take (num_args - k) o drop k o fst o strip_type) ty; - val names = Name.build_context (ts |> (fold o fold_aterms) Term.declare_term_frees); - val vs = Name.invent_names names "a" tys; + val given = length ts; + val delta = wanted - given; + val tys = (take delta o drop given o binder_types) ty; + val used = Name.build_context ((fold o fold_aterms) Term.declare_term_frees ts); + val vs_tys = Name.invent_names used "a" tys; + val rty = (drop delta o binder_types) ty ---> body_type ty; in fold_map (translate_typ ctxt algbr eqngr permissive) tys - ##>> translate_case ctxt algbr eqngr permissive some_thm pattern_schema ((c, ty), ts @ map Free vs) - #>> (fn (tys, t) => map2 (fn (v, _) => pair (SOME v)) vs tys `|==> t) + ##>> translate_case ctxt algbr eqngr permissive some_thm pattern_schema ((c, ty), ts @ map Free vs_tys) + ##>> translate_typ ctxt algbr eqngr permissive rty + #>> (fn ((tys, t), rty) => map2 (fn (v, _) => pair (SOME v)) vs_tys tys `|==> (t, rty)) end - else if length ts > num_args then - translate_case ctxt algbr eqngr permissive some_thm pattern_schema ((c, ty), take num_args ts) - ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm o rpair NONE) (drop num_args ts) + else if length ts > wanted then + translate_case ctxt algbr eqngr permissive some_thm pattern_schema ((c, ty), take wanted ts) + ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm o rpair NONE) (drop wanted ts) #>> (fn (t, ts) => t `$$ ts) else translate_case ctxt algbr eqngr permissive some_thm pattern_schema ((c, ty), ts) diff -r 61fba09a3456 -r d19c45c7195b src/Tools/nbe.ML --- a/src/Tools/nbe.ML Sun Feb 12 20:49:31 2023 +0000 +++ b/src/Tools/nbe.ML Sun Feb 12 20:49:39 2023 +0000 @@ -326,7 +326,7 @@ in of_iapp match_cont t' (fold_rev (cons o of_iterm NONE) ts []) end and of_iapp match_cont (IConst { sym, dicts = dss, ... }) ts = constapp sym dss ts | of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound_optional v) ts - | of_iapp match_cont ((v, _) `|=> t) ts = + | of_iapp match_cont ((v, _) `|=> (t, _)) ts = nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound_optional v]) (of_iterm NONE t))) ts | of_iapp match_cont (ICase { term = t, clauses = clauses, primitive = t0, ... }) ts = nbe_apps (ml_cases (of_iterm NONE t) @@ -421,7 +421,7 @@ fun dummy_const sym dss = IConst { sym = sym, typargs = [], dicts = dss, - dom = [], annotation = NONE }; + dom = [], annotation = NONE, range = ITyVar "" }; fun eqns_of_stmt (_, Code_Thingol.NoStmt) = []