pierre.derathe
/
Isabelle_DOF
Archived
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Some useful stuff on the Type and Sign interfaces documented,

This commit is contained in:
Burkhart Wolff 2018-04-17 16:25:32 +02:00
parent cf1f4399eb
commit a39e0b1b19
1 changed files with 49 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

49
MyCommentedIsabelle.thy
View File

@ -76,7 +76,54 @@ op --;
op ?;
*}
subsubsection\<open> Kernel: terms, types, thms \<close>
text \<open>A basic data-structure of the kernel is term.ML \<close>
ML{* open Term;
(*
type indexname = string * int
type class = string
type sort = class list
type arity = string * sort list * sort
datatype typ =
Type of string * typ list |
TFree of string * sort |
TVar of indexname * sort
datatype term =
Const of string * typ |
Free of string * typ |
Var of indexname * typ |
Bound of int |
Abs of string * typ * term |
$ of term * term
exception TYPE of string * typ list * term list
exception TERM of string * term list
*)
(* there is a joker type that can be added as place-holder during term construction.*)
Term.dummyT : typ
*}
text{* Jokers can be eliminated by the type inference. *}
ML{*
Sign.typ_instance: theory -> typ * typ -> bool;
Sign.typ_unify: theory -> typ * typ -> Type.tyenv * int -> Type.tyenv * int;
Sign.const_type: theory -> string -> typ option;
Sign.certify_term: theory -> term -> term * typ * int;
Sign.cert_term: theory -> term -> term;
*}
text{* This is actually an abstract wrapper on the structure Type which contains the heart of
the type inference. *}
ML{*
Type.typ_instance: Type.tsig -> typ * typ -> bool
(* raises TYPE_MATCH *)
*}
subsubsection\<open> Front End: Parsing issues \<close>
(* Tokens and Bindings *)
ML{*
@ -612,4 +659,6 @@ fun document_antiq check_file ctxt (name, pos) =
*}
ML{* Type_Infer_Context.prepare_positions *}
end