X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationPp.ml;fp=helm%2Focaml%2Fcic_notation%2FcicNotationPp.ml;h=0000000000000000000000000000000000000000;hb=9a0e4f3be9f70662f18d2d3b6dd60ae79fba565b;hp=b5a2e04f22a9b9e837ce4694a4d1a6234c815949;hpb=f59550b5a9cdddbb348697201fae7d736d6b96c5;p=helm.git diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml deleted file mode 100644 index b5a2e04f2..000000000 --- a/helm/ocaml/cic_notation/cicNotationPp.ml +++ /dev/null @@ -1,259 +0,0 @@ -(* 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/ - *) - -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 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 body) - | Ast.Binder (kind, var, body) -> - sprintf "\\%s %s.%s" (pp_binder kind) (pp_capture_variable var) - (pp_term body) - | Ast.Case (term, indtype, typ, patterns) -> - sprintf "%smatch %s%s with %s" - (match typ with None -> "" | Some t -> sprintf "[%s]" (pp_term t)) - (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) - | _ -> "")) - (pp_patterns patterns) - | Ast.Cast (t1, t2) -> sprintf "(%s: %s)" (pp_term t1) (pp_term t2) - | Ast.LetIn (var, t1, t2) -> - sprintf "let %s = %s in %s" (pp_capture_variable var) (pp_term t1) - (pp_term t2) - | Ast.LetRec (kind, definitions, term) -> - sprintf "let %s %s in %s" - (match kind with `Inductive -> "rec" | `CoInductive -> "corec") - (String.concat " and " - (List.map - (fun (var, body, _) -> - sprintf "%s = %s" (pp_capture_variable var) (pp_term body)) - 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 - if pp_parens then sprintf "(%s)" t_pp - else 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 ((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 vars))) - (pp_term term) - -and pp_patterns patterns = - sprintf "[%s]" (String.concat " | " (List.map pp_pattern patterns)) - -and pp_capture_variable = function - | term, None -> pp_term term - | term, Some typ -> "(" ^ pp_term term ^ ": " ^ pp_term typ ^ ")" - -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 t = pp_term ~pp_parens:false t - -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) -