desugar.ml (7653B)
1 open Util 2 open Node 3 module B = Builtin 4 module C = Concrete 5 module A = Abstract 6 module E = Error 7 8 let add2 (x0, y0) (x1, y1) = (x0 + x1, y0 + y1) 9 10 let rec bind_and_annot_count 11 : C.patt -> int * int 12 = fun p -> match p.data with 13 | C.PWild -> (0, 0) 14 | C.PBind _ -> (1, 0) 15 | C.PAnnot (p, _) -> add2 (bind_and_annot_count p) (0, 1) 16 | C.PVariant _ -> (0, 0) 17 | C.PTuple _ -> (0, 0) 18 | C.PUnit -> (0, 0) 19 | C.PNat _ -> (0, 0) 20 | C.PAnd (p, q) -> add2 (bind_and_annot_count p) (bind_and_annot_count q) 21 | C.POr _ -> no_impl "or patterns" 22 | C.PParen p -> bind_and_annot_count p 23 24 let array_loc 25 : 'a. 'a node array -> Loc.t 26 = function 27 | [||] -> invalid_arg "Desugar.array_loc: empty node array" 28 | nodes -> Loc.of_locs nodes.(0).loc nodes.(Array.length nodes - 1).loc 29 30 let synth_var_name 31 : string -> A.var_name 32 = fun name -> Loc.Nowhere @$ Name.Var.Of name 33 34 let synth_tag_name 35 : string -> A.tag_name 36 = fun name -> Loc.Nowhere @$ Name.Tag.Of name 37 38 let synth_term_data 39 : string -> A.term 40 = fun tag -> Loc.Nowhere @$ A.Data (synth_tag_name tag, [||]) 41 42 let synth_term_datatype_unit: A.term = 43 let ctor = Loc.Nowhere @$ [||] in 44 let ctors = Name.Tag.Map.singleton (Name.Tag.Of "0") ctor in 45 Loc.Nowhere @$ A.DataType ctors 46 47 let synth_term_var 48 : string -> int -> A.term 49 = fun name i -> Loc.Nowhere @$ A.Var (synth_var_name name, i) 50 51 let synth_case 52 : A.patt -> A.term -> A.case 53 = fun patt body -> Loc.Nowhere @$ {A.patt; A.body} 54 55 let synth_binder 56 : Plicity.t -> A.patt -> A.binder 57 = fun plicity patt -> Loc.Nowhere @$ {A.plicity; A.patt} 58 59 let synth_patt_wild: A.patt = 60 Loc.Nowhere @$ { 61 A.names = [||]; 62 A.typs = [||]; 63 A.disc = Loc.Nowhere @$ A.DWild; 64 } 65 66 let synth_patt_wild_unit: A.patt = 67 Loc.Nowhere @$ { 68 A.names = [||]; 69 A.typs = [|synth_term_datatype_unit|]; 70 A.disc = Loc.Nowhere @$ A.DWild; 71 } 72 73 let synth_patt_data 74 : string -> A.patt 75 = fun tag -> 76 Loc.Nowhere @$ { 77 A.names = [||]; 78 A.typs = [||]; 79 A.disc = Loc.Nowhere @$ A.DData { 80 tag = synth_tag_name tag; 81 subpatts = [||]; 82 }; 83 } 84 85 let binop 86 : C.binop -> string 87 = function 88 | C.LOr | C.LAnd -> 89 impossible "Desugar.binop: LOr and Land are handled specially" 90 | C.Lt -> "<" 91 | C.Le -> "<=" 92 | C.Eq -> "=" 93 | C.Ge -> ">" 94 | C.Gt -> ">" 95 | C.Ne -> "<>" 96 | C.Add -> "+" 97 | C.Sub -> "-" 98 | C.Mul -> "*" 99 | C.Div -> "/" 100 | C.Mod -> "%" 101 102 let rec term 103 : C.term -> A.term 104 = fun {loc; data = t} -> match t with 105 | C.Let (definers, body) -> 106 loc @$ A.Let (Array.map definer definers, term body) 107 | C.Seq (t, u) -> 108 let definer = Loc.Nowhere @$ { 109 A.recursive = false; 110 A.lhs = synth_patt_wild_unit; 111 A.rhs = term t; 112 } in 113 loc @$ A.Let ([|definer|], term u) 114 | C.Match (scrutinee, cases) -> 115 loc @$ A.Match (term scrutinee, Array.map case cases) 116 | C.If ({data = C.TrueCond s; _}, t, f) -> 117 loc @$ term_if (synth_patt_data "true") (term s) (term t) (term f) 118 | C.If ({data = C.PattCond (p, s); _}, t, f) -> 119 loc @$ term_if (patt p) (term s) (term t) (term f) 120 | C.Iff ({data = C.TrueCond s; _ }, t) -> 121 loc @$ term_if (synth_patt_data "true") (term s) (term t) (synth_term_data "0") 122 | C.Iff ({data = C.PattCond (p, s); _}, t) -> 123 loc @$ term_if (patt p) (term s) (term t) (synth_term_data "0") 124 | C.Annot (t, u) -> loc @$ A.Annot (term t, term u) 125 | C.BinOp (t, C.LOr, u) -> 126 loc @$ term_if (synth_patt_data "true") (term t) (synth_term_data "true") (term u) 127 | C.BinOp (t, C.LAnd, u) -> 128 loc @$ term_if (synth_patt_data "true") (term t) (term u) (synth_term_data "false") 129 | C.BinOp (t, o, u) -> 130 loc @$ A.App (synth_term_var (binop o) 0, [|term t; term u|]) 131 | C.App (fn, args) -> loc @$ A.App (term fn, Array.map term args) 132 | C.Fn (params, body) -> 133 let multibinder = 134 if Array.length params = 0 then 135 Loc.Nowhere @$ [|synth_binder Plicity.Ex synth_patt_wild_unit|] 136 else 137 array_loc params @$ Array.map param params in 138 let abstraction = loc @$ {A.multibinder; A.term = term body} in 139 loc @$ A.Fn abstraction 140 | C.FnType (doms, cod) -> 141 let multibinder = array_loc doms @$ Array.map domain doms in 142 let abstraction = loc @$ {A.multibinder; A.term = term cod} in 143 loc @$ A.FnType abstraction 144 | C.Variant (tag, fields) -> loc @$ A.Data (tag, Array.map term fields) 145 | C.VariantType ctors -> 146 let insert m {loc = ctor_loc; data = C.Ctor (tag, doms)} = 147 if Name.Tag.Map.mem tag.data m then 148 E.abort tag.loc (E.DesugarDuplicateTag tag.data) 149 else 150 let binders = ctor_loc @$ Array.map domain doms in 151 Name.Tag.Map.add tag.data binders m in 152 let ctors = Array.fold_left insert Name.Tag.Map.empty ctors in 153 loc @$ A.DataType ctors 154 | C.Tuple fields -> 155 loc @$ A.TupleData (Array.map term fields) 156 | C.TupleType doms -> 157 let tag = Name.Tag.Of (string_of_int (Array.length doms)) in 158 let binders = 159 if Array.length doms = 0 then 160 Loc.Nowhere @$ [||] 161 else 162 array_loc doms @$ Array.map domain doms in 163 loc @$ A.DataType (Name.Tag.Map.singleton tag binders) 164 | C.Unit -> loc @$ A.Data (synth_tag_name "0", [||]) 165 | C.Nat n -> loc @$ A.Nat n 166 | C.IndexedVar (x, i) -> loc @$ A.Var (x, i) 167 | C.Var x -> loc @$ A.Var (x, 0) 168 | C.Paren t -> term t 169 170 and term_if 171 : A.patt -> A.term -> A.term -> A.term -> A.term' 172 = fun p s t f -> 173 A.Match (s, [| 174 synth_case p t; 175 synth_case synth_patt_wild f; 176 |]) 177 178 and definer 179 : C.definer -> A.definer 180 = fun {loc; data = d} -> loc @$ match d with 181 | C.Definer (lhs, rhs) -> 182 {A.recursive = false; A.lhs = patt lhs; A.rhs = term rhs} 183 | C.RecDefiner (lhs, rhs) -> 184 {A.recursive = true; A.lhs = patt lhs; A.rhs = term rhs} 185 186 and case 187 : C.case -> A.case 188 = fun {loc; data = C.Case (p, t)} -> 189 loc @$ {A.patt = patt p; A.body = term t} 190 191 and param 192 : C.param -> A.binder 193 = fun {loc; data = C.Param (plicity, p)} -> 194 loc @$ {A.plicity; A.patt = patt p} 195 196 and domain 197 : C.domain -> A.binder 198 = fun {loc; data = dom} -> loc @$ match dom with 199 | C.ExplicitDomain t -> 200 let p = Loc.Nowhere @$ { 201 A.names = [||]; 202 A.typs = [|term t|]; 203 A.disc = Loc.Nowhere @$ A.DWild; 204 } in 205 {A.plicity = Plicity.Ex; A.patt = p} 206 | C.ImplicitTypeDomain p -> 207 let p = patt p in 208 let p = p.loc @$ { 209 A.names = p.data.names; 210 A.typs = Array.append [|Loc.Nowhere @$ A.Builtin B.Type|] p.data.typs; 211 A.disc = p.data.disc; 212 } in 213 {A.plicity = Plicity.Im; A.patt = p} 214 | C.AnnotDomain (plicity, p, t) -> 215 let p = patt p in 216 let p = p.loc @$ { 217 A.names = p.data.names; 218 A.typs = Array.append [|term t|] p.data.typs; 219 A.disc = p.data.disc; 220 } in 221 {A.plicity; A.patt = p} 222 223 and patt 224 : C.patt -> A.patt 225 = fun p -> 226 let (bind_count, annot_count) = bind_and_annot_count p in 227 let names = Inc_array.make bind_count in 228 let typs = Inc_array.make annot_count in 229 let disc = discriminant names typs p in 230 let names = Inc_array.to_array names in 231 let typs = Inc_array.to_array typs in 232 p.loc @$ {A.names; A.typs; A.disc} 233 234 and discriminant 235 : A.var_name Inc_array.t -> A.term Inc_array.t -> C.patt -> A.discriminant 236 = fun names typs {loc; data = p} -> match p with 237 | C.PWild -> loc @$ A.DWild 238 | C.PBind name -> 239 Inc_array.add names name; 240 loc @$ A.DWild 241 | C.PAnnot (p, typ) -> 242 Inc_array.add typs (term typ); 243 discriminant names typs p 244 | C.PVariant (tag, ps) -> loc @$ A.DData {tag; subpatts = Array.map patt ps} 245 | C.PTuple ps -> 246 let tag = synth_tag_name (string_of_int (Array.length ps)) in 247 loc @$ A.DData {tag; subpatts = Array.map patt ps} 248 | C.PUnit -> loc @$ A.DData {tag = synth_tag_name "0"; subpatts = [||]} 249 | C.PNat _ -> no_impl "nat patterns" 250 | C.PAnd (p, q) -> 251 let pdisc = discriminant names typs p in 252 let qdisc = discriminant names typs q in 253 begin match pdisc.data, qdisc.data with 254 | A.DWild, A.DWild -> loc @$ A.DWild 255 | A.DWild, A.DData _ -> qdisc 256 | A.DData _, A.DWild -> pdisc 257 | A.DData _, A.DData _ -> E.abort loc E.DesugarDataAndData 258 end 259 | C.POr _ -> no_impl "or patterns" 260 | C.PParen p -> discriminant names typs p