X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcontent2pres.ml;h=ef79ab4ad254aebac239a96dbf31f83281565e59;hb=7e9904185ceff75884783dbf0bad506b8521b857;hp=a2a010f7d0e925b812ed368e05e99d06b0320a90;hpb=9ab5ca8acba80b19a939eea2cd87761507e7128b;p=helm.git diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml index a2a010f7d..ef79ab4ad 100644 --- a/helm/ocaml/cic_transformations/content2pres.ml +++ b/helm/ocaml/cic_transformations/content2pres.ml @@ -53,7 +53,7 @@ let rec split n l = let is_big_general countterm p = - let maxsize = Cexpr2pres.maxsize in + let maxsize = Ast2pres.maxsize in let module Con = Content in let rec countp current_size p = if current_size > maxsize then current_size @@ -126,7 +126,7 @@ let is_big_general countterm p = (size > maxsize) ;; -let is_big = is_big_general (Cexpr2pres.countterm) +let is_big = is_big_general (Ast2pres.countterm) ;; let get_xref = @@ -186,6 +186,10 @@ let make_args_for_apply term2pres args = | _ -> assert false ;; +let get_name = function + | Some s -> s + | None -> "_" + let rec justification term2pres p = let module Con = Content in let module P = Mpresentation in @@ -758,86 +762,165 @@ proof2pres p exception ToDo;; -let aaa = ref 0 +let counter = ref 0 + +let conjecture2pres term2pres (id, n, context, ty) = + (B.b_h [Some "helm", "xref", id] + (((List.map + (function + | None -> + B.b_h [] + [ B.b_object (p_mi [] "_") ; + B.b_object (p_mo [] ":?") ; + B.b_object (p_mi [] "_")] + | Some (`Declaration d) + | Some (`Hypothesis d) -> + let { Content.dec_name = + dec_name ; Content.dec_type = ty } = d + in + B.b_h [] + [ B.b_object + (p_mi [] + (match dec_name with + None -> "_" + | Some n -> n)); + B.b_text [] ":"; + term2pres ty ] + | Some (`Definition d) -> + let + { Content.def_name = def_name ; + Content.def_term = bo } = d + in + B.b_h [] + [ B.b_object (p_mi [] + (match def_name with + None -> "_" + | Some n -> n)) ; + B.b_text [] ":=" ; + term2pres bo] + | Some (`Proof p) -> + let proof_name = p.Content.proof_name in + B.b_h [] + [ B.b_object (p_mi [] + (match proof_name with + None -> "_" + | Some n -> n)) ; + B.b_text [] ":=" ; + proof2pres term2pres p]) + (List.rev context)) @ + [ B.b_text [] "|-" ; + B.b_object (p_mi [] (string_of_int n)) ; + B.b_text [] ":" ; + term2pres ty ]))) + +let metasenv2pres term2pres = function + | None -> [] + | Some metasenv' -> + (* Conjectures are in their own table to make *) + (* diffing the DOM trees easier. *) + [B.b_v [] + ((B.b_text [] + ("Conjectures:" ^ + (let _ = incr counter; in (string_of_int !counter)))) :: + (List.map (conjecture2pres term2pres) metasenv'))] + +let params2pres params = + let param2pres uri = + B.b_text [Some "xlink", "href", UriManager.string_of_uri uri] + (UriManager.name_of_uri uri) + in + let rec spatiate = function + | [] -> [] + | hd :: [] -> [hd] + | hd :: tl -> hd :: B.b_text [] ", " :: spatiate tl + in + match params with + | [] -> [] + | p -> + let params = spatiate (List.map param2pres p) in + [B.b_space; + B.b_h [] (B.b_text [] "[" :: params @ [ B.b_text [] "]" ])] + +let recursion_kind2pres params kind = + let kind = + match kind with + | `Recursive _ -> "Recursive definition" + | `CoRecursive -> "CoRecursive definition" + | `Inductive _ -> "Inductive definition" + | `CoInductive _ -> "CoInductive definition" + in + B.b_h [] (B.b_text [] kind :: params2pres params) + +let inductive2pres term2pres ind = + let constructor2pres decl = + B.b_h [] [ + B.b_text [] ("| " ^ get_name decl.Content.dec_name ^ ":"); + B.b_space; + term2pres decl.Content.dec_type + ] + in + B.b_v [] + (B.b_h [] [ + B.b_text [] (ind.Content.inductive_name ^ " of arity "); + term2pres ind.Content.inductive_type ] + :: List.map constructor2pres ind.Content.inductive_constructors) + +let joint_def2pres term2pres def = + match def with + | `Inductive ind -> inductive2pres term2pres ind + | _ -> assert false (* ZACK or raise ToDo? *) let content2pres term2pres (id,params,metasenv,obj) = - let module K = Content in - match obj with - `Def (K.Const,thesis,`Proof p) -> - B.b_v - [None,"helm:xref","id"] - ([B.b_text [] ("UNFINISHED PROOF " ^ id ^"(" ^ String.concat " ; " (List.map UriManager.string_of_uri params)^ ")") ; - B.b_text [] "THESIS:" ; - B.indent (term2pres thesis)] @ - (match metasenv with - None -> [] - | Some metasenv' -> - (* Conjectures are in their own table to make *) - (* diffing the DOM trees easier. *) - (B.b_v [] - ((B.b_text [] ("CONJECTURES:" ^ (let _ = incr aaa; in (string_of_int !aaa)))):: - (List.map - (function - (id,n,context,ty) -> - (B.b_h [Some "helm", "xref", id] - (((List.map - (function - None -> - B.b_h [] - [ B.b_object (p_mi [] "_") ; - B.b_object (p_mo [] ":?") ; - B.b_object (p_mi [] "_")] - | Some (`Declaration d) - | Some (`Hypothesis d) -> - let - { K.dec_name = dec_name ; - K.dec_type = ty } = d - in - B.b_h [] - [ B.b_object (p_mi [] - (match dec_name with - None -> "_" - | Some n -> n)) ; - B.b_text [] ":" ; - term2pres ty] - | Some (`Definition d) -> - let - { K.def_name = def_name ; - K.def_term = bo } = d - in - B.b_h [] - [ B.b_object (p_mi [] - (match def_name with - None -> "_" - | Some n -> n)) ; - B.b_text [] ":=" ; - term2pres bo] - | Some (`Proof p) -> - let proof_name = p.K.proof_name in - B.b_h [] - [ B.b_object (p_mi [] - (match proof_name with - None -> "_" - | Some n -> n)) ; - B.b_text [] ":=" ; - proof2pres term2pres p] - ) (List.rev context)) @ - [ B.b_text [] "|-" ; - B.b_object (p_mi [] (string_of_int n)) ; - B.b_text [] ":" ; - term2pres ty ]) - )) - ) metasenv')) - )::[proof2pres term2pres p] - ) - ) - | _ -> raise ToDo + match obj with + | `Def (Content.Const, thesis, `Proof p) -> + let name = get_name p.Content.proof_name in + B.b_v + [Some "helm","xref","id"] + ([ B.b_h [] (B.b_text [] ("Proof " ^ name) :: params2pres params); + B.b_text [] "Thesis:"; + B.indent (term2pres thesis) ] @ + metasenv2pres term2pres metasenv @ + [proof2pres term2pres p]) + | `Def (_, ty, `Definition body) -> + let name = get_name body.Content.def_name in + B.b_v + [Some "helm","xref","id"] + ([B.b_h [] (B.b_text [] ("Definition " ^ name) :: params2pres params); + B.b_text [] "Type:"; + B.indent (term2pres ty)] @ + metasenv2pres term2pres metasenv @ + [term2pres body.Content.def_term]) + | `Decl (_, `Declaration decl) + | `Decl (_, `Hypothesis decl) -> + let name = get_name decl.Content.dec_name in + B.b_v + [Some "helm","xref","id"] + ([B.b_h [] (B.b_text [] ("Axiom " ^ name) :: params2pres params); + B.b_text [] "Type:"; + B.indent (term2pres decl.Content.dec_type)] @ + metasenv2pres term2pres metasenv) + | `Joint joint -> + B.b_v [] + (recursion_kind2pres params joint.Content.joint_kind + :: List.map (joint_def2pres term2pres) joint.Content.joint_defs) + | _ -> raise ToDo ;; +(* let content2pres ~ids_to_inner_sorts = content2pres (function p -> (Cexpr2pres.cexpr2pres_charcount (Content_expressions.acic2cexpr ids_to_inner_sorts p))) ;; +*) + +let content2pres ~ids_to_inner_sorts = + content2pres + (fun annterm -> + let (ast, ids_to_uris) as arg = + Acic2Ast.ast_of_acic ids_to_inner_sorts annterm + in + let astBox = Ast2pres.ast2astBox arg in + Box.map (fun ast -> Ast2pres.ast2mpres (ast, ids_to_uris)) astBox)