Merge branch '1.0' of git+ssh://scm.gforge.inria.fr/gitroot/easycrypt…

…/easycrypt into 1.0

src/ecAlgTactic.ml

@@ -11,6 +11,12 @@ module Axioms = struct
   let tmod  = EcPath.fromqsymbol ([EcCoreLib.id_top; "AlgTactic"], "Requires")
   let tname = "domain"
 
+
+  let tmod_and_deps =
+    tmod :: [
+      EcPath.fromqsymbol ([EcCoreLib.id_top; "Ring"], "Field")
+    ]
+
   let zero  = "rzero"
   let one   = "rone"
   let add   = "add"
@@ -215,4 +221,6 @@ let t_field r eqs (f1, f2) g =
 
 (* -------------------------------------------------------------------- *)
 let is_module_loaded env =
-  EcEnv.Theory.by_path_opt Axioms.tmod env <> None
+  List.for_all
+    (fun x -> EcEnv.Theory.by_path_opt x env <> None)
+    Axioms.tmod_and_deps

src/ecAlgebra.mli

@@ -27,6 +27,7 @@ type ring = {
 }
 
 val ring_equal : ring -> ring -> bool
+
 (* -------------------------------------------------------------------- *)
 type field = {
   f_ring : ring;

src/ecCommands.ml

@@ -124,7 +124,7 @@ let rec process_type (scope : EcScope.scope) (tyd : ptydecl located) =
   let tyname = (tyd.pl_desc.pty_tyvars, tyd.pl_desc.pty_name) in
   let scope = 
     match tyd.pl_desc.pty_body with
-    | PTYD_Abstract    -> EcScope.Ty.add          scope (mk_loc tyd.pl_loc tyname)
+    | PTYD_Abstract bd -> EcScope.Ty.add          scope (mk_loc tyd.pl_loc tyname) bd
     | PTYD_Alias    bd -> EcScope.Ty.define       scope (mk_loc tyd.pl_loc tyname) bd
     | PTYD_Datatype bd -> EcScope.Ty.add_datatype scope (mk_loc tyd.pl_loc tyname) bd
     | PTYD_Record   bd -> EcScope.Ty.add_record   scope (mk_loc tyd.pl_loc tyname) bd

src/ecDecl.ml

@@ -153,6 +153,7 @@ let operator_as_fix (op : operator) =
 
 (* -------------------------------------------------------------------- *)
 type typeclass = {
+  tc_prt : EcPath.path option;
   tc_ops : (EcIdent.t * EcTypes.ty) list;
   tc_axs : (EcSymbols.symbol * EcFol.form) list;
 }

src/ecDecl.mli

@@ -95,6 +95,7 @@ type axiom = {
 
 (* -------------------------------------------------------------------- *)
 type typeclass = {
+  tc_prt : EcPath.path option;
   tc_ops : (EcIdent.t * EcTypes.ty) list;
   tc_axs : (EcSymbols.symbol * form) list;
 }

src/ecEnv.ml

@@ -755,7 +755,7 @@ module MC = struct
 
       let tsubst =
         { ty_subst_id with
-          ts_def = Mp.add mypath ([], tvar self) Mp.empty }
+            ts_def = Mp.add mypath ([], tvar self) Mp.empty }
       in
 
       let operators =
@@ -803,14 +803,6 @@ module MC = struct
     in
       mc
 
-(*
-type typeclass = {
-  tc_ops : (EcIdent.t * EcTypes.ty) list;
-  tc_axs : form list;
-}
-*)
-
-
   let import_typeclass p ax env =
     import (_up_typeclass true) (IPPath p) ax env
 
@@ -1191,7 +1183,12 @@ module TypeClass = struct
       MC.import_typeclass p obj env
 
   let rebind name tc env =
-    MC.bind_typeclass name tc env
+    let env = MC.bind_typeclass name tc env in
+      match tc.tc_prt with
+      | None -> env
+      | Some prt ->
+          let myself = EcPath.pqname (root env) name in
+            { env with env_tc = TC.Graph.add ~src:myself ~dst:prt env.env_tc }
 
   let bind name tc env =
     { (rebind name tc env) with
@@ -2550,6 +2547,26 @@ module Theory = struct
 
     | _ -> inst
 
+  (* ------------------------------------------------------------------ *)
+  let rec bind_tc_cth path gr cth =
+    List.fold_left (bind_tc_cth_item path) gr cth.cth_struct
+
+  and bind_tc_cth_item path gr item =
+    let xpath x = EcPath.pqname path x in
+
+    match item with
+    | CTh_theory (x, cth) ->
+        bind_tc_cth (xpath x) gr cth 
+
+    | CTh_typeclass (x, tc) -> begin
+        match tc.tc_prt with
+        | None     -> gr
+        | Some prt -> TC.Graph.add ~src:(xpath x) ~dst:prt gr
+    end
+
+    | _ -> gr
+
+  (* ------------------------------------------------------------------ *)
   let bind name cth env =
     let env = MC.bind_theory name cth.cth3_theory env in
     { env with
@@ -2558,7 +2575,10 @@ module Theory = struct
         env_item = (CTh_theory (name, cth.cth3_theory)) :: env.env_item; 
         env_tci  = bind_instance_cth
                      (EcPath.pqname (root env) name)
-                     env.env_tci cth.cth3_theory; }
+                     env.env_tci cth.cth3_theory;
+        env_tc   = bind_tc_cth
+                     (EcPath.pqname (root env) name)
+                     env.env_tc cth.cth3_theory; }
 
   (* ------------------------------------------------------------------ *)
   let rebind name cth env =
@@ -2651,8 +2671,9 @@ module Theory = struct
           env_comps   = comps;
           env_w3      = EcWhy3.rebind env.env_w3 cth.cth3_rebind; }
     in
