mlw_dty.ml 5.49 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-2012                                               *)
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
(*    Guillaume Melquiond                                                 *)
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

(* destructive types for program type inference *)

open Why3
open Ident
open Ty
open Term
open Ptree
open Mlw_ty
open Mlw_ty.T
open Mlw_expr
31
open Mlw_module
32
33
34
35

type dity = dity_desc ref

and dity_desc = {
36
  uid : int;
37
38
39
40
41
  node: dity_node;
  ity : ity Lazy.t;
}

and dity_node =
42
  | Duvar of Ptree.ident (* user type variable *)
43
44
45
46
  | Dvar
  | Dits of itysymbol * dity list
  | Dts  of tysymbol  * dity list

47
48
49
50
let unique = let r = ref 0 in fun () -> incr r; !r

let create n l = ref { uid = unique (); node = n; ity = l }

51
52
let create_user_type_variable x =
  let id = id_user x.id x.id_loc in
53
  create (Duvar x) (lazy (ity_var (create_tvsymbol id)))
54
55
56

let create_type_variable () =
  let id = id_fresh "a" in
57
  create Dvar (lazy (ity_var (create_tvsymbol id)))
58
59
60
61

let ity_of_dity d = Lazy.force !d.ity

let its_app its dl =
62
  create (Dits (its, dl)) (lazy (ity_app_fresh its (List.map ity_of_dity dl)))
63
64

let ts_app ts dl =
65
  create (Dts (ts, dl)) (lazy (ity_pur ts (List.map ity_of_dity dl)))
66
67
68
69

(* unification *)

let rec unify d1 d2 =
70
  if !d1.uid <> !d2.uid then begin
71
    begin match !d1.node, !d2.node with
72
    | Dvar, _ ->
73
        ()
74
75
    | _, Dvar ->
        d2 := !d1
76
    | Duvar s1, Duvar s2 when s1.id = s2.id ->
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
        ()
    | Dits (its1, dl1), Dits (its2, dl2) when its_equal its1 its2 ->
        if List.length dl1 <> List.length dl2 then raise Exit;
        List.iter2 unify dl1 dl2
    | Dts (ts1, dl1), Dts (ts2, dl2) when ts_equal ts1 ts2 ->
        if List.length dl1 <> List.length dl2 then raise Exit;
        List.iter2 unify dl1 dl2
    | _ ->
        raise Exit
    end;
    d1 := !d2
  end

let unify d1 d2 =
  try unify d1 d2
  with Exit -> raise (TypeMismatch (ity_of_dity d1, ity_of_dity d2))

let find_type_variable htv tv =
  try
    Htv.find htv tv
  with Not_found ->
    let dtv = create_type_variable () in
    Htv.add htv tv dtv;
    dtv

102
103
type darrow = dity list * dity

104
105
106
107
108
109
110
let rec dity_of_ity htv ity = match ity.ity_node with
  | Ityvar tv -> find_type_variable htv tv
  | Itypur (ts, ityl) -> ts_app ts (List.map (dity_of_ity htv) ityl)
  | Ityapp (its, ityl, _) -> its_app its (List.map (dity_of_ity htv) ityl)

let dity_of_vtv htv v = dity_of_ity htv v.vtv_ity

111
112
113
114
115
let specialize_vtvalue vtv =
  let htv = Htv.create 17 in
  [], dity_of_vtv htv vtv

let specialize_vtarrow vta =
116
117
118
119
120
121
122
  let htv = Htv.create 17 in
  let rec decompose args a =
    let args = dity_of_vtv htv a.vta_arg :: args in
    match a.vta_result with
    | VTvalue v -> List.rev args, dity_of_vtv htv v
    | VTarrow a1 -> decompose args a1
  in
123
  decompose [] vta
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138

let specialize_plsymbol pls =
  let htv = Htv.create 17 in
  List.map (dity_of_vtv htv) pls.pl_args, dity_of_vtv htv pls.pl_value

let dity_of_ty htv ty = dity_of_ity htv (ity_of_ty ty)

let specialize_lsymbol ls =
  let htv = Htv.create 17 in
  let ty = match ls.ls_value with
    | None -> dity_of_ity htv ity_bool
    | Some ty -> dity_of_ty htv ty
  in
  List.map (dity_of_ty htv) ls.ls_args, ty

139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
let specialize_prgsymbol = function
  | PV pv -> specialize_vtvalue pv.pv_vtv
  | PA pa -> specialize_vtarrow pa.pa_vta
  | PS ps -> specialize_vtarrow ps.ps_vta
  | PL pl -> specialize_plsymbol pl

let specialize_darrow (args, res) =
  let htv = Hashtbl.create 17 in
  let rec specialize_dity d =
    try Hashtbl.find htv !d.uid
    with Not_found ->
      let d = match !d.node with
        | Dvar -> create_type_variable ()
        | Duvar s -> create_user_type_variable s
        | Dits (its, dl) -> its_app its (List.map specialize_dity dl)
        | Dts (ts, dl) -> ts_app ts (List.map specialize_dity dl)
      in
      Hashtbl.add htv !d.uid d;
      d
  in
  List.map specialize_dity args, specialize_dity res

let match_darrow ps da =
  let rec match_arrow s vta (args, res) =
    let s, args = match args with
      | [] -> assert false
      | arg :: args ->
        let ity1 = vta.vta_arg.vtv_ity in
        let ity2 = ity_of_dity arg in
        ity_match s ity1 ity2, args
    in
    match vta.vta_result with
      | VTvalue v -> assert (args = []); ity_match s v.vtv_ity (ity_of_dity res)
      | VTarrow a -> match_arrow s a (args, res)
  in
  match_arrow ity_subst_empty ps.ps_vta da