src/Tools/Metis/src/Term.sml

removed obsolete Markup_Tree.flatten/filter;

(* ========================================================================= *)
(* FIRST ORDER LOGIC TERMS                                                   *)
(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)

structure Term :> Term =
struct

open Useful;

(* ------------------------------------------------------------------------- *)
(* Helper functions.                                                         *)
(* ------------------------------------------------------------------------- *)

fun stripSuffix pred s =
    let
      fun f 0 = ""
        | f n =
          let
            val n' = n - 1
          in
            if pred (String.sub (s,n')) then f n'
            else String.substring (s,0,n)
          end
    in
      f (size s)
    end;

(* ------------------------------------------------------------------------- *)
(* A type of first order logic terms.                                        *)
(* ------------------------------------------------------------------------- *)

type var = Name.name;

type functionName = Name.name;

type function = functionName * int;

type const = functionName;

datatype term =
    Var of Name.name
  | Fn of Name.name * term list;

(* ------------------------------------------------------------------------- *)
(* Constructors and destructors.                                             *)
(* ------------------------------------------------------------------------- *)

(* Variables *)

fun destVar (Var v) = v
  | destVar (Fn _) = raise Error "destVar";

val isVar = can destVar;

fun equalVar v (Var v') = v = v'
  | equalVar _ _ = false;

(* Functions *)

fun destFn (Fn f) = f
  | destFn (Var _) = raise Error "destFn";

val isFn = can destFn;

fun fnName tm = fst (destFn tm);

fun fnArguments tm = snd (destFn tm);

fun fnArity tm = length (fnArguments tm);

fun fnFunction tm = (fnName tm, fnArity tm);

local
  fun func fs [] = fs
    | func fs (Var _ :: tms) = func fs tms
    | func fs (Fn (n,l) :: tms) =
      func (NameAritySet.add fs (n, length l)) (l @ tms);
in
  fun functions tm = func NameAritySet.empty [tm];
end;

local
  fun func fs [] = fs
    | func fs (Var _ :: tms) = func fs tms
    | func fs (Fn (n,l) :: tms) = func (NameSet.add fs n) (l @ tms);
in
  fun functionNames tm = func NameSet.empty [tm];
end;

(* Constants *)

fun mkConst c = (Fn (c, []));

fun destConst (Fn (c, [])) = c
  | destConst _ = raise Error "destConst";

val isConst = can destConst;

(* Binary functions *)

fun mkBinop f (a,b) = Fn (f,[a,b]);

fun destBinop f (Fn (x,[a,b])) =
    if x = f then (a,b) else raise Error "Term.destBinop: wrong binop"
  | destBinop _ _ = raise Error "Term.destBinop: not a binop";

fun isBinop f = can (destBinop f);

(* ------------------------------------------------------------------------- *)
(* The size of a term in symbols.                                            *)
(* ------------------------------------------------------------------------- *)

val VAR_SYMBOLS = 1;

val FN_SYMBOLS = 1;

local
  fun sz n [] = n
    | sz n (Var _ :: tms) = sz (n + VAR_SYMBOLS) tms
    | sz n (Fn (func,args) :: tms) = sz (n + FN_SYMBOLS) (args @ tms);
in
  fun symbols tm = sz 0 [tm];
end;

(* ------------------------------------------------------------------------- *)
(* A total comparison function for terms.                                    *)
(* ------------------------------------------------------------------------- *)

local
  fun cmp [] [] = EQUAL
    | cmp (Var _ :: _) (Fn _ :: _) = LESS
    | cmp (Fn _ :: _) (Var _ :: _) = GREATER
    | cmp (Var v1 :: tms1) (Var v2 :: tms2) =
      (case Name.compare (v1,v2) of
         LESS => LESS
       | EQUAL => cmp tms1 tms2
       | GREATER => GREATER)
    | cmp (Fn (f1,a1) :: tms1) (Fn (f2,a2) :: tms2) =
      (case Name.compare (f1,f2) of
         LESS => LESS
       | EQUAL =>
         (case Int.compare (length a1, length a2) of
            LESS => LESS
          | EQUAL => cmp (a1 @ tms1) (a2 @ tms2)
          | GREATER => GREATER)
       | GREATER => GREATER)
    | cmp _ _ = raise Bug "Term.compare";
in
  fun compare (tm1,tm2) = cmp [tm1] [tm2];
end;

(* ------------------------------------------------------------------------- *)
(* Subterms.                                                                 *)
(* ------------------------------------------------------------------------- *)

type path = int list;

fun subterm tm [] = tm
  | subterm (Var _) (_ :: _) = raise Error "Term.subterm: Var"
  | subterm (Fn (_,tms)) (h :: t) =
    if h >= length tms then raise Error "Term.replace: Fn"
    else subterm (List.nth (tms,h)) t;

local
  fun subtms [] acc = acc
    | subtms ((path,tm) :: rest) acc =
      let
        fun f (n,arg) = (n :: path, arg)

        val acc = (rev path, tm) :: acc
      in
        case tm of
          Var _ => subtms rest acc
        | Fn (_,args) => subtms (map f (enumerate args) @ rest) acc
      end;
in
  fun subterms tm = subtms [([],tm)] [];
end;

fun replace tm ([],res) = if res = tm then tm else res
  | replace tm (h :: t, res) =
    case tm of
      Var _ => raise Error "Term.replace: Var"
    | Fn (func,tms) =>
      if h >= length tms then raise Error "Term.replace: Fn"
      else
        let
          val arg = List.nth (tms,h)
          val arg' = replace arg (t,res)
        in
          if Sharing.pointerEqual (arg',arg) then tm
          else Fn (func, updateNth (h,arg') tms)
        end;

fun find pred =
    let
      fun search [] = NONE
        | search ((path,tm) :: rest) =
          if pred tm then SOME (rev path)
          else
            case tm of
              Var _ => search rest
            | Fn (_,a) =>
              let
                val subtms = map (fn (i,t) => (i :: path, t)) (enumerate a)
              in
                search (subtms @ rest)
              end
    in
      fn tm => search [([],tm)]
    end;

val ppPath = Parser.ppList Parser.ppInt;

val pathToString = Parser.toString ppPath;

(* ------------------------------------------------------------------------- *)
(* Free variables.                                                           *)
(* ------------------------------------------------------------------------- *)

local
  fun free _ [] = false
    | free v (Var w :: tms) = v = w orelse free v tms
    | free v (Fn (_,args) :: tms) = free v (args @ tms);
in
  fun freeIn v tm = free v [tm];
end;

local
  fun free vs [] = vs
    | free vs (Var v :: tms) = free (NameSet.add vs v) tms
    | free vs (Fn (_,args) :: tms) = free vs (args @ tms);
in
  fun freeVars tm = free NameSet.empty [tm];
end;

(* ------------------------------------------------------------------------- *)
(* Fresh variables.                                                          *)
(* ------------------------------------------------------------------------- *)

local
  val prefix  = "_";

  fun numVar i = Var (mkPrefix prefix (Int.toString i));
in
  fun newVar () = numVar (newInt ());

  fun newVars n = map numVar (newInts n);
end;

fun variantPrime avoid =
    let
      fun f v = if NameSet.member v avoid then f (v ^ "'") else v
    in
      f
    end;

fun variantNum avoid v =
    if not (NameSet.member v avoid) then v
    else
      let
        val v = stripSuffix Char.isDigit v
                                                                    
        fun f n =
            let
              val v_n = v ^ Int.toString n
            in
              if NameSet.member v_n avoid then f (n + 1) else v_n
            end
      in
        f 0
      end;

(* ------------------------------------------------------------------------- *)
(* Special support for terms with type annotations.                          *)
(* ------------------------------------------------------------------------- *)

fun isTypedVar (Var _) = true
  | isTypedVar (Fn (":", [Var _, _])) = true
  | isTypedVar (Fn _) = false;

local
  fun sz n [] = n
    | sz n (Var _ :: tms) = sz (n + 1) tms
    | sz n (Fn (":",[tm,_]) :: tms) = sz n (tm :: tms)
    | sz n (Fn (_,args) :: tms) = sz (n + 1) (args @ tms);
in
  fun typedSymbols tm = sz 0 [tm];
end;

local
  fun subtms [] acc = acc
    | subtms ((_, Var _) :: rest) acc = subtms rest acc
    | subtms ((_, Fn (":", [Var _, _])) :: rest) acc = subtms rest acc
    | subtms ((path, tm as Fn func) :: rest) acc =
      let
        fun f (n,arg) = (n :: path, arg)

        val acc = (rev path, tm) :: acc
      in
        case func of
          (":",[arg,_]) => subtms ((0 :: path, arg) :: rest) acc
        | (_,args) => subtms (map f (enumerate args) @ rest) acc
      end;
in
  fun nonVarTypedSubterms tm = subtms [([],tm)] [];
end;

(* ------------------------------------------------------------------------- *)
(* Special support for terms with an explicit function application operator. *)
(* ------------------------------------------------------------------------- *)

fun mkComb (f,a) = Fn (".",[f,a]);

fun destComb (Fn (".",[f,a])) = (f,a)
  | destComb _ = raise Error "destComb";

val isComb = can destComb;

fun listMkComb (f,l) = foldl mkComb f l;

local
  fun strip tms (Fn (".",[f,a])) = strip (a :: tms) f
    | strip tms tm = (tm,tms);
in
  fun stripComb tm = strip [] tm;
end;

(* ------------------------------------------------------------------------- *)
(* Parsing and pretty printing.                                              *)
(* ------------------------------------------------------------------------- *)

(* Operators parsed and printed infix *)

val infixes : Parser.infixities ref = ref
  [(* ML symbols *)
   {token = " / ", precedence = 7, leftAssoc = true},
   {token = " div ", precedence = 7, leftAssoc = true},
   {token = " mod ", precedence = 7, leftAssoc = true},
   {token = " * ", precedence = 7, leftAssoc = true},
   {token = " + ", precedence = 6, leftAssoc = true},
   {token = " - ", precedence = 6, leftAssoc = true},
   {token = " ^ ", precedence = 6, leftAssoc = true},
   {token = " @ ", precedence = 5, leftAssoc = false},
   {token = " :: ", precedence = 5, leftAssoc = false},
   {token = " = ", precedence = 4, leftAssoc = true},
   {token = " <> ", precedence = 4, leftAssoc = true},
   {token = " <= ", precedence = 4, leftAssoc = true},
   {token = " < ", precedence = 4, leftAssoc = true},
   {token = " >= ", precedence = 4, leftAssoc = true},
   {token = " > ", precedence = 4, leftAssoc = true},
   {token = " o ", precedence = 3, leftAssoc = true},
   {token = " -> ", precedence = 2, leftAssoc = false},  (* inferred prec *)
   {token = " : ", precedence = 1, leftAssoc = false},  (* inferred prec *)
   {token = ", ", precedence = 0, leftAssoc = false},  (* inferred prec *)

   (* Logical connectives *)
   {token = " /\\ ", precedence = ~1, leftAssoc = false},
   {token = " \\/ ", precedence = ~2, leftAssoc = false},
   {token = " ==> ", precedence = ~3, leftAssoc = false},
   {token = " <=> ", precedence = ~4, leftAssoc = false},

   (* Other symbols *)
   {token = " . ", precedence = 9, leftAssoc = true},  (* function app *)
   {token = " ** ", precedence = 8, leftAssoc = true},
   {token = " ++ ", precedence = 6, leftAssoc = true},
   {token = " -- ", precedence = 6, leftAssoc = true},
   {token = " == ", precedence = 4, leftAssoc = true}];

(* The negation symbol *)

val negation : Name.name ref = ref "~";

(* Binder symbols *)

val binders : Name.name list ref = ref ["\\","!","?","?!"];

(* Bracket symbols *)

val brackets : (Name.name * Name.name) list ref = ref [("[","]"),("{","}")];

(* Pretty printing *)

local
  open Parser;
in
  fun pp inputPpstrm inputTerm =
      let
        val quants = !binders
        and iOps = !infixes
        and neg = !negation
        and bracks = !brackets

        val bracks = map (fn (b1,b2) => (b1 ^ b2, b1, b2)) bracks

        val bTokens = map #2 bracks @ map #3 bracks

        val iTokens = infixTokens iOps

        fun destI (Fn (f,[a,b])) =
            if mem f iTokens then SOME (f,a,b) else NONE
          | destI _ = NONE

        val iPrinter = ppInfixes iOps destI

        val specialTokens = neg :: quants @ ["$","(",")"] @ bTokens @ iTokens

        fun vName bv s = NameSet.member s bv

        fun checkVarName bv s = if vName bv s then s else "$" ^ s

        fun varName bv = ppMap (checkVarName bv) ppString

        fun checkFunctionName bv s =
            if mem s specialTokens orelse vName bv s then "(" ^ s ^ ")" else s

        fun functionName bv = ppMap (checkFunctionName bv) ppString

        fun isI tm = Option.isSome (destI tm)

        fun stripNeg (tm as Fn (f,[a])) =
            if f <> neg then (0,tm)
            else let val (n,tm) = stripNeg a in (n + 1, tm) end
          | stripNeg tm = (0,tm)

        val destQuant =
            let
              fun dest q (Fn (q', [Var v, body])) =
                  if q <> q' then NONE
                  else
                    (case dest q body of
                       NONE => SOME (q,v,[],body)
                     | SOME (_,v',vs,body) => SOME (q, v, v' :: vs, body))
                | dest _ _ = NONE
            in
              fn tm => Useful.first (fn q => dest q tm) quants
            end

        fun isQuant tm = Option.isSome (destQuant tm)

        fun destBrack (Fn (b,[tm])) =
            (case List.find (fn (n,_,_) => n = b) bracks of
               NONE => NONE
             | SOME (_,b1,b2) => SOME (b1,tm,b2))
          | destBrack _ = NONE

        fun isBrack tm = Option.isSome (destBrack tm)
            
        fun functionArgument bv ppstrm tm =
            (addBreak ppstrm (1,0);
             if isBrack tm then customBracket bv ppstrm tm
             else if isVar tm orelse isConst tm then basic bv ppstrm tm
             else bracket bv ppstrm tm)

        and basic bv ppstrm (Var v) = varName bv ppstrm v
          | basic bv ppstrm (Fn (f,args)) =
            (beginBlock ppstrm Inconsistent 2;
             functionName bv ppstrm f;
             app (functionArgument bv ppstrm) args;
             endBlock ppstrm)

        and customBracket bv ppstrm tm =
            case destBrack tm of
              SOME (b1,tm,b2) => ppBracket b1 b2 (term bv) ppstrm tm
            | NONE => basic bv ppstrm tm

        and innerQuant bv ppstrm tm =
            case destQuant tm of
              NONE => term bv ppstrm tm
            | SOME (q,v,vs,tm) =>
              let
                val bv = NameSet.addList (NameSet.add bv v) vs
              in
                addString ppstrm q;
                varName bv ppstrm v;
                app (fn v => (addBreak ppstrm (1,0); varName bv ppstrm v)) vs;
                addString ppstrm ".";
                addBreak ppstrm (1,0);
                innerQuant bv ppstrm tm
              end

        and quantifier bv ppstrm tm =
            if not (isQuant tm) then customBracket bv ppstrm tm
            else
              (beginBlock ppstrm Inconsistent 2;
               innerQuant bv ppstrm tm;
               endBlock ppstrm)

        and molecule bv ppstrm (tm,r) =
            let
              val (n,tm) = stripNeg tm
            in
              beginBlock ppstrm Inconsistent n;
              funpow n (fn () => addString ppstrm neg) ();
              if isI tm orelse (r andalso isQuant tm) then bracket bv ppstrm tm
              else quantifier bv ppstrm tm;
              endBlock ppstrm
            end

        and term bv ppstrm tm = iPrinter (molecule bv) ppstrm (tm,false)

        and bracket bv ppstrm tm = ppBracket "(" ")" (term bv) ppstrm tm
  in
    term NameSet.empty
  end inputPpstrm inputTerm;
end;

fun toString tm = Parser.toString pp tm;

(* Parsing *)

local
  open Parser;

  infixr 9 >>++
  infixr 8 ++
  infixr 7 >>
  infixr 6 ||

  val isAlphaNum =
      let
        val alphaNumChars = explode "_'"
      in
        fn c => mem c alphaNumChars orelse Char.isAlphaNum c
      end;

  local
    val alphaNumToken = atLeastOne (some isAlphaNum) >> implode;

    val symbolToken =
        let
          fun isNeg c = str c = !negation
                        
          val symbolChars = explode "<>=-*+/\\?@|!$%&#^:;~"

          fun isSymbol c = mem c symbolChars

          fun isNonNegSymbol c = not (isNeg c) andalso isSymbol c
        in
          some isNeg >> str ||
          (some isNonNegSymbol ++ many (some isSymbol)) >> (implode o op::)
        end;

    val punctToken =
        let
          val punctChars = explode "()[]{}.,"

          fun isPunct c = mem c punctChars
        in
          some isPunct >> str
        end;

    val lexToken = alphaNumToken || symbolToken || punctToken;

    val space = many (some Char.isSpace);
  in
    val lexer = (space ++ lexToken ++ space) >> (fn (_,(tok,_)) => tok);
  end;

  fun termParser inputStream =
      let
        val quants = !binders
        and iOps = !infixes
        and neg = !negation
        and bracks = ("(",")") :: !brackets

        val bracks = map (fn (b1,b2) => (b1 ^ b2, b1, b2)) bracks

        val bTokens = map #2 bracks @ map #3 bracks

        fun possibleVarName "" = false
          | possibleVarName s = isAlphaNum (String.sub (s,0))

        fun vName bv s = NameSet.member s bv

        val iTokens = infixTokens iOps

        val iParser = parseInfixes iOps (fn (f,a,b) => Fn (f,[a,b]))

        val specialTokens = neg :: quants @ ["$"] @ bTokens @ iTokens

        fun varName bv =
            Parser.some (vName bv) ||
            (exact "$" ++ some possibleVarName) >> (fn (_,s) => s)

        fun fName bv s = not (mem s specialTokens) andalso not (vName bv s)

        fun functionName bv =
            Parser.some (fName bv) ||
            (exact "(" ++ any ++ exact ")") >> (fn (_,(s,_)) => s)

        fun basic bv tokens =
            let
              val var = varName bv >> Var

              val const = functionName bv >> (fn f => Fn (f,[]))

              fun bracket (ab,a,b) =
                  (exact a ++ term bv ++ exact b) >>
                  (fn (_,(tm,_)) => if ab = "()" then tm else Fn (ab,[tm]))

              fun quantifier q =
                  let
                    fun bind (v,t) = Fn (q, [Var v, t])
                  in
                    (exact q ++ atLeastOne (some possibleVarName) ++
                     exact ".") >>++
                    (fn (_,(vs,_)) =>
                        term (NameSet.addList bv vs) >>
                        (fn body => foldr bind body vs))
                  end
            in
              var ||
              const ||
              first (map bracket bracks) ||
              first (map quantifier quants)
            end tokens

        and molecule bv tokens =
            let
              val negations = many (exact neg) >> length

              val function =
                  (functionName bv ++ many (basic bv)) >> Fn || basic bv
            in
              (negations ++ function) >>
              (fn (n,tm) => funpow n (fn t => Fn (neg,[t])) tm)
            end tokens

        and term bv tokens = iParser (molecule bv) tokens
      in
        term NameSet.empty
      end inputStream;
in
  fun fromString input =
      let
        val chars = Stream.fromList (explode input)

        val tokens = everything (lexer >> singleton) chars

        val terms = everything (termParser >> singleton) tokens
      in
        case Stream.toList terms of
          [tm] => tm
        | _ => raise Error "Syntax.stringToTerm"
      end;
end;

local
  val antiquotedTermToString =
      Parser.toString (Parser.ppBracket "(" ")" pp);
in
  val parse = Parser.parseQuotation antiquotedTermToString fromString;
end;

end

structure TermOrdered =
struct type t = Term.term val compare = Term.compare end

structure TermSet = ElementSet (TermOrdered);

structure TermMap = KeyMap (TermOrdered);