528 |-> Proof_Context.read_term_pattern |
528 |-> Proof_Context.read_term_pattern |
529 |> numbers_to_string (*TODO drop*) |
529 |> numbers_to_string (*TODO drop*) |
530 |> typ_a2real; (*TODO drop*) |
530 |> typ_a2real; (*TODO drop*) |
531 fun str2term str = parse_patt (ThyC.get_theory "Isac_Knowledge") str |
531 fun str2term str = parse_patt (ThyC.get_theory "Isac_Knowledge") str |
532 |
532 |
533 (* TODO decide with Test_Isac *) |
|
534 fun is_atom t = length (vars t) = 1 |
|
535 fun is_atom (Const ("Float.Float",_) $ _) = true |
533 fun is_atom (Const ("Float.Float",_) $ _) = true |
536 | is_atom (Const ("ComplexI.I'_'_",_)) = true |
534 | is_atom (Const ("ComplexI.I'_'_",_)) = true |
537 | is_atom (Const ("Groups.times_class.times",_) $ t $ Const ("ComplexI.I'_'_",_)) = is_atom t |
535 | is_atom (Const ("Groups.times_class.times",_) $ t $ Const ("ComplexI.I'_'_",_)) = is_atom t |
538 | is_atom (Const ("Groups.plus_class.plus",_) $ t1 $ Const ("ComplexI.I'_'_",_)) = is_atom t1 |
536 | is_atom (Const ("Groups.plus_class.plus",_) $ t1 $ Const ("ComplexI.I'_'_",_)) = is_atom t1 |
539 | is_atom (Const ("Groups.plus_class.plus",_) $ t1 $ |
537 | is_atom (Const ("Groups.plus_class.plus",_) $ t1 $ |
595 fun negates p1 p2 = negat (p1, p2) orelse negat (swap (p1, p2)); |
593 fun negates p1 p2 = negat (p1, p2) orelse negat (swap (p1, p2)); |
596 |
594 |
597 fun raise_type_conflicts ts = |
595 fun raise_type_conflicts ts = |
598 let |
596 let |
599 val dups = duplicates (op =) (map (fst o dest_Free) ts) |
597 val dups = duplicates (op =) (map (fst o dest_Free) ts) |
600 val confl = filter (fn Free (str, _) => member op = dups str) ts |
598 val confl = filter (fn Free (str, _) => member op = dups str |
|
599 | _ => false) ts |
601 in |
600 in |
602 if confl = [] |
601 if confl = [] |
603 then () |
602 then () |
604 else raise TYPE ("formalisation inconsistent w.r.t. type inference: ", |
603 else raise TYPE ("formalisation inconsistent w.r.t. type inference: ", |
605 map (snd o dest_Free)confl, confl) |
604 map (snd o dest_Free)confl, confl) |