Coercions (wip)

src/core/dterm.ml

@@ -303,42 +303,36 @@ 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 tuc ?loc node =
-let rec dterm_expected dt dty =
+  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
+      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
+      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

src/core/theory.ml

@@ -348,15 +348,15 @@ let known_meta kn al =
 
 
 let add_coercion crcmap m al = match al with
-  | [MAls ({ls_args = [{ ty_node = Tyapp (ty1,_) }];
-           ls_value = Some { ty_node = Tyapp (ty2,_) }} as ls)] ->
-     let crcmap1 =
-       try Mts.find ty1 crcmap
-       with Not_found -> Mts.empty in
+  | [MAls ({ls_args  = [{ ty_node = Tyapp (ty1,_) }];
+            ls_value = Some { ty_node = Tyapp (ty2,_) }} as ls)] ->
+     let crcmap1 = try Mts.find ty1 crcmap with Not_found -> Mts.empty in
      let crcmap2  = Mts.add ty2 ls crcmap1 in
      Mts.add ty1 crcmap2 crcmap
   | _ -> assert false
 
+let meta_coercion = register_meta ~desc:"coercion" "coercion" [MTlsymbol]
+
 let add_tdecl uc td = match td.td_node with
   | Decl d -> { uc with
       uc_decls = td :: uc.uc_decls;
@@ -369,10 +369,9 @@ let add_tdecl uc td = match td.td_node with
       uc_used  = Sid.union uc.uc_used (Sid.add th.th_name th.th_used) }
   | Clone (_,sm) -> known_clone uc.uc_known sm;
       { uc with uc_decls = td :: uc.uc_decls }
-  | Meta (m,al) when m.meta_name = "coercion" ->
+  | Meta (m,al) when meta_equal m meta_coercion ->
      known_meta uc.uc_known al;
-     { uc with uc_decls = td :: uc.uc_decls;
-               uc_crcmap = add_coercion uc.uc_crcmap m al  }
+     { uc with uc_crcmap = add_coercion uc.uc_crcmap m al  }
   | Meta (_,al) -> known_meta uc.uc_known al;
       { uc with uc_decls = td :: uc.uc_decls }
 
@@ -839,7 +838,6 @@ let builtin_theory =
   let uc = add_ty_decl uc ts_int in
   let uc = add_ty_decl uc ts_real in
   let uc = add_param_decl uc ps_equ in
-  let _ = register_meta ~desc:"coercion" "coercion" [MTlsymbol] in
   close_theory uc
 
 let create_theory ?(path=[]) n =