path: root/src/trace/coqTerms.ml

(**************************************************************************)
(*                                                                        *)
(*     SMTCoq                                                             *)
(*     Copyright (C) 2011 - 2021                                          *)
(*                                                                        *)
(*     See file "AUTHORS" for the list of authors                         *)
(*                                                                        *)
(*   This file is distributed under the terms of the CeCILL-C licence     *)
(*                                                                        *)
(**************************************************************************)


open SmtMisc


type coqTerm = CoqInterface.constr lazy_t

let gc prefix constant =
  lazy (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref (prefix ^ "." ^ constant)))


(* Int63 *)
let int63_prefix = "num.int63"
let int63_gc = gc int63_prefix
let cint = int63_gc "type"
let ceq63 = int63_gc "eqb"

(* PArray *)
let array_prefix = "array.array"
let array_gc = gc array_prefix
let carray = array_gc "type"
let cmake = array_gc "make"
let cset = array_gc "set"

(* is_true *)
let cis_true = gc "core.is_true" "is_true"

(* nat *)
let nat_prefix = "num.nat"
let nat_gc = gc nat_prefix
let cnat = nat_gc "type"
let cO = nat_gc "O"
let cS = nat_gc "S"

(* Positive *)
let positive_prefix = "num.pos"
let positive_gc = gc positive_prefix
let cpositive = positive_gc "type"
let cxI = positive_gc "xI"
let cxO = positive_gc "xO"
let cxH = positive_gc "xH"
let ceqbP = positive_gc "eqb"

(* N *)
let n_prefix = "num.N"
let n_gc = gc n_prefix
let cN = n_gc "type"
let cN0 = n_gc "N0"
let cNpos = n_gc "Npos"
let cof_nat = n_gc "of_nat"

(* Z *)
let z_prefix = "num.Z"
let z_gc = gc z_prefix
let cZ = z_gc "type"
let cZ0 = z_gc "Z0"
let cZpos = z_gc "Zpos"
let cZneg = z_gc "Zneg"
let copp = z_gc "opp"
let cadd = z_gc "add"
let csub = z_gc "sub"
let cmul = z_gc "mul"
let cltb = z_gc "ltb"
let cleb = z_gc "leb"
let cgeb = z_gc "geb"
let cgtb = z_gc "gtb"
let ceqbZ = z_gc "eqb"

(* Booleans *)
let bool_prefix = "core.bool"
let bool_gc = gc bool_prefix
let cbool = bool_gc "type"
let ctrue = bool_gc "true"
let cfalse = bool_gc "false"
let candb = bool_gc "andb"
let corb = bool_gc "orb"
let cxorb = bool_gc "xorb"
let cnegb = bool_gc "negb"
let cimplb = bool_gc "implb"
let ceqb = bool_gc "eqb"
let cifb = bool_gc "ifb"
let creflect = bool_gc "reflect"

(* Lists *)
let list_prefix = "core.list"
let list_gc = gc list_prefix
let clist = list_gc "type"
let cnil = list_gc "nil"
let ccons = list_gc "cons"
let clength = list_gc "length"

(* Option *)
let option_prefix = "core.option"
let option_gc = gc option_prefix
let coption = option_gc "type"
let cSome = option_gc "Some"
let cNone = option_gc "None"

(* Pairs *)
let pair_prefix = "core.prod"
let pair_gc = gc pair_prefix
let cpair = pair_gc "intro"
let cprod = pair_gc "type"

(* Dependent pairs *)
let sigT_prefix = "core.sigT"
let sigT_gc = gc sigT_prefix
let csigT = sigT_gc "type"

(* Logical Operators *)
let cnot = gc "core.not" "type"
let cconj = gc "core.and" "conj"
let cand = gc "core.and" "type"
let ciff = gc "core.iff" "type"

(* Equality *)
let eq_prefix = "core.eq"
let eq_gc = gc eq_prefix
let ceq = eq_gc "type"
let crefl_equal = eq_gc "refl"

(* Micromega *)
let micromega_prefix = "micromega.ZMicromega"
let micromega_gc = gc micromega_prefix
let micromega_coq_proofTerm = micromega_gc "ZArithProof"

