diff options
Diffstat (limited to 'contrib/jprover')
| -rw-r--r-- | contrib/jprover/jall.ml | 13 | ||||
| -rw-r--r-- | contrib/jprover/jprover.ml4 | 21 | ||||
| -rw-r--r-- | contrib/jprover/jtunify.ml | 2 |
3 files changed, 12 insertions, 24 deletions
diff --git a/contrib/jprover/jall.ml b/contrib/jprover/jall.ml index 876dc6c0..a2a72676 100644 --- a/contrib/jprover/jall.ml +++ b/contrib/jprover/jall.ml @@ -1788,11 +1788,13 @@ struct else if o = ("",Orr,dummyt,dummyt) then (* Orr is a dummy for no d-gen. rule *) ptree else +(* let (x1,x2,x3,x4) = r and (y1,y2,y3,y4) = o in -(* print_endline ("top or_l: "^x1); + print_endline ("top or_l: "^x1); print_endline ("or_l address: "^addr); - print_endline ("top dgen-rule: "^y1); *) + print_endline ("top dgen-rule: "^y1); +*) trans_add_branch r o addr "" ptree dglist (subrel,tsubrel) (* Isolate layer and outer recursion structure *) @@ -1989,8 +1991,7 @@ struct let (srel,sren) = build_formula_rel dtreelist slist predname in (srel @ rest_rel),(sren @ rest_renlist) | Gamma -> - let n = Array.length suctrees - and succlist = (Array.to_list suctrees) in + let succlist = (Array.to_list suctrees) in let dtreelist = (List.map (fun x -> (1,x)) succlist) in (* if (nonemptys suctrees 0 n) = 1 then let (srel,sren) = build_formula_rel dtreelist slist pos.name in @@ -3039,8 +3040,7 @@ struct if (p.pt = Delta) then (* keep the tree ordering for the successor position only *) let psucc = List.hd succs in let ppsuccs = tpredsucc psucc ftree in - let pre = List.hd ppsuccs - and sucs = List.tl ppsuccs in + let sucs = List.tl ppsuccs in replace_ordering (psucc.name) sucs redpo (* union the succsets of psucc *) else redpo @@ -4582,7 +4582,6 @@ let gen_prover mult_limit logic calculus hyps concls = let (input_map,renamed_termlist) = renam_free_vars (hyps @ concls) in let (ftree,red_ordering,eqlist,(sigmaQ,sigmaJ),ext_proof) = prove mult_limit renamed_termlist logic in let sequent_proof = reconstruct ftree red_ordering sigmaQ ext_proof logic calculus in - let (ptree,count_ax) = bproof sequent_proof in let idl = build_formula_id ftree in (* print_ftree ftree; apple *) (* transform types and rename constants *) diff --git a/contrib/jprover/jprover.ml4 b/contrib/jprover/jprover.ml4 index dd76438f..294943f7 100644 --- a/contrib/jprover/jprover.ml4 +++ b/contrib/jprover/jprover.ml4 @@ -51,7 +51,7 @@ let mbreak s = Format.print_flush (); print_string ("-break at: "^s); let jp_error re = raise (JT.RefineError ("jprover", JT.StringError re)) (* print Coq constructor *) -let print_constr ct = Pp.ppnl (PR.prterm ct); Format.print_flush () +let print_constr ct = Pp.ppnl (PR.pr_lconstr ct); Format.print_flush () let rec print_constr_list = function | [] -> () @@ -361,7 +361,7 @@ let dyn_impl id gl = (TCL.tclTHENLAST (TCL.tclTHENS (T.cut b) [T.intro_using id2;TCL.tclIDTAC]) (T.apply_term (TR.mkVar (short_addr id)) - [TR.mkMeta (Clenv.new_meta())])) gl + [TR.mkMeta (Evarutil.new_meta())])) gl let dyn_allr c = (* [c] must be an eigenvariable which replaces [v] *) HT.h_intro (N.id_of_string c) @@ -390,7 +390,7 @@ let dyn_truer = (* Do the proof by the guidance of JProver. *) let do_one_step inf = - let (rule, (s1, t1), ((s2, t2) as k)) = inf in + let (rule, (s1, t1), (s2, t2)) = inf in begin (*i if not (Jterm.is_xnil_term t2) then begin @@ -542,20 +542,9 @@ let jpn n gls = TCL.tclTHEN (TCL.tclTRY T.red_in_concl) (TCL.tclTHEN (unfail_gen (List.map TR.mkVar ls)) (jp n)) gls -(* -let dyn_jpn l gls = - match l with - | [PT.Integer n] -> jpn n - | _ -> jp_error "Impossible!!!" - - -let h_jp = TM.hide_tactic "Jp" dyn_jp - -let h_jpn = TM.hide_tactic "Jpn" dyn_jpn -*) -TACTIC EXTEND Jprover - [ "Jp" natural_opt(n) ] -> [ jpn n ] +TACTIC EXTEND jprover + [ "jp" natural_opt(n) ] -> [ jpn n ] END (* diff --git a/contrib/jprover/jtunify.ml b/contrib/jprover/jtunify.ml index 2295e62c..91aa6b4b 100644 --- a/contrib/jprover/jtunify.ml +++ b/contrib/jprover/jtunify.ml @@ -177,7 +177,7 @@ let rec combine subst ((ov,oslist) as one_subst) = else (f::rest_combine) -let compose ((n,subst) as sigma) ((ov,oslist) as one_subst) = +let compose ((n,subst) as _sigma) ((ov,oslist) as one_subst) = let com = combine subst one_subst in (* begin print_endline "!!!!!!!!!test print!!!!!!!!!!"; |