aboutsummaryrefslogtreecommitdiffstats
path: root/src/trace/smtCommands.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/trace/smtCommands.ml')
-rw-r--r--src/trace/smtCommands.ml236
1 files changed, 118 insertions, 118 deletions
diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml
index 43365ef..1a990f1 100644
--- a/src/trace/smtCommands.ml
+++ b/src/trace/smtCommands.ml
@@ -34,10 +34,10 @@ let cchecker_b = gen_constant euf_checker_modules "checker_b"
let cchecker_eq_correct =
gen_constant euf_checker_modules "checker_eq_correct"
let cchecker_eq = gen_constant euf_checker_modules "checker_eq"
-let csetup_checker_step_debug =
- gen_constant euf_checker_modules "setup_checker_step_debug"
-let cchecker_step_debug = gen_constant euf_checker_modules "checker_step_debug"
-let cstep = gen_constant euf_checker_modules "step"
+(* let csetup_checker_step_debug =
+ * gen_constant euf_checker_modules "setup_checker_step_debug" *)
+(* let cchecker_step_debug = gen_constant euf_checker_modules "checker_step_debug" *)
+(* let cstep = gen_constant euf_checker_modules "step" *)
let cchecker_debug = gen_constant euf_checker_modules "checker_debug"
let cname_step = gen_constant euf_checker_modules "name_step"
@@ -315,7 +315,7 @@ let checker (rt, ro, ra, rf, roots, max_id, confl) =
Term.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|],
mklApp cchecker [|v 7 (*t_i*); v 6 (*t_func*); v 5 (*t_atom*); v 4 (*t_form*); v 1 (*d*); v 2 (*used_roots*); v 3 (*c*)|]))))))) in
- let res = Vnorm.cbv_vm (Global.env ()) tm (Lazy.force CoqTerms.cbool) in
+ let res = Structures.cbv_vm (Global.env ()) tm (Lazy.force CoqTerms.cbool) in
Format.eprintf " = %s\n : bool@."
(if Term.eq_constr res (Lazy.force CoqTerms.ctrue) then
"true" else "false")
@@ -389,7 +389,7 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) =
mklApp cchecker_debug [|v 7 (*t_i*); v 6 (*t_func*); v 5 (*t_atom*);
v 4 (*t_form*); v 1 (*d*); v 2 (*used_roots*); v 3 (*c*)|]))))))) in
- let res = Vnorm.cbv_vm (Global.env ()) tm
+ let res = Structures.cbv_vm (Global.env ()) tm
(mklApp coption
[|mklApp cprod
[|Lazy.force cnat; Lazy.force cname_step|]|]) in
@@ -453,117 +453,117 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) =
-let rec of_coq_list cl =
- match Term.decompose_app cl with
- | c, _ when Term.eq_constr c (Lazy.force cnil) -> []
- | c, [_; x; cr] when Term.eq_constr c (Lazy.force ccons) ->
- x :: of_coq_list cr
- | _ -> assert false
-
-
-let checker_debug_step t_i t_func t_atom t_form root used_root trace
- (rt, ro, ra, rf, roots, max_id, confl) =
-
- let t_i' = make_t_i rt in
- let ce5 = Structures.mkUConst t_i' in
- let ct_i = Term.mkConst (declare_constant t_i
- (DefinitionEntry ce5, IsDefinition Definition)) in
-
- let t_func' = make_t_func ro ct_i in
- let ce6 = Structures.mkUConst t_func' in
- let ct_func =
- Term.mkConst (declare_constant t_func
- (DefinitionEntry ce6, IsDefinition Definition)) in
-
- let t_atom' = Atom.interp_tbl ra in
- let ce1 = Structures.mkUConst t_atom' in
- let ct_atom =
- Term.mkConst (declare_constant t_atom
- (DefinitionEntry ce1, IsDefinition Definition)) in
-
- let t_form' = snd (Form.interp_tbl rf) in
- let ce2 = Structures.mkUConst t_form' in
- let ct_form =
- Term.mkConst (declare_constant t_form
- (DefinitionEntry ce2, IsDefinition Definition)) in
-
- let (tres, last_root, cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i))
- (interp_conseq_uf ct_i)
- (certif_ops (Some [|ct_i; ct_func; ct_atom; ct_form|])) confl None in
- List.iter (fun (v,ty) ->
- let _ = Structures.declare_new_variable v ty in
- print_assm ty
- ) cuts;
-
- let used_roots = compute_roots roots last_root in
- let croots =
- 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;
- Structures.mkArray (Lazy.force cint, res) in
- let cused_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|];
- Structures.mkArray (Lazy.force cint, res)|] in
- let ce3 = Structures.mkUConst croots in
- let _ = declare_constant root
- (DefinitionEntry ce3, IsDefinition Definition) in
- let ce3' = Structures.mkUConst cused_roots in
- let _ = declare_constant used_root
- (DefinitionEntry ce3', IsDefinition Definition) in
-
- let certif =
- mklApp cCertif [|ct_i; ct_func; ct_atom; ct_form; mkInt (max_id + 1);
- tres;mkInt (get_pos confl)|] in
- let ce4 = Structures.mkUConst certif in
- let _ = declare_constant trace
- (DefinitionEntry ce4, IsDefinition Definition) in
-
- let setup =
- mklApp csetup_checker_step_debug
- [| ct_i; ct_func; ct_atom; ct_form; croots; cused_roots; certif |] in
-
- let setup = Vnorm.cbv_vm (Global.env ()) setup
- (mklApp cprod
- [|Lazy.force cState_S_t;
- mklApp clist [|mklApp cstep
- [|ct_i; ct_func; ct_atom; ct_form|]|]|]) in
-
- let s, steps = match Term.decompose_app setup with
- | c, [_; _; s; csteps] when Term.eq_constr c (Lazy.force cpair) ->
- s, of_coq_list csteps
- | _ -> assert false
- in
-
- let cpt = ref (List.length roots) in
- let debug_step s step =
- incr cpt;
- Format.eprintf "%d@." !cpt;
- let tm =
- mklApp cchecker_step_debug
- [| ct_i; ct_func; ct_atom; ct_form; s; step |] in
-
- let res =
- Vnorm.cbv_vm (Global.env ()) tm
- (mklApp cprod [|Lazy.force cState_S_t; Lazy.force cbool|]) in
-
- match Term.decompose_app res with
- | c, [_; _; s; cbad] when Term.eq_constr c (Lazy.force cpair) ->
- if not (mk_bool cbad) then s
- else Structures.error ("Step number " ^ string_of_int !cpt ^
- " (" ^ string_coq_constr
- (fst (Term.decompose_app step)) ^ ")" ^
- " of the certificate likely failed." )
- | _ -> assert false
- in
-
- List.fold_left debug_step s steps |> ignore;
-
- Structures.error ("Debug checker is only meant to be used for certificates \
- that fail to be checked by SMTCoq.")
+(* let rec of_coq_list cl =
+ * match Term.decompose_app cl with
+ * | c, _ when Term.eq_constr c (Lazy.force cnil) -> []
+ * | c, [_; x; cr] when Term.eq_constr c (Lazy.force ccons) ->
+ * x :: of_coq_list cr
+ * | _ -> assert false *)
+
+
+(* let checker_debug_step t_i t_func t_atom t_form root used_root trace
+ * (rt, ro, ra, rf, roots, max_id, confl) =
+ *
+ * let t_i' = make_t_i rt in
+ * let ce5 = Structures.mkUConst t_i' in
+ * let ct_i = Term.mkConst (declare_constant t_i
+ * (DefinitionEntry ce5, IsDefinition Definition)) in
+ *
+ * let t_func' = make_t_func ro ct_i in
+ * let ce6 = Structures.mkUConst t_func' in
+ * let ct_func =
+ * Term.mkConst (declare_constant t_func
+ * (DefinitionEntry ce6, IsDefinition Definition)) in
+ *
+ * let t_atom' = Atom.interp_tbl ra in
+ * let ce1 = Structures.mkUConst t_atom' in
+ * let ct_atom =
+ * Term.mkConst (declare_constant t_atom
+ * (DefinitionEntry ce1, IsDefinition Definition)) in
+ *
+ * let t_form' = snd (Form.interp_tbl rf) in
+ * let ce2 = Structures.mkUConst t_form' in
+ * let ct_form =
+ * Term.mkConst (declare_constant t_form
+ * (DefinitionEntry ce2, IsDefinition Definition)) in
+ *
+ * let (tres, last_root, cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i))
+ * (interp_conseq_uf ct_i)
+ * (certif_ops (Some [|ct_i; ct_func; ct_atom; ct_form|])) confl None in
+ * List.iter (fun (v,ty) ->
+ * let _ = Structures.declare_new_variable v ty in
+ * print_assm ty
+ * ) cuts;
+ *
+ * let used_roots = compute_roots roots last_root in
+ * let croots =
+ * 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;
+ * Structures.mkArray (Lazy.force cint, res) in
+ * let cused_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|];
+ * Structures.mkArray (Lazy.force cint, res)|] in
+ * let ce3 = Structures.mkUConst croots in
+ * let _ = declare_constant root
+ * (DefinitionEntry ce3, IsDefinition Definition) in
+ * let ce3' = Structures.mkUConst cused_roots in
+ * let _ = declare_constant used_root
+ * (DefinitionEntry ce3', IsDefinition Definition) in
+ *
+ * let certif =
+ * mklApp cCertif [|ct_i; ct_func; ct_atom; ct_form; mkInt (max_id + 1);
+ * tres;mkInt (get_pos confl)|] in
+ * let ce4 = Structures.mkUConst certif in
+ * let _ = declare_constant trace
+ * (DefinitionEntry ce4, IsDefinition Definition) in
+ *
+ * let setup =
+ * mklApp csetup_checker_step_debug
+ * [| ct_i; ct_func; ct_atom; ct_form; croots; cused_roots; certif |] in
+ *
+ * let setup = Structures.cbv_vm (Global.env ()) setup
+ * (mklApp cprod
+ * [|Lazy.force cState_S_t;
+ * mklApp clist [|mklApp cstep
+ * [|ct_i; ct_func; ct_atom; ct_form|]|]|]) in
+ *
+ * let s, steps = match Term.decompose_app setup with
+ * | c, [_; _; s; csteps] when Term.eq_constr c (Lazy.force cpair) ->
+ * s, of_coq_list csteps
+ * | _ -> assert false
+ * in
+ *
+ * let cpt = ref (List.length roots) in
+ * let debug_step s step =
+ * incr cpt;
+ * Format.eprintf "%d@." !cpt;
+ * let tm =
+ * mklApp cchecker_step_debug
+ * [| ct_i; ct_func; ct_atom; ct_form; s; step |] in
+ *
+ * let res =
+ * Structures.cbv_vm (Global.env ()) tm
+ * (mklApp cprod [|Lazy.force cState_S_t; Lazy.force cbool|]) in
+ *
+ * match Term.decompose_app res with
+ * | c, [_; _; s; cbad] when Term.eq_constr c (Lazy.force cpair) ->
+ * if not (mk_bool cbad) then s
+ * else Structures.error ("Step number " ^ string_of_int !cpt ^
+ * " (" ^ string_coq_constr
+ * (fst (Term.decompose_app step)) ^ ")" ^
+ * " of the certificate likely failed." )
+ * | _ -> assert false
+ * in
+ *
+ * List.fold_left debug_step s steps |> ignore;
+ *
+ * Structures.error ("Debug checker is only meant to be used for certificates \
+ * that fail to be checked by SMTCoq.") *)
@@ -725,7 +725,7 @@ let core_tactic call_solver solver_logic rt ro ra rf ra' rf' vm_cast lcpl lcepl
let tlcepl = List.map (Structures.interp_constr env sigma) lcepl in
let lcpl = lcpl @ tlcepl in
- let lcl = List.map (Retyping.get_type_of env sigma) lcpl in
+ let lcl = List.map (Structures.retyping_get_type_of env sigma) lcpl in
let lsmt = List.map (of_coq_lemma rt ro ra' rf' env sigma solver_logic) lcl in
let l_pl_ls = List.combine (List.combine lcl lcpl) lsmt in
generated by cgit (git 2.34.1) at 2024-06-26 16:21:07 +0000