X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Facic_content%2FcicNotationPp.ml;h=49cefaec7db3f7f76652d9e24e9543bd4de9f495;hb=c4ca5dc437886c8a2cf0e34a5fbb17cdb1f4353b;hp=590de7c5462f4fe5b097113f19ff20133da23a5d;hpb=4cdf45f08cd95641a094312ddc558320b874fa16;p=helm.git diff --git a/components/acic_content/cicNotationPp.ml b/components/acic_content/cicNotationPp.ml index 590de7c54..49cefaec7 100644 --- a/components/acic_content/cicNotationPp.ml +++ b/components/acic_content/cicNotationPp.ml @@ -92,13 +92,12 @@ let rec pp_term ?(pp_parens = true) t = | Ast.Binder (`Pi, (Ast.Ident ("_", None), typ), body) -> sprintf "%s \\to %s" (match typ with None -> "?" | Some typ -> pp_term typ) - (pp_term body) + (pp_term ~pp_parens:true body) | Ast.Binder (kind, var, body) -> sprintf "\\%s %s.%s" (pp_binder kind) (pp_capture_variable var) - (pp_term body) + (pp_term ~pp_parens:true body) | Ast.Case (term, indtype, typ, patterns) -> - sprintf "%smatch %s%s with %s" - (match typ with None -> "" | Some t -> sprintf "[%s]" (pp_term t)) + sprintf "match %s%s%s with %s" (pp_term term) (match indtype with | None -> "" @@ -107,20 +106,43 @@ let rec pp_term ?(pp_parens = true) t = (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 t1) (pp_term t2) + | Ast.Cast (t1, t2) -> sprintf "(%s: %s)" (pp_term ~pp_parens:true t1) (pp_term ~pp_parens:true t2) | Ast.LetIn (var, t1, t2) -> - sprintf "let %s = %s in %s" (pp_capture_variable var) (pp_term t1) - (pp_term t2) + sprintf "let %s \\def %s in %s" (pp_capture_variable var) (pp_term ~pp_parens:true t1) + (pp_term ~pp_parens:true t2) | Ast.LetRec (kind, definitions, term) -> - sprintf "let %s %s in %s" + let strip i t = + let rec aux i l = function + | Ast.Binder (_, var, body) when i > 0 -> aux (pred i) (var :: l) body + | body -> List.rev l, body + in + aux i [] t + in + let rec get_guard i = function + | [] -> assert false + | [term, _] when i = 1 -> term + | _ :: tl -> get_guard (pred i) tl + in + let map (var, body, i) = + let id, vars, typ, body = match var with + | term, Some typ -> + let pvars, pbody = strip i typ in + let _, bbody = strip i body in + term, pvars, pbody, bbody + | _ -> assert false + in + sprintf "%s %s on %s: %s \\def %s" + (pp_term ~pp_parens:false term) + (String.concat " " (List.map pp_capture_variable vars)) + (pp_term ~pp_parens:false (get_guard i vars)) + (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 - (fun (var, body, _) -> - sprintf "%s = %s" (pp_capture_variable var) (pp_term body)) - definitions)) + (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) -> @@ -147,8 +169,13 @@ let rec pp_term ?(pp_parens = true) t = | Ast.Magic m -> pp_magic m | Ast.Variable v -> pp_variable v in - if pp_parens then sprintf "(%s)" t_pp - else t_pp + 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) @@ -172,13 +199,9 @@ and pp_patterns patterns = sprintf "[%s]" (String.concat " | " (List.map pp_pattern patterns)) and pp_capture_variable = - let clean s = - let s = String.sub s 1 (String.length s - 1) in - String.sub s 0 (String.length s - 1) - in function - | term, None -> pp_term term - | term, Some typ -> "(" ^ clean (pp_term term) ^ ": " ^ pp_term typ ^ ")" + | term, None -> pp_term ~pp_parens:false term + | term, Some typ -> "(" ^ pp_term ~pp_parens:false term ^ ": " ^ pp_term typ ^ ")" and pp_box_spec (kind, spacing, indent) = let int_of_bool b = if b then 1 else 0 in @@ -239,7 +262,9 @@ and pp_variable = function | Ast.Ascription (t, n) -> assert false | Ast.FreshVar n -> "fresh " ^ n -let pp_term t = pp_term ~pp_parens:false t +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 = function | [] -> "" @@ -251,20 +276,24 @@ let pp_params = function params) let pp_flavour = function - | `Definition -> "Definition" + | `Definition -> "definition" | `Fact -> "fact" | `Goal -> "goal" | `Lemma -> "lemma" | `Remark -> "remark" | `Theorem -> "theorem" | `Variant -> "variant" + | `Axiom -> "axiom" let pp_fields fields = (if fields <> [] then "\n" else "") ^ String.concat ";\n" (List.map - (fun (name,ty,coercion) -> - " " ^ name ^ if coercion then ":>" else ": " ^ pp_term ty) fields) + (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 = function | Ast.Inductive (params, types) -> @@ -287,16 +316,16 @@ let pp_obj = function in fst_typ_pp ^ String.concat "" (List.map pp_type tl)) | Ast.Theorem (flavour, name, typ, body) -> - sprintf "%s %s: %s %s" + sprintf "%s %s:\n %s\n%s" (pp_flavour flavour) name (pp_term typ) (match body with | None -> "" - | Some body -> "\\def " ^ pp_term body) + | Some body -> "\\def\n " ^ pp_term body) | Ast.Record (params,name,ty,fields) -> - "record " ^ name ^ " " ^ pp_params params ^ " \\def {" ^ - pp_fields fields ^ "}" + "record " ^ name ^ " " ^ pp_params params ^ ": " ^ pp_term ty ^ + " \\def {" ^ pp_fields fields ^ "\n}" let rec pp_value = function | Env.TermValue t -> sprintf "$%s$" (pp_term t)