(* Bit vectors *)
let bv_prefix = "SMTCoq.bva.BVList.BITVECTOR_LIST"
let bv_gc = gc bv_prefix
let cbitvector = bv_gc "bitvector"
let cof_bits = bv_gc "of_bits"
let cbitOf = bv_gc "bitOf"
let cbv_eq = bv_gc "bv_eq"
let cbv_not = bv_gc "bv_not"
let cbv_neg = bv_gc "bv_neg"
let cbv_and = bv_gc "bv_and"
let cbv_or = bv_gc "bv_or"
let cbv_xor = bv_gc "bv_xor"
let cbv_add = bv_gc "bv_add"
let cbv_mult = bv_gc "bv_mult"
let cbv_ult = bv_gc "bv_ult"
let cbv_slt = bv_gc "bv_slt"
let cbv_concat = bv_gc "bv_concat"
let cbv_extr = bv_gc "bv_extr"
let cbv_zextn = bv_gc "bv_zextn"
let cbv_sextn = bv_gc "bv_sextn"
let cbv_shl = bv_gc "bv_shl"
let cbv_shr = bv_gc "bv_shr"

(* Arrays *)
let array_prefix = "SMTCoq.array.FArray"
let array_gc = gc array_prefix
let cfarray = array_gc "farray"
let cselect = array_gc "select"
let cstore = array_gc "store"
let cdiff = array_gc "diff"
let cequalarray = array_gc "equal"

(* SMTCoq terms *)
let state_prefix = "SMTCoq.State"
let state_gc = gc state_prefix
let cState_C_t = state_gc "C.t"
let cState_S_t = state_gc "S.t"

let misc_prefix = "SMTCoq.Misc"
let misc_gc = gc misc_prefix
let cdistinct = misc_gc "distinct"

let terms_prefix = "SMTCoq.SMT_terms"
let terms_gc = gc terms_prefix

let ctype = terms_gc "Typ.type"
let cTZ = terms_gc "Typ.TZ"
let cTbool = terms_gc "Typ.Tbool"
let cTpositive = terms_gc "Typ.Tpositive"
let cTBV = terms_gc "Typ.TBV"
let cTFArray = terms_gc "Typ.TFArray"
let cTindex = terms_gc "Typ.Tindex"

let cinterp_t = terms_gc "Typ.interp"
let cdec_interp = terms_gc "Typ.dec_interp"
let cord_interp = terms_gc "Typ.ord_interp"
let ccomp_interp = terms_gc "Typ.comp_interp"
let cinh_interp = terms_gc "Typ.inh_interp"

let cinterp_eqb = terms_gc "Typ.i_eqb"

let ctval =  terms_gc "Atom.tval"
let cTval =  terms_gc "Atom.Tval"

let cCO_xH = terms_gc "Atom.CO_xH"
let cCO_Z0 = terms_gc "Atom.CO_Z0"
let cCO_BV = terms_gc "Atom.CO_BV"

let cUO_xO = terms_gc "Atom.UO_xO"
let cUO_xI = terms_gc "Atom.UO_xI"
let cUO_Zpos = terms_gc "Atom.UO_Zpos"
let cUO_Zneg = terms_gc "Atom.UO_Zneg"
let cUO_Zopp = terms_gc "Atom.UO_Zopp"
let cUO_BVbitOf = terms_gc "Atom.UO_BVbitOf"
let cUO_BVnot = terms_gc "Atom.UO_BVnot"
let cUO_BVneg = terms_gc "Atom.UO_BVneg"
let cUO_BVextr = terms_gc "Atom.UO_BVextr"
let cUO_BVzextn = terms_gc "Atom.UO_BVzextn"
let cUO_BVsextn = terms_gc "Atom.UO_BVsextn"

