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.
40 Require Import HaskProofCategory.
42 Require Import ReificationsIsomorphicToGeneralizedArrows.
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 Extract Inductive ascii => "Char" [ "you_forgot_to_patch_coq" ] "you_forgot_to_patch_coq".
64 Extract Constant zero => "'\000'".
65 Extract Constant one => "'\001'".
66 Extract Constant shift => "shiftAscii".
68 Unset Extraction Optimize.
69 Unset Extraction AutoInline.
71 Variable Name : Type. Extract Inlined Constant Name => "Name.Name".
72 Variable mkSystemName : Unique -> string -> nat -> Name.
73 Extract Inlined Constant mkSystemName =>
74 "(\u s d -> Name.mkSystemName u (OccName.mkOccName (OccName.varNameDepth (nat2int d)) s))".
75 Variable mkTyVar : Name -> Kind -> CoreVar.
76 Extract Inlined Constant mkTyVar => "(\n k -> Var.mkTyVar n (kindToCoreKind k))".
77 Variable mkCoVar : Name -> CoreType -> CoreType -> CoreVar.
78 Extract Inlined Constant mkCoVar => "(\n t1 t2 -> Var.mkCoVar n (Coercion.mkCoKind t1 t2))".
79 Variable mkExVar : Name -> CoreType -> CoreVar.
80 Extract Inlined Constant mkExVar => "Id.mkLocalId".
83 Context (ce:@CoreExpr CoreVar).
85 Definition Γ : TypeEnv := nil.
87 Definition Δ : CoercionEnv Γ := nil.
89 Definition φ : TyVarResolver Γ :=
90 fun cv => Error ("unbound tyvar: " +++ toString (cv:CoreVar)).
91 (*fun tv => error ("tried to get the representative of an unbound tyvar:" +++ (getCoreVarOccString tv)).*)
93 Definition ψ : CoVarResolver Γ Δ :=
94 fun cv => Error ("tried to get the representative of an unbound covar!" (*+++ (getTypeVarOccString cv)*)).
96 (* We need to be able to resolve unbound exprvars, but we can be sure their types will have no
97 * free tyvars in them *)
98 Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ :=
99 match coreVarToWeakVar cv with
100 | WExprVar wev => match weakTypeToTypeOfKind φ wev ★ with
101 | Error s => Prelude_error ("Error converting weakType of top-level variable "+++
102 toString cv+++": " +++ s)
105 | WTypeVar _ => Prelude_error "top-level xi got a type variable"
106 | WCoerVar _ => Prelude_error "top-level xi got a coercion variable"
110 Definition header : string :=
111 "\documentclass[9pt]{article}"+++eol+++
112 "\usepackage{amsmath}"+++eol+++
113 "\usepackage{amssymb}"+++eol+++
114 "\usepackage{proof}"+++eol+++
115 "\usepackage{mathpartir} % http://cristal.inria.fr/~remy/latex/"+++eol+++
116 "\usepackage{trfrac} % http://www.utdallas.edu/~hamlen/trfrac.sty"+++eol+++
117 "\def\code#1#2{\Box_{#1} #2}"+++eol+++
118 "\usepackage[paperwidth=200in,centering]{geometry}"+++eol+++
119 "\usepackage[displaymath,tightpage,active]{preview}"+++eol+++
120 "\begin{document}"+++eol+++
121 "\begin{preview}"+++eol.
123 Definition footer : string :=
124 eol+++"\end{preview}"+++
125 eol+++"\end{document}"+++
128 (* core-to-string (-dcoqpass) *)
129 Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string :=
130 addErrorMessage ("input CoreSyn: " +++ toString ce)
131 (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
132 coreExprToWeakExpr ce >>= fun we =>
133 addErrorMessage ("WeakExpr: " +++ toString we)
134 ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
135 ((weakTypeOfWeakExpr we) >>= fun t =>
136 (addErrorMessage ("WeakType: " +++ toString t)
137 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
138 addErrorMessage ("HaskType: " +++ toString τ)
139 ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => false) τ nil we) >>= fun e =>
140 OK (eol+++"$$"+++ toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ e))+++"$$"+++eol)
143 Definition coreToStringExpr (ce:@CoreExpr CoreVar) : string :=
144 match coreToStringExpr' ce with
146 | Error s => Prelude_error s
149 Definition coreToStringBind (binds:@CoreBind CoreVar) : string :=
151 | CoreNonRec _ e => coreToStringExpr e
152 | CoreRec lbe => fold_left (fun x y => x+++eol+++eol+++y) (map (fun x => coreToStringExpr (snd x)) lbe) ""
155 Definition coqPassCoreToString (lbinds:list (@CoreBind CoreVar)) : string :=
157 (fold_left (fun x y => x+++eol+++eol+++y) (map coreToStringBind lbinds) "")
161 (* core-to-core (-fcoqpass) *)
164 Definition mkWeakTypeVar (u:Unique)(k:Kind) : WeakTypeVar :=
165 weakTypeVar (mkTyVar (mkSystemName u "tv" O) k) k.
166 Definition mkWeakCoerVar (u:Unique)(k:Kind)(t1 t2:WeakType) : WeakCoerVar :=
167 weakCoerVar (mkCoVar (mkSystemName u "cv" O) (weakTypeToCoreType t1) (weakTypeToCoreType t2)) k t1 t2.
168 Definition mkWeakExprVar (u:Unique)(t:WeakType) : WeakExprVar :=
169 weakExprVar (mkExVar (mkSystemName u "ev" O) (weakTypeToCoreType t)) t.
171 Context (hetmet_brak : WeakExprVar).
172 Context (hetmet_esc : WeakExprVar).
173 Context (uniqueSupply : UniqSupply).
175 Definition useUniqueSupply {T}(ut:UniqM T) : ???T :=
178 f uniqueSupply >>= fun x => OK (snd x)
181 Definition larger : forall ln:list nat, { n:nat & forall n', In n' ln -> gt n n' }.
187 destruct IHln as [n pf].
188 exists (plus (S n) a).
192 fold (@In _ n' ln) in H.
197 Definition FreshNat : @FreshMonad nat.
198 refine {| FMT := fun T => nat -> prod nat T
204 set (larger tl) as q.
205 destruct q as [n' pf].
211 refine {| returnM := fun a (v:a) => _ |}.
212 intro n. exact (n,v).
215 destruct q as [n' v].
220 Definition unFresh {T} : @FreshM _ FreshNat T -> T.
227 Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
228 addErrorMessage ("input CoreSyn: " +++ toString ce)
229 (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
230 coreExprToWeakExpr ce >>= fun we =>
231 addErrorMessage ("WeakExpr: " +++ toString we)
232 ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
233 ((weakTypeOfWeakExpr we) >>= fun t =>
234 (addErrorMessage ("WeakType: " +++ toString t)
235 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
237 ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
239 (addErrorMessage ("HaskStrong...")
240 (let haskProof := @expr2proof _ _ _ _ _ _ e
241 in (* insert HaskProof-to-HaskProof manipulations here *)
242 OK ((@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
244 (snd e') >>= fun e'' =>
245 strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
248 OK (weakExprToCoreExpr q)
251 Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) :=
252 match coreToCoreExpr' ce with
254 | Error s => Prelude_error s
257 Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
259 | CoreNonRec v e => CoreNonRec v (coreToCoreExpr e)
260 | CoreRec lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
263 Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
264 map coreToCoreBind lbinds.
268 Definition coqPassCoreToCore
269 (hetmet_brak : CoreVar)
270 (hetmet_esc : CoreVar)
271 (uniqueSupply : UniqSupply)
272 (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
273 match coreVarToWeakVar hetmet_brak with
274 | WExprVar hetmet_brak' => match coreVarToWeakVar hetmet_esc with
275 | WExprVar hetmet_esc' => coqPassCoreToCore' hetmet_brak' hetmet_esc' uniqueSupply lbinds
276 | _ => Prelude_error "IMPOSSIBLE"
278 | _ => Prelude_error "IMPOSSIBLE"