forked from Isabelle_DOF/Isabelle_DOF
Merge branch 'master' of https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF
This commit is contained in:
commit
ea5c4e2fa9
24
Isa_DOF.thy
24
Isa_DOF.thy
|
@ -550,15 +550,20 @@ fun read_fields raw_fields ctxt =
|
|||
let
|
||||
val Ts = Syntax.read_typs ctxt (map (fn ((_, raw_T, _),_) => raw_T) raw_fields);
|
||||
val terms = map ((map_option (Syntax.read_term ctxt)) o snd) raw_fields
|
||||
fun read x = let val _ = writeln ("CCC"^x)
|
||||
in Syntax.read_term ctxt x end
|
||||
fun annotate ((_, raw_T, _),SOME raw_term) =(SOME (read ("("^raw_term^")::"^raw_T))
|
||||
handle ERROR _ => error("type mismatch:"^raw_T)
|
||||
(* BAD STYLE : better would be catching
|
||||
exn. *) )
|
||||
|annotate ((_, _, _),_) = NONE
|
||||
val generalize_typ = Term.map_type_tfree (fn (str,sort)=> Term.TVar((str,0),sort));
|
||||
fun test t1 t2 = Sign.typ_instance (Proof_Context.theory_of ctxt)(t1, generalize_typ t2)
|
||||
fun check_default (ty,SOME trm) =
|
||||
let val ty' = (type_of trm)
|
||||
in if test ty ty'
|
||||
then ()
|
||||
else error("type mismatch:"^
|
||||
(Syntax.string_of_typ ctxt ty')^":"^
|
||||
(Syntax.string_of_typ ctxt ty))
|
||||
end
|
||||
(* BAD STYLE : better would be catching exn. *)
|
||||
|check_default (_,_) = ()
|
||||
val fields = map2 (fn ((x, _, mx),_) => fn T => (x, T, mx)) raw_fields Ts;
|
||||
(* val _ = map annotate raw_fields (* checking types conform to defaults *) *)
|
||||
val _ = map check_default (Ts ~~ terms) (* checking types conform to defaults *)
|
||||
val ctxt' = fold Variable.declare_typ Ts ctxt;
|
||||
in (fields, terms, ctxt') end;
|
||||
|
||||
|
@ -648,4 +653,7 @@ Term_Style.parse;
|
|||
Sign.certify_term;
|
||||
\<close>
|
||||
|
||||
|
||||
|
||||
|
||||
end
|
|
@ -121,6 +121,19 @@ Type.typ_instance: Type.tsig -> typ * typ -> bool
|
|||
|
||||
*}
|
||||
|
||||
text{* Type generalization is no longer part of the standard API. Here is a way to
|
||||
overcome this:*}
|
||||
|
||||
ML{*
|
||||
val ty = @{typ "'a option"};
|
||||
val ty' = @{typ "int option"};
|
||||
Sign.typ_instance @{theory}(ty', ty);
|
||||
val generalize_typ = Term.map_type_tfree (fn (str,sort)=> Term.TVar((str,0),sort));
|
||||
Sign.typ_instance @{theory} (ty', generalize_typ ty)
|
||||
*}
|
||||
|
||||
|
||||
|
||||
subsubsection\<open> Front End: Parsing issues \<close>
|
||||
|
||||
|
||||
|
|
|
@ -8,7 +8,7 @@ doc_class title =
|
|||
short_title :: "string option" <= "None"
|
||||
|
||||
doc_class subtitle =
|
||||
abbrev :: "string option" <= "[]"
|
||||
abbrev :: "string option" <= "None"
|
||||
|
||||
-- \<open>adding a contribution list and checking that it is cited as well in tech as in conclusion. ? \<close>
|
||||
|
||||
|
@ -16,7 +16,7 @@ doc_class author =
|
|||
affiliation :: "string"
|
||||
|
||||
doc_class abstract =
|
||||
keyword_list :: "string list" <= None
|
||||
keyword_list :: "string list" <= "[]"
|
||||
|
||||
doc_class text_section =
|
||||
main_author :: "author option" <= None
|
||||
|
@ -53,7 +53,7 @@ doc_class related_work = conclusion +
|
|||
main_author :: "author option" <= None
|
||||
|
||||
doc_class bibliography =
|
||||
style :: "string option" <= "''LNCS''"
|
||||
style :: "string option" <= "Some ''LNCS''"
|
||||
|
||||
text{* Besides subtyping, there is another relation between
|
||||
doc_classes: a class can be a \emph{monitor} to other ones,
|
||||
|
|
Reference in New Issue