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{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=\maxdimen,paperheight=\maxdimen]{geometry}"+++eol+++
119 "\usepackage[tightpage,active]{preview}"+++eol+++
120 "\begin{document}"+++eol+++
121 "\setlength\PreviewBorder{5pt}"+++eol+++.
123 Definition footer : string :=
124 eol+++"\end{document}"+++
127 (* core-to-string (-dcoqpass) *)
128 Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string :=
129 addErrorMessage ("input CoreSyn: " +++ toString ce)
130 (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
131 coreExprToWeakExpr ce >>= fun we =>
132 addErrorMessage ("WeakExpr: " +++ toString we)
133 ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
134 ((weakTypeOfWeakExpr we) >>= fun t =>
135 (addErrorMessage ("WeakType: " +++ toString t)
136 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
137 addErrorMessage ("HaskType: " +++ toString τ)
138 ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => false) τ nil we) >>= fun e =>
139 OK (eol+++eol+++eol+++
140 "\begin{preview}"+++eol
142 toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ e))+++
144 "\end{preview}"+++eol+++eol+++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 coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
232 addErrorMessage ("input CoreSyn: " +++ toString ce)
233 (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
234 coreExprToWeakExpr ce >>= fun we =>
235 addErrorMessage ("WeakExpr: " +++ toString we)
236 ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
237 ((weakTypeOfWeakExpr we) >>= fun t =>
238 (addErrorMessage ("WeakType: " +++ toString t)
239 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
241 ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
243 (addErrorMessage ("HaskStrong...")
244 (let haskProof := @expr2proof _ _ _ _ _ _ e
245 in (* insert HaskProof-to-HaskProof manipulations here *)
246 OK ((@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
248 (snd e') >>= fun e'' =>
249 strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
252 OK (weakExprToCoreExpr q)
255 Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) :=
256 match coreToCoreExpr' ce with
258 | Error s => Prelude_error s
261 Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
263 | CoreNonRec v e => CoreNonRec v (coreToCoreExpr e)
264 | CoreRec lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
267 Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
268 map coreToCoreBind lbinds.
272 Definition coqPassCoreToCore
273 (hetmet_brak : CoreVar)
274 (hetmet_esc : CoreVar)
275 (uniqueSupply : UniqSupply)
276 (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
277 match coreVarToWeakVar hetmet_brak with
278 | WExprVar hetmet_brak' => match coreVarToWeakVar hetmet_esc with
279 | WExprVar hetmet_esc' => coqPassCoreToCore' hetmet_brak' hetmet_esc' uniqueSupply lbinds
280 | _ => Prelude_error "IMPOSSIBLE"
282 | _ => Prelude_error "IMPOSSIBLE"