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 HaskFlattener.
38 Open Scope string_scope.
39 Extraction Language Haskell.
41 (*Extract Inductive vec => "([])" [ "([])" "(:)" ].*)
42 (*Extract Inductive Tree => "([])" [ "([])" "(:)" ].*)
43 (*Extract Inlined Constant map => "Prelude.map".*)
45 (* I try to reuse Haskell types mostly to get the "deriving Show" aspect *)
46 Extract Inductive option => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ].
47 Extract Inductive list => "([])" [ "([])" "(:)" ].
48 Extract Inductive string => "Prelude.String" [ "[]" "(:)" ].
49 Extract Inductive prod => "(,)" [ "(,)" ].
50 Extract Inductive sum => "Prelude.Either" [ "Prelude.Left" "Prelude.Right" ].
51 Extract Inductive sumbool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
52 Extract Inductive bool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
53 Extract Inductive unit => "()" [ "()" ].
54 Extract Inlined Constant string_dec => "(==)".
55 Extract Inlined Constant ascii_dec => "(==)".
57 Extract Inductive ascii => "Char" [ "you_forgot_to_patch_coq" ] "you_forgot_to_patch_coq".
58 Extract Constant zero => "'\000'".
59 Extract Constant one => "'\001'".
60 Extract Constant shift => "shiftAscii".
62 Unset Extraction Optimize.
63 Unset Extraction AutoInline.
65 Variable Name : Type. Extract Inlined Constant Name => "Name.Name".
66 Variable mkSystemName : Unique -> string -> nat -> Name.
67 Extract Inlined Constant mkSystemName =>
68 "(\u s d -> Name.mkSystemName u (OccName.mkOccName (OccName.varNameDepth (nat2int d)) s))".
69 Variable mkTyVar : Name -> Kind -> CoreVar.
70 Extract Inlined Constant mkTyVar => "(\n k -> Var.mkTyVar n (kindToCoreKind k))".
71 Variable mkCoVar : Name -> CoreType -> CoreType -> CoreVar.
72 Extract Inlined Constant mkCoVar => "(\n t1 t2 -> Var.mkCoVar n (Coercion.mkCoKind t1 t2))".
73 Variable mkExVar : Name -> CoreType -> CoreVar.
74 Extract Inlined Constant mkExVar => "Id.mkLocalId".
77 Context (ce:@CoreExpr CoreVar).
79 Definition Γ : TypeEnv := nil.
81 Definition Δ : CoercionEnv Γ := nil.
83 Definition φ : TyVarResolver Γ :=
84 fun cv => Error ("unbound tyvar: " +++ toString (cv:CoreVar)).
85 (*fun tv => error ("tried to get the representative of an unbound tyvar:" +++ (getCoreVarOccString tv)).*)
87 Definition ψ : CoVarResolver Γ Δ :=
88 fun cv => Error ("tried to get the representative of an unbound covar!" (*+++ (getTypeVarOccString cv)*)).
90 (* We need to be able to resolve unbound exprvars, but we can be sure their types will have no
91 * free tyvars in them *)
92 Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ :=
93 match coreVarToWeakVar cv with
94 | WExprVar wev => match weakTypeToTypeOfKind φ wev ★ with
95 | Error s => Prelude_error ("Error converting weakType of top-level variable "+++
96 toString cv+++": " +++ s)
99 | WTypeVar _ => Prelude_error "top-level xi got a type variable"
100 | WCoerVar _ => Prelude_error "top-level xi got a coercion variable"
103 Definition header : string :=
104 "\documentclass{article}"+++eol+++
105 "\usepackage{amsmath}"+++eol+++
106 "\usepackage{amssymb}"+++eol+++
107 "\usepackage{proof}"+++eol+++
108 "\usepackage{trfrac} % http://www.utdallas.edu/~hamlen/trfrac.sty"+++eol+++
109 "\def\code#1#2{\Box_{#1} #2}"+++eol+++
110 "\usepackage[paperwidth=\maxdimen,paperheight=\maxdimen]{geometry}"+++eol+++
111 "\usepackage[tightpage,active]{preview}"+++eol+++
112 "\begin{document}"+++eol+++
113 "\setlength\PreviewBorder{5pt}"+++eol.
115 Definition footer : string :=
116 eol+++"\end{document}"+++
119 (* core-to-string (-dcoqpass) *)
120 Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string :=
121 addErrorMessage ("input CoreSyn: " +++ toString ce)
122 (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
123 coreExprToWeakExpr ce >>= fun we =>
124 addErrorMessage ("WeakExpr: " +++ toString we)
125 ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
126 ((weakTypeOfWeakExpr we) >>= fun t =>
127 (addErrorMessage ("WeakType: " +++ toString t)
128 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
129 addErrorMessage ("HaskType: " +++ toString τ)
130 ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => false) τ nil we) >>= fun e =>
131 OK (eol+++eol+++eol+++
132 "\begin{preview}"+++eol+++
134 toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ e))+++
136 "\end{preview}"+++eol+++eol+++eol)
139 Definition coreToStringExpr (ce:@CoreExpr CoreVar) : string :=
140 match coreToStringExpr' ce with
142 | Error s => Prelude_error s
145 Definition coreToStringBind (binds:@CoreBind CoreVar) : string :=
147 | CoreNonRec _ e => coreToStringExpr e
148 | CoreRec lbe => fold_left (fun x y => x+++eol+++eol+++y) (map (fun x => coreToStringExpr (snd x)) lbe) ""
151 Definition coqPassCoreToString (lbinds:list (@CoreBind CoreVar)) : string :=
153 (fold_left (fun x y => x+++eol+++eol+++y) (map coreToStringBind lbinds) "")
157 (* core-to-core (-fcoqpass) *)
160 Definition mkWeakTypeVar (u:Unique)(k:Kind) : WeakTypeVar :=
161 weakTypeVar (mkTyVar (mkSystemName u "tv" O) k) k.
162 Definition mkWeakCoerVar (u:Unique)(k:Kind)(t1 t2:WeakType) : WeakCoerVar :=
163 weakCoerVar (mkCoVar (mkSystemName u "cv" O) (weakTypeToCoreType t1) (weakTypeToCoreType t2)) k t1 t2.
164 Definition mkWeakExprVar (u:Unique)(t:WeakType) : WeakExprVar :=
165 weakExprVar (mkExVar (mkSystemName u "ev" O) (weakTypeToCoreType t)) t.
167 Context (hetmet_brak : WeakExprVar).
168 Context (hetmet_esc : WeakExprVar).
169 Context (uniqueSupply : UniqSupply).
171 Definition useUniqueSupply {T}(ut:UniqM T) : ???T :=
174 f uniqueSupply >>= fun x => OK (snd x)
177 Definition larger : forall ln:list nat, { n:nat & forall n', In n' ln -> gt n n' }.
183 destruct IHln as [n pf].
184 exists (plus (S n) a).
188 fold (@In _ n' ln) in H.
193 Definition FreshNat : @FreshMonad nat.
194 refine {| FMT := fun T => nat -> prod nat T
200 set (larger tl) as q.
201 destruct q as [n' pf].
207 refine {| returnM := fun a (v:a) => _ |}.
208 intro n. exact (n,v).
211 destruct q as [n' v].
216 Definition unFresh {T} : @FreshM _ FreshNat T -> T.
223 Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
224 addErrorMessage ("input CoreSyn: " +++ toString ce)
225 (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
226 coreExprToWeakExpr ce >>= fun we =>
227 addErrorMessage ("WeakExpr: " +++ toString we)
228 ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
229 ((weakTypeOfWeakExpr we) >>= fun t =>
230 (addErrorMessage ("WeakType: " +++ toString t)
231 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
233 ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
235 (addErrorMessage ("HaskStrong...")
236 (let haskProof := (*flatten_proof'*) (@expr2proof _ _ _ _ _ _ e)
237 in (* insert HaskProof-to-HaskProof manipulations here *)
238 OK ((@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
240 (snd e') >>= fun e'' =>
241 strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
244 OK (weakExprToCoreExpr q)
247 Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) :=
248 match coreToCoreExpr' ce with
250 | Error s => Prelude_error s
253 Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
255 | CoreNonRec v e => CoreNonRec v (coreToCoreExpr e)
256 | CoreRec lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
259 Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
260 map coreToCoreBind lbinds.
264 Definition coreVarToWeakExprVarOrError cv :=
265 match coreVarToWeakVar cv with
267 | _ => Prelude_error "IMPOSSIBLE"
270 Definition coqPassCoreToCore
271 (hetmet_brak : CoreVar)
272 (hetmet_esc : CoreVar)
273 (uniqueSupply : UniqSupply)
274 (lbinds:list (@CoreBind CoreVar)
275 ) : list (@CoreBind CoreVar) :=
277 (coreVarToWeakExprVarOrError hetmet_brak)
278 (coreVarToWeakExprVarOrError hetmet_esc)