-       { env with env_tci =
-           bind_instance_cth thpath env.env_tci cth.cth3_theory; }
+       { env with
+           env_tci = bind_instance_cth thpath env.env_tci cth.cth3_theory;
+           env_tc  = bind_tc_cth thpath env.env_tc cth.cth3_theory; }
 end
 
 (* -------------------------------------------------------------------- *)

src/ecHiLogic.ml

@@ -1089,6 +1089,8 @@ let process_algebra mode kind eqs g =
     in List.map eq1 eqs
   in
 
+  let tparams = (LDecl.tohyps hyps).h_tvar in
+
   let tactic =
     match
       match mode, kind with
@@ -1099,13 +1101,13 @@ let process_algebra mode kind eqs g =
     with
     | `Ring t ->
         let r =
-          match TT.get_ring ty env with
+          match TT.get_ring (tparams, ty) env with
           | None   -> tacuerror "cannot find a ring structure"
           | Some r -> r
         in t r eqs (f1, f2)
     | `Field t ->
         let r =
-          match TT.get_field ty env with
+          match TT.get_field (tparams, ty) env with
           | None   -> tacuerror "cannot find a field structure"
           | Some r -> r
         in t r eqs (f1, f2)

src/ecParser.mly

@@ -1313,7 +1313,10 @@ rec_field_def:
 
 typedecl:
 | TYPE td=rlist1(tyd_name, COMMA)
-    { List.map (mk_tydecl^~ PTYD_Abstract) td }
+    { List.map (mk_tydecl^~ (PTYD_Abstract [])) td }
+
+| TYPE td=tyd_name LTCOLON tcs=rlist1(qident, COMMA)
+    { [mk_tydecl td (PTYD_Abstract tcs)] }
 
 | TYPE td=tyd_name EQ te=loc(type_exp)
     { [mk_tydecl td (PTYD_Alias te)] }
@@ -1343,7 +1346,7 @@ tc_inth:
 
 tc_body: ops=tc_op* axs=tc_ax* { (ops, axs) };
 
-tc_op: OP x=ident COLON ty=loc(type_exp) { (x, ty) };
+tc_op: OP x=oident COLON ty=loc(type_exp) { (x, ty) };
 
 tc_ax: AXIOM x=ident COLON ax=form { (x, ax) };
 
@@ -1359,10 +1362,10 @@ tycinstance:
 ;
 
 tyci_op:
-| OP x=ident EQ tg=qoident
+| OP x=oident EQ tg=qoident
     { (x, ([], tg)) }
 
-| OP x=ident EQ tg=qoident LTCOLON tvi=plist0(loc(type_exp), COMMA) GT
+| OP x=oident EQ tg=qoident LTCOLON tvi=plist0(loc(type_exp), COMMA) GT
     { (x, (tvi, tg)) }
 ;
 

src/ecParsetree.ml

@@ -187,7 +187,7 @@ type ptydecl = {
 }
 
 and ptydbody =
-| PTYD_Abstract
+| PTYD_Abstract of pqsymbol list
 | PTYD_Alias    of pty
 | PTYD_Record   of precord
 | PTYD_Datatype of pdatatype

src/ecScope.ml

@@ -1578,13 +1578,19 @@ module Ty = struct
       scope
 
   (* ------------------------------------------------------------------ *)
-  let add (scope : scope) info =
+  let add (scope : scope) info tcs =
     assert (scope.sc_pr_uc = None);
