1 (*********************************************************************************************************************************)
4 (* This module is the "top level" for extraction *)
6 (*********************************************************************************************************************************)
8 Require Import Coq.Strings.Ascii.
9 Require Import Coq.Strings.String.
10 Require Import Coq.Lists.List.
12 Require Import Preamble.
13 Require Import General.
15 Require Import NaturalDeduction.
17 Require Import HaskKinds.
18 Require Import HaskLiteralsAndTyCons.
19 Require Import HaskCoreVars.
20 Require Import HaskCoreTypes.
21 Require Import HaskCore.
22 Require Import HaskWeakVars.
23 Require Import HaskWeakTypes.
24 Require Import HaskWeak.
25 Require Import HaskStrongTypes.
26 Require Import HaskStrong.
27 Require Import HaskProof.
28 Require Import HaskCoreToWeak.
29 Require Import HaskWeakToStrong.
30 Require Import HaskStrongToProof.
31 Require Import HaskProofToLatex.
32 Require Import HaskStrongToWeak.
33 Require Import HaskWeakToCore.
34 Require Import HaskProofToStrong.
36 Require Import ProgrammingLanguage.
38 Require Import HaskProofFlattener.
39 Require Import HaskProofStratified.
41 Require Import ReificationsIsomorphicToGeneralizedArrows.
43 Open Scope string_scope.
44 Extraction Language Haskell.
46 (*Extract Inductive vec => "([])" [ "([])" "(:)" ].*)
47 (*Extract Inductive Tree => "([])" [ "([])" "(:)" ].*)
48 (*Extract Inlined Constant map => "Prelude.map".*)
50 (* I try to reuse Haskell types mostly to get the "deriving Show" aspect *)
51 Extract Inductive option => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ].
52 Extract Inductive list => "([])" [ "([])" "(:)" ].
53 Extract Inductive string => "Prelude.String" [ "[]" "(:)" ].
54 Extract Inductive prod => "(,)" [ "(,)" ].
55 Extract Inductive sum => "Prelude.Either" [ "Prelude.Left" "Prelude.Right" ].
56 Extract Inductive sumbool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
57 Extract Inductive bool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
58 Extract Inductive unit => "()" [ "()" ].
59 Extract Inlined Constant string_dec => "(==)".
60 Extract Inlined Constant ascii_dec => "(==)".
62 Extract Inductive ascii => "Char" [ "you_forgot_to_patch_coq" ] "you_forgot_to_patch_coq".
63 Extract Constant zero => "'\000'".
64 Extract Constant one => "'\001'".
65 Extract Constant shift => "shiftAscii".
67 Unset Extraction Optimize.
68 Unset Extraction AutoInline.
70 Variable Name : Type. Extract Inlined Constant Name => "Name.Name".
71 Variable mkSystemName : Unique -> string -> nat -> Name.
72 Extract Inlined Constant mkSystemName =>
73 "(\u s d -> Name.mkSystemName u (OccName.mkOccName (OccName.varNameDepth (nat2int d)) s))".
74 Variable mkTyVar : Name -> Kind -> CoreVar.
75 Extract Inlined Constant mkTyVar => "(\n k -> Var.mkTyVar n (kindToCoreKind k))".
76 Variable mkCoVar : Name -> CoreType -> CoreType -> CoreVar.
77 Extract Inlined Constant mkCoVar => "(\n t1 t2 -> Var.mkCoVar n (Coercion.mkCoKind t1 t2))".
78 Variable mkExVar : Name -> CoreType -> CoreVar.
79 Extract Inlined Constant mkExVar => "Id.mkLocalId".
82 Context (ce:@CoreExpr CoreVar).
84 Definition Γ : TypeEnv := nil.
86 Definition Δ : CoercionEnv Γ := nil.
88 Definition φ : TyVarResolver Γ :=
89 fun cv => Error ("unbound tyvar: " +++ toString (cv:CoreVar)).
90 (*fun tv => error ("tried to get the representative of an unbound tyvar:" +++ (getCoreVarOccString tv)).*)
92 Definition ψ : CoVarResolver Γ Δ :=
93 fun cv => Error ("tried to get the representative of an unbound covar!" (*+++ (getTypeVarOccString cv)*)).
95 (* We need to be able to resolve unbound exprvars, but we can be sure their types will have no
96 * free tyvars in them *)
97 Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ :=
98 match coreVarToWeakVar cv with
99 | WExprVar wev => match weakTypeToTypeOfKind φ wev ★ with
100 | Error s => Prelude_error ("Error converting weakType of top-level variable "+++
101 toString cv+++": " +++ s)
104 | WTypeVar _ => Prelude_error "top-level xi got a type variable"
105 | WCoerVar _ => Prelude_error "top-level xi got a coercion variable"
109 Definition header : string :=
110 "\documentclass{article}"+++eol+++
111 "\usepackage{amsmath}"+++eol+++
112 "\usepackage{amssymb}"+++eol+++
113 "\usepackage{proof}"+++eol+++
114 (* "\usepackage{mathpartir} % http://cristal.inria.fr/~remy/latex/"+++eol+++*)
115 "\usepackage{trfrac} % http://www.utdallas.edu/~hamlen/trfrac.sty"+++eol+++
116 "\def\code#1#2{\Box_{#1} #2}"+++eol+++
117 "\usepackage[paperwidth=\maxdimen,paperheight=\maxdimen]{geometry}"+++eol+++
118 "\usepackage[tightpage,active]{preview}"+++eol+++
119 "\begin{document}"+++eol+++
120 "\setlength\PreviewBorder{5pt}"+++eol.
122 Definition footer : string :=
123 eol+++"\end{document}"+++
126 (* core-to-string (-dcoqpass) *)
127 Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string :=
128 addErrorMessage ("input CoreSyn: " +++ toString ce)
129 (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
130 coreExprToWeakExpr ce >>= fun we =>
131 addErrorMessage ("WeakExpr: " +++ toString we)
132 ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
133 ((weakTypeOfWeakExpr we) >>= fun t =>
134 (addErrorMessage ("WeakType: " +++ toString t)
135 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
136 addErrorMessage ("HaskType: " +++ toString τ)
137 ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => false) τ nil we) >>= fun e =>
138 OK (eol+++eol+++eol+++
139 "\begin{preview}"+++eol+++
141 toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ e))+++
143 "\end{preview}"+++eol+++eol+++eol)
146 Definition coreToStringExpr (ce:@CoreExpr CoreVar) : string :=
147 match coreToStringExpr' ce with
149 | Error s => Prelude_error s
152 Definition coreToStringBind (binds:@CoreBind CoreVar) : string :=
154 | CoreNonRec _ e => coreToStringExpr e
155 | CoreRec lbe => fold_left (fun x y => x+++eol+++eol+++y) (map (fun x => coreToStringExpr (snd x)) lbe) ""
158 Definition coqPassCoreToString (lbinds:list (@CoreBind CoreVar)) : string :=
160 (fold_left (fun x y => x+++eol+++eol+++y) (map coreToStringBind lbinds) "")
164 (* core-to-core (-fcoqpass) *)
167 Definition mkWeakTypeVar (u:Unique)(k:Kind) : WeakTypeVar :=
168 weakTypeVar (mkTyVar (mkSystemName u "tv" O) k) k.
169 Definition mkWeakCoerVar (u:Unique)(k:Kind)(t1 t2:WeakType) : WeakCoerVar :=
170 weakCoerVar (mkCoVar (mkSystemName u "cv" O) (weakTypeToCoreType t1) (weakTypeToCoreType t2)) k t1 t2.
171 Definition mkWeakExprVar (u:Unique)(t:WeakType) : WeakExprVar :=
172 weakExprVar (mkExVar (mkSystemName u "ev" O) (weakTypeToCoreType t)) t.
174 Context (hetmet_brak : WeakExprVar).
175 Context (hetmet_esc : WeakExprVar).
176 Context (uniqueSupply : UniqSupply).
178 Definition useUniqueSupply {T}(ut:UniqM T) : ???T :=
181 f uniqueSupply >>= fun x => OK (snd x)
184 Definition larger : forall ln:list nat, { n:nat & forall n', In n' ln -> gt n n' }.
190 destruct IHln as [n pf].
191 exists (plus (S n) a).
195 fold (@In _ n' ln) in H.
200 Definition FreshNat : @FreshMonad nat.
201 refine {| FMT := fun T => nat -> prod nat T
207 set (larger tl) as q.
208 destruct q as [n' pf].
214 refine {| returnM := fun a (v:a) => _ |}.
215 intro n. exact (n,v).
218 destruct q as [n' v].
223 Definition unFresh {T} : @FreshM _ FreshNat T -> T.
230 Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
231 addErrorMessage ("input CoreSyn: " +++ toString ce)
232 (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
233 coreExprToWeakExpr ce >>= fun we =>
234 addErrorMessage ("WeakExpr: " +++ toString we)
235 ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
236 ((weakTypeOfWeakExpr we) >>= fun t =>
237 (addErrorMessage ("WeakType: " +++ toString t)
238 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
240 ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
242 (addErrorMessage ("HaskStrong...")
243 (let haskProof := @expr2proof _ _ _ _ _ _ e
244 in (* insert HaskProof-to-HaskProof manipulations here *)
245 OK ((@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
247 (snd e') >>= fun e'' =>
248 strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
251 OK (weakExprToCoreExpr q)
254 Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) :=
255 match coreToCoreExpr' ce with
257 | Error s => Prelude_error s
260 Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
262 | CoreNonRec v e => CoreNonRec v (coreToCoreExpr e)
263 | CoreRec lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
266 Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
267 map coreToCoreBind lbinds.
271 Definition coqPassCoreToCore
272 (hetmet_brak : CoreVar)
273 (hetmet_esc : CoreVar)
274 (uniqueSupply : UniqSupply)
275 (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
276 match coreVarToWeakVar hetmet_brak with
277 | WExprVar hetmet_brak' => match coreVarToWeakVar hetmet_esc with
278 | WExprVar hetmet_esc' => coqPassCoreToCore' hetmet_brak' hetmet_esc' uniqueSupply lbinds
279 | _ => Prelude_error "IMPOSSIBLE"
281 | _ => Prelude_error "IMPOSSIBLE"