src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
changeset 49165 c6ccaf6df93c
parent 49161 a8e74375d971
child 49167 68623861e0f2
equal deleted inserted replaced
49162:bd6a18a1a5af 49165:c6ccaf6df93c
    62       |> Library.foldr1 (merge_type_args_constrained lthy);
    62       |> Library.foldr1 (merge_type_args_constrained lthy);
    63     val As = map fst constrained_As;
    63     val As = map fst constrained_As;
    64     val As' = map dest_TFree As;
    64     val As' = map dest_TFree As;
    65 
    65 
    66     val _ = (case duplicates (op =) As of [] => ()
    66     val _ = (case duplicates (op =) As of [] => ()
    67       | T :: _ => error ("Duplicate type parameter " ^ quote (Syntax.string_of_typ lthy T)));
    67       | A :: _ => error ("Duplicate type parameter " ^ quote (Syntax.string_of_typ lthy A)));
    68 
    68 
    69     (* TODO: print timing information for sugar *)
    69     (* TODO: print timing information for sugar *)
    70     (* TODO: check that no type variables occur in the rhss that's not in the lhss *)
       
    71     (* TODO: use sort constraints on type args *)
    70     (* TODO: use sort constraints on type args *)
    72     (* TODO: use mixfix *)
    71     (* TODO: use mixfix *)
    73 
    72 
    74     val N = length specs;
    73     val N = length specs;
    75 
    74 
    92     val ctr_argsss = map (map args_of) ctr_specss;
    91     val ctr_argsss = map (map args_of) ctr_specss;
    93     val ctr_mixfixess = map (map mixfix_of_ctr) ctr_specss;
    92     val ctr_mixfixess = map (map mixfix_of_ctr) ctr_specss;
    94 
    93 
    95     val sel_bindersss = map (map (map fst)) ctr_argsss;
    94     val sel_bindersss = map (map (map fst)) ctr_argsss;
    96     val ctr_Tsss = map (map (map (prepare_typ fake_lthy o snd))) ctr_argsss;
    95     val ctr_Tsss = map (map (map (prepare_typ fake_lthy o snd))) ctr_argsss;
       
    96 
       
    97     val rhs_As = (case subtract (op =) As' (fold (fold (fold Term.add_tfreesT)) ctr_Tsss []) of
       
    98         [] => ()
       
    99       | A' :: _ => error ("Extra type variables on rhs: " ^
       
   100           quote (Syntax.string_of_typ lthy (TFree A'))));
       
   101 
       
   102     (* TODO: check that no type variables occur in the rhss that's not in the lhss *)
       
   103 
    97 
   104 
    98     val (Bs, C) =
   105     val (Bs, C) =
    99       lthy
   106       lthy
   100       |> fold (fold (fn s => Variable.declare_typ (TFree (s, dummyS))) o type_args_of) specs
   107       |> fold (fold (fn s => Variable.declare_typ (TFree (s, dummyS))) o type_args_of) specs
   101       |> mk_TFrees N
   108       |> mk_TFrees N