coercions wip

src/core/dterm.ml

@@ -235,6 +235,10 @@ let dty_unify_app ls unify (l1: 'a list) (l2: dty list) =
   try List.iter2 unify l1 l2 with Invalid_argument _ ->
     raise (BadArity (ls, List.length l1))
 
+let dty_unify_app_map ls unify (l1: 'a list) (l2: dty list) =
+  try List.map2 unify l1 l2 with Invalid_argument _ ->
+    raise (BadArity (ls, List.length l1))
+
 let dpat_expected_type dp dty =
   try dty_unify dp.dp_dty dty with Exit -> Loc.errorm ?loc:dp.dp_loc
     "This pattern has type %a,@ but is expected to have type %a"
@@ -259,6 +263,15 @@ let dexpr_expected_type dt dty = match dty with
   | Some dty -> dterm_expected_type dt dty
   | None -> dfmla_expected_type dt
 
+
+let ts_of_dty = function
+  | Dapp (ts, _) | Duty { ty_node = Tyapp (ts , _)} -> ts
+  | _ -> assert false (*fixme*)
+
+
+let darg_expected dt_dty dty = dty_unify dt_dty dty
+
+
 (** Constructors *)
 
 let dpattern ?loc node =
@@ -290,42 +303,80 @@ let dpattern ?loc node =
   let dty, vars = Loc.try1 ?loc get_dty node in
   { dp_node = node; dp_dty = dty; dp_vars = vars; dp_loc = loc }
 
-let dterm ?loc node =
-  let get_dty = function
+
+
+
+
+let dterm tuc ?loc node =
+let rec dterm_expected dt dty =
+    match dt.dt_dty with
+    | Some dt_dty ->
+       begin
+         try
+           dty_unify dt_dty dty; dt
+         with Exit ->
+           begin
+             match ty_of_dty false dt_dty, ty_of_dty false dty with
+             | { ty_node = Tyapp (ts1, _) }
+             , { ty_node = Tyapp (ts2, _) } ->
+                begin
+                  try
+                    let ls =
+                      Mts.find ts2 (Mts.find ts1 tuc.Theory.uc_crcmap) in
+                    dterm_node loc (DTapp (ls, [dt]))
+                  with Not_found ->
+                    Loc.errorm ?loc:dt.dt_loc
+                               "This term has type %a,@ but is expected to have type %a"
+                               print_dty dt_dty
+                               print_dty dty
+                end
+             | _  ->  Loc.errorm ?loc:dt.dt_loc
+                                 "This term has type %a,@ but is expected to have type %a"
+                                 print_dty dt_dty print_dty dty
+           end
+       end
+    | None ->
+       try
+         dty_unify dty_bool dty; dt
+       with Exit ->  Loc.error ?loc:dt.dt_loc TermExpected
+
+and dterm_node loc node =
+    let f ty = { dt_node = node; dt_dty = ty; dt_loc = loc } in
+    match node with
     | DTvar (_,dty) ->
-        Some dty
+       f (Some dty)
     | DTgvar vs ->
-        Some (dty_of_ty vs.vs_ty)
+       f (Some (dty_of_ty vs.vs_ty))
     | DTconst (Number.ConstInt _) ->
-        Some dty_int
+       f (Some dty_int)
     | DTconst (Number.ConstReal _) ->
-        Some dty_real
-    | DTapp (ls,dtl) ->
-        let dtyl, dty = specialize_ls ls in
-        dty_unify_app ls dterm_expected_type dtl dtyl;
-        dty
+       f (Some dty_real)
+    | DTapp (ls, dtl) ->
+       let dtyl, dty = specialize_ls ls in
+       { dt_node = DTapp (ls, dty_unify_app_map ls dterm_expected dtl dtyl);
+         dt_dty  = dty;
+         dt_loc  = loc }
     | DTfapp ({dt_dty = Some res} as dt1,dt2) ->
-        let rec not_arrow = function
-          | Dvar {contents = Dval dty} -> not_arrow dty
-          | Duty {ty_node = Tyapp (ts,_)}
-          | Dapp (ts,_) -> not (ts_equal ts Ty.ts_func)
-          | Dvar _ -> false | _ -> true in
-        if not_arrow res then Loc.errorm ?loc:dt1.dt_loc
-          "This term has type %a,@ it cannot be applied" print_dty res;
-        let dtyl, dty = specialize_ls fs_func_app in
-        dty_unify_app fs_func_app dterm_expected_type [dt1;dt2] dtyl;
-        dty
+       let rec not_arrow = function
+         | Dvar {contents = Dval dty} -> not_arrow dty
+         | Duty {ty_node = Tyapp (ts,_)} | Dapp (ts,_) -> not (ts_equal ts Ty.ts_func)
+         | Dvar _ -> false | _ -> true in
+       if not_arrow res then Loc.errorm ?loc:dt1.dt_loc
+                                        "This term has type %a,@ it cannot be applied" print_dty res;
+       let dtyl, dty = specialize_ls fs_func_app in
+       dty_unify_app fs_func_app dterm_expected_type [dt1;dt2] dtyl;
+       f dty
     | DTfapp ({dt_dty = None; dt_loc = loc},_) ->
-        Loc.errorm ?loc "This term has type bool,@ it cannot be applied"
+       Loc.errorm ?loc "This term has type bool,@ it cannot be applied"
     | DTif (df,dt1,dt2) ->
-        dfmla_expected_type df;
-        dexpr_expected_type dt2 dt1.dt_dty;
-        if dt2.dt_dty = None then None else dt1.dt_dty
+       dfmla_expected_type df;
+       dexpr_expected_type dt2 dt1.dt_dty;
+       if dt2.dt_dty = None then f None else f dt1.dt_dty
     | DTlet (dt,_,df) ->
-        ignore (dty_of_dterm dt);
-        df.dt_dty
+       ignore (dty_of_dterm dt);
+       f df.dt_dty
     | DTcase (_,[]) ->
-        raise EmptyCase
+       raise EmptyCase
     | DTcase (dt,(dp1,df1)::bl) ->
         dterm_expected_type dt dp1.dp_dty;
         let check (dp,df) =
@@ -333,39 +384,39 @@ let dterm ?loc node =
           dexpr_expected_type df df1.dt_dty in
         List.iter check bl;
         let is_fmla (_,df) = df.dt_dty = None in
-        if List.exists is_fmla bl then None else df1.dt_dty
+        if List.exists is_fmla bl then f None else f df1.dt_dty
     | DTeps (_,dty,df) ->
-        dfmla_expected_type df;
-        Some dty
+       dfmla_expected_type df;
+       f (Some dty)
     | DTquant (DTlambda,vl,_,df) ->
-        let res = Opt.get_def dty_bool df.dt_dty in
-        let app (_,l,_) r = Dapp (ts_func,[l;r]) in
-        Some (List.fold_right app vl res)
+       let res = Opt.get_def dty_bool df.dt_dty in
+       let app (_,l,_) r = Dapp (ts_func,[l;r]) in
+       f (Some (List.fold_right app vl res))
     | DTquant ((DTforall|DTexists),_,_,df) ->
-        dfmla_expected_type df;
-        None
+       dfmla_expected_type df;
+       f None
     | DTbinop (_,df1,df2) ->
         dfmla_expected_type df1;
         dfmla_expected_type df2;
-        None
+        f None
     | DTnot df ->
         dfmla_expected_type df;
-        None
+        f None
     | DTtrue | DTfalse ->
         (* we put here [Some dty_bool] instead of [None] because we can
            always replace [true] by [True] and [false] by [False], so that
            there is no need to count these constructs as "formulas" which
            require explicit if-then-else conversion to bool *)
-        Some dty_bool
+       f (Some dty_bool)
     | DTcast (dt,ty) ->
-        let dty = dty_of_ty ty in
-        dterm_expected_type dt dty;
-        Some dty
+       let dty = dty_of_ty ty in
+           dterm_expected dt dty
     | DTuloc (dt,_)
     | DTlabel (dt,_) ->
-        dt.dt_dty in
-  let dty = Loc.try1 ?loc get_dty node in
-  { dt_node = node; dt_dty = dty; dt_loc = loc }
+       f (dt.dt_dty)
+  in Loc.try1 ?loc (dterm_node loc) node
+
+
 
 (** Final stage *)
 

src/core/dterm.mli

@@ -99,7 +99,7 @@ val denv_get_opt : denv -> string -> dterm_node option
 
 val dpattern : ?loc:Loc.position -> dpattern_node -> dpattern
 
-val dterm : ?loc:Loc.position -> dterm_node -> dterm
+val dterm : Theory.theory_uc -> ?loc:Loc.position -> dterm_node -> dterm
 
 (** Final stage *)
 

src/parser/typing.ml

@@ -210,17 +210,17 @@ let is_reusable dt = match dt.dt_node with
   | DTapp (_,[]) -> true
   | _ -> false
 
-let mk_var n dt =
+let mk_var tuc n dt =
   let dty = match dt.dt_dty with
     | None -> dty_of_ty ty_bool
     | Some dty -> dty in
-  Dterm.dterm ?loc:dt.dt_loc (DTvar (n, dty))
+  Dterm.dterm tuc ?loc:dt.dt_loc (DTvar (n, dty))
 
-let mk_let ~loc n dt node =
-  DTlet (dt, id_user n loc, Dterm.dterm ~loc node)
+let mk_let tuc ~loc n dt node =
+  DTlet (dt, id_user n loc, Dterm.dterm tuc ~loc node)
 
-let mk_closure loc ls =
-  let mk dt = Dterm.dterm ~loc dt in
+let mk_closure tuc loc ls =
+  let mk dt = Dterm.dterm tuc ~loc dt in
   let mk_v i _ =
     Some (id_user ("y" ^ string_of_int i) loc), dty_fresh (), None in
   let mk_t (id, dty, _) = mk (DTvar ((Opt.get id).pre_name, dty)) in
@@ -230,12 +230,12 @@ let mk_closure loc ls =
 let rec dterm tuc gvars at denv {term_desc = desc; term_loc = loc} =
   let func_app e el =
     List.fold_left (fun e1 (loc, e2) ->
-      DTfapp (Dterm.dterm ~loc e1, e2)) e el
+      DTfapp (Dterm.dterm tuc ~loc e1, e2)) e el
   in
   let rec apply_ls loc ls al l el = match l, el with
     | (_::l), (e::el) -> apply_ls loc ls (e::al) l el
     | [], _ -> func_app (DTapp (ls, List.rev_map snd al)) el
-    | _, [] -> func_app (mk_closure loc ls) (List.rev_append al el)
+    | _, [] -> func_app (mk_closure tuc loc ls) (List.rev_append al el)
   in
   let qualid_app q el = match gvars at q with
     | Some v -> func_app (DTgvar v.pv_vs) el
@@ -259,7 +259,7 @@ let rec dterm tuc gvars at denv {term_desc = desc; term_loc = loc} =
     | _ ->
         func_app (DTfapp (dterm tuc gvars at denv e1, e2)) el
   in
-  Dterm.dterm ~loc (match desc with
+  Dterm.dterm tuc ~loc (match desc with
   | Ptree.Tident q ->
       qualid_app q []
   | Ptree.Tidapp (q, tl) ->
@@ -276,15 +276,15 @@ let rec dterm tuc gvars at denv {term_desc = desc; term_loc = loc} =
         if op.id_str = "infix <>" then
           let op = { op with id_str = "infix =" } in
           let ls = find_lsymbol tuc (Qident op) in
-          DTnot (Dterm.dterm ~loc (DTapp (ls, [de1;de2])))
+          DTnot (Dterm.dterm tuc ~loc (DTapp (ls, [de1;de2])))
         else
           DTapp (find_lsymbol tuc (Qident op), [de1;de2]) in
       let rec chain loc de1 op1 = function
         | { term_desc = Ptree.Tinfix (e2, op2, e3); term_loc = loc23 } ->
             let de2 = dterm tuc gvars at denv e2 in
             let loc12 = loc_cutoff loc loc23 e2.term_loc in
-            let de12 = Dterm.dterm ~loc:loc12 (apply loc12 de1 op1 de2) in
-            let de23 = Dterm.dterm ~loc:loc23 (chain loc23 de2 op2 e3) in
+            let de12 = Dterm.dterm tuc ~loc:loc12 (apply loc12 de1 op1 de2) in
+            let de23 = Dterm.dterm tuc ~loc:loc23 (chain loc23 de2 op2 e3) in
             DTbinop (DTand, de12, de23)
         | e23 ->
             apply loc de1 op1 (dterm tuc gvars at denv e23) in
@@ -321,8 +321,8 @@ let rec dterm tuc gvars at denv {term_desc = desc; term_loc = loc} =
         | { term_desc = Ptree.Tbinop (e2, DTiff, e3); term_loc = loc23 } ->
             let de2 = dterm tuc gvars at denv e2 in
             let loc12 = loc_cutoff loc loc23 e2.term_loc in
-            let de12 = Dterm.dterm ~loc:loc12 (DTbinop (DTiff, de1, de2)) in
-            let de23 = Dterm.dterm ~loc:loc23 (chain loc23 de2 e3) in
+            let de12 = Dterm.dterm tuc ~loc:loc12 (DTbinop (DTiff, de1, de2)) in
+            let de23 = Dterm.dterm tuc ~loc:loc23 (chain loc23 de2 e3) in
             DTbinop (DTand, de12, de23)
         | { term_desc = Ptree.Tbinop (_, DTimplies, _); term_loc = loc23 } ->
             Loc.errorm ~loc:loc23 "An unparenthesized implication cannot be \
@@ -351,13 +351,13 @@ let rec dterm tuc gvars at denv {term_desc = desc; term_loc = loc} =
   | Ptree.Tupdate (e1, fl) ->
       let e1 = dterm tuc gvars at denv e1 in
       let re = is_reusable e1 in
-      let v = if re then e1 else mk_var "q " e1 in
+      let v = if re then e1 else mk_var tuc "q " e1 in
       let get_val _ pj = function
         | Some e -> dterm tuc gvars at denv e
-        | None -> Dterm.dterm ~loc (DTapp (pj,[v])) in
+        | None -> Dterm.dterm tuc ~loc (DTapp (pj,[v])) in
       let cs, fl = parse_record ~loc tuc get_val fl in
       let d = DTapp (cs, fl) in
-      if re then d else mk_let ~loc "q " e1 d
+      if re then d else mk_let tuc ~loc "q " e1 d
   | Ptree.Tat (e1, l) ->
       DTlabel (dterm tuc gvars (Some l.id_str) denv e1, Slab.empty)
   | Ptree.Tnamed (Lpos uloc, e1) ->