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.
16 Require Import NaturalDeductionToLatex.
18 Require Import HaskKinds.
19 Require Import HaskLiteralsAndTyCons.
20 Require Import HaskCoreVars.
21 Require Import HaskCoreTypes.
22 Require Import HaskCore.
23 Require Import HaskWeakVars.
24 Require Import HaskWeakTypes.
25 Require Import HaskWeak.
26 Require Import HaskStrongTypes.
27 Require Import HaskStrong.
28 Require Import HaskProof.
29 Require Import HaskCoreToWeak.
30 Require Import HaskWeakToStrong.
31 Require Import HaskStrongToProof.
32 Require Import HaskProofToLatex.
33 Require Import HaskStrongToWeak.
34 Require Import HaskWeakToCore.
35 Require Import HaskProofToStrong.
37 Require Import ProgrammingLanguage.
39 Require Import HaskProofCategory.
41 Require Import HaskStrongCategory.
43 Require Import ReificationsIsomorphicToGeneralizedArrows.
45 Open Scope string_scope.
46 Extraction Language Haskell.
48 (*Extract Inductive vec => "([])" [ "([])" "(:)" ].*)
49 (*Extract Inductive Tree => "([])" [ "([])" "(:)" ].*)
50 (*Extract Inlined Constant map => "Prelude.map".*)
52 (* I try to reuse Haskell types mostly to get the "deriving Show" aspect *)
53 Extract Inductive option => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ].
54 Extract Inductive list => "([])" [ "([])" "(:)" ].
55 Extract Inductive string => "Prelude.String" [ "[]" "(:)" ].
56 Extract Inductive prod => "(,)" [ "(,)" ].
57 Extract Inductive sum => "Prelude.Either" [ "Prelude.Left" "Prelude.Right" ].
58 Extract Inductive sumbool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
59 Extract Inductive bool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
60 Extract Inductive unit => "()" [ "()" ].
61 Extract Inlined Constant string_dec => "(==)".
62 Extract Inlined Constant ascii_dec => "(==)".
64 (* adapted from ExtrOcamlString.v *)
65 Extract Inductive ascii => "Char" [ "you_forgot_to_patch_coq" ] "you_forgot_to_patch_coq".
66 Extract Constant zero => "'\000'".
67 Extract Constant one => "'\001'".
68 Extract Constant shift => "shiftAscii".
70 Unset Extraction Optimize.
71 Unset Extraction AutoInline.
73 Variable Name : Type. Extract Inlined Constant Name => "Name.Name".
74 Variable mkSystemName : Unique -> string -> nat -> Name.
75 Extract Inlined Constant mkSystemName =>
76 "(\u s d -> Name.mkSystemName u (OccName.mkOccName (OccName.varNameDepth (nat2int d)) s))".
77 Variable mkTyVar : Name -> Kind -> CoreVar.
78 Extract Inlined Constant mkTyVar => "(\n k -> Var.mkTyVar n (kindToCoreKind k))".
79 Variable mkCoVar : Name -> CoreType -> CoreType -> CoreVar.
80 Extract Inlined Constant mkCoVar => "(\n t1 t2 -> Var.mkCoVar n (Coercion.mkCoKind t1 t2))".
81 Variable mkExVar : Name -> CoreType -> CoreVar.
82 Extract Inlined Constant mkExVar => "Id.mkLocalId".
85 Context (ce:@CoreExpr CoreVar).
87 Definition Γ : TypeEnv := nil.
89 Definition Δ : CoercionEnv Γ := nil.
91 Definition φ : TyVarResolver Γ :=
92 fun cv => Error ("unbound tyvar: " +++ toString (cv:CoreVar)).
93 (*fun tv => error ("tried to get the representative of an unbound tyvar:" +++ (getCoreVarOccString tv)).*)
95 Definition ψ : CoVarResolver Γ Δ :=
96 fun cv => Error ("tried to get the representative of an unbound covar!" (*+++ (getTypeVarOccString cv)*)).
98 (* We need to be able to resolve unbound exprvars, but we can be sure their types will have no
99 * free tyvars in them *)
100 Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ :=
101 match coreVarToWeakVar cv with
102 | WExprVar wev => match weakTypeToTypeOfKind φ wev ★ with
103 | Error s => Prelude_error ("Error converting weakType of top-level variable "+++
104 toString cv+++": " +++ s)
107 | WTypeVar _ => Prelude_error "top-level xi got a type variable"
108 | WCoerVar _ => Prelude_error "top-level xi got a coercion variable"
112 (* core-to-string (-dcoqpass) *)
114 Definition header : string :=
115 "\documentclass[9pt]{article}"+++eol+++
116 "\usepackage{amsmath}"+++eol+++
117 "\usepackage{amssymb}"+++eol+++
118 "\usepackage{proof}"+++eol+++
119 "\usepackage{mathpartir} % http://cristal.inria.fr/~remy/latex/"+++eol+++
120 "\usepackage{trfrac} % http://www.utdallas.edu/~hamlen/trfrac.sty"+++eol+++
121 "\def\code#1#2{\Box_{#1} #2}"+++eol+++
122 "\usepackage[paperwidth=200in,centering]{geometry}"+++eol+++
123 "\usepackage[displaymath,tightpage,active]{preview}"+++eol+++
124 "\begin{document}"+++eol+++
125 "\begin{preview}"+++eol.
127 Definition footer : string :=
128 eol+++"\end{preview}"+++
129 eol+++"\end{document}"+++
133 Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string :=
134 addErrorMessage ("input CoreSyn: " +++ toString ce)
135 (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
136 coreExprToWeakExpr ce >>= fun we =>
137 addErrorMessage ("WeakExpr: " +++ toString we)
138 ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
139 ((weakTypeOfWeakExpr we) >>= fun t =>
140 (addErrorMessage ("WeakType: " +++ toString t)
141 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
142 addErrorMessage ("HaskType: " +++ toString τ)
143 ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => false) τ nil we) >>= fun e =>
144 OK (eol+++"$$"+++ toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ e))+++"$$"+++eol)
147 Definition coreToStringExpr (ce:@CoreExpr CoreVar) : string :=
148 match coreToStringExpr' ce with
150 | Error s => Prelude_error s
153 Definition coreToStringBind (binds:@CoreBind CoreVar) : string :=
155 | CoreNonRec _ e => coreToStringExpr e
156 | CoreRec lbe => fold_left (fun x y => x+++eol+++eol+++y) (map (fun x => coreToStringExpr (snd x)) lbe) ""
159 Definition coqPassCoreToString (lbinds:list (@CoreBind CoreVar)) : string :=
161 (fold_left (fun x y => x+++eol+++eol+++y) (map coreToStringBind lbinds) "")
165 (* core-to-core (-fcoqpass) *)
168 Definition mkWeakTypeVar (u:Unique)(k:Kind) : WeakTypeVar :=
169 weakTypeVar (mkTyVar (mkSystemName u "tv" O) k) k.
170 Definition mkWeakCoerVar (u:Unique)(k:Kind)(t1 t2:WeakType) : WeakCoerVar :=
171 weakCoerVar (mkCoVar (mkSystemName u "cv" O) (weakTypeToCoreType t1) (weakTypeToCoreType t2)) k t1 t2.
172 Definition mkWeakExprVar (u:Unique)(t:WeakType) : WeakExprVar :=
173 weakExprVar (mkExVar (mkSystemName u "ev" O) (weakTypeToCoreType t)) t.
175 Context (hetmet_brak : WeakExprVar).
176 Context (hetmet_esc : WeakExprVar).
177 Context (uniqueSupply : UniqSupply).
179 Definition useUniqueSupply {T}(ut:UniqM T) : ???T :=
182 f uniqueSupply >>= fun x => OK (snd x)
185 Definition larger : forall ln:list nat, { n:nat & forall n', In n' ln -> gt n n' }.
191 destruct IHln as [n pf].
192 exists (plus (S n) a).
196 fold (@In _ n' ln) in H.
201 Definition FreshNat : @FreshMonad nat.
202 refine {| FMT := fun T => nat -> prod nat T
208 set (larger tl) as q.
209 destruct q as [n' pf].
215 refine {| returnM := fun a (v:a) => _ |}.
216 intro n. exact (n,v).
219 destruct q as [n' v].
224 Definition unFresh {T} : @FreshM _ FreshNat T -> T.
231 Definition env := ★::nil.
232 Definition freshTV : HaskType env ★ := haskTyVarToType (FreshHaskTyVar _).
233 Definition idproof0 : ND Rule [] [env > nil > [] |- [freshTV--->freshTV @@ nil]].
239 eapply (RURule _ _ _ _ (RuCanL _ _)) .
245 Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
246 addErrorMessage ("input CoreSyn: " +++ toString ce)
247 (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
248 coreExprToWeakExpr ce >>= fun we =>
249 addErrorMessage ("WeakExpr: " +++ toString we)
250 ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
251 ((weakTypeOfWeakExpr we) >>= fun t =>
252 (addErrorMessage ("WeakType: " +++ toString t)
253 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
254 addErrorMessage ("HaskType: " +++ toString τ)
255 ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
256 (let haskProof := @expr2proof _ _ _ _ _ _ e
257 in (* insert HaskProof-to-HaskProof manipulations here *)
258 (unFresh (@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof))
259 >>= fun e' => Error (@toString _ (ExprToString _ _ _ _) (projT2 e'))
262 Prelude_error (@toString _ (@ExprToString nat _ _ _ _ _ _) (projT2 e'))
268 strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
271 >>= fun q => Error (toString q)
276 Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
277 addErrorMessage ("input CoreSyn: " +++ toString ce)
278 (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
279 coreExprToWeakExpr ce >>= fun we =>
280 addErrorMessage ("WeakExpr: " +++ toString we)
281 ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
282 ((weakTypeOfWeakExpr we) >>= fun t =>
283 (addErrorMessage ("WeakType: " +++ toString t)
284 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
286 ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
288 (addErrorMessage ("HaskStrong...")
289 (let haskProof := @expr2proof _ _ _ _ _ _ e
290 in (* insert HaskProof-to-HaskProof manipulations here *)
291 OK ((@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
293 (snd e') >>= fun e'' =>
294 strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
297 OK (weakExprToCoreExpr q)
300 Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) :=
301 match coreToCoreExpr' ce with
303 | Error s => Prelude_error s
306 Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
308 | CoreNonRec v e => CoreNonRec v (coreToCoreExpr e)
309 | CoreRec lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
312 Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
313 map coreToCoreBind lbinds.
317 Definition coqPassCoreToCore
318 (hetmet_brak : CoreVar)
319 (hetmet_esc : CoreVar)
320 (uniqueSupply : UniqSupply)
321 (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
322 match coreVarToWeakVar hetmet_brak with
323 | WExprVar hetmet_brak' => match coreVarToWeakVar hetmet_esc with
324 | WExprVar hetmet_esc' => coqPassCoreToCore' hetmet_brak' hetmet_esc' uniqueSupply lbinds
325 | _ => Prelude_error "IMPOSSIBLE"
327 | _ => Prelude_error "IMPOSSIBLE"