extending isolate

ivy/ivy_parser.py

@@ -945,6 +945,27 @@ if not (iu.get_numeric_version() <= [1,1]):
         d.lineno = get_lineno(p,2)
         p[0] = p[1]
         p[0].declare(d)
+    def p_top_opttrusted_isolate_callatom_eq_lcb_top_rcb_with_callatoms(p):
+        'top : top opttrusted ISOLATE SYMBOL optargs EQ LCB top RCB'
+        p[0] = p[1]
+        module = p[8]
+        prefargs = [Variable('V'+str(idx),pr.sort) for idx,pr in enumerate(p[4])]
+        pref = Atom(p[3],prefargs)
+    #    p[0].define((pref.rep,get_lineno(p,2)))
+        if not p[7]:
+            p[0].declare(ObjectDecl(pref))
+        vsubst = dict((pr.rep,v) for pr,v in zip(p[4],prefargs))
+        inst_mod(p[0],module,pref,{},vsubst)
+        # for decl in module.decls:
+        #     idecl = subst_prefix_atoms_ast(decl,subst,pref,module.defined)
+        #     p[0].declare(idecl)
+        stack.pop()
+        ty = TrustedIsolateDef if p[2] else IsolateDef
+        d = IsolateDecl(ty(*([Atom(p[4],p[5])] + p[7] + p[9])))
+        d.args[0].with_args = len(p[9])
+        d.lineno = get_lineno(p,2)
+        p[0] = p[1]
+        p[0].declare(d)
     def p_top_extract_callatom_eq_callatoms(p):
         'top : top EXTRACT SYMBOL optargs EQ callatoms'
         d = IsolateDecl(ExtractDef(*([Atom(p[3],p[4])] + p[6])))

test/schema1.ivy

@@ -55,18 +55,31 @@ object counting = {
             0 if B <= 0 else (cardUpTo(S,B-1)+1 if member(B-1,S) else cardUpTo(S,B-1))
 	proof rec[t]
 
-	definition succ(X:t,Y:t) = (Y-1 = X)
+	object succ_def = {
+	    definition succ(X:t,Y:t) = (Y-1 = X)
+	}
 
     }
 
     isolate iso = spec with impl
 }
 
+object successor = {
+    object spec = {
+	
+	property succ(X,Y) -> X < Y
+	property ~(X < Y & Y < Z & succ(X,Z))
+
+    }
+    object impl = {
+	interpret t -> int
+    }
+    isolate iso = spec with impl,counting.impl.succ_def
+}
+
 object disjointness = {
 
     object spec = {
-	axiom succ(X,Y) -> X < Y
-	axiom ~(X < Y & Y < Z & succ(X,Z))
 
 	relation disjoint(X:s,Y:s)
 
@@ -79,7 +92,12 @@ object disjointness = {
 	named lerr(X,Y)
 	proof lep[t]
 
-	axiom [induc] exists E. succ(E,lerr(X,Y))
+	object succ_lemma = {
+	    object spec = {
+		property [induc] exists E. succ(E,lerr(X,Y))
+	    }
+	    isolate iso = spec with counting.impl.succ_def
+	}
 
 	definition card(S) = cardUpTo(S,n)
 
@@ -88,7 +106,7 @@ object disjointness = {
 	interpret r->int
     }
 
-    isolate iso = spec with counting
+    isolate iso = spec with counting,successor
 }