X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=components%2Facic_content%2FcicNotationPp.ml;fp=components%2Facic_content%2FcicNotationPp.ml;h=50312ff12e117d7208fcbc6437400305bd317c52;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1 diff --git a/components/acic_content/cicNotationPp.ml b/components/acic_content/cicNotationPp.ml new file mode 100644 index 000000000..50312ff12 --- /dev/null +++ b/components/acic_content/cicNotationPp.ml @@ -0,0 +1,355 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +(* $Id$ *) + +open Printf + +module Ast = CicNotationPt +module Env = CicNotationEnv + + (* when set to true debugging information, not in sync with input syntax, will + * be added to the output of pp_term. + * set to false if you need, for example, cut and paste from matitac output to + * matitatop *) +let debug_printing = true + +let pp_binder = function + | `Lambda -> "lambda" + | `Pi -> "Pi" + | `Exists -> "exists" + | `Forall -> "forall" + +let pp_literal = + if debug_printing then + (function (* debugging version *) + | `Symbol s -> sprintf "symbol(%s)" s + | `Keyword s -> sprintf "keyword(%s)" s + | `Number s -> sprintf "number(%s)" s) + else + (function + | `Symbol s + | `Keyword s + | `Number s -> s) + +let pp_assoc = + function + | Gramext.NonA -> "NonA" + | Gramext.LeftA -> "LeftA" + | Gramext.RightA -> "RightA" + +let pp_pos = + function +(* `None -> "`None" *) + | `Left -> "`Left" + | `Right -> "`Right" + | `Inner -> "`Inner" + +let pp_attribute = + function + | `IdRef id -> sprintf "x(%s)" id + | `XmlAttrs attrs -> + sprintf "X(%s)" + (String.concat ";" + (List.map (fun (_, n, v) -> sprintf "%s=%s" n v) attrs)) + | `Level (prec, assoc) -> sprintf "L(%d%s)" prec (pp_assoc assoc) + | `Raw _ -> "R" + | `Loc _ -> "@" + | `ChildPos p -> sprintf "P(%s)" (pp_pos p) + +let pp_capture_variable pp_term = + function + | term, None -> pp_term (* ~pp_parens:false *) term + | term, Some typ -> "(" ^ pp_term (* ~pp_parens:false *) term ^ ": " ^ pp_term typ ^ ")" + +let rec pp_term ?(pp_parens = true) t = + let t_pp = + match t with + | Ast.AttributedTerm (attr, term) when debug_printing -> + sprintf "%s[%s]" (pp_attribute attr) (pp_term ~pp_parens:false term) + | Ast.AttributedTerm (`Raw text, _) -> text + | Ast.AttributedTerm (_, term) -> pp_term ~pp_parens:false term + | Ast.Appl terms -> + sprintf "%s" (String.concat " " (List.map pp_term terms)) + | Ast.Binder (`Forall, (Ast.Ident ("_", None), typ), body) + | Ast.Binder (`Pi, (Ast.Ident ("_", None), typ), body) -> + sprintf "%s \\to %s" + (match typ with None -> "?" | Some typ -> pp_term typ) + (pp_term ~pp_parens:true body) + | Ast.Binder (kind, var, body) -> + sprintf "\\%s %s.%s" (pp_binder kind) (pp_capture_variable pp_term var) + (pp_term ~pp_parens:true body) + | Ast.Case (term, indtype, typ, patterns) -> + sprintf "match %s%s%s with %s" + (pp_term term) + (match indtype with + | None -> "" + | Some (ty, href_opt) -> + sprintf " in %s%s" ty + (match debug_printing, href_opt with + | true, Some uri -> + sprintf "(i.e.%s)" (UriManager.string_of_uri uri) + | _ -> "")) + (match typ with None -> "" | Some t -> sprintf " return %s" (pp_term t)) + (pp_patterns patterns) + | Ast.Cast (t1, t2) -> sprintf "(%s: %s)" (pp_term ~pp_parens:true t1) (pp_term ~pp_parens:true t2) + | Ast.LetIn ((var,t2), t1, t3) -> +(* let t2 = match t2 with None -> Ast.Implicit | Some t -> t in *) + sprintf "let %s \\def %s in %s" (pp_term var) +(* (pp_term ~pp_parens:true t2) *) + (pp_term ~pp_parens:true t1) + (pp_term ~pp_parens:true t3) + | Ast.LetRec (kind, definitions, term) -> + let rec get_guard i = function + | [] -> (*assert false*) Ast.Implicit + | [term, _] when i = 1 -> term + | _ :: tl -> get_guard (pred i) tl + in + let map (params, (id,typ), body, i) = + let typ = + match typ with + None -> Ast.Implicit + | Some typ -> typ + in + sprintf "%s %s on %s: %s \\def %s" + (pp_term ~pp_parens:false term) + (String.concat " " (List.map (pp_capture_variable pp_term) params)) + (pp_term ~pp_parens:false (get_guard i params)) + (pp_term typ) (pp_term body) + in + sprintf "let %s %s in %s" + (match kind with `Inductive -> "rec" | `CoInductive -> "corec") + (String.concat " and " (List.map map definitions)) + (pp_term term) + | Ast.Ident (name, Some []) | Ast.Ident (name, None) + | Ast.Uri (name, Some []) | Ast.Uri (name, None) -> + name + | Ast.Ident (name, Some substs) + | Ast.Uri (name, Some substs) -> + sprintf "%s \\subst [%s]" name (pp_substs substs) + | Ast.Implicit -> "?" + | Ast.Meta (index, substs) -> + sprintf "%d[%s]" index + (String.concat "; " + (List.map (function None -> "_" | Some t -> pp_term t) substs)) + | Ast.Num (num, _) -> num + | Ast.Sort `Set -> "Set" + | Ast.Sort `Prop -> "Prop" + | Ast.Sort (`Type _) -> "Type" + | Ast.Sort `CProp -> "CProp" + | Ast.Symbol (name, _) -> "'" ^ name + + | Ast.UserInput -> "" + + | Ast.Literal l -> pp_literal l + | Ast.Layout l -> pp_layout l + | Ast.Magic m -> pp_magic m + | Ast.Variable v -> pp_variable v + in + match pp_parens, t with + | false, _ + | true, Ast.Implicit + | true, Ast.Sort _ + | true, Ast.Ident (_, Some []) + | true, Ast.Ident (_, None) -> t_pp + | _ -> sprintf "(%s)" t_pp + +and pp_subst (name, term) = sprintf "%s \\Assign %s" name (pp_term term) +and pp_substs substs = String.concat "; " (List.map pp_subst substs) + +and pp_pattern = + function + Ast.Pattern (head, href, vars), term -> + let head_pp = + head ^ + (match debug_printing, href with + | true, Some uri -> sprintf "(i.e.%s)" (UriManager.string_of_uri uri) + | _ -> "") + in + sprintf "%s \\Rightarrow %s" + (match vars with + | [] -> head_pp + | _ -> + sprintf "(%s %s)" head_pp + (String.concat " " (List.map (pp_capture_variable pp_term) vars))) + (pp_term term) + | Ast.Wildcard, term -> + sprintf "_ \\Rightarrow %s" (pp_term term) + +and pp_patterns patterns = + sprintf "[%s]" (String.concat " | " (List.map pp_pattern patterns)) + +and pp_box_spec (kind, spacing, indent) = + let int_of_bool b = if b then 1 else 0 in + let kind_string = + match kind with + Ast.H -> "H" | Ast.V -> "V" | Ast.HV -> "HV" | Ast.HOV -> "HOV" + in + sprintf "%sBOX%d%d" kind_string (int_of_bool spacing) (int_of_bool indent) + +and pp_layout = function + | Ast.Sub (t1, t2) -> sprintf "%s \\SUB %s" (pp_term t1) (pp_term t2) + | Ast.Sup (t1, t2) -> sprintf "%s \\SUP %s" (pp_term t1) (pp_term t2) + | Ast.Below (t1, t2) -> sprintf "%s \\BELOW %s" (pp_term t1) (pp_term t2) + | Ast.Above (t1, t2) -> sprintf "%s \\ABOVE %s" (pp_term t1) (pp_term t2) + | Ast.Over (t1, t2) -> sprintf "[%s \\OVER %s]" (pp_term t1) (pp_term t2) + | Ast.Atop (t1, t2) -> sprintf "[%s \\ATOP %s]" (pp_term t1) (pp_term t2) + | Ast.Frac (t1, t2) -> sprintf "\\FRAC %s %s" (pp_term t1) (pp_term t2) + | Ast.Sqrt t -> sprintf "\\SQRT %s" (pp_term t) + | Ast.Root (arg, index) -> + sprintf "\\ROOT %s \\OF %s" (pp_term index) (pp_term arg) + | Ast.Break -> "\\BREAK" +(* | Space -> "\\SPACE" *) + | Ast.Box (box_spec, terms) -> + sprintf "\\%s [%s]" (pp_box_spec box_spec) + (String.concat " " (List.map pp_term terms)) + | Ast.Group terms -> + sprintf "\\GROUP [%s]" (String.concat " " (List.map pp_term terms)) + +and pp_magic = function + | Ast.List0 (t, sep_opt) -> + sprintf "list0 %s%s" (pp_term t) (pp_sep_opt sep_opt) + | Ast.List1 (t, sep_opt) -> + sprintf "list1 %s%s" (pp_term t) (pp_sep_opt sep_opt) + | Ast.Opt t -> sprintf "opt %s" (pp_term t) + | Ast.Fold (kind, p_base, names, p_rec) -> + let acc = match names with acc :: _ -> acc | _ -> assert false in + sprintf "fold %s %s rec %s %s" + (pp_fold_kind kind) (pp_term p_base) acc (pp_term p_rec) + | Ast.Default (p_some, p_none) -> + sprintf "default %s %s" (pp_term p_some) (pp_term p_none) + | Ast.If (p_test, p_true, p_false) -> + sprintf "if %s then %s else %s" + (pp_term p_test) (pp_term p_true) (pp_term p_false) + | Ast.Fail -> "fail" + +and pp_fold_kind = function + | `Left -> "left" + | `Right -> "right" + +and pp_sep_opt = function + | None -> "" + | Some sep -> sprintf " sep %s" (pp_literal sep) + +and pp_variable = function + | Ast.NumVar s -> "number " ^ s + | Ast.IdentVar s -> "ident " ^ s + | Ast.TermVar s -> "term " ^ s + | Ast.Ascription (t, n) -> assert false + | Ast.FreshVar n -> "fresh " ^ n + +let _pp_term = ref (pp_term ~pp_parens:false) +let pp_term t = !_pp_term t +let set_pp_term f = _pp_term := f + +let pp_params pp_term = function + | [] -> "" + | params -> " " ^ String.concat " " (List.map (pp_capture_variable pp_term) params) + +let pp_flavour = function + | `Definition -> "definition" + | `MutualDefinition -> assert false + | `Fact -> "fact" + | `Goal -> "goal" + | `Lemma -> "lemma" + | `Remark -> "remark" + | `Theorem -> "theorem" + | `Variant -> "variant" + | `Axiom -> "axiom" + +let pp_fields pp_term fields = + (if fields <> [] then "\n" else "") ^ + String.concat ";\n" + (List.map + (fun (name,ty,coercion,arity) -> + " " ^ name ^ + if coercion then (":" ^ + if arity > 0 then string_of_int arity else "" ^ ">") else ": " ^ + pp_term ty) fields) + +let pp_obj pp_term = function + | Ast.Inductive (params, types) -> + let pp_constructors constructors = + String.concat "\n" + (List.map (fun (name, typ) -> sprintf "| %s: %s" name (pp_term typ)) + constructors) + in + let pp_type (name, _, typ, constructors) = + sprintf "\nwith %s: %s \\def\n%s" name (pp_term typ) + (pp_constructors constructors) + in + (match types with + | [] -> assert false + | (name, inductive, typ, constructors) :: tl -> + let fst_typ_pp = + sprintf "%sinductive %s%s: %s \\def\n%s" + (if inductive then "" else "co") name (pp_params pp_term params) + (pp_term typ) (pp_constructors constructors) + in + fst_typ_pp ^ String.concat "" (List.map pp_type tl)) + | Ast.Theorem (`MutualDefinition, name, typ, body) -> + sprintf "<>" + | Ast.Theorem (flavour, name, typ, body) -> + sprintf "%s %s:\n %s\n%s" + (pp_flavour flavour) + name + (pp_term typ) + (match body with + | None -> "" + | Some body -> "\\def\n " ^ pp_term body) + | Ast.Record (params,name,ty,fields) -> + "record " ^ name ^ " " ^ pp_params pp_term params ^ ": " ^ pp_term ty ^ + " \\def {" ^ pp_fields pp_term fields ^ "\n}" + +let rec pp_value = function + | Env.TermValue t -> sprintf "$%s$" (pp_term t) + | Env.StringValue s -> sprintf "\"%s\"" s + | Env.NumValue n -> n + | Env.OptValue (Some v) -> "Some " ^ pp_value v + | Env.OptValue None -> "None" + | Env.ListValue l -> sprintf "[%s]" (String.concat "; " (List.map pp_value l)) + +let rec pp_value_type = + function + | Env.TermType -> "Term" + | Env.StringType -> "String" + | Env.NumType -> "Number" + | Env.OptType t -> "Maybe " ^ pp_value_type t + | Env.ListType l -> "List " ^ pp_value_type l + +let pp_env env = + String.concat "; " + (List.map + (fun (name, (ty, value)) -> + sprintf "%s : %s = %s" name (pp_value_type ty) (pp_value value)) + env) + +let rec pp_cic_appl_pattern = function + | Ast.UriPattern uri -> UriManager.string_of_uri uri + | Ast.VarPattern name -> name + | Ast.ImplicitPattern -> "_" + | Ast.ApplPattern aps -> + sprintf "(%s)" (String.concat " " (List.map pp_cic_appl_pattern aps)) +