diff.ml

   1: (******************************************************************************
   2:  * Définitions du type des termes différentiels et utilitaires de bases
   3:  *****************************************************************************)
   4: 
   5: open List;;
   6: open Term_lexer;;
   7: 
   8: type diff_term   = DiffVar of int * string
   9:                  | DiffApp of diff_term * bunch
  10:                  | DiffAbs of string * int * diff_term
  11:                  | DiffStar
  12: and bunch        = monomial list
  13: and monomial     = (diff_term * int)
  14: ;;
  15: 
  16: type var_degrees = int list;;
  17: 
  18: (* affichage *)
  19: let rec string_of_diff : diff_term -> string =
  20:   fun t ->
  21:     match t with
  22:         DiffVar(_, x)        -> x
  23:       | DiffStar             -> "*"
  24:       | DiffAbs(x, _, u)     -> "[" ^ x ^ "]" ^ (string_of_diff u)
  25:       | DiffApp(f, b)        ->
  26:           "<" ^ (string_of_diff f) ^ ">" ^
  27:             match b with
  28:                 []         -> "{}"
  29:               | [(a, n)]  -> string_of_monome a n
  30:               | (a, n)::b'  -> "{" ^
  31:                   (fold_left (fun s (t, p) ->  s ^ " . " ^
  32:                                 (string_of_monome t p))
  33:                      (string_of_monome a n) b') ^ "}"
  34: 
  35: and string_of_monome : diff_term -> int -> string =
  36:   fun t p ->
  37:     if p = 1 then string_of_diff t
  38:     else match t with
  39:         DiffVar(_, x) -> x ^ "^" ^ (string_of_int p)
  40:       | _ ->
  41:           "(" ^ (string_of_diff t) ^ ")" ^ "^" ^ (string_of_int p)
  42: ;;
  43: 
  44: (* Opérations sur les degrés : une liste ne contenant que des 0 est égale à la
  45:    liste vide ; toutes les opérations supposent que le dernier élément de
  46:    chaque liste passée en argument est non nul et rendent un résultat de
  47:    même. *)
  48: let rec make_degrees : int -> int -> var_degrees =
  49:   fun n d ->
  50:     if d = 0 then []
  51:     else let rec make n =
  52:       if n = 0 then [d]
  53:       else 0::(make (n-1))
  54:     in make n
  55: ;;
  56: 
  57: let rec degrees_mult : int -> var_degrees -> var_degrees =
  58:   fun n ->
  59:     if n = 0 then fun _ -> []
  60:     else let rec mult =
  61:       function
  62:           [] -> []
  63:         | p::deg -> (n*p)::(mult deg)
  64:     in mult
  65: ;;
  66: 
  67: let rec degrees_substract : var_degrees -> var_degrees -> var_degrees =
  68:   fun deg1 deg2 ->
  69:     match (deg1, deg2) with
  70:         ([], []) -> []
  71:       | (deg, []) -> deg
  72:       | ([], _) -> failwith "degrees_substract : deg2 > deg1"
  73:       | (n::deg1', p::deg2') ->
  74:           if n < p then failwith "degrees_substract : deg2 > deg1"
  75:           else if n = p
  76:           then
  77:             let deg = degrees_substract deg1' deg2'
  78:             in if deg = [] then [] else 0::deg
  79:           else (n-p)::(degrees_substract deg1' deg2')
  80: ;;
  81: 
  82: let rec degrees_add : var_degrees -> var_degrees -> var_degrees =
  83:   fun deg1 deg2 ->
  84:     match (deg1, deg2) with
  85:         ([], deg) | (deg, []) -> deg
  86:       | (n::deg1', p::deg2') ->
  87:           let s = n+p
  88:           and deg = degrees_add deg1' deg2'
  89:           in if s = 0 && deg = [] then [] else s::deg
  90: ;;
  91: 
  92: let rec degrees_eq : var_degrees -> var_degrees -> bool =
  93:   fun deg1 deg2 ->
  94:     try degrees_substract deg1 deg2 = []
  95:     with Failure(_) -> false
  96: ;;
  97: 
  98: (* Opérations de base sur les termes différentiels. *)
  99: let rec diff_eq : diff_term -> diff_term -> bool =
 100:   fun t1 t2 ->
 101:     match (t1, t2) with
 102:         (DiffStar, DiffStar) -> true
 103:       | (DiffVar(n1, s1), DiffVar(n2, s2)) ->
 104:           (* On ne compare les noms que si la variable est libre *)
 105:           n1 = n2 && (n1 >= 0 || s1 = s2)
 106:       | (DiffApp(f1, b1), DiffApp(f2, b2)) ->
 107:           diff_eq f1 f2 && bunch_eq b1 b2
 108:       | (DiffAbs(_, d1, u1),  DiffAbs(_, d2, u2)) ->
 109:           d1 = d2 && diff_eq u1 u2
 110:       | _ -> false
 111: 
 112: (* Égalité de bunch *)
 113: and bunch_eq : bunch -> bunch -> bool =
 114:   fun b1 b2 ->
 115:     match b1 with
 116:         [] -> b2 = []
 117:       | m1::b1' ->
 118:           try
 119:             let b2' = bunch_divide b2 m1
 120:             in bunch_eq b1' b2'
 121:           with Not_found -> false
 122: 
 123: and bunch_divide : bunch -> monomial -> bunch =
 124:   fun b ((t, p) as m) ->
 125:     match b with
 126:         [] -> if p = 0 then [] else raise Not_found
 127:       | ((t', p') as m')::b' ->
 128:         if diff_eq t t'
 129:         then
 130:           if p' > p then (t', p' - p)::b'
 131:           else if p' = p  then b'
 132:           else bunch_divide b' (t, (p'-p))
 133:         else m'::(bunch_divide b' m)
 134: ;;
 135: 
 136: (* Ajout d'un élément *)
 137: let rec monomial_bunch_mult : monomial -> bunch -> bunch =
 138:   fun ((t, n) as m) ->
 139:     function
 140:         [] -> if n = 0 then [] else [m]
 141:       | (t', p)::b' ->
 142:           if diff_eq t t'
 143:           then (t', n + p)::b'
 144:           else (t', p)::(monomial_bunch_mult m b')
 145: ;;
 146: 
 147: let rec bunch_mult : bunch -> bunch -> bunch =
 148:   fun b1 b2 ->
 149:     match b1 with
 150:         [] -> b2
 151:       | m::b1' -> bunch_mult b1' (monomial_bunch_mult m b2)
 152: ;;
 153: 
 154: let rec bunch_power : bunch -> int -> bunch =
 155:   fun b n ->
 156:     let rec pow =
 157:       function
 158:           [] -> []
 159:         | (t, p)::b -> (t, n*p)::(pow b)
 160:     in if n = 0 then [] else pow b
 161: ;;
 162: 
 163: let rec bunch_length : bunch -> int =
 164:   function
 165:       [] -> 0
 166:     | (_, n):: b' -> n + (bunch_length b')
 167: ;;
 168: 
 169: (*****************************************************************************
 170:  * Parsing
 171:  *****************************************************************************
 172:  *
 173:  * diff   = '$' ident | '#' ident
 174:           | var | '[' var ']' diff  | '<' diff  '>' bunch
 175:  * bunch  = monome | '{' monome {'.' monome} '}'
 176:  * monome = terme ['^' int] | '(' terme ')' ['^' int]
 177:  *
 178:  * Exemples : [x]<x>{x . x} = [x]<x>{x^2} = [x]<x>x^2
 179:  *            [f][x]<f>{<f>{x . x} . <f>{x . x}} = [f][x]<f>(<f>x^2)^2
 180:  *            [f][x]<f>{(<f>x)^2 . <f>x^2}
 181:  *            [f]<f>([z]z)^2
 182:  *
 183:  * define_dmacro "f11" "<<f>{}>{}"
 184:  * define_diff   "s1" "[f][x]<<f>#f11><<f>#f11>#f11"
 185:  * define_diff   "s2" "[f][x]<<f><<f>#f11>#f11>#f11"
 186:  *
 187:  *****************************************************************************)
 188: 
 189: 
 190: (* Tables des termes et macros différentiels prédéfinis *)
 191: let diff_table : (string,  diff_term) Hashtbl.t = Hashtbl.create(17)
 192: and diff_macros_table : (string, string) Hashtbl.t = Hashtbl.create(17)
 193: ;;
 194: 
 195: let rec diff_of_stream : token_stream -> diff_term = fun tokens ->
 196:   let rec parse_term : string list -> token_stream -> (diff_term * var_degrees)
 197:     = fun binders  ->
 198:       parser
 199:           [< 'Kwd '$'; 'Ident name >] -> (Hashtbl.find diff_table name, [])
 200:         | [< 'Kwd '#'; 'Ident name >] ->
 201:             parse_term binders
 202:               (term_lexer (Hashtbl.find diff_macros_table name))
 203:         | [< 'Kwd '[';
 204:              'Ident x ?? "no variable in lambda";
 205:              'Kwd ']' ?? "lambda not terminated" ;
 206:              (t, deg_t) = parse_term (x::binders) >] -> (
 207:             match deg_t with
 208:                 [] -> (DiffAbs(x, 0, t), [])
 209:               | d::deg' -> (DiffAbs(x, d, t), deg')
 210:           )
 211:         | [< 'Kwd '<';
 212:              (t, deg_t) = parse_term binders;
 213:              'Kwd '>' ?? "application not terminated";
 214:              (b, deg_b) = parse_bunch binders; >] ->
 215:             (DiffApp(t, b), degrees_add deg_t deg_b)
 216:         | [< 'Ident x >] ->
 217:             let index = index_of x binders
 218:             in (DiffVar(index, x), make_degrees index 1)
 219:         | [< 'Kwd '*' >] -> (DiffStar, [])
 220: 
 221:   and parse_bunch : string list -> token_stream -> (bunch * var_degrees) =
 222:     fun binders ->
 223:       parser
 224:           [< 'Kwd '{';
 225:              b = parse_monome_list binders >] -> b
 226:         | [< ((t, n), deg_t) = parse_monome binders >] ->
 227:             ([(t, n)], degrees_mult n deg_t)
 228: 
 229:   and parse_monome_list : string list -> token_stream -> (bunch * var_degrees)
 230:     = fun binders ->
 231:       parser
 232:           [< ((t, n)  as m, deg_t) = parse_monome binders; rest >] -> (
 233:             match Stream.peek rest with
 234:                 Some(Kwd('.')) ->
 235:                   Stream.junk rest;
 236:                   let (b, deg_b) = parse_monome_list binders rest
 237:                   in (monomial_bunch_mult m b,
 238:                       degrees_add (degrees_mult n deg_t) deg_b)
 239:               | Some(Kwd('}'))  ->
 240:                   Stream.junk rest;
 241:                   ([(t, n)], degrees_mult n deg_t)
 242:               | _ -> raise (Stream.Error("invalid char in bunch"))
 243:           )
 244:         | [< 'Kwd '}' >] -> ([], [])
 245: 
 246:   and parse_monome : string list -> token_stream -> (monomial * var_degrees) =
 247:     fun binders ->
 248:       parser
 249:         | [< 'Kwd '(';
 250:              (t, deg_t) = parse_term binders;
 251:              'Kwd ')' ?? "missing closing paren";
 252:              n = parse_exponant >] -> ((t, n), deg_t)
 253:         | [< (t, deg_t) = parse_term binders;
 254:              n = parse_exponant >] -> ((t, n), deg_t)
 255: 
 256:   and parse_exponant : token_stream -> int =
 257:     parser
 258:         [< 'Kwd '^'; 'Int n >] -> n
 259:       | [< >] -> 1
 260: 
 261:   in let (t, _) = parse_term [] tokens
 262:   in match Stream.peek tokens with
 263:       Some(_) -> raise (Stream.Error("garbage at end of stream"))
 264:     | None    -> t
 265: 
 266: and diff_of_string : string -> diff_term =
 267:   fun s -> diff_of_stream (term_lexer s)
 268: ;;
 269: 
 270: let define_diff : string -> string -> unit = fun name term ->
 271:   Hashtbl.replace diff_table name (diff_of_string term)
 272: and define_dmacro : string -> string -> unit = fun name term ->
 273:   Hashtbl.replace diff_macros_table name term
 274: ;;
 275: 

This document was generated using caml2html