X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationPp.ml;h=9118d1c11d359c4c9767252ee0cb7e290cd6ab9e;hb=f981a524748846acc29b76b6e616af110b4ee13d;hp=e04b00b7057cbd622fce15ed55daee247e07057b;hpb=ba2dfe6409e95bf9e558dc0d4be382b068671409;p=helm.git diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml index e04b00b70..9118d1c11 100644 --- a/helm/ocaml/cic_notation/cicNotationPp.ml +++ b/helm/ocaml/cic_notation/cicNotationPp.ml @@ -28,7 +28,11 @@ open Printf open CicNotationEnv open CicNotationPt -let print_attributes = true + (* 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 = false let pp_binder = function | `Lambda -> "lambda" @@ -36,68 +40,82 @@ let pp_binder = function | `Exists -> "exists" | `Forall -> "forall" -let pp_literal = function +let pp_literal = function (* debugging version *) | `Symbol s -> sprintf "symbol(%s)" s | `Keyword s -> sprintf "keyword(%s)" s | `Number s -> sprintf "number(%s)" s -let rec pp_term = function - | AttributedTerm (`Href _, term) when print_attributes -> - sprintf "#[%s]" (pp_term term) - | AttributedTerm (_, term) when print_attributes -> - sprintf "@[%s]" (pp_term term) - | AttributedTerm (_, term) -> pp_term term - - | Appl terms -> - sprintf "(%s)" (String.concat " " (List.map pp_term terms)) - | Binder (`Forall, (Ident ("_", None), typ), body) - | Binder (`Pi, (Ident ("_", None), typ), body) -> - sprintf "(%s \\to %s)" - (match typ with None -> "?" | Some typ -> pp_term typ) - (pp_term body) - | Binder (kind, var, body) -> - sprintf "\\%s %s.%s" (pp_binder kind) (pp_capture_variable var) - (pp_term body) - | Case (term, indtype, typ, patterns) -> - sprintf "%smatch %s with %s" - (match typ with None -> "" | Some t -> sprintf "<%s>" (pp_term t)) - (pp_term term) (pp_patterns patterns) - | LetIn (var, t1, t2) -> - sprintf "let %s = %s in %s" (pp_capture_variable var) (pp_term t1) - (pp_term t2) - | 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) - | Ident (name, Some []) | Ident (name, None) - | Uri (name, Some []) | Uri (name, None) -> - name - | Ident (name, Some substs) - | Uri (name, Some substs) -> - sprintf "%s \\subst [%s]" name (pp_substs substs) - | Implicit -> "?" - | Meta (index, substs) -> - sprintf "%d[%s]" index - (String.concat "; " - (List.map (function None -> "_" | Some term -> pp_term term) substs)) - | Num (num, _) -> num - | Sort `Set -> "Set" - | Sort `Prop -> "Prop" - | Sort `Type -> "Type" - | Sort `CProp -> "CProp" - | Symbol (name, _) -> name - - | UserInput -> "" - - | Literal l -> pp_literal l - | Layout l -> pp_layout l - | Magic m -> pp_magic m - | Variable v -> pp_variable v +(* let pp_literal = function + | `Symbol s + | `Keyword s + | `Number s -> s *) + +let rec pp_term ?(pp_parens = true) t = + let t_pp = + match t with + | AttributedTerm (`Href _, term) when debug_printing -> + sprintf "#[%s]" (pp_term ~pp_parens:false term) + | AttributedTerm (`IdRef id, term) when debug_printing -> + sprintf "x(%s)[%s]" id (pp_term ~pp_parens:false term) + | AttributedTerm (_, term) when debug_printing -> + sprintf "@[%s]" (pp_term ~pp_parens:false term) + | AttributedTerm (`Raw text, _) -> text + | AttributedTerm (_, term) -> pp_term ~pp_parens:false term + + | Appl terms -> + sprintf "%s" (String.concat " " (List.map pp_term terms)) + | Binder (`Forall, (Ident ("_", None), typ), body) + | Binder (`Pi, (Ident ("_", None), typ), body) -> + sprintf "%s \\to %s" + (match typ with None -> "?" | Some typ -> pp_term typ) + (pp_term body) + | Binder (kind, var, body) -> + sprintf "\\%s %s.%s" (pp_binder kind) (pp_capture_variable var) + (pp_term body) + | Case (term, indtype, typ, patterns) -> + sprintf "%smatch %s with %s" + (match typ with None -> "" | Some t -> sprintf "[%s]" (pp_term t)) + (pp_term term) (pp_patterns patterns) + | Cast (t1, t2) -> sprintf "(%s: %s)" (pp_term t1) (pp_term t2) + | LetIn (var, t1, t2) -> + sprintf "let %s = %s in %s" (pp_capture_variable var) (pp_term t1) + (pp_term t2) + | 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) + | Ident (name, Some []) | Ident (name, None) + | Uri (name, Some []) | Uri (name, None) -> + name + | Ident (name, Some substs) + | Uri (name, Some substs) -> + sprintf "%s \\subst [%s]" name (pp_substs substs) + | Implicit -> "?" + | Meta (index, substs) -> + sprintf "%d[%s]" index + (String.concat "; " + (List.map (function None -> "_" | Some t -> pp_term t) substs)) + | Num (num, _) -> num + | Sort `Set -> "Set" + | Sort `Prop -> "Prop" + | Sort `Type -> "Type" + | Sort `CProp -> "CProp" + | Symbol (name, _) -> "'" ^ name + + | UserInput -> "" + + | Literal l -> pp_literal l + | Layout l -> pp_layout l + | Magic m -> pp_magic m + | 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) @@ -141,23 +159,23 @@ and pp_layout = function | Box (box_spec, terms) -> sprintf "\\%s [%s]" (pp_box_spec box_spec) (String.concat " " (List.map pp_term terms)) + | Group terms -> + sprintf "\\GROUP [%s]" (String.concat " " (List.map pp_term terms)) and pp_magic = function - | List0 (t, sep_opt) -> - sprintf "\\LIST0 %s%s" (pp_term t) (pp_sep_opt sep_opt) - | List1 (t, sep_opt) -> - sprintf "\\LIST1 %s%s" (pp_term t) (pp_sep_opt sep_opt) - | Opt t -> sprintf "\\OPT %s" (pp_term t) - | Fold (k, p_base, names, p_rec) -> + | List0 (t, sep_opt) -> sprintf "list0 %s%s" (pp_term t) (pp_sep_opt sep_opt) + | List1 (t, sep_opt) -> sprintf "list1 %s%s" (pp_term t) (pp_sep_opt sep_opt) + | Opt t -> sprintf "opt %s" (pp_term t) + | Fold (kind, p_base, names, p_rec) -> let acc = match names with acc :: _ -> acc | _ -> assert false in - sprintf "\\FOLD %s \\[%s\\] \\LAMBDA %s \\[%s\\]" - (pp_fold_kind k) (pp_term p_base) acc (pp_term p_rec) + sprintf "fold %s %s rec %s %s" + (pp_fold_kind kind) (pp_term p_base) acc (pp_term p_rec) | Default (p_some, p_none) -> - sprintf "\\DEFAULT \\[%s\\] \\[%s\\]" (pp_term p_some) (pp_term p_none) + sprintf "default %s %s" (pp_term p_some) (pp_term p_none) | If (p_test, p_true, p_false) -> - sprintf "\\IF \\[%s\\] \\[%s\\] \\[%s\\]" + sprintf "if %s then %s else %s" (pp_term p_test) (pp_term p_true) (pp_term p_false) - | Fail -> "\\FAIL" + | Fail -> "fail" and pp_fold_kind = function | `Left -> "left" @@ -165,14 +183,16 @@ and pp_fold_kind = function and pp_sep_opt = function | None -> "" - | Some sep -> sprintf "\\SEP %s" (pp_literal sep) + | Some sep -> sprintf " sep %s" (pp_literal sep) and pp_variable = function - | NumVar s -> "\\NUM " ^ s - | IdentVar s -> "\\IDENT " ^ s - | TermVar s -> "\\TERM " ^ s - | Ascription (t, n) -> sprintf "[%s \\AS %s]" (pp_term t) n - | FreshVar n -> "\\FRESH " ^ n + | NumVar s -> "number " ^ s + | IdentVar s -> "ident " ^ s + | TermVar s -> "term " ^ s + | Ascription (t, n) -> assert false + | FreshVar n -> "fresh " ^ n + +let pp_term t = pp_term ~pp_parens:false t let rec pp_value = function | TermValue t -> sprintf "$%s$" (pp_term t)