Require Import General.
Require Import NaturalDeduction.
-Require Import NaturalDeductionToLatex.
Require Import HaskKinds.
Require Import HaskLiteralsAndTyCons.
Require Import HaskWeakToCore.
Require Import HaskProofToStrong.
-Require Import ProgrammingLanguage.
-Require Import HaskProofCategory.
-Require Import ReificationsIsomorphicToGeneralizedArrows.
-
-(*Require Import HaskStrongCategory.*)
+(*Require Import HaskProofFlattener.*)
+(*Require Import HaskProofStratified.*)
Open Scope string_scope.
Extraction Language Haskell.
Extract Inlined Constant string_dec => "(==)".
Extract Inlined Constant ascii_dec => "(==)".
-(* adapted from ExtrOcamlString.v *)
Extract Inductive ascii => "Char" [ "you_forgot_to_patch_coq" ] "you_forgot_to_patch_coq".
Extract Constant zero => "'\000'".
Extract Constant one => "'\001'".
end.
- (* core-to-string (-dcoqpass) *)
-
Definition header : string :=
- "\documentclass[9pt]{article}"+++eol+++
+ "\documentclass{article}"+++eol+++
"\usepackage{amsmath}"+++eol+++
"\usepackage{amssymb}"+++eol+++
"\usepackage{proof}"+++eol+++
- "\usepackage{mathpartir} % http://cristal.inria.fr/~remy/latex/"+++eol+++
+(* "\usepackage{mathpartir} % http://cristal.inria.fr/~remy/latex/"+++eol+++*)
"\usepackage{trfrac} % http://www.utdallas.edu/~hamlen/trfrac.sty"+++eol+++
"\def\code#1#2{\Box_{#1} #2}"+++eol+++
- "\usepackage[paperwidth=200in,centering]{geometry}"+++eol+++
- "\usepackage[displaymath,tightpage,active]{preview}"+++eol+++
+ "\usepackage[paperwidth=\maxdimen,paperheight=\maxdimen]{geometry}"+++eol+++
+ "\usepackage[tightpage,active]{preview}"+++eol+++
"\begin{document}"+++eol+++
- "\begin{preview}"+++eol.
+ "\setlength\PreviewBorder{5pt}"+++eol.
Definition footer : string :=
- eol+++"\end{preview}"+++
eol+++"\end{document}"+++
eol.
-
+ (* core-to-string (-dcoqpass) *)
Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string :=
addErrorMessage ("input CoreSyn: " +++ toString ce)
(addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
addErrorMessage ("HaskType: " +++ toString τ)
((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => false) τ nil we) >>= fun e =>
- OK (eol+++"$$"+++ toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ e))+++"$$"+++eol)
+ OK (eol+++eol+++eol+++
+ "\begin{preview}"+++eol+++
+ "$\displaystyle "+++
+ toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ e))+++
+ " $"+++eol+++
+ "\end{preview}"+++eol+++eol+++eol)
)))))))).
Definition coreToStringExpr (ce:@CoreExpr CoreVar) : string :=
apply t.
Defined.
-(*
- Definition env := ★::nil.
- Definition freshTV : HaskType env ★ := haskTyVarToType (FreshHaskTyVar _).
- Definition idproof0 : ND Rule [] [env > nil > [] |- [freshTV--->freshTV @@ nil]].
- eapply nd_comp.
- eapply nd_comp.
- eapply nd_rule.
- apply RVar.
- eapply nd_rule
- eapply (RArrange _ _ _ _ (RuCanL _ _)) .
- eapply nd_rule.
- eapply RLam.
- Defined.
-
-
- Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
- addErrorMessage ("input CoreSyn: " +++ toString ce)
- (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
- coreExprToWeakExpr ce >>= fun we =>
- addErrorMessage ("WeakExpr: " +++ toString we)
- ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
- ((weakTypeOfWeakExpr we) >>= fun t =>
- (addErrorMessage ("WeakType: " +++ toString t)
- ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
- addErrorMessage ("HaskType: " +++ toString τ)
- ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
- (let haskProof := @expr2proof _ _ _ _ _ _ e
- in (* insert HaskProof-to-HaskProof manipulations here *)
- (unFresh (@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof))
- >>= fun e' => Error (@toString _ (ExprToString _ _ _ _) (projT2 e'))
-(*
- >>= fun e' =>
- Prelude_error (@toString _ (@ExprToString nat _ _ _ _ _ _) (projT2 e'))
- *)
-)
-)))))))).
-(* Error "X").*)
-(*
- strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
- (projT2 e')
- INil
- >>= fun q => Error (toString q)
- ))))))))).
-*)*)
-
-
Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
addErrorMessage ("input CoreSyn: " +++ toString ce)
(addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (