370 |
370 |
371 (* ------------------------------------------------------------------------- *) |
371 (* ------------------------------------------------------------------------- *) |
372 (* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL *) |
372 (* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL *) |
373 (* ------------------------------------------------------------------------- *) |
373 (* ------------------------------------------------------------------------- *) |
374 |
374 |
375 val typ_of_dtyp = Nitpick_Util.typ_of_dtyp |
375 fun typ_of_dtyp _ typ_assoc (Datatype.DtTFree a) = |
|
376 the (AList.lookup (op =) typ_assoc (Datatype.DtTFree a)) |
|
377 | typ_of_dtyp descr typ_assoc (Datatype.DtType (s, Us)) = |
|
378 Type (s, map (typ_of_dtyp descr typ_assoc) Us) |
|
379 | typ_of_dtyp descr typ_assoc (Datatype.DtRec i) = |
|
380 let val (s, ds, _) = the (AList.lookup (op =) descr i) in |
|
381 Type (s, map (typ_of_dtyp descr typ_assoc) ds) |
|
382 end |
|
383 |
376 val close_form = ATP_Util.close_form |
384 val close_form = ATP_Util.close_form |
377 val monomorphic_term = ATP_Util.monomorphic_term |
385 val monomorphic_term = ATP_Util.monomorphic_term |
378 val specialize_type = ATP_Util.specialize_type |
386 val specialize_type = ATP_Util.specialize_type |
379 |
387 |
380 (* ------------------------------------------------------------------------- *) |
388 (* ------------------------------------------------------------------------- *) |