let types = List.rev_map to_ident types in
sprintf "decompose %s %s%s" (pp_idents types) (opt_string_pp what) (pp_intros_specs (None, names))
| Demodulate _ -> "demodulate"
let types = List.rev_map to_ident types in
sprintf "decompose %s %s%s" (pp_idents types) (opt_string_pp what) (pp_intros_specs (None, names))
| Demodulate _ -> "demodulate"
| Elim (_, term, using, num, idents) ->
sprintf "elim " ^ term_pp term ^
(match using with None -> "" | Some term -> " using " ^ term_pp term)
| Elim (_, term, using, num, idents) ->
sprintf "elim " ^ term_pp term ^
(match using with None -> "" | Some term -> " using " ^ term_pp term)
| Intros (_, None, []) -> "intros"
| Inversion (_, term) -> "inversion " ^ term_pp term
| Intros (_, num, idents) ->
| Intros (_, None, []) -> "intros"
| Inversion (_, term) -> "inversion " ^ term_pp term
| Intros (_, num, idents) ->
| Symmetry _ -> "symmetry"
| Transitivity (_, term) -> "transitivity " ^ term_pp term
(* Tattiche Aggiunte *)
| Assume (_, ident , term) -> "assume" ^ ident ^ ":" ^ term_pp term
| Suppose (_, term, ident,term1) -> "suppose" ^ term_pp term ^ "(" ^ ident ^ ")" ^ (match term1 with None -> " " | Some term1 -> term_pp term1)
| Bydone (_, term) -> "by" ^ (match term with None -> "_" | Some term -> term_pp term) ^ "done"
| Symmetry _ -> "symmetry"
| Transitivity (_, term) -> "transitivity " ^ term_pp term
(* Tattiche Aggiunte *)
| Assume (_, ident , term) -> "assume" ^ ident ^ ":" ^ term_pp term
| Suppose (_, term, ident,term1) -> "suppose" ^ term_pp term ^ "(" ^ ident ^ ")" ^ (match term1 with None -> " " | Some term1 -> term_pp term1)
| Bydone (_, term) -> "by" ^ (match term with None -> "_" | Some term -> term_pp term) ^ "done"
- | By_term_we_proved (_, term, term1, ident, term2) -> "by" ^ (match term with None -> "_" | Some term -> term_pp term) ^ "we proved" ^ term_pp term1 ^ "(" ^ident^ ")" ^
+ | By_term_we_proved (_, term, term1, ident, term2) -> "by" ^ (match term with None -> "_" | Some term -> term_pp term) ^ "we proved" ^ term_pp term1 ^ (match ident with None -> "" | Some ident -> "(" ^ident^ ")") ^
- | We_need_to_prove (_, term, ident, term1) -> "we need to prove" ^ term_pp term ^ "(" ^ ident ^ ")" ^ (match term1 with None -> " " | Some term1 -> term_pp term1)
+ | We_need_to_prove (_, term, ident, term1) -> "we need to prove" ^ term_pp term ^ (match ident with None -> "" | Some ident -> "(" ^ ident ^ ")") ^ (match term1 with None -> " " | Some term1 -> term_pp term1)
| We_proceed_by_induction_on (_, term, term1) -> "we proceed by induction on" ^ term_pp term ^ "to prove" ^ term_pp term1
| Byinduction (_, term, ident) -> "by induction hypothesis we know" ^ term_pp term ^ "(" ^ ident ^ ")"
| Thesisbecomes (_, term) -> "the thesis becomes " ^ term_pp term
| We_proceed_by_induction_on (_, term, term1) -> "we proceed by induction on" ^ term_pp term ^ "to prove" ^ term_pp term1
| Byinduction (_, term, ident) -> "by induction hypothesis we know" ^ term_pp term ^ "(" ^ ident ^ ")"
| Thesisbecomes (_, term) -> "the thesis becomes " ^ term_pp term
| WElim (_, t) -> "whelp elim " ^ term_pp t
| WMatch (_, term) -> "whelp match " ^ term_pp term
(* real macros *)
| WElim (_, t) -> "whelp elim " ^ term_pp t
| WMatch (_, term) -> "whelp match " ^ term_pp term
(* real macros *)
-let pp_coercion uri do_composites =
- sprintf "coercion %s (* %s *)" (UriManager.string_of_uri uri)
+let pp_coercion uri do_composites arity =
+ sprintf "coercion %s %d (* %s *)" (UriManager.string_of_uri uri) arity
-let pp_command ~obj_pp = function
+let pp_command ~term_pp ~obj_pp = function
+ | Coercion (_, uri, do_composites, i) -> pp_coercion uri do_composites i
+ | Default (_,what,uris) -> pp_default what uris
+ | Drop _ -> "drop"
+ | Relation (_,id,a,aeq,refl,sym,trans) ->
+ "relation " ^ term_pp aeq ^ " on " ^ term_pp a ^
+ (match refl with
+ Some r -> " reflexivity proved by " ^ term_pp r
+ | None -> "") ^
+ (match sym with
+ Some r -> " symmetry proved by " ^ term_pp r
+ | None -> "") ^
+ (match trans with
+ Some r -> " transitivity proved by " ^ term_pp r
+ | None -> "")
| Print (_,s) -> "print " ^ s
| Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value
| Print (_,s) -> "print " ^ s
| Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value
- | Coercion (_, uri, do_composites) -> pp_coercion uri do_composites
- | Obj (_,obj) -> obj_pp obj
- | Default (_,what,uris) ->
- pp_default what uris
| First (_, tacs) -> sprintf "tries [%s]" (pp_tacticals ~sep:" | " tacs)
| Try (_, tac) -> "try " ^ pp_tactical ~term_pp ~lazy_term_pp tac
| Solve (_, tac) -> sprintf "solve [%s]" (pp_tacticals ~sep:" | " tac)
| First (_, tacs) -> sprintf "tries [%s]" (pp_tacticals ~sep:" | " tacs)
| Try (_, tac) -> "try " ^ pp_tactical ~term_pp ~lazy_term_pp tac
| Solve (_, tac) -> sprintf "solve [%s]" (pp_tacticals ~sep:" | " tac)
pp_tactical ~lazy_term_pp ~term_pp tac
^ pp_tactical ~lazy_term_pp ~term_pp punct
| Tactical (_, tac, None) -> pp_tactical ~lazy_term_pp ~term_pp tac
pp_tactical ~lazy_term_pp ~term_pp tac
^ pp_tactical ~lazy_term_pp ~term_pp punct
| Tactical (_, tac, None) -> pp_tactical ~lazy_term_pp ~term_pp tac