1.1 --- a/src/Tools/isac/Specify/o-model.sml	Fri May 08 18:30:21 2020 +0200
     1.2 +++ b/src/Tools/isac/Specify/o-model.sml	Sat May 09 11:55:51 2020 +0200
     1.3 @@ -1,7 +1,11 @@
     1.4  (* Title:  Specify/o-model.sml
     1.5     Author: Walther Neuper 110226
     1.6     (c) due to copyright terms
     1.7 - *)
     1.8 +
     1.9 +Original model created initially from Formale.T and Model_Pattern.T;
    1.10 +This model makes student's editing via I_Model.T more efficient.
    1.11 +TODO: revise with an example with more than 1 variant.
    1.12 +*)
    1.13  
    1.14  signature ORIGINAL_MODEL =
    1.15  sig
    1.16 @@ -15,8 +19,6 @@
    1.17  
    1.18    val init: Formalise.model -> theory -> Model_Pattern.T -> T
    1.19  
    1.20 -  val split_dts: term -> descriptor * term list
    1.21 -  val split_dts': term * term -> term list
    1.22    val add_field: theory -> Model_Pattern.T -> term * 'b -> m_field * descriptor * 'b
    1.23    val add_variants: ('a * ''b * 'c) list -> (int * ('a * ''b * 'c)) list
    1.24    val max: variants -> int
    1.25 @@ -52,47 +54,6 @@
    1.26    UnparseC.term t ^ ", " ^ (strs2str o (map UnparseC.term)) ts ^ ")";
    1.27  val preoris2str = (strs2str' o (map (linefeed o preori2str)));
    1.28  
    1.29 -(* special handling for lists. ?WN:14.5.03 ??!? *)
    1.30 -fun dest_list (d, ts) = 
    1.31 -  let fun dest t = 
    1.32 -    if Input_Descript.is_list_dsc d andalso not (Input_Descript.is_unl d) andalso not (is_Free t) (*..for pbt*)
    1.33 -    then TermC.isalist2list t
    1.34 -    else [t]
    1.35 -  in (flat o (map dest)) ts end;
    1.36 -
    1.37 -(* take list-term apart w.r.t. handling elementwise input: @{term "[a, b]"} \<rightarrow> ["[a]","[b]"] *)
    1.38 -fun take_apart t =
    1.39 -  let val elems = TermC.isalist2list t
    1.40 -  in map ((TermC.list2isalist (type_of (hd elems))) o single) elems end;
    1.41 -
    1.42 -(* decompose an input into description, terms (ev. elems of lists),
    1.43 -    and the value for the problem-environment; inv to comp_dts   *)
    1.44 -fun split_dts (t as d $ arg) =
    1.45 -    if Input_Descript.is_dsc d
    1.46 -    then if Input_Descript.is_list_dsc d andalso TermC.is_list arg andalso Input_Descript.is_unl d |> not
    1.47 -      then (d, take_apart arg)
    1.48 -      else (d, [arg])
    1.49 -    else (TermC.empty, TermC.dest_list' t)
    1.50 -  | split_dts t =
    1.51 -    let val t' as (h, _) = strip_comb t;
    1.52 -    in
    1.53 -      if Input_Descript.is_dsc h
    1.54 -      then (h, dest_list t')
    1.55 -      else (TermC.empty, TermC.dest_list' t)
    1.56 -    end;
    1.57 -
    1.58 -(* version returning ts only *)
    1.59 -fun split_dts' (d, arg) = 
    1.60 -    if Input_Descript.is_dsc d
    1.61 -    then if Input_Descript.is_list_dsc d
    1.62 -      then if TermC.is_list arg
    1.63 -	      then if Input_Descript.is_unl d
    1.64 -	        then ([arg])           (* e.g. someList [1,3,2]                 *)
    1.65 -		      else (take_apart arg)  (* [a,b] --> SML[ [a], [b] ]SML          *)
    1.66 -	      else ([arg])             (* a variable or metavariable for a list *)
    1.67 -	     else ([arg])
    1.68 -    else (TermC.dest_list' arg)
    1.69 -
    1.70  (* compare d and dsc in pbt and transfer field to pre-ori *)
    1.71  fun add_field (_: theory) pbt (d,ts) = 
    1.72    let fun eq d pt = (d = (fst o snd) pt);
    1.73 @@ -158,7 +119,7 @@
    1.74      let
    1.75        val model = (map (fn str => str
    1.76                       |> TermC.parseNEW'' thy
    1.77 -                     |> split_dts
    1.78 +                     |> Input_Descript.split
    1.79                       |> add_field thy pbt) fmz)
    1.80                    |> add_variants;
    1.81        val maxv = model |> map fst |> max;