From 7072c4591668d2c21211a744d3719f6b42d1e7b9 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Tue, 13 Jan 2015 17:11:29 +0100 Subject: Identify ML functions that depend on native-coq --- src/Make.native | 88 -------- src/Makefile.native | 416 ------------------------------------- src/configure.sh | 4 +- src/trace/coqTerms.ml | 10 +- src/trace/satAtom.ml | 2 +- src/trace/smtAtom.ml | 6 +- src/trace/smtForm.ml | 4 +- src/trace/smtMisc.ml | 2 +- src/trace/smtTrace.ml | 16 +- src/verit/verit.ml | 12 +- src/versions/native/Make | 91 ++++++++ src/versions/native/Makefile | 424 ++++++++++++++++++++++++++++++++++++++ src/versions/native/structures.ml | 26 +++ src/zchaff/zchaff.ml | 8 +- 14 files changed, 571 insertions(+), 538 deletions(-) delete mode 100644 src/Make.native delete mode 100644 src/Makefile.native create mode 100644 src/versions/native/Make create mode 100644 src/versions/native/Makefile create mode 100644 src/versions/native/structures.ml diff --git a/src/Make.native b/src/Make.native deleted file mode 100644 index 34e6dc2..0000000 --- a/src/Make.native +++ /dev/null @@ -1,88 +0,0 @@ -######################################################################## -## This file is intended to developers, please do not use it to ## -## generate a Makefile, rather use the provided Makefile. ## -######################################################################## - - - - -######################################################################## -## To generate the Makefile: ## -## coq_makefile -f Make -o Makefile ## -## Change the "all" target into: ## -## all: ml $(CMXFILES) $(CMXA) $(CMXS) $(VOFILES) ## -## Change the "install-natdynlink" target: change CMXSFILES into CMXS and add the same thing for CMXA and VCMXS. ## -## Change the "install" target: change CMO into CMX. ## -## Finally, suppress the "Makefile" target and add to the "clean" target: ## -## - rm -f NSMTCoq* cnf/NSMTCoq* euf/NSMTCoq* lia/NSMTCoq* spl/NSMTCoq* ../unit-tests/NSMTCoq* ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml verit/smtlib2_parse.mli verit/smtlib2_parse.ml verit/smtlib2_lex.ml ## -######################################################################## - - --R . SMTCoq - --I cnf --I euf --I lia --I trace --I verit --I zchaff - --custom "cd ../unit-tests; make" "" "test" - --custom "$(CAMLLEX) $<" "%.mll" "%.ml" --custom "$(CAMLYACC) $<" "%.mly" "%.ml %.mli" --custom "" "verit/veritParser.ml verit/veritLexer.ml verit/smtlib2_parse.ml verit/smtlib2_lex.ml" "ml" - --custom "$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^" "trace/smtMisc.cmx trace/coqTerms.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx verit/smtlib2_util.cmx verit/smtlib2_ast.cmx verit/smtlib2_parse.cmx verit/smtlib2_lex.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx verit/smtlib2_genConstr.cmx verit/verit.cmx trace/smt_tactic.cmx" "$(CMXA)" --custom "$(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^" "$(CMXA)" "$(CMXS)" - -CMXA = trace/smtcoq.cmxa -CMXS = trace/smt_tactic.cmxs -VCMXS = "NSMTCoq_State.cmxs NSMTCoq_Misc.cmxs NSMTCoq_SMT_terms.cmxs cnf/NSMTCoq_cnf_Cnf.cmxs euf/NSMTCoq_euf_Euf.cmxs lia/NSMTCoq_lia_Lia.cmxs spl/NSMTCoq_spl_Syntactic.cmxs spl/NSMTCoq_spl_Arithmetic.cmxs spl/NSMTCoq_spl_Operators.cmxs NSMTCoq_Trace.cmxs NSMTCoq_SMTCoq.cmxs NSMTCoq_State.cmi NSMTCoq_Misc.cmi NSMTCoq_SMT_terms.cmi cnf/NSMTCoq_cnf_Cnf.cmi euf/NSMTCoq_euf_Euf.cmi lia/NSMTCoq_lia_Lia.cmi spl/NSMTCoq_spl_Syntactic.cmxs spl/NSMTCoq_spl_Arithmetic.cmi spl/NSMTCoq_spl_Operators.cmi NSMTCoq_Trace.cmi NSMTCoq_Trace.cmi NSMTCoq_SMTCoq.cmi" -CAMLLEX = $(CAMLBIN)ocamllex -CAMLYACC = $(CAMLBIN)ocamlyacc - -trace/coqTerms.ml -trace/satAtom.ml -trace/smtAtom.ml -trace/smtAtom.mli -trace/smtCertif.ml -trace/smtCnf.ml -trace/smtForm.ml -trace/smtForm.mli -trace/smtMisc.ml -trace/smt_tactic.ml4 -trace/smtTrace.ml - -verit/smtlib2_ast.ml -verit/smtlib2_genConstr.ml -verit/smtlib2_lex.ml -verit/smtlib2_parse.ml -verit/smtlib2_util.ml -verit/veritParser.ml -verit/veritLexer.ml -verit/verit.ml -verit/veritSyntax.ml -verit/veritSyntax.mli - -zchaff/cnfParser.ml -zchaff/satParser.ml -zchaff/zchaff.ml -zchaff/zchaffParser.ml - -cnf/Cnf.v - -euf/Euf.v - -lia/lia.ml -lia/Lia.v - -spl/Syntactic.v -spl/Arithmetic.v -spl/Operators.v - -Misc.v -SMTCoq.v -SMT_terms.v -State.v -Trace.v diff --git a/src/Makefile.native b/src/Makefile.native deleted file mode 100644 index 2ec982f..0000000 --- a/src/Makefile.native +++ /dev/null @@ -1,416 +0,0 @@ -############################################################################# -## v # The Coq Proof Assistant ## -## "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) - -%.cmo: %.ml4 - $(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $< - -%.cmx: %.ml4 - $(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $< - -%.ml4.d: %.ml4 - $(OCAMLDEP) -slash $(OCAMLLIBS) $(PP) -impl "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) - -%.cmo: %.ml - $(CAMLC) $(ZDEBUG) $(ZFLAGS) $< - -%.cmx: %.ml - $(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $< - -%.ml.d: %.ml - $(OCAMLDEP) -slash $(OCAMLLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) - -%.cmxs: %.cmx - $(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $< - -%.vo %.glob: %.v - $(COQC) $(COQDEBUG) $(COQFLAGS) $* - -%.vi: %.v - $(COQC) -i $(COQDEBUG) $(COQFLAGS) $* - -%.g: %.v - $(GALLINA) $< - -%.tex: %.v - $(COQDOC) $(COQDOCFLAGS) -latex $< -o $@ - -%.html: %.v %.glob - $(COQDOC) $(COQDOCFLAGS) -html $< -o $@ - -%.g.tex: %.v - $(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@ - -%.g.html: %.v %.glob - $(COQDOC)$(COQDOCFLAGS) -html -g $< -o $@ - -%.v.d: %.v - $(COQDEP) -slash $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) - -%.v.beautified: - $(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $* - -# WARNING -# -# This Makefile has been automagically generated -# Edit at your own risks ! -# -# END OF WARNING - diff --git a/src/configure.sh b/src/configure.sh index 04da739..d889828 100755 --- a/src/configure.sh +++ b/src/configure.sh @@ -3,7 +3,7 @@ set -e if [ $@ -a $@ = -standard ]; then - cp Makefile.standard Makefile + cp versions/standard/Makefile Makefile else - cp Makefile.native Makefile + cp versions/native/Makefile Makefile fi diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml index 1ee6448..8046a47 100644 --- a/src/trace/coqTerms.ml +++ b/src/trace/coqTerms.ml @@ -18,15 +18,11 @@ open Coqlib let gen_constant modules constant = lazy (gen_constant_in_modules "SMT" modules constant) (* Int63 *) -let int63_modules = [["Coq";"Numbers";"Cyclic";"Int63";"Int63Native"]] - -let cint = gen_constant int63_modules "int" -let ceq63 = gen_constant int63_modules "eqb" +let cint = gen_constant Structures.int63_modules "int" +let ceq63 = gen_constant Structures.int63_modules "eqb" (* PArray *) -let parray_modules = [["Coq";"Array";"PArray"]] - -let carray = gen_constant parray_modules "array" +let carray = gen_constant Structures.parray_modules "array" (* Positive *) let positive_modules = [["Coq";"Numbers";"BinNums"]; diff --git a/src/trace/satAtom.ml b/src/trace/satAtom.ml index ca72504..f381407 100644 --- a/src/trace/satAtom.ml +++ b/src/trace/satAtom.ml @@ -53,7 +53,7 @@ module Atom = t let interp_tbl reify = - Term.mkArray (Lazy.force cbool, atom_tbl reify) + Structures.mkArray (Lazy.force cbool, atom_tbl reify) end diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml index 3164692..392ef2e 100644 --- a/src/trace/smtAtom.ml +++ b/src/trace/smtAtom.ml @@ -100,7 +100,7 @@ module Btype = | Tindex it -> t.(it.index) <- it.hval | _ -> () in Hashtbl.iter set reify.tbl; - Term.mkArray (Lazy.force ctyp_eqb, t) + Structures.mkArray (Lazy.force ctyp_eqb, t) let to_list reify = let set _ t acc = match t with @@ -291,7 +291,7 @@ module Op = let set _ v = t.(v.index) <- mk_Tval v.hval.tparams v.hval.tres v.hval.op_val in Hashtbl.iter set reify.tbl; - Term.mkArray (tval, t) + Structures.mkArray (tval, t) let to_list reify = let set _ op acc = @@ -651,7 +651,7 @@ module Atom = let interp_tbl reify = let t = to_array reify (Lazy.force dft_atom) a_to_coq in - Term.mkArray (Lazy.force catom, t) + Structures.mkArray (Lazy.force catom, t) (** Producing a Coq term corresponding to the interpretation of an atom *) diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml index 6075b3f..c7856f3 100644 --- a/src/trace/smtForm.ml +++ b/src/trace/smtForm.ml @@ -413,7 +413,7 @@ module Make (Atom:ATOM) = let args_to_coq args = let cargs = Array.make (Array.length args + 1) (mkInt 0) in Array.iteri (fun i hf -> cargs.(i) <- to_coq hf) args; - Term.mkArray (Lazy.force cint, cargs) + Structures.mkArray (Lazy.force cint, cargs) let pf_to_coq = function | Fatom a -> mklApp cFatom [|mkInt (Atom.index a)|] @@ -449,7 +449,7 @@ module Make (Atom:ATOM) = let interp_tbl reify = let (i,t) = to_array reify (Lazy.force cFtrue) pf_to_coq in - (mkInt i, Term.mkArray (Lazy.force cform, t)) + (mkInt i, Structures.mkArray (Lazy.force cform, t)) let nvars reify = reify.count (** Producing a Coq term corresponding to the interpretation of a formula *) diff --git a/src/trace/smtMisc.ml b/src/trace/smtMisc.ml index 02e5f26..849c0d7 100644 --- a/src/trace/smtMisc.ml +++ b/src/trace/smtMisc.ml @@ -20,7 +20,7 @@ let cInt_tbl = Hashtbl.create 17 let mkInt i = try Hashtbl.find cInt_tbl i with Not_found -> - let ci = Term.mkInt (Uint63.of_int i) in + let ci = Structures.mkInt i in Hashtbl.add cInt_tbl i ci; ci diff --git a/src/trace/smtTrace.ml b/src/trace/smtTrace.ml index 8420ca1..b96807f 100644 --- a/src/trace/smtTrace.ml +++ b/src/trace/smtTrace.ml @@ -295,7 +295,7 @@ let to_coq to_lit (cstep, l := tl | _ -> assert false done; - mklApp cRes [|mkInt (get_pos c); Term.mkArray (Lazy.force cint, args)|] + mklApp cRes [|mkInt (get_pos c); Structures.mkArray (Lazy.force cint, args)|] | Other other -> begin match other with | ImmFlatten (c',f) -> mklApp cImmFlatten [|out_c c;out_c c'; out_f f|] @@ -330,25 +330,25 @@ let to_coq to_lit (cstep, | _ -> assert false in let step = Lazy.force cstep in let def_step = - mklApp cRes [|mkInt 0; Term.mkArray (Lazy.force cint, [|mkInt 0|]) |] in + mklApp cRes [|mkInt 0; Structures.mkArray (Lazy.force cint, [|mkInt 0|]) |] in let r = ref confl in let nc = ref 0 in while not (isRoot !r.kind) do r := prev !r; incr nc done; let last_root = !r in let size = !nc in - let max = (Parray.trunc_size (Uint63.of_int 4194303)) - 1 in + let max = Structures.max_array_size - 1 in let q,r1 = size / max, size mod max in let trace = let len = if r1 = 0 then q + 1 else q + 2 in - Array.make len (Term.mkArray (step, [|def_step|])) in + Array.make len (Structures.mkArray (step, [|def_step|])) in for j = 0 to q - 1 do - let tracej = Array.make (Parray.trunc_size (Uint63.of_int 4194303)) def_step in + let tracej = Array.make Structures.max_array_size def_step in for i = 0 to max - 1 do r := next !r; tracej.(i) <- step_to_coq !r; done; - trace.(j) <- Term.mkArray (step, tracej) + trace.(j) <- Structures.mkArray (step, tracej) done; if r1 <> 0 then begin let traceq = Array.make (r1 + 1) def_step in @@ -356,10 +356,10 @@ let to_coq to_lit (cstep, r := next !r; traceq.(i) <- step_to_coq !r; done; - trace.(q) <- Term.mkArray (step, traceq) + trace.(q) <- Structures.mkArray (step, traceq) end; - (Term.mkArray (mklApp carray [|step|], trace), last_root) + (Structures.mkArray (mklApp carray [|step|], trace), last_root) diff --git a/src/verit/verit.ml b/src/verit/verit.ml index 87e74a6..0ae0bc9 100644 --- a/src/verit/verit.ml +++ b/src/verit/verit.ml @@ -157,13 +157,13 @@ let parse_certif t_i t_func t_atom t_form root used_root trace fsmt fproof = let res = Array.make (List.length roots + 1) (mkInt 0) in let i = ref 0 in List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots; - Term.mkArray (Lazy.force cint, res) in + Structures.mkArray (Lazy.force cint, res) in let used_roots = let l = List.length used_roots in let res = Array.make (l + 1) (mkInt 0) in let i = ref (l-1) in List.iter (fun j -> res.(!i) <- mkInt j; decr i) used_roots; - mklApp cSome [|mklApp carray [|Lazy.force cint|]; Term.mkArray (Lazy.force cint, res)|] in + mklApp cSome [|mklApp carray [|Lazy.force cint|]; Structures.mkArray (Lazy.force cint, res)|] in let ce3 = { const_entry_body = roots; const_entry_type = None; @@ -238,12 +238,12 @@ let theorem name fsmt fproof = let res = Array.make (l + 1) (mkInt 0) in let i = ref (l-1) in List.iter (fun j -> res.(!i) <- mkInt j; decr i) used_roots; - mklApp cSome [|mklApp carray [|Lazy.force cint|]; Term.mkArray (Lazy.force cint, res)|] in + mklApp cSome [|mklApp carray [|Lazy.force cint|]; Structures.mkArray (Lazy.force cint, res)|] in let rootsCstr = let res = Array.make (List.length roots + 1) (mkInt 0) in let i = ref 0 in List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots; - Term.mkArray (Lazy.force cint, res) in + Structures.mkArray (Lazy.force cint, res) in let t_atom = Atom.interp_tbl ra in let t_form = snd (Form.interp_tbl rf) in @@ -298,13 +298,13 @@ let checker fsmt fproof = let res = Array.make (l + 1) (mkInt 0) in let i = ref (l-1) in List.iter (fun j -> res.(!i) <- mkInt j; decr i) used_roots; - mklApp cSome [|mklApp carray [|Lazy.force cint|]; Term.mkArray (Lazy.force cint, res)|] in + mklApp cSome [|mklApp carray [|Lazy.force cint|]; Structures.mkArray (Lazy.force cint, res)|] in let t9 = Unix.time () in (* for debug *) let rootsCstr = let res = Array.make (List.length roots + 1) (mkInt 0) in let i = ref 0 in List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots; - Term.mkArray (Lazy.force cint, res) in + Structures.mkArray (Lazy.force cint, res) in let t10 = Unix.time () in (* for debug *) let t_i = make_t_i rt in diff --git a/src/versions/native/Make b/src/versions/native/Make new file mode 100644 index 0000000..5695872 --- /dev/null +++ b/src/versions/native/Make @@ -0,0 +1,91 @@ +######################################################################## +## This file is intended to developers, please do not use it to ## +## generate a Makefile, rather use the provided Makefile. ## +######################################################################## + + + + +######################################################################## +## To generate the Makefile: ## +## coq_makefile -f Make -o Makefile ## +## Change the "all" target into: ## +## all: ml $(CMXFILES) $(CMXA) $(CMXS) $(VOFILES) ## +## Change the "install-natdynlink" target: change CMXSFILES into CMXS and add the same thing for CMXA and VCMXS. ## +## Change the "install" target: change CMO into CMX. ## +## Finally, suppress the "Makefile" target and add to the "clean" target: ## +## - rm -f NSMTCoq* cnf/NSMTCoq* euf/NSMTCoq* lia/NSMTCoq* spl/NSMTCoq* ../unit-tests/NSMTCoq* ../unit-tests/*.vo ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml verit/smtlib2_parse.mli verit/smtlib2_parse.ml verit/smtlib2_lex.ml ## +######################################################################## + + +-R . SMTCoq + +-I cnf +-I euf +-I lia +-I trace +-I verit +-I zchaff +-I versions/native + +-custom "cd ../unit-tests; make" "" "test" + +-custom "$(CAMLLEX) $<" "%.mll" "%.ml" +-custom "$(CAMLYACC) $<" "%.mly" "%.ml %.mli" +-custom "" "verit/veritParser.ml verit/veritLexer.ml verit/smtlib2_parse.ml verit/smtlib2_lex.ml" "ml" + +-custom "$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^" "versions/native/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx verit/smtlib2_util.cmx verit/smtlib2_ast.cmx verit/smtlib2_parse.cmx verit/smtlib2_lex.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx verit/smtlib2_genConstr.cmx verit/verit.cmx trace/smt_tactic.cmx" "$(CMXA)" +-custom "$(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^" "$(CMXA)" "$(CMXS)" + +CMXA = trace/smtcoq.cmxa +CMXS = trace/smt_tactic.cmxs +VCMXS = "NSMTCoq_State.cmxs NSMTCoq_Misc.cmxs NSMTCoq_SMT_terms.cmxs cnf/NSMTCoq_cnf_Cnf.cmxs euf/NSMTCoq_euf_Euf.cmxs lia/NSMTCoq_lia_Lia.cmxs spl/NSMTCoq_spl_Syntactic.cmxs spl/NSMTCoq_spl_Arithmetic.cmxs spl/NSMTCoq_spl_Operators.cmxs NSMTCoq_Trace.cmxs NSMTCoq_SMTCoq.cmxs NSMTCoq_State.cmi NSMTCoq_Misc.cmi NSMTCoq_SMT_terms.cmi cnf/NSMTCoq_cnf_Cnf.cmi euf/NSMTCoq_euf_Euf.cmi lia/NSMTCoq_lia_Lia.cmi spl/NSMTCoq_spl_Syntactic.cmxs spl/NSMTCoq_spl_Arithmetic.cmi spl/NSMTCoq_spl_Operators.cmi NSMTCoq_Trace.cmi NSMTCoq_Trace.cmi NSMTCoq_SMTCoq.cmi" +CAMLLEX = $(CAMLBIN)ocamllex +CAMLYACC = $(CAMLBIN)ocamlyacc + +versions/native/structures.ml + +trace/coqTerms.ml +trace/satAtom.ml +trace/smtAtom.ml +trace/smtAtom.mli +trace/smtCertif.ml +trace/smtCnf.ml +trace/smtForm.ml +trace/smtForm.mli +trace/smtMisc.ml +trace/smt_tactic.ml4 +trace/smtTrace.ml + +verit/smtlib2_ast.ml +verit/smtlib2_genConstr.ml +verit/smtlib2_lex.ml +verit/smtlib2_parse.ml +verit/smtlib2_util.ml +verit/veritParser.ml +verit/veritLexer.ml +verit/verit.ml +verit/veritSyntax.ml +verit/veritSyntax.mli + +zchaff/cnfParser.ml +zchaff/satParser.ml +zchaff/zchaff.ml +zchaff/zchaffParser.ml + +cnf/Cnf.v + +euf/Euf.v + +lia/lia.ml +lia/Lia.v + +spl/Syntactic.v +spl/Arithmetic.v +spl/Operators.v + +Misc.v +SMTCoq.v +SMT_terms.v +State.v +Trace.v diff --git a/src/versions/native/Makefile b/src/versions/native/Makefile new file mode 100644 index 0000000..7162b56 --- /dev/null +++ b/src/versions/native/Makefile @@ -0,0 +1,424 @@ +############################################################################# +## v # The Coq Proof Assistant ## +## "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) + +%.cmo: %.ml4 + $(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $< + +%.cmx: %.ml4 + $(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $< + +%.ml4.d: %.ml4 + $(OCAMLDEP) -slash $(OCAMLLIBS) $(PP) -impl "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) + +%.cmo: %.ml + $(CAMLC) $(ZDEBUG) $(ZFLAGS) $< + +%.cmx: %.ml + $(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $< + +%.ml.d: %.ml + $(OCAMLDEP) -slash $(OCAMLLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) + +%.cmxs: %.cmx + $(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $< + +%.vo %.glob: %.v + $(COQC) $(COQDEBUG) $(COQFLAGS) $* + +%.vi: %.v + $(COQC) -i $(COQDEBUG) $(COQFLAGS) $* + +%.g: %.v + $(GALLINA) $< + +%.tex: %.v + $(COQDOC) $(COQDOCFLAGS) -latex $< -o $@ + +%.html: %.v %.glob + $(COQDOC) $(COQDOCFLAGS) -html $< -o $@ + +%.g.tex: %.v + $(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@ + +%.g.html: %.v %.glob + $(COQDOC)$(COQDOCFLAGS) -html -g $< -o $@ + +%.v.d: %.v + $(COQDEP) -slash $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) + +%.v.beautified: + $(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $* + +# WARNING +# +# This Makefile has been automagically generated +# Edit at your own risks ! +# +# END OF WARNING + diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml new file mode 100644 index 0000000..8f74c32 --- /dev/null +++ b/src/versions/native/structures.ml @@ -0,0 +1,26 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2015 *) +(* *) +(* Michaël Armand *) +(* Benjamin Grégoire *) +(* Chantal Keller *) +(* *) +(* Inria - École Polytechnique - MSR-Inria Joint Lab *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) + +(* Int63 *) +let int63_modules = [["Coq";"Numbers";"Cyclic";"Int63";"Int63Native"]] + +let mkInt i = Term.mkInt (Uint63.of_int i) + + +(* PArray *) +let parray_modules = [["Coq";"Array";"PArray"]] + +let max_array_size = Parray.trunc_size (Uint63.of_int 4194303) +let mkArray = Term.mkArray diff --git a/src/zchaff/zchaff.ml b/src/zchaff/zchaff.ml index b94a0cc..8c07fc7 100644 --- a/src/zchaff/zchaff.ml +++ b/src/zchaff/zchaff.ml @@ -139,7 +139,7 @@ let import_cnf_trace reloc filename first last = let make_roots first last = let cint = Lazy.force cint in - let roots = Array.make (last.id + 2) (Term.mkArray (cint, Array.make 1 (mkInt 0))) in + let roots = Array.make (last.id + 2) (Structures.mkArray (cint, Array.make 1 (mkInt 0))) in let mk_elem l = let x = match Form.pform l with | Fatom x -> x + 2 @@ -150,15 +150,15 @@ let make_roots first last = let root = Array.of_list (get_val !r) in let croot = Array.make (Array.length root + 1) (mkInt 0) in Array.iteri (fun i l -> croot.(i) <- mk_elem l) root; - roots.(!r.id) <- Term.mkArray (cint, croot); + roots.(!r.id) <- Structures.mkArray (cint, croot); r := next !r done; let root = Array.of_list (get_val !r) in let croot = Array.make (Array.length root + 1) (mkInt 0) in Array.iteri (fun i l -> croot.(i) <- mk_elem l) root; - roots.(!r.id) <- Term.mkArray (cint, croot); + roots.(!r.id) <- Structures.mkArray (cint, croot); - Term.mkArray (mklApp carray [|cint|], roots) + Structures.mkArray (mklApp carray [|cint|], roots) let interp_roots first last = let tbl = Hashtbl.create 17 in -- cgit