IntToNat.fs

module RInGen.IntToNat
open SMTLIB2
open SMTLIB2.IdentGenerator
open RInGen.SubstituteOperations
open SMTLIB2.Operations
open Rule

type IntToNat () =
    inherit TheorySubstitutor ()
    let nat_sort_name = gensymp "Nat"
    let nat_sort = nat_sort_name |> ADTSort

    let Z_constr, _, _ as Z_entry = ADTExtensions.generateConstructorAndTesterOps "Z" [] nat_sort
    let S_constr, _, _ as S_entry = ADTExtensions.generateConstructorAndTesterOps "Z" ["unS", nat_sort] nat_sort
    let Z = Term.apply0 Z_constr
    let S = Term.apply1 S_constr

    let rec int_to_natrec (n : int64) = if n <= 0L then Z else S (int_to_natrec (n - 1L))

    let x = gensymp "x"
    let y = gensymp "y"
    let r = gensymp "r"
    let z = gensymp "z"
    let xid = TIdent(x, nat_sort)
    let yid = TIdent(y, nat_sort)
    let rid = TIdent(r, nat_sort)
    let zid = TIdent(z, nat_sort)

    let nat_datatype = command.DeclareDatatype(nat_sort_name, [Z_entry; S_entry])

    let add_app, add_def, add_op = Relativization.createBinaryOperation "add" nat_sort nat_sort nat_sort
    let minus_app, minus_def, minus_op = Relativization.createBinaryOperation "minus" nat_sort nat_sort nat_sort
    let mult_app, mult_def, mult_op = Relativization.createBinaryOperation "mult" nat_sort nat_sort nat_sort
    let div_app, div_def, div_op = Relativization.createBinaryOperation "div" nat_sort nat_sort nat_sort
    let mod_app, mod_def, mod_op = Relativization.createBinaryOperation "mod" nat_sort nat_sort nat_sort
    let le_app, le_def, le_op = Relativization.createBinaryRelation "le" nat_sort nat_sort
    let ge_app, ge_def, ge_op = Relativization.createBinaryRelation "ge" nat_sort nat_sort
    let lt_app, lt_def, lt_op = Relativization.createBinaryRelation "lt" nat_sort nat_sort
    let gt_app, gt_def, gt_op = Relativization.createBinaryRelation "gt" nat_sort nat_sort
    let add_decl =
        [
            clARule [] (add_app Z yid yid)
            clARule [add_app xid yid rid] (add_app (S xid) yid (S rid))
        ]
    let minus_decl =
        [
            clARule [] (minus_app Z yid Z)
            clARule [minus_app xid yid rid] (minus_app (S xid) yid (S rid))
        ]
    let le_decl =
        [
            clARule [] (le_app Z yid)
            clARule [le_app xid yid] (le_app (S xid) (S yid))
        ]
    let ge_decl =
        [
            clARule [] (ge_app yid Z)
            clARule [ge_app xid yid] (ge_app (S xid) (S yid))
        ]
    let lt_decl =
        [
            clARule [] (lt_app Z (S yid))
            clARule [lt_app xid yid] (lt_app (S xid) (S yid))
        ]
    let gt_decl =
        [
            clARule [] (gt_app (S yid) Z)
            clARule [gt_app xid yid] (gt_app (S xid) (S yid))
        ]
    let mult_decl =
        [
            clARule [] (mult_app Z yid Z)
            clARule [mult_app xid yid rid; add_app rid yid zid] (mult_app (S xid) yid zid)
        ]
    let div_decl =
        [
            clARule [lt_app xid yid] (div_app xid yid Z)
            clARule [ge_app xid yid; minus_app xid yid zid; div_app zid yid rid] (div_app xid yid (S rid))
        ]
    let mod_decl =
        [
            clARule [lt_app xid yid] (mod_app xid yid xid)
            clARule [ge_app xid yid; minus_app xid yid zid; mod_app zid yid rid] (mod_app xid yid rid)
        ]

    let substitutions =
        [
            "+", (add_op, true)
            "-", (minus_op, true)
            "*", (mult_op, true)
            "div", (div_op, true)
            "mod", (mod_op, true)
            "<=", (le_op, false)
            ">=", (ge_op, false)
            ">", (gt_op, false)
            "<", (lt_op, false)
        ] |> List.map (fun (name, op) -> Map.find name elementaryOperations, op) |> Map.ofList
    let preamble =
        List.map OriginalCommand [nat_datatype; add_def; minus_def; le_def; ge_def; lt_def; gt_def; mult_def; div_def; mod_def]
        @ List.map TransformedCommand (add_decl @ minus_decl @ le_decl @ ge_decl @ lt_decl @ gt_decl @ mult_decl @ div_decl @ mod_decl)

    let intConstToNat (s: symbol) =
        let r = ref 0L
        if System.Int64.TryParse(s.ToString(), r) then Some (int_to_natrec r.Value) else None

    override x.GenerateDeclarations() = preamble, nat_sort, substitutions, intConstToNat

    override x.TryMapSort(s) = if s = IntSort then Some nat_sort else None