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

   Author: Walther Neuper

   (c) due to copyright terms

*)

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(**)