X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fcontent%2FnotationPp.ml;h=a69ca90abe27206bc7dfbac121d3e6b73f1b03e2;hb=8bbe582d87984526f40182c4409cbfd43108cb79;hp=8828a03216bb74c64b71db833276fdd8c500d662;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git diff --git a/matitaB/components/content/notationPp.ml b/matitaB/components/content/notationPp.ml index 8828a0321..a69ca90ab 100644 --- a/matitaB/components/content/notationPp.ml +++ b/matitaB/components/content/notationPp.ml @@ -42,17 +42,17 @@ let pp_binder = function | `Exists -> "exists" | `Forall -> "forall" -let pp_literal = +(* XXX: ignoring the optional CSYMBOL + * (it's fine if this is only used for pretty printing output notations) *) +let pp_literal (_,t) = 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) + (match t with (* debugging version *) + | `Symbol _ -> + sprintf "symbol(%s)" (NotationUtil.string_of_literal t) + | `Keyword _ -> + sprintf "keyword(%s)" (NotationUtil.string_of_literal t) + | `Number _ -> sprintf "number(%s)" (NotationUtil.string_of_literal t)) + else NotationUtil.string_of_literal t let pp_pos = function @@ -70,7 +70,8 @@ let pp_attribute = (List.map (fun (_, n, v) -> sprintf "%s=%s" n v) attrs)) | `Level (prec) -> sprintf "L(%d)" prec | `Raw _ -> "R" - | `Loc _ -> "@" + | `Loc l -> let x,y = HExtlib.loc_of_floc l in + "@" ^ (string_of_int x) ^ "," ^ (string_of_int y) | `ChildPos p -> sprintf "P(%s)" (pp_pos p) let pp_capture_variable pp_term = @@ -79,21 +80,33 @@ let pp_capture_variable pp_term = | term, Some typ -> "(" ^ pp_term (* ~pp_parens:false *) term ^ ": " ^ pp_term typ ^ ")" let rec pp_term (status : #NCic.status) ?(pp_parens = true) t = + let debug_printing = true in + let pp_ident = function + | Ast.Ident (id,`Ambiguous) -> "A:" ^ id + | Ast.Ident (id,`Rel) -> "R:" ^ id + | Ast.Ident (id,`Uri u) -> ("U:(" ^ id ^ "," ^ u ^ ")") + | _ -> "E" + in let pp_term = pp_term status in 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 (`Raw text, t) -> "RAW:(" ^ (pp_term t) ^ ")" | 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) -> + | Ast.Binder (`Forall, (Ast.Ident ("_", `Ambiguous), typ), body) + | Ast.Binder (`Forall, (Ast.Ident ("_", `Rel), typ), body) + | Ast.Binder (`Pi, (Ast.Ident ("_", `Ambiguous), typ), body) + | Ast.Binder (`Pi, (Ast.Ident ("_", `Rel), 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.%s" (pp_binder kind) (pp_ident var) (pp_capture_variable pp_term var) + *) 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) -> @@ -103,7 +116,7 @@ let rec pp_term (status : #NCic.status) ?(pp_parens = true) t = | None -> "" | Some (ty, href_opt) -> sprintf " in %s%s" ty - (match debug_printing, href_opt with + (match (*debug_printing*) true, href_opt with | true, Some uri -> sprintf "(i.e.%s)" (NReference.string_of_reference uri) | _ -> "")) @@ -138,13 +151,9 @@ let rec pp_term (status : #NCic.status) ?(pp_parens = true) t = (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, _ ) -> pp_ident t | Ast.NRef nref -> NReference.string_of_reference nref | Ast.NCic cic -> status#ppterm ~metasenv:[] ~context:[] ~subst:[] cic - | Ast.Ident (name, Some substs) - | Ast.Uri (name, Some substs) -> - sprintf "%s \\subst [%s]" name (pp_substs status substs) | Ast.Implicit `Vector -> "…" | Ast.Implicit `JustOne -> "?" | Ast.Implicit (`Tagged name) -> "?"^name @@ -157,35 +166,32 @@ let rec pp_term (status : #NCic.status) ?(pp_parens = true) t = | Ast.Sort `Prop -> "Prop" | Ast.Sort (`NType s)-> "Type[" ^ s ^ "]" | Ast.Sort (`NCProp s)-> "CProp[" ^ s ^ "]" - | Ast.Symbol (name, _) -> "'" ^ name + | Ast.Symbol (name, None) -> "'" ^ name + | Ast.Symbol (name, Some (_,desc)) -> "'" ^ name ^ ":" ^ desc | Ast.UserInput -> "%" - | Ast.Literal l -> pp_literal l - | Ast.Layout l -> pp_layout status l - | Ast.Magic m -> pp_magic status m - | Ast.Variable v -> pp_variable v + | Ast.Literal l -> "literal:(" ^ (pp_literal l) ^ ")" + | Ast.Layout l -> "layout:(" ^ (pp_layout status l) ^ ")" + | Ast.Magic m -> "magic:(" ^ (pp_magic status m) ^ ")" + | Ast.Variable v -> "variable:" ^ (pp_variable v) in match pp_parens, t with | false, _ | true, Ast.Implicit _ | true, Ast.UserInput | true, Ast.Sort _ - | true, Ast.Ident (_, Some []) - | true, Ast.Ident (_, None) -> t_pp - | _ -> sprintf "(%s)" t_pp - -and pp_subst status (name, term) = - sprintf "%s \\Assign %s" name (pp_term status term) -and pp_substs status substs = String.concat "; " (List.map (pp_subst status) substs) + | true, Ast.Ident _ -> t_pp + | _ -> sprintf "(%s)" t_pp and pp_pattern status = function Ast.Pattern (head, href, vars), term -> let head_pp = head ^ - (match debug_printing, href with + (match (*debug_printing*)true, href with | true, Some uri -> sprintf "(i.e.%s)" (NReference.string_of_reference uri) + | true, None -> "(i.e.ambiguous)" | _ -> "") in sprintf "%s \\Rightarrow %s" @@ -267,7 +273,7 @@ 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 (None,sep)) and pp_variable = function | Ast.NumVar s -> "number " ^ s @@ -337,6 +343,7 @@ let rec pp_value (status: #NCic.status) = function | Env.OptValue (Some v) -> "Some " ^ pp_value status v | Env.OptValue None -> "None" | Env.ListValue l -> sprintf "[%s]" (String.concat "; " (List.map (pp_value status) l)) + | Env.DisambiguationValue _ -> sprintf "#" let rec pp_value_type = function @@ -345,6 +352,7 @@ let rec pp_value_type = | Env.NumType -> "Number" | Env.OptType t -> "Maybe " ^ pp_value_type t | Env.ListType l -> "List " ^ pp_value_type l + | Env.NoType -> "NoType" let pp_env status env = String.concat "; "