Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Conversion logging #4

Open
wants to merge 4 commits into
base: master
Choose a base branch
from
Open

Conversion logging #4

Changes from 1 commit
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
e001b69
Ruby script to find all parameters of CONV_TAC
szegedy Mar 28, 2017
8f46f59
Added loogging of CONV_TAC.
szegedy Mar 28, 2017
c8fad59
Added forgotten file log.ml
szegedy Mar 28, 2017
1357d91
Merge remote-tracking branch 'origin/master'
szegedy Mar 28, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions log.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ and tactic_log =
| Fake_log (* see VALID *)
| Label_tac_log of string * thm
| Accept_tac_log of thm
| Conv_tac_log of conv (* TODO will need to expand since conv:term->thm *)
| Conv_tac_log of string * conv (* TODO will need to expand since conv:term->thm *)
| Abs_tac_log
| Mk_comb_tac_log
| Disch_tac_log
Expand Down Expand Up @@ -108,7 +108,7 @@ let tactic_name taclog =
Fake_log -> "Fake_log"
| Label_tac_log (st, th) -> "Label_tac_log"
| Accept_tac_log th -> "Accept_tac_log"
| Conv_tac_log c -> "Conv_tac_log"
| Conv_tac_log (_, c) -> "Conv_tac_log"
| Abs_tac_log -> "Abs_tac_log"
| Mk_comb_tac_log -> "Mk_comb_tac_log"
| Disch_tac_log -> "Disch_tac_log"
Expand Down Expand Up @@ -143,7 +143,7 @@ let sexp_tactic_log taclog =
Fake_log -> simple "Fake_log"
| Label_tac_log (st, th) -> Snode [Sleaf "Label_tac_log"; Sleaf st; sexp_thm th]
| Accept_tac_log th -> thm "Accept_tac_log" th
| Conv_tac_log c -> Snode [Sleaf "Conv_tac_log"; sexp_conv c]
| Conv_tac_log (s, c) -> Snode [Sleaf "Conv_tac_log"; Sleaf s; sexp_conv c]
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This will break any S-expr parser that we write, since the leaf strings aren't escaped. Let's leave it out for now.

| Abs_tac_log -> simple "Abs_tac_log"
| Mk_comb_tac_log -> simple "Mk_comb_tac_log"
| Disch_tac_log -> simple "Disch_tac_log"
Expand Down Expand Up @@ -173,7 +173,7 @@ let sexp_tactic_log taclog =
| Backchain_tac_log th -> thm "Backchain_tac_log" th
| Imp_subst_tac_log th -> thm "Imp_subst_tac_log" th
| Unknown_log -> simple "Unknown_log";;

let rec sexp_proof_log plog =
let Proof_log ((gl:goal), (taclog:tactic_log), (logl:proof_log list)) = plog in
Snode [Sleaf "p"; sexp_goal gl; sexp_tactic_log taclog; Snode (map sexp_proof_log logl)]
Expand Down