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 HaskProofFlattener.*)
37 (*Require Import HaskProofStratified.*)
39 Open Scope string_scope.
40 Extraction Language Haskell.
42 (*Extract Inductive vec => "([])" [ "([])" "(:)" ].*)
43 (*Extract Inductive Tree => "([])" [ "([])" "(:)" ].*)
44 (*Extract Inlined Constant map => "Prelude.map".*)
46 (* I try to reuse Haskell types mostly to get the "deriving Show" aspect *)
47 Extract Inductive option => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ].
48 Extract Inductive list => "([])" [ "([])" "(:)" ].
49 Extract Inductive string => "Prelude.String" [ "[]" "(:)" ].
50 Extract Inductive prod => "(,)" [ "(,)" ].
51 Extract Inductive sum => "Prelude.Either" [ "Prelude.Left" "Prelude.Right" ].
52 Extract Inductive sumbool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
53 Extract Inductive bool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
54 Extract Inductive unit => "()" [ "()" ].
55 Extract Inlined Constant string_dec => "(==)".
56 Extract Inlined Constant ascii_dec => "(==)".
58 Extract Inductive ascii => "Char" [ "you_forgot_to_patch_coq" ] "you_forgot_to_patch_coq".
59 Extract Constant zero => "'\000'".
60 Extract Constant one => "'\001'".
61 Extract Constant shift => "shiftAscii".
63 Unset Extraction Optimize.
64 Unset Extraction AutoInline.
66 Variable Name : Type. Extract Inlined Constant Name => "Name.Name".
67 Variable mkSystemName : Unique -> string -> nat -> Name.
68 Extract Inlined Constant mkSystemName =>
69 "(\u s d -> Name.mkSystemName u (OccName.mkOccName (OccName.varNameDepth (nat2int d)) s))".
70 Variable mkTyVar : Name -> Kind -> CoreVar.
71 Extract Inlined Constant mkTyVar => "(\n k -> Var.mkTyVar n (kindToCoreKind k))".
72 Variable mkCoVar : Name -> CoreType -> CoreType -> CoreVar.
73 Extract Inlined Constant mkCoVar => "(\n t1 t2 -> Var.mkCoVar n (Coercion.mkCoKind t1 t2))".
74 Variable mkExVar : Name -> CoreType -> CoreVar.
75 Extract Inlined Constant mkExVar => "Id.mkLocalId".
78 Context (ce:@CoreExpr CoreVar).
80 Definition Γ : TypeEnv := nil.
82 Definition Δ : CoercionEnv Γ := nil.
84 Definition φ : TyVarResolver Γ :=
85 fun cv => Error ("unbound tyvar: " +++ toString (cv:CoreVar)).
86 (*fun tv => error ("tried to get the representative of an unbound tyvar:" +++ (getCoreVarOccString tv)).*)
88 Definition ψ : CoVarResolver Γ Δ :=
89 fun cv => Error ("tried to get the representative of an unbound covar!" (*+++ (getTypeVarOccString cv)*)).
91 (* We need to be able to resolve unbound exprvars, but we can be sure their types will have no
92 * free tyvars in them *)
93 Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ :=
94 match coreVarToWeakVar cv with
95 | WExprVar wev => match weakTypeToTypeOfKind φ wev ★ with
96 | Error s => Prelude_error ("Error converting weakType of top-level variable "+++
97 toString cv+++": " +++ s)
100 | WTypeVar _ => Prelude_error "top-level xi got a type variable"
101 | WCoerVar _ => Prelude_error "top-level xi got a coercion variable"
105 Definition header : string :=
106 "\documentclass{article}"+++eol+++
107 "\usepackage{amsmath}"+++eol+++
108 "\usepackage{amssymb}"+++eol+++
109 "\usepackage{proof}"+++eol+++
110 (* "\usepackage{mathpartir} % http://cristal.inria.fr/~remy/latex/"+++eol+++*)
111 "\usepackage{trfrac} % http://www.utdallas.edu/~hamlen/trfrac.sty"+++eol+++
112 "\def\code#1#2{\Box_{#1} #2}"+++eol+++
113 "\usepackage[paperwidth=\maxdimen,paperheight=\maxdimen]{geometry}"+++eol+++
114 "\usepackage[tightpage,active]{preview}"+++eol+++
115 "\begin{document}"+++eol+++
116 "\setlength\PreviewBorder{5pt}"+++eol.
118 Definition footer : string :=
119 eol+++"\end{document}"+++
122 (* core-to-string (-dcoqpass) *)
123 Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string :=
124 addErrorMessage ("input CoreSyn: " +++ toString ce)
125 (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
126 coreExprToWeakExpr ce >>= fun we =>
127 addErrorMessage ("WeakExpr: " +++ toString we)
128 ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
129 ((weakTypeOfWeakExpr we) >>= fun t =>
130 (addErrorMessage ("WeakType: " +++ toString t)
131 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
132 addErrorMessage ("HaskType: " +++ toString τ)
133 ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => false) τ nil we) >>= fun e =>
134 OK (eol+++eol+++eol+++
135 "\begin{preview}"+++eol+++
137 toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ e))+++
139 "\end{preview}"+++eol+++eol+++eol)
142 Definition coreToStringExpr (ce:@CoreExpr CoreVar) : string :=
143 match coreToStringExpr' ce with
145 | Error s => Prelude_error s
148 Definition coreToStringBind (binds:@CoreBind CoreVar) : string :=
150 | CoreNonRec _ e => coreToStringExpr e
151 | CoreRec lbe => fold_left (fun x y => x+++eol+++eol+++y) (map (fun x => coreToStringExpr (snd x)) lbe) ""
154 Definition coqPassCoreToString (lbinds:list (@CoreBind CoreVar)) : string :=
156 (fold_left (fun x y => x+++eol+++eol+++y) (map coreToStringBind lbinds) "")
160 (* core-to-core (-fcoqpass) *)
163 Definition mkWeakTypeVar (u:Unique)(k:Kind) : WeakTypeVar :=
164 weakTypeVar (mkTyVar (mkSystemName u "tv" O) k) k.
165 Definition mkWeakCoerVar (u:Unique)(k:Kind)(t1 t2:WeakType) : WeakCoerVar :=
166 weakCoerVar (mkCoVar (mkSystemName u "cv" O) (weakTypeToCoreType t1) (weakTypeToCoreType t2)) k t1 t2.
167 Definition mkWeakExprVar (u:Unique)(t:WeakType) : WeakExprVar :=
168 weakExprVar (mkExVar (mkSystemName u "ev" O) (weakTypeToCoreType t)) t.
170 Context (hetmet_brak : WeakExprVar).
171 Context (hetmet_esc : WeakExprVar).
172 Context (uniqueSupply : UniqSupply).
174 Definition useUniqueSupply {T}(ut:UniqM T) : ???T :=
177 f uniqueSupply >>= fun x => OK (snd x)
180 Definition larger : forall ln:list nat, { n:nat & forall n', In n' ln -> gt n n' }.
186 destruct IHln as [n pf].
187 exists (plus (S n) a).
191 fold (@In _ n' ln) in H.
196 Definition FreshNat : @FreshMonad nat.
197 refine {| FMT := fun T => nat -> prod nat T
203 set (larger tl) as q.
204 destruct q as [n' pf].
210 refine {| returnM := fun a (v:a) => _ |}.
211 intro n. exact (n,v).
214 destruct q as [n' v].
219 Definition unFresh {T} : @FreshM _ FreshNat T -> T.
226 Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
227 addErrorMessage ("input CoreSyn: " +++ toString ce)
228 (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
229 coreExprToWeakExpr ce >>= fun we =>
230 addErrorMessage ("WeakExpr: " +++ toString we)
231 ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
232 ((weakTypeOfWeakExpr we) >>= fun t =>
233 (addErrorMessage ("WeakType: " +++ toString t)
234 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
236 ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
238 (addErrorMessage ("HaskStrong...")
239 (let haskProof := @expr2proof _ _ _ _ _ _ e
240 in (* insert HaskProof-to-HaskProof manipulations here *)
241 OK ((@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
243 (snd e') >>= fun e'' =>
244 strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
247 OK (weakExprToCoreExpr q)
250 Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) :=
251 match coreToCoreExpr' ce with
253 | Error s => Prelude_error s
256 Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
258 | CoreNonRec v e => CoreNonRec v (coreToCoreExpr e)
259 | CoreRec lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
262 Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
263 map coreToCoreBind lbinds.
267 Definition coqPassCoreToCore
268 (hetmet_brak : CoreVar)
269 (hetmet_esc : CoreVar)
270 (uniqueSupply : UniqSupply)
271 (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
272 match coreVarToWeakVar hetmet_brak with
273 | WExprVar hetmet_brak' => match coreVarToWeakVar hetmet_esc with
274 | WExprVar hetmet_esc' => coqPassCoreToCore' hetmet_brak' hetmet_esc' uniqueSupply lbinds
275 | _ => Prelude_error "IMPOSSIBLE"
277 | _ => Prelude_error "IMPOSSIBLE"