+
     let (args, name) = info.pl_desc and loc = info.pl_loc in
+    let tcs =
+      List.map
+        (fun tc -> fst (EcEnv.TypeClass.lookup (unloc tc) scope.sc_env))
+        tcs
+    in
     let ue = TT.transtyvars scope.sc_env (loc, Some args) in
     let tydecl = {
       tyd_params = EcUnify.UniEnv.tparams ue;
-      tyd_type   = `Abstract Sp.empty;
+      tyd_type   = `Abstract (Sp.of_list tcs);
     } in
       bind scope (unloc name, tydecl)
 
@@ -1623,7 +1629,7 @@ module Ty = struct
             match EcEnv.TypeClass.lookup_opt uptc scenv with
             | None -> hierror ~loc:uploc "unknown type-class: `%s'"
                         (string_of_qsymbol uptc)
-            | Some (p, _) -> p)
+            | Some (tcp, _) -> tcp)
       in
 
       let asty  =
@@ -1643,7 +1649,9 @@ module Ty = struct
       let operators =
         let check1 (x, ty) =
           let ue = EcUnify.UniEnv.create (Some []) in
-            (EcIdent.create (unloc x), transty tp_tydecl scenv ue ty)
+          let ty = transty tp_tydecl scenv ue ty in
+          let ty = Tuni.offun (EcUnify.UniEnv.close ue) ty in
+            (EcIdent.create (unloc x), ty)
         in
           tcd.ptc_ops |> List.map check1 in
 
@@ -1652,12 +1660,14 @@ module Ty = struct
         let scenv = EcEnv.Var.bind_locals operators scenv in
         let check1 (x, ax) =
           let ue = EcUnify.UniEnv.create (Some []) in
-            (unloc x, trans_prop scenv ue ax)
+          let ax = trans_prop scenv ue ax in
+          let ax = EcFol.Fsubst.uni (EcUnify.UniEnv.close ue) ax in
+            (unloc x, ax)
         in
           tcd.ptc_axs |> List.map check1 in
 
       (* Construct actual type-class *)
-      { tc_ops = operators; tc_axs = axioms; }
+      { tc_prt = uptc; tc_ops = operators; tc_axs = axioms; }
     in
       bindclass scope (name, tclass)
 
@@ -1758,6 +1768,12 @@ module Ty = struct
             ignore (Ax.save escope pt.pl_loc))
         axs
 
