X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcontent2pres.ml;h=46585f14cd80c1036782f580c649f10ac5939de7;hb=43f61eedd2a1f499166de33a98af00b767dcc117;hp=019538169e4669aecea0b26832a1463debaeec12;hpb=f7b2e35a7bdadb4fdf0e640428e694703ddf67a5;p=helm.git diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml index 019538169..46585f14c 100644 --- a/helm/ocaml/cic_transformations/content2pres.ml +++ b/helm/ocaml/cic_transformations/content2pres.ml @@ -42,7 +42,7 @@ let rec split n l = let is_big_general countterm p = let maxsize = Cexpr2pres.maxsize in - let module Con = Cic2content in + let module Con = Content in let rec countp current_size p = if current_size > maxsize then current_size else @@ -62,23 +62,23 @@ let is_big_general countterm p = if current_size > maxsize then maxsize else (match e with - Con.Declaration d -> + `Declaration d -> (match d.Con.dec_name with Some s -> current_size + 4 + (String.length s) | None -> prerr_endline "NO NAME!!"; assert false) - | Con.Hypothesis h -> + | `Hypothesis h -> (match h.Con.dec_name with Some s -> current_size + 4 + (String.length s) | None -> prerr_endline "NO NAME!!"; assert false) - | Con.Proof p -> countp current_size p - | Con.Definition d -> + | `Proof p -> countp current_size p + | `Definition d -> (match d.Con.def_name with Some s -> let c1 = (current_size + 4 + (String.length s)) in (countterm c1 d.Con.def_term) | None -> prerr_endline "NO NAME!!"; assert false) - | Con.Joint ho -> maxsize + 1) (* we assume is big *) + | `Joint ho -> maxsize + 1) (* we assume is big *) and countapplycontext current_size ac = List.fold_left countp current_size ac @@ -119,31 +119,31 @@ let make_row items concl = let module P = Mpresentation in (match concl with P.Mtable _ -> (* big! *) - P.Mtable ([("align","baseline 1");("equalrows","false"); - ("columnalign","left")], + P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; + None,"columnalign","left"], [P.Mtr([],[P.Mtd ([],P.Mrow([],items))]); P.Mtr ([],[P.Mtd ([],P.indented concl)])]) | _ -> (* small *) - P.Mrow([],items@[P.Mspace([("width","0.1cm")]);concl])) + P.Mrow([],items@[P.Mspace([None,"width","0.1cm"]);concl])) ;; let make_concl verb concl = let module P = Mpresentation in (match concl with P.Mtable _ -> (* big! *) - P.Mtable ([("align","baseline 1");("equalrows","false"); - ("columnalign","left")], - [P.Mtr([],[P.Mtd ([],P.Mtext([("mathcolor","Red")],verb))]); + P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; + None,"columnalign","left"], + [P.Mtr([],[P.Mtd ([],P.Mtext([None,"mathcolor","Red"],verb))]); P.Mtr ([],[P.Mtd ([],P.indented concl)])]) | _ -> (* small *) P.Mrow([], - [P.Mtext([("mathcolor","Red")],verb); - P.Mspace([("width","0.1cm")]); + [P.Mtext([None,"mathcolor","Red"],verb); + P.Mspace([None,"width","0.1cm"]); concl])) ;; let make_args_for_apply term2pres args = - let module Con = Cic2content in + let module Con = Content in let module P = Mpresentation in let rec make_arg_for_apply is_first arg row = (match arg with @@ -157,10 +157,10 @@ let make_args_for_apply term2pres args = | Con.Term t -> if is_first then (term2pres t)::row - else P.Mspace([("width","0.1cm")])::P.Mi([],"_")::row + else P.Mspace([None,"width","0.1cm"])::P.Mi([],"_")::row | Con.ArgProof _ | Con.ArgMethod _ -> - P.Mspace([("width","0.1cm")])::P.Mi([],"_")::row) in + P.Mspace([None,"width","0.1cm"])::P.Mi([],"_")::row) in match args with hd::tl -> make_arg_for_apply true hd @@ -168,7 +168,7 @@ let make_args_for_apply term2pres args = | _ -> assert false;; let rec justification term2pres p = - let module Con = Cic2content in + let module Con = Content in let module P = Mpresentation in if ((p.Con.proof_conclude.Con.conclude_method = "Exact") or ((p.Con.proof_context = []) & @@ -177,19 +177,19 @@ let rec justification term2pres p = let pres_args = make_args_for_apply term2pres p.Con.proof_conclude.Con.conclude_args in P.Mrow([], - P.Mtext([("mathcolor","Red")],"by")::P.Mspace([("width","0.1cm")]):: + P.Mtext([None,"mathcolor","Red"],"by")::P.Mspace([None,"width","0.1cm"]):: P.Mo([],"(")::pres_args@[P.Mo([],")")]) else proof2pres term2pres p and proof2pres term2pres p = let rec proof2pres p = - let module Con = Cic2content in + let module Con = Content in let module P = Mpresentation in let indent = let is_decl e = (match e with - Con.Declaration _ - | Con.Hypothesis _ -> true + `Declaration _ + | `Hypothesis _ -> true | _ -> false) in ((List.filter is_decl p.Con.proof_context) != []) in let concl = @@ -215,11 +215,11 @@ and proof2pres term2pres p = None -> P.Mtext([],"NO PROOF!!!") | Some c -> c) in let action = - P.Maction([("actiontype","toggle")], + P.Maction([None,"actiontype","toggle"], [(make_concl "proof of" ac); body]) in - P.Mtable ([("align","baseline 1");("equalrows","false"); - ("columnalign","left")], + P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; + None,"columnalign","left"], [P.Mtr ([],[P.Mtd ([],P.Mfenced([],[P.Mtext ([],name)]))]); P.Mtr ([],[P.Mtd ([], P.indented action)])]) @@ -227,8 +227,8 @@ and proof2pres term2pres p = let module P = Mpresentation in List.fold_right (fun ce continuation -> - P.Mtable([("align","baseline 1");("equalrows","false"); - ("columnalign","left")], + P.Mtable([None,"align","baseline 1"; None,"equalrows","false"; + None,"columnalign","left"], [P.Mtr([],[P.Mtd ([],ce2pres ce)]); P.Mtr([],[P.Mtd ([], continuation)])])) c continuation @@ -239,36 +239,36 @@ and proof2pres term2pres p = and ce2pres = let module P = Mpresentation in - let module Con = Cic2content in + let module Con = Content in function - Con.Declaration d -> + `Declaration d -> (match d.Con.dec_name with Some s -> let ty = term2pres d.Con.dec_type in P.Mrow ([], - [P.Mtext([("mathcolor","Red")],"Assume"); - P.Mspace([("width","0.1cm")]); + [P.Mtext([None,"mathcolor","Red"],"Assume"); + P.Mspace([None,"width","0.1cm"]); P.Mi([],s); P.Mtext([],":"); ty]) | None -> prerr_endline "NO NAME!!"; assert false) - | Con.Hypothesis h -> + | `Hypothesis h -> (match h.Con.dec_name with Some s -> let ty = term2pres h.Con.dec_type in P.Mrow ([], - [P.Mtext([("mathcolor","Red")],"Suppose"); - P.Mspace([("width","0.1cm")]); + [P.Mtext([None,"mathcolor","Red"],"Suppose"); + P.Mspace([None,"width","0.1cm"]); P.Mtext([],"("); P.Mi ([],s); P.Mtext([],")"); - P.Mspace([("width","0.1cm")]); + P.Mspace([None,"width","0.1cm"]); ty]) | None -> prerr_endline "NO NAME!!"; assert false) - | Con.Proof p -> proof2pres p - | Con.Definition d -> + | `Proof p -> proof2pres p + | `Definition d -> (match d.Con.def_name with Some s -> let term = term2pres d.Con.def_term in @@ -279,7 +279,7 @@ and proof2pres term2pres p = term]) | None -> prerr_endline "NO NAME!!"; assert false) - | Con.Joint ho -> + | `Joint ho -> P.Mtext ([],"jointdef") and acontext2pres ac continuation indent = @@ -291,8 +291,8 @@ and proof2pres term2pres p = P.indented (proof2pres p) else proof2pres p in - P.Mtable([("align","baseline 1");("equalrows","false"); - ("columnalign","left")], + P.Mtable([None,"align","baseline 1"; None,"equalrows","false"; + None,"columnalign","left"], [P.Mtr([],[P.Mtd ([],hd)]); P.Mtr([],[P.Mtd ([], continuation)])])) ac continuation @@ -322,7 +322,7 @@ and proof2pres term2pres p = [P.Mtd ([], conclude_aux conclude)]) and conclude_aux conclude = - let module Con = Cic2content in + let module Con = Content in let module P = Mpresentation in if conclude.Con.conclude_method = "TD_Conversion" then let expected = @@ -338,7 +338,7 @@ and proof2pres term2pres p = None -> P.Mtext([],"NO SYNTH!!!") | Some c -> (term2pres c)) in P.Mtable - ([("align","baseline 1");("equalrows","false");("columnalign","left")], + ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"], [P.Mtr([],[P.Mtd([],make_concl "we must prove" expected)]); P.Mtr([],[P.Mtd([],make_concl "or equivalently" synth)]); P.Mtr([],[P.Mtd([],proof2pres subproof)])]) @@ -358,7 +358,7 @@ and proof2pres term2pres p = [Con.Term t] -> term2pres t | _ -> assert false) in make_row - [arg;P.Mspace([("width","0.1cm")]);P.Mtext([],"proves")] conclusion + [arg;P.Mspace([None,"width","0.1cm"]);P.Mtext([],"proves")] conclusion else if conclude.Con.conclude_method = "Intros+LetTac" then let conclusion = (match conclude.Con.conclude_conclusion with @@ -367,8 +367,8 @@ and proof2pres term2pres p = (match conclude.Con.conclude_args with [Con.ArgProof p] -> P.Mtable - ([("align","baseline 1");("equalrows","false"); - ("columnalign","left")], + ([None,"align","baseline 1"; None,"equalrows","false"; + None,"columnalign","left"], [P.Mtr([],[P.Mtd([],proof2pres p)]); P.Mtr([],[P.Mtd([], (make_concl "we proved *" conclusion))])]); @@ -392,14 +392,14 @@ and proof2pres term2pres p = (match conclude.Con.conclude_conclusion with None -> P.Mtext([],"NO Conclusion!!!") | Some c -> term2pres c) in - P.Mtable ([("align","baseline 1");("equalrows","false"); - ("columnalign","left")], + P.Mtable ([None,"align","baseline 1";None,"equalrows","false"; + None,"columnalign","left"], [P.Mtr ([],[P.Mtd ([],P.Mrow([],[ - P.Mtext([("mathcolor","Red")],"rewrite"); - P.Mspace([("width","0.1cm")]);term1; - P.Mspace([("width","0.1cm")]); - P.Mtext([("mathcolor","Red")],"with"); - P.Mspace([("width","0.1cm")]);term2]))]); + P.Mtext([None,"mathcolor","Red"],"rewrite"); + P.Mspace([None,"width","0.1cm"]);term1; + P.Mspace([None,"width","0.1cm"]); + P.Mtext([None,"mathcolor","Red"],"with"); + P.Mspace([None,"width","0.1cm"]);term2]))]); P.Mtr ([],[P.Mtd ([],P.indented justif)]); P.Mtr ([],[P.Mtd ([],make_concl "we proved" conclusion)])]) else if conclude.Con.conclude_method = "Apply" then @@ -407,35 +407,35 @@ and proof2pres term2pres p = make_args_for_apply term2pres conclude.Con.conclude_args in let by = P.Mrow([], - P.Mtext([("mathcolor","Red")],"by")::P.Mspace([("width","0.1cm")]):: + P.Mtext([None,"mathcolor","Red"],"by")::P.Mspace([None,"width","0.1cm"]):: P.Mo([],"(")::pres_args@[P.Mo([],")")]) in match conclude.Con.conclude_conclusion with None -> P.Mrow([],[P.Mtext([],"QUA");by]) | Some t -> let concl = (term2pres t) in let ann_concl = make_concl "we proved" concl in - P.Mtable ([("align","baseline 1");("equalrows","false"); - ("columnalign","left")], + P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; + None,"columnalign","left"], [P.Mtr ([],[P.Mtd ([],by)]); P.Mtr ([],[P.Mtd ([],ann_concl)])]) else let body = P.Mtable - ([("align","baseline 1");("equalrows","false");("columnalign","left")], + ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"], [P.Mtr ([],[P.Mtd ([],P.Mtext([],"Apply method" ^ conclude.Con.conclude_method ^ " to"))]); P.Mtr ([], [P.Mtd ([], (P.indented (P.Mtable - ([("align","baseline 1");("equalrows","false"); - ("columnalign","left")], + ([None,"align","baseline 1"; None,"equalrows","false"; + None,"columnalign","left"], args2pres conclude.Con.conclude_args))))])]) in match conclude.Con.conclude_conclusion with None -> body | Some t -> let concl = (term2pres t) in let ann_concl = make_concl "we proved" concl in - P.Mtable ([("align","baseline 1");("equalrows","false"); - ("columnalign","left")], + P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; + None,"columnalign","left"], [P.Mtr ([],[P.Mtd ([],body)]); P.Mtr ([],[P.Mtd ([],ann_concl)])]) @@ -446,7 +446,7 @@ and proof2pres term2pres p = and arg2pres = let module P = Mpresentation in - let module Con = Cic2content in + let module Con = Content in function Con.Aux n -> P.Mtext ([],"aux " ^ string_of_int n) @@ -461,7 +461,7 @@ and proof2pres term2pres p = and byinduction conclude = let module P = Mpresentation in - let module Con = Cic2content in + let module Con = Content in let proof_conclusion = (match conclude.Con.conclude_conclusion with None -> P.Mtext([],"No conclusion???") @@ -494,7 +494,7 @@ and proof2pres term2pres p = let we_proved = (make_concl "we proved" proof_conclusion) in P.Mtable - ([("align","baseline 1");("equalrows","false");("columnalign","left")], + ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"], P.Mtr ([],[P.Mtd ([],induction_on)]):: P.Mtr ([],[P.Mtd ([],to_prove)]):: (make_cases args_for_cases) @ @@ -507,7 +507,7 @@ and proof2pres term2pres p = and make_case = let module P = Mpresentation in - let module Con = Cic2content in + let module Con = Content in function Con.ArgProof p -> let name = @@ -517,20 +517,20 @@ and proof2pres term2pres p = let indhyps,args = List.partition (function - Con.Hypothesis h -> h.Con.dec_inductive + `Hypothesis h -> h.Con.dec_inductive | _ -> false) p.Con.proof_context in let pattern_aux = List.fold_right (fun e p -> let dec = (match e with - Con.Declaration h - | Con.Hypothesis h -> + `Declaration h + | `Hypothesis h -> let name = (match h.Con.dec_name with None -> "NO NAME???" | Some n ->n) in - [P.Mspace([("width","0.1cm")]); + [P.Mspace([None,"width","0.1cm"]); P.Mi ([],name); P.Mtext([],":"); (term2pres h.Con.dec_type)] @@ -538,8 +538,8 @@ and proof2pres term2pres p = dec@p) args [] in let pattern = P.Mtr ([],[P.Mtd ([],P.Mrow([], - P.Mtext([],"Case")::P.Mspace([("width","0.1cm")])::name::pattern_aux@ - [P.Mspace([("width","0.1cm")]); + P.Mtext([],"Case")::P.Mspace([None,"width","0.1cm"])::name::pattern_aux@ + [P.Mspace([None,"width","0.1cm"]); P.Mtext([],"->")]))]) in let subconcl = (match p.Con.proof_conclude.Con.conclude_conclusion with @@ -557,7 +557,7 @@ and proof2pres term2pres p = (P.Mtext([],"by induction hypothesis we know:")))]) in let make_hyp = function - Con.Hypothesis h -> + `Hypothesis h -> let name = (match h.Con.dec_name with None -> "no name" @@ -566,7 +566,7 @@ and proof2pres term2pres p = [P.Mtext([],"("); P.Mi ([],name); P.Mtext([],")"); - P.Mspace([("width","0.1cm")]); + P.Mspace([None,"width","0.1cm"]); term2pres h.Con.dec_type])) | _ -> assert false in let hyps = @@ -579,8 +579,8 @@ and proof2pres term2pres p = let body = conclude2pres p.Con.proof_conclude true in let presacontext = acontext2pres p.Con.proof_apply_context body true in - P.Mtable ([("align","baseline 1");("equalrows","false"); - ("columnalign","left")], + P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; + None,"columnalign","left"], pattern::asubconcl::induction_hypothesis@ [P.Mtr([],[P.Mtd([],presacontext)])]) | _ -> assert false in @@ -588,11 +588,43 @@ and proof2pres term2pres p = proof2pres p ;; -(* -let content2pres = - proof2pres - (function p -> Cexpr2pres.cexpr2pres_charcount (Content_expressions.acic2cexpr p)) -;; *) - +exception ToDo;; +let content2pres term2pres (id,params,metasenv,obj) = + let module Con = Content in + let module P = Mpresentation in + match obj with + `Def (Con.Const,thesis,`Proof p) -> + P.Mtable + [None,"align","baseline 1"; + None,"equalrows","false"; + None,"columnalign","left"; + None,"helm:xref","id"] + [(*P.Mtr [] + [P.Mtd [] + (P.Mrow [] + [P.Mtext [] ("UNFINISHED PROOF" ^ id ^"(" ^ params ^ ")")])] ; +*) + P.Mtr [] + [P.Mtd [] + (P.Mrow [] + [P.Mtext [] "THESIS:"])] ; + P.Mtr [] + [P.Mtd [] + (P.Mrow [] + [P.Mphantom [] + (P.Mtext [] "__") ; + term2pres thesis])] ; + P.Mtr [] + [P.Mtd [] + (P.Mrow [] + [proof2pres term2pres p])]] + | _ -> raise ToDo +;; +let content2pres ~ids_to_inner_sorts = + content2pres + (function p -> + (Cexpr2pres.cexpr2pres_charcount + (Content_expressions.acic2cexpr ids_to_inner_sorts p))) +;;