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 HaskProofFlattener.
40 Require Import HaskProofStratified.
41 Require Import HaskProofCategory.
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 Extract Inductive ascii => "Char" [ "you_forgot_to_patch_coq" ] "you_forgot_to_patch_coq".
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: " +++ toString (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 converting weakType of top-level variable "+++
103 toString cv+++": " +++ s)
106 | WTypeVar _ => Prelude_error "top-level xi got a type variable"
107 | WCoerVar _ => Prelude_error "top-level xi got a coercion variable"
111 Definition header : string :=
112 "\documentclass[9pt]{article}"+++eol+++
113 "\usepackage{amsmath}"+++eol+++
114 "\usepackage{amssymb}"+++eol+++
115 "\usepackage{proof}"+++eol+++
116 "\usepackage{mathpartir} % http://cristal.inria.fr/~remy/latex/"+++eol+++
117 "\usepackage{trfrac} % http://www.utdallas.edu/~hamlen/trfrac.sty"+++eol+++
118 "\def\code#1#2{\Box_{#1} #2}"+++eol+++
119 "\usepackage[paperwidth=200in,centering]{geometry}"+++eol+++
120 "\usepackage[displaymath,tightpage,active]{preview}"+++eol+++
121 "\begin{document}"+++eol+++
122 "\begin{preview}"+++eol.
124 Definition footer : string :=
125 eol+++"\end{preview}"+++
126 eol+++"\end{document}"+++
129 (* core-to-string (-dcoqpass) *)
130 Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string :=
131 addErrorMessage ("input CoreSyn: " +++ toString ce)
132 (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
133 coreExprToWeakExpr ce >>= fun we =>
134 addErrorMessage ("WeakExpr: " +++ toString we)
135 ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
136 ((weakTypeOfWeakExpr we) >>= fun t =>
137 (addErrorMessage ("WeakType: " +++ toString t)
138 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
139 addErrorMessage ("HaskType: " +++ toString τ)
140 ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => false) τ nil we) >>= fun e =>
141 OK (eol+++"$$"+++ toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ e))+++"$$"+++eol)
144 Definition coreToStringExpr (ce:@CoreExpr CoreVar) : string :=
145 match coreToStringExpr' ce with
147 | Error s => Prelude_error s
150 Definition coreToStringBind (binds:@CoreBind CoreVar) : string :=
152 | CoreNonRec _ e => coreToStringExpr e
153 | CoreRec lbe => fold_left (fun x y => x+++eol+++eol+++y) (map (fun x => coreToStringExpr (snd x)) lbe) ""
156 Definition coqPassCoreToString (lbinds:list (@CoreBind CoreVar)) : string :=
158 (fold_left (fun x y => x+++eol+++eol+++y) (map coreToStringBind lbinds) "")
162 (* core-to-core (-fcoqpass) *)
165 Definition mkWeakTypeVar (u:Unique)(k:Kind) : WeakTypeVar :=
166 weakTypeVar (mkTyVar (mkSystemName u "tv" O) k) k.
167 Definition mkWeakCoerVar (u:Unique)(k:Kind)(t1 t2:WeakType) : WeakCoerVar :=
168 weakCoerVar (mkCoVar (mkSystemName u "cv" O) (weakTypeToCoreType t1) (weakTypeToCoreType t2)) k t1 t2.
169 Definition mkWeakExprVar (u:Unique)(t:WeakType) : WeakExprVar :=
170 weakExprVar (mkExVar (mkSystemName u "ev" O) (weakTypeToCoreType t)) t.
172 Context (hetmet_brak : WeakExprVar).
173 Context (hetmet_esc : WeakExprVar).
174 Context (uniqueSupply : UniqSupply).
176 Definition useUniqueSupply {T}(ut:UniqM T) : ???T :=
179 f uniqueSupply >>= fun x => OK (snd x)
182 Definition larger : forall ln:list nat, { n:nat & forall n', In n' ln -> gt n n' }.
188 destruct IHln as [n pf].
189 exists (plus (S n) a).
193 fold (@In _ n' ln) in H.
198 Definition FreshNat : @FreshMonad nat.
199 refine {| FMT := fun T => nat -> prod nat T
205 set (larger tl) as q.
206 destruct q as [n' pf].
212 refine {| returnM := fun a (v:a) => _ |}.
213 intro n. exact (n,v).
216 destruct q as [n' v].
221 Definition unFresh {T} : @FreshM _ FreshNat T -> T.
228 Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
229 addErrorMessage ("input CoreSyn: " +++ toString ce)
230 (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
231 coreExprToWeakExpr ce >>= fun we =>
232 addErrorMessage ("WeakExpr: " +++ toString we)
233 ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
234 ((weakTypeOfWeakExpr we) >>= fun t =>
235 (addErrorMessage ("WeakType: " +++ toString t)
236 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
238 ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
240 (addErrorMessage ("HaskStrong...")
241 (let haskProof := @expr2proof _ _ _ _ _ _ e
242 in (* insert HaskProof-to-HaskProof manipulations here *)
243 OK ((@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
245 (snd e') >>= fun e'' =>
246 strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
249 OK (weakExprToCoreExpr q)
252 Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) :=
253 match coreToCoreExpr' ce with
255 | Error s => Prelude_error s
258 Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
260 | CoreNonRec v e => CoreNonRec v (coreToCoreExpr e)
261 | CoreRec lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
264 Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
265 map coreToCoreBind lbinds.
269 Definition coqPassCoreToCore
270 (hetmet_brak : CoreVar)
271 (hetmet_esc : CoreVar)
272 (uniqueSupply : UniqSupply)
273 (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
274 match coreVarToWeakVar hetmet_brak with
275 | WExprVar hetmet_brak' => match coreVarToWeakVar hetmet_esc with
276 | WExprVar hetmet_esc' => coqPassCoreToCore' hetmet_brak' hetmet_esc' uniqueSupply lbinds
277 | _ => Prelude_error "IMPOSSIBLE"
279 | _ => Prelude_error "IMPOSSIBLE"