X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcontent2pres.ml;h=5d6923237e0b73ad25800f92edea881365d9f6bf;hb=6f65a2e518d723ea722b23bfd9fa0162ff8be457;hp=019538169e4669aecea0b26832a1463debaeec12;hpb=b266dce15b2f669a70daaee3bd0887f8d9c345b2;p=helm.git diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml index 019538169..5d6923237 100644 --- a/helm/ocaml/cic_transformations/content2pres.ml +++ b/helm/ocaml/cic_transformations/content2pres.ml @@ -119,26 +119,26 @@ 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])) ;; @@ -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 @@ -177,7 +177,7 @@ 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 @@ -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 @@ -246,8 +246,8 @@ and proof2pres term2pres p = 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]) @@ -258,12 +258,12 @@ and proof2pres term2pres p = 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) @@ -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 @@ -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)])]) @@ -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) @ @@ -530,7 +530,7 @@ and proof2pres term2pres p = (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 @@ -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