1 (* need this or the Haskell extraction fails *)
2 Set Printing Width 1300000.
4 Require Import Coq.Lists.List.
5 Require Import Coq.Strings.Ascii.
6 Require Import Coq.Strings.String.
8 Require Import Preamble.
9 Require Import General.
11 Require Import NaturalDeduction.
12 Require Import NaturalDeductionToLatex.
14 Require Import HaskKinds.
15 Require Import HaskLiteralsAndTyCons.
16 Require Import HaskCoreVars.
17 Require Import HaskCoreTypes.
18 Require Import HaskCore.
19 Require Import HaskWeakVars.
20 Require Import HaskWeakTypes.
21 Require Import HaskWeak.
22 Require Import HaskStrongTypes.
23 Require Import HaskStrong.
24 Require Import HaskProof.
25 Require Import HaskCoreToWeak.
26 Require Import HaskWeakToStrong.
27 Require Import HaskStrongToProof.
28 (*Require Import HaskProofToStrong.*)
29 Require Import HaskProofToLatex.
30 Require Import HaskStrongToWeak.
31 Require Import HaskWeakToCore.
33 Open Scope string_scope.
34 Extraction Language Haskell.
36 (* I try to reuse Haskell types mostly to get the "deriving Show" aspect *)
37 Extract Inductive option => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ].
38 Extract Inductive list => "([])" [ "([])" "(:)" ].
39 (*Extract Inductive vec => "([])" [ "([])" "(:)" ].*)
40 (*Extract Inductive Tree => "([])" [ "([])" "(:)" ].*)
41 Extract Inlined Constant map => "Prelude.map".
42 Extract Inductive string => "Prelude.String" [ "([])" "(:)" ].
43 Extract Inductive prod => "(,)" [ "(,)" ].
44 Extract Inductive sum => "Prelude.Either" [ "Prelude.Left" "Prelude.Right" ].
45 Extract Inductive sumbool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
46 Extract Inductive bool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
47 Extract Inductive unit => "()" [ "()" ].
48 Extract Inlined Constant string_dec => "(==)".
49 Extract Inlined Constant ascii_dec => "(==)".
50 Extract Inductive string => "Prelude.String" [ "[]" "(:)" ].
52 (* adapted from ExtrOcamlString.v *)
53 Extract Inductive ascii => "Prelude.Char" [ "bin2ascii" ] "bin2ascii'".
54 Extract Constant zero => "'\000'".
55 Extract Constant one => "'\001'".
56 Extract Constant shift => "shiftAscii".
58 Unset Extraction Optimize.
59 Unset Extraction AutoInline.
62 Variable Name : Type. Extract Inlined Constant Name => "Name.Name".
63 Variable mkSystemName : Unique -> string -> nat -> Name.
64 Extract Inlined Constant mkSystemName => "(\u s d -> Name.mkSystemName u (OccName.mkOccName (OccName.varNameDepth (nat2int d)) s))".
65 Variable mkTyVar : Name -> Kind -> CoreVar.
66 Extract Inlined Constant mkTyVar => "(\n k -> Var.mkTyVar n (kindToCoreKind k))".
67 Variable mkCoVar : Name -> CoreType -> CoreType -> CoreVar.
68 Extract Inlined Constant mkCoVar => "(\n t1 t2 -> Var.mkCoVar n (Coercion.mkCoKind t1 t2))".
69 Variable mkExVar : Name -> CoreType -> CoreVar.
70 Extract Inlined Constant mkExVar => "Id.mkLocalId".
73 Context (ce:@CoreExpr CoreVar).
75 Definition Γ : TypeEnv := nil.
77 Definition Δ : CoercionEnv Γ := nil.
79 Definition φ : TyVarResolver Γ :=
80 fun cv => Error ("unbound tyvar: " +++ (cv:CoreVar)).
81 (*fun tv => error ("tried to get the representative of an unbound tyvar:" +++ (getCoreVarOccString tv)).*)
83 Definition ψ : CoVarResolver Γ Δ :=
84 fun cv => Error ("tried to get the representative of an unbound covar!" (*+++ (getTypeVarOccString cv)*)).
86 (* We need to be able to resolve unbound exprvars, but we can be sure their types will have no
87 * free tyvars in them *)
88 Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ :=
89 match coreVarToWeakVar cv with
90 | WExprVar wev => match weakTypeToTypeOfKind φ wev ★ with
91 | Error s => Prelude_error ("Error in top-level xi: " +++ s)
94 | WTypeVar _ => Prelude_error "top-level xi got a type variable"
95 | WCoerVar _ => Prelude_error "top-level xi got a coercion variable"
99 (* core-to-string (-dcoqpass) *)
101 Definition header : string :=
102 "\documentclass[9pt]{article}"+++eol+++
103 "\usepackage{amsmath}"+++eol+++
104 "\usepackage{amssymb}"+++eol+++
105 "\usepackage{proof}"+++eol+++
106 "\usepackage{mathpartir} % http://cristal.inria.fr/~remy/latex/"+++eol+++
107 "\usepackage{trfrac} % http://www.utdallas.edu/~hamlen/trfrac.sty"+++eol+++
108 "\def\code#1#2{\Box_{#1} #2}"+++eol+++
109 "\usepackage[paperwidth=200in,centering]{geometry}"+++eol+++
110 "\usepackage[displaymath,tightpage,active]{preview}"+++eol+++
111 "\begin{document}"+++eol+++
112 "\begin{preview}"+++eol.
114 Definition footer : string :=
115 eol+++"\end{preview}"+++
116 eol+++"\end{document}"+++
119 Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string :=
120 addErrorMessage ("input CoreSyn: " +++ ce)
121 (addErrorMessage ("input CoreType: " +++ coreTypeOfCoreExpr ce) (
122 coreExprToWeakExpr ce >>= fun we =>
123 addErrorMessage ("WeakExpr: " +++ we)
124 ((addErrorMessage ("CoreType of WeakExpr: " +++ coreTypeOfCoreExpr (weakExprToCoreExpr we))
125 ((weakTypeOfWeakExpr we) >>= fun t =>
126 (addErrorMessage ("WeakType: " +++ t)
127 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
128 addErrorMessage ("HaskType: " +++ τ)
129 ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
130 OK (eol+++"$$"+++ nd_ml_toLatex (@expr2proof _ _ _ _ _ _ e)+++"$$"+++eol)
133 Definition coreToStringExpr (ce:@CoreExpr CoreVar) : string :=
134 match coreToStringExpr' ce with
136 | Error s => Prelude_error s
139 Definition coreToStringBind (binds:@CoreBind CoreVar) : string :=
141 | CoreNonRec _ e => coreToStringExpr e
142 | CoreRec lbe => fold_left (fun x y => x+++eol+++eol+++y) (map (fun x => coreToStringExpr (snd x)) lbe) ""
145 Definition coqPassCoreToString (lbinds:list (@CoreBind CoreVar)) : string :=
147 (fold_left (fun x y => x+++eol+++eol+++y) (map coreToStringBind lbinds) "")
151 (* core-to-core (-fcoqpass) *)
154 Definition mkWeakTypeVar (u:Unique)(k:Kind) : WeakTypeVar :=
155 weakTypeVar (mkTyVar (mkSystemName u "tv" O) k) k.
156 Definition mkWeakCoerVar (u:Unique)(k:Kind)(t1 t2:WeakType) : WeakCoerVar :=
157 weakCoerVar (mkCoVar (mkSystemName u "cv" O) (weakTypeToCoreType t1) (weakTypeToCoreType t2)) k t1 t2.
158 Definition mkWeakExprVar (u:Unique)(t:WeakType) : WeakExprVar :=
159 weakExprVar (mkExVar (mkSystemName u "ev" O) (weakTypeToCoreType t)) t.
161 Context (hetmet_brak : WeakExprVar).
162 Context (hetmet_esc : WeakExprVar).
163 Context (uniqueSupply : UniqSupply).
165 Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
166 addErrorMessage ("input CoreSyn: " +++ ce)
167 (addErrorMessage ("input CoreType: " +++ coreTypeOfCoreExpr ce) (
168 coreExprToWeakExpr ce >>= fun we =>
169 addErrorMessage ("WeakExpr: " +++ we)
170 ((addErrorMessage ("CoreType of WeakExpr: " +++ coreTypeOfCoreExpr (weakExprToCoreExpr we))
171 ((weakTypeOfWeakExpr we) >>= fun t =>
172 (addErrorMessage ("WeakType: " +++ t)
173 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
175 ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
176 (* insert HaskStrong-to-HaskStrong manipulations here *)
177 strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply e INil
178 >>= fun q => OK (weakExprToCoreExpr q)
180 OK (weakExprToCoreExpr we)
184 Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) :=
185 match coreToCoreExpr' ce with
187 | Error s => Prelude_error s
190 Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
192 | CoreNonRec v e => CoreNonRec v (coreToCoreExpr e)
193 | CoreRec lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
196 Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
197 map coreToCoreBind lbinds.
201 Definition coqPassCoreToCore
202 (hetmet_brak : CoreVar)
203 (hetmet_esc : CoreVar)
204 (uniqueSupply : UniqSupply)
205 (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
206 match coreVarToWeakVar hetmet_brak with
207 | WExprVar hetmet_brak' => match coreVarToWeakVar hetmet_esc with
208 | WExprVar hetmet_esc' => coqPassCoreToCore' hetmet_brak' hetmet_esc' uniqueSupply lbinds
209 | _ => Prelude_error "IMPOSSIBLE"
211 | _ => Prelude_error "IMPOSSIBLE"
216 Extraction "Extraction.hs" coqPassCoreToString coqPassCoreToCore.