+  (* ------------------------------------------------------------------ *)
+  let p_zmod    = EcPath.fromqsymbol ([EcCoreLib.id_top; "Ring"; "ZModule"], "zmodule")
+  let p_ring    = EcPath.fromqsymbol ([EcCoreLib.id_top; "Ring"; "ComRing"], "ring"   )
+  let p_idomain = EcPath.fromqsymbol ([EcCoreLib.id_top; "Ring"; "IDomain"], "idomain")
+  let p_field   = EcPath.fromqsymbol ([EcCoreLib.id_top; "Ring"; "Field"  ], "field"  )
+
   (* ------------------------------------------------------------------ *)
   let ring_of_symmap env ty boolean symbols =
     { r_type  = ty;
@@ -1780,20 +1796,24 @@ module Ty = struct
 
   let addring (scope : scope) mode (boolean, { pl_desc = tci; pl_loc = loc }) =
     if not (EcAlgTactic.is_module_loaded scope.sc_env) then
-      hierror "load AlgTactic first";
+      hierror "load AlgTactic/Ring first";
 
     let ty =
       let ue = TT.transtyvars scope.sc_env (loc, Some (fst tci.pti_type)) in
       let ty = transty tp_tydecl scope.sc_env ue (snd tci.pti_type) in
         assert (EcUnify.UniEnv.closed ue);
-        (EcUnify.UniEnv.tparams ue, ty)
+        (EcUnify.UniEnv.tparams ue, Tuni.offun (EcUnify.UniEnv.close ue) ty)
     in
     let symbols = EcAlgTactic.ring_symbols scope.sc_env boolean (snd ty) in
     let symbols = check_tci_operators scope.sc_env ty tci.pti_ops symbols in
     let cr      = ring_of_symmap scope.sc_env (snd ty) boolean symbols in
     let axioms  = EcAlgTactic.ring_axioms scope.sc_env cr in
       check_tci_axioms scope mode tci.pti_axs axioms;
-      { scope with sc_env = EcEnv.Algebra.add_ring (snd ty) cr scope.sc_env }
+      { scope with sc_env =
+          List.fold_left
+            (fun env p -> EcEnv.TypeClass.add_instance ty (`General p) env)
+            (EcEnv.Algebra.add_ring (snd ty) cr scope.sc_env)
+            [p_zmod; p_ring; p_idomain] }
 
   (* ------------------------------------------------------------------ *)
   let field_of_symmap env ty symbols =
@@ -1803,20 +1823,24 @@ module Ty = struct
 
   let addfield (scope : scope) mode { pl_desc = tci; pl_loc = loc; } =
     if not (EcAlgTactic.is_module_loaded scope.sc_env) then
-      hierror "load AlgTactic first";
+      hierror "load AlgTactic/Ring first";
 
     let ty =
       let ue = TT.transtyvars scope.sc_env (loc, Some (fst tci.pti_type)) in
       let ty = transty tp_tydecl scope.sc_env ue (snd tci.pti_type) in
         assert (EcUnify.UniEnv.closed ue);
-        (EcUnify.UniEnv.tparams ue, ty)
+        (EcUnify.UniEnv.tparams ue, Tuni.offun (EcUnify.UniEnv.close ue) ty)
     in
     let symbols = EcAlgTactic.field_symbols scope.sc_env (snd ty) in
     let symbols = check_tci_operators scope.sc_env ty tci.pti_ops symbols in
     let cr      = field_of_symmap scope.sc_env (snd ty) symbols in
     let axioms  = EcAlgTactic.field_axioms scope.sc_env cr in
       check_tci_axioms scope mode tci.pti_axs axioms;
-      { scope with sc_env = EcEnv.Algebra.add_field (snd ty) cr scope.sc_env }
+      { scope with sc_env =
+          List.fold_left
+            (fun env p -> EcEnv.TypeClass.add_instance ty (`General p) env)
+            (EcEnv.Algebra.add_field (snd ty) cr scope.sc_env)
+            [p_zmod; p_ring; p_idomain; p_field] }
 
   (* ------------------------------------------------------------------ *)
   let symbols_of_tc (_env : EcEnv.env) ty (tcp, tc) =
@@ -1831,7 +1855,7 @@ module Ty = struct
       let ue = TT.transtyvars scope.sc_env (loc, Some (fst tci.pti_type)) in
       let ty = transty tp_tydecl scope.sc_env ue (snd tci.pti_type) in
         assert (EcUnify.UniEnv.closed ue);
-        (EcUnify.UniEnv.tparams ue, ty)
+        (EcUnify.UniEnv.tparams ue, Tuni.offun (EcUnify.UniEnv.close ue) ty)
     in
 
     let (tcp, tc) =
@@ -1848,6 +1872,14 @@ module Ty = struct
     { scope with
         sc_env = EcEnv.TypeClass.add_instance ty (`General tcp) scope.sc_env }
 
+(*
+          let ue = EcUnify.UniEnv.create (Some []) in
+          let ty = fst (EcUnify.UniEnv.openty ue (fst ty) None (snd ty)) in
+            try  EcUnify.hastc scope.sc_env ue ty (Sp.singleton (fst tc)); tc
+            with EcUnify.UnificationFailure _ ->
+              hierror "type must be an instance of `%s'" (EcPath.tostring (fst tc))
+*)
+
   (* ------------------------------------------------------------------ *)
   let add_instance (scope : scope) mode ({ pl_desc = tci } as toptci) =
     match unloc tci.pti_name with

src/ecScope.mli

@@ -68,7 +68,7 @@ end
 module Ty : sig
   type tydname = (ptyparams * psymbol) located
 
-  val add : scope -> tydname -> scope
+  val add : scope -> tydname -> pqsymbol list -> scope
 
   val add_class    : scope -> ptypeclass located -> scope
   val add_instance : scope -> Ax.mode -> ptycinstance located -> scope

src/ecSubst.ml

@@ -418,9 +418,10 @@ let subst_instance (s : _subst) tci =
 
 (* -------------------------------------------------------------------- *)
 let subst_type_class (s : _subst) tc =
-  let ops = List.map (snd_map s.s_ty) tc.tc_ops in
-  let axs = List.map (snd_map (subst_form s)) tc.tc_axs in
-    { tc_ops = ops; tc_axs = axs; }
+  let tc_prt = tc.tc_prt |> omap s.s_p in
+  let tc_ops = List.map (snd_map s.s_ty) tc.tc_ops in
+  let tc_axs = List.map (snd_map (subst_form s)) tc.tc_axs in
+    { tc_prt; tc_ops; tc_axs; }
 
 (* -------------------------------------------------------------------- *)
 (* SUBSTITUTION OVER THEORIES *)