let cBO_Zplus = terms_gc "Atom.BO_Zplus"
let cBO_Zminus = terms_gc "Atom.BO_Zminus"
let cBO_Zmult = terms_gc "Atom.BO_Zmult"
let cBO_Zlt = terms_gc "Atom.BO_Zlt"
let cBO_Zle = terms_gc "Atom.BO_Zle"
let cBO_Zge = terms_gc "Atom.BO_Zge"
let cBO_Zgt = terms_gc "Atom.BO_Zgt"
let cBO_eq = terms_gc "Atom.BO_eq"
let cBO_BVand = terms_gc "Atom.BO_BVand"
let cBO_BVor = terms_gc "Atom.BO_BVor"
let cBO_BVxor = terms_gc "Atom.BO_BVxor"
let cBO_BVadd = terms_gc "Atom.BO_BVadd"
let cBO_BVmult = terms_gc "Atom.BO_BVmult"
let cBO_BVult = terms_gc "Atom.BO_BVult"
let cBO_BVslt = terms_gc "Atom.BO_BVslt"
let cBO_BVconcat = terms_gc "Atom.BO_BVconcat"
let cBO_BVshl = terms_gc "Atom.BO_BVshl"
let cBO_BVshr = terms_gc "Atom.BO_BVshr"
let cBO_select = terms_gc "Atom.BO_select"
let cBO_diffarray = terms_gc "Atom.BO_diffarray"

let cTO_store = terms_gc "Atom.TO_store"

let cNO_distinct = terms_gc "Atom.NO_distinct"

let catom = terms_gc "Atom.atom"
let cAcop = terms_gc "Atom.Acop"
let cAuop = terms_gc "Atom.Auop"
let cAbop = terms_gc "Atom.Abop"
let cAtop = terms_gc "Atom.Atop"
let cAnop = terms_gc "Atom.Anop"
let cAapp = terms_gc "Atom.Aapp"

let cform  = terms_gc "Form.form"
let cFatom = terms_gc "Form.Fatom"
let cFtrue = terms_gc "Form.Ftrue"
let cFfalse = terms_gc "Form.Ffalse"
let cFnot2 = terms_gc "Form.Fnot2"
let cFand = terms_gc "Form.Fand"
let cFor = terms_gc "Form.For"
let cFxor = terms_gc "Form.Fxor"
let cFimp = terms_gc "Form.Fimp"
let cFiff = terms_gc "Form.Fiff"
let cFite = terms_gc "Form.Fite"
let cFbbT = terms_gc "Form.FbbT"

(* SMTCoq Classes *)
let classes_prefix = "SMTCoq.classes.SMT_classes"
let classes_gc = gc classes_prefix
let ctyp_compdec = classes_gc "typ_compdec"
let cTyp_compdec = classes_gc "Typ_compdec"
let cte_carrier = classes_gc "te_carrier"
let cte_compdec = classes_gc "te_compdec"
let ceqb_of_compdec = classes_gc "eqb_of_compdec"
let cCompDec = classes_gc "CompDec"

let classesi_prefix = "SMTCoq.classes.SMT_classes_instances"
let classesi_gc = gc classesi_prefix
let cunit_typ_compdec = classesi_gc "unit_typ_compdec"
let cbool_compdec = classesi_gc "bool_compdec"
let cZ_compdec = classesi_gc "Z_compdec"
let cPositive_compdec = classesi_gc "Positive_compdec"
let cBV_compdec = classesi_gc "BV_compdec"
let cFArray_compdec = classesi_gc "FArray_compdec"

(* SMTCoq Trace *)
let sat_checker_prefix = "SMTCoq.Trace.Sat_Checker"
let sat_checker_gc = gc sat_checker_prefix
let csat_checker_valid = sat_checker_gc "valid"
let csat_checker_interp_var = sat_checker_gc "interp_var"
let csat_checker_Certif = sat_checker_gc "Certif"
let csat_checker_dimacs = sat_checker_gc "dimacs"
let csat_checker_certif = sat_checker_gc "certif"
let csat_checker_theorem_checker = sat_checker_gc "theorem_checker"
let csat_checker_checker = sat_checker_gc "checker"

let cnf_checker_prefix = "SMTCoq.Trace.Cnf_Checker"
let cnf_checker_gc = gc cnf_checker_prefix
let ccnf_checker_certif = cnf_checker_gc "certif"
let ccnf_checker_Certif = cnf_checker_gc "Certif"
let ccnf_checker_checker_b_correct = cnf_checker_gc "checker_b_correct"
let ccnf_checker_checker_b = cnf_checker_gc "checker_b"
let ccnf_checker_checker_eq_correct = cnf_checker_gc "checker_eq_correct"
let ccnf_checker_checker_eq = cnf_checker_gc "checker_eq"

