1 (* need this or the Haskell extraction fails *)
2 Set Printing Width 1300000.
4 Require Import Coq.Strings.Ascii.
5 Require Import Coq.Strings.String.
6 Require Import Coq.Lists.List.
8 Require Import Preamble.
9 Require Import General.
11 Require Import NaturalDeduction.
12 Require Import NaturalDeductionToLatex.
14 Require Import HaskKinds.
15 Require Import HaskLiteralsAndTyCons.
16 Require Import HaskCoreVars.
17 Require Import HaskCoreTypes.
18 Require Import HaskCore.
19 Require Import HaskWeakVars.
20 Require Import HaskWeakTypes.
21 Require Import HaskWeak.
22 Require Import HaskStrongTypes.
23 Require Import HaskStrong.
24 Require Import HaskProof.
25 Require Import HaskCoreToWeak.
26 Require Import HaskWeakToStrong.
27 Require Import HaskStrongToProof.
28 Require Import HaskProofToStrong.
29 Require Import HaskProofToLatex.
30 Require Import HaskStrongToWeak.
31 Require Import HaskWeakToCore.
33 Open Scope string_scope.
34 Extraction Language Haskell.
36 (*Extract Inductive vec => "([])" [ "([])" "(:)" ].*)
37 (*Extract Inductive Tree => "([])" [ "([])" "(:)" ].*)
38 (*Extract Inlined Constant map => "Prelude.map".*)
40 (* I try to reuse Haskell types mostly to get the "deriving Show" aspect *)
41 Extract Inductive option => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ].
42 Extract Inductive list => "([])" [ "([])" "(:)" ].
43 Extract Inductive string => "Prelude.String" [ "[]" "(:)" ].
44 Extract Inductive prod => "(,)" [ "(,)" ].
45 Extract Inductive sum => "Prelude.Either" [ "Prelude.Left" "Prelude.Right" ].
46 Extract Inductive sumbool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
47 Extract Inductive bool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
48 Extract Inductive unit => "()" [ "()" ].
49 Extract Inlined Constant string_dec => "(==)".
50 Extract Inlined Constant ascii_dec => "(==)".
52 (* adapted from ExtrOcamlString.v *)
53 Extract Inductive ascii => "Char" [ "bin2ascii" ] "bin2ascii'".
54 Extract Constant zero => "'\000'".
55 Extract Constant one => "'\001'".
56 Extract Constant shift => "shiftAscii".
58 Unset Extraction Optimize.
59 Unset Extraction AutoInline.
61 Variable Name : Type. Extract Inlined Constant Name => "Name.Name".
62 Variable mkSystemName : Unique -> string -> nat -> Name.
63 Extract Inlined Constant mkSystemName =>
64 "(\u s d -> Name.mkSystemName u (OccName.mkOccName (OccName.varNameDepth (nat2int d)) s))".
65 Variable mkTyVar : Name -> Kind -> CoreVar.
66 Extract Inlined Constant mkTyVar => "(\n k -> Var.mkTyVar n (kindToCoreKind k))".
67 Variable mkCoVar : Name -> CoreType -> CoreType -> CoreVar.
68 Extract Inlined Constant mkCoVar => "(\n t1 t2 -> Var.mkCoVar n (Coercion.mkCoKind t1 t2))".
69 Variable mkExVar : Name -> CoreType -> CoreVar.
70 Extract Inlined Constant mkExVar => "Id.mkLocalId".
73 Context (ce:@CoreExpr CoreVar).
75 Definition Γ : TypeEnv := nil.
77 Definition Δ : CoercionEnv Γ := nil.
79 Definition φ : TyVarResolver Γ :=
80 fun cv => Error ("unbound tyvar: " +++ (cv:CoreVar)).
81 (*fun tv => error ("tried to get the representative of an unbound tyvar:" +++ (getCoreVarOccString tv)).*)
83 Definition ψ : CoVarResolver Γ Δ :=
84 fun cv => Error ("tried to get the representative of an unbound covar!" (*+++ (getTypeVarOccString cv)*)).
86 (* We need to be able to resolve unbound exprvars, but we can be sure their types will have no
87 * free tyvars in them *)
88 Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ :=
89 match coreVarToWeakVar cv with
90 | WExprVar wev => match weakTypeToTypeOfKind φ wev ★ with
91 | Error s => Prelude_error ("Error in top-level xi: " +++ s)
94 | WTypeVar _ => Prelude_error "top-level xi got a type variable"
95 | WCoerVar _ => Prelude_error "top-level xi got a coercion variable"
99 (* core-to-string (-dcoqpass) *)
101 Definition header : string :=
102 "\documentclass[9pt]{article}"+++eol+++
103 "\usepackage{amsmath}"+++eol+++
104 "\usepackage{amssymb}"+++eol+++
105 "\usepackage{proof}"+++eol+++
106 "\usepackage{mathpartir} % http://cristal.inria.fr/~remy/latex/"+++eol+++
107 "\usepackage{trfrac} % http://www.utdallas.edu/~hamlen/trfrac.sty"+++eol+++
108 "\def\code#1#2{\Box_{#1} #2}"+++eol+++
109 "\usepackage[paperwidth=200in,centering]{geometry}"+++eol+++
110 "\usepackage[displaymath,tightpage,active]{preview}"+++eol+++
111 "\begin{document}"+++eol+++
112 "\begin{preview}"+++eol.
114 Definition footer : string :=
115 eol+++"\end{preview}"+++
116 eol+++"\end{document}"+++
120 Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string :=
121 addErrorMessage ("input CoreSyn: " +++ ce)
122 (addErrorMessage ("input CoreType: " +++ coreTypeOfCoreExpr ce) (
123 coreExprToWeakExpr ce >>= fun we =>
124 addErrorMessage ("WeakExpr: " +++ we)
125 ((addErrorMessage ("CoreType of WeakExpr: " +++ coreTypeOfCoreExpr (weakExprToCoreExpr we))
126 ((weakTypeOfWeakExpr we) >>= fun t =>
127 (addErrorMessage ("WeakType: " +++ t)
128 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
129 addErrorMessage ("HaskType: " +++ τ)
130 ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
131 OK (eol+++"$$"+++ nd_ml_toLatex (@expr2proof _ _ _ _ _ _ e)+++"$$"+++eol)
134 Definition coreToStringExpr (ce:@CoreExpr CoreVar) : string :=
135 match coreToStringExpr' ce with
137 | Error s => Prelude_error s
140 Definition coreToStringBind (binds:@CoreBind CoreVar) : string :=
142 | CoreNonRec _ e => coreToStringExpr e
143 | CoreRec lbe => fold_left (fun x y => x+++eol+++eol+++y) (map (fun x => coreToStringExpr (snd x)) lbe) ""
146 Definition coqPassCoreToString (lbinds:list (@CoreBind CoreVar)) : string :=
148 (fold_left (fun x y => x+++eol+++eol+++y) (map coreToStringBind lbinds) "")
152 (* core-to-core (-fcoqpass) *)
155 Definition mkWeakTypeVar (u:Unique)(k:Kind) : WeakTypeVar :=
156 weakTypeVar (mkTyVar (mkSystemName u "tv" O) k) k.
157 Definition mkWeakCoerVar (u:Unique)(k:Kind)(t1 t2:WeakType) : WeakCoerVar :=
158 weakCoerVar (mkCoVar (mkSystemName u "cv" O) (weakTypeToCoreType t1) (weakTypeToCoreType t2)) k t1 t2.
159 Definition mkWeakExprVar (u:Unique)(t:WeakType) : WeakExprVar :=
160 weakExprVar (mkExVar (mkSystemName u "ev" O) (weakTypeToCoreType t)) t.
162 Context (hetmet_brak : WeakExprVar).
163 Context (hetmet_esc : WeakExprVar).
164 Context (uniqueSupply : UniqSupply).
166 Definition useUniqueSupply {T}(ut:UniqM T) : ???T :=
169 f uniqueSupply >>= fun x => OK (snd x)
172 Definition larger : forall ln:list nat, { n:nat & forall n', In n' ln -> gt n n' }.
178 destruct IHln as [n pf].
179 exists (plus (S n) a).
183 fold (@In _ n' ln) in H.
188 Definition FreshNat : @FreshMonad nat.
189 refine {| FMT := fun T => nat -> prod nat T
195 set (larger tl) as q.
196 destruct q as [n' pf].
202 refine {| returnM := fun a (v:a) => _ |}.
203 intro n. exact (n,v).
206 destruct q as [n' v].
211 Definition unFresh {T} : @FreshM _ FreshNat T -> T.
218 Definition env := ★::nil.
219 Definition freshTV : HaskType env ★ := haskTyVarToType (FreshHaskTyVar _).
220 Definition idproof0 : ND Rule [] [env > nil > [] |- [freshTV--->freshTV @@ nil]].
226 eapply (RURule _ _ _ _ (RuCanL _ _)) .
231 Definition TInt : HaskType nil ★.
232 assert (tyConKind' intPrimTyCon = ★).
235 unfold HaskType; intros.
239 Definition idproof1 : ND Rule [] [nil > nil > [TInt @@ nil] |- [TInt @@ nil]].
245 HaskTAll(Γ:=nil) ★ (fun TV ite tv => (TApp (TApp TArrow (TVar tv)) (TVar tv))).
247 Definition idproof : ND Rule [] [nil > nil > [] |- [idtype @@ nil]].
248 eapply nd_comp; [ idtac | eapply nd_rule ; eapply RAbsT ].
253 Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
254 addErrorMessage ("input CoreSyn: " +++ ce)
255 (addErrorMessage ("input CoreType: " +++ coreTypeOfCoreExpr ce) (
256 coreExprToWeakExpr ce >>= fun we =>
257 addErrorMessage ("WeakExpr: " +++ we)
258 ((addErrorMessage ("CoreType of WeakExpr: " +++ coreTypeOfCoreExpr (weakExprToCoreExpr we))
259 ((weakTypeOfWeakExpr we) >>= fun t =>
260 (addErrorMessage ("WeakType: " +++ t)
261 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
262 addErrorMessage ("HaskType: " +++ τ)
263 ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
264 (let haskProof := @expr2proof _ _ _ _ _ _ e
265 in (* insert HaskProof-to-HaskProof manipulations here *)
266 (unFresh (@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof))
267 >>= fun e' => Error (@toString _ (ExprToString _ _ _ _) (projT2 e'))
270 Prelude_error (@toString _ (@ExprToString nat _ _ _ _ _ _) (projT2 e'))
276 strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
279 >>= fun q => Error (toString q)
284 Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
285 addErrorMessage ("input CoreSyn: " +++ ce)
286 (addErrorMessage ("input CoreType: " +++ coreTypeOfCoreExpr ce) (
287 coreExprToWeakExpr ce >>= fun we =>
288 addErrorMessage ("WeakExpr: " +++ we)
289 ((addErrorMessage ("CoreType of WeakExpr: " +++ coreTypeOfCoreExpr (weakExprToCoreExpr we))
290 ((weakTypeOfWeakExpr we) >>= fun t =>
291 (addErrorMessage ("WeakType: " +++ t)
292 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
294 ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
296 (addErrorMessage ("HaskStrong...")
297 (let haskProof := @expr2proof _ _ _ _ _ _ e
298 in (* insert HaskProof-to-HaskProof manipulations here *)
299 OK ((@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
301 (snd e') >>= fun e'' =>
302 strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
305 OK (weakExprToCoreExpr q)
308 Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) :=
309 match coreToCoreExpr' ce with
311 | Error s => Prelude_error s
314 Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
316 | CoreNonRec v e => CoreNonRec v (coreToCoreExpr e)
317 | CoreRec lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
320 Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
321 map coreToCoreBind lbinds.
325 Definition coqPassCoreToCore
326 (hetmet_brak : CoreVar)
327 (hetmet_esc : CoreVar)
328 (uniqueSupply : UniqSupply)
329 (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
330 match coreVarToWeakVar hetmet_brak with
331 | WExprVar hetmet_brak' => match coreVarToWeakVar hetmet_esc with
332 | WExprVar hetmet_esc' => coqPassCoreToCore' hetmet_brak' hetmet_esc' uniqueSupply lbinds
333 | _ => Prelude_error "IMPOSSIBLE"
335 | _ => Prelude_error "IMPOSSIBLE"
339 (*Set Extraction Optimize.*)
340 (*Set Extraction AutoInline.*)
341 Extraction "Extraction.hs" coqPassCoreToString coqPassCoreToCore.