X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FtacticAstPp.ml;h=eebc73c89c1e1cdb5b01a5ff32c2a02590573af2;hb=46f19eadce5f3a11c0ae26934fd8d1b597906416;hp=0d539ddbe93cf0c5f450d4fd6fd8c90cde708ed2;hpb=9983d0f08f594ddc01700c972d2a2c0f47d32d59;p=helm.git diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml index 0d539ddbe..eebc73c89 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.ml +++ b/helm/ocaml/cic_transformations/tacticAstPp.ml @@ -28,9 +28,12 @@ open Printf open TacticAst let tactical_terminator = "." +let tactic_terminator = tactical_terminator +let command_terminator = tactical_terminator let tactical_separator = ";" -let pp_term term = CicAstPp.pp_term term +let pp_term_ast term = CicAstPp.pp_term term +let pp_term_cic term = CicPp.ppterm term let pp_idents idents = "[" ^ String.concat "; " idents ^ "]" @@ -40,57 +43,60 @@ let pp_reduction_kind = function | `Whd -> "whd" let rec pp_tactic = function - | LocatedTactic (loc, tac) -> pp_tactic tac - | Absurd term -> "absurd" ^ pp_term term - | Apply term -> "apply " ^ pp_term term - | Auto -> "auto" - | Assumption -> "assumption" - | Change (t1, t2, where) -> - sprintf "change %s with %s%s" (pp_term t1) (pp_term t2) + | Absurd (_, term) -> "absurd" ^ pp_term_ast term + | Apply (_, term) -> "apply " ^ pp_term_ast term + | Auto _ -> "auto" + | Assumption _ -> "assumption" + | Change (_, t1, t2, where) -> + sprintf "change %s with %s%s" (pp_term_ast t1) (pp_term_ast t2) (match where with None -> "" | Some ident -> "in " ^ ident) - | Change_pattern (_, _, _) -> assert false (* TODO *) - | Contradiction -> "contradiction" - | Cut term -> "cut " ^ pp_term term - | Decompose (ident, principles) -> + | Change_pattern (_, _, _, _) -> assert false (* TODO *) + | Contradiction _ -> "contradiction" + | Cut (_, term) -> "cut " ^ pp_term_ast term + | Decompose (_, ident, principles) -> sprintf "decompose %s %s" (pp_idents principles) ident - | Discriminate ident -> "discriminate " ^ ident - | Elim (term, using) -> - sprintf "elim " ^ pp_term term ^ - (match using with None -> "" | Some term -> " using " ^ pp_term term) - | ElimType term -> "elim type " ^ pp_term term - | Exact term -> "exact " ^ pp_term term - | Exists -> "exists" - | Fold (kind, term) -> - sprintf "fold %s %s" (pp_reduction_kind kind) (pp_term term) - | Fourier -> "fourier" - | Hint -> "hint" - | Injection ident -> "injection " ^ ident - | Intros (None, []) -> "intro" - | Intros (num, idents) -> + | Discriminate (_, ident) -> "discriminate " ^ ident + | Elim (_, term, using) -> + sprintf "elim " ^ pp_term_ast term ^ + (match using with None -> "" | Some term -> " using " ^ pp_term_ast term) + | ElimType (_, term) -> "elim type " ^ pp_term_ast term + | Exact (_, term) -> "exact " ^ pp_term_ast term + | Exists _ -> "exists" + | Fold (_, kind, term) -> + sprintf "fold %s %s" (pp_reduction_kind kind) (pp_term_ast term) + | Goal (_, n) -> "goal " ^ string_of_int n + | Fourier _ -> "fourier" + | Injection (_, ident) -> "injection " ^ ident + | Intros (_, None, []) -> "intro" + | Intros (_, num, idents) -> sprintf "intros%s%s" (match num with None -> "" | Some num -> " " ^ string_of_int num) (match idents with [] -> "" | idents -> " " ^ pp_idents idents) - | Left -> "left" - | LetIn (term, ident) -> sprintf "let %s in %s" (pp_term term) ident - | Reduce (kind, None) - | Reduce (kind, Some ([], `Goal)) -> pp_reduction_kind kind - | Reduce (kind, Some ([], `Everywhere)) -> + | Left _ -> "left" + | LetIn (_, term, ident) -> sprintf "let %s in %s" (pp_term_ast term) ident + | Reduce (_, kind, None) + | Reduce (_, kind, Some ([], `Goal)) -> pp_reduction_kind kind + | Reduce (_, kind, Some ([], `Everywhere)) -> sprintf "%s in hyp" (pp_reduction_kind kind) - | Reduce (kind, Some (terms, `Goal)) -> + | Reduce (_, kind, Some (terms, `Goal)) -> sprintf "%s %s" (pp_reduction_kind kind) - (String.concat ", " (List.map pp_term terms)) - | Reduce (kind, Some (terms, `Everywhere)) -> + (String.concat ", " (List.map pp_term_ast terms)) + | Reduce (_, kind, Some (terms, `Everywhere)) -> sprintf "%s in hyp %s" (pp_reduction_kind kind) - (String.concat ", " (List.map pp_term terms)) - | Reflexivity -> "reflexivity" - | Replace (t1, t2) -> sprintf "replace %s with %s" (pp_term t1) (pp_term t2) - | Replace_pattern (_, _) -> assert false (* TODO *) - | Rewrite (_, _, _) -> assert false (* TODO *) - | Right -> "right" - | Ring -> "ring" - | Split -> "split" - | Symmetry -> "symmetry" - | Transitivity term -> "transitivity " ^ pp_term term + (String.concat ", " (List.map pp_term_ast terms)) + | Reflexivity _ -> "reflexivity" + | Replace (_, t1, t2) -> + sprintf "replace %s with %s" (pp_term_ast t1) (pp_term_ast t2) + | Replace_pattern (_, _, _) -> assert false (* TODO *) + | Rewrite (_, pos, t, None) -> + sprintf "rewrite %s %s" + (if pos = `Left then "left" else "right") (pp_term_ast t) + | Rewrite _ -> assert false (* TODO *) + | Right _ -> "right" + | Ring _ -> "ring" + | Split _ -> "split" + | Symmetry _ -> "symmetry" + | Transitivity (_, term) -> "transitivity " ^ pp_term_ast term let pp_flavour = function | `Definition -> "Definition" @@ -106,38 +112,59 @@ let pp_search_kind = function | `Match -> "match" | `Elim -> "elim" -let pp_command = function - | Abort -> "Abort" - | Baseuri (Some uri) -> sprintf "Baseuri \"%s\"" uri - | Baseuri None -> "Baseuri" - | Check term -> sprintf "Check %s" (pp_term term) - | Proof -> "Proof" - | Qed name -> - (match name with None -> "Qed" | Some name -> sprintf "Save %s" name) - | Quit -> "Quit" - | Redo None -> "Redo" - | Redo (Some n) -> sprintf "Redo %d" n - | Search_pat (kind, pat) -> +let pp_macro pp_term = function + (* Whelp *) + | WInstance (_, term) -> "whelp instance " ^ pp_term term + | WHint (_, t) -> "whelp hint " ^ pp_term t + | WLocate (_, s) -> "whelp locate " ^ s + | WElim (_, t) -> "whelp elim " ^ pp_term t + | WMatch (_, term) -> "whelp match " ^ pp_term term + (* real macros *) + | Abort _ -> "Abort" + | Check (_, term) -> sprintf "Check %s" (pp_term term) + | Hint _ -> "hint" + | Redo (_, None) -> "Redo" + | Redo (_, Some n) -> sprintf "Redo %d" n + | Search_pat (_, kind, pat) -> sprintf "search %s \"%s\"" (pp_search_kind kind) pat - | Search_term (kind, term) -> + | Search_term (_, kind, term) -> sprintf "search %s %s" (pp_search_kind kind) (pp_term term) - | Inductive (params, types) -> + | Undo (_, None) -> "Undo" + | Undo (_, Some n) -> sprintf "Undo %d" n + | Print (_, name) -> sprintf "Print \"%s\"" name + | Quit _ -> "Quit" + +let pp_macro_ast = pp_macro pp_term_ast +let pp_macro_cic = pp_macro pp_term_cic + +let pp_alias = function + | Ident_alias (id, uri) -> sprintf "alias id \"%s\" = \"%s\"" id uri + | Symbol_alias (symb, instance, desc) -> + sprintf "alias symbol \"%s\" (instance %d) = \"%s\"" + symb instance desc + | Number_alias (instance,desc) -> + sprintf "alias num (instance %d) = \"%s\"" instance desc + +let pp_command = function + | Qed _ -> "qed" + | Set (_, name, value) -> sprintf "Set \"%s\" \"%s\"" name value + | Inductive (_, params, types) -> let pp_params = function | [] -> "" | params -> " " ^ String.concat " " (List.map - (fun (name, typ) -> sprintf "(%s:%s)" name (pp_term typ)) + (fun (name, typ) -> sprintf "(%s:%s)" name (pp_term_ast typ)) params) in let pp_constructors constructors = String.concat "\n" - (List.map (fun (name, typ) -> sprintf "| %s: %s" name (pp_term typ)) + (List.map (fun (name, typ) -> sprintf "| %s: %s" name (pp_term_ast typ)) constructors) in let pp_type (name, _, typ, constructors) = - sprintf "\nwith %s: %s \\def\n%s" name (pp_term typ) + sprintf "\nwith %s: %s \\def\n%s" name (pp_term_ast typ) (pp_constructors constructors) in (match types with @@ -146,37 +173,49 @@ let pp_command = function let fst_typ_pp = sprintf "%sinductive %s%s: %s \\def\n%s" (if inductive then "" else "co") name (pp_params params) - (pp_term typ) (pp_constructors constructors) + (pp_term_ast typ) (pp_constructors constructors) in fst_typ_pp ^ String.concat "" (List.map pp_type tl)) - | Theorem (flavour, name, typ, body) -> + | Theorem (_, flavour, name, typ, body) -> sprintf "%s %s: %s %s" (pp_flavour flavour) (match name with None -> "" | Some name -> name) - (pp_term typ) + (pp_term_ast typ) (match body with | None -> "" - | Some body -> "\\def " ^ pp_term body) - | Undo None -> "Undo" - | Undo (Some n) -> sprintf "Undo %d" n + | Some body -> "\\def " ^ pp_term_ast body) + | Coercion (_,_) -> "Coercion IMPLEMENT ME!!!!!" + | Alias (_,s) -> pp_alias s let rec pp_tactical = function - | LocatedTactical (loc, tac) -> pp_tactical tac - - | Tactic tac -> pp_tactic tac - | Command cmd -> pp_command cmd - - | Fail -> "fail" - | Do (count, tac) -> sprintf "do %d %s" count (pp_tactical tac) - | IdTac -> "id" - | Repeat tac -> "repeat " ^ pp_tactical tac - | Seq tacs -> pp_tacticals tacs - | Then (tac, tacs) -> sprintf "%s [%s]" (pp_tactical tac) (pp_tacticals tacs) - | Tries tacs -> sprintf "tries [%s]" (pp_tacticals tacs) - | Try tac -> "try " ^ pp_tactical tac + | Tactic (_, tac) -> pp_tactic tac + + | Fail _ -> "fail" + | Do (_, count, tac) -> sprintf "do %d %s" count (pp_tactical tac) + | IdTac _ -> "id" + | Repeat (_, tac) -> "repeat " ^ pp_tactical tac + | Seq (_, tacs) -> pp_tacticals tacs + | Then (_, tac, tacs) -> + sprintf "%s [%s]" (pp_tactical tac) (pp_tacticals tacs) + | Tries (_, tacs) -> sprintf "tries [%s]" (pp_tacticals tacs) + | Try (_, tac) -> "try " ^ pp_tactical tac and pp_tacticals tacs = String.concat (tactical_separator ^ " ") (List.map pp_tactical tacs) let pp_tactical tac = pp_tactical tac ^ tactical_terminator - +let pp_tactic tac = pp_tactic tac ^ tactic_terminator +let pp_command tac = pp_command tac ^ command_terminator + +let pp_executable = function + | Macro (_,x) -> pp_macro_ast x + | Tactical (_,x) -> pp_tactical x + | Command (_,x) -> pp_command x + +let pp_comment = function + | Note (_,str) -> sprintf "(* %s *)" str + | Code (_,code) -> sprintf "(** %s. **)" (pp_executable code) + +let pp_statement = function + | Executable (_, ex) -> pp_executable ex + | Comment (_, c) -> pp_comment c