X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent%2FnotationPp.ml;h=8828a03216bb74c64b71db833276fdd8c500d662;hb=894d518aa760c9f816ddb0dc2b3fa88e1fe20a94;hp=a101747df7371d46fb54a54b0d84823faa2b4eaf;hpb=8a660ee06d72cfee52c707bb1d8d8be3bab0d682;p=helm.git diff --git a/matita/components/content/notationPp.ml b/matita/components/content/notationPp.ml index a101747df..8828a0321 100644 --- a/matita/components/content/notationPp.ml +++ b/matita/components/content/notationPp.ml @@ -78,7 +78,8 @@ let pp_capture_variable pp_term = | 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 rec pp_term (status : #NCic.status) ?(pp_parens = true) t = + let pp_term = pp_term status in let t_pp = match t with | Ast.AttributedTerm (attr, term) when debug_printing -> @@ -104,10 +105,10 @@ let rec pp_term ?(pp_parens = true) t = sprintf " in %s%s" ty (match debug_printing, href_opt with | true, Some uri -> - sprintf "(i.e.%s)" (UriManager.string_of_uri uri) + sprintf "(i.e.%s)" (NReference.string_of_reference uri) | _ -> "")) (match typ with None -> "" | Some t -> sprintf " return %s" (pp_term t)) - (pp_patterns patterns) + (pp_patterns status 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 *) @@ -140,10 +141,10 @@ let rec pp_term ?(pp_parens = true) t = | Ast.Ident (name, Some []) | Ast.Ident (name, None) | Ast.Uri (name, Some []) | Ast.Uri (name, None) -> name | Ast.NRef nref -> NReference.string_of_reference nref - | Ast.NCic cic -> NCicPp.ppterm ~metasenv:[] ~context:[] ~subst:[] cic + | 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 substs) + sprintf "%s \\subst [%s]" name (pp_substs status substs) | Ast.Implicit `Vector -> "…" | Ast.Implicit `JustOne -> "?" | Ast.Implicit (`Tagged name) -> "?"^name @@ -154,8 +155,6 @@ let rec pp_term ?(pp_parens = true) t = | Ast.Num (num, _) -> num | Ast.Sort `Set -> "Set" | Ast.Sort `Prop -> "Prop" - | Ast.Sort (`Type _) -> "Type" - | Ast.Sort (`CProp _)-> "CProp" | Ast.Sort (`NType s)-> "Type[" ^ s ^ "]" | Ast.Sort (`NCProp s)-> "CProp[" ^ s ^ "]" | Ast.Symbol (name, _) -> "'" ^ name @@ -163,8 +162,8 @@ let rec pp_term ?(pp_parens = true) t = | Ast.UserInput -> "%" | Ast.Literal l -> pp_literal l - | Ast.Layout l -> pp_layout l - | Ast.Magic m -> pp_magic m + | Ast.Layout l -> pp_layout status l + | Ast.Magic m -> pp_magic status m | Ast.Variable v -> pp_variable v in match pp_parens, t with @@ -176,16 +175,17 @@ let rec pp_term ?(pp_parens = true) t = | 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_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) -and pp_pattern = +and pp_pattern status = 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) + | true, Some uri -> sprintf "(i.e.%s)" (NReference.string_of_reference uri) | _ -> "") in sprintf "%s \\Rightarrow %s" @@ -193,13 +193,13 @@ and pp_pattern = | [] -> head_pp | _ -> sprintf "(%s %s)" head_pp - (String.concat " " (List.map (pp_capture_variable pp_term) vars))) - (pp_term term) + (String.concat " " (List.map (pp_capture_variable (pp_term status)) vars))) + (pp_term status term) | Ast.Wildcard, term -> - sprintf "_ \\Rightarrow %s" (pp_term term) + sprintf "_ \\Rightarrow %s" (pp_term status term) -and pp_patterns patterns = - sprintf "[%s]" (String.concat " | " (List.map pp_pattern patterns)) +and pp_patterns status patterns = + sprintf "[%s]" (String.concat " | " (List.map (pp_pattern status) patterns)) and pp_box_spec (kind, spacing, indent) = let int_of_bool b = if b then 1 else 0 in @@ -209,7 +209,9 @@ and pp_box_spec (kind, spacing, indent) = in sprintf "%sBOX%d%d" kind_string (int_of_bool spacing) (int_of_bool indent) -and pp_layout = function +and pp_layout status = + let pp_term = pp_term status in + 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) @@ -240,7 +242,9 @@ and pp_layout = function (String.concat " " (List.map (fun (k,v) -> k^"="^v) l)) (String.concat " " (List.map pp_term terms)) -and pp_magic = function +and pp_magic status = + let pp_term = pp_term status in + function | Ast.List0 (t, sep_opt) -> sprintf "list0 %s%s" (pp_term t) (pp_sep_opt sep_opt) | Ast.List1 (t, sep_opt) -> @@ -274,24 +278,13 @@ and pp_variable = function | Ast.FreshVar n -> "fresh " ^ n let _pp_term = ref (pp_term ~pp_parens:false) -let pp_term t = !_pp_term t +let pp_term status t = !_pp_term (status :> NCic.status) 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" @@ -324,11 +317,9 @@ let pp_obj pp_term = function (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) + (NCicPp.string_of_flavour flavour) name (pp_term typ) (match body with @@ -338,13 +329,14 @@ let pp_obj pp_term = function "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 +let rec pp_value (status: #NCic.status) = function + | Env.TermValue t -> sprintf "$%s$" (pp_term status t) + | Env.StringValue (Env.Ident s) -> sprintf "\"%s\"" s + | Env.StringValue (Env.Var s) -> sprintf "\"${ident %s}\"" s | Env.NumValue n -> n - | Env.OptValue (Some v) -> "Some " ^ pp_value v + | Env.OptValue (Some v) -> "Some " ^ pp_value status v | Env.OptValue None -> "None" - | Env.ListValue l -> sprintf "[%s]" (String.concat "; " (List.map pp_value l)) + | Env.ListValue l -> sprintf "[%s]" (String.concat "; " (List.map (pp_value status) l)) let rec pp_value_type = function @@ -354,15 +346,14 @@ let rec pp_value_type = | Env.OptType t -> "Maybe " ^ pp_value_type t | Env.ListType l -> "List " ^ pp_value_type l -let pp_env env = +let pp_env status env = String.concat "; " (List.map (fun (name, (ty, value)) -> - sprintf "%s : %s = %s" name (pp_value_type ty) (pp_value value)) + sprintf "%s : %s = %s" name (pp_value_type ty) (pp_value status value)) env) let rec pp_cic_appl_pattern = function - | Ast.UriPattern uri -> UriManager.string_of_uri uri | Ast.NRefPattern nref -> NReference.string_of_reference nref | Ast.VarPattern name -> name | Ast.ImplicitPattern -> "?"