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 (*Require Import HaskStrongCategory.*)
47 Open Scope string_scope.
48 Extraction Language Haskell.
50 (*Extract Inductive vec => "([])" [ "([])" "(:)" ].*)
51 (*Extract Inductive Tree => "([])" [ "([])" "(:)" ].*)
52 (*Extract Inlined Constant map => "Prelude.map".*)
54 (* I try to reuse Haskell types mostly to get the "deriving Show" aspect *)
55 Extract Inductive option => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ].
56 Extract Inductive list => "([])" [ "([])" "(:)" ].
57 Extract Inductive string => "Prelude.String" [ "[]" "(:)" ].
58 Extract Inductive prod => "(,)" [ "(,)" ].
59 Extract Inductive sum => "Prelude.Either" [ "Prelude.Left" "Prelude.Right" ].
60 Extract Inductive sumbool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
61 Extract Inductive bool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
62 Extract Inductive unit => "()" [ "()" ].
63 Extract Inlined Constant string_dec => "(==)".
64 Extract Inlined Constant ascii_dec => "(==)".
66 (* adapted from ExtrOcamlString.v *)
67 Extract Inductive ascii => "Char" [ "you_forgot_to_patch_coq" ] "you_forgot_to_patch_coq".
68 Extract Constant zero => "'\000'".
69 Extract Constant one => "'\001'".
70 Extract Constant shift => "shiftAscii".
72 Unset Extraction Optimize.
73 Unset Extraction AutoInline.
75 Variable Name : Type. Extract Inlined Constant Name => "Name.Name".
76 Variable mkSystemName : Unique -> string -> nat -> Name.
77 Extract Inlined Constant mkSystemName =>
78 "(\u s d -> Name.mkSystemName u (OccName.mkOccName (OccName.varNameDepth (nat2int d)) s))".
79 Variable mkTyVar : Name -> Kind -> CoreVar.
80 Extract Inlined Constant mkTyVar => "(\n k -> Var.mkTyVar n (kindToCoreKind k))".
81 Variable mkCoVar : Name -> CoreType -> CoreType -> CoreVar.
82 Extract Inlined Constant mkCoVar => "(\n t1 t2 -> Var.mkCoVar n (Coercion.mkCoKind t1 t2))".
83 Variable mkExVar : Name -> CoreType -> CoreVar.
84 Extract Inlined Constant mkExVar => "Id.mkLocalId".
87 Context (ce:@CoreExpr CoreVar).
89 Definition Γ : TypeEnv := nil.
91 Definition Δ : CoercionEnv Γ := nil.
93 Definition φ : TyVarResolver Γ :=
94 fun cv => Error ("unbound tyvar: " +++ toString (cv:CoreVar)).
95 (*fun tv => error ("tried to get the representative of an unbound tyvar:" +++ (getCoreVarOccString tv)).*)
97 Definition ψ : CoVarResolver Γ Δ :=
98 fun cv => Error ("tried to get the representative of an unbound covar!" (*+++ (getTypeVarOccString cv)*)).
100 (* We need to be able to resolve unbound exprvars, but we can be sure their types will have no
101 * free tyvars in them *)
102 Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ :=
103 match coreVarToWeakVar cv with
104 | WExprVar wev => match weakTypeToTypeOfKind φ wev ★ with
105 | Error s => Prelude_error ("Error converting weakType of top-level variable "+++
106 toString cv+++": " +++ s)
109 | WTypeVar _ => Prelude_error "top-level xi got a type variable"
110 | WCoerVar _ => Prelude_error "top-level xi got a coercion variable"
114 (* core-to-string (-dcoqpass) *)
116 Definition header : string :=
117 "\documentclass[9pt]{article}"+++eol+++
118 "\usepackage{amsmath}"+++eol+++
119 "\usepackage{amssymb}"+++eol+++
120 "\usepackage{proof}"+++eol+++
121 "\usepackage{mathpartir} % http://cristal.inria.fr/~remy/latex/"+++eol+++
122 "\usepackage{trfrac} % http://www.utdallas.edu/~hamlen/trfrac.sty"+++eol+++
123 "\def\code#1#2{\Box_{#1} #2}"+++eol+++
124 "\usepackage[paperwidth=200in,centering]{geometry}"+++eol+++
125 "\usepackage[displaymath,tightpage,active]{preview}"+++eol+++
126 "\begin{document}"+++eol+++
127 "\begin{preview}"+++eol.
129 Definition footer : string :=
130 eol+++"\end{preview}"+++
131 eol+++"\end{document}"+++
135 Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string :=
136 addErrorMessage ("input CoreSyn: " +++ toString ce)
137 (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
138 coreExprToWeakExpr ce >>= fun we =>
139 addErrorMessage ("WeakExpr: " +++ toString we)
140 ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
141 ((weakTypeOfWeakExpr we) >>= fun t =>
142 (addErrorMessage ("WeakType: " +++ toString t)
143 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
144 addErrorMessage ("HaskType: " +++ toString τ)
145 ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => false) τ nil we) >>= fun e =>
146 OK (eol+++"$$"+++ toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ e))+++"$$"+++eol)
149 Definition coreToStringExpr (ce:@CoreExpr CoreVar) : string :=
150 match coreToStringExpr' ce with
152 | Error s => Prelude_error s
155 Definition coreToStringBind (binds:@CoreBind CoreVar) : string :=
157 | CoreNonRec _ e => coreToStringExpr e
158 | CoreRec lbe => fold_left (fun x y => x+++eol+++eol+++y) (map (fun x => coreToStringExpr (snd x)) lbe) ""
161 Definition coqPassCoreToString (lbinds:list (@CoreBind CoreVar)) : string :=
163 (fold_left (fun x y => x+++eol+++eol+++y) (map coreToStringBind lbinds) "")
167 (* core-to-core (-fcoqpass) *)
170 Definition mkWeakTypeVar (u:Unique)(k:Kind) : WeakTypeVar :=
171 weakTypeVar (mkTyVar (mkSystemName u "tv" O) k) k.
172 Definition mkWeakCoerVar (u:Unique)(k:Kind)(t1 t2:WeakType) : WeakCoerVar :=
173 weakCoerVar (mkCoVar (mkSystemName u "cv" O) (weakTypeToCoreType t1) (weakTypeToCoreType t2)) k t1 t2.
174 Definition mkWeakExprVar (u:Unique)(t:WeakType) : WeakExprVar :=
175 weakExprVar (mkExVar (mkSystemName u "ev" O) (weakTypeToCoreType t)) t.
177 Context (hetmet_brak : WeakExprVar).
178 Context (hetmet_esc : WeakExprVar).
179 Context (uniqueSupply : UniqSupply).
181 Definition useUniqueSupply {T}(ut:UniqM T) : ???T :=
184 f uniqueSupply >>= fun x => OK (snd x)
187 Definition larger : forall ln:list nat, { n:nat & forall n', In n' ln -> gt n n' }.
193 destruct IHln as [n pf].
194 exists (plus (S n) a).
198 fold (@In _ n' ln) in H.
203 Definition FreshNat : @FreshMonad nat.
204 refine {| FMT := fun T => nat -> prod nat T
210 set (larger tl) as q.
211 destruct q as [n' pf].
217 refine {| returnM := fun a (v:a) => _ |}.
218 intro n. exact (n,v).
221 destruct q as [n' v].
226 Definition unFresh {T} : @FreshM _ FreshNat T -> T.
234 Definition env := ★::nil.
235 Definition freshTV : HaskType env ★ := haskTyVarToType (FreshHaskTyVar _).
236 Definition idproof0 : ND Rule [] [env > nil > [] |- [freshTV--->freshTV @@ nil]].
242 eapply (RArrange _ _ _ _ (RuCanL _ _)) .
248 Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
249 addErrorMessage ("input CoreSyn: " +++ toString ce)
250 (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
251 coreExprToWeakExpr ce >>= fun we =>
252 addErrorMessage ("WeakExpr: " +++ toString we)
253 ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
254 ((weakTypeOfWeakExpr we) >>= fun t =>
255 (addErrorMessage ("WeakType: " +++ toString t)
256 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
257 addErrorMessage ("HaskType: " +++ toString τ)
258 ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
259 (let haskProof := @expr2proof _ _ _ _ _ _ e
260 in (* insert HaskProof-to-HaskProof manipulations here *)
261 (unFresh (@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof))
262 >>= fun e' => Error (@toString _ (ExprToString _ _ _ _) (projT2 e'))
265 Prelude_error (@toString _ (@ExprToString nat _ _ _ _ _ _) (projT2 e'))
271 strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
274 >>= fun q => Error (toString q)
279 Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
280 addErrorMessage ("input CoreSyn: " +++ toString ce)
281 (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
282 coreExprToWeakExpr ce >>= fun we =>
283 addErrorMessage ("WeakExpr: " +++ toString we)
284 ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
285 ((weakTypeOfWeakExpr we) >>= fun t =>
286 (addErrorMessage ("WeakType: " +++ toString t)
287 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
289 ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
291 (addErrorMessage ("HaskStrong...")
292 (let haskProof := @expr2proof _ _ _ _ _ _ e
293 in (* insert HaskProof-to-HaskProof manipulations here *)
294 OK ((@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
296 (snd e') >>= fun e'' =>
297 strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
300 OK (weakExprToCoreExpr q)
303 Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) :=
304 match coreToCoreExpr' ce with
306 | Error s => Prelude_error s
309 Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
311 | CoreNonRec v e => CoreNonRec v (coreToCoreExpr e)
312 | CoreRec lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
315 Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
316 map coreToCoreBind lbinds.
320 Definition coqPassCoreToCore
321 (hetmet_brak : CoreVar)
322 (hetmet_esc : CoreVar)
323 (uniqueSupply : UniqSupply)
324 (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
325 match coreVarToWeakVar hetmet_brak with
326 | WExprVar hetmet_brak' => match coreVarToWeakVar hetmet_esc with
327 | WExprVar hetmet_esc' => coqPassCoreToCore' hetmet_brak' hetmet_esc' uniqueSupply lbinds
328 | _ => Prelude_error "IMPOSSIBLE"
330 | _ => Prelude_error "IMPOSSIBLE"