Symmetries.ml

(* Copyright INRIA and Microsoft Corporation, 2008-2013. *)
(* DDMF is distributed under CeCILL-B license. *)

INCLUDE "preamble.ml"

(* Would it be cautious to use None here? *)
(* Also, it seems one should be able to call SymmetriesProof with this type *)
(* as last argument, instead of passing a string. *)
type t = NoSym | Odd | Even

let string_of_symmetry = function
| NoSym -> assert false
| Odd -> "odd"
| Even -> "even"

let validity_domain () =
  let singDistance =
    << min(map(abs, [solve(op(nops(fdiffeq), fdiffeq) = 0, x)])): >> in
  <:par< for all complex numbers <:imath< x >>>> @:@
  (if <:bool< $(singDistance) < infinity >> then
    <:par< with <:imath< |x| < $(symb:singDistance) >>.>>
   else <:par<.>>)

let title _ = <:text<Symmetries>>

let_service Symmetries
  (def : diffeq maple)
  (yofz : fcall maple)
  (func_of_var : string)
  (func_of_neg : string) :
  DC.sec_entities * t with { title = title } =

  (* This duplication of code will be removed when we are able to run *)
  (* symmetriesProof without display, to get the output and use it, *)
  (* and display the display only later. *)

  <:unit<
    unassign('iniconds','y','x'):
    fdiffeq := gfun:-formatdiffeq([$(def),$(yofz)],'y','x','iniconds'):
    if evalb(op(1,fdiffeq) <> 0) then
      defHom := gfun:-diffeqtohomdiffeq($(def),y(x)):
      unassign('iniconds','y','x'):
      fdiffeq := gfun:-formatdiffeq([defHom,$(yofz)],'y','x','iniconds'):
    end if ;

    altDiffeq := subs(x = -x, fdiffeq):
    for i from 2 to nops(altDiffeq) do
      if type(i, odd) then
        altDiffeq := subsop(i = -op(i,altDiffeq), altDiffeq)
      end if
    end do:

    diffeqSymmetric := evalb(fdiffeq = altDiffeq):
    originRegular := evalb(subs(x=0, op(-1,fdiffeq)) <> 0):
    enoughICs := evalb(nops(iniconds) = nops(fdiffeq) - 2):
    isOdd := originRegular and enoughICs and diffeqSymmetric:
    isEven := originRegular and enoughICs and diffeqSymmetric:

    for i from 1 to nops(iniconds) do
      if (-1)^i*op(2,op(i,iniconds)) <> -op(2,op(i,iniconds)) then
        isEven := false;
      end if;
      if (-1)^i*op(2,op(i,iniconds)) <> op(2,op(i,iniconds)) then
        isOdd := false;
      end if;
    end do;
  >> ;

  let sym =
    if <:bool< isOdd >> then Odd
    else if <:bool< isEven >> then Even
    else NoSym in
  let body =
    if sym != NoSym then
      let str_sym = string_of_symmetry sym in
      let math_sym = match sym with
      | NoSym -> assert false
      | Odd -> func_of_var ^ " = -" ^ func_of_neg
      | Even -> func_of_var ^ " = " ^ func_of_neg
      and link =
        DC.link_service
          (SymmetriesProof.descr
             (def, yofz, func_of_var, func_of_neg, str_sym) None)
          <:text<proof>> in
      (<:par<
          The function <:imath< $(str: func_of_var) >> is $(str: str_sym):
          <:dmath< $(str:math_sym) >>
         >> @:@
         validity_domain ()) @@@
        <:par< See the $(link). >>
    else DC.ent_null in
  (DC.section <:text<Symmetry>> body, sym)

Generated by GNU Enscript 1.6.5.90.