Lines Matching refs:function
14 (* The basic idea is to duplicate a datatype declaration at each type used and a function *)
16 (* and function. *)
46 fun is_fun t = (* the term is a function? *)
59 (* Format: [function's name |-> [type |-> instantiation set] ] *)
62 (* Format: [function's name |-> a set of new defitions] *)
172 (* SOME (#1 ((strip_comb o lhs o concl o SPEC_ALL o DB.definition) (f_str ^ "_def"))) (* be a predefined function *) *)
182 if is_pabs M then (* an embedded function *)
215 else if is_fun M then (* function application *)
227 (* handle _ => M.mkDict strOrder (* not function application *) *)
255 (* format: function name |-> new definition *)
272 val MonoFunc = ref (M.mkDict tvarWithTypeOrder) (* a map from polymorphic function name to the names of its clones *)
275 (* Create the clones of a function according to the instantiation information in the instantiation map *)
297 if null insts then (* the function is already monomorphistic, no instantiations are needed *)
310 else (* instantiate types and replace all polymorphic function calls with corresponding monomorphic calls *)