diff options
Diffstat (limited to 'proofs/proof_trees.ml')
| -rw-r--r-- | proofs/proof_trees.ml | 119 |
1 files changed, 0 insertions, 119 deletions
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml index 86ec64c76..34e9a06e7 100644 --- a/proofs/proof_trees.ml +++ b/proofs/proof_trees.ml @@ -248,122 +248,3 @@ let pr_subgoals_existential sigma = function let prest = pr_rec 2 rest in v 0 (int(List.length rest+1) ++ str" subgoals" ++ cut () ++ pg1 ++ prest ++ fnl ()) - -(* -open Ast -open Termast -open Tacexpr -open Rawterm - -let ast_of_cvt_bind f = function - | (NoDepBinding n,c) -> ope ("BINDING", [(num n); ope ("CONSTR",[(f c)])]) - | (DepBinding id,c) -> ope ("BINDING", [nvar id; ope ("CONSTR",[(f c)])]) - | (AnonymousBinding,c) -> ope ("BINDING", [ope ("CONSTR",[(f c)])]) - -let rec ast_of_cvt_intro_pattern = function - | WildPat -> ope ("WILDCAR",[]) - | IdPat id -> nvar id -(* | DisjPat l -> ope ("DISJPATTERN", (List.map ast_of_cvt_intro_pattern l))*) - | ConjPat l -> ope ("CONJPATTERN", (List.map ast_of_cvt_intro_pattern l)) -*) -(* -(* Gives the ast list corresponding to a reduction flag *) -open RedFlags - -let last_of_cvt_flags red = - (if (red_set red fBETA) then [ope("Beta",[])] - else [])@ - (let (n_unf,lconst) = red_get_const red in - let lqid = - List.map - (function - | EvalVarRef id -> nvar id - | EvalConstRef kn -> - ast_of_qualid - (shortest_qualid_of_global None (ConstRef kn))) - lconst in - if lqid = [] then [] - else if n_unf then [ope("Delta",[]);ope("UnfBut",lqid)] - else [ope("Delta",[]);ope("Unf",lqid)])@ - (if (red_set red fIOTA) then [ope("Iota",[])] - else []) -*) -(* -(* Gives the ast corresponding to a reduction expression *) -open Rawterm - -let ast_of_cvt_redexp = function - | Red _ -> ope ("Red",[]) - | Hnf -> ope("Hnf",[]) - | Simpl -> ope("Simpl",[]) -(* - | Cbv flg -> ope("Cbv",last_of_cvt_flags flg) - | Lazy flg -> ope("Lazy",last_of_cvt_flags flg) -*) - | Unfold l -> - ope("Unfold",List.map (fun (locc,sp) -> ope("UNFOLD", - [match sp with - | EvalVarRef id -> nvar id - | EvalConstRef kn -> - ast_of_qualid - (shortest_qualid_of_global None (ConstRef kn))] - @(List.map num locc))) l) - | Fold l -> - ope("Fold",List.map (fun c -> ope ("CONSTR", - [ast_of_constr false (Global.env ()) c])) l) - | Pattern l -> - ope("Pattern",List.map (fun (locc,csr) -> ope("PATTERN", - [ope ("CONSTR",[ast_of_constr false (Global.env ()) csr])]@ - (List.map num locc))) l) -*) -(* Gives the ast corresponding to a tactic argument *) -(* -let ast_of_cvt_arg = function - | Identifier id -> nvar id -(* - | Qualid qid -> ast_of_qualid qid -*) - | Quoted_string s -> string s - | Integer n -> num n -(* | Command c -> ope ("CONSTR",[c])*) - | Constr c -> - ope ("CONSTR",[ast_of_constr false (Global.env ()) c]) - | OpenConstr (_,c) -> - ope ("CONSTR",[ast_of_constr false (Global.env ()) c]) - | Constr_context _ -> - anomalylabstrm "ast_of_cvt_arg" (str - "Constr_context argument could not be used") - | Clause idl -> - let transl = function - | InHyp id -> ope ("INHYP", [nvar id]) - | InHypType id -> ope ("INHYPTYPE", [nvar id]) in - ope ("CLAUSE", List.map transl idl) -(* - | Bindings bl -> ope ("BINDINGS", - List.map (ast_of_cvt_bind (fun x -> x)) bl) - | Cbindings bl -> - ope ("BINDINGS", - List.map - (ast_of_cvt_bind - (ast_of_constr false (Global.env ()))) bl) -*) -(* TODO - | Tacexp ast -> ope ("TACTIC",[ast]) - | Tac (tac,ast) -> ast -*) - | Redexp red -> ope("REDEXP",[ast_of_cvt_redexp red]) - | Fixexp (id,n,c) -> ope ("FIXEXP",[nvar id; num n; ope ("CONSTR",[ast_of_constr false (Global.env ()) c])]) - | Cofixexp (id,c) -> ope ("COFIXEXP",[nvar id; ope ("CONSTR",[ast_of_constr false (Global.env ()) c])]) -(* | Intropattern p -> ast_of_cvt_intro_pattern p*) - | Letpatterns (gl_occ_opt,hyp_occ_list) -> - let hyps_pats = - List.map - (fun (id,l) -> - ope ("HYPPATTERN", nvar id :: (List.map num l))) - hyp_occ_list in - let all_pats = - match gl_occ_opt with - | None -> hyps_pats - | Some l -> hyps_pats @ [ope ("CCLPATTERN", List.map num l)] in - ope ("LETPATTERNS", all_pats) -*) |