let euf_checker_prefix = "SMTCoq.Trace.Euf_Checker"
let euf_checker_gc = gc euf_checker_prefix
let ceuf_checker_Certif = euf_checker_gc "Certif"
let ceuf_checker_certif = euf_checker_gc "certif"
let ceuf_checker_checker = euf_checker_gc "checker"
let ceuf_checker_checker_correct = euf_checker_gc "checker_correct"
let ceuf_checker_checker_b_correct = euf_checker_gc "checker_b_correct"
let ceuf_checker_checker_b = euf_checker_gc "checker_b"
let ceuf_checker_checker_eq_correct = euf_checker_gc "checker_eq_correct"
let ceuf_checker_checker_eq = euf_checker_gc "checker_eq"
let ceuf_checker_checker_debug = euf_checker_gc "checker_debug"
let ceuf_checker_name_step = euf_checker_gc "name_step"
let ceuf_checker_Name_Res = euf_checker_gc "Name_Res"
let ceuf_checker_Name_Weaken = euf_checker_gc "Name_Weaken"
let ceuf_checker_Name_ImmFlatten = euf_checker_gc "Name_ImmFlatten"
let ceuf_checker_Name_CTrue = euf_checker_gc "Name_CTrue"
let ceuf_checker_Name_CFalse = euf_checker_gc "Name_CFalse"
let ceuf_checker_Name_BuildDef = euf_checker_gc "Name_BuildDef"
let ceuf_checker_Name_BuildDef2 = euf_checker_gc "Name_BuildDef2"
let ceuf_checker_Name_BuildProj = euf_checker_gc "Name_BuildProj"
let ceuf_checker_Name_ImmBuildDef = euf_checker_gc "Name_ImmBuildDef"
let ceuf_checker_Name_ImmBuildDef2 = euf_checker_gc "Name_ImmBuildDef2"
let ceuf_checker_Name_ImmBuildProj = euf_checker_gc "Name_ImmBuildProj"
let ceuf_checker_Name_EqTr = euf_checker_gc "Name_EqTr"
let ceuf_checker_Name_EqCgr = euf_checker_gc "Name_EqCgr"
let ceuf_checker_Name_EqCgrP = euf_checker_gc "Name_EqCgrP"
let ceuf_checker_Name_LiaMicromega = euf_checker_gc "Name_LiaMicromega"
let ceuf_checker_Name_LiaDiseq = euf_checker_gc "Name_LiaDiseq"
let ceuf_checker_Name_SplArith = euf_checker_gc "Name_SplArith"
let ceuf_checker_Name_SplDistinctElim = euf_checker_gc "Name_SplDistinctElim"
let ceuf_checker_Name_BBVar = euf_checker_gc "Name_BBVar"
let ceuf_checker_Name_BBConst = euf_checker_gc "Name_BBConst"
let ceuf_checker_Name_BBOp = euf_checker_gc "Name_BBOp"
let ceuf_checker_Name_BBNot = euf_checker_gc "Name_BBNot"
let ceuf_checker_Name_BBNeg = euf_checker_gc "Name_BBNeg"
let ceuf_checker_Name_BBAdd = euf_checker_gc "Name_BBAdd"
let ceuf_checker_Name_BBConcat = euf_checker_gc "Name_BBConcat"
let ceuf_checker_Name_BBMul = euf_checker_gc "Name_BBMul"
let ceuf_checker_Name_BBUlt = euf_checker_gc "Name_BBUlt"
let ceuf_checker_Name_BBSlt = euf_checker_gc "Name_BBSlt"
let ceuf_checker_Name_BBEq = euf_checker_gc "Name_BBEq"
let ceuf_checker_Name_BBDiseq = euf_checker_gc "Name_BBDiseq"
let ceuf_checker_Name_BBExtract = euf_checker_gc "Name_BBExtract"
let ceuf_checker_Name_BBZextend = euf_checker_gc "Name_BBZextend"
let ceuf_checker_Name_BBSextend = euf_checker_gc "Name_BBSextend"
let ceuf_checker_Name_BBShl = euf_checker_gc "Name_BBShl"
let ceuf_checker_Name_BBShr = euf_checker_gc "Name_BBShr"
let ceuf_checker_Name_RowEq = euf_checker_gc "Name_RowEq"
let ceuf_checker_Name_RowNeq = euf_checker_gc "Name_RowNeq"
let ceuf_checker_Name_Ext = euf_checker_gc "Name_Ext"
let ceuf_checker_Name_Hole = euf_checker_gc "Name_Hole"

