1 (*********************************************************************************************************************************)
4 (* This module is the "top level" for extraction *)
6 (*********************************************************************************************************************************)
8 (* need this or the Haskell extraction fails *)
9 Set Printing Width 1300000.
11 Require Import Coq.Strings.Ascii.
12 Require Import Coq.Strings.String.
13 Require Import Coq.Lists.List.
15 Require Import Preamble.
16 Require Import General.
18 Require Import NaturalDeduction.
19 Require Import NaturalDeductionToLatex.
21 Require Import HaskKinds.
22 Require Import HaskLiteralsAndTyCons.
23 Require Import HaskCoreVars.
24 Require Import HaskCoreTypes.
25 Require Import HaskCore.
26 Require Import HaskWeakVars.
27 Require Import HaskWeakTypes.
28 Require Import HaskWeak.
29 Require Import HaskStrongTypes.
30 Require Import HaskStrong.
31 Require Import HaskProof.
32 Require Import HaskCoreToWeak.
33 Require Import HaskWeakToStrong.
34 Require Import HaskStrongToProof.
35 Require Import HaskProofToLatex.
36 Require Import HaskStrongToWeak.
37 Require Import HaskWeakToCore.
38 Require Import HaskProofToStrong.
40 Require Import HaskProofCategory.
41 Require Import HaskStrongCategory.
42 Require Import ReificationsEquivalentToGeneralizedArrows.
44 Open Scope string_scope.
45 Extraction Language Haskell.
47 (*Extract Inductive vec => "([])" [ "([])" "(:)" ].*)
48 (*Extract Inductive Tree => "([])" [ "([])" "(:)" ].*)
49 (*Extract Inlined Constant map => "Prelude.map".*)
51 (* I try to reuse Haskell types mostly to get the "deriving Show" aspect *)
52 Extract Inductive option => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ].
53 Extract Inductive list => "([])" [ "([])" "(:)" ].
54 Extract Inductive string => "Prelude.String" [ "[]" "(:)" ].
55 Extract Inductive prod => "(,)" [ "(,)" ].
56 Extract Inductive sum => "Prelude.Either" [ "Prelude.Left" "Prelude.Right" ].
57 Extract Inductive sumbool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
58 Extract Inductive bool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
59 Extract Inductive unit => "()" [ "()" ].
60 Extract Inlined Constant string_dec => "(==)".
61 Extract Inlined Constant ascii_dec => "(==)".
63 (* adapted from ExtrOcamlString.v *)
64 Extract Inductive ascii => "Char" [ "bin2ascii" ] "bin2ascii'".
65 Extract Constant zero => "'\000'".
66 Extract Constant one => "'\001'".
67 Extract Constant shift => "shiftAscii".
69 Unset Extraction Optimize.
70 Unset Extraction AutoInline.
72 Variable Name : Type. Extract Inlined Constant Name => "Name.Name".
73 Variable mkSystemName : Unique -> string -> nat -> Name.
74 Extract Inlined Constant mkSystemName =>
75 "(\u s d -> Name.mkSystemName u (OccName.mkOccName (OccName.varNameDepth (nat2int d)) s))".
76 Variable mkTyVar : Name -> Kind -> CoreVar.
77 Extract Inlined Constant mkTyVar => "(\n k -> Var.mkTyVar n (kindToCoreKind k))".
78 Variable mkCoVar : Name -> CoreType -> CoreType -> CoreVar.
79 Extract Inlined Constant mkCoVar => "(\n t1 t2 -> Var.mkCoVar n (Coercion.mkCoKind t1 t2))".
80 Variable mkExVar : Name -> CoreType -> CoreVar.
81 Extract Inlined Constant mkExVar => "Id.mkLocalId".
84 Context (ce:@CoreExpr CoreVar).
86 Definition Γ : TypeEnv := nil.
88 Definition Δ : CoercionEnv Γ := nil.
90 Definition φ : TyVarResolver Γ :=
91 fun cv => Error ("unbound tyvar: " +++ (cv:CoreVar)).
92 (*fun tv => error ("tried to get the representative of an unbound tyvar:" +++ (getCoreVarOccString tv)).*)
94 Definition ψ : CoVarResolver Γ Δ :=
95 fun cv => Error ("tried to get the representative of an unbound covar!" (*+++ (getTypeVarOccString cv)*)).
97 (* We need to be able to resolve unbound exprvars, but we can be sure their types will have no
98 * free tyvars in them *)
99 Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ :=
100 match coreVarToWeakVar cv with
101 | WExprVar wev => match weakTypeToTypeOfKind φ wev ★ with
102 | Error s => Prelude_error ("Error in top-level xi: " +++ s)
105 | WTypeVar _ => Prelude_error "top-level xi got a type variable"
106 | WCoerVar _ => Prelude_error "top-level xi got a coercion variable"
110 (* core-to-string (-dcoqpass) *)
112 Definition header : string :=
113 "\documentclass[9pt]{article}"+++eol+++
114 "\usepackage{amsmath}"+++eol+++
115 "\usepackage{amssymb}"+++eol+++
116 "\usepackage{proof}"+++eol+++
117 "\usepackage{mathpartir} % http://cristal.inria.fr/~remy/latex/"+++eol+++
118 "\usepackage{trfrac} % http://www.utdallas.edu/~hamlen/trfrac.sty"+++eol+++
119 "\def\code#1#2{\Box_{#1} #2}"+++eol+++
120 "\usepackage[paperwidth=200in,centering]{geometry}"+++eol+++
121 "\usepackage[displaymath,tightpage,active]{preview}"+++eol+++
122 "\begin{document}"+++eol+++
123 "\begin{preview}"+++eol.
125 Definition footer : string :=
126 eol+++"\end{preview}"+++
127 eol+++"\end{document}"+++
131 Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string :=
132 addErrorMessage ("input CoreSyn: " +++ ce)
133 (addErrorMessage ("input CoreType: " +++ coreTypeOfCoreExpr ce) (
134 coreExprToWeakExpr ce >>= fun we =>
135 addErrorMessage ("WeakExpr: " +++ we)
136 ((addErrorMessage ("CoreType of WeakExpr: " +++ coreTypeOfCoreExpr (weakExprToCoreExpr we))
137 ((weakTypeOfWeakExpr we) >>= fun t =>
138 (addErrorMessage ("WeakType: " +++ t)
139 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
140 addErrorMessage ("HaskType: " +++ τ)
141 ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
142 OK (eol+++"$$"+++ nd_ml_toLatex (@expr2proof _ _ _ _ _ _ e)+++"$$"+++eol)
145 Definition coreToStringExpr (ce:@CoreExpr CoreVar) : string :=
146 match coreToStringExpr' ce with
148 | Error s => Prelude_error s
151 Definition coreToStringBind (binds:@CoreBind CoreVar) : string :=
153 | CoreNonRec _ e => coreToStringExpr e
154 | CoreRec lbe => fold_left (fun x y => x+++eol+++eol+++y) (map (fun x => coreToStringExpr (snd x)) lbe) ""
157 Definition coqPassCoreToString (lbinds:list (@CoreBind CoreVar)) : string :=
159 (fold_left (fun x y => x+++eol+++eol+++y) (map coreToStringBind lbinds) "")
163 (* core-to-core (-fcoqpass) *)
166 Definition mkWeakTypeVar (u:Unique)(k:Kind) : WeakTypeVar :=
167 weakTypeVar (mkTyVar (mkSystemName u "tv" O) k) k.
168 Definition mkWeakCoerVar (u:Unique)(k:Kind)(t1 t2:WeakType) : WeakCoerVar :=
169 weakCoerVar (mkCoVar (mkSystemName u "cv" O) (weakTypeToCoreType t1) (weakTypeToCoreType t2)) k t1 t2.
170 Definition mkWeakExprVar (u:Unique)(t:WeakType) : WeakExprVar :=
171 weakExprVar (mkExVar (mkSystemName u "ev" O) (weakTypeToCoreType t)) t.
173 Context (hetmet_brak : WeakExprVar).
174 Context (hetmet_esc : WeakExprVar).
175 Context (uniqueSupply : UniqSupply).
177 Definition useUniqueSupply {T}(ut:UniqM T) : ???T :=
180 f uniqueSupply >>= fun x => OK (snd x)
183 Definition larger : forall ln:list nat, { n:nat & forall n', In n' ln -> gt n n' }.
189 destruct IHln as [n pf].
190 exists (plus (S n) a).
194 fold (@In _ n' ln) in H.
199 Definition FreshNat : @FreshMonad nat.
200 refine {| FMT := fun T => nat -> prod nat T
206 set (larger tl) as q.
207 destruct q as [n' pf].
213 refine {| returnM := fun a (v:a) => _ |}.
214 intro n. exact (n,v).
217 destruct q as [n' v].
222 Definition unFresh {T} : @FreshM _ FreshNat T -> T.
229 Definition env := ★::nil.
230 Definition freshTV : HaskType env ★ := haskTyVarToType (FreshHaskTyVar _).
231 Definition idproof0 : ND Rule [] [env > nil > [] |- [freshTV--->freshTV @@ nil]].
237 eapply (RURule _ _ _ _ (RuCanL _ _)) .
242 Definition TInt : HaskType nil ★.
243 assert (tyConKind' intPrimTyCon = ★).
245 unfold HaskType; intros.
249 Definition idproof1 : ND Rule [] [nil > nil > [TInt @@ nil] |- [TInt @@ nil]].
255 HaskTAll(Γ:=nil) ★ (fun TV ite tv => (TApp (TApp TArrow (TVar tv)) (TVar tv))).
257 Definition idproof : ND Rule [] [nil > nil > [] |- [idtype @@ nil]].
258 eapply nd_comp; [ idtac | eapply nd_rule ; eapply RAbsT ].
263 Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
264 addErrorMessage ("input CoreSyn: " +++ ce)
265 (addErrorMessage ("input CoreType: " +++ coreTypeOfCoreExpr ce) (
266 coreExprToWeakExpr ce >>= fun we =>
267 addErrorMessage ("WeakExpr: " +++ we)
268 ((addErrorMessage ("CoreType of WeakExpr: " +++ coreTypeOfCoreExpr (weakExprToCoreExpr we))
269 ((weakTypeOfWeakExpr we) >>= fun t =>
270 (addErrorMessage ("WeakType: " +++ t)
271 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
272 addErrorMessage ("HaskType: " +++ τ)
273 ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
274 (let haskProof := @expr2proof _ _ _ _ _ _ e
275 in (* insert HaskProof-to-HaskProof manipulations here *)
276 (unFresh (@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof))
277 >>= fun e' => Error (@toString _ (ExprToString _ _ _ _) (projT2 e'))
280 Prelude_error (@toString _ (@ExprToString nat _ _ _ _ _ _) (projT2 e'))
286 strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
289 >>= fun q => Error (toString q)
294 Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
295 addErrorMessage ("input CoreSyn: " +++ ce)
296 (addErrorMessage ("input CoreType: " +++ coreTypeOfCoreExpr ce) (
297 coreExprToWeakExpr ce >>= fun we =>
298 addErrorMessage ("WeakExpr: " +++ we)
299 ((addErrorMessage ("CoreType of WeakExpr: " +++ coreTypeOfCoreExpr (weakExprToCoreExpr we))
300 ((weakTypeOfWeakExpr we) >>= fun t =>
301 (addErrorMessage ("WeakType: " +++ t)
302 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
304 ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
306 (addErrorMessage ("HaskStrong...")
307 (let haskProof := @expr2proof _ _ _ _ _ _ e
308 in (* insert HaskProof-to-HaskProof manipulations here *)
309 OK ((@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
311 (snd e') >>= fun e'' =>
312 strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
315 OK (weakExprToCoreExpr q)
318 Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) :=
319 match coreToCoreExpr' ce with
321 | Error s => Prelude_error s
324 Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
326 | CoreNonRec v e => CoreNonRec v (coreToCoreExpr e)
327 | CoreRec lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
330 Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
331 map coreToCoreBind lbinds.
335 Definition coqPassCoreToCore
336 (hetmet_brak : CoreVar)
337 (hetmet_esc : CoreVar)
338 (uniqueSupply : UniqSupply)
339 (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
340 match coreVarToWeakVar hetmet_brak with
341 | WExprVar hetmet_brak' => match coreVarToWeakVar hetmet_esc with
342 | WExprVar hetmet_esc' => coqPassCoreToCore' hetmet_brak' hetmet_esc' uniqueSupply lbinds
343 | _ => Prelude_error "IMPOSSIBLE"
345 | _ => Prelude_error "IMPOSSIBLE"
349 (*Set Extraction Optimize.*)
350 (*Set Extraction AutoInline.*)
351 Extraction "Extraction.hs" coqPassCoreToString coqPassCoreToCore.