(* Title:  MathEngBasic/calc-tree-elem.sml

   Author: Walther Neuper 191026

   (c) due to copyright terms

Definitions for Tactic.T and Ctree.

*)

signature MODEL_DEFINITION =

sig

  type form_T

  type form_model

  type form_spec

  val form_empty : form_T

  type variants

  type m_field = Model_Pattern.m_field

  type descriptor = Model_Pattern.descriptor

  type o_model

  type o_model_single

  val o_model_to_string : o_model -> string

  val o_model_single_to_string : o_model_single -> string

  val o_model_empty : o_model_single

  type i_model

  type i_model_single

  datatype i_model_feedback = Cor of (term * (term list)) * (term * (term list))

    | Syn of TermC.as_string | Typ of TermC.as_string | Inc of (term * (term list))	* (term * (term list))

    | Sup of (term * (term list)) | Mis of (term * term) | Par of TermC.as_string

  val i_model_empty : i_model_single

end

(**)                   

structure Model_Def(**): MODEL_DEFINITION(**) =        

struct

(**)

type m_field = Model_Pattern.m_field;

type descriptor = Model_Pattern.descriptor;

(** definitions for Formalise.T **)

type form_model = TermC.as_string list;

type form_spec = Spec.T;

type form_T = form_model * form_spec;

val form_empty = ([], Spec.empty);

type variants = int list; (* variants given by Formalise.T *)

(** definitions for O_Model.T **)

type o_model_single =

  (int *           (* sequence of input, 0 = untouched, drop with PIDE *)

	variants * (* pointers to variants given in Formalise.T        *)

	m_field *  (* #Given | #Find | #Relat                          *)

	term *     (* descriptor, see Input_Descript.thy               *)

	term list  (* isalist2list t | [t]                             *)

	);

type o_model = o_model_single list;

val o_model_empty = (0, [], "", TermC.empty, [TermC.empty]) : o_model_single;

fun o_model_single_to_string (i, vs, fi, t, ts) = 

  "(" ^ string_of_int i ^ ", " ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ "," ^

  UnparseC.term t ^ ", " ^ (strs2str o (map UnparseC.term)) ts ^ ")";

val o_model_to_string = strs2str' o (map (linefeed o o_model_single_to_string));

(** definitions for I_Model.T **)

datatype i_model_feedback = 

  Cor of (term *   (* correct input: descriptor, see Input_Descript.thy    *)

    (term list)) *            (* set as list for element-wise input        *)

   (term * (term list))       (* elem of penv -?- penv delayed to future   *)

| Syn of TermC.as_string      (* syntax error: drop with PIDE ?            *)

| Typ of TermC.as_string      (* type error: drop with PIDE ?              *)

| Inc of (term * (term list))	* (term * (term list)) (* penv -?-           *)

| Sup of (term * (term list)) (* superfluous; input not found in O_Model.T *)

| Mis of (term * term)        (* missing; for feedback                     *)

| Par of TermC.as_string;     (* internal state from fun parsitm           *)

type i_model_single = 

  int *             (* sequence of input, 0 = untouched, drop with PIDE ?  *)

  variants *        (* pointers to variants given in Formalise.T           *)

  bool *            (* input on this item is not/complete                  *)

  m_field *         (* #Given | #Find | #Relate                            *)

  i_model_feedback; (* see above                                           *)

type i_model = i_model_single list;

val i_model_empty = (0, [], false, "i_model_empty", Syn "i_model_empty");

(**)end(**)