type certif_ops =
  coqTerm * coqTerm * coqTerm *
  coqTerm * coqTerm * coqTerm *
  coqTerm * coqTerm * coqTerm *
  coqTerm * coqTerm * coqTerm *
  coqTerm * coqTerm * coqTerm *
  coqTerm * coqTerm * coqTerm *
  coqTerm * coqTerm * coqTerm *
  coqTerm * coqTerm * coqTerm *
  coqTerm * coqTerm * coqTerm *
  coqTerm * coqTerm * coqTerm *
  coqTerm * coqTerm * coqTerm *
  coqTerm * coqTerm * coqTerm *
  coqTerm * coqTerm * coqTerm *
  coqTerm * coqTerm
let make_certif_ops prefix args =
  let gc = gc prefix in
  let gen_constant c =
    match args with
      | Some args -> lazy (mklApp (gc c) args)
      | None -> gc c in
 (gen_constant "step",
  gen_constant "Res", gen_constant "Weaken", gen_constant "ImmFlatten",
  gen_constant "CTrue", gen_constant "CFalse",
  gen_constant "BuildDef", gen_constant "BuildDef2",
  gen_constant "BuildProj",
  gen_constant "ImmBuildProj", gen_constant "ImmBuildDef",
  gen_constant"ImmBuildDef2",
  gen_constant "EqTr", gen_constant "EqCgr", gen_constant "EqCgrP",
  gen_constant "LiaMicromega", gen_constant "LiaDiseq",
  gen_constant "SplArith", gen_constant "SplDistinctElim",
  gen_constant "BBVar", gen_constant "BBConst",
  gen_constant "BBOp", gen_constant "BBNot", gen_constant "BBEq",
  gen_constant "BBDiseq",
  gen_constant "BBNeg", gen_constant "BBAdd", gen_constant "BBMul",
  gen_constant "BBUlt", gen_constant "BBSlt", gen_constant "BBConcat",
  gen_constant "BBExtract", gen_constant "BBZextend", gen_constant "BBSextend",
  gen_constant "BBShl", gen_constant "BBShr",
  gen_constant "RowEq", gen_constant "RowNeq", gen_constant "Ext",
  gen_constant "Hole", gen_constant "ForallInst")
let csat_checker_certif_ops = make_certif_ops sat_checker_prefix None
let ccnf_checker_certif_ops = make_certif_ops cnf_checker_prefix None
let ceuf_checker_certif_ops = make_certif_ops euf_checker_prefix


(** Useful constructions *)

let ceq_refl_true =
  lazy (mklApp crefl_equal [|Lazy.force cbool;Lazy.force ctrue|])

let eq_refl_true () = Lazy.force ceq_refl_true

let vm_cast_true_no_check t =
  CoqInterface.mkCast(eq_refl_true (),
              CoqInterface.vmcast,
              mklApp ceq [|Lazy.force cbool; t; Lazy.force ctrue|])

