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 HaskFlattener.
38 Open Scope string_scope.
39 Extraction Language Haskell.
41 (*Extract Inductive vec => "([])" [ "([])" "(:)" ].*)
42 (*Extract Inductive Tree => "([])" [ "([])" "(:)" ].*)
43 (*Extract Inlined Constant map => "Prelude.map".*)
45 (* I try to reuse Haskell types mostly to get the "deriving Show" aspect *)
46 Extract Inductive option => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ].
47 Extract Inductive list => "([])" [ "([])" "(:)" ].
48 Extract Inductive string => "Prelude.String" [ "[]" "(:)" ].
49 Extract Inductive prod => "(,)" [ "(,)" ].
50 Extract Inductive sum => "Prelude.Either" [ "Prelude.Left" "Prelude.Right" ].
51 Extract Inductive sumbool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
52 Extract Inductive bool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
53 Extract Inductive unit => "()" [ "()" ].
54 Extract Inlined Constant string_dec => "(==)".
55 Extract Inlined Constant ascii_dec => "(==)".
57 Extract Inductive ascii => "Char" [ "you_forgot_to_patch_coq" ] "you_forgot_to_patch_coq".
58 Extract Constant zero => "'\000'".
59 Extract Constant one => "'\001'".
60 Extract Constant shift => "shiftAscii".
62 Unset Extraction Optimize.
63 Unset Extraction AutoInline.
65 Variable Name : Type. Extract Inlined Constant Name => "Name.Name".
66 Variable mkSystemName : Unique -> string -> nat -> Name.
67 Extract Inlined Constant mkSystemName =>
68 "(\u s d -> Name.mkSystemName u (OccName.mkOccName (OccName.varNameDepth (nat2int d)) s))".
69 Variable mkTyVar : Name -> Kind -> CoreVar.
70 Extract Inlined Constant mkTyVar => "(\n k -> Var.mkTyVar n (kindToCoreKind k))".
71 Variable mkCoVar : Name -> CoreType -> CoreType -> CoreVar.
72 Extract Inlined Constant mkCoVar => "(\n t1 t2 -> Var.mkCoVar n (Coercion.mkCoKind t1 t2))".
73 Variable mkExVar : Name -> CoreType -> CoreVar.
74 Extract Inlined Constant mkExVar => "Id.mkLocalId".
77 Context (ce:@CoreExpr CoreVar).
79 Definition Γ : TypeEnv := nil.
81 Definition Δ : CoercionEnv Γ := nil.
83 Definition φ : TyVarResolver Γ :=
84 fun cv => Error ("unbound tyvar: " +++ toString (cv:CoreVar)).
85 (*fun tv => error ("tried to get the representative of an unbound tyvar:" +++ (getCoreVarOccString tv)).*)
87 Definition ψ : CoVarResolver Γ Δ :=
88 fun cv => Error ("tried to get the representative of an unbound covar!" (*+++ (getTypeVarOccString cv)*)).
90 (* We need to be able to resolve unbound exprvars, but we can be sure their types will have no
91 * free tyvars in them *)
92 Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ :=
93 match coreVarToWeakVar cv with
94 | WExprVar wev => match weakTypeToTypeOfKind φ wev ★ with
95 | Error s => Prelude_error ("Error converting weakType of top-level variable "+++
96 toString cv+++": " +++ s)
99 | WTypeVar _ => Prelude_error "top-level xi got a type variable"
100 | WCoerVar _ => Prelude_error "top-level xi got a coercion variable"
103 Definition header : string :=
104 "\documentclass{article}"+++eol+++
105 "\usepackage{amsmath}"+++eol+++
106 "\usepackage{amssymb}"+++eol+++
107 "\usepackage{proof}"+++eol+++
108 "\usepackage{trfrac} % http://www.utdallas.edu/~hamlen/trfrac.sty"+++eol+++
109 "\def\code#1#2{\Box_{#1} #2}"+++eol+++
110 "\usepackage[paperwidth=\maxdimen,paperheight=\maxdimen]{geometry}"+++eol+++
111 "\usepackage[tightpage,active]{preview}"+++eol+++
112 "\begin{document}"+++eol+++
113 "\setlength\PreviewBorder{5pt}"+++eol.
115 Definition footer : string :=
116 eol+++"\end{document}"+++
119 (* core-to-string (-dcoqpass) *)
120 Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string :=
121 addErrorMessage ("input CoreSyn: " +++ toString ce)
122 (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
123 coreExprToWeakExpr ce >>= fun we =>
124 addErrorMessage ("WeakExpr: " +++ toString we)
125 ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
126 ((weakTypeOfWeakExpr we) >>= fun t =>
127 (addErrorMessage ("WeakType: " +++ toString t)
128 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
129 addErrorMessage ("HaskType: " +++ toString τ)
130 ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => false) τ nil we) >>= fun e =>
131 OK (eol+++eol+++eol+++
132 "\begin{preview}"+++eol+++
134 toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ e))+++
136 "\end{preview}"+++eol+++eol+++eol)
139 Definition coreToStringExpr (ce:@CoreExpr CoreVar) : string :=
140 match coreToStringExpr' ce with
142 | Error s => Prelude_error s
145 Definition coreToStringBind (binds:@CoreBind CoreVar) : string :=
147 | CoreNonRec _ e => coreToStringExpr e
148 | CoreRec lbe => fold_left (fun x y => x+++eol+++eol+++y) (map (fun x => coreToStringExpr (snd x)) lbe) ""
151 Definition coqPassCoreToString (lbinds:list (@CoreBind CoreVar)) : string :=
153 (fold_left (fun x y => x+++eol+++eol+++y) (map coreToStringBind lbinds) "")
157 (* core-to-core (-fcoqpass) *)
160 Definition mkWeakTypeVar (u:Unique)(k:Kind) : WeakTypeVar :=
161 weakTypeVar (mkTyVar (mkSystemName u "tv" O) k) k.
162 Definition mkWeakCoerVar (u:Unique)(k:Kind)(t1 t2:WeakType) : WeakCoerVar :=
163 weakCoerVar (mkCoVar (mkSystemName u "cv" O) (weakTypeToCoreType t1) (weakTypeToCoreType t2)) k t1 t2.
164 Definition mkWeakExprVar (u:Unique)(t:WeakType) : WeakExprVar :=
165 weakExprVar (mkExVar (mkSystemName u "ev" O) (weakTypeToCoreType t)) t.
167 Context (hetmet_brak : WeakExprVar).
168 Context (hetmet_esc : WeakExprVar).
169 Context (hetmet_flatten : WeakExprVar).
170 Context (hetmet_unflatten : WeakExprVar).
171 Context (hetmet_flattened_id : WeakExprVar).
172 Context (uniqueSupply : UniqSupply).
174 Definition useUniqueSupply {T}(ut:UniqM T) : ???T :=
177 f uniqueSupply >>= fun x => OK (snd x)
180 Definition larger : forall ln:list nat, { n:nat & forall n', In n' ln -> gt n n' }.
186 destruct IHln as [n pf].
187 exists (plus (S n) a).
191 fold (@In _ n' ln) in H.
196 Definition FreshNat : @FreshMonad nat.
197 refine {| FMT := fun T => nat -> prod nat T
203 set (larger tl) as q.
204 destruct q as [n' pf].
210 refine {| returnM := fun a (v:a) => _ |}.
211 intro n. exact (n,v).
214 destruct q as [n' v].
219 Definition unFresh {T} : @FreshM _ FreshNat T -> T.
228 Definition coreVarToWeakExprVarOrError cv :=
229 match coreVarToWeakVar cv with
231 | _ => Prelude_error "IMPOSSIBLE"
234 Definition curry {Γ}{Δ}{a}{s}{Σ}{lev} :
236 [ Γ > Δ > Σ |- [a ---> s @@ lev ] ]
237 [ Γ > Δ > Σ,,[a @@ lev] |- [ s @@ lev ] ].
238 eapply nd_comp; [ idtac | eapply nd_rule; apply (@RApp Γ Δ Σ [a@@lev] a s lev) ].
239 eapply nd_comp; [ apply nd_rlecnac | idtac ].
246 Definition fToC1 {Γ}{Δ}{a}{s}{lev} :
247 ND Rule [] [ Γ > Δ > [ ] |- [a ---> s @@ lev ] ] ->
248 ND Rule [] [ Γ > Δ > [a @@ lev] |- [ s @@ lev ] ].
252 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
256 Definition fToC2 {Γ}{Δ}{a1}{a2}{s}{lev} :
257 ND Rule [] [ Γ > Δ > [] |- [a1 ---> (a2 ---> s) @@ lev ] ] ->
258 ND Rule [] [ Γ > Δ > [a1 @@ lev],,[a2 @@ lev] |- [ s @@ lev ] ].
272 Section coqPassCoreToCore.
274 (hetmet_brak : CoreVar)
275 (hetmet_esc : CoreVar)
276 (hetmet_flatten : CoreVar)
277 (hetmet_unflatten : CoreVar)
278 (hetmet_flattened_id : CoreVar)
279 (uniqueSupply : UniqSupply)
280 (lbinds:list (@CoreBind CoreVar))
281 (hetmet_PGArrowTyCon : TyFun)
282 (hetmet_pga_id : CoreVar)
283 (hetmet_pga_comp : CoreVar)
284 (hetmet_pga_first : CoreVar)
285 (hetmet_pga_second : CoreVar)
286 (hetmet_pga_cancell : CoreVar)
287 (hetmet_pga_cancelr : CoreVar)
288 (hetmet_pga_uncancell : CoreVar)
289 (hetmet_pga_uncancelr : CoreVar)
290 (hetmet_pga_assoc : CoreVar)
291 (hetmet_pga_unassoc : CoreVar)
292 (hetmet_pga_copy : CoreVar)
293 (hetmet_pga_drop : CoreVar)
294 (hetmet_pga_swap : CoreVar)
295 (hetmet_pga_applyl : CoreVar)
296 (hetmet_pga_applyr : CoreVar)
297 (hetmet_pga_curryl : CoreVar)
298 (hetmet_pga_curryr : CoreVar)
301 Definition ga_unit TV : RawHaskType TV ★ := @TyFunApp TV UnitTyCon nil ★ TyFunApp_nil.
302 Definition ga_prod TV (a b:RawHaskType TV ★) : RawHaskType TV ★ :=
303 TApp (TApp (@TyFunApp TV PairTyCon nil _ TyFunApp_nil) a) b.
304 Definition ga_type {TV}(a:RawHaskType TV ECKind)(b c:RawHaskType TV ★) : RawHaskType TV ★ :=
305 TApp (TApp (TApp (@TyFunApp TV
307 nil _ TyFunApp_nil) a) b) c.
308 Definition ga := @ga_mk ga_unit ga_prod (@ga_type).
310 Definition ga_type' {Γ}(a:HaskType Γ ECKind)(b c:HaskType Γ ★) : HaskType Γ ★ :=
311 fun TV ite => TApp (TApp (TApp (@TyFunApp TV
313 nil _ TyFunApp_nil) (a TV ite)) (b TV ite)) (c TV ite).
315 Definition mkGlob2' {Γ}{κ₁}{κ₂}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ ★) :
316 IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::nil) -> HaskType Γ ★.
323 Definition mkGlob2 {Γ}{Δ}{l}{κ₁}{κ₂}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ ★) x y
324 : ND Rule [] [ Γ > Δ > [] |- [f x y @@ l] ].
326 refine (@RGlobal Γ Δ l
327 {| glob_wv := coreVarToWeakExprVarOrError cv
328 ; glob_kinds := κ₁ :: κ₂ :: nil
329 ; glob_tf := mkGlob2'(Γ:=Γ) f
330 |} (ICons _ _ x (ICons _ _ y INil))).
333 Definition mkGlob3' {Γ}{κ₁}{κ₂}{κ₃}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ ★) :
334 IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::κ₃::nil) -> HaskType Γ ★.
342 Definition mkGlob3 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ ★) x y z
343 : ND Rule [] [ Γ > Δ > [] |- [f x y z @@ l] ].
345 refine (@RGlobal Γ Δ l
346 {| glob_wv := coreVarToWeakExprVarOrError cv
347 ; glob_kinds := κ₁ :: κ₂ :: κ₃ :: nil
348 ; glob_tf := mkGlob3'(Γ:=Γ) f
349 |} (ICons _ _ x (ICons _ _ y (ICons _ _ z INil)))).
352 Definition mkGlob4' {Γ}{κ₁}{κ₂}{κ₃}{κ₄}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ κ₄ -> HaskType Γ ★) :
353 IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::κ₃::κ₄::nil) -> HaskType Γ ★.
362 Definition mkGlob4 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}{κ₄}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ κ₄ -> HaskType Γ ★) x y z q
363 : ND Rule [] [ Γ > Δ > [] |- [f x y z q @@ l] ].
365 refine (@RGlobal Γ Δ l
366 {| glob_wv := coreVarToWeakExprVarOrError cv
367 ; glob_kinds := κ₁ :: κ₂ :: κ₃ :: κ₄ :: nil
368 ; glob_tf := mkGlob4'(Γ:=Γ) f
369 |} (ICons _ _ x (ICons _ _ y (ICons _ _ z (ICons _ _ q INil))))).
372 Definition gat {Γ}(x:Tree ??(HaskType Γ ★)) := @ga_mk_tree ga_unit ga_prod _ x.
374 Instance my_ga : garrow ga_unit ga_prod (@ga_type) :=
375 { ga_id := fun Γ Δ ec l a => mkGlob2 hetmet_pga_id (fun ec a => ga_type' ec a a) ec (gat a)
376 ; ga_cancelr := fun Γ Δ ec l a => mkGlob2 hetmet_pga_cancelr (fun ec a => ga_type' ec _ a) ec (gat a)
377 ; ga_cancell := fun Γ Δ ec l a => mkGlob2 hetmet_pga_cancell (fun ec a => ga_type' ec _ a) ec (gat a)
378 ; ga_uncancelr := fun Γ Δ ec l a => mkGlob2 hetmet_pga_uncancelr (fun ec a => ga_type' ec a _) ec (gat a)
379 ; ga_uncancell := fun Γ Δ ec l a => mkGlob2 hetmet_pga_uncancell (fun ec a => ga_type' ec a _) ec (gat a)
380 ; ga_assoc := fun Γ Δ ec l a b c => mkGlob4 hetmet_pga_assoc (fun ec a b c => ga_type' ec _ _) ec (gat a) (gat b) (gat c)
381 ; ga_unassoc := fun Γ Δ ec l a b c => mkGlob4 hetmet_pga_unassoc (fun ec a b c => ga_type' ec _ _) ec (gat a) (gat b) (gat c)
382 ; ga_swap := fun Γ Δ ec l a b => mkGlob3 hetmet_pga_swap (fun ec a b => ga_type' ec _ _) ec (gat a) (gat b)
383 ; ga_drop := fun Γ Δ ec l a => mkGlob2 hetmet_pga_drop (fun ec a => ga_type' ec _ _) ec (gat a)
384 ; ga_copy := fun Γ Δ ec l a => mkGlob2 hetmet_pga_copy (fun ec a => ga_type' ec _ _) ec (gat a)
385 ; ga_first := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_first (fun ec a b c => _) ec (gat a) (gat b) (gat x))
386 ; ga_second := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_second (fun ec a b c => _) ec (gat a) (gat b) (gat x))
387 ; ga_comp := fun Γ Δ ec l a b c => fToC2 (mkGlob4 hetmet_pga_comp (fun ec a b c => _) ec (gat a) (gat b) (gat c))
388 (* ; ga_lit := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_lit))*)
389 (* ; ga_curry := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_curry))*)
390 (* ; ga_apply := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_apply))*)
391 (* ; ga_kappa := fun Γ Δ ec l a => fToC1 (nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_kappa)))*)
392 ; ga_lit := fun Γ Δ ec l a => Prelude_error "ga_lit"
393 ; ga_curry := fun Γ Δ ec l a b c => Prelude_error "ga_curry"
394 ; ga_apply := fun Γ Δ ec l a b c => Prelude_error "ga_apply"
395 ; ga_kappa := fun Γ Δ ec l a => Prelude_error "ga_kappa"
398 Definition hetmet_brak' := coreVarToWeakExprVarOrError hetmet_brak.
399 Definition hetmet_esc' := coreVarToWeakExprVarOrError hetmet_esc.
400 Definition hetmet_flatten' := coreVarToWeakExprVarOrError hetmet_flatten.
401 Definition hetmet_unflatten' := coreVarToWeakExprVarOrError hetmet_unflatten.
402 Definition hetmet_flattened_id' := coreVarToWeakExprVarOrError hetmet_flattened_id.
404 Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
405 addErrorMessage ("input CoreSyn: " +++ toString ce)
406 (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
407 coreExprToWeakExpr ce >>= fun we =>
408 addErrorMessage ("WeakExpr: " +++ toString we)
409 ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
410 ((weakTypeOfWeakExpr we) >>= fun t =>
411 (addErrorMessage ("WeakType: " +++ toString t)
412 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
414 ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
416 (addErrorMessage ("HaskStrong...")
417 (let haskProof := flatten_proof hetmet_flatten' hetmet_unflatten'
418 hetmet_flattened_id' my_ga (@expr2proof _ _ _ _ _ _ e)
419 in (* insert HaskProof-to-HaskProof manipulations here *)
420 OK ((@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
422 (snd e') >>= fun e'' =>
423 strongExprToWeakExpr hetmet_brak' hetmet_esc'
424 mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
427 OK (weakExprToCoreExpr q)
430 Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) :=
431 match coreToCoreExpr' ce with
433 | Error s => Prelude_error s
436 Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
438 | CoreNonRec v e => let e' := coreToCoreExpr e in CoreNonRec (setVarType v (coreTypeOfCoreExpr e')) e'
440 | CoreRec lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
441 (* FIXME: doesn't deal with the case where top level recursive binds change type *)
443 match coreToCoreExpr (CoreELet lbe) (CoreELit HaskMachNullAddr) with
444 | CoreELet (CoreRec lbe') => lbe'
446 ("coreToCoreExpr was given a letrec, " +++
447 "but returned something that wasn't a letrec: " +++ toString x)
452 Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
453 map coreToCoreBind lbinds.
455 End coqPassCoreToCore.
457 Definition coqPassCoreToCore
458 (hetmet_brak : CoreVar)
459 (hetmet_esc : CoreVar)
460 (hetmet_flatten : CoreVar)
461 (hetmet_unflatten : CoreVar)
462 (hetmet_flattened_id : CoreVar)
463 (uniqueSupply : UniqSupply)
464 (lbinds:list (@CoreBind CoreVar))
465 (hetmet_PGArrowTyCon : TyFun)
466 (hetmet_pga_id : CoreVar)
467 (hetmet_pga_comp : CoreVar)
468 (hetmet_pga_first : CoreVar)
469 (hetmet_pga_second : CoreVar)
470 (hetmet_pga_cancell : CoreVar)
471 (hetmet_pga_cancelr : CoreVar)
472 (hetmet_pga_uncancell : CoreVar)
473 (hetmet_pga_uncancelr : CoreVar)
474 (hetmet_pga_assoc : CoreVar)
475 (hetmet_pga_unassoc : CoreVar)
476 (hetmet_pga_copy : CoreVar)
477 (hetmet_pga_drop : CoreVar)
478 (hetmet_pga_swap : CoreVar)
479 (hetmet_pga_applyl : CoreVar)
480 (hetmet_pga_applyr : CoreVar)
481 (hetmet_pga_curryl : CoreVar)
482 (hetmet_pga_curryr : CoreVar) : list (@CoreBind CoreVar) :=