(* Title:  BaseDefinitions/error-pattern-def.sml

    Author: Walther Neuper

    (c) due to copyright terms

 Here is a minimum of code required for theory Know_Store,

 further code see structure Error_Pattern.

 *)

 signature ERROR_PATTERN_DEFINITION =

 sig

   eqtype id

   type T = id * term list * thm list

   val s_to_string : T list -> string

   type fill_in_id

   type fill_in

 end

 (**)

 structure Error_Pattern_Def(**): ERROR_PATTERN_DEFINITION(**) =

 struct

 (**)

 type id = Rule_Def.errpatID

 type T =

   id          (* one identifier for a list of patterns                    *)

   * term list (* error patterns                                           *)

   * thm list  (* thms related to error patterns; note that respective lhs 

                  do not match (which reflects student's error).

                  fillpatterns are stored with these thms.                 *)

 fun errpat2str (id, tms, thms) =

   "(\"" ^ id ^ "\",\n" ^ UnparseC.terms tms ^ ",\n" ^ ThmC_Def.string_of_thms thms

 fun s_to_string errpats = (strs2str' o (map errpat2str)) errpats

 (* for (at least) 2 kinds of access:

   (1) given an id, find the respective fill_in's (e.g. in fun find_fill_patterns)

   (2) given a thm, find respective fill_in's *)

 type fill_in_id = string

 type fill_in =

   fill_in_id  (* DESIGN ?TODO: give an order w.r.t difficulty ? *)

   * term      (* the pattern with fill-in gaps                  *)

   * id;       (* which the fill_in would be a help for          

                  DESIGN ?TODO: list for several patterns ?      *)

 (**)end(**)