X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcontent2pres.ml;h=1429826479f0cd5f87f6f715ca931eeab8e09aa9;hb=bbe7741f3bbaacb93f2876c018dace82f5e929b8;hp=29da14591e9fd6946f1e0062412ece9457985288;hpb=e5f4d8fa36a154bbc0a555eefa5ccc0bdb29afb0;p=helm.git diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml index 29da14591..142982647 100644 --- a/helm/ocaml/cic_transformations/content2pres.ml +++ b/helm/ocaml/cic_transformations/content2pres.ml @@ -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 @@ -250,17 +254,33 @@ and proof2pres term2pres p = (fun ce continuation -> let xref = get_xref ce in B.V([Some "helm", "xref", xref ], - [B.H([Some "helm", "xref", "ce_"^xref],[ce2pres ce]); + [B.H([Some "helm", "xref", "ce_"^xref], + [ce2pres_in_proof_context_element ce]); continuation])) tl continuation in let hd_xref= get_xref hd in B.V([], [B.H([Some "helm", "xref", "ce_"^hd_xref], - [ce2pres hd]); + [ce2pres_in_proof_context_element hd]); continuation']) - - and ce2pres = + + and ce2pres_in_joint_context_element = function + | `Inductive _ -> assert false (* TODO *) + | (`Declaration _) as x -> ce2pres x + | (`Hypothesis _) as x -> ce2pres x + | (`Proof _) as x -> ce2pres x + | (`Definition _) as x -> ce2pres x + + and ce2pres_in_proof_context_element = function + | `Joint ho -> + B.H ([],(List.map ce2pres_in_joint_context_element ho.Content.joint_defs)) + | (`Declaration _) as x -> ce2pres x + | (`Hypothesis _) as x -> ce2pres x + | (`Proof _) as x -> ce2pres x + | (`Definition _) as x -> ce2pres x + + and ce2pres = let module Con = Content in - function + function `Declaration d -> (match d.Con.dec_name with Some s -> @@ -300,8 +320,6 @@ and proof2pres term2pres p = term]) | None -> prerr_endline "NO NAME!!"; assert false) - | `Joint ho -> - B.Text ([],"jointdef") and acontext2pres ac continuation indent = let module Con = Content in @@ -376,7 +394,11 @@ and proof2pres term2pres p = let arg = (match conclude.Con.conclude_args with [Con.Term t] -> term2pres t - | _ -> assert false) in + | [Con.Premise p] -> + (match p.Con.premise_binder with + | None -> assert false; (* unnamed hypothesis ??? *) + | Some s -> B.Text([],s)) + | err -> assert false) in (match conclude.Con.conclude_conclusion with None -> B.b_h [] [B.b_kw "Consider"; B.b_space; arg] @@ -495,7 +517,7 @@ and proof2pres term2pres p = B.Text ([],"a proof???") | Con.ArgMethod s -> B.Text ([],"a method???")) in - (make_concl "we proceede by cases on" case_arg) in + (make_concl "we proceed by cases on" case_arg) in let to_prove = (make_concl "to prove" proof_conclusion) in B.V @@ -531,7 +553,7 @@ and proof2pres term2pres p = B.Text ([],"a proof???") | Con.ArgMethod s -> B.Text ([],"a method???")) in - (make_concl "we proceede by induction on" arg) in + (make_concl "we proceed by induction on" arg) in let to_prove = (make_concl "to prove" proof_conclusion) in B.V @@ -820,24 +842,59 @@ let metasenv2pres term2pres = function (let _ = incr counter; in (string_of_int !counter)))) :: (List.map (conjecture2pres term2pres) metasenv'))] -let get_name = function - | Some s -> s - | None -> "_" +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 pp_params = function - | [] -> "" - | params -> - " (" ^ - String.concat " ; " (List.map UriManager.string_of_uri params) ^ - ")" +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) = match obj with | `Def (Content.Const, thesis, `Proof p) -> let name = get_name p.Content.proof_name in B.b_v - [None,"helm:xref","id"] - ([ B.b_text [] ("Proof " ^ name ^ pp_params params); + [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 @ @@ -845,8 +902,8 @@ let content2pres term2pres (id,params,metasenv,obj) = | `Def (_, ty, `Definition body) -> let name = get_name body.Content.def_name in B.b_v - [None,"helm:xref","id"] - ([B.b_text [] ("Definition " ^ name ^ pp_params params); + [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 @ @@ -855,11 +912,15 @@ let content2pres term2pres (id,params,metasenv,obj) = | `Decl (_, `Hypothesis decl) -> let name = get_name decl.Content.dec_name in B.b_v - [None,"helm:xref","id"] - ([B.b_text [] ("Axiom " ^ name ^ pp_params params); + [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 ;;