equal
deleted
inserted
replaced
7 *) |
7 *) |
8 |
8 |
9 signature BNF_LFP = |
9 signature BNF_LFP = |
10 sig |
10 sig |
11 val construct_lfp: mixfix list -> binding list -> binding list -> binding list -> |
11 val construct_lfp: mixfix list -> binding list -> binding list -> binding list -> |
12 binding list list -> (string * sort) list option -> typ list * typ list list -> |
12 binding list list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list -> |
13 BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory |
13 local_theory -> BNF_FP_Util.fp_result * local_theory |
14 end; |
14 end; |
15 |
15 |
16 structure BNF_LFP : BNF_LFP = |
16 structure BNF_LFP : BNF_LFP = |
17 struct |
17 struct |
18 |
18 |
59 val Bss = replicate n allBs; |
59 val Bss = replicate n allBs; |
60 val allCs = passiveAs @ activeCs; |
60 val allCs = passiveAs @ activeCs; |
61 val allCs' = passiveBs @ activeCs; |
61 val allCs' = passiveBs @ activeCs; |
62 val Css' = replicate n allCs'; |
62 val Css' = replicate n allCs'; |
63 |
63 |
64 (* typs *) |
64 (* types *) |
65 val dead_poss = |
65 val dead_poss = |
66 (case resBs of |
66 map (fn T => if member (op =) deads (TFree T) then SOME (TFree T) else NONE) resBs; |
67 NONE => map SOME deads @ replicate m NONE |
|
68 | SOME Ts => map (fn T => if member (op =) deads (TFree T) then SOME (TFree T) else NONE) Ts); |
|
69 fun mk_param NONE passive = (hd passive, tl passive) |
67 fun mk_param NONE passive = (hd passive, tl passive) |
70 | mk_param (SOME a) passive = (a, passive); |
68 | mk_param (SOME a) passive = (a, passive); |
71 val mk_params = fold_map mk_param dead_poss #> fst; |
69 val mk_params = fold_map mk_param dead_poss #> fst; |
72 |
70 |
73 fun mk_FTs Ts = map2 (fn Ds => mk_T_of_bnf Ds Ts) Dss bnfs; |
71 fun mk_FTs Ts = map2 (fn Ds => mk_T_of_bnf Ds Ts) Dss bnfs; |