(* This version checks convertibility right away instead of delaying it at
   Qed. This allows to report issues to the user as soon as he/she runs one of
   SMTCoq's tactics. *)
let vm_cast_true env t =
  try
    CoqInterface.vm_conv Reduction.CUMUL env
      (mklApp ceq
         [|Lazy.force cbool; Lazy.force ctrue; Lazy.force ctrue|])
      (mklApp ceq [|Lazy.force cbool; t; Lazy.force ctrue|]);
    vm_cast_true_no_check t
  with Reduction.NotConvertible ->
    CoqInterface.error ("SMTCoq was not able to check the proof certificate.")


(* Compute a nat *)
let rec mkNat = function
  | 0 -> Lazy.force cO
  | i -> mklApp cS [|mkNat (i-1)|]

(* Compute a positive *)
let rec mkPositive = function
  | 1 -> Lazy.force cxH
  | i ->
     let c = if (i mod 2) = 0 then cxO else cxI in
     mklApp c [|mkPositive (i / 2)|]

(* Compute a N *)
let mkN = function
  | 0 -> Lazy.force cN0
  | i -> mklApp cNpos [|mkPositive i|]

(* Compute a Boolean *)
let mkBool = function
  | true -> Lazy.force ctrue
  | false -> Lazy.force cfalse

(* Compute a Boolean list *)
let rec mk_bv_list = function
  | [] -> mklApp cnil [|Lazy.force cbool|]
  | b :: bv ->
    mklApp ccons [|Lazy.force cbool; mkBool b; mk_bv_list bv|]

(* Compute an array *)
let mkArray : Constr.types * Constr.t array -> Constr.t =
  fun (ty, a) ->
  let l = (Array.length a) - 1 in
  snd (Array.fold_left (fun (i,acc) c ->
                        let acc' =
                          if i = l then
                            acc
                          else
                            mklApp cset [|ty; acc; mkInt i; c|] in
                        (i+1,acc')
                       ) (0, mklApp cmake [|ty; mkInt l; a.(l)|]) a)


(* Reification *)
let mk_bool b =
  let c, args = CoqInterface.decompose_app b in
  if CoqInterface.eq_constr c (Lazy.force ctrue) then true
  else if CoqInterface.eq_constr c (Lazy.force cfalse) then false
  else assert false

let rec mk_bool_list bs =
  let c, args = CoqInterface.decompose_app bs in
  if CoqInterface.eq_constr c (Lazy.force cnil) then []
  else if CoqInterface.eq_constr c (Lazy.force ccons) then
    match args with
    | [_; b; bs] -> mk_bool b :: mk_bool_list bs
    | _ -> assert false
  else assert false

let rec mk_nat n =
  let c, args = CoqInterface.decompose_app n in
  if CoqInterface.eq_constr c (Lazy.force cO) then
    0
  else if CoqInterface.eq_constr c (Lazy.force cS) then
    match args with
    | [n] -> (mk_nat n) + 1
    | _ -> assert false
  else assert false

let rec mk_positive n =
  let c, args = CoqInterface.decompose_app n in
  if CoqInterface.eq_constr c (Lazy.force cxH) then
    1
  else if CoqInterface.eq_constr c (Lazy.force cxO) then
    match args with
    | [n] -> 2 * (mk_positive n)
    | _ -> assert false
  else if CoqInterface.eq_constr c (Lazy.force cxI) then
    match args with
    | [n] -> 2 * (mk_positive n) + 1
    | _ -> assert false
  else assert false


let mk_N n =
  let c, args = CoqInterface.decompose_app n in
  if CoqInterface.eq_constr c (Lazy.force cN0) then
    0
  else if CoqInterface.eq_constr c (Lazy.force cNpos) then
    match args with
    | [n] -> mk_positive n
    | _ -> assert false
  else assert false


let mk_Z n =
  let c, args = CoqInterface.decompose_app n in
  if CoqInterface.eq_constr c (Lazy.force cZ0) then 0
  else if CoqInterface.eq_constr c (Lazy.force cZpos) then
    match args with
    | [n] -> mk_positive n
    | _ -> assert false
  else if CoqInterface.eq_constr c (Lazy.force cZneg) then
    match args with
    | [n] -> - mk_positive n
    | _ -> assert false
  else assert false


(* size of bivectors are either N.of_nat (length l) or an N *)
let mk_bvsize n =
  let c, args = CoqInterface.decompose_app n in
  if CoqInterface.eq_constr c (Lazy.force cof_nat) then
    match args with
    | [nl] ->
      let c, args = CoqInterface.decompose_app nl in
      if CoqInterface.eq_constr c (Lazy.force clength) then
        match args with
        | [_; l] -> List.length (mk_bool_list l)
        | _ -> assert false
      else assert false
    | _ -> assert false
  else mk_N n

(** Switches between constr and OCaml *)
(* Transform a option constr into a constr option *)
let option_of_constr_option co =
  let c, args = CoqInterface.decompose_app co in
  if c = Lazy.force cSome then
    match args with
      | [_;c] -> Some c
      | _ -> assert false
  else
    None

(* Transform a tuple of constr into a (reversed) list of constr *)
let list_of_constr_tuple =
  let rec list_of_constr_tuple acc t =
    let c, args = CoqInterface.decompose_app t in
    if c = Lazy.force cpair then
      match args with
        | [_;_;t1;t2] ->
           let acc' = list_of_constr_tuple acc t1 in
           list_of_constr_tuple acc' t2
        | _ -> assert false
    else
      t::acc
  in
  list_of